Commit a225790a authored by Robbert Krebbers's avatar Robbert Krebbers

Attach ghost data to locations.

parent 31bf88ff
From iris.algebra Require Import auth gmap frac agree.
From iris.algebra Require Import auth gmap frac agree csum excl.
From iris.base_logic.lib Require Export own.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
......@@ -7,21 +7,36 @@ Import uPred.
Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
gmapUR L (prodR fracR (agreeR (leibnizC V))).
Definition gen_metaUR (L : Type) `{Countable L} : ucmraT :=
gmapUR L (agreeR gnameC).
Definition to_gen_heap {L V} `{Countable L} : gmap L V gen_heapUR L V :=
fmap (λ v, (1%Qp, to_agree (v : leibnizC V))).
Definition to_gen_meta `{Countable L} : gmap L gname gen_metaUR L :=
fmap to_agree.
(** The CMRA we need. *)
Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
gen_heap_name : gname
gen_meta_inG :> inG Σ (authR (gen_metaUR L));
gen_meta_data_inG :> inG Σ (csumR (exclR unitC) (agreeR positiveC));
gen_heap_name : gname;
gen_meta_name : gname
}.
Arguments gen_heap_name {_ _ _ _ _} _ : assert.
Arguments gen_meta_name {_ _ _ _ _} _ : assert.
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} :=
{ gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }.
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V));
gen_meta_preG_inG :> inG Σ (authR (gen_metaUR L));
gen_meta_data_preG_inG :> inG Σ (csumR (exclR unitC) (agreeR positiveC));
}.
Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors :=
#[GFunctor (authR (gen_heapUR L V))].
Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
GFunctor (authR (gen_heapUR L V));
GFunctor (authR (gen_metaUR L));
GFunctor (csumR (exclR unitC) (agreeR positiveC))
].
Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
subG (gen_heapΣ L V) Σ gen_heapPreG L V Σ.
......@@ -30,14 +45,30 @@ Proof. solve_inG. Qed.
Section definitions.
Context `{Countable L, hG : !gen_heapG L V Σ}.
Definition gen_heap_ctx (σ : gmap L V) : iProp Σ :=
own (gen_heap_name hG) ( (to_gen_heap σ)).
Definition gen_heap_ctx (σ : gmap L V) : iProp Σ := ( m,
dom _ m dom (gset L) σ
own (gen_heap_name hG) ( (to_gen_heap σ))
own (gen_meta_name hG) ( (to_gen_meta m)))%I.
Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
own (gen_heap_name hG) ( {[ l := (q, to_agree (v : leibnizC V)) ]}).
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
Definition mapsto := mapsto_aux.(unseal).
Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
Definition meta_token_def (l : L) : iProp Σ :=
( γm, own (gen_meta_name hG) ( {[ l := to_agree γm ]})
own γm (Cinl (Excl ())))%I.
Definition meta_token_aux : seal (@meta_token_def). by eexists. Qed.
Definition meta_token := meta_token_aux.(unseal).
Definition meta_token_eq : @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
Definition meta_def `{Countable A} (l : L) (x : A) : iProp Σ :=
( γm, own (gen_meta_name hG) ( {[ l := to_agree γm ]})
own γm (Cinr (to_agree (encode x))))%I.
Definition meta_aux : seal (@meta_def). by eexists. Qed.
Definition meta {A dA cA} := meta_aux.(unseal) A dA cA.
Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
End definitions.
Local Notation "l ↦{ q } v" := (mapsto l q v)
......@@ -51,6 +82,7 @@ Local Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
Section to_gen_heap.
Context (L V : Type) `{Countable L}.
Implicit Types σ : gmap L V.
Implicit Types m : gmap L gname.
(** Conversion to heaps and back *)
Lemma to_gen_heap_valid σ : to_gen_heap σ.
......@@ -67,17 +99,25 @@ Section to_gen_heap.
Lemma to_gen_heap_insert l v σ :
to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizC V))]> (to_gen_heap σ).
Proof. by rewrite /to_gen_heap fmap_insert. Qed.
Lemma to_gen_heap_delete l σ :
to_gen_heap (delete l σ) = delete l (to_gen_heap σ).
Proof. by rewrite /to_gen_heap fmap_delete. Qed.
Lemma to_gen_meta_valid m : to_gen_meta m.
Proof. intros l. rewrite lookup_fmap. by case (m !! l). Qed.
Lemma lookup_to_gen_meta_None m l : m !! l = None to_gen_meta m !! l = None.
Proof. by rewrite /to_gen_meta lookup_fmap=> ->. Qed.
Lemma to_gen_meta_insert l m γm :
to_gen_meta (<[l:=γm]> m) = <[l:=to_agree γm]> (to_gen_meta m).
Proof. by rewrite /to_gen_meta fmap_insert. Qed.
End to_gen_heap.
Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
(|==> _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
Proof.
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
iMod (own_alloc ( to_gen_heap σ)) as (γh) "Hh".
{ rewrite auth_auth_valid. exact: to_gen_heap_valid. }
iModIntro. by iExists (GenHeapG L V Σ _ _ _ γ).
iMod (own_alloc ( to_gen_meta )) as (γm) "Hm".
{ rewrite auth_auth_valid. exact: to_gen_meta_valid. }
iModIntro. iExists (GenHeapG L V Σ _ _ _ _ _ γh γm).
iExists ; simpl. iFrame "Hh Hm". by rewrite dom_empty_L.
Qed.
Section gen_heap.
......@@ -85,6 +125,7 @@ Section gen_heap.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : V iProp Σ.
Implicit Types σ : gmap L V.
Implicit Types m : gmap L gname.
Implicit Types h g : gen_heapUR L V.
Implicit Types l : L.
Implicit Types v : V.
......@@ -131,44 +172,74 @@ Section gen_heap.
iApply (mapsto_valid l _ v2). by iFrame.
Qed.
(** General properties of [meta] and [meta_token] *)
Global Instance meta_token_timeless l : Timeless (meta_token l).
Proof. rewrite meta_token_eq /meta_token_def. apply _. Qed.
Global Instance meta_timeless `{Countable A} l (x : A) : Timeless (meta l x).
Proof. rewrite meta_eq /meta_def. apply _. Qed.
Global Instance meta_persistent `{Countable A} l (x : A) : Persistent (meta l x).
Proof. rewrite meta_eq /meta_def. apply _. Qed.
Lemma meta_agree `{Countable A} l (x1 x2 : A) :
meta l x1 - meta l x2 - x1 = x2.
Proof.
rewrite meta_eq /meta_def.
iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
iAssert γm1 = γm2 %I as %->.
{ iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
move: Hγ. rewrite -auth_frag_op op_singleton=> /auth_frag_valid /=.
rewrite singleton_valid. apply: agree_op_invL'. }
iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
move: Hγ=> /agree_op_invL'. by intros ?%(inj _).
Qed.
Lemma meta_set `{Countable A} l (x : A) : meta_token l == meta l x.
Proof.
rewrite meta_token_eq meta_eq /meta_token_def /meta_def.
iDestruct 1 as (γm) "[Hγm Hm]". iExists γm. iFrame "Hγm".
iApply (own_update with "Hm"). by apply cmra_update_exclusive.
Qed.
(** Update lemmas *)
Lemma gen_heap_alloc σ l v :
σ !! l = None gen_heap_ctx σ == gen_heap_ctx (<[l:=v]>σ) l v.
σ !! l = None
gen_heap_ctx σ == gen_heap_ctx (<[l:=v]>σ) l v meta_token l.
Proof.
iIntros (?) "Hσ". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iIntros (Hσl). rewrite /gen_heap_ctx mapsto_eq /mapsto_def meta_token_eq /meta_token_def /=.
iDestruct 1 as (m Hσm) "[Hσ Hm]".
iMod (own_update with "Hσ") as "[Hσ Hl]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizC _)))=> //.
by apply lookup_to_gen_heap_None. }
iModIntro. rewrite to_gen_heap_insert. iFrame.
iMod (own_alloc (Cinl (Excl ()))) as (γm) "Hγm"; first done.
iMod (own_update with "Hm") as "[Hm Hlm]".
{ eapply auth_update_alloc.
eapply (alloc_singleton_local_update _ l (to_agree γm))=> //.
apply lookup_to_gen_meta_None.
move: Hσl. rewrite -!(not_elem_of_dom (D:=gset L)). set_solver. }
iModIntro. iFrame "Hl". iSplitL "Hσ Hm"; last by eauto with iFrame.
iExists (<[l:=γm]> m).
rewrite to_gen_heap_insert to_gen_meta_insert !dom_insert_L. iFrame.
iPureIntro. set_solver.
Qed.
Lemma gen_heap_alloc_gen σ σ' :
σ' ## σ gen_heap_ctx σ == gen_heap_ctx (σ' σ) [ map] l v σ', l v.
Proof.
revert σ; induction σ' as [| l v σ' Hl IHσ'] using map_ind;
iIntros (σ Hσdisj) "Hσ".
- by rewrite left_id big_opM_empty; iFrame.
- iMod (IHσ' with "Hσ") as "[Hσ m]"; first by eapply map_disjoint_insert_l.
rewrite big_opM_insert //; iFrame.
assert (σ !! l = None).
{ eapply map_disjoint_Some_r; first by eauto.
rewrite lookup_insert //. }
rewrite -insert_union_l //.
iMod (gen_heap_alloc with "Hσ") as "[$ $]"; last done.
apply lookup_union_None; split; auto.
Qed.
Lemma gen_heap_dealloc σ l v :
gen_heap_ctx σ - l v == gen_heap_ctx (delete l σ).
σ' ## σ
gen_heap_ctx σ ==
gen_heap_ctx (σ' σ) ([ map] l v σ', l v) ([ map] l _ σ', meta_token l).
Proof.
iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
rewrite to_gen_heap_delete. iApply (own_update_2 with "Hσ Hl").
eapply auth_update_dealloc, (delete_singleton_local_update _ _ _).
revert σ; induction σ' as [| l v σ' Hl IH] using map_ind; iIntros (σ Hdisj) "Hσ".
{ rewrite left_id_L. auto. }
iMod (IH with "Hσ") as "[Hσ'σ Hσ']"; first by eapply map_disjoint_insert_l.
decompose_map_disjoint.
rewrite !big_opM_insert // -insert_union_l //.
by iMod (gen_heap_alloc with "Hσ'σ") as "($ & $ & $)";
first by apply lookup_union_None.
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 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iDestruct (own_valid_2 with "Hσ Hl")
as %[Hl%gen_heap_singleton_included _]%auth_both_valid; auto.
Qed.
......@@ -176,13 +247,16 @@ Section gen_heap.
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 1 as (m Hσm) "[Hσ Hm]".
iIntros "Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iDestruct (own_valid_2 with "Hσ Hl")
as %[Hl%gen_heap_singleton_included _]%auth_both_valid.
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ eapply auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, to_agree (v2:leibnizC _)))=> //.
by rewrite /to_gen_heap lookup_fmap Hl. }
iModIntro. rewrite to_gen_heap_insert. iFrame.
iModIntro. iFrame "Hl". iExists m. rewrite to_gen_heap_insert. iFrame.
iPureIntro. apply (elem_of_dom_2 (D:=gset L)) in Hl.
rewrite dom_insert_L. set_solver.
Qed.
End gen_heap.
......@@ -32,7 +32,7 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
Definition array `{!heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
([ list] i v vs, loc_add l i v)%I.
([ list] i v vs, (l + i) v)%I.
Notation "l ↦∗ vs" := (array l vs)
(at level 20, format "l ↦∗ vs") : bi_scope.
......@@ -218,7 +218,7 @@ Lemma array_singleton l v : l ↦∗ [v] ⊣⊢ l ↦ v.
Proof. by rewrite /array /= right_id loc_add_0. Qed.
Lemma array_app l vs ws :
l ↦∗ (vs ++ ws) l ↦∗ vs (loc_add l (length vs)) ↦∗ ws.
l ↦∗ (vs ++ ws) l ↦∗ vs (l + length vs) ↦∗ ws.
Proof.
rewrite /array big_sepL_app.
setoid_rewrite Nat2Z.inj_add.
......@@ -234,70 +234,82 @@ Proof.
Qed.
Lemma heap_array_to_array l vs :
([ map] i v heap_array l vs, i v)%I - l ↦∗ vs.
([ map] l' v heap_array l vs, l' v) - l ↦∗ vs.
Proof.
iIntros "Hvs".
iInduction vs as [|v vs] "IH" forall (l); simpl.
{ by rewrite big_opM_empty /array big_opL_nil. }
iIntros "Hvs". iInduction vs as [|v vs] "IH" forall (l); simpl.
{ by rewrite /array. }
rewrite big_opM_union; last first.
{ apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
intros (j&?&Hjl&_)%heap_array_lookup.
rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl;
apply loc_add_inj in Hjl; lia. }
rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
rewrite array_cons.
rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]".
by iApply "IH".
Qed.
Lemma heap_array_to_seq_meta l vs n :
length vs = n
([ map] l' _ heap_array l vs, meta_token l') -
[ list] i seq 0 n, meta_token (l + (i : nat)).
Proof.
iIntros (<-) "Hvs". iInduction vs as [|v vs] "IH" forall (l)=> //=.
rewrite big_opM_union; last first.
{ apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
intros (j&?&Hjl&_)%heap_array_lookup.
rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
rewrite loc_add_0 -fmap_seq big_sepL_fmap.
setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
setoid_rewrite <-loc_add_assoc.
rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
Qed.
(** Heap *)
Lemma wp_allocN s E v n :
0 < n
{{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
{{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v }}}.
{{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v
[ list] i seq 0 (Z.to_nat n), meta_token (l + (i : nat)) }}}.
Proof.
iIntros (Hn Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by auto with lia.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
iMod (@gen_heap_alloc_gen with "Hσ") as "(Hσ & Hl & Hm)".
{ apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
rewrite replicate_length Z2Nat.id; auto with lia. }
iModIntro; iSplit; auto.
iFrame. iApply "HΦ".
by iApply heap_array_to_array.
iModIntro; iSplit; first done. iFrame "Hσ Hκs". iApply "HΦ". iSplitL "Hl".
- by iApply heap_array_to_array.
- iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
Qed.
Lemma twp_allocN s E v n :
0 < n
[[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
[[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v }]].
[[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v
[ list] i seq 0 (Z.to_nat n), meta_token (l + (i : nat)) }]].
Proof.
iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
iMod (@gen_heap_alloc_gen with "Hσ") as "(Hσ & Hl & Hm)".
{ apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
rewrite replicate_length Z2Nat.id; auto with lia. }
iModIntro; iSplit; auto.
iFrame; iSplit; auto. iApply "HΦ".
by iApply heap_array_to_array.
iModIntro; do 2 (iSplit; first done). iFrame "Hσ Hκs". iApply "HΦ". iSplitL "Hl".
- by iApply heap_array_to_array.
- iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
Qed.
Lemma wp_alloc s E v :
{{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l v }}}.
{{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l v meta_token l }}}.
Proof.
iIntros (Φ) "_ HΦ".
iApply wp_allocN; auto with lia.
iNext; iIntros (l) "H".
iApply "HΦ".
by rewrite array_singleton.
iIntros (Φ) "_ HΦ". iApply wp_allocN; auto with lia.
iIntros "!>" (l) "/= (? & ? & _)".
rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
Qed.
Lemma twp_alloc s E v :
[[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l v }]].
[[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l v meta_token l }]].
Proof.
iIntros (Φ) "_ HΦ".
iApply twp_allocN; auto with lia.
iIntros (l) "H".
iApply "HΦ".
by rewrite array_singleton.
iIntros (Φ) "_ HΦ". iApply twp_allocN; auto with lia.
iIntros (l) "/= (? & ? & _)".
rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
Qed.
Lemma wp_load s E l q v :
......
......@@ -189,7 +189,7 @@ Proof.
rewrite -wp_bind. eapply wand_apply; first exact: wp_allocN.
rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
by rewrite right_id HΔ'.
apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r.
Qed.
Lemma tac_twp_allocN Δ s E j K v n Φ :
0 < n
......@@ -203,7 +203,7 @@ Proof.
rewrite -twp_bind. eapply wand_apply; first exact: twp_allocN.
rewrite left_id. apply forall_intro=> l.
destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
by rewrite right_id HΔ'.
apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r.
Qed.
Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
......@@ -217,7 +217,7 @@ Proof.
rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
by rewrite right_id HΔ'.
apply wand_intro_l. by rewrite (sep_elim_l (l v)%I) right_id wand_elim_r.
Qed.
Lemma tac_twp_alloc Δ s E j K v Φ :
( l, Δ',
......@@ -229,7 +229,7 @@ Proof.
rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc.
rewrite left_id. apply forall_intro=> l.
destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
by rewrite right_id HΔ'.
apply wand_intro_l. by rewrite (sep_elim_l (l v)%I) right_id wand_elim_r.
Qed.
Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
......
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