add in modified double_wp

extraction, bv32 and registers

README.md

+based on branch extract_bv32_reg

bv_op.mlw

+module BV_OP
+  
+  use bv.BV32  
+  
+  let function bv_add i1 i2:int 
+    ensures { 
+      result = BV32.to_int (BV32.add (BV32.of_int i1) (BV32.of_int i2))
+    }
+  =
+    let v1: BV32.t = BV32.of_int i1 in
+    let v2: BV32.t = BV32.of_int i2 in
+    let v: BV32.t = BV32.add v1 v2 in
+    BV32.to_int v 
+  
+  meta rewrite_def function bv_add
+
+  (*meta rewrite_def function bv_add
+  (* stupid test *)
+  use int.Int
+  use bv.BV32 
+  (*
+  constant bv_add : int -> int -> int = fun x y -> x + y 
+  *)
+
+  let function bv_add i1 i2:int 
+      ensures { 
+        result = i1 + i2
+      }
+    = i1 + i2
+
+  meta rewrite_def function bv_add
+  
+  (*
+  lemma bv_add_com:
+    forall v1 v2. bv_add v1 v2 = bv_add v2 v1
+  *)
+  *)
+end
\ No newline at end of file

bv_op/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="5">
+<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="2000"/>
+<file name="../bv_op.mlw" proved="true">
+<theory name="BV_OP" proved="true">
+ <goal name="VC bv_add" expl="VC for bv_add" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="70"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>

com_aexpr.mlw

