Commit b0039d65 authored by Robbert Krebbers's avatar Robbert Krebbers

Generalize heap construction and mapsto connective.

parent cd0ae810
......@@ -92,13 +92,13 @@ program_logic/language.v
program_logic/ectx_language.v
program_logic/ectxi_language.v
program_logic/ectx_lifting.v
program_logic/gen_heap.v
heap_lang/lang.v
heap_lang/tactics.v
heap_lang/wp_tactics.v
heap_lang/lifting.v
heap_lang/rules.v
heap_lang/derived.v
heap_lang/notation.v
heap_lang/heap.v
heap_lang/lib/spawn.v
heap_lang/lib/par.v
heap_lang/lib/assert.v
......
From iris.program_logic Require Export weakestpre adequacy.
From iris.heap_lang Require Export heap.
From iris.program_logic Require Export weakestpre adequacy gen_heap.
From iris.heap_lang Require Export rules.
From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ;
heap_preG_heap :> inG Σ (authR heapUR)
heap_preG_heap :> gen_heapPreG loc val Σ
}.
Definition heapΣ : gFunctors := #[invΣ; GFunctor (constRF (authR heapUR))].
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. intros [? ?%subG_inG]%subG_inv. split; apply _. Qed.
Proof. intros [? ?]%subG_inv; split; apply _. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
( `{heapG Σ}, True WP e {{ v, ⌜φ v }})
adequate e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
iMod (own_alloc ( to_heap σ)) as (γ) "Hh".
{ apply: auth_auth_valid. exact: to_heap_valid. }
iModIntro. iExists (λ σ, own γ ( to_heap σ)); iFrame.
set (Hheap := HeapG _ _ _ γ). iApply (Hwp _).
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
{ apply: auth_auth_valid. exact: to_gen_heap_valid. }
iModIntro. iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
set (Hheap := GenHeapG loc val Σ _ _ _ _ γ).
iApply (Hwp (HeapG _ _ _)).
Qed.
From iris.heap_lang Require Export lifting.
From iris.heap_lang Require Export rules.
Import uPred.
(** Define some derived forms, and derived lemmas about them. *)
......@@ -12,7 +12,7 @@ Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
Section derived.
Context `{irisG heap_lang Σ}.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
......
From iris.heap_lang Require Export lifting.
From iris.algebra Require Import auth gmap frac dec_agree.
From iris.base_logic.lib Require Export invariants.
From iris.base_logic.lib Require Import fractional.
From iris.program_logic Require Import ectx_lifting.
From iris.proofmode Require Import tactics.
Import uPred.
(* TODO: The entire construction could be generalized to arbitrary languages that have
a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
predicates over finmaps instead of just ownP. *)
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
Definition to_heap : state heapUR := fmap (λ v, (1%Qp, DecAgree v)).
(** The CMRA we need. *)
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
heap_inG :> inG Σ (authR heapUR);
heap_name : gname
}.
Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
state_interp σ := own heap_name ( to_heap σ)
}.
Section definitions.
Context `{heapG Σ}.
Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
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.
End definitions.
Typeclasses Opaque heap_mapsto.
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.
Notation "l ↦{ q } -" := ( v, l {q} v)%I
(at level 20, q at level 50, format "l ↦{ q } -") : uPred_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : uPred_scope.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.
Section heap.
Context {Σ : gFunctors}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types σ : state.
Implicit Types h g : heapUR.
(** Conversion to heaps and back *)
Lemma to_heap_valid σ : to_heap σ.
Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
Lemma lookup_to_heap_None σ l : σ !! l = None to_heap σ !! l = None.
Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
Lemma heap_singleton_included σ l q v :
{[l := (q, DecAgree v)]} to_heap σ σ !! l = Some v.
Proof.
rewrite singleton_included=> -[[q' av] [/leibniz_equiv_iff Hl Hqv]].
move: Hl. rewrite /to_heap lookup_fmap fmap_Some=> -[v' [Hl [??]]]; subst.
by move: Hqv=> /Some_pair_included_total_2 [_ /DecAgree_included ->].
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.
Context `{heapG Σ}.
(** General properties of mapsto *)
Global Instance heap_mapsto_timeless l q v : TimelessP (l {q} v).
Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
Global Instance heap_mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
Proof.
intros p q. by rewrite heap_mapsto_eq -own_op -auth_frag_op
op_singleton pair_op dec_agree_idemp.
Qed.
Global Instance heap_mapsto_as_fractional l q v :
AsFractional (l {q} v) (λ q, l {q} v)%I q.
Proof. done. Qed.
Lemma heap_mapsto_agree l q1 q2 v1 v2 : l {q1} v1 l {q2} v2 v1 = v2.
Proof.
rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
by move=> [_ /= /dec_agree_op_inv [?]].
Qed.
Global Instance heap_ex_mapsto_fractional l : Fractional (λ q, l {q} -)%I.
Proof.
intros p q. iSplit.
- iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
- iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
iDestruct (heap_mapsto_agree with "[$H1 $H2]") as %->. iExists v2. by iFrame.
Qed.
Global Instance heap_ex_mapsto_as_fractional l q :
AsFractional (l {q} -) (λ q, l {q} -)%I q.
Proof. done. Qed.
Lemma heap_mapsto_valid l q v : l {q} v q.
Proof.
rewrite heap_mapsto_eq /heap_mapsto_def own_valid !discrete_valid.
by apply pure_mono=> /auth_own_valid /singleton_valid [??].
Qed.
Lemma heap_mapsto_valid_2 l q1 q2 v1 v2 :
l {q1} v1 l {q2} v2 (q1 + q2)%Qp.
Proof.
iIntros "[H1 H2]". iDestruct (heap_mapsto_agree with "[$H1 $H2]") as %->.
iApply (heap_mapsto_valid l _ v2). by iFrame.
Qed.
(** Weakest precondition *)
Lemma wp_alloc E e v :
to_val e = Some v
{{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l v }}}.
Proof.
iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>"; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (own_update with "Hσ") as "[Hσ Hl]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ _ (1%Qp, DecAgree _))=> //.
by apply lookup_to_heap_None. }
iModIntro; iSplit=> //. rewrite to_heap_insert. iFrame.
iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
Qed.
Lemma wp_load E l q v :
{{{ l {q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l {q} v }}}.
Proof.
iIntros (Φ) ">Hl HΦ". rewrite heap_mapsto_eq /heap_mapsto_def.
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (own_valid_2 with "Hσ Hl")
as %[?%heap_singleton_included _]%auth_valid_discrete_2.
iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma wp_store E l v' e v :
to_val e = Some v
{{{ l v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l v }}}.
Proof.
iIntros (<-%of_to_val Φ) ">Hl HΦ". rewrite heap_mapsto_eq /heap_mapsto_def.
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (own_valid_2 with "Hσ Hl")
as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (own_update_2 with "Hσ Hl") as "[Hσ1 Hl]".
{ eapply auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, DecAgree _))=> //.
by rewrite /to_heap lookup_fmap Hl. }
iModIntro. iSplit=>//. rewrite to_heap_insert. iFrame. 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
{{{ l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ".
rewrite heap_mapsto_eq /heap_mapsto_def.
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (own_valid_2 with "Hσ Hl")
as %[?%heap_singleton_included _]%auth_valid_discrete_2.
iSplit; first by eauto.
iNext; iIntros (v2' σ2 efs Hstep); inv_head_step. (* FIXME: this inversion is slow *)
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 :
to_val e1 = Some v1 to_val e2 = Some v2
{{{ l v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{ RET LitV (LitBool true); l v2 }}}.
Proof.
iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
rewrite heap_mapsto_eq /heap_mapsto_def.
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (own_valid_2 with "Hσ Hl")
as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
iSplit; first by eauto.
iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iMod (own_update_2 with "Hσ Hl") as "[Hσ1 Hl]".
{ eapply auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, DecAgree _))=> //.
by rewrite /to_heap lookup_fmap Hl. }
iModIntro. iSplit=>//. rewrite to_heap_insert. iFrame. by iApply "HΦ".
Qed.
End heap.
From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth.
......
From iris.heap_lang Require Import heap notation.
From iris.heap_lang Require Export rules notation.
From iris.base_logic.lib Require Export invariants.
Structure lock Σ `{!heapG Σ} := Lock {
(* -- operations -- *)
......
From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
......@@ -71,7 +72,7 @@ Proof.
- iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
+ iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. by iApply "HΦ".
+ iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
+ iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
Qed.
End proof.
......
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Export wp_tactics heap.
From iris.heap_lang Require Export wp_tactics rules.
Import uPred.
Ltac wp_strip_later ::= iNext.
......
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Export weakestpre gen_heap.
From iris.program_logic Require Import ectx_lifting.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics.
......@@ -6,6 +6,25 @@ From iris.proofmode Require Import tactics.
From iris.prelude Require Import fin_maps.
Import uPred.
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
heapG_gen_heapG :> gen_heapG loc val Σ
}.
Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
state_interp := gen_heap_ctx
}.
(** Override the notations so that scopes and coercions work out *)
Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
(at level 20, q at level 50, format "l ↦{ q } v") : uPred_scope.
Notation "l ↦ v" :=
(mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : uPred_scope.
Notation "l ↦{ q } -" := ( v, l {q} v)%I
(at level 20, q at level 50, format "l ↦{ q } -") : uPred_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : uPred_scope.
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and
simplifies hypothesis related to conversions from and to values, and finite map
......@@ -15,6 +34,8 @@ Ltac inv_head_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : _ = of_val ?v |- _ =>
is_var v; destruct v; first[discriminate H|injection H as H]
| H : head_step ?e _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
......@@ -28,8 +49,8 @@ Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.
Section lifting.
Context `{irisG heap_lang Σ}.
Section rules.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types efs : list expr.
......@@ -134,4 +155,63 @@ Proof.
rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e2 e0)); eauto.
intros; inv_head_step; eauto.
Qed.
End lifting.
(** Heap *)
Lemma wp_alloc E e v :
to_val e = Some v
{{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l v }}}.
Proof.
iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>"; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma wp_load E l q v :
{{{ l {q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l {q} v }}}.
Proof.
iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma wp_store E l v' e v :
to_val e = Some v
{{{ l v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l v }}}.
Proof.
iIntros (<-%of_to_val Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. 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
{{{ l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 :
to_val e1 = Some v1 to_val e2 = Some v2
{{{ l v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{ RET LitV (LitBool true); l v2 }}}.
Proof.
iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
End rules.
From iris.algebra Require Import auth gmap frac dec_agree.
From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import fractional.
From iris.proofmode Require Import tactics.
Import uPred.
Definition gen_heapUR (L V : Type) `{Countable L, EqDecision V} : ucmraT :=
gmapUR L (prodR fracR (dec_agreeR V)).
Definition to_gen_heap `{Countable L, EqDecision V} : gmap L V gen_heapUR L V :=
fmap (λ v, (1%Qp, DecAgree v)).
(** The CMRA we need. *)
Class gen_heapG (L V : Type) (Σ : gFunctors)
`{Countable L, EqDecision V} := GenHeapG {
gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
gen_heap_name : gname
}.
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L, EqDecision V} :=
{ gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }.
Definition gen_heapΣ (L V : Type) `{Countable L, EqDecision V} : gFunctors :=
#[GFunctor (constRF (authR (gen_heapUR L V)))].
Instance subG_gen_heapPreG {Σ} `{Countable L, EqDecision V} :
subG (gen_heapΣ L V) Σ gen_heapPreG L V Σ.
Proof. intros ?%subG_inG; split; apply _. Qed.
Section definitions.
Context `{gen_heapG L V Σ}.
Definition gen_heap_ctx (σ : gmap L V) : iProp Σ :=
own gen_heap_name ( to_gen_heap σ).
Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
own gen_heap_name ( {[ l := (q, DecAgree v) ]}).
Definition mapsto_aux : { x | x = @mapsto_def }. by eexists. Qed.
Definition mapsto := proj1_sig mapsto_aux.
Definition mapsto_eq : @mapsto = @mapsto_def := proj2_sig mapsto_aux.
End definitions.
Local Notation "l ↦{ q } v" := (mapsto l q v)
(at level 20, q at level 50, format "l ↦{ q } v") : uPred_scope.
Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : uPred_scope.
Local Notation "l ↦{ q } -" := ( v, l {q} v)%I
(at level 20, q at level 50, format "l ↦{ q } -") : uPred_scope.
Local Notation "l ↦ -" := (l {1} -)%I (at level 20) : uPred_scope.
Section gen_heap.
Context `{gen_heapG L V Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : V iProp Σ.
Implicit Types σ : gmap L V.
Implicit Types h g : gen_heapUR L V.
(** Conversion to heaps and back *)
Lemma to_gen_heap_valid σ : to_gen_heap σ.
Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
Lemma lookup_to_gen_heap_None σ l : σ !! l = None to_gen_heap σ !! l = None.
Proof. by rewrite /to_gen_heap lookup_fmap=> ->. Qed.
Lemma gen_heap_singleton_included σ l q v :
{[l := (q, DecAgree v)]} to_gen_heap σ σ !! l = Some v.
Proof.
rewrite singleton_included=> -[[q' av] [/leibniz_equiv_iff Hl Hqv]].
move: Hl. rewrite /to_gen_heap lookup_fmap fmap_Some=> -[v' [Hl [??]]]; subst.
by move: Hqv=> /Some_pair_included_total_2 [_ /DecAgree_included ->].
Qed.
Lemma to_gen_heap_insert l v σ :
to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_gen_heap σ).
Proof. by rewrite /to_gen_heap fmap_insert. Qed.
(** General properties of mapsto *)
Global Instance mapsto_timeless l q v : TimelessP (l {q} v).
Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
Proof.
intros p q. by rewrite mapsto_eq -own_op -auth_frag_op
op_singleton pair_op dec_agree_idemp.
Qed.
Global Instance mapsto_as_fractional l q v :
AsFractional (l {q} v) (λ q, l {q} v)%I q.
Proof. done. Qed.
Lemma mapsto_agree l q1 q2 v1 v2 : l {q1} v1 l {q2} v2 v1 = v2.
Proof.
rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
by move=> [_ /= /dec_agree_op_inv [?]].
Qed.
Global Instance heap_ex_mapsto_fractional l : Fractional (λ q, l {q} -)%I.
Proof.
intros p q. iSplit.
- iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
- iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
iDestruct (mapsto_agree with "[$H1 $H2]") as %->. iExists v2. by iFrame.
Qed.
Global Instance heap_ex_mapsto_as_fractional l q :
AsFractional (l {q} -) (λ q, l {q} -)%I q.
Proof. done. Qed.
Lemma mapsto_valid l q v : l {q} v q.
Proof.
rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
by apply pure_mono=> /auth_own_valid /singleton_valid [??].
Qed.
Lemma mapsto_valid_2 l q1 q2 v1 v2 :
l {q1} v1 l {q2} v2 (q1 + q2)%Qp.
Proof.
iIntros "[H1 H2]". iDestruct (mapsto_agree with "[$H1 $H2]") as %->.
iApply (mapsto_valid l _ v2). by iFrame.
Qed.
Lemma gen_heap_alloc σ l v :
σ !! l = None gen_heap_ctx σ == gen_heap_ctx (<[l:=v]>σ) l v.
Proof.
iIntros (?) "Hσ". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iMod (own_update with "Hσ") as "[Hσ Hl]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ _ (1%Qp, DecAgree v))=> //.
by apply lookup_to_gen_heap_None. }
iModIntro. rewrite to_gen_heap_insert. iFrame.
Qed.
Lemma gen_heap_valid σ l q v : gen_heap_ctx σ - l {q} v - ⌜σ !! l = Some v.
Proof.
iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iDestruct (own_valid_2 with "Hσ Hl")
as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2; auto.
Qed.
Lemma gen_heap_update σ l v1 v2 :
gen_heap_ctx σ - l v1 == gen_heap_ctx (<[l:=v2]>σ) l v2.
Proof.
iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iDestruct (own_valid_2 with "Hσ Hl")
as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ eapply auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, DecAgree v2))=> //.
by rewrite /to_gen_heap lookup_fmap Hl. }
iModIntro. rewrite to_gen_heap_insert. iFrame.
Qed.
End gen_heap.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment