Merge pull request #880 from GaloisInc/fast-f2

submodule updates for the `fast-f2` cryptol branch
GaloisInc · Oct 28, 2020 · 9d85f06 · 9d85f06
2 parents d12eb10 + 7f57175
commit 9d85f06
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 2 deletions.
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/deps/saw-core b/deps/saw-core
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
+1 −1		.github/ci.sh
+1 −1		cryptol-remote-api/src/CryptolServer/Data/Expression.hs
+4 −3		cryptol.cabal
+3 −33		lib/Cryptol.cry
+46 −0		lib/Cryptol/Reference.cry
+6 −6		src/Cryptol/Eval.hs
+28 −0		src/Cryptol/Eval/Concrete.hs
+1 −1		src/Cryptol/Eval/Value.hs
+48 −0		src/Cryptol/F2.hs
+1 −1		src/Cryptol/ModuleSystem.hs
+17 −15		src/Cryptol/ModuleSystem/Base.hs
+4 −0		src/Cryptol/Prelude.hs
+27 −20		src/Cryptol/Symbolic/SBV.hs
+17 −4		src/Cryptol/Symbolic/What4.hs
+4 −0		src/Cryptol/Utils/Ident.hs
+8 −8		tests/issues/T146.icry.stdout
+3 −3		tests/issues/T820.icry.stdout
+2 −2		tests/issues/issue290v2.icry.stdout
+2 −2		tests/issues/issue723.icry.stdout
+6 −6		tests/issues/issue910.icry.stdout
+33 −0		tests/regression/f2polytest.cry
+6 −0		tests/regression/f2polytest.icry
+94 −0		tests/regression/f2polytest.icry.stdout
+86 −86		tests/regression/instance.icry.stdout
+11 −11		tests/regression/tc-errors.icry.stdout
+10 −5		cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+27 −10		cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
+2 −2		saw-core/tests/src/Tests/Rewriter.hs