+(* Register based compiler for arithmetic expressions *)
+
+module Compile_aexpr_reg
+
+  use int.Int
+  use list.List
+  use list.Length
+  use list.Append
+  use imp.Imp
+  use vm.Vm
+  use state.State
+  use state.Reg
+  use logic.Compiler_logic
+  use specs.VM_instr_spec
+
+  (* Compilation scheme: the generated code for arithmetic expressions
+     put the result of the expression on the stack. *)
+  function aexpr_post (a:aexpr) (len:pos) (idr:idr) : post 'a =
+    fun _ p ms ms' -> 
+      let VMS p1 r1 s1 m1 = ms in 
+      let VMS p2 r2 s2 m2 = ms' in
+      p1 = p /\
+      p2 = p + len /\ 
+      (forall r'. r' < idr -> read r1 r' = read r2 r') /\ (* preserve lower registers *)
+      read r2 idr  = aeval m1 a /\ (* result in idr *)
+      s2 = s1 /\ (* preserve stack *) 
+      m2 = m1 (* preserve memory *)
+      
+  meta rewrite_def function aexpr_post
+
+  let rec compile_aexpr (a:aexpr) (idr: idr) :  hl 'a
+    ensures { result.pre --> trivial_pre }
+    ensures { result.post --> aexpr_post a result.code.length idr}
+    variant { a }
+    = let c = match a with
+      | Anum n      -> $ iimmf idr n
+      | Avar x      -> $ iloadf idr x 
+      | Aadd a1 a2  -> $ 
+        compile_aexpr a1 idr -- $ compile_aexpr a2 (idr + 1) -- $ iaddrf (idr + 1) idr idr
+      | Aaddu a1 a2 -> $ 
+        compile_aexpr a1 idr -- $ compile_aexpr a2 (idr + 1) -- $ iaddurf (idr + 1) idr idr
+      | Asub a1 a2  -> $ 
+        compile_aexpr a2 idr -- $ compile_aexpr a1 (idr + 1) -- $ isubrf (idr + 1) idr idr
+      end in
+      hoare trivial_pre c (aexpr_post a c.wcode.length idr)
+
+  (* Check that the above specification indeed implies the
+     natural one. *)
+  
+   let compile_aexpr_natural (a:aexpr) (idr:idr) : code
+    ensures { forall c p r1 s m. codeseq_at c p result ->
+        exists r2.
+        transition_star c (VMS p r1 s m)
+                          (VMS (p + length result) r2 s m) 
+        /\
+        forall r. r < idr -> read r2 r = read r1 r  /\
+        read r2 idr = aeval m a  
+    }
+  = let res = compile_aexpr a idr : hl unit in
+    assert { res.pre = trivial_pre }; (* we have a trivial precod *)
+    assert { forall p r s m. res.pre () p (VMS p r s m) }; 
+ 
+    assert { forall p ms. res.pre () p ms ->
+      exists ms'. 
+      res.post () p ms ms' /\ contextual_irrelevance res.code p ms ms' /\
+      let VMS p1 r1 s1 m1 = ms in
+      let VMS p2 r2 s2 m2 = ms' in
+      p2 = p1 + res.code.length /\ m2 = m1 /\ s2 = s1 /\ 
+      forall r. r < idr -> read r2 r = read r1 r  /\
+      read r2 idr = aeval m1 a    
+    };
+    
+    res.code
+
+end
+
+(*
+(* Register based compiler for arithmetic expressions, k registers *)
+module Compile_aexpr_reg_k
+
+  use int.Int
+  use list.List
+  use list.Length
+  use list.Append
+  use imp.Imp
+  use vm.Vm
+  use state.State
+  use state.Reg
+  use logic.Compiler_logic
+  use specs.VM_instr_spec
+
+  (** we have k registers, namely 0,1,...,k-1,
+      and there are at least two of them, otherwise we can't add *)
+  val constant k: int
+    ensures { 2 <= result }
+    
+  (* Compilation scheme: the generated code for arithmetic expressions
+     put the result of the expression on the stack. *)
+  function aexpr_post (a:aexpr) (len:pos) (idr:idr) : post 'a =
+    fun _ p ms ms' -> 
+      let VMS p1 r1 s1 m1 = ms in 
+      let VMS p2 r2 s2 m2 = ms' in
+      p1 = p /\
+      p2 = p + len /\ 
+      (forall r'. r' < idr -> read r1 r' = read r2 r') /\ (* preserve lower registers *)
+      read r2 idr  = aeval m1 a /\ (* result in idr *)
+      s2 = s1 /\ (* preserve stack *) 
+      m2 = m1 (* preserve memory *)
+      
+  meta rewrite_def function aexpr_post
+
+  let rec compile_aexpr (a:aexpr) (idr: idr) :  hl 'a
+    requires { 0 <= idr < k }
+    ensures { result.pre --> trivial_pre }
+    ensures { result.post --> aexpr_post a result.code.length idr}
+    variant { a }
+    = let c = match a with
+      | Anum n     -> $ iimmf idr n
+      | Avar x     -> $ iloadf idr x 
+      | Aadd a1 a2 -> 
+        if idr < k - 1 then 
+          $ compile_aexpr a1 idr --  
+          $ compile_aexpr a2 (idr + 1) --  
+          $ iaddrf (idr + 1) idr idr
+        else 
+          $ ipushf (k - 2) -- 
+          $ compile_aexpr a1 (k - 2) -- 
+          $ compile_aexpr a2 (k - 1) --
+          $ iaddrf (k - 2) (k - 1) (k - 1)--
+          $ ipopf (k - 2)           
+        
+      | Asub a1 a2 -> 
+        if idr < k - 1 then 
+          $ compile_aexpr a2 idr -- 
+          $ compile_aexpr a1 (idr + 1) -- 
+          $ isubrf (idr + 1) idr idr
+        else 
+          $ ipushf (k - 2) -- 
+          $ compile_aexpr a1 (k - 2) -- 
+          $ compile_aexpr a2 (k - 1) --
+          $ isubrf (k - 2) (k - 1) (k - 1) --
+          $ ipopf (k - 2) 
+      end in
+      hoare trivial_pre c (aexpr_post a c.wcode.length idr)
+
+  (* Check that the above specification indeed implies the
+     natural one. *)
+  
+   let compile_aexpr_natural (a:aexpr) (idr:idr) : code
+    requires { 0 <= idr < k }
+    ensures { forall c p r1 s m. codeseq_at c p result ->
+        exists r2.
+        transition_star c (VMS p r1 s m)
+                          (VMS (p + length result) r2 s m) 
+        /\
+        forall r. r < idr -> read r2 r = read r1 r  /\
+        read r2 idr = aeval m a  
+    }
+  = let res = compile_aexpr a idr : hl unit in
+    assert { res.pre = trivial_pre }; (* we have a trivial precod *)
+    assert { forall p r s m. res.pre () p (VMS p r s m) }; 
+ 
+    assert { forall p ms. res.pre () p ms ->
+      exists ms'. 
+      res.post () p ms ms' /\ contextual_irrelevance res.code p ms ms' /\
+      let VMS p1 r1 s1 m1 = ms in
+      let VMS p2 r2 s2 m2 = ms' in
+      p2 = p1 + res.code.length /\ m2 = m1 /\ s2 = s1 /\ 
+      forall r. r < idr -> read r2 r = read r1 r  /\
+      read r2 idr = aeval m1 a    
+    };
+    
+    res.code
+
+end
+
+(* Register based compiler for arithmetic expressions, optimal k registers *)
+module Compile_aexpr_reg_k_optimal
+
+  use int.Int
+  use int.MinMax
+  use list.List
+  use list.Length
+  use list.Append
+  use imp.Imp
+  use vm.Vm
+  use state.State
+  use state.Reg
+  use logic.Compiler_logic
+  use specs.VM_instr_spec
+
+  (** we have k registers, namely 0,1,...,k-1,
+      and there are at least two of them, otherwise we can't add *)
+  val constant k: int
+    ensures { 2 <= result }
+    
+  (** the minimal number of registers needed to evaluate e *)
+  let rec function n (e: aexpr) : int
+  variant { e }
+  ensures { result > 0 }
+  = match e with
+    | Anum _     -> 1
+    | Avar _     -> 1
+    | Aadd e1 e2 -> let n1 = n e1 in let n2 = n e2 in
+                    if n1 = n2 then 1 + n1 else max n1 n2
+    | Asub e1 e2 -> let n1 = n e1 in let n2 = n e2 in
+                    if n1 = n2 then 1 + n1 else max n1 n2
+    end
+  meta rewrite_def function n
+  
+  
+  (** Note: This is of course inefficient to recompute function `n` many
+      times. A realistic implementation would compute `n e` once for
+      each sub-expression `e`, either with a first pass of tree decoration,
+      or with function `compile` returning the value of `n e` as well,
+      in a bottom-up way *)
+
+  function measure (e: aexpr) : int =
+    match e with
+    | Anum _      -> 0
+    | Avar _      -> 0
+    | Aadd e1 e2  -> 1 + measure e1 + measure e2 + if n e1 >= n e2 then 0 else 1 
+    | Aaddu e1 e2 -> 1 + measure e1 + measure e2 + if n e1 >= n e2 then 0 else 1 
+    | Asub e1 e2  -> 1 + measure e1 + measure e2 + if n e1 >= n e2 then 0 else 1
+    end
+
+  lemma measure_nonneg: forall e. measure e >= 0
+    
+  (* Compilation scheme: the generated code for arithmetic expressions
+     put the result of the expression on the stack. *)
+  function aexpr_post (a:aexpr) (len:pos) (idr:idr) : post 'a =
+    fun _ p ms ms' -> 
+      let VMS p1 r1 s1 m1 = ms in 
+      let VMS p2 r2 s2 m2 = ms' in
+      p1 = p /\
+      p2 = p + len /\ 
+      (forall r'. r' < idr -> read r1 r' = read r2 r') /\ (* preserve lower registers *)
+      read r2 idr  = aeval m1 a /\ (* result in idr *)
+      s2 = s1 /\ (* preserve stack *) 
+      m2 = m1 (* preserve memory *)
+      
+  meta rewrite_def function aexpr_post
+
+  let rec compile_aexpr (a:aexpr) (idr: idr) (ghost left: int) :  hl 'a
+    requires { n a <= left } 
+    requires { 0 <= idr < k }
+    variant  { measure a }
+    ensures  { result.pre --> trivial_pre }
+    ensures  { result.post --> aexpr_post a result.code.length idr }
+    = 
+      let c = match a with
+      | Anum n     -> $ iimmf idr n
+      | Avar x     -> $ iloadf idr x 
+      | Aadd a1 a2 -> 
+        if n a1 >= n a2 then (* we compile a1 first *)
+          if idr < k - 1 then 
+            $ compile_aexpr a1 idr left --  
+            $ compile_aexpr a2 (idr + 1) (left - 1) --  
+            $ iaddrf (idr + 1) idr idr
+          else 
+            (
+            assert { idr = k - 1 }; 
+            $ ipushf (idr - 1) -- 
+            $ compile_aexpr a1 (idr - 1) (left + 1) -- 
+            $ compile_aexpr a2 idr left --
+            $ iaddrf (idr - 1) idr idr --
+            $ ipopf (idr - 1)
+            )
+        else (* we compile a2 first, by swapping *)
+          $ compile_aexpr (Aadd a2 a1) idr left 
+      | Asub a1 a2 -> 
+        if idr < k - 1 then 
+          if n a1 >= n a2 then (* we compile a1 first *)
+            $ compile_aexpr a1 idr left -- 
+            $ compile_aexpr a2 (idr + 1) (left - 1) -- 
+            $ isubrf idr (idr + 1) idr
+          else
+            $ compile_aexpr a2 idr left -- 
+            $ compile_aexpr a1 (idr + 1) (left - 1) -- 
+            $ isubrf (idr + 1) idr idr
+        else 
+          $ ipushf (idr - 1) -- 
+          $ compile_aexpr a1 (idr - 1) (left + 1) -- 
+          $ compile_aexpr a2 idr left --
+          $ isubrf (idr - 1) idr idr --
+          $ ipopf (idr - 1) 
+      
+      end in
+      hoare trivial_pre c (aexpr_post a c.wcode.length idr)
+
+  (* Check that the above specification indeed implies the
+     natural one. *)
+  
+   let compile_aexpr_natural (a:aexpr) (idr:idr) : code
+    requires { 0 <= idr < k }
+    ensures { forall c p r1 s m. codeseq_at c p result ->
+        exists r2.
+        transition_star c (VMS p r1 s m)
+                          (VMS (p + length result) r2 s m) 
+        /\
+        forall r. r < idr -> read r2 r = read r1 r  /\
+        read r2 idr = aeval m a  
+    }
+  = let res = compile_aexpr a idr (ghost n a): hl unit in
+    assert { res.pre = trivial_pre }; (* we have a trivial precod *)
+    assert { forall p r s m. res.pre () p (VMS p r s m) }; 
+ 
+    assert { forall p ms. res.pre () p ms ->
+      exists ms'. 
+      res.post () p ms ms' /\ contextual_irrelevance res.code p ms ms' /\
+      let VMS p1 r1 s1 m1 = ms in
+      let VMS p2 r2 s2 m2 = ms' in
+      p2 = p1 + res.code.length /\ m2 = m1 /\ s2 = s1 /\ 
+      forall r. r < idr -> read r2 r = read r1 r  /\
+      read r2 idr = aeval m1 a    
+    };
+    
+    res.code
+   
+end
+
+*)

extract.sh

+#!/bin/sh
+echo "why3 extract --recursive --modular -D ocaml64 -D ocaml64_bv.drv *.mlw -o ../../ocaml/extract -L ."
+why3 extract --recursive --modular -D ocaml64 -D ocaml64_bv.drv *.mlw -o ../../ocaml/extract -L .

imp.mlw

+theory Imp
+
+  use state.State
+  use bool.Bool
+  use int.Int
+  use bv_op.BV_OP
+
+  (* ************************ SYNTAX ************************ *)
+  type aexpr =
+    | Anum int
+    | Avar id
+    | Aadd aexpr aexpr 
+    | Asub aexpr aexpr
+    | Aaddu aexpr aexpr
+
+  type bexpr =
+    | Btrue
+    | Bfalse
+    | Bnot bexpr
+    | Beq aexpr aexpr
+    | Ble aexpr aexpr
+    | Band bexpr bexpr
+    
+  type com =
+    | Cskip
+    | Cassign id aexpr
+    | Cseq com com
+    | Cif bexpr com com
+    | Cwhile bexpr com
+
+
+  (* ************************  SEMANTICS ************************ *)
+  function aeval  (st:state) (e:aexpr) : int =
+    match e with
+      | Anum n      -> n
+      | Avar x      -> st[x]
+      | Aadd e1 e2  -> aeval st e1 + aeval st e2
+      | Asub e1 e2  -> aeval st e1 - aeval st e2
+      | Aaddu e1 e2 -> bv_add (aeval st e1) (aeval st e2)
+    end
+
+  function beval (st:state) (b:bexpr) : bool =
+    match b with
+      | Btrue      -> true
+      | Bfalse     -> false
+      | Bnot b'    -> notb (beval st b')
+      | Beq a1 a2  -> aeval st a1 = aeval st a2
+      | Ble a1 a2  -> aeval st a1 <= aeval st a2  
+      | Band b1 b2 -> andb (beval st b1) (beval st b2)
+      
+    end
+
+  inductive ceval state com state =
+    (* skip *)
+    | E_Skip : forall m. ceval m Cskip m
+
+    (* assignement *)
+    | E_Ass  : forall m a x. ceval m (Cassign x a) m[x <- aeval m a]
+
+    (* sequence *)
+    | E_Seq : forall cmd1 cmd2 m0 m1 m2.
+        ceval m0 cmd1 m1 -> ceval m1 cmd2 m2 -> ceval m0 (Cseq cmd1 cmd2) m2
+
+    (* if then else *)
+    | E_IfTrue : forall m0 m1 cond cmd1 cmd2. beval m0 cond ->
+        ceval m0 cmd1 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
+
+    | E_IfFalse : forall m0 m1 cond cmd1 cmd2. not beval m0 cond ->
+        ceval m0 cmd2 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
+
+    (* while *)
+    | E_WhileEnd : forall cond m body. not beval m cond ->
+        ceval m (Cwhile cond body) m
+
+    | E_WhileLoop : forall mi mj mf cond body. beval mi cond ->
+        ceval mi body mj -> ceval mj (Cwhile cond body) mf ->
+          ceval mi (Cwhile cond body) mf
+
+
+  (* Determinstic semantics *)
+  lemma ceval_deterministic_aux : forall c mi mf1. ceval mi c mf1 ->
+      forall mf2. ([@inversion] ceval mi c mf2) -> mf1 = mf2
+
+  lemma ceval_deterministic : forall c mi mf1 mf2.
+      ceval mi c mf1 ->  ceval mi c mf2 -> mf1 = mf2
+
+end
+

imp_ex_assignment.mlw

+module Imp_ex
+
+  use imp.Imp
+  use state.State
+  use bool.Bool
+  use int.Int
+  use bv_op.BV_OP 
+
+  let rec aeval_ex  (st:state) (e:aexpr) : int 
+    variant { e }
+    ensures { result = aeval st e }
+  =
+    match e with
+      | Anum n      -> n
+      | Avar x      -> st[x]
+      | Aadd e1 e2  -> aeval_ex st e1 + aeval_ex st e2
+      | Aaddu e1 e2 -> bv_add (aeval_ex st e1) (aeval_ex st e2)
+      | Asub e1 e2  -> aeval_ex st e1 - aeval_ex st e2
+    end
+
+
+  let rec beval_ex (st:state) (b:bexpr) : bool 
+    variant { b }
+    ensures { result = beval st b }
+  =
+    match b with
+      | Btrue      -> true
+      | Bfalse     -> false
+      | Bnot b'    -> notb (beval_ex st b')
+      | Band b1 b2 -> andb (beval_ex st b1) (beval_ex st b2)
+      | Beq a1 a2  -> aeval_ex st a1 = aeval_ex st a2
+      | Ble a1 a2  -> aeval_ex st a1 <= aeval_ex st a2
+    end
+
+
+  let rec ceval_ex (st:state) (c:com): state
+    (* diverges (* uncomment when actually diverging*) *)   
+    ensures { ceval st c result }
+    =
+    match c with
+    | Cskip -> st
+    | Cassign id aexpr -> st
+    | Cseq c1 c2 -> st 
+    | Cif bexpr c1 c2 -> st
+    | Cwhile bexpr com -> st
+    end
+end
\ No newline at end of file

