Commit 1aa814f0 authored by MARCHE Claude's avatar MARCHE Claude

bigInt: Z.add proved

parent a6917e6b
......@@ -161,3 +161,173 @@ end
module Z
use import map.Map
use import mach.int.Int31
use import mach.array.Array31
use import ref.Ref
use import int.Int
use import int.Power
constant base : int = 32768
constant max_digit : int = 16384
constant min_digit : int = -16384
type t = { mutable digits: array int31 }
predicate ok_array (a:array int31) =
forall i:int. 0 <= i < to_int a.length ->
min_digit <= to_int a[i] < max_digit
predicate ok (x:t) = ok_array x.digits
(* [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
(* =
if 0 <= n < l /\ n < m then
x.[n] + base * value_sub x (n+1) m l
else 0
*)
axiom value_sub_next:
forall x,n,m,l.
value_sub x n m l =
if 0 <= n < l /\ n < m then
to_int (Map.get x n) + base * value_sub x (n+1) m l
else 0
use map.MapEq
let rec lemma value_sub_frame (x y:map int int31) (n m l:int)
requires { MapEq.map_eq_sub x y n m }
variant { m - n }
ensures { value_sub x n m l = value_sub y n m l }
=
if n < m then value_sub_frame x y (n+1) m l else ()
let rec lemma value_sub_tail (x:map int int31) (n m l :int)
requires { 0 <= n <= m < l }
variant { m - n }
ensures {
value_sub x n (m+1) l =
value_sub x n m l + to_int (Map.get x m) * power base (m-n) }
= if n < m then value_sub_tail x (n+1) m l else ()
let rec lemma value_sub_tail_end (x:map int int31) (n m l :int)
requires { 0 <= n <= m /\ m >= l }
variant { m - n }
ensures { value_sub x n (m+1) l = value_sub x n m l }
= if n < m then value_sub_tail_end x (n+1) m l else ()
function value_array (x:array int31) : int =
value_sub x.elts 0 (to_int x.length) (to_int x.length)
function value (x:t) : int = value_array x.digits
let from_small_int (n:int31) : t
requires { min_digit <= to_int n < max_digit }
ensures { ok result }
ensures { value result = to_int n }
=
let a = Array31.make (of_int 1) n in
{ digits = a }
exception TooManyDigits
let add_array (x y:array int31) : array int31
requires { ok_array x /\ ok_array y }
requires { to_int x.length <= to_int y.length }
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 minusone = of_int (-1) in
let base31 = of_int base in
let min_digit31 = of_int min_digit in
let max_digit31 = of_int max_digit in
let l = x.length in
let h = y.length in
if Int31.(>=) h (of_int Int31.max_int31) then raise TooManyDigits;
let arr = Array31.make (Int31.(+) h one) zero in
let carry = ref zero in
let i = ref zero in
while Int31.(<) !i l do
invariant { 0 <= to_int !i <= to_int l }
invariant { -1 <= to_int !carry <= 1 }
invariant {
forall j. 0 <= j < to_int !i -> min_digit <= to_int arr[j] < max_digit }
invariant {
value_sub arr.elts 0 (to_int !i) (to_int h + 1)
+ (to_int !carry) * power base (to_int !i) =
value_sub x.elts 0 (to_int !i) (to_int l)
+ value_sub y.elts 0 (to_int !i) (to_int h) }
variant { to_int l - to_int !i }
'L:
let sum = Int31.(+) (Int31.(+) x[!i] y[!i]) !carry in
if Int31.(>=) sum max_digit31
then begin arr[!i] <- Int31.(-) sum base31; carry := one end
else
if Int31.(<) sum min_digit31
then begin arr[!i] <- Int31.(+) sum base31; carry := minusone end
else begin arr[!i] <- sum; carry := zero end;
assert {
MapEq.map_eq_sub arr.elts (at arr 'L).elts 0 (to_int !i) };
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) };
i := Int31.(+) !i one;
done;
while Int31.(<) !i h do
invariant { to_int l <= to_int !i <= to_int h }
invariant { -1 <= to_int !carry <= 1 }
invariant { forall j. 0 <= j < to_int !i ->
min_digit <= to_int arr[j] < max_digit }
invariant {
value_sub arr.elts 0 (to_int !i) (to_int h + 1)
+ (to_int !carry) * power base (to_int !i) =
value_sub x.elts 0 (to_int l) (to_int l)
+ value_sub y.elts 0 (to_int !i) (to_int h) }
variant { to_int h - to_int !i }
'L:
let sum = Int31.(+) y[!i] !carry in
if Int31.(>=) sum max_digit31
then begin arr[!i] <- Int31.(-) sum base31; carry := one end
else
if Int31.(<) sum min_digit31
then begin arr[!i] <- Int31.(+) sum base31; carry := minusone end
else begin arr[!i] <- sum; carry := zero end;
assert {
MapEq.map_eq_sub arr.elts (at arr 'L).elts 0 (to_int !i) };
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) };
i := Int31.(+) !i one;
done;
'L:
arr[!i] <- !carry;
assert {
MapEq.map_eq_sub arr.elts (at arr 'L).elts 0 (to_int !i) };
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) };
arr
let add (x y:t) : t
requires { ok x /\ ok y }
ensures { ok result }
ensures { value result = value x + value y }
raises { TooManyDigits -> true }
= let l1 = x.digits.length in
let l2 = y.digits.length in
let res =
if Int31.(<=) l1 l2 then
add_array x.digits y.digits
else add_array y.digits x.digits
in
{ digits = res }
end
This source diff could not be displayed because it is too large. You can view the blob instead.
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