Commit 33b1bf54 authored by Léon Gondelman's avatar Léon Gondelman

wip on simple exh-inh optimize

parent a94786e6
From iris.heap_lang Require Export proofmode notation.
From iris.proofmode Require Import coq_tactics.
Section vcg.
Context `{heapG Σ}.
......@@ -32,25 +33,6 @@ Section vcg.
| _ => Base (WP e {{ v, wp_interp (Φ v)}})
end%I.
Lemma vcg_sound e Φ:
wp_interp (vcg e (λ v, Base (Φ v))) WP e {{v, Φ v}}.
Admitted.
Lemma tac_vcg_sound Δ e Φ :
envs_entails Δ (wp_interp (vcg e (λ v, Base (Φ v))))
envs_entails Δ (WP e {{ Φ }}).
Proof. rewrite /envs_entails. intros. by rewrite - (vcg_sound e Φ).
Qed.
Declare Reduction vcg_cbv := cbv [ wp_interp vcg ].
Ltac vcg_cbv :=
match goal with
|- ?u => let v := eval vcg_cbv in u in change v
end.
Ltac wp_vcg := eapply tac_vcg_sound; vcg_cbv.
(***************** OPTIMIZATION ********************)
Fixpoint optimize (Φ : wp_expr) : wp_expr :=
match Φ with
| Base Φ1 => Φ
......@@ -63,6 +45,16 @@ Section vcg.
end.
Lemma vcg_sound e Φ:
wp_interp (vcg e (λ v, Base (Φ v))) WP e {{v, Φ v}}.
Admitted.
Lemma tac_vcg_sound Δ e Φ :
envs_entails Δ (wp_interp (vcg e (λ v, Base (Φ v))))
envs_entails Δ (WP e {{ Φ }}).
Proof. rewrite /envs_entails. intros. by rewrite - (vcg_sound e Φ).
Qed.
Lemma vcg_opt_sound e Φ:
wp_interp (optimize (vcg e (λ v, Base (Φ v)))) WP e {{v, Φ v}}.
Admitted.
......@@ -73,23 +65,36 @@ Section vcg.
Proof. rewrite /envs_entails. intros. by rewrite -(vcg_opt_sound e Φ).
Qed.
Declare Reduction vcg_opt_cbv := cbv [ wp_interp optimize vcg ].
Ltac vcg_opt_cbv :=
match goal with
|- ?u => let v := eval vcg_opt_cbv in u in change v
end.
Ltac wp_opt_vcg := eapply tac_vcg_opt_sound; vcg_opt_cbv;
try case_bool_decide; simplify_eq.
End vcg.
Declare Reduction vcg_cbv := cbv [ wp_interp vcg ].
Ltac vcg_cbv :=
match goal with
|- ?u => let v := eval vcg_cbv in u in change v
end.
Ltac wp_vcg := eapply tac_vcg_sound; vcg_cbv.
(* Variable (l: loc) (n: Z) (Φ: val → iProp Σ). *)
(* Eval simpl in vcg (!#l + !#l) (λ v : val, Base (Φ v))%I. *)
Declare Reduction vcg_opt_cbv := cbv [ wp_interp optimize vcg ].
Ltac vcg_opt_cbv :=
match goal with
|- ?u => let v := eval vcg_opt_cbv in u in change v
end.
Ltac wp_opt_vcg := eapply tac_vcg_opt_sound; vcg_opt_cbv;
try case_bool_decide; simplify_eq.
Section Tests_vcg.
Context `{heapG Σ}.
(* Variable (l k: loc) (n: Z) (Φ: val → iProp Σ). *)
(* Eval simpl in vcg (!#l + !#k) (λ v : val, Base (Φ v))%I. *)
(* Eval simpl in optimize (vcg (!#l + !#l) (λ v : val, Base (Φ v)))%I. *)
(* Eval simpl in wp_interp (vcg (!#l + !#l) (λ v : val, Base (Φ v))%I). *)
(* Eval simpl in *)
(* (vcg (#l <- ! #l + #1) (λ _ : val, Base (l ↦ #(n + 1))))%I. *)
(* (vcg (#l <- ! #l + #1) (λ _ : val, Base (l ↦ #(n + 1))))%I. *)
(* Eval simpl in vcg (#21 + #21) (λ v, Base (⌜ v = #42⌝)%I). *)
......@@ -144,4 +149,18 @@ Section vcg.
(* wp_load. do 4 (wp_load; wp_op). eauto. *)
Qed.
End vcg.
\ No newline at end of file
Lemma test6 (l1 l2: loc) (n m: Z) :
l1 #n - l2 #m - WP (!#l1 + !#l2) {{ v, v = #(n + m) l1 #n l2 #m }}.
Proof.
iIntros "Hl1 Hl2".
(* --- PROOF BY VCG --- *) wp_opt_vcg.
- iCombine "Hl1" "Hl2" as "Habsurd". admit.
- eauto 42 with iFrame.
iExists l1, #n. iSplit; first done.
iSplitL "Hl1"; first done.
eauto 15 with iFrame.
(* --- PROOF BY WP --- *)
(* do 2 wp_load. wp_op. eauto with iFrame. *)
Admitted.
End Tests_vcg.
\ No newline at end of file
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