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

fix naive_vcgen

parent c36dda2a
...@@ -13,7 +13,7 @@ Section vcg. ...@@ -13,7 +13,7 @@ Section vcg.
match a with match a with
| Base Φ => Φ | Base Φ => Φ
| Inhale w Φ => (l:loc) v, w = #l l v wp_interp (Φ v) | 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) | IsSome mx Φ => v, mx = Some v wp_interp (Φ v)
end%I. end%I.
...@@ -33,6 +33,8 @@ Section vcg. ...@@ -33,6 +33,8 @@ Section vcg.
end%I. end%I.
Eval simpl in vcg (#21 + #21) (λ v, Base ( v = #42)%I).
Lemma vcg_sound e Φ: 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. Admitted.
...@@ -50,51 +52,63 @@ Section vcg. ...@@ -50,51 +52,63 @@ Section vcg.
end. end.
Ltac wp_vcg := eapply tac_vcg_sound; vcg_cbv. 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: Lemma test1: WP #21 + #21 {{ v, v = #42 }}%I.
(True WP expr1 {{ v, v = #42 }})%I.
Proof. Proof.
rewrite/ expr1. iIntros. iIntros.
(* PROOF BY VCG *) (* --- PROOF BY VCG ---*) wp_vcg.
wp_vcg. eauto.
iExists #42. eauto. (* --- PROOF BY WP --- *)
(*PROOF BY WP *)
(* wp_op. *) (* wp_op. *)
Qed. Qed.
Lemma test_expr2 (l: loc) : Lemma test2 (l: loc) :
l #21 - WP (expr2 l) {{ v, l #21 v = #42}}. l #21 - WP (!#l + #21) {{ v, l #21 v = #42}}.
Proof. Proof.
rewrite/ expr2. iIntros "H". iIntros "H".
(* PROOF BY VCG *) (* --- PROOF BY VCG --- *) wp_vcg.
wp_vcg. eauto 42 with iFrame.
iExists l, #21. iSplit; first done. iFrame. (* --- PROOF BY WP --- *)
iExists l. iIntros "[_ H]". eauto.
(*PROOF BY WP *)
(* wp_load. wp_op. eauto. *) (* wp_load. wp_op. eauto. *)
Qed. Qed.
(* Variable (l': loc) (n': Z). *) Lemma test3 (l: loc) (n: Z) :
(* Eval simpl in l #n - WP (#l <- !#l + #1) {{ _, l #(n + 1) }}.
(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) }}.
Proof. Proof.
rewrite/ incr. iIntros "H". iIntros "H".
(* PROOF BY VCG *) (* --- PROOF BY VCG --- *) wp_vcg.
wp_vcg. eauto 17 with iFrame.
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]".
(*PROOF BY WP *) (*PROOF BY WP *)
(* wp_load. wp_op. wp_store. done. *) (* wp_load. wp_op. wp_store. done. *)
Qed. 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. 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