mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-14 11:16:33 +03:00
51 lines
1.3 KiB
Plaintext
51 lines
1.3 KiB
Plaintext
module Karatsuba where
|
|
|
|
kmult : {limb,n} (fin n, fin limb, limb >= 6, n>=1) => [n] -> [n] -> [2*n]
|
|
kmult x y =
|
|
if `n <= (demote`{limb, max (width limb) (width n)}) then
|
|
(zero#x)*(zero#y)
|
|
else
|
|
take (splitmult`{limb} (make_atleast`{limb} x) (make_atleast`{limb} y))
|
|
|
|
make_atleast : {n, m, a} (fin n, fin m, Zero a) => [m]a -> [max n m]a
|
|
make_atleast x = zero#x
|
|
|
|
splitmult : {limb,n} (fin n, fin limb, limb >= 6, n>=6)
|
|
=> [n] -> [n] -> [2*n]
|
|
|
|
splitmult x y = (ac # bd) + (zero # ad_bc # (zero:[low]))
|
|
where
|
|
type hi = n/2
|
|
type low = n - hi
|
|
|
|
(a,b) = splitAt`{hi} x
|
|
(c,d) = splitAt`{hi} y
|
|
|
|
ac : [2*hi]
|
|
ac = kmult`{limb,hi} a c
|
|
|
|
bd : [2*low]
|
|
bd = kmult`{limb,low} b d
|
|
|
|
a_b = (zext a) + (zext b)
|
|
c_d = (zext c) + (zext d)
|
|
|
|
ad_bc : [2*(low+1)]
|
|
ad_bc = (kmult`{limb,low+1} a_b c_d) - (zext ac) - (zext bd)
|
|
|
|
|
|
property splitmult_correct_tiny (x:[9]) (y:[9]) =
|
|
zext x * zext y == splitmult`{limb=7} x y
|
|
|
|
property splitmult_correct_small (x:[11]) (y:[11]) =
|
|
zext x * zext y == splitmult`{limb=7} x y
|
|
|
|
property splitmult_correct_medium(x:[17]) (y:[17]) =
|
|
zext x * zext y == splitmult`{limb=7} x y
|
|
|
|
property splitmult_correct_large (x:[59]) (y:[59]) =
|
|
zext x * zext y == splitmult`{limb=7} x y
|
|
|
|
property splitmult_correct_huge (x:[511]) (y:[511]) =
|
|
zext x * zext y == splitmult`{limb=63} x y
|