Commit bf38948f authored by Dan Frumin's avatar Dan Frumin

Simplify the Treiber stack refinement

The simplification is acheieved by removing the stackUR workaround.
That RA was used to enusure that the nodes that were parts of the
stack do not change themselves -- this is crucial for the safety of
pop and iter operations.

Now this is achieved by using duplicable propositions (∃ q, n ↦ᵢ{q} v)
to ensure that the node are still alive/not freed.
parent 3792938d
......@@ -32,7 +32,6 @@ theories/examples/counter.v
theories/examples/lateearlychoice.v
theories/examples/par.v
theories/examples/bit.v
theories/examples/stack/stack_rules.v
theories/examples/stack/CG_stack.v
theories/examples/stack/FG_stack.v
theories/examples/stack/refinement.v
......@@ -52,4 +51,4 @@ theories/tests/tactics2.v
theories/tests/liftings.v
theories/tests/value.v
theories/examples/coqpl.v
theories/examples/brouwers.v
\ No newline at end of file
theories/examples/brouwers.v
From iris.proofmode Require Import tactics.
From iris_logrel Require Import logrel.
From iris_logrel.examples.stack Require Import
CG_stack FG_stack stack_rules refinement.
CG_stack FG_stack refinement.
Section Mod_refinement.
Context `{HLR : logrelG Σ}.
......@@ -9,15 +9,15 @@ Section Mod_refinement.
Implicit Types Δ : listC D.
Import lang.
Program Definition sint {LG : logrelG Σ} {Z : stackPreG Σ} τi : prodC valC valC -n> iProp Σ := λne vv,
( γ (l stk stk' : loc), (vv.2) = (#stk', #l)%V (vv.1) = #stk
inv (stackN .@ (stk,stk')) (sinv' γ τi stk stk' l))%I.
Program Definition sint τi : prodC valC valC -n> iProp Σ := λne vv,
( (l stk stk' : loc), (vv.2) = (#stk', #l)%V (vv.1) = #stk
inv (stackN .@ (stk,stk')) (sinv τi stk stk' l))%I.
Solve Obligations with solve_proper.
Instance sint_persistent `{logrelG Σ, stackPreG Σ} τi vv : Persistent (sint τi vv).
Instance sint_persistent τi vv : Persistent (sint τi vv).
Proof. apply _. Qed.
Lemma module_refinement `{SPG : stackPreG Σ} Δ Γ :
Lemma module_refinement Δ Γ :
{Δ;Γ} FG_stack.stackmod log CG_stack.stackmod : TForall $ TExists $ TProd (TProd
(TArrow TUnit (TVar 0))
(TArrow (TVar 0) (TSum TUnit (TVar 1))))
......@@ -40,25 +40,16 @@ Section Mod_refinement.
rel_alloc_r as l "Hl".
rel_vals.
rewrite -persistent.
iMod (own_alloc ( ( : stackUR))) as (γ) "Hemp"; first done.
pose (SG := StackG Σ _ γ).
iAssert (prestack_owns γ ) with "[Hemp]" as "Hoe".
{ rewrite /prestack_owns big_sepM_empty fmap_empty.
iFrame "Hemp". }
iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
iAssert (preStackLink γ τi (#istk, FoldV (InjLV #()))) with "[Histk]" as "#HLK".
{ rewrite preStackLink_unfold.
iExists _, _. iSplitR; simpl; trivial.
iFrame "Histk". iLeft. iSplit; trivial. }
iAssert (sinv' γ τi stk stk' l) with "[Hoe Hstk Hstk' HLK Hl]" as "Hinv".
{ iExists _, _, _. by iFrame. }
iAssert (sinv τi stk stk' l) with "[-]" as "Hinv".
{ iExists _,_. iFrame.
rewrite stack_link_unfold. iExists _; iSplitL; eauto. }
iMod (inv_alloc (stackN.@(stk,stk')) with "[Hinv]") as "#Hinv".
{ iNext. iExact "Hinv". }
iModIntro.
iExists γ, l, stk, stk'. eauto.
iExists l, stk, stk'. eauto.
- iApply bin_log_related_arrow_val; eauto.
iAlways. iIntros (? ?) "#Hvv /=".
iDestruct "Hvv" as (γ l stk stk') "(% & % & #Hinv)".
iDestruct "Hvv" as (l stk stk') "(% & % & #Hinv)".
simplify_eq/=.
rel_let_l.
rel_let_r.
......@@ -73,15 +64,12 @@ Section Mod_refinement.
replace (TSum TUnit (TVar 1))
with (TSum TUnit (TVar 0)).[ren (+1)] by done.
iApply bin_log_related_weaken_2.
pose (SG := StackG Σ _ γ).
change γ with stack_name.
iApply (FG_CG_pop_refinement' (stackN.@(stk,stk'))).
{ solve_ndisj. }
by rewrite sinv_unfold.
iApply (FG_CG_pop_refinement' (stackN.@(stk,stk')) with "Hinv").
solve_ndisj.
- iApply bin_log_related_arrow_val; eauto.
{ unlock FG_push. done. }
iAlways. iIntros (? ?) "#Hvv /=".
iDestruct "Hvv" as (γ l stk stk') "(% & % & #Hinv)".
iDestruct "Hvv" as (l stk stk') "(% & % & #Hinv)".
simplify_eq/=.
rel_let_r.
Transparent FG_push.
......@@ -98,11 +86,8 @@ Section Mod_refinement.
with ((CG_locked_push $/ LitV stk' $/ LitV l) v')%E; last first.
{ unlock CG_locked_push. simpl_subst/=. done. }
change TUnit with (TUnit.[ren (+1)]).
pose (SG := StackG Σ _ γ).
change γ with stack_name.
iApply (FG_CG_push_refinement (stackN.@(stk,stk')) with "[Hinv] Hτi").
{ solve_ndisj. }
by rewrite sinv_unfold.
iApply (FG_CG_push_refinement (stackN.@(stk,stk')) with "Hinv Hτi").
solve_ndisj.
Qed.
End Mod_refinement.
......@@ -113,7 +98,6 @@ Theorem module_ctx_refinement :
(TArrow (TVar 0) (TSum TUnit (TVar 1))))
(TArrow (TVar 0) (TArrow (TVar 1) TUnit)).
Proof.
set (Σ := #[logrelΣ; GFunctor (authR stackUR)]).
eapply (logrel_ctxequiv Σ); [solve_closed.. | intros ].
eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
apply module_refinement.
Qed.
From iris.proofmode Require Import tactics.
From iris_logrel Require Import logrel.
From iris_logrel.examples.stack Require Import
CG_stack FG_stack stack_rules.
From iris_logrel.examples.stack Require Import CG_stack FG_stack.
Definition stackN : namespace := nroot .@ "stack".
......@@ -11,32 +10,81 @@ Section Stack_refinement.
Implicit Types Δ : listC D.
Import lang.
Definition sinv' {SPG : authG Σ stackUR} γ τi stk stk' l' : iProp Σ :=
( (istk : loc) v h, (prestack_owns γ h)
stk' ↦ₛ v
stk ↦ᵢ (FoldV #istk)
preStackLink γ τi (#istk, v)
l' ↦ₛ #false)%I.
Notation DD := (prodC locC valC -n> iProp Σ).
Context `{stackG Σ}.
Definition sinv τi stk stk' l : iProp Σ :=
( (istk : loc) v h, (stack_owns h)
stk' ↦ₛ v
stk ↦ᵢ (FoldV #istk)
StackLink τi (#istk, v)
l ↦ₛ #false)%I.
Lemma sinv_unfold τi stk stk' l :
sinv τi stk stk' l = sinv' stack_name τi stk stk' l.
Proof. reflexivity. Qed.
(** The "partial pointsto" proposition is duplicable *)
Local Instance istk_fromand (istk : loc) (w : val) :
FromAnd false ( q, istk ↦ᵢ{q} w) ( q, istk ↦ᵢ{q} w) ( q, istk ↦ᵢ{q} w).
Proof.
rewrite /FromAnd. iIntros "[H1 H2]".
iDestruct "H1" as (q1) "H1". iDestruct "H2" as (q2) "H2".
iCombine "H1 H2" as "H". eauto.
Qed.
Local Instance istk_intoand (istk : loc) (w : val) :
IntoAnd false ( q, istk ↦ᵢ{q} w) ( q, istk ↦ᵢ{q} w) ( q, istk ↦ᵢ{q} w).
Proof.
rewrite /IntoAnd. iDestruct 1 as (q) "[H1 H2]".
iSplitL "H1"; eauto.
Qed.
Program Definition stack_link_pre (τi : D) : DD -n> DD := λne P vv,
( w, ( q, vv.1 ↦ᵢ{q} w)
( (w = NONEV vv.2 = FoldV NONEV)
( (y1 : val) (z1 : loc) (y2 z2 : val),
w = SOMEV (PairV y1 (FoldV #z1))
vv.2 = FoldV (SOMEV (PairV y2 z2))
τi (y1, y2)
P (z1, z2))))%I.
Solve Obligations with solve_proper.
Global Instance stack_link_pre_contractive τi : Contractive (stack_link_pre τi).
Proof. solve_contractive. Qed.
Definition stack_link (Q : D) : DD := fixpoint (stack_link_pre Q).
Lemma stack_link_unfold (Q : D) (istk : loc) (v : val) :
stack_link Q (istk, v)
( w, ( q, istk ↦ᵢ{q} w)
((w = NONEV v = FoldV NONEV)
( (y1 : val) (z1 : loc) (y2 z2 : val),
w = SOMEV (PairV y1 (FoldV #z1))
v = FoldV (SOMEV (PairV y2 z2))
Q (y1, y2)
stack_link Q (z1, z2))))%I.
Proof. by rewrite {1}/stack_link fixpoint_unfold. Qed.
(** Actually, the whole `stack_link` predicate is duplicable *)
Local Instance stack_link_intoand (Q : D) (istk : loc) (v : val) :
IntoAnd false (stack_link Q (istk, v)) (stack_link Q (istk, v)) (stack_link Q (istk, v)).
Proof.
rewrite /IntoAnd. iLöb as "IH" forall (istk v).
rewrite {1 2 3}stack_link_unfold.
iDestruct 1 as (w) "([Histk Histk2] & [HLK | HLK])".
- iDestruct "HLK" as "[% %]".
iSplitL "Histk"; iExists _; iFrame; eauto.
- iDestruct "HLK" as (y1 z1 y2 z2) "(% & % & #HQ & HLK)".
iDestruct ("IH" with "HLK") as "[HLK HLK2]".
iClear "IH".
iSplitL "Histk HLK"; iExists _; iFrame; iRight; iExists _,_,_,_; eauto.
Qed.
Definition sinv (τi : D) stk stk' l' : iProp Σ :=
( (istk : loc) v,
stk' ↦ₛ v
l' ↦ₛ #false
stk ↦ᵢ (FoldV #istk)
stack_link τi (istk, v))%I.
Ltac close_sinv Hcl asn :=
iMod (Hcl with asn) as "_";
[iNext; rewrite /sinv; iExists _,_,_; by iFrame |]; try iModIntro.
[iNext; rewrite /sinv; iExists _,_; by iFrame |]; try iModIntro.
Lemma FG_CG_push_refinement N st st' (τi : D) (v v' : val) l Γ :
N ## logrelN
inv N (sinv τi st st' l) - τi (v,v') -
Γ (FG_push $/ (LitV (Loc st))) v log (CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) v' : TUnit.
Γ (FG_push $/ (LitV (Loc st))) v
log
(CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) v' : TUnit.
Proof.
iIntros (?) "#Hinv #Hvv'". iIntros (Δ).
Transparent FG_push.
......@@ -44,40 +92,36 @@ Section Stack_refinement.
iLöb as "IH".
rel_rec_l.
rel_load_l_atomic.
iInv N as (istk w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".
iInv N as (istk w) "(>Hst' & >Hl & >Hst & HLK)" "Hclose".
iExists (FoldV #istk). iFrame.
iModIntro. iNext. iIntros "Hst".
close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
close_sinv "Hclose" "[Hst Hst' Hl HLK]". clear w.
rel_rec_l.
rel_alloc_l as nstk "Hnstk". simpl.
rel_cas_l_atomic.
iInv N as (istk' w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".
iInv N as (istk' w) "(>Hst' & >Hl & >Hst & HLK)" "Hclose".
iExists (FoldV #istk'). iFrame.
iModIntro.
destruct (decide (istk' = istk)) as [e | nestk]; subst.
- (* CAS succeeds *)
iSplitR; first by iIntros ([]).
iIntros (?). iNext. iIntros "Hst".
rel_apply_r (CG_push_r with "Hst' Hl").
{ solve_ndisj. }
iIntros "Hst' Hl".
iMod (stack_owns_alloc with "[$Hoe $Hnstk]") as "[Hoe Hnstk]".
iMod ("Hclose" with "[Hst Hoe Hst' Hl HLK Hnstk]").
{ iNext. rewrite {2}/sinv. iExists _,_,_.
iFrame "Hoe Hst' Hst Hl".
rewrite (StackLink_unfold _ (# nstk, _)).
iExists _, _. iSplitR; auto.
iFrame "Hnstk".
iRight. iExists _, _, _, _. auto. }
rel_if_true_l.
by rel_vals.
iModIntro. iSplit.
- (* CAS fails *)
iSplitL; last by (iIntros (?); congruence).
iIntros (?); iNext; iIntros "Hst".
close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
close_sinv "Hclose" "[Hst Hst' Hl HLK]". clear w.
rel_if_false_l. simpl.
rel_rec_l.
by iApply "IH".
- (* CAS succeeds *)
iIntros (?). simplify_eq/=. iNext. iIntros "Hst".
rel_apply_r (CG_push_r with "Hst' Hl").
{ solve_ndisj. }
iIntros "Hst' Hl".
iMod ("Hclose" with "[Hst Hst' Hl HLK Hnstk]").
{ iNext. rewrite {2}/sinv. iExists _,_.
iFrame "Hst' Hst Hl".
rewrite (stack_link_unfold _ nstk).
iExists _. iSplitL "Hnstk".
- iExists 1%Qp; iFrame.
- iRight. iExists _,_,_,_. eauto. }
rel_if_true_l.
iApply bin_log_related_unit.
Qed.
Lemma FG_CG_pop_refinement' N st st' (τi : D) l Δ Γ :
......@@ -85,7 +129,7 @@ Section Stack_refinement.
inv N (sinv τi st st' l) -
{τi::Δ;Γ} (FG_pop $/ LitV (Loc st)) #() log (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l)) #() : TSum TUnit (TVar 0).
Proof.
Transparent CG_locked_pop FG_pop CG_pop.
Transparent CG_locked_pop FG_pop CG_pop.
iIntros (?) "#Hinv".
iLöb as "IH".
rewrite {2}/FG_pop. unlock. simpl_subst/=.
......@@ -102,120 +146,98 @@ replace ((rec: "pop" "st" <> :=
rel_rec_l.
rel_load_l_atomic.
iInv N as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
iInv N as (istk w) "(>Hst' & >Hl & >Hst & HLK)" "Hclose".
iExists _. iFrame.
iModIntro. iNext. iIntros "Hst /=".
rel_rec_l.
rel_unfold_l.
iPoseProof "HLK" as "HLK'".
rewrite {1}StackLink_unfold.
iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
iDestruct "HLK" as "[HLK HLK2]".
rewrite {1}stack_link_unfold.
iDestruct "HLK" as (w') "(Histk & HLK)".
iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
- (* The stack is empty *)
rel_apply_r (CG_pop_fail_r with "Hst' Hl").
{ solve_ndisj. }
iIntros "Hst' Hl".
close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear h. iClear "HLK'".
rel_load_l_atomic.
iInv N 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_l.
rel_rec_l.
close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".
(* duplicate the top node *)
iDestruct "Histk" as "[Histk Histk2]".
close_sinv "Hclose" "[Hst' Hst Hl HLK2]".
iDestruct "Histk2" as (q) "Histk2".
rel_load_l. rel_let_l.
rel_case_l. rel_let_l.
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 h.
rel_load_l_atomic.
iInv N 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_case_l.
rel_rec_l.
do 2 (rel_proj_l; rel_rec_l).
close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]". clear h istk v.
iDestruct "HLK" as (y1 z1 y2 z2) "(% & % & #Hτ & HLK_tail)"; simplify_eq/=.
(* duplicate the top node *)
close_sinv "Hclose" "[Hst' Hst Hl HLK2]".
iDestruct "Histk" as (q) "Histk".
rel_load_l. rel_let_l.
repeat (rel_pure_l _).
rel_cas_l_atomic.
iInv N as (istk v h) "[Hoe [Hst' [Hst [HLK2 Hl]]]]" "Hclose".
iInv N as (istk' w) "(>Hst' & >Hl & >Hst & HLK)" "Hclose".
iExists _. iFrame.
iModIntro.
destruct (decide (istk = istk2)) as [? |NE]; simplify_eq/=.
+ (* CAS succeeds *)
iSplitR; first by (iIntros (?); contradiction).
iIntros "%". iNext. iIntros "Hst".
iModIntro. iSplit.
+ (* CAS fails *) iIntros (?); simplify_eq/=.
iNext. iIntros "Hst".
rel_if_l.
close_sinv "Hclose" "[Hst Hst' Hl HLK]".
rel_rec_l.
iApply "IH".
+ (* CAS succeeds *) iIntros (?); simplify_eq/=.
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/=.
rewrite (stack_link_unfold _ istk).
iDestruct "HLK" as (w') "(Histk2 & HLK)".
iAssert (w' = InjRV (y1, FoldV #z1))%I with "[Histk Histk2]" as %->.
{ iDestruct "Histk2" as (?) "Histk2".
iApply (mapsto_agree with "Histk2 Histk"). }
iDestruct "HLK" as "[[% %] | HLK]"; first by congruence.
iDestruct "HLK" as (? ? ? ? ? ?) "[#Hτ2 HLK]". simplify_eq/=.
rel_apply_r (CG_pop_suc_r with "Hst' Hl").
{ solve_ndisj. }
iIntros "Hst' Hl".
iMod ("Hclose" with "[-]").
{ iNext. rewrite /sinv.
rewrite (StackLink_unfold _ (ym2, z2)).
iDestruct "HLK_tail" as (yn2loc ?) "[% _]"; simplify_eq /=.
iExists _,_,_. by iFrame. }
close_sinv "Hclose" "[-]".
rel_vals.
{ iModIntro. iRight.
iExists (_,_). eauto. }
+ (* CAS fails *)
iSplitL; last by (iIntros (?); congruence).
iIntros (?). iNext. iIntros "Hst".
rel_if_l.
close_sinv "Hclose" "[Hoe Hst Hst' Hl HLK2]".
rel_rec_l.
iApply "IH".
Qed.
Lemma FG_CG_pop_refinement st st' (τi : D) l Δ Γ :
inv stackN (sinv τi st st' l) -
Lemma FG_CG_pop_refinement st st' (τi : D) l N Δ Γ :
N ## logrelN
inv N (sinv τi st st' l) -
{τi::Δ;Γ} FG_pop $/ LitV (Loc st) log CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l) : TArrow TUnit (TSum TUnit (TVar 0)).
Proof.
iIntros "#Hinv".
iIntros (?) "#Hinv".
iApply bin_log_related_arrow_val; eauto.
{ unlock FG_pop CG_locked_pop. reflexivity. }
{ unlock FG_pop CG_locked_pop. reflexivity. }
{ unlock FG_pop CG_locked_pop. simpl_subst/=. solve_closed. }
{ unlock FG_pop CG_locked_pop. simpl_subst/=. solve_closed. }
iAlways. iIntros (? ?) "[% %]". simplify_eq/=.
iApply (FG_CG_pop_refinement' stackN); eauto.
{ solve_ndisj. }
iApply (FG_CG_pop_refinement' N); eauto.
Qed.
Lemma FG_CG_iter_refinement st st' (τi : D) l Δ Γ:
inv stackN (sinv τi st st' l) -
Lemma FG_CG_iter_refinement st st' (τi : D) l N Δ Γ:
N ## logrelN
inv N (sinv τi st st' l) -
{τi::Δ;Γ} FG_read_iter $/ LitV (Loc st) log CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l) : TArrow (TArrow (TVar 0) TUnit) TUnit.
Proof.
iIntros "#Hinv".
iIntros (?) "#Hinv".
Transparent FG_read_iter CG_snap_iter.
unfold FG_read_iter, CG_snap_iter. unlock.
simpl_subst/=.
iApply bin_log_related_arrow_val; eauto.
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.
rel_rec_l. rel_rec_r.
Transparent CG_snap. unlock CG_snap.
rel_rec_r.
rel_rec_r.
rel_rec_r.
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".
iInv N as (istk w) "(>Hst' & >Hl & >Hst & HLK)" "Hclose".
iExists _. iFrame.
iModIntro. iNext. iIntros "Hst /=".
......@@ -228,72 +250,33 @@ replace ((rec: "pop" "st" <> :=
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.
rel_rec_r. rel_let_r.
rel_let_l.
iLöb as "IH" forall (istk v) "HLK".
rel_rec_l.
rel_unfold_l.
rel_rec_r.
iPoseProof "HLK" as "HLK'".
iDestruct "HLK" as "[HLK HLK2]".
iMod ("Hclose" with "[Hst' HLK2 Hst Hl]") as "_".
{ iNext. iExists _, _. iFrame. }
iLöb as "IH" forall (istk w).
rewrite {1}StackLink_unfold.
iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
rewrite {1}stack_link_unfold.
iDestruct "HLK" as (w') "([Histk Histk2] & HLK)".
iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
- (* The stack is empty *)
rel_fold_r.
rel_case_r.
rel_rec_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.
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]".
simpl.
iApply (bin_log_related_app _ _ _ _ _ _ TUnit with "[] [Hτ]"). (* TODO: abbreivate this as related_let *)
+ iApply bin_log_related_arrow; eauto.
iAlways. iIntros (? ?) "?"; simplify_eq/=.
rel_rec_l.
rel_rec_l.
rel_rec_r.
rel_rec_r.
rel_proj_r.
iPoseProof "HLK_tail" as "HLK_tail.bak".
rewrite {1}StackLink_unfold.
iDestruct "HLK_tail" as (? ?) "[% [? HLK_tail]]"; simplify_eq/=.
by iApply "IH".
+ clear.
iClear "IH Histk HLK_tail HLK HLK'".
iSpecialize ("Hff" $! (y1,y2) with "Hτ").
iApply (related_ret with "[Hff]").
done.
iDestruct "Histk2" as (q) "Histk2".
rel_fold_r. rel_case_r. rel_rec_r.
rel_fold_l. rel_load_l. rel_case_l.
rel_let_l. iApply bin_log_related_unit.
- (* The stack has a top element *)
iDestruct "HLK" as (y1 z1 y2 z2) "(% & % & #Hτ & HLK_tail)"; simplify_eq/=.
iDestruct "Histk2" as (q) "Histk2".
rel_fold_r. rel_case_r. rel_rec_r. rel_proj_r.
rel_fold_l. rel_load_l. rel_case_l.
rel_let_l. rel_proj_l. rel_let_l. rel_proj_l. rel_let_l.
iApply bin_log_related_seq'.
{ iApply bin_log_related_app; eauto. by rel_vals. }
rel_rec_r. rel_proj_r. rel_let_r.
rel_let_l. rel_let_l.
iApply ("IH" with "HLK_tail").
Qed.
End Stack_refinement.
......@@ -311,7 +294,7 @@ Section Full_refinement.
end.
(* α. (α Unit) * (Unit Unit + α) * ((α Unit) Unit) *)
Lemma FG_CG_stack_refinement `{SPG: stackPreG Σ, logrelG Σ} Δ Γ :
Lemma FG_CG_stack_refinement `{logrelG Σ} Δ Γ :
{Δ;Γ} FG_stack log CG_stack : TForall (TProd (TProd
(TArrow (TVar 0) TUnit)
(TArrow TUnit (TSum TUnit (TVar 0))))
......@@ -332,21 +315,11 @@ Section Full_refinement.
rel_alloc_l as st "Hst".
simpl.
rel_rec_l.
iMod (own_alloc ( ( : stackUR))) as (γ) "Hemp"; first done.
set (istkG := StackG _ _ γ).
change γ with (@stack_name _ istkG).
change (@stack_pre_inG _ SPG) with (@stack_inG _ istkG).
clearbody istkG. clear γ SPG.
iAssert (@stack_owns _ istkG _ ) with "[Hemp]" as "Hoe".
{ rewrite /stack_owns /prestack_owns big_sepM_empty fmap_empty.
iFrame "Hemp". }
iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
iAssert (StackLink τi (#istk, FoldV (InjLV Unit))) with "[Histk]" as "#HLK".
{ rewrite StackLink_unfold.
iExists _, _. iSplitR; simpl; trivial.
iFrame "Histk". iLeft. iSplit; trivial. }
iAssert (sinv τi st st' l) with "[Hoe Hst Hst' HLK Hl]" as "Hinv".
{ iExists _, _, _. by iFrame. }
iAssert (stack_link τi (istk, FoldV (InjLV Unit))) with "[Histk]" as "HLK".
{ rewrite stack_link_unfold.
iExists _. iSplitL; simpl; eauto. }
iAssert (sinv τi st st' l) with "[Hst Hst' HLK Hl]" as "Hinv".
{ iExists _, _. by iFrame. }
iMod (inv_alloc stackN with "[Hinv]") as "#Hinv".
{ iNext. iExact "Hinv". }
unlock FG_stack_body.
......@@ -372,17 +345,19 @@ Section Full_refinement.
replace_r ((CG_locked_push $/ LitV (Loc st') $/ LitV (Loc l)) v2)%E.
{ unlock CG_locked_push. simpl_subst/=. reflexivity. }
iApply (FG_CG_push_refinement with "Hinv Hτ").
{ solve_ndisj. }
solve_ndisj.
- replace_l (FG_pop $/ LitV (Loc st))%E.
{ unlock FG_pop. by simpl_subst/=. }
replace_r (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l))%E.
{ unlock CG_locked_pop. by simpl_subst/=. }
iApply (FG_CG_pop_refinement with "Hinv").
solve_ndisj.
- replace_l (FG_read_iter $/ LitV (Loc st))%E.
{ unlock FG_read_iter. by simpl_subst/=. }
replace_r (CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l))%E.
{ unlock CG_snap_iter. by simpl_subst/=. }
iApply (FG_CG_iter_refinement with "Hinv").
solve_ndisj.
Qed.
Theorem stack_ctx_refinement :
......@@ -391,8 +366,7 @@ Section Full_refinement.
(TArrow TUnit (TSum TUnit (TVar 0))))
(TArrow (TArrow (TVar 0) TUnit) TUnit)).
Proof.
set (Σ := #[logrelΣ; GFunctor (authR stackUR)]).
eapply (logrel_ctxequiv Σ); [solve_closed.. | intros ].
eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
apply FG_CG_stack_refinement.
Qed.
End Full_refinement.
From iris.algebra Require Import gmap agree.
From iris.base_logic.lib Require Export auth.
From iris_logrel Require Export logrel.
Import uPred.
Definition stackUR : ucmraT := gmapUR loc (agreeR valC).
Class stackG Σ :=
StackG { stack_inG :> authG Σ stackUR; stack_name : gname }.
Class stackPreG Σ := StackPreG { stack_pre_inG :> authG Σ stackUR }.
Definition stackΣ : gFunctors := #[authΣ stackUR].
Instance subG_stackPreG {Σ} : subG stackΣ Σ stackPreG Σ.
Proof. solve_inG. Qed.
(* Instance stackG_stackPreG {Σ} : stackG Σ stackPreG Σ. *)
(* Proof. intros [S ?]. by constructor. Qed. *)
Definition prestack_mapsto `{authG Σ stackUR} (γ : gname) (l : loc) (v : val) : iProp Σ :=
own γ ( {[ l := to_agree v ]}).
Definition stack_mapsto `{stackG Σ} l v : iProp Σ := prestack_mapsto stack_name l v.
Notation "l ↦ˢᵗᵏ v" := (stack_mapsto l v) (at level 20) : uPred_scope.
Section Rules_pre.
Context `{authG Σ stackUR}.
Variable (γ : gname).
Notation D := (prodC valC valC -n> iProp Σ).
Notation "l ↦ˢᵗᵏ v" := (prestack_mapsto γ l v) (at level 20) : uPred_scope.
Global Instance stack_mapsto_persistent l v : Persistent (l ↦ˢᵗᵏ v).
Proof. apply _. Qed.
Lemma prestack_mapstos_agree_uncurried l v w : l ↦ˢᵗᵏ v l ↦ˢᵗᵏ w v = w.
Proof.
rewrite -own_op -auth_frag_op op_singleton.
change (own γ ( {[l := to_agree v to_agree w]}))
with (auth_own γ {[l := to_agree v to_agree w]}).
rewrite auth_own_valid. iIntros "Hvalid". iDestruct "Hvalid" as %Hvalid.
rewrite singleton_valid in Hvalid *.
intros Hagree. by rewrite (agree_op_inv' v w Hagree).
Qed.
Lemma prestack_mapstos_agree l v w : l ↦ˢᵗᵏ v - l ↦ˢᵗᵏ w - v = w.
Proof.
iIntros "??".
iApply prestack_mapstos_agree_uncurried. by iFrame.
Qed.
(* stacklink Q := {((Loc l), nil) l ↦ˢᵗᵏ (InjL #()) }
{((Loc l), cons y2 z2) y1 z1, l ↦ˢᵗᵏ (y1, z1)
(y1, y2) Q
stacklink Q (z1, z2) }*)
Program Definition preStackLink_pre (Q : D) : D -n> D := λne P v,
( (l : loc) w, v.1 = # l l ↦ˢᵗᵏ w
((w = InjLV #() v.2 = FoldV (InjLV #()))