imp_test.mlw

+module Imp_test
+
+  use state.State
+  use imp.Imp
+  use int.Int
+
+  constant st : state = const 0
+  
+  goal ex1: (* 1 + 2 *)
+    aeval st (Aadd (Anum 1) (Anum 2)) = 3
+    
+  goal ex2: (* (1 - 2) + 2 *)
+    aeval st (Aadd (Asub (Anum 1) (Anum 2)) (Anum 2)) = 1
+    
+  goal ex3: (* a = 0, a + 2 *) 
+    aeval st (Aadd (Avar (Id 1)) (Anum 2)) = 2
+
+  goal ex4: (* a = 7, a + 2 *)
+    let st' = st[(Id 1) <- 7] in (* <-- update the state, st[Id 1] = 7 *)
+    aeval st' (Aadd (Avar (Id 1)) (Anum 2)) = 9
+
+  constant a_id : id = Id 1 (* <-- we introduce the constant a_id *)
+  
+  goal ex5: (* a = 7, a + 2 *)
+    let st = st[a_id <- 7] in        (* <-- used in the following *)
+    aeval st (Aadd (Avar a_id) (Anum 2)) = 9 
+    
+  goal ex6: (* on primitive "+" *)
+    forall a. a > 2 -> 2 + a > 4  
+    
+  goal ex7: (* addition on "imp" expression *)
+    forall a. a > 2 ->
+    aeval st (Aadd (Anum a) (Anum 2)) > 4
+
+  goal ex8: (* addition via state *)
+    forall a. a > 2 ->
+      let st = st[a_id <- a] in 
+      aeval st (Aadd (Avar a_id) (Anum 2)) > 4
+    
+end

