Commit 9fe45fba authored by Léon Gondelman's avatar Léon Gondelman
Browse files

bye bye wp_expr.

parent ee9d4038
......@@ -12,10 +12,10 @@ TODO
simpl never)
- Write more tests with unknown stuff in it
add tests like `!(l := 10;;;; l)`
- Support alloc in `vcg_wp`
[DONE] Support alloc in `vcg_wp`
- Automatically come up with the new `E`, `m` and `dv` and stuff in the unknown case
- Finish the proofs
- Maybe drop `wp_expr`? We are not taking it as an input of anything anymore
[DONE] Maybe drop `wp_expr`? We are not taking it as an input of anything anymore
Less urgent TODO
......@@ -37,45 +37,16 @@ Inductive dfrac :=
Section vcg.
Context `{amonadG Σ}.
(** Deep embedding of formulae used to build the verification condition generator *)
Inductive wp_expr :=
| Base : iProp Σ wp_expr
| MapstoStar : dloc (frac dval wp_expr) wp_expr
| MapstoStarFull : dloc (dval 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
| UMod : wp_expr wp_expr.
Arguments Base _%I.
Fixpoint wp_interp (E : known_locs) (a : wp_expr) : iProp Σ :=
match a with
| Base Φ => Φ
| MapstoStar dl Φ =>
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 E (Φ (dValUnknown v))
| 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 Φ =>
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 :=
Fixpoint mapsto_wand_list_aux (E: known_locs) (m : denv) (Φ : iProp Σ) (i : nat) : iProp Σ :=
match m with
| [] => Φ
| None :: m' => mapsto_wand_list_aux m' Φ (S i)
| None :: m' => mapsto_wand_list_aux E m' Φ (S i)
| Some (DenvItem x q dv) :: m' =>
MapstoWand (dLoc i) dv x q (mapsto_wand_list_aux m' Φ (S i))
end.
dloc_interp E (dLoc i) C[x]{q} dval_interp E dv - mapsto_wand_list_aux E m' Φ (S i)
end%I.
Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
mapsto_wand_list_aux m Φ O.
Definition mapsto_wand_list (E: known_locs) (m : denv) (Φ : iProp Σ ) : iProp Σ :=
mapsto_wand_list_aux E m Φ O.
Definition popstack (mOut : list denv) : option (list denv * denv) :=
......@@ -84,7 +55,7 @@ Section vcg.
| m::ms => Some (ms, m)
end.
Fixpoint vcg_sp (E: known_locs) (mIn : denv) (mOut : list denv) (de : dcexpr)
Fixpoint vcg_sp (E: known_locs) (mIn : denv) (mOut : list denv) (de : dcexpr)
: option (denv * list denv * denv * dval) :=
match de with
| dCRet dv => Some (mIn, mOut, [], dv)
......@@ -122,60 +93,62 @@ Section vcg.
Definition vcg_wp_unknown (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv)
(Φ : known_locs denv dval wp_expr) : wp_expr :=
mapsto_wand_list m $ Base $
awp (dcexpr_interp E de) R (λ v,
(Φ : known_locs denv dval iProp Σ) : iProp Σ :=
mapsto_wand_list E m
(awp (dcexpr_interp E de) R (λ v,
E' m' dv,
v = dval_interp E' dv
E `prefix_of` E'
(denv_wf E' m')
dval_wf E' dv
denv_interp E' m'
wp_interp E' (Φ E' m' dv))%I.
(Φ E' m' dv)))%I.
Arguments vcg_wp_unknown : simpl never.
Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
(Φ : denv dval wp_expr) : wp_expr :=
(Φ : denv dval iProp Σ) : iProp Σ :=
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)
mapsto_wand_list E m ( q v,
dloc_interp E (dLoc i) C{q} v
(dloc_interp E (dLoc i) C[ULvl]{q} dval_interp E (dValUnknown v) -
Φ [] (dValUnknown v)))
end
| _ =>
mapsto_wand_list m $ IsLoc dv (λ dl,
MapstoStar dl $ λ q dw,
MapstoWand dl dw ULvl q (Φ [] dw))
end.
| _ => mapsto_wand_list E m ( l : loc, dval_interp E dv = #l
( q v, l C{q} v (l C{q} v - Φ [] (dValUnknown v))))%I
end%I.
Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
(Φ : denv dval wp_expr) : wp_expr :=
(Φ : denv dval iProp Σ) : iProp Σ :=
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)
mapsto_wand_list E m ( v : val,
dloc_interp E (dLoc i) C v
(dloc_interp E (dLoc i) C[LLvl] dval_interp E dv2 - Φ [] dv2))
end
| _ =>
mapsto_wand_list m $ IsLoc dv1 (λ dl,
MapstoStarFull dl $ λ _,
MapstoWand dl dv2 LLvl 1 (Φ [] dv2))
end.
mapsto_wand_list E m ( l : loc,
dval_interp E dv1 = #l v : val,
dloc_interp E (dLocUnknown l) C v
(dloc_interp E (dLocUnknown l) C[LLvl] dval_interp E dv2 - Φ [] dv2))%I
end%I.
Definition vcg_wp_bin_op (E : known_locs) (op : bin_op) (dv1 dv2 : dval)
(m : denv) (Φ : denv dval wp_expr) : wp_expr :=
(m : denv) (Φ : denv dval iProp Σ) : iProp Σ :=
match dbin_op_eval E op dv1 dv2 with
| dSome dw => Φ m dw
| dUnknown (Some dw) => Φ m dw
| _ => Base False
end.
| _ => False
end%I.
Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
(R : iProp Σ) (Φ : known_locs denv dval wp_expr) : wp_expr :=
(R : iProp Σ) (Φ : known_locs denv dval iProp Σ) : iProp Σ :=
match de with
| dCRet dv => Φ E m dv
| dCLoad de1 =>
......@@ -210,24 +183,23 @@ Section vcg.
vcg_wp E m de R (λ E m dv,
match dun_op_eval E op dv with
| dSome dw => Φ E m dw
| mdw => IsSome mdw (Φ E m)
| mdw => x, doption_interp mdw = Some x Φ E m x
end)
| dCSeq de1 de2 =>
vcg_wp E m de1 R (λ E m _,
UMod (vcg_wp E (denv_unlock m) de2 R Φ))
U (vcg_wp E (denv_unlock m) de2 R Φ))
| _ => vcg_wp_unknown R E de m Φ
end.
end%I.
End vcg.
Section vcg_spec.
Context `{amonadG Σ}.
Lemma mapsto_wand_list_aux_spec E m t (k : nat) :
wp_interp E (mapsto_wand_list_aux m t k) -
Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
mapsto_wand_list_aux E m Φ k -
([ list] ndio m, from_option
(λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
default 1%positive (E !! (k + n)%nat) C[lv]{q} dval_interp E dv) True dio) -
wp_interp E t.
(λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
default 1%positive (E !! (k + n)%nat) C[lv]{q} dval_interp E dv) True dio) - Φ.
Proof.
generalize dependent k.
induction m; simpl. eauto.
......@@ -240,8 +212,8 @@ Section vcg_spec.
intros n y ?. simpl. assert ((k + S n)%nat = (S k + n)%nat) as -> by omega. done.
Qed.
Lemma mapsto_wand_list_spec E m t :
wp_interp E (mapsto_wand_list m t) - denv_interp E m - wp_interp E t.
Lemma mapsto_wand_list_spec E m Φ :
mapsto_wand_list E m Φ - denv_interp E m - Φ.
Proof.
unfold mapsto_wand_list, denv_interp.
iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
......@@ -292,7 +264,6 @@ Section vcg_spec.
denv_interp E mIn'
denv_stack_interp (reverse mOut) (reverse mOut') E
(awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv denv_interp E mNew'))).
Proof.
Proof.
revert mIn mOut mIn' mOut' mNew' dv. induction de;
iIntros (mIn mOut mIn' mOut' mNew' dv Hsp) "HmIn"; simplify_eq/=.
......@@ -335,7 +306,7 @@ Section vcg_spec.
iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]". simplify_eq/=.
iExists _, _; iSplit; eauto.
rewrite -denv_merge_interp -denv_insert_interp.
iDestruct ("Hl" with "[$HmNew1 $HmNew2]") as "[$ $]".
iDestruct ("Hl" with "[$HmNew1 $HmNew2]") as "[$ $]".
iIntros "Hl". by iFrame.
- specialize (IHde1 mIn mOut).
destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|]; simplify_eq /=.
......@@ -381,7 +352,7 @@ Section vcg_spec.
iIntros (?) "[% HmNew1]".
rewrite (denv_unlock_interp E mNew1).
(* rewrite (denv_unlock_interp E (denv_stack_merge mOut1)). *)
iModIntro.
iModIntro.
awp_seq. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
iApply (awp_wand with "Hawp2"). iIntros (?) "[% HmNew2]". rewrite -denv_merge_interp.
iSplit; eauto. iFrame.
......@@ -398,7 +369,7 @@ Section vcg_spec.
iDestruct "Hawp" as "[HmOut $]". iApply denv_stack_merge_interp.
by iApply denv_stack_reverse.
Qed.
Lemma denv_wf_stack_merge ms E :
Forall (denv_wf E) ms
denv_wf E (denv_stack_merge ms).
......@@ -477,10 +448,10 @@ Section vcg_spec.
Lemma vcg_wp_unknown_correct R E m de Φ :
denv_wf E m
denv_interp E m -
wp_interp E (vcg_wp_unknown R E de m Φ) -
vcg_wp_unknown R E de m Φ -
awp (dcexpr_interp E de) R (λ v, E' dv m',
E `prefix_of` E' dval_interp E' dv = v dval_wf E' dv
denv_wf E' m' denv_interp E' m' wp_interp E' (Φ E' m' dv)).
denv_wf E' m' denv_interp E' m' Φ E' m' dv).
Proof.
rewrite /vcg_wp_unknown mapsto_wand_list_spec.
iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
......@@ -492,10 +463,10 @@ Section vcg_spec.
Lemma vcg_wp_load_correct E m dv Φ :
denv_wf E m
denv_interp E m -
wp_interp E (vcg_wp_load E dv m (Φ E)) -
vcg_wp_load E dv m (Φ E) -
(l:loc) q w, dval_interp E dv = #l l C{q} w (l C{q} w -
E' dv' m', E `prefix_of` E' dval_interp E' dv' = w dval_wf E' dv'
denv_wf E' m' denv_interp E' m' wp_interp E' (Φ E' m' dv')).
denv_wf E' m' denv_interp E' m' Φ E' m' dv').
Proof.
rewrite /vcg_wp_load. destruct (is_dloc E dv) as [i|] eqn:Hdloc.
+ destruct (denv_lookup i m) as [[q dv'] |] eqn:Hlkp; simpl; simplify_eq /=.
......@@ -526,11 +497,11 @@ Section vcg_spec.
E0 `prefix_of` E dval_wf E dv1 dval_wf E dv2
denv_wf E (denv_merge mOut m)
denv_interp E m -
wp_interp E (vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) (Φ E)) -
vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) (Φ E) -
denv_interp E mOut -
w : val, bin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w
( E' dv m', E0 `prefix_of` E' dval_interp E' dv = w dval_wf E' dv
denv_wf E' m' denv_interp E' m' wp_interp E' (Φ E' m' dv)).
denv_wf E' m' denv_interp E' m' Φ E' m' dv).
Proof.
iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin; first done.
......@@ -552,11 +523,11 @@ Section vcg_spec.
denv_wf E m
dval_wf E dv2
denv_interp E m -
wp_interp E (vcg_wp_store E dv1 dv2 m (Φ E)) -
vcg_wp_store E dv1 dv2 m (Φ E) -
(l : loc) (w : val), dval_interp E dv1 = #l
l C w (l C[LLvl] dval_interp E dv2 -
E' dv m', E0 `prefix_of` E' dval_interp E' dv = dval_interp E dv2
dval_wf E' dv denv_wf E' m' denv_interp E' m' wp_interp E' (Φ E' m' dv)).
dval_wf E' dv denv_wf E' m' denv_interp E' m' Φ E' m' dv).
Proof.
iIntros (Hpre Hwf Hwf2) "Hm Hwp". rewrite{1} /vcg_wp_store; fold vcg_wp.
destruct (is_dloc E dv1) as [i|] eqn:Hdloc.
......@@ -571,14 +542,14 @@ Section vcg_spec.
rewrite -denv_insert_interp. iFrame.
+ rewrite mapsto_wand_list_spec.
iSpecialize ("Hwp" with "[Hm]"); iFrame.
iDestruct "Hwp" as (dv_old) "[Hl Hwp]"; fold wp_interp.
iDestruct "Hwp" as (dv_old) "[Hl Hwp]";
iExists (dloc_interp E (dLoc i)), dv_old; iSplit; first done. iFrame.
iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
- rewrite mapsto_wand_list_spec.
iSpecialize ("Hwp" with "[Hm]"); iFrame.
iDestruct "Hwp" as (l ->) "Hwp"; fold wp_interp.
iDestruct "Hwp" as (v) "[Hdv Hwp]"; fold wp_interp.
iDestruct "Hwp" as (l ->) "Hwp";
iDestruct "Hwp" as (v) "[Hdv Hwp]";
iExists l,v ; iSplit; first done. iFrame.
iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
......@@ -590,10 +561,10 @@ Section vcg_spec.
dcexpr_wf E de
denv_wf E m
denv_interp E m -
wp_interp E (vcg_wp E m de R Φ) -
vcg_wp E m de R Φ -
awp (dcexpr_interp E de) R (λ v, E' dv m',
E `prefix_of` E' dval_interp E' dv = v dval_wf E' dv
denv_wf E' m' denv_interp E' m' wp_interp E' (Φ E' m' dv)).
denv_wf E' m' denv_interp E' m' Φ E' m' dv).
Proof.
revert Φ E m. induction de; intros Φ E m Hwf; iIntros (Hmwf) "Hm Hwp".
- iApply awp_ret. wp_value_head.
......@@ -633,7 +604,7 @@ Section vcg_spec.
rewrite (dval_interp_mono E E') //.
iApply (vcg_wp_store_correct with "[-H] H");
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
rewrite -!denv_merge_interp. iFrame "Hm'".
rewrite -!denv_merge_interp. iFrame "Hm'".
rewrite -!(denv_interp_mono E E'); eauto. iFrame.
- rewrite{1} /vcg_wp; fold vcg_wp.
simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2].
......@@ -706,8 +677,8 @@ Section vcg_spec.
ListOfMapsto Γls E m
IntoDCexpr E e de
environments.envs_entails (environments.Envs Γp Γs_out c)
(wp_interp E (vcg_wp E m de R (λ E m dv,
mapsto_wand_list m $ Base (Φ (dval_interp E dv)))))
(vcg_wp E m de R (λ E m dv,
mapsto_wand_list E m (Φ (dval_interp E dv))))
environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Proof.
rewrite /IntoDCexpr /=. intros Hsplit ->.
......@@ -722,7 +693,13 @@ Section vcg_spec.
Qed.
End vcg_spec.
(* Arguments wp_interp : simpl never. *)
Declare Reduction vcg_cbv :=
cbv [ vcg_wp vcg_wp_bin_op vcg_wp_store vcg_wp_load mapsto_wand_list vcg_wp_unknown].
Ltac vcg_compute :=
match goal with
|- ?u => let v := eval vcg_cbv in u in change v
end.
Ltac vcg_solver :=
eapply tac_vcg_sound;
......@@ -732,4 +709,4 @@ Ltac vcg_solver :=
| (* denv_wf E m *)
| apply _ (* ListOfMapsto Γls E m *)
| apply _ (* IntoDCexpr E e dce *)
| simpl ]; intuition.
| vcg_compute; simpl ]; intuition.
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