Commit 9e4642cf authored by Robbert Krebbers's avatar Robbert Krebbers

Array hacking.

parent 87adc879
......@@ -61,31 +61,27 @@ Class amonadG (Σ : gFunctors) := AMonadG {
Section a_wp.
Context `{amonadG Σ}.
(* X ⊆ σ^{-1}(L) *)
Definition correct_locks (X : gset val) (preσ : gset loc) : Prop :=
set_Forall (λ v, l : loc, v = #l l preσ) X.
Definition env_inv (env : val) : iProp Σ :=
( (X : gset val) (σ : gmap loc (lvl*val)),
is_mset env X
full_locking_heap σ
correct_locks X (locked_locs σ))%I.
( (X : gset cloc) (σ : gmap cloc (lvl * val)),
X locked_locs σ
is_mset env X
full_locking_heap σ)%I.
Definition flock_resources (γ : flock_name) (I : gmap prop_id (iProp Σ * frac)) :=
([ map] i p I, flock_res γ i p.1 p.2)%I.
Definition awp (e : expr)
(R : iProp Σ) (Φ : val iProp Σ) : iProp Σ :=
tc_opaque (WP e {{ ev, (γ : flock_name) (env : val) (l : val) (I : gmap prop_id (iProp Σ * frac)),
is_flock amonadN γ l -
flock_resources γ I -
(([ map] p I, p.1) (env_inv env R)) -
WP ev env l {{ v, Φ v flock_resources γ I }}
tc_opaque (WP e {{ ev,
(γ : flock_name) (env : val) (l : val) (I : gmap prop_id (iProp Σ * frac)),
is_flock amonadN γ l -
flock_resources γ I -
([ map] p I, p.1) (env_inv env R) -
WP ev env l {{ v, Φ v flock_resources γ I }}
}})%I.
Global Instance elim_bupd_awp p e Φ :
ElimModal True p false (|==> P) P
(awp e R Φ) (awp e R Φ).
ElimModal True p false (|==> P) P (awp e R Φ) (awp e R Φ).
Proof.
iIntros (P R _) "[HP HA]".
rewrite /awp /tc_opaque /= bi.intuitionistically_if_elim.
......@@ -234,8 +230,8 @@ Section a_wp_rules.
Lemma awp_atomic_env (e : expr) (ev : val) R Φ :
IntoVal e ev
( env, env_inv env - R -
WP ev env {{ w, env_inv env R Φ w }}) -
AWP (a_atomic_env e) @ R {{ Φ }}.
WP ev env {{ w, (env_inv env R Φ w) }}) -
AWP a_atomic_env e @ R {{ Φ }}.
Proof.
iIntros (<-) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam.
iIntros (γ env l I) "#Hlock Hres #Heq". do 2 wp_lam.
......@@ -255,7 +251,7 @@ Section a_wp_rules.
AWP e1 @ R {{ Ψ1 }} -
AWP e2 @ R {{ Ψ2 }} -
( w1 w2, Ψ1 w1 - Ψ2 w2 - Φ (w1,w2)%V) -
AWP (a_par e1 e2) @ R {{ Φ }}.
AWP e1 ||| e2 @ R {{ Φ }}.
Proof.
iIntros "Hwp1 Hwp2 HΦ". rewrite /a_par /awp /=.
wp_bind e1. iApply (wp_wand with "Hwp1").
......@@ -303,8 +299,8 @@ Section a_wp_run.
wp_apply (newlock_cancel_spec amonadN); first done.
iIntros (k γ') "#Hlock". rewrite- wp_fupd.
iMod (flock_res_single_alloc _ _ _ (env_inv env R)%I
with "Hlock [Henv Hσ $HR]") as (i) "[_ Hres]"; first done.
{ iNext. iExists , . iFrame. eauto. }
with "Hlock [Henv Hσ $HR]") as (i) "[_ Hres]"; first done.
{ iNext. iExists , . rewrite /locked_locs dom_empty_L. by iFrame. }
iSpecialize ("Hwp" $! amg).
iMod (wp_value_inv with "Hwp") as "Hwp".
wp_let. wp_bind (ev env k).
......
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac auth.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.lib Require Import locking_heap mset flock U list.
From iris_c.c_translation Require Import proofmode.
Notation "♯ l" := (a_ret (LitV l%Z%V)) (at level 8, format "♯ l").
Notation "♯ l" := (a_ret (Lit l%Z%V)) (at level 8, format "♯ l") : expr_scope.
Definition a_alloc : val := λ: "x",
Definition a_alloc : val := λ: "n" "x",
"v" ←ᶜ "x" ;;
a_atomic_env (λ: <>, ref "v").
a_atomic_env (λ: <>, lreplicate "n" "v").
Notation "'allocᶜ' e1" := (a_alloc e1%E) (at level 80) : expr_scope.
Definition a_store : val := λ: "x1" "x2",
"vv" ←ᶜ "x1" ||| "x2" ;;
a_atomic_env (λ: "env",
mset_add (Fst "vv") "env" ;;
Fst "vv" <- Snd "vv" ;;
Snd "vv"
let: "l" := Fst (Fst "vv") in
let: "i" := Snd (Fst "vv") in
let: "v" := Snd "vv" in
mset_add ("l", "i") "env" ;;
let: "ll" := !"l" in
"l" <- linsert "i" "v" "ll" ;;
"v"
).
Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
Definition a_load : val := λ: "x",
"v" ←ᶜ "x";;
a_atomic_env (λ: "env",
assert: (mset_member "v" "env" = #false);;
!"v"
let: "l" := Fst "v" in
let: "i" := Snd "v" in
assert: (mset_member ("l", "i") "env" = #false);;
let: "ll" := !"l" in
llookup "i" "ll"
).
Notation "∗ᶜ e" :=
(a_load e)%E (at level 9, right associativity) : expr_scope.
......@@ -93,6 +100,7 @@ Definition a_invoke: val := λ: "f" "arg",
Section proofs.
Context `{amonadG Σ}.
(*
Lemma a_alloc_spec R Φ e :
AWP e @ R {{ v, ∀ l : loc, l ↦C v -∗ Φ #l }} -∗
AWP allocᶜ e @ R {{ Φ }}.
......@@ -119,26 +127,12 @@ Section proofs.
iPureIntro. by rewrite locked_locs_alloc_unlocked.
- iApply ("H" with "Hl'").
Qed.
(* DF TODO: move this somewhere else? *)
Lemma big_sepM_insert_overwrite `{Countable K, EqDecision K} {A : Type}
(Φ : K A iProp Σ) (m : gmap K A) i x x' :
m !! i = Some x
([ map] ky m, Φ k y)
Φ i x (Φ i x' - ([ map] ky <[i:=x']> m, Φ k y)).
Proof.
intros ?.
rewrite {1}big_sepM_delete //. iIntros "[$ ?]".
rewrite -insert_delete big_sepM_insert ?lookup_delete //.
eauto with iFrame.
Qed.
*)
Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
AWP e1 @ R {{ Ψ1 }} -
AWP e2 @ R {{ Ψ2 }} -
( v1 v2,
Ψ1 v1 - Ψ2 v2 - (l : loc) w,
v1 = #l l C w (l C[LLvl] v2 - Φ v2)) -
( v1 v2, Ψ1 v1 - Ψ2 v2 - w, v1 C w (v1 C[LLvl] v2 - Φ v2)) -
AWP e1 = e2 @ R {{ Φ }}.
Proof.
iIntros "H1 H2 HΦ".
......@@ -146,91 +140,51 @@ Section proofs.
awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam.
iApply awp_bind. iApply (awp_par with "H1 H2").
iIntros "!>" (w1 w2) "H1 H2 !>". awp_lam.
iDestruct ("HΦ" with "H1 H2") as (l w ->) "[Hl HΦ]".
iDestruct ("HΦ" with "H1 H2") as (w) "[Hl HΦ]".
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hl.
assert (#l X).
{ unfold correct_locks in *. intros Hx. apply Hl.
destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
wp_let. wp_proj.
wp_apply (mset_add_spec with "HX"); first done.
iIntros "HX". wp_seq.
iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %?.
do 2 wp_proj.
iDestruct "Hσ" as "[Hσ Hls]".
rewrite {1}mapsto_eq /mapsto_def.
iDestruct "Hl" as (b' Hb%lvl_included) "Hl".
assert (b' = ULvl) as -> by (destruct b'; naive_solver).
rewrite (big_sepM_insert_overwrite _ _ l _ (ULvl, w2)) ?lookup_insert //.
iDestruct "Hls" as "[Hl' Hls] /=".
wp_store.
iSpecialize ("Hls" with "Hl'").
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ apply (auth_update _ _ (to_locking_heap (<[l:=(ULvl,w2)]>σ)) {[l := (1%Qp, ULvl, agree.to_agree w2)]}).
rewrite !to_locking_heap_insert.
eapply (gmap.singleton_local_update (to_locking_heap σ)); first by apply to_locking_heap_lookup_Some.
by apply exclusive_local_update. }
iCombine "Hσ Hls" as "Hσ".
iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ [Hl]") as "[Hσ Hl]".
{ rewrite mapsto_eq /mapsto_def. eauto. }
wp_proj. iFrame "HR". iSplitR "HΦ Hl".
- iExists ({[#l]} X),(<[l:=(LLvl,w2)]> σ). iFrame. iSplitL.
+ rewrite /full_locking_heap insert_insert //.
+ (* TODO: a separate lemma somewhere *)
iPureIntro. rewrite locked_locs_lock.
revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
- by iApply "HΦ".
iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hw1.
iMod (locking_heap_store with "Hσ Hl") as (l i ll vs -> Hl Hi) "[Hl Hclose]".
wp_let. do 2 wp_proj; wp_let. do 2 wp_proj; wp_let. wp_proj; wp_let.
wp_apply (mset_add_spec with "[$]"); [set_solver|]; iIntros "Hlocks /="; wp_seq.
wp_load; wp_let.
wp_apply (linsert_spec with "[//]"); [eauto|]; iIntros (ll' Hl').
iApply wp_fupd. wp_store.
iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
iIntros "!> !> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
iExists ({[(#l, #i)%V]} X), _. iFrame "Hσ". rewrite locked_locs_lock.
iIntros "{$Hlocks} !%". set_solver.
Qed.
Lemma a_load_spec_exists_frac R Φ e :
AWP e @ R {{ v, (l : loc) (q : Qp) (w : val), v = #l l C{q} w (l C{q} w - Φ w) }} -
AWP e @ R {{ v, q w, v C{q} w (v C{q} w - Φ w) }} -
AWP ∗ᶜe @ R {{ Φ }}.
Proof.
iIntros "H".
awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
iApply awp_bind.
iApply (awp_wand with "H"). clear v.
iIntros (v). iDestruct 1 as (l q w) "(% & Hl & HΦ)". subst.
awp_lam.
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hl.
assert (#l X).
{ unfold correct_locks in *. intros Hx. apply Hl.
destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. }
wp_lam. wp_apply wp_assert.
wp_apply (mset_member_spec with "HX").
iIntros "Henv /=". case_decide; first by exfalso. simpl.
wp_op. iSplit; eauto. iNext. wp_seq.
iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hσl.
rewrite mapsto_eq /mapsto_def.
iDestruct "Hl" as (b' Hb%lvl_included) "Hl".
assert (b' = ULvl) as -> by (destruct b'; naive_solver).
iDestruct "Hσ" as "[Hσ Hls]".
rewrite (big_sepM_lookup_acc _ _ l) //. iDestruct "Hls" as "[Hl' Hls] /=".
wp_load. iSpecialize ("Hls" with "Hl'").
iFrame "HR".
iSplitR "HΦ Hl".
- iExists X,σ. by iFrame.
- iApply "HΦ". eauto.
iApply awp_bind. iApply (awp_wand with "H"). clear v.
iIntros (v). iDestruct 1 as (q w) "[Hl HΦ]". awp_lam.
iApply awp_atomic_env. iIntros (env) "Henv HR".
iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hv.
iMod (locking_heap_load with "Hσ Hl") as (l i ll vs -> Hl Hi) "[Hl Hclose]".
wp_let. wp_proj; wp_let. wp_proj; wp_let.
wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
rewrite bool_decide_false; last set_solver.
wp_op. iSplit; first done. iNext; wp_seq.
wp_load; wp_let. wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
iDestruct ("Hclose" with "Hl") as "[Hσ Hl]".
iIntros "!> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
iExists X, _. by iFrame.
Qed.
Lemma a_load_spec R Φ q e :
AWP e @ R {{ v, (l : loc) (w : val), v = #l l C{q} w (l C{q} w - Φ w) }} -
AWP e @ R {{ v, w, v C{q} w (v C{q} w - Φ w) }} -
AWP ∗ᶜe @ R {{ Φ }}.
Proof.
iIntros "H".
iApply a_load_spec_exists_frac.
iIntros "H". iApply a_load_spec_exists_frac.
awp_apply (awp_wand with "H").
iIntros (v) "H". iDestruct "H" as (l w ->) "[H1 H2]".
eauto with iFrame.
iIntros (v). iDestruct 1 as (w) "[H1 H2]"; eauto with iFrame.
Qed.
Lemma a_un_op_spec R Φ e op:
......@@ -293,33 +247,30 @@ Section proofs.
Lemma a_pre_bin_op_spec R Φ Ψ1 Ψ2 e1 e2 op :
AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 - R -
l v w, l C v v1 = #l
bin_op_eval op v v2 = Some w
(l C[LLvl] w - R Φ v)) -
v w, v1 C v
bin_op_eval op v v2 = Some w
(v1 C[LLvl] w - R Φ v)) -
AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
Proof.
iIntros "He1 He2 HΦ". rewrite /a_pre_bin_op.
awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
iIntros (v1 v2) "Hv1 Hv2". iNext. awp_let.
iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
iApply awp_atomic. iNext.
iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (l v w) "(Hl & % & % & HΦ)".
iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (v w) "(Hl & % & HΦ)".
simplify_eq/=. iExists True%I. rewrite left_id. awp_lam.
iApply awp_bind. awp_proj. iApply a_load_spec. iApply awp_ret. wp_value_head.
iExists l, v; iFrame. iSplit; eauto.
iExists v; iFrame.
iIntros "Hl". awp_let. iApply awp_bind.
iApply (a_store_spec _ _ (λ v', v' = #l)%I
(λ v', v' = w)%I
with "[] [] [-]").
iApply (a_store_spec _ _
(λ v', v' = v1)%I (λ v', v' = w)%I with "[] [] [-]").
- awp_proj. iApply awp_ret; by wp_value_head.
- iApply (a_bin_op_spec _ _ (λ v', v' = v)%I
(λ v', v' = v2)%I);
- iApply (a_bin_op_spec _ _ (λ v', v' = v)%I (λ v', v' = v2)%I);
try (try awp_proj; iApply awp_ret; by wp_value_head).
iNext. iIntros (? ? -> ->). eauto.
- iNext. iIntros (? ? -> ->).
iExists _,_; iFrame. iSplit; eauto.
iIntros "?". awp_seq. iApply awp_ret; wp_value_head.
iExists _; iFrame. iIntros "?". awp_seq. iApply awp_ret; wp_value_head.
iIntros "_". by iApply "HΦ".
Qed.
......@@ -328,26 +279,19 @@ Section proofs.
AWP (a_seq #()) @ R {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /a_seq. awp_lam.
iApply awp_atomic_env.
iIntros (env) "Henv HR".
iApply wp_fupd.
rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
wp_lam. iApply (mset_clear_spec with "HX").
iNext. iIntros "HX".
iApply awp_atomic_env. iIntros (env) "Henv $". iApply wp_fupd.
iDestruct "Henv" as (X σ _) "[Hlocks Hσ]".
wp_lam. wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
iDestruct "HΦ" as (us) "[Hus HΦ]".
clear Hlocks.
iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl.
- iModIntro. iFrame "HR". iSplitR "HΦ".
+ iExists , σ. iFrame. iPureIntro.
rewrite /correct_locks /set_Forall. set_solver.
- iModIntro. iSplitR "HΦ".
+ iExists , σ. by iFrame.
+ by iApply "HΦ".
- iDestruct "Hus" as "[Hu Hus]".
iDestruct (full_locking_heap_present with "Hu Hσ") as %[z Hz].
iMod (locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]".
iApply ("IH" with "Hus [HΦ Hu] Hσ HR HX").
{ iIntros "Hus". iApply "HΦ". by iFrame. }
iApply ("IH" with "Hus [HΦ Hu] Hσ Hlocks").
iIntros "Hus". iApply "HΦ". by iFrame.
Qed.
Lemma a_sequence_spec R Φ (f e : expr) :
......
......@@ -8,7 +8,7 @@ Section U.
(** * Unlocking modality *)
Definition U (P : iProp Σ) : iProp Σ :=
( ls : list (loc * (frac * val)),
( ls : list (cloc * (frac * val)),
([ list] x ls, x.1 C[LLvl]{x.2.1} x.2.2)
(([ list] x ls, x.1 C{x.2.1} x.2.2) - P))%I.
......
......@@ -70,7 +70,7 @@ Lemma ltail_spec hd vs v :
{{{ is_list hd (v :: vs) }}} ltail hd {{{ hd', RET hd'; is_list hd' vs }}}.
Proof. iIntros (Φ (hd'&->&?)) "HΦ". repeat wp_pure _. by iApply "HΦ". Qed.
Lemma llookup_spec_spec i hd vs v :
Lemma llookup_spec i hd vs v :
vs !! i = Some v
{{{ is_list hd vs }}} llookup #i hd {{{ RET v; True }}}.
Proof.
......@@ -82,7 +82,7 @@ Proof.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
Qed.
Lemma linsert_spec_spec i hd vs v :
Lemma linsert_spec i hd vs v :
is_Some (vs !! i)
{{{ is_list hd vs }}} linsert #i v hd {{{ hd', RET hd'; is_list hd' (<[i:=v]> vs) }}}.
Proof.
......
From iris.algebra Require Import cmra auth gmap frac agree.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Export own.
From iris.heap_lang Require Import lang lifting.
From iris.proofmode Require Import tactics.
From iris_c.lib Require Import list.
Set Default Proof Using "Type".
Import uPred.
Inductive lvl :=
| LLvl : lvl
......@@ -23,11 +22,15 @@ Instance lvl_op : Op lvl := λ lv1 lv2,
Instance lvl_valid : Valid lvl := λ _, True.
Instance lvl_unit : Unit lvl := LLvl.
Instance lvl_pcore : PCore lvl := λ _, Some LLvl.
Lemma lvl_included lv1 lv2 : lv1 lv2 lv1 = lv2 lv1 = LLvl lv2 = ULvl.
Lemma lvl_included lv1 lv2 :
lv1 lv2 match lv2 with
| ULvl => True
| LLvl => if lv1 is LLvl then True else False
end.
Proof.
split.
- intros [[] ->%leibniz_equiv]; destruct lv1; naive_solver.
- intros [->|[-> ->]]. exists lv2. by destruct lv2. by exists ULvl.
- intros [[] ->%leibniz_equiv]; by destruct lv1.
- exists lv2. by destruct lv1, lv2.
Qed.
Lemma lvl_idemp (lv : lvl) : lv lv = lv.
......@@ -53,8 +56,10 @@ Proof. split; try (apply _ || done). by intros []. Qed.
Canonical Structure lvlUR : ucmraT := UcmraT lvl lvl_ucmra_mixin.
(* Auth (Loc -> (Q * Level)) *)
Notation cloc := val (only parsing).
Definition locking_heapUR : ucmraT :=
gmapUR loc (prodR (prodR fracR lvlUR) (agreeR valC)).
gmapUR cloc (prodR (prodR fracR lvlUR) (agreeR valC)).
(** The CMRA we need. *)
Class locking_heapG (Σ : gFunctors) := LHeapG {
......@@ -74,43 +79,47 @@ Proof. solve_inG. Qed.
Section definitions.
Context `{hG : locking_heapG Σ, !heapG Σ}.
Definition to_locking_heap (σ : gmap loc (lvl * val)) : locking_heapUR :=
Definition to_locking_heap (σ : gmap cloc (lvl * val)) : locking_heapUR :=
fmap (λ '(lv,v), (1%Qp, lv, to_agree v)) σ.
Definition is_lock_lvl (a : loc * (lvl * val)) : bool :=
match a.2.1 with
| LLvl => true
| ULvl => false
end.
(* σ^{-1}(L) *)
Definition locked_locs (σ : gmap loc (lvl * val)) : gset loc :=
dom (gset loc) (filter is_lock_lvl σ).
Definition locked_locs (σ : gmap cloc (lvl * val)) : gset cloc :=
dom _ (filter (λ x, x.2.1 = LLvl) σ).
Definition full_locking_heap (σ : gmap loc (lvl * val)) :=
(own lheap_name ( (to_locking_heap σ)) [ map] lbvσ, l bv.2)%I.
Definition cloc_loc_idx (cl : cloc) : option (loc * nat) :=
match cl with
| (LitV (LitLoc l), LitV (LitInt i))%V => guard (0 i); Some (l, Z.to_nat i)
| _ => None
end.
Definition full_locking_heap (σ : gmap cloc (lvl * val)) :=
( τ : gmap loc (list (lvl * val)),
cl, σ !! cl = ''(l,i) cloc_loc_idx cl; τ !! l = lookup (M:=list _) i
own lheap_name ( (to_locking_heap σ))
[ map] llvvs τ, lv, l lv is_list lv (snd <$> lvvs) )%I.
Definition mapsto_def (l : loc) (lv : lvl) (q : frac) (v: val) : iProp Σ :=
( lv' : lvl, lv lv'
own lheap_name ( {[ l := (q, lv', to_agree v) ]}))%I.
Definition mapsto_def (cl : cloc) (lv : lvl) (q : frac) (v: val) : iProp Σ :=
( lv',
lv lv'
own lheap_name ( {[ cl := (q, lv', to_agree v) ]}))%I.
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
Definition mapsto := unseal mapsto_aux.
Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
End definitions.
Notation "l ↦C[ lv ]{ q } v" :=
(mapsto l lv q%Qp v%V)
(at level 20, lv, q at level 50, format "l ↦C[ lv ]{ q } v") : bi_scope.
Notation "l ↦C[ lv ] v" := (l C[lv]{1} v)%I
(at level 20, lv at level 50, format "l ↦C[ lv ] v") : bi_scope.
Notation "l ↦C{ q } v" := (l C[ULvl]{q} v)%I
(at level 20, q at level 50, format "l ↦C{ q } v") : bi_scope.
Notation "l ↦C v" := (l C[ULvl]{1} v)%I
(at level 20, format "l ↦C v") : bi_scope.
Notation "cl ↦C[ lv ]{ q } v" :=
(mapsto cl lv q%Qp v%V)
(at level 20, lv, q at level 50, format "cl ↦C[ lv ]{ q } v") : bi_scope.
Notation "cl ↦C[ lv ] v" := (cl C[lv]{1} v)%I
(at level 20, lv at level 50, format "cl ↦C[ lv ] v") : bi_scope.
Notation "cl ↦C{ q } v" := (cl C[ULvl]{q} v)%I
(at level 20, q at level 50, format "cl ↦C{ q } v") : bi_scope.
Notation "cl ↦C v" := (cl C[ULvl]{1} v)%I
(at level 20, format "cl ↦C v") : bi_scope.
Lemma to_locking_heap_valid (σ : gmap loc (lvl * val)) : to_locking_heap σ.
Proof. intros l. rewrite lookup_fmap. by destruct (σ !! l) as [[]|]. Qed.
Lemma to_locking_heap_valid (σ : gmap cloc (lvl * val)) : to_locking_heap σ.
Proof. intros cl. rewrite lookup_fmap. by destruct (σ !! cl) as [[]|]. Qed.
Lemma locking_heap_init `{locking_heapPreG Σ, !heapG Σ} :
(|==> _ : locking_heapG Σ, full_locking_heap )%I.
......@@ -118,45 +127,20 @@ Proof.
iMod (own_alloc ( to_locking_heap )) as (γ) "Hh".
{ apply: auth_auth_valid. exact: to_locking_heap_valid. }
iModIntro. iExists (LHeapG Σ _ γ).
rewrite /full_locking_heap big_sepM_empty //. by iFrame.
iExists . iSplit; last by iFrame.
iIntros "!%" (cl). destruct (cloc_loc_idx cl) as [[]|]; by rewrite /= ?lookup_empty.
Qed.
Section properties.
Context `{hG : locking_heapG Σ, !heapG Σ}.
Implicit Type σ : gmap loc (lvl * val).
Implicit Type σ : gmap cloc (lvl * val).
Implicit Type lv : lvl.
Implicit Type l : loc.
Implicit Type i : nat.
Implicit Type cl : cloc.
Global Instance mapsto_timeless l lv q v : Timeless (l C[lv]{q} v).
Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
Global Instance mapsto_fractional l lv v : Fractional (λ q, l C[lv]{q} v)%I.
Proof.
intros p q. rewrite mapsto_eq /mapsto_def. iSplit.
- iDestruct 1 as (lv' ?) "Hl". rewrite -(lvl_idemp lv').
iDestruct "Hl" as "[Hl Hl']". iSplitL "Hl"; eauto.
- iIntros "[H1 H2]".
iDestruct "H1" as (lv1 ?) "Hl1". iDestruct "H2" as (lv2 ?) "Hl2".
iCombine "Hl1 Hl2" as "Hl".
rewrite frac_op'. iExists (lv1 lv2). iFrame. destruct lv1,lv2; eauto.
Qed.
Global Instance mapsto_as_fractional l q lv v :
AsFractional (l C[lv]{q} v) (λ q, l C[lv]{q} v)%I q.
Proof. split. done. apply _. Qed.
Lemma mapsto_downgrade' lv lv' l q v : lv lv' l C[lv']{q} v - l C[lv]{q} v.
Proof.
rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (lv'' ?) "Ho".
iExists lv''. iSplit; eauto. iPureIntro. by transitivity lv'.
Qed.
Lemma mapsto_downgrade lv l q v : l C{q} v - l C[lv]{q} v.
Proof. apply mapsto_downgrade'. apply lvl_included. destruct lv; eauto. Qed.
Lemma mapsto_value_agree lv lv' l q q' v v' :
l C[lv]{q} v - l C[lv']{q'} v' - v = v'.
Lemma mapsto_value_agree lv lv' cl q q' v v' :
cl C[lv]{q} v - cl C[lv']{q'} v' - v = v'.
Proof.
rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (lv1 ?) "Hl1". iDestruct 1 as (lv2 ?) "Hl2".
......@@ -164,62 +148,98 @@ Section properties.
revert Ho. rewrite /= op_singleton singleton_valid. by intros [_ ?%agree_op_invL'].
Qed.
Lemma mapsto_combine lv lv' l q q' v :
l C[lv]{q} v - l C[lv']{q'} v - l C[lvlv']{q+q'} v.
Lemma mapsto_combine lv lv' cl q q' v :
cl C[lv]{q} v - cl C[lv']{q'} v - cl C[lvlv']{q+q'} v.
Proof.
rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (lv1 ?) "Hl1". iDestruct 1 as (lv2 ?) "Hl2".
iExists (lv1 lv2). iSplitR.
{ iPureIntro. destruct lv,lv',lv1,lv2; eauto. }
iCombine "Hl1 Hl2" as "Hl". rewrite frac_op'. iFrame.
{ iPureIntro. by apply: cmra_mono. }
iCombine "Hl1 Hl2" as "Hl". rewrite frac_op'. by iFrame.
Qed.
Global Instance from_sep_mapsto l lv lv' q q' v :
FromSep (l C[lvlv']{q+q'} v) (l C[lv]{q} v) (l C[lv']{q'} v).
Global Instance from_sep_mapsto cl lv lv' q q' v :
FromSep (cl C[lvlv']{q+q'} v) (cl C[lv]{q} v) (cl C[lv']{q'} v).
Proof.
rewrite /FromSep. iIntros "[Hl1 Hl2]".
iApply (mapsto_combine with "Hl1 Hl2").
Qed.
Lemma to_locking_heap_insert σ l lv v :
to_locking_heap (<[l := (lv,v)]> σ) = <[l := (1%Qp, lv, to_agree v)]>(to_locking_heap σ).
Global Instance mapsto_timeless cl lv q v : Timeless (cl C[lv]{q} v).
Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
Global Instance mapsto_fractional cl lv v : Fractional (λ q, cl C[lv]{q} v)%I.
Proof.
intros p q. iSplit.
- rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (lv' ?) "Hl".