imp_test/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="5">
+<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<file name="../state.mlw" proved="true">
+<theory name="State" proved="true">
+ <goal name="VC get" expl="VC for get" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC set" expl="VC for set" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC mixfix []" expl="VC for mixfix []" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC mixfix [&lt;-]" expl="VC for mixfix [<-]" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC const" expl="VC for const" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+<theory name="Reg" proved="true">
+ <goal name="VC read" expl="VC for read" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC write" expl="VC for write" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC const" expl="VC for const" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../imp_test.mlw">
+<theory name="Imp_test">
+ <goal name="ex1">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="82"/></proof>
+ </goal>
+ <goal name="ex2">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="101"/></proof>
+ </goal>
+ <goal name="ex3">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof>
+ <proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
+ </goal>
+ <goal name="ex4" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="97"/></proof>
+ </goal>
+ <goal name="ex5">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof>
+ </goal>
+ <goal name="ex6">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="74"/></proof>
+ </goal>
+ <goal name="ex7">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="84"/></proof>
+ </goal>
+ <goal name="ex8">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="100"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../imp_ex.mlw" proved="true">
+<theory name="Imp_Ex" proved="true">
+ <goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true">
+ <proof prover="0"><result status="valid" time="0.52" steps="783"/></proof>
+ </goal>
+ <goal name="VC beval_ex" expl="VC for beval_ex" proved="true">
+ <proof prover="0"><result status="valid" time="0.22" steps="667"/></proof>
+ </goal>
+ <goal name="VC ceval_ex" expl="VC for ceval_ex" proved="true">
+ <proof prover="0"><result status="valid" time="0.08" steps="237"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../imp_ex_assignment.mlw">
+<theory name="Imp_ex">
+ <goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true">
+ <proof prover="0"><result status="valid" time="0.68" steps="783"/></proof>
+ </goal>
+ <goal name="VC beval_ex" expl="VC for beval_ex" proved="true">
+ <proof prover="0"><result status="valid" time="0.20" steps="667"/></proof>
+ </goal>
+ <goal name="VC ceval_ex" expl="VC for ceval_ex">
+ <transf name="split_vc" >
+  <goal name="VC ceval_ex.0" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="74"/></proof>
+  </goal>
+  <goal name="VC ceval_ex.1" expl="postcondition">
+  <proof prover="0"><result status="timeout" time="1.00"/></proof>
+  </goal>
+  <goal name="VC ceval_ex.2" expl="postcondition">
+  <proof prover="0"><result status="timeout" time="1.00"/></proof>
+  </goal>
+  <goal name="VC ceval_ex.3" expl="postcondition">
+  <proof prover="0"><result status="timeout" time="1.00"/></proof>
+  </goal>
+  <goal name="VC ceval_ex.4" expl="postcondition">
+  <proof prover="0"><result status="timeout" time="1.00"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+<file name="../imp.mlw" proved="true">
+<theory name="Imp" proved="true">
+ <goal name="ceval_deterministic_aux" proved="true">
+ <transf name="induction_pr" proved="true" >
+  <goal name="ceval_deterministic_aux.0" proved="true">
+  <proof prover="0"><result status="valid" time="0.05" steps="135"/></proof>
+  </goal>
+  <goal name="ceval_deterministic_aux.1" proved="true">
+  <proof prover="0"><result status="valid" time="0.08" steps="180"/></proof>
+  </goal>
+  <goal name="ceval_deterministic_aux.2" proved="true">
+  <transf name="induction_pr" proved="true" >
+   <goal name="ceval_deterministic_aux.2.0" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.2.1" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.2.2" proved="true">
+   <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
+   <proof prover="1"><result status="valid" time="0.11"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.2.3" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.2.4" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.2.5" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.2.6" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="ceval_deterministic_aux.3" proved="true">
+  <transf name="induction_pr" proved="true" >
+   <goal name="ceval_deterministic_aux.3.0" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.3.1" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.3.2" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.3.3" proved="true">
+   <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
+   <proof prover="1"><result status="valid" time="0.06"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.3.4" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.3.5" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="85"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.3.6" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="ceval_deterministic_aux.4" proved="true">
+  <transf name="induction_pr" proved="true" >
+   <goal name="ceval_deterministic_aux.4.0" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.4.1" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.4.2" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.4.3" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.4.4" proved="true">
+   <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
+   <proof prover="1"><result status="valid" time="0.06"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.4.5" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.4.6" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="ceval_deterministic_aux.5" proved="true">
+  <proof prover="0"><result status="valid" time="0.05" steps="133"/></proof>
+  </goal>
+  <goal name="ceval_deterministic_aux.6" proved="true">
+  <transf name="induction_pr" proved="true" >
+   <goal name="ceval_deterministic_aux.6.0" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.6.1" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.6.2" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.6.3" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.6.4" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.6.5" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.6.6" proved="true">
+   <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
+   <proof prover="1"><result status="valid" time="0.11"/></proof>
+   </goal>
+  </transf>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="107"/></proof>
+ </goal>
+ <goal name="VC beval">
+ <proof prover="0"><result status="valid" time="0.02" steps="73"/></proof>
+ </goal>
+ <goal name="VC aeval">
+ <proof prover="0"><result status="valid" time="0.01" steps="73"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>

