Commit eab446ca authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Rename functions to match their GMP equivalents

parent 9585835c
......@@ -11,11 +11,11 @@ module Add
use types.Types
use lemmas.Lemmas
(** `add_limb r x y sz` adds to `x` the value of the limb `y`,
(** `wmpn_add_1 r x y sz` adds to `x` the value of the limb `y`,
writes the result in `r` and returns the carry. `r` and `x`
have size `sz`. This corresponds to the function `mpn_add_1` *)
(* r and x must be separated. This is enforced by Why3 regions in typing *)
let add_limb (r x:t) (y:limb) (sz:int32) : limb
let wmpn_add_1 (r x:t) (y:limb) (sz:int32) : limb
requires { valid x sz }
requires { valid r sz }
requires { sz > 0 } (* ? GMP does the same for 0 and 1*)
......@@ -74,10 +74,10 @@ module Add
end
(** `add_limbs r x y sz` adds `x[0..sz-1]` and `y[0..sz-1]` and writes the result in `r`.
(** `wmpn_add_n r x y sz` adds `x[0..sz-1]` and `y[0..sz-1]` and writes the result in `r`.
Returns the carry, either `0` or `1`. Corresponds to the function `mpn_add_n`. *)
let add_limbs (r x y:t) (sz:int32) : limb
let wmpn_add_n (r x y:t) (sz:int32) : limb
requires { valid x sz }
requires { valid y sz }
requires { valid r sz }
......@@ -119,10 +119,10 @@ module Add
done;
!c
(** `add r x y sx sy` adds `(x, sx)` to `(y, sy)` and writes the
(** `wmpn_add r x y sx sy` adds `(x, sx)` to `(y, sy)` and writes the
result in `(r, sx)`. `sx` must be greater than or equal to
`sy`. Returns carry, either 0 or 1. Corresponds to `mpn_add`. *)
let add (r x y:t) (sx sy:int32) : limb
let wmpn_add (r x y:t) (sx sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx }
requires { valid y sy }
......@@ -209,7 +209,7 @@ module Add
done;
!c
let add_in_place (x y:t) (sx sy:int32) : limb
let wmpn_add_in_place (x y:t) (sx sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx }
requires { valid y sy }
......@@ -306,10 +306,10 @@ module Add
use int.EuclideanDivision
(** `incr x y sz` adds to `x` the value of the limb `y` in place.
(** `wmpn_incr x y sz` adds to `x` the value of the limb `y` in place.
`x` has size `sz`. The addition must not overflow. This corresponds
to `mpn_incr` *)
let incr (x:t) (y:limb) (ghost sz:int32) : unit
to `mpn_wmpn_incr` *)
let wmpn_incr (x:t) (y:limb) (ghost sz:int32) : unit
requires { valid x sz }
requires { sz > 0 }
requires { value x sz + y < power radix sz }
......@@ -366,10 +366,10 @@ module Add
so (pelts x)[x.offset + k] = (pelts ox)[x.offset + k]};
value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sz)
(** `incr_1 x sz` adds 1 to `x` in place.
(** `wmpn_incr_1 x sz` adds 1 to `x` in place.
`x` has size `sz`. The addition must not overflow.
This corresponds to `mpn_incr` *)
let incr_1 (x:t) (ghost sz:int32) : unit
This corresponds to `mpn_wmpn_incr` *)
let wmpn_incr_1 (x:t) (ghost sz:int32) : unit
requires { valid x sz }
requires { sz > 0 }
requires { value x sz + 1 < power radix sz }
......
This diff is collapsed.
......@@ -13,9 +13,9 @@ module Compare
function compare_int (x y:int) : int =
if x < y then -1 else if x=y then 0 else 1
(** `compare_same_size` compares `x[0..sz-1]` and `y[0..sz-1]` as unsigned integers.
(** `wmpn_cmp` compares `x[0..sz-1]` and `y[0..sz-1]` as unsigned integers.
It corresponds to `GMPN_CMP`. *)
let compare_same_size (x y:t) (sz:int32) : int32
let wmpn_cmp (x y:t) (sz:int32) : int32
requires { valid x sz }
requires { valid y sz }
ensures { result = compare_int (value x sz) (value y sz) }
......
......@@ -8,136 +8,136 @@
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../compare.mlw" proved="true">
<theory name="Compare" proved="true">
<goal name="VC compare_same_size" expl="VC for compare_same_size" proved="true">
<goal name="VC wmpn_cmp" expl="VC for wmpn_cmp" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC compare_same_size.0" expl="loop invariant init" proved="true">
<goal name="VC wmpn_cmp.0" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
<goal name="VC compare_same_size.1" expl="loop invariant init" proved="true">
<goal name="VC wmpn_cmp.1" expl="loop invariant init" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="10"/></proof>
</goal>
<goal name="VC compare_same_size.2" expl="integer overflow" proved="true">
<goal name="VC wmpn_cmp.2" expl="integer overflow" proved="true">
<proof prover="5"><result status="valid" time="0.09" steps="21"/></proof>
</goal>
<goal name="VC compare_same_size.3" expl="assertion" proved="true">
<goal name="VC wmpn_cmp.3" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="39"/></proof>
</goal>
<goal name="VC compare_same_size.4" expl="precondition" proved="true">
<goal name="VC wmpn_cmp.4" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="46"/></proof>
</goal>
<goal name="VC compare_same_size.5" expl="integer overflow" proved="true">
<goal name="VC wmpn_cmp.5" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="24"/></proof>
</goal>
<goal name="VC compare_same_size.6" expl="integer overflow" proved="true">
<goal name="VC wmpn_cmp.6" expl="integer overflow" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="26"/></proof>
</goal>
<goal name="VC compare_same_size.7" expl="assertion" proved="true">
<goal name="VC wmpn_cmp.7" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="16"/></proof>
</goal>
<goal name="VC compare_same_size.8" expl="precondition" proved="true">
<goal name="VC wmpn_cmp.8" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
<goal name="VC compare_same_size.9" expl="precondition" proved="true">
<goal name="VC wmpn_cmp.9" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.06" steps="28"/></proof>
</goal>
<goal name="VC compare_same_size.10" expl="precondition" proved="true">
<goal name="VC wmpn_cmp.10" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="20"/></proof>
</goal>
<goal name="VC compare_same_size.11" expl="precondition" proved="true">
<goal name="VC wmpn_cmp.11" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="21"/></proof>
</goal>
<goal name="VC compare_same_size.12" expl="assertion" proved="true">
<goal name="VC wmpn_cmp.12" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="51"/></proof>
</goal>
<goal name="VC compare_same_size.13" expl="precondition" proved="true">
<goal name="VC wmpn_cmp.13" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="23"/></proof>
</goal>
<goal name="VC compare_same_size.14" expl="precondition" proved="true">
<goal name="VC wmpn_cmp.14" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.07" steps="24"/></proof>
</goal>
<goal name="VC compare_same_size.15" expl="precondition" proved="true">
<goal name="VC wmpn_cmp.15" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC compare_same_size.16" expl="assertion" proved="true">
<goal name="VC wmpn_cmp.16" expl="assertion" proved="true">
<transf name="inline_all" proved="true" >
<goal name="VC compare_same_size.16.0" expl="assertion" proved="true">
<goal name="VC wmpn_cmp.16.0" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="19"/></proof>
</goal>
</transf>
</goal>
<goal name="VC compare_same_size.17" expl="assertion" proved="true">
<goal name="VC wmpn_cmp.17" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC compare_same_size.17.0" expl="VC for compare_same_size" proved="true">
<goal name="VC wmpn_cmp.17.0" expl="VC for wmpn_cmp" proved="true">
<proof prover="1" memlimit="2000"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC compare_same_size.17.1" expl="VC for compare_same_size" proved="true">
<goal name="VC wmpn_cmp.17.1" expl="VC for wmpn_cmp" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="VC compare_same_size.18" expl="integer overflow" proved="true">
<goal name="VC wmpn_cmp.18" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC compare_same_size.19" expl="postcondition" proved="true">
<goal name="VC wmpn_cmp.19" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC compare_same_size.20" expl="assertion" proved="true">
<goal name="VC wmpn_cmp.20" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="26"/></proof>
</goal>
<goal name="VC compare_same_size.21" expl="precondition" proved="true">
<goal name="VC wmpn_cmp.21" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC compare_same_size.22" expl="assertion" proved="true">
<goal name="VC wmpn_cmp.22" expl="assertion" proved="true">
<transf name="inline_all" proved="true" >
<goal name="VC compare_same_size.22.0" expl="assertion" proved="true">
<goal name="VC wmpn_cmp.22.0" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.05" steps="20"/></proof>
</goal>
</transf>
</goal>
<goal name="VC compare_same_size.23" expl="assertion" proved="true">
<goal name="VC wmpn_cmp.23" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC compare_same_size.23.0" expl="VC for compare_same_size" proved="true">
<goal name="VC wmpn_cmp.23.0" expl="VC for wmpn_cmp" proved="true">
<proof prover="1" memlimit="2000"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC compare_same_size.23.1" expl="VC for compare_same_size" proved="true">
<goal name="VC wmpn_cmp.23.1" expl="VC for wmpn_cmp" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC compare_same_size.24" expl="integer overflow" proved="true">
<goal name="VC wmpn_cmp.24" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.23" steps="43"/></proof>
</goal>
<goal name="VC compare_same_size.25" expl="integer overflow" proved="true">
<goal name="VC wmpn_cmp.25" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC compare_same_size.26" expl="postcondition" proved="true">
<goal name="VC wmpn_cmp.26" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC compare_same_size.27" expl="loop variant decrease" proved="true">
<goal name="VC wmpn_cmp.27" expl="loop variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="20"/></proof>
</goal>
<goal name="VC compare_same_size.28" expl="loop invariant preservation" proved="true">
<goal name="VC wmpn_cmp.28" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="20"/></proof>
</goal>
<goal name="VC compare_same_size.29" expl="loop invariant preservation" proved="true">
<goal name="VC wmpn_cmp.29" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="44"/></proof>
</goal>
<goal name="VC compare_same_size.30" expl="precondition" proved="true">
<goal name="VC wmpn_cmp.30" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="43"/></proof>
</goal>
<goal name="VC compare_same_size.31" expl="integer overflow" proved="true">
<goal name="VC wmpn_cmp.31" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC compare_same_size.32" expl="postcondition" proved="true">
<goal name="VC wmpn_cmp.32" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.10" steps="37"/></proof>
</goal>
</transf>
......
......@@ -318,11 +318,11 @@ module Div
assert { !qh * d + !r = ul + radix * uh };
(!qh,!r)
(** `divmod_1 q x y sz` divides `(x, sz)` by `y`, writes the quotient
(** `wmpn_divrem_1 q x y sz` divides `(x, sz)` by `y`, writes the quotient
in `(q, sz)` and returns the remainder. Corresponds to
`mpn_divmod_1`. *)
`mpn_wmpn_divrem_1`. *)
(* TODO develop further decimal points (qxn) *)
let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
let wmpn_divrem_1 (q x:t) (y:limb) (sz:int32) : limb
requires { valid x sz }
requires { valid q sz }
requires { 0 < sz }
......@@ -1340,7 +1340,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
let ghost vy = value y (p2i sy) in
let x1 = ref limb_zero in
let x0 = ref limb_zero in
let r = compare_same_size xd y sy in
let r = wmpn_cmp xd y sy in
let qh = (*begin
ensures { r >= 0 -> result = 1 }
ensures { r < 0 -> result = 0 }*)
......@@ -1367,7 +1367,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
if (not (Limb.(=) qh limb_zero))
then begin
assert { qh = 1 };
let ghost b = sub_in_place xd y sy sy in
let ghost b = wmpn_sub_in_place xd y sy sy in
begin
ensures { value (x at PreAdjust) sx =
(value !qp (sx - sy - !i)
......@@ -2398,7 +2398,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
so 0 <= j < xc.Array.length
} ;
value_sub_frame (pelts x) xc.elts x.offset (x.offset + p2i !i);
let c = add_in_place xd y (Int32.(-) sy one) (Int32.(-) sy one) in
let c = wmpn_add_in_place xd y (Int32.(-) sy one) (Int32.(-) sy one) in
begin
ensures { value x !i
= value (x at Adjust) !i }
......@@ -3109,7 +3109,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
+ value x sy };
qh
let divmod_2 (q x y:t) (sx:int32) : limb
let wmpn_divrem_2 (q x y:t) (sx:int32) : limb
requires { 2 <= sx }
requires { valid x sx }
requires { valid y 2 }
......@@ -3376,7 +3376,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
assert { value y sy >= power radix (sy - 1) };
if (Int32.(=) sy one)
then
let lr = divmod_1 q x (C.get y) sx in
let lr = wmpn_divrem_1 q x (C.get y) sx in
C.set r lr
else
if (Int32.(=) sy two)
......@@ -3385,13 +3385,13 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
let ghost p = power 2 (p2i clz) in
if Int32.(=) clz zero
then begin
copy nx x sx;
wmpn_copyi nx x sx;
value_sub_shift_no_change (pelts x) x.offset (p2i sx) (p2i sx) limb_zero;
C.set_ofs nx sx limb_zero;
value_sub_frame_shift (pelts x) (pelts nx) x.offset nx.offset (p2i sx);
label Div2_ns in
let ghost _qh = divmod_2 q nx y (Int32.(+) sx one) in
copy r nx sy;
let ghost _qh = wmpn_divrem_2 q nx y (Int32.(+) sx one) in
wmpn_copyi r nx sy;
assert { value x sx
= value q (sx - sy + 1) * value y sy
+ value r sy
......@@ -3430,7 +3430,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
()
end
else begin
let ghost _c = lshift ny y sy (Limb.of_int32 clz) in
let ghost _c = wmpn_lshift ny y sy (Limb.of_int32 clz) in
begin
ensures { normalized ny sy }
ensures { value ny sy = power 2 clz * value y sy }
......@@ -3479,7 +3479,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
so ndh >= div radix 2
};
end;
let h = lshift nx x sx (Limb.of_int32 clz) in
let h = wmpn_lshift nx x sx (Limb.of_int32 clz) in
C.set_ofs nx sx h;
begin
ensures { value nx (sx + 1)
......@@ -3496,8 +3496,8 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
end;
label Div2_s in
(* TODO don't add 1 when not needed, cf "adjust" in GMP algo *)
let ghost _qh = divmod_2 q nx ny (Int32.(+) sx one) in
let ghost _l = rshift r nx sy (Limb.of_int32 clz) in
let ghost _qh = wmpn_divrem_2 q nx ny (Int32.(+) sx one) in
let ghost _l = wmpn_rshift r nx sy (Limb.of_int32 clz) in
begin ensures { value nx 2 = p * value r 2 }
assert { _l = 0
by
......@@ -3624,7 +3624,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
let ghost p = power 2 (p2i clz) in
if Int32.(=) clz zero
then begin
copy nx x sx;
wmpn_copyi nx x sx;
value_sub_shift_no_change (pelts x) x.offset
(p2i sx) (p2i sx) limb_zero;
C.set_ofs nx sx limb_zero;
......@@ -3659,7 +3659,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
= dh * power radix (sx - 1))) };
label Div_ns in
let ghost _qh = div_sb_qr q nx y (Int32.(+) sx adjust) sy in
copy r nx sy;
wmpn_copyi r nx sy;
assert { value x sx
= value q (sx - sy + adjust) * value y sy
+ value r sy
......@@ -3705,7 +3705,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
end
end
else begin
let ghost _c = lshift ny y sy (Limb.of_int32 clz) in
let ghost _c = wmpn_lshift ny y sy (Limb.of_int32 clz) in
begin
ensures { normalized ny sy }
ensures { value ny sy
......@@ -3762,7 +3762,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
so ndh >= div radix 2
};
end;
let h = lshift nx x sx (Limb.of_int32 clz) in
let h = wmpn_lshift nx x sx (Limb.of_int32 clz) in
label Shifted in
C.set_ofs nx sx h;
begin
......@@ -3851,7 +3851,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
= p * dh * power radix (sy - 1 + sx - sy)
= p * dh * power radix (sx - 1))) };
let ghost _qh = div_sb_qr q nx ny (Int32.(+) sx adjust) sy in
let ghost _l = rshift r nx sy (Limb.of_int32 clz) in
let ghost _l = wmpn_rshift r nx sy (Limb.of_int32 clz) in
begin ensures { value nx sy = p * value r sy }
assert { _l = 0
by
......@@ -3984,7 +3984,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
end
end
let tdiv_qr (q r x y:t) (sx sy:int32) : unit
let wmpn_tdiv_qr (q r x y:t) (sx sy:int32) : unit
requires { 1 <= sy <= sx <= (Int32.max_int32 - 1) }
requires { valid x sx }
requires { valid y sy }
......
This diff is collapsed.
......@@ -113,11 +113,11 @@ module Logical
};
r
(** `lshift r x sz cnt` shifts `(x, sz)` `cnt` bits to the left and
(** `wmpn_lshift r x sz cnt` shifts `(x, sz)` `cnt` bits to the left and
writes the result in `(r, sz)`. Returns the `cnt` most significant
bits of `(x, sz)`. Corresponds to `mpn_lshift`. *)
bits of `(x, sz)`. Corresponds to `mpn_wmpn_lshift`. *)
(*TODO overlapping allowed if r >= x*)
let lshift (r x:t) (sz:int32) (cnt:limb) : limb
let wmpn_lshift (r x:t) (sz:int32) (cnt:limb) : limb
requires { 0 < cnt < Limb.length }
requires { valid r sz }
requires { valid x sz }
......@@ -252,11 +252,11 @@ module Logical
value_sub_head (pelts r) r.offset (r.offset + p2i sz);
retval
(** `rshift r x sz cnt` shifts `(x, sz)` `cnt` bits to the right and
(** `wmpn_rshift r x sz cnt` shifts `(x, sz)` `cnt` bits to the right and
writes the result in `(r, sz)`. Returns the `cnt` least significant
bits of `(x, sz)`. Corresponds to `mpn_rshift`. *)
bits of `(x, sz)`. Corresponds to `mpn_wmpn_rshift`. *)
(*TODO overlapping allowed if r <= x*)
let rshift (r x:t) (sz:int32) (cnt:limb) : limb
let wmpn_rshift (r x:t) (sz:int32) (cnt:limb) : limb
requires { valid x sz }
requires { valid r sz }
requires { 0 < cnt < Limb.length }
......
......@@ -14,10 +14,10 @@ module Mul
use add.Add
(** `mul_limb r x y sz` multiplies `x[0..sz-1]` by the limb `y` and
(** `wmpn_mul_1 r x y sz` multiplies `x[0..sz-1]` by the limb `y` and
writes the n least significant limbs in `r`, and returns the most
significant limb. It corresponds to `mpn_mul_1`. *)
let mul_limb (r x:t) (y:limb) (sz:int32) : limb
let wmpn_mul_1 (r x:t) (y:limb) (sz:int32) : limb
requires { valid x sz }
requires { valid r sz }
ensures { value r sz + (power radix sz) * result
......@@ -70,11 +70,11 @@ module Mul
done;
!c
(** `addmul_limb r x y sz` multiplies `(x, sz)` by `y`, adds the `sz`
(** `wmpn_addmul_1 r x y sz` multiplies `(x, sz)` by `y`, adds the `sz`
least significant limbs to `(r, sz)` and writes the result in `(r, sz)`.
Returns the most significant limb of the product plus the carry
of the addition. Corresponds to `mpn_addmul_1`.*)
let addmul_limb (r x:t) (y:limb) (sz:int32):limb
let wmpn_addmul_1 (r x:t) (y:limb) (sz:int32):limb
requires { valid x sz }
requires { valid r sz }
ensures { value r sz + (power radix sz) * result
......@@ -148,10 +148,10 @@ module Mul
done;
!c
(** `mul_limbs r x y sz` multiplies `(x, sz)` and `(y, sz)` and
(** `wmpn_mul_n r x y sz` multiplies `(x, sz)` and `(y, sz)` and
writes the result to `(r, 2*sz)`. `r` must not overlap with either
`x` or `y`. Corresponds to `mpn_mul_n`. *)
let mul_limbs (r x y:t) (sz:int32) : unit
let wmpn_mul_n (r x y:t) (sz:int32) : unit
requires { sz > 0 }
requires { valid x sz }
requires { valid y sz }
......@@ -162,7 +162,7 @@ module Mul
ensures { forall j. (j < offset r \/ offset r + (sz + sz) <= j)
-> (pelts r)[j] = old (pelts r)[j] }
=
zero r sz;
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
......@@ -184,7 +184,7 @@ module Mul
assert { value !rp sz
= value_sub (pelts r) (offset r + !i) (offset r + (!i + sz)) };
ly := get_ofs y !i;
let c' = addmul_limb !rp x !ly sz in
let c' = wmpn_addmul_1 !rp x !ly sz in
assert { value !rp sz + power radix sz * c'
= value (!rp at StartLoop) sz + value x sz * !ly };
assert { MapEq.map_eq_sub (pelts r) (pelts r at StartLoop)
......@@ -225,7 +225,7 @@ module Mul
rp.contents <- C.incr !rp one;
done
let addmul_limbs (r x y:t) (sz:int32) : limb
let wmpn_addmul_n (r x y:t) (sz:int32) : limb
requires { sz > 0 }
requires { valid x sz }
requires { valid y sz }
......@@ -262,7 +262,7 @@ module Mul
assert { value !rp sz
= value_sub (pelts r) (r.offset + !i) (r.offset + (!i + sz)) };
ly := get_ofs y !i;
let c' = addmul_limb !rp x !ly sz in
let c' = wmpn_addmul_1 !rp x !ly sz in
assert { forall j. (!rp).offset + sz <= j ->
(pelts (old r)) [j] = (pelts r)[j]
by (pelts r)[j]
......@@ -312,10 +312,10 @@ module Mul
done;
!c
(** `mul r x y sx sy` multiplies `(x, sx)` and `(y,sy)` and writes
(** `wmpn_mul r x y sx sy` multiplies `(x, sx)` and `(y,sy)` and writes
the result in `(r, sx+sy)`. `sx` must be greater than or equal to
`sy`. Corresponds to `mpn_mul`. *)
let mul (r x y:t) (sx sy:int32) : unit
let wmpn_mul (r x y:t) (sx sy:int32) : unit
requires { 0 < sy <= sx }
requires { valid x sx }
requires { valid y sy }
......@@ -327,7 +327,7 @@ module Mul
(*ensures { result = (pelts r)[r.offset + sx + sy - 1] }*)
=
let ly = ref (C.get y) in
let c = mul_limb r x !ly sx in
let c = wmpn_mul_1 r x !ly sx in
value_sub_update_no_change (pelts r) (r.offset + p2i sx)
r.offset (r.offset + p2i sx - 1) c;
set_ofs r sx c;
......@@ -354,7 +354,7 @@ module Mul
assert { value !rp sx =
value_sub (pelts r) (r.offset + !i) (r.offset + (!i + sx)) };
ly := get_ofs y !i;
let res = addmul_limb !rp x !ly sx in
let res = wmpn_addmul_1 !rp x !ly sx in
assert { value !rp sx + power radix sx * res
= value (!rp at StartLoop) sx + value x sx * !ly };
assert { MapEq.map_eq_sub (pelts r) (pelts r at StartLoop)
......
This diff is collapsed.
......@@ -12,10 +12,10 @@ module Sub
use lemmas.Lemmas
(** `sub_limb r x y sz` subtracts `y` from `(x, sz)` and writes
(** `wmpn_sub_1 r x y sz` subtracts `y` from `(x, sz)` and writes
the result to `(r, sz)`. Returns borrow, either 0 or
1. Corresponds to `mpn_sub_1`. *)
let sub_limb (r x:t) (y:limb) (sz:int32) : limb
let wmpn_sub_1 (r x:t) (y:limb) (sz:int32) : limb
requires { valid x sz }
requires { valid r sz }
requires { 0 < sz }
......@@ -73,10 +73,10 @@ module Sub
!b
end
(** `sub_limbs r x y sz` subtracts `(y, sz)` from `(x, sz)` and
(** `wmpn_sub_n r x y sz` subtracts `(y, sz)` from `(x, sz)` and
writes the result to `(r, sz)`. Returns borrow, either 0 or
1. Corresponds to `mpn_sub_n`. *)
let sub_limbs (r x y:t) (sz:int32) : limb
let wmpn_sub_n (r x y:t) (sz:int32) : limb
requires { valid x sz }
requires { valid y sz }
requires { valid r sz }
......@@ -117,10 +117,10 @@ module Sub
done;
!b
(** `sub r x y sx sy` subtracts `(y,sy)` from `(x, sx)` and writes the
(** `wmpn_sub r x y sx sy` subtracts `(y,sy)` from `(x, sx)` and writes the
result in `(r, sx)`. `sx` must be greater than or equal to
`sy`. Returns borrow, either 0 or 1. Corresponds to `mpn_sub`. *)
let sub (r x y:t) (sx sy:int32) : limb
let wmpn_sub (r x y:t) (sx sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx }
requires { valid y sy }
......@@ -208,7 +208,7 @@ module Sub
done;
!b
let sub_in_place (x y:t) (sx sy:int32) : limb
let wmpn_sub_in_place (x y:t) (sx sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx }
requires { valid y sy }
......@@ -305,10 +305,10 @@ module Sub
end
end
(** `decr x y sz` subtracts from `x` the value of the limb `y` in place.
(** `wmpn_decr x y sz` subtracts from `x` the value of the limb `y` in place.
`x` has size `sz`. The subtraction must not overflow. This corresponds
to `mpn_decr` *)
let decr (x:t) (y:limb) (ghost sz:int32) : unit
to `mpn_wmpn_decr` *)
let wmpn_decr (x:t) (y:limb) (ghost sz:int32) : unit
requires { valid x sz }
requires { sz > 0 }
requires { 0 <= value x sz - y }
......@@ -369,8 +369,8 @@ module Sub
(** `incr_1 x sz` subtracts 1 from `x` in place.
`x` has size `sz`. The subtraction must not overflow.
This corresponds to `mpn_decr` *)
let decr_1 (x:t) (ghost sz:int32) : unit
This corresponds to `mpn_wmpn_decr` *)
let wmpn_decr_1 (x:t) (ghost sz:int32) : unit
requires { valid x sz }
requires { sz > 0 }
requires { 0 <= value x sz - 1 }
......
This diff is collapsed.
......@@ -110,7 +110,7 @@ int main () {
c = mpn_add (refp, ap, an, bp, bn);
#endif
#ifdef TEST_WHY3
refc = add (rp, ap, bp, an, bn);
refc = wmpn_add (rp, ap, bp, an, bn);
#endif
#ifdef BENCH
......@@ -174,7 +174,7 @@ int main () {
mpn_mul (refp, ap, an, bp, bn);
#endif
#ifdef TEST_WHY3
mul (rp, ap, bp, an, bn);
wmpn_mul (rp, ap, bp, an, bn);
#endif
#ifdef BENCH
......@@ -238,7 +238,7 @@ int main () {
mpn_div_qr (refq, refr, an, bp, bn);
#endif
#ifdef TEST_WHY3
tdiv_qr(rq, rr, ap, bp, an, bn);
wmpn_tdiv_qr(rq, rr, ap, bp, an, bn);
#endif
#ifdef BENCH
......
......@@ -98,23 +98,23 @@ let rec toom22_mul (r x y scratch: ptr limb) (sx sy:int32) (ghost k: int) : unit
if (Int32.(=) s n)
then
if begin ensures { result <-> value x0 n < value x1 n }
Int32.(<) (compare_same_size x0 x1 n) 0
Int32.(<) (wmpn_cmp x0 x1 n) 0
end
then begin
let ghost b = sub_limbs xsm1 x1 x0 n in
let ghost b = wmpn_sub_n xsm1 x1 x0 n in
no_borrow_ptr x1 x0 xsm1 (p2i n) (p2i n) b;
vm1_neg := true end
else let ghost b = sub_limbs xsm1 x0 x1 n in
else let ghost b = wmpn_sub_n xsm1 x0 x1 n in
no_borrow_ptr x0 x1 xsm1 (p2i n) (p2i n) b
else
(* n-s=1*)
if (Limb.(=) (get_ofs x0 s) 0) &&
(Int32.(<) (compare_same_size x0 x1 s) 0)
(Int32.(<) (wmpn_cmp x0 x1 s) 0)
then begin
assert { value x0 s < value x1 s };
value_tail x0 s;
assert { value x0 n = value x0 s };
let ghost b = sub_limbs xsm1 x1 x0 s in
let ghost b = wmpn_sub_n xsm1 x1 x0 s in
no_borrow_ptr x1 x0 xsm1 (p2i s) (p2i s) b;
value_sub_shift_no_change (pelts xsm1) (xsm1.offset) (p2i s) (p2i s) 0;
set_ofs xsm1 s 0;
......@@ -122,7 +122,7 @@ let rec toom22_mul (r x y scratch: ptr limb) (sx sy:int32) (ghost k: int) : unit
value_tail xsm1 s
end
else begin
let b = sub_limbs xsm1 x0 x1 s in
let b = wmpn_sub_n xsm1 x0 x1 s in
label Borrow in
value_sub_shift_no_change (pelts xsm1) (xsm1.offset) (p2i s) (p2i s) b;
let lx = get_ofs x0 s in
......@@ -142,32 +142,32 @@ let rec toom22_mul (r x y scratch: ptr limb) (sx sy:int32) (ghost k: int) : unit
if (Int32.(=) t n)
then
if begin ensures { result <-> value y0 n < value y1 n }
Int32.(<) (compare_same_size y0 y1 n) 0
Int32.(<) (wmpn_cmp y0 y1 n) 0
end
then begin
let ghost b = sub_limbs ysm1 y1 y0 n in
let ghost b = wmpn_sub_n ysm1 y1 y0 n in
no_borrow_ptr y1 y0 ysm1 (p2i n) (p2i n) b;
vm1_neg := not !vm1_neg end
else
let ghost b = sub_limbs ysm1 y0 y1 n in
let ghost b = wmpn_sub_n ysm1 y0 y1 n in
no_borrow_ptr y0 y1 ysm1 (p2i n) (p2i n) b;
else
let y0t = C.incr y0 t in
let c0 = (Int32.(=) (is_zero y0t (Int32.(-) n t)) 1) in
let c1 = (Int32.(<) (compare_same_size y0 y1 t) 0) in
let c0 = (Int32.(=) (wmpn_zero_p y0t (Int32.(-) n t)) 1) in
let c1 = (Int32.(<) (wmpn_cmp y0 y1 t) 0) in
if c0 && c1
then begin
assert { value y0 t < value y1 t };
value_concat y0 t n;
assert { value y0 n = value y0 t };
let ghost b = sub_limbs ysm1 y1 y0 t in
let ghost b = wmpn_sub_n ysm1 y1 y0 t in
no_borrow_ptr y1 y0 ysm1 (p2i t) (p2i t) b;
assert { forall j. (j < offset r \/ offset r + sx + sy <= j)
-> (pelts r)[j] = (pelts r)[j] at BSM1 };
label Zero in
let ghost ysm1z = { ysm1 } in
let ysm1t = C.incr ysm1 t in
zero ysm1t (Int32.(-) n t);
wmpn_zero ysm1t (Int32.(-) n t);
value_sub_frame_shift (pelts ysm1) (pelts ysm1z)
(offset ysm1) (offset ysm1z) (p2i t);
assert { value ysm1 t = value ysm1 t at Zero };
......@@ -187,7 +187,7 @@ let rec toom22_mul (r x y scratch: ptr limb) (sx sy:int32) (ghost k: int) : unit
\/ (not c1
so value y1 t <= value y0 t
so value y0 t <= value y0 n) };
let ghost b = sub ysm1 y0 y1 n t in
let ghost b = wmpn_sub ysm1 y0 y1 n t in
no_borrow_ptr y0 y1 ysm1 (p2i n) (p2i t) b;
end
end;
......@@ -245,16 +245,16 @@ let rec toom22_mul (r x y scratch: ptr limb) (sx sy:int32) (ghost k: int) : unit
let ghost hvinf = value vinfn (int32'int s + int32'int t- int32'int n) in
assert { lv0 + m * hv0 = a0 * b0 };