1module Number.F2m (tests) where
2
3import Imports hiding ((.&.))
4import Data.Bits
5import Data.Maybe
6import Crypto.Number.Basic (log2)
7import Crypto.Number.F2m
8
9addTests = testGroup "addF2m"
10    [ testProperty "commutative"
11        $ \a b -> a `addF2m` b == b `addF2m` a
12    , testProperty "associative"
13        $ \a b c -> (a `addF2m` b) `addF2m` c == a `addF2m` (b `addF2m` c)
14    , testProperty "0 is neutral"
15        $ \a -> a `addF2m` 0 == a
16    , testProperty "nullable"
17        $ \a -> a `addF2m` a == 0
18    , testProperty "works per bit"
19        $ \a b -> (a `addF2m` b) .&. b == (a .&. b) `addF2m` b
20    ]
21
22modTests = testGroup "modF2m"
23    [ testProperty "idempotent"
24        $ \(Positive m) (NonNegative a) -> modF2m m a == modF2m m (modF2m m a)
25    , testProperty "upper bound"
26        $ \(Positive m) (NonNegative a) -> modF2m m a < 2 ^ log2 m
27    , testProperty "reach upper"
28        $ \(Positive m) -> let a = 2 ^ log2 m - 1 in modF2m m (m `addF2m` a) == a
29    , testProperty "lower bound"
30        $ \(Positive m) (NonNegative a) -> modF2m m a >= 0
31    , testProperty "reach lower"
32        $ \(Positive m) -> modF2m m m == 0
33    , testProperty "additive"
34        $ \(Positive m) (NonNegative a) (NonNegative b)
35            -> modF2m m a `addF2m` modF2m m b == modF2m m (a `addF2m` b)
36    ]
37
38mulTests = testGroup "mulF2m"
39    [ testProperty "commutative"
40        $ \(Positive m) (NonNegative a) (NonNegative b) -> mulF2m m a b == mulF2m m b a
41    , testProperty "associative"
42        $ \(Positive m) (NonNegative a) (NonNegative b) (NonNegative c)
43            -> mulF2m m (mulF2m m a b) c == mulF2m m a (mulF2m m b c)
44    , testProperty "1 is neutral"
45        $ \(Positive m) (NonNegative a) -> mulF2m m a 1 == modF2m m a
46    , testProperty "0 is annihilator"
47        $ \(Positive m) (NonNegative a) -> mulF2m m a 0 == 0
48    , testProperty "distributive"
49        $ \(Positive m) (NonNegative a) (NonNegative b) (NonNegative c)
50            -> mulF2m m a (b `addF2m` c) == mulF2m m a b `addF2m` mulF2m m a c
51    ]
52
53squareTests = testGroup "squareF2m"
54    [ testProperty "sqr(a) == a * a"
55        $ \(Positive m) (NonNegative a) -> mulF2m m a a == squareF2m m a
56    -- disabled because we require @m@ to be a suitable modulus and there is no
57    -- way to guarantee this
58    -- , testProperty "sqrt(a) * sqrt(a) = a"
59    --     $ \(Positive m) (NonNegative aa) -> let a = sqrtF2m m aa in mulF2m m a a == modF2m m aa
60    , testProperty "sqrt(a) * sqrt(a) = a in GF(2^16)"
61        $ let m = 65581 :: Integer -- x^16 + x^5 + x^3 + x^2 + 1
62              nums = [0 .. 65535 :: Integer]
63          in  nums == [let y = sqrtF2m m x in squareF2m m y | x <- nums]
64    ]
65
66powTests = testGroup "powF2m"
67    [ testProperty "2 is square"
68        $ \(Positive m) (NonNegative a) -> powF2m m a 2 == squareF2m m a
69    , testProperty "1 is identity"
70        $ \(Positive m) (NonNegative a) -> powF2m m a 1 == modF2m m a
71    , testProperty "0 is annihilator"
72        $ \(Positive m) (NonNegative a) -> powF2m m a 0 == modF2m m 1
73    , testProperty "(a * b) ^ c == (a ^ c) * (b ^ c)"
74        $ \(Positive m) (NonNegative a) (NonNegative b) (NonNegative c)
75            -> powF2m m (mulF2m m a b) c == mulF2m m (powF2m m a c) (powF2m m b c)
76    , testProperty "a ^ (b + c) == (a ^ b) * (a ^ c)"
77        $ \(Positive m) (NonNegative a) (NonNegative b) (NonNegative c)
78            -> powF2m m a (b + c) == mulF2m m (powF2m m a b) (powF2m m a c)
79    , testProperty "a ^ (b * c) == (a ^ b) ^ c"
80        $ \(Positive m) (NonNegative a) (NonNegative b) (NonNegative c)
81            -> powF2m m a (b * c) == powF2m m (powF2m m a b) c
82    ]
83
84invTests = testGroup "invF2m"
85    [ testProperty "1 / a * a == 1"
86        $ \(Positive m) (NonNegative a)
87            -> maybe True (\c -> mulF2m m c a == modF2m m 1) (invF2m m a)
88    , testProperty "1 / a == a (mod a^2-1)"
89        $ \(NonNegative a) -> a < 2 || invF2m (squareF2m' a `addF2m` 1) a == Just a
90    ]
91
92divTests = testGroup "divF2m"
93    [ testProperty "1 / a == inv a"
94        $ \(Positive m) (NonNegative a) -> divF2m m 1 a == invF2m m a
95    , testProperty "a / b == a * inv b"
96        $ \(Positive m) (NonNegative a) (NonNegative b)
97            -> divF2m m a b == (mulF2m m a <$> invF2m m b)
98    , testProperty "a * b / b == a"
99        $ \(Positive m) (NonNegative a) (NonNegative b)
100            -> isNothing (invF2m m b) || divF2m m (mulF2m m a b) b == Just (modF2m m a)
101    ]
102
103tests = testGroup "number.F2m"
104    [ addTests
105    , modTests
106    , mulTests
107    , squareTests
108    , powTests
109    , invTests
110    , divTests
111    ]
112