Commit c72fb6c1 authored by Amin Timany's avatar Amin Timany

Change notation for literals

parent ee9baa0d
...@@ -187,8 +187,8 @@ Qed. ...@@ -187,8 +187,8 @@ Qed.
Definition ctx_refines (Γ : list type) Definition ctx_refines (Γ : list type)
(e e' : expr) (τ : type) := K thp σ v, (e e' : expr) (τ : type) := K thp σ v,
typed_ctx K Γ τ [] TUnit typed_ctx K Γ τ [] TUnit
rtc step ([fill_ctx K e], ) (# v :: thp, σ) rtc step ([fill_ctx K e], ) (of_val v :: thp, σ)
thp' σ' v', rtc step ([fill_ctx K e'], ) (# v' :: thp', σ'). thp' σ' v', rtc step ([fill_ctx K e'], ) (of_val v' :: thp', σ').
Notation "Γ ⊨ e '≤ctx≤' e' : τ" := Notation "Γ ⊨ e '≤ctx≤' e' : τ" :=
(ctx_refines Γ e e' τ) (at level 74, e, e', τ at next level). (ctx_refines Γ e e' τ) (at level 74, e, e', τ at next level).
......
...@@ -3,7 +3,7 @@ From iris_logrel.F_mu_ref_conc Require Export examples.lock. ...@@ -3,7 +3,7 @@ From iris_logrel.F_mu_ref_conc Require Export examples.lock.
From iris_logrel.F_mu_ref_conc Require Import soundness_binary. From iris_logrel.F_mu_ref_conc Require Import soundness_binary.
Definition CG_increment (x : expr) : expr := Definition CG_increment (x : expr) : expr :=
Rec (Store x.[ren (+ 2)] (BinOp Add ( 1) (Load x.[ren (+ 2)]))). Rec (Store x.[ren (+ 2)] (BinOp Add (#n 1) (Load x.[ren (+ 2)]))).
Definition CG_locked_increment (x l : expr) : expr := Definition CG_locked_increment (x l : expr) : expr :=
with_lock (CG_increment x) l. with_lock (CG_increment x) l.
...@@ -18,21 +18,21 @@ Definition CG_counter_body (x l : expr) : expr := ...@@ -18,21 +18,21 @@ Definition CG_counter_body (x l : expr) : expr :=
Definition CG_counter : expr := Definition CG_counter : expr :=
App App
(Rec $ App (Rec (CG_counter_body (Var 1) (Var 3))) (Rec $ App (Rec (CG_counter_body (Var 1) (Var 3)))
(Alloc ( 0))) (Alloc (#n 0)))
newlock. newlock.
Definition FG_increment (x : expr) : expr := Definition FG_increment (x : expr) : expr :=
Rec $ App Rec $ App
(Rec $ (Rec $
(* try increment *) (* try increment *)
If (CAS x.[ren (+4)] (Var 1) (BinOp Add ( 1) (Var 1))) If (CAS x.[ren (+4)] (Var 1) (BinOp Add (#n 1) (Var 1)))
Unit (* increment succeeds we return unit *) Unit (* increment succeeds we return unit *)
(App (Var 2) (Var 3)) (* increment fails, we try again *)) (App (Var 2) (Var 3)) (* increment fails, we try again *))
(Load x.[ren (+2)]) (* read the counter *). (Load x.[ren (+2)]) (* read the counter *).
Definition FG_counter_body (x : expr) : expr := Definition FG_counter_body (x : expr) : expr :=
Pair (FG_increment x) (counter_read x). Pair (FG_increment x) (counter_read x).
Definition FG_counter : expr := Definition FG_counter : expr :=
App (Rec (FG_counter_body (Var 1))) (Alloc ( 0)). App (Rec (FG_counter_body (Var 1))) (Alloc (#n 0)).
Section CG_Counter. Section CG_Counter.
Context `{cfgSG Σ, heapIG Σ}. Context `{cfgSG Σ, heapIG Σ}.
...@@ -59,12 +59,12 @@ Section CG_Counter. ...@@ -59,12 +59,12 @@ Section CG_Counter.
Lemma steps_CG_increment E ρ j K x n: Lemma steps_CG_increment E ρ j K x n:
nclose specN E nclose specN E
spec_ctx ρ x ↦ₛ (v n) j fill K (App (CG_increment (Loc x)) Unit) spec_ctx ρ x ↦ₛ (#nv n) j fill K (App (CG_increment (Loc x)) Unit)
={E}=> j fill K (Unit) x ↦ₛ (v (S n)). ={E}=> j fill K (Unit) x ↦ₛ (#nv (S n)).
Proof. Proof.
iIntros {HNE} "[#Hspec [Hx Hj]]". unfold CG_increment. iIntros {HNE} "[#Hspec [Hx Hj]]". unfold CG_increment.
iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iPvs (step_load _ _ j (K ++ [StoreRCtx (LocV _); BinOpRCtx _ (v _)]) iPvs (step_load _ _ j (K ++ [StoreRCtx (LocV _); BinOpRCtx _ (#nv _)])
_ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto. _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
rewrite ?fill_app. simpl. rewrite ?fill_app. simpl.
iFrame "Hspec Hj"; trivial. iFrame "Hspec Hj"; trivial.
...@@ -119,9 +119,9 @@ Section CG_Counter. ...@@ -119,9 +119,9 @@ Section CG_Counter.
Lemma steps_CG_locked_increment E ρ j K x n l : Lemma steps_CG_locked_increment E ρ j K x n l :
nclose specN E nclose specN E
spec_ctx ρ x ↦ₛ (v n) l ↦ₛ (v false) spec_ctx ρ x ↦ₛ (#nv n) l ↦ₛ (#v false)
j fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit) j fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
={E}=> j fill K Unit x ↦ₛ (v S n) l ↦ₛ (v false). ={E}=> j fill K Unit x ↦ₛ (#nv S n) l ↦ₛ (#v false).
Proof. Proof.
iIntros {HNE} "[#Hspec [Hx [Hl Hj]]]". iIntros {HNE} "[#Hspec [Hx [Hl Hj]]]".
iPvs (steps_with_lock iPvs (steps_with_lock
...@@ -159,9 +159,9 @@ Section CG_Counter. ...@@ -159,9 +159,9 @@ Section CG_Counter.
Lemma steps_counter_read E ρ j K x n : Lemma steps_counter_read E ρ j K x n :
nclose specN E nclose specN E
spec_ctx ρ x ↦ₛ (v n) spec_ctx ρ x ↦ₛ (#nv n)
j fill K (App (counter_read (Loc x)) Unit) j fill K (App (counter_read (Loc x)) Unit)
={E}=> j fill K ( n) x ↦ₛ (v n). ={E}=> j fill K (#n n) x ↦ₛ (#nv n).
Proof. Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read. intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read.
iPvs (step_rec _ _ j K _ Unit with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ Unit with "[Hj]") as "Hj"; eauto.
...@@ -282,7 +282,7 @@ Section CG_Counter. ...@@ -282,7 +282,7 @@ Section CG_Counter.
iApply wp_alloc; trivial; iFrame "Hheap"; iNext; iIntros {cnt} "Hcnt /=". iApply wp_alloc; trivial; iFrame "Hheap"; iNext; iIntros {cnt} "Hcnt /=".
iPvsIntro. iPvsIntro.
(* establishing the invariant *) (* establishing the invariant *)
iAssert (( n, l ↦ₛ (v false) cnt ↦ᵢ (v n) cnt' ↦ₛ (v n) )%I) iAssert (( n, l ↦ₛ (#v false) cnt ↦ᵢ (#nv n) cnt' ↦ₛ (#nv n) )%I)
with "[Hl Hcnt Hcnt']" as "Hinv". with "[Hl Hcnt Hcnt']" as "Hinv".
{ iExists _. by iFrame. } { iExists _. by iFrame. }
iPvs (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial. iPvs (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
...@@ -332,7 +332,7 @@ Section CG_Counter. ...@@ -332,7 +332,7 @@ Section CG_Counter.
iExists UnitV; iFrame; auto. iExists UnitV; iFrame; auto.
+ (* CAS fails *) + (* CAS fails *)
(* In this case, we perform a recursive call *) (* In this case, we perform a recursive call *)
iApply (wp_cas_fail _ _ _ (v n')); simpl; trivial; iApply (wp_cas_fail _ _ _ (#nv n')); simpl; trivial;
[inversion 1; subst; auto | | iFrame "Hheap"]. solve_ndisj. [inversion 1; subst; auto | | iFrame "Hheap"]. solve_ndisj.
iIntros "{$Hcnt} > Hcnt". iPvsIntro. iIntros "{$Hcnt} > Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|]. iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
...@@ -351,7 +351,7 @@ Section CG_Counter. ...@@ -351,7 +351,7 @@ Section CG_Counter.
iApply wp_load; [|iFrame "Hheap"]. solve_ndisj. iApply wp_load; [|iFrame "Hheap"]. solve_ndisj.
iIntros "{$Hcnt} > Hcnt". iPvsIntro. iIntros "{$Hcnt} > Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|]. iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iExists (v _); eauto. iExists (#nv _); eauto.
Unshelve. solve_ndisj. Unshelve. solve_ndisj.
Qed. Qed.
End CG_Counter. End CG_Counter.
......
From iris.proofmode Require Import invariants ghost_ownership tactics. From iris.proofmode Require Import invariants ghost_ownership tactics.
From iris_logrel.F_mu_ref_conc Require Export rules_binary typing. From iris_logrel.F_mu_ref_conc Require Export rules_binary typing.
Definition newlock : expr := Alloc ( false). Definition newlock : expr := Alloc (# false).
Definition acquire : expr := Definition acquire : expr :=
Rec (If (CAS (Var 1) ( false) ( true)) (Unit) (App (Var 0) (Var 1))). Rec (If (CAS (Var 1) (# false) (# true)) (Unit) (App (Var 0) (Var 1))).
Definition release : expr := Rec (Store (Var 1) ( false)). Definition release : expr := Rec (Store (Var 1) (# false)).
Definition with_lock (e : expr) (l : expr) : expr := Definition with_lock (e : expr) (l : expr) : expr :=
Rec Rec
...@@ -79,7 +79,7 @@ Section proof. ...@@ -79,7 +79,7 @@ Section proof.
Lemma steps_newlock E ρ j K : Lemma steps_newlock E ρ j K :
nclose specN E nclose specN E
spec_ctx ρ j fill K newlock spec_ctx ρ j fill K newlock
={E}=> l, j fill K (Loc l) l ↦ₛ (v false). ={E}=> l, j fill K (Loc l) l ↦ₛ (#v false).
Proof. Proof.
iIntros {HNE} "[#Hspec Hj]". iIntros {HNE} "[#Hspec Hj]".
by iPvs (step_alloc _ _ j K with "[Hj]") as "Hj"; eauto. by iPvs (step_alloc _ _ j K with "[Hj]") as "Hj"; eauto.
...@@ -89,8 +89,8 @@ Section proof. ...@@ -89,8 +89,8 @@ Section proof.
Lemma steps_acquire E ρ j K l : Lemma steps_acquire E ρ j K l :
nclose specN E nclose specN E
spec_ctx ρ l ↦ₛ (v false) j fill K (App acquire (Loc l)) spec_ctx ρ l ↦ₛ (#v false) j fill K (App acquire (Loc l))
={E}=> j fill K Unit l ↦ₛ (v true). ={E}=> j fill K Unit l ↦ₛ (#v true).
Proof. Proof.
iIntros {HNE} "[#Hspec [Hl Hj]]". unfold acquire. iIntros {HNE} "[#Hspec [Hl Hj]]". unfold acquire.
iPvs (step_rec _ _ j K with "[Hj]") as "Hj"; eauto. done. iPvs (step_rec _ _ j K with "[Hj]") as "Hj"; eauto. done.
...@@ -110,8 +110,8 @@ Section proof. ...@@ -110,8 +110,8 @@ Section proof.
Lemma steps_release E ρ j K l b: Lemma steps_release E ρ j K l b:
nclose specN E nclose specN E
spec_ctx ρ l ↦ₛ (v b) j fill K (App release (Loc l)) spec_ctx ρ l ↦ₛ (#v b) j fill K (App release (Loc l))
={E}=> j fill K Unit l ↦ₛ (v false). ={E}=> j fill K Unit l ↦ₛ (#v false).
Proof. Proof.
iIntros {HNE} "[#Hspec [Hl Hj]]". unfold release. iIntros {HNE} "[#Hspec [Hl Hj]]". unfold release.
iPvs (step_rec _ _ j K with "[Hj]") as "Hj"; eauto; try done. iPvs (step_rec _ _ j K with "[Hj]") as "Hj"; eauto; try done.
...@@ -126,11 +126,11 @@ Section proof. ...@@ -126,11 +126,11 @@ Section proof.
Lemma steps_with_lock E ρ j K e l P Q v w: Lemma steps_with_lock E ρ j K e l P Q v w:
nclose specN E nclose specN E
( f, e.[f] = e) (* e is a closed term *) ( f, e.[f] = e) (* e is a closed term *)
( K', spec_ctx ρ P j fill K' (App e (# w)) ( K', spec_ctx ρ P j fill K' (App e (of_val w))
={E}=> j fill K' (# v) Q) ={E}=> j fill K' (of_val v) Q)
spec_ctx ρ P l ↦ₛ (v false) spec_ctx ρ P l ↦ₛ (#v false)
j fill K (App (with_lock e (Loc l)) (# w)) j fill K (App (with_lock e (Loc l)) (of_val w))
={E}=> j fill K (# v) Q l ↦ₛ (v false). ={E}=> j fill K (of_val v) Q l ↦ₛ (#v false).
Proof. Proof.
iIntros {HNE H1 H2} "[#Hspec [HP [Hl Hj]]]". iIntros {HNE H1 H2} "[#Hspec [HP [Hl Hj]]]".
iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
......
...@@ -78,7 +78,7 @@ Section CG_Stack. ...@@ -78,7 +78,7 @@ Section CG_Stack.
Lemma steps_CG_push E ρ j K st v w : Lemma steps_CG_push E ρ j K st v w :
nclose specN E nclose specN E
spec_ctx ρ st ↦ₛ v j fill K (App (CG_push (Loc st)) (# w)) spec_ctx ρ st ↦ₛ v j fill K (App (CG_push (Loc st)) (of_val w))
={E}=> j fill K Unit st ↦ₛ FoldV (InjRV (PairV w v)). ={E}=> j fill K Unit st ↦ₛ FoldV (InjRV (PairV w v)).
Proof. Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push. intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push.
...@@ -133,9 +133,9 @@ Section CG_Stack. ...@@ -133,9 +133,9 @@ Section CG_Stack.
Lemma steps_CG_locked_push E ρ j K st w v l : Lemma steps_CG_locked_push E ρ j K st w v l :
nclose specN E nclose specN E
spec_ctx ρ st ↦ₛ v l ↦ₛ (v false) spec_ctx ρ st ↦ₛ v l ↦ₛ (#v false)
j fill K (App (CG_locked_push (Loc st) (Loc l)) (# w)) j fill K (App (CG_locked_push (Loc st) (Loc l)) (of_val w))
={E}=> j fill K Unit st ↦ₛ FoldV (InjRV (PairV w v)) l ↦ₛ (v false). ={E}=> j fill K Unit st ↦ₛ FoldV (InjRV (PairV w v)) l ↦ₛ (#v false).
Proof. Proof.
intros HNE. iIntros "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_push. intros HNE. iIntros "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_push.
iPvs (steps_with_lock iPvs (steps_with_lock
...@@ -176,7 +176,7 @@ Section CG_Stack. ...@@ -176,7 +176,7 @@ Section CG_Stack.
nclose specN E nclose specN E
spec_ctx ρ st ↦ₛ FoldV (InjRV (PairV w v)) spec_ctx ρ st ↦ₛ FoldV (InjRV (PairV w v))
j fill K (App (CG_pop (Loc st)) Unit) j fill K (App (CG_pop (Loc st)) Unit)
={E}=> j fill K (InjR (# w)) st ↦ₛ v. ={E}=> j fill K (InjR (of_val w)) st ↦ₛ v.
Proof. Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop. intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop.
iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
...@@ -277,9 +277,9 @@ Section CG_Stack. ...@@ -277,9 +277,9 @@ Section CG_Stack.
Lemma steps_CG_locked_pop_suc E ρ j K st v w l : Lemma steps_CG_locked_pop_suc E ρ j K st v w l :
nclose specN E nclose specN E
spec_ctx ρ st ↦ₛ FoldV (InjRV (PairV w v)) l ↦ₛ (v false) spec_ctx ρ st ↦ₛ FoldV (InjRV (PairV w v)) l ↦ₛ (#v false)
j fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit) j fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
={E}=> j fill K (InjR (# w)) st ↦ₛ v l ↦ₛ (v false). ={E}=> j fill K (InjR (of_val w)) st ↦ₛ v l ↦ₛ (#v false).
Proof. Proof.
iIntros {HNE} "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop. iIntros {HNE} "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
iPvs (steps_with_lock _ _ j K _ _ _ _ (InjRV w) UnitV _ _ iPvs (steps_with_lock _ _ j K _ _ _ _ (InjRV w) UnitV _ _
...@@ -292,9 +292,9 @@ Section CG_Stack. ...@@ -292,9 +292,9 @@ Section CG_Stack.
Lemma steps_CG_locked_pop_fail E ρ j K st l : Lemma steps_CG_locked_pop_fail E ρ j K st l :
nclose specN E nclose specN E
spec_ctx ρ st ↦ₛ FoldV (InjLV UnitV) l ↦ₛ (v false) spec_ctx ρ st ↦ₛ FoldV (InjLV UnitV) l ↦ₛ (#v false)
j fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit) j fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
={E}=> j fill K (InjL Unit) st ↦ₛ FoldV (InjLV UnitV) l ↦ₛ (v false). ={E}=> j fill K (InjL Unit) st ↦ₛ FoldV (InjLV UnitV) l ↦ₛ (#v false).
Proof. Proof.
iIntros {HNE} "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop. iIntros {HNE} "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
iPvs (steps_with_lock _ _ j K _ _ _ _ (InjLV UnitV) UnitV _ _ iPvs (steps_with_lock _ _ j K _ _ _ _ (InjLV UnitV) UnitV _ _
...@@ -340,9 +340,9 @@ Section CG_Stack. ...@@ -340,9 +340,9 @@ Section CG_Stack.
Lemma steps_CG_snap E ρ j K st v l : Lemma steps_CG_snap E ρ j K st v l :
nclose specN E nclose specN E
spec_ctx ρ st ↦ₛ v l ↦ₛ (v false) spec_ctx ρ st ↦ₛ v l ↦ₛ (#v false)
j fill K (App (CG_snap (Loc st) (Loc l)) Unit) j fill K (App (CG_snap (Loc st) (Loc l)) Unit)
={E}=> j (fill K (# v)) st ↦ₛ v l ↦ₛ (v false). ={E}=> j (fill K (of_val v)) st ↦ₛ v l ↦ₛ (#v false).
Proof. Proof.
iIntros {HNE} "[#Hspec [Hx [Hl Hj]]]". unfold CG_snap. iIntros {HNE} "[#Hspec [Hx [Hl Hj]]]". unfold CG_snap.
iPvs (steps_with_lock _ _ j K _ _ _ _ v UnitV _ _ iPvs (steps_with_lock _ _ j K _ _ _ _ v UnitV _ _
...@@ -406,14 +406,15 @@ Section CG_Stack. ...@@ -406,14 +406,15 @@ Section CG_Stack.
Lemma steps_CG_iter E ρ j K f v w : Lemma steps_CG_iter E ρ j K f v w :
nclose specN E nclose specN E
spec_ctx ρ spec_ctx ρ
j fill K (App (CG_iter (# f)) (Fold (InjR (Pair (# w) (# v))))) j fill K (App (CG_iter (of_val f))
(Fold (InjR (Pair (of_val w) (of_val v)))))
={E}=> ={E}=>
j fill K j fill K
(App (App
(Rec (Rec
(App ((CG_iter (# f)).[ren (+2)]) (App ((CG_iter (of_val f)).[ren (+2)])
(Snd (Pair ((# w).[ren (+2)]) (# v).[ren (+2)])))) (Snd (Pair ((of_val w).[ren (+2)]) (of_val v).[ren (+2)]))))
(App (# f) (# w))). (App (of_val f) (of_val w))).
Proof. Proof.
iIntros {HNE} "[#Hspec Hj]". unfold CG_iter. iIntros {HNE} "[#Hspec Hj]". unfold CG_iter.
iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
...@@ -439,7 +440,7 @@ Section CG_Stack. ...@@ -439,7 +440,7 @@ Section CG_Stack.
Lemma steps_CG_iter_end E ρ j K f : Lemma steps_CG_iter_end E ρ j K f :
nclose specN E nclose specN E
spec_ctx ρ j fill K (App (CG_iter (# f)) (Fold (InjL Unit))) spec_ctx ρ j fill K (App (CG_iter (of_val f)) (Fold (InjL Unit)))
={E}=> j fill K Unit. ={E}=> j fill K Unit.
Proof. Proof.
iIntros {HNE} "[#Hspec Hj]". unfold CG_iter. iIntros {HNE} "[#Hspec Hj]". unfold CG_iter.
......
...@@ -76,7 +76,7 @@ Section Stack_refinement. ...@@ -76,7 +76,7 @@ Section Stack_refinement.
stk' ↦ₛ v stk' ↦ₛ v
stk ↦ᵢ (FoldV (LocV istk)) stk ↦ᵢ (FoldV (LocV istk))
StackLink τi (LocV istk, v) StackLink τi (LocV istk, v)
l ↦ₛ (v false) l ↦ₛ (#v false)
)%I) with "[Hoe Hstk Hstk' HLK Hl]" as "Hinv". )%I) with "[Hoe Hstk Hstk' HLK Hl]" as "Hinv".
{ iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl HLK". } { iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl HLK". }
iPvs (inv_alloc stackN with "[Hinv]") as "#Hinv"; trivial. iPvs (inv_alloc stackN with "[Hinv]") as "#Hinv"; trivial.
...@@ -272,9 +272,9 @@ Section Stack_refinement. ...@@ -272,9 +272,9 @@ Section Stack_refinement.
iPvs (step_rec _ _ _ _ _ _ _ _ _ with "[Hj]") as "Hj". iPvs (step_rec _ _ _ _ _ _ _ _ _ with "[Hj]") as "Hj".
{ by iFrame "Hspec Hj". } { by iFrame "Hspec Hj". }
asimpl. rewrite FG_iter_subst CG_snap_subst CG_iter_subst. asimpl. asimpl. rewrite FG_iter_subst CG_snap_subst CG_iter_subst. asimpl.
replace (FG_iter (# f1)) with (# (FG_iterV (# f1))) replace (FG_iter (of_val f1)) with (of_val (FG_iterV (of_val f1)))
by (by rewrite FG_iter_of_val). by (by rewrite FG_iter_of_val).
replace (CG_iter (# f2)) with (# (CG_iterV (# f2))) replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2)))
by (by rewrite CG_iter_of_val). by (by rewrite CG_iter_of_val).
iApply (@wp_bind _ _ _ [AppRCtx _]); iApply wp_wand_l; iApply (@wp_bind _ _ _ [AppRCtx _]); iApply wp_wand_l;
iSplitR; [iIntros {w} "Hw"; iExact "Hw"|]. iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
...@@ -344,7 +344,7 @@ Section Stack_refinement. ...@@ -344,7 +344,7 @@ Section Stack_refinement.
rewrite fill_app; simpl. subst. asimpl. rewrite fill_app; simpl. subst. asimpl.
iPvs (step_rec _ _ _ _ _ _ _ _ _ with "[Hj]") as "Hj". iPvs (step_rec _ _ _ _ _ _ _ _ _ with "[Hj]") as "Hj".
{ by iFrame "Hspec Hj". } asimpl. rewrite CG_iter_subst. asimpl. { by iFrame "Hspec Hj". } asimpl. rewrite CG_iter_subst. asimpl.
replace (CG_iter (# f2)) with (# (CG_iterV (# f2))) replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2)))
by (by rewrite CG_iter_of_val). by (by rewrite CG_iter_of_val).
iPvs (step_snd _ _ _ (K ++ [AppRCtx _]) _ _ _ _ _ _ _ with "[Hj]") iPvs (step_snd _ _ _ (K ++ [AppRCtx _]) _ _ _ _ _ _ _ with "[Hj]")
as "Hj". as "Hj".
...@@ -352,7 +352,7 @@ Section Stack_refinement. ...@@ -352,7 +352,7 @@ Section Stack_refinement.
rewrite fill_app; simpl. rewrite fill_app; simpl.
iApply wp_rec; simpl; trivial. iApply wp_rec; simpl; trivial.
iNext. rewrite FG_iter_subst. asimpl. iNext. rewrite FG_iter_subst. asimpl.
replace (FG_iter (# f1)) with (# (FG_iterV (# f1))) replace (FG_iter (of_val f1)) with (of_val (FG_iterV (of_val f1)))
by (by rewrite FG_iter_of_val). by (by rewrite FG_iter_of_val).
iApply (@wp_bind _ _ _ [AppRCtx _]); iApply (@wp_bind _ _ _ [AppRCtx _]);
iApply wp_wand_l; iSplitR; [iIntros {w''} "Hw"; iExact "Hw"|]. iApply wp_wand_l; iSplitR; [iIntros {w''} "Hw"; iExact "Hw"|].
......
...@@ -39,7 +39,7 @@ Section fundamental. ...@@ -39,7 +39,7 @@ Section fundamental.
env_PersistentP Δ env_PersistentP Δ
heapI_ctx spec_ctx ρ Γ * Δ vvs j fill K (e'.[env_subst (vvs.*2)]) heapI_ctx spec_ctx ρ Γ * Δ vvs j fill K (e'.[env_subst (vvs.*2)])
WP e.[env_subst (vvs.*1)] {{ v, v', WP e.[env_subst (vvs.*1)] {{ v, v',
j fill K (# v') interp τ Δ (v, v') }}. j fill K (of_val v') interp τ Δ (v, v') }}.
Proof. Proof.
iIntros {Hlog Δ vvs ρ j K ?} "(#Hh & #Hs & HΓ & Hj)". iIntros {Hlog Δ vvs ρ j K ?} "(#Hh & #Hs & HΓ & Hj)".
iApply (Hlog with "[HΓ] *"); iFrame; eauto. iApply (Hlog with "[HΓ] *"); iFrame; eauto.
...@@ -61,16 +61,16 @@ Section fundamental. ...@@ -61,16 +61,16 @@ Section fundamental.
value_case. iExists UnitV; eauto. value_case. iExists UnitV; eauto.
Qed. Qed.
Lemma bin_log_related_nat Γ n : Γ n log n : TNat. Lemma bin_log_related_nat Γ n : Γ #n n log #n n : TNat.
Proof. Proof.
iIntros {Δ vvs ρ ?} "#(Hh & Hs & HΓ)"; iIntros {j K} "Hj /=". iIntros {Δ vvs ρ ?} "#(Hh & Hs & HΓ)"; iIntros {j K} "Hj /=".
value_case. iExists (v _); eauto. value_case. iExists (#nv _); eauto.
Qed. Qed.
Lemma bin_log_related_bool Γ b : Γ b log b : TBool. Lemma bin_log_related_bool Γ b : Γ # b log # b : TBool.
Proof. Proof.
iIntros {Δ vvs ρ ?} "#(Hh & Hs & HΓ)"; iIntros {j K} "Hj /=". iIntros {Δ vvs ρ ?} "#(Hh & Hs & HΓ)"; iIntros {j K} "Hj /=".
value_case. iExists (v _); eauto. value_case. iExists (#v _); eauto.
Qed. Qed.
Lemma bin_log_related_pair Γ e1 e2 e1' e2' τ1 τ2 Lemma bin_log_related_pair Γ e1 e2 e1' e2' τ1 τ2
...@@ -94,7 +94,7 @@ Section fundamental. ...@@ -94,7 +94,7 @@ Section fundamental.
iIntros {Δ vvs ρ ?} "#(Hh & Hs & HΓ)"; iIntros {j K} "Hj /=". iIntros {Δ vvs ρ ?} "#(Hh & Hs & HΓ)"; iIntros {j K} "Hj /=".
smart_wp_bind (FstCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ j (K ++ [FstCtx])); cbn. smart_wp_bind (FstCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ j (K ++ [FstCtx])); cbn.
iDestruct "Hiv" as { [w1 w1'] [w2 w2'] } "#[% [Hw1 Hw2]]"; simplify_eq. iDestruct "Hiv" as { [w1 w1'] [w2 w2'] } "#[% [Hw1 Hw2]]"; simplify_eq.
iPvs (step_fst _ _ j K (# w1') w1' (# w2') w2' with "* [-]") as "Hw"; eauto. iPvs (step_fst _ _ j K (of_val w1') w1' (of_val w2') w2' with "* [-]") as "Hw"; eauto.
iApply wp_fst; eauto. iApply wp_fst; eauto.
Qed. Qed.
...@@ -105,7 +105,7 @@ Section fundamental. ...@@ -105,7 +105,7 @@ Section fundamental.
iIntros {Δ vvs ρ ?} "#(Hh & Hs & HΓ)"; iIntros {j K} "Hj /=". iIntros {Δ vvs ρ ?} "#(Hh & Hs & HΓ)"; iIntros {j K} "Hj /=".
smart_wp_bind (SndCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ j (K ++ [SndCtx])); cbn. smart_wp_bind (SndCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ j (K ++ [SndCtx])); cbn.
iDestruct "Hiv" as { [w1 w1'] [w2 w2'] } "#[% [Hw1 Hw2]]"; simplify_eq. iDestruct "Hiv" as { [w1 w1'] [w2 w2'] } "#[% [Hw1 Hw2]]"; simplify_eq.
iPvs (step_snd _ _ j K (# w1') w1' (# w2') w2' with "* [-]") as "Hw"; eauto. iPvs (step_snd _ _ j K (of_val w1') w1' (of_val w2') w2' with "* [-]") as "Hw"; eauto.
iApply wp_snd; eauto. iApply wp_snd; eauto.
Qed. Qed.
...@@ -147,13 +147,13 @@ Section fundamental. ...@@ -147,13 +147,13 @@ Section fundamental.
('IHHtyped1 _ _ _ j (K ++ [CaseCtx _ _])); cbn. ('IHHtyped1 _ _ _ j (K ++ [CaseCtx _ _])); cbn.
iDestruct "Hiv" as "[Hiv|Hiv]". iDestruct "Hiv" as "[Hiv|Hiv]".
- iDestruct "Hiv" as { [w w'] } "[% Hw]"; simplify_eq. - iDestruct "Hiv" as { [w w'] } "[% Hw]"; simplify_eq.
iPvs (step_case_inl _ _ j K (# w') w' with "* [-]") as "Hz"; eauto. iPvs (step_case_inl _ _ j K (of_val w') w' with "* [-]") as "Hz"; eauto.
iApply wp_case_inl; auto 1 using to_of_val. iNext. iApply wp_case_inl; auto 1 using to_of_val. iNext.
asimpl. erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto). asimpl. erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
iApply ('IHHtyped2 _ ((w,w') :: vvs)); repeat iSplit; eauto. iApply ('IHHtyped2 _ ((w,w') :: vvs)); repeat iSplit; eauto.
iApply interp_env_cons; auto. iApply interp_env_cons; auto.
- iDestruct "Hiv" as { [w w'] } "[% Hw]"; simplify_eq. - iDestruct "Hiv" as { [w w'] } "[% Hw]"; simplify_eq.
iPvs (step_case_inr _ _ j K (# w') w' with "* [-]") as "Hz"; eauto. iPvs (step_case_inr _ _ j K (of_val w') w' with "* [-]") as "Hz"; eauto.
iApply wp_case_inr; auto 1 using to_of_val. iNext. iApply wp_case_inr; auto 1 using to_of_val. iNext.
asimpl. erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto). asimpl. erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
iApply ('IHHtyped3 _ ((w,w') :: vvs)); repeat iSplit; eauto. iApply ('IHHtyped3 _ ((w,w') :: vvs)); repeat iSplit; eauto.
...@@ -205,8 +205,8 @@ Section fundamental. ...@@ -205,8 +205,8 @@ Section fundamental.
iLöb as "IH". iIntros { [v v'] } "#Hiv". iIntros {j' K'} "Hj". iLöb as "IH". iIntros { [v v'] } "#Hiv". iIntros {j' K'} "Hj".
iDestruct (interp_env_length with "HΓ") as %?. iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_rec; auto 1 using to_of_val. iNext. iApply wp_rec; auto 1 using to_of_val. iNext.
iPvs (step_rec _ _ j' K' _ (# v') v' with "* [-]") as "Hz"; eauto. iPvs (step_rec _ _ j' K' _ (of_val v') v' with "* [-]") as "Hz"; eauto.
asimpl. change (Rec ?e) with (# (RecV e)). asimpl. change (Rec ?e) with (of_val (RecV e)).
erewrite !n_closed_subst_head_simpl_2 by (rewrite ?fmap_length; eauto). erewrite !n_closed_subst_head_simpl_2 by (rewrite ?fmap_length; eauto).
iApply ('IHHtyped _ ((_,_) :: (v,v') :: vvs)); repeat iSplit; eauto. iApply ('IHHtyped _ ((_,_) :: (v,v') :: vvs)); repeat iSplit; eauto.
iApply interp_env_cons; iSplit; [|iApply interp_env_cons]; auto. iApply interp_env_cons; iSplit; [|iApply interp_env_cons]; auto.
...@@ -279,7 +279,7 @@ Section fundamental. ...@@ -279,7 +279,7 @@ Section fundamental.
rewrite /= fixpoint_unfold /=. rewrite /= fixpoint_unfold /=.
change (fixpoint _) with (interp (TRec τ) Δ). change (fixpoint _) with (interp (TRec τ) Δ).
iDestruct "Hiw" as { [w w'] } "#[% Hiz]"; simplify_eq/=. iDestruct "Hiw" as { [w w'] } "#[% Hiz]"; simplify_eq/=.
iPvs (step_Fold _ _ j K (# w') w' with "* [-]") as "Hz"; eauto. iPvs (step_Fold _ _ j K (of_val w') w' with "* [-]") as "Hz"; eauto.
iApply wp_fold; cbn; auto. iApply wp_fold; cbn; auto.
iNext; iPvsIntro; iExists _; iFrame "Hz". by rewrite -interp_subst. iNext; iPvsIntro; iExists _; iFrame "Hz". by rewrite -interp_subst.
Qed. Qed.
...@@ -301,7 +301,7 @@ Section fundamental. ...@@ -301,7 +301,7 @@ Section fundamental.
Proof. Proof.
iIntros {Δ vvs ρ ?} "#(Hh & Hs & HΓ)"; iIntros {j K} "Hj /=". iIntros {Δ vvs ρ ?} "#(Hh & Hs & HΓ)"; iIntros {j K} "Hj /=".
smart_wp_bind (AllocCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ j (K ++ [AllocCtx])). smart_wp_bind (AllocCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ j (K ++ [AllocCtx])).
iPvs (step_alloc _ _ j K (# v') v' with "* [-]") as {l'} "[Hj Hl]"; eauto. iPvs (step_alloc _ _ j K (of_val v') v' with "* [-]") as {l'} "[Hj Hl]"; eauto.
iApply wp_alloc; auto. iApply wp_alloc; auto.
iIntros "{$Hh} >"; iIntros {l} "Hl'". iIntros "{$Hh} >"; iIntros {l} "Hl'".
iPvs (inv_alloc (logN .@ (l,l')) _ ( w : val * val, iPvs (inv_alloc (logN .@ (l,l')) _ ( w : val * val,
...@@ -341,7 +341,7 @@ Section fundamental. ...@@ -341,7 +341,7 @@ Section fundamental.
iInv (logN .@ (l,l')) as { [v v'] } "[Hv1 [Hv2 #Hv]]". iInv (logN .@ (l,l')) as { [v v'] } "[Hv1 [Hv2 #Hv]]".
{ eapply bool_decide_spec; eauto using to_of_val. } { eapply bool_decide_spec; eauto using to_of_val. }
iTimeless "Hv2". iTimeless "Hv2".
iPvs (step_store _ _ j K l' v' (# w') w' with "[Hw Hv2]") iPvs (step_store _ _ j K l' v' (of_val w') w' with "[Hw Hv2]")
as "[Hw Hv2]"; [eauto|solve_ndisj|by iFrame|]. as "[Hw Hv2]"; [eauto|solve_ndisj|by iFrame|].
iApply wp_store; auto using to_of_val. solve_ndisj. iApply wp_store; auto using to_of_val. solve_ndisj.
iIntros "{$Hh $Hv1} > Hv1". iPvsIntro. iSplitL "Hv1 Hv2". iIntros "{$Hh $Hv1} > Hv1". iPvsIntro. iSplitL "Hv1 Hv2".
...@@ -368,22 +368,22 @@ Section fundamental. ...@@ -368,22 +368,22 @@ Section fundamental.
{ eapply bool_decide_spec; eauto 10 using to_of_val. } { eapply bool_decide_spec; eauto 10 using to_of_val. }
iTimeless "Hv2". iTimeless "Hv2".
destruct (decide (v = w)) as [|Hneq]; subst. destruct (decide (v = w)) as [|Hneq]; subst.
- iPvs (step_cas_suc _ _ j K l' (# w') w' v' (# u') u' - iPvs (step_cas_suc _ _ j K l' (of_val w') w' v' (of_val u') u'
with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj. with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
{ iIntros "{$Hs $Hu $Hv2} >". { iIntros "{$Hs $Hu $Hv2} >".
rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. } rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
iApply wp_cas_suc; eauto using to_of_val; first solve_ndisj. iApply wp_cas_suc; eauto using to_of_val; first solve_ndisj.
iIntros "{$Hh $Hv1} > Hv1". iPvsIntro. iSplitL "Hv1 Hv2". iIntros "{$Hh $Hv1} > Hv1". iPvsIntro. iSplitL "Hv1 Hv2".
+ iNext; iExists (_, _); by iFrame. + iNext; iExists (_, _); by iFrame.
+ iExists (v true); iFrame; eauto. + iExists (#v true); iFrame; eauto.
- iPvs (step_cas_fail _ _ j K l' 1 v' (# w') w' (# u') u' - iPvs (step_cas_fail _ _ j K l' 1 v' (of_val w') w' (of_val u') u'
with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj. with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
{ iIntros "{$Hs $Hu $Hv2} >". { iIntros "{$Hs $Hu $Hv2} >".
rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. } rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
iApply wp_cas_fail; eauto using to_of_val; first solve_ndisj. iApply wp_cas_fail; eauto using to_of_val; first solve_ndisj.
iIntros "{$Hh $Hv1} > Hv1". iPvsIntro. iSplitL "Hv1 Hv2". iIntros "{$Hh $Hv1} > Hv1". iPvsIntro. iSplitL "Hv1 Hv2".
+ iNext; iExists (_, _); by iFrame. + iNext; iExists (_, _); by iFrame.
+ iExists (v false); eauto. + iExists (#v false); eauto.
Qed.