Commit c36dda2a authored by Léon Gondelman's avatar Léon Gondelman

Just a sketch of a very naive vcgen for heap-lang,

without any optimisation.

Next steps:
 modify definition of wp_expr, with a deep embedding of
  - functions : to allow optimisation go recursively through lambdas,
    in particular, to allow exhale-inhale optimisation;
  - conjunction and equations : to allow optimisation
    of redundant and trivial equations
parent 4fde9aa2
......@@ -9,7 +9,8 @@ theories/c_translation/monad.v
theories/c_translation/proofmode.v
theories/c_translation/translation.v
theories/c_translation/derived.v
theories/heap_lang_vcgen/naive.v
theories/tests/test1.v
theories/tests/fact.v
theories/tests/gcd.v
theories/tests/lists.v
\ No newline at end of file
theories/tests/lists.v
From iris.heap_lang Require Export proofmode notation.
From iris.proofmode Require Import coq_tactics.
Section vcg.
Context `{heapG Σ}.
Inductive wp_expr :=
| Base : iProp Σ wp_expr
| Inhale : val (val wp_expr) wp_expr
| Exhale : val val wp_expr wp_expr
| IsSome : option val (val wp_expr) wp_expr.
Fixpoint wp_interp (a: wp_expr) : iProp Σ :=
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 Φ
| IsSome mx Φ => v, mx = Some v wp_interp (Φ v)
end%I.
Fixpoint vcg (e: expr) (Φ: val wp_expr) : wp_expr :=
match e with
| BinOp op e1 e2 =>
vcg e1 (λ v1, vcg e2 (λ v2, IsSome (bin_op_eval op v1 v2) Φ))
| Store e1 e2 =>
vcg e1 (λ l,
vcg e2 (λ v,
Inhale l (λ _, Exhale l v (Φ #()))))
| Load e1 =>
vcg e1 (λ l, Inhale l (λ v, Exhale l v (Φ v)))
| Lit (LitInt n) => Φ #n
| Lit (LitLoc l) => Φ #l
| _ => 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.
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.
Proof.
rewrite/ expr1. iIntros.
(* PROOF BY VCG *)
wp_vcg.
iExists #42. eauto.
(*PROOF BY WP *)
(* wp_op. *)
Qed.
Lemma test_expr2 (l: loc) :
l #21 - WP (expr2 l) {{ 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 *)
(* 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) }}.
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]".
(*PROOF BY WP *)
(* wp_load. wp_op. wp_store. done. *)
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