Commit 8ab8d007 authored by MARCHE Claude's avatar MARCHE Claude

new version of multiprecision arithmetic

parent 1e1c2f0c
module N
use import map.Map
use import mach.array.Array31
use import mach.int.Int31
use import ref.Ref
use import int.Int
use import int.Power
lemma power_non_neg:
forall x y. x >= 0 /\ y >= 0 -> power x y >= 0
(** limb can be any unsigned integer type *)
type limb
clone mach.int.Bounded_int as Limb
with type t = limb, constant min = zero (* from int.Int *)
axiom limb_max_bound: 1 <= Limb.max
constant radix : int = Limb.max + 1
function l2i (x:limb) : int = Limb.to_int x
function p2i (i:int31) : int = Int31.to_int i
type t = { mutable digits: array limb }
(** [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 limb) (n:int) (m:int) : int
(* =
if n < m then
x.[n] + radix * value_sub x (n+1) m
else 0
*)
axiom value_sub_next:
forall x,n,m.
value_sub x n m =
if n < m then
l2i (Map.get x n) + radix * value_sub x (n+1) m
else 0
use map.MapEq
let rec lemma value_sub_frame (x y:map int limb) (n m:int)
requires { MapEq.map_eq_sub x y n m }
variant { m - n }
ensures { value_sub x n m = value_sub y n m }
=
if n < m then value_sub_frame x y (n+1) m else ()
let rec lemma value_sub_tail (x:map int limb) (n m:int)
requires { n <= m }
variant { m - n }
ensures {
value_sub x n (m+1) =
value_sub x n m + l2i (Map.get x m) * power radix (m-n) }
= if n < m then value_sub_tail x (n+1) m else ()
let rec lemma value_sub_concat (x:map int limb) (n m l:int)
requires { n <= m <= l}
variant { m - n }
ensures {
value_sub x n l =
value_sub x n m + value_sub x m l * power radix (m-n) }
= if n < m then value_sub_concat x (n+1) m l else ()
function value_array (x:array limb) : int =
value_sub x.elts 0 (p2i x.length)
function value (x:t) : int = value_array x.digits
(** {2 conversion from a small integer} *)
let zero () =
{ digits = Array31.make (Int31.of_int 0) (Limb.of_int 0) }
let from_limb (n:limb) : t
ensures { value result = l2i n }
= { digits = Array31.make (Int31.of_int 1) n }
(** {2 Comparisons} *)
lemma value_sub_upper_bound:
forall x:map int limb, x1 x2:int. x1 <= x2 ->
value_sub x x1 x2 < power radix (x2 - x1)
lemma value_sub_lower_bound:
forall x:map int limb, x1 x2:int. x1 <= x2 ->
0 <= value_sub x x1 x2
lemma value_sub_lower_bound_tight:
forall x:map int limb, x1 x2:int. x1 < x2 ->
power radix (x2-x1-1) * l2i (Map.get x (x2-1)) <= value_sub x x1 x2
lemma value_sub_upper_bound_tight:
forall x:map int limb, x1 x2:int. x1 < x2 ->
value_sub x x1 x2 < power radix (x2-x1-1) * (l2i (Map.get x (x2-1)) + 1)
exception Break int31
function compare_int (x y:int) : int =
if x < y then -1 else if x=y then 0 else 1
let compare_limbs (x y:array limb) (x1 x2 y1 y2:int31) : int31
requires { 0 <= p2i x1 <= p2i x2 <= p2i x.length }
requires { 0 <= p2i y1 <= p2i y2 <= p2i y.length }
requires { p2i x2 - p2i x1 >= p2i y2 - p2i y1 }
ensures { p2i result = compare_int
(value_sub x.elts (p2i x1) (p2i x2))
(value_sub y.elts (p2i y1) (p2i y2)) }
= let limb_zero = Limb.of_int 0 in
let zero = Int31.of_int 0 in
let one = Int31.of_int 1 in
let minus_one = Int31.of_int (-1) in
let i = ref x2 in
let x3 = Int31.(+) x1 (Int31.(-) y2 y1) in
try
while Int31.(>) !i x3 do
invariant { p2i x3 <= p2i !i <= p2i x2 }
invariant { value_sub x.elts (p2i !i) (p2i x2) = 0 }
variant { p2i !i }
i := Int31.(-) !i one;
if Limb.ne x[!i] limb_zero then
begin
assert { value_sub x.elts (p2i x1) (p2i !i + 1) >= power radix (p2i !i - p2i x1) };
assert { value_sub x.elts (p2i x1) (p2i x2) = value_sub x.elts (p2i x1) (p2i !i + 1)
+ power radix (p2i !i + 1 - p2i x1) * value_sub x.elts (p2i !i + 1) (p2i x2)};
assert { value_sub x.elts (p2i x1) (p2i x2) >= power radix (p2i !i - p2i x1) };
assert { value_sub y.elts (p2i y1) (p2i y2) < power radix (p2i y2 - p2i y1) };
assert { power radix (p2i y2 - p2i y1) <= power radix (p2i !i - p2i x1) };
raise (Break one);
end
done;
while Int31.(>) !i x1 do
invariant { p2i x1 <= p2i !i <= p2i x3 }
invariant {
value_sub x.elts (p2i !i) (p2i x2) =
value_sub y.elts (p2i y1 + (p2i !i - p2i x1)) (p2i y2) }
variant { p2i !i }
i := Int31.(-) !i one;
let j = Int31.(+) y1 (Int31.(-) !i x1) in
assert { value_sub x.elts (p2i x1) (p2i x2) = value_sub x.elts (p2i x1) (p2i !i + 1)
+ power radix (p2i !i + 1 - p2i x1) * value_sub x.elts (p2i !i + 1) (p2i x2)};
assert { value_sub y.elts (p2i y1) (p2i y2) = value_sub y.elts (p2i y1) (p2i j + 1)
+ power radix (p2i j + 1 - p2i y1) * value_sub y.elts (p2i j + 1) (p2i y2)};
if Limb.(<) x[!i] y[j] then
begin
assert { value_sub x.elts (p2i x1) (p2i !i + 1) < power radix (p2i !i - p2i x1) * (l2i x[p2i !i] + 1) };
assert { power radix (p2i !i - p2i x1) * (l2i x[p2i !i] + 1) <= power radix (p2i j - p2i y1) * l2i y[p2i j] };
assert { power radix (p2i j - p2i y1) * l2i y[p2i j] <= value_sub y.elts (p2i y1) (p2i j + 1) };
raise (Break minus_one);
end;
if Limb.(>) x[!i] y[j] then
begin
assert { value_sub y.elts (p2i y1) (p2i j + 1) < power radix (p2i j - p2i y1) * (l2i y[p2i j] + 1) };
assert { power radix (p2i j - p2i y1) * (l2i y[p2i j] + 1) <= power radix (p2i !i - p2i x1) * l2i x[p2i !i] };
assert { power radix (p2i !i - p2i x1) * l2i x[p2i !i] <= value_sub x.elts (p2i x1) (p2i !i + 1) };
raise (Break one);
end
done;
zero
with Break x -> x
end
let compare (x y:t) : int31
ensures { p2i result = compare_int (value x) (value y) }
= let zero = Int31.of_int 0 in
let lx = x.digits.length in
let ly = y.digits.length in
if Int31.(>=) lx ly then compare_limbs x.digits y.digits zero lx zero ly
else Int31.(-_) (compare_limbs y.digits x.digits zero ly zero lx)
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