update sessions

examples/double_wp/compiler.mlw

@@ -6,7 +6,6 @@
 (* Compiler for arithmetic expressions *)
 module Compile_aexpr
 
-  meta compute_max_steps 0x10000
 
   use import int.Int
   use import list.List

examples/double_wp/compiler/compiler_Compile_com_WP_parameter_compile_com_1.v

@@ -2,6 +2,7 @@
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.
+Require HighOrd.
 Require int.Int.
 Require int.Abs.
 Require int.EuclideanDivision.
@@ -38,12 +39,6 @@ Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
   {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
   forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
 
-Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
-  b -> (map a b).
-
-Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
-  forall (b1:b) (a1:a), ((get (const b1: (map a b)) a1) = b1).
-
 (* Why3 assumption *)
 Inductive id :=
   | Id : Z -> id.
@@ -318,17 +313,6 @@ Definition vm_terminates (c:(list instr)) (mi:(map id Z)) (mf:(map id
   (Init.Datatypes.cons Ihalt Init.Datatypes.nil)) /\ (transition_star c
   (VMS 0%Z Init.Datatypes.nil mi) (VMS p Init.Datatypes.nil mf)).
 
-Axiom func : forall (a:Type) (b:Type), Type.
-Parameter func_WhyType : forall (a:Type) {a_WT:WhyType a}
-  (b:Type) {b_WT:WhyType b}, WhyType (func a b).
-Existing Instance func_WhyType.
-
-(* Why3 assumption *)
-Definition pred (a:Type) := (a -> bool).
-
-Parameter infix_at: forall {a:Type} {a_WT:WhyType a}
-  {b:Type} {b_WT:WhyType b}, (a -> b) -> a -> b.
-
 (* Why3 assumption *)
 Definition fst {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} (p:(a*
   b)%type): a := match p with
@@ -342,7 +326,7 @@ Definition snd {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} (p:(a*
   end.
 
 (* Why3 assumption *)
-Definition pred1 := (machine_state -> bool).
+Definition pred := (machine_state -> bool).
 
 (* Why3 assumption *)
 Definition rel := (machine_state -> (machine_state -> bool)).
@@ -806,7 +790,7 @@ Axiom loop_variant_def : forall {a:Type} {a_WT:WhyType a}, forall (c:com)
   end.
 
 Require Import Why3.
-Ltac ae := why3 "Alt-Ergo,0.95.2,".
+Ltac ae := why3 "Alt-Ergo,0.99.1,".
 Ltac cvc := why3 "CVC4,1.4,".
 
 (* Why3 goal *)

examples/double_wp/specs.mlw

 
 module VM_instr_spec
 
+  meta compute_max_steps 0x10000
+
   use import int.Int
   use import list.List
   use import list.Length
@@ -148,11 +150,12 @@ module VM_instr_spec
         if cond n1 n2 then VMS (p+ofs+1) s m else VMS (p+1) s m
       | _ -> ms
       end
+  meta rewrite_def function icjump_fun
 
   let create_cjump (code_cd:code) (ghost cond:cond) (ghost ofs:ofs) : hl 'a
-    requires { forall c p1 n1 n2. codeseq_at c p1 code_cd ->
-      let p2 = (if cond n1 n2 then p1 + 1 + ofs else p1 + 1) in
-      forall s m. transition c (VMS p1 (push n2 (push n1 s)) m) (VMS p2 s m) }
+    requires { forall c p1 n1 n2 s m. codeseq_at c p1 code_cd ->
+      let p2 = (if cond n1 n2 then p1 + ofs + 1 else p1 + 1) in
+      transition c (VMS p1 (push n2 (push n1 s)) m) (VMS p2 s m) }
     ensures { result.pre = ibinop_pre /\ result.post = icjump_post cond ofs }
     ensures { result.code.length = code_cd.length /\ hl_correctness result }
   = let c = $ ifunf ibinop_pre code_cd (icjump_fun cond ofs) in
@@ -206,6 +209,7 @@ module VM_instr_spec
       | VMS p (Cons n s) m -> VMS (p+1) s m[x <- n]
       | _ -> ms
       end
+  meta rewrite_def function isetvar_fun
 
   let isetvarf (x: id) : hl 'a
     ensures { result.pre  = isetvar_pre /\ result.post = isetvar_post x  }