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

Toom32

parent 24a6ca4b
......@@ -470,6 +470,8 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt);
syntax val count_leading_zeros "__builtin_clzll(%1)"
syntax val of_int32 "(uint64_t)%1"
syntax val to_int64 "(int64_t)%1"
syntax val of_int64 "(uint64_t)%1"
end
......
......@@ -26,11 +26,11 @@ cfiles: why3 dir
extract: why3 dir cfiles
CFILES = build/uint64gmp.c build/div.c build/logical.c build/mul.c build/sub.c build/add.c build/compare.c build/util.c build/int32.c
CFILES = build/uint64gmp.c build/toom.c build/div.c build/logical.c build/mul.c build/sub.c build/add.c build/compare.c build/util.c build/int32.c
tests: extract check-gmp
gcc -O2 -Wall -Wno-unused-function -g -std=gnu99 tests.c $(CFILES) -I$(GMP_DIR) -Irandom -L$(GMP_LIB) -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -lgmp -o build/tests
gcc -O2 -Wall -Wno-unused-function -g -std=gnu99 -DCOMPARE_MINI tests.c $(CFILES) -I$(GMP_DIR) -Irandom -Imini-gmp -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -o build/minitests
gcc -O2 -Wall -Wno-unused-function -g -std=c11 -pedantic tests.c $(CFILES) -I$(GMP_DIR) -Irandom -L$(GMP_LIB) -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -lgmp -o build/tests
gcc -O2 -Wall -Wno-unused-function -g -std=c11 -pedantic -DCOMPARE_MINI tests.c $(CFILES) -I$(GMP_DIR) -Irandom -Imini-gmp -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -o build/minitests
./build/tests
./build/minitests
......
......@@ -38,7 +38,6 @@ module Add
invariant { forall j. (j < offset r \/ offset r + sz <= j)
-> (pelts r)[j] = old (pelts r)[j] }
variant { sz - !i }
label StartLoop in
lx := get_ofs x !i;
let (res, carry) = add_with_carry !lx !c limb_zero in
set_ofs r !i res;
......@@ -429,4 +428,55 @@ 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)
let wmpn_add_1_in_place (x:t) (y:limb) (sz:int32) : limb
requires { valid x sz }
requires { sz > 0 }
ensures { value x sz + (power radix sz) * result = value (old x) sz + y }
ensures { 0 <= result <= 1 }
ensures { forall j. (j < offset x \/ offset x + sz <= j)
-> (pelts x)[j] = old (pelts x)[j] }
writes { x.data.elts }
= let ghost ox = { x } in
let c = ref y in
let lx = ref 0 in
let i = ref 0 in
while Int32.(<) !i sz && not (Limb.(=) !c 0) do
invariant { 0 <= !i <= sz }
invariant { !i > 0 -> 0 <= !c <= 1 }
invariant { value x !i + (power radix !i) * !c =
value ox !i + y }
invariant { forall j. (j < offset x \/ offset x + !i <= j)
-> (pelts x)[j] = old (pelts x)[j] }
variant { sz - !i }
label StartLoop in
lx := get_ofs x !i;
assert { !lx = (pelts ox)[offset ox + !i] };
let (res, carry) = add_with_carry !lx !c 0 in
assert { res + radix * carry = !lx + !c }; (* TODO remove this *)
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
(x.offset + p2i sz) res;
set_ofs x !i res;
assert { forall j. !i < j < sz ->
(pelts x)[x.offset + j]
= (pelts ox)[x.offset + j] };
assert { value x !i = value x !i at StartLoop };
assert { value x !i + (power radix !i) * !c = value ox !i + y };
c := carry;
value_tail x !i;
value_tail ox !i;
assert { value x (!i+1) + (power radix (!i+1)) * !c
= value ox (!i+1) + y };
i := Int32.(+) !i 1;
done;
value_concat x !i sz;
value_concat ox !i sz;
assert { forall j. x.offset + !i <= j < x.offset + sz ->
(pelts x)[j] = (pelts ox)[j]
by let k = j - x.offset in
!i <= k < sz
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);
!c
end
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -99,7 +99,7 @@ module Lemmas
ensures {
value_sub x n (m+1) =
value_sub x n m + (Map.get x m) * power radix (m-n) }
= [@vc:sp] if n < m then value_sub_tail x (n+1) m else ()(*assert { 1+2=3 }*)
= [@vc:sp] 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}
......
This diff is collapsed.
......@@ -430,4 +430,56 @@ module Sub
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)
let wmpn_sub_1_in_place (x:t) (y:limb) (sz:int32) : limb
requires { valid x sz }
requires { sz > 0 }
ensures { value x sz - (power radix sz) * result = value (old x) sz - y }
ensures { 0 <= result <= 1 }
ensures { forall j. (j < offset x \/ offset x + sz <= j)
-> (pelts x)[j] = old (pelts x)[j] }
writes { x.data.elts }
= let ghost ox = { x } in
let b = ref y in
let lx = ref 0 in
let i = ref 0 in
while Int32.(<) !i sz && not (Limb.(=) !b 0) do
invariant { 0 <= !i <= sz }
invariant { !i > 0 -> 0 <= !b <= 1 }
invariant { value x !i - (power radix !i) * !b =
value ox !i - y }
invariant { forall j. (j < offset x \/ offset x + !i <= j)
-> (pelts x)[j] = old (pelts x)[j] }
variant { sz - !i }
label StartLoop in
lx := get_ofs x !i;
assert { !lx = (pelts ox)[offset ox + !i] };
let (res, borrow) = sub_with_borrow !lx !b 0 in
assert { res - radix * borrow = !lx - !b }; (* TODO remove this *)
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
(x.offset + p2i sz) res;
set_ofs x !i res;
assert { forall j. !i < j < sz ->
(pelts x)[x.offset + j]
= (pelts ox)[x.offset + j] };
assert { value x !i = value x !i at StartLoop };
assert { value x !i - (power radix !i) * !b = value ox !i - y };
b := borrow;
value_tail x !i;
value_tail ox !i;
assert { value x (!i+1) - (power radix (!i+1)) * !b
= value ox (!i+1) - y };
i := Int32.(+) !i 1;
done;
value_concat x !i sz;
value_concat ox !i sz;
assert { forall j. x.offset + !i <= j < x.offset + sz ->
(pelts x)[j] = (pelts ox)[j]
by let k = j - x.offset in
!i <= k < sz
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);
!b
end
This diff is collapsed.
This diff is collapsed.
......@@ -9,5 +9,6 @@ module Wmpn
use export logical.Logical
use export mul.Mul
use export div.Div
use export toom.Toom
end
\ No newline at end of file
......@@ -569,6 +569,7 @@ module UInt64GMP
use int.EuclideanDivision
use int.Power
use Int32
use Int64
use export UInt64Gen
clone export UnsignedGMP with
......@@ -622,4 +623,12 @@ module UInt64GMP
requires { Int32.to_int x >= 0 }
ensures { to_int result = Int32.to_int x }
val to_int64(x:uint64) : int64
requires { x <= max_int64 }
ensures { Int64.to_int result = x }
val of_int64(x:int64) : uint64
requires { 0 <= x }
ensures { to_int result = x }
end
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