Commit e05af4c4 authored by Robbert Krebbers's avatar Robbert Krebbers

Many changes.

- Better representation of symbolic integers
- Better representation of symbolic locations
- Support while in the vcg
- Support alloc in the vcg
- A better reification mechanism
- Better proofmode support for mapsto with lists
- Normalize fractions
- Restructure lots of proofs
- ...
parent 02d768f0
......@@ -7,6 +7,7 @@ theories/lib/spin_lock.v
theories/lib/flock.v
theories/lib/locking_heap.v
theories/lib/U.v
theories/lib/Q.v
theories/c_translation/monad.v
theories/c_translation/proofmode.v
theories/c_translation/translation.v
......@@ -14,6 +15,7 @@ theories/vcgen/dcexpr.v
theories/vcgen/denv.v
theories/vcgen/vcgen.v
theories/vcgen/proofmode.v
theories/vcgen/reification.v
theories/tests/basics.v
theories/tests/invoke.v
theories/tests/unknowns.v
......
......@@ -7,5 +7,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris-c-monad"]
depends: [
"coq-iris" { (= "dev.2018-11-08.2.9eee9408") | (= "dev") }
"coq-iris" { (= "dev.2018-11-09.0.87ef9033") | (= "dev") }
]
......@@ -11,6 +11,7 @@ Definition a_alloc : val := λ: "x1" "x2",
"vv" ←ᶜ "x1" ||| "x2" ;;
let: "n" := Fst "vv" in
let: "v" := Snd "vv" in
assert: (#0 < "n");;
a_atomic_env (λ: <>, SOME (ref (SOME (lreplicate "n" "v")), #0)).
Notation "'allocᶜ' ( e1 , e2 )" := (a_alloc e1%E e2%E) (at level 80) : expr_scope.
......@@ -117,7 +118,7 @@ Notation "'whileᶜ' ( e1 ) { e2 }" := (a_while (λ: <>, e1)%E (λ: <>, e2)%E)
format "'whileᶜ' ( e1 ) { e2 }") : expr_scope.
(* A version of while with value lambdas, this is an artifact because of the way
heap_lang works in Coq *)
Notation "'whileVᶜ' ( e1 ) { e2 }" := (a_while (λ: <>, e1)%V (λ: <>, e2)%V)
Notation "'whileVᶜ' ( e1 ) { e2 }" := (a_while (LamV <> e1)%V (LamV <> e2)%V)
(at level 200, e1, e2 at level 200,
format "'whileVᶜ' ( e1 ) { e2 }") : expr_scope.
......@@ -188,7 +189,7 @@ Definition cbin_op_eval (op : cbin_op) (v1 v2 : val) : option val :=
| PtrPlusOp =>
cl cloc_of_val v1;
o int_of_val v2;
Some (cloc_to_val (cloc_plus cl o))
Some (cloc_to_val (cl + o))
| PtrLtOp =>
cl1 cloc_of_val v1;
cl2 cloc_of_val v2;
......@@ -211,10 +212,9 @@ 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 : Z,
v1 = #n
(0 n)%Z
l, l C replicate (Z.to_nat n) v2 - Φ (cloc_to_val l)) -
( v1 v2, Ψ1 v1 - Ψ2 v2 - n : nat,
v1 = #n n 0%nat
l, l C replicate n v2 - Φ (cloc_to_val l)) -
AWP alloc(e1, e2) @ R {{ Φ }}.
Proof.
iIntros "H1 H2 HΦ".
......@@ -224,17 +224,19 @@ Section proofs.
iApply awp_bind. iApply (awp_par with "H1 H2").
iIntros "!>" (w1 w2) "H1 H2 !>". awp_pures.
iDestruct ("HΦ" with "H1 H2") as (n -> ?) "HΦ".
awp_apply wp_assert. wp_op. rewrite bool_decide_true; last lia.
iSplit; first done. iNext. awp_pures.
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Φ" $! (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.
iSplitL "Hlocks 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.
- by iApply ("HΦ" $! (CLoc l 0)).
Qed.
Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
......@@ -255,7 +257,7 @@ Section proofs.
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_loc cl), #(cloc_offset cl))%V X) as HclX.
assert ((#(cloc_base cl), #(cloc_offset cl))%V X) as HclX.
{ intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. }
iMod (full_locking_heap_store_upd with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
wp_pures. rewrite cloc_to_val_eq. wp_pures.
......@@ -267,7 +269,7 @@ Section proofs.
iApply wp_fupd. wp_store.
iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
iIntros "!> !> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ".
iExists ({[(#(cloc_loc cl), #(cloc_offset cl))%V]} X), _.
iExists ({[(#(cloc_base cl), #(cloc_offset cl))%V]} X), _.
iFrame "Hσ Hlocks". iPureIntro. rewrite locked_locs_lock. set_solver.
Qed.
......@@ -284,7 +286,7 @@ Section proofs.
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.
assert ((#(cloc_loc cl), #(cloc_offset cl))%V X) as HclX.
assert ((#(cloc_base cl), #(cloc_offset cl))%V X) as HclX.
{ intros Hcl. destruct (HX _ Hcl) as (?&[=]%cloc_to_of_val&?); naive_solver. }
iMod (full_locking_heap_load_upd with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
wp_pures. rewrite cloc_to_val_eq. wp_pures.
......@@ -334,7 +336,7 @@ Section proofs.
Qed.
Lemma a_seq_bind_spec R Φ x e1 e2 :
AWP e1 @ R {{ v, U (AWP subst x v e2 @ R {{ Φ }}) }} -
AWP e1 @ R {{ v, U (AWP subst' x v e2 @ R {{ Φ }}) }} -
AWP x ←ᶜ e1 ; e2 @ R {{ Φ }}.
Proof.
iIntros "H". awp_pures. iApply a_seq_bind_spec'.
......@@ -355,7 +357,7 @@ Section proofs.
Lemma a_while_spec R Φ c e :
AWP whileV (c) { e } @ R {{ Φ }} -
AWP while (c) { e } @ R {{ Φ }}.
Proof. iIntros "H". awp_pures. by rewrite -!lock. Qed.
Proof. iIntros "H". by awp_pures. Qed.
Lemma a_whileV_spec R Φ c e :
(* The later is crucial for Löb induction *)
......@@ -368,9 +370,8 @@ Section proofs.
awp_apply (a_wp_awp with "H"). iIntros (v) "H". awp_lam. awp_pures.
iApply a_seq_bind_spec'. iApply (awp_wand with "H").
iIntros (v') "[[-> H] | [-> H]] !>".
- awp_pures. iApply a_seq_bind_spec'. awp_lam.
iApply (awp_wand with "H").
iIntros (w) "H !>". by awp_lam.
- awp_pures. iApply a_seq_bind_spec'.
iApply (awp_wand with "H"); iIntros (w) "H !>". by awp_lam.
- awp_pures. iApply awp_ret. by iApply wp_value.
Qed.
......@@ -388,7 +389,7 @@ Section proofs.
iApply (awp_wand with "H"); iIntros (_) "HI !>". by iApply "IH".
Qed.
Lemma a_invoke_spec R Ψ Φ (f : val) ea :
Lemma a_call_spec R Ψ Φ (f : val) ea :
AWP ea @ R {{ Ψ }} -
( a, Ψ a - U (R - R', R' (AWP f a @ R' {{ v, R' - R Φ v }}))) -
AWP call (f, ea) @ R {{ Φ }}.
......@@ -419,7 +420,7 @@ Section proofs.
AWP e1 @ R {{ v1, v2, Ψ2 v2 - cl (n : Z),
v1 = cloc_to_val cl
v2 = #n
Φ (cloc_to_val (cloc_plus cl n)) }} -
Φ (cloc_to_val (cl + n)) }} -
AWP a_ptr_plus e1 e2 @ R {{ Φ }}.
Proof.
iIntros "He2 HΦ".
......@@ -488,11 +489,11 @@ 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 -
( v1 v2, Ψ1 v1 - Ψ2 v2 -
cl v w, v1 = cloc_to_val cl
cl C v
cbin_op_eval op v v2 = Some w
(cl C[LLvl] w - R Φ v)) -
(cl C[LLvl] w - Φ v)) -
AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
Proof.
iIntros "He1 He2 HΦ".
......@@ -501,8 +502,8 @@ Section proofs.
iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
iIntros (v1 v2) "Hv1 Hv2 !>". awp_pures.
iApply awp_atomic.
iIntros "!> R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (cl v w ->) "(Hl & % & HΦ)".
simplify_eq/=. iExists True%I. rewrite left_id. awp_pures.
iIntros "!> HR". iDestruct ("HΦ" with "Hv1 Hv2") as (cl v w ->) "(Hl & % & HΦ)".
simplify_eq/=. iExists True%I. iSplit; first done. awp_pures.
iApply awp_bind. iApply a_load_spec. iApply awp_ret. iApply wp_value.
iExists cl, v; iFrame. iSplit; first done.
iIntros "Hl". awp_pures. iApply awp_bind.
......@@ -515,7 +516,7 @@ Section proofs.
- iIntros (? ? -> ->).
iExists _, _; iFrame. iSplit; first done.
iIntros "?". awp_seq. iApply awp_ret; iApply wp_value.
iIntros "_". by iApply "HΦ".
iIntros "_". iFrame "HR". by iApply "HΦ".
Qed.
End proofs.
......
From iris.algebra Require Export frac.
From Coq Require Export QArith Qcanon.
Lemma Q_plus_nonneg p q : (0 < p)%Q (0 < q)%Q (0 < p + q)%Q.
Proof.
intros. apply Qlt_trans with p=> //. by rewrite -{1}(Qplus_0_r p) Qplus_lt_r.
Qed.
Lemma Q_div_nonneg p n : (0 < p)%Q (0 < p / Zpos n)%Q.
Proof. intros. by apply Qlt_shift_div_l. Qed.
Instance Q_eq_dec : EqDecision Q.
Proof. solve_decision. Defined.
Instance Q_Qeq_dec : RelDecision Qeq.
Proof. intros pq; apply Qeq_dec. Defined.
Instance Q_lt_dec : RelDecision Qlt.
Proof. refine (λ p q, cast_if (Qlt_le_dec p q)); auto using Qle_not_lt. Defined.
Fixpoint Pos_to_pred_nat (p : positive) : nat :=
match p with
| xH => 0
| xO p => S (2 * Pos_to_pred_nat p)
| xI p => S (S (2 * Pos_to_pred_nat p))
end.
Definition Q_to_Qp (q : Q) : Qp :=
match Qred q with
| Qmake (Zpos n) 1 => Nat.iter (Pos_to_pred_nat n) (λ n, 1 + n) 1
| Qmake (Zpos n) d => Nat.iter (Pos_to_pred_nat n) (λ n, 1 + n) 1 / d
| _ => 1 (* dummy *)
end%Qp.
Arguments Q_to_Qp !_ /.
Arguments Pos.mul !_ !_ /.
Local Arguments Q_to_Qp : simpl never.
Lemma Q_to_Qp_le_0 q : ¬(0 < q)%Q Q_to_Qp q = 1%Qp.
Proof.
destruct q as [[|n|n] d]=> //=.
rewrite /Q_to_Qp /Qred /=. by destruct (Pos.ggcd _ _) as [? [??]].
Qed.
Lemma Q_to_Qp_1 : Q_to_Qp 1 = 1%Qp.
Proof. done. Qed.
Lemma Pos_to_pred_Q_spec p :
Nat.iter (Pos_to_pred_nat p) (λ n, 1 + n)%Qp 1%Qp == Qmake (Z.pos p) 1.
Proof.
cut ( q,
Nat.iter (Pos_to_pred_nat p) (λ n, 1 + n)%Qp q == Qmake (Z.pos p) 1 + q - 1).
{ intros ->. rewrite /Qeq /=; lia. }
induction p as [p IH|p IH|]=> q' //=.
- rewrite !Qred_correct !Nat_iter_add !IH /=. rewrite /Qeq /=; lia.
- rewrite !Qred_correct !Nat_iter_add !IH /=. rewrite /Qeq /=; lia.
- rewrite /Qeq /=; lia.
Qed.
(* this (Qp_car (Q_to_Qp q)) : Q) == q *)
Lemma Q_of_to_Qp (q : Q) : (0 < q)%Q (Q_to_Qp q : Q) == q.
Proof.
rewrite -{1 3}(Qred_correct q) /Q_to_Qp.
destruct (Qred q) as [[|n|n] d]=> ? //=.
destruct d as [d|d|]=> //=.
- by rewrite Pos_to_pred_Q_spec !Qred_correct /Qeq /= Z.mul_1_r.
- by rewrite Pos_to_pred_Q_spec !Qred_correct /Qeq /= Z.mul_1_r.
- by rewrite Pos_to_pred_Q_spec.
Qed.
(* Q_to_Qp (this (Qp_car q) : Q) = q *)
Lemma Q_to_of_Qp (q : Qp) : Q_to_Qp (q : Q) = q.
Proof. apply Qp_eq, Qc_is_canon. destruct q as [n d]. by rewrite Q_of_to_Qp. Qed.
Instance Q_to_Qp_proper : Proper (Qeq ==> (=)) Q_to_Qp.
Proof. rewrite /Q_to_Qp. by intros p p' ->%Qred_complete. Qed.
Lemma Q_to_Qp_plus p q :
(0 < p)%Q (0 < q)%Q Q_to_Qp (p + q) = (Q_to_Qp p + Q_to_Qp q)%Qp.
Proof.
intros. assert (0 < p + q)%Q by eauto using Q_plus_nonneg.
apply Qp_eq, Qc_is_canon. by rewrite /= Qred_correct !Q_of_to_Qp.
Qed.
Lemma Q_to_Qp_div q p :
(0 < q)%Q Q_to_Qp (q / Zpos p) = (Q_to_Qp q / p)%Qp.
Proof.
intros. assert (0 < q / Z.pos p)%Q by eauto using Q_div_nonneg.
apply Qp_eq, Qc_is_canon. by rewrite /= !Qred_correct !Q_of_to_Qp.
Qed.
......@@ -64,9 +64,9 @@ Section U.
Proof. rewrite /IntoUnlock. reflexivity. Qed.
Global Instance into_unlock_id P : IntoUnlock P P | 10.
Proof. apply U_intro. Qed.
Global Instance into_unlock_unlock l q v :
IntoUnlock (l C[LLvl]{q} v)%I (l C{q} v)%I | 0.
Proof. apply U_unlock. Qed.
Global Instance into_unlock_unlock l q v x :
IntoUnlock (l C[x]{q} v)%I (l C{q} v)%I | 0.
Proof. destruct x. apply U_unlock. apply U_intro. Qed.
Lemma modality_U_mixin :
modality_mixin U MIEnvId (MIEnvTransform IntoUnlock).
......
......@@ -20,6 +20,7 @@ Instance lvl_op : Op lvl := λ lv1 lv2,
| _,ULvl => ULvl
| _,_ => LLvl
end.
Arguments lvl_op !_ !_ /.
Instance lvl_valid : Valid lvl := λ _, True.
Instance lvl_unit : Unit lvl := LLvl.
Instance lvl_pcore : PCore lvl := λ _, Some LLvl.
......@@ -61,7 +62,7 @@ See: https://coq.inria.fr/refman/language/gallina-extensions.html#primitive-reco
*)
Set Primitive Projections.
Record cloc := CLoc {
cloc_loc : loc;
cloc_base : loc;
cloc_offset : Z
}.
Unset Primitive Projections.
......@@ -72,14 +73,13 @@ Proof. solve_decision. Qed.
Instance cloc_countable : Countable cloc | 0.
Proof.
apply inj_countable' with
(f:=(λ x, (cloc_loc x, cloc_offset x)))
(f:=(λ x, (cloc_base x, cloc_offset x)))
(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 (CLoc inhabitant inhabitant).
(* Auth (CLoc -> (Q * Level)) *)
Definition locking_heapUR : ucmraT :=
gmapUR cloc (prodR (prodR fracR lvlUR) (agreeR valC)).
......@@ -111,13 +111,14 @@ Section definitions.
(** Pointer arithmetic *)
Definition cloc_lt (p q : cloc) : bool :=
bool_decide (cloc_loc p = cloc_loc q)
bool_decide (cloc_base p = cloc_base q)
&& 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).
CLoc (cloc_base cl) (i + cloc_offset cl).
Definition cloc_to_val (cl : cloc) : val :=
locked (SOMEV (#(cloc_loc cl), #(cloc_offset cl)))%V.
locked (SOMEV (#(cloc_base cl), #(cloc_offset cl)))%V.
Definition cloc_of_val (v : val) : option cloc :=
match v return option cloc with
| SOMEV (LitV (LitLoc l), LitV (LitInt i))%V => Some (CLoc l i)
......@@ -129,7 +130,7 @@ Section definitions.
map_Forall (λ cl _, 0 cloc_offset cl)%Z σ
cl, (0 cloc_offset cl)%Z
σ !! cl =
τ !! (cloc_loc cl)
τ !! (cloc_base cl)
= lookup (M:=list _) (Z.to_nat (cloc_offset cl))
own lheap_name ( (to_locking_heap σ))
[ map] llvvs τ, lv, l SOMEV lv is_list lv (snd <$> lvvs) )%I.
......@@ -143,8 +144,15 @@ Section definitions.
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
Definition mapsto := unseal mapsto_aux.
Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
Definition mapsto_list (cl : cloc) (q : frac) (vs : list val) : iProp Σ :=
([ list] i v vs, mapsto (cloc_plus cl i) ULvl q v)%I.
End definitions.
Typeclasses Opaque mapsto_list.
Infix "+∗" := (cloc_plus) (at level 50) : stdpp_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.
......@@ -156,10 +164,10 @@ 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_plus cl i C{q} v)%I
(mapsto_list cl q vs)%I
(at level 20, q at level 50, format "cl ↦C{ q }∗ vs") : bi_scope.
Notation "cl ↦C∗ vs" :=
([ list] i v vs, cloc_plus cl i C v)%I
(mapsto_list cl 1 vs)%I
(at level 20, format "cl ↦C∗ vs") : bi_scope.
Lemma to_locking_heap_valid (σ : gmap cloc (lvl * val)) : to_locking_heap σ.
......@@ -174,7 +182,7 @@ Proof.
Qed.
Section properties.
Context `{hG : locking_heapG Σ, !heapG Σ}.
Context `{locking_heapG Σ, !heapG Σ}.
Implicit Type σ : gmap cloc (lvl * val).
Implicit Type lv : lvl.
Implicit Type l : loc.
......@@ -212,7 +220,6 @@ Section properties.
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.
......@@ -222,11 +229,13 @@ Section properties.
- iIntros "[H1 H2]". iDestruct (mapsto_combine with "H1 H2") as "H".
by rewrite lvl_idemp.
Qed.
Global Instance mapsto_as_fractional cl q lv v :
AsFractional (cl C[lv]{q} v) (λ q, cl C[lv]{q} v)%I q.
Proof. split. done. apply _. Qed.
Global Instance mapsto_list_timeless cl q vs : Timeless (cl C{q} vs).
Proof. rewrite /mapsto_list; apply _. Qed.
Lemma mapsto_downgrade' lv lv' cl q v :
lv lv' cl C[lv']{q} v - cl C[lv]{q} v.
Proof.
......@@ -237,12 +246,28 @@ 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_plus_0 cl : cloc_plus cl 0 = cl.
Lemma cloc_plus_0 cl : 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).
Lemma cloc_plus_plus cl i j : (cl + i) + j = cl + (i + j).
Proof. by rewrite /cloc_plus /= Z.add_assoc (Z.add_comm i j). Qed.
Global Instance cloc_plus_inj cl : Inj (=) (=) (cloc_plus cl).
Proof. intros i j [=]; lia. Qed.
Lemma mapsto_list_nil cl q : cl C{q} [] True.
Proof. done. Qed.
Lemma mapsto_list_singleton cl q v : cl C{q} [v] cl C{q} v.
Proof. by rewrite /mapsto_list big_sepL_singleton. Qed.
Lemma mapsto_list_app cl q vs1 vs2 :
cl C{q} (vs1 ++ vs2) cl C{q} vs1 (cl + length vs1) C{q} vs2.
Proof.
rewrite /mapsto_list /= big_sepL_app.
by setoid_rewrite cloc_plus_plus; setoid_rewrite Nat2Z.inj_add.
Qed.
Lemma mapsto_list_cons cl q v vs :
cl C{q} (v :: vs) cl C{q} v (cl + 1) C{q} vs.
Proof. by rewrite (mapsto_list_app _ _ [_]) mapsto_list_singleton. Qed.
Lemma cloc_to_val_eq : cloc_to_val = λ cl, SOMEV (#(cloc_loc cl), #(cloc_offset cl))%V.
Lemma cloc_to_val_eq : cloc_to_val = λ cl, SOMEV (#(cloc_base 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. Qed.
......@@ -334,8 +359,8 @@ Section properties.
full_locking_heap σ - cl C[lv]{q} v == ll vs,
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).
cloc_base cl SOMEV ll
(cloc_base cl SOMEV ll - full_locking_heap σ cl C[lv]{q} v).
Proof.
iDestruct 1 as (τ [Hnat Hτ]) "[Hσ Hτ]".
rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ??) "Hl".
......@@ -355,10 +380,10 @@ Section properties.
full_locking_heap σ - cl C[lv] v == ll vs,
is_list ll vs
vs !! Z.to_nat (cloc_offset cl) = Some v
cloc_loc cl SOMEV ll
cloc_base cl SOMEV ll
( ll' lv' v',
is_list ll' (<[Z.to_nat (cloc_offset cl):=v']>vs) -
cloc_loc cl SOMEV ll' ==
cloc_base cl SOMEV ll' ==
full_locking_heap (<[cl:=(lv',v')]>σ) cl C[lv'] v').
Proof.
iDestruct 1 as (τ [Hnat Hτ]) "[Hσ Hτ]".
......@@ -376,7 +401,7 @@ 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:=(<[Z.to_nat (cloc_offset cl):=(lv''',v')]> lvvs)]>τ).
iExists (<[cloc_base cl:=(<[Z.to_nat (cloc_offset cl):=(lv''',v')]> lvvs)]>τ).
rewrite to_locking_heap_insert. iFrame "Hσ". iSplit.
{ iPureIntro. split; [by apply map_Forall_insert_2; eauto|].
destruct cl as [l i]=> -[l' i'] ?; simpl in *.
......@@ -477,6 +502,7 @@ Section properties.
- 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. }
rewrite /mapsto_list.
iApply (big_sepL_impl with "Hl"); iIntros "!>" (i v _) "Hl".
rewrite mapsto_eq /mapsto_def /=. eauto 10 with lia.
Qed.
......@@ -498,7 +524,7 @@ 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:=(<[Z.to_nat (cloc_offset cl):=(ULvl,v)]> lvvs)]>τ).
iExists (<[cloc_base cl:=(<[Z.to_nat (cloc_offset cl):=(ULvl,v)]> lvvs)]>τ).
rewrite to_locking_heap_insert. iFrame "Hσ". iSplit.
{ iPureIntro. split; [by apply map_Forall_insert_2; eauto|].
destruct cl as [l i]=> -[l' i'] ?; simpl in *.
......@@ -516,3 +542,41 @@ Section properties.
by rewrite list_fmap_insert /= list_insert_id ?list_lookup_fmap ?Hi.
Qed.
End properties.
Section proofmode.
Context `{locking_heapG Σ, !heapG Σ}.
Global Instance into_pure_mapsto_nil cl q : IntoPure (cl C{q} []) True.
Proof. done. Qed.
Global Instance from_pure_mapsto_nil a cl q : FromPure a (cl C{q} []) True | 100.
Proof. by rewrite /FromPure bi.affinely_if_elim. Qed.
Global Instance into_sep_mapsto_list_cons cl q vs v vs' :
IsCons vs v vs'
IntoSep (cl C{q} vs) (cl C{q} v) ((cl + 1) C{q} vs').
Proof. rewrite /IsCons=> ->. by rewrite /IntoSep mapsto_list_cons. Qed.
Global Instance into_sep_mapsto_list_app cl q vs vs1 vs2 :
IsApp vs vs1 vs2
IntoSep (cl C{q} vs) (cl C{q} vs1) ((cl + length vs1) C{q} vs2).
Proof. rewrite /IsApp=> ->. by rewrite /IntoSep mapsto_list_app. Qed.
Global Instance from_sep_mapsto_list_cons cl q vs v vs' :
IsCons vs v vs'
FromSep (cl C{q} vs) (cl C{q} v) ((cl + 1) C{q} vs').
Proof. rewrite /IsCons=> ->. by rewrite /FromSep mapsto_list_cons. Qed.
Global Instance from_sep_mapsto_list_app cl q vs vs1 vs2 :
IsApp vs vs1 vs2
FromSep (cl C{q} vs) (cl C{q} vs1) ((cl + length vs1) C{q} vs2).
Proof. rewrite /IsApp=> ->. by rewrite /FromSep mapsto_list_app. Qed.
Global Instance frame_big_sepL_cons p R Q cl q vs v vs' :
IsCons vs v vs'
Frame p R (cl C{q} v (cl + 1) C{q} vs') Q
Frame p R (cl C{q} vs) Q.
Proof. rewrite /IsCons=>->. by rewrite /Frame mapsto_list_cons. Qed.
Global Instance frame_big_sepL_app p R Q cl q vs vs1 vs2 :
IsApp vs vs1 vs2
Frame p R (cl C{q} vs1 (cl + length vs1) C{q} vs2) Q
Frame p R (cl C{q} vs) Q.
Proof. rewrite /IsApp=>->. by rewrite /Frame mapsto_list_app. Qed.
End proofmode.
......@@ -5,50 +5,35 @@ Section test.
Context `{amonadG Σ}.
(** dereferencing *)