imp_test/why3session.xml.bak

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<file name="../state.mlw" proved="true">
+<theory name="State" proved="true">
+ <goal name="VC get" expl="VC for get" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC set" expl="VC for set" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC mixfix []" expl="VC for mixfix []" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC mixfix [&lt;-]" expl="VC for mixfix [<-]" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC const" expl="VC for const" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+<theory name="Reg" proved="true">
+ <goal name="VC read" expl="VC for read" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC write" expl="VC for write" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC const" expl="VC for const" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../imp_test.mlw">
+<theory name="Imp_test">
+ <goal name="ex1" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="82"/></proof>
+ </goal>
+ <goal name="ex2" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="101"/></proof>
+ </goal>
+ <goal name="ex3" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="97"/></proof>
+ <proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
+ </goal>
+ <goal name="ex4">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof>
+ </goal>
+ <goal name="ex5">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof>
+ </goal>
+ <goal name="ex6">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="74"/></proof>
+ </goal>
+ <goal name="ex7">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="84"/></proof>
+ </goal>
+ <goal name="ex8">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="100"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../imp_ex_assignment.mlw">
+<theory name="Imp_ex">
+ <goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true">
+ <proof prover="0"><result status="valid" time="0.68" steps="783"/></proof>
+ </goal>
+ <goal name="VC beval_ex" expl="VC for beval_ex" proved="true">
+ <proof prover="0"><result status="valid" time="0.20" steps="667"/></proof>
+ </goal>
+ <goal name="VC ceval_ex" expl="VC for ceval_ex">
+ <transf name="split_vc" >
+  <goal name="VC ceval_ex.0" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="74"/></proof>
+  </goal>
+  <goal name="VC ceval_ex.1" expl="postcondition">
+  <proof prover="0"><result status="timeout" time="1.00"/></proof>
+  </goal>
+  <goal name="VC ceval_ex.2" expl="postcondition">
+  <proof prover="0"><result status="timeout" time="1.00"/></proof>
+  </goal>
+  <goal name="VC ceval_ex.3" expl="postcondition">
+  <proof prover="0"><result status="timeout" time="1.00"/></proof>
+  </goal>
+  <goal name="VC ceval_ex.4" expl="postcondition">
+  <proof prover="0"><result status="timeout" time="1.00"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+<file name="../imp_ex.mlw" proved="true">
+<theory name="Imp_Ex" proved="true">
+ <goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true">
+ <proof prover="0"><result status="valid" time="0.52" steps="783"/></proof>
+ </goal>
+ <goal name="VC beval_ex" expl="VC for beval_ex" proved="true">
+ <proof prover="0"><result status="valid" time="0.22" steps="667"/></proof>
+ </goal>
+ <goal name="VC ceval_ex" expl="VC for ceval_ex" proved="true">
+ <proof prover="0"><result status="valid" time="0.08" steps="237"/></proof>
+ </goal>
+</theory>
+</file>
+<file name="../imp.mlw" proved="true">
+<theory name="Imp" proved="true">
+ <goal name="ceval_deterministic_aux" proved="true">
+ <transf name="induction_pr" proved="true" >
+  <goal name="ceval_deterministic_aux.0" proved="true">
+  <proof prover="0"><result status="valid" time="0.05" steps="135"/></proof>
+  </goal>
+  <goal name="ceval_deterministic_aux.1" proved="true">
+  <proof prover="0"><result status="valid" time="0.08" steps="180"/></proof>
+  </goal>
+  <goal name="ceval_deterministic_aux.2" proved="true">
+  <transf name="induction_pr" proved="true" >
+   <goal name="ceval_deterministic_aux.2.0" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.2.1" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.2.2" proved="true">
+   <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
+   <proof prover="1"><result status="valid" time="0.11"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.2.3" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.2.4" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.2.5" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.2.6" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="ceval_deterministic_aux.3" proved="true">
+  <transf name="induction_pr" proved="true" >
+   <goal name="ceval_deterministic_aux.3.0" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.3.1" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.3.2" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.3.3" proved="true">
+   <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
+   <proof prover="1"><result status="valid" time="0.06"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.3.4" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.3.5" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="85"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.3.6" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="ceval_deterministic_aux.4" proved="true">
+  <transf name="induction_pr" proved="true" >
+   <goal name="ceval_deterministic_aux.4.0" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.4.1" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.4.2" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.4.3" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.4.4" proved="true">
+   <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
+   <proof prover="1"><result status="valid" time="0.06"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.4.5" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.4.6" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="ceval_deterministic_aux.5" proved="true">
+  <proof prover="0"><result status="valid" time="0.05" steps="133"/></proof>
+  </goal>
+  <goal name="ceval_deterministic_aux.6" proved="true">
+  <transf name="induction_pr" proved="true" >
+   <goal name="ceval_deterministic_aux.6.0" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.6.1" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.6.2" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.6.3" proved="true">
+   <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.6.4" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.6.5" proved="true">
+   <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
+   </goal>
+   <goal name="ceval_deterministic_aux.6.6" proved="true">
+   <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
+   <proof prover="1"><result status="valid" time="0.11"/></proof>
+   </goal>
+  </transf>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="ceval_deterministic" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="107"/></proof>
+ </goal>
+ <goal name="VC beval">
+ <proof prover="0"><result status="valid" time="0.02" steps="73"/></proof>
+ </goal>
+ <goal name="VC aeval">
+ <proof prover="0"><result status="valid" time="0.01" steps="73"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>