Exemples: portage complet de double-wp vers le nouveau système

  (+ élimination de la preuve Coq)

examples/double_wp/compiler.mlw

@@ -24,15 +24,15 @@ module Compile_aexpr
   meta rewrite_def function aexpr_post
 
   let rec compile_aexpr (a:aexpr) :  hl 'a
-    ensures { result.pre = trivial_pre /\ hl_correctness result }
-    ensures { result.post = aexpr_post a result.code.length }
+    ensures { result <% (trivial_pre,aexpr_post a result.code.length) }
+    ensures { hl_correctness result }
     variant { a }
     = let c = match a with
       | Anum n     -> $ iconstf n
       | Avar x     -> $ ivarf x
-      | Aadd a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~  $ iaddf ()
-      | Asub a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~  $ isubf ()
-      | Amul a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~  $ imulf ()
+      | Aadd a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 --  $ iaddf ()
+      | Asub a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 --  $ isubf ()
+      | Amul a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 --  $ imulf ()
       end in
       hoare trivial_pre c (aexpr_post a c.wcode.length)
 
@@ -74,9 +74,9 @@ module Compile_bexpr
   meta rewrite_def function exec_cond
 
   let rec compile_bexpr (b:bexpr) (cond:bool) (ofs:ofs) :  hl 'a
-    ensures { result.pre = trivial_pre /\ hl_correctness result }
-    ensures { result.post =
-              bexpr_post b cond (result.code.length + ofs) result.code.length }
+    ensures { let len = result.code.length in
+      result <% (trivial_pre,bexpr_post b cond (len + ofs) len) }
+    ensures { hl_correctness result }
     variant { b }
   = let c = match b with
     | Btrue      -> $ if cond then ibranchf ofs else inil ()
@@ -85,10 +85,10 @@ module Compile_bexpr
     | Band b1 b2 ->
       let c2  = $ compile_bexpr b2 cond ofs % exec_cond b1 true in
       let ofs = if cond then length c2.wcode else ofs + length c2.wcode in
-      $ compile_bexpr b1 false ofs ~ c2
-    | Beq a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~
+      $ compile_bexpr b1 false ofs -- c2
+    | Beq a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 --
                    $ if cond then ibeqf ofs else ibnef ofs
-    | Ble a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~
+    | Ble a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 --
                    $ if cond then iblef ofs else ibgtf ofs
     end in
     let ghost post = bexpr_post b cond (c.wcode.length + ofs) c.wcode.length in
@@ -145,40 +145,48 @@ module Compile_com
       pi = p /\ s0 = si /\ exists mf. ceval m0 c mf /\ ceval mi c mf
   meta rewrite_def function loop_invariant
 
