From a94786e6d23dbe01107252665cfeedf0e5f835e6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Gondelman?= Date: Wed, 16 May 2018 15:22:07 +0200 Subject: [PATCH] wip on simple exh-inh optimize --- theories/heap_lang_vcgen/naive.v | 77 +++++++++++++++++++++++--------- 1 file changed, 55 insertions(+), 22 deletions(-) diff --git a/theories/heap_lang_vcgen/naive.v b/theories/heap_lang_vcgen/naive.v index c0c8970..4b30355 100644 --- a/theories/heap_lang_vcgen/naive.v +++ b/theories/heap_lang_vcgen/naive.v @@ -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 -- GitLab