diff --git a/theories/examples/stack/CG_stack.v b/theories/examples/stack/CG_stack.v
index 3cb045229f9eaf290e82dadd36bd4e6937691d07..250a1f28eb2672a60b6e60f0777b045679b6b4eb 100644
--- a/theories/examples/stack/CG_stack.v
+++ b/theories/examples/stack/CG_stack.v
@@ -34,17 +34,27 @@ Definition CG_stack : val := Λ:
(CG_new_stack, λ: "stt", CG_locked_pop "stt",
λ: "stt" "x", CG_locked_push "stt" "x").
+Fixpoint val_of_list (ls : list val) : val :=
+ match ls with
+ | [] => NONEV
+ | v::vs => CONSV v (val_of_list vs)
+ end.
+
+Definition is_stack `{!relocG Σ} (rs : val) (ls : list val) : iProp Σ :=
+ ∃ (st : loc) l, ⌜rs = (#st, l)%V⌠∗ is_locked_r l false ∗ st ↦ₛ val_of_list ls.
+
Section rules.
- Context `{relocG Σ}.
+ Context `{!relocG Σ}.
- Lemma refines_CG_push_r st l (v w : val) E t K A :
+ Lemma refines_CG_push_r rs tl v E t K A :
nclose relocN ⊆ E →
- st ↦ₛ v -∗ is_locked_r l false -∗
- (st ↦ₛ SOMEV (w, v) -∗ is_locked_r l false
+ is_stack rs tl -∗
+ (is_stack rs (v::tl)
-∗ REL t << fill K (of_val #()) @ E : A) -∗
- REL t << fill K (CG_locked_push (#st, l)%V w) @ E : A.
+ REL t << fill K (CG_locked_push rs v) @ E : A.
Proof.
- iIntros (?) "Hst Hl Hlog".
+ iIntros (?). iDestruct 1 as (st l ->) "[Hl Hst]".
+ iIntros "Hlog".
rel_rec_r. repeat rel_pure_r.
rel_apply_r (refines_acquire_r with "Hl").
iIntros "Hl". repeat rel_pure_r.
@@ -53,18 +63,19 @@ Section rules.
rel_store_r. repeat rel_pure_r.
rel_apply_r (refines_release_r with "Hl").
iIntros "Hl".
- iApply ("Hlog" with "Hst Hl").
+ iApply ("Hlog" with "[Hst Hl]").
+ iExists _,_. eauto with iFrame.
Qed.
- Lemma refines_CG_pop_suc_r st l (w v : val) E t K A :
+ Lemma refines_CG_pop_suc_r rs w tl E t K A :
nclose relocN ⊆ E →
- st ↦ₛ SOMEV (w, v) -∗
- is_locked_r l false -∗
- (st ↦ₛ v -∗ is_locked_r l false
- -∗ REL t << fill K (of_val (SOMEV w)) @ E : A) -∗
- REL t << fill K (CG_locked_pop (#st, l)%V) @ E : A.
+ is_stack rs (w::tl) -∗
+ (is_stack rs tl -∗
+ REL t << fill K (of_val (SOMEV w)) @ E : A) -∗
+ REL t << fill K (CG_locked_pop rs) @ E : A.
Proof.
- iIntros (?) "Hst Hl Hlog".
+ iIntros (?). iDestruct 1 as (st l ->) "[Hl Hst]".
+ iIntros "Hlog".
rel_rec_r. repeat rel_pure_r.
rel_apply_r (refines_acquire_r with "Hl").
iIntros "Hl". repeat rel_pure_r. rel_rec_r.
@@ -72,18 +83,18 @@ Section rules.
rel_store_r. repeat rel_pure_r.
rel_apply_r (refines_release_r with "Hl").
iIntros "Hl". repeat rel_pure_r.
- iApply ("Hlog" with "Hst Hl").
+ iApply ("Hlog" with "[Hst Hl]"). iExists _,_; eauto with iFrame.
Qed.
- Lemma refines_CG_pop_fail_r st l E t K A :
+ Lemma refines_CG_pop_fail_r rs E t K A :
nclose relocN ⊆ E →
- st ↦ₛ NONEV -∗
- is_locked_r l false -∗
- (st ↦ₛ NONEV -∗ is_locked_r l false
+ is_stack rs [] -∗
+ (is_stack rs []
-∗ REL t << fill K (of_val NONEV) @ E : A) -∗
- REL t << fill K (CG_locked_pop (#st, l)%V) @ E : A.
+ REL t << fill K (CG_locked_pop rs) @ E : A.
Proof.
- iIntros (?) "Hst Hl Hlog".
+ iIntros (?). iDestruct 1 as (st l ->) "[Hl Hst]".
+ iIntros "Hlog".
rel_rec_r. repeat rel_pure_r.
rel_apply_r (refines_acquire_r with "Hl").
iIntros "Hl". repeat rel_pure_r.
@@ -91,7 +102,7 @@ Section rules.
rel_load_r. rel_rec_r. repeat rel_pure_r.
rel_apply_r (refines_release_r with "Hl").
iIntros "Hl". repeat rel_pure_r.
- iApply ("Hlog" with "Hst Hl").
+ iApply ("Hlog" with "[Hst Hl]"). iExists _,_; eauto with iFrame.
Qed.
End rules.
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index d1c82066a5a2c6837ecbce938dbce008601c861b..cf961ac345ad0ca2ca3cd2875c154472627018ac 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -21,171 +21,148 @@ Section proof.
iSplitL "H1"; eauto with iFrame.
Qed.
- Notation D := (locO -n> valO -n> iPropO Σ).
-
- Program Definition stack_link_pre (A : lrel Σ) : D -n> D := λne S v1 v2,
- (∃ w, (∃ q, v1 ↦{q} w) ∗
- ((⌜w = NONEV⌠∧ ⌜v2 = NONEVâŒ)
- ∨(∃ (y1 : val) (z1 : loc) (y2 z2 : val),
- ⌜w = SOMEV (y1, #z1)âŒ
- ∗ ⌜v2 = SOMEV (y2, z2)âŒ
- ∗ A y1 y2 ∗ ▷ S z1 z2)))%I.
- Solve Obligations with solve_proper.
-
- Global Instance stack_link_pre_contractive A : Contractive (stack_link_pre A).
- Proof. solve_contractive. Qed.
-
- Definition stack_link A := fixpoint (stack_link_pre A).
-
- Lemma stack_link_unfold (A : lrel Σ) (istk : loc) (v : val) :
- stack_link A istk v ≡
- (∃ w, (∃ q, istk ↦{q} w) ∗
- ((⌜w = NONEV⌠∧ ⌜v = NONEVâŒ)
- ∨ (∃ (y1 : val) (z1 : loc) (y2 z2 : val),
- ⌜w = SOMEV (y1,#z1)âŒ
- ∗ ⌜v = SOMEV (y2, z2)âŒ
- ∗ A y1 y2
- ∗ ▷ stack_link A z1 z2)))%I.
+ Fixpoint stack_contents (v1 : loc) (ls : list val) :=
+ match ls with
+ | [] => ∃ q, v1 ↦{q} NONEV
+ | h::tl => ∃ (z1 : loc) q, v1 ↦{q} SOMEV (h, #z1) ∗
+ stack_contents z1 tl
+ end%I.
+
+ Definition stack_link (A : lrel Σ) (v1 : loc) (v2 : val) :=
+ (∃ (ls1 : list val) (ls2 : list val),
+ stack_contents v1 ls1 ∗ is_stack v2 ls2 ∗
+ [∗ list] v1;v2 ∈ ls1;ls2, A v1 v2)%I.
+
+ (** Actually, the whole `stack_contents` predicate is duplicable *)
+ Local Instance stack_contents_intoand (istk : loc) (ls : list val) :
+ IntoSep (stack_contents istk ls) (stack_contents istk ls) (stack_contents istk ls).
Proof.
- rewrite {1}/stack_link.
- transitivity (stack_link_pre A (fixpoint (stack_link_pre A)) istk v).
- (* TODO: rewrite fixpoint_unfold. *)
- { f_equiv. f_equiv. apply fixpoint_unfold. }
- reflexivity.
+ rewrite /IntoSep /=.
+ revert istk. induction ls as [|h ls]; intros istk; simpl.
+ - apply istk_intoand.
+ - iDestruct 1 as (z1 q) "[Histk Hc]".
+ rewrite IHls. iDestruct "Hc" as "[Hc1 Hc2]". iDestruct "Histk" as "[Histk1 Histk2]".
+ iSplitL "Hc1 Histk1"; iExists _, (q/2)%Qp; by iFrame.
Qed.
- (** Actually, the whole `stack_link` predicate is duplicable *)
- Local Instance stack_link_intoand (A : lrel Σ) (istk : loc) (v : val) :
- IntoSep (stack_link A istk v) (stack_link A istk v) (stack_link A istk v).
+ Lemma stack_contents_agree istk ls ls' :
+ stack_contents istk ls -∗ stack_contents istk ls' -∗ ⌜ls = ls'âŒ.
Proof.
- rewrite /IntoSep /=. 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.
+ revert istk ls'. induction ls as [|h ls]; intros istk ls'; simpl.
+ - iDestruct 1 as (q) "Histk".
+ destruct ls' as [|h' ls']; first by eauto.
+ simpl. iDestruct 1 as (z q') "[Histk' _]".
+ iDestruct (gen_heap.mapsto_agree with "Histk' Histk") as %Hfoo.
+ exfalso. naive_solver.
+ - iDestruct 1 as (z q) "[Histk Hls]".
+ destruct ls' as [|h' ls']; simpl.
+ + iDestruct 1 as (q') "Histk'".
+ iDestruct (gen_heap.mapsto_agree with "Histk' Histk") as %Hfoo.
+ exfalso. naive_solver.
+ + iDestruct 1 as (z' q') "[Histk' Hls']".
+ iDestruct (gen_heap.mapsto_agree with "Histk' Histk") as %Hfoo. simplify_eq/=.
+ iDestruct (IHls with "Hls Hls'") as %Hbar. simplify_eq/=.
+ eauto.
Qed.
- Definition sinv (A : lrel Σ) stk stk' l' : iProp Σ :=
- (∃ (istk : loc) v,
- stk' ↦ₛ v
- ∗ is_locked_r l' false
- ∗ stk ↦ #istk
- ∗ stack_link A istk v)%I.
+ Definition sinv (A : lrel Σ) stk stk' : iProp Σ :=
+ (∃ (istk : loc), stk ↦ #istk ∗ stack_link A istk stk')%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 || iFrame; iExists _,_; by eauto with iFrame) |]; try iModIntro.
- Lemma FG_CG_push_refinement N st st' (A : lrel Σ) l (v v' : val) :
+ Lemma FG_CG_push_refinement N st st' (A : lrel Σ) (v v' : val) :
N ## relocN →
- inv N (sinv A st st' l) -∗
+ inv N (sinv A st st') -∗
A v v' -∗
REL (FG_push #st v)
<<
- (CG_locked_push (#st', l)%V v') : ().
+ (CG_locked_push st' v') : ().
Proof.
iIntros (?) "#Hinv #Hvv".
rel_rec_l. iLöb as "IH".
- repeat rel_pure_l.
+ rel_pures_l.
rel_load_l_atomic.
- iInv N as (istk w) "(>Hst' & >Hl & >Hst & HLK)" "Hclose".
+ iInv N as (isk) "(>Hstk & Hlnk)" "Hclose".
iExists _. iFrame.
- iModIntro. iNext. iIntros "Hst".
- close_sinv "Hclose" "[Hst Hst' Hl HLK]". clear w.
- repeat rel_pure_l.
+ iModIntro. iNext. iIntros "Hstk".
+ close_sinv "Hclose" "[Hlnk Hstk]".
+ rel_pures_l.
rel_alloc_l nstk as "Hnstk".
rel_cmpxchg_l_atomic.
- iInv N as (istk' w) "(>Hst' & >Hl & >Hst & HLK)" "Hclose".
- iExists _. iFrame "Hst".
+ iInv N as (isk') "(>Hstk & Hlnk)" "Hclose".
+ iExists _. iFrame "Hstk".
iModIntro. iSplit.
- (* CmpXchg fails *)
- iIntros (?); iNext; iIntros "Hst".
- close_sinv "Hclose" "[Hst Hst' Hl HLK]". clear w.
- rel_pures_l. simpl.
- rel_rec_l.
- by iApply "IH".
+ iIntros (?); iNext; iIntros "Hstk".
+ close_sinv "Hclose" "[Hlnk Hstk]".
+ rel_pures_l. rel_rec_l. by iApply "IH".
- (* CmpXchg succeeds *)
- iIntros (?). simplify_eq/=. iNext. iIntros "Hst".
- rel_apply_r (refines_CG_push_r with "Hst' Hl").
- 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_pures_l.
- rel_values.
+ iIntros (?). simplify_eq/=. iNext. iIntros "Hstk".
+ rewrite /stack_link. iDestruct "Hlnk" as (ls1 ls2) "(Hls1 & Hls2 & #HA)".
+ rel_apply_r (refines_CG_push_r with "Hls2").
+ iIntros "Hls2".
+ iMod ("Hclose" with "[-]").
+ { iNext. rewrite {2}/sinv. iExists _. iFrame.
+ iExists (v::ls1),_. simpl. iFrame "Hls2 Hvv HA".
+ iExists _,_. iFrame. }
+ rel_pures_l. rel_values.
Qed.
- Lemma FG_CG_pop_refinement N st st' (A : lrel Σ) l :
+ Lemma FG_CG_pop_refinement N st st' (A : lrel Σ) :
N ## relocN →
- inv N (sinv A st st' l) -∗
+ inv N (sinv A st st') -∗
REL FG_pop #st
<<
- CG_locked_pop (#st', l)%V : () + A.
+ CG_locked_pop st' : () + A.
Proof.
iIntros (?) "#Hinv".
iLöb as "IH". rel_rec_l.
rel_load_l_atomic.
- iInv N as (istk w) "(>Hst' & >Hl & >Hst & HLK)" "Hclose".
- iExists _. iFrame "Hst".
- iModIntro. iNext. iIntros "Hst /=".
- repeat rel_pure_l. rel_rec_l.
- 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 (refines_CG_pop_fail_r with "Hst' Hl").
- iIntros "Hst' Hl".
- (* duplicate the top node *)
- iDestruct "Histk" as "[Histk Histk2]".
- close_sinv "Hclose" "[Hst' Hst Hl HLK2]".
- iDestruct "Histk2" as (q) "Histk2".
- rel_load_l. repeat rel_pure_l.
- rel_values.
+ iInv N as (istk) "(>Hstk & Hlnk)" "Hclose".
+ iExists _. iFrame "Hstk".
+ iModIntro. iNext. iIntros "Hstk /=".
+ rel_pures_l. rel_rec_l.
+ iDestruct "Hlnk" as (ls1 ls2) "(Hls1 & Hls2 & #HA)".
+ iDestruct "Hls1" as "[Histk1 Histk2]".
+ destruct ls1 as [|h1 ls1]; iSimpl in "Histk1".
+ - iDestruct (big_sepL2_length with "HA") as %Hfoo.
+ assert (ls2 = []) as -> by (apply length_zero_iff_nil; done). clear Hfoo.
+ rel_apply_r (refines_CG_pop_fail_r with "Hls2").
+ iIntros "Hls2".
+ close_sinv "Hclose" "[Histk2 Hstk Hls2]".
+ iDestruct "Histk1" as (q) "Histk'". rel_load_l.
+ rel_pures_l. rel_values.
iModIntro. iExists _,_. eauto.
- - (* The stack has a value *)
- 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. repeat rel_pure_l.
+ - iDestruct "Histk1" as (z1 q) "[Histk1 Hrest]".
+ close_sinv "Hclose" "[Histk2 Hstk Hls2]".
+ rel_load_l. rel_pures_l.
rel_cmpxchg_l_atomic.
- iInv N as (istk' w) "(>Hst' & >Hl & >Hst & HLK)" "Hclose".
- iExists _. iFrame "Hst".
- iModIntro. iSplit.
- + (* CmpXchg fails *) iIntros (?); simplify_eq/=.
- iNext. iIntros "Hst".
- rel_pures_l.
- close_sinv "Hclose" "[Hst Hst' Hl HLK]".
- iApply "IH".
- + (* CmpXchg succeeds *) iIntros (?); simplify_eq/=.
- iNext. iIntros "Hst".
- rel_pures_l.
- rewrite (stack_link_unfold _ istk).
- iDestruct "HLK" as (w') "(Histk2 & HLK)".
- iAssert (⌜w' = InjRV (y1, #z1)âŒ)%I with "[Histk Histk2]" as %->.
- { iDestruct "Histk2" as (?) "Histk2".
- iApply (gen_heap.mapsto_agree with "Histk2 Histk"). }
- iDestruct "HLK" as "[[% %] | HLK]"; first by congruence.
- iDestruct "HLK" as (? ? ? ? ? ?) "[#HÏ„2 HLK]". simplify_eq/=.
- rel_apply_r (refines_CG_pop_suc_r with "Hst' Hl").
- iIntros "Hst' Hl".
+ iInv N as (istk') "(>Hstk & Hlnk)" "Hclose".
+ iModIntro. iExists _. iFrame "Hstk". iSplit.
+ + iIntros (?). iNext. iIntros "Hstk".
+ close_sinv "Hclose" "[Hstk Hlnk]".
+ rel_pures_l. iApply "IH".
+ + iIntros (?). simplify_eq/=. iNext.
+ iIntros "Hstk". rel_pures_l.
+ iDestruct "Hlnk" as (ls1' ls2') "(Hc2 & Hst & #HA')".
+ iDestruct "Hrest" as "[Hrest Hz1]".
+ iAssert (stack_contents istk (h1::ls1)) with "[Histk1 Hrest]" as "Histk1".
+ { simpl. iExists _,_. by iFrame. }
+ iDestruct (stack_contents_agree with "Histk1 Hc2") as %<-.
+ iClear "HA".
+ rewrite big_sepL2_cons_inv_l. iDestruct "HA'" as (h2 l2' ->) "[Hh HA]".
+ rel_apply_r (refines_CG_pop_suc_r with "Hst").
+ iIntros "Hst".
close_sinv "Hclose" "[-]".
- rel_pures_l.
rel_values. iModIntro. iExists _,_; eauto.
Qed.
Definition stackInt A : lrel Σ := LRel (λ v1 v2,
- ∃ (l : val) (stk stk' : loc), ⌜v2 = (#stk', l)%V⌠∗ ⌜v1 = #stkâŒ
- ∗ inv (stackN .@ (stk,stk')) (sinv A stk stk' l))%I.
+ ∃ (stk : loc), ⌜v1 = #stkâŒ
+ ∗ inv (stackN .@ (stk,v2)) (sinv A stk v2))%I.
Lemma stack_refinement :
⊢ REL FG_stack << CG_stack : ∀ A, ∃ B, (() → B) * (B → () + A) * (B → A → ()).
@@ -202,22 +179,23 @@ Section proof.
rel_apply_r refines_newlock_r. iIntros (l) "Hl".
rel_pure_r. rel_alloc_r st' as "Hst'". rel_pure_r.
rel_values.
- iMod (inv_alloc (stackN.@(st,st')) _ (sinv A st st' l) with "[-]")
+ iMod (inv_alloc (stackN.@(st,(#st', l)%V)) _ (sinv A st (#st', l)%V) with "[-]")
as "#Hinv".
- { iNext. iExists _,_. iFrame.
- rewrite stack_link_unfold. iExists _.
- iSplitL; eauto. }
- iModIntro. iExists _,_,_. iFrame "Hinv". eauto.
+ { iNext. iExists _. iFrame. iExists [],[]. simpl.
+ iSplitL "Hisk"; first by eauto.
+ rewrite right_id. rewrite /is_stack.
+ iExists _,_; eauto with iFrame. }
+ iModIntro. iExists _. eauto with iFrame.
- rel_pure_l. rel_pure_r. iApply refines_arrow_val.
iAlways. iIntros (st1 st2) "Hst".
rel_rec_l. rel_rec_r.
- iDestruct "Hst" as (??? ??) "#Hst". simplify_eq/=.
+ iDestruct "Hst" as (??) "#Hst". simplify_eq/=.
iApply (FG_CG_pop_refinement with "Hst").
solve_ndisj.
- rel_pure_l. rel_pure_r. iApply refines_arrow_val.
iAlways. iIntros (st1 st2) "Hst".
rel_rec_l. rel_rec_r.
- iDestruct "Hst" as (??? ??) "#Hst". simplify_eq/=.
+ iDestruct "Hst" as (??) "#Hst". simplify_eq/=.
rel_pure_l. rel_pure_r. iApply refines_arrow_val.
iAlways. iIntros (x1 x2) "Hx".
rel_rec_l. rel_rec_r.
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index 8b43ac1ddb0eaa3a4383cd94711cf30b1351ef49..bd191d09efb5558b02de77f5c35437dbfe4fc5c5 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -23,7 +23,8 @@ are:
From iris.algebra Require Import auth gmap agree list excl.
From iris.base_logic.lib Require Import auth.
From reloc Require Export reloc experimental.helping.offers.
-From reloc Require Import examples.stack.CG_stack lib.list.
+From reloc Require Import lib.list.
+From reloc.examples.stack Require Import CG_stack refinement.
(** * Source code *)
Definition pop_st_no_offer : val := λ: "r" "mb" "pop",
@@ -219,6 +220,26 @@ Section offerReg_rules.
End offerReg_rules.
+(* TODO: this goes in Iris *)
+Section sep_list2.
+ Context `{!relocG Σ} {A B : Type}.
+ Implicit Types Φ Ψ : nat → A → B → iProp Σ.
+
+ Lemma big_sepL2_nil_inv_l Φ l2 :
+ ([∗ list] k↦y1;y2 ∈ []; l2, Φ k y1 y2) -∗ ⌜l2 = []âŒ.
+ Proof.
+ rewrite big_sepL2_alt bi.and_elim_l /= -length_zero_iff_nil.
+ by apply bi.pure_mono.
+ Qed.
+ Lemma big_sepL2_nil_inv_r Φ l1 :
+ ([∗ list] k↦y1;y2 ∈ l1; [], Φ k y1 y2) -∗ ⌜l1 = []âŒ.
+ Proof.
+ rewrite big_sepL2_alt bi.and_elim_l /= length_zero_iff_nil.
+ by apply bi.pure_mono.
+ Qed.
+
+End sep_list2.
+
(** * Refinement proof *)
Section refinement.
Context `{!relocG Σ, !offerRegPreG Σ, !offerG Σ}.
@@ -279,147 +300,132 @@ Section refinement.
Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
Proof. intros [|][|]; simpl; congruence. Qed.
- (** This will be the type of the stack linking predicate... *)
- Local Notation D := (olocO -d> valO -d> iPropO Σ).
- (** .. which we compute as the following fixed point: *)
- Definition stack_link_pre (A : lrel Σ) : D → D := λ S ol v2,
- match ol return _ with
- | None => ⌜v2 = NONEVâŒ
- | Some l => ∃ (h : val) (t : option loc) (h' t' : val),
- ⌜v2 = SOMEV (h', t')âŒ
- ∗ (∃ q, l ↦{q} (h, oloc_to_val t))
- ∗ A h h' ∗ ▷ S t t'
+ Fixpoint stack_contents (ol : option loc) (ls : list val) :=
+ match ol,ls with
+ | None,[] => True
+ | Some l,(h::t) =>
+ ∃ (ol : option loc),
+ ∃ q, l ↦{q} (h, oloc_to_val ol) ∗ stack_contents ol t
+ | _,_ => False
end%I.
- Global Instance stack_link_pre_contractive A : Contractive (stack_link_pre A).
+
+ Existing Instance istk_fromand.
+ Existing Instance istk_intoand.
+ Local Instance stack_contents_intoand (istk : option loc) (ls : list val) :
+ IntoSep (stack_contents istk ls) (stack_contents istk ls) (stack_contents istk ls).
Proof.
- intros n S1 S2 HS. solve_proper_prepare.
- repeat (first [apply HS | f_contractive | f_equiv]).
+ rewrite /IntoSep /=.
+ revert istk. induction ls as [|h ls]; intros istk; simpl.
+ - destruct istk; eauto.
+ - destruct istk; last by eauto. iDestruct 1 as (z1 q) "[Histk Hc]".
+ rewrite IHls. iDestruct "Hc" as "[Hc1 Hc2]". iDestruct "Histk" as "[Histk1 Histk2]".
+ iSplitL "Hc1 Histk1"; iExists _, (q/2)%Qp; by iFrame.
Qed.
- Definition stack_link A := fixpoint (stack_link_pre A).
-
- Lemma stack_link_unfold A ol v2 :
- stack_link A ol v2 ≡
- (match ol with
- | None => ⌜v2 = NONEVâŒ
- | Some l => ∃ (h : val) (t : option loc) (h' t' : val),
- ⌜v2 = SOMEV (h', t')âŒ
- ∗ (∃ q, l ↦{q} (h, oloc_to_val t))
- ∗ A h h' ∗ ▷ stack_link A t t'
- end%I).
- Proof. apply (fixpoint_unfold (stack_link_pre A)). Qed.
-
- Lemma stack_link_empty A : ⊢ stack_link A None NILV.
- Proof. rewrite stack_link_unfold; by iPureIntro. Qed.
-
- Lemma stack_link_cons A l h h' t t' q :
- A h h' -∗
- ▷ stack_link A t t' -∗
- l ↦{q} (h, oloc_to_val t) -∗
- stack_link A (Some l) (CONSV h' t').
+ Lemma stack_contents_agree istk ls ls' :
+ stack_contents istk ls -∗ stack_contents istk ls' -∗ ⌜ls = ls'âŒ.
Proof.
- iIntros "Hh Ht Hl".
- rewrite (stack_link_unfold A (Some _)).
- iExists _,_,_,_. iFrame "Hh Ht". iSplit; eauto with iFrame.
+ revert istk ls'. induction ls as [|h ls]; intros istk ls'; simpl.
+ - destruct istk; eauto.
+ destruct ls' as [|h' ls']; simpl; eauto.
+ - destruct istk; last eauto.
+ iDestruct 1 as (z q) "[Histk Hls]".
+ destruct ls' as [|h' ls']; simpl; eauto.
+ iDestruct 1 as (z' q') "[Histk' Hls']".
+ iDestruct (gen_heap.mapsto_agree with "Histk' Histk") as %Hfoo. simplify_eq/=.
+ iDestruct (IHls with "Hls Hls'") as %Hbar. simplify_eq/=.
+ eauto.
Qed.
(** ** The main invariant that we will use for the proof *)
- Definition stackInv A oname (st st' mb : loc) (lc : val) : iProp Σ :=
- (∃ ol v2 (N : offerReg),
- is_locked_r lc false
- ∗ st ↦ oloc_to_val ol
- ∗ st' ↦ₛ v2
- ∗ stack_link A ol v2
+ Definition stackInv A oname (st mb : loc) (st' : val) : iProp Σ :=
+ (∃ ol (N : offerReg) ls1 ls2,
+ st ↦ oloc_to_val ol
+ ∗ stack_contents ol ls1
+ ∗ is_stack st' ls2
+ ∗ ([∗ list] v1;v2 ∈ ls1;ls2, A v1 v2)
∗ (mb ↦ NONEV (* the mailbox is either empty or contains an offer that is in the registry *)
∨ (∃ (l : loc) v1 v2 γ j K,
A v1 v2
∗ mb ↦ SOMEV (v1, #l)
∗ ⌜N !! l = Some (v2, γ, j, K)âŒ))
∗ own oname (◠to_offer_reg N)
- ∗ offerInv N (#st', lc))%I.
+ ∗ offerInv N st')%I.
(** ** The proof itself *)
(* First the case where no offers is accepted *)
- Lemma pop_no_helping_refinement A γo st st' mb lk :
- inv stackN (stackInv A γo st st' mb lk) -∗
+ Lemma pop_no_helping_refinement A γo st st' mb :
+ inv stackN (stackInv A γo st mb st') -∗
(REL pop_st #st #mb
<<
- CG_locked_pop (#st', lk)%V : () + A) -∗
+ CG_locked_pop st' : () + A) -∗
REL pop_st_no_offer #st #mb pop_st
<<
- CG_locked_pop (#st', lk)%V : () + A.
+ CG_locked_pop st' : () + A.
Proof.
iIntros "#Hinv IH". rel_rec_l. rel_pures_l.
rel_load_l_atomic.
- iInv stackN as (s1 s2 N) "(Hlk & Hst1 & Hst2 & Hrel & Hmb & HNown & HN)" "Hcl".
- iModIntro. iExists _; iFrame. iNext. iIntros "Hst1".
- rewrite stack_link_unfold.
- destruct s1 as [l|]; last first.
- - (* Stack is empty *)
- iDestruct "Hrel" as "->". iSimpl.
- rel_pures_l.
- rel_apply_r (refines_CG_pop_fail_r with "Hst2 Hlk").
- iIntros "Hst' Hlk".
- iMod ("Hcl" with "[-]") as "_".
- { iNext. iExists _,_,_. iFrame.
- iApply stack_link_empty. }
- rel_values. iModIntro. iExists #(),#().
- iLeft; repeat iSplit; eauto with iFrame.
- - iDestruct "Hrel" as (h t h' t' ->) "(Hl & #Hh & Ht)". iSimpl.
+ iInv stackN as (ol N ls1 ls2) "(Hol & Hst1 & Hst2 & HA & Hmb & Hown & HN)" "Hcl".
+ iModIntro. iExists _; iFrame. iNext. iIntros "Hol".
+ destruct ls1 as [|h1 ls1].
+ - iSimpl in "Hst1".
+ destruct ol; first by eauto with iFrame.
rel_pures_l.
- iDestruct "Hl" as "[Hl Hl2]".
- iMod ("Hcl" with "[-IH Hl]") as "_".
- { iNext. iExists _,_,_. iFrame.
- iDestruct "Hl2" as (q) "Hl2".
- iApply (stack_link_cons with "Hh Ht Hl2"). }
- iDestruct "Hl" as (q) "Hl".
- rel_load_l. rel_pures_l.
+ rewrite (big_sepL2_nil_inv_l _ ls2). iDestruct "HA" as %->.
+ simpl. rel_pures_l.
+ rel_apply_r (refines_CG_pop_fail_r with "Hst2").
+ iIntros "Hst2". iMod ("Hcl" with "[-IH]") as "_".
+ { iNext. iExists None,_,[],_. simpl; iFrame.
+ by rewrite big_sepL2_nil. }
+ rel_values. iExists _,_. eauto with iFrame.
+ - iDestruct "Hst1" as "[Hst1 Hst1']".
+ iSimpl in "Hst1". destruct ol as [l|]; last by eauto with iFrame.
+ iDestruct "Hst1" as (ol q) "[[Hl Hl'] [Hol' Hol2]]".
+ rel_pures_l. iMod ("Hcl" with "[-Hl IH Hst1' Hol2]") as "_".
+ { iNext. iExists (Some l),_,(h1::ls1),_. iFrame.
+ simpl. eauto with iFrame. }
+ rel_load_l. rel_pures_l. iClear "Hl".
rel_cmpxchg_l_atomic.
- iInv stackN as (s1 s2 N') "(Hlk & Hst1 & Hst2 & Hrel & Hmb & HNown & HN)" "Hcl".
- iModIntro. iExists _; iFrame "Hst1". iSplit.
- + (* Going to retry *)
- iIntros (Hs1). iNext. iIntros "Hst1".
- rel_pures_l.
+ iInv stackN as (ol2 N' ls1' ls2') "(Hol & Hst1 & Hst2 & HA & Hmb & Hown & HN)" "Hcl".
+ iModIntro. iExists _. iFrame "Hol". iSplit.
+ + iIntros (?). iNext.
+ iIntros "Hol". rel_pures_l.
iMod ("Hcl" with "[-IH]").
- { iNext. iExists _,_,_. by iFrame. }
+ { iNext. iExists _,_,_,_. by iFrame. }
iApply "IH".
- + (* Going to succeed *)
- iIntros (Hs1). iNext. iIntros "Hst1".
- rel_pures_l.
- assert (s1 = Some l) as ->.
- { revert Hs1. destruct s1; simpl; congruence. }
- rewrite stack_link_unfold.
- iDestruct "Hrel" as (h1 t1 h1' t1' ->) "([Hl2 Hl3] & #Hh' & Hrel)".
- rel_apply_r (refines_CG_pop_suc_r with "Hst2 Hlk").
- iIntros "Hst' Hlk".
- iDestruct "Hl2" as (?) "Hl2".
- iDestruct (gen_heap.mapsto_agree with "Hl Hl2") as %?.
- simplify_eq/=.
- iMod ("Hcl" with "[-IH Hl Hl2]").
- { iNext. iExists _,_,_. by iFrame. }
- rel_values. iModIntro. iExists h1,h1'.
- iRight. repeat iSplit; eauto with iFrame.
+ + iIntros (?). iNext.
+ iIntros "Hol". rel_pures_l.
+ assert (ol2 = Some l) as ->.
+ { destruct ol2; by simplify_eq/=. }
+ iDestruct (stack_contents_agree with "Hst1 Hst1'") as %->.
+ rewrite big_sepL2_cons_inv_l.
+ iDestruct "HA" as (h2 ls2'' ->) "[#Hh HA]".
+ rel_apply_r (refines_CG_pop_suc_r with "Hst2").
+ iIntros "Hst2".
+ iMod ("Hcl" with "[-]").
+ { iNext. iExists _,_,_,_. by iFrame. }
+ rel_values. iExists _,_. eauto with iFrame.
Qed.
- Lemma pop_refinement A γo st st' mb lk :
- inv stackN (stackInv A γo st st' mb lk) -∗
+ Lemma pop_refinement A γo st st' mb :
+ inv stackN (stackInv A γo st mb st') -∗
REL pop_st #st #mb
<<
- CG_locked_pop (#st', lk)%V : () + A.
+ CG_locked_pop st' : () + A.
Proof.
iIntros "#Hinv".
iLöb as "IH".
rel_rec_l. rel_pures_l.
rel_load_l_atomic.
- iInv stackN as (s1 s2 N) "(>Hl & >Hst1 & >Hst2 & Hrel & Hmb & HNown & HN)" "Hcl"; simplify_eq.
+ iInv stackN as (ol N ls1 ls2) "(Hol & Hst1 & Hst2 & HA & Hmb & HNown & HN)" "Hcl".
iDestruct "Hmb" as "[Hmb | Hmb]".
- (* NO OFFER *)
iModIntro. iExists _; iFrame.
iNext. iIntros "Hmb".
rel_pures_l.
iMod ("Hcl" with "[-]") as "_".
- { iNext. iExists _, _, _; iFrame. }
+ { iNext. iExists _, _, _, _; by iFrame. }
iApply (pop_no_helping_refinement with "Hinv IH").
- (* YES OFFER *)
iDestruct "Hmb" as (l v1 v2 γ j K) "(#Hv & Hmb & >HNl)".
@@ -431,14 +437,15 @@ Section refinement.
iModIntro. iExists _; iFrame.
iNext. iIntros "Hmb".
iMod ("Hcl" with "[-Hlown IH]") as "_".
- { iNext. iExists _, _, _; iFrame.
+ { iNext. iExists _, _, _, _; iFrame.
iSplitL "Hmb".
- iRight. iExists _, _, _, _, _, _.
eauto with iFrame.
- by iApply "HN". }
rel_pures_l. rel_apply_l (take_offer_l _ ).
- iInv stackN as (s1' s2' N') "(>Hl & >Hst1 & >Hst2 & Hrel & Hmb & HNown & HN)" "Hcl"; simplify_eq.
+ iInv stackN as (ol' N' ls1' ls2') "(Hol & Hst1 & Hst2 & HA & Hmb & HNown & HN)" "Hcl".
+ simplify_eq/=.
iMod "HNown".
iDestruct (offerReg_frag_lookup with "HNown Hlown") as %?.
rewrite /offerInv (big_sepM_lookup_acc _ _ l); eauto. iSimpl in "HN".
@@ -447,14 +454,15 @@ Section refinement.
+ (* Did not manage to accept an offer *)
iIntros "HNl".
iMod ("Hcl" with "[-IH]") as "_".
- { iNext. iExists _,_,_. iFrame.
+ { iNext. iExists _,_,_,_. iFrame.
by iApply "HN". }
rel_pures_l.
iApply (pop_no_helping_refinement with "Hinv IH").
+ (* An offer was accepted *)
iIntros "Hj Hoff". rel_pures_l.
+ iDestruct "Hst2" as (st2l lk ->) "[Hlk Hst2]".
tp_rec j. tp_pures j. tp_rec j.
- unlock is_locked_r. iDestruct "Hl" as (lk' ->) "Hl".
+ unlock is_locked_r. iDestruct "Hlk" as (lk' ->) "Hl".
(* TODO: make all the tp_ tactics work without the need for an explicit Fupd *)
iApply refines_spec_ctx. iIntros "#HÏ".
iApply fupd_refines.
@@ -468,21 +476,21 @@ Section refinement.
iSpecialize ("HN" with "Hoff").
iClear "HÏ". iModIntro.
- rel_apply_r (refines_CG_pop_suc_r with "Hst2 [Hl]").
- { iExists _. by iFrame "Hl". }
- iIntros "Hst2 Hl".
+ rel_apply_r (refines_CG_pop_suc_r with "[Hst2 Hl]").
+ { iExists st2l,#lk'. rewrite /is_locked_r. by eauto with iFrame. }
+ iIntros "Hst2".
iMod ("Hcl" with "[-]") as "_".
- { iNext. iExists _,_,_. by iFrame. }
+ { iNext. iExists _,_,_,_. by eauto with iFrame. }
rel_values. iModIntro. iExists v1,v2.
iRight. repeat iSplit; eauto with iFrame.
Qed.
- Lemma push_refinement A γo st st' mb lk h1 h2 :
- inv stackN (stackInv A γo st st' mb lk) -∗
+ Lemma push_refinement A γo st st' mb h1 h2 :
+ inv stackN (stackInv A γo st mb st') -∗
A h1 h2 -∗
REL push_st #st #mb h1
<<
- CG_locked_push (#st', lk)%V h2 : ().
+ CG_locked_push st' h2 : ().
Proof.
iIntros "#Hinv #Hh".
iLöb as "IH".
@@ -491,7 +499,7 @@ Section refinement.
rel_apply_l mk_offer_l. iIntros (γ off) "Hoff Htok".
rel_pures_l.
rel_store_l_atomic. (* we update the mailbox and store the offer in the registry *)
- iInv stackN as (s1 s2 N) "(Hl & Hst1 & Hst2 & Hrel & Hmb & HNown & HN)" "Hcl".
+ iInv stackN as (ol N ls1 ls2) "(Hol & Hst1 & Hst2 & HA & Hmb & HNown & HN)" "Hcl".
iModIntro.
(* first we need to show that mb is allocated / owned *)
iAssert (∃ v, ▷ mb ↦ v)%I with "[Hmb]" as (v) "Hmb".
@@ -508,14 +516,16 @@ Section refinement.
iDestruct (offerInv_excl with "HN Hoff") as %?.
iMod (offerReg_alloc off h2 γ j K' with "HNown") as "[HNown #Hfrag]"; eauto.
iMod ("Hcl" with "[-]") as "_".
- { iNext. iExists _,_,_; iFrame.
+ { iNext. iExists _,_,_,_; iFrame.
iSplitL "Hmb".
- iRight. iExists off, h1, h2, _, _, _. iFrame "Hmb Hh".
iPureIntro. by rewrite lookup_insert.
- rewrite /offerInv big_sepM_insert; eauto with iFrame. }
iModIntro. iNext.
- iInv stackN as (s1' s2' N') "(Hl & Hst1 & Hst2 & Hrel & Hmb & >HNown & HN)" "Hcl".
- iModIntro. iDestruct (offerReg_frag_lookup with "HNown Hfrag") as %Hfoo.
+ iInv stackN as (ol' N' ls1' ls2') "(Hol & Hst1 & Hst2 & HA & Hmb & HNown & HN)" "Hcl".
+ simplify_eq/=.
+ iMod "HNown". iModIntro.
+ iDestruct (offerReg_frag_lookup with "HNown Hfrag") as %Hfoo.
rewrite /offerInv.
(* TODO: separate lemma *)
rewrite (big_sepM_lookup_acc _ N'); eauto.
@@ -524,43 +534,44 @@ Section refinement.
- (* The offer was already accepted *)
iSpecialize ("HN" with "Hoff").
iMod ("Hcl" with "[-]") as "_".
- { iNext. iExists _,_,_; iFrame. }
+ { iNext. iExists _,_,_,_; iFrame. }
rel_pures_l. rel_values.
- (* The offer has been successfully revoked. We have to do the actual push. *)
iSpecialize ("HN" with "Hoff").
iMod ("Hcl" with "[-]") as "_".
- { iNext. iExists _,_,_; iFrame. }
+ { iNext. iExists _,_,_,_; iFrame. }
clear.
rel_pures_l. rel_load_l_atomic.
- iInv stackN as (s1 s2 N) "(>Hl & >Hst1 & >Hst2 & Hrel & Hmb & HNown & HN)" "Hcl"; simplify_eq.
- iModIntro. iExists _. iFrame "Hst1". iNext. iIntros "Hst1".
+ iInv stackN as (ol N ls1 ls2) "(Hol & Hst1 & Hst2 & HA & Hmb & HNown & HN)" "Hcl".
+ iModIntro. iExists _. iFrame. iNext. iIntros "Hol".
iMod ("Hcl" with "[-]") as "_".
- { iNext. iExists _,_,_; iFrame. }
+ { iNext. iExists _,_,_,_; iFrame. }
rel_pures_l. rel_alloc_l new as "Hnew". rel_pures_l.
- rel_cmpxchg_l_atomic; first by destruct s1.
- iInv stackN as (s1' s2' N') "(>Hl & >Hst1 & >Hst2 & Hrel & Hmb & HNown & HN)" "Hcl"; simplify_eq.
- iModIntro. iExists _. iFrame "Hst1". iSplit.
- + iIntros (?). iNext. iIntros "Hst1".
+ rel_cmpxchg_l_atomic; first by destruct ol.
+ iInv stackN as (ol' N' ls1' ls2') "(Hol & Hst1 & Hst2 & HA & Hmb & HNown & HN)" "Hcl".
+ iModIntro. iExists _. iFrame "Hol". iSplit.
+ + iIntros (?). iNext. iIntros "Hol".
iMod ("Hcl" with "[-]") as "_".
- { iNext. iExists _,_,_; by iFrame. }
+ { iNext. iExists _,_,_,_; by iFrame. }
rel_pures_l. iApply "IH".
+ iIntros (?); simplify_eq/=. iNext.
- iIntros "Hst1".
- rel_apply_r (refines_CG_push_r with "Hst2 Hl").
- iIntros "Hst2 Hl".
- iDestruct (stack_link_cons _ new h1 h2
- with "Hh Hrel Hnew") as "Hrel".
+ iIntros "Hol".
+ rel_apply_r (refines_CG_push_r with "Hst2").
+ iIntros "Hst2".
iMod ("Hcl" with "[-]") as "_".
- { iNext. iExists _,_,_; by iFrame. }
+ { iNext. iExists (Some new),_,(h1::ls1'),_; iFrame.
+ simpl. by eauto with iFrame. }
rel_pures_l. rel_values.
Qed.
- Lemma refinement A :
- ⊢ REL mk_stack #() << CG_mkstack #() : (() → () + A) * (A → ()).
+ Lemma refinement :
+ ⊢ REL mk_stack << CG_mkstack : ∀ A, (() → () + A) * (A → ()).
Proof.
+ rel_values. iModIntro. iIntros (A). iModIntro.
+ iIntros (? ?) "[-> ->]".
rel_rec_r. rel_pures_r. rel_rec_r.
rel_apply_r refines_newlock_r. iIntros (lk) "Hlk".
rel_pures_r.
@@ -571,12 +582,12 @@ Section refinement.
rel_alloc_l st as "Hst". do 4 rel_pure_l. (*XXX: doing rel_pures_l reduces too much *)
iMod (own_alloc (◠to_offer_reg ∅ : authR offerRegR)) as (γo) "Hor".
{ apply auth_auth_valid. apply to_offer_reg_valid. }
- iMod (inv_alloc stackN _ (stackInv A γo st st' mb lk) with "[-]") as "#Hinv".
+ iMod (inv_alloc stackN _ (stackInv A γo st mb (#st', lk)%V) with "[-]") as "#Hinv".
{ iNext. unfold stackInv.
- iExists None, _, _. iFrame.
+ iExists None, _, [],[]. iFrame.
iSplit; eauto.
- - iApply stack_link_empty.
- - iApply offerInv_empty. }
+ - rewrite /is_stack. iExists _,_. eauto with iFrame.
+ - iSplit; first done. iApply offerInv_empty. }
iApply refines_pair; last first.
(* * Push refinement *)
{ rel_arrow_val. iIntros (h1 h2) "#Hh"; simplify_eq/=.