Commit 4911a6e6 authored by Simon Friis Vindum's avatar Simon Friis Vindum

Small tweaks to refinement proof of stack

parent c3423d5a
......@@ -38,11 +38,9 @@ Section Stack_refinement.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iAsimpl.
iApply (wp_bind (fill [AllocCtx; AppRCtx (RecV _)]));
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iApply (wp_bind (fill [AllocCtx; AppRCtx (RecV _)])).
iApply wp_alloc; first done. iNext; iIntros (istk) "Histk".
iApply (wp_bind (fill [AppRCtx (RecV _)]));
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iApply (wp_bind (fill [AppRCtx (RecV _)])).
iApply wp_alloc; first done. iNext; iIntros (stk) "Hstk".
simpl. iApply wp_pure_step_later; trivial. iNext. simpl.
iAsimpl.
......@@ -89,29 +87,26 @@ Section Stack_refinement.
iNext.
rewrite -(FG_push_folding (Loc stk)).
iAsimpl.
iApply (wp_bind (fill [LetInCtx _]));
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iInv stackN as (istk v h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose".
iApply (wp_bind (fill [LetInCtx _])).
iInv stackN as (istk v h) "(Hoe & Hstk' & Hstk & HLK & Hl)" "Hclose".
iApply (wp_load with "Hstk"). iNext. iIntros "Hstk".
iMod ("Hclose" with "[Hoe Hstk' HLK Hl Hstk]") as "_".
{ iNext. iExists _, _, _; by iFrame "Hoe Hstk' HLK Hl Hstk". }
clear v h.
iApply wp_pure_step_later; auto using to_of_val.
iModIntro. iNext. iAsimpl.
iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _); IfCtx _ _]));
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _); IfCtx _ _])).
iApply wp_alloc; simpl; trivial.
iNext. iIntros (ltmp) "Hltmp".
iApply (wp_bind (fill [IfCtx _ _]));
iApply wp_wand_l; iSplitR; [iIntros (w) "H"; iExact "H"|].
iInv stackN as (istk2 v h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose".
iApply (wp_bind (fill [IfCtx _ _])).
iInv stackN as (istk2 v h) "(Hoe & Hstk' & Hstk & HLK & Hl)" "Hclose".
(* deciding whether CAS will succeed or fail *)
destruct (decide (istk = istk2)) as [|Hneq]; subst.
* (* CAS succeeds *)
(* In this case, the specification pushes *)
iMod "Hstk'". iMod "Hl".
iMod (steps_CG_locked_push _ j K with "[Hj Hl Hstk']")
as "[Hj [Hstk' Hl]]"; first solve_ndisj.
as "(Hj & Hstk' & Hl)"; first solve_ndisj.
{ rewrite CG_locked_push_of_val. by iFrame "Hspec Hstk' Hj". }
iApply (wp_cas_suc with "Hstk"); auto.
iNext. iIntros "Hstk".
......@@ -131,16 +126,15 @@ Section Stack_refinement.
{ iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
iApply wp_pure_step_later; auto. iModIntro. iNext. by iApply "Hlat".
+ (* refinement of pop *)
iAlways. clear j K. iIntros ( [v1 v2] ) "[% %]".
iIntros (j K) "Hj /="; simplify_eq/=.
iAlways. clear j K. iIntros ( [v1 v2] ) "[-> ->]".
iIntros (j K) "Hj /=".
rewrite -(FG_pop_folding (Loc stk)).
iLöb as "Hlat".
rewrite {2}(FG_pop_folding (Loc stk)).
iApply wp_pure_step_later; auto. iNext.
rewrite -(FG_pop_folding (Loc stk)).
iAsimpl.
iApply (wp_bind (fill [LetInCtx _]));
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iApply (wp_bind (fill [LetInCtx _])).
iInv stackN as (istk v h) "[Hoe [Hstk' [Hstk [#HLK Hl]]]]" "Hclose".
iApply (wp_load with "Hstk"). iNext. iIntros "Hstk".
iPoseProof "HLK" as "HLK'".
......@@ -156,8 +150,7 @@ Section Stack_refinement.
iModIntro.
iApply wp_pure_step_later; auto. iNext. iAsimpl.
clear h.
iApply (wp_bind (fill [LetInCtx _]));
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [LetInCtx _])).
iClear "HLK".
iInv stackN as (istk3 w h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose".
iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]".
......@@ -176,10 +169,9 @@ Section Stack_refinement.
iModIntro. iApply wp_pure_step_later; auto.
iNext. iAsimpl.
clear h.
iApply (wp_bind (fill [LetInCtx _]));
iApply wp_wand_l; iSplitR; [iIntros (w') "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [LetInCtx _])).
iClear "HLK".
iInv stackN as (istk3 w' h) "[Hoe [Hstk' [Hstk [HLK Hl]]]]" "Hclose".
iInv stackN as (istk3 w' h) "(Hoe & Hstk' & Hstk & HLK & Hl)" "Hclose".
iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]".
iApply (wp_load with "Histk"). iNext; iIntros "Histk".
iDestruct ("HLoe" with "Histk") as "Hh".
......@@ -190,16 +182,13 @@ Section Stack_refinement.
iDestruct "HLK'" as (y1 z1 y2 z2) "[% HLK']". subst. simpl.
iApply wp_pure_step_later; first done.
iNext. iAsimpl.
iApply (wp_bind (fill [UnfoldCtx; CasRCtx (LocV _) (LocV _); IfCtx _ _]));
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [UnfoldCtx; CasRCtx (LocV _) (LocV _); IfCtx _ _])).
iAsimpl. iApply wp_pure_step_later; auto.
simpl. iNext. iApply wp_value.
iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _); IfCtx _ _]));
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _); IfCtx _ _])).
iAsimpl. iApply wp_pure_step_later; auto.
simpl. iNext. iApply wp_value.
iApply (wp_bind (fill [IfCtx _ _]));
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [IfCtx _ _])).
clear istk3 h. iAsimpl.
iInv stackN as (istk3 w h) "[Hoe [Hstk' [Hstk [#HLK Hl]]]]" "Hclose".
(* deciding whether CAS will succeed or fail *)
......@@ -227,8 +216,7 @@ Section Stack_refinement.
iExists _, _; iSplitR; trivial.
by iFrame "HLK". }
iApply wp_pure_step_later; auto. iModIntro. iNext.
iApply (wp_bind (fill [InjRCtx])); iApply wp_wand_l;
iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [InjRCtx])).
iApply wp_pure_step_later; auto. iApply wp_value.
iNext. iApply wp_value; simpl.
iExists (InjRV _); iFrame "Hj".
......@@ -247,8 +235,7 @@ Section Stack_refinement.
by (by rewrite FG_iter_of_val).
replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2)))
by (by rewrite CG_iter_of_val).
iApply (wp_bind (fill [FoldCtx; AppRCtx _])); iApply wp_wand_l;
iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [FoldCtx; AppRCtx _])).
iInv stackN as (istk3 w h) "[Hoe [>Hstk' [>Hstk [#HLK >Hl]]]]" "Hclose".
iMod (steps_CG_snap _ _ (AppRCtx _ :: K)
with "[Hstk' Hj Hl]") as "[Hj [Hstk' Hl]]"; first solve_ndisj.
......@@ -263,11 +250,9 @@ Section Stack_refinement.
iApply wp_pure_step_later; simpl; trivial.
rewrite -FG_iter_folding. iAsimpl.
iNext.
iApply (wp_bind (fill [LoadCtx; CaseCtx _ _])); iApply wp_wand_l;
iSplitR; [iIntros (v) "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [LoadCtx; CaseCtx _ _])).
iApply wp_pure_step_later; trivial. iApply wp_value. iNext.
iApply (wp_bind (fill [CaseCtx _ _])); iApply wp_wand_l;
iSplitR; [iIntros (v) "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [CaseCtx _ _])).
rewrite StackLink_unfold.
iDestruct "HLK" as (istk4 v) "[% [Hmpt HLK]]"; simplify_eq/=.
iInv stackN as (istk5 v' h) "[Hoe [Hstk' [Hstk [HLK' Hl]]]]" "Hclose".
......@@ -291,12 +276,10 @@ Section Stack_refinement.
iApply wp_pure_step_later; simpl; rewrite ?to_of_val; trivial.
iAsimpl.
iModIntro. iNext.
iApply (wp_bind (fill [AppRCtx _; SeqCtx _]));
iApply wp_wand_l; iSplitR; [iIntros (w') "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [AppRCtx _; SeqCtx _])).
iApply wp_pure_step_later; simpl; rewrite ?to_of_val; trivial. iNext.
iApply wp_value.
iApply (wp_bind (fill [SeqCtx _]));
iApply wp_wand_l; iSplitR; [iIntros (w') "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [SeqCtx _])).
rewrite StackLink_unfold.
iDestruct "HLK''" as (istk6 w') "[% HLK]"; simplify_eq/=.
iSpecialize ("Hfs" $! (yn1, zn1) with "Hrel").
......@@ -314,8 +297,7 @@ Section Stack_refinement.
iNext. simpl.
replace (FG_iter (of_val f1)) with (of_val (FG_iterV (of_val f1)))
by (by rewrite FG_iter_of_val).
iApply (wp_bind (fill [AppRCtx _]));
iApply wp_wand_l; iSplitR; [iIntros (w'') "Hw"; iExact "Hw"|].
iApply (wp_bind (fill [AppRCtx _])).
iApply wp_pure_step_later; auto using to_of_val.
simpl. iNext. rewrite -FG_iter_folding. iApply wp_value.
iApply ("Hlat" $! istk6 zn2 with "[Hj] [HLK]"); trivial.
......
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