Commit 72a26f71 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

just a commented suggestion about vcg_wp. Also need to understand the need of append_inhale_list

parent 0e5fd3bb
......@@ -143,8 +143,8 @@ Section vcg.
| dCVal dv => Some (s, nil, dv)
| dCLoad de1 =>
''(s1, s2, dv1) vcg_sp E s de1;
i is_dloc E dv1;
''(s1', ((x, q), dv2)) find_and_remove s1 (dLoc i);
i is_dloc E dv1;
''(s1', ((x, q), dv2)) find_and_remove s1 (dLoc i);
if (bool_decide (x = ULvl))
then
(* NB: 'x' can be a Coq variable, so here we can't check that 'x' is Ulvl *)
......@@ -231,6 +231,31 @@ 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
......@@ -291,17 +316,17 @@ Section vcg.
eauto with iFrame.
Qed.
Lemma tac_vcg_sound Γs_in Γs_out Γls Γp ps c e R Φ E F dce :
Lemma tac_vcg_sound Γs_in Γs_out Γls Γp ps c e R Φ E dce :
MapstoListFromEnv Γs_in Γs_out Γls
E = env_to_known_locs Γls
ListOfMapsto Γls E ps
IntoDCexpr E e dce
vcg_wp E ps dce R (λ dv, Base (Φ (dval_interp E dv))) = F
coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_out c) (env_ps_dv_interp E ps - wp_interp_sane E F)
coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_out c)
(env_ps_dv_interp E ps - wp_interp_sane E (vcg_wp E ps dce R (λ dv, Base (Φ (dval_interp E dv)))))
coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_in c) (awp e R Φ).
Proof.
rewrite /IntoDCexpr /=. intros Hsplit ->.
rewrite /ListOfMapsto. intros Hexhale -> <- Hgoal.
rewrite /ListOfMapsto. intros Hexhale -> Hgoal.
eapply tac_envs_split_mapsto; try eassumption.
revert Hgoal. rewrite coq_tactics.envs_entails_eq.
rewrite wp_interp_sane_sound (vcg_wp_correct R).
......@@ -310,4 +335,47 @@ Section vcg.
iIntros (v) "H". by iDestruct "H" as (dv) "[-> $]".
Qed.
End vcg.
\ No newline at end of file
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.
*)
Supports Markdown
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