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

proof of add in progress

parent 8ab8d007
......@@ -106,7 +106,7 @@ module N
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
exception Break31 int31
function compare_int (x y:int) : int =
if x < y then -1 else if x=y then 0 else 1
......@@ -138,7 +138,7 @@ module N
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);
raise (Break31 one);
end
done;
while Int31.(>) !i x1 do
......@@ -158,18 +158,18 @@ module N
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);
raise (Break31 minus_one);
end;
if Limb.(>) x[!i] y[j] then
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);
raise (Break31 one);
end
done;
zero
with Break x -> x
with Break31 x -> x
end
......@@ -179,9 +179,84 @@ module N
= 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
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)
(** {2 addition} *)
exception Break
val addc (x y:limb) (c:bool) : (limb,bool)
returns { (r,d) ->
l2i r + (if d then radix else 0) =
l2i x + l2i y + (if c then 1 else 0) }
val add_limb (x:array limb) (y:limb) (x1 x2:int31) : limb
requires { 0 <= p2i x1 <= p2i x2 <= p2i x.length }
writes { x }
(*
ensures { MapEq.map_eq_sub (old x) x 0 (p2i x1) }
ensures { MapEq.map_eq_sub (old x) x (p2i x2) (p2i x.length) }
*)
ensures { value_array x + power radix (p2i x2) * l2i result
= value_array (old x) + power radix (p2i x1) * l2i y }
(*
= let limb_zero = Limb.of_int 0 in
let i = ref x1 in
let c = ref y in
while Int31.(<) !i x2 && Limb.ne !c limb_zero do
done;
!c
*)
let add_limbs (x y:array limb) (x1 x2 y1 y2:int31) : limb
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 }
writes { x }
ensures { value_array x + power radix (p2i x2) * l2i result
= value_array (old x) + power radix (p2i x1) * value_sub y.elts (p2i y1) (p2i y2) }
= 'Init:
let one = Int31.of_int 1 in
let i = ref y1 in
let c = ref false in
while Int31.(<) !i y2 do
invariant { p2i y1 <= p2i !i <= p2i y2 }
invariant {
let j = p2i x1 + (p2i !i - p2i y1) in
value_array x + power radix j * (if !c then 1 else 0)
= value_array (at x 'Init) + power radix (p2i x1) * value_sub y.elts (p2i y1) (p2i !i) }
variant { p2i y2 - p2i !i }
let j = Int31.(+) x1 (Int31.(-) !i y1) in
let (r,c') = addc x[j] y[!i] !c in
'L:
x[j] <- r;
assert { value_array x = value_array (at x 'L)
+ power radix (p2i j) * (l2i r - l2i (at x 'L)[p2i j]) };
assert { value_sub y.elts (p2i y1) (p2i !i + 1) =
value_sub y.elts (p2i y1) (p2i !i)
+ power radix (p2i !i - p2i y1) * l2i y[p2i !i] };
assert { power radix (p2i j + 1) = power radix (p2i j) * radix };
c := c';
i := Int31.(+) !i one;
assert { !c = False ->
let j = p2i x1 + (p2i !i - p2i y1) in
value_array x = value_array (at x 'Init) + power radix (p2i x1) * value_sub y.elts (p2i y1) (p2i !i) };
assert { !c = True ->
let j = p2i x1 + (p2i !i - p2i y1) in
value_array x + power radix j
= value_array (at x 'Init) + power radix (p2i x1) * value_sub y.elts (p2i y1) (p2i !i) };
assert { (if True then 1 else 0) = 0+1 };
assert { (if False then 1 else 0) = 0+0 };
assert {
let j = p2i x1 + (p2i !i - p2i y1) in
value_array x + power radix j * (if !c then 1 else 0)
= value_array (at x 'Init) + power radix (p2i x1) * value_sub y.elts (p2i y1) (p2i !i) };
done;
if !c then add_limb x (Limb.of_int 1) (Int31.(+) x1 (Int31.(-) y2 y1)) x2
else Limb.of_int 0
end
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