Commit 25324e99 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Remove some useless casts and qualifiers

parent 06e1fdc8
......@@ -27,15 +27,15 @@ module Add
writes { r.data.elts }
=
let lx = ref (C.get x) in
let res = Limb.add_mod !lx y in
let i = ref (1:int32) in
let c = ref (0:limb) in
let res = add_mod !lx y in
let i = ref 1 in
let c = ref 0 in
C.set r res;
if (Limb.(<) res !lx)
if (res < !lx)
then begin
c := 1;
assert { radix + res = !lx + y };
while (Int32.(<) !i sz) do
while (!i < sz) do
invariant { 1 <= !i <= sz }
invariant { 0 <= !c <= 1 }
invariant { !i = sz \/ !c = 1 }
......@@ -46,13 +46,13 @@ module Add
variant { sz - !i }
assert { !c = 1 };
lx := get_ofs x !i;
let res = Limb.add_mod !lx 1 in
let res = add_mod !lx 1 in
set_ofs r !i res;
assert { value r !i + (power radix !i) * !c = value x !i + y };
value_tail r !i;
value_tail x !i;
i := Int32.(+) !i 1;
if not (Limb.(=) res 0)
i := !i + 1;
if res <> 0
then begin
c := 0;
assert { res = !lx + 1 };
......@@ -65,7 +65,7 @@ module Add
end
done;
end;
while Int32.(<) !i sz do
while !i < sz do
invariant { !i = sz \/ !c = 0 }
invariant { 0 <= !i <= sz }
invariant { value r !i + (power radix !i) * !c =
......@@ -79,7 +79,7 @@ module Add
value x !i + y };
value_tail r !i;
value_tail x !i;
i := Int32.(+) !i (Int32.of_int 1);
i := !i + 1;
done;
!c
......@@ -97,12 +97,11 @@ module Add
-> (pelts r)[j] = old (pelts r)[j] }
writes { r.data.elts }
=
let limb_zero = Limb.of_int 0 in
let lx = ref limb_zero in
let ly = ref limb_zero in
let c = ref limb_zero in
let i = ref (Int32.of_int 0) in
while Int32.(<) !i sz do
let lx = ref 0 in
let ly = ref 0 in
let c = ref 0 in
let i = ref 0 in
while !i < sz do
variant { sz - !i }
invariant { 0 <= !i <= sz }
invariant { value r !i + (power radix !i) * !c =
......@@ -124,7 +123,7 @@ module Add
value_tail y !i;
assert { value r (!i+1) + (power radix (!i+1)) * !c =
value x (!i+1) + value y (!i+1) };
i := Int32.(+) !i (Int32.of_int 1);
i := !i + 1;
done;
!c
......@@ -143,12 +142,11 @@ module Add
ensures { 0 <= result <= 1 }
writes { r.data.elts }
=
let limb_zero = Limb.of_int 0 in
let lx = ref limb_zero in
let ly = ref limb_zero in
let c = ref limb_zero in
let i = ref (Int32.of_int 0) in
while Int32.(<) !i sy do
let lx = ref 0 in
let ly = ref 0 in
let c = ref 0 in
let i = ref 0 in
while !i < sy do
variant { sy - !i }
invariant { 0 <= !i <= sy }
invariant { value r !i + (power radix !i) * !c =
......@@ -169,11 +167,11 @@ module Add
value_tail y !i;
assert { value r (!i+1) + (power radix (!i+1)) * !c =
value x (!i+1) + value y (!i+1) };
i := Int32.(+) !i (Int32.of_int 1);
i := !i + 1;
done;
if (not (Limb.(=) !c 0))
if (!c <> 0)
then begin
while Int32.(<) !i sx do
while !i < sx do
variant { sx - !i }
invariant { sy <= !i <= sx }
invariant { value r !i + (power radix !i) * !c =
......@@ -184,14 +182,14 @@ module Add
-> (pelts r)[j] = old (pelts r)[j] }
assert { !c = 1 };
lx := get_ofs x !i;
let res = Limb.add_mod !lx (1:limb) in
let res = add_mod !lx (1:limb) in
set_ofs r !i res;
assert { value r !i + (power radix !i) =
value x !i + value y sy };
value_tail r !i;
value_tail x !i;
i := Int32.(+) !i 1;
if (not (Limb.(=) res 0))
i := !i + 1;
if res <> 0
then begin
c := 0;
assert { res = !lx + 1 };
......@@ -204,7 +202,7 @@ module Add
end
done
end;
while Int32.(<) !i sx do
while !i < sx do
variant { sx - !i }
invariant { sy <= !i <= sx }
invariant { !i = sx \/ !c = 0 }
......@@ -220,7 +218,7 @@ module Add
assert { value r !i = value x !i + value y sy }; (* true with this, should not be needed *)
assert { value r (!i+1) + power radix (!i+1) * !c
= value x (!i+1) + value y sy };
i := Int32.(+) !i (Int32.of_int 1);
i := !i + 1;
done;
!c
......@@ -236,12 +234,11 @@ module Add
writes { x.data.elts }
=
let ghost ox = { x } in
let limb_zero = Limb.of_int 0 in
let lx = ref limb_zero in
let ly = ref limb_zero in
let c = ref limb_zero in
let i = ref (Int32.of_int 0) in
while Int32.(<) !i sy do
let lx = ref 0 in
let ly = ref 0 in
let c = ref 0 in
let i = ref 0 in
while !i < sy do
variant { sy - !i }
invariant { 0 <= !i <= sy }
invariant { value x !i + (power radix !i) * !c =
......@@ -270,11 +267,11 @@ module Add
value_tail y !i;
assert { value x (!i+1) + (power radix (!i+1)) * !c =
value ox (!i+1) + value y (!i+1) };
i := Int32.(+) !i (Int32.of_int 1);
i := !i + 1;
done;
if (not (Limb.(=) !c 0))
if (!c <> 0)
then begin
while Int32.(<) !i sx do
while !i < sx do
variant { sx - !i }
invariant { sy <= !i <= sx }
invariant { value x !i + (power radix !i) * !c =
......@@ -288,7 +285,7 @@ module Add
assert { !c = 1 };
lx := get_ofs x !i;
assert { !lx = (pelts ox)[ox.offset + !i] };
let res = Limb.add_mod !lx 1 in
let res = add_mod !lx 1 in
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
(x.offset + p2i sx) res;
......@@ -298,8 +295,8 @@ module Add
(pelts x)[x.offset + j] = (pelts ox) [x.offset + j] };
value_tail ox !i;
value_tail x !i;
i := Int32.(+) !i (Int32.of_int 1);
if (not (Limb.(=) res 0))
i := !i + 1;
if (res <> 0)
then begin
c := 0;
assert { res = !lx + 1 };
......@@ -343,13 +340,13 @@ module Add
let c = ref (0:limb) in
let lx : ref limb = ref (C.get x) in
let i : ref int32 = ref 1 in
let res = Limb.add_mod !lx y in
let res = add_mod !lx y in
C.set x res;
if (Limb.(<) res !lx)
if (res < !lx)
then begin
c := 1;
assert { radix + res = !lx + y };
while not (Limb.(=) !c 0) do
while (!c <> 0) do
invariant { 1 <= !i <= sz }
invariant { !i = sz -> !c = 0 }
invariant { 0 <= !c <= 1 }
......@@ -363,7 +360,7 @@ module Add
assert { !c = 1 };
lx := get_ofs x !i;
assert { !lx = (pelts ox)[ox.offset + !i] };
let res = Limb.add_mod !lx 1 in
let res = add_mod !lx 1 in
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
(x.offset + p2i sz) res;
......@@ -374,8 +371,8 @@ module Add
assert { value x !i + (power radix !i) * !c = value ox !i + y };
value_tail x !i;
value_tail ox !i;
i := Int32.(+) !i 1;
if not (Limb.(=) res 0)
i := !i + 1;
if res <> 0
then begin
c := 0;
assert { res = !lx + 1 };
......@@ -418,7 +415,7 @@ module Add
let ghost c : ref limb = ref 1 in
let lx : ref limb = ref 0 in
let i : ref int32 = ref 0 in
while (Limb.(=) !r 0) do
while (!r = 0) do
invariant { 0 <= !i <= sz }
invariant { !i = sz -> !r <> 0 }
invariant { !r <> 0 <-> !c = 0 }
......@@ -435,7 +432,7 @@ module Add
assert { !lx = (pelts ox)[ox.offset + !i] };
let res = add_mod !lx 1 in
r := res;
ghost (if Limb.(=) res 0 then c := 1 else c := 0);
ghost (if res = 0 then c := 1 else c := 0);
assert { res + radix * !c = !lx + 1 };
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
......@@ -449,7 +446,7 @@ module Add
value_tail ox !i;
assert { value x (!i+1) + power radix (!i+1) * !c =
value ox (!i+1) + 1 };
i := Int32.(+) !i 1;
i := !i + 1;
assert { !i = sz -> !c = 0
by value x sz + power radix sz * !c = value ox sz + 1
so value ox sz + 1 < power radix sz
......@@ -476,13 +473,13 @@ module Add
let c = ref 0 in
let lx = ref (C.get x) in
let i = ref 1 in
let res = Limb.add_mod !lx y in
let res = add_mod !lx y in
C.set x res;
if (Limb.(<) res !lx)
if (res < !lx)
then begin
c := 1;
assert { radix + res = !lx + y };
while Int32.(<) !i sz do
while !i < sz do
invariant { 1 <= !i <= sz }
invariant { 0 <= !c <= 1 }
invariant { !c = 1 \/ !i = sz }
......@@ -494,7 +491,7 @@ module Add
assert { !c = 1 };
lx := get_ofs x !i;
assert { !lx = (pelts ox)[offset ox + !i] };
let res = Limb.add_mod !lx 1 in
let res = add_mod !lx 1 in
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
(x.offset + p2i sz) res;
......@@ -505,8 +502,8 @@ module Add
assert { value x !i + (power radix !i) * !c = value ox !i + y };
value_tail x !i;
value_tail ox !i;
i := Int32.(+) !i 1;
if not (Limb.(=) res 0)
i := !i + 1;
if (res <> 0)
then begin
c := 0;
assert { res = !lx + 1 };
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -21,68 +21,64 @@ module Compare
ensures { result = compare_int (value x sz) (value y sz) }
=
let i = ref sz in
try
while Int32.(>=) !i (Int32.of_int 1) do
variant { !i }
invariant { 0 <= !i <= sz }
invariant { forall j. !i <= j < sz ->
(pelts x)[x.offset+j] = (pelts y)[y.offset+j] }
assert { forall j. 0 <= j < sz - !i ->
let k = !i+j in
!i <= k < sz ->
(pelts x)[x.offset+k] = (pelts y)[y.offset+k] /\
(pelts x)[!i+x.offset+j] = (pelts y)[!i+y.offset+j] };
value_sub_frame_shift (pelts x) (pelts y) (p2i !i+x.offset)
(p2i !i+y.offset) ((p2i sz) - (p2i !i));
let ghost k = p2i !i in
i := Int32.(-) !i (Int32.of_int 1);
assert { 0 <= !i < sz };
let lx = get_ofs x !i in
let ly = get_ofs y !i in
if (not (Limb.(=) lx ly))
then begin
value_sub_concat (pelts x) x.offset (x.offset+k) (x.offset+p2i sz);
value_sub_concat (pelts y) y.offset (y.offset+k) (y.offset+p2i sz);
assert { compare_int (value x sz)
(value y sz)
= compare_int (value x k) (value y k) };
value_sub_tail (pelts x) x.offset (x.offset+k-1);
value_sub_tail (pelts y) y.offset (y.offset+k-1);
if Limb.(>) lx ly
then begin
value_sub_upper_bound (pelts y) y.offset (y.offset+k-1);
value_sub_lower_bound (pelts x) x.offset (x.offset+k-1);
assert { value x k - value y k =
(l2i lx - ly) * (power radix (k-1))
- ((value y (k-1)) - (value x (k-1)))
};
assert { (lx - ly) * (power radix (k-1))
>= power radix (k-1)
> ((value y (k-1)) - (value x (k-1)))
};
raise Return32 (Int32.of_int 1)
end
else begin
assert { ly > lx };
value_sub_upper_bound (pelts x) x.offset (x.offset+k-1);
value_sub_lower_bound (pelts y) y.offset (y.offset+k-1);
assert { value y k - value x k =
(ly - lx) * (power radix (k-1))
- ((value x (k-1)) - (value y (k-1)))
while !i >= 1 do
variant { !i }
invariant { 0 <= !i <= sz }
invariant { forall j. !i <= j < sz ->
(pelts x)[x.offset+j] = (pelts y)[y.offset+j] }
assert { forall j. 0 <= j < sz - !i ->
let k = !i+j in
!i <= k < sz ->
(pelts x)[x.offset+k] = (pelts y)[y.offset+k] /\
(pelts x)[!i+x.offset+j] = (pelts y)[!i+y.offset+j] };
value_sub_frame_shift (pelts x) (pelts y) (p2i !i+x.offset)
(p2i !i+y.offset) ((p2i sz) - (p2i !i));
let ghost k = p2i !i in
i := !i - 1;
assert { 0 <= !i < sz };
let lx = get_ofs x !i in
let ly = get_ofs y !i in
if (not (lx = ly))
then begin
value_sub_concat (pelts x) x.offset (x.offset+k) (x.offset+p2i sz);
value_sub_concat (pelts y) y.offset (y.offset+k) (y.offset+p2i sz);
assert { compare_int (value x sz)
(value y sz)
= compare_int (value x k) (value y k) };
value_sub_tail (pelts x) x.offset (x.offset+k-1);
value_sub_tail (pelts y) y.offset (y.offset+k-1);
if lx > ly
then begin
value_sub_upper_bound (pelts y) y.offset (y.offset+k-1);
value_sub_lower_bound (pelts x) x.offset (x.offset+k-1);
assert { value x k - value y k =
(l2i lx - ly) * (power radix (k-1))
- ((value y (k-1)) - (value x (k-1)))
};
assert { (ly - lx) * (power radix (k-1))
>= power radix (k-1)
> ((value x (k-1)) - (value y (k-1)))
assert { (lx - ly) * (power radix (k-1))
>= power radix (k-1)
> ((value y (k-1)) - (value x (k-1)))
};
raise Return32 (Int32.(-_) (Int32.of_int 1))
end
end
else ()
done;
value_sub_frame_shift (pelts x) (pelts y) x.offset y.offset (p2i sz);
Int32.of_int 0
with Return32 r -> r
end
return 1
end
else begin
assert { ly > lx };
value_sub_upper_bound (pelts x) x.offset (x.offset+k-1);
value_sub_lower_bound (pelts y) y.offset (y.offset+k-1);
assert { value y k - value x k =
(ly - lx) * (power radix (k-1))
- ((value x (k-1)) - (value y (k-1)))
};
assert { (ly - lx) * (power radix (k-1))
>= power radix (k-1)
> ((value x (k-1)) - (value y (k-1)))
};
return -1
end
end
else ()
done;
value_sub_frame_shift (pelts x) (pelts y) x.offset y.offset (p2i sz);
0
end
This diff is collapsed.
This diff is collapsed.
......@@ -36,8 +36,7 @@ module Logical
returns { (r,_d) -> l2i r <= radix - (power 2 cnt) }
returns { (_r,d) -> l2i d < power 2 cnt }
=
let uzero = Limb.of_int 0 in
if (Limb.(=) cnt uzero) then (x, uzero)
if cnt = 0 then (x, 0)
else
begin
let (r:limb,d:limb) = lsld x cnt in
......@@ -45,8 +44,8 @@ module Logical
let ghost q = power 2 (Limb.length - l2i cnt) in
assert { p > 0 /\ q > 0 };
assert { radix = p * q by
radix = power 2 Limb.length = power 2 (cnt + (Limb.length - cnt))
= p*q };
radix = power 2 Limb.length = power 2 (cnt + (Limb.length - cnt))
= p*q };
assert { mod radix p = 0
by mod radix p
= mod (p * q + 0) p
......@@ -125,18 +124,15 @@ module Logical
ensures { value r sz + (power radix sz) * result =
value x sz * (power 2 (cnt)) }
=
let limb_zero = Limb.of_int 0 in
let zero = Int32.of_int 0 in
let one = Int32.of_int 1 in
let msb = Int32.(-) sz one in
let msb = sz - 1 in
let xp = ref (C.incr x msb) in
let rp = ref (C.incr r msb) in
let high = ref limb_zero in
let high = ref 0 in
let low = ref (C.get !xp) in
let i = ref msb in
let l, retval = lsld_ext !low cnt in
high := l;
while (Int32.(>) !i zero) do
while (!i > 0) do
variant { !i }
invariant { 0 <= !i < sz }
invariant { radix * value_sub (pelts r) (r.offset + 1 + !i) (r.offset + sz)
......@@ -158,14 +154,14 @@ module Logical
low := C.get !xp;
let l,h = lsld_ext !low cnt in
assert { !high + h < radix };
let ghost v = Limb.(+) !high h in
let ghost v = !high + h in
value_sub_update_no_change (pelts r) (!rp).offset (r.offset + 1 + p2i !i)
(r.offset + p2i sz) v;
C.set !rp (Limb.(+) !high h);
C.set !rp (!high + h);
rp.contents <- C.incr !rp (-1);
high := l;
let ghost k = p2i !i in
i := Int32.(-) !i one;
i := !i - 1;
value_sub_head (pelts r) (r.offset + k) (r.offset + p2i sz);
value_sub_head (pelts !xp) (!xp).offset (x.offset + p2i sz);
assert { radix
......@@ -263,18 +259,16 @@ module Logical
ensures { result + radix * value r sz
= value x sz * (power 2 (Limb.length - cnt)) }
=
let tnc = Limb.(-) (Limb.of_int Limb.length) cnt in
let zero = Int32.of_int 0 in
let one = Int32.of_int 1 in
let msb = Int32.(-) sz one in
let xp = ref (C.incr x zero) in
let rp = ref (C.incr r zero) in
let tnc = (Limb.of_int Limb.length) - cnt in
let msb = sz - 1 in
let xp = ref (C.incr x 0) in
let rp = ref (C.incr r 0) in
let high = ref (C.get !xp) in
let retval, h = lsld_ext !high tnc in
let low = ref h in
let i = ref zero in
let i = ref 0 in
let ghost c = power 2 (l2i tnc) in
while (Int32.(<) !i msb) do
while (!i < msb) do
variant { sz - !i }
invariant { 0 <= !i <= msb }
invariant { retval + radix * (value r !i
......@@ -292,13 +286,13 @@ module Logical
invariant { pelts !xp = pelts x }
invariant { !low < c}
label StartLoop in
xp.contents <- C.incr !xp one;
xp.contents <- C.incr !xp 1;
high := C.get !xp;
let l,h = lsld_ext !high tnc in
assert { !low + l < radix };
let ghost v = Limb.(+) !low l in
let ghost v = !low + l in
value_sub_shift_no_change (pelts r) r.offset (p2i !i) (p2i !i) v;
C.set !rp (Limb.(+) !low l);
C.set !rp (!low + l);
assert { value r !i = value (r at StartLoop) !i };
value_tail r !i;
value_tail x (!i+1);
......@@ -314,8 +308,8 @@ module Logical
assert { retval + radix * (value r (!i+1)
+ (power radix (!i+1)) * !low)
= value x (!i+2) * c };
i := Int32.(+) !i one;
rp.contents <- C.incr !rp one;
i := !i + 1;
rp.contents <- C.incr !rp 1;
done;
label EndLoop in
assert { retval + radix * (value r msb
......@@ -348,17 +342,17 @@ module Logical
value (old x) sz * power 2 cnt }
=
label Start in
let msb = Int32.(-) sz 1 in
let msb = sz - 1 in
let xp = ref (C.incr x msb) in
let ghost ox = { x } in
let ghost oxp = ref (C.incr ox msb) in
let high = ref (Limb.of_int 0) in
let high = ref 0 in
let low = ref (C.get !xp) in
let i = ref msb in
let l, retval = lsld_ext !low cnt in
high := l;
let ghost c = power 2 (l2i cnt) in
while (Int32.(>) !i 0) do
while (!i > 0) do
variant { !i }
invariant { 0 <= !i < sz }
invariant { radix * value_sub (pelts x) (x.offset + !i + 1) (x.offset + sz)
......@@ -387,13 +381,13 @@ module Logical
so offset !oxp = offset x + (!i-1) = offset !xp };
let l, h = lsld_ext !low cnt in
assert { !high + h < radix };
let ghost v = Limb.(+) !high h in
let ghost v = !high + h in
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + 1 + p2i !i)
(x.offset + p2i sz) v;
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
x.offset (x.offset + p2i !i) v;
C.set_ofs !xp 1 (Limb.(+) !high h);
C.set_ofs !xp 1 (!high + h);
assert { value_sub (pelts x) (x.offset + !i + 1) (x.offset + sz)
= (value_sub (pelts x) (x.offset + !i + 1) (x.offset + sz)
at StartLoop) };
......@@ -417,7 +411,7 @@ module Logical
assert { radix * value_sub (pelts x) (x.offset + !i) (x.offset + sz)
+ (power radix (sz - (!i - 1))) * retval + !high
= value !oxp (sz - !i + 1) * c };
i := Int32.(-) !i 1;
i := !i - 1;
assert { forall j. 0 <= j <= !i ->
(pelts x)[offset x + j] = (pelts ox)[offset x + j]
by (pelts x)[offset x + j] = (pelts x at StartLoop)[offset x + j]
......@@ -442,8 +436,8 @@ module Logical
ensures { result + radix * value x sz
= value (old x) sz * (power 2 (Limb.length - cnt)) }
=
let tnc = Limb.(-) (Limb.of_int Limb.length) cnt in
let msb = Int32.(-) sz 1 in
let tnc = (Limb.of_int Limb.length) - cnt in
let msb = sz - 1 in
let xp = ref (C.incr x 0) in
let ghost ox = { x } in
let ghost oxp = ref (C.incr ox 0) in
......@@ -452,7 +446,7 @@ module Logical
let low = ref h in
let i = ref 0 in
let ghost c = power 2 (l2i tnc) in
while (Int32.(<) !i msb) do
while (!i < msb) do
variant { sz - !i }
invariant { 0 <= !i <= msb }
invariant { retval + radix * (value x !i + (power radix !i) * !low)
......@@ -482,11 +476,11 @@ module Logical
= (pelts x)[x.offset + (!i + 1)] = !high };
let l, h = lsld_ext !high tnc in
assert { !low + l < radix };
let ghost v = Limb.(+) !low l in
let ghost v = !low + l in
value_sub_shift_no_change (pelts x) (x.offset) (p2i !i) (p2i !i) v;
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + 1 + p2i !i) (x.offset + p2i sz) v;
C.set_ofs !xp (-1) (Limb.(+) !low l);
C.set_ofs !xp (-1) (!low + l);
assert { value x !i = value (x at StartLoop) !i };
value_tail x !i;
value_tail ox (!i+1);
......@@ -501,7 +495,7 @@ module Logical
(* nonlinear part *)
assert { retval + radix * (value x (!i+1) + power radix (!i+1) * !low)
= value ox (!i+2) * c };
i := Int32.(+) !i 1;
i := !i + 1;
assert { forall j. !i <= j < sz ->
(pelts x)[offset x + j] = (pelts ox)[offset x + j]
by (pelts x)[offset x + j] = (pelts x at StartLoop)[offset x + j]
......@@ -518,8 +512,5 @@ module Logical
value_tail x msb;
assert { value x sz = value (x at EndLoop) msb + (power radix msb) * !low };
retval
end
......@@ -26,11 +26,10 @@ module Mul
-> (pelts r)[j] = old (pelts r)[j] }
writes { r.data.elts }
=
let limb_zero = Limb.of_int 0 in
let lx = ref limb_zero in
let c = ref limb_zero in
let i = ref (Int32.of_int 0) in
while Int32.(<) !i sz do
let lx = ref 0 in
let c = ref 0 in
let i = ref 0 in
while !i < sz do
variant { sz - !i }
invariant { 0 <= !i <= sz }
invariant { value r !i + (power radix !i) * !c =
......@@ -39,13 +38,7 @@ module Mul
-> (pelts r)[j] = old (pelts r)[j] }
label StartLoop in
lx := get_ofs x !i;
let rl, rh = Limb.mul_double !lx y in
let res, carry = Limb.add_with_carry rl !c limb_zero in
label BeforeWrite in
value_sub_shift_no_change (pelts r) r.offset (p2i !i) (p2i !i) res;
set_ofs r !i res;
assert { value r !i + (power radix !i) * !c =
value x !i * y };
let rl, rh = mul_double !lx y in
assert { rh < radix - 1
by
(!lx * y <= !lx * (radix-1) <= (radix-1)*(radix-1)
......@@ -58,7 +51,15 @@ module Mul
so
radix * rh <= (radix -1) * (radix -1)
};
c := Limb.(+) rh carry;
let res = add_mod rl !c in
c := rh;
[@vc:sp] if res < rl then c := !c + 1;
assert { res + radix * !c = !lx * y + (!c at StartLoop) };
label BeforeWrite in
value_sub_shift_no_change (pelts r) r.offset (p2i !i) (p2i !i) res;
set_ofs r !i res;
assert { value r !i + ((power radix !i) * !c at StartLoop) =
value x !i * y };
value_tail r !i;
value_tail x !i;
assert { value x (!i+1) * y
......@@ -66,7 +67,7 @@ module Mul
(*nonlinear, needed for reflection*)
assert { value r (!i+1) + (power radix (!i+1)) * !c =
value x (!i+1) * y };
i := Int32.(+) !i (Int32.of_int 1);
i := !i + 1;
done;
!c
......@@ -84,12 +85,11 @@ module Mul
ensures { forall j. (j < r.offset \/ r.offset + sz <= j) ->
(pelts r)[j] = (pelts (old r))[j] }
=
let limb_zero = Limb.of_int 0 in
let lx = ref limb_zero in
let lr = ref limb_zero in
let c = ref limb_zero in
let i = ref (Int32.of_int 0) in
while Int32.(<) !i sz do
let lx = ref 0 in
let lr = ref 0 in
let c = ref 0 in
let i = ref 0 in
while !i < sz do
variant { sz - !i }
invariant { 0 <= !i <= sz }
invariant { value r !i + (power radix !i) * !c
......@@ -103,8 +103,8 @@ module Mul
lx := get_ofs x !i;
lr := get_ofs r !i;
assert { !lr = (pelts (old r))[r.offset + !i] };
let rl, rh = Limb.mul_double !lx y in
let res, carry = Limb.add3 !lr rl !c in
let rl, rh = mul_double !lx y in
let res, carry = add3 !lr rl !c in
value_tail r !i;
value_tail x !i;
assert { value (old r) (!i+1) = value (old r) !i + power radix !i * !lr };
......@@ -137,14 +137,14 @@ module Mul
rl + radix * rh <= (radix-1)*(radix-1) };
assert { rh = radix - 2 -> carry <= 1
by rl <= 1 };
c := Limb.(+) rh carry;
c := rh + carry;
assert { value x (!i + 1) * y
= value x !i * y + (power radix !i) * (!lx * y) };
(* nonlinear part *)
assert { value r (!i+1) + (power radix (!i+1)) * !c
= value (old r) (!i+1)
+ value x (!i+1) * y };
i := Int32.(+) !i (Int32.of_int 1);
i := !i + 1;
done;
!c
......@@ -163,12 +163,10 @@ module Mul
-> (pelts r)[j] = old (pelts r)[j] }
=
wmpn_zero r sz;
let limb_zero = Limb.of_int 0 in
let one = Int32.of_int 1 in
let rp = ref (C.incr r (Int32.of_int 0)) in
let ly = ref limb_zero in
let i = ref (Int32.of_int 0) in
while Int32.(<) !i sz do
let rp = ref (C.incr r 0) in
let ly = ref 0 in
let i = ref 0 in
while !i < sz do
invariant { 0 <= !i <= sz }
invariant { value r (!i + sz) = value x sz * value y !i }
invariant { (!rp).offset = r.offset + !i }
......@@ -221,8 +219,8 @@ module Mul
= value x sz * value y !i + (power radix !i) * (value x sz * !ly) };
(* nonlinear *)
assert { value r (!i + sz + 1) = value x sz * value y (!i+1) };
i := Int32.(+) !i one;
rp.contents <- C.incr !rp one;
i := !i + 1;
rp.contents <- C.incr !rp 1;
done
let wmpn_addmul_n (r x y:t) (sz:int32) : limb
......@@ -236,14 +234,12 @@ module Mul
= value (old r) (sz + sz)
+ value x sz * value y sz }
=
let limb_zero = Limb.of_int 0 in
let one = Int32.of_int 1 in
let rp = ref (C.incr r (Int32.of_int 0)) in
let ly = ref limb_zero in
let lr = ref limb_zero in
let c = ref limb_zero in
let i = ref (Int32.of_int 0) in
while Int32.(<) !i sz do