Skip to content
GitLab
Commit ecdbeb34 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Build optimizer into vcg_wp. 

All proofs are broken.
parent 30ea6a8d
Hide whitespace changes
Inline Side-by-side
theories/vcgen/denv.v
View file @ ecdbeb34
......@@ -49,6 +49,19 @@ Section denv.
| S i => None :: denv_singleton i lv q dv
end.
Fixpoint denv_lookup (i : nat) (m: denv) : option (frac * dval) :=
match m with
| [] => None
| dio :: m' =>
match i with
| O =>
''(DenvItem lv q dv) ← dio;
guard (lv = ULvl);
Some (q, dv)
| S i => denv_lookup i m'
end
end.
Fixpoint denv_insert (i : nat) (x: lvl) (q: frac) (dv: dval) (m: denv) : denv :=
match m with
| [] => denv_singleton i x q dv
......@@ -62,16 +75,6 @@ Section denv.
end
end.
Fixpoint denv_replace_full (i : nat) (dv: dval) (m: denv) : option denv :=
match m with
| [] => None
| dio :: m' =>
match i with
| O => '' _ ← dio; Some (Some (DenvItem LLvl 1%Qp dv) :: m')
| S i => m' ← denv_replace_full i dv m'; Some (dio :: m')
end
end.
Fixpoint denv_delete_frac (i : nat) (m : denv) : option (denv * frac * dval) :=
match m with
| [] => None
......@@ -146,13 +149,6 @@ Section denv_spec.
denv_interp E m1 ∗ denv_interp E m2 ⊣⊢ denv_interp E (denv_merge m1 m2).
Proof. Admitted.
Lemma denv_replace_interp E m i dv m':
denv_replace_full i dv m = Some m' →
∃ x q dv0 m0,
(denv_interp E m0 ∗ dloc_interp E (dLoc i) ↦C[x]{q} dval_interp E dv0 ⊣⊢ denv_interp E m) ∧
(denv_interp E m0 ∗ dloc_interp E (dLoc i) ↦C[LLvl]{1} dval_interp E dv ⊣⊢ denv_interp E m').
Proof. Admitted.
Lemma denv_delete_frac_interp E i m m' q dv :
denv_delete_frac i m = Some (m', q, dv) →
denv_interp E m' ∗ dloc_interp E (dLoc i) ↦C{q} dval_interp E dv ⊣⊢ denv_interp E m.
......
theories/vcgen/test.v
View file @ ecdbeb34
......@@ -18,7 +18,7 @@ Section tests_vcg.
awp (a_store (a_ret #s) (a_load (a_ret #l))) R (λ _, s ↦C[LLvl] #1 ∗ l ↦C #1).
Proof.
iIntros "Hs Hl".
vcg_opt_solver. rewrite Qp_half_half. eauto with iFrame.
vcg_solver. eauto with iFrame.
Qed.
Lemma store_load_load (s1 s2 l : loc) R :
......@@ -27,21 +27,33 @@ Section tests_vcg.
(a_bin_op PlusOp (a_load (a_ret #s1)) (a_ret #42))) R (λ _, s1 ↦C #1 ∗ l ↦C #1).
(* (a_store (a_ret #s2) (a_load (a_ret #l)))) R (λ _, s1 ↦U #1 ∗ l ↦U #1). *)
Proof.
iIntros "Hs1 Hl Hs2".
iApply (a_sequence_spec). vcg_opt_solver.
iIntros "Hs2 Hl Hs1". iModIntro. awp_lam. vcg_opt_solver. rewrite Qp_half_half.
eauto with iFrame.
iIntros "Hs1 Hl Hs2". vcg_solver. iModIntro.
rewrite Qp_half_half. eauto with iFrame.
Qed.
Lemma test3 (l : loc) :
l ↦C #1 -∗
awp (a_bin_op PlusOp (a_store (a_ret #l) (a_ret #2))
(a_store (a_ret #l) (a_ret #2)))%E True (λ v, True).
Proof. iIntros "Hl". vcg_opt_solver. Abort.
Proof. iIntros "Hl". vcg_solver. Abort.
Lemma test4 (l : loc) (e: expr) `{Closed [] e}:
(∀ Φ, Φ #10 -∗ awp e True Φ) -∗
l ↦C #1 -∗
awp (a_bin_op PlusOp (a_store (a_ret #l) (a_ret #2))
e) True (λ v, True).
Proof. iIntros "Hl". vcg_opt_solver. Abort.
Proof.
iIntros "He Hl". vcg_solver.
iApply "He".
(* Now we need some way to mechanically continue, i.e run the
optimizer now. *)
(* What I do here is a way to do so, but it's not really right:
- We need to reify everything again. New constants or locations could have
been introduced like the `#10` in this example.
- `simpl` will probably unfold too much, and as such, it does not work in
a nested fashion. *)
iApply (optimize_sound []);
[iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
iExists (dValUnknown (#12)). done.
Qed.
End tests_vcg.
theories/vcgen/tests/swap.v
View file @ ecdbeb34
......@@ -19,26 +19,6 @@ Section tests_vcg.
awp (swap #l1 #l2 #r) R (λ _, l2 ↦C #1 ∗ l1 ↦C #2).
Proof.
iIntros "Hr [Hl1 Hl2]". do 3 awp_lam.
vcg_opt_solver. simpl. eauto with iFrame.
Qed.
Lemma swap_spec_by_vcg (l1 l2 r : loc) (v1 v2: nat) R :
r ↦C #0 -∗ l1 ↦C #1 ∗ l2 ↦C #2 -∗
awp (swap #l1 #l2 #r) R (λ _, l2 ↦C #1 ∗ l1 ↦C #2).
Proof.
iIntros "Hr [Hl1 Hl2]". do 3 awp_lam.
vcg_solver. compute[denv_interp]. simpl.
iIntros "(Hl2 & Hl1 & Hr & _)". iFrame.
iIntros "Hl2 Hl1 Hr".
iExists l1; iSplit; first done. iExists 1%Qp, #1. iFrame "Hl1". iIntros "Hl1".
iExists #0. iFrame "Hr". iIntros "Hr". iModIntro. iFrame.
iIntros "Hl2 Hl1 Hr". iExists (dLoc 0); iSplit; first done. simpl. iExists 1%Qp, (dLitV (dLitInt 2)).
iFrame "Hl2". simpl. iIntros "Hl2". iExists (dLitV (dLitInt 1)). iFrame "Hl1". iIntros "Hl1".
iModIntro. iFrame.
iIntros "Hl2 Hl1 Hr". iExists (dLoc 2); iSplit; first done. simpl. iExists 1%Qp, (dLitV (dLitInt 1)).
iFrame "Hr". iIntros "Hr". iExists (dLitV (dLitInt 2)). simpl. iFrame "Hl2". iIntros "Hl2".
iModIntro. iFrame.
vcg_solver. iIntros "!> !> !>". eauto with iFrame.
Qed.
End tests_vcg.
theories/vcgen/vcgen.v
View file @ ecdbeb34
......@@ -23,7 +23,6 @@ Section vcg.
| Base : iProp Σ → wp_expr
| MapstoStar : dloc → (frac → dval → wp_expr) → wp_expr
| MapstoStarFull : dloc → (dval → wp_expr) → wp_expr
| MapstoStarKnown : dloc → dval → lvl → frac → wp_expr → wp_expr
| MapstoWand : dloc → dval → lvl → frac → wp_expr → wp_expr
| IsSome {A} : doption A → (A → wp_expr) → wp_expr
| IsLoc : dval → (dloc → wp_expr) → wp_expr
......@@ -38,8 +37,6 @@ Section vcg.
∃ q dv, dloc_interp E dl ↦C{q} dval_interp E dv ∗ wp_interp E (Φ q dv)
| MapstoStarFull dl Φ =>
∃ dv, dloc_interp E dl ↦C{1} dval_interp E dv ∗ wp_interp E (Φ dv)
| MapstoStarKnown dl dv x q Φ =>
dloc_interp E dl ↦C[x]{q} dval_interp E dv ∗ wp_interp E Φ
| MapstoWand dl dv x q Φ =>
dloc_interp E dl ↦C[x]{q} dval_interp E dv -∗ wp_interp E Φ
| IsSome dmx Φ => ∃ x, ⌜doption_interp dmx = Some x⌝ ∧ wp_interp E (Φ x)
......@@ -55,8 +52,6 @@ Section vcg.
∃ q v, dloc_interp E dl ↦C{q} v ∗ wp_interp_sane E (Φ q (dValUnknown v))
| MapstoStarFull dl Φ =>
∃ v, dloc_interp E dl ↦C{1} v ∗ wp_interp E (Φ (dValUnknown v))
| MapstoStarKnown dl dv x q Φ =>
dloc_interp E dl ↦C[x]{q} dval_interp E dv ∗ wp_interp_sane E Φ
| MapstoWand dl dv x q Φ =>
dloc_interp E dl ↦C[x]{q} dval_interp E dv -∗ wp_interp_sane E Φ
| IsSome dmx Φ =>
......@@ -80,177 +75,161 @@ Section vcg.
Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
mapsto_wand_list_aux m Φ O.
Fixpoint mapsto_star_list_aux (m : denv) (Φ : wp_expr) (i : nat) : wp_expr :=
match m with
| [] => Φ
| dio :: m' =>
match dio with
| None => mapsto_star_list_aux m' Φ (S i)
| Some (DenvItem x q dv) =>
MapstoStarKnown (dLoc i) dv x q (mapsto_star_list_aux m' Φ (S i))
end
end.
Definition mapsto_star_list (m : denv) (Φ : wp_expr) : wp_expr :=
mapsto_star_list_aux m Φ O.
Fixpoint vcg_sp (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
match de with
| dCRet dv => Some (m, nil, dv)
| dCLoad de1 =>
''(mIn, mOut, dl) ← vcg_sp E m de1;
i ← is_dloc E dl;
''(mIn1, q, dv) ← denv_delete_frac i mIn;
Some (mIn1, denv_insert i ULvl q dv mOut, dv)
''(mIn, mOut, dl) ← vcg_sp E m de1;
i ← is_dloc E dl;
''(mIn1, mOut2, q, dv) ← denv_delete_frac_2 i mIn mOut;
Some (mIn1, denv_insert i ULvl q dv mOut2, dv)
| dCStore de1 de2 =>
''(mIn1, mOut1, dl) ← vcg_sp E m de1;
i ← is_dloc E dl;
''(mIn2, mOut2, dv) ← vcg_sp E mIn1 de2;
''(mIn3, mOut3, _) ← denv_delete_full_2 i mIn2 (denv_merge mOut1 mOut2);
Some (mIn3, denv_insert i LLvl 1%Qp dv mOut3, dv)
''(mIn1, mOut1, dl) ← vcg_sp E m de1;
i ← is_dloc E dl;
''(mIn2, mOut2, dv) ← vcg_sp E mIn1 de2;
''(mIn3, mOut3, _) ← denv_delete_full_2 i mIn2 (denv_merge mOut1 mOut2);
Some (mIn3, denv_insert i LLvl 1 dv mOut3, dv)
| dCBinOp op de1 de2 =>
''(mIn1, mOut1, dv1) ← vcg_sp E m de1;
''(mIn2, mOut2, dv2) ← vcg_sp E mIn1 de2;
match dbin_op_eval E op dv1 dv2 with
| dSome dv => Some (mIn2, denv_merge mOut1 mOut2, dv)
| dNone | dUnknown _ => None
(* | dUnknown (Some dv) => RK: probably just fail with None *)
end
''(mIn1, mOut1, dv1) ← vcg_sp E m de1;
''(mIn2, mOut2, dv2) ← vcg_sp E mIn1 de2;
match dbin_op_eval E op dv1 dv2 with
| dSome dv => Some (mIn2, denv_merge mOut1 mOut2, dv)
| dNone | dUnknown _ => None
end
| dCUnOp op de =>
''(mIn, mOut, dv) ← vcg_sp E m de;
''(mIn, mOut, dv) ← vcg_sp E m de;
match dun_op_eval E op dv with
| dSome dv' => Some (mIn, mOut, dv')
| dNone | dUnknown _ => None
end
| dCSeq de1 de2 =>
''(mIn1, mOut1, _) ← vcg_sp E m de1;
''(mIn2, mOut2, dv2) ← vcg_sp E mIn1 de2;
(*TODO: can we improve it with (denv_unlock mIn1) instead of mIn1 *)
Some (mIn2, denv_merge (denv_unlock mOut1) mOut2, dv2)
''(mIn1, mOut1, _) ← vcg_sp E m de1;
''(mIn2, mOut2, dv2) ← vcg_sp E (denv_unlock mIn1) de2;
Some (mIn2, denv_merge (denv_unlock mOut1) mOut2, dv2)
| dCAlloc _ | dCUnknown _ => None
end.
Fixpoint vcg_wp (E: known_locs) (m: denv) (de : dcexpr) (R : iProp Σ) (Φ : denv → dval → wp_expr) : wp_expr :=
match de with
| dCRet dv => Φ m dv
| dCLoad de1 =>
vcg_wp E m de1 R (λ m' dv, IsLoc dv (λ l, MapstoStar l (λ q w, MapstoWand l w ULvl q (Φ m' w))))
| dCStore de1 de2 =>
match vcg_sp E m de1 with
| Some (mIn, mOut, dv1) =>
match dv1 with
| dLitV (dLitLoc (dLoc i)) =>
mapsto_star_list m
(mapsto_wand_list mIn
(vcg_wp E mIn de2 R (λ m' dv2,
mapsto_wand_list mOut
(MapstoStarFull (dLoc i) (λ _, MapstoWand (dLoc i) dv2 LLvl 1
match denv_replace_full i dv2 m' with
| Some mf => (Φ mf dv2)
| None => Base False (*TODO: maybe this is too strong, return just (Φ m' dv2) *)
end)))))
| dLitV (dLitInt _) | dLitV (dLitBool _) | dLitV dLitUnit => Base False
| _ =>
IsLoc dv1 (λ dl,
mapsto_star_list m
(mapsto_wand_list mIn
(vcg_wp E mIn de2 R (λ m' dv2,
mapsto_wand_list mOut
(MapstoStarFull dl (λ _,
(MapstoWand dl dv2 LLvl 1%Qp (Φ m' dv2))))))))
end
| None => (*TODO: maybe this brunch also needs modification of the environment m' *)
match vcg_sp E m de2 with
| Some (mIn, mOut, dv2) =>
mapsto_star_list m
(mapsto_wand_list mIn
(vcg_wp E mIn de1 R (λ m' dv1,
IsLoc dv1 (λ dl,
mapsto_wand_list mOut
(MapstoStarFull dl
(λ _, MapstoWand dl dv2 LLvl 1
(Φ m' dv2 )))))))
| None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ m (dValUnknown v))))
end
end
| dCBinOp op de1 de2 =>
match vcg_sp E m de1 with
| Some (mIn, mOut, dv1) =>
mapsto_star_list m
(mapsto_wand_list mIn (vcg_wp E mIn de2 R (λ m' dv2,
mapsto_wand_list mOut (IsSome (dbin_op_eval E op dv1 dv2) (Φ (denv_merge mOut m'))))))
| None =>
match vcg_sp E m de2 with
| Some (mIn, mOut, dv2) =>
mapsto_star_list m
(mapsto_wand_list mIn (vcg_wp E mIn de1 R (λ m' dv1,
mapsto_wand_list mOut (IsSome (dbin_op_eval E op dv1 dv2) (Φ (denv_merge mOut m'))))))
| None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ m (dValUnknown v))))
end
end
| dCUnOp op de => vcg_wp E m de R (λ m' dv, IsSome (dun_op_eval E op dv) (Φ m'))
| dCSeq de1 de2 => vcg_wp E m de1 R (λ m' _, UMod (vcg_wp E (denv_unlock m') de2 R Φ))
| _ => Base (awp (dcexpr_interp E de) R (λ v, wp_interp_sane E (Φ m (dValUnknown v))))
end.
Fixpoint optimize (m : denv) (Φ : wp_expr) : wp_expr :=
match Φ with
| Base Φ1 => mapsto_wand_list m Φ
| Base Φ1 => Base Φ1
| MapstoStar (dLoc i) Φ1 =>
match denv_delete_frac i m with
| Some (m1, q1, dv) => optimize m1 (Φ1 q1 dv)
| None => MapstoStar (dLoc i) (λ q dv, optimize m (Φ1 q dv))
end
match denv_delete_frac i m with
| Some (m1, q1, dv) => optimize m1 (Φ1 q1 dv)
| None => MapstoStar (dLoc i) (λ q dv, optimize m (Φ1 q dv))
end
| MapstoStarFull (dLoc i) Φ1 =>
match denv_delete_full i m with
| Some (m1, dv) => optimize m1 (Φ1 dv)
| None => MapstoStarFull (dLoc i) (λ dv, optimize m (Φ1 dv))
end
| MapstoStarKnown (dLoc i) dv x q Φ1 =>
if (bool_decide (q = 1%Qp))
then
match denv_delete_full i m with
| Some (m1, dv1) =>
if bool_decide (dv = dv1) then optimize m1 Φ1
else MapstoStarKnown (dLoc i) dv x Qp_one (optimize m Φ1)
| None => MapstoStarKnown (dLoc i) dv x 1 (optimize m Φ1)
end
else
match denv_delete_frac i m with
| Some (m1, q1, dv1) =>
(*TODO: here we still have an issue with frac. *)
if (bool_decide (q = q1) && bool_decide (dv = dv1))
then optimize m1 Φ1
else MapstoStarKnown (dLoc i) dv x q (optimize m Φ1)
| None => MapstoStarKnown (dLoc i) dv x q (optimize m Φ1)
end
match denv_delete_full i m with
| Some (m1, dv) => optimize m1 (Φ1 dv)
| None => MapstoStarFull (dLoc i) (λ dv, optimize m (Φ1 dv))
end
| MapstoWand (dLoc i) dv x q Φ1 => optimize (denv_insert i x q dv m) Φ1
| MapstoStar dl Φ1 => MapstoStar dl (λ q dv, optimize m (Φ1 q dv))
| MapstoStarFull dl Φ1 => MapstoStarFull dl (λ dv, optimize m (Φ1 dv))
| MapstoStarKnown dl dv x q Φ1 => MapstoStarKnown dl dv x q (optimize m Φ1)
| MapstoWand dl w x q Φ1 => MapstoWand dl w x q (optimize m Φ1)
| IsSome dmx Φ1 =>
match dmx with
| dNone => Base False
| dSome x => optimize m (Φ1 x)
| _ => IsSome dmx (λ v, optimize m (Φ1 v))
end
match dmx with
| dNone => Base False
| dSome x => optimize m (Φ1 x)
| _ => IsSome dmx (λ v, optimize m (Φ1 v))
end
| IsLoc dv Φ1 =>
match dv with
| dLitV (dLitLoc l) => optimize m (Φ1 l)
| dLitV (dLitUnknown _) | dValUnknown _ => IsLoc dv (λ v, optimize m (Φ1 v))
| _ => Base False
end
match dv with
| dLitV (dLitLoc l) => optimize m (Φ1 l)
| dLitV (dLitUnknown _) | dValUnknown _ => IsLoc dv (λ v, optimize m (Φ1 v))
| _ => Base False
end
| UMod Φ => optimize (denv_unlock m) Φ
end.
Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
(Φ : denv → dval → wp_expr) : wp_expr :=
match is_dloc E dv with
| Some i =>
match denv_lookup i m with
| Some (_, dw) => Φ m dw
| None =>
mapsto_wand_list m $ MapstoStar (dLoc i) $ λ q dw,
MapstoWand (dLoc i) dw ULvl q (Φ [] dw)
end
| _ => Base False
end.
Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
(Φ : denv → dval → wp_expr) : wp_expr :=
match is_dloc E dv1 with
| Some i =>
match denv_delete_full i m with
| Some (m', dw) => Φ (denv_insert i LLvl 1 dv2 m') dv2
| None =>
mapsto_wand_list m $ MapstoStarFull (dLoc i) $ λ _,
MapstoWand (dLoc i) dv2 LLvl 1 (Φ [] dv2)
end
| _ => Base False
end.
Definition vcg_wp_bin_op (E : known_locs) (op : bin_op) (dv1 dv2 : dval)
(m : denv) (Φ : denv → dval → wp_expr) : wp_expr :=
match dbin_op_eval E op dv1 dv2 with
| dSome dw => Φ m dw
| mdw => mapsto_wand_list m $ IsSome mdw (Φ [])
end.
Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
(R : iProp Σ) (Φ : denv → dval → wp_expr) : wp_expr :=
match de with
| dCRet dv => Φ m dv
| dCLoad de1 =>
vcg_wp E m de1 R (λ m' dv, vcg_wp_load E dv m Φ)
| dCStore de1 de2 =>
match vcg_sp E m de1 with
| Some (mIn, mOut, dv1) =>
vcg_wp E mIn de2 R (λ mIn dv2,
vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) Φ)
| None =>
match vcg_sp E m de2 with
| Some (mIn, mOut, dv2) =>
vcg_wp E mIn de1 R (λ mIn dv1,
vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) Φ)
| None =>
mapsto_wand_list m $ Base $
awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ [] (dValUnknown v)))
end
end
| dCBinOp op de1 de2 =>
match vcg_sp E m de1 with
| Some (mIn, mOut, dv1) =>
vcg_wp E mIn de2 R (λ mIn dv2,
vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) Φ)
| None =>
match vcg_sp E m de2 with
| Some (mIn, mOut, dv2) =>
vcg_wp E mIn de1 R (λ mIn dv1,
vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) Φ)
| None =>
mapsto_wand_list m $ Base $
awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ [] (dValUnknown v)))
end
end
| dCUnOp op de =>
vcg_wp E m de R (λ m dv,
match dun_op_eval E op dv with
| dSome dw => Φ m dw
| mdw => IsSome mdw (Φ m)
end)
| dCSeq de1 de2 =>
vcg_wp E m de1 R (λ m _,
UMod (vcg_wp E (denv_unlock m) de2 R Φ))
| _ =>
mapsto_wand_list m $ Base $
awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ [] (dValUnknown v)))
end.
End vcg.
Section vcg_spec.
Context `{amonadG Σ}.
Lemma wp_interp_sane_sound E a : wp_interp_sane E a ⊢ wp_interp E a.
Proof.
Proof. (*
generalize dependent E.
induction a.
- done.
......@@ -266,8 +245,9 @@ Section vcg_spec.
- simpl. iIntros (E) "He". iDestruct "He" as (l) "[H1 H2]".
iExists (dLocUnknown l). simpl. iFrame. by iApply H0.
- simpl. intros E. by apply U_mono.
Qed.
Qed. *) Admitted.
(*
Lemma mapsto_star_list_spec E m t :
wp_interp E (mapsto_star_list m t) -∗ denv_interp E m ∗ wp_interp E t.
Proof.
......@@ -292,8 +272,8 @@ Section vcg_spec.
Lemma vcg_sp_correct E m de mIn mOut dv R :
vcg_sp E m de = Some (mIn, mOut, dv) →
denv_interp E m -∗
denv_interp E mIn ∗
awp (dcexpr_interp E de) R (λ v, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mOut).
denv_interp E mIn ∗
awp (dcexpr_interp E de) R (λ v, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mOut).
Proof.
revert m mIn mOut dv. induction de;
iIntros (m mIn mOut dv Hsp) "Hm"; simplify_eq/=.
......@@ -374,8 +354,9 @@ Section vcg_spec.
Qed.
Lemma vcg_wp_correct R E m de Φ :
wp_interp E (vcg_wp E m de R Φ) ⊢
awp (dcexpr_interp E de) R
denv_interp E m -∗
wp_interp E (vcg_wp E m de R Φ) -∗
awp (dcexpr_interp E de) R
(λ v, ∃ dv m', ⌜dval_interp E dv = v⌝ ∧ wp_interp E (Φ m' dv)).
Proof.
revert Φ m. induction de; intros Φ m.
......@@ -507,11 +488,12 @@ Section vcg_spec.
- iIntros "Hawp". iApply (awp_wand with "Hawp"). iIntros (v) "H".
rewrite wp_interp_sane_sound. iExists _,_; iFrame; eauto.
Qed.
*)
Lemma optimize_sound (m: denv) E (Φ: wp_expr) :
wp_interp E (optimize m Φ) -∗
denv_interp E m -∗ (wp_interp E Φ).
Proof.
Proof. (*
generalize dependent m.
induction Φ; simpl; intros m.
- rewrite mapsto_wand_list_spec /=; done.
......@@ -586,7 +568,8 @@ Section vcg_spec.
- iIntros "HΦ Hm".
rewrite IHΦ. iDestruct (denv_unlock_interp with "Hm") as "Hm".
iModIntro. by iApply "HΦ".
Qed.
*)
Admitted.
Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
MapstoListFromEnv Γs_in Γs_out Γls →
......@@ -594,19 +577,13 @@ Section vcg_spec.
ListOfMapsto Γls E m →
IntoDCexpr E e dce →
environments.envs_entails (environments.Envs Γp Γs_out c)
(denv_interp E m -∗ wp_interp E (vcg_wp E m dce R (λ _ dv, Base (Φ (dval_interp E dv))))) →
(wp_interp_sane E (vcg_wp E m dce R (λ m dv,
mapsto_wand_list m $ Base (Φ (dval_interp E dv))))) →
environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Proof.
rewrite /IntoDCexpr /=. intros Hsplit ->.
rewrite /ListOfMapsto. intros Hexhale -> Hgoal.
eapply tac_envs_split_mapsto; try eassumption.
revert Hgoal. rewrite environments.envs_entails_eq.
rewrite (vcg_wp_correct R).
intros ->. iIntros "H1 H2".
iSpecialize ("H1" with "H2"). iApply (awp_wand with "H1").
iIntros (v) "H". by iDestruct "H" as (dv _) "[-> H]".
Qed.
Admitted.
(*
Lemma tac_vcg_opt_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
MapstoListFromEnv Γs_in Γs_out Γls →
E = penv_to_known_locs Γls →
......@@ -620,16 +597,20 @@ Section vcg_spec.
revert Hgoal. rewrite environments.envs_entails_eq. intros ->.
rewrite wp_interp_sane_sound optimize_sound. done.
Qed.
*)
End vcg_spec.
Arguments wp_interp : simpl never.
Ltac vcg_solver :=
eapply tac_vcg_sound;
[ apply _ (* MapstoListFromEnv Γs_in Γs_out Γls *)
| compute; reflexivity (* E = penv_to_known_locs Γls *)
| apply _ (* ListOfMapsto Γls E m *)
| apply _ (* IntoDCexpr E e dce *)
|