Skip to content

GitLab

Commit e5406329 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Start working on adding arrays.

parent 9e4642cf
Hide whitespace changes
Inline Side-by-side
Showing with 317 additions and 302 deletions
theories/c_translation/monad.v
View file @ e5406329
......@@ -62,8 +62,8 @@ Section a_wp.
Context `{amonadG Σ}.
Definition env_inv (env : val) : iProp Σ :=
(∃ (X : gset cloc) (σ : gmap cloc (lvl * val)),
⌜ X ⊆ locked_locs σ ⌝ ∧
(∃ (X : gset val) (σ : gmap cloc (lvl * val)),
⌜ ∀ v, v ∈ X → ∃ cl, cloc_of_val v = Some cl ∧ cl ∈ locked_locs σ ⌝ ∧
is_mset env X ∗
full_locking_heap σ)%I.
......@@ -300,7 +300,7 @@ Section a_wp_run.
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 ∅, ∅. rewrite /locked_locs dom_empty_L. by iFrame. }
{ iNext. iExists ∅, ∅. iFrame. iPureIntro; set_solver. }
iSpecialize ("Hwp" $! amg).
iMod (wp_value_inv with "Hwp") as "Hwp".
wp_let. wp_bind (ev env k).
......
theories/c_translation/translation.v
View file @ e5406329
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.heap_lang Require Import assert par.
From iris.algebra Require Import frac auth.
From iris_c.lib Require Import locking_heap mset flock U list.
From iris_c.lib Require Import mset flock list.
From iris_c.lib Require Export locking_heap U.
From iris_c.c_translation Require Export monad.
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.
Notation "♯ₗ l" := (a_ret (cloc_to_val l)) (at level 8, format "♯ₗ l") : expr_scope.
Definition a_alloc : val := λ: "n" "x",
"v" ←ᶜ "x" ;;ᶜ
a_atomic_env (λ: <>, lreplicate "n" "v").
Notation "'allocᶜ' e1" := (a_alloc e1%E) (at level 80) : expr_scope.
Definition a_alloc : val := λ: "x1" "x2",
"vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ
let: "n" := Fst "vv" in
let: "v" := Snd "vv" in
a_atomic_env (λ: <>, (ref (lreplicate "n" "v"), #0)).
Notation "'allocᶜ' ( e1 , e2 )" := (a_alloc e1%E e2%E) (at level 80) : expr_scope.
Definition a_store : val := λ: "x1" "x2",
"vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ
......@@ -100,39 +105,36 @@ 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 {{ Φ }}.
Lemma a_alloc_spec R Φ Ψ1 Ψ2 e1 e2 :
AWP e1 @ R {{ Ψ1 }} -∗
AWP e2 @ R {{ Ψ2 }} -∗
▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ n : nat,
⌜ v1 = #n ⌝ ∧
∀ l, (l,O) ↦C∗ replicate n v2 -∗ Φ (cloc_to_val (l,O))) -∗
AWP allocᶜ(e1, e2) @ 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) "H". awp_lam.
iIntros "H1 H2 HΦ".
awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
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_let. do 2 (awp_proj; awp_let).
iDestruct ("HΦ" with "H1 H2") as (n ->) "HΦ".
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
iApply wp_fupd.
wp_let. wp_alloc l as "Hl".
iAssert ⌜σ !! l = None⌝%I with "[Hl Hσ]" as %Hl.
{ remember (σ !! l) as σl. destruct σl as [[? ?]|]; simplify_eq; eauto.
iDestruct "Hσ" as "[_ Hls]".
iExFalso. rewrite (big_sepM_lookup _ σ l _); last eauto.
by iDestruct (mapsto_valid_2 l with "Hl Hls") as %[]. }
iMod (locking_heap_alloc σ l ULvl v with "Hl Hσ") as "[Hσ Hl']"; eauto.
iModIntro. iFrame "HR". iSplitR "H Hl'".
- iExists X,(<[l:=(ULvl,v)]>σ). iFrame.
iPureIntro. by rewrite locked_locs_alloc_unlocked.
- iApply ("H" with "Hl'").
iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_let.
wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
iApply wp_fupd. wp_alloc l as "Hl".
iMod (locking_heap_alloc with "Hσ Hl") as (?) "[Hσ Hl]"; first done.
iIntros "!> !>". iSplitL "Hlocks Hσ"; [|by iApply "HΦ"].
iExists X, _. iFrame.
iIntros "!%". intros w Hw. destruct (HX _ Hw) as (cl&Hcl&Hin).
exists cl; split; first done. by rewrite locked_locs_alloc_heap.
Qed.
*)
Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
AWP e1 @ R {{ Ψ1 }} -∗
AWP e2 @ R {{ Ψ2 }} -∗
▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ w, v1 ↦C w ∗ (v1 ↦C[LLvl] v2 -∗ Φ v2)) -∗
▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ cl w,
⌜ v1 = cloc_to_val cl ⌝ ∧ cl ↦C w ∗ (cl ↦C[LLvl] v2 -∗ Φ v2)) -∗
AWP e1 =ᶜ e2 @ R {{ Φ }}.
Proof.
iIntros "H1 H2 HΦ".
......@@ -140,37 +142,45 @@ 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 (w) "[Hl HΦ]".
iDestruct ("HΦ" with "H1 H2") as ([l i] w ->) "[Hl HΦ]".
iApply awp_atomic_env.
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]".
assert ((#l, #i)%V ∉ X).
{ intros Hcl. destruct (HX _ Hcl) as ([??]&[=]%cloc_to_of_val&?); naive_solver. }
iMod (locking_heap_store with "Hσ Hl") as (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_apply (mset_add_spec with "[$]"); first done.
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.
iIntros "{$Hlocks} !%".
intros v [->%elem_of_singleton|?]%elem_of_union; last set_solver.
eexists; split; [apply (cloc_of_to_val (l,i))|set_solver].
Qed.
Lemma a_load_spec_exists_frac R Φ e :
AWP e @ R {{ v, ∃ q w, v ↦C{q} w ∗ (v ↦C{q} w -∗ Φ w) }} -∗
AWP e @ R {{ v, ∃ cl q w, ⌜ v = cloc_to_val cl ⌝ ∧
cl ↦C{q} w ∗ (cl ↦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 (q w) "[Hl HΦ]". awp_lam.
iIntros (v). iDestruct 1 as ([l i] 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]".
assert ((#l, #i)%V ∉ X).
{ intros Hcl. destruct (HX _ Hcl) as ([??]&[=]%cloc_to_of_val&?); naive_solver. }
iMod (locking_heap_load with "Hσ Hl") as (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.
rewrite bool_decide_false //.
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]".
......@@ -179,12 +189,14 @@ Section proofs.
Qed.
Lemma a_load_spec R Φ q e :
AWP e @ R {{ v, ∃ w, v ↦C{q} w ∗ (v ↦C{q} w -∗ Φ w) }} -∗
AWP e @ R {{ v, ∃ cl w,
⌜ v = cloc_to_val cl ⌝ ∧
cl ↦C{q} w ∗ (cl ↦C{q} w -∗ Φ w) }} -∗
AWP ∗ᶜe @ R {{ Φ }}.
Proof.
iIntros "H". iApply a_load_spec_exists_frac.
awp_apply (awp_wand with "H").
iIntros (v). iDestruct 1 as (w) "[H1 H2]"; eauto with iFrame.
iIntros (v). iDestruct 1 as (cl w ->) "[H1 H2]"; eauto with iFrame.
Qed.
Lemma a_un_op_spec R Φ e op:
......@@ -229,8 +241,7 @@ Section proofs.
Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) :
AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗
▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗
∃ w, ⌜bin_op_eval op v1 v2 = Some w⌝ ∧ Φ w)-∗
▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ w, ⌜bin_op_eval op v1 v2 = Some w⌝ ∧ Φ w) -∗
AWP a_bin_op op e1 e2 @ R {{ Φ }}.
Proof.
iIntros "H1 H2 HΦ".
......@@ -247,9 +258,10 @@ 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 -∗
∃ v w, v1 ↦C v ∗
⌜ bin_op_eval op v v2 = Some w ⌝ ∗
(v1 ↦C[LLvl] w -∗ R ∗ Φ v)) -∗
∃ cl v w, ⌜ v1 = cloc_to_val cl ⌝ ∧
cl ↦C v ∗
⌜ bin_op_eval op v v2 = Some w ⌝ ∗
(cl ↦C[LLvl] w -∗ R ∗ Φ v)) -∗
AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
Proof.
iIntros "He1 He2 HΦ". rewrite /a_pre_bin_op.
......@@ -258,19 +270,20 @@ Section proofs.
iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
iApply awp_atomic. iNext.
iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (v w) "(Hl & % & HΦ)".
iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (cl 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 v; iFrame.
iExists cl, v; iFrame. iSplit; first done.
iIntros "Hl". awp_let. iApply awp_bind.
iApply (a_store_spec _ _
(λ v', ⌜v' = v1⌝)%I (λ v', ⌜v' = w⌝)%I with "[] [] [-]").
(λ v', ⌜v' = cloc_to_val cl⌝)%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);
try (try awp_proj; iApply awp_ret; by wp_value_head).
iNext. iIntros (? ? -> ->). eauto.
- iNext. iIntros (? ? -> ->).
iExists _; iFrame. iIntros "?". awp_seq. iApply awp_ret; wp_value_head.
iExists _, _; iFrame. iSplit; first done.
iIntros "?". awp_seq. iApply awp_ret; wp_value_head.
iIntros "_". by iApply "HΦ".
Qed.
......@@ -407,7 +420,7 @@ Section proofs.
Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
I -∗
□ (I -∗ AWP c @ R {{ v, (⌜v = #false⌝ ∧ U (Φ #())) ∨
(⌜v = #true⌝ ∧ ▷ (AWP b @ R {{ _, U I }})) }}) -∗
(⌜v = #true⌝ ∧ ▷ AWP b @ R {{ _, U I }}) }}) -∗
AWP whileᶜ (c) { b } @ R {{ Φ }}.
Proof.
iIntros "Hi #Hinv". iLöb as "IH".
......
theories/lib/locking_heap.v
View file @ e5406329
......@@ -4,6 +4,7 @@ From iris.base_logic.lib Require Export own.
From iris.proofmode Require Import tactics.
From iris_c.lib Require Import list.
Set Default Proof Using "Type".
Local Open Scope nat_scope.
Inductive lvl :=
| LLvl : lvl
......@@ -56,7 +57,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 cloc : Type := loc * nat.
Instance cloc_eq_dec : EqDecision cloc | 0 := _.
Instance cloc_countable : Countable cloc | 0 := _.
Instance cloc_inhabited : Inhabited cloc | 0 := _.
Definition locking_heapUR : ucmraT :=
gmapUR cloc (prodR (prodR fracR lvlUR) (agreeR valC)).
......@@ -86,15 +90,18 @@ Section definitions.
Definition locked_locs (σ : gmap cloc (lvl * val)) : gset cloc :=
dom _ (filter (λ x, x.2.1 = LLvl) σ).
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)
Definition cloc_add (cl : cloc) (i : nat) : cloc := (cl.1, cl.2 + i).
Definition cloc_to_val (cl : cloc) : val := (#cl.1, #cl.2).
Definition cloc_of_val (v : val) : option cloc :=
match v return option (loc * nat) with
| (LitV (LitLoc l), LitV (LitInt i))%V => guard (0 ≤ i)%Z; 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 ⌝ ∧
⌜ ∀ cl, σ !! cl = τ !! cl.1 ≫= lookup (M:=list _) cl.2 ⌝ ∧
own lheap_name (● (to_locking_heap σ)) ∗
[∗ map] l↦lvvs ∈ τ, ∃ lv, l ↦ lv ∧ ⌜ is_list lv (snd <$> lvvs) ⌝)%I.
......@@ -118,6 +125,13 @@ Notation "cl ↦C{ q } v" := (cl ↦C[ULvl]{q} v)%I
Notation "cl ↦C v" := (cl ↦C[ULvl]{1} v)%I
(at level 20, format "cl ↦C v") : bi_scope.
Notation "cl ↦C{ q }∗ vs" :=
([∗ list] i ↦ v ∈ vs, cloc_add cl i ↦C{q} v)%I
(at level 20, q at level 50, format "cl ↦C{ q }∗ vs") : bi_scope.
Notation "cl ↦C∗ vs" :=
([∗ list] i ↦ v ∈ vs, cloc_add cl i ↦C v)%I
(at level 20, format "cl ↦C∗ vs") : bi_scope.
Lemma to_locking_heap_valid (σ : gmap cloc (lvl * val)) : ✓ to_locking_heap σ.
Proof. intros cl. rewrite lookup_fmap. by destruct (σ !! cl) as [[]|]. Qed.
......@@ -126,9 +140,7 @@ Lemma locking_heap_init `{locking_heapPreG Σ, !heapG Σ} :
Proof.
iMod (own_alloc (● to_locking_heap ∅)) as (γ) "Hh".
{ apply: auth_auth_valid. exact: to_locking_heap_valid. }
iModIntro. iExists (LHeapG Σ _ γ).
iExists ∅. iSplit; last by iFrame.
iIntros "!%" (cl). destruct (cloc_loc_idx cl) as [[]|]; by rewrite /= ?lookup_empty.
iModIntro. iExists (LHeapG Σ _ γ), ∅. auto.
Qed.
Section properties.
......@@ -192,15 +204,15 @@ Section properties.
Lemma mapsto_downgrade lv cl q v : cl ↦C{q} v -∗ cl ↦C[lv]{q} v.
Proof. apply mapsto_downgrade'. by apply lvl_included. Qed.
Lemma cloc_loc_idx_Some_inv cl l i : cloc_loc_idx cl = Some (l, i) → cl = (#l, #i)%V.
Lemma cloc_of_to_val cl : cloc_of_val (cloc_to_val cl) = Some cl.
Proof. destruct cl. by rewrite /= option_guard_True ?Nat2Z.id; last lia. Qed.
Lemma cloc_to_of_val v cl : cloc_of_val v = Some cl → cloc_to_val cl = v.
Proof.
intros. destruct cl; repeat (case_match || simplify_option_eq); auto.
rewrite /cloc_of_val /cloc_to_val=> ?.
destruct cl; repeat (case_match || simplify_option_eq); auto.
by rewrite Z2Nat.inj_pos positive_nat_Z.
Qed.
Lemma cloc_loc_idx_Some l i : cloc_loc_idx (#l, #i) = Some (l, i).
Proof. by rewrite /= option_guard_True ?Nat2Z.id; last lia. Qed.
Lemma to_locking_heap_insert σ cl lv v :
to_locking_heap (<[cl:=(lv,v)]> σ) = <[cl:=(1%Qp, lv, to_agree v)]>(to_locking_heap σ).
Proof. by rewrite /to_locking_heap fmap_insert. Qed.
......@@ -279,18 +291,17 @@ Section properties.
Qed.
Lemma locking_heap_load cl lv q v σ :
full_locking_heap σ -∗ cl ↦C[lv]{q} v ==∗ ∃ l i ll vs,
⌜ cl = (#l, #i)%V ⌝ ∧ ⌜ is_list ll vs ⌝ ∧ ⌜ vs !! i = Some v ⌝ ∗
l ↦ ll ∗ (l ↦ ll -∗ full_locking_heap σ ∗ cl ↦C[lv]{q} v).
full_locking_heap σ -∗ cl ↦C[lv]{q} v ==∗ ∃ ll vs,
⌜ is_list ll vs ⌝ ∧ ⌜ vs !! cl.2 = Some v ⌝ ∗
cl.1 ↦ ll ∗ (cl.1 ↦ ll -∗ full_locking_heap σ ∗ cl ↦C[lv]{q} v).
Proof.
iDestruct 1 as (τ Hτ) "[Hσ Hτ]".
rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl".
iDestruct (own_valid_2 with "Hσ Hl")
as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2.
move: (Hσ); rewrite Hτ=> /bind_Some [[l i] [/cloc_loc_idx_Some_inv ?]].
move=> /bind_Some [lvvs [? Hi]].
move: (Hσ); rewrite Hτ=> /bind_Some [lvvs [? Hi]].
iDestruct (big_sepM_lookup_acc with "Hτ") as "[H Hclose]"; first done.
iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists l, i, ll, lvvs.*2.
iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists ll, lvvs.*2.
repeat iSplit; auto.
{ iPureIntro. by rewrite list_lookup_fmap Hi. }
iIntros "{$Hll} Hll". iDestruct ("Hclose" with "[Hll]") as "Hτ"; eauto.
......@@ -299,20 +310,19 @@ Section properties.
Qed.
Lemma locking_heap_store cl lv v σ :
full_locking_heap σ -∗ cl ↦C[lv] v ==∗ ∃ l i ll vs,
⌜ cl = (#l, #i)%V ⌝ ∧ ⌜ is_list ll vs ⌝ ∧ ⌜ vs !! i = Some v ⌝ ∗
l ↦ ll ∗
(∀ ll' lv' v', ⌜ is_list ll' (<[i:=v']>vs) ⌝ -∗ l ↦ ll' ==∗
full_locking_heap σ -∗ cl ↦C[lv] v ==∗ ∃ ll vs,
⌜ is_list ll vs ⌝ ∧ ⌜ vs !! cl.2 = Some v ⌝ ∗
cl.1 ↦ ll ∗
(∀ ll' lv' v', ⌜ is_list ll' (<[cl.2:=v']>vs) ⌝ -∗ cl.1 ↦ ll' ==∗
full_locking_heap (<[cl:=(lv',v')]>σ) ∗ cl ↦C[lv'] v').
Proof.
iDestruct 1 as (τ Hτ) "[Hσ Hτ]".
rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl".
iDestruct (own_valid_2 with "Hσ Hl")
as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2.
move: (Hσ); rewrite Hτ=> /bind_Some [[l i] [/cloc_loc_idx_Some_inv ?]]; subst.
move=> /bind_Some [lvvs [Hτl Hi]].
move: (Hσ); rewrite Hτ=> /bind_Some [lvvs [Hτl Hi]].
iDestruct (big_sepM_delete with "Hτ") as "[H Hτ]"; first done.
iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists l, i, ll, lvvs.*2.
iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists ll, lvvs.*2.
repeat iSplit; auto.
{ iPureIntro. by rewrite list_lookup_fmap Hi. }
iIntros "{$Hll}" (ll' lv''' v' ?) "Hll".
......@@ -321,59 +331,100 @@ Section properties.
(exclusive_local_update _ (1%Qp, lv''', to_agree v'));
first by apply to_locking_heap_lookup_Some. }
iModIntro. iSplitL "Hσ Hτ Hll"; last auto.
iExists (<[l:=(<[i:=(lv''',v')]> lvvs)]>τ).
rewrite to_locking_heap_insert. iFrame "Hσ"; iSplit.
{ iPureIntro=> cl'. destruct (decide ((#l, #i)%V = cl')) as [<-|?].
{ rewrite cloc_loc_idx_Some /= !lookup_insert /= list_lookup_insert //.
by eapply lookup_lt_Some. }
rewrite lookup_insert_ne // Hτ.
destruct (cloc_loc_idx cl') as [[k j]|] eqn:Hcl'; simpl; last done.
apply cloc_loc_idx_Some_inv in Hcl' as ->. destruct (decide (l = k)) as [->|].
{ rewrite lookup_insert /= list_lookup_insert_ne ?Hτl //. congruence. }
by rewrite lookup_insert_ne. }
iExists (<[cl.1:=(<[cl.2:=(lv''',v')]> lvvs)]>τ).
rewrite to_locking_heap_insert. iFrame "Hσ". iSplit.
{ destruct cl as [l i]; iPureIntro=> -[l' i']; simpl in *.
destruct (decide (l' = l)) as [->|?].
{ destruct (decide (i' = i)) as [->|?].
- rewrite !lookup_insert /= list_lookup_insert //. by eapply lookup_lt_Some.
- rewrite lookup_insert /= list_lookup_insert_ne //.
rewrite lookup_insert_ne; last congruence. by rewrite Hτ Hτl. }
rewrite !lookup_insert_ne; [|congruence..]. by rewrite Hτ. }
rewrite -insert_delete.
iApply (big_sepM_insert with "[$Hτ Hll]"); first by rewrite lookup_delete.
iExists ll'. iFrame. by rewrite list_fmap_insert.
Qed.
(*
Lemma locking_heap_alloc cl lv v σ :
Definition alloc_heap (σ : gmap cloc (lvl * val)) (l : loc) :
list val → nat → gmap cloc (lvl * val) :=
foldr (λ v go i, <[(l,i):=(ULvl,v)]> (go (S i))) (λ _, σ).
Lemma alloc_heap_None σ l vs j1 j2 :
(∀ i, σ !! (l,i) = None) →
j2 < j1 → alloc_heap σ l vs j1 !! (l, j2) = None.
Proof.
intros Hσi. revert j1 j2. induction vs as [|v' vs IH]=> j1 j2 ?; csimpl.
{ by rewrite Hσi. }
rewrite lookup_insert_ne; last (intros [=]; lia).
by rewrite IH; last lia.
Qed.
Lemma alloc_heap_lookup σ l vs i j :
(∀ i, σ !! (l,i) = None) →
alloc_heap σ l vs j !! (l, j + i) = ((ULvl,) <$> vs) !! i.
Proof.
intros Hσi. revert i j. induction vs as [|v vs IH]=> i j; csimpl.
{ by rewrite Hσi. }
destruct i as [|i]; simpl.
{ by rewrite Nat.add_0_r lookup_insert. }
rewrite Nat.add_succ_r lookup_insert_ne; last (intros [=]; lia).
apply (IH i (S j)).
Qed.
Lemma alloc_heap_lookup_ne σ l l' vs i j :
l ≠ l' →
alloc_heap σ l vs j !! (l', i) = σ !! (l', i).
Proof.
intros Hl. revert i j. induction vs as [|v vs IH]=> i j //; csimpl.
by rewrite lookup_insert_ne; last congruence.
Qed.
Lemma locked_locs_alloc_heap σ l vs j :
(∀ i, σ !! (l,i) = None) →
locked_locs (alloc_heap σ l vs j) = locked_locs σ.
Proof.
intros ?. revert j. induction vs as [|v vs IH]=> j //=.
rewrite locked_locs_alloc_unlocked // alloc_heap_None //; lia.
Qed.
Lemma locking_heap_alloc l ll vs σ :
is_list ll vs →
full_locking_heap σ -∗ l ↦ ll ==∗ full_locking_heap σ ∗ ll ↦
(∀ ll' lv' v', ⌜ is_list ll' (<[i:=v']>vs) ⌝ -∗ l ↦ ll' ==∗
full_locking_heap (<[cl:=(lv',v')]>σ) ∗ cl ↦C[lv'] v').
full_locking_heap σ -∗ l ↦ ll ==∗
⌜ ∀ i, σ !! (l,i) = None ⌝ ∧
full_locking_heap (alloc_heap σ l vs O) ∗ (l,0) ↦C∗ vs.
Proof.
iDestruct 1 as (τ Hτ) "[Hσ Hτ]".
rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl".
iDestruct (own_valid_2 with "Hσ Hl")
as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2.
move: (Hσ); rewrite Hτ=> /bind_Some [[l i] [/cloc_loc_idx_Some_inv ?]]; subst.
move=> /bind_Some [lvvs [Hτl Hi]].
iDestruct (big_sepM_delete with "Hτ") as "[H Hτ]"; first done.
iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists l, i, ll, lvvs.*2.
repeat iSplit; auto.
{ iPureIntro. by rewrite list_lookup_fmap Hi. }
iIntros "{$Hll}" (ll' lv''' v' ?) "Hll".
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ by eapply auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, lv''', to_agree v'));
first by apply to_locking_heap_lookup_Some. }
iModIntro. iSplitL "Hσ Hτ Hll"; last auto.
iExists (<[l:=(<[i:=(lv''',v')]> lvvs)]>τ).
rewrite to_locking_heap_insert. iFrame "Hσ"; iSplit.
{ iPureIntro=> cl'. destruct (decide ((#l, #i)%V = cl')) as [<-|?].
{ rewrite cloc_loc_idx_Some /= !lookup_insert /= list_lookup_insert //.
by eapply lookup_lt_Some. }
rewrite lookup_insert_ne // Hτ.
destruct (cloc_loc_idx cl') as [[k j]|] eqn:Hcl'; simpl; last done.
apply cloc_loc_idx_Some_inv in Hcl' as ->. destruct (decide (l = k)) as [->|].
{ rewrite lookup_insert /= list_lookup_insert_ne ?Hτl //. congruence. }
by rewrite lookup_insert_ne. }
rewrite -insert_delete.
iApply (big_sepM_insert with "[$Hτ Hll]"); first by rewrite lookup_delete.
iExists ll'. iFrame. by rewrite list_fmap_insert.
intros Hll. iDestruct 1 as (τ Hτ) "[Hσ Hτ]". iIntros "Hll".
set (f := foldr (λ v go i, <[(l,i):=(ULvl,v)]> (go (S i))) (λ _, σ)).
iAssert ⌜ τ !! l = None ⌝%I as %Hτi.
{ rewrite eq_None_not_Some. iIntros ([lvv ?]).
iDestruct (big_sepM_lookup with "Hτ") as (ll') "[Hll' _]"; first done.
by iDestruct (mapsto_valid_2 with "Hll Hll'") as %[]. }
iAssert ⌜ ∀ i, σ !! (l,i) = None ⌝%I as %Hσi.
{ iIntros (i). by rewrite Hτ Hτi. }
iAssert (|==> own lheap_name (● to_locking_heap (f vs 0)) ∗
[∗ list] i↦v ∈ vs, own lheap_name (◯ {[ (l,0 + i) := (1%Qp, ULvl,to_agree v) ]}))%I
with "[Hσ]" as ">[Hσ Hl]".
{ clear Hll. generalize 0=> j.
iInduction vs as [|v vs] "IH" forall (j); simpl; first by iFrame.
iMod ("IH" $! (S j) with "Hσ") as "[Hσ Hls]".
iMod (own_update with "Hσ") as "[Hσ Hl]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ (l,j) (1%Qp, ULvl, to_agree v)); try done.
apply to_locking_heap_lookup_None. rewrite alloc_heap_None //. lia. }
iModIntro. rewrite -to_locking_heap_insert Nat.add_0_r; iFrame "Hσ Hl".
iApply (big_sepL_impl with "Hls"); iIntros "!>" (k w _) "?".
by rewrite Nat.add_succ_r. }
iModIntro. iSplit; first done. iSplitL "Hσ Hτ Hll".
{ iExists (<[l:=(ULvl,) <$> vs]> τ). iFrame "Hσ". iSplit.
- iPureIntro=> -[l' i] /=. destruct (decide (l' = l)) as [->|].
+ rewrite