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

wip on simple exh-inh optimize

parent b68e76c6
......@@ -33,10 +33,8 @@ Section vcg.
end%I.
Eval simpl in vcg (#21 + #21) (λ v, Base ( v = #42)%I).
Lemma vcg_sound e Φ:
wp_interp (vcg e (λ v, Base (Φ v))) WP e {{v, Φ v}}.
wp_interp (vcg e (λ v, Base (Φ v))) WP e {{v, Φ v}}.
Admitted.
Lemma tac_vcg_sound Δ e Φ :
......@@ -52,6 +50,48 @@ Section vcg.
end.
Ltac wp_vcg := eapply tac_vcg_sound; vcg_cbv.
(***************** OPTIMIZATION ********************)
Fixpoint optimize (Φ : wp_expr) : wp_expr :=
match Φ with
| Base Φ1 => Φ
| Inhale w Φ1 => Inhale w (λ v, optimize (Φ1 v))
| Exhale l1 w (Inhale l2 Φ1) =>
if bool_decide (l1 = l2) then optimize (Φ1 w)
else Exhale l1 w (Inhale l2 (λ v, optimize (Φ1 v)))
| Exhale w v Φ1 => Exhale w v (optimize Φ1)
| IsSome mx Φ1 => IsSome mx (λ v, optimize (Φ1 v))
end.
Lemma vcg_opt_sound e Φ:
wp_interp (optimize (vcg e (λ v, Base (Φ v)))) WP e {{v, Φ v}}.
Admitted.
Lemma tac_vcg_opt_sound Δ e Φ :
envs_entails Δ (wp_interp (optimize (vcg e (λ v, Base (Φ v)))))
envs_entails Δ (WP e {{ Φ }}).
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.
(* Variable (l: loc) (n: Z) (Φ: val → iProp Σ). *)
(* Eval simpl in vcg (!#l + !#l) (λ 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. *)
(* Eval simpl in vcg (#21 + #21) (λ v, Base (⌜ v = #42⌝)%I). *)
Lemma test1: WP #21 + #21 {{ v, v = #42 }}%I.
Proof.
......@@ -86,29 +126,22 @@ Section vcg.
l #n - WP (!#l + !#l) {{ v, v = #(n + n) l #n }}.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *) wp_vcg.
eauto 20 with iFrame.
(* --- PROOF BY VCG --- *) wp_opt_vcg.
eauto 17 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. wp_load. wp_op. eauto. *)
Qed.
(* Lemma test5 (l: loc) (n: Z) : *)
(* l ↦ #n -∗ WP (!#l + !#l + !#l + !#l + !#l + !#l) *)
(* {{ v, ⌜v = #(n + n + n + n + n + n)⌝ ∧ l ↦ #n }}. *)
(* Proof. *)
(* iIntros "H". *)
(* (* --- PROOF BY VCG --- *) wp_vcg. *)
(* eauto 54 with iFrame. *)
(* (* --- PROOF BY WP --- *) *)
(* (* wp_load. do 5 (wp_load; wp_op). eauto. *) *)
(* Qed. *)
(* Variable (l: loc) (n: Z) (Φ: val → iProp Σ).
Eval simpl in 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. *)
Lemma test5 (l: loc) (n: Z) :
l #n - WP (!#l + !#l + !#l + !#l)
{{ v, v = #(n + n + n + n) l #n }}.
Proof.
iIntros "H".
(* --- PROOF BY VCG --- *) wp_opt_vcg.
eauto 29 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. do 4 (wp_load; wp_op). eauto. *)
Qed.
End 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