From b68e76c6bd29f1737325d0bb4a48eb90ef947eb5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Gondelman?= Date: Wed, 16 May 2018 14:33:04 +0200 Subject: [PATCH] fix naive_vcgen --- theories/heap_lang_vcgen/naive.v | 80 +++++++++++++++++++------------- 1 file changed, 47 insertions(+), 33 deletions(-) diff --git a/theories/heap_lang_vcgen/naive.v b/theories/heap_lang_vcgen/naive.v index 7cc132c..c0c8970 100644 --- a/theories/heap_lang_vcgen/naive.v +++ b/theories/heap_lang_vcgen/naive.v @@ -13,7 +13,7 @@ Section vcg. match a with | Base Φ => Φ | Inhale w Φ => ∃ (l:loc) v, ⌜w = #l⌝ ∧ l ↦ v ∗ wp_interp (Φ v) - | Exhale w v Φ => ∃ (l:loc), ⌜w = #l⌝ ∧ l ↦ v -∗ wp_interp Φ + | Exhale w v Φ => ∃ (l:loc), ⌜w = #l⌝ ∧ (l ↦ v -∗ wp_interp Φ) | IsSome mx Φ => ∃ v, ⌜mx = Some v⌝ ∧ wp_interp (Φ v) end%I. @@ -33,6 +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}}. Admitted. @@ -50,51 +52,63 @@ Section vcg. end. Ltac wp_vcg := eapply tac_vcg_sound; vcg_cbv. - Definition expr1 : expr := #21 + #21. - Definition expr2 (l: loc) : expr := !#l + #21. - Definition incr (l: loc) : expr := #l <- !#l + #1. - Lemma test_vcg_expr1: - (⌜True⌝ → WP expr1 {{ v, ⌜v = #42⌝ }})%I. + Lemma test1: WP #21 + #21 {{ v, ⌜v = #42⌝ }}%I. Proof. - rewrite/ expr1. iIntros. - (* PROOF BY VCG *) - wp_vcg. - iExists #42. eauto. - (*PROOF BY WP *) + iIntros. + (* --- PROOF BY VCG ---*) wp_vcg. + eauto. + (* --- PROOF BY WP --- *) (* wp_op. *) Qed. - Lemma test_expr2 (l: loc) : - l ↦ #21 -∗ WP (expr2 l) {{ v, l ↦ #21 ∧ ⌜v = #42⌝}}. + Lemma test2 (l: loc) : + l ↦ #21 -∗ WP (!#l + #21) {{ v, l ↦ #21 ∧ ⌜v = #42⌝}}. Proof. - rewrite/ expr2. iIntros "H". - (* PROOF BY VCG *) - wp_vcg. - iExists l, #21. iSplit; first done. iFrame. - iExists l. iIntros "[_ H]". eauto. - (*PROOF BY WP *) + iIntros "H". + (* --- PROOF BY VCG --- *) wp_vcg. + eauto 42 with iFrame. + (* --- PROOF BY WP --- *) (* wp_load. wp_op. eauto. *) Qed. - (* Variable (l': loc) (n': Z). *) - (* Eval simpl in - (vcg (#l' <- ! #l' + #1) (λ _ : val, Base (l' ↦ #(n' + 1))))%I. *) - - Lemma test_incr (l: loc) (n: Z) : - l ↦ #n -∗ WP (incr l) {{ _, l ↦ #(n + 1) }}. + Lemma test3 (l: loc) (n: Z) : + l ↦ #n -∗ WP (#l <- !#l + #1) {{ _, l ↦ #(n + 1) }}. Proof. - rewrite/ incr. iIntros "H". - (* PROOF BY VCG *) - wp_vcg. - iExists l, #n. rewrite/ bin_op_eval /=; iSplit; first done; iFrame. - iExists l; iIntros "[_ H]". - iExists #(n + 1); iSplit; first done; iFrame. - iExists l, #n; iSplit; first done; iFrame. - iExists l. by iIntros "[_ H]". + iIntros "H". + (* --- PROOF BY VCG --- *) wp_vcg. + eauto 17 with iFrame. (*PROOF BY WP *) (* wp_load. wp_op. wp_store. done. *) Qed. + Lemma test4 (l: loc) (n: Z) : + 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 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. *) End vcg. \ No newline at end of file -- GitLab