Commit a95c5091 authored by Dan Frumin's avatar Dan Frumin

Make the steps_ lemma curried in the stack example

parent c958e6ec
......@@ -62,10 +62,11 @@ Section CG_Counter.
Lemma steps_CG_increment E ρ j K x n:
nclose specN E
spec_ctx ρ x ↦ₛ (#nv n) j fill K (App (CG_increment (Loc x)) Unit)
|={E}=> j fill K (Unit) x ↦ₛ (#nv (S n)).
spec_ctx ρ - x ↦ₛ (#nv n)
- j fill K (App (CG_increment (Loc x)) Unit)
={E}= j fill K (Unit) x ↦ₛ (#nv (S n)).
Proof.
iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_increment.
iIntros (HNE) "#Hspec Hx Hj". unfold CG_increment.
tp_rec j.
tp_load j.
tp_op j. tp_normalise j.
......@@ -111,16 +112,15 @@ Section CG_Counter.
Lemma steps_CG_locked_increment E ρ j K x n l :
nclose specN E
spec_ctx ρ x ↦ₛ (#nv n) l ↦ₛ (#v false)
j fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
spec_ctx ρ - x ↦ₛ (#nv n) - l ↦ₛ (#v false)
- j fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
={E}= j fill K Unit x ↦ₛ (#nv S n) l ↦ₛ (#v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]".
iMod (steps_with_lock _ _ j K _ _ _ _ UnitV UnitV _ _ with "[Hj Hx Hl]") as "Hj"; last by iFrame.
- iIntros (K') "[#Hspec [Hx Hj]]".
iApply steps_CG_increment; first done. iFrame "Hspec Hj Hx"; trivial.
- by iFrame "Hspec Hj Hx".
Unshelve. all: trivial.
iIntros (HNE) "#Hspec Hx Hl Hj".
iMod (steps_with_lock _ _ _ K _ _ _ _ UnitV UnitV _ _ with "Hspec Hx Hl Hj") as "Hj"; last by iFrame.
{ iIntros (K') "#Hspec Hx Hj /=".
iApply (steps_CG_increment E with "Hspec Hx"); auto. }
Unshelve. all: trivial.
Qed.
Global Opaque CG_locked_increment.
......@@ -150,11 +150,11 @@ Section CG_Counter.
Lemma steps_counter_read E ρ j K x n :
nclose specN E
spec_ctx ρ x ↦ₛ (#nv n)
j fill K (App (counter_read (Loc x)) Unit)
spec_ctx ρ - x ↦ₛ (#nv n)
- j fill K (App (counter_read (Loc x)) Unit)
={E}= j fill K (#n n) x ↦ₛ (#nv n).
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read.
intros HNE. iIntros "#Hspec Hx Hj". unfold counter_read.
tp_rec j.
tp_load j. tp_normalise j.
by iFrame.
......@@ -250,10 +250,8 @@ Section CG_Counter.
iClear "HΓ". cbn -[FG_counter CG_counter].
rewrite ?empty_env_subst /CG_counter /FG_counter.
iApply fupd_wp.
iMod (steps_newlock _ _ j (K ++ [AppRCtx (RecV _)]) _ with "[Hj]")
as (l) "[Hj Hl]"; eauto.
{ rewrite fill_app /=. by iFrame. }
rewrite fill_app /=.
tp_bind j newlock.
iMod (steps_newlock with "Hspec Hj") as (l) "[Hj Hl]"; eauto.
tp_rec j.
asimpl. rewrite CG_locked_increment_subst /=.
rewrite counter_read_subst /=.
......@@ -306,9 +304,7 @@ Section CG_Counter.
destruct (decide (n = n')) as [|Hneq]; subst.
+ (* CAS succeeds *)
(* In this case, we perform increment in the coarse-grained one *)
iMod (steps_CG_locked_increment
_ _ _ _ _ _ _ _ with "[Hj Hl Hcnt']") as "[Hj [Hcnt' Hl]]".
{ iFrame "Hspec Hcnt' Hl Hj"; trivial. }
iMod (steps_CG_locked_increment with "Hspec Hcnt' Hl Hj") as "[Hj [Hcnt' Hl]]"; first by solve_ndisj.
iApply (wp_cas_suc with "[Hcnt]"); auto.
iNext. iIntros "Hcnt".
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
......@@ -334,13 +330,12 @@ Section CG_Counter.
iNext.
iApply wp_atomic; eauto.
iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose".
iMod (steps_counter_read with "[$Hspec $Hj $Hcnt']") as "[Hj Hcnt']"; first by solve_ndisj.
iMod (steps_counter_read with "Hspec Hcnt' Hj") as "[Hj Hcnt']"; first by solve_ndisj.
iApply (wp_load with "[Hcnt]"); eauto.
iNext. iIntros "Hcnt".
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists _; iFrame "Hl Hcnt Hcnt'". }
iExists (#nv _); eauto.
Unshelve. all: solve_ndisj.
Qed.
End CG_Counter.
......
......@@ -84,10 +84,10 @@ Section proof.
Lemma steps_newlock E ρ j K :
nclose specN E
spec_ctx ρ j fill K newlock
|={E}=> l, j fill K (Loc l) l ↦ₛ (#v false).
spec_ctx ρ - j fill K newlock
={E}= l, j fill K (Loc l) l ↦ₛ (#v false).
Proof.
iIntros (HNE) "[#Hspec Hj]".
iIntros (HNE) "#Hspec Hj".
tp_alloc j as l "Hl". tp_normalise j.
by iExists _; iFrame.
Qed.
......@@ -96,10 +96,10 @@ Section proof.
Lemma steps_acquire E ρ j K l :
nclose specN E
spec_ctx ρ l ↦ₛ (#v false) j fill K (App acquire (Loc l))
|={E}=> j fill K Unit l ↦ₛ (#v true).
spec_ctx ρ - l ↦ₛ (#v false) - j fill K (App acquire (Loc l))
={E}= j fill K Unit l ↦ₛ (#v true).
Proof.
iIntros (HNE) "[#Hspec [Hl Hj]]". unfold acquire.
iIntros (HNE) "#Hspec Hl Hj". unfold acquire.
tp_rec j.
tp_cas_suc j.
tp_if_true j. tp_normalise j.
......@@ -110,10 +110,10 @@ Section proof.
Lemma steps_release E ρ j K l b:
nclose specN E
spec_ctx ρ l ↦ₛ (#v b) j fill K (App release (Loc l))
|={E}=> j fill K Unit l ↦ₛ (#v false).
spec_ctx ρ - l ↦ₛ (#v b) - j fill K (App release (Loc l))
={E}= j fill K Unit l ↦ₛ (#v false).
Proof.
iIntros (HNE) "[#Hspec [Hl Hj]]". unfold release.
iIntros (HNE) "#Hspec Hl Hj". unfold release.
tp_rec j.
tp_store j. tp_normalise j.
by iFrame.
......@@ -124,27 +124,27 @@ Section proof.
Lemma steps_with_lock E ρ j K e l P Q v w:
nclose specN E
( f, e.[f] = e) (* e is a closed term *)
( K', spec_ctx ρ P j fill K' (App e (of_val w))
|={E}=> j fill K' (of_val v) Q)
spec_ctx ρ P l ↦ₛ (#v false)
j fill K (App (with_lock e (Loc l)) (of_val w))
|={E}=> j fill K (of_val v) Q l ↦ₛ (#v false).
( K', spec_ctx ρ - P - j fill K' (App e (of_val w))
={E}= j fill K' (of_val v) Q)
spec_ctx ρ - P - l ↦ₛ (#v false)
- j fill K (App (with_lock e (Loc l)) (of_val w))
={E}= j fill K (of_val v) Q l ↦ₛ (#v false).
Proof.
iIntros (HNE H1 H2) "[#Hspec [HP [Hl Hj]]]".
iIntros (HNE H1 H2) "#Hspec HP Hl Hj".
tp_rec j; eauto using to_of_val.
asimpl. rewrite H1.
(* TODO: a tp_apply tactic similar to that of iApply *)
tp_bind j (App acquire (Loc l)).
iMod (steps_acquire _ _ j with "[$Hspec $Hj $Hl]") as "[Hj Hl]"; eauto.
iMod (steps_acquire _ _ j with "Hspec Hl Hj") as "[Hj Hl]"; eauto.
tp_rec j.
asimpl. rewrite H1.
tp_bind j (App e _).
iMod (H2 with "[$Hspec $Hj $HP]") as "[Hj HQ]".
iMod (H2 with "Hspec HP Hj") as "[Hj HQ]".
tp_normalise j.
tp_rec j; eauto using to_of_val.
asimpl.
tp_bind j (App release _).
iMod (steps_release with "[$Hspec $Hj $Hl]") as "[Hj Hl]"; auto.
iMod (steps_release with "Hspec Hl Hj") as "[Hj Hl]"; auto.
tp_rec j.
tp_normalise j. asimpl.
by iFrame.
......
......@@ -98,10 +98,10 @@ Section CG_Stack.
Lemma steps_CG_push E ρ j K st v w :
nclose specN E
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)).
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)).
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push.
intros HNE. iIntros "#Hspec Hx Hj". unfold CG_push.
tp_rec j; eauto using to_of_val.
tp_normalise j.
tp_load j. tp_normalise j.
......@@ -144,19 +144,16 @@ Section CG_Stack.
Lemma steps_CG_locked_push E ρ j K st w v l :
nclose specN E
spec_ctx ρ st ↦ₛ v l ↦ₛ (#v false)
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).
spec_ctx ρ - st ↦ₛ v - l ↦ₛ (#v false)
- 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).
Proof.
iIntros (?) "(#Hspec & Hst & Hl & Hj)".
iIntros (?) "#Hspec Hst Hl Hj".
unfold CG_locked_push.
(* TODO would be nice to be able to determine that e := Loc l for instance *)
iMod (steps_with_lock _ _ j K (CG_push (Loc st)) l _ _ UnitV _ _ _ with "[Hspec Hst Hj Hl]") as "Hj"; last done.
- iIntros (K') "(#Hspec & HQ & Hj)".
iApply steps_CG_push; first eauto.
iFrame "Hspec Hj". iFrame "HQ".
- by iFrame.
Unshelve. all: trivial.
iMod (steps_with_lock _ _ _ _ _ _ _ _ UnitV with "Hspec Hst Hl Hj") as "Hj"; auto.
iIntros (K') "#Hspec HQ Hj".
iApply (steps_CG_push with "Hspec HQ"); auto.
Qed.
Global Opaque CG_locked_push.
......@@ -187,11 +184,11 @@ Section CG_Stack.
Lemma steps_CG_pop_suc E ρ j K st v w :
nclose specN E
spec_ctx ρ st ↦ₛ FoldV (InjRV (PairV w v))
j fill K (App (CG_pop (Loc st)) Unit)
|={E}=> j fill K (InjR (of_val w)) st ↦ₛ v.
spec_ctx ρ - st ↦ₛ FoldV (InjRV (PairV w v))
- j fill K (App (CG_pop (Loc st)) Unit)
={E}= j fill K (InjR (of_val w)) st ↦ₛ v.
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop.
intros HNE. iIntros "#Hspec Hx Hj". unfold CG_pop.
tp_rec j. asimpl.
tp_load j. tp_normalise j.
tp_fold j; simpl; first by rewrite ?to_of_val /=.
......@@ -206,11 +203,11 @@ Section CG_Stack.
Lemma steps_CG_pop_fail E ρ j K st :
nclose specN E
spec_ctx ρ st ↦ₛ FoldV (InjLV UnitV)
j fill K (App (CG_pop (Loc st)) Unit)
|={E}=> j fill K (InjL Unit) st ↦ₛ FoldV (InjLV UnitV).
spec_ctx ρ - st ↦ₛ FoldV (InjLV UnitV)
- j fill K (App (CG_pop (Loc st)) Unit)
={E}= j fill K (InjL Unit) st ↦ₛ FoldV (InjLV UnitV).
Proof.
iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_pop.
iIntros (HNE) "#Hspec Hx Hj". unfold CG_pop.
tp_rec j.
tp_load j. asimpl. tp_normalise j.
tp_fold j.
......@@ -253,32 +250,30 @@ Section CG_Stack.
Lemma steps_CG_locked_pop_suc E ρ j K st v w l :
nclose specN E
spec_ctx ρ st ↦ₛ FoldV (InjRV (PairV w v)) l ↦ₛ (#v false)
j fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
|={E}=> j fill K (InjR (of_val w)) st ↦ₛ 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)
={E}= j fill K (InjR (of_val w)) st ↦ₛ v l ↦ₛ (#v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
iMod (steps_with_lock _ _ j K _ _ _ _ (InjRV w) UnitV _ _
with "[Hj Hx Hl]") as "Hj"; last done.
- iIntros (K') "[#Hspec [Hx Hj]]".
iApply steps_CG_pop_suc; first done. iFrame "Hspec Hj Hx"; trivial.
- iFrame "Hspec Hj Hx"; trivial.
Unshelve. all: trivial.
iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_locked_pop.
iMod (steps_with_lock _ _ _ _ _ _ _ _ (InjRV w) UnitV _ _
with "Hspec Hx Hl Hj") as "Hj"; auto.
iIntros (K') "#Hspec Hx Hj".
iApply (steps_CG_pop_suc with "Hspec Hx Hj"). trivial.
Unshelve. all: trivial.
Qed.
Lemma steps_CG_locked_pop_fail E ρ j K st l :
nclose specN E
spec_ctx ρ st ↦ₛ FoldV (InjLV UnitV) l ↦ₛ (#v false)
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).
spec_ctx ρ - st ↦ₛ FoldV (InjLV UnitV) - l ↦ₛ (#v false)
- 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).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
iMod (steps_with_lock _ _ j K _ _ _ _ (InjLV UnitV) UnitV _ _
with "[Hj Hx Hl]") as "Hj"; last done.
- iIntros (K') "[#Hspec [Hx Hj]] /=".
iApply steps_CG_pop_fail; first done. iFrame "Hspec Hj Hx"; trivial.
- iFrame "Hspec Hj Hx"; trivial.
Unshelve. all: trivial.
iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_locked_pop.
iMod (steps_with_lock _ _ _ _ _ _ _ _ (InjLV UnitV) UnitV _ _
with "Hspec Hx Hl Hj") as "Hj"; auto.
iIntros (K') "#Hspec Hx Hj /=".
iApply (steps_CG_pop_fail with "Hspec Hx Hj"). trivial.
Unshelve. all: trivial.
Qed.
Global Opaque CG_locked_pop.
......@@ -316,14 +311,14 @@ Section CG_Stack.
Lemma steps_CG_snap E ρ j K st v l :
nclose specN E
spec_ctx ρ st ↦ₛ v l ↦ₛ (#v false)
j fill K (App (CG_snap (Loc st) (Loc l)) Unit)
|={E}=> j (fill K (of_val v)) st ↦ₛ v l ↦ₛ (#v false).
spec_ctx ρ - st ↦ₛ v - l ↦ₛ (#v false)
- j fill K (App (CG_snap (Loc st) (Loc l)) Unit)
={E}= j (fill K (of_val v)) st ↦ₛ v l ↦ₛ (#v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_snap.
iIntros (HNE) "#Hspec Hx Hl Hj". unfold CG_snap.
iMod (steps_with_lock _ _ j K _ _ _ _ v UnitV _ _
with "[Hj Hx Hl]") as "Hj"; last done; [|by iFrame "Hspec Hx Hl Hj"].
iIntros (K') "[#Hspec [Hx Hj]]".
with "Hspec Hx Hl Hj") as "Hj"; auto.
iIntros (K') "#Hspec Hx Hj".
tp_rec j.
tp_load j. tp_normalise j.
by iFrame.
......@@ -377,17 +372,16 @@ Section CG_Stack.
Lemma steps_CG_iter E ρ j K f v w :
nclose specN E
spec_ctx ρ
j fill K (App (CG_iter (of_val f))
(Fold (InjR (Pair (of_val w) (of_val v)))))
|={E}=>
j fill K
(App
(Rec
(App ((CG_iter (of_val f)).[ren (+2)])
(Snd (Pair ((of_val w).[ren (+2)]) (of_val v).[ren (+2)]))))
(App (of_val f) (of_val w))).
- j fill K (App (CG_iter (of_val f))
(Fold (InjR (Pair (of_val w) (of_val v)))))
={E}= j fill K
(App
(Rec
(App ((CG_iter (of_val f)).[ren (+2)])
(Snd (Pair ((of_val w).[ren (+2)]) (of_val v).[ren (+2)]))))
(App (of_val f) (of_val w))).
Proof.
iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
iIntros (HNE) "#Hspec Hj". unfold CG_iter.
tp_rec j; first by (rewrite /= ?to_of_val /=).
rewrite -CG_iter_folding. Opaque CG_iter.
tp_fold j; first by (rewrite /= ?to_of_val /=).
......@@ -402,10 +396,10 @@ Section CG_Stack.
Lemma steps_CG_iter_end E ρ j K f :
nclose specN E
spec_ctx ρ j fill K (App (CG_iter (of_val f)) (Fold (InjL Unit)))
|={E}=> j fill K Unit.
spec_ctx ρ - j fill K (App (CG_iter (of_val f)) (Fold (InjL Unit)))
={E}= j fill K Unit.
Proof.
iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
iIntros (HNE) "#Hspec Hj". unfold CG_iter.
tp_rec j.
tp_fold j.
tp_case_inl j. tp_normalise j.
......
......@@ -63,9 +63,8 @@ Section Stack_refinement.
end) with ( stackN) by reflexivity.
replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2))) by (rewrite CG_iter_of_val; done).
tp_bind j (App (CG_snap _ _) ())%E.
iMod (steps_CG_snap with "[$Hs Hst' Hl Hj]") as "(Hj & Hst' & Hl)";
iMod (steps_CG_snap with "Hs Hst' Hl Hj") as "(Hj & Hst' & Hl)";
first solve_ndisj.
{ iFrame "Hst'". iFrame. }
tp_normalise j.
close_sinv "Hclose" "[Hoe Hst' Hst HLK Hl]".
......@@ -89,7 +88,7 @@ Section Stack_refinement.
iNext.
iApply fupd_wp.
rewrite CG_iter_of_val /=.
iMod (steps_CG_iter_end with "[$Hs $Hj]") as "Hj"; first solve_ndisj.
iMod (steps_CG_iter_end with "Hs Hj") as "Hj"; first solve_ndisj.
iModIntro.
iApply wp_value; auto.
iExists UnitV. iFrame. eauto.
......@@ -101,7 +100,7 @@ Section Stack_refinement.
iNext. iModIntro.
wp_bind (App (of_val f1) _).
rewrite CG_iter_of_val.
iMod (steps_CG_iter with "[$Hs $Hj]") as "Hj"; first solve_ndisj.
iMod (steps_CG_iter with "Hs Hj") as "Hj"; first solve_ndisj.
rewrite CG_iter_subst.
tp_bind j (App (of_val f2) _).
iSpecialize ("Hff" $! (y1, y2) with "Hy").
......@@ -153,7 +152,7 @@ Section Stack_refinement.
iInv stackN as (istk2 v h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose". (* TODO : why can we remove the later here?*)
destruct (decide (istk = istk2)) as [Heq|Hneq]; first subst istk.
* (* Case CAS succeeds *)
iMod (steps_CG_locked_push _ _ j K st' v2 with "[$Hj $Hs $Hst' $Hl]") as "[Hj [Hst' Hl]]"; first solve_ndisj.
iMod (steps_CG_locked_push _ _ j K st' v2 with "Hs Hst' Hl Hj") as "[Hj [Hst' Hl]]"; first solve_ndisj.
iApply (wp_cas_suc with "Hst"); auto.
iNext. iIntros "Hst".
......@@ -196,7 +195,7 @@ Section Stack_refinement.
(* Checking whether the stack is empty *)
rewrite {2}StackLink_unfold.
iDestruct "HLK'" as (istk2 w) "[% [Hmpt [[% %]|HLK']]]"; simplify_eq/=.
+ iMod (steps_CG_locked_pop_fail with "[$Hs $Hst' $Hl $Hj]")
+ iMod (steps_CG_locked_pop_fail with "Hs Hst' Hl Hj")
as "(Hj & Hstk' & Hl)"; first solve_ndisj.
close_sinv "Hclose" "[Hoe Hstk' Hst Hl]".
wp_bind (Unfold _). iApply wp_fold; first by auto using to_of_val. iNext.
......@@ -249,7 +248,7 @@ Section Stack_refinement.
iDestruct "HLK'" as (yn1 yn2 zn1 zn2)
"[% [% [#Hrel HLK'']]]"; simplify_eq/=.
(* Now we have proven that specification can also pop. *)
iMod (steps_CG_locked_pop_suc with "[$Hs $Hst' $Hl $Hj]")
iMod (steps_CG_locked_pop_suc with "Hs Hst' Hl Hj")
as "[Hj [Hst' Hl]]"; first solve_ndisj.
iMod ("Hclose" with "[-Hj]") as "_".
{ iNext.
......@@ -297,7 +296,7 @@ Section Stack_refinement.
iApply fupd_wp.
tp_tlam j.
tp_bind j newlock.
iMod (steps_newlock with "[$Hj]") as (l') "[Hj Hl']"; eauto.
iMod (steps_newlock with "Hspec Hj") as (l') "[Hj Hl']"; eauto.
tp_normalise j.
tp_rec j.
tp_alloc j as stk' "Hstk'".
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment