Commit 0fc880d8 authored by Dan Frumin's avatar Dan Frumin

Make `cloc` a primitive record.

This way we get eta-equality definitionally, and `cloc_plus l 0`
simplifies to `l`.
parent 45e74acc
...@@ -193,7 +193,7 @@ Section proofs. ...@@ -193,7 +193,7 @@ Section proofs.
iApply wp_fupd. wp_alloc l as "Hl". iApply wp_fupd. wp_alloc l as "Hl".
iMod (locking_heap_alloc with "Hσ Hl") as (?) "[Hσ Hl]"; first done. iMod (locking_heap_alloc with "Hσ Hl") as (?) "[Hσ Hl]"; first done.
iIntros "!> !>". rewrite cloc_to_val_eq. iIntros "!> !>". rewrite cloc_to_val_eq.
iSplitL "Hlocks Hσ"; [|by iApply ("HΦ" $! (l, 0%nat))]. iSplitL "Hlocks Hσ"; [|by iApply ("HΦ" $! (MkCloc l 0))].
iExists X, _. iFrame. iExists X, _. iFrame.
iIntros "!%". intros w Hw. destruct (HX _ Hw) as (cl&Hcl&Hin). iIntros "!%". intros w Hw. destruct (HX _ Hw) as (cl&Hcl&Hin).
exists cl; split; first done. by rewrite locked_locs_alloc_heap. exists cl; split; first done. by rewrite locked_locs_alloc_heap.
...@@ -428,7 +428,7 @@ Section proofs. ...@@ -428,7 +428,7 @@ Section proofs.
iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ /=". iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ /=".
rewrite cloc_to_val_eq. rewrite cloc_to_val_eq.
do 3 awp_proj. awp_op. awp_let. do 2 awp_proj. do 3 awp_proj. awp_op. awp_let. do 2 awp_proj.
iApply awp_ret. iApply wp_value. by rewrite -Nat2Z.inj_add. iApply awp_ret. iApply wp_value. by rewrite Nat.add_comm -Nat2Z.inj_add.
Qed. Qed.
Lemma a_ptr_lt_spec R Φ Ψ1 e1 e2 : Lemma a_ptr_lt_spec R Φ Ψ1 e1 e2 :
......
...@@ -56,12 +56,28 @@ Lemma lvl_ucmra_mixin : UcmraMixin lvl. ...@@ -56,12 +56,28 @@ Lemma lvl_ucmra_mixin : UcmraMixin lvl.
Proof. split; try (apply _ || done). by intros []. Qed. Proof. split; try (apply _ || done). by intros []. Qed.
Canonical Structure lvlUR : ucmraT := UcmraT lvl lvl_ucmra_mixin. Canonical Structure lvlUR : ucmraT := UcmraT lvl lvl_ucmra_mixin.
(* Auth (Loc -> (Q * Level)) *) (** Here we use a Primitive Record to get an eta-rule for cloc
Definition cloc : Type := loc * nat. See: https://coq.inria.fr/refman/language/gallina-extensions.html#primitive-record-types
Instance cloc_eq_dec : EqDecision cloc | 0 := _. *)
Instance cloc_countable : Countable cloc | 0 := _. Set Primitive Projections.
Instance cloc_inhabited : Inhabited cloc | 0 := _. Record cloc := MkCloc {
cloc_loc : loc;
cloc_offset : nat
}.
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).
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.
(* Auth (CLoc -> (Q * Level)) *)
Definition locking_heapUR : ucmraT := Definition locking_heapUR : ucmraT :=
gmapUR cloc (prodR (prodR fracR lvlUR) (agreeR valC)). gmapUR cloc (prodR (prodR fracR lvlUR) (agreeR valC)).
...@@ -92,13 +108,18 @@ Section definitions. ...@@ -92,13 +108,18 @@ Section definitions.
(** Pointer arithmetic *) (** Pointer arithmetic *)
Definition cloc_lt (p q : cloc) : bool := Definition cloc_lt (p q : cloc) : bool :=
bool_decide (p.1 = q.1) && bool_decide (p.2 < q.2)%nat. bool_decide (cloc_loc p = cloc_loc q)
Definition cloc_plus (cl : cloc) (i : nat) : cloc := (cl.1, cl.2 + i). && 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).
Definition cloc_to_val (cl : cloc) : val := locked (#cl.1, #cl.2)%V. Definition cloc_to_val (cl : cloc) : val :=
locked (#(cloc_loc cl), #(cloc_offset cl))%V.
Definition cloc_of_val (v : val) : option cloc := Definition cloc_of_val (v : val) : option cloc :=
match v return option (loc * nat) with match v return option cloc with
| (LitV (LitLoc l), LitV (LitInt i))%V => guard (0 i)%Z; Some (l, Z.to_nat i) | (LitV (LitLoc l), LitV (LitInt i))%V =>
guard (0 i)%Z;
Some $ MkCloc l (Z.to_nat i)
| _ => None | _ => None
end. end.
Definition offset_of_val (v: val) : option nat := Definition offset_of_val (v: val) : option nat :=
...@@ -109,7 +130,8 @@ Section definitions. ...@@ -109,7 +130,8 @@ Section definitions.
Definition full_locking_heap (σ : gmap cloc (lvl * val)) := Definition full_locking_heap (σ : gmap cloc (lvl * val)) :=
( τ : gmap loc (list (lvl * val)), ( τ : gmap loc (list (lvl * val)),
cl, σ !! cl = τ !! cl.1 = lookup (M:=list _) cl.2 cl, σ !! cl = τ !! (cloc_loc cl)
= lookup (M:=list _) (cloc_offset cl)
own lheap_name ( (to_locking_heap σ)) own lheap_name ( (to_locking_heap σ))
[ map] llvvs τ, lv, l SOMEV lv is_list lv (snd <$> lvvs) )%I. [ map] llvvs τ, lv, l SOMEV lv is_list lv (snd <$> lvvs) )%I.
...@@ -213,11 +235,11 @@ Section properties. ...@@ -213,11 +235,11 @@ Section properties.
Proof. apply mapsto_downgrade'. by apply lvl_included. Qed. Proof. apply mapsto_downgrade'. by apply lvl_included. Qed.
Lemma cloc_plus_0 cl : cloc_plus cl 0 = cl. Lemma cloc_plus_0 cl : cloc_plus cl 0 = cl.
Proof. rewrite /cloc_plus Nat.add_0_r. by destruct cl. Qed. 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 : cloc_plus (cloc_plus cl i) j = cloc_plus cl (i + j).
Proof. by rewrite /cloc_plus /= Nat.add_assoc. Qed. Proof. by rewrite /cloc_plus /= Nat.add_assoc (Nat.add_comm i j). Qed.
Lemma cloc_to_val_eq : cloc_to_val = λ cl, (#cl.1, #cl.2)%V. Lemma cloc_to_val_eq : cloc_to_val = λ cl, (#(cloc_loc cl), #(cloc_offset cl))%V.
Proof. rewrite /cloc_to_val. by unlock. Qed. Proof. rewrite /cloc_to_val. by unlock. Qed.
Lemma cloc_of_to_val cl : cloc_of_val (cloc_to_val cl) = Some cl. Lemma cloc_of_to_val cl : cloc_of_val (cloc_to_val cl) = Some cl.
Proof. Proof.
...@@ -321,8 +343,9 @@ Section properties. ...@@ -321,8 +343,9 @@ Section properties.
Lemma locking_heap_load cl lv q v σ : Lemma locking_heap_load cl lv q v σ :
full_locking_heap σ - cl C[lv]{q} v == ll vs, full_locking_heap σ - cl C[lv]{q} v == ll vs,
is_list ll vs vs !! cl.2 = Some v is_list ll vs vs !! (cloc_offset cl) = Some v
cl.1 SOMEV ll (cl.1 SOMEV ll - full_locking_heap σ cl C[lv]{q} v). (cloc_loc cl) SOMEV ll
((cloc_loc cl) SOMEV ll - full_locking_heap σ cl C[lv]{q} v).
Proof. Proof.
iDestruct 1 as (τ Hτ) "[Hσ Hτ]". iDestruct 1 as (τ Hτ) "[Hσ Hτ]".
rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl". rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl".
...@@ -340,9 +363,11 @@ Section properties. ...@@ -340,9 +363,11 @@ Section properties.
Lemma locking_heap_store cl lv v σ : Lemma locking_heap_store cl lv v σ :
full_locking_heap σ - cl C[lv] v == ll vs, full_locking_heap σ - cl C[lv] v == ll vs,
is_list ll vs vs !! cl.2 = Some v is_list ll vs vs !! (cloc_offset cl) = Some v
cl.1 SOMEV ll (cloc_loc cl) SOMEV ll
( ll' lv' v', is_list ll' (<[cl.2:=v']>vs) - cl.1 SOMEV ll' == ( ll' lv' v',
is_list ll' (<[cloc_offset cl:=v']>vs) -
(cloc_loc cl) SOMEV ll' ==
full_locking_heap (<[cl:=(lv',v')]>σ) cl C[lv'] v'). full_locking_heap (<[cl:=(lv',v')]>σ) cl C[lv'] v').
Proof. Proof.
iDestruct 1 as (τ Hτ) "[Hσ Hτ]". iDestruct 1 as (τ Hτ) "[Hσ Hτ]".
...@@ -360,7 +385,7 @@ Section properties. ...@@ -360,7 +385,7 @@ Section properties.
(exclusive_local_update _ (1%Qp, lv''', to_agree v')); (exclusive_local_update _ (1%Qp, lv''', to_agree v'));
first by apply to_locking_heap_lookup_Some. } first by apply to_locking_heap_lookup_Some. }
iModIntro. iSplitL "Hσ Hτ Hll"; last auto. iModIntro. iSplitL "Hσ Hτ Hll"; last auto.
iExists (<[cl.1:=(<[cl.2:=(lv''',v')]> lvvs)]>τ). iExists (<[cloc_loc cl:=(<[cloc_offset cl:=(lv''',v')]> lvvs)]>τ).
rewrite to_locking_heap_insert. iFrame "Hσ". iSplit. rewrite to_locking_heap_insert. iFrame "Hσ". iSplit.
{ destruct cl as [l i]; iPureIntro=> -[l' i']; simpl in *. { destruct cl as [l i]; iPureIntro=> -[l' i']; simpl in *.
destruct (decide (l' = l)) as [->|?]. destruct (decide (l' = l)) as [->|?].
...@@ -376,11 +401,11 @@ Section properties. ...@@ -376,11 +401,11 @@ Section properties.
Definition alloc_heap (σ : gmap cloc (lvl * val)) (l : loc) : Definition alloc_heap (σ : gmap cloc (lvl * val)) (l : loc) :
list val nat gmap cloc (lvl * val) := list val nat gmap cloc (lvl * val) :=
foldr (λ v go i, <[(l,i):=(ULvl,v)]> (go (S i))) (λ _, σ). foldr (λ v go i, <[MkCloc l i:=(ULvl,v)]> (go (S i))) (λ _, σ).
Lemma alloc_heap_None σ l vs j1 j2 : Lemma alloc_heap_None σ l vs j1 j2 :
( i, σ !! (l,i) = None) ( i, σ !! MkCloc l i = None)
j2 < j1 alloc_heap σ l vs j1 !! (l, j2) = None. j2 < j1 alloc_heap σ l vs j1 !! (MkCloc l j2) = None.
Proof. Proof.
intros Hσi. revert j1 j2. induction vs as [|v' vs IH]=> j1 j2 ?; csimpl. intros Hσi. revert j1 j2. induction vs as [|v' vs IH]=> j1 j2 ?; csimpl.
{ by rewrite Hσi. } { by rewrite Hσi. }
...@@ -389,8 +414,8 @@ Section properties. ...@@ -389,8 +414,8 @@ Section properties.
Qed. Qed.
Lemma alloc_heap_lookup σ l vs i j : Lemma alloc_heap_lookup σ l vs i j :
( i, σ !! (l,i) = None) ( i, σ !! MkCloc l i = None)
alloc_heap σ l vs j !! (l, j + i) = ((ULvl,) <$> vs) !! i. alloc_heap σ l vs j !! MkCloc l (j + i) = ((ULvl,) <$> vs) !! i.
Proof. Proof.
intros Hσi. revert i j. induction vs as [|v vs IH]=> i j; csimpl. intros Hσi. revert i j. induction vs as [|v vs IH]=> i j; csimpl.
{ by rewrite Hσi. } { by rewrite Hσi. }
...@@ -402,14 +427,14 @@ Section properties. ...@@ -402,14 +427,14 @@ Section properties.
Lemma alloc_heap_lookup_ne σ l l' vs i j : Lemma alloc_heap_lookup_ne σ l l' vs i j :
l l' l l'
alloc_heap σ l vs j !! (l', i) = σ !! (l', i). alloc_heap σ l vs j !! MkCloc l' i = σ !! MkCloc l' i.
Proof. Proof.
intros Hl. revert i j. induction vs as [|v vs IH]=> i j //; csimpl. intros Hl. revert i j. induction vs as [|v vs IH]=> i j //; csimpl.
by rewrite lookup_insert_ne; last congruence. by rewrite lookup_insert_ne; last congruence.
Qed. Qed.
Lemma locked_locs_alloc_heap σ l vs j : Lemma locked_locs_alloc_heap σ l vs j :
( i, σ !! (l,i) = None) ( i, σ !! MkCloc l i = None)
locked_locs (alloc_heap σ l vs j) = locked_locs σ. locked_locs (alloc_heap σ l vs j) = locked_locs σ.
Proof. Proof.
intros ?. revert j. induction vs as [|v vs IH]=> j //=. intros ?. revert j. induction vs as [|v vs IH]=> j //=.
...@@ -419,28 +444,30 @@ Section properties. ...@@ -419,28 +444,30 @@ Section properties.
Lemma locking_heap_alloc l ll vs σ : Lemma locking_heap_alloc l ll vs σ :
is_list ll vs is_list ll vs
full_locking_heap σ - l SOMEV ll == full_locking_heap σ - l SOMEV ll ==
i, σ !! (l,i) = None i, σ !! MkCloc l i = None
full_locking_heap (alloc_heap σ l vs O) (l,0) C vs. full_locking_heap (alloc_heap σ l vs O) MkCloc l 0 C vs.
Proof. Proof.
intros Hll. iDestruct 1 as (τ Hτ) "[Hσ Hτ]". iIntros "Hll". intros Hll. iDestruct 1 as (τ Hτ) "[Hσ Hτ]". iIntros "Hll".
set (f := foldr (λ v go i, <[(l,i):=(ULvl,v)]> (go (S i))) (λ _, σ)). set (f := foldr (λ v go i, <[MkCloc l i:=(ULvl,v)]> (go (S i))) (λ _, σ)).
iAssert τ !! l = None %I as %Hτi. iAssert τ !! l = None %I as %Hτi.
{ rewrite eq_None_not_Some. iIntros ([lvv ?]). { rewrite eq_None_not_Some. iIntros ([lvv ?]).
iDestruct (big_sepM_lookup with "Hτ") as (ll') "[Hll' _]"; first done. iDestruct (big_sepM_lookup with "Hτ") as (ll') "[Hll' _]"; first done.
by iDestruct (mapsto_valid_2 with "Hll Hll'") as %[]. } by iDestruct (mapsto_valid_2 with "Hll Hll'") as %[]. }
iAssert i, σ !! (l,i) = None %I as %Hσi. iAssert i, σ !! MkCloc l i = None %I as %Hσi.
{ iIntros (i). by rewrite Hτ Hτi. } { iIntros (i). by rewrite Hτ Hτi. }
iAssert (|==> own lheap_name ( to_locking_heap (f vs 0)) iAssert (|==> own lheap_name ( to_locking_heap (f vs 0))
[ list] iv vs, own lheap_name ( {[ (l,0 + i) := (1%Qp, ULvl,to_agree v) ]}))%I [ list] iv vs, own lheap_name ( {[ MkCloc l (i+0) := (1%Qp, ULvl,to_agree v) ]}))%I
with "[Hσ]" as ">[Hσ Hl]". with "[Hσ]" as ">[Hσ Hl]".
{ clear Hll. generalize 0=> j. { clear Hll. generalize 0=> j.
iInduction vs as [|v vs] "IH" forall (j); simpl; first by iFrame. iInduction vs as [|v vs] "IH" forall (j); simpl; first by iFrame.
iMod ("IH" $! (S j) with "Hσ") as "[Hσ Hls]". iMod ("IH" $! (S j) with "Hσ") as "[Hσ Hls]".
iMod (own_update with "Hσ") as "[Hσ Hl]". iMod (own_update with "Hσ") as "[Hσ Hl]".
{ eapply auth_update_alloc, { eapply auth_update_alloc,
(alloc_singleton_local_update _ (l,j) (1%Qp, ULvl, to_agree v)); try done. (alloc_singleton_local_update _ (MkCloc l j)
(1%Qp, ULvl, to_agree v)); try done.
apply to_locking_heap_lookup_None. rewrite alloc_heap_None //. lia. } apply to_locking_heap_lookup_None. rewrite alloc_heap_None //. lia. }
iModIntro. rewrite -to_locking_heap_insert Nat.add_0_r; iFrame "Hσ Hl". iModIntro.
rewrite -to_locking_heap_insert /=. iFrame "Hσ Hl".
iApply (big_sepL_impl with "Hls"); iIntros "!>" (k w _) "?". iApply (big_sepL_impl with "Hls"); iIntros "!>" (k w _) "?".
by rewrite Nat.add_succ_r. } by rewrite Nat.add_succ_r. }
iModIntro. iSplit; first done. iSplitL "Hσ Hτ Hll". iModIntro. iSplit; first done. iSplitL "Hσ Hτ Hll".
...@@ -472,7 +499,7 @@ Section properties. ...@@ -472,7 +499,7 @@ Section properties.
first by apply to_locking_heap_lookup_Some. first by apply to_locking_heap_lookup_Some.
intros h Hh. fold_leibniz. intros ->. split; eauto. } intros h Hh. fold_leibniz. intros ->. split; eauto. }
iModIntro. iSplitR "Hl"; last by eauto with iFrame. iModIntro. iSplitR "Hl"; last by eauto with iFrame.
iExists (<[cl.1:=(<[cl.2:=(ULvl,v)]> lvvs)]>τ). iExists (<[cloc_loc cl:=(<[cloc_offset cl:=(ULvl,v)]> lvvs)]>τ).
rewrite to_locking_heap_insert. iFrame "Hσ". iSplit. rewrite to_locking_heap_insert. iFrame "Hσ". iSplit.
{ destruct cl as [l i]; iPureIntro=> -[l' i']; simpl in *. { destruct cl as [l i]; iPureIntro=> -[l' i']; simpl in *.
destruct (decide (l' = l)) as [->|?]. destruct (decide (l' = l)) as [->|?].
......
...@@ -963,13 +963,14 @@ Section denv_spec. ...@@ -963,13 +963,14 @@ Section denv_spec.
rewrite !big_sepL_cons. rewrite !big_sepL_cons.
iDestruct "H" as "[H1 H2]". iDestruct "H" as "[H1 H2]".
iSplitL "H1". iSplitL "H1".
+ destruct dio as [[lvl q] dv|] ; simplify_eq /=; last done. + destruct dio as [[lvl q dv]|] ; simplify_eq /=; last done.
assert (dval_interp E denv_dval0 = dval_interp E' denv_dval0). assert (dval_interp E dv = dval_interp E' dv) as ->.
apply andb_True in Haux as [Haux1 Haux2]. { destruct_and!. by apply dval_interp_mono. }
apply dval_interp_mono; done. rewrite H0.
assert (dloc_interp E (dLoc (i + 0) 0) = assert (dloc_interp E (dLoc (i + 0) 0) =
dloc_interp E' (dLoc (i + 0) 0)). dloc_interp E' (dLoc (i + 0) 0)) as ->.
admit. rewrite H3. iFrame. { apply dloc_interp_mono; auto.
rewrite !Nat.add_0_r. admit. }
iFrame.
+ iSpecialize ("IHm" $! (S i)). + iSpecialize ("IHm" $! (S i)).
iAssert ([ list] i0dio0 m, from_option iAssert ([ list] i0dio0 m, from_option
(λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |}, (λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
......
...@@ -42,14 +42,6 @@ Section splitenv. ...@@ -42,14 +42,6 @@ Section splitenv.
by rewrite env_lookup_snoc_ne in Hsnoc. by rewrite env_lookup_snoc_ne in Hsnoc.
Qed. Qed.
(* RK: total hack to handle cloc_plus 0 in the environment. FIXME *)
Global Instance mapsto_list_from_env_snoc_Γls_plus_0 Γin Γout Γls i l q v lvl :
MapstoListFromEnv Γin Γout Γls
MapstoListFromEnv (Esnoc Γin i (cloc_plus l 0 C[lvl]{q} v))
Γout
(PenvItem l lvl q v :: Γls) | 1.
Proof. rewrite cloc_plus_0. apply mapsto_list_from_env_snoc_Γls. Qed.
Class ListOfMapsto (Γls : penv) (E : known_locs) (ps : denv) := Class ListOfMapsto (Γls : penv) (E : known_locs) (ps : denv) :=
list_of_mapsto : penv_interp Γls denv_interp E ps. list_of_mapsto : penv_interp Γls denv_interp E ps.
...@@ -64,7 +56,7 @@ Section splitenv. ...@@ -64,7 +56,7 @@ Section splitenv.
(denv_insert i x q dv ps). (denv_insert i x q dv ps).
Proof. Proof.
rewrite /LocLookup /ListOfMapsto /penv_interp=> Hi [-> ?] HΓls /=. rewrite /LocLookup /ListOfMapsto /penv_interp=> Hi [-> ?] HΓls /=.
iIntros "[Hl H] /=". rewrite HΓls -denv_insert_interp /= Hi cloc_plus_0. iFrame. iIntros "[Hl H] /=". rewrite HΓls -denv_insert_interp /= Hi. iFrame.
Qed. Qed.
Lemma tac_envs_split_mapsto Γs_in Γs_out Γls Γp c ps P: Lemma tac_envs_split_mapsto Γs_in Γs_out Γls Γp c ps P:
......
...@@ -11,7 +11,7 @@ Section test. ...@@ -11,7 +11,7 @@ Section test.
Lemma test1 (l : cloc) (v: val) : Lemma test1 (l : cloc) (v: val) :
l C v - AWP ∗ᶜ ♯ₗl {{ w, w = v l C v }}. l C v - AWP ∗ᶜ ♯ₗl {{ w, w = v l C v }}.
Proof. Proof.
iIntros "Hl1". vcg_solver. rewrite cloc_plus_0. auto. iIntros "Hl1". vcg_solver. auto.
Qed. Qed.
(* double dereferencing *) (* double dereferencing *)
...@@ -19,19 +19,19 @@ Section test. ...@@ -19,19 +19,19 @@ Section test.
l1 C cloc_to_val l2 - l2 C v - l1 C cloc_to_val l2 - l2 C v -
AWP ∗ᶜ ∗ᶜ ♯ₗl1 {{ v, v = #1 l1 C cloc_to_val l2 - l2 C v }}. AWP ∗ᶜ ∗ᶜ ♯ₗl1 {{ v, v = #1 l1 C cloc_to_val l2 - l2 C v }}.
Proof. Proof.
iIntros "Hl1 Hl2". vcg_solver. rewrite ?cloc_plus_0. auto. iIntros "Hl1 Hl2". vcg_solver. auto.
Qed. Qed.
Lemma test3 (l : cloc) (v: val) : Lemma test3 (l : cloc) (v: val) :
l C v - AWP ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗl {{ w, w = v l C v }}. l C v - AWP ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗl {{ w, w = v l C v }}.
Proof. Proof.
iIntros "Hl1". vcg_solver. rewrite ?cloc_plus_0. auto. iIntros "Hl1". vcg_solver. auto.
Qed. Qed.
Lemma test4 (l : cloc) (v1 v2: val) : Lemma test4 (l : cloc) (v1 v2: val) :
l C v1 - AWP ♯ₗl = a_ret v2 {{ v, v = v2 l C[LLvl] v2 }}. l C v1 - AWP ♯ₗl = a_ret v2 {{ v, v = v2 l C[LLvl] v2 }}.
Proof. Proof.
iIntros "Hl1". vcg_solver. rewrite ?cloc_plus_0. auto. iIntros "Hl1". vcg_solver. auto.
Qed. Qed.
(* double dereferencing & modification *) (* double dereferencing & modification *)
...@@ -42,7 +42,7 @@ Section test. ...@@ -42,7 +42,7 @@ Section test.
{{ w, w = v2 {{ w, w = v2
l1 C cloc_to_val r2 l2 C v1 r1 C cloc_to_val r2 - r2 C v2 }}. l1 C cloc_to_val r2 l2 C v1 r1 C cloc_to_val r2 - r2 C v2 }}.
Proof. Proof.
iIntros "**". vcg_solver. rewrite ?cloc_plus_0. eauto 40. iIntros "**". vcg_solver. eauto 40.
Qed. Qed.
Lemma test_par_1 (l1 l2 : cloc) (v1 v2: val) : Lemma test_par_1 (l1 l2 : cloc) (v1 v2: val) :
...@@ -50,7 +50,7 @@ Section test. ...@@ -50,7 +50,7 @@ Section test.
AWP ∗ᶜ ♯ₗl1 ||| ∗ᶜ ♯ₗl2 AWP ∗ᶜ ♯ₗl1 ||| ∗ᶜ ♯ₗl2
{{ w, w = (v1, v2)%V l1 C v1 l2 C v2 }}. {{ w, w = (v1, v2)%V l1 C v1 l2 C v2 }}.
Proof. Proof.
iIntros "**". vcg_solver. rewrite Qp_half_half ?cloc_plus_0. eauto with iFrame. iIntros "**". vcg_solver. rewrite Qp_half_half. eauto with iFrame.
Qed. Qed.
Lemma test_par_2 (l1 l2 : cloc) (v1 v2: val) : Lemma test_par_2 (l1 l2 : cloc) (v1 v2: val) :
...@@ -58,7 +58,7 @@ Section test. ...@@ -58,7 +58,7 @@ Section test.
AWP (♯ₗl1 = a_ret v2) ||| (♯ₗl2 = a_ret v1) AWP (♯ₗl1 = a_ret v2) ||| (♯ₗl2 = a_ret v1)
{{ w, w = (v2, v1)%V l1 C[LLvl] v2 l2 C[LLvl] v1 }}. {{ w, w = (v2, v1)%V l1 C[LLvl] v2 l2 C[LLvl] v1 }}.
Proof. Proof.
iIntros "**". vcg_solver. rewrite ?cloc_plus_0. eauto with iFrame. iIntros "**". vcg_solver. eauto with iFrame.
Qed. Qed.
...@@ -70,7 +70,7 @@ Section test. ...@@ -70,7 +70,7 @@ Section test.
Proof. Proof.
iIntros "Hl". vcg_solver. iIntros "Hl". vcg_solver.
iIntros "Hl". awp_lam. awp_ret_value. iIntros "Hl". awp_lam. awp_ret_value.
vcg_continue. rewrite ?cloc_plus_0. eauto. vcg_continue. eauto.
Qed. Qed.
Definition plus_pair : val := λ: "vv", Definition plus_pair : val := λ: "vv",
...@@ -94,14 +94,14 @@ Section test. ...@@ -94,14 +94,14 @@ Section test.
iIntros. vcg_solver. iIntros "Hl". awp_lam. iIntros. vcg_solver. iIntros "Hl". awp_lam.
do 2 (awp_proj; awp_let). do 2 (awp_proj; awp_let).
vcg_solver. iIntros "Hl". vcg_continue. vcg_solver. iIntros "Hl". vcg_continue.
rewrite Qp_half_half ?cloc_plus_0. eauto 42 with iFrame. rewrite Qp_half_half. eauto 42 with iFrame.
Qed. Qed.
Lemma test6 (l : cloc) (z0 : Z) R: Lemma test6 (l : cloc) (z0 : Z) R:
l C #z0 - l C #z0 -
AWP ♯ₗl += 1 @ R {{ v, v = #z0 l C[LLvl] #(z0+1) }}. AWP ♯ₗl += 1 @ R {{ v, v = #z0 l C[LLvl] #(z0+1) }}.
Proof. Proof.
iIntros "Hl". vcg_solver. rewrite ?cloc_plus_0. eauto. iIntros "Hl". vcg_solver. eauto.
Qed. Qed.
Lemma test7 (l k : cloc) (z0 z1 : Z) R: Lemma test7 (l k : cloc) (z0 z1 : Z) R:
...@@ -110,7 +110,7 @@ Section test. ...@@ -110,7 +110,7 @@ Section test.
AWP (♯ₗl += 1) + (∗ᶜ♯ₗk) @ AWP (♯ₗl += 1) + (∗ᶜ♯ₗk) @
R {{ v, v = #(z0+z1) l C[LLvl] #(z0+1) k C #z1 }}. R {{ v, v = #(z0+z1) l C[LLvl] #(z0+1) k C #z1 }}.
Proof. Proof.
iIntros "Hl Hk". vcg_solver. rewrite ?cloc_plus_0. eauto with iFrame. iIntros "Hl Hk". vcg_solver. eauto with iFrame.
Qed. Qed.
End test. End test.
...@@ -26,7 +26,7 @@ Section factorial_spec. ...@@ -26,7 +26,7 @@ Section factorial_spec.
l C #n - (l C[LLvl] #(n+1) - Φ #(n+1)) - l C #n - (l C[LLvl] #(n+1) - Φ #(n+1)) -
AWP incr (cloc_to_val l) @ R {{ Φ }}. AWP incr (cloc_to_val l) @ R {{ Φ }}.
Proof. Proof.
iIntros "Hl HΦ". awp_lam. vcg_solver. rewrite ?cloc_plus_0. auto. iIntros "Hl HΦ". awp_lam. vcg_solver. auto.
Qed. Qed.
Lemma factorial_body_spec (n k : nat) (c r: cloc) R : Lemma factorial_body_spec (n k : nat) (c r: cloc) R :
...@@ -36,13 +36,13 @@ Section factorial_spec. ...@@ -36,13 +36,13 @@ Section factorial_spec.
Proof. Proof.
iIntros "(Hk & Hc & Hr)". do 3 awp_lam. iIntros "(Hk & Hc & Hr)". do 3 awp_lam.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec'. iNext. iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec'. iNext.
vcg_solver. rewrite Qp_half_half ?cloc_plus_0. iIntros "Hr Hc". vcg_solver. rewrite Qp_half_half. iIntros "Hr Hc".
case_bool_decide. case_bool_decide.
+ iLeft. iSplit; eauto. + iLeft. iSplit; eauto.
iApply a_sequence_spec'; iNext. iApply a_sequence_spec'; iNext.
iApply (incr_spec with "Hc"). iIntros "Hc". iApply (incr_spec with "Hc"). iIntros "Hc".
iModIntro. vcg_solver. iIntros "Hc Hr". iModIntro. vcg_solver. iIntros "Hc Hr".
iModIntro. rewrite ?cloc_plus_0. iModIntro.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->. assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
{ rewrite Nat.add_1_r /fact. lia. } { rewrite Nat.add_1_r /fact. lia. }
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia. assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
...@@ -59,7 +59,6 @@ Section factorial_spec. ...@@ -59,7 +59,6 @@ Section factorial_spec.
iApply awp_bind. awp_alloc_ret r "[Hr _]". iApply awp_bind. awp_alloc_ret r "[Hr _]".
iApply awp_bind. awp_alloc_ret c "[Hc _]". iApply awp_bind. awp_alloc_ret c "[Hc _]".
iApply a_sequence_spec'. iNext. iApply a_sequence_spec'. iNext.
rewrite ?cloc_plus_0.
iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[Hr Hc]"). iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia. - iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
- iIntros (?) "[Hc Hr]". iModIntro. - iIntros (?) "[Hc Hr]". iModIntro.
...@@ -73,17 +72,16 @@ Section factorial_spec. ...@@ -73,17 +72,16 @@ Section factorial_spec.
iApply awp_bind. awp_alloc_ret r "[Hr _]". iApply awp_bind. awp_alloc_ret r "[Hr _]".
iApply awp_bind. awp_alloc_ret c "[Hc _]". iApply awp_bind. awp_alloc_ret c "[Hc _]".
iApply a_sequence_spec'. iNext. do 3 awp_lam. iApply a_sequence_spec'. iNext. do 3 awp_lam.
rewrite ?cloc_plus_0.
iApply (a_while_inv_spec iApply (a_while_inv_spec
(k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]"). (k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]").
- iExists O. eauto with iFrame lia. - iExists O. eauto with iFrame lia.
- iModIntro. iIntros "H". iDestruct "H" as (k) "(H & Hc & Hr)". - iModIntro. iIntros "H". iDestruct "H" as (k) "(H & Hc & Hr)".
vcg_solver. rewrite ?cloc_plus_0. iIntros "Hr Hc". vcg_solver. iIntros "Hr Hc".
case_bool_decide. case_bool_decide.
+ iRight. iSplit; eauto. + iRight. iSplit; eauto.
iNext. iApply a_sequence_spec'. iNext. rewrite Qp_half_half ?cloc_plus_0. iNext. iApply a_sequence_spec'. iNext. rewrite Qp_half_half.
iApply (incr_spec with "Hc"). iApply (incr_spec with "Hc").
iIntros "Hc". iModIntro. vcg_solver. rewrite ?cloc_plus_0. iIntros "Hc". iModIntro. vcg_solver.
iIntros "Hc Hr". iModIntro. iIntros "Hc Hr". iModIntro.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->. assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
{ rewrite Nat.add_1_r /fact. lia. } { rewrite Nat.add_1_r /fact. lia. }
......
...@@ -23,10 +23,10 @@ Section memcpy. ...@@ -23,10 +23,10 @@ Section memcpy.
(* ⌜take i ls1 = take i ls2⌝ -∗ *) (* ⌜take i ls1 = take i ls2⌝ -∗ *)
p C ls1 - p C ls1 -
q C ls2 - q C ls2 -
pp