-  function loop_post (c : com) (len: pos) : pre ('a,machine_state) =
-    fun x p msf -> let VMS _ s0 m0 = snd x in let VMS pf sf mf = msf in
-      pf = p + len /\ s0 = sf /\ ceval m0 c mf
-  meta rewrite_def function loop_post
-
   function loop_variant (c:com) (test:bexpr) : post 'a =
     fun _ _ msj msi -> let VMS pj sj mj = msj in let VMS pi si mi = msi in
-       pj = pi /\ sj = si /\ ceval mi c mj /\ beval mi test
-  meta rewrite_def function loop_variant
+       ceval mi c mj /\ beval mi test
+  lemma loop_variant_lemma : forall c test,x:'a,p msj msi.
+    loop_variant c test x p msj msi =
+      let VMS pj sj mj = msj in let VMS pi si mi = msi in
+      ceval mi c mj /\ beval mi test
+  meta rewrite lemma loop_variant_lemma
+
+  (* Well-foundedness of the loop variant. *)
+  lemma loop_variant_acc : forall c test,x:'a,p mi mj.
+    let wh = Cwhile test c in let var = (loop_variant c test x p) in
+    (ceval mi wh mj -> forall pi si. acc var (VMS pi si mi))
+    by forall pi si mi mj mf. ceval mi c mj /\ beval mi test ->
+      ceval mj wh mf /\ (forall pj sj. acc var (VMS pj sj mj)) ->
+      acc var (VMS pi si mi) by
+      (forall pk sk mk. var (VMS pk sk mk) (VMS pi si mi) -> mk = mj)
 
   let rec compile_com (cmd: com) : hl 'a
-    ensures  { result.pre = com_pre cmd /\ hl_correctness result }
-    ensures  { result.post = com_post cmd result.code.length }
+    ensures  { hl_correctness result }
+    ensures  { let len = result.code.length in
+      result <% (com_pre cmd,com_post cmd len) }
     variant  { cmd }
   = let res = match cmd with
     | Cskip              -> $ inil ()
-    | Cassign x a        -> $ compile_aexpr a  ~ $ isetvarf x
-    | Cseq cmd1 cmd2     -> $ compile_com cmd1 ~ $ compile_com cmd2
+    | Cassign x a        -> $ compile_aexpr a  -- $ isetvarf x
+    | Cseq cmd1 cmd2     -> $ compile_com cmd1 -- $ compile_com cmd2
     | Cif cond cmd1 cmd2 -> let code_false = compile_com cmd2 in
-      let code_true = $ compile_com cmd1 ~ $ ibranchf code_false.code.length in
-      $ compile_bexpr cond false code_true.wcode.length ~
-      (code_true % exec_cond cond true) ~
+      let code_true = $ compile_com cmd1 -- $ ibranchf code_false.code.length in
+      $ compile_bexpr cond false code_true.wcode.length --
+      (code_true % exec_cond cond true) --
       ($ code_false % exec_cond_old cond false)
-    | Cwhile test body  -> let code_body = compile_com body in
+    | Cwhile test body  ->
+      let code_body = compile_com body in
       let body_length = length code_body.code + 1 in
       let code_test = compile_bexpr test false body_length in
       let ofs = length code_test.code + body_length in
-      let wp_while = $ code_test ~
-          ($ code_body ~ $ ibranchf (- ofs)) % exec_cond test true in
-      let ghost inv  = loop_invariant cmd in
-      let ghost var  = loop_variant body test  in
-      let ghost post = loop_post cmd ofs in
-      let hl_while = hoare inv wp_while (loop_progress inv post var) in
-      $ inil () ~ $ make_loop_hl hl_while inv post var
+      let wp_while = $ code_test --
+          ($ code_body -- $ ibranchf (- ofs)) % exec_cond test true in
+      let ghost inv = loop_invariant cmd in
+      let ghost var = loop_variant body test in
+      $ inil () -- make_loop wp_while inv (exec_cond test true) var
     end in
     hoare (com_pre cmd) res (com_post cmd res.wcode.length)
 
@@ -188,7 +196,7 @@ module Compile_com
       transition_star c (VMS p s m) (VMS (p + length result) s m') }
   = let res = compile_com com : hl unit in
     assert { forall c p s m m'. ceval m com m' -> codeseq_at c p res.code ->
-      res.pre () p (VMS p s m) && (forall ms'. res.post () p (VMS p s m) ms' ->
+     res.pre () p (VMS p s m) && (forall ms'. res.post () p (VMS p s m) ms' ->
       ms' = VMS (p + length res.code) s m') };
     res.code
 

examples/double_wp/logic.mlw

@@ -16,6 +16,9 @@ module Compiler_logic
   function snd (p: ('a,'b)) : 'b = let (_,y) = p in y
   meta rewrite_def function snd
 
+  predicate (-->) (x y:'a) = "rewrite" x = y
+  meta rewrite_def predicate (-->)
+
   (* Unary predicates over machine states *)
   type pred  = machine_state -> bool
 
@@ -30,14 +33,25 @@ module Compiler_logic
   type post 'a = 'a -> pos -> rel
 
   (* Hoare triples with explicit pre & post *)
-  type hl 'a = { code: code; ghost pre : pre 'a; ghost post: post 'a }
+  type hl 'a = { code: code; ghost pre : pre {'a}; ghost post: post {'a} }
+
+  (* (<%): pack the pre/post rewriting.
+     lock is an artifact to prevent unrolling of
+     h's definition recursively. *)
+  let function lock () : (int,int) =
+    ensures { result = (0,0) }
+    while false do variant { 0 } () done; (0,0)
+  predicate (<%) (h:hl 'a) (x:(pre 'a,post 'a)) =
+    let (pr,ps) = x in
+    h --> { code = let (_,_) = lock () in h.code; pre = pr; post = ps }
+  meta rewrite_def predicate (<%)
 
   (* Predicate transformer type. Same auxiliary variables as for
      Hoare triples. *)
   type wp_trans 'a = 'a -> pos -> pred -> pred
 
   (* Code with backward predicate transformer. *)
-  type wp 'a = { wcode : code; ghost wp : wp_trans 'a }
+  type wp 'a = { wcode : code; ghost wp : wp_trans {'a} }
 
   (* Machine transition valid whatever the global code is. *)
   predicate contextual_irrelevance (c:code) (p:pos) (ms1 ms2:machine_state) =
@@ -53,12 +67,9 @@ module Compiler_logic
     forall x:'a,p post ms. (code.wp x p post) ms ->
       exists ms'. post ms' /\ contextual_irrelevance code.wcode p ms ms'
 
-
   (* WP combinator for sequence. Similar to the standard WP calculus
      for sequence. The initial machine state is memorized in auxiliary
      variables for potential use in the second code specification. *)
-  (*** Technical: Why3 refuse the logic call in program,
-       so we cannot define it in function of (wp 'a) arguments only. *)
   function seq_wp
     (l1:int) (w1:wp_trans 'a) (w2:wp_trans ('a,machine_state)) : wp_trans 'a =
     fun x p q ms -> w1 x p (w2 (x,ms) (p+l1) q) ms
@@ -69,10 +80,10 @@ module Compiler_logic
   meta rewrite lemma seq_wp_lemma
 
   (* Code combinator for sequence, with wp. *)
-  let (~) (s1 : wp 'a) (s2 : wp ('a, machine_state)) : wp 'a
+  let (--) (s1 : wp 'a) (s2 : wp ('a, machine_state)) : wp 'a
     requires { wp_correctness s1 /\ wp_correctness s2 }
     ensures  { result.wcode.length = s1.wcode.length + s2.wcode.length }
-    ensures  { result.wp = seq_wp s1.wcode.length s1.wp s2.wp }
+    ensures  { result.wp --> seq_wp s1.wcode.length s1.wp s2.wp }
     ensures  { wp_correctness result }
   = let code = s1.wcode ++ s2.wcode in
     let res = { wcode = code; wp = seq_wp s1.wcode.length s1.wp s2.wp } in
@@ -94,9 +105,9 @@ module Compiler_logic
   (* Code combinator for conditional execution.
      Similar to WP calculus for (if cond then s). *)
 
-  let (%) (s:wp 'a) (ghost cond:pre 'a) : wp 'a
+  let (%) (s:wp 'a) (ghost cond:pre {'a}) : wp 'a
     requires { wp_correctness s }
-    ensures  { result.wp = fork_wp s.wp cond }
+    ensures  { result.wp --> fork_wp s.wp cond }
     ensures  { result.wcode.length = s.wcode.length /\ wp_correctness result }
   = { wcode = s.wcode; wp = fork_wp s.wp cond }
 
@@ -115,16 +126,17 @@ module Compiler_logic
   let ($_) (c:hl 'a) : wp 'a
     requires { hl_correctness c }
     ensures  { result.wcode.length = c.code.length }
-    ensures  { result.wp = towp_wp c.pre c.post /\ wp_correctness result }
+    ensures  { result.wp --> towp_wp c.pre c.post }
+    ensures  { wp_correctness result }
   = { wcode = c.code; wp = towp_wp c.pre c.post }
 
   (* Equip code with pre/post-condition. That is here that proof happen.
      (P -> wp (c,Q)). Anologous to checking function/abstract block
      specification. *)
-  let hoare (ghost pre:pre 'a) (c:wp 'a) (ghost post:post 'a) : hl 'a
+  let hoare (ghost pre:pre {'a}) (c:wp 'a) (ghost post:post {'a}) : hl 'a
     requires { wp_correctness c }
     requires { forall x p ms. pre x p ms -> (c.wp x p (post x p ms)) ms }
-    ensures  { result.pre = pre /\ result.post = post }
+    ensures  { result <% (pre,post) }
     ensures  { result.code.length = c.wcode.length /\ hl_correctness result}
   = { code = c.wcode ; pre = pre; post = post }
 
@@ -135,33 +147,43 @@ module Compiler_logic
   inductive acc ('a -> 'a -> bool) 'a =
     | Acc : forall r, x:'a. (forall y. r y x -> acc r y) -> acc r x
 
-  (* An iteration of the loop should make progress
-     towards the postcondition: either achieve the postcondition,
-     or preserve the invariant and "decrease" according to
-     a well-founded relation. *)
-  function loop_progress (inv post:pre 'a) (var:post 'a) : post 'a =
-    fun x p ms ms' -> (inv x p ms' /\ var x p ms' ms) \/ post x p ms'
-  meta rewrite_def function loop_progress
-
-  function forget_old (post:pre 'a) : post 'a =
-    fun x p _ -> post x p
-  meta rewrite_def function forget_old
-
-  (* Variant of hoare triplet introduction rule for looping code.
-     - inv is the loop invariant
-     - post is the loop postcondition
-     - var is a well-founded relation over states satisfying the
-       invariant. *)
-  let make_loop_hl (c:hl 'a) (ghost inv post:pre 'a) (ghost var:post 'a) : hl 'a
-    requires { hl_correctness c }
-    requires { forall x p ms. inv x p ms -> acc (var x p) ms }
-    requires { c.pre = inv }
-    requires { c.post = loop_progress inv post var }
-    ensures { result.pre = inv /\ result.post = forget_old post }
-    ensures { result.code.length = c.code.length /\ hl_correctness result }
-  = let res = { code = c.code ; pre = inv ; post = forget_old post } in
-    assert { forall x p ms.  inv x p ms -> acc (var x p) ms && exists ms'.
-      contextual_irrelevance res.code p ms ms' /\ forget_old post x p ms ms' };
+  (* Utility: some flavor of conjonction. *)
+  function pconj (p1:pred) (x:machine_state)
+                 (p2:machine_state -> pred) : pred =
+                 fun y -> p1 y && p2 y x
+  lemma pconj_lemma : forall p1 x p2 y. pconj p1 x p2 y <-> p1 y && p2 y x
+  meta rewrite lemma pconj_lemma
+
+  (* WP combinator for looping construction. Similar to weakest precondition
+     for while loops. *)
+
+  function loop_wp (w:wp_trans 'a) (inv cont:pre 'a)
+                                   (var:post 'a) : wp_trans 'a =
+    fun x p q ms -> inv x p ms && acc (var x p) ms && forall ms'. inv x p ms' ->
+      if cont x p ms'
+      then w x p (pconj (inv x p) ms' (var x p)) ms'
+      else w x p q ms'
+
+  lemma loop_wp_lemma : forall w:wp_trans 'a,inv cont var x p q ms.
+    loop_wp w inv cont var x p q ms <->
+      inv x p ms && acc (var x p) ms && forall ms'. inv x p ms' ->
+        (cont x p ms' -> w x p (pconj (inv x p) ms' (var x p)) ms')
+        /\ (not cont x p ms' -> w x p q ms')
+
+  meta rewrite lemma loop_wp_lemma
+
+  (* Code combinator for looping construct. *)
+  let make_loop (c:wp 'a) (ghost inv cont:pre {'a})
+                          (ghost var:post {'a}) : wp 'a
+    requires { wp_correctness c }
+    ensures { result.wp --> loop_wp c.wp inv cont var }
+    ensures { wp_correctness result }
+    ensures { result.wcode.length = c.wcode.length }
+  = let res = { wcode = c.wcode; wp = loop_wp c.wp inv cont var } in
+    assert { forall x p q ms0. res.wp x p q ms0 ->
+      forall ms. inv x p ms -> acc (var x p) ms ->
+        exists ms'. contextual_irrelevance res.wcode p ms ms' /\ q ms'
+    };
     res
 
 end

examples/double_wp/state/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+<file name="../state.why" expanded="true">
+<theory name="State" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
+</theory>
+</file>
+</why3session>