preliminary version of machine arithmetic

bench/bench

@@ -96,6 +96,7 @@ echo ""
 
 echo "=== Checking modules ==="
 goods modules
+goods modules/mach
 echo ""
 
 echo "=== Checking bad files ==="

examples/binary_search.mlw

@@ -88,87 +88,35 @@ end
 
 module BinarySearchInt32
 
-  use import arith.Int32
+  use import mach.int.Int32
   use import ref.Ref
-  use import array.Array
+  use import mach.array.Array32
 
   (* the code and its specification *)
 
-  exception Break int (* raised to exit the loop *)
-  exception Not_found (* raised to signal a search failure *)
+  exception Break int32 (* raised to exit the loop *)
+  exception Not_found   (* raised to signal a search failure *)
 
-  let binary_search (a : array int) (v : int)
-    requires { length a <= max_int }
-    requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
-    ensures  { 0 <= result < length a /\ a[result] = v }
-    raises   { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
+  let binary_search (a : array int32) (v : int32)
+    requires { forall i1 i2 : int. 0 <= i1 <= i2 < to_int a.length ->
+               to_int a[i1] <= to_int a[i2] }
+    ensures  { 0 <= to_int result < to_int a.length /\ a[to_int result] = v }
+    raises   { Not_found ->
+                 forall i:int. 0 <= i < to_int a.length -> a[i] <> v }
   = try
-      let l = ref 0 in
-      let u = ref (length a - 1) in
+      let l = ref (of_int 0) in
+      let u = ref (length a - of_int 1) in
       while !l <= !u do
-        invariant { 0 <= !l /\ !u < length a }
-        invariant {
-          forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
-        variant { !u - !l }
-        let m = !l + div (!u - !l) 2 in
-        assert { !l <= m <= !u };
+        invariant { 0 <= to_int !l /\ to_int !u < to_int a.length }
+        invariant { forall i : int. 0 <= i < to_int a.length ->
+                    a[i] = v -> to_int !l <= i <= to_int !u }
+        variant   { to_int !u - to_int !l }
+        let m = !l + (!u - !l) / of_int 2 in
+        assert { to_int !l <= to_int m <= to_int !u };
         if a[m] < v then
-          l := m + 1
+          l := m + of_int 1
         else if a[m] > v then
-          u := m - 1
-        else
-          raise (Break m)
-      done;
-      raise Not_found
-    with Break i ->
-      i
-    end
-
-end
-
-
-
-(* another binary search using machine integers:
-   32-bit integers for indexes and
-   64-bit integers for values *)
-
-module BinarySearchMachineInts
-
-  use import int.Int
-  use mach_int.Int32
-  use mach_int.Int64
-  use import ref.Ref
-  use import array.Array
-
-  (* the code and its specification *)
-
-  exception Break Int32.int32 (* raised to exit the loop *)
-  exception Not_found (* raised to signal a search failure *)
-
-  let binary_search (a : array Int64.int64) (v : Int64.int64) : Int32.int32
-    requires { length a <= Int32.max_int32 }
-    requires { forall i1 i2 : int. 
-      0 <= i1 <= i2 < length a -> Int64.to_int a[i1] <= Int64.to_int a[i2] }
-    ensures  { 0 <= Int32.to_int result < length a /\ 
-               Int64.to_int a[Int32.to_int result] = Int64.to_int v }
-    raises   { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
-  = try
-      let l = ref (Int32.of_int 0) in
-      let u = ref (Int32.sub (Int32.of_int (length a)) (Int32.of_int 1)) in
-      while Int32.le !l !u do
-        invariant { 0 <= Int32.to_int !l /\ Int32.to_int !u < length a }
-        invariant {
-          forall i : int. 0 <= i < length a -> a[i] = v -> 
-            Int32.to_int !l <= i <= Int32.to_int !u }
-        variant { Int32.to_int !u - Int32.to_int !l }
-        let m = 
-          Int32.add !l (Int32.div (Int32.sub !u !l) (Int32.of_int 2)) 
-        in
-        assert { Int32.to_int !l <= Int32.to_int m <= Int32.to_int !u };
-        if Int64.lt a[Int32.to_int m] v then
-          l := Int32.add m (Int32.of_int 1)
-        else if Int64.gt a[Int32.to_int m] v then
-          u := Int32.sub m (Int32.of_int 1)
+          u := m - of_int 1
         else
           raise (Break m)
       done;

examples/queens.mlw

@@ -229,7 +229,7 @@ end
 module NQueensBits
 
   use import Bits
-  use import arith.Int
+  use import mach.int.Int
   use import ref.Refint
   use import Solution
 

modules/arith.mlw

-
-(** {1 Arithmetic for programs} *)
-
-(** {2 Integer Division}
-
-It is checked that divisor is not null.
-
-*)
-
-module Int
-
-  use export int.Int
-  use export int.ComputerDivision
-
-  let (/) (x: int) (y:int)
-    requires { y <> 0 } ensures { result = div x y }
-  = div x y
-
-end
-
-(** {2 Machine integers}
-
-32-bit integers and such go here.
-
-*)
-
-module Int32
-
-  use export int.Int
-
-  function min_int : int = -2147483648
-  function max_int : int =  2147483647
-
-  let (+) (x: int) (y:int)
-    requires { min_int <= x + y <= max_int } ensures { result = x + y }
-  = x + y
-
-  let (-) (x: int) (y:int)
-    requires { min_int <= x - y <= max_int } ensures { result = x - y }
-  = x - y
-
-  let (-_) (x: int)
-    requires { min_int <= -x <= max_int } ensures { result = -x }
-  = -x
-
-  let (*) (x: int) (y:int)
-    requires { min_int <= x * y <= max_int } ensures { result = x * y }
-  = x * y
-
-  use export int.ComputerDivision
-
-  let (/) (x: int) (y:int)
-    requires { y <> 0 && min_int <= div x y <= max_int }
-    ensures { result = div x y }
-  = div x y
-
-end
-
-(** {2 Division on real numbers}
-
-See also {h <a href="floating_point.why.html">Floating-Point theories</a>.}
-
-*)
-
-module Real
-
-  use import real.Real
-  use export real.RealInfix
-  use export real.FromInt
-
-  let (/.) (x: real) (y: real)
-    requires { y <> 0. } ensures { result = x / y }
-  = x / y
-
-end

modules/mach/array.mlw

+(** {1 Arrays} *)
+
+(** {2 Arrays with 32-bit indices} *)
+
+module Array32
+
+  use import mach.int.Int32
+  use import map.Map as M
+
+  type array 'a model { length: int32; mutable elts: map int 'a }
+    invariant { 0 <= to_int self.length }
+
+  function get (a: array ~'a) (i: int) : 'a = M.get a.elts i
+
+  function set (a: array ~'a) (i: int) (v: 'a) : array 'a =
+    { a with elts = M.set a.elts i v }
+
+  (** syntactic sugar *)
+  function ([]) (a: array 'a) (i: int) : 'a = get a i
+  function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
+
+  val ([]) (a: array ~'a) (i: int32) : 'a
+    requires { 0 <= to_int i < to_int a.length }
+    ensures  { result = a[to_int i] }
+
+  val ([]<-) (a: array ~'a) (i: int32) (v: 'a) : unit writes {a}
+    requires { 0 <= to_int i < to_int a.length }
+    ensures  { a.elts = M.set (old a.elts) (to_int i) v }
+
+  val length (a: array ~'a) : int32 ensures { result = a.length }
+
+  (** unsafe get/set operations with no precondition *)
+  exception OutOfBounds
+
+  let defensive_get (a: array 'a) (i: int32)
+    ensures { 0 <= to_int i < to_int a.length }
+    ensures { result = a[to_int i] }
+    raises  { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
+  = if i < of_int 0 || i >= length a then raise OutOfBounds;
+    a[i]
+
+  let defensive_set (a: array 'a) (i: int32) (v: 'a)
+    ensures { 0 <= to_int i < to_int a.length }
+    ensures { a = (old a)[to_int i <- v] }
+    raises  { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
+  = if i < of_int 0 || i >= length a then raise OutOfBounds;
+    a[i] <- v
+
+  function make (n: int32) (v: ~'a) : array 'a =
+    { length = n; elts = M.const v }
+
+  val make (n: int32) (v: ~'a) : array 'a
+    requires { to_int n >= 0 }
+    ensures  { result = make n v }
+
+  val append (a1: array ~'a) (a2: array 'a) : array 'a
+    ensures { to_int result.length = to_int a1.length + to_int a2.length }
+    ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] }
+    ensures { forall i:int. 0 <= i < to_int a2.length ->
+              result[to_int a1.length + i] = a2[i] }
+
+  val sub (a: array ~'a) (ofs: int32) (len: int32) : array 'a
+    requires { 0 <= to_int ofs /\ 0 <= to_int len }
+    requires { to_int ofs + to_int len <= to_int a.length }
+    ensures  { result.length = len }
+    ensures  { forall i:int. 0 <= i < to_int len ->
+               result[i] = a[to_int ofs + i] }
+
+  val copy (a: array ~'a) : array 'a
+    ensures  { result.length = a.length }
+    ensures  { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }
+
+  let fill (a: array ~'a) (ofs: int32) (len: int32) (v: 'a)
+    requires { 0 <= to_int ofs /\ 0 <= to_int len }
+    requires { to_int ofs + to_int len <= to_int a.length }
+    ensures  { forall i:int.
+      (0 <= i < to_int ofs \/
+        to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
+    ensures  { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
+               a[i] = v }
+  = 'Init:
+    for k = 0 to Int.(-) (to_int len) 1 do (* FIXME: for loop on int32 *)
+      invariant { forall i:int.
+        (0 <= i < to_int ofs \/
+          to_int ofs + to_int len <= i < to_int a.length) ->
+        a[i] = (at a 'Init)[i] }
+      invariant { forall i:int. to_int ofs <= i < to_int ofs + k -> a[i] = v }
+      let k = of_int k in
+      a[ofs + k] <- v
+    done
+
+  val blit (a1: array ~'a) (ofs1: int32)
+                 (a2: array 'a) (ofs2: int32) (len: int32) : unit writes {a2}
+    requires { 0 <= to_int ofs1 /\ 0 <= to_int len }
+    requires { to_int ofs1 + to_int len <= to_int a1.length }
+    requires { 0 <= to_int ofs2 /\
+               to_int ofs2 + to_int len <= to_int a2.length }
+    ensures  { forall i:int.
+      (0 <= i < to_int ofs2 \/
+       to_int ofs2 + to_int len <= i < to_int a2.length) ->
+       a2[i] = (old a2)[i] }
+    ensures  { forall i:int.
+      to_int ofs2 <= i < to_int ofs2 + to_int len ->
+      a2[i] = a1[to_int ofs1 + i - to_int ofs2] }
+
+  val self_blit (a: array ~'a) (ofs1: int32) (ofs2: int32) (len: int32) : unit
+    writes {a}
+    requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
+               to_int ofs1 + to_int len <= to_int a.length }
+    requires { 0 <= to_int ofs2 /\ to_int ofs2 + to_int len <= to_int a.length }
+    ensures  { forall i:int.
+      (0 <= i < to_int ofs2 \/
+       to_int ofs2 + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
+    ensures  { forall i:int.
+      to_int ofs2 <= i < to_int ofs2 + to_int len ->
+      a[i] = (old a)[to_int ofs1 + i - to_int ofs2] }
+
+end

modules/mach/int.mlw

+
+(** {1 Arithmetic for programs} *)
+
+(** {2 Integer Division}
+
+It is checked that divisor is not null.
+
+*)
+
+module Int
+
+  use export int.Int
+  use export int.ComputerDivision
+
+  let (/) (x: int) (y:int)
+    requires { y <> 0 } ensures { result = div x y }
+  = div x y
+
+end
+
+(** {2 Division on real numbers}
+
+See also {h <a href="floating_point.why.html">Floating-Point theories</a>.}
+
+*)
+
+module Real
+
+  use import real.Real
+  use export real.RealInfix
+  use export real.FromInt
+
+  let (/.) (x: real) (y: real)
+    requires { y <> 0. } ensures { result = x / y }
+  = x / y
+
+end
+
+
+(** {2 Machine integers}
+
+32-bit integers and such go here.
+
+*)
+
+module Bounded_int
+
+  use export int.Int
+
+  type t
+
+  constant min : int
+  constant max : int
+
+  function to_int (n:t) : int
+
+  predicate in_bounds (n:int) = min <= n <= max
+
+  axiom to_int_in_bounds: forall n:t. in_bounds (to_int n)
+
+  val of_int (n:int) : t
+    requires { "expl:integer overflow" in_bounds n }
+    ensures  { to_int result = n }
+
+  val (+) (a:t) (b:t) : t
+    requires { "expl:integer overflow" in_bounds (to_int a + to_int b) }
+    ensures   { to_int result = to_int a + to_int b }
+
+  val (-) (a:t) (b:t) : t
+    requires { "expl:integer overflow" in_bounds (to_int a - to_int b) }
+    ensures  { to_int result = to_int a - to_int b }
+
+  val (*) (a:t) (b:t) : t
+    requires { "expl:integer overflow" in_bounds (to_int a * to_int b) }
+    ensures  { to_int result = to_int a * to_int b }
+
+  val (-_) (a:t) : t
+    requires { "expl:integer overflow" in_bounds (- (to_int a)) }
+    ensures  { to_int result = - (to_int a) }
+
+  axiom extensionality: forall x y: t. to_int x = to_int y -> x = y
+
+  val (<=) (a:t) (b:t) : bool
+    ensures  { result = True <-> to_int a <= to_int b }
+
+  val (<) (a:t) (b:t) : bool
+    ensures  { result = True <-> to_int a < to_int b }
+
+  val (>=) (a:t) (b:t) : bool
+    ensures  { result = True <-> to_int a >= to_int b }
+
+  val (>) (a:t) (b:t) : bool
+    ensures  { result = True <-> to_int a > to_int b }
+
+  use import int.ComputerDivision
+
+  val (/) (a:t) (b:t) : t
+    requires { "expl:division by zero" to_int b <> 0 }
+    requires { "expl:integer overflow" in_bounds (div (to_int a) (to_int b)) }
+    ensures  { to_int result = div (to_int a) (to_int b) }
+
+end
+
+module Int32
+
+  use import int.Int
+
+  type int32
+
+  constant min_int32 : int = - 0x80000000
+  constant max_int32 : int =   0x7fffffff
+
+  clone export Bounded_int with
+    type t = int32,
+    constant min = min_int32,
+    constant max = max_int32
+
+end
+
+module UInt32
+
+  type uint32
+
+  constant min_uint32 : int = 0x00000000
+  constant max_uint32 : int = 0xffffffff
+
+  clone export Bounded_int with
+    type t = uint32,
+    constant min = min_uint32,
+    constant max = max_uint32
+
+end
+
+module Int64
+
+  use import int.Int
+
+  type int64
+
+  constant min_int64 : int = - 0x8000000000000000
+  constant max_int64 : int =   0x7fffffffffffffff
+
+  clone export Bounded_int with
+    type t = int64,
+    constant min = min_int64,
+    constant max = max_int64
+
+end
+
+module UInt64
+
+  use import int.Int
+
+  type uint64
+
+  constant min_uint64 : int =  0x0000000000000000
+  constant max_uint64 : int =  0xffffffffffffffff
+
+  clone export Bounded_int with
+    type t = uint64,
+    constant min = min_uint64,
+    constant max = max_uint64
+
+end

modules/mach_int.mlw

-
-
-module Bounded_int
-
-use export int.Int
-
-type t
-
-constant min : int
-
-constant max : int
-
-function to_int (n:t) : int
-
-predicate in_bounds (n:int) = min <= n <= max
-
-axiom to_int_in_bounds: forall n:t. in_bounds (to_int n)
-
-val of_int (n:int) : t
-  requires { "expl:integer overflow" in_bounds n }
-  ensures { to_int result = n }
-
-val add (a:t) (b:t) : t
-  requires { "expl:integer overflow" in_bounds (to_int a + to_int b) }
-  ensures { to_int result = to_int a + to_int b }
-
-val sub (a:t) (b:t) : t
-  requires { "expl:integer overflow" in_bounds (to_int a - to_int b) }
-  ensures { to_int result = to_int a - to_int b }
-
-val mul (a:t) (b:t) : t
-  requires { "expl:integer overflow" in_bounds (to_int a * to_int b) }
-  ensures { to_int result = to_int a * to_int b }
-
-val neg (a:t) : t
-  requires { "expl:integer overflow" in_bounds (- (to_int a)) }
-  ensures { to_int result = - (to_int a) }
-
-val eq (a:t) (b:t) : bool
-  requires { true }
-  ensures  { if result = True then to_int a = to_int b else to_int a <> to_int b }
-
-val ne (a:t) (b:t) : bool
-  requires { true }
-  ensures  { if result = True then to_int a <> to_int b else to_int a = to_int b }
-
-val le (a:t) (b:t) : bool
-  requires { true }
-  ensures  { if result = True then to_int a <= to_int b else to_int a > to_int b }
-
-val lt (a:t) (b:t) : bool
-  requires { true }
-  ensures  { if result = True then to_int a < to_int b else to_int a >= to_int b }
-
-val ge (a:t) (b:t) : bool
-  requires { true }
-  ensures  { if result = True then to_int a >= to_int b else to_int a < to_int b }
-
-val gt (a:t) (b:t) : bool
-  requires { true }
-  ensures  { if result = True then to_int a > to_int b else to_int a <= to_int b }
-
-use import int.ComputerDivision
-
-val div (a:t) (b:t) : t
-  requires { "expl:division by zero" to_int b <> 0 }
-  requires { "expl:integer overflow"
-    in_bounds (ComputerDivision.div (to_int a) (to_int b)) }
-  ensures {
-    to_int result = ComputerDivision.div (to_int a) (to_int b) }
-
-end
-
-
-module Int32
-
-use import int.Int
-
-type int32
-
-constant min_int32 : int = - 0x80000000
-
-constant max_int32 : int =   0x7fffffff
-
-clone export Bounded_int with
-  type t = int32,
-  constant min = min_int32,
-  constant max = max_int32
-
-end
-
-module UInt32
-
-type uint32
-
-constant min_uint32 : int = 0x00000000
-
-constant max_uint32 : int = 0xffffffff
-
-clone export Bounded_int with
-  type t = uint32,
-  constant min = min_uint32,
-  constant max = max_uint32
-
-end
-
-
-
-
-module Int64
-
-use import int.Int
-
-type int64
-
-constant min_int64 : int = - 0x8000000000000000
-
-constant max_int64 : int =   0x7fffffffffffffff
-
-clone export Bounded_int with
-  type t = int64,
-  constant min = min_int64,
-  constant max = max_int64
-
-end
-