Commit 4577bfa3 authored by Arthur Azevedo de Amorim's avatar Arthur Azevedo de Amorim
Browse files

Port Coq files to Iris 3.3.0.

parent 0a42f504
...@@ -23,6 +23,8 @@ _*_.tex ...@@ -23,6 +23,8 @@ _*_.tex
*.fdb_latexmk *.fdb_latexmk
*.fls *.fls
*.vo *.vo
*.vos
*.vok
*.glob *.glob
*.v.d *.v.d
*.vio *.vio
......
...@@ -29,7 +29,7 @@ Section compatibility. ...@@ -29,7 +29,7 @@ Section compatibility.
(** * Compatibility rules for expression typing *) (** * Compatibility rules for expression typing *)
(** * Variables *) (** * Variables *)
Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A (Γ x : A)%I. Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A Γ x : A.
Proof. Proof.
iIntros (HΓx vs) "!# #HΓ /=". iIntros (HΓx vs) "!# #HΓ /=".
iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done. iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done.
...@@ -159,11 +159,11 @@ Section compatibility. ...@@ -159,11 +159,11 @@ Section compatibility.
(** * Compatibility rules for value typing *) (** * Compatibility rules for value typing *)
(** ** Base types *) (** ** Base types *)
Lemma UnitV_sem_typed : ( #() : ())%I. Lemma UnitV_sem_typed : #() : ().
Proof. by iPureIntro. Qed. Proof. by iPureIntro. Qed.
Lemma BoolV_sem_typed (b : bool) : ( #b : sem_ty_bool)%I. Lemma BoolV_sem_typed (b : bool) : #b : sem_ty_bool.
Proof. by iExists b. Qed. Proof. by iExists b. Qed.
Lemma IntV_sem_typed (n : Z) : ( #n : sem_ty_int)%I. Lemma IntV_sem_typed (n : Z) : #n : sem_ty_int.
Proof. (* FILL IN YOUR PROOF *) Admitted. Proof. (* FILL IN YOUR PROOF *) Admitted.
(** ** Products and sums *) (** ** Products and sums *)
......
...@@ -35,9 +35,9 @@ Section fundamental. ...@@ -35,9 +35,9 @@ Section fundamental.
such mutually inductive proofs, we need to make sure ourselves that the such mutually inductive proofs, we need to make sure ourselves that the
induction hypotheses is only used on smaller derivations. *) induction hypotheses is only used on smaller derivations. *)
Theorem fundamental Γ e τ ρ Theorem fundamental Γ e τ ρ
(Hty : Γ e : τ) : (interp_env Γ ρ e : τ ρ)%I (Hty : Γ e : τ) : interp_env Γ ρ e : τ ρ
with fundamental_val v τ ρ with fundamental_val v τ ρ
(Hty : v : τ) : ( v : τ ρ)%I. (Hty : v : τ) : v : τ ρ.
Proof. Proof.
- destruct Hty; simpl. - destruct Hty; simpl.
+ iApply Var_sem_typed. by apply lookup_interp_env. + iApply Var_sem_typed. by apply lookup_interp_env.
......
...@@ -291,7 +291,7 @@ Definition add_two : val := λ: "x", ...@@ -291,7 +291,7 @@ Definition add_two : val := λ: "x",
(** While this function is rather convoluted, the specification is precisely (** While this function is rather convoluted, the specification is precisely
what you would expect---it adds [2]. *) what you would expect---it adds [2]. *)
Lemma wp_add_two `{!heapG Σ} (x : Z) : Lemma wp_add_two `{!heapG Σ} (x : Z) :
WP add_two #x {{ w, w = #(2 + x) }}%I. WP add_two #x {{ w, w = #(2 + x) }}.
(** Note that this weakest precondition does not have a premise (i.e. the (** Note that this weakest precondition does not have a premise (i.e. the
lemma does not involve a magic wand [-∗] at the top-level, as we have seen in lemma does not involve a magic wand [-∗] at the top-level, as we have seen in
previous examples). We thus use the scope [%I] ([I] of "Iris") to instruct Coq previous examples). We thus use the scope [%I] ([I] of "Iris") to instruct Coq
...@@ -406,7 +406,7 @@ Definition add_two_fancy : val := λ: "x", ...@@ -406,7 +406,7 @@ Definition add_two_fancy : val := λ: "x",
!"lx". !"lx".
Lemma wp_add_two_fancy `{!heapG Σ} (x : Z) : Lemma wp_add_two_fancy `{!heapG Σ} (x : Z) :
WP add_two_fancy #x {{ w, w = #(2 + x) }}%I. WP add_two_fancy #x {{ w, w = #(2 + x) }}.
Proof. (* FILL IN YOUR PROOF *) Admitted. Proof. (* FILL IN YOUR PROOF *) Admitted.
(** * Reasoning about "unsafe" programs *) (** * Reasoning about "unsafe" programs *)
...@@ -424,7 +424,7 @@ Definition unsafe_pure : val := λ: <>, ...@@ -424,7 +424,7 @@ Definition unsafe_pure : val := λ: <>,
if: #true then #13 else #13 #37. if: #true then #13 else #13 #37.
Lemma wp_unsafe_pure `{!heapG Σ} : Lemma wp_unsafe_pure `{!heapG Σ} :
WP unsafe_pure #() {{ v, v = #13 }}%I. WP unsafe_pure #() {{ v, v = #13 }}.
Proof. Proof.
rewrite /unsafe_pure. rewrite /unsafe_pure.
wp_pures. wp_pures.
...@@ -437,5 +437,5 @@ Definition unsafe_ref : val := λ: <>, ...@@ -437,5 +437,5 @@ Definition unsafe_ref : val := λ: <>,
let: "l" := ref #0 in "l" <- #true;; !"l". let: "l" := ref #0 in "l" <- #true;; !"l".
Lemma wp_unsafe_ref `{!heapG Σ} : Lemma wp_unsafe_ref `{!heapG Σ} :
WP unsafe_ref #() {{ v, v = #true }}%I. WP unsafe_ref #() {{ v, v = #true }}.
Proof. (* FILL IN YOUR PROOF *) Admitted. Proof. (* FILL IN YOUR PROOF *) Admitted.
...@@ -6,7 +6,7 @@ Section parametricity. ...@@ -6,7 +6,7 @@ Section parametricity.
(** * The polymorphic identity function *) (** * The polymorphic identity function *)
Lemma identity_param `{!heapPreG Σ} e (v : val) σ w es σ' : Lemma identity_param `{!heapPreG Σ} e (v : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A A)%I) ( `{!heapG Σ}, e : A, A A)
rtc erased_step ([e <_> v]%E, σ) (of_val w :: es, σ') w = v. rtc erased_step ([e <_> v]%E, σ) (of_val w :: es, σ') w = v.
Proof. Proof.
intros He. intros He.
...@@ -24,20 +24,20 @@ Section parametricity. ...@@ -24,20 +24,20 @@ Section parametricity.
(** * Exercise (empty_type_param, easy) *) (** * Exercise (empty_type_param, easy) *)
Lemma empty_type_param `{!heapPreG Σ} e (v : val) σ w es σ' : Lemma empty_type_param `{!heapPreG Σ} e (v : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A)%I) ( `{!heapG Σ}, e : A, A)
rtc erased_step ([e <_>]%E, σ) (of_val w :: es, σ') rtc erased_step ([e <_>]%E, σ) (of_val w :: es, σ')
False. False.
Proof. (* FILL IN YOUR PROOF *) Admitted. Proof. (* FILL IN YOUR PROOF *) Admitted.
(** * Exercise (boolean_param, moderate) *) (** * Exercise (boolean_param, moderate) *)
Lemma boolean_param `{!heapPreG Σ} e (v1 v2 : val) σ w es σ' : Lemma boolean_param `{!heapPreG Σ} e (v1 v2 : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A A A)%I) ( `{!heapG Σ}, e : A, A A A)
rtc erased_step ([e <_> v1 v2]%E, σ) (of_val w :: es, σ') w = v1 w = v2. rtc erased_step ([e <_> v1 v2]%E, σ) (of_val w :: es, σ') w = v1 w = v2.
Proof. (* FILL IN YOUR PROOF *) Admitted. Proof. (* FILL IN YOUR PROOF *) Admitted.
(** * Exercise (nat_param, hard) *) (** * Exercise (nat_param, hard) *)
Lemma nat_param `{!heapPreG Σ} e σ w es σ' : Lemma nat_param `{!heapPreG Σ} e σ w es σ' :
( `{!heapG Σ}, ( e : A, (A A) A A)%I) ( `{!heapG Σ}, e : A, (A A) A A)
rtc erased_step ([e <_> (λ: "n", "n" + #1)%V #0]%E, σ) rtc erased_step ([e <_> (λ: "n", "n" + #1)%V #0]%E, σ)
(of_val w :: es, σ') n : nat, w = #n. (of_val w :: es, σ') n : nat, w = #n.
Proof. (* FILL IN YOUR PROOF *) Admitted. Proof. (* FILL IN YOUR PROOF *) Admitted.
...@@ -45,10 +45,10 @@ Section parametricity. ...@@ -45,10 +45,10 @@ Section parametricity.
(** * Exercise (strong_nat_param, hard) *) (** * Exercise (strong_nat_param, hard) *)
Lemma strong_nat_param `{!heapPreG Σ} e σ w es σ' (vf vz : val) φ : Lemma strong_nat_param `{!heapPreG Σ} e σ w es σ' (vf vz : val) φ :
( `{!heapG Σ}, Φ : sem_ty Σ, ( `{!heapG Σ}, Φ : sem_ty Σ,
( e : A, (A A) A A)%I ( e : A, (A A) A A)
( w, {{{ Φ w }}} vf w {{{ w', RET w'; Φ w' }}})%I ( w, {{{ Φ w }}} vf w {{{ w', RET w'; Φ w' }}})
(Φ vz)%I ( Φ vz)
( w, Φ w - ⌜φ w)%I) ( w, Φ w - ⌜φ w))
rtc erased_step ([e <_> vf vz]%E, σ) (of_val w :: es, σ') φ w. rtc erased_step ([e <_> vf vz]%E, σ) (of_val w :: es, σ') φ w.
Proof. (* FILL IN YOUR PROOF *) Admitted. Proof. (* FILL IN YOUR PROOF *) Admitted.
End parametricity. End parametricity.
...@@ -20,21 +20,21 @@ The proposition [adequate NotStuck e σ (λ v σ, φ v)] (which is defined in th ...@@ -20,21 +20,21 @@ The proposition [adequate NotStuck e σ (λ v σ, φ v)] (which is defined in th
Iris library) means that [e], starting in heap [σ] does not get stuck, and if Iris library) means that [e], starting in heap [σ] does not get stuck, and if
[e] reduces to a value [v], we have [φ v]. *) [e] reduces to a value [v], we have [φ v]. *)
Lemma sem_gen_type_safety `{!heapPreG Σ} e σ φ : Lemma sem_gen_type_safety `{!heapPreG Σ} e σ φ :
( `{!heapG Σ}, A : sem_ty Σ, ( v, A v - ⌜φ v) ( e : A)%I) ( `{!heapG Σ}, A : sem_ty Σ, ( v, A v - ⌜φ v) e : A)
adequate NotStuck e σ (λ v σ, φ v). adequate NotStuck e σ (λ v σ, φ v).
Proof. Proof.
intros Hty. apply (heap_adequacy Σ NotStuck e σ)=> // ?. intros Hty. apply (heap_adequacy Σ NotStuck e σ)=> // ?.
specialize (Hty _) as (A & HA & Hty). specialize (Hty _) as (A & HA & Hty).
iStartProof. iDestruct (Hty $! ) as "#He". iStartProof. iDestruct (Hty $! ) as "#He".
iSpecialize ("He" with "[]"); first by rewrite /env_sem_typed. iSpecialize ("He" with "[]"); first by rewrite /env_sem_typed.
rewrite subst_map_empty. iApply (wp_wand with "He"); auto. rewrite subst_map_empty. iIntros "?". iApply (wp_wand with "He"); auto.
by iIntros; iApply HA. by iIntros; iApply HA.
Qed. Qed.
(** The actual theorem for semantic type safety lemma states that semantically (** The actual theorem for semantic type safety lemma states that semantically
typed closed programs do not get stuck. It is a simple consequence of the lemma [sem_gen_type_safety] above. *) typed closed programs do not get stuck. It is a simple consequence of the lemma [sem_gen_type_safety] above. *)
Theorem sem_type_safety `{!heapPreG Σ} e σ es σ' e' : Theorem sem_type_safety `{!heapPreG Σ} e σ es σ' e' :
( `{!heapG Σ}, A, ( e : A)%I) ( `{!heapG Σ}, A, e : A)
rtc erased_step ([e], σ) (es, σ') e' es rtc erased_step ([e], σ) (es, σ') e' es
is_Some (to_val e') reducible e' σ'. is_Some (to_val e') reducible e' σ'.
Proof. Proof.
......
...@@ -90,7 +90,7 @@ Section sem_typed. ...@@ -90,7 +90,7 @@ Section sem_typed.
iIntros "#HA #HΓ". by iApply (big_sepM2_insert_2 with "[] HΓ"). iIntros "#HA #HΓ". by iApply (big_sepM2_insert_2 with "[] HΓ").
Qed. Qed.
Lemma env_sem_typed_empty : env_sem_typed . Lemma env_sem_typed_empty : env_sem_typed .
Proof. iIntros "". by rewrite /env_sem_typed. Qed. Proof. iIntros "". by rewrite /env_sem_typed. Qed.
Lemma env_sem_typed_empty_l_inv vs : env_sem_typed vs - vs = ∅⌝. Lemma env_sem_typed_empty_l_inv vs : env_sem_typed vs - vs = ∅⌝.
Proof. by iIntros "?"; iApply big_sepM2_empty_r. Qed. Proof. by iIntros "?"; iApply big_sepM2_empty_r. Qed.
......
From iris.algebra Require Import auth. From iris.algebra Require Import auth numbers.
From iris.base_logic Require Import lib.own. From iris.base_logic Require Import lib.own.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
...@@ -14,8 +14,8 @@ generic mechanism for ghost state. These resources satisfy the following laws: ...@@ -14,8 +14,8 @@ generic mechanism for ghost state. These resources satisfy the following laws:
>> >>
*) *)
Class symbolG Σ := { symbol_inG :> inG Σ (authR mnatUR) }. Class symbolG Σ := { symbol_inG :> inG Σ (authR max_natUR) }.
Definition symbolΣ : gFunctors := #[GFunctor (authR mnatUR)]. Definition symbolΣ : gFunctors := #[GFunctor (authR max_natUR)].
Instance subG_symbolΣ {Σ} : subG symbolΣ Σ symbolG Σ. Instance subG_symbolΣ {Σ} : subG symbolΣ Σ symbolG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
...@@ -23,8 +23,8 @@ Proof. solve_inG. Qed. ...@@ -23,8 +23,8 @@ Proof. solve_inG. Qed.
Section symbol_ghost. Section symbol_ghost.
Context `{!symbolG Σ}. Context `{!symbolG Σ}.
Definition counter (γ : gname) (n : nat) : iProp Σ := own γ ( (n : mnat)). Definition counter (γ : gname) (n : nat) : iProp Σ := own γ ( (MaxNat n)).
Definition symbol (γ : gname) (n : nat) : iProp Σ := own γ ( (S n : mnat)). Definition symbol (γ : gname) (n : nat) : iProp Σ := own γ ( (MaxNat (S n))).
Global Instance counter_timeless γ n : Timeless (counter γ n). Global Instance counter_timeless γ n : Timeless (counter γ n).
Proof. apply _. Qed. Proof. apply _. Qed.
...@@ -34,9 +34,9 @@ Section symbol_ghost. ...@@ -34,9 +34,9 @@ Section symbol_ghost.
Global Instance symbol_persistent γ n : Persistent (symbol γ n). Global Instance symbol_persistent γ n : Persistent (symbol γ n).
Proof. apply _. Qed. Proof. apply _. Qed.
Lemma counter_alloc n : (|==> γ, counter γ n)%I. Lemma counter_alloc n : |==> γ, counter γ n.
Proof. Proof.
iMod (own_alloc ( (n:mnat) (n:mnat))) as (γ) "[Hγ Hγf]"; iMod (own_alloc ( (MaxNat n) (MaxNat n))) as (γ) "[Hγ Hγf]";
first by apply auth_both_valid. first by apply auth_both_valid.
iExists γ. by iFrame. iExists γ. by iFrame.
Qed. Qed.
...@@ -49,14 +49,15 @@ Section symbol_ghost. ...@@ -49,14 +49,15 @@ Section symbol_ghost.
Lemma counter_inc γ n : counter γ n == counter γ (S n) symbol γ n. Lemma counter_inc γ n : counter γ n == counter γ (S n) symbol γ n.
Proof. Proof.
rewrite -own_op. rewrite -own_op.
apply own_update, auth_update_alloc, mnat_local_update. omega. apply own_update, auth_update_alloc, max_nat_local_update.
simpl. omega.
Qed. Qed.
Lemma symbol_obs γ s n : counter γ n - symbol γ s - (s < n)%nat. Lemma symbol_obs γ s n : counter γ n - symbol γ s - (s < n)%nat.
Proof. Proof.
iIntros "Hc Hs". iIntros "Hc Hs".
iDestruct (own_valid_2 with "Hc Hs") as %[?%mnat_included _]%auth_both_valid. iDestruct (own_valid_2 with "Hc Hs") as %[?%max_nat_included _]%auth_both_valid.
iPureIntro. omega. iPureIntro. simpl in *. omega.
Qed. Qed.
End symbol_ghost. End symbol_ghost.
......
...@@ -29,7 +29,7 @@ Section two_state_ghost. ...@@ -29,7 +29,7 @@ Section two_state_ghost.
Definition two_state_final (γ : gname) : iProp Σ := Definition two_state_final (γ : gname) : iProp Σ :=
own γ ( (Some ())). own γ ( (Some ())).
Lemma two_state_init : (|==> γ, two_state_auth γ false)%I. Lemma two_state_init : |==> γ, two_state_auth γ false.
Proof. iApply own_alloc. by apply auth_auth_valid. Qed. Proof. iApply own_alloc. by apply auth_auth_valid. Qed.
Lemma two_state_update γ b : Lemma two_state_update γ b :
......
...@@ -10,7 +10,7 @@ Section unsafe. ...@@ -10,7 +10,7 @@ Section unsafe.
if: #true then #13 else #13 #37. if: #true then #13 else #13 #37.
>> >>
*) *)
Lemma sem_typed_unsafe_pure : ( unsafe_pure : (() sem_ty_int))%I. Lemma sem_typed_unsafe_pure : unsafe_pure : (() sem_ty_int).
Proof. Proof.
iIntros (vs) "!# HΓ /=". iApply wp_value. iIntros (vs) "!# HΓ /=". iApply wp_value.
iIntros "!#" (? ->). wp_lam. wp_if. iIntros "!#" (? ->). wp_lam. wp_if.
...@@ -24,7 +24,7 @@ Section unsafe. ...@@ -24,7 +24,7 @@ Section unsafe.
Definition unsafe_ref : val := λ: <>, Definition unsafe_ref : val := λ: <>,
let: "l" := ref #0 in "l" <- #true;; !"l". let: "l" := ref #0 in "l" <- #true;; !"l".
>> *) >> *)
Lemma sem_typed_unsafe_ref : ( unsafe_ref : (() sem_ty_bool))%I. Lemma sem_typed_unsafe_ref : unsafe_ref : (() sem_ty_bool).
Proof. Proof.
iIntros (vs) "!# HΓ /=". iApply wp_value. iIntros (vs) "!# HΓ /=". iApply wp_value.
iIntros "!#" (? ->). wp_lam. iIntros "!#" (? ->). wp_lam.
...@@ -41,7 +41,7 @@ Section unsafe. ...@@ -41,7 +41,7 @@ Section unsafe.
(λ: <>, assert: !"l" #0)). (λ: <>, assert: !"l" #0)).
Lemma sem_typed_unsafe_ref_ne_0 : Lemma sem_typed_unsafe_ref_ne_0 :
( unsafe_ref_ne_0 : (() (sem_ty_int ()) * (() ())))%I. unsafe_ref_ne_0 : (() (sem_ty_int ()) * (() ())).
Proof. Proof.
iIntros (vs) "!# HΓ /=". iApply wp_value. iIntros (vs) "!# HΓ /=". iApply wp_value.
iIntros "!#" (? ->). iIntros "!#" (? ->).
...@@ -87,7 +87,7 @@ Section unsafe. ...@@ -87,7 +87,7 @@ Section unsafe.
λ: <>, let: "l" := ref #0 in λ: <>, "l" <- #true;; !"l". λ: <>, let: "l" := ref #0 in λ: <>, "l" <- #true;; !"l".
Lemma sem_typed_unsafe_ref_reuse `{!two_stateG Σ}: Lemma sem_typed_unsafe_ref_reuse `{!two_stateG Σ}:
( unsafe_ref_reuse : (() (() sem_ty_bool)))%I. unsafe_ref_reuse : (() (() sem_ty_bool)).
Proof. Proof.
iIntros (vs) "!# HΓ /=". iApply wp_value. iIntros (vs) "!# HΓ /=". iApply wp_value.
iIntros "!#" (? ->). wp_lam. iIntros "!#" (? ->). wp_lam.
...@@ -137,7 +137,7 @@ Section unsafe. ...@@ -137,7 +137,7 @@ Section unsafe.
Definition sem_ty_symbol (γ : gname) : sem_ty Σ := SemTy (λ w, Definition sem_ty_symbol (γ : gname) : sem_ty Σ := SemTy (λ w,
n : nat, w = #n symbol γ n)%I. n : nat, w = #n symbol γ n)%I.
Lemma sem_typed_symbol_adt Γ : (Γ symbol_adt : symbol_adt_ty)%I. Lemma sem_typed_symbol_adt Γ : Γ symbol_adt : symbol_adt_ty.
Proof. Proof.
iIntros (vs) "!# _ /=". iApply wp_value. iIntros (vs) "!# _ /=". iApply wp_value.
iIntros "!#" (v ->). wp_lam. wp_alloc l as "Hl"; wp_pures. iIntros "!#" (v ->). wp_lam. wp_alloc l as "Hl"; wp_pures.
......
...@@ -29,7 +29,7 @@ Section compatibility. ...@@ -29,7 +29,7 @@ Section compatibility.
(** * Compatibility rules for expression typing *) (** * Compatibility rules for expression typing *)
(** * Variables *) (** * Variables *)
Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A (Γ x : A)%I. Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A Γ x : A.
Proof. Proof.
iIntros (HΓx vs) "!# #HΓ /=". iIntros (HΓx vs) "!# #HΓ /=".
iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done. iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done.
...@@ -220,11 +220,11 @@ Section compatibility. ...@@ -220,11 +220,11 @@ Section compatibility.
(** * Compatibility rules for value typing *) (** * Compatibility rules for value typing *)
(** ** Base types *) (** ** Base types *)
Lemma UnitV_sem_typed : ( #() : ())%I. Lemma UnitV_sem_typed : #() : ().
Proof. by iPureIntro. Qed. Proof. by iPureIntro. Qed.
Lemma BoolV_sem_typed (b : bool) : ( #b : sem_ty_bool)%I. Lemma BoolV_sem_typed (b : bool) : #b : sem_ty_bool.
Proof. by iExists b. Qed. Proof. by iExists b. Qed.
Lemma IntV_sem_typed (n : Z) : ( #n : sem_ty_int)%I. Lemma IntV_sem_typed (n : Z) : #n : sem_ty_int.
(* REMOVE *) Proof. by iExists n. Qed. (* REMOVE *) Proof. by iExists n. Qed.
(** ** Products and sums *) (** ** Products and sums *)
......
...@@ -35,9 +35,9 @@ Section fundamental. ...@@ -35,9 +35,9 @@ Section fundamental.
such mutually inductive proofs, we need to make sure ourselves that the such mutually inductive proofs, we need to make sure ourselves that the
induction hypotheses is only used on smaller derivations. *) induction hypotheses is only used on smaller derivations. *)
Theorem fundamental Γ e τ ρ Theorem fundamental Γ e τ ρ
(Hty : Γ e : τ) : (interp_env Γ ρ e : τ ρ)%I (Hty : Γ e : τ) : interp_env Γ ρ e : τ ρ
with fundamental_val v τ ρ with fundamental_val v τ ρ
(Hty : v : τ) : ( v : τ ρ)%I. (Hty : v : τ) : v : τ ρ.
Proof. Proof.
- destruct Hty; simpl. - destruct Hty; simpl.
+ iApply Var_sem_typed. by apply lookup_interp_env. + iApply Var_sem_typed. by apply lookup_interp_env.
......
...@@ -293,7 +293,7 @@ Definition add_two : val := λ: "x", ...@@ -293,7 +293,7 @@ Definition add_two : val := λ: "x",
(** While this function is rather convoluted, the specification is precisely (** While this function is rather convoluted, the specification is precisely
what you would expect---it adds [2]. *) what you would expect---it adds [2]. *)
Lemma wp_add_two `{!heapG Σ} (x : Z) : Lemma wp_add_two `{!heapG Σ} (x : Z) :
WP add_two #x {{ w, w = #(2 + x) }}%I. WP add_two #x {{ w, w = #(2 + x) }}.
(** Note that this weakest precondition does not have a premise (i.e. the (** Note that this weakest precondition does not have a premise (i.e. the
lemma does not involve a magic wand [-∗] at the top-level, as we have seen in lemma does not involve a magic wand [-∗] at the top-level, as we have seen in
previous examples). We thus use the scope [%I] ([I] of "Iris") to instruct Coq previous examples). We thus use the scope [%I] ([I] of "Iris") to instruct Coq
...@@ -344,7 +344,7 @@ work operate both on the MoSeL proof goal and the MoSeL proof context. *) ...@@ -344,7 +344,7 @@ work operate both on the MoSeL proof goal and the MoSeL proof context. *)
iApply wp_twice. iApply wp_twice.
wp_load. wp_store. wp_load. wp_store.
wp_load. wp_store. wp_load. wp_store.
rewrite (_ : 2 = (1 + 1)) // -Z.add_assoc. rewrite Z.add_assoc (_ : (1 + 1)%Z = 2) //.
iFrame. iFrame.
auto. auto.
Qed. Qed.
...@@ -417,7 +417,7 @@ Definition add_two_fancy : val := λ: "x", ...@@ -417,7 +417,7 @@ Definition add_two_fancy : val := λ: "x",
!"lx". !"lx".
Lemma wp_add_two_fancy `{!heapG Σ} (x : Z) : Lemma wp_add_two_fancy `{!heapG Σ} (x : Z) :
WP add_two_fancy #x {{ w, w = #(2 + x) }}%I. WP add_two_fancy #x {{ w, w = #(2 + x) }}.
(* REMOVE *) Proof. (* REMOVE *) Proof.
rewrite /add_two_fancy. wp_pures. rewrite /add_two_fancy. wp_pures.
wp_alloc lf as "Hlf". wp_alloc lf as "Hlf".
...@@ -446,7 +446,7 @@ Definition unsafe_pure : val := λ: <>, ...@@ -446,7 +446,7 @@ Definition unsafe_pure : val := λ: <>,
if: #true then #13 else #13 #37. if: #true then #13 else #13 #37.
Lemma wp_unsafe_pure `{!heapG Σ} : Lemma wp_unsafe_pure `{!heapG Σ} :
WP unsafe_pure #() {{ v, v = #13 }}%I. WP unsafe_pure #() {{ v, v = #13 }}.
Proof. Proof.
rewrite /unsafe_pure. rewrite /unsafe_pure.
wp_pures. wp_pures.
...@@ -459,7 +459,7 @@ Definition unsafe_ref : val := λ: <>, ...@@ -459,7 +459,7 @@ Definition unsafe_ref : val := λ: <>,
let: "l" := ref #0 in "l" <- #true;; !"l". let: "l" := ref #0 in "l" <- #true;; !"l".
Lemma wp_unsafe_ref `{!heapG Σ} : Lemma wp_unsafe_ref `{!heapG Σ} :
WP unsafe_ref #() {{ v, v = #true }}%I. WP unsafe_ref #() {{ v, v = #true }}.
(* REMOVE *) Proof. (* REMOVE *) Proof.
rewrite /unsafe_ref. wp_pures. rewrite /unsafe_ref. wp_pures.
wp_alloc l. wp_alloc l.
......
...@@ -6,7 +6,7 @@ Section parametricity. ...@@ -6,7 +6,7 @@ Section parametricity.
(** * The polymorphic identity function *) (** * The polymorphic identity function *)
Lemma identity_param `{!heapPreG Σ} e (v : val) σ w es σ' : Lemma identity_param `{!heapPreG Σ} e (v : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A A)%I) ( `{!heapG Σ}, e : A, A A)
rtc erased_step ([e <_> v]%E, σ) (of_val w :: es, σ') w = v. rtc erased_step ([e <_> v]%E, σ) (of_val w :: es, σ') w = v.
Proof. Proof.