Commit a733bce4 authored by MARCHE Claude's avatar MARCHE Claude

bigInt: proof of compare in progress

parent b475210f
(** A library for arbitrary-precision integer arithmetic *)
(** {1 A library for arbitrary-precision integer arithmetic} *)
module N
......@@ -11,10 +11,18 @@ module N
use import int.Int
use import int.Power
(** {2 data type for unbound integers and invariants} *)
constant base : int = 10000
(** a power of ten whose square fits on 31 bits *)
type t = { mutable digits: array int31 }
(** an unbounded integer is stored in an array of 31 bits integers,
with all values between 0 included and [base] excluded
index 0 is the lsb. the msb is never 0.
*)
predicate ok_array (a:array int31) =
(to_int a.length >= 1 -> to_int a[to_int a.length - 1] <> 0) /\
forall i:int. 0 <= i < to_int a.length ->
......@@ -22,6 +30,9 @@ module N
predicate ok (x:t) = ok_array x.digits
(** {2 value stored in an array} *)
(* [value_sub x n m] denotes the integer represented by
the digits x[n..m-1] with lsb at index n *)
function value_sub (x:map int int31) (n:int) (m:int) (l:int): int
......@@ -79,6 +90,33 @@ module N
function value (x:t) : int = value_array x.digits
(** {2 general lemmas} *)
(* moved to stdlib
lemma power_monotonic:
forall x y z. 0 <= x <= y -> power z x <= power z y
*)
lemma value_zero:
forall x:array int31.
let l = to_int x.length in
l = 0 -> value_array x = 0
lemma value_bounds_sub:
forall x:map int int31, n l:int. 0 < n <= l ->
(forall i:int. 0 <= i < n-1 -> 0 <= to_int (Map.get x i) < base) ->
0 < to_int (Map.get x (n-1)) < base ->
power base (n-1) <= value_sub x 0 n l < power base n
lemma value_bounds_array:
forall x:array int31. ok_array x ->
let l = to_int x.length in
l > 0 -> power base (l-1) <= value_array x < power base l
(** {2 conversion from a small integer} *)
let from_small_int (n:int31) : t
requires { 0 <= to_int n < base }
ensures { ok result }
......@@ -92,6 +130,56 @@ module N
in
{ digits = a }
(** {2 Comparisons} *)
exception Break
(* Comparisons *)
let compare_array (x y:array int31) : int31
requires { ok_array x /\ ok_array y }
ensures { -1 <= to_int result <= 1 }
ensures { to_int result = -1 -> value_array x < value_array y }
ensures { to_int result = 0 -> value_array x = value_array y }
ensures { to_int result = 1 -> value_array x > value_array y }
= let zero = of_int 0 in
let one = of_int 1 in
let minus_one = of_int (-1) in
let l1 = x.length in
let l2 = y.length in
if Int31.(<) l1 l2 then minus_one else
if Int31.(>) l1 l2 then one else
let i = ref l1 in
let res = ref zero in
let ghost acc = ref 0 in
try
while Int31.(>) !i zero do
invariant { to_int !res = 0 }
(* needed to be sure it is zero at normal exit ! *)
invariant { 0 <= to_int !i <= to_int l1 }
invariant {
value_array x = value_sub x.elts 0 (to_int !i) (to_int l1) + !acc
}
invariant {
value_array y = value_sub y.elts 0 (to_int !i) (to_int l1) + !acc
}
variant { to_int !i }
i := Int31.(-) !i one;
if Int31.(<) x[!i] y[!i] then (res := minus_one; raise Break);
if Int31.(>) x[!i] y[!i] then (res := one; raise Break);
acc := !acc + power base (to_int !i) * to_int x[!i];
done;
raise Break
with Break -> !res
end
let eq (x y:t) : bool
requires { ok x /\ ok y }
ensures { if result then value x = value y else value x <> value y }
= Int31.eq (compare_array x.digits y.digits) (of_int 0)
(** {2 arithmetic operations} *)
exception TooManyDigits
let add_array (x y:array int31) : array int31
......@@ -176,7 +264,7 @@ module N
assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
value_sub (at arr 'L).elts 0 (to_int !i) (to_int h + 1) };
assert { value_array arr = value_array x + value_array y };
abstract
abstract
ensures { -1 <= to_int !non_null_idx <= to_int !i }
ensures { to_int !non_null_idx >= 0 -> to_int arr[to_int !non_null_idx] <> 0 }
ensures {
......@@ -194,9 +282,9 @@ module N
MapEq.map_eq_sub arr.elts arr'.elts 0 (to_int len) };
assert { value_sub arr.elts 0 (to_int len) (to_int len) =
value_sub arr'.elts 0 (to_int len) (to_int len) } ;
assert { to_int arr'.length >= 1 ->
assert { to_int arr'.length >= 1 ->
to_int arr'[to_int arr'.length - 1] <> 0 };
assert { forall j. 0 <= j < to_int arr'.length ->
assert { forall j. 0 <= j < to_int arr'.length ->
0 <= to_int arr'[j] < base };
arr'
......@@ -214,7 +302,26 @@ module N
in
{ digits = res }
(* Multiplication: school book algorithm *)
(*
let rec mul_array (x y:array int31) : array int31
requires { ok_array x /\ ok_array y }
ensures { ok_array result }
ensures { value_array result = value_array x * value_array y }
raises { TooManyDigits -> true }
= let zero = of_int 0 in
let one = of_int 1 in
let two = of_int 2 in
let base31 = of_int 10000 in
assert { to_int base31 = base };
let l1 = x.digits.length in
let l2 = y.digits.length in
TODO
*)
(* Multiplication: Karatsuba algorithm
let rec mul_array (x y:array int31) : array int31
requires { ok_array x /\ ok_array y }
ensures { ok_array result }
......@@ -233,8 +340,12 @@ module N
let h = Int31.(/) n base31 in
let l = Int31.(-) n (Int31.(*) h base31) in
if Int31.eq h zero then
let arr = Array31.make one l in
{ digits = arr }
if Int31.eq l zero then
let arr = Array31.make zero zero in
{ digits = arr }
else
let arr = Array31.make one l in
{ digits = arr }
else
let arr = Array31.make two l in
arr.(1) <- h;
......@@ -260,6 +371,8 @@ module N
let z2 = mul_array high1 high2 in
(*
return (z2*10^(2*m2))+((z1-z2-z0)*10^(m2))+(z0)
-> we need subtraction !
*)
let mul (x y:t) : t
......
This diff is collapsed.
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