Add a basic integration test that excercises the polynomial

arithmetic primitives and the `rme` proof method.
GaloisInc · Oct 28, 2020 · 7f57175 · 7f57175
1 parent da4dee8
commit 7f57175
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/intTests/test0063_polyarith/test.saw b/intTests/test0063_polyarith/test.saw
@@ -0,0 +1,13 @@
+let {{
+
+thm : {n,m} (fin n, fin m, n > m, m >= 1) => [n] -> [m] -> Bit
+thm x y = y != 0 ==> 
+    pmult y (pdiv x y) ^ (zero # pmod x y) == zero`{[m-1]}#x
+
+}};
+
+print_term (rewrite (cryptol_ss ())
+  (unfold_term ["thm"] {{ thm`{16,4} }}));
+
+prove_print rme {{ thm`{16,8} }};
+prove_print rme {{ thm`{20,10} }};
diff --git a/intTests/test0063_polyarith/test.sh b/intTests/test0063_polyarith/test.sh
@@ -0,0 +1 @@
+$SAW test.saw