Library iris.heap_lang.refine_heap
From iris.heap_lang Require Export refine heap lifting notation wp_tactics.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
From iris.proofmode Require Import weakestpre invariants.
Import uPred.
Definition sheapN : namespace := nroot .@ "sheap".
Definition sheapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
Ltac wp_strip_later ::= iNext.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
From iris.proofmode Require Import weakestpre invariants.
Import uPred.
Definition sheapN : namespace := nroot .@ "sheap".
Definition sheapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
Ltac wp_strip_later ::= iNext.
The CMRA we need.
The Functor we need.
Definition sheapGF : gFunctor := authGF heapUR.
Section definitions.
Context `{i : sheapG Λ Σ}.
Context `{refineG Λ Σ (delayed_lang (heap_lang) Kd Fd) (S Kd × (Kd + 3))}.
Existing Instances gmap_empty.
Definition sheap_mapsto_def (l : loc) (q : Qp) (v: val) : iPropG Λ Σ :=
auth_own sheap_name {[ l := (q, DecAgree v) ]}.
Definition sheap_mapsto_aux : { x | x = @sheap_mapsto_def }. by eexists. Qed.
Definition sheap_mapsto := proj1_sig sheap_mapsto_aux.
Definition sheap_mapsto_eq : @sheap_mapsto = @sheap_mapsto_def :=
proj2_sig sheap_mapsto_aux.
Definition sheap_inv (h : heapUR) : iPropG Λ Σ :=
ownSP (of_heap h).
Definition sheap_ctx : iPropG Λ Σ :=
auth_ctx sheap_name sheapN sheap_inv.
Global Instance sheap_inv_proper : Proper ((≡) ==> (⊣⊢)) sheap_inv.
Proof. solve_proper. Qed.
Global Instance sheap_ctx_relevant : RelevantP sheap_ctx.
Proof. apply _. Qed.
Global Instance sheap_ctx_affine : AffineP sheap_ctx.
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque sheap_ctx sheap_mapsto.
Notation "l ↦s{ q } v" := (sheap_mapsto l q v)
(at level 20, q at level 50, format "l ↦s{ q } v") : uPred_scope.
Notation "l ↦s v" := (sheap_mapsto l 1 v) (at level 20) : uPred_scope.
Section heap.
Context {Σ : gFunctors}.
Context `{refineG Λ Σ (delayed_lang (heap_lang) Kd Fd) (S Kd × (Kd + 3))}.
Implicit Types P Q : iPropG Λ Σ.
Implicit Types Φ : val → iPropG Λ Σ.
Implicit Types σ : state.
Implicit Types h g : heapUR.
Hint Resolve heap_store_valid.
Section definitions.
Context `{i : sheapG Λ Σ}.
Context `{refineG Λ Σ (delayed_lang (heap_lang) Kd Fd) (S Kd × (Kd + 3))}.
Existing Instances gmap_empty.
Definition sheap_mapsto_def (l : loc) (q : Qp) (v: val) : iPropG Λ Σ :=
auth_own sheap_name {[ l := (q, DecAgree v) ]}.
Definition sheap_mapsto_aux : { x | x = @sheap_mapsto_def }. by eexists. Qed.
Definition sheap_mapsto := proj1_sig sheap_mapsto_aux.
Definition sheap_mapsto_eq : @sheap_mapsto = @sheap_mapsto_def :=
proj2_sig sheap_mapsto_aux.
Definition sheap_inv (h : heapUR) : iPropG Λ Σ :=
ownSP (of_heap h).
Definition sheap_ctx : iPropG Λ Σ :=
auth_ctx sheap_name sheapN sheap_inv.
Global Instance sheap_inv_proper : Proper ((≡) ==> (⊣⊢)) sheap_inv.
Proof. solve_proper. Qed.
Global Instance sheap_ctx_relevant : RelevantP sheap_ctx.
Proof. apply _. Qed.
Global Instance sheap_ctx_affine : AffineP sheap_ctx.
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque sheap_ctx sheap_mapsto.
Notation "l ↦s{ q } v" := (sheap_mapsto l q v)
(at level 20, q at level 50, format "l ↦s{ q } v") : uPred_scope.
Notation "l ↦s v" := (sheap_mapsto l 1 v) (at level 20) : uPred_scope.
Section heap.
Context {Σ : gFunctors}.
Context `{refineG Λ Σ (delayed_lang (heap_lang) Kd Fd) (S Kd × (Kd + 3))}.
Implicit Types P Q : iPropG Λ Σ.
Implicit Types Φ : val → iPropG Λ Σ.
Implicit Types σ : state.
Implicit Types h g : heapUR.
Hint Resolve heap_store_valid.
Allocation
Lemma sheap_alloc E σ :
authG Λ Σ heapUR → nclose sheapN ⊆ E →
ownSP σ ={E}=> ∃ _ : sheapG Λ Σ, sheap_ctx ★ [★ map] l↦v ∈ σ, l ↦s v.
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{rewrite [ownSP _](affine_intro _ (ownSP (of_heap (to_heap σ)))); last auto.
rewrite [ownSP _]later_intro.
apply (auth_alloc (ownSP ∘ of_heap) sheapN E); auto using to_heap_valid. }
apply pvs_mono, exist_elim⇒ γ.
rewrite -(exist_intro (SHeapG _ _ _ γ)) /sheap_ctx; apply sep_mono_r.
rewrite sheap_mapsto_eq /sheap_mapsto /sheap_name.
induction σ as [|l v σ Hl IH] using map_ind.
{ rewrite big_sepM_empty. rewrite emp_True.
rewrite /auth_own. apply affine_intro; first apply _; auto. }
rewrite to_heap_insert big_sepM_insert //.
rewrite (insert_singleton_op (to_heap σ));
last by rewrite lookup_fmap Hl; auto.
by rewrite auth_own_op IH.
Qed.
Context `{sheapG Λ Σ}.
Existing Instances gmap_empty.
authG Λ Σ heapUR → nclose sheapN ⊆ E →
ownSP σ ={E}=> ∃ _ : sheapG Λ Σ, sheap_ctx ★ [★ map] l↦v ∈ σ, l ↦s v.
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{rewrite [ownSP _](affine_intro _ (ownSP (of_heap (to_heap σ)))); last auto.
rewrite [ownSP _]later_intro.
apply (auth_alloc (ownSP ∘ of_heap) sheapN E); auto using to_heap_valid. }
apply pvs_mono, exist_elim⇒ γ.
rewrite -(exist_intro (SHeapG _ _ _ γ)) /sheap_ctx; apply sep_mono_r.
rewrite sheap_mapsto_eq /sheap_mapsto /sheap_name.
induction σ as [|l v σ Hl IH] using map_ind.
{ rewrite big_sepM_empty. rewrite emp_True.
rewrite /auth_own. apply affine_intro; first apply _; auto. }
rewrite to_heap_insert big_sepM_insert //.
rewrite (insert_singleton_op (to_heap σ));
last by rewrite lookup_fmap Hl; auto.
by rewrite auth_own_op IH.
Qed.
Context `{sheapG Λ Σ}.
Existing Instances gmap_empty.
General properties of mapsto
Global Instance sheap_mapsto_timeless l q v : ATimelessP (l ↦s{q} v).
Proof. rewrite sheap_mapsto_eq /sheap_mapsto_def. apply _. Qed.
Global Instance sheap_mapsto_affine l q v : AffineP (l ↦s{q} v).
Proof. rewrite sheap_mapsto_eq /sheap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_map_affine σ:
AffineP ([★ map] l↦v ∈ σ, l ↦s v)%I.
Proof.
intros; apply big_sep_affine.
rewrite /AffineL. induction map_to_list as [| a ?]; simpl; eauto using nil_affine.
destruct a; simpl; apply cons_affine; eauto using sheap_mapsto_affine.
Qed.
Lemma sheap_mapsto_op_eq l q1 q2 v : (l ↦s{q1} v ★ l ↦s{q2} v) ⊣⊢ l ↦s{q1+q2} v.
Proof. by rewrite sheap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp. Qed.
Lemma sheap_mapsto_op l q1 q2 v1 v2 :
(l ↦s{q1} v1 ★ l ↦s{q2} v2) ⊣⊢ (⧆ (v1 = v2) ★ l ↦s{q1+q2} v1).
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite sheap_mapsto_op_eq pure_equiv // -emp_True left_id. }
rewrite sheap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_ne //.
apply (anti_symm (⊢)); last by apply pure_elim_sep_l.
rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
rewrite option_validI prod_validI frac_validI discrete_valid.
rewrite affine_and comm affine_elim comm.
by apply pure_elim_r.
Qed.
Lemma sheap_mapsto_op_split l q v : l ↦s{q} v ⊣⊢ (l ↦s{q/2} v ★ l ↦s{q/2} v).
Proof. by rewrite sheap_mapsto_op_eq Qp_div_2. Qed.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export weakestpre.
From iris.heap_lang Require Export wp_tactics heap.
Implicit Types Δ : envs (iResUR Λ (globalF Σ)).
Context (d d': nat).
Context (Hd_le: (d ≤ Kd)%nat).
Context (Hd'_le: (d' ≤ Kd)%nat).
Proof. rewrite sheap_mapsto_eq /sheap_mapsto_def. apply _. Qed.
Global Instance sheap_mapsto_affine l q v : AffineP (l ↦s{q} v).
Proof. rewrite sheap_mapsto_eq /sheap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_map_affine σ:
AffineP ([★ map] l↦v ∈ σ, l ↦s v)%I.
Proof.
intros; apply big_sep_affine.
rewrite /AffineL. induction map_to_list as [| a ?]; simpl; eauto using nil_affine.
destruct a; simpl; apply cons_affine; eauto using sheap_mapsto_affine.
Qed.
Lemma sheap_mapsto_op_eq l q1 q2 v : (l ↦s{q1} v ★ l ↦s{q2} v) ⊣⊢ l ↦s{q1+q2} v.
Proof. by rewrite sheap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp. Qed.
Lemma sheap_mapsto_op l q1 q2 v1 v2 :
(l ↦s{q1} v1 ★ l ↦s{q2} v2) ⊣⊢ (⧆ (v1 = v2) ★ l ↦s{q1+q2} v1).
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite sheap_mapsto_op_eq pure_equiv // -emp_True left_id. }
rewrite sheap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_ne //.
apply (anti_symm (⊢)); last by apply pure_elim_sep_l.
rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
rewrite option_validI prod_validI frac_validI discrete_valid.
rewrite affine_and comm affine_elim comm.
by apply pure_elim_r.
Qed.
Lemma sheap_mapsto_op_split l q v : l ↦s{q} v ⊣⊢ (l ↦s{q/2} v ★ l ↦s{q/2} v).
Proof. by rewrite sheap_mapsto_op_eq Qp_div_2. Qed.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export weakestpre.
From iris.heap_lang Require Export wp_tactics heap.
Implicit Types Δ : envs (iResUR Λ (globalF Σ)).
Context (d d': nat).
Context (Hd_le: (d ≤ Kd)%nat).
Context (Hd'_le: (d' ≤ Kd)%nat).
Refine precondition
Lemma refine_alloc E i K e v:
to_val e = Some v → nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Alloc e) K d) ⊢
(|={E}=>> ∃ l, l ↦s v ★ ownT i (Lit (LitLoc l)) K d').
Proof.
iIntros (??) "[#Hinv HΦ]". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite (refine_alloc_pst' (E ∖ sheapN)); eauto.
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
rewrite /auth_inv.
iPoseProof (auth_empty sheap_name (E ∖ sheapN)) as "Hheap".
rewrite affine_elim.
iPvs "Hheap".
rewrite /auth_own.
rewrite own_valid_r. rewrite auth_validI //= and_elim_r.
iDestruct "Hγ" as "(Hγ&%)".
iCombine "Hγ" "Hheap" as "Hheap2".
pose (l := fresh (dom _ (of_heap a'))).
pose (a := ({[l := (1%Qp, DecAgree v)]} ⋅ a')).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := (1%Qp, DecAgree v)]})%I (E ∖ sheapN) with "Hheap2")
as "Hown".
{
rewrite /a.
generalize (auth_update ∅ a' {[l := (1%Qp, DecAgree v)]}).
rewrite ?left_id ?right_id. intros Hupd. eapply Hupd; eauto.
eapply alloc_unit_singleton_local_update.
- apply of_heap_None, (not_elem_of_dom (D:= gset _)), is_fresh; auto.
- econstructor; simpl; rewrite //=.
}
iDestruct "Hown" as "[Hγ Hγf]".
iPvsIntro. iSplitL "Hγ HS".
- apply affine_intro; first apply _.
iNext. iExists (a). iFrame "Hγ". apply affine_intro; first apply _.
rewrite /a. iClear "Hinv". rewrite -of_heap_insert -(insert_singleton_op a'); auto.
apply of_heap_None, (not_elem_of_dom (D:= gset _)), is_fresh; auto.
- iExists l. rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own. iFrame "Hγf".
iClear "Hinv"; auto.
Qed.
Lemma refine_load E i K l q v:
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Load (Lit (LitLoc l))) K d ★ l ↦s{q} v)
⊢ (|={E}=>> ownT i (of_val v) K d' ★ l ↦s{q} v).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own.
iCombine "Hγ" "Hpt" as "Hγ'".
rewrite own_valid_r. rewrite auth_validI //=.
iDestruct "Hγ'" as "(Hγ'&Hval)".
rewrite affine_and.
iDestruct "Hval" as "(Hval&%)".
rewrite affine_exist. iDestruct "Hval" as (b) "Hval".
rewrite left_id. iDestruct "Hval" as "%".
iDestruct "Hγ'" as "(Hγ&Hpt)".
rewrite (refine_load_pst (E ∖ sheapN) (of_heap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
iPvsIntro. iSplitL "HS Hγ".
- apply affine_intro; first apply _.
iNext. rewrite /auth_inv. iExists a'. iFrame "Hγ". apply affine_intro; first apply _.
iClear "Hinv". auto.
- iClear "Hinv". iFrame "HT"; auto.
Qed.
Lemma refine_store E i K l v' e v:
to_val e = Some v → nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Store (Lit (LitLoc l)) e) K d ★ l ↦s v')
⊢ (|={E}=>> ownT i (Lit (LitUnit)) K d' ★ l ↦s v).
Proof.
iIntros (??) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own.
iCombine "Hγ" "Hpt" as "Hγ'".
rewrite own_valid_r. rewrite auth_validI //=.
iDestruct "Hγ'" as "(Hγ'&Hval)".
rewrite affine_and.
iDestruct "Hval" as "(Hval&%)".
rewrite affine_exist. iDestruct "Hval" as (b) "Hval".
rewrite left_id. iDestruct "Hval" as "%".
rewrite (refine_store_pst (E ∖ sheapN) (of_heap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l := (1%Qp, DecAgree v)]} ⋅ b)).
iPoseProof (own_update _ _ (● a ⋅ ◯ {[l := (1%Qp, DecAgree v)]})%I (E ∖ sheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
iPvs "Hown".
iDestruct "Hown" as "[Hγ Hγf]".
iPvsIntro. iSplitL "Hγ HS".
- apply affine_intro; first apply _.
iNext. iExists (a). iFrame "Hγ". apply affine_intro; first apply _.
rewrite /a. iClear "Hinv".
setoid_subst. rewrite ?of_heap_singleton_op //; last by eapply heap_store_valid.
by rewrite insert_insert.
- iFrame "HT". iClear "Hinv". auto.
Qed.
Lemma refine_cas_fail E i K l q v' e1 v1 e2 v2:
to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (CAS (Lit (LitLoc l)) e1 e2) K d ★ l ↦s{q} v')
⊢ (|={E}=>> ownT i (Lit (LitBool false)) K d' ★ l ↦s{q} v').
Proof.
iIntros (????) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own.
iCombine "Hγ" "Hpt" as "Hγ'".
rewrite own_valid_r. rewrite auth_validI //=.
iDestruct "Hγ'" as "(Hγ'&Hval)".
rewrite affine_and.
iDestruct "Hval" as "(Hval&%)".
rewrite affine_exist. iDestruct "Hval" as (b) "Hval".
rewrite left_id. iDestruct "Hval" as "%".
iDestruct "Hγ'" as "(Hγ&Hpt)".
rewrite (refine_cas_fail_pst (E ∖ sheapN) (of_heap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
iPvsIntro. iSplitL "HS Hγ".
- apply affine_intro; first apply _.
iNext. rewrite /auth_inv. iExists a'. iFrame "Hγ". apply affine_intro; first apply _.
iClear "Hinv". auto.
- iClear "Hinv". iFrame "HT"; auto.
Qed.
Lemma refine_cas_suc E i K l e1 v1 e2 v2:
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (CAS (Lit (LitLoc l)) e1 e2) K d ★ l ↦s v1)
⊢ (|={E}=>> ownT i (Lit (LitBool true)) K d' ★ l ↦s v2).
Proof.
iIntros (???) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own.
iCombine "Hγ" "Hpt" as "Hγ'".
rewrite own_valid_r. rewrite auth_validI //=.
iDestruct "Hγ'" as "(Hγ'&Hval)".
rewrite affine_and.
iDestruct "Hval" as "(Hval&%)".
rewrite affine_exist. iDestruct "Hval" as (b) "Hval".
rewrite left_id. iDestruct "Hval" as "%".
rewrite (refine_cas_suc_pst (E ∖ sheapN) (of_heap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l := (1%Qp, DecAgree v2)]} ⋅ b)).
iPoseProof (own_update _ _ (● a ⋅ ◯ {[l := (1%Qp, DecAgree v2)]})%I (E ∖ sheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
iPvs "Hown".
iDestruct "Hown" as "[Hγ Hγf]".
iPvsIntro. iSplitL "Hγ HS".
- apply affine_intro; first apply _.
iNext. iExists (a). iFrame "Hγ". apply affine_intro; first apply _.
rewrite /a. iClear "Hinv".
setoid_subst. rewrite ?of_heap_singleton_op //; last by eapply heap_store_valid.
by rewrite insert_insert.
- iFrame "HT". iClear "Hinv". auto.
Qed.
Lemma refine_swap E i K l v e v':
to_val e = Some v' → nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Swap (Lit (LitLoc l)) e) K d ★ l ↦s v)
⊢ (|={E}=>> ownT i (of_val v) K d' ★ l ↦s v').
Proof.
iIntros (??) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own.
iCombine "Hγ" "Hpt" as "Hγ'".
rewrite own_valid_r. rewrite auth_validI //=.
iDestruct "Hγ'" as "(Hγ'&Hval)".
rewrite affine_and.
iDestruct "Hval" as "(Hval&%)".
rewrite affine_exist. iDestruct "Hval" as (b) "Hval".
rewrite left_id. iDestruct "Hval" as "%".
rewrite (refine_swap_pst (E ∖ sheapN) (of_heap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l := (1%Qp, DecAgree v')]} ⋅ b)).
iPoseProof (own_update _ _ (● a ⋅ ◯ {[l := (1%Qp, DecAgree v')]})%I (E ∖ sheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
iPvs "Hown".
iDestruct "Hown" as "[Hγ Hγf]".
iPvsIntro. iSplitL "Hγ HS".
- apply affine_intro; first apply _.
iNext. iExists (a). iFrame "Hγ". apply affine_intro; first apply _.
rewrite /a. iClear "Hinv".
setoid_subst. rewrite ?of_heap_singleton_op //; last by eapply heap_store_valid.
by rewrite insert_insert.
- iFrame "HT". iClear "Hinv". auto.
Qed.
Lemma refine_fai E i K l k:
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (FAI (Lit (LitLoc l))) K d ★ l ↦s (LitV $ LitInt k))
⊢ (|={E}=>> ownT i (Lit $ LitInt k) K d' ★ l ↦s (LitV $ LitInt (k+1))).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own.
iCombine "Hγ" "Hpt" as "Hγ'".
rewrite own_valid_r. rewrite auth_validI //=.
iDestruct "Hγ'" as "(Hγ'&Hval)".
rewrite affine_and.
iDestruct "Hval" as "(Hval&%)".
rewrite affine_exist. iDestruct "Hval" as (b) "Hval".
rewrite left_id. iDestruct "Hval" as "%".
rewrite (refine_fai_pst (E ∖ sheapN) (of_heap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l := (1%Qp, DecAgree (LitV $ LitInt (k+1)))]} ⋅ b)).
iPoseProof (own_update _ _ (● a ⋅ ◯ {[l := (1%Qp, DecAgree (LitV $ LitInt (k+1)))]})%I
(E ∖ sheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
iPvs "Hown".
iDestruct "Hown" as "[Hγ Hγf]".
iPvsIntro. iSplitL "Hγ HS".
- apply affine_intro; first apply _.
iNext. iExists (a). iFrame "Hγ". apply affine_intro; first apply _.
rewrite /a. iClear "Hinv".
setoid_subst. rewrite ?of_heap_singleton_op //; last by eapply heap_store_valid.
by rewrite insert_insert.
- iFrame "HT". iClear "Hinv". auto.
Qed.
Lemma refine_heap_pure_det_nofork E K N e1 e2 i:
(1 ≤ N ∧ N ≤ S Kd)%nat →
to_val e1 = None →
(∀ σ, nsteps (prim_step_nofork _) N (e1, σ) (e2, σ)) →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i e1 K d)
⊢ (|={E}=>> ownT i e2 K d').
Proof.
iIntros (?? Hstep ?) "(#Hinv&HΦ)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite (ownT_ownSP_step_nofork); eauto.
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
iPvsIntro. iSplitL "HS Hγ".
- apply affine_intro; first apply _.
iNext. rewrite /auth_inv. iExists a'. iFrame "Hγ". apply affine_intro; first apply _.
iClear "Hinv". auto.
- iClear "Hinv". iFrame "HT"; auto.
Qed.
Lemma refine_heap_pure_det_nofork1 E K e1 e2 i:
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ None = ef') →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i e1 K d)
⊢ (|={E}=>> ownT i e2 K d').
Proof.
iIntros (? Hred Hdet ?) "(#Hinv&HΦ)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
edestruct (Hred (of_heap a')) as (?&?&?&Hprim).
edestruct Hdet as (?&?&Hnfork); eauto. subst.
rewrite (ownT_ownSP_step_nofork_ctx1); eauto.
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
iPvsIntro. iSplitL "HS Hγ".
- apply affine_intro; first apply _.
iNext. rewrite /auth_inv. iExists a'. iFrame "Hγ". apply affine_intro; first apply _.
iClear "Hinv". auto.
- iClear "Hinv". iFrame "HT"; auto.
Qed.
Lemma refine_heap_pure_det' E K e1 e2 i:
(∀ σ E, (ownT i e1 K d ★ ownSP σ) ⊢ |={E}=>> ownT i e2 K d' ★ ownSP σ) →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i e1 K d)
⊢ (|={E}=>> ownT i e2 K d').
Proof.
iIntros (Hstep ?) "(#Hinv&HΦ)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite Hstep; eauto.
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
iPvsIntro. iSplitL "HS Hγ".
- apply affine_intro; first apply _.
iNext. rewrite /auth_inv. iExists a'. iFrame "Hγ". apply affine_intro; first apply _.
iClear "Hinv". auto.
- iClear "Hinv". iFrame "HT"; auto.
Qed.
Lemma refine_fork E K e i :
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Fork e) K d) ⊢
|={E}=>> ∃ i', ownT i (Lit LitUnit) K d' ★ ownT i' e [] (fresh_delay _ Fd e).
Proof.
iIntros (?) "(#Hinv&HΦ)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite (refine_fork_pst); eauto.
iPsvs "Hrefine".
iDestruct "Hrefine" as (i') "(HT&HT'&HS)".
iPvsIntro. iSplitL "HS Hγ".
- apply affine_intro; first apply _.
iNext. rewrite /auth_inv. iExists a'. iFrame "Hγ". apply affine_intro; first apply _.
iClear "Hinv". auto.
- iClear "Hinv". iFrame "HT"; auto.
Qed.
Lemma refine_rec E K f x erec e1 e2 i :
e1 = Rec f x erec →
is_Some (to_val e2) →
Closed (f :b: x :b: []) erec →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (App e1 e2) K d) ⊢
|={E}=>> ownT i (subst' x e2 (subst' f e1 erec)) K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_rec_pst. Qed.
Lemma refine_un_op E op K l l' i:
un_op_eval op l = Some l' →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (UnOp op (Lit l)) K d) ⊢
|={E}=>> ownT i (Lit l') K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_un_op_pst. Qed.
Lemma refine_bin_op E op K l1 l2 l' i:
bin_op_eval op l1 l2 = Some l' →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (BinOp op (Lit l1) (Lit l2)) K d) ⊢
|={E}=>> ownT i (Lit l') K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_bin_op_pst. Qed.
Lemma refine_if_true E K e1 e2 i :
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (If (Lit (LitBool true)) e1 e2) K d) ⊢
|={E}=>> ownT i e1 K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_if_true_pst. Qed.
Lemma refine_if_false E K e1 e2 i :
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (If (Lit (LitBool false)) e1 e2) K d) ⊢
|={E}=>> ownT i e2 K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_if_false_pst. Qed.
Lemma refine_fst E K e1 v1 e2 v2 i :
to_val e1 = Some v1 → to_val e2 = Some v2 →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Fst (Pair e1 e2)) K d) ⊢
|={E}=>> ownT i e1 K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_fst_pst. Qed.
Lemma refine_snd E K e1 v1 e2 v2 i :
to_val e1 = Some v1 → to_val e2 = Some v2 →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Snd (Pair e1 e2)) K d) ⊢
|={E}=>> ownT i e2 K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_snd_pst. Qed.
Lemma refine_case_inl E K e0 v0 e1 e2 i :
to_val e0 = Some v0 →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Case (InjL e0) e1 e2) K d) ⊢
|={E}=>> ownT i (App e1 e0) K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_case_inl_pst. Qed.
Lemma refine_case_inr E K e0 v0 e1 e2 i :
to_val e0 = Some v0 →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Case (InjR e0) e1 e2) K d) ⊢
|={E}=>> ownT i (App e2 e0) K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_case_inr_pst. Qed.
to_val e = Some v → nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Alloc e) K d) ⊢
(|={E}=>> ∃ l, l ↦s v ★ ownT i (Lit (LitLoc l)) K d').
Proof.
iIntros (??) "[#Hinv HΦ]". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite (refine_alloc_pst' (E ∖ sheapN)); eauto.
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
rewrite /auth_inv.
iPoseProof (auth_empty sheap_name (E ∖ sheapN)) as "Hheap".
rewrite affine_elim.
iPvs "Hheap".
rewrite /auth_own.
rewrite own_valid_r. rewrite auth_validI //= and_elim_r.
iDestruct "Hγ" as "(Hγ&%)".
iCombine "Hγ" "Hheap" as "Hheap2".
pose (l := fresh (dom _ (of_heap a'))).
pose (a := ({[l := (1%Qp, DecAgree v)]} ⋅ a')).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := (1%Qp, DecAgree v)]})%I (E ∖ sheapN) with "Hheap2")
as "Hown".
{
rewrite /a.
generalize (auth_update ∅ a' {[l := (1%Qp, DecAgree v)]}).
rewrite ?left_id ?right_id. intros Hupd. eapply Hupd; eauto.
eapply alloc_unit_singleton_local_update.
- apply of_heap_None, (not_elem_of_dom (D:= gset _)), is_fresh; auto.
- econstructor; simpl; rewrite //=.
}
iDestruct "Hown" as "[Hγ Hγf]".
iPvsIntro. iSplitL "Hγ HS".
- apply affine_intro; first apply _.
iNext. iExists (a). iFrame "Hγ". apply affine_intro; first apply _.
rewrite /a. iClear "Hinv". rewrite -of_heap_insert -(insert_singleton_op a'); auto.
apply of_heap_None, (not_elem_of_dom (D:= gset _)), is_fresh; auto.
- iExists l. rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own. iFrame "Hγf".
iClear "Hinv"; auto.
Qed.
Lemma refine_load E i K l q v:
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Load (Lit (LitLoc l))) K d ★ l ↦s{q} v)
⊢ (|={E}=>> ownT i (of_val v) K d' ★ l ↦s{q} v).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own.
iCombine "Hγ" "Hpt" as "Hγ'".
rewrite own_valid_r. rewrite auth_validI //=.
iDestruct "Hγ'" as "(Hγ'&Hval)".
rewrite affine_and.
iDestruct "Hval" as "(Hval&%)".
rewrite affine_exist. iDestruct "Hval" as (b) "Hval".
rewrite left_id. iDestruct "Hval" as "%".
iDestruct "Hγ'" as "(Hγ&Hpt)".
rewrite (refine_load_pst (E ∖ sheapN) (of_heap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
iPvsIntro. iSplitL "HS Hγ".
- apply affine_intro; first apply _.
iNext. rewrite /auth_inv. iExists a'. iFrame "Hγ". apply affine_intro; first apply _.
iClear "Hinv". auto.
- iClear "Hinv". iFrame "HT"; auto.
Qed.
Lemma refine_store E i K l v' e v:
to_val e = Some v → nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Store (Lit (LitLoc l)) e) K d ★ l ↦s v')
⊢ (|={E}=>> ownT i (Lit (LitUnit)) K d' ★ l ↦s v).
Proof.
iIntros (??) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own.
iCombine "Hγ" "Hpt" as "Hγ'".
rewrite own_valid_r. rewrite auth_validI //=.
iDestruct "Hγ'" as "(Hγ'&Hval)".
rewrite affine_and.
iDestruct "Hval" as "(Hval&%)".
rewrite affine_exist. iDestruct "Hval" as (b) "Hval".
rewrite left_id. iDestruct "Hval" as "%".
rewrite (refine_store_pst (E ∖ sheapN) (of_heap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l := (1%Qp, DecAgree v)]} ⋅ b)).
iPoseProof (own_update _ _ (● a ⋅ ◯ {[l := (1%Qp, DecAgree v)]})%I (E ∖ sheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
iPvs "Hown".
iDestruct "Hown" as "[Hγ Hγf]".
iPvsIntro. iSplitL "Hγ HS".
- apply affine_intro; first apply _.
iNext. iExists (a). iFrame "Hγ". apply affine_intro; first apply _.
rewrite /a. iClear "Hinv".
setoid_subst. rewrite ?of_heap_singleton_op //; last by eapply heap_store_valid.
by rewrite insert_insert.
- iFrame "HT". iClear "Hinv". auto.
Qed.
Lemma refine_cas_fail E i K l q v' e1 v1 e2 v2:
to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (CAS (Lit (LitLoc l)) e1 e2) K d ★ l ↦s{q} v')
⊢ (|={E}=>> ownT i (Lit (LitBool false)) K d' ★ l ↦s{q} v').
Proof.
iIntros (????) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own.
iCombine "Hγ" "Hpt" as "Hγ'".
rewrite own_valid_r. rewrite auth_validI //=.
iDestruct "Hγ'" as "(Hγ'&Hval)".
rewrite affine_and.
iDestruct "Hval" as "(Hval&%)".
rewrite affine_exist. iDestruct "Hval" as (b) "Hval".
rewrite left_id. iDestruct "Hval" as "%".
iDestruct "Hγ'" as "(Hγ&Hpt)".
rewrite (refine_cas_fail_pst (E ∖ sheapN) (of_heap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
iPvsIntro. iSplitL "HS Hγ".
- apply affine_intro; first apply _.
iNext. rewrite /auth_inv. iExists a'. iFrame "Hγ". apply affine_intro; first apply _.
iClear "Hinv". auto.
- iClear "Hinv". iFrame "HT"; auto.
Qed.
Lemma refine_cas_suc E i K l e1 v1 e2 v2:
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (CAS (Lit (LitLoc l)) e1 e2) K d ★ l ↦s v1)
⊢ (|={E}=>> ownT i (Lit (LitBool true)) K d' ★ l ↦s v2).
Proof.
iIntros (???) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own.
iCombine "Hγ" "Hpt" as "Hγ'".
rewrite own_valid_r. rewrite auth_validI //=.
iDestruct "Hγ'" as "(Hγ'&Hval)".
rewrite affine_and.
iDestruct "Hval" as "(Hval&%)".
rewrite affine_exist. iDestruct "Hval" as (b) "Hval".
rewrite left_id. iDestruct "Hval" as "%".
rewrite (refine_cas_suc_pst (E ∖ sheapN) (of_heap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l := (1%Qp, DecAgree v2)]} ⋅ b)).
iPoseProof (own_update _ _ (● a ⋅ ◯ {[l := (1%Qp, DecAgree v2)]})%I (E ∖ sheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
iPvs "Hown".
iDestruct "Hown" as "[Hγ Hγf]".
iPvsIntro. iSplitL "Hγ HS".
- apply affine_intro; first apply _.
iNext. iExists (a). iFrame "Hγ". apply affine_intro; first apply _.
rewrite /a. iClear "Hinv".
setoid_subst. rewrite ?of_heap_singleton_op //; last by eapply heap_store_valid.
by rewrite insert_insert.
- iFrame "HT". iClear "Hinv". auto.
Qed.
Lemma refine_swap E i K l v e v':
to_val e = Some v' → nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Swap (Lit (LitLoc l)) e) K d ★ l ↦s v)
⊢ (|={E}=>> ownT i (of_val v) K d' ★ l ↦s v').
Proof.
iIntros (??) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own.
iCombine "Hγ" "Hpt" as "Hγ'".
rewrite own_valid_r. rewrite auth_validI //=.
iDestruct "Hγ'" as "(Hγ'&Hval)".
rewrite affine_and.
iDestruct "Hval" as "(Hval&%)".
rewrite affine_exist. iDestruct "Hval" as (b) "Hval".
rewrite left_id. iDestruct "Hval" as "%".
rewrite (refine_swap_pst (E ∖ sheapN) (of_heap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l := (1%Qp, DecAgree v')]} ⋅ b)).
iPoseProof (own_update _ _ (● a ⋅ ◯ {[l := (1%Qp, DecAgree v')]})%I (E ∖ sheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
iPvs "Hown".
iDestruct "Hown" as "[Hγ Hγf]".
iPvsIntro. iSplitL "Hγ HS".
- apply affine_intro; first apply _.
iNext. iExists (a). iFrame "Hγ". apply affine_intro; first apply _.
rewrite /a. iClear "Hinv".
setoid_subst. rewrite ?of_heap_singleton_op //; last by eapply heap_store_valid.
by rewrite insert_insert.
- iFrame "HT". iClear "Hinv". auto.
Qed.
Lemma refine_fai E i K l k:
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (FAI (Lit (LitLoc l))) K d ★ l ↦s (LitV $ LitInt k))
⊢ (|={E}=>> ownT i (Lit $ LitInt k) K d' ★ l ↦s (LitV $ LitInt (k+1))).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite sheap_mapsto_eq /sheap_mapsto_def /auth_own.
iCombine "Hγ" "Hpt" as "Hγ'".
rewrite own_valid_r. rewrite auth_validI //=.
iDestruct "Hγ'" as "(Hγ'&Hval)".
rewrite affine_and.
iDestruct "Hval" as "(Hval&%)".
rewrite affine_exist. iDestruct "Hval" as (b) "Hval".
rewrite left_id. iDestruct "Hval" as "%".
rewrite (refine_fai_pst (E ∖ sheapN) (of_heap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l := (1%Qp, DecAgree (LitV $ LitInt (k+1)))]} ⋅ b)).
iPoseProof (own_update _ _ (● a ⋅ ◯ {[l := (1%Qp, DecAgree (LitV $ LitInt (k+1)))]})%I
(E ∖ sheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
iPvs "Hown".
iDestruct "Hown" as "[Hγ Hγf]".
iPvsIntro. iSplitL "Hγ HS".
- apply affine_intro; first apply _.
iNext. iExists (a). iFrame "Hγ". apply affine_intro; first apply _.
rewrite /a. iClear "Hinv".
setoid_subst. rewrite ?of_heap_singleton_op //; last by eapply heap_store_valid.
by rewrite insert_insert.
- iFrame "HT". iClear "Hinv". auto.
Qed.
Lemma refine_heap_pure_det_nofork E K N e1 e2 i:
(1 ≤ N ∧ N ≤ S Kd)%nat →
to_val e1 = None →
(∀ σ, nsteps (prim_step_nofork _) N (e1, σ) (e2, σ)) →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i e1 K d)
⊢ (|={E}=>> ownT i e2 K d').
Proof.
iIntros (?? Hstep ?) "(#Hinv&HΦ)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite (ownT_ownSP_step_nofork); eauto.
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
iPvsIntro. iSplitL "HS Hγ".
- apply affine_intro; first apply _.
iNext. rewrite /auth_inv. iExists a'. iFrame "Hγ". apply affine_intro; first apply _.
iClear "Hinv". auto.
- iClear "Hinv". iFrame "HT"; auto.
Qed.
Lemma refine_heap_pure_det_nofork1 E K e1 e2 i:
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ None = ef') →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i e1 K d)
⊢ (|={E}=>> ownT i e2 K d').
Proof.
iIntros (? Hred Hdet ?) "(#Hinv&HΦ)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
edestruct (Hred (of_heap a')) as (?&?&?&Hprim).
edestruct Hdet as (?&?&Hnfork); eauto. subst.
rewrite (ownT_ownSP_step_nofork_ctx1); eauto.
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
iPvsIntro. iSplitL "HS Hγ".
- apply affine_intro; first apply _.
iNext. rewrite /auth_inv. iExists a'. iFrame "Hγ". apply affine_intro; first apply _.
iClear "Hinv". auto.
- iClear "Hinv". iFrame "HT"; auto.
Qed.
Lemma refine_heap_pure_det' E K e1 e2 i:
(∀ σ E, (ownT i e1 K d ★ ownSP σ) ⊢ |={E}=>> ownT i e2 K d' ★ ownSP σ) →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i e1 K d)
⊢ (|={E}=>> ownT i e2 K d').
Proof.
iIntros (Hstep ?) "(#Hinv&HΦ)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite Hstep; eauto.
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
iPvsIntro. iSplitL "HS Hγ".
- apply affine_intro; first apply _.
iNext. rewrite /auth_inv. iExists a'. iFrame "Hγ". apply affine_intro; first apply _.
iClear "Hinv". auto.
- iClear "Hinv". iFrame "HT"; auto.
Qed.
Lemma refine_fork E K e i :
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Fork e) K d) ⊢
|={E}=>> ∃ i', ownT i (Lit LitUnit) K d' ★ ownT i' e [] (fresh_delay _ Fd e).
Proof.
iIntros (?) "(#Hinv&HΦ)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as (a') "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ".
iTimeless "Hφ".
rewrite /sheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite (refine_fork_pst); eauto.
iPsvs "Hrefine".
iDestruct "Hrefine" as (i') "(HT&HT'&HS)".
iPvsIntro. iSplitL "HS Hγ".
- apply affine_intro; first apply _.
iNext. rewrite /auth_inv. iExists a'. iFrame "Hγ". apply affine_intro; first apply _.
iClear "Hinv". auto.
- iClear "Hinv". iFrame "HT"; auto.
Qed.
Lemma refine_rec E K f x erec e1 e2 i :
e1 = Rec f x erec →
is_Some (to_val e2) →
Closed (f :b: x :b: []) erec →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (App e1 e2) K d) ⊢
|={E}=>> ownT i (subst' x e2 (subst' f e1 erec)) K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_rec_pst. Qed.
Lemma refine_un_op E op K l l' i:
un_op_eval op l = Some l' →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (UnOp op (Lit l)) K d) ⊢
|={E}=>> ownT i (Lit l') K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_un_op_pst. Qed.
Lemma refine_bin_op E op K l1 l2 l' i:
bin_op_eval op l1 l2 = Some l' →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (BinOp op (Lit l1) (Lit l2)) K d) ⊢
|={E}=>> ownT i (Lit l') K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_bin_op_pst. Qed.
Lemma refine_if_true E K e1 e2 i :
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (If (Lit (LitBool true)) e1 e2) K d) ⊢
|={E}=>> ownT i e1 K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_if_true_pst. Qed.
Lemma refine_if_false E K e1 e2 i :
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (If (Lit (LitBool false)) e1 e2) K d) ⊢
|={E}=>> ownT i e2 K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_if_false_pst. Qed.
Lemma refine_fst E K e1 v1 e2 v2 i :
to_val e1 = Some v1 → to_val e2 = Some v2 →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Fst (Pair e1 e2)) K d) ⊢
|={E}=>> ownT i e1 K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_fst_pst. Qed.
Lemma refine_snd E K e1 v1 e2 v2 i :
to_val e1 = Some v1 → to_val e2 = Some v2 →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Snd (Pair e1 e2)) K d) ⊢
|={E}=>> ownT i e2 K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_snd_pst. Qed.
Lemma refine_case_inl E K e0 v0 e1 e2 i :
to_val e0 = Some v0 →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Case (InjL e0) e1 e2) K d) ⊢
|={E}=>> ownT i (App e1 e0) K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_case_inl_pst. Qed.
Lemma refine_case_inr E K e0 v0 e1 e2 i :
to_val e0 = Some v0 →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Case (InjR e0) e1 e2) K d) ⊢
|={E}=>> ownT i (App e2 e0) K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_case_inr_pst. Qed.
Proof rules for the sugar
Lemma refine_lam E K x ef e i:
is_Some (to_val e) → Closed (x :b: []) ef →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (App (Lam x ef) e) K d)
⊢ |={E}=>> ownT i (subst' x e ef) K d'.
Proof. intros. rewrite (refine_rec _ _ BAnon) //; eauto. Qed.
Lemma refine_let E K x e1 e2 i:
is_Some (to_val e1) → Closed (x :b: []) e2 →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Let x e1 e2) K d)
⊢ |={E}=>> ownT i (subst' x e1 e2) K d'.
Proof. apply refine_lam; eauto. Qed.
Lemma refine_seq E K e1 e2 i:
is_Some (to_val e1) → Closed [] e2 →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Seq e1 e2) K d)
⊢ |={E}=>> ownT i e2 K d'.
Proof. intros ??. apply refine_lam; eauto. Qed.
Lemma refine_skip E K i:
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i Skip K d)
⊢ |={E}=>> ownT i (Lit LitUnit) K d'.
Proof. by eapply refine_seq; eauto. Qed.
Lemma refine_delay E e K i:
(d' < d)%nat →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i e K d)
⊢ |={E}=>> ownT i e K d'.
Proof.
intros Hlt ?. eapply refine_heap_pure_det'; eauto. intros.
eapply ownT_ownSP_delay; eauto.
split; omega.
Qed.
End heap.
is_Some (to_val e) → Closed (x :b: []) ef →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (App (Lam x ef) e) K d)
⊢ |={E}=>> ownT i (subst' x e ef) K d'.
Proof. intros. rewrite (refine_rec _ _ BAnon) //; eauto. Qed.
Lemma refine_let E K x e1 e2 i:
is_Some (to_val e1) → Closed (x :b: []) e2 →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Let x e1 e2) K d)
⊢ |={E}=>> ownT i (subst' x e1 e2) K d'.
Proof. apply refine_lam; eauto. Qed.
Lemma refine_seq E K e1 e2 i:
is_Some (to_val e1) → Closed [] e2 →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i (Seq e1 e2) K d)
⊢ |={E}=>> ownT i e2 K d'.
Proof. intros ??. apply refine_lam; eauto. Qed.
Lemma refine_skip E K i:
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i Skip K d)
⊢ |={E}=>> ownT i (Lit LitUnit) K d'.
Proof. by eapply refine_seq; eauto. Qed.
Lemma refine_delay E e K i:
(d' < d)%nat →
nclose sheapN ⊆ E →
(sheap_ctx ★ ownT i e K d)
⊢ |={E}=>> ownT i e K d'.
Proof.
intros Hlt ?. eapply refine_heap_pure_det'; eauto. intros.
eapply ownT_ownSP_delay; eauto.
split; omega.
Qed.
End heap.