From 4f1516076057e9ca8de87290a097fe5e20a66c77 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Thu, 7 Dec 2017 20:00:36 +0100
Subject: [PATCH] Implement and prove wps

---
 wp.v | 68 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 68 insertions(+)

diff --git a/wp.v b/wp.v
index 535d245..4f65a1c 100644
--- a/wp.v
+++ b/wp.v
@@ -3,6 +3,7 @@
 (***** Partie 1 : definition de While ****************************************)
 
 Require Import ZArith.BinInt.
+Require Import FunctionalExtensionality.
 Require Import Omega.
 Import Z.
 
@@ -584,5 +585,72 @@ Proof.
   apply wp_correctness_provable.
 Qed.
 
+(***** Assertions syntaxiques******** ****************************************)
+
+Inductive SynAssert : Type:=
+| ATop: SynAssert
+| ABot: SynAssert
+| ANeg: SynAssert -> SynAssert
+| AAnd: SynAssert -> SynAssert -> SynAssert
+| AOr: SynAssert -> SynAssert -> SynAssert
+| AImplies: SynAssert -> SynAssert -> SynAssert
+| AExpr: Expr -> SynAssert
+| AForall: Var -> SynAssert -> SynAssert
+| AExists: Var -> SynAssert -> SynAssert
+| ASubstZ: Var -> Z -> SynAssert -> SynAssert
+| ASubstE: Var -> Expr -> SynAssert -> SynAssert.
+
+Fixpoint aInterp (src: SynAssert): Assert :=
+  fun (mem: Mem) => match src with
+  | ATop => True
+  | ABot => False
+  | ANeg x => ~ (aInterp x mem)
+  | AAnd x y => (aInterp x mem) /\ (aInterp y mem)
+  | AOr x y => (aInterp x mem) \/ (aInterp y mem)
+  | AImplies x y => (~ (aInterp x mem)) \/ (aInterp y mem)
+  | AExpr exp => exp mem <> 0%Z
+  | AForall v x => forall (z: Z), aInterp x (mem [v <- z])
+  | AExists v x => exists (z: Z), aInterp x (mem [v <- z])
+  | ASubstZ v z x => aInterp x (mem [v <- z])
+  | ASubstE v e x => aInterp x (mem [v <- (e mem)])
+  end.
+
+Fixpoint wps (instr: Instr) (asser: SynAssert) : SynAssert := match instr with
+| skip => asser
+| abort => ATop
+| assign x expr => ASubstE x expr asser
+| seq s1 s2 => wps s1 (wps s2 asser)
+| ifelse guard sIf sElse =>
+    AAnd
+      (AImplies (AExpr guard) (wps sIf asser))
+      (AImplies (ANeg (AExpr guard)) (wps sElse asser))
+| while guard body => ABot
+end.
+
+Lemma aInterpConsistent (instr: Instr):
+  forall post, aInterp (wps instr post) = wp instr (aInterp post).
+Proof.
+  induction instr; intros post; simpl; trivial.
+  * (* sequence *)
+    rewrite <- (IHinstr2 post).
+    rewrite (IHinstr1 (wps instr2 post)).
+    congruence.
+  * (* if/else *)
+    rewrite <- (IHinstr2 post).
+    rewrite <- (IHinstr1 post).
+    unfold assertAnd; unfold assertImpl; unfold assertOfExpr; unfold assertOr;
+      unfold assertNot; simpl.
+    apply functional_extensionality; intros mem; simpl. congruence.
+Qed.
+
+Theorem wps_correctness (instr: Instr):
+  forall post,
+    ( |= [| aInterp (wps instr post) |] instr [| aInterp post |] ) % assert.
+Proof.
+  intro post.
+  rewrite (aInterpConsistent instr).
+  apply wp_correctness.
+Qed.
+
 (* vim: ts=2 sw=2
 *)