Skip to content

GitLab

Commit ead93333 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Use `Z`s for pointer offsets, makes thing more uniform and supports pointer subtraction.

parent a249c071
Hide whitespace changes
Inline Side-by-side
Showing with 126 additions and 118 deletions
_CoqProject
View file @ ead93333
......@@ -21,5 +21,4 @@ theories/tests/swap.v
theories/tests/fact.v
theories/tests/memcpy.v
theories/tests/gcd.v
theories/tests/binop.v
# theories/tests/lists.v
theories/c_translation/translation.v
View file @ ead93333
......@@ -158,12 +158,15 @@ Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 20, right associativity) : ex
Notation "e1 +∗ᶜ e2" := (a_bin_op PtrPlusOp e1%E e2%E) (at level 50) : expr_scope.
Notation "e1 <∗ᶜ e2" := (a_bin_op PtrLtOp e1%E e2%E) (at level 70) : expr_scope.
Definition int_of_val (v : val) : option Z :=
match v with LitV (LitInt x) => Some x | _ => None end.
Definition cbin_op_eval (op : cbin_op) (v1 v2 : val) : option val :=
match op with
| CBinOp op' => bin_op_eval op' v1 v2
| PtrPlusOp =>
cl ← cloc_of_val v1;
o ← offset_of_val v2;
o ← int_of_val v2;
Some (cloc_to_val (cloc_plus cl o))
| PtrLtOp =>
cl1 ← cloc_of_val v1;
......@@ -187,10 +190,11 @@ Section proofs.
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 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ n : Z,
⌜ v1 = #n ⌝ ∧
∀ l, l ↦C∗ replicate n v2 -∗ Φ (cloc_to_val l)) -∗
AWP allocᶜ (e1, e2) @ R {{ Φ }}.
⌜ (0 ≤ n)%Z ⌝ ∧
∀ l, l ↦C∗ replicate (Z.to_nat n) v2 -∗ Φ (cloc_to_val l)) -∗
AWP allocᶜ(e1, e2) @ R {{ Φ }}.
Proof.
iIntros "H1 H2 HΦ".
awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2".
......@@ -198,14 +202,15 @@ Section proofs.
awp_lam. awp_pures.
iApply awp_bind. iApply (awp_par with "H1 H2").
iIntros "!>" (w1 w2) "H1 H2 !>". awp_pures.
iDestruct ("HΦ" with "H1 H2") as (n ->) "HΦ".
iDestruct ("HΦ" with "H1 H2") as (n -> ?) "HΦ".
iApply awp_atomic_env.
iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_pures.
iEval (rewrite -(Z2Nat.id n) //).
wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
wp_alloc l as "Hl".
iMod (full_locking_heap_alloc_upd with "Hσ Hl") as (?) "[Hσ Hl]"; first done.
wp_pures. iIntros "!>". rewrite cloc_to_val_eq.
iSplitL "Hlocks Hσ"; [|by iApply ("HΦ" $! (MkCloc l 0))].
iSplitL "Hlocks Hσ"; [|by iApply ("HΦ" $! (CLoc l 0))].
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.
......@@ -228,6 +233,7 @@ Section proofs.
iApply awp_atomic_env.
iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hw1.
iDestruct (mapsto_offset_non_neg with "Hl") as %?.
assert (cloc_to_val cl ∉ X) as HclX.
{ intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. }
rewrite cloc_to_val_eq in HclX.
......@@ -235,8 +241,9 @@ Section proofs.
wp_pures. rewrite cloc_to_val_eq. wp_pures.
wp_apply (mset_add_spec with "[$]"); first done.
iIntros "Hlocks /="; wp_pures.
wp_load.
wp_apply (linsert_spec with "[//]"); [eauto|]; iIntros (ll' Hl').
wp_load; wp_match.
iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
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Φ".
......@@ -255,6 +262,7 @@ Section proofs.
awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. awp_pures.
iApply awp_bind. iApply (awp_wand with "H"). clear v.
iIntros (v). iDestruct 1 as (cl q w ->) "[Hl HΦ]". awp_pures.
iDestruct (mapsto_offset_non_neg with "Hl") as %?.
iApply awp_atomic_env. iIntros (env) "Henv HR".
iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hv.
......@@ -266,7 +274,9 @@ Section proofs.
wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
rewrite bool_decide_false //.
wp_op. iSplit; first done. iNext; wp_seq.
wp_load; wp_match. wp_apply (llookup_spec with "[//]"); [done|]; iIntros "_".
wp_load; wp_match.
iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
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.
......@@ -389,7 +399,7 @@ Section proofs.
Lemma a_ptr_plus_spec R Φ Ψ2 e1 e2 :
AWP e2 @ R {{ Ψ2 }} -∗
AWP e1 @ R {{ v1, ∀ v2, Ψ2 v2 -∗ ∃ cl (n : nat),
AWP e1 @ R {{ v1, ∀ v2, Ψ2 v2 -∗ ∃ cl (n : Z),
⌜ v1 = cloc_to_val cl ⌝ ∗
⌜ v2 = #n ⌝ ∗
Φ (cloc_to_val (cloc_plus cl n)) }} -∗
......@@ -402,7 +412,7 @@ Section proofs.
iIntros "!>" (v1 v2) "Hv1 Hv2 !>". awp_pures.
iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ /=".
rewrite cloc_to_val_eq.
awp_pures. iApply awp_ret. iApply wp_value. by rewrite -Nat2Z.inj_add.
awp_pures. iApply awp_ret. by iApply wp_value.
Qed.
Lemma a_ptr_lt_spec R Φ Ψ1 e1 e2 :
......@@ -422,8 +432,7 @@ Section proofs.
rewrite cloc_to_val_eq /cloc_lt /=. awp_pures.
case_bool_decide as Hp; subst.
- rewrite (bool_decide_true (#ql = #ql)) //. awp_pures.
iApply awp_ret. iApply wp_value.
rewrite (bool_decide_iff (pi < qi) (pi < qi)%Z); eauto using Nat2Z.inj_lt.
iApply awp_ret. by iApply wp_value.
- rewrite /= bool_decide_false; last congruence.
awp_if. iApply awp_ret. by iApply wp_value.
Qed.
......@@ -446,9 +455,10 @@ Section proofs.
iIntros (v1) "HΨ1"; iIntros (v2) "HΨ2".
iDestruct ("HΦ" with "HΨ1 HΨ2") as (w Hop) "HΦ"; simpl in *.
destruct (cloc_of_val v1) as [cl|] eqn:Hcl; simplify_eq/=.
destruct (offset_of_val v2) as [o|] eqn:Ho; simplify_eq/=.
destruct (int_of_val v2) as [o|] eqn:Ho; simplify_eq/=.
iExists cl,o. iFrame.
rewrite -(cloc_to_of_val v1 cl) // (offset_to_of_val v2 o) //.
rewrite -(cloc_to_of_val v1 cl) //.
by destruct v2; repeat (case_match || simplify_eq/=).
- iApply (a_ptr_lt_spec with "H1").
iApply (awp_wand with "H2").
iIntros (v2) "HΨ2"; iIntros (v1) "HΨ1".
......@@ -468,7 +478,7 @@ Section proofs.
(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.
iIntros "He1 He2 HΦ".
awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2".
awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam; awp_pures.
iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
......
theories/lib/locking_heap.v
View file @ ead93333
......@@ -60,22 +60,25 @@ Canonical Structure lvlUR : ucmraT := UcmraT lvl lvl_ucmra_mixin.
See: https://coq.inria.fr/refman/language/gallina-extensions.html#primitive-record-types
*)
Set Primitive Projections.
Record cloc := MkCloc {
Record cloc := CLoc {
cloc_loc : loc;
cloc_offset : nat
cloc_offset : Z
}.
Unset Primitive Projections.
Add Printing Constructor cloc.
Instance cloc_eq_dec : EqDecision cloc | 0.
Proof. solve_decision. Qed.
Instance cloc_countable : Countable cloc | 0.
Proof.
apply inj_countable' with
(f:=(λ x, (cloc_loc x, cloc_offset x)))
(g:=λ '(l,n), MkCloc l n).
(g:=λ '(l,n), CLoc l n).
reflexivity. (* This line wouldn't work if we were not using primitive projections *)
Qed.
Instance cloc_inhabited : Inhabited cloc | 0 :=
populate (MkCloc inhabitant inhabitant).
Unset Primitive Projections.
populate (CLoc inhabitant inhabitant).
(* Auth (CLoc -> (Q * Level)) *)
Definition locking_heapUR : ucmraT :=
......@@ -109,35 +112,32 @@ Section definitions.
(** Pointer arithmetic *)
Definition cloc_lt (p q : cloc) : bool :=
bool_decide (cloc_loc p = cloc_loc q)
&& bool_decide (cloc_offset p < cloc_offset q)%nat.
Definition cloc_plus (cl : cloc) (i : nat) : cloc :=
MkCloc (cloc_loc cl) (i + cloc_offset cl).
&& bool_decide (cloc_offset p < cloc_offset q)%Z.
Definition cloc_plus (cl : cloc) (i : Z) : cloc :=
CLoc (cloc_loc cl) (i + cloc_offset cl).
Definition cloc_to_val (cl : cloc) : val :=
locked (#(cloc_loc cl), #(cloc_offset cl))%V.
Definition cloc_of_val (v : val) : option cloc :=
match v return option cloc with
| (LitV (LitLoc l), LitV (LitInt i))%V =>
guard (0 ≤ i)%Z;
Some $ MkCloc l (Z.to_nat i)
| _ => None
end.
Definition offset_of_val (v: val) : option nat :=
match v with
| LitV (LitInt i) => guard (0 ≤ i)%Z; Some (Z.to_nat i)
| (LitV (LitLoc l), LitV (LitInt i))%V => Some (CLoc l i)
| _ => None
end.
Definition full_locking_heap (σ : gmap cloc (lvl * val)) :=
(∃ τ : gmap loc (list (lvl * val)),
⌜ ∀ cl, σ !! cl = τ !! (cloc_loc cl)
≫= lookup (M:=list _) (cloc_offset cl) ⌝ ∧
⌜ map_Forall (λ cl _, 0 ≤ cloc_offset cl)%Z σ ∧
∀ cl, (0 ≤ cloc_offset cl)%Z →
σ !! cl =
τ !! (cloc_loc cl)
≫= lookup (M:=list _) (Z.to_nat (cloc_offset cl)) ⌝ ∧
own lheap_name (● (to_locking_heap σ)) ∗
[∗ map] l↦lvvs ∈ τ, ∃ lv, l ↦ SOMEV lv ∧ ⌜ is_list lv (snd <$> lvvs) ⌝)%I.
Definition mapsto_def (cl : cloc) (lv : lvl) (q : frac) (v: val) : iProp Σ :=
(∃ lv',
⌜lv ≼ lv'⌝ ∧
⌜ 0 ≤ cloc_offset cl ⌝%Z ∧
own lheap_name (◯ {[ cl := (q, lv', to_agree v) ]}))%I.
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
......@@ -178,14 +178,17 @@ Section properties.
Implicit Type σ : gmap cloc (lvl * val).
Implicit Type lv : lvl.
Implicit Type l : loc.
Implicit Type i : nat.
Implicit Type cl : cloc.
Lemma mapsto_offset_non_neg cl lv q v :
cl ↦C[lv]{q} v -∗ ⌜ (0 ≤ cloc_offset cl)%Z ⌝.
Proof. rewrite mapsto_eq /mapsto_def. by iDestruct 1 as (lv1 ??) "_". Qed.
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".
iDestruct 1 as (lv1 ??) "Hl1". iDestruct 1 as (lv2 ? _) "Hl2".
iDestruct (own_valid_2 with "Hl1 Hl2") as %Ho%auth_own_valid. iPureIntro.
revert Ho. rewrite /= op_singleton singleton_valid. by intros [_ ?%agree_op_invL'].
Qed.
......@@ -194,7 +197,7 @@ Section properties.
cl ↦C[lv]{q} v -∗ cl ↦C[lv']{q'} v -∗ cl ↦C[lv⋅lv']{q+q'} v.
Proof.
rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (lv1 ?) "Hl1". iDestruct 1 as (lv2 ?) "Hl2".
iDestruct 1 as (lv1 ??) "Hl1". iDestruct 1 as (lv2 ? _) "Hl2".
iExists (lv1 ⋅ lv2). iSplitR.
{ iPureIntro. by apply: cmra_mono. }
iCombine "Hl1 Hl2" as "Hl". rewrite frac_op'. by iFrame.
......@@ -214,7 +217,7 @@ Section properties.
Proof.
intros p q. iSplit.
- rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (lv' ?) "Hl". rewrite -(lvl_idemp lv').
iDestruct 1 as (lv' ??) "Hl". rewrite -(lvl_idemp lv').
iDestruct "Hl" as "[Hl Hl']". iSplitL "Hl"; eauto 10.
- iIntros "[H1 H2]". iDestruct (mapsto_combine with "H1 H2") as "H".
by rewrite lvl_idemp.
......@@ -237,33 +240,20 @@ Section properties.
Lemma cloc_plus_0 cl : cloc_plus cl 0 = cl.
Proof. reflexivity. Qed.
Lemma cloc_plus_plus cl i j : cloc_plus (cloc_plus cl i) j = cloc_plus cl (i + j).
Proof. by rewrite /cloc_plus /= Nat.add_assoc (Nat.add_comm i j). Qed.
Proof. by rewrite /cloc_plus /= Z.add_assoc (Z.add_comm i j). Qed.
Lemma cloc_to_val_eq : cloc_to_val = λ cl, (#(cloc_loc cl), #(cloc_offset cl))%V.
Proof. rewrite /cloc_to_val. by unlock. Qed.
Lemma cloc_of_to_val cl : cloc_of_val (cloc_to_val cl) = Some cl.
Proof.
destruct cl.
by rewrite cloc_to_val_eq /= option_guard_True ?Nat2Z.id; last lia.
Qed.
Proof. destruct cl. by rewrite cloc_to_val_eq. Qed.
Lemma cloc_to_of_val v cl : cloc_of_val v = Some cl → cloc_to_val cl = v.
Proof.
rewrite /cloc_of_val cloc_to_val_eq=> ?.
destruct cl; repeat (case_match || simplify_option_eq); auto.
by rewrite Z2Nat.inj_pos positive_nat_Z.
Qed.
Global Instance cloc_to_val_inj : Inj (=) (=) cloc_to_val.
Proof. intros cl1 cl2 Hcl. apply (inj Some). by rewrite -!cloc_of_to_val Hcl. Qed.
Lemma offset_of_to_val (o : nat) : offset_of_val #o = Some o.
Proof. by rewrite /= option_guard_True ?Nat2Z.id; last lia. Qed.
Lemma offset_to_of_val v (o : nat) : offset_of_val v = Some o → v = #o.
Proof.
rewrite /offset_of_val =>?.
repeat (case_match; simplify_option_eq); eauto.
rewrite Z2Nat.inj_pos positive_nat_Z //.
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.
......@@ -314,7 +304,8 @@ Section properties.
cl ↦C{q} v -∗ full_locking_heap σ -∗ ⌜σ !! cl = Some (ULvl,v)⌝.
Proof.
rewrite mapsto_eq /mapsto_def /full_locking_heap.
iDestruct 1 as ([] []%lvl_included) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]".
iDestruct 1 as ([] []%lvl_included _) "Hl".
iDestruct 1 as (τ Hτ) "[Hfull Hmap]".
iDestruct (own_valid_2 with "Hfull Hl")
as %[[[] [[]%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2; auto.
Qed.
......@@ -334,25 +325,26 @@ Section properties.
cl ↦C[LLvl]{q} v -∗ full_locking_heap σ -∗ ⌜is_Some (σ !! cl)⌝.
Proof.
rewrite mapsto_eq /mapsto_def /full_locking_heap.
iDestruct 1 as (lv _) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]".
iDestruct 1 as (lv _ _) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]".
iDestruct (own_valid_2 with "Hfull Hl")
as %[[y [? ?]]%heap_singleton_included _]%auth_valid_discrete_2; eauto.
Qed.
Lemma full_locking_heap_load_upd cl lv q v σ :
full_locking_heap σ -∗ cl ↦C[lv]{q} v ==∗ ∃ ll vs,
⌜ is_list ll vs ⌝ ∧ ⌜ vs !! (cloc_offset cl) = Some v ⌝ ∗
(cloc_loc cl) ↦ SOMEV ll ∗
((cloc_loc cl) ↦ SOMEV ll -∗ full_locking_heap σ ∗ cl ↦C[lv]{q} v).
⌜ is_list ll vs ⌝ ∧
⌜ vs !! Z.to_nat (cloc_offset cl) = Some v ⌝ ∗
cloc_loc cl ↦ SOMEV ll ∗
(cloc_loc cl ↦ SOMEV 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 1 as (τ [Hnat 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 [lvvs [? Hi]].
move: (Hσ). rewrite Hτ; last by eauto. move=> /bind_Some [lvvs [? Hi]].
iDestruct (big_sepM_lookup_acc with "Hτ") as "[H Hclose]"; first done.
iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists ll, lvvs.*2.
repeat iSplit; auto.
repeat iSplit; eauto.
{ iPureIntro. by rewrite list_lookup_fmap Hi. }
iIntros "{$Hll} Hll". iDestruct ("Hclose" with "[Hll]") as "Hτ"; eauto.
iSplitL "Hσ Hτ"; first (iExists τ; by eauto with iFrame).
......@@ -361,21 +353,22 @@ Section properties.
Lemma full_locking_heap_store_upd cl lv v σ :
full_locking_heap σ -∗ cl ↦C[lv] v ==∗ ∃ ll vs,
⌜ is_list ll vs ⌝ ∧ ⌜ vs !! (cloc_offset cl) = Some v ⌝ ∗
(cloc_loc cl) ↦ SOMEV ll ∗
⌜ is_list ll vs ⌝ ∧
⌜ vs !! Z.to_nat (cloc_offset cl) = Some v ⌝ ∗
cloc_loc cl ↦ SOMEV ll ∗
(∀ ll' lv' v',
⌜ is_list ll' (<[cloc_offset cl:=v']>vs) ⌝ -∗
(cloc_loc cl) ↦ SOMEV ll' ==∗
⌜ is_list ll' (<[Z.to_nat (cloc_offset cl):=v']>vs) ⌝ -∗
cloc_loc cl ↦ SOMEV 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 1 as (τ [Hnat 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 [lvvs [Hτl Hi]].
move: (Hσ). rewrite Hτ; last by eauto. 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 ll, lvvs.*2.
repeat iSplit; auto.
repeat iSplit; eauto.
{ iPureIntro. by rewrite list_lookup_fmap Hi. }
iIntros "{$Hll}" (ll' lv''' v' ?) "Hll".
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
......@@ -383,27 +376,30 @@ 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 (<[cloc_loc cl:=(<[cloc_offset cl:=(lv''',v')]> lvvs)]>τ).
iExists (<[cloc_loc cl:=(<[Z.to_nat (cloc_offset cl):=(lv''',v')]> lvvs)]>τ).
rewrite to_locking_heap_insert. iFrame "Hσ". iSplit.
{ destruct cl as [l i]; iPureIntro=> -[l' i']; simpl in *.
{ iPureIntro. split; [by apply map_Forall_insert_2; eauto|].
destruct cl as [l i]=> -[l' i'] ?; simpl in *.
assert (0 ≤ i)%Z by (by eapply (Hnat (CLoc l i))).
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 /=.
rewrite list_lookup_insert_ne ?Z2Nat.inj_iff //=.
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.
iExists ll'. iFrame. rewrite list_fmap_insert /=. auto.
Qed.
Definition alloc_heap (σ : gmap cloc (lvl * val)) (l : loc) :
list val → nat → gmap cloc (lvl * val) :=
foldr (λ v go i, <[MkCloc l i:=(ULvl,v)]> (go (S i))) (λ _, σ).
foldr (λ v go (i : nat), <[CLoc l i:=(ULvl,v)]> (go (S i))) (λ _, σ).
Lemma alloc_heap_None σ l vs j1 j2 :
(∀ i, σ !! MkCloc l i = None) →
j2 < j1 → alloc_heap σ l vs j1 !! (MkCloc l j2) = None.
(∀ i, σ !! CLoc l i = None) →
j2 < j1 → alloc_heap σ l vs j1 !! (CLoc l j2) = None.
Proof.
intros Hσi. revert j1 j2. induction vs as [|v' vs IH]=> j1 j2 ?; csimpl.
{ by rewrite Hσi. }
......@@ -411,28 +407,29 @@ Section properties.
by rewrite IH; last lia.
Qed.
Lemma alloc_heap_lookup σ l vs i j :
(∀ i, σ !! MkCloc l i = None) →
alloc_heap σ l vs j !! MkCloc l (j + i) = ((ULvl,) <$> vs) !! i.
Lemma alloc_heap_lookup σ l vs (i j : nat) :
(∀ i, σ !! CLoc l i = None) →
alloc_heap σ l vs j !! CLoc 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).
{ by rewrite Z.add_0_r lookup_insert. }
rewrite Nat2Z.inj_succ Z.add_succ_r -Z.add_succ_l -Nat2Z.inj_succ.
rewrite 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 !! MkCloc l' i = σ !! MkCloc l' i.
alloc_heap σ l vs j !! CLoc l' i = σ !! CLoc 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, σ !! MkCloc l i = None) →
(∀ i, σ !! CLoc l i = None) →
locked_locs (alloc_heap σ l vs j) = locked_locs σ.
Proof.
intros ?. revert j. induction vs as [|v vs IH]=> j //=.
......@@ -442,53 +439,57 @@ Section properties.
Lemma full_locking_heap_alloc_upd l ll vs σ :
is_list ll vs →
full_locking_heap σ -∗ l ↦ SOMEV ll ==∗
⌜ ∀ i, σ !! MkCloc l i = None ⌝ ∧
full_locking_heap (alloc_heap σ l vs O) ∗ MkCloc l 0 ↦C∗ vs.
⌜ ∀ i, σ !! CLoc l i = None ⌝ ∧
full_locking_heap (alloc_heap σ l vs O) ∗ CLoc l 0 ↦C∗ vs.
Proof.
intros Hll. iDestruct 1 as (τ Hτ) "[Hσ Hτ]". iIntros "Hll".
set (f := foldr (λ v go i, <[MkCloc l i:=(ULvl,v)]> (go (S i))) (λ _, σ)).
intros Hll. iDestruct 1 as (τ [Hnat Hτ]) "[Hσ Hτ]". iIntros "Hll".
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, σ !! MkCloc 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 (◯ {[ MkCloc l (i+0) := (1%Qp, ULvl,to_agree v) ]}))%I
iAssert ⌜ ∀ i, σ !! CLoc l i = None ⌝%I as %Hσi.
{ iIntros (i) "!%". apply eq_None_not_Some=> -[[lv v] Hi].
move: (Hi). rewrite Hτ; last by eauto. by rewrite Hτi. }
iAssert (|==> own lheap_name (● to_locking_heap (alloc_heap σ l vs 0)) ∗
[∗ list] i↦v ∈ vs, own lheap_name (◯ {[ CLoc l (i+0) := (1%Qp, ULvl,to_agree v) ]}))%I
with "[Hσ]" as ">[Hσ Hl]".
{ clear Hll. generalize 0=> j.
{ clear Hll. change 0%Z with (Z.of_nat 0). 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 _ (MkCloc l j)
(alloc_singleton_local_update _ (CLoc 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 /=. iFrame "Hσ Hl".
iApply (big_sepL_impl with "Hls"); iIntros "!>" (k w _) "?".
by rewrite Nat.add_succ_r. }
by rewrite Nat2Z.inj_succ Z.add_succ_r -Z.add_succ_l -Nat2Z.inj_succ. }
iModIntro. iSplit; first done. iSplitL "Hσ Hτ Hll".
{ iExists (<[l:=(ULvl,) <$> vs]> τ). iFrame "Hσ". iSplit.
- iPureIntro=> -[l' i] /=. destruct (decide (l' = l)) as [->|].
+ rewrite lookup_insert /=. by apply (alloc_heap_lookup _ _ _ _ 0).
- iPureIntro. split.
{ clear -Hnat. generalize 0. induction vs as [|v vs IH]=> j //=.
apply map_Forall_insert_2; simpl; eauto with lia. }
move=> -[l' i] /= ? . destruct (decide (l' = l)) as [->|].
+ rewrite lookup_insert /=. rewrite -{1}(Z2Nat.id i) //.
by apply (alloc_heap_lookup _ _ _ _ 0).
+ by rewrite lookup_insert_ne //= alloc_heap_lookup_ne // Hτ.
- iApply (big_sepM_insert with "[$Hτ Hll]"); first done.
iExists _. iFrame "Hll".
by rewrite -list_fmap_compose (list_fmap_ext _ id _ vs) ?list_fmap_id. }
iApply (big_sepL_impl with "Hl"); iIntros "!>" (i v _) "Hl".
rewrite mapsto_eq /mapsto_def. eauto.
rewrite mapsto_eq /mapsto_def /=. eauto 10 with lia.
Qed.
Lemma full_locking_heap_unlock cl v lv q σ :
full_locking_heap σ -∗ cl ↦C[lv]{q} v ==∗
full_locking_heap (<[cl:=(ULvl,v)]>σ) ∗ cl ↦C{q} v.
Proof.
iDestruct 1 as (τ Hτ) "[Hσ Hτ]".
rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl".
iDestruct 1 as (τ [Hnat 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 [lvvs [Hτl Hi]].
move: (Hσ); rewrite Hτ; last by eauto. move=> /bind_Some [lvvs [Hτl Hi]].
iDestruct (big_sepM_delete with "Hτ") as "[H Hτ]"; first done.
iDestruct "H" as (ll) "[Hll %]".
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
......@@ -497,14 +498,17 @@ Section properties.
first by apply to_locking_heap_lookup_Some.
intros h Hh. fold_leibniz. intros ->. split; eauto. }
iModIntro. iSplitR "Hl"; last by eauto with iFrame.
iExists (<[cloc_loc cl:=(<[cloc_offset cl:=(ULvl,v)]> lvvs)]>τ).
iExists (<[cloc_loc cl:=(<[Z.to_nat (cloc_offset cl):=(ULvl,v)]> lvvs)]>τ).