Commit 3414daf7 authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft

Some headway in division launcher proof

parent df181567
......@@ -4,7 +4,7 @@ why3:
extract:
why3 extract -D c -o build mp2.mlw -T N
tests: extract
gcc -O3 -Wall -g -std=gnu99 tests.c build/mp2.mlw__N.c -lgmp -o tests
gcc -O1 -Wall -g -std=gnu99 tests.c build/mp2.mlw__N.c -lgmp -o tests
benchwhy3: extract
gcc -O3 -Wall -g -std=gnu99 -DTEST_WHY3 tests.c build/mp2.mlw__N.c -lgmp -o why3bench
benchgmp: extract
......
......@@ -1570,6 +1570,27 @@ module N
(r,d)
end
let clz_ext (x:limb) : int32
requires { x > 0 }
ensures { power 2 result * x < radix }
ensures { 2 * power 2 result * x >= radix }
ensures { 0 <= result < Limb.length }
ensures { power 2 result * x <= radix - power 2 result }
=
let r = count_leading_zeros x in
let ghost p = power 2 (p2i r) in
let ghost q = power 2 (Limb.length - p2i r) in
assert { p * x <= radix - p
by
p * q = radix
so mod radix p = mod (q * p) p = 0
so mod (p * x) p = 0
so p * x < radix
so mod (radix - p) p = mod (p * (-1) + radix) p
= mod radix p = 0
};
r
(** [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]. *)
......@@ -5372,6 +5393,9 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
let limb_zero = Limb.of_int 0 in
let zero = Int32.of_int 0 in
let two = Int32.of_int 2 in
value_sub_tail (pelts y) y.offset (y.offset + p2i sy - 1);
value_sub_lower_bound (pelts y) y.offset (y.offset + p2i sy - 1);
assert { value_sub_shift y sy >= power radix (sy - 1) };
if (Int32.(=) sy one)
then
let lr = divmod_1 q x (C.get y) sx in
......@@ -5379,32 +5403,145 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
else
if (Int32.(=) sy two)
then
let clz = count_leading_zeros (C.get_ofs y (Int32.(-) sy one)) in
let clz = clz_ext (C.get_ofs y (Int32.(-) sy one)) in
let ghost p = power 2 (p2i clz) in
if Int32.(=) clz zero
then begin
copy nx x sx;
(*value_sub_frame_shift (pelts x) (pelts nx) x.offset nx.offset (p2i 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 _ = divmod_2 q nx y (Int32.(+) sx one) in
let _qh = divmod_2 q nx y (Int32.(+) sx one) in
copy r nx sy;
assert { value_sub_shift x sx
= value_sub_shift q (sx - sy + 1) * value_sub_shift y sy
+ value_sub_shift r sy
by value_sub_shift r sy = value_sub_shift nx sy
by value_sub_shift r sy = value_sub_shift nx sy
so value_sub_shift (nx at Div2_ns) (sx + 1) < power radix sx
so value_sub_shift (nx at Div2_ns) (sx + 1)
= value_sub_shift (nx at Div2_ns) sx
so (_qh = 0
by
power radix sx
> value_sub_shift (nx at Div2_ns) (sx + 1)
= (value_sub_shift q (sx - 1) + power radix (sx - 1) * _qh)
* value_sub_shift y 2
+ value_sub_shift nx 2
so value_sub_shift nx 2 >= 0
so value_sub_shift y 2 >= radix
so value_sub_shift q (sx - 1) >= 0
so _qh >= 0
so (value_sub_shift q (sx - 1) + power radix (sx - 1) * _qh)
* value_sub_shift y 2
+ value_sub_shift nx 2
>= (value_sub_shift q (sx - 1)
+ power radix (sx - 1) * _qh)
* value_sub_shift y 2
>= (value_sub_shift q (sx - 1)
+ power radix (sx - 1) * _qh)
* radix
>= power radix (sx - 1) * _qh * radix
= power radix sx * _qh
so power radix sx > power radix sx * _qh
)
so value_sub_shift x sx = value_sub_shift (nx at Div2_ns) sx
};
()
end
else begin
let _c = lshift ny y sy (Limb.of_int32 clz) in
let _c = lshift ny y sy (Limb.of_int32 clz) in
begin ensures { normalized ny sy }
let ghost dh = (pelts y)[y.offset + p2i sy - 1] in
assert { value_sub_shift y sy
= value_sub_shift y (sy - 1) + power radix (sy - 1) * dh };
value_sub_upper_bound (pelts y) y.offset (y.offset + p2i sy - 1);
value_sub_tail (pelts ny) ny.offset (ny.offset + p2i sy - 1);
value_sub_upper_bound (pelts ny) ny.offset (ny.offset + p2i sy - 1);
let ghost ndh = (pelts ny)[ny.offset + p2i sy - 1] in
assert { normalized ny sy
by
value_sub_shift y sy < (dh + 1) * power radix (sy - 1)
so value_sub_shift ny sy + (power radix sy) * _c
= power 2 clz * value_sub_shift y sy
= power 2 clz
* (value_sub_shift y (sy - 1)
+ dh * power radix (sy - 1))
so power 2 clz * dh <= radix - power 2 clz
so value_sub_shift ny sy + (power radix sy) * _c
= power 2 clz * value_sub_shift y (sy - 1)
+ power 2 clz * dh * power radix (sy - 1)
< power 2 clz * power radix (sy - 1)
+ power 2 clz * dh * power radix (sy - 1)
<= power 2 clz * power radix (sy - 1)
+ (radix - power 2 clz) * power radix (sy - 1)
= radix * power radix (sy - 1)
= power radix sy
so _c = 0
so value_sub_shift ny sy
= power 2 clz * value_sub_shift y sy
so value_sub_shift y sy >= dh * power radix (sy - 1)
so value_sub_shift ny sy
>= power 2 clz * dh * power radix (sy - 1)
so value_sub_shift ny sy =
value_sub_shift ny (sy - 1) + power radix (sy - 1) * ndh
< power radix (sy - 1) + power radix (sy - 1) * ndh
= power radix (sy - 1) * (ndh + 1)
so power radix (sy - 1) * (ndh + 1)
> power radix (sy - 1) * (power 2 clz * dh)
so ndh + 1 > power 2 clz * dh
so ndh >= power 2 clz * dh
so 2 * power 2 clz * dh >= radix
so 2 * ndh >= radix
so ndh >= div radix 2
};
end;
let h = lshift nx x sx (Limb.of_int32 clz) in
C.set_ofs nx sx h;
label Div2_s in
(* TODO don't add 1 when not needed, cf "adjust" in GMP algo *)
let _ = divmod_2 q nx ny (Int32.(+) sx one) in
let _qh = divmod_2 q nx ny (Int32.(+) sx one) in
let _ = rshift r nx sy (Limb.of_int32 clz) in
assert { value_sub_shift x sx
= value_sub_shift q (sx - sy + 1) * value_sub_shift y sy
+ value_sub_shift r sy
by
value_sub_shift (nx at Div2_s) (sx + 1)
= (value_sub_shift q (sx - 1) + power radix (sx - 1) * _qh)
* value_sub_shift ny 2
+ value_sub_shift nx 2
so value_sub_shift (nx at Div2_s) (sx + 1)
= p * value_sub_shift x sx
so value_sub_shift ny 2 = p * value_sub_shift y 2
so (_qh = 0
by
value_sub_shift x sx < power radix sx
so value_sub_shift y 2 >= radix
so value_sub_shift ny 2 >= p * radix
so value_sub_shift q (sx - 1) >= 0
so value_sub_shift nx 2 >= 0
so (value_sub_shift q (sx - 1) + power radix (sx - 1) * _qh)
* value_sub_shift ny 2
+ value_sub_shift nx 2
>= (value_sub_shift q (sx - 1)
+ power radix (sx - 1) * _qh)
* value_sub_shift ny 2
>= (value_sub_shift q (sx - 1)
+ power radix (sx - 1) * _qh)
* p * radix
>= power radix (sx - 1) * _qh * p * radix
= power radix sx * p * _qh
so power radix sx * p
> value_sub_shift (nx at Div2_s) (sx + 1)
>= power radix sx * p * _qh
)
so value_sub_shift nx 2 = p * value_sub_shift r 2
so p * value_sub_shift x sx
= value_sub_shift q (sx - 1) * p * value_sub_shift y 2
+ p * value_sub_shift r 2
= p * (value_sub_shift q (sx - 1) * value_sub_shift y 2
+ value_sub_shift r 2)
};
()
end
else
......
......@@ -258,8 +258,8 @@ module UInt32
val count_leading_zeros (x:uint32) : int32
requires { to_int x > 0 }
ensures { (power 2 (Int32.to_int result)) * to_int x <= max_uint32 }
ensures { 2 * (power 2 (Int32.to_int result)) * to_int x > max_uint32 }
ensures { (power 2 (Int32.to_int result)) * to_int x < max_uint32 }
ensures { 2 * (power 2 (Int32.to_int result)) * to_int x >= max_uint32 }
ensures { 0 <= Int32.to_int result < 32 }
val of_int32(x:int32) : uint32
......@@ -420,8 +420,8 @@ module UInt64
val count_leading_zeros (x:uint64) : int32
requires { to_int x > 0 }
ensures { (power 2 (Int32.to_int result)) * to_int x <= max_uint64 }
ensures { 2 * (power 2 (Int32.to_int result)) * to_int x > max_uint64 }
ensures { (power 2 (Int32.to_int result)) * to_int x < max_uint64 }
ensures { 2 * (power 2 (Int32.to_int result)) * to_int x >= max_uint64 }
ensures { 0 <= Int32.to_int result < 64 }
val of_int32(x:int32) : uint64
......
......@@ -555,7 +555,7 @@ module Translate = struct
(*TODO check it's actually unused *)
then expr info env e
else if ity_equal pv.pv_ity ity_unit
|| pv.pv_vs.vs_name.id_string.[0] = '_'
|| pv.pv_vs.vs_name.id_string = "_"
then let env' = {env with computes_return_value = false} in
([], C.Sseq (C.Sblock(expr info env' le),
C.Sblock(expr info env e)))
......
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