Commit 5fb2e503 authored by Robbert Krebbers's avatar Robbert Krebbers

Random stuff that breaks everything:

- Add support for fst/snd/pair to the vcg_gen + reified expressions for non-monadic expressions.
- Make `cloc_to_val` locked so that it will _never_ be unfolded.
- Support locations + offsets in the reified language.
- Drop `vcg_compute`, it left huge thunks of computation, making some things super slow. Just use `simpl` with appropriate `Arguments` instead.
parent 84d87469
......@@ -120,16 +120,16 @@ 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;
Some (cloc_to_val (cloc_add cl o))
cl cloc_of_val v1;
o offset_of_val v2;
Some (cloc_to_val (cloc_plus cl o))
| PtrLtOp =>
cl1 cloc_of_val v1;
cl2 cloc_of_val v2;
Some #(cloc_lt cl1 cl2)
cl1 cloc_of_val v1;
cl2 cloc_of_val v2;
Some #(cloc_lt cl1 cl2)
end.
Definition a_ptr_add : val := λ: "x" "y",
Definition a_ptr_plus : val := λ: "x" "y",
"lo" ←ᶜ ("x" ||| "y");;
let: "o'" := Snd (Fst "lo") + Snd "lo" in
a_ret (Fst (Fst "lo"), "o'").
......@@ -142,11 +142,10 @@ Definition a_ptr_lt : val := λ: "x" "y",
Definition a_bin_op (op : cbin_op) : val :=
match op with
| CBinOp op' =>
λ: "x1" "x2",
"vv" ←ᶜ "x1" ||| "x2" ;;
a_ret (BinOp op' (Fst "vv") (Snd "vv"))
| PtrPlusOp => a_ptr_add
| CBinOp op' => λ: "x1" "x2",
"vv" ←ᶜ "x1" ||| "x2" ;;
a_ret (BinOp op' (Fst "vv") (Snd "vv"))
| PtrPlusOp => a_ptr_plus
| PtrLtOp => a_ptr_lt
end.
......@@ -193,7 +192,8 @@ Section proofs.
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Φ" $! (l, 0%nat))].
iIntros "!> !>". rewrite cloc_to_val_eq.
iSplitL "Hlocks Hσ"; [|by iApply ("HΦ" $! (l, 0%nat))].
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.
......@@ -211,14 +211,15 @@ 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 i] w ->) "[Hl HΦ]".
iDestruct ("HΦ" with "H1 H2") as (cl 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.
assert ((#l, #i)%V X).
{ intros Hcl. destruct (HX _ Hcl) as ([??]&[=]%cloc_to_of_val&?); naive_solver. }
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.
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_let. rewrite cloc_to_val_eq. do 2 wp_proj; wp_let. do 2 wp_proj; wp_let. wp_proj; wp_let.
wp_apply (mset_add_spec with "[$]"); first done.
iIntros "Hlocks /="; wp_seq.
wp_load; wp_match.
......@@ -226,10 +227,10 @@ 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 ({[(#l, #i)%V]} X), _. iFrame "Hσ". rewrite locked_locs_lock.
iIntros "{$Hlocks} !%".
iExists ({[cloc_to_val cl]} X), _. iFrame "Hσ". rewrite locked_locs_lock.
iSplit; last by rewrite cloc_to_val_eq. iPureIntro.
intros v [->%elem_of_singleton|?]%elem_of_union; last set_solver.
eexists; split; [apply (cloc_of_to_val (l,i))|set_solver].
eexists. split; [apply (cloc_of_to_val cl)|set_solver].
Qed.
Lemma a_load_spec_exists_frac R Φ e :
......@@ -240,14 +241,15 @@ Section proofs.
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 i] q w ->) "[Hl HΦ]". awp_lam.
iIntros (v). iDestruct 1 as (cl 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.
assert ((#l, #i)%V X).
{ intros Hcl. destruct (HX _ Hcl) as ([??]&[=]%cloc_to_of_val&?); naive_solver. }
assert (cloc_to_val cl X) as HclX.
{ intros Hcl. destruct (HX _ Hcl) as (?&[=]%cloc_to_of_val&?); naive_solver. }
rewrite cloc_to_val_eq in HclX.
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_let. rewrite cloc_to_val_eq. 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 //.
wp_op. iSplit; first done. iNext; wp_seq.
......@@ -282,7 +284,7 @@ Section proofs.
Lemma a_seq_spec R Φ :
U (Φ #()) -
AWP (a_seq #()) @ R {{ Φ }}.
AWP a_seq #() @ R {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /a_seq. awp_lam.
iApply awp_atomic_env. iIntros (env) "Henv $". iApply wp_fupd.
......@@ -410,20 +412,21 @@ Section proofs.
iRight. iSplit; eauto. by awp_seq.
Qed.
Lemma a_ptr_add_spec R Φ Ψ2 e1 e2 :
Lemma a_ptr_plus_spec R Φ Ψ2 e1 e2 :
AWP e2 @ R {{ Ψ2 }} -
AWP e1 @ R {{ v1, v2, Ψ2 v2 - cl (n : nat),
v1 = cloc_to_val cl
v2 = #n
Φ (cloc_to_val (cloc_add cl n)) }} -
AWP a_ptr_add e1 e2 @ R {{ Φ }}.
Φ (cloc_to_val (cloc_plus cl n)) }} -
AWP a_ptr_plus e1 e2 @ R {{ Φ }}.
Proof.
iIntros "He2 HΦ". rewrite /a_ptr_add.
iIntros "He2 HΦ". rewrite /a_ptr_plus.
awp_apply (a_wp_awp with "HΦ"); 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 !>". awp_let.
iDestruct ("Hv1" with "Hv2") as ([l o] n -> ->) "HΦ /=".
iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ /=".
rewrite cloc_to_val_eq.
do 3 awp_proj. awp_op. awp_let. do 2 awp_proj.
iApply awp_ret. iApply wp_value. by rewrite -Nat2Z.inj_add.
Qed.
......@@ -436,12 +439,13 @@ Section proofs.
Φ #(cloc_lt p q) }} -
AWP a_ptr_lt e1 e2 @ R {{ Φ }}.
Proof.
iIntros "He1 HΦ". rewrite /a_ptr_add.
iIntros "He1 HΦ". rewrite /a_ptr_plus.
awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
awp_apply (a_wp_awp with "HΦ"); iIntros (a2) "Ha2". awp_lam.
iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
iDestruct ("Hv2" with "Hv1") as ([pl pi] [ql qi] -> ->) "HΦ /=".
rewrite cloc_to_val_eq.
do 2 (awp_proj; awp_let). do 2 awp_proj.
unfold cloc_lt; simpl. case_bool_decide as Hp; subst; awp_op.
- rewrite (bool_decide_true (LitV ql = LitV ql)) //. awp_if. do 2 awp_proj.
......@@ -466,7 +470,7 @@ Section proofs.
iNext. awp_lam. iApply awp_ret. do 2 wp_proj.
iSpecialize ("HΦ" with "HΨ1 HΨ2").
iDestruct "HΦ" as (w0) "[% H]". by wp_pure _.
- iApply (a_ptr_add_spec with "H2").
- iApply (a_ptr_plus_spec with "H2").
iApply (awp_wand with "H1").
iIntros (v1) "HΨ1". iNext.
iIntros (v2) "HΨ2". iDestruct ("HΦ" with "HΨ1 HΨ2") as (w hop) "HΦ".
......
......@@ -93,9 +93,9 @@ Section definitions.
(** Pointer arithmetic *)
Definition cloc_lt (p q : cloc) : bool :=
bool_decide (p.1 = q.1) && bool_decide (p.2 < q.2)%nat.
Definition cloc_add (cl : cloc) (i : nat) : cloc := (cl.1, cl.2 + i).
Definition cloc_plus (cl : cloc) (i : nat) : cloc := (cl.1, cl.2 + i).
Definition cloc_to_val (cl : cloc) : val := (#cl.1, #cl.2).
Definition cloc_to_val (cl : cloc) : val := locked (#cl.1, #cl.2)%V.
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)
......@@ -134,10 +134,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_add cl i C{q} v)%I
([ list] i v vs, cloc_plus 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
([ list] i v vs, cloc_plus 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 σ.
......@@ -212,19 +212,27 @@ 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_add_0 cl : cloc_add cl 0 = cl.
Proof. rewrite /cloc_add Nat.add_0_r. by destruct cl. Qed.
Lemma cloc_add_add cl i j : cloc_add (cloc_add cl i) j = cloc_add cl (i + j).
Proof. by rewrite /cloc_add /= Nat.add_assoc. Qed.
Lemma cloc_plus_0 cl : cloc_plus cl 0 = cl.
Proof. rewrite /cloc_plus Nat.add_0_r. by destruct cl. 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. Qed.
Lemma cloc_to_val_eq : cloc_to_val = λ cl, (#cl.1, #cl.2)%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 /= option_guard_True ?Nat2Z.id; last lia. Qed.
Proof.
destruct cl.
by rewrite cloc_to_val_eq /= 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.
rewrite /cloc_of_val /cloc_to_val=> ?.
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.
......
This diff is collapsed.
......@@ -7,15 +7,16 @@ From iris.algebra Require Import frac.
Section denv.
Definition is_dloc (E: known_locs) (dv: dval) : option nat :=
match dv with
| dLocV (dLoc i) => Some i
| dLocV (dLoc i 0) => Some i
| _ => None
end.
Global Arguments is_dloc _ !_ /.
Record penv_item := PenvItem {
penv_loc : cloc;
penv_level : lvl;
penv_frac : frac;
penv_val : val
penv_val : val
}.
Record denv_item := DenvItem {
......@@ -36,7 +37,7 @@ Section denv.
| None :: m' => denv_wf_val E m'
end.
Fixpoint denv_wf_len (E: known_locs) (m: denv) : bool :=
Fixpoint denv_wf_len (E: known_locs) (m: denv) : bool :=
match E, m with
| _, [] => true
| _ :: E', _ :: m' => denv_wf_len E m'
......@@ -47,7 +48,7 @@ Section denv.
denv_wf_val E m && denv_wf_len E m.
Definition denv_item_opt_merge
(dio1 dio2 : option denv_item) : option denv_item :=
(dio1 dio2 : option denv_item) : option denv_item :=
match dio1, dio2 with
| None, dio | dio, None => dio
| Some di1, Some di2 =>
......@@ -175,11 +176,10 @@ Section denv.
end.
End denv.
Lemma is_dloc_some E dv i : is_dloc E dv = Some i dv = dLocV (dLoc i).
Proof. by destruct dv as [| |[]|]; intros; simplify_eq /=. Qed.
Lemma is_dloc_Some E dv i : is_dloc E dv = Some i dv = dLocV (dLoc i 0).
Proof. by destruct dv as [| |[? []|]|]; intros; simplify_eq /=. Qed.
Lemma denv_merge_nil_r m :
denv_merge m [] = m.
Lemma denv_merge_nil_r m : denv_merge m [] = m.
Proof. induction m; simpl; eauto. Qed.
Section denv_spec.
......@@ -189,7 +189,8 @@ Section denv_spec.
Definition denv_interp (L : known_locs) (m : denv) : iProp Σ :=
([ list] i dio m,
from_option (λ '(DenvItem lv q dv),
dloc_interp L (dLoc i) C[lv]{q} dval_interp L dv) True dio)%I.
dloc_interp L (dLoc i 0) C[lv]{q} dval_interp L dv) True dio)%I.
(* ↑ FIX THAT *)
Fixpoint denv_stack_interp (ms1 ms2 : list denv) E (P : iProp Σ) :=
match ms1,ms2 with
......@@ -206,7 +207,7 @@ Section denv_spec.
Definition denv_interp_aux (L : known_locs) (m : denv) (k : nat) : iProp Σ :=
([ list] i dio m,
from_option (λ '(DenvItem lv q dv),
dloc_interp L (dLoc (k+i)) C[lv]{q} dval_interp L dv) True dio)%I.
dloc_interp L (dLoc (k+i) 0) C[lv]{q} dval_interp L dv) True dio)%I.
(** ** Helper lemmas *)
Lemma denv_interp_aux_0 L m :
......@@ -231,7 +232,7 @@ Section denv_spec.
(** ** Correctness of the `denv_` functions w.r.t. the interpretation *)
Lemma denv_interp_singleton_aux E i k x q dv :
dloc_interp E (dLoc (k+i)) C[x]{q} dval_interp E dv
dloc_interp E (dLoc (k+i) 0) C[x]{q} dval_interp E dv
denv_interp_aux E (denv_singleton i x q dv) k.
Proof.
assert ((lookup i (denv_singleton i x q dv)) =
......@@ -250,7 +251,7 @@ Section denv_spec.
Qed.
Lemma denv_insert_interp_aux E m i k x q dv :
denv_interp_aux E m k dloc_interp E (dLoc (k+i)) C[x]{q} dval_interp E dv
denv_interp_aux E m k dloc_interp E (dLoc (k+i) 0) C[x]{q} dval_interp E dv
denv_interp_aux E (denv_insert i x q dv m) k.
Proof.
Opaque dval_interp dloc_interp.
......@@ -289,7 +290,7 @@ Section denv_spec.
Qed.
Lemma denv_insert_interp E m i x q dv :
denv_interp E m dloc_interp E (dLoc i) C[x]{q} dval_interp E dv
denv_interp E m dloc_interp E (dLoc i 0) C[x]{q} dval_interp E dv
denv_interp E (denv_insert i x q dv m).
Proof. by rewrite -!denv_interp_aux_0 denv_insert_interp_aux. Qed.
......@@ -330,7 +331,7 @@ Section denv_spec.
Lemma denv_delete_frac_interp_aux E i k m m' q dv :
denv_delete_frac i m = Some (m', q, dv)
denv_interp_aux E m k
denv_interp_aux E m' k dloc_interp E (dLoc (k+i)) C{q} dval_interp E dv.
denv_interp_aux E m' k dloc_interp E (dLoc (k+i) 0) C{q} dval_interp E dv.
Proof.
iInduction m as [|dio m] "IHm" forall (i k m').
- simpl. iIntros (Hz). inversion Hz.
......@@ -356,7 +357,7 @@ Section denv_spec.
Lemma denv_delete_frac_interp_aux_flip E i k m m' q dv :
denv_delete_frac i m = Some (m', q, dv)
(denv_interp_aux E m' k dloc_interp E (dLoc (k+i)) C{q} dval_interp E dv)
(denv_interp_aux E m' k dloc_interp E (dLoc (k+i) 0) C{q} dval_interp E dv)
- denv_interp_aux E m k.
Proof.
iInduction m as [|dio m] "IHm" forall (i k m').
......@@ -383,7 +384,7 @@ Section denv_spec.
Lemma denv_delete_frac_interp E i m m' q dv :
denv_delete_frac i m = Some (m', q, dv)
denv_interp E m
denv_interp E m' dloc_interp E (dLoc i) C{q} dval_interp E dv.
denv_interp E m' dloc_interp E (dLoc i 0) C{q} dval_interp E dv.
Proof.
intros ?.
by rewrite -!denv_interp_aux_0 denv_delete_frac_interp_aux.
......@@ -392,7 +393,7 @@ Section denv_spec.
Lemma denv_delete_full_interp_aux E i k m m' q dv :
denv_delete_full_aux i m = Some (m', q, dv)
denv_interp_aux E m k
denv_interp_aux E m' k dloc_interp E (dLoc (k+i)) C{q} dval_interp E dv.
denv_interp_aux E m' k dloc_interp E (dLoc (k+i) 0) C{q} dval_interp E dv.
Proof.
iInduction m as [|dio m] "IHm" forall (i k m').
- simpl. iIntros (Hz). inversion Hz.
......@@ -418,7 +419,7 @@ Section denv_spec.
Lemma denv_delete_full_interp_aux_flip E i k m m' q dv :
denv_delete_full_aux i m = Some (m', q, dv)
denv_interp_aux E m' k dloc_interp E (dLoc (k+i)) C{q} dval_interp E dv
denv_interp_aux E m' k dloc_interp E (dLoc (k+i) 0) C{q} dval_interp E dv
denv_interp_aux E m k.
Proof.
iInduction m as [|dio m] "IHm" forall (i k m').
......@@ -445,7 +446,7 @@ Section denv_spec.
Lemma denv_delete_full_interp E i m m' dv :
denv_delete_full i m = Some (m', dv)
denv_interp E m
denv_interp E m' dloc_interp E (dLoc i) C{1} dval_interp E dv.
denv_interp E m' dloc_interp E (dLoc i 0) C{1} dval_interp E dv.
Proof.
rewrite /denv_delete_full.
destruct (denv_delete_full_aux i m)
......@@ -457,7 +458,7 @@ Section denv_spec.
Lemma denv_lookup_interp E i q dv m:
denv_lookup i m = Some (q, dv)
m', denv_interp E m
dloc_interp E (dLoc i) C{q} dval_interp E dv denv_interp E m'.
dloc_interp E (dLoc i 0) C{q} dval_interp E dv denv_interp E m'.
Proof.
rewrite /denv_lookup=>?.
destruct (denv_delete_full_aux i m)
......@@ -582,7 +583,7 @@ Section denv_spec.
Lemma denv_delete_frac_stack_interp E i ms ms' q dv :
denv_delete_frac_stack i ms = Some (ms', q, dv)
denv_stack_interp ms ms' E (dloc_interp E (dLoc i) C{q} dval_interp E dv)%I.
denv_stack_interp ms ms' E (dloc_interp E (dLoc i 0) C{q} dval_interp E dv)%I.
Proof.
iInduction ms as [|m ms] "IH" forall (ms'); iIntros (Hdel); simplify_eq/=.
destruct (denv_delete_frac i m) as [[[m' q'] dv']|] eqn:Hm; simplify_eq/=.
......@@ -597,7 +598,7 @@ Section denv_spec.
Lemma denv_delete_full_stack_interp E i ms ms' q dv :
denv_delete_full_stack_aux i ms = Some (ms', q, dv)
denv_stack_interp ms ms' E (dloc_interp E (dLoc i) C{q} dval_interp E dv)%I.
denv_stack_interp ms ms' E (dloc_interp E (dLoc i 0) C{q} dval_interp E dv)%I.
Proof.
iInduction ms as [|m ms] "IH" forall (ms' q dv);
iIntros (Hdel); simplify_eq/=.
......@@ -627,7 +628,7 @@ Section denv_spec.
denv_delete_full_2 i ms m = Some (ms', m', dv)
denv_stack_interp ms ms' E
(denv_interp E m -
denv_interp E m' dloc_interp E (dLoc i) C dval_interp E dv)%I.
denv_interp E m' dloc_interp E (dLoc i 0) C dval_interp E dv)%I.
Proof.
rewrite /denv_delete_full_2. intros.
destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] dv1]|] eqn:Hms;
......@@ -653,7 +654,7 @@ Section denv_spec.
denv_delete_frac_2 i ms m = Some (ms', m', q, dv)
denv_stack_interp ms ms' E
(denv_interp E m -
denv_interp E m' dloc_interp E (dLoc i) C{q} dval_interp E dv)%I.
denv_interp E m' dloc_interp E (dLoc i 0) C{q} dval_interp E dv)%I.
Proof.
rewrite /denv_delete_frac_2. intros.
destruct (denv_delete_frac_stack i ms)
......
......@@ -19,7 +19,7 @@ Section splitenv.
MapstoListFromEnv Γin Γout Γls
MapstoListFromEnv (Esnoc Γin i P) (Esnoc Γout i P) Γls | 100.
Proof.
destruct 1; split; simpl.
destruct 1; split; simpl.
- rewrite mapsto_list_from_env0. iIntros "(H1 & H2 & H3)". iFrame.
- intro Hwf. inversion Hwf; subst. apply mapsto_list_from_env_wf0 in H4.
apply Esnoc_wf; last done. by apply mapsto_list_from_env_lookup_None0.
......@@ -31,10 +31,9 @@ Section splitenv.
MapstoListFromEnv Γin Γout Γls
MapstoListFromEnv (Esnoc Γin i (l C[lvl]{q} v))
Γout
(PenvItem l lvl q v :: Γls).
(PenvItem l lvl q v :: Γls) | 3.
Proof.
destruct 1.
split.
destruct 1. split.
- iIntros "[H1 H2] /=". iFrame.
by rewrite mapsto_list_from_env0.
- intros Heq. inversion Heq; simplify_eq /=. by apply mapsto_list_from_env_wf0.
......@@ -43,6 +42,14 @@ Section splitenv.
by rewrite env_lookup_snoc_ne in Hsnoc.
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) :=
list_of_mapsto : penv_interp Γls denv_interp E ps.
......@@ -57,7 +64,7 @@ Section splitenv.
(denv_insert i x q dv ps).
Proof.
rewrite /LocLookup /ListOfMapsto /penv_interp=> Hi [-> ?] HΓls /=.
iIntros "[Hl H] /=". rewrite HΓls -denv_insert_interp /= Hi. iFrame.
iIntros "[Hl H] /=". rewrite HΓls -denv_insert_interp /= Hi cloc_plus_0. iFrame.
Qed.
Lemma tac_envs_split_mapsto Γs_in Γs_out Γls Γp c ps P:
......
......@@ -12,7 +12,7 @@ Section test.
l C v - awp (∗ᶜ ♯ₗl) True (λ w, w = v l C v).
Proof.
iIntros "Hl1". vcg_solver. auto.
Qed.
Qed.
(* double dereferencing *)
Lemma test2 (l1 l2 : cloc) (v: val) :
......
......@@ -9,7 +9,7 @@ Definition incr : val := λ: "l",
(a_ret "l") = (∗ᶜ (a_ret "l") + 1).
Definition factorial_body : val := λ: "n" "c" "r",
while ((∗ᶜ (a_ret "c")) < (a_ret "n"))
while (∗ᶜ (a_ret "c") < (a_ret "n"))
{ incr "c" ;
a_ret "r" = ((∗ᶜ (a_ret "r")) * (∗ᶜ (a_ret "c"))) }.
......@@ -22,11 +22,6 @@ Definition factorial : val := λ: "n",
Section factorial_spec.
Context `{amonadG Σ}.
Ltac etaprod l :=
compute[cloc_add];
rewrite ?Nat.add_0_r;
assert ((l.1, l.2) = l) as -> by (destruct l; auto).
Lemma incr_spec (l : cloc) (n : Z) R Φ :
l C #n - (l C[LLvl] #(n+1) - Φ #(n+1)) -
AWP incr (cloc_to_val l) @ R {{ Φ }}.
......@@ -61,8 +56,8 @@ Section factorial_spec.
AWP factorial #n @ R {{ v, v = #(fact n) }}%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret r "[Hr _]". etaprod r.
iApply awp_bind. awp_alloc_ret c "[Hc _]". etaprod c.
iApply awp_bind. awp_alloc_ret r "[Hr _]".
iApply awp_bind. awp_alloc_ret c "[Hc _]".
iApply a_sequence_spec'. iNext.
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.
......@@ -74,8 +69,8 @@ Section factorial_spec.
awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret r "[Hr _]". etaprod r.
iApply awp_bind. awp_alloc_ret c "[Hc _]". etaprod c.
iApply awp_bind. awp_alloc_ret r "[Hr _]".
iApply awp_bind. awp_alloc_ret c "[Hc _]".
iApply a_sequence_spec'. iNext. do 3 awp_lam.
iApply (a_while_inv_spec
(k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]").
......
......@@ -8,10 +8,6 @@ From iris_c.lib Require Import locking_heap U.
Section memcpy.
Context `{amonadG Σ}.
Ltac etaprod l :=
rewrite ?Nat.add_0_r;
assert ((l.1, l.2) = l) as -> by (destruct l; auto).
Definition memcpy : val := λ: "arg",
"p" ←ᶜ a_alloc 1 (a_ret (Fst "arg"));;
"q" ←ᶜ a_alloc 1 (a_ret (Fst (Snd "arg")));;
......@@ -94,12 +90,24 @@ Section memcpy.
q C ls2 -
AWP a_invoke memcpy (♯ₗp ||| (♯ₗq ||| n)) @ R {{ _, p C ls2 q C ls2 }}.
Proof.
iIntros (? ?) "Hp Hq".
iApply a_invoke_simpl. vcg_solver. iModIntro.
awp_lam. iApply awp_bind. vcg_solver. repeat awp_proj. iApply awp_ret; wp_value_head.
vcg_continue. iExists 1%nat; iSplit; first done.
iIntros ([pp ppi]) "[Hpp _]". vcg_continue. iIntros "Hll". awp_let.
iApply awp_bind. vcg_solver. (*
iIntros (? ?) "Hp Hq". iApply a_invoke_simpl. vcg_solver. iModIntro.
awp_lam. iApply awp_bind. vcg_solver. iExists 1%nat; iSplit; first done.
iIntros (pp) "[Hpp _]". vcg_continue. iIntros "Hpp". awp_let.
iApply awp_bind. vcg_solver. iIntros "Hpp". iExists 1%nat; iSplit; first done.
iIntros (qq) "[Hqq _]". vcg_continue. iIntros "Hpp Hqq". awp_let.
repeat awp_proj. awp_let.
set (e :=( while (∗ᶜ (a_ret (cloc_to_val (cloc_plus pp 0))) <∗ᶜ a_ret "pend") { (a_ret (cloc_to_val (cloc_plus pp 0)) +=
1) =
∗ᶜ (a_ret (cloc_to_val (cloc_plus qq 0)) +=
1) })%E).
Check awp_bind.
iApply awp_bind. unfold e. apply _.
vcg_solver.
iIntros "Hpp Hqq". cloc_to_val (c iExists 1%nat; iSplit; first done.
(*
awp_proj. iApply awp_ret; wp_value_head.
iNext. iIntros (? ->). iExists 1%nat. iSplit; eauto.
iIntros (pp) "[Hpp _]". rewrite {3}/cloc_add. etaprod pp.
......
......@@ -9,47 +9,40 @@ Section tests_vcg.
Context `{amonadG Σ}.
Definition swap : val := λ: "l1" "l2" "r",
(a_store (a_ret "r") (a_load (a_ret "l1"))) ;
(a_store (a_ret "l1") (a_load (a_ret "l2"))) ;
(a_store (a_ret "l2") (a_load (a_ret "r"))) ;
(a_ret #0).
(a_ret "r") = ∗ᶜ (a_ret "l1") ;
(a_ret "l1") = ∗ᶜ (a_ret "l2") ;
(a_ret "l2") = ∗ᶜ (a_ret "r") ;
().
Lemma swap_spec_by_vcg_opt (l1 l2 r : cloc) (v1 v2: val) R :
r C #0 - l1 C v1 l2 C v2 -
awp (swap (cloc_to_val l1) (cloc_to_val l2) (cloc_to_val r)) R (λ _, l2 C v1 l1 C v2).
Proof.
iIntros "Hr [Hl1 Hl2]". do 3 awp_lam.
vcg_solver. iIntros "!> !> !>". eauto with iFrame.
vcg_solver. iIntros "!> !> !> **". eauto with iFrame.
Qed.
Definition swap_with_alloc : val := λ: "l1" "l2",
a_bind (λ: "r",
(a_store (a_ret "r") (a_load (a_ret "l1"))) ;
(a_store (a_ret "l1") (a_load (a_ret "l2"))) ;
((a_store (a_ret "l2") (a_load (a_ret "r")))) ; a_ret #())
(a_alloc 1 0).
Lemma load_spec (l : loc ) (v1 v2: val) R :
(l,1%nat) C v1 -