Add regression test for the primality testing constraint

and finite field inverse computations.

tests/regression/primes.cry

@@ -0,0 +1,38 @@
+
+z1prime : {n} (prime n) => Z n
+z1prime = 1
+
+z1_2 = z1prime`{2}
+z1_3 = z1prime`{3}
+z1_17 = z1prime`{17}
+z1_2_17m1 = z1prime`{2^^17 - 1}
+
+
+type p192 = 6277101735386680763835789423207666416083908700390324961279
+type p224 = 26959946667150639794667015087019630673557916260026308143510066298881
+type p256 = 115792089210356248762697446949407573530086143415290314195533631308867097853951
+type p384 = 39402006196394479212279040100143613805079739270465446667948293404245721771496870329047266088258938001861606973112319
+type p521 = 6864797660130609714981900799081393217269435300143305409394463459185543183397656052122559640661454554977296311391480858037121987999716643812574028291115057151
+
+recip_correct : {p} (prime p) => Z p -> Bool
+recip_correct x = x == 0 \/ x * recip x == 1
+
+property recip_correct_17   = recip_correct`{17}
+property recip_correct_1021 = recip_correct`{1021}
+property recip_correct_p192 = recip_correct`{p192}
+property recip_correct_p224 = recip_correct`{p224}
+property recip_correct_p256 = recip_correct`{p256}
+property recip_correct_p384 = recip_correct`{p384}
+property recip_correct_p521 = recip_correct`{p521}
+
+moddiv_eq : {p} (prime p, p >= 3) => Z p -> Z p -> Bool
+moddiv_eq x y = y == 0 \/ (x /. y) * y == x
+
+property moddiv_eq17   = moddiv_eq`{17}
+property moddiv_eq1021 = moddiv_eq`{1021}
+
+property moddiv_eq_p192 = moddiv_eq`{p192}
+property moddiv_eq_p224 = moddiv_eq`{p224}
+property moddiv_eq_p256 = moddiv_eq`{p256}
+property moddiv_eq_p384 = moddiv_eq`{p384}
+property moddiv_eq_p521 = moddiv_eq`{p521}

tests/regression/primes.icry

@@ -0,0 +1,21 @@
+:l primes.cry
+:check
+
+z1_2
+z1_3
+z1_17
+z1_2_17m1
+
+z1prime`{8}
+z1prime`{p192*p521}
+
+:set prover=w4-z3
+:prove recip_correct_17
+:prove recip_correct_1021
+:prove recip_correct_p192
+:prove recip_correct_p224
+:prove recip_correct_p256
+:prove recip_correct_p384
+:prove recip_correct_p521
+
+:prove moddiv_eq17

tests/regression/primes.icry.stdout

@@ -0,0 +1,73 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+property recip_correct_17 Using exhaustive testing.
+Testing... Passed 17 tests.
+Q.E.D.
+property recip_correct_1021 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 9.33% (95 of 1021 values)
+property recip_correct_p192 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.00% (100 of 2^^192 values)
+property recip_correct_p224 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.00% (100 of 2^^224 values)
+property recip_correct_p256 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.00% (100 of 2^^256 values)
+property recip_correct_p384 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.00% (100 of 2^^384 values)
+property recip_correct_p521 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.00% (100 of 2^^521 values)
+property moddiv_eq17 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 29.29% (85 of 289 values)
+property moddiv_eq1021 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.01% (100 of 1042441 values)
+property moddiv_eq_p192 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.00% (100 of 2^^384 values)
+property moddiv_eq_p224 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.00% (100 of 2^^448 values)
+property moddiv_eq_p256 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.00% (100 of 2^^512 values)
+property moddiv_eq_p384 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.00% (100 of 2^^768 values)
+property moddiv_eq_p521 Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.00% (100 of 2^^1042 values)
+1
+1
+1
+1
+
+[error] at <interactive>:1:1--1:8:
+  Unsolvable constraints:
+    • prime 8
+        arising from
+        use of expression z1prime
+        at <interactive>:1:1--1:8
+    • Reason: 8 is not a prime number
+
+[error] at <interactive>:1:1--1:8:
+  Unsolvable constraints:
+    • prime 43091033305484275771318189120554014028061750499173210735564075069516863836988716943216254409932734872431737796205873180054667648466751626159946491190398490019830895369540999907009814461968819338016648922197947056129
+        arising from
+        use of expression z1prime
+        at <interactive>:1:1--1:8
+    • Reason: 43091033305484275771318189120554014028061750499173210735564075069516863836988716943216254409932734872431737796205873180054667648466751626159946491190398490019830895369540999907009814461968819338016648922197947056129 is not a prime number
+Q.E.D.
+Q.E.D.
+Q.E.D.
+Q.E.D.
+Q.E.D.
+Q.E.D.
+Q.E.D.
+Q.E.D.