Commit 5b5d7cbc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove dval_interp (insane).

parent b8549d28
......@@ -51,45 +51,27 @@ Section vcg.
Arguments Base _%I.
Fixpoint wp_interp (E : known_locs) (a : wp_expr) : iProp Σ :=
match a with
| Base P => P
| MapstoStar dl Φ =>
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)
| 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)
| IsLoc dv Φ =>
dl : dloc, dval_interp E dv = #(dloc_interp E dl) wp_interp E (Φ dl)
| UMod P => U (wp_interp E P)
end%I.
Fixpoint wp_interp_sane (E : known_locs) (a : wp_expr) : iProp Σ :=
match a with
| Base Φ => Φ
| MapstoStar dl Φ =>
q v, dloc_interp E dl C{q} v wp_interp_sane E (Φ q (dValUnknown v))
q v, dloc_interp E dl C{q} v wp_interp E (Φ q (dValUnknown v))
| MapstoStarFull dl Φ =>
v, dloc_interp E dl C{1} v wp_interp_sane E (Φ (dValUnknown v))
v, dloc_interp E dl C{1} v wp_interp E (Φ (dValUnknown v))
| MapstoWand dl dv x q Φ =>
dloc_interp E dl C[x]{q} dval_interp E dv - wp_interp_sane E Φ
dloc_interp E dl C[x]{q} dval_interp E dv - wp_interp E Φ
| IsSome dmx Φ =>
x, doption_interp dmx = Some x wp_interp_sane E (Φ x)
x, doption_interp dmx = Some x wp_interp E (Φ x)
| IsLoc dv Φ =>
l : loc, dval_interp E dv = #l wp_interp_sane E (Φ (dLocUnknown l))
| UMod P => U (wp_interp_sane E P)
l : loc, dval_interp E dv = #l wp_interp E (Φ (dLocUnknown l))
| UMod P => U (wp_interp E P)
end%I.
Fixpoint mapsto_wand_list_aux (m : denv) (Φ : wp_expr) (i : nat) : wp_expr :=
match m with
| [] => Φ
| dio :: m' =>
match dio with
| None => mapsto_wand_list_aux m' Φ (S i)
| Some (DenvItem x q dv) =>
MapstoWand (dLoc i) dv x q (mapsto_wand_list_aux m' Φ (S i))
end
| None :: m' => mapsto_wand_list_aux m' Φ (S i)
| Some (DenvItem x q dv) :: m' =>
MapstoWand (dLoc i) dv x q (mapsto_wand_list_aux m' Φ (S i))
end.
Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
......@@ -139,7 +121,7 @@ Section vcg.
E `prefix_of` E'
(denv_wf E' m')
denv_interp E' m'
wp_interp_sane E' (Φ E' m' dv))%I.
wp_interp E' (Φ E' m' dv))%I.
Arguments vcg_wp_unknown : simpl never.
Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
......@@ -230,24 +212,6 @@ End vcg.
Section vcg_spec.
Context `{amonadG Σ}.
Lemma wp_interp_sane_sound E a : wp_interp_sane E a wp_interp E a.
Proof.
generalize dependent E.
induction a.
- done.
- simpl. iIntros (E) "He". iDestruct "He" as (q v) "[H1 H2]".
iExists q, (dValUnknown v). iFrame. by (iApply H0).
- simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
iExists (dValUnknown v). simpl. iFrame. by (iApply H0).
- simpl. iIntros (E) "He H". iApply IHa. by iApply "He".
- simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
iExists v. iFrame. by iApply H0.
- 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.
Lemma mapsto_wand_list_aux_spec E m t (k : nat) :
wp_interp E (mapsto_wand_list_aux m t k) -
([ list] ndio m, from_option
......@@ -388,7 +352,6 @@ Section vcg_spec.
iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
iApply (awp_wand with "Hwp"). iIntros (v) "H".
iDestruct "H" as (E' m' dv ->) "(% & % & Hm & Hwp)".
rewrite wp_interp_sane_sound.
iExists E', dv, m'. repeat (iSplit; first done); iFrame.
Qed.
......@@ -410,17 +373,17 @@ Section vcg_spec.
rewrite Hm0. iSplit; first done. eauto with iFrame.
* rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
iSpecialize ("Hwp" with "Hm"). simpl.
iDestruct "Hwp" as (q dv') "[Hl Hwp]". apply is_dloc_some in Hdloc. subst.
iExists (dloc_interp E (dLoc i)), q, (dval_interp E dv'). iSplit; first done.
iDestruct "Hwp" as (q v') "[Hl Hwp]". apply is_dloc_some in Hdloc. subst.
iExists (dloc_interp E (dLoc i)), q, v'. iSplit; first done.
iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists E, dv', []; repeat (iSplit; first done); iFrame.
iExists E, (dValUnknown v'), []; repeat (iSplit; first done); iFrame.
unfold denv_interp, denv_wf. eauto.
+ rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
iSpecialize ("Hwp" with "Hm"); simpl.
iDestruct "Hwp" as (dl) "(-> & Hwp)". iDestruct "Hwp" as (q dv') "[Hl Hwp]".
iExists (dloc_interp E dl), q, (dval_interp E dv'). iSplit; first done.
iDestruct "Hwp" as (l) "(-> & Hwp)". iDestruct "Hwp" as (q v') "[Hl Hwp]".
iExists l, q, v'. iSplit; first done.
iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists E, dv', []; iSplit; first done. iFrame. unfold denv_interp, denv_wf. eauto.
iExists E, (dValUnknown v'), []; iSplit; first done. iFrame. unfold denv_interp, denv_wf. eauto.
Qed.
Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
......@@ -599,7 +562,7 @@ Section vcg_spec.
ListOfMapsto Γls E m
IntoDCexpr E e de
environments.envs_entails (environments.Envs Γp Γs_out c)
(wp_interp_sane E (vcg_wp E m de R (λ E m dv,
(wp_interp E (vcg_wp E m de R (λ E m dv,
mapsto_wand_list m $ Base (Φ (dval_interp E dv)))))
environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Proof.
......@@ -608,7 +571,7 @@ Section vcg_spec.
eapply tac_envs_split_mapsto; try eassumption.
revert Hgoal. rewrite environments.envs_entails_eq.
rewrite (vcg_wp_correct R); last done.
iIntros (->) "H1 H2". rewrite wp_interp_sane_sound.
iIntros (->) "H1 H2".
iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre) "(-> & Hmwf & Hm & Hwp)".
rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment