Library iris.heap_lang.heap
From iris.heap_lang Require Export lifting.
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.
Import uPred.
Definition heapN : namespace := nroot .@ "heap".
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
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.
Import uPred.
Definition heapN : namespace := nroot .@ "heap".
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
The CMRA we need.
The Functor we need.
Definition heapGF : gFunctor := authGF heapUR.
Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)).
Definition of_heap : heapUR → state := omap (maybe DecAgree ∘ snd).
Section definitions.
Context `{heapG Σ}.
Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iPropG heap_lang Σ :=
auth_own heap_name {[ l := (q, DecAgree v) ]}.
Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
Definition heap_mapsto := proj1_sig heap_mapsto_aux.
Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
proj2_sig heap_mapsto_aux.
Definition heap_inv (h : heapUR) : iPropG heap_lang Σ :=
ownP (of_heap h).
Definition heap_ctx : iPropG heap_lang Σ :=
auth_ctx heap_name heapN heap_inv.
Global Instance heap_inv_proper : Proper ((≡) ==> (⊣⊢)) heap_inv.
Proof. solve_proper. Qed.
Global Instance heap_ctx_relevant : RelevantP heap_ctx.
Proof. apply _. Qed.
Global Instance heap_ctx_affine : AffineP heap_ctx.
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque heap_ctx heap_mapsto.
Instance: Params (@heap_inv) 1.
Instance: Params (@heap_mapsto) 4.
Instance: Params (@heap_ctx) 2.
Notation "l ↦{ q } v" := (heap_mapsto l q v)
(at level 20, q at level 50, format "l ↦{ q } v") : uPred_scope.
Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
Section heap.
Context {Σ : gFunctors}.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val → iPropG heap_lang Σ.
Implicit Types σ : state.
Implicit Types h g : heapUR.
Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)).
Definition of_heap : heapUR → state := omap (maybe DecAgree ∘ snd).
Section definitions.
Context `{heapG Σ}.
Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iPropG heap_lang Σ :=
auth_own heap_name {[ l := (q, DecAgree v) ]}.
Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
Definition heap_mapsto := proj1_sig heap_mapsto_aux.
Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
proj2_sig heap_mapsto_aux.
Definition heap_inv (h : heapUR) : iPropG heap_lang Σ :=
ownP (of_heap h).
Definition heap_ctx : iPropG heap_lang Σ :=
auth_ctx heap_name heapN heap_inv.
Global Instance heap_inv_proper : Proper ((≡) ==> (⊣⊢)) heap_inv.
Proof. solve_proper. Qed.
Global Instance heap_ctx_relevant : RelevantP heap_ctx.
Proof. apply _. Qed.
Global Instance heap_ctx_affine : AffineP heap_ctx.
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque heap_ctx heap_mapsto.
Instance: Params (@heap_inv) 1.
Instance: Params (@heap_mapsto) 4.
Instance: Params (@heap_ctx) 2.
Notation "l ↦{ q } v" := (heap_mapsto l q v)
(at level 20, q at level 50, format "l ↦{ q } v") : uPred_scope.
Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
Section heap.
Context {Σ : gFunctors}.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val → iPropG heap_lang Σ.
Implicit Types σ : state.
Implicit Types h g : heapUR.
Conversion to heaps and back
Global Instance of_heap_proper : Proper ((≡) ==> (=)) of_heap.
Proof. solve_proper. Qed.
Lemma from_to_heap σ : of_heap (to_heap σ) = σ.
Proof.
apply map_eq⇒l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
Qed.
Lemma to_heap_valid σ : ✓ to_heap σ.
Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
Lemma of_heap_insert l v h :
of_heap (<[l:=(1%Qp, DecAgree v)]> h) = <[l:=v]> (of_heap h).
Proof. by rewrite /of_heap -(omap_insert _ _ _ (1%Qp, DecAgree v)). Qed.
Lemma of_heap_singleton_op l q v h :
✓ ({[l := (q, DecAgree v)]} ⋅ h) →
of_heap ({[l := (q, DecAgree v)]} ⋅ h) = <[l:=v]> (of_heap h).
Proof.
intros Hv. apply map_eq⇒ l'; destruct (decide (l' = l)) as [->|].
- move: (Hv l). rewrite /of_heap lookup_insert
lookup_omap (lookup_op _ h) lookup_singleton.
case _:(h !! l)=>[[q' [v'|]]|] //=; last by move⇒ [??].
move⇒ [? /dec_agree_op_inv [->]]. by rewrite dec_agree_idemp.
- rewrite /of_heap lookup_insert_ne // !lookup_omap.
by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L.
Qed.
Lemma to_heap_insert l v σ :
to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ).
Proof. by rewrite /to_heap -fmap_insert. Qed.
Lemma of_heap_None h l : ✓ h → of_heap h !! l = None → h !! l = None.
Proof.
move⇒ /(_ l). rewrite /of_heap lookup_omap.
by case: (h !! l)=> [[q [v|]]|] //=; destruct 1; auto.
Qed.
Lemma heap_store_valid l h v1 v2 :
✓ ({[l := (1%Qp, DecAgree v1)]} ⋅ h) →
✓ ({[l := (1%Qp, DecAgree v2)]} ⋅ h).
Proof.
intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
- rewrite !lookup_op !lookup_singleton.
by case: (h !! l)=> [x|] // /Some_valid/exclusive_l.
- by rewrite !lookup_op !lookup_singleton_ne.
Qed.
Hint Resolve heap_store_valid.
Proof. solve_proper. Qed.
Lemma from_to_heap σ : of_heap (to_heap σ) = σ.
Proof.
apply map_eq⇒l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
Qed.
Lemma to_heap_valid σ : ✓ to_heap σ.
Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
Lemma of_heap_insert l v h :
of_heap (<[l:=(1%Qp, DecAgree v)]> h) = <[l:=v]> (of_heap h).
Proof. by rewrite /of_heap -(omap_insert _ _ _ (1%Qp, DecAgree v)). Qed.
Lemma of_heap_singleton_op l q v h :
✓ ({[l := (q, DecAgree v)]} ⋅ h) →
of_heap ({[l := (q, DecAgree v)]} ⋅ h) = <[l:=v]> (of_heap h).
Proof.
intros Hv. apply map_eq⇒ l'; destruct (decide (l' = l)) as [->|].
- move: (Hv l). rewrite /of_heap lookup_insert
lookup_omap (lookup_op _ h) lookup_singleton.
case _:(h !! l)=>[[q' [v'|]]|] //=; last by move⇒ [??].
move⇒ [? /dec_agree_op_inv [->]]. by rewrite dec_agree_idemp.
- rewrite /of_heap lookup_insert_ne // !lookup_omap.
by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L.
Qed.
Lemma to_heap_insert l v σ :
to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ).
Proof. by rewrite /to_heap -fmap_insert. Qed.
Lemma of_heap_None h l : ✓ h → of_heap h !! l = None → h !! l = None.
Proof.
move⇒ /(_ l). rewrite /of_heap lookup_omap.
by case: (h !! l)=> [[q [v|]]|] //=; destruct 1; auto.
Qed.
Lemma heap_store_valid l h v1 v2 :
✓ ({[l := (1%Qp, DecAgree v1)]} ⋅ h) →
✓ ({[l := (1%Qp, DecAgree v2)]} ⋅ h).
Proof.
intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
- rewrite !lookup_op !lookup_singleton.
by case: (h !! l)=> [x|] // /Some_valid/exclusive_l.
- by rewrite !lookup_op !lookup_singleton_ne.
Qed.
Hint Resolve heap_store_valid.
Allocation
Lemma heap_alloc E σ :
authG heap_lang Σ heapUR → nclose heapN ⊆ E →
ownP σ ={E}=> ∃ _ : heapG Σ, heap_ctx ★ [★ map] l↦v ∈ σ, l ↦ v.
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{rewrite [ownP _](affine_intro _ (ownP (of_heap (to_heap σ)))); last auto.
rewrite [ownP _]later_intro.
apply (auth_alloc (ownP ∘ of_heap) heapN E); auto using to_heap_valid. }
apply pvs_mono, exist_elim⇒ γ.
rewrite -(exist_intro (HeapG _ _ γ)) /heap_ctx. apply sep_mono_r.
rewrite heap_mapsto_eq /heap_mapsto_def /heap_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 `{heapG Σ}.
authG heap_lang Σ heapUR → nclose heapN ⊆ E →
ownP σ ={E}=> ∃ _ : heapG Σ, heap_ctx ★ [★ map] l↦v ∈ σ, l ↦ v.
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{rewrite [ownP _](affine_intro _ (ownP (of_heap (to_heap σ)))); last auto.
rewrite [ownP _]later_intro.
apply (auth_alloc (ownP ∘ of_heap) heapN E); auto using to_heap_valid. }
apply pvs_mono, exist_elim⇒ γ.
rewrite -(exist_intro (HeapG _ _ γ)) /heap_ctx. apply sep_mono_r.
rewrite heap_mapsto_eq /heap_mapsto_def /heap_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 `{heapG Σ}.
General properties of mapsto
Global Instance heap_mapsto_timeless l q v : ATimelessP (l ↦{q} v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_affine l q v : AffineP (l ↦{q} v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_map_affine σ:
AffineP ([★ map] l↦v ∈σ, l ↦ 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 heap_mapsto_affine.
Qed.
Lemma heap_mapsto_op_eq l q1 q2 v : (l ↦{q1} v ★ l ↦{q2} v) ⊣⊢ l ↦{q1+q2} v.
Proof. by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp. Qed.
Lemma heap_mapsto_op l q1 q2 v1 v2 :
(l ↦{q1} v1 ★ l ↦{q2} v2) ⊣⊢ (⧆ (v1 = v2) ★ l ↦{q1+q2} v1).
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq pure_equiv // -emp_True left_id. }
rewrite heap_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 heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v).
Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_affine l q v : AffineP (l ↦{q} v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_map_affine σ:
AffineP ([★ map] l↦v ∈σ, l ↦ 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 heap_mapsto_affine.
Qed.
Lemma heap_mapsto_op_eq l q1 q2 v : (l ↦{q1} v ★ l ↦{q2} v) ⊣⊢ l ↦{q1+q2} v.
Proof. by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp. Qed.
Lemma heap_mapsto_op l q1 q2 v1 v2 :
(l ↦{q1} v1 ★ l ↦{q2} v2) ⊣⊢ (⧆ (v1 = v2) ★ l ↦{q1+q2} v1).
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq pure_equiv // -emp_True left_id. }
rewrite heap_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 heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v).
Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
Weakest precondition
Lemma wp_alloc E e v Φ :
to_val e = Some v → nclose heapN ⊆ E →
(heap_ctx ★ ▷ ∀ l, l ↦ v -★ |={E ∖ heapN}=>> Φ (LitV $ LitLoc l)) ⊢ WP Alloc e @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap".
iApply wp_pvs; iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hinv". iSplitL "Hheap"; first (iIntros "@"; by iNext).
iIntros (h). rewrite left_id.
iIntros "[% Hheap]". rewrite /heap_inv.
pose (l := fresh (dom _ (of_heap h))).
iExists {[ l := (1%Qp, DecAgree v) ]}.
rewrite -(insert_singleton_op h);
last by (apply of_heap_None, (not_elem_of_dom (D:= gset _)), is_fresh).
iSplitL "".
{ iPureIntro. apply alloc_unit_singleton_local_update; last done.
by apply of_heap_None, (not_elem_of_dom (D:= gset _)), is_fresh; eauto. }
iIntros "Hauth".
iApply wp_alloc_pst'. iFrame "Hheap". iNext.
iIntros "Hheap".
rewrite -of_heap_insert.
rewrite -{1}(affine_affine (ownP _)) {1}(later_intro (ownP _)).
iFrame "Hheap".
iSpecialize ("HΦ" $! l). rewrite -(pvs_intro).
iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
Qed.
Lemma wp_load E l q v Φ :
nclose heapN ⊆ E →
(heap_ctx ★ ⧆▷ l ↦{q} v ★ ▷(⧆ l ↦{q} v -★ |={E ∖ heapN}=>> (Φ v)))
⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
iIntros (?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iExists _.
iSplitL "".
{ iPureIntro. reflexivity. }
iIntros "Hauth".
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "Hown". rewrite -pvs_intro. iApply "HΦ".
by iIntros "@".
Qed.
Lemma wp_store E l v' e v Φ :
to_val e = Some v → nclose heapN ⊆ E →
(heap_ctx ★ ⧆▷ l ↦ v' ★ ▷ (l ↦ v -★ |={E ∖ heapN}=>> ( Φ (LitV LitUnit))))
⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iExists {[ l := (1%Qp, DecAgree v) ]}.
iSplitL "".
{ iPureIntro; by apply singleton_local_update, exclusive_local_update. }
iIntros "Hauth".
iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); eauto; first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
rewrite insert_insert !of_heap_singleton_op; eauto.
iFrame "Hown". rewrite -pvs_intro. by iApply "HΦ".
Qed.
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose heapN ⊆ E →
heap_ctx ★ ⧆▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ |={E ∖ heapN}=>> Φ (LitV (LitBool false)))
⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ??) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iExists {[ l := (q, DecAgree v') ]}.
iSplitL "".
{ iPureIntro; naive_solver. }
iIntros "Hauth".
iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "HownP". iApply "HΦ"; done.
Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose heapN ⊆ E →
heap_ctx ★ ⧆▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ |={E ∖ heapN}=>> (Φ (LitV (LitBool true))))
⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iExists {[ l := (1%Qp, DecAgree v2) ]}.
iSplitL "".
{ iPureIntro; by apply singleton_local_update, exclusive_local_update. }
iIntros "Hauth".
iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "HownP".
iApply psvs_mono; last auto. iIntros "$"; auto.
iApply ("HΦ"); done.
Qed.
Lemma wp_swap E l v e v' Φ :
to_val e = Some v' → nclose heapN ⊆ E →
heap_ctx ★ ⧆▷ l ↦ v ★ ▷ (l ↦ v' -★ |={E ∖ heapN}=>> (Φ v))
⊢ WP Swap (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iExists {[ l := (1%Qp, DecAgree v') ]}.
iSplitL "".
{ iPureIntro; by apply singleton_local_update, exclusive_local_update. }
iIntros "Hauth".
iApply (wp_swap_pst _ (<[l:=v]>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "HownP".
iApply psvs_mono; last auto. iIntros "$"; auto.
iApply ("HΦ"); done.
Qed.
Lemma wp_fai E l k Φ :
nclose heapN ⊆ E →
heap_ctx ★ ⧆▷ l ↦ (LitV $ LitInt k)
★ ▷ (l ↦ (LitV $ LitInt (k+1)) -★ |={E ∖ heapN}=>> (Φ (LitV $ LitInt k)))
⊢ WP FAI (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
iIntros (?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iExists {[ l := (1%Qp, DecAgree (LitV $ LitInt (k+1))) ]}.
iSplitL "".
{ iPureIntro; by apply singleton_local_update, exclusive_local_update. }
iIntros "Hauth".
iApply (wp_fai_pst _ (<[l:=LitV $ LitInt k]>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "HownP".
iApply psvs_mono; last auto. iIntros "$"; auto.
iApply ("HΦ"); done.
Qed.
End heap.
to_val e = Some v → nclose heapN ⊆ E →
(heap_ctx ★ ▷ ∀ l, l ↦ v -★ |={E ∖ heapN}=>> Φ (LitV $ LitLoc l)) ⊢ WP Alloc e @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap".
iApply wp_pvs; iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hinv". iSplitL "Hheap"; first (iIntros "@"; by iNext).
iIntros (h). rewrite left_id.
iIntros "[% Hheap]". rewrite /heap_inv.
pose (l := fresh (dom _ (of_heap h))).
iExists {[ l := (1%Qp, DecAgree v) ]}.
rewrite -(insert_singleton_op h);
last by (apply of_heap_None, (not_elem_of_dom (D:= gset _)), is_fresh).
iSplitL "".
{ iPureIntro. apply alloc_unit_singleton_local_update; last done.
by apply of_heap_None, (not_elem_of_dom (D:= gset _)), is_fresh; eauto. }
iIntros "Hauth".
iApply wp_alloc_pst'. iFrame "Hheap". iNext.
iIntros "Hheap".
rewrite -of_heap_insert.
rewrite -{1}(affine_affine (ownP _)) {1}(later_intro (ownP _)).
iFrame "Hheap".
iSpecialize ("HΦ" $! l). rewrite -(pvs_intro).
iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
Qed.
Lemma wp_load E l q v Φ :
nclose heapN ⊆ E →
(heap_ctx ★ ⧆▷ l ↦{q} v ★ ▷(⧆ l ↦{q} v -★ |={E ∖ heapN}=>> (Φ v)))
⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
iIntros (?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iExists _.
iSplitL "".
{ iPureIntro. reflexivity. }
iIntros "Hauth".
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "Hown". rewrite -pvs_intro. iApply "HΦ".
by iIntros "@".
Qed.
Lemma wp_store E l v' e v Φ :
to_val e = Some v → nclose heapN ⊆ E →
(heap_ctx ★ ⧆▷ l ↦ v' ★ ▷ (l ↦ v -★ |={E ∖ heapN}=>> ( Φ (LitV LitUnit))))
⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iExists {[ l := (1%Qp, DecAgree v) ]}.
iSplitL "".
{ iPureIntro; by apply singleton_local_update, exclusive_local_update. }
iIntros "Hauth".
iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); eauto; first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
rewrite insert_insert !of_heap_singleton_op; eauto.
iFrame "Hown". rewrite -pvs_intro. by iApply "HΦ".
Qed.
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose heapN ⊆ E →
heap_ctx ★ ⧆▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ |={E ∖ heapN}=>> Φ (LitV (LitBool false)))
⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ??) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iExists {[ l := (q, DecAgree v') ]}.
iSplitL "".
{ iPureIntro; naive_solver. }
iIntros "Hauth".
iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "HownP". iApply "HΦ"; done.
Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose heapN ⊆ E →
heap_ctx ★ ⧆▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ |={E ∖ heapN}=>> (Φ (LitV (LitBool true))))
⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iExists {[ l := (1%Qp, DecAgree v2) ]}.
iSplitL "".
{ iPureIntro; by apply singleton_local_update, exclusive_local_update. }
iIntros "Hauth".
iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "HownP".
iApply psvs_mono; last auto. iIntros "$"; auto.
iApply ("HΦ"); done.
Qed.
Lemma wp_swap E l v e v' Φ :
to_val e = Some v' → nclose heapN ⊆ E →
heap_ctx ★ ⧆▷ l ↦ v ★ ▷ (l ↦ v' -★ |={E ∖ heapN}=>> (Φ v))
⊢ WP Swap (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iExists {[ l := (1%Qp, DecAgree v') ]}.
iSplitL "".
{ iPureIntro; by apply singleton_local_update, exclusive_local_update. }
iIntros "Hauth".
iApply (wp_swap_pst _ (<[l:=v]>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "HownP".
iApply psvs_mono; last auto. iIntros "$"; auto.
iApply ("HΦ"); done.
Qed.
Lemma wp_fai E l k Φ :
nclose heapN ⊆ E →
heap_ctx ★ ⧆▷ l ↦ (LitV $ LitInt k)
★ ▷ (l ↦ (LitV $ LitInt (k+1)) -★ |={E ∖ heapN}=>> (Φ (LitV $ LitInt k)))
⊢ WP FAI (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
iIntros (?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply (auth_afsa_alt heap_inv (wp_fsa _)); eauto with fsaV.
iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iExists {[ l := (1%Qp, DecAgree (LitV $ LitInt (k+1))) ]}.
iSplitL "".
{ iPureIntro; by apply singleton_local_update, exclusive_local_update. }
iIntros "Hauth".
iApply (wp_fai_pst _ (<[l:=LitV $ LitInt k]>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
iFrame "HownP".
iApply psvs_mono; last auto. iIntros "$"; auto.
iApply ("HΦ"); done.
Qed.
End heap.