63-bit integers

new module mach.int.Refint63
new module mach.int.MinMax63
new module mach.matrix.Matrix63
mach.array.Array63: type array renamed into array63
parent e4b9cb9c
......@@ -186,7 +186,7 @@ module mach.array.Array32
end
module mach.array.Array63
syntax type array "(%1 array)"
syntax type array63 "(%1 array)"
syntax val make "Array.make"
syntax val ([]) "Array.get"
......
......@@ -154,13 +154,13 @@ module MachineArithmetic
use import mach.array.Array63
use import mach.int.Int63
predicate is_board (board: array int63) (pos: int) =
predicate is_board (board: array63 int63) (pos: int) =
forall q: int. 0 <= q < pos ->
0 <= to_int board[q] < to_int (length board)
exception MInconsistent
let mcheck_is_consistent (board: array int63) (pos: int63)
let mcheck_is_consistent (board: array63 int63) (pos: int63)
requires { 0 <= to_int pos < to_int (length board) }
requires { is_board board (to_int pos + 1) }
= try
......@@ -184,7 +184,7 @@ module MachineArithmetic
use mach.peano.Peano as P
let rec mcount_bt_queens
(solutions: ref P.t) (board: array int63) (n: int63) (pos: int63)
(solutions: ref P.t) (board: array63 int63) (n: int63) (pos: int63)
requires { to_int (length board) = to_int n }
requires { 0 <= to_int pos <= to_int n }
requires { is_board board (to_int pos) }
......@@ -205,7 +205,7 @@ module MachineArithmetic
i := !i + of_int 1
done
let mcount_queens (board: array int63) (n: int63) : P.t
let mcount_queens (board: array63 int63) (n: int63) : P.t
requires { to_int (length board) = to_int n }
ensures { true }
=
......
......@@ -241,68 +241,68 @@ module Array63
use import mach.int.Int63
use import map.Map as M
type array 'a model { length: int63; mutable elts: map int 'a }
type array63 'a model { length: int63; 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 get (a: array63 ~'a) (i: int) : 'a = M.get a.elts i
function set (a: array ~'a) (i: int) (v: 'a) : array 'a =
function set (a: array63 ~'a) (i: int) (v: 'a) : array63 '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
function ([]) (a: array63 'a) (i: int) : 'a = get a i
function ([<-]) (a: array63 'a) (i: int) (v: 'a) : array63 'a = set a i v
val ([]) (a: array ~'a) (i: int63) : 'a
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
val ([]) (a: array63 ~'a) (i: int63) : 'a
requires { "expl:index in array63 bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
val ([]<-) (a: array ~'a) (i: int63) (v: 'a) : unit writes {a}
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
val ([]<-) (a: array63 ~'a) (i: int63) (v: 'a) : unit writes {a}
requires { "expl:index in array63 bounds" 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) : int63 ensures { result = a.length }
val length (a: array63 ~'a) : int63 ensures { result = a.length }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: array 'a) (i: int63)
let defensive_get (a: array63 'a) (i: int63)
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: int63) (v: 'a)
let defensive_set (a: array63 'a) (i: int63) (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
val make (n: int63) (v: ~'a) : array 'a
requires { "expl:array creation size" to_int n >= 0 }
val make (n: int63) (v: ~'a) : array63 'a
requires { "expl:array63 creation size" to_int n >= 0 }
ensures { length result = n }
ensures { forall i:int. 0 <= i < to_int n -> get result i = v }
val append (a1: array ~'a) (a2: array 'a) : array 'a
val append (a1: array63 ~'a) (a2: array63 'a) : array63 '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: int63) (len: int63) : array 'a
val sub (a: array63 ~'a) (ofs: int63) (len: int63) : array63 '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
val copy (a: array63 ~'a) : array63 '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: int63) (len: int63) (v: 'a)
let fill (a: array63 ~'a) (ofs: int63) (len: int63) (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.
......@@ -321,8 +321,8 @@ module Array63
a[ofs + k] <- v
done
val blit (a1: array ~'a) (ofs1: int63)
(a2: array 'a) (ofs2: int63) (len: int63) : unit writes {a2}
val blit (a1: array63 ~'a) (ofs1: int63)
(a2: array63 'a) (ofs2: int63) (len: int63) : 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 /\
......@@ -335,7 +335,7 @@ module Array63
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: int63) (ofs2: int63) (len: int63) : unit
val self_blit (a: array63 ~'a) (ofs1: int63) (ofs2: int63) (len: int63) : unit
writes {a}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
to_int ofs1 + to_int len <= to_int a.length }
......
......@@ -225,6 +225,51 @@ module Int63
*)
end
module Refint63
use import Int63
use export ref.Ref
let incr (r: ref int63) : unit
requires { "expl:integer overflow" to_int !r < max_int63 }
ensures { to_int !r = to_int (old !r) + 1 }
= r := !r + of_int 1
let decr (r: ref int63) : unit
requires { "expl:integer overflow" min_int63 < to_int !r }
ensures { to_int !r = to_int (old !r) - 1 }
= r := !r - of_int 1
let (+=) (r: ref int63) (v: int63) : unit
requires { "expl:integer overflow" in_bounds (to_int !r + to_int v) }
ensures { to_int !r = to_int (old !r) + to_int v }
= r := !r + v
let (-=) (r: ref int63) (v: int63) : unit
requires { "expl:integer overflow" in_bounds (to_int !r - to_int v) }
ensures { to_int !r = to_int (old !r) - to_int v }
= r := !r - v
let ( *= ) (r: ref int63) (v: int63) : unit
requires { "expl:integer overflow" in_bounds (to_int !r * to_int v) }
ensures { to_int !r = to_int (old !r) * to_int v }
= r := !r * v
end
module MinMax63
use import Int63
let min (x y: int63) : int63
ensures { result = if to_int x <= to_int y then x else y }
= if x <= y then x else y
let max (x y: int63) : int63
ensures { result = if to_int x >= to_int y then x else y }
= if x >= y then x else y
end
module Int64
use import int.Int
......
(** {1 Matrices} *)
module Matrix63
use import mach.int.Int63
use import map.Map as M
type matrix 'a
model { rows: int63; columns: int63; mutable elts: map int (map int 'a) }
invariant { 0 <= to_int self.rows /\ 0 <= to_int self.columns }
function get (a: matrix 'a) (r c: int) : 'a =
M.get (M.get a.elts r) c
function set (a: matrix 'a) (r c: int) (v: 'a) : matrix 'a =
{ a with elts = M.set a.elts r (M.set (M.get a.elts r) c v) }
predicate valid_index (a: matrix 'a) (r c: int63) =
0 <= to_int r < to_int a.rows /\ 0 <= to_int c < to_int a.columns
val get (a: matrix 'a) (r c: int63) : 'a
requires { "expl:index in array bounds" valid_index a r c }
ensures { result = get a (to_int r) (to_int c) }
val set (a: matrix 'a) (r c: int63) (v: 'a) : unit
requires { "expl:index in array bounds" valid_index a r c }
writes { a }
ensures { a.elts = M.set (old a.elts) (to_int r)
(M.set (M.get (old a.elts) (to_int r)) (to_int c) v) }
val rows (a: matrix 'a) : int63 ensures { result = a.rows }
val columns (a: matrix 'a) : int63 ensures { result = a.columns }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: matrix 'a) (r c: int63) : 'a
ensures { "expl:index in array bounds" valid_index a r c }
ensures { result = get a (to_int r) (to_int c) }
raises { OutOfBounds -> not (valid_index a r c) }
= if r < of_int 0 || r >= a.rows || c < of_int 0 || c >= a.columns then
raise OutOfBounds;
get a r c
let defensive_set (a: matrix 'a) (r c: int63) (v: 'a) : unit
ensures { "expl:index in array bounds" valid_index a r c }
ensures { a.elts = M.set (old a.elts)
(to_int r) (M.set (M.get (old a.elts) (to_int r)) (to_int c) v) }
raises { OutOfBounds -> not (valid_index a r c) /\ a = old a }
= if r < of_int 0 || r >= a.rows || c < of_int 0 || c >= a.columns then
raise OutOfBounds;
set a r c v
val make (r c: int63) (v: 'a) : matrix 'a
requires { to_int r >= 0 /\ to_int c >= 0 }
ensures { result.rows = r }
ensures { result.columns = c }
ensures { forall i j. 0 <= i < to_int r /\ 0 <= j < to_int c ->
get result i j = v }
val copy (a: matrix 'a) : matrix 'a
ensures { result.rows = a.rows /\ result.columns = a.columns }
ensures { forall r:int. 0 <= r < to_int result.rows ->
forall c:int. 0 <= c < to_int result.columns ->
get result r c = get a r c }
end
......@@ -19,12 +19,12 @@ module Matrix
0 <= r < a.rows /\ 0 <= c < a.columns
val get (a: matrix 'a) (r c: int) : 'a
requires { valid_index a r c }
requires { "expl:index in array bounds" valid_index a r c }
ensures { result = get a r c }
val set (a: matrix 'a) (r c: int) (v: 'a) : unit
requires { valid_index a r c }
writes {a}
requires { "expl:index in array bounds" valid_index a r c }
writes { a }
ensures { a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v)}
val rows (a: matrix 'a) : int ensures { result = a.rows }
......@@ -34,14 +34,14 @@ module Matrix
exception OutOfBounds
let defensive_get (a: matrix 'a) (r c: int) : 'a
ensures { valid_index a r c }
ensures { "expl:index in array bounds" valid_index a r c }
ensures { result = get a r c }
raises { OutOfBounds -> not (valid_index a r c) }
= if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
get a r c
let defensive_set (a: matrix 'a) (r c: int) (v: 'a) : unit
ensures { valid_index a r c }
ensures { "expl:index in array bounds" valid_index a r c }
ensures { a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v)}
raises { OutOfBounds -> not (valid_index a r c) /\ a = old a }
= if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
......@@ -49,9 +49,9 @@ module Matrix
val make (r c: int) (v: 'a) : matrix 'a
requires { r >= 0 /\ c >= 0 }
ensures { result.rows = r }
ensures { result.columns = c }
ensures { forall i j. 0 <= i < r /\ 0 <= j < c -> get result i j = v }
ensures { result.rows = r }
ensures { result.columns = c }
ensures { forall i j. 0 <= i < r /\ 0 <= j < c -> get result i j = v }
val copy (a: matrix 'a) : matrix 'a
ensures { result.rows = a.rows /\ result.columns = a.columns }
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment