Library iris.array_lang.heap
From iris.array_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 (gmapUR nat (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 (gmapUR nat (prodR fracR (dec_agreeR val))).
The CMRA we need.
The Functor we need.
Definition heapGF : gFunctor := authGF heapUR.
Definition to_heap : state → heapUR :=
fmap (λ (blk: gmap nat val), fmap (λ v, (1%Qp, DecAgree v)) blk).
Definition of_heap : heapUR → state := fmap (λ (blk: gmap nat _), omap (maybe DecAgree ∘ snd) blk).
Section definitions.
Context `{heapG Σ}.
Definition heap_mapsto_def (l : loc) (off: nat) (q : Qp) (v: val) : iPropG heap_lang Σ :=
auth_own heap_name {[ l := {[ off := (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 ^^ off ↦{ q } v" := (heap_mapsto l off q v)
(at level 20, q at level 50, format "l ^^ off ↦{ q } v") : uPred_scope.
Notation "l ^^ off ↦ v" := (heap_mapsto l off 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 (λ (blk: gmap nat val), fmap (λ v, (1%Qp, DecAgree v)) blk).
Definition of_heap : heapUR → state := fmap (λ (blk: gmap nat _), omap (maybe DecAgree ∘ snd) blk).
Section definitions.
Context `{heapG Σ}.
Definition heap_mapsto_def (l : loc) (off: nat) (q : Qp) (v: val) : iPropG heap_lang Σ :=
auth_own heap_name {[ l := {[ off := (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 ^^ off ↦{ q } v" := (heap_mapsto l off q v)
(at level 20, q at level 50, format "l ^^ off ↦{ q } v") : uPred_scope.
Notation "l ^^ off ↦ v" := (heap_mapsto l off 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_fmap lookup_fmap.
case (σ !! l); last done.
intros blk. rewrite //=; f_equal.
apply map_eq⇒off.
rewrite lookup_omap lookup_fmap //=.
by case (blk !! off).
Qed.
Lemma to_heap_valid σ : ✓ to_heap σ.
Proof.
intros l. rewrite lookup_fmap. case (σ !! l); last done.
intros blk. rewrite //= ⇒ off.
rewrite lookup_fmap. by case (blk !! off).
Qed.
Lemma of_heap_insert0 l blk h :
of_heap (<[l:=blk]>h) = <[l:=omap (maybe DecAgree ∘ snd) blk]> (of_heap h).
Proof. by rewrite /of_heap fmap_insert. Qed.
Definition of_Some (om: option (gmap nat val)) : gmap nat val :=
match om with
| None ⇒ ∅
| Some m ⇒ m
end.
Lemma of_heap_singleton_op l off q v h :
✓ ({[l := {[off := (q, DecAgree v)]}]} ⋅ h) →
of_heap ({[l := {[off := (q, DecAgree v)]} ]} ⋅ h)
= <[l:=<[off := v]> (of_Some (of_heap h !! l))]> (of_heap h).
Proof.
intros Hv. apply map_eq⇒ l'; destruct (decide (l' = l)) as [->|].
- move: (Hv l). rewrite /of_Some /of_heap lookup_insert ?lookup_fmap.
rewrite (lookup_op _ h) lookup_singleton.
case _:(h !! l).
× intros blk Hvb.
rewrite //= ; f_equal.
apply map_eq⇒ off'; destruct (decide (off' = off)) as [->|].
** move: (Hvb off). rewrite /of_heap lookup_insert lookup_omap (lookup_op) lookup_singleton.
case _:(blk !! off)=>[[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 _ _) lookup_singleton_ne // left_id_L.
× intros Hvb. rewrite (proj2 (fmap_None (λ blk, omap (maybe DecAgree ∘ snd) blk) None)); eauto.
intros. rewrite fmap_Some. eexists; split; first eauto.
rewrite insert_empty. move: Hvb. rewrite right_id.
intros Hvb. rewrite /valid /cmra_valid //= /option_valid //= in Hvb.
specialize (Hvb off). rewrite lookup_singleton in Hvb. inversion Hvb as [??].
apply map_eq⇒i. rewrite lookup_omap.
destruct (decide (i = off)) as [->|].
** rewrite ?lookup_singleton //=.
** rewrite ?lookup_singleton_ne //=.
- rewrite /of_heap lookup_insert_ne // !lookup_fmap.
by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L.
Qed.
Lemma to_heap_insert0 l blk σ :
to_heap (<[l:=blk]> σ) = <[l:=(λ v, (1%Qp, DecAgree v)) <$> blk]> (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_fmap.
by case: (h !! l).
Qed.
Lemma heap_store_valid l off blk h v1 v2 :
✓ ({[l := <[off := (1%Qp, DecAgree v1)]>blk]} ⋅ h) →
✓ ({[l := <[off := (1%Qp, DecAgree v2)]>blk]} ⋅ h).
Proof.
intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
- rewrite !lookup_op !lookup_singleton.
case: (h !! l).
× intros blk' Hvb off'.
move: (Hvb off').
destruct (decide (off' = off)) as [->|].
** rewrite !lookup_op !lookup_insert.
by case: (blk' !! off)=>[x|] // /Some_valid/exclusive_l.
** by rewrite !lookup_op !lookup_insert_ne.
× rewrite right_id right_id⇒Hvb off'.
move: (Hvb off').
destruct (decide (off' = off)) as [->|].
** rewrite !lookup_insert.
by rewrite // /Some_valid/exclusive_l.
** by rewrite !lookup_insert_ne.
- 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_fmap lookup_fmap.
case (σ !! l); last done.
intros blk. rewrite //=; f_equal.
apply map_eq⇒off.
rewrite lookup_omap lookup_fmap //=.
by case (blk !! off).
Qed.
Lemma to_heap_valid σ : ✓ to_heap σ.
Proof.
intros l. rewrite lookup_fmap. case (σ !! l); last done.
intros blk. rewrite //= ⇒ off.
rewrite lookup_fmap. by case (blk !! off).
Qed.
Lemma of_heap_insert0 l blk h :
of_heap (<[l:=blk]>h) = <[l:=omap (maybe DecAgree ∘ snd) blk]> (of_heap h).
Proof. by rewrite /of_heap fmap_insert. Qed.
Definition of_Some (om: option (gmap nat val)) : gmap nat val :=
match om with
| None ⇒ ∅
| Some m ⇒ m
end.
Lemma of_heap_singleton_op l off q v h :
✓ ({[l := {[off := (q, DecAgree v)]}]} ⋅ h) →
of_heap ({[l := {[off := (q, DecAgree v)]} ]} ⋅ h)
= <[l:=<[off := v]> (of_Some (of_heap h !! l))]> (of_heap h).
Proof.
intros Hv. apply map_eq⇒ l'; destruct (decide (l' = l)) as [->|].
- move: (Hv l). rewrite /of_Some /of_heap lookup_insert ?lookup_fmap.
rewrite (lookup_op _ h) lookup_singleton.
case _:(h !! l).
× intros blk Hvb.
rewrite //= ; f_equal.
apply map_eq⇒ off'; destruct (decide (off' = off)) as [->|].
** move: (Hvb off). rewrite /of_heap lookup_insert lookup_omap (lookup_op) lookup_singleton.
case _:(blk !! off)=>[[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 _ _) lookup_singleton_ne // left_id_L.
× intros Hvb. rewrite (proj2 (fmap_None (λ blk, omap (maybe DecAgree ∘ snd) blk) None)); eauto.
intros. rewrite fmap_Some. eexists; split; first eauto.
rewrite insert_empty. move: Hvb. rewrite right_id.
intros Hvb. rewrite /valid /cmra_valid //= /option_valid //= in Hvb.
specialize (Hvb off). rewrite lookup_singleton in Hvb. inversion Hvb as [??].
apply map_eq⇒i. rewrite lookup_omap.
destruct (decide (i = off)) as [->|].
** rewrite ?lookup_singleton //=.
** rewrite ?lookup_singleton_ne //=.
- rewrite /of_heap lookup_insert_ne // !lookup_fmap.
by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L.
Qed.
Lemma to_heap_insert0 l blk σ :
to_heap (<[l:=blk]> σ) = <[l:=(λ v, (1%Qp, DecAgree v)) <$> blk]> (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_fmap.
by case: (h !! l).
Qed.
Lemma heap_store_valid l off blk h v1 v2 :
✓ ({[l := <[off := (1%Qp, DecAgree v1)]>blk]} ⋅ h) →
✓ ({[l := <[off := (1%Qp, DecAgree v2)]>blk]} ⋅ h).
Proof.
intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
- rewrite !lookup_op !lookup_singleton.
case: (h !! l).
× intros blk' Hvb off'.
move: (Hvb off').
destruct (decide (off' = off)) as [->|].
** rewrite !lookup_op !lookup_insert.
by case: (blk' !! off)=>[x|] // /Some_valid/exclusive_l.
** by rewrite !lookup_op !lookup_insert_ne.
× rewrite right_id right_id⇒Hvb off'.
move: (Hvb off').
destruct (decide (off' = off)) as [->|].
** rewrite !lookup_insert.
by rewrite // /Some_valid/exclusive_l.
** by rewrite !lookup_insert_ne.
- 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↦blk ∈ σ,
[★ map ] off↦v ∈ blk, l ^^ off ↦ 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 blk σ Hl IH] using map_ind.
{ rewrite big_sepM_empty. rewrite emp_True.
rewrite /auth_own. apply affine_intro; first apply _; auto. }
rewrite to_heap_insert0 big_sepM_insert //=.
rewrite (insert_singleton_op (to_heap σ));
last by rewrite lookup_fmap Hl; auto.
rewrite auth_own_op.
induction blk as [|off v blk Hoff IH'] using map_ind.
{ rewrite big_sepM_empty fmap_empty //=.
rewrite IH. apply sep_mono; auto. rewrite /auth_own.
rewrite emp_True. rewrite /auth_own. apply affine_intro; first apply _; auto. }
rewrite big_sepM_insert //. rewrite fmap_insert //=.
rewrite insert_singleton_op //=; last first.
{ rewrite lookup_fmap // Hoff //. }
rewrite -op_singleton auth_own_op //=.
by rewrite -assoc IH' assoc.
Qed.
Context `{heapG Σ}.
authG heap_lang Σ heapUR → nclose heapN ⊆ E →
ownP σ ={E}=> ∃ _ : heapG Σ, heap_ctx ★ [★ map] l↦blk ∈ σ,
[★ map ] off↦v ∈ blk, l ^^ off ↦ 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 blk σ Hl IH] using map_ind.
{ rewrite big_sepM_empty. rewrite emp_True.
rewrite /auth_own. apply affine_intro; first apply _; auto. }
rewrite to_heap_insert0 big_sepM_insert //=.
rewrite (insert_singleton_op (to_heap σ));
last by rewrite lookup_fmap Hl; auto.
rewrite auth_own_op.
induction blk as [|off v blk Hoff IH'] using map_ind.
{ rewrite big_sepM_empty fmap_empty //=.
rewrite IH. apply sep_mono; auto. rewrite /auth_own.
rewrite emp_True. rewrite /auth_own. apply affine_intro; first apply _; auto. }
rewrite big_sepM_insert //. rewrite fmap_insert //=.
rewrite insert_singleton_op //=; last first.
{ rewrite lookup_fmap // Hoff //. }
rewrite -op_singleton auth_own_op //=.
by rewrite -assoc IH' assoc.
Qed.
Context `{heapG Σ}.
General properties of mapsto
Global Instance heap_mapsto_timeless l off q v : ATimelessP (l ^^ off ↦{q} v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_affine l off q v : AffineP (l ^^ off ↦{q} v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_map_affine σ:
AffineP ([★ map] l↦blk ∈σ, [★ map] off↦v ∈ blk, l ^^ off ↦ 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; clear.
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; clear.
Qed.
Lemma heap_mapsto_op_eq l off q1 q2 v :
(l ^^ off ↦{q1} v ★ l ^^ off ↦{q2} v) ⊣⊢ l ^^ off ↦{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 off q1 q2 v1 v2 :
(l ^^ off ↦{q1} v1 ★ l ^^ off ↦{q2} v2) ⊣⊢ (⧆ (v1 = v2) ★ l ^^ off ↦{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.
rewrite gmap_validI (forall_elim off) 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 off q v : l ^^ off ↦{q} v ⊣⊢ (l ^^ off ↦{q/2} v ★ l ^^ off ↦{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 off q v : AffineP (l ^^ off ↦{q} v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_map_affine σ:
AffineP ([★ map] l↦blk ∈σ, [★ map] off↦v ∈ blk, l ^^ off ↦ 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; clear.
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; clear.
Qed.
Lemma heap_mapsto_op_eq l off q1 q2 v :
(l ^^ off ↦{q1} v ★ l ^^ off ↦{q2} v) ⊣⊢ l ^^ off ↦{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 off q1 q2 v1 v2 :
(l ^^ off ↦{q1} v1 ★ l ^^ off ↦{q2} v2) ⊣⊢ (⧆ (v1 = v2) ★ l ^^ off ↦{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.
rewrite gmap_validI (forall_elim off) 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 off q v : l ^^ off ↦{q} v ⊣⊢ (l ^^ off ↦{q/2} v ★ l ^^ off ↦{q/2} v).
Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
Weakest precondition
Fixpoint blockpt (l: loc) (off: nat) (vs: list val) :=
match vs with
| [] ⇒ Emp%I
| v :: vs' ⇒ (l ^^ off ↦ v ★ blockpt l (S off) vs')%I
end.
Lemma blockpt_snoc l n vs v:
blockpt l n (vs ++ [v]) ⊣⊢ blockpt l n vs ★ (l ^^ (n + length vs) ↦ v).
Proof.
revert l n v. induction vs; intros; rewrite //= ?left_id ?right_id //.
rewrite IHvs.
replace (n + S (length vs))%nat with (S n + length vs)%nat by omega.
rewrite assoc. repeat apply sep_proper; eauto.
Qed.
Lemma repeat_cons {A: Type} n (v: A): repeat v (S n) = [v] ++ repeat v n.
induction n; rewrite //=.
Qed.
Lemma repeat_snoc {A: Type} n (v: A): repeat v (S n) = repeat v n ++ [v].
Proof.
induction n; first done.
rewrite repeat_cons. symmetry. by rewrite {1}repeat_cons IHn .
Qed.
Lemma wp_alloc E e (sz: Z) v Φ :
to_val e = Some v → nclose heapN ⊆ E →
(heap_ctx ★ ▷ ∀ l, blockpt l 0 (repeat v (S $ Z.to_nat sz))
-★ |={E ∖ heapN}=>> Φ (LitV $ LitLoc l 0))
⊢ WP Alloc e (Lit $ LitInt sz) @ 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 := (λ v, (1%Qp, DecAgree v)) <$> set_block v (Z.to_nat sz) ∅]}.
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.
× by apply of_heap_None, (not_elem_of_dom (D:= gset _)), is_fresh; eauto.
× clear; induction (Z.to_nat sz) as [| sz'].
{ rewrite /set_block⇒off.
destruct off; rewrite lookup_fmap.
** rewrite lookup_insert //.
** rewrite lookup_insert_ne //. }
rewrite //= ⇒ off.
destruct (decide (off = S sz')) as [->|].
** rewrite lookup_fmap lookup_insert //.
** rewrite lookup_fmap lookup_insert_ne // -lookup_fmap //.
}
iIntros "Hauth".
iApply wp_alloc_pst'. iFrame "Hheap". iNext.
iIntros "Hheap".
rewrite /l /of_heap fmap_insert.
rewrite -{1}(affine_affine (ownP _)) {1}(later_intro (ownP _)).
assert(omap (maybe DecAgree ∘ snd)
((λ v0 : val, (1%Qp, DecAgree v0)) <$>
set_block v (Z.to_nat sz) ∅)
= set_block v (Z.to_nat sz) ∅) as Heq.
{ clear; induction (Z.to_nat sz) as [| sz'].
- rewrite /set_block insert_empty.
rewrite map_fmap_singleton; erewrite omap_singleton; eauto.
- rewrite //= fmap_insert; erewrite omap_insert; eauto.
rewrite IHsz' //.
}
rewrite Heq.
iFrame "Hheap".
iSpecialize ("HΦ" $! l). rewrite -(pvs_intro).
iApply "HΦ".
iRevert "Hinv". iRevert "Hauth".
cut (Emp ⊢ auth_own heap_name
{[fresh
(dom (gset positive)
((λ blk : gmap nat (fracR × dec_agree val),
omap (maybe DecAgree ∘ snd) blk) <$> h))
:= (λ v0 : val, (1%Qp, DecAgree v0)) <$> set_block v (Z.to_nat sz) ∅]} -★
□ auth_ctx heap_name heapN
(λ h0 : heapUR,
ownP
((λ blk : gmap nat (fracR × dec_agree val),
omap (maybe DecAgree ∘ snd) blk) <$> h0)) -★
blockpt l 0 (repeat v (S (Z.to_nat sz))))%I.
{ intros Hcut. rewrite -Hcut; eauto. }
clear Heq.
induction (Z.to_nat sz) as [| sz' IHsz']; iIntros "_ Hauth #Hinv".
{
simpl blockpt. rewrite right_id.
rewrite fmap_insert. rewrite insert_singleton_op; last auto.
rewrite -op_singleton auth_own_op.
rewrite heap_mapsto_eq /heap_mapsto_def.
iDestruct "Hauth" as "(Hauth'&_)"; done.
}
rewrite repeat_snoc blockpt_snoc.
rewrite fmap_insert. rewrite insert_singleton_op //=; last first.
{ clear. rewrite lookup_fmap. apply fmap_None.
cut (∀ n: nat, (n > sz')%nat → set_block v sz' ∅ !! n = None).
{ intros H. eapply H. omega. }
induction sz'.
- intros. rewrite lookup_insert_ne; eauto. omega.
- intros; rewrite lookup_insert_ne; eauto. apply IHsz'; omega.
omega.
}
rewrite -op_singleton auth_own_op.
iDestruct "Hauth" as "(?&Hrec)".
iSplitL "Hrec".
- iPoseProof IHsz' as "IHsz".
iSpecialize ("IHsz" with "[Hrec] []"); done.
- rewrite heap_mapsto_eq /heap_mapsto_def.
cut (length (repeat v sz') = sz').
{ intros →. done. }
clear; induction sz'; rewrite //=. eauto.
Qed.
Lemma wp_load E l off q v Φ :
nclose heapN ⊆ E →
(heap_ctx ★ ⧆▷ l ^^ off ↦{q} v ★ ▷(⧆ l ^^ off ↦{q} v -★ |={E ∖ heapN}=>> (Φ v)))
⊢ WP Load (Lit (LitLoc l off)) @ 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:=<[off:=v]>(of_Some (of_heap h !! l))]>(of_heap h))).
{ by rewrite ?lookup_insert. }
{ 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 off v' e v Φ :
to_val e = Some v → nclose heapN ⊆ E →
(heap_ctx ★ ⧆▷ l ^^ off ↦ v' ★ ▷ (l ^^ off ↦ v -★ |={E ∖ heapN}=>> ( Φ (LitV LitUnit))))
⊢ WP Store (Lit (LitLoc l off)) 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 := {[off := (1%Qp, DecAgree v)]} ]}.
iSplitL "".
{ iPureIntro. by do 2 apply singleton_local_update; apply exclusive_local_update. }
iIntros "Hauth".
iApply (wp_store_pst _ (<[l:=<[off:=v']>(of_Some (of_heap h !! l))]>(of_heap h))); eauto.
{ by rewrite ?lookup_insert. }
{ 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; last first.
{ eapply heap_store_valid. eauto. }
rewrite insert_insert; eauto.
iFrame "Hown". rewrite -pvs_intro. by iApply "HΦ".
Qed.
Lemma wp_cas_fail E l off q v' e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose heapN ⊆ E →
heap_ctx ★ ⧆▷ l ^^ off ↦{q} v' ★ ▷ (l ^^ off ↦{q} v' -★ |={E ∖ heapN}=>> Φ (LitV (LitBool false)))
⊢ WP CAS (Lit (LitLoc l off)) 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 := {[off := (q%Qp, DecAgree v')]} ]}.
iSplitL "".
{ iPureIntro; naive_solver. }
iIntros "Hauth".
iApply (wp_cas_fail_pst _ (<[l:=<[off :=v']>(of_Some (of_heap h !! l))]>(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 off e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose heapN ⊆ E →
heap_ctx ★ ⧆▷ l ^^ off ↦ v1 ★ ▷ (l ^^ off ↦ v2 -★ |={E ∖ heapN}=>> (Φ (LitV (LitBool true))))
⊢ WP CAS (Lit (LitLoc l off)) 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 := {[off := (1%Qp, DecAgree v2)]} ]}.
iSplitL "".
{ iPureIntro; by do 2 apply singleton_local_update; apply exclusive_local_update. }
iIntros "Hauth".
iApply (wp_cas_suc_pst _ (<[l:=<[off:=v1]>(of_Some (of_heap h !! l))]>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto; last first.
{ eapply heap_store_valid. eauto. }
iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
rewrite insert_insert; eauto.
iFrame "HownP".
iApply psvs_mono; last auto. iIntros "$"; auto.
iApply ("HΦ"); done.
Qed.
End heap.
match vs with
| [] ⇒ Emp%I
| v :: vs' ⇒ (l ^^ off ↦ v ★ blockpt l (S off) vs')%I
end.
Lemma blockpt_snoc l n vs v:
blockpt l n (vs ++ [v]) ⊣⊢ blockpt l n vs ★ (l ^^ (n + length vs) ↦ v).
Proof.
revert l n v. induction vs; intros; rewrite //= ?left_id ?right_id //.
rewrite IHvs.
replace (n + S (length vs))%nat with (S n + length vs)%nat by omega.
rewrite assoc. repeat apply sep_proper; eauto.
Qed.
Lemma repeat_cons {A: Type} n (v: A): repeat v (S n) = [v] ++ repeat v n.
induction n; rewrite //=.
Qed.
Lemma repeat_snoc {A: Type} n (v: A): repeat v (S n) = repeat v n ++ [v].
Proof.
induction n; first done.
rewrite repeat_cons. symmetry. by rewrite {1}repeat_cons IHn .
Qed.
Lemma wp_alloc E e (sz: Z) v Φ :
to_val e = Some v → nclose heapN ⊆ E →
(heap_ctx ★ ▷ ∀ l, blockpt l 0 (repeat v (S $ Z.to_nat sz))
-★ |={E ∖ heapN}=>> Φ (LitV $ LitLoc l 0))
⊢ WP Alloc e (Lit $ LitInt sz) @ 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 := (λ v, (1%Qp, DecAgree v)) <$> set_block v (Z.to_nat sz) ∅]}.
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.
× by apply of_heap_None, (not_elem_of_dom (D:= gset _)), is_fresh; eauto.
× clear; induction (Z.to_nat sz) as [| sz'].
{ rewrite /set_block⇒off.
destruct off; rewrite lookup_fmap.
** rewrite lookup_insert //.
** rewrite lookup_insert_ne //. }
rewrite //= ⇒ off.
destruct (decide (off = S sz')) as [->|].
** rewrite lookup_fmap lookup_insert //.
** rewrite lookup_fmap lookup_insert_ne // -lookup_fmap //.
}
iIntros "Hauth".
iApply wp_alloc_pst'. iFrame "Hheap". iNext.
iIntros "Hheap".
rewrite /l /of_heap fmap_insert.
rewrite -{1}(affine_affine (ownP _)) {1}(later_intro (ownP _)).
assert(omap (maybe DecAgree ∘ snd)
((λ v0 : val, (1%Qp, DecAgree v0)) <$>
set_block v (Z.to_nat sz) ∅)
= set_block v (Z.to_nat sz) ∅) as Heq.
{ clear; induction (Z.to_nat sz) as [| sz'].
- rewrite /set_block insert_empty.
rewrite map_fmap_singleton; erewrite omap_singleton; eauto.
- rewrite //= fmap_insert; erewrite omap_insert; eauto.
rewrite IHsz' //.
}
rewrite Heq.
iFrame "Hheap".
iSpecialize ("HΦ" $! l). rewrite -(pvs_intro).
iApply "HΦ".
iRevert "Hinv". iRevert "Hauth".
cut (Emp ⊢ auth_own heap_name
{[fresh
(dom (gset positive)
((λ blk : gmap nat (fracR × dec_agree val),
omap (maybe DecAgree ∘ snd) blk) <$> h))
:= (λ v0 : val, (1%Qp, DecAgree v0)) <$> set_block v (Z.to_nat sz) ∅]} -★
□ auth_ctx heap_name heapN
(λ h0 : heapUR,
ownP
((λ blk : gmap nat (fracR × dec_agree val),
omap (maybe DecAgree ∘ snd) blk) <$> h0)) -★
blockpt l 0 (repeat v (S (Z.to_nat sz))))%I.
{ intros Hcut. rewrite -Hcut; eauto. }
clear Heq.
induction (Z.to_nat sz) as [| sz' IHsz']; iIntros "_ Hauth #Hinv".
{
simpl blockpt. rewrite right_id.
rewrite fmap_insert. rewrite insert_singleton_op; last auto.
rewrite -op_singleton auth_own_op.
rewrite heap_mapsto_eq /heap_mapsto_def.
iDestruct "Hauth" as "(Hauth'&_)"; done.
}
rewrite repeat_snoc blockpt_snoc.
rewrite fmap_insert. rewrite insert_singleton_op //=; last first.
{ clear. rewrite lookup_fmap. apply fmap_None.
cut (∀ n: nat, (n > sz')%nat → set_block v sz' ∅ !! n = None).
{ intros H. eapply H. omega. }
induction sz'.
- intros. rewrite lookup_insert_ne; eauto. omega.
- intros; rewrite lookup_insert_ne; eauto. apply IHsz'; omega.
omega.
}
rewrite -op_singleton auth_own_op.
iDestruct "Hauth" as "(?&Hrec)".
iSplitL "Hrec".
- iPoseProof IHsz' as "IHsz".
iSpecialize ("IHsz" with "[Hrec] []"); done.
- rewrite heap_mapsto_eq /heap_mapsto_def.
cut (length (repeat v sz') = sz').
{ intros →. done. }
clear; induction sz'; rewrite //=. eauto.
Qed.
Lemma wp_load E l off q v Φ :
nclose heapN ⊆ E →
(heap_ctx ★ ⧆▷ l ^^ off ↦{q} v ★ ▷(⧆ l ^^ off ↦{q} v -★ |={E ∖ heapN}=>> (Φ v)))
⊢ WP Load (Lit (LitLoc l off)) @ 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:=<[off:=v]>(of_Some (of_heap h !! l))]>(of_heap h))).
{ by rewrite ?lookup_insert. }
{ 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 off v' e v Φ :
to_val e = Some v → nclose heapN ⊆ E →
(heap_ctx ★ ⧆▷ l ^^ off ↦ v' ★ ▷ (l ^^ off ↦ v -★ |={E ∖ heapN}=>> ( Φ (LitV LitUnit))))
⊢ WP Store (Lit (LitLoc l off)) 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 := {[off := (1%Qp, DecAgree v)]} ]}.
iSplitL "".
{ iPureIntro. by do 2 apply singleton_local_update; apply exclusive_local_update. }
iIntros "Hauth".
iApply (wp_store_pst _ (<[l:=<[off:=v']>(of_Some (of_heap h !! l))]>(of_heap h))); eauto.
{ by rewrite ?lookup_insert. }
{ 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; last first.
{ eapply heap_store_valid. eauto. }
rewrite insert_insert; eauto.
iFrame "Hown". rewrite -pvs_intro. by iApply "HΦ".
Qed.
Lemma wp_cas_fail E l off q v' e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose heapN ⊆ E →
heap_ctx ★ ⧆▷ l ^^ off ↦{q} v' ★ ▷ (l ^^ off ↦{q} v' -★ |={E ∖ heapN}=>> Φ (LitV (LitBool false)))
⊢ WP CAS (Lit (LitLoc l off)) 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 := {[off := (q%Qp, DecAgree v')]} ]}.
iSplitL "".
{ iPureIntro; naive_solver. }
iIntros "Hauth".
iApply (wp_cas_fail_pst _ (<[l:=<[off :=v']>(of_Some (of_heap h !! l))]>(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 off e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose heapN ⊆ E →
heap_ctx ★ ⧆▷ l ^^ off ↦ v1 ★ ▷ (l ^^ off ↦ v2 -★ |={E ∖ heapN}=>> (Φ (LitV (LitBool true))))
⊢ WP CAS (Lit (LitLoc l off)) 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 := {[off := (1%Qp, DecAgree v2)]} ]}.
iSplitL "".
{ iPureIntro; by do 2 apply singleton_local_update; apply exclusive_local_update. }
iIntros "Hauth".
iApply (wp_cas_suc_pst _ (<[l:=<[off:=v1]>(of_Some (of_heap h !! l))]>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto; last first.
{ eapply heap_store_valid. eauto. }
iFrame "Hl". iNext.
iIntros "HownP".
rewrite -{1}(affine_affine (ownP _)).
rewrite {1}(later_intro (ownP _)).
rewrite insert_insert; eauto.
iFrame "HownP".
iApply psvs_mono; last auto. iIntros "$"; auto.
iApply ("HΦ"); done.
Qed.
End heap.