Library iris.chan_lang.refine_heap
From iris.chan_lang Require Export lang derived refine.
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 scheapN : namespace := nroot .@ "scheap".
Definition scheapUR : ucmraT :=
gmapUR loc (exclR (prodC (listC valC) (listC valC)) trivial_stepN trivial_stepN_ustep).
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 scheapN : namespace := nroot .@ "scheap".
Definition scheapUR : ucmraT :=
gmapUR loc (exclR (prodC (listC valC) (listC valC)) trivial_stepN trivial_stepN_ustep).
The CMRA we need.
The Functor we need.
Definition scheapGF : gFunctor := authGF scheapUR.
Definition to_cheap : state → scheapUR := fmap (λ v, (Excl v)).
Definition of_cheap : scheapUR → state :=
omap (maybe Excl).
Section definitions.
Context `{i : scheapG Λ Σ}.
Context `{refineG Λ Σ (delayed_lang (chan_lang) Kd Fd) (S Kd × (Kd + 3))}.
Existing Instances gmap_empty.
Definition scheap_mapsto_def (l : loc) (v : list val × list val) : iPropG Λ Σ :=
auth_own scheap_name {[ l := (Excl v) ]}.
Definition scheap_mapsto_aux : { x | x = @scheap_mapsto_def }. by eexists. Qed.
Definition scheap_mapsto := proj1_sig scheap_mapsto_aux.
Definition scheap_mapsto_eq : @scheap_mapsto = @scheap_mapsto_def :=
proj2_sig scheap_mapsto_aux.
Definition scheap_inv (h : scheapUR) : iPropG Λ Σ :=
ownSP (of_cheap h).
Definition scheap_ctx : iPropG Λ Σ :=
auth_ctx scheap_name scheapN scheap_inv.
Global Instance scheap_inv_proper : Proper ((≡) ==> (⊣⊢)) scheap_inv.
Proof. solve_proper. Qed.
Global Instance scheap_ctx_relevant : RelevantP scheap_ctx.
Proof. apply _. Qed.
Global Instance scheap_ctx_affine : AffineP scheap_ctx.
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque scheap_ctx scheap_mapsto.
Notation "l ↦c v" := (scheap_mapsto l v)
(at level 20, format "l ↦c v") : uPred_scope.
Section heap.
Context {Σ : gFunctors}.
Context `{refineG Λ Σ (delayed_lang (chan_lang) Kd Fd) (S Kd × (Kd + 3))}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG Λ Σ.
Implicit Types Φ : val → iPropG Λ Σ.
Implicit Types σ : state.
Implicit Types h g : scheapUR.
Definition to_cheap : state → scheapUR := fmap (λ v, (Excl v)).
Definition of_cheap : scheapUR → state :=
omap (maybe Excl).
Section definitions.
Context `{i : scheapG Λ Σ}.
Context `{refineG Λ Σ (delayed_lang (chan_lang) Kd Fd) (S Kd × (Kd + 3))}.
Existing Instances gmap_empty.
Definition scheap_mapsto_def (l : loc) (v : list val × list val) : iPropG Λ Σ :=
auth_own scheap_name {[ l := (Excl v) ]}.
Definition scheap_mapsto_aux : { x | x = @scheap_mapsto_def }. by eexists. Qed.
Definition scheap_mapsto := proj1_sig scheap_mapsto_aux.
Definition scheap_mapsto_eq : @scheap_mapsto = @scheap_mapsto_def :=
proj2_sig scheap_mapsto_aux.
Definition scheap_inv (h : scheapUR) : iPropG Λ Σ :=
ownSP (of_cheap h).
Definition scheap_ctx : iPropG Λ Σ :=
auth_ctx scheap_name scheapN scheap_inv.
Global Instance scheap_inv_proper : Proper ((≡) ==> (⊣⊢)) scheap_inv.
Proof. solve_proper. Qed.
Global Instance scheap_ctx_relevant : RelevantP scheap_ctx.
Proof. apply _. Qed.
Global Instance scheap_ctx_affine : AffineP scheap_ctx.
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque scheap_ctx scheap_mapsto.
Notation "l ↦c v" := (scheap_mapsto l v)
(at level 20, format "l ↦c v") : uPred_scope.
Section heap.
Context {Σ : gFunctors}.
Context `{refineG Λ Σ (delayed_lang (chan_lang) Kd Fd) (S Kd × (Kd + 3))}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG Λ Σ.
Implicit Types Φ : val → iPropG Λ Σ.
Implicit Types σ : state.
Implicit Types h g : scheapUR.
Conversion to channel heaps and back
Global Instance of_cheap_proper : Proper ((≡) ==> (=)) of_cheap.
Proof. solve_proper. Qed.
Lemma from_to_heap σ : of_cheap (to_cheap σ) = σ.
Proof.
apply map_eq⇒l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
Qed.
Lemma to_heap_valid σ : ✓ to_cheap σ.
Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
Lemma of_heap_insert l v h :
of_cheap (<[l:=(Excl v)]> h) = <[l:=v]> (of_cheap h).
Proof. by rewrite /of_cheap -(omap_insert _ _ _ (Excl v)). Qed.
Lemma of_heap_singleton_op l v h :
✓ ({[l := Excl v]} ⋅ h) →
of_cheap ({[l := (Excl v)]} ⋅ h) = <[l:=v]> (of_cheap h).
Proof.
intros Hv. apply map_eq⇒ l'; destruct (decide (l' = l)) as [->|].
- move: (Hv l). rewrite /of_cheap lookup_insert
lookup_omap (lookup_op _ h) lookup_singleton.
case _:(h !! l)=>[[v'|]|] //=.
- rewrite /of_cheap lookup_insert_ne // !lookup_omap.
by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L.
Qed.
Lemma to_heap_insert l v σ :
to_cheap (<[l:=v]> σ) = <[l:=(Excl v)]> (to_cheap σ).
Proof. by rewrite /to_cheap -fmap_insert. Qed.
Lemma of_heap_None h l :
✓ h → of_cheap h !! l = None → h !! l = None.
Proof.
move⇒ /(_ l). rewrite /of_cheap lookup_omap.
case: (h !! l)=> [[v|]|] //=; destruct 1; auto.
Qed.
Lemma heap_store_valid l h v1 v2 :
✓ ({[l := (Excl v1)]} ⋅ h) →
✓ ({[l := (Excl v2)]} ⋅ h).
Proof.
intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
- rewrite !lookup_op !lookup_singleton.
case: (h !! l)=>[[v'|]|]; [|done|done]=> //.
- by rewrite !lookup_op !lookup_singleton_ne.
Qed.
Hint Resolve heap_store_valid.
Proof. solve_proper. Qed.
Lemma from_to_heap σ : of_cheap (to_cheap σ) = σ.
Proof.
apply map_eq⇒l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
Qed.
Lemma to_heap_valid σ : ✓ to_cheap σ.
Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
Lemma of_heap_insert l v h :
of_cheap (<[l:=(Excl v)]> h) = <[l:=v]> (of_cheap h).
Proof. by rewrite /of_cheap -(omap_insert _ _ _ (Excl v)). Qed.
Lemma of_heap_singleton_op l v h :
✓ ({[l := Excl v]} ⋅ h) →
of_cheap ({[l := (Excl v)]} ⋅ h) = <[l:=v]> (of_cheap h).
Proof.
intros Hv. apply map_eq⇒ l'; destruct (decide (l' = l)) as [->|].
- move: (Hv l). rewrite /of_cheap lookup_insert
lookup_omap (lookup_op _ h) lookup_singleton.
case _:(h !! l)=>[[v'|]|] //=.
- rewrite /of_cheap lookup_insert_ne // !lookup_omap.
by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L.
Qed.
Lemma to_heap_insert l v σ :
to_cheap (<[l:=v]> σ) = <[l:=(Excl v)]> (to_cheap σ).
Proof. by rewrite /to_cheap -fmap_insert. Qed.
Lemma of_heap_None h l :
✓ h → of_cheap h !! l = None → h !! l = None.
Proof.
move⇒ /(_ l). rewrite /of_cheap lookup_omap.
case: (h !! l)=> [[v|]|] //=; destruct 1; auto.
Qed.
Lemma heap_store_valid l h v1 v2 :
✓ ({[l := (Excl v1)]} ⋅ h) →
✓ ({[l := (Excl v2)]} ⋅ h).
Proof.
intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
- rewrite !lookup_op !lookup_singleton.
case: (h !! l)=>[[v'|]|]; [|done|done]=> //.
- by rewrite !lookup_op !lookup_singleton_ne.
Qed.
Hint Resolve heap_store_valid.
Allocation
Lemma scheap_alloc E σ :
authG Λ Σ scheapUR → nclose scheapN ⊆ E →
ownSP σ ={E}=> ∃ _ : scheapG Λ Σ, scheap_ctx ★ [★ map] l↦v ∈ σ, l ↦c v.
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{rewrite [ownSP _](affine_intro _ (ownSP (of_cheap (to_cheap σ)))); last auto.
rewrite [ownSP _]later_intro.
apply (auth_alloc (ownSP ∘ of_cheap) scheapN E); auto using to_heap_valid. }
apply pvs_mono, exist_elim⇒ γ.
rewrite -(exist_intro (SCheapG _ _ _ γ)) /scheap_ctx; apply sep_mono_r.
rewrite scheap_mapsto_eq /scheap_mapsto /scheap_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_cheap σ));
last by rewrite lookup_fmap Hl; auto.
by rewrite auth_own_op IH.
Qed.
Context `{scheapG Λ Σ}.
Existing Instances gmap_empty.
authG Λ Σ scheapUR → nclose scheapN ⊆ E →
ownSP σ ={E}=> ∃ _ : scheapG Λ Σ, scheap_ctx ★ [★ map] l↦v ∈ σ, l ↦c v.
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{rewrite [ownSP _](affine_intro _ (ownSP (of_cheap (to_cheap σ)))); last auto.
rewrite [ownSP _]later_intro.
apply (auth_alloc (ownSP ∘ of_cheap) scheapN E); auto using to_heap_valid. }
apply pvs_mono, exist_elim⇒ γ.
rewrite -(exist_intro (SCheapG _ _ _ γ)) /scheap_ctx; apply sep_mono_r.
rewrite scheap_mapsto_eq /scheap_mapsto /scheap_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_cheap σ));
last by rewrite lookup_fmap Hl; auto.
by rewrite auth_own_op IH.
Qed.
Context `{scheapG Λ Σ}.
Existing Instances gmap_empty.
General properties of mapsto
Global Instance scheap_mapsto_timeless l v : ATimelessP (l ↦c v).
Proof. rewrite scheap_mapsto_eq /scheap_mapsto_def. apply _. Qed.
Global Instance scheap_mapsto_affine l v : AffineP (l ↦c v).
Proof. rewrite scheap_mapsto_eq /scheap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_map_affine σ:
AffineP ([★ map] l↦v ∈ σ, l ↦c 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 scheap_mapsto_affine.
Qed.
Lemma scheap_mapsto_op l v1 v2 :
(l ↦c v1 ★ l ↦c v2) ⊣⊢ False.
Proof.
rewrite scheap_mapsto_eq -auth_own_op op_singleton //.
apply (anti_symm (⊢)); last by apply False_elim.
rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
rewrite option_validI excl_validI /op /excl_op //=.
apply affine_elim.
Qed.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export weakestpre.
Implicit Types Δ : envs (iResUR Λ (globalF Σ)).
Context (d d': nat).
Context (Hd_le: (d ≤ Kd)%nat).
Context (Hd'_le: (d' ≤ Kd)%nat).
Proof. rewrite scheap_mapsto_eq /scheap_mapsto_def. apply _. Qed.
Global Instance scheap_mapsto_affine l v : AffineP (l ↦c v).
Proof. rewrite scheap_mapsto_eq /scheap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_map_affine σ:
AffineP ([★ map] l↦v ∈ σ, l ↦c 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 scheap_mapsto_affine.
Qed.
Lemma scheap_mapsto_op l v1 v2 :
(l ↦c v1 ★ l ↦c v2) ⊣⊢ False.
Proof.
rewrite scheap_mapsto_eq -auth_own_op op_singleton //.
apply (anti_symm (⊢)); last by apply False_elim.
rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
rewrite option_validI excl_validI /op /excl_op //=.
apply affine_elim.
Qed.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export weakestpre.
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 :
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Alloc) K d) ⊢
(|={E}=>> ∃ l, l ↦c ([], [])
★ ownT i (Pair (Lit (LitLoc l cleft))
(Lit (LitLoc l cright))) K d').
Proof.
iIntros (?) "[#Hinv HΦ]". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite (refine_alloc_pst' (E ∖ scheapN) _ _ _ d'); eauto.
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
rewrite /auth_inv.
iPoseProof (auth_empty scheap_name (E ∖ scheapN)) 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_cheap a'))).
pose (a := ({[l :=(Excl ([], []))]} ⋅ a')).
iPoseProof (own_update _ _ (● a ⋅ ◯ {[l := (Excl ([], []))]})%I (E ∖ scheapN) with "Hheap2")
as "Hown".
{ rewrite /a //=.
generalize (auth_update ∅ a' {[ l := Excl ([], []) ]}).
rewrite ?left_id ?right_id. intros Hupd. eapply Hupd; eauto.
eapply alloc_singleton_local_update.
- apply of_heap_None, (not_elem_of_dom (D:= gset _)).
× by rewrite //= left_id.
× rewrite //= left_id; eapply is_fresh.
- econstructor; simpl; rewrite //=.
}
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". 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 scheap_mapsto_eq /scheap_mapsto_def /auth_own. iFrame "Hγf".
iClear "Hinv"; auto.
Qed.
Lemma refine_recv_miss_left E i K l l1:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Recv (Lit (LitLoc l cleft))) K d ★ l ↦c (l1, []))
⊢ (|={E}=>> ownT i (Recv (Lit (LitLoc l cleft))) K d' ★ l ↦c (l1, [])).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_recv_left_miss_pst (E ∖ scheapN) (of_cheap 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 _.
done.
- by iFrame "HT".
Qed.
Lemma refine_recv_miss_right E i K l l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Recv (Lit (LitLoc l cright))) K d ★ l ↦c ([], l2))
⊢ (|={E}=>> ownT i (Recv (Lit (LitLoc l cright))) K d' ★ l ↦c ([], l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_recv_right_miss_pst (E ∖ scheapN) (of_cheap 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 _.
done.
- by iFrame "HT".
Qed.
Lemma refine_recv_left E i K l v l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Recv (Lit (LitLoc l cleft))) K d ★ l ↦c (l1, v :: l2))
⊢ (|={E}=>> ownT i (Pair (Lit (LitLoc l cleft)) (of_val v)) K d' ★ l ↦c (l1, l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_recv_left_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2)]})%I (E ∖ scheapN) with "Hγ'") as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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.
- by iFrame "HT".
Qed.
Lemma refine_recv_right E i K l v l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Recv (Lit (LitLoc l cright))) K d ★ l ↦c (v :: l1, l2))
⊢ (|={E}=>> ownT i (Pair (Lit (LitLoc l cright)) (of_val v)) K d' ★ l ↦c (l1, l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_recv_right_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_send_left E i K l e v l1 l2:
to_val e = Some v → nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Send (Lit (LitLoc l cleft)) e) K d ★ l ↦c (l1, l2))
⊢ (|={E}=>> ownT i (Lit (LitLoc l cleft)) K d' ★ l ↦c (l1 ++ [v], l2)).
Proof.
iIntros (??) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_send_left_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1 ++ [v], l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1 ++ [v], l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_send_right E i K l e v l1 l2:
to_val e = Some v → nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Send (Lit (LitLoc l cright)) e) K d ★ l ↦c (l1, l2))
⊢ (|={E}=>> ownT i (Lit (LitLoc l cright)) K d' ★ l ↦c (l1, l2 ++ [v])).
Proof.
iIntros (??) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_send_right_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2 ++ [v])]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2 ++ [v])]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_select_left E i K l s l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Select (Lit (LitLoc l cleft)) s) K d ★ l ↦c (l1, l2))
⊢ (|={E}=>> ownT i (Lit (LitLoc l cleft)) K d'
★ l ↦c (l1 ++ [label_to_sum s], l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_select_left_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (v := label_to_sum s).
pose (a := ({[l :=Excl (l1 ++ [v], l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1 ++ [v], l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_select_right E i K l s l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Select (Lit (LitLoc l cright)) s) K d ★ l ↦c (l1, l2))
⊢ (|={E}=>> ownT i (Lit (LitLoc l cright)) K d'
★ l ↦c (l1, l2 ++ [(label_to_sum s)])).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_select_right_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (v := label_to_sum s).
pose (a := ({[l :=Excl (l1, l2 ++ [v])]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2 ++ [v])]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_rcase_miss_left E i K l e1 e2 l1:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d ★ l ↦c (l1, []))
⊢ (|={E}=>> ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d' ★ l ↦c (l1, [])).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_rcase_left_miss_pst (E ∖ scheapN) (of_cheap 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_rcase_miss_right E i K l e1 e2 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d ★ l ↦c ([], l2))
⊢ (|={E}=>> ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d' ★ l ↦c ([], l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_rcase_right_miss_pst (E ∖ scheapN) (of_cheap 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_rcase_left_left E i K l e1 e2 l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d
★ l ↦c (l1, InjLV (LitV LitUnit) :: l2))
⊢ (|={E}=>> ownT i (App e1 (Lit (LitLoc l cleft))) K d' ★ l ↦c (l1, l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_rcase_left_left_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_rcase_left_right E i K l e1 e2 l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d
★ l ↦c (l1, InjRV (LitV LitUnit) :: l2))
⊢ (|={E}=>> ownT i (App e2 (Lit (LitLoc l cleft))) K d' ★ l ↦c (l1, l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_rcase_left_right_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_rcase_right_left E i K l e1 e2 l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d
★ l ↦c (InjLV (LitV LitUnit) :: l1, l2))
⊢ (|={E}=>> ownT i (App e1 (Lit (LitLoc l cright))) K d' ★ l ↦c (l1, l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_rcase_right_left_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_rcase_right_right E i K l e1 e2 l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d
★ l ↦c (InjRV (LitV LitUnit) :: l1, l2))
⊢ (|={E}=>> ownT i (App e2 (Lit (LitLoc l cright))) K d' ★ l ↦c (l1, l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_rcase_right_right_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_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 scheapN ⊆ E →
(scheap_ctx ★ ownT i e1 K d)
⊢ (|={E}=>> ownT i e2 K d').
Proof.
iIntros (? Hred Hdet ?) "(#Hinv&HΦ)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
edestruct (Hred (of_cheap 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 scheapN ⊆ E →
(scheap_ctx ★ ownT i e1 K d)
⊢ (|={E}=>> ownT i e2 K d').
Proof.
iIntros (Hstep ?) "(#Hinv&HΦ)". rewrite /scheap_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 /scheap_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 scheapN ⊆ E →
(scheap_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 /scheap_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 /scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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_letp E K x y e1 v1 e2 v2 eb i :
to_val e1 = Some v1 → to_val e2 = Some v2 →
Closed (x :b: y :b: []) eb →
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Letp x y (Pair e1 e2) eb) K d) ⊢
|={E}=>> ownT i (subst' y e2 (subst' x e1 eb)) K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_letp_pst. Qed.
Lemma refine_case_inl E K e0 v0 e1 e2 i :
to_val e0 = Some v0 →
nclose scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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.
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Alloc) K d) ⊢
(|={E}=>> ∃ l, l ↦c ([], [])
★ ownT i (Pair (Lit (LitLoc l cleft))
(Lit (LitLoc l cright))) K d').
Proof.
iIntros (?) "[#Hinv HΦ]". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite (refine_alloc_pst' (E ∖ scheapN) _ _ _ d'); eauto.
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
rewrite /auth_inv.
iPoseProof (auth_empty scheap_name (E ∖ scheapN)) 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_cheap a'))).
pose (a := ({[l :=(Excl ([], []))]} ⋅ a')).
iPoseProof (own_update _ _ (● a ⋅ ◯ {[l := (Excl ([], []))]})%I (E ∖ scheapN) with "Hheap2")
as "Hown".
{ rewrite /a //=.
generalize (auth_update ∅ a' {[ l := Excl ([], []) ]}).
rewrite ?left_id ?right_id. intros Hupd. eapply Hupd; eauto.
eapply alloc_singleton_local_update.
- apply of_heap_None, (not_elem_of_dom (D:= gset _)).
× by rewrite //= left_id.
× rewrite //= left_id; eapply is_fresh.
- econstructor; simpl; rewrite //=.
}
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". 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 scheap_mapsto_eq /scheap_mapsto_def /auth_own. iFrame "Hγf".
iClear "Hinv"; auto.
Qed.
Lemma refine_recv_miss_left E i K l l1:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Recv (Lit (LitLoc l cleft))) K d ★ l ↦c (l1, []))
⊢ (|={E}=>> ownT i (Recv (Lit (LitLoc l cleft))) K d' ★ l ↦c (l1, [])).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_recv_left_miss_pst (E ∖ scheapN) (of_cheap 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 _.
done.
- by iFrame "HT".
Qed.
Lemma refine_recv_miss_right E i K l l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Recv (Lit (LitLoc l cright))) K d ★ l ↦c ([], l2))
⊢ (|={E}=>> ownT i (Recv (Lit (LitLoc l cright))) K d' ★ l ↦c ([], l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_recv_right_miss_pst (E ∖ scheapN) (of_cheap 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 _.
done.
- by iFrame "HT".
Qed.
Lemma refine_recv_left E i K l v l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Recv (Lit (LitLoc l cleft))) K d ★ l ↦c (l1, v :: l2))
⊢ (|={E}=>> ownT i (Pair (Lit (LitLoc l cleft)) (of_val v)) K d' ★ l ↦c (l1, l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_recv_left_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2)]})%I (E ∖ scheapN) with "Hγ'") as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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.
- by iFrame "HT".
Qed.
Lemma refine_recv_right E i K l v l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Recv (Lit (LitLoc l cright))) K d ★ l ↦c (v :: l1, l2))
⊢ (|={E}=>> ownT i (Pair (Lit (LitLoc l cright)) (of_val v)) K d' ★ l ↦c (l1, l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_recv_right_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_send_left E i K l e v l1 l2:
to_val e = Some v → nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Send (Lit (LitLoc l cleft)) e) K d ★ l ↦c (l1, l2))
⊢ (|={E}=>> ownT i (Lit (LitLoc l cleft)) K d' ★ l ↦c (l1 ++ [v], l2)).
Proof.
iIntros (??) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_send_left_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1 ++ [v], l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1 ++ [v], l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_send_right E i K l e v l1 l2:
to_val e = Some v → nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Send (Lit (LitLoc l cright)) e) K d ★ l ↦c (l1, l2))
⊢ (|={E}=>> ownT i (Lit (LitLoc l cright)) K d' ★ l ↦c (l1, l2 ++ [v])).
Proof.
iIntros (??) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_send_right_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2 ++ [v])]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2 ++ [v])]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_select_left E i K l s l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Select (Lit (LitLoc l cleft)) s) K d ★ l ↦c (l1, l2))
⊢ (|={E}=>> ownT i (Lit (LitLoc l cleft)) K d'
★ l ↦c (l1 ++ [label_to_sum s], l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_select_left_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (v := label_to_sum s).
pose (a := ({[l :=Excl (l1 ++ [v], l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1 ++ [v], l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_select_right E i K l s l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Select (Lit (LitLoc l cright)) s) K d ★ l ↦c (l1, l2))
⊢ (|={E}=>> ownT i (Lit (LitLoc l cright)) K d'
★ l ↦c (l1, l2 ++ [(label_to_sum s)])).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_select_right_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (v := label_to_sum s).
pose (a := ({[l :=Excl (l1, l2 ++ [v])]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2 ++ [v])]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_rcase_miss_left E i K l e1 e2 l1:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d ★ l ↦c (l1, []))
⊢ (|={E}=>> ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d' ★ l ↦c (l1, [])).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_rcase_left_miss_pst (E ∖ scheapN) (of_cheap 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_rcase_miss_right E i K l e1 e2 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d ★ l ↦c ([], l2))
⊢ (|={E}=>> ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d' ★ l ↦c ([], l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_rcase_right_miss_pst (E ∖ scheapN) (of_cheap 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_rcase_left_left E i K l e1 e2 l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d
★ l ↦c (l1, InjLV (LitV LitUnit) :: l2))
⊢ (|={E}=>> ownT i (App e1 (Lit (LitLoc l cleft))) K d' ★ l ↦c (l1, l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_rcase_left_left_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_rcase_left_right E i K l e1 e2 l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (RCase (Lit (LitLoc l cleft)) e1 e2) K d
★ l ↦c (l1, InjRV (LitV LitUnit) :: l2))
⊢ (|={E}=>> ownT i (App e2 (Lit (LitLoc l cleft))) K d' ★ l ↦c (l1, l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_rcase_left_right_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_rcase_right_left E i K l e1 e2 l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d
★ l ↦c (InjLV (LitV LitUnit) :: l1, l2))
⊢ (|={E}=>> ownT i (App e1 (Lit (LitLoc l cright))) K d' ★ l ↦c (l1, l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_rcase_right_left_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_rcase_right_right E i K l e1 e2 l1 l2:
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (RCase (Lit (LitLoc l cright)) e1 e2) K d
★ l ↦c (InjRV (LitV LitUnit) :: l1, l2))
⊢ (|={E}=>> ownT i (App e2 (Lit (LitLoc l cright))) K d' ★ l ↦c (l1, l2)).
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
rewrite scheap_mapsto_eq /scheap_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_rcase_right_right_pst (E ∖ scheapN) (of_cheap a')); eauto;
last (by setoid_subst; rewrite of_heap_singleton_op // lookup_insert).
iPsvs "Hrefine".
iDestruct "Hrefine" as "(HT&HS)".
pose (a := ({[l :=Excl (l1, l2)]} ⋅ b)).
iPvs (own_update _ _ (● a ⋅ ◯ {[l := Excl (l1, l2)]})%I (E ∖ scheapN) with "Hγ'")
as "Hown".
{ rewrite /a. setoid_subst.
by eapply auth_update, singleton_local_update, exclusive_local_update. }
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_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 scheapN ⊆ E →
(scheap_ctx ★ ownT i e1 K d)
⊢ (|={E}=>> ownT i e2 K d').
Proof.
iIntros (? Hred Hdet ?) "(#Hinv&HΦ)". rewrite /scheap_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 /scheap_inv.
rewrite affine_elim affine_elim affine_elim.
iCombine "HΦ" "Hφ" as "Hrefine".
edestruct (Hred (of_cheap 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 scheapN ⊆ E →
(scheap_ctx ★ ownT i e1 K d)
⊢ (|={E}=>> ownT i e2 K d').
Proof.
iIntros (Hstep ?) "(#Hinv&HΦ)". rewrite /scheap_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 /scheap_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 scheapN ⊆ E →
(scheap_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 /scheap_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 /scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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_letp E K x y e1 v1 e2 v2 eb i :
to_val e1 = Some v1 → to_val e2 = Some v2 →
Closed (x :b: y :b: []) eb →
nclose scheapN ⊆ E →
(scheap_ctx ★ ownT i (Letp x y (Pair e1 e2) eb) K d) ⊢
|={E}=>> ownT i (subst' y e2 (subst' x e1 eb)) K d'.
Proof. intros; eapply refine_heap_pure_det'; eauto using refine_letp_pst. Qed.
Lemma refine_case_inl E K e0 v0 e1 e2 i :
to_val e0 = Some v0 →
nclose scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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 scheapN ⊆ E →
(scheap_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.