Skip to content

GitLab

Commit 07aac180 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Finish porting to Iris 3.0.

parent e2c29658
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 243 additions and 489 deletions
F_mu/fundamental.v
View file @ 07aac180
......@@ -15,13 +15,12 @@ Section fundamental.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (wp_bind [ctx]);
iApply wp_wand_l;
iSplitL; [|iApply Hp; trivial]; cbn;
iApply (wp_wand with "[-]"); [iApply Hp; trivial|]; cbn;
iIntros (v) Hv.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → log_typed Γ e τ.
Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e : τ.
Proof.
induction 1; iIntros (Δ vs HΔ) "#HΓ"; cbn.
- (* var *)
......
F_mu/soundness.v
View file @ 07aac180
......@@ -3,18 +3,16 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
(∀ `{irisG lang Σ}, log_typed [] e τ) →
(∀ `{irisG lang Σ}, [] ⊨ e : τ) →
rtc step ([e], σ) (thp, σ') → e' ∈ thp →
is_Some (to_val e') ∨ reducible e' σ'.
Proof.
intros Hlog ??. cut (adequate e σ (λ _, True)); first (intros [_ ?]; eauto).
eapply (wp_adequacy Σ); eauto.
iIntros (Hinv).
iModIntro. iExists (λ _, True%I). iSplitR;eauto.
iIntros (Hinv). iModIntro. iExists (λ _, True%I). iSplit=> //.
rewrite -(empty_env_subst e).
set (HΣ := IrisG () _ Hinv (fun _ => True)%I).
iApply wp_wand_l; iSplitR; [|iApply Hlog]; eauto.
by iApply interp_env_nil.
set (HΣ := IrisG _ _ Hinv (λ _, True)%I).
iApply (wp_wand with "[]"). iApply Hlog; eauto. by iApply interp_env_nil. auto.
Qed.
Corollary type_soundness e τ e' thp σ σ' :
......
F_mu_ref/fundamental.v
View file @ 07aac180
......@@ -14,8 +14,8 @@ Section fundamental.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (wp_bind [ctx]);
iApply wp_wand_l;
iSplitR; [|iApply Hp; trivial]; iIntros (v) Hv; cbn.
iApply (wp_wand with "[-]"); [iApply Hp; trivial|]; cbn;
iIntros (v) Hv; cbn.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
......
F_mu_ref/fundamental_binary.v
View file @ 07aac180
......@@ -4,8 +4,7 @@ From iris_logrel.F_mu_ref Require Import rules_binary.
From iris.base_logic Require Export big_op.
Section bin_log_def.
Context `{cfgSG Σ}.
Context `{!heapG Σ}.
Context `{heapG Σ,cfgSG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Definition bin_log_related (Γ : list type) (e e' : expr) (τ : type) := ∀ Δ vvs (ρ : cfg lang),
......@@ -17,8 +16,7 @@ Notation "Γ ⊨ e '≤log≤' e' : τ" :=
(bin_log_related Γ e e' τ) (at level 74, e, e', τ at next level).
Section fundamental.
Context `{cfgSG Σ}.
Context `{!heapG Σ}.
Context `{heapG Σ,cfgSG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types e : expr.
Implicit Types Δ : listC D.
......@@ -27,10 +25,9 @@ Section fundamental.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) ident(w)
constr(Hv) uconstr(Hp) :=
iApply (wp_bind [ctx]);
iApply wp_wand_l; iSplitR;
[|iApply Hp; rewrite ?fill_app /=; iFrame "#"; trivial];
let Htmp := iFresh in
iIntros (v) Htmp; iDestruct Htmp as (w) Hv;
iApply (wp_wand with "[-]");
[iApply Hp; rewrite ?fill_app /=; iFrame "#"; trivial|];
iIntros (v); iDestruct 1 as (w) Hv;
rewrite fill_app; simpl.
Local Ltac value_case := iApply wp_value; eauto using to_of_val.
......
F_mu_ref/rules.v
View file @ 07aac180
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
From iris.base_logic Require Export invariants big_op.
From iris.algebra Require Import frac agree gmap.
From iris.base_logic.lib Require Import auth.
From iris.algebra Require Import auth frac agree gmap.
From iris_logrel.F_mu_ref Require Export lang.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Export gen_heap.
......
F_mu_ref/rules_binary.v
View file @ 07aac180
From iris.program_logic Require Import lifting.
From iris.algebra Require Import frac agree gmap list.
From iris.base_logic Require Import big_op auth.
From iris.algebra Require Import auth frac agree gmap list.
From iris.base_logic Require Import big_op.
From iris_logrel.F_mu_ref Require Export rules.
From iris.proofmode Require Import tactics.
Import uPred.
......@@ -11,11 +11,7 @@ Definition specN := nroot .@ "spec".
Definition cfgUR := prodUR (optionUR (exclR exprC)) (gen_heapUR loc val).
(** The CMRA for the thread pool. *)
Class cfgSG Σ :=
CFGSG {
cfg_inG :> inG Σ (authR cfgUR);
cfg_name : gname
}.
Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }.
Definition spec_ctx `{cfgSG Σ} (ρ : cfg lang) : iProp Σ :=
(∃ e, ∃ σ, own cfg_name (● (Excl' e, to_gen_heap σ))
......@@ -26,14 +22,13 @@ Definition spec_inv `{cfgSG Σ} `{invG Σ} (ρ : cfg lang) : iProp Σ :=
Section definitionsS.
Context `{cfgSG Σ}.
Definition heapS_mapsto (l : loc) (q : Qp) (v: val) : iProp Σ :=
own cfg_name (◯ (∅, {[ l := (q, to_agree v) ]})).
Definition tpool_mapsto (e: expr) : iProp Σ :=
own cfg_name (◯ (Excl' e, ∅)).
Global Instance heapS_mapsto_timeless l q v : TimelessP (heapS_mapsto l q v).
Proof. apply _. Qed.
End definitionsS.
......@@ -65,20 +60,16 @@ Section cfg.
nclose specN ⊆ E →
spec_inv ρ ∗ ⤇ fill K e ={E}=∗ ⤇ fill K e'.
Proof.
iIntros (??) "[Hinv Hj]". rewrite /spec_ctx /auth_inv /tpool_mapsto.
iIntros (??) "[Hinv Hj]". rewrite /spec_ctx /tpool_mapsto.
iInv specN as ">Hspec" "Hclose".
iDestruct "Hspec" as (e'' σ) "[Hown %]".
iDestruct (((@own_valid_2 Σ _ _ cfg_name (● (Excl' e'', to_gen_heap σ))) (◯ (Excl' (fill K e), ∅))) with "Hown Hj")
as %[[?%Excl_included%leibniz_equiv _]%prod_included Hvalid]%auth_valid_discrete_2.
subst.
iDestruct (@own_valid_2 with "Hown Hj")
as %[[?%Excl_included%leibniz_equiv _]%prod_included Hvalid]%auth_valid_discrete_2; subst.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ eapply auth_update, prod_local_update_1, option_local_update,
(exclusive_local_update _ (Excl (fill K e'))).
by inversion Hvalid.
}
iFrame "Hj".
iApply "Hclose". iNext. iExists (fill K e'). iExists σ.
iFrame.
{ by eapply auth_update, prod_local_update_1, option_local_update,
(exclusive_local_update _ (Excl (fill K e'))). }
iFrame "Hj".
iApply "Hclose". iNext. iExists (fill K e'). iExists σ. iFrame.
iPureIntro. eapply rtc_r, step_insert_no_fork; eauto.
Qed.
......@@ -191,5 +182,4 @@ Section cfg.
spec_inv ρ ∗ ⤇ fill K (Case (InjR e0) e1 e2)
={E}=∗ ⤇ fill K (e2.[e0/]).
Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.
End cfg.
F_mu_ref/soundness.v
View file @ 07aac180
......@@ -9,7 +9,7 @@ Class heapPreG Σ := HeapPreG {
}.
Theorem soundness Σ `{heapPreG Σ} e τ e' thp σ σ' :
(∀ `{heapG Σ}, log_typed [] e τ) →
(∀ `{heapG Σ}, [] ⊨ e : τ) →
rtc step ([e], σ) (thp, σ') → e' ∈ thp →
is_Some (to_val e') ∨ reducible e' σ'.
Proof.
......@@ -17,14 +17,13 @@ Proof.
eapply (wp_adequacy Σ _); eauto.
iIntros (Hinv).
iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
- apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)).
- iModIntro. iExists (λ σ, own γ (● to_gen_heap σ)); iFrame.
set (HΣ := IrisG _ _ Hinv (λ σ, own γ (● to_gen_heap σ))%I).
iApply wp_wand_r.
iSplitR. rewrite -(empty_env_subst e).
set (HeapΣ := (HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
{ apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). }
iModIntro. iExists (λ σ, own γ (● to_gen_heap σ)); iFrame.
set (HeapΣ := (HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
iApply (wp_wand with "[]").
- rewrite -(empty_env_subst e).
iApply (Hlog HeapΣ [] []). iApply (@interp_env_nil _ HeapΣ).
eauto.
- auto.
Qed.
Corollary type_soundness e τ e' thp σ σ' :
......@@ -34,7 +33,7 @@ Corollary type_soundness e τ e' thp σ σ' :
Proof.
intros ??. set (Σ := #[invΣ ; gen_heapΣ loc val]).
set (HG := HeapPreG Σ _ _).
eapply (soundness Σ).
eapply (soundness Σ).
- intros ?. by apply fundamental.
- eauto.
Qed.
F_mu_ref/soundness_binary.v
View file @ 07aac180
From iris_logrel.F_mu_ref Require Export context_refinement.
From iris.algebra Require Import frac agree.
From iris.base_logic Require Import big_op auth.
From iris.algebra Require Import auth frac agree.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
From iris_logrel.F_mu_ref Require Import soundness.
Lemma basic_soundness Σ `{heapPreG Σ, authG Σ cfgUR}
Lemma basic_soundness Σ `{heapPreG Σ, inG Σ (authR cfgUR)}
e e' τ v thp hp :
(∀ `{cfgSG Σ} `{!heapG Σ}, [] ⊨ e ≤log≤ e' : τ) →
(∀ `{heapG Σ, cfgSG Σ}, [] ⊨ e ≤log≤ e' : τ) →
rtc step ([e], ∅) (of_val v :: thp, hp) →
(∃ thp' hp' v', rtc step ([e'], ∅) (of_val v' :: thp', hp')).
Proof.
intros Hlog Hsteps.
cut (adequate e ∅ (λ _, ∃ thp' h v, rtc step ([e'], ∅) (of_val v :: thp', h))).
{ destruct 1; naive_solver. }
eapply (wp_adequacy Σ); first by apply _.
eapply (wp_adequacy Σ); first by apply _.
iIntros (Hinv).
iMod (own_alloc (● to_gen_heap ∅)) as (γ) "Hh".
{ apply (auth_auth_valid _ (to_gen_heap_valid _ _ ∅)). }
......@@ -26,37 +26,30 @@ Proof.
{ iNext. iExists e', ∅. iSplit; eauto.
rewrite /to_gen_heap fin_maps.map_fmap_empty.
iFrame. }
set (HΣ := IrisG _ _ Hinv (λ σ, own γ (● to_gen_heap σ))%I).
set (HeapΣ := (HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
set (HeapΣ := HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ)).
iExists (λ σ, own γ (● to_gen_heap σ)); iFrame.
iApply wp_fupd. iApply wp_wand_r.
iSplitL.
iPoseProof ((Hlog Hcfg HeapΣ) with "[Hcfg]") as "Hrel".
{
iFrame "Hcfg".
iApply (@logrel_binary.interp_env_nil Σ HeapΣ).
}
rewrite (empty_env_subst e). iApply ("Hrel" $! []).
{
iApply wp_fupd. iApply (wp_wand with "[-]").
- iPoseProof (Hlog _ _ with "[$Hcfg]") as "Hrel".
{ iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
rewrite (empty_env_subst e). iApply ("Hrel" $! []).
rewrite /tpool_mapsto (empty_env_subst e'). asimpl. iFrame.
}
iIntros (v'). iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as ">Hinv" "Hclose".
iDestruct "Hinv" as (e'' σ) "[Hown %]".
rewrite /tpool_mapsto /auth.auth_own /=.
iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
move: Hvalid=> /auth_valid_discrete_2
[/prod_included [Hv2 _] _]. apply Excl_included, leibniz_equiv in Hv2. subst.
iMod ("Hclose" with "[-]") as "_".
- iExists (#v2), σ. auto.
- iIntros "!> !%". eauto.
Qed.
- iIntros (v'). iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as ">Hinv" "Hclose".
iDestruct "Hinv" as (e'' σ) "[Hown %]".
rewrite /tpool_mapsto /=.
iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
move: Hvalid=> /auth_valid_discrete_2
[/prod_included [Hv2 _] _]. apply Excl_included, leibniz_equiv in Hv2. subst.
iMod ("Hclose" with "[-]") as "_".
+ iExists (#v2), σ. auto.
+ iIntros "!> !%". eauto.
Qed.
Lemma binary_soundness Σ `{heapPreG Σ, authG Σ cfgUR}
Lemma binary_soundness Σ `{heapPreG Σ, inG Σ (authR cfgUR)}
Γ e e' τ :
(∀ f, e.[upn (length Γ) f] = e) →
(∀ f, e'.[upn (length Γ) f] = e') →
(∀ `{cfgSG Σ} `{!heapG Σ}, Γ ⊨ e ≤log≤ e' : τ) →
(∀ `{heapG Σ, cfgSG Σ}, Γ ⊨ e ≤log≤ e' : τ) →
Γ ⊨ e ≤ctx≤ e' : τ.
Proof.
intros He He' Hlog K thp σ v ?. eapply (basic_soundness Σ)=> ??.
......
F_mu_ref_conc/examples/counter.v
View file @ 07aac180
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth.
From iris_logrel.F_mu_ref_conc Require Export examples.lock.
From iris_logrel.F_mu_ref_conc Require Import soundness_binary.
From iris.program_logic Require Import adequacy.
......@@ -36,9 +37,8 @@ Definition FG_counter : expr :=
App (Rec (FG_counter_body (Var 1))) (Alloc (#n 0)).
Section CG_Counter.
Context `{cfgSG Σ}.
Context `{heapIG Σ}.
Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types Δ : listC D.
......@@ -124,7 +124,7 @@ Section CG_Counter.
nclose specN ⊆ E →
spec_ctx ρ ∗ x ↦ₛ (#nv n) ∗ l ↦ₛ (#♭v false)
∗ j ⤇ fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
⊢ |={E}=> j ⤇ fill K Unit ∗ x ↦ₛ (#nv S n) ∗ l ↦ₛ (#♭v false).
={E}=∗ j ⤇ fill K Unit ∗ x ↦ₛ (#nv S n) ∗ l ↦ₛ (#♭v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]".
iMod (steps_with_lock
......@@ -164,7 +164,7 @@ Section CG_Counter.
nclose specN ⊆ E →
spec_ctx ρ ∗ x ↦ₛ (#nv n)
∗ j ⤇ fill K (App (counter_read (Loc x)) Unit)
⊢ |={E}=> j ⤇ fill K (#n n) ∗ x ↦ₛ (#nv n).
={E}=∗ j ⤇ fill K (#n n) ∗ x ↦ₛ (#nv n).
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read.
iMod (step_rec _ _ j K _ Unit with "[Hj]") as "Hj"; eauto.
......@@ -372,7 +372,7 @@ Theorem counter_ctx_refinement :
[] ⊨ FG_counter ≤ctx≤ CG_counter :
TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
Proof.
set (Σ := #[invΣ ; gen_heapΣ loc val ; authΣ cfgUR]).
set (Σ := #[invΣ ; gen_heapΣ loc val ; GFunctor (authR cfgUR) ]).
set (HG := soundness_unary.HeapPreIG Σ _ _).
eapply (binary_soundness Σ _); auto.
intros. apply FG_CG_counter_refinement.
......
F_mu_ref_conc/examples/stack/CG_stack.v
View file @ 07aac180
......@@ -58,7 +58,7 @@ Definition CG_stack : expr :=
(Alloc (Fold (InjL Unit))))) newlock).
Section CG_Stack.
Context `{cfgSG Σ}.
Context `{heapIG Σ, cfgSG Σ}.
Lemma CG_push_type st Γ τ :
typed Γ st (Tref (CG_StackType τ)) →
......
F_mu_ref_conc/examples/stack/refinement.v
View file @ 07aac180
This diff is collapsed.
F_mu_ref_conc/examples/stack/stack_rules.v
View file @ 07aac180
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Import logrel_binary.
From iris.algebra Require Import gmap dec_agree.
From iris.base_logic Require Import auth.
From iris.algebra Require Import auth gmap.
Import uPred.
From iris.algebra Require deprecated.
Import deprecated.dec_agree.
Definition stackUR : ucmraT := gmapUR loc (dec_agreeR val).
Lemma stackR_self_op (h : stackUR) : h ≡ h ⋅ h.
Proof.
intros i. rewrite lookup_op.
match goal with
|- ?A ≡ ?B ⋅ ?B => change B with A; destruct A as [c|]
end; trivial.
destruct c as [c|]; cbv -[equiv decide];
try destruct decide; trivial; tauto.
Qed.
Class stackG Σ :=
StackG { stack_inG :> authG Σ stackUR; stack_name : gname }.
StackG { stack_inG :> inG Σ (authR stackUR); stack_name : gname }.
Definition stack_mapsto `{stackG Σ} (l : loc) (v : val) : iProp Σ :=
own stack_name (◯ {[ l := DecAgree v ]}).
Notation "l ↦ˢᵗᵏ v" := (stack_mapsto l v) (at level 20) : uPred_scope.
Section Rules.
Context `{stackG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Definition stack_mapsto (l : loc) (v: val) : iProp Σ :=
auth_own stack_name {[ l := DecAgree v ]}.
Notation "l ↦ˢᵗᵏ v" := (stack_mapsto l v) (at level 20) : uPred_scope.
Lemma stack_mapsto_dup l v : l ↦ˢᵗᵏ v ⊢ l ↦ˢᵗᵏ v ∗ l ↦ˢᵗᵏ v.
Proof.
by rewrite /stack_mapsto /auth_own -own_op -auth_frag_op -stackR_self_op.
Qed.
Global Instance stack_mapsto_persistent l v : PersistentP (l ↦ˢᵗᵏ v).
Proof. apply _. Qed.
Lemma stack_mapstos_agree l v w:
l ↦ˢᵗᵏ v ∗ l ↦ˢᵗᵏ w ⊢ l ↦ˢᵗᵏ v ∗ l ↦ˢᵗᵏ w ∧ v = w.
Lemma stack_mapstos_agree l v w : l ↦ˢᵗᵏ v ∗ l ↦ˢᵗᵏ w ⊢ ⌜v = w⌝.
Proof.
iIntros "H".
rewrite -own_op.
iDestruct (own_valid _ with "H") as %Hvalid.
rewrite own_op. unfold stack_mapsto, auth_own.
iDestruct "H" as "[$ $]".
specialize (Hvalid l). rewrite lookup_op ?lookup_singleton in Hvalid.
cbv -[decide] in Hvalid; destruct decide; trivial.
rewrite -own_op -auth_frag_op op_singleton own_valid.
by iIntros ([=]%auth_own_valid%singleton_valid%dec_agree_op_inv).
Qed.
Program Definition StackLink_pre (Q : D) : D -n> D := λne P v,
(∃ l w, v.1 = LocV l ∗ l ↦ˢᵗᵏ w ∗
((w = InjLV UnitV ∧ v.2 = FoldV (InjLV UnitV)) ∨
(∃ y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1)) ∗
v.2 = FoldV (InjRV (PairV y2 z2)) ∗ Q (y1, y2) ∗ ▷ P(z1, z2))))%I.
(∃ l w, ⌜v.1 = LocV l⌝ ∗ l ↦ˢᵗᵏ w ∗
((⌜w = InjLV UnitV⌝ ∧ ⌜v.2 = FoldV (InjLV UnitV)⌝) ∨
(∃ y1 z1 y2 z2, ⌜w = InjRV (PairV y1 (FoldV z1))⌝ ∗
⌜v.2 = FoldV (InjRV (PairV y2 z2))⌝ ∗ Q (y1, y2) ∗ ▷ P(z1, z2))))%I.
Solve Obligations with solve_proper.
Global Instance StackLink_pre_contractive Q : Contractive (StackLink_pre Q).
Proof.
intros n P1 P2 HP v; simpl. repeat (apply exist_ne => ?).
repeat apply sep_ne; trivial. rewrite or_ne; trivial.
repeat (apply exist_ne => ?).
repeat apply sep_ne; trivial.
apply later_contractive => i ?. by apply HP.
Qed.
Proof. solve_contractive. Qed.
Definition StackLink Q := fixpoint (StackLink_pre Q).
Definition StackLink (Q : D) : D := fixpoint (StackLink_pre Q).
Lemma StackLink_unfold Q v :
StackLink Q v ≡ (∃ l w,
v.1 = LocV l ∗ l ↦ˢᵗᵏ w ∗
((w = InjLV UnitV ∧ v.2 = FoldV (InjLV UnitV)) ∨
(∃ y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1))
∗ v.2 = FoldV (InjRV (PairV y2 z2))
⌜v.1 = LocV l⌝ ∗ l ↦ˢᵗᵏ w ∗
((⌜w = InjLV UnitV⌝ ∧ ⌜v.2 = FoldV (InjLV UnitV)⌝) ∨
(∃ y1 z1 y2 z2, ⌜w = InjRV (PairV y1 (FoldV z1))⌝
∗ ⌜v.2 = FoldV (InjRV (PairV y2 z2))⌝
∗ Q (y1, y2) ∗ ▷ @StackLink Q (z1, z2))))%I.
Proof. by rewrite {1}/StackLink fixpoint_unfold. Qed.
Global Opaque StackLink. (* So that we can only use the unfold above. *)
Lemma StackLink_dup (Q : D) v `{∀ vw, PersistentP (Q vw)} :
StackLink Q v ⊢ StackLink Q v ∗ StackLink Q v.
Global Instance StackLink_persistent (Q : D) v `{∀ vw, PersistentP (Q vw)} :
PersistentP (StackLink Q v).
Proof.
iIntros "H". iLöb as "Hlat" forall (v). rewrite StackLink_unfold.
iDestruct "H" as (l w) "[% [Hl Hr]]"; subst.
iDestruct (stack_mapsto_dup with "[Hl]") as "[Hl1 Hl2]"; first eauto.
iDestruct "Hr" as "[#Hr|Hr]".
{ iSplitL "Hl1".
- iExists _, _; iFrame "Hl1"; eauto.
- iExists _, _; iFrame "Hl2"; eauto. }
iIntros "H". iLöb as "IH" forall (v). rewrite StackLink_unfold.
iDestruct "H" as (l w) "[% [#Hl [#Hr|Hr]]]"; subst.
{ iExists l, w; iAlways; eauto. }
iDestruct "Hr" as (y1 z1 y2 z2) "[#H1 [#H2 [#HQ H']]]".
rewrite later_forall; setoid_rewrite later_wand.
iDestruct ("Hlat" $! (z1, z2) with "H'") as "[HS1 HS2]".
iSplitL "Hl1 HS1".
- iExists _, _; iFrame "Hl1"; eauto 10.
- iExists _, _; iFrame "Hl2"; eauto 10.
Qed.
Lemma stackR_valid (h : stackUR) (i : loc) :
✓ h → h !! i = None ∨ ∃ v, h !! i = Some (DecAgree v).
Proof.
intros Hh; specialize (Hh i).
by match type of Hh with
✓ ?A => match goal with
| |- ?B = _ ∨ (∃ _, ?C = _) =>
change B with A; change C with A;
destruct A as [[c|]|]; inversion H; eauto
end
end.
rewrite later_forall. iDestruct ("IH" with "* H'") as "#H''". iClear "H'".
iAlways. eauto 20.
Qed.
Lemma stackR_alloc (h : stackUR) (i : loc) (v : val) :
h !! i = None → ● h ~~> ● (<[i := DecAgree v]> h) ⋅ ◯ {[i := DecAgree v]}.
Proof.
intros H1; apply cmra_total_update.
intros n z H2. rewrite (insert_singleton_op h); auto.
destruct z as [[ze |] zo];
unfold validN, cmra_validN in *; simpl in *; trivial.
destruct H2 as [H21 H22]; split.
- revert H21; rewrite !left_id. apply cmra_monoN_l.
- intros j. rewrite lookup_op.
destruct (decide (i = j)) as [|Hneq]; subst.
+ rewrite H1. rewrite lookup_singleton. constructor.
+ rewrite lookup_singleton_ne; trivial.
specialize (H22 j).
revert H22.
match goal with
|- ✓{_} ?B → ✓{_} (_ ⋅ ?A) =>
change B with A; destruct A; by try constructor
end.
Qed.
Proof. intros. by apply auth_update_alloc, alloc_singleton_local_update. Qed.
Lemma dec_agree_valid_op_eq (x y : dec_agreeR val) :
✓ (Some x ⋅ Some y) → x = y.
Proof.
intros H1.
destruct x as [x|]; destruct y as [y|]; trivial;
cbv -[decide] in H1; try destruct decide; subst; simpl; intuition trivial.
Qed.
Lemma stackR_auth_is_subheap (h h' : stackUR) :
✓ (● h ⋅ ◯ h') → ∀ i x, h' !! i = Some x → h !! i = Some x.
Proof.
intros H1 i x H2.
destruct H1 as [H11 H12]; simpl in H11.
specialize (H11 1).
destruct H11 as [z H11].
revert H11; rewrite ucmra_unit_left_id => H11.
eapply cmra_extend in H11; [| by apply cmra_valid_validN].
destruct H11 as (z1 & z2 & H31 & H32 & H33); simpl in *.
specialize (H32 i).
assert (H4 : ✓ (z1 ⋅ z2))by (by rewrite -H31).
apply leibniz_equiv.
rewrite H31. rewrite lookup_op.
specialize (H4 i). rewrite ?lookup_op in H4.
revert H32; rewrite H2 => H32.
match type of H32 with
?C ≡{_}≡ _ =>
match goal with
|- ?A ⋅ ?B ≡ _ =>
change C with A in *; destruct A as [a|]; inversion H32; subst
end
end.
match type of H32 with
?C ≡{_}≡ _ =>
match goal with
|- ?A ⋅ ?B ≡ _ => destruct B
end
end.
- set (H5 := dec_agree_valid_op_eq _ _ H4); clearbody H5. subst.
inversion H3; subst.
destruct x as [x|]; cbv -[decide]; try destruct decide;
constructor; intuition trivial.
- inversion H3; subst. constructor; trivial.
Qed.
Context {iI : heapIG Σ}.
Context `{heapIG Σ}.
Definition stack_owns (h : stackUR) :=
(own stack_name (● h)
∗ [∗ map] l ↦ v ∈ h, match v with
| DecAgree v' => l ↦ᵢ v'
| _ => True
| _ => False
end)%I.
Lemma stack_owns_alloc E h l v :
stack_owns h ∗ l ↦ᵢ v
⊢ |={E}=> stack_owns (<[l := DecAgree v]> h) ∗ l ↦ˢᵗᵏ v.
Lemma stack_owns_alloc h l v :
stack_owns h ∗ l ↦ᵢ v ==∗ stack_owns (<[l := DecAgree v]> h) ∗ l ↦ˢᵗᵏ v.
Proof.
iIntros "[[Hown Hall] Hl]".