Commit 3b9627d9 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

a small clean-up of vcgen.v before rewriting it with denv instead of env

parent d6562729
......@@ -43,6 +43,7 @@ Section vcg.
((val iProp Σ) wp_expr)
((val iProp Σ) wp_expr)
(dval dval wp_expr) wp_expr.
Arguments Base _%I.
Fixpoint wp_interp (E : env_locs) (a : wp_expr) : iProp Σ :=
......@@ -62,7 +63,7 @@ Section vcg.
wp_interp E (P1 Ψ1)
wp_interp E (P2 Ψ2)
(v1 v2 : val), Ψ1 v1 - Ψ2 v2 - wp_interp E (P3 (dValUnknown v1) (dValUnknown v2))
end%I.
end%I.
Fixpoint wp_interp_sane (E : env_locs) (a : wp_expr) : iProp Σ :=
match a with
......@@ -84,28 +85,6 @@ Section vcg.
v1 v2, Ψ1 v1 - Ψ2 v2 - wp_interp_sane E (P3 (dValUnknown v1) (dValUnknown v2))
end%I.
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 (v) "[H1 H2]".
iExists (dValUnknown v). simpl. iFrame. by iApply H0.
- simpl. iIntros (E) "(He & H)". iFrame. by iApply IHa.
- 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.
- simpl. intros E.
iDestruct 1 as (Ψ1 Ψ2) "(HΨ1 & HΨ2 & HΦ)".
iExists _,_.
iSplitL "HΨ1". by iApply H0.
iSplitL "HΨ2". by iApply H1.
iIntros (v1 v2) "Hv1 Hv2". iApply H2.
iApply ("HΦ" with "Hv1 Hv2").
Qed.
Fixpoint append_exhale_list (ps : env_ps_dv) (Φ : wp_expr) : wp_expr :=
match ps with
......@@ -119,28 +98,7 @@ Section vcg.
| [] => Φ
end.
Lemma vcg_inhale_list_sound E s t :
wp_interp E (append_inhale_list s t) - env_ps_dv_interp E s wp_interp E t.
Proof.
unfold env_ps_dv_interp.
induction s as [| [i [[x q] w]] s']; simpl.
- by iIntros "$ _".
- iIntros "[H1 H2]". iFrame "H1". by iApply (IHs' with "H2").
Qed.
Lemma vcg_exhale_list_sound E s t :
wp_interp E (append_exhale_list s t) - env_ps_dv_interp E s - wp_interp E t.
Proof.
unfold env_ps_dv_interp.
induction s as [| [i [[x q] w]] s']; simpl.
- by iIntros "$ _".
- iIntros "H [H1 H2]".
iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
Qed.
(* vcg_sp E s de = Some (s1, s2, dv)
(* vcg_sp E s de = Some (s1, s2, dv)
- s1 = s / resources for de
- s2 = new resources that you get from de
*)
......@@ -178,6 +136,67 @@ Section vcg.
end
end.
Fixpoint vcg_wp (E: env_locs) (s: env_ps_dv) (de : dcexpr) (R : iProp Σ) (Φ : dval wp_expr) : wp_expr :=
match de with
| dCVal dv => Φ dv
| dCLoad de1 => vcg_wp E s de1 R (λ dv, IsLoc dv (λ l, Inhale l 1%Qp (λ w, Exhale l w ULvl 1%Qp (Φ w))))
| dCBinOp op de1 de2 =>
match vcg_sp E s de1 with
| Some (s1, s2, dv1) =>
append_inhale_list s (vcg_wp E s1 de2 R (λ dv2,
append_exhale_list (s1 ++ s2) (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
| None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
end
| _ => 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.
generalize dependent E.
induction a.
- done.
- simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
iExists (dValUnknown v). simpl. iFrame. by iApply H0.
- simpl. iIntros (E) "(He & H)". iFrame. by iApply IHa.
- 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.
- simpl. intros E.
iDestruct 1 as (Ψ1 Ψ2) "(HΨ1 & HΨ2 & HΦ)".
iExists _,_.
iSplitL "HΨ1". by iApply H0.
iSplitL "HΨ2". by iApply H1.
iIntros (v1 v2) "Hv1 Hv2". iApply H2.
iApply ("HΦ" with "Hv1 Hv2").
Qed.
Lemma vcg_inhale_list_sound E s t :
wp_interp E (append_inhale_list s t) - env_ps_dv_interp E s wp_interp E t.
Proof.
unfold env_ps_dv_interp.
induction s as [| [i [[x q] w]] s']; simpl.
- by iIntros "$ _".
- iIntros "[H1 H2]". iFrame "H1". by iApply (IHs' with "H2").
Qed.
Lemma vcg_exhale_list_sound E s t :
wp_interp E (append_exhale_list s t) - env_ps_dv_interp E s - wp_interp E t.
Proof.
unfold env_ps_dv_interp.
induction s as [| [i [[x q] w]] s']; simpl.
- by iIntros "$ _".
- iIntros "H [H1 H2]".
iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
Qed.
Lemma vcg_sp_correct E s de ps1 ps2 dv R :
vcg_sp E s de = Some (ps1, ps2, dv)
env_ps_dv_interp E s -
......@@ -239,45 +258,6 @@ Section vcg.
+ iCombine "Hs2' Hs2''" as "Hs2". iFrame.
Qed.
(* Suggestion for vcg_wp *)
(* Fixpoint vcg_wp (E: env_locs) (s: env_ps_dv) (de : dcexpr) (R : iProp Σ) (Φ : dval → wp_expr) : wp_expr :=
match vcg_sp E s de with
| Some (s1, s2, dv) => append_inhale_list s1 (append_exhale_list s2 (Φ dv))
| None =>
match de with
| dCVal dv => Φ dv
| dCLoad de1 => vcg_wp E s de1 R (λ dv, IsLoc dv (λ l, Inhale l 1%Qp (λ w, Exhale l w ULvl 1%Qp (Φ w))))
| dCBinOp op de1 de2 =>
match vcg_sp E s de1 with
| Some (s1, s2, dv1) =>
append_inhale_list s (vcg_wp E s1 de2 R (λ dv2,
append_exhale_list (s1 ++ s2) (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
| None =>
match vcg_sp E s de2 with
| Some (s1, s2, dv2) =>
append_inhale_list s (vcg_wp E s1 de1 R (λ dv1,
append_exhale_list (s1 ++ s2) (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
| None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
end
end
| dCStore de1 de2 => (*TODO*) Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
end
end.
*)
Fixpoint vcg_wp (E: env_locs) (s: env_ps_dv) (de : dcexpr) (R : iProp Σ) (Φ : dval wp_expr) : wp_expr :=
match de with
| dCVal dv => Φ dv
| dCLoad de1 => vcg_wp E s de1 R (λ dv, IsLoc dv (λ l, Inhale l 1%Qp (λ w, Exhale l w ULvl 1%Qp (Φ w))))
| dCBinOp op de1 de2 =>
match vcg_sp E s de1 with
| Some (s1, s2, dv1) =>
append_inhale_list s (vcg_wp E s1 de2 R (λ dv2,
append_exhale_list (s1 ++ s2) (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
| None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
end
| _ => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
end.
Lemma vcg_wp_correct R E s de Φ :
wp_interp E (vcg_wp E s de R Φ)
awp (dcexpr_interp E de) R (λ v, dv, dval_interp E dv = v wp_interp E (Φ dv)).
......@@ -343,47 +323,4 @@ Section vcg.
iIntros (v) "H". by iDestruct "H" as (dv) "[-> $]".
Qed.
End vcg.
(*
Ltac vcg_solver :=
eapply tac_vcg_sound;
[ apply _
| compute; reflexivity
| apply _
| apply _
| simpl ].
Section Tests_vcg.
Context `{amonadG Σ}.
Notation "l ↦( x , q ) v" :=
(mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l ↦( x , q ) v").
Lemma test1 (l : loc) :
l ↦U #1 -∗
awp (a_load (a_ret #l))%E True (fun v => ⌜v = #1⌝ ∗ l ↦U #1).
Proof.
iIntros "Hl".
vcg_solver.
iIntros "[H _]"; simplify_eq /=. unfold ps_lvl, ps_frc. simpl in *.
Admitted.
Lemma test2 (l : loc) :
l ↦U #1 -∗
awp (a_store (a_ret #l) (a_ret #3))%E True (fun v => ⌜v = #3⌝ ∗ l ↦L #3).
Proof.
iIntros "Hl".
vcg_solver.
iIntros "[H _]"; simplify_eq /=. simpl.
iExists (λ v, ∃ l : loc, ⌜v = #l⌝ ∗ l ↦U #1)%I, (λ v, l ↦U #1)%I.
repeat iSplitL; eauto.
iIntros (v1 v2). iDestruct 1 as (l' ->) "Hl'".
iIntros "Hl". iExists l'. iSplit; eauto.
iExists #1. iFrame.
Qed.
*)
End vcg_spec.
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