Skip to content

GitLab

Commit c958e6ec authored by Dan Frumin's avatar Dan Frumin
Browse files
Options

[F_mu_ref_conc] simplify the refinement proof for the stack example

parent 10632f27
Hide whitespace changes
Inline Side-by-side
Showing with 385 additions and 297 deletions
F_mu_ref_conc/examples/stack/refinement.v
View file @ c958e6ec
From iris.algebra Require Import auth.
From iris.program_logic Require Import adequacy ectxi_language.
From iris_logrel.F_mu_ref_conc Require Import soundness_binary.
From iris_logrel.F_mu_ref_conc Require Import lang tactics soundness_binary notation.
From iris_logrel.F_mu_ref_conc.examples Require Import lock.
From iris_logrel.F_mu_ref_conc.examples.stack Require Import
CG_stack FG_stack stack_rules.
From iris.proofmode Require Import tactics.
Definition stackN : namespace := nroot .@ "stack".
......@@ -12,7 +11,270 @@ Section Stack_refinement.
Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types Δ : listC D.
Import lang.
Definition sinv τi stk stk' l' {SH: stackG Σ} : iProp Σ
:= (∃ istk v h, (stack_owns h)
∗ stk' ↦ₛ v
∗ stk ↦ᵢ (FoldV (#istk))
∗ StackLink τi (#istk, v)
∗ l' ↦ₛ (#♭v false))%I.
Ltac close_sinv Hcl asn :=
iMod (Hcl with asn) as "_";
[iNext; rewrite /sinv; iExists _,_,_; by iFrame |]; try iModIntro.
Definition CG_snap_iterV (st l : expr) : val :=
RecV (App (CG_iter (Var 1)) (App (CG_snap st.[ren (+2)] l.[ren (+2)]) Unit)).
Definition FG_read_iterV (st : expr) : val :=
RecV (App (FG_iter (Var 1)) (Load st.[ren (+2)])).
Lemma FG_CG_iter_refinement ρ st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ}:
spec_ctx ρ -∗ inv stackN (sinv τi st st' l) -∗
⟦ TArrow (TArrow (TVar 0) TUnit) TUnit ⟧ (τi::Δ) (FG_read_iterV (#st)%E, (CG_snap_iterV #st' #l)%E).
Proof.
iIntros "#Hs #Hinv".
iAlways. iIntros ([f1 f2]) "#Hff /=".
iIntros (j K) "Hj /=".
iApply wp_rec; auto using to_of_val.
iNext. simpl. rewrite FG_iter_subst. simpl.
replace (FG_iter (of_val f1)) with (of_val (FG_iterV (of_val f1))) by (rewrite FG_iter_of_val; done).
wp_bind (Load #st)%E.
iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
iApply (wp_load with "Hst"). iNext. iIntros "Hst".
tp_rec j; auto using to_of_val.
tp_normalise j.
rewrite CG_iter_subst CG_snap_subst. asimpl.
replace (match @up_close namespace coPset nclose stackN return coPset with
| @exist _ _ t2 _ =>
@exist coPset_raw (fun t : coPset_raw => Is_true (coPset_wf t))
match coPset_opp_raw t2 return coPset_raw with
| coPLeaf b =>
match b return coPset_raw with
| true => coPLeaf true
| false => coPLeaf false
end
| coPNode b l0 r => coPNode b l0 r
end
(coPset_intersection_wf (coPLeaf true)
(coPset_opp_raw t2) I (coPset_opp_wf t2))
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)";
first solve_ndisj.
{ iFrame "Hst'". iFrame. }
tp_normalise j.
close_sinv "Hclose" "[Hoe Hst' Hst HLK Hl]".
iLöb as "IH" forall (istk v) "HLK".
iApply wp_rec; auto. iNext. asimpl.
wp_bind (Unfold _). iApply wp_fold; auto. iNext.
iModIntro. wp_bind (Load _).
clear h.
iInv stackN as (istk2 v' h) "[Hoe [Hst' [Hst [HLK' Hl]]]]" "Hclose".
rewrite StackLink_unfold.
iDestruct "HLK" as (istkl w) "[% [Histk HLK]]". simplify_eq/=.
iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histkl Hoe]".
iApply (wp_load with "Histkl"). iNext. iIntros "Histkl".
iSpecialize ("Hoe" with "Histkl").
close_sinv "Hclose" "[Hoe Hst Hst' HLK' Hl]".
iDestruct "HLK" as "[[% %]|HLK]"; subst.
+ (* the stack is empty *)
iApply wp_case_inl; auto.
iNext.
iApply fupd_wp.
rewrite CG_iter_of_val /=.
iMod (steps_CG_iter_end with "[$Hs $Hj]") as "Hj"; first solve_ndisj.
iModIntro.
iApply wp_value; auto.
iExists UnitV. iFrame. eauto.
+ iDestruct "HLK" as (y1 z1 y2 z2) "[% [% [Hy Hsl]]]". subst.
simpl.
iApply wp_case_inr; first by rewrite /= ?to_of_val /=.
iNext. asimpl.
wp_bind (Fst _). iApply wp_fst; try by (auto using to_of_val || rewrite /= ?to_of_val /=).
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.
rewrite CG_iter_subst.
tp_bind j (App (of_val f2) _).
iSpecialize ("Hff" $! (y1, y2) with "Hy").
iSpecialize ("Hff" $! j (K ++ _) with "Hj"). simpl.
iApply (wp_wand with "Hff").
iIntros (v). iDestruct 1 as (v2) "[Hj [% %]]".
tp_normalise j. asimpl.
iApply fupd_wp. tp_rec j; auto using to_of_val.
asimpl.
rewrite CG_iter_subst. asimpl.
replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2)))
by (by rewrite CG_iter_of_val).
tp_snd j; auto using to_of_val.
tp_normalise j.
iModIntro.
iPoseProof "Hsl" as "Hsl'".
rewrite {2}StackLink_unfold.
iDestruct "Hsl'" as (zl w') "[% [Hzl Hsl']]". simplify_eq/=.
iSpecialize ("IH" $! zl z2).
iPoseProof (persistentP ((StackLink τi) (#zl, z2)) with "Hsl") as "Hsl_box".
iSpecialize ("IH" with "Hsl_box").
iSpecialize ("IH" with "Hj").
iApply wp_rec; auto. iNext. asimpl.
wp_bind (Snd _). iApply wp_snd; auto using to_of_val.
Qed.
Lemma FG_CG_push_refinement ρ st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ}:
spec_ctx ρ -∗ inv stackN (sinv τi st st' l) -∗
⟦ TArrow (TVar 0) TUnit ⟧ (τi::Δ) (FG_pushV (#st)%E, (CG_locked_pushV #st' #l)%E).
Proof.
iIntros "#Hs #Hinv".
iAlways. iIntros ([v1 v2]) "#Hvv".
iIntros (j K) "Hj /=".
rewrite CG_locked_push_of_val.
iLöb as "IH".
iApply wp_rec; eauto using to_of_val. iNext.
asimpl.
wp_bind (Load #st)%E.
iApply wp_atomic; eauto.
iInv stackN as (istk v h) "[Hoe [Hst' [Hst [HLK Hl]]]]" "Hclose".
iModIntro. iApply (wp_load _ st 1 (FoldV #istk) with "Hst"). iNext.
iIntros "Hst".
close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]".
iApply wp_rec; eauto using to_of_val. iNext. asimpl.
wp_bind (ref (InjR _))%E.
iApply wp_alloc.
{ simpl. rewrite ?to_of_val /=. auto. } iNext. iIntros (istk') "Histk'".
wp_bind (CAS _ _ _). clear v h.
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.
iApply (wp_cas_suc with "Hst"); auto.
iNext. iIntros "Hst".
iMod (stack_owns_alloc with "[$Hoe $Histk']") as "[Hoe Histk']".
iMod ("Hclose" with "[HLK Hst Hoe Hl Hst' Histk']").
{ iNext. rewrite /sinv. iExists _,_,_.
iFrame.
rewrite (StackLink_unfold _ ((LocV istk'), _)).
iExists _, _. iSplitR; auto.
iFrame "Histk'".
iRight. iExists _, _, _, _. auto.
}
iModIntro. iApply wp_if_true. iNext.
iApply wp_value; eauto. iExists _; iSplitL; auto; simpl.
done.
* (* Case CAS fails *)
iApply (wp_cas_fail with "Hst"); auto.
congruence. iNext. iIntros "Hst".
close_sinv "Hclose" "[HLK Hst Hoe Hl Hst' Histk']".
iApply wp_if_false. iNext.
iApply "IH". iFrame.
Qed.
Lemma FG_CG_pop_refinement ρ st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ}:
spec_ctx ρ -∗ inv stackN (sinv τi st st' l) -∗
⟦ TArrow TUnit (TSum TUnit (TVar 0)) ⟧ (τi::Δ) (FG_popV (#st)%E, (CG_locked_popV #st' #l)%E).
Proof.
iIntros "#Hs #Hinv".
iAlways. iIntros ( [v1 v2] ) "[% %]". subst.
iIntros (j K) "Hj /="; simplify_eq/=.
rewrite CG_locked_pop_of_val FG_pop_of_val.
iLöb as "IH".
rewrite {2}(FG_pop_folding).
iApply wp_rec; first by auto using to_of_val. iNext.
rewrite -(FG_pop_folding #st)%E. asimpl.
wp_bind (Load _).
iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
iApply (wp_load with "Hst"). iNext. iIntros "Hst".
iPoseProof "HLK" as "HLK'".
(* 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]")
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.
iModIntro. iApply wp_rec; first auto using to_of_val. iNext. asimpl.
clear h.
wp_bind (Load _). iClear "HLK".
iInv stackN as (istk3 w h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]".
iApply (wp_load with "Histk"). iNext. iIntros "Histk".
iSpecialize ("HLoe" with "Histk").
close_sinv "Hclose" "[HLoe Hst' Hst HLK Hl]".
iApply wp_rec; first by auto. iNext. asimpl.
iApply wp_case_inl; auto. iNext.
iApply wp_value; auto.
iExists (InjLV ())%V. iFrame "Hj".
iLeft. iExists (_,_). iSplit; auto.
+ close_sinv "Hclose" "[Hoe Hst' Hst Hl]".
wp_bind (Unfold _). iApply wp_fold; first auto. iNext.
iApply wp_rec; first auto. iNext. asimpl.
wp_bind (Load _).
clear h.
iClear "HLK".
iInv stackN as (istk3 w' h) "[Hoe [Hst' [Hst [HLK Hl]]]]" "Hclose".
iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]".
iApply (wp_load with "Histk"). iNext; iIntros "Histk".
iSpecialize ("HLoe" with "Histk").
close_sinv "Hclose" "[HLoe Hl Hst Hst' HLK]".
iApply wp_rec; first auto using to_of_val. iNext. asimpl.
iDestruct "HLK'" as (y1 z1 y2 z2) "(% & % & Hτ & HLK2)"; subst.
simpl.
iApply wp_case_inr.
{ by rewrite /= ?to_of_val /=. } iNext.
asimpl.
wp_bind (Snd _).
iApply wp_snd; try by (rewrite /= to_of_val /=). iNext.
(* now to decide if CAS succeeds or not *)
iClear "HLK2". clear h. iModIntro.
wp_bind (CAS _ _ _).
iInv stackN as (istk w h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
(* deciding whether CAS will succeed or fail *)
destruct (decide (istk = istk2)) as [Heq|Hneq]; subst.
* (* CAS successful *)
iApply (wp_cas_suc with "Hst"); try by (rewrite /= ?to_of_val /=).
iNext. iIntros "Hst".
iPoseProof "HLK" as "HLK'".
rewrite {2}StackLink_unfold.
iDestruct "HLK'" as (? ?) "[% [Hmpt' HLK']]"; simplify_eq/=.
iDestruct (stack_mapstos_agree with "[$Hmpt $Hmpt']") as "%". subst.
iDestruct "HLK'" as "[[% %]|HLK']"; simplify_eq/=.
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]")
as "[Hj [Hst' Hl]]"; first solve_ndisj.
iMod ("Hclose" with "[-Hj]") as "_".
{ iNext.
iPoseProof "HLK''" as "HLK2".
rewrite {2}(StackLink_unfold _ (yn2, zn2)).
iDestruct "HLK2" as (yn2loc ?) "[% _]"; simplify_eq /=.
iExists _,_,_. iFrame. iFrame "HLK''". }
iModIntro.
iApply wp_if_true. iNext.
wp_bind (Fst _).
iApply wp_fst; try by (auto using to_of_val || rewrite /= ?to_of_val /=). iNext.
iModIntro.
iApply wp_value; try by rewrite /= ?to_of_val /=.
iExists (InjRV zn1). iFrame "Hj".
iRight. iExists (_,_). simpl. iSplit; auto.
* (* CAS fails *)
iApply (wp_cas_fail with "Hst"); try by (rewrite /= ?to_of_val /=).
congruence.
iNext. iIntros "Hst".
close_sinv "Hclose" "[-Hj]".
iApply wp_if_false. iNext.
by iApply "IH".
Qed.
(* ∀ α. (α → Unit) * (Unit → Unit + α) * ((α → Unit) → Unit) *)
Lemma FG_CG_counter_refinement :
[] ⊨ FG_stack ≤log≤ CG_stack : TForall (TProd (TProd
(TArrow (TVar 0) TUnit)
......@@ -22,36 +284,36 @@ Section Stack_refinement.
(* executing the preambles *)
iIntros (Δ [|??] ρ ?) "#[Hspec HΓ]"; iIntros (j K) "Hj"; last first.
{ iDestruct (interp_env_length with "HΓ") as %[=]. }
iClear "HΓ". cbn -[FG_stack CG_stack].
rewrite ?empty_env_subst /CG_stack /FG_stack.
iClear "HΓ". cbn -[FG_stack CG_stack].
rewrite ?empty_env_subst /CG_stack /FG_stack.
iApply wp_value; eauto.
iExists (TLamV _); iFrame "Hj".
clear j K. iAlways. iIntros (τi) "%". iIntros (j K) "Hj /=".
iMod (step_tlam _ _ j K with "[Hj]") as "Hj"; eauto.
iApply wp_tlam; iNext.
iMod (steps_newlock _ _ j (K ++ [AppRCtx (RecV _)]) with "[Hj]")
as (l) "[Hj Hl]"; eauto.
{ rewrite fill_app; simpl. iFrame "Hspec Hj"; trivial. }
rewrite fill_app; simpl.
iMod (step_rec _ _ j K with "[$Hj]") as "Hj"; eauto.
simpl.
rewrite CG_locked_push_subst CG_locked_pop_subst
CG_iter_subst CG_snap_subst. simpl. asimpl.
iMod (step_alloc _ _ j (K ++ [AppRCtx (RecV _)]) with "[Hj]")
as (stk') "[Hj Hstk']"; [| |rewrite fill_app; simpl; by iFrame|]; auto.
rewrite fill_app; simpl.
iMod (step_rec _ _ j K with "[$Hj]") as "Hj"; eauto.
simpl.
iExists (Λ: _)%V; iFrame "Hj".
fold (interp (TProd (TProd
(TArrow (TVar 0) TUnit)
(TArrow TUnit (TSum TUnit (TVar 0))))
(TArrow (TArrow (TVar 0) TUnit) TUnit))).
clear j K. iAlways. iIntros (τi) "%".
iIntros (j K) "Hj /=".
iApply fupd_wp.
tp_tlam j.
tp_bind j newlock.
iMod (steps_newlock with "[$Hj]") as (l') "[Hj Hl']"; eauto.
tp_normalise j.
tp_rec j.
tp_alloc j as stk' "Hstk'".
rewrite CG_locked_push_subst CG_locked_pop_subst
CG_iter_subst CG_snap_subst. simpl. asimpl.
iApply (wp_bind [AppRCtx (RecV _); AllocCtx; FoldCtx]);
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iApply wp_alloc; first done. iNext; iIntros (istk) "Histk".
iApply (wp_bind [AppRCtx (RecV _)]);
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iApply wp_alloc; first done. iNext; iIntros (stk) "Hstk".
simpl. iApply wp_rec; trivial. iNext. simpl.
rewrite FG_push_subst FG_pop_subst FG_iter_subst. simpl. asimpl.
tp_normalise j.
tp_rec j.
tp_normalise j. rewrite ?CG_locked_push_subst ?CG_locked_pop_subst
?CG_iter_subst ?CG_snap_subst. simpl. asimpl.
iApply wp_tlam. iNext.
wp_bind (ref (InjL _))%E. iApply wp_alloc; eauto. iNext. iIntros (l) "Hl".
wp_bind (ref _)%E. iApply wp_alloc; eauto. iNext. iIntros (stk) "Hstk".
iApply wp_rec; eauto. iNext.
simpl. rewrite FG_push_subst FG_pop_subst FG_iter_subst /=.
asimpl.
(* establishing the invariant *)
iMod (own_alloc (● (∅ : stackUR))) as (γ) "Hemp"; first done.
set (istkG := StackG _ _ γ).
......@@ -59,276 +321,54 @@ Section Stack_refinement.
change H1 with (@stack_inG _ istkG).
clearbody istkG. clear γ H1.
iAssert (@stack_owns _ istkG _ ∅) with "[Hemp]" as "Hoe".
{ rewrite /stack_owns big_sepM_empty. iFrame "Hemp"; trivial. }
iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe Hls]".
iAssert (StackLink τi (LocV istk, FoldV (InjLV UnitV))) with "[Hls]" as "HLK".
{ rewrite /stack_owns big_sepM_empty. eauto. }
iMod (stack_owns_alloc with "[$Hoe $Hl]") as "[Hoe Hls]".
iAssert (StackLink τi (#l, FoldV (InjLV UnitV))) with "[Hls]" as "HLK".
{ rewrite StackLink_unfold.
iExists _, _. iSplitR; simpl; trivial.
iFrame "Hls". iLeft. iSplit; trivial. }
iAssert ((∃ istk v h, (stack_owns h)
∗ stk' ↦ₛ v
∗ stk ↦ᵢ (FoldV (LocV istk))
∗ StackLink τi (LocV istk, v)
∗ l ↦ₛ (#♭v false)
)%I) with "[Hoe Hstk Hstk' HLK Hl]" as "Hinv".
{ iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl HLK". }
iMod (inv_alloc stackN with "[Hinv]") as "#Hinv"; trivial.
{ iNext; iExact "Hinv". }
clear istk.
iAssert (sinv τi stk stk' l') with "[Hoe Hstk Hstk' HLK Hl']" as "Hinv".
{ iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl' HLK". }
iMod (inv_alloc stackN with "[$Hinv]") as "#Hinv".
clear l.
Opaque stack_owns.
(* splitting *)
iApply wp_value; simpl; trivial.
iApply wp_value; first by eauto.
iExists (PairV (PairV (CG_locked_pushV _ _) (CG_locked_popV _ _)) (RecV _)).
simpl. rewrite CG_locked_push_of_val CG_locked_pop_of_val. iFrame "Hj".
simpl. rewrite CG_locked_push_of_val CG_locked_pop_of_val. iFrame "Hj".
iExists (_, _), (_, _); iSplit; eauto.
iSplit.
(* refinement of push and pop *)
- iExists (_, _), (_, _); iSplit; eauto. iSplit.
+ (* refinement of push *)
iAlways. clear j K. iIntros ( [v1 v2] ) "#Hrel". iIntros (j K) "Hj /=".
rewrite -(FG_push_folding (Loc stk)).
iLöb as "Hlat".
rewrite {2}(FG_push_folding (Loc stk)).
iApply wp_rec; auto using to_of_val.
iNext.
rewrite -(FG_push_folding (Loc stk)).
asimpl.
iApply (wp_bind [AppRCtx (RecV _)]);
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
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_rec; auto using to_of_val.
iNext. asimpl.
iApply (wp_bind [IfCtx _ _; CasRCtx (LocV _) (FoldV (LocV _));
FoldCtx]);
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iApply wp_alloc; simpl; trivial; [by rewrite to_of_val|].
iNext. iIntros (ltmp) "Hltmp".
iApply (wp_bind [IfCtx _ _]);
iApply wp_wand_l; iSplitR; [by iIntros (w) "$"|].
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.
{ rewrite CG_locked_push_of_val. by iFrame "Hspec Hstk' Hj". }
iApply (wp_cas_suc with "Hstk"); auto.
iNext. iIntros "Hstk".
iMod ("Hclose" with ">[-Hj]") as "_".
{ iMod (stack_owns_alloc with "[$Hoe $Hltmp]") as "[Hoe Hpt]".
iModIntro. iNext. iExists ltmp, _, _.
iFrame "Hoe Hstk' Hstk Hl".
do 2 rewrite StackLink_unfold.
rewrite -StackLink_unfold.
iExists _, _. iSplit; trivial.
iFrame "Hpt". eauto 10. }
iModIntro.
iApply wp_if_true. iNext; iApply wp_value; trivial.
iExists UnitV; eauto.
* iApply (wp_cas_fail with "Hstk"); auto. congruence.
iNext. iIntros "Hstk". iMod ("Hclose" with "[-Hj]").
{ iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
iApply wp_if_false. iNext. by iApply "Hlat".
+ (* refinement of pop *)
iAlways. clear j K. iIntros ( [v1 v2] ) "[% %]".
iIntros (j K) "Hj /="; simplify_eq/=.
rewrite -(FG_pop_folding (Loc stk)).
iLöb as "Hlat".
rewrite {2}(FG_pop_folding (Loc stk)).
iApply wp_rec; auto using to_of_val.
iNext.
rewrite -(FG_pop_folding (Loc stk)).
asimpl.
iApply (wp_bind [AppRCtx (RecV _); UnfoldCtx]);
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iInv stackN as (istk v h) "[Hoe [Hstk' [Hstk [#HLK Hl]]]]" "Hclose".
iApply (wp_load with "Hstk"). iNext. iIntros "Hstk".
iPoseProof "HLK" as "HLK'".
(* Checking whether the stack is empty *)
rewrite {2}StackLink_unfold.
iDestruct "HLK'" as (istk2 w) "[% [Hmpt [[% %]|HLK']]]"; simplify_eq/=.
* (* The stack is empty *)
iMod (steps_CG_locked_pop_fail with "[$Hspec $Hstk' $Hl $Hj]")
as "[Hj [Hstk' Hl]]"; first solve_ndisj.
iMod ("Hclose" with "[-Hj Hmpt]") as "_".
{ iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
iApply (wp_bind [AppRCtx (RecV _)]);
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iApply wp_fold; simpl; auto using to_of_val.
iNext. iModIntro. iApply wp_rec; auto using to_of_val. iNext. asimpl.
clear h.
iApply (wp_bind [AppRCtx (RecV _)]);
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
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]".
iApply (wp_load with "Histk").
iNext. iIntros "Histk". iMod ("Hclose" with "[-Hj]") as "_".
{ iNext. iExists _, _, _. iFrame "Hstk' Hstk HLK Hl".
by iApply "HLoe". }
iApply wp_rec; simpl; trivial.
iNext. asimpl.
iApply wp_case_inl; trivial.
iNext. iApply wp_value; simpl; trivial. iExists (InjLV UnitV).
iSplit; trivial. iLeft. iExists (_, _); repeat iSplit; simpl; trivial.
* (* The stack is not empty *)
iMod ("Hclose" with "[-Hj Hmpt HLK']") as "_".
{ iNext. iExists _, _, _. by iFrame "Hstk' Hstk HLK Hl". }
iApply (wp_bind [AppRCtx (RecV _)]);
iApply wp_wand_l; iSplitR; [iIntros (w') "Hw"; iExact "Hw"|].
iApply wp_fold; simpl; auto using to_of_val.
iNext. iApply wp_rec; auto using to_of_val. iNext. asimpl.
clear h.
iApply (wp_bind [AppRCtx (RecV _)]);
iApply wp_wand_l; iSplitR; [iIntros (w') "Hw"; iExact "Hw"|].
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]".
iApply (wp_load with "Histk"). iNext; iIntros "Histk".
iDestruct ("HLoe" with "Histk") as "Hh".
iMod ("Hclose" with "[-Hj Hmpt HLK']") as "_".
{ iNext. iExists _, _, _. by iFrame "Hstk' Hstk HLK Hl". }
iApply wp_rec; auto using to_of_val.
iNext. asimpl.
iDestruct "HLK'" as (y1 z1 y2 z2) "[% HLK']". subst. simpl.
iApply wp_case_inr; [simpl; by rewrite ?to_of_val |].
iNext.
iApply (wp_bind [IfCtx _ _; CasRCtx (LocV _) (FoldV (LocV _))]);
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
asimpl. iApply wp_snd; [simpl; by rewrite ?to_of_val |
simpl; by rewrite ?to_of_val |].
simpl. iNext. iModIntro.
iApply (wp_bind [IfCtx _ _]);
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
clear istk3 h. asimpl.
iInv stackN as (istk3 w h) "[Hoe [Hstk' [Hstk [#HLK Hl]]]]" "Hclose".
(* deciding whether CAS will succeed or fail *)
destruct (decide (istk2 = istk3)) as [|Hneq]; subst.
-- (* CAS succeeds *)
(* In this case, the specification pushes *)
iApply (wp_cas_suc with "Hstk"); simpl; auto. by rewrite to_of_val.
iNext. iIntros "Hstk {HLK'}". iPoseProof "HLK" as "HLK'".
rewrite {2}StackLink_unfold.
iDestruct "HLK'" as (istk4 w2) "[% [Hmpt' HLK']]"; simplify_eq/=.
iDestruct (stack_mapstos_agree with "[$Hmpt $Hmpt']") as %?.
iDestruct "HLK'" as "[[% %]|HLK']"; simplify_eq/=.
iDestruct "HLK'" as (yn1 yn2 zn1 zn2)
"[% [% [#Hrel HLK'']]]"; simplify_eq/=.
(* Now we have proven that specification can also pop. *)
rewrite CG_locked_pop_of_val.
iMod (steps_CG_locked_pop_suc with "[$Hspec $Hstk' $Hl $Hj]")
as "[Hj [Hstk' Hl]]"; first solve_ndisj.
iMod ("Hclose" with "[-Hj]") as "_".
{ iNext. iIntros "{Hmpt Hmpt' HLK}". rewrite StackLink_unfold.
iDestruct "HLK''" as (istk5 w2) "[% [Hmpt HLK]]"; simplify_eq/=.
iExists istk5, _, _. iFrame "Hoe Hstk' Hstk Hl".
rewrite StackLink_unfold.
iExists _, _; iSplitR; trivial.
by iFrame "HLK". }
iApply wp_if_true. iNext.
iApply (wp_bind [InjRCtx]); iApply wp_wand_l;
iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iApply wp_fst; [simpl; by rewrite ?to_of_val |
simpl; by rewrite ?to_of_val |].
iNext. iModIntro. iApply wp_value; simpl.
{ by rewrite to_of_val. }
iExists (InjRV _); iFrame "Hj".
iRight. iExists (_, _). iSplit; trivial.
-- (* CAS will fail *)
iApply (wp_cas_fail with "Hstk"); [rewrite /= ?to_of_val //; congruence..|].
iNext. iIntros "Hstk". iMod ("Hclose" with "[-Hj]") as "_".
{ iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk HLK Hl". }
iApply wp_if_false. iNext. by iApply "Hlat".
- (* refinement of iter *)
iAlways. clear j K. iIntros ( [f1 f2] ) "/= #Hfs". iIntros (j K) "Hj".
iApply wp_rec; auto using to_of_val. iNext.
iMod (step_rec with "[$Hspec $Hj]") as "Hj"; [by rewrite to_of_val|solve_ndisj|].
asimpl. rewrite FG_iter_subst CG_snap_subst CG_iter_subst. asimpl.
replace (FG_iter (of_val f1)) with (of_val (FG_iterV (of_val f1)))
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 [AppRCtx _]); iApply wp_wand_l;
iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iInv stackN as (istk3 w h) "[Hoe [>Hstk' [>Hstk [#HLK >Hl]]]]" "Hclose".
iMod (steps_CG_snap _ _ _ (K ++ [AppRCtx _])
with "[Hstk' Hj Hl]") as "[Hj [Hstk' Hl]]"; first solve_ndisj.
{ rewrite ?fill_app. simpl. by iFrame "Hspec Hstk' Hl Hj". }