Skip to content

GitLab

R
ReLoC-v1
Commit 2961c9a7 authored by Dan Frumin's avatar Dan Frumin
Browse files
Options

Port the stack refinement example

parent ef040112
Hide whitespace changes
Inline Side-by-side
Showing with 303 additions and 387 deletions
F_mu_ref_conc/examples/stack/CG_stack.v
View file @ 2961c9a7
......@@ -30,7 +30,7 @@ Definition CG_pop : val := λ: "st" <>,
Definition CG_locked_pop : val := λ: "st" "l" <>,
acquire "l";; (let: "v" := CG_pop "st" #() in (release "l";; "v")).
acquire "l";; (let: "v" := CG_pop "st" () in (release "l";; "v")).
(* snap st l = with_lock (λ _, load st) l *)
Definition CG_snap : val := λ: "st" "l" <>,
......@@ -66,7 +66,7 @@ Definition CG_stack : val :=
CG_stack_body "st" "l".
Section CG_Stack.
Context `{heapIG Σ, cfgSG Σ}.
Context `{logrelG Σ}.
Lemma CG_push_type Γ τ :
typed Γ CG_push (TArrow (Tref (CG_StackType τ)) (TArrow τ TUnit)).
......
F_mu_ref_conc/examples/stack/FG_stack.v
View file @ 2961c9a7
......@@ -10,7 +10,7 @@ Notation Nile := (Fold (Alloc (InjL Unit))).
Definition FG_push : val := rec: "push" "st" := λ: "x",
let: "stv" := !"st" in
if: (CAS "st" "stv" (Conse "x" "stv"))
then #()
then ()
else "push" "st" "x".
......@@ -28,11 +28,11 @@ Definition FG_pop : val := rec: "pop" "st" := λ: <>,
let: "stv" := !"st" in
let: "x" := !(Unfold "stv") in
case: "x" of
InjL => λ: <>, InjL #()
InjL => λ: <>, InjL ()
| InjR => λ: "x", let: "y" := Fst "x" in let: "ys" := Snd "x" in
if: (CAS "st" "stv" "ys")
then (InjR "y")
else "pop" "st" #()
else "pop" "st" ()
end.
(* iter f = λ st.
......@@ -41,7 +41,7 @@ Definition FG_pop : val := rec: "pop" "st" := λ: <>,
| cons y ys => f y ;; iter f ys *)
Definition FG_iter : val := rec: "iter" "f" := λ: "st",
case: !(Unfold "st") of
InjL => λ: <>, #()
InjL => λ: <>, ()
| InjR => λ: "x",
let: "y" := Fst "x" in
let: "ys" := Snd "x" in
......
F_mu_ref_conc/examples/stack/refinement.v
View file @ 2961c9a7
......@@ -8,7 +8,7 @@ From iris_logrel.F_mu_ref_conc.examples.stack Require Import
Definition stackN : namespace := nroot .@ "stack".
Section Stack_refinement.
Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}.
Context `{logrelG Σ, stackG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types Δ : listC D.
Import lang.
......@@ -24,41 +24,41 @@ Section Stack_refinement.
iMod (Hcl with asn) as "_";
[iNext; rewrite /sinv; iExists _,_,_; by iFrame |]; try iModIntro.
Lemma FG_CG_push_refinement ρ st st' (τi : D) (v v' : val) l {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ} Γ :
spec_ctx ρ -∗ inv stackN (sinv τi st st' l) -∗ τi (v,v') -∗
Lemma FG_CG_push_refinement st st' (τi : D) (v v' : val) l {τP : ∀ ww, PersistentP (τi ww)} Γ :
inv stackN (sinv τi st st' l) -∗ τi (v,v') -∗
Γ ⊨ ((FG_push $/ (LocV st)) v)%E ≤log≤ ((CG_locked_push $/ (LocV st') $/ (LocV l)) v')%E : TUnit.
Proof.
iIntros "#Hs #Hinv #Hvv'".
iIntros "#Hinv #Hvv'". iIntros (Δ).
Transparent FG_push.
unfold CG_locked_push. unlock. simpl_subst/=.
rel_rec_r.
unfold FG_push. unlock. simpl_subst/=.
iLöb as "IH".
rel_rec_l.
rel_load_l under stackN as "Hst" "Hclose". simpl.
iDestruct "Hst" as (istk w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]".
iExists (FoldV #istk). iFrame.
iModIntro. iNext. iIntros "Hst".
rel_load_l_atomic.
iInv stackN as (istk w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".
iExists (FoldV #istk). iFrame.
iModIntro. iNext. iIntros "Hst".
close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
rel_rec_l.
rel_alloc_l as nstk "Hnstk". solve_to_val. (* TODO: rel_tactics *) simpl.
rel_cas_l under stackN as "Hst" "Hclose". simpl.
iDestruct "Hst" as (istk' w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]".
iExists (FoldV #istk'). iFrame.
iModIntro.
rel_alloc_l as nstk "Hnstk". simpl.
rel_cas_l_atomic.
iInv stackN as (istk' w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".
iExists (FoldV #istk'). iFrame.
iModIntro.
destruct (decide (istk' = istk)) as [e | nestk]; subst.
- (* CAS succeeds *) iRight.
iSplitR; first done.
iNext. iIntros "Hst".
rel_bind_r (acquire #l)%E. iApply (bin_log_related_acquire_r with "Hl").
- (* CAS succeeds *)
iSplitR; first by iIntros ([]).
iIntros (?). iNext. iIntros "Hst".
rel_apply_r (bin_log_related_acquire_r with "Hl").
{ solve_ndisj. }
iIntros "Hl /=".
rel_rec_r.
unfold CG_push. unlock. do 2 rel_rec_r.
rel_load_r.
rel_store_r. solve_to_val. (* TODO rel_tactics *) simpl.
rel_store_r.
rel_rec_r.
rel_bind_r (release #l)%E. iApply (bin_log_related_release_r with "Hl").
rel_apply_r (bin_log_related_release_r with "Hl").
{ solve_ndisj. }
iIntros "Hl /=".
iApply fupd_logrel'. (* TODO iMod should pick this up on its own *)
......@@ -71,426 +71,342 @@ Section Stack_refinement.
iExists _, _. iSplitR; auto.
iFrame "Hnstk".
iRight. iExists _, _, _, _. auto. }
rel_if_true_l. simpl.
rel_if_true_l.
by rel_vals.
- (* CAS fails *) iLeft.
iSplitR; first by (iPureIntro; congruence).
iNext. iIntros "Hst".
- (* CAS fails *)
iSplitL; last by (iIntros (?); congruence).
iIntros (?); iNext; iIntros "Hst".
close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
rel_if_false_l. simpl.
rel_rec_l.
by iApply "IH".
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) -∗
Γ ⊨ (FG_pop $/ LocV st)%E ≤log≤ (CG_locked_pop $/ LocV st' $/ LocV l)%E : TArrow TUnit (TSum TUnit (TVar 0)).
Lemma FG_CG_pop_refinement st st' (τi : D) l {τP : ∀ ww, PersistentP (τi ww)} Δ Γ :
inv stackN (sinv τi st st' l) -∗
{⊤,⊤;τi::Δ;Γ} ⊨ (FG_pop $/ LocV st)%E ≤log≤ (CG_locked_pop $/ LocV st' $/ LocV l)%E : TArrow TUnit (TSum TUnit (TVar 0)).
Proof.
iIntros "#Hs #Hinv".
Transparent CG_locked_pop FG_pop.
unfold FG_pop. unfold CG_locked_pop. unlock.
iIntros "#Hinv".
Transparent CG_locked_pop FG_pop CG_pop.
unfold FG_pop, CG_locked_pop. unlock.
simpl_subst/=.
iApply bin_log_related_arrow; eauto.
iAlways. iIntros (Δ ?) "_".
iApply bin_log_related_arrow; eauto.
iAlways. iIntros ([? ?]) "[% %]". simplify_eq/=.
rel_rec_r.
rel_rec_l.
iLöb as "IH".
rel_load_l under stackN as "Hst" "Hclose".
iDestruct "Hst" as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]".
iExists _. iFrame.
iModIntro. iNext. iIntros "Hst /=".
rel_load_l_atomic.
iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
iExists _. iFrame.
iModIntro. iNext. iIntros "Hst /=".
rel_rec_l.
rel_unfold_l.
iPoseProof "HLK" as "HLK'".
Transparent CG_pop.
rewrite {1}StackLink_unfold.
iDestruct "HLK" as (istk''' w) "(% & Histk & HLK)". simplify_eq/=.
iDestruct "HLK" as "[[% %] | HLK]".
- (* The stack is empty *) simplify_eq/=.
rel_bind_r (acquire #l)%E. iApply (bin_log_related_acquire_r with "Hl").
iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
- (* The stack is empty *)
rel_apply_r (bin_log_related_acquire_r with "Hl").
{ solve_ndisj. }
iIntros "Hl /=".
unfold CG_pop. unlock.
rel_rec_r.
rel_rec_r.
rel_rec_r.
repeat rel_rec_r.
rel_load_r.
rel_fold_r.
rel_case_inl_r.
rel_rec_r.
rel_rec_r.
rel_bind_r (release #l)%E. iApply (bin_log_related_release_r with "Hl").
rel_case_r.
repeat rel_rec_r.
rel_apply_r (bin_log_related_release_r with "Hl").
{ solve_ndisj. }
iIntros "Hl /=".
rel_rec_r.
close_sinv "Hclose" "[Hoe Hst' Hst Hl]". clear h.
rel_rec_l.
rel_unfold_l. simpl.
rel_load_l under stackN as "Hst" "Hclose".
iDestruct "Hst" as (istk2 v2 h) "[Hoe [Hst' [Hst [HLK2 Hl]]]]".
iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i HLoe]".
iExists _. iFrame "Histk_i".
iModIntro. iNext. iIntros "Histk_i /=".
iSpecialize ("HLoe" with "Histk_i").
close_sinv "Hclose" "[HLoe Hst' Hst Hl HLK2]". clear h.
close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear h. iClear "HLK'".
rel_load_l_atomic.
iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
iExists _. iFrame "Histk_i".
iModIntro. iNext. iIntros "Histk_i /=".
iSpecialize ("Hoe" with "Histk_i").
rel_rec_l.
rel_case_inl_l. simpl.
rel_case_l.
rel_rec_l.
iApply bin_log_related_injl; eauto.
by rel_vals.
close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".
rel_vals.
{ iModIntro. iLeft. iExists (_,_). eauto. }
- (* The stack has a value *)
iDestruct "HLK" as (y1 z1 y2 z2) "(% & % & Hτ & HLK_tail)"; simplify_eq/=.
close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear.
rel_rec_l.
rel_unfold_l. simpl.
rel_load_l under stackN as "Hst" "Hclose".
iDestruct "Hst" as (istk v h) "[Hoe [Hst' [Hst [HLK Hl]]]]".
iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk' HLoe]".
iExists _. iFrame.
iModIntro. iNext. iIntros "Histk' /=".
iSpecialize ("HLoe" with "Histk'").
close_sinv "Hclose" "[HLoe Hst' Hst Hl HLK]". clear.
rel_rec_l.
rel_case_inr_l. simpl.
rel_rec_l.
rel_fst_l. simpl.
close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear h.
rel_load_l_atomic.
iInv stackN as (istk v h) "[Hoe [Hst' [Hst [HLK Hl]]]]" "Hclose".
iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
iExists _. iFrame.
iModIntro. iNext. iIntros "Histk_i /=".
iSpecialize ("Hoe" with "Histk_i").
rel_rec_l.
rel_snd_l. simpl.
rel_case_l.
rel_rec_l.
rel_cas_l under stackN as "Hst" "Hclose".
solve_to_val. (* TODO rel_tactics *)
iDestruct "Hst" as (istk2 v2 h) "[Hoe [Hst' [Hst [HLK2 Hl]]]]".
iExists _. iFrame.
iModIntro.
destruct (decide (istk2 = istk''')) as [? |NE]; simplify_eq/=.
+ (* CAS succeeds *) iRight.
iSplitR; eauto.
iNext. iIntros "Hst".
rel_bind_r (acquire #l)%E. iApply (bin_log_related_acquire_r with "Hl").
do 2 (rel_proj_l; rel_rec_l).
close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]". clear h istk v.
rel_cas_l_atomic.
iInv stackN as (istk v h) "[Hoe [Hst' [Hst [HLK2 Hl]]]]" "Hclose".
iExists _. iFrame.
iModIntro.
destruct (decide (istk = istk2)) as [? |NE]; simplify_eq/=.
+ (* CAS succeeds *)
iSplitR; first by (iIntros (?); contradiction).
iIntros "%". iNext. iIntros "Hst".
rel_if_l.
rewrite (StackLink_unfold _ (#istk2, v)).
iDestruct "HLK2" as (istk2' v') "[% [#Histk' HLK2]]"; simplify_eq/=.
iDestruct (stack_mapstos_agree with "Histk Histk'") as "%"; simplify_eq/=.
iDestruct "HLK2" as "[[% %]|HLK2]"; simplify_eq/=.
iDestruct "HLK2" as (ym1 ym2 zm1 zm2)
"[% [% [#Hrel #HLK2_tail]]]"; simplify_eq/=.
rel_apply_r (bin_log_related_acquire_r with "Hl").
{ solve_ndisj. }
iIntros "Hl /=".
rel_rec_r.
unfold CG_pop. unlock.
rel_rec_r.
rel_rec_r.
repeat rel_rec_r.
rel_load_r.
rewrite (StackLink_unfold _ (#istk''', v2)).
iDestruct "HLK2" as (? ?) "[% [Hmpt2 HLK2]]"; simplify_eq/=.
iDestruct (stack_mapstos_agree with "Histk Hmpt2") as "%"; simplify_eq/=.
iDestruct "HLK2" as "[[% %]|HLK2]"; simplify_eq/=.
iDestruct "HLK2" as (ym1 ym2 zm1 zm2)
"[% [% [Hrel HLK2_tail]]]"; simplify_eq/=.
rel_fold_r. solve_to_val. (* TODO rel_tactics *)
rel_case_inr_r. solve_to_val. (* TODO rel_tactics *)
rel_fold_r.
rel_case_r.
rel_rec_r.
rel_snd_r; try solve_to_val. (* TODO rel_tactics *)
rel_store_r. solve_to_val. (* TODO rel_tactics *) simpl.
rel_proj_r.
rel_store_r.
rel_rec_r.
rel_fst_r; [ solve_to_val | solve_to_val | ].
rel_proj_r.
rel_rec_r.
rel_bind_r (release #l)%E. iApply (bin_log_related_release_r with "Hl").
rel_apply_r (bin_log_related_release_r with "Hl").
{ solve_ndisj. }
iIntros "Hl /=".
rel_rec_r.
iMod ("Hclose" with "[-]").
{ iNext. rewrite /sinv.
iPoseProof "HLK2_tail" as "HLK2z".
rewrite (StackLink_unfold _ (ym2, z2)).
iDestruct "HLK_tail" as (yn2loc ?) "[% _]"; simplify_eq /=.
iExists _,_,_. iFrame. }
rel_if_true_l. simpl.
iApply bin_log_related_injr; eauto.
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/=.
+ tp_apply j steps_CG_locked_pop_fail with "Hst' Hl" as "[Hstk' Hl]".
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. *)
tp_apply j steps_CG_locked_pop_suc with "Hst' Hl"
as "[Hst' Hl]".
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 iMod ("IH" with "Hj").
iExists _,_,_. by iFrame. }
rel_vals.
{ iModIntro. iRight.
iExists (_,_). eauto. }
+ (* CAS fails *)
iSplitL; last by (iIntros (?); congruence).
iIntros (?). iNext. iIntros "Hst".
rel_if_l.
close_sinv "Hclose" "[-]".
do 2 rel_rec_l.
iApply "IH".
Qed.
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::Δ)
(lamsubst FG_read_iter (LocV st)
, lamsubst (lamsubst CG_snap_iter (LocV st')) (LocV l)).
Lemma FG_CG_iter_refinement st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ} Γ:
inv stackN (sinv τi st st' l) -∗
{⊤,⊤;τi::Δ;Γ} ⊨ (FG_read_iter $/ LocV st)%E ≤log≤ (CG_snap_iter $/ LocV st' $/ LocV l)%E : TArrow (TArrow (TVar 0) TUnit) TUnit.
Proof.
iIntros "#Hs #Hinv".
iIntros (j K) "Hj /=".
unfold CG_snap_iter, FG_read_iter.
Transparent CG_iter. Transparent FG_iter.
unfold CG_iter, FG_iter. unlock. simpl.
iApply wp_value; auto.
{ simpl. rewrite decide_left. done. }
iModIntro. iExists (RecV _ _ _). simpl. iFrame "Hj".
clear j K.
iAlways. iIntros ([f1 f2]). iIntros "#Hff /=".
iIntros (j K) "Hj /=".
iApply wp_rec; eauto using to_of_val.
{ solve_closed. }
iModIntro. iNext. simpl.
wp_bind (Load #st)%E.
iIntros "#Hinv".
Transparent FG_read_iter CG_snap_iter.
unfold FG_read_iter, CG_snap_iter. unlock.
simpl_subst/=.
iApply bin_log_related_arrow; eauto.
iAlways. iIntros ([f1 f2]) "#Hff".
rel_rec_r.
rel_rec_l.
Transparent FG_iter CG_iter. unlock FG_iter CG_iter.
rel_rec_l.
rel_rec_r.
Transparent CG_snap. unlock CG_snap.
rel_rec_r.
rel_rec_r.
rel_rec_r.
rel_load_l_atomic.
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.
Opaque coPset_difference.
asimpl.
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.
tp_apply j steps_CG_snap with "Hst' Hl" as "[Hst' Hl]".
tp_normalise j.
close_sinv "Hclose" "[Hoe Hst' Hst HLK Hl]".
iExists _. iFrame.
iModIntro. iNext. iIntros "Hst /=".
rel_apply_r (bin_log_related_acquire_r with "Hl").
{ solve_ndisj. }
iIntros "Hl /=".
rel_rec_r.
rel_load_r.
rel_rec_r.
rel_apply_r (bin_log_related_release_r with "Hl").
{ solve_ndisj. }
iIntros "Hl /=".
rel_rec_r.
close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]". clear h.
iLöb as "IH" forall (istk v) "HLK".
rel_rec_l.
rel_unfold_l.
rel_rec_r.
iPoseProof "HLK" as "HLK'".
rewrite {1}StackLink_unfold.
iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
- (* The stack is empty *)
rel_fold_r.
rel_case_r.
rel_rec_r.
iApply wp_rec; auto. iNext. asimpl.
wp_bind (Unfold _). iApply wp_fold; auto. iNext.
iModIntro. wp_bind (Load _).
rel_load_l_atomic.
iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
iExists _. iFrame "Histk_i".
iModIntro. iNext. iIntros "Histk_i /=".
iSpecialize ("Hoe" with "Histk_i").
rel_case_l.
rel_rec_l.
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 /=.
tp_apply j steps_CG_iter_end.
iModIntro.
iApply wp_value; auto.
iExists UnitV. iFrame. eauto.
+ iDestruct "HLK" as (y1 z1 y2 z2) "[% [% [Hy Hsl]]]". subst.
close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]". iClear "HLK".
by rel_vals.
- (* The stack has a value *)
iDestruct "HLK" as (y1 z1 y2 z2) "(% & % & Hτ & HLK_tail)"; simplify_eq/=.
rel_fold_r.
rel_case_r.
rel_rec_r.
rel_fst_r.
rel_load_l_atomic.
iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
iExists _. iFrame "Histk_i".
iModIntro. iNext. iIntros "Histk_i /=".
iSpecialize ("Hoe" with "Histk_i").
rel_case_l.
rel_rec_l.
rel_fst_l.
rel_rec_l.
rel_snd_l.
rel_rec_l.
close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".
iSpecialize ("Hff" $! (y1,y2) with "Hτ").
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.
tp_apply j steps_CG_iter.
rewrite CG_iter_subst.
tp_bind j (App (of_val f2) _).
iSpecialize ("Hff" $! (y1, y2) with "[Hy]"); first by iFrame.
iSpecialize ("Hff" $! j (K ++ _) with "Hj"). simpl.
iApply fupd_wp. iMod "Hff". iModIntro.
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)))