From da2e2c53d83a4c00018e2ce8d37335c06503f130 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Tue, 29 Sep 2020 14:49:30 -0700
Subject: [PATCH] Add regression test for the primality testing constraint and
 finite field inverse computations.

---
 tests/regression/primes.cry         | 38 +++++++++++++++
 tests/regression/primes.icry        | 21 +++++++++
 tests/regression/primes.icry.stdout | 73 +++++++++++++++++++++++++++++
 3 files changed, 132 insertions(+)
 create mode 100644 tests/regression/primes.cry
 create mode 100644 tests/regression/primes.icry
 create mode 100644 tests/regression/primes.icry.stdout

diff --git a/tests/regression/primes.cry b/tests/regression/primes.cry
new file mode 100644
index 000000000..4c60ee527
--- /dev/null
+++ b/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}
diff --git a/tests/regression/primes.icry b/tests/regression/primes.icry
new file mode 100644
index 000000000..06c36c2cf
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/tests/regression/primes.icry.stdout b/tests/regression/primes.icry.stdout
new file mode 100644
index 000000000..9a2ed204a
--- /dev/null
+++ b/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.