Merge pull request #2012 from GaloisInc/bump-cryptol-specs

Bump cryptol specs
GaloisInc · Jan 30, 2024 · 03f9285 · 03f9285
2 parents adce60e + 5632ce5
commit 03f9285
Show file tree

Hide file tree

Showing 7 changed files with 23 additions and 12 deletions.
diff --git a/deps/cryptol-specs b/deps/cryptol-specs
diff --git a/examples/aes/aes.saw b/examples/aes/aes.saw
@@ -1,3 +1,4 @@
+import "../../deps/cryptol-specs/Common/GF28.cry";
 import "../../deps/cryptol-specs/Primitive/Symmetric/Cipher/Block/AES.cry";
 
 print "Proving encrypt_lemma...";

diff --git a/intTests/test0001/javamd5test.saw b/intTests/test0001/javamd5test.saw
@@ -1,4 +1,4 @@
-import "../../deps/cryptol-specs/Primitive/Keyless/Hash/MD5.cry";
+import "../../deps/cryptol-specs/Primitive/Keyless/Hash/MD5.md";
 
 let md5_spec = do {
     msgref <- jvm_alloc_array 16 java_byte;
@@ -35,17 +35,27 @@ tf <- lemma "(x : Vec 32 Bool) -> EqTrue (bvEq 32 (bvOr 32 (bvShl 32 x 23) (bvSh
 r1 <- lemma "(x : Vec 8 Bool) -> EqTrue (bvEq 32 (bvAnd 32 (bvNat 32 255) (bvSExt 24 7 x)) (bvUExt 24 8 x))";
 r2 <- lemma "(a b c d : Vec 8 Bool) -> EqTrue (bvEq 32 (bvOr 32 (bvOr 32 (bvOr 32 (bvUExt 24 8 a) (bvShl 32 (bvUExt 24 8 b) 8)) (bvShl 32 (bvUExt 24 8 c) 16)) (bvShl 32 (bvUExt 24 8 d) 24)) (append 24 8 Bool (append 16 8 Bool (append 8 8 Bool d c) b) a))";
 
-// FIXME: This rewrite rule (as well as the unfolding of "md5" and
-// "pad" in the proof script below) are a workaround for saw-script
-// issue #1010. When that is fixed, we should get rid of them.
-r3 <- lemma "EqTrue (bvEq 1 [True] (bvNat 1 1))";
+// FIXME: This rewrite rule (as well as the use of the `unfolding` tactic in the
+// proof script below) are a workaround for saw-script issue #1010. When that is
+// fixed, we should get rid of them. Note that `[1]` (used in the `pad`
+// function) in SAWScript is translated to `ecNumber (TCNum 1) Bool PLiteralBit`
+// in SAWCore, which is why the latter is mentioned in this rewrite rule.
+r3 <- lemma "EqTrue (bvEq 1 [ecNumber (TCNum 1) Bool PLiteralBit] (bvNat 1 1))";
 
-let ss = addsimps [t0,t1,t2,t3,t4,t5,t6,t7,t8,t9,ta,tb,tc,td,te,tf,r1,r2,r3] empty_ss;
+// The `convert` function has nested uses of `groupBy` and `join`, which seems
+// give SAW difficulty in reasoning about it. We rewrite `convert` to eliminate
+// some of these nested `groupBy`s and `join`s.
+r4 <- prove_print w4 {{ \(x : [16][32]) -> groupBy`{32} (convert (join x)) == map (\y -> join (reverse (groupBy`{8} y))) x }};
+
+let ss = addsimps [t0,t1,t2,t3,t4,t5,t6,t7,t8,t9,ta,tb,tc,td,te,tf,r1,r2,r3,r4] empty_ss;
 
 c <- java_load_class "JavaMD5";
 jvm_verify c "computeMD5" [] false md5_spec
   do {
-    unfolding ["md5", "pad"];
+    // We unfold everything needed to expose the definition of `pad` (which is
+    // referenced in `r3`) and the call to `convert` in `processMsg` (which is
+    // referenced in `r4`).
+    unfolding ["md5", "prepMsg", "processMsg", "pad"];
     simplify ss;
     goal_eval;
     w4;

diff --git a/intTests/test0002/test.saw b/intTests/test0002/test.saw
@@ -1,4 +1,4 @@
-import "../../deps/cryptol-specs/Primitive/Keyless/Hash/MD5.cry";
+import "../../deps/cryptol-specs/Primitive/Keyless/Hash/MD5.md";
 
 let main = do {
    java_md5 <- read_aig "../support/JavaMD5.aig";

diff --git a/intTests/test0006/test.saw b/intTests/test0006/test.saw
@@ -1,4 +1,4 @@
-import "../../deps/cryptol-specs/Primitive/Keyless/Hash/MD5.cry";
+import "../../deps/cryptol-specs/Primitive/Keyless/Hash/MD5.md";
 
 let main = do {
    print "ref type";

diff --git a/intTests/test0006_w4/test.saw b/intTests/test0006_w4/test.saw
@@ -1,4 +1,4 @@
-import "../../deps/cryptol-specs/Primitive/Keyless/Hash/MD5.cry";
+import "../../deps/cryptol-specs/Primitive/Keyless/Hash/MD5.md";
 
 let main = do {
    print "ref type";

diff --git a/intTests/test_ffi_verify_salsa/salsa.cry b/intTests/test_ffi_verify_salsa/salsa.cry
@@ -1,4 +1,4 @@
 import Primitive::Symmetric::Cipher::Stream::Salsa20 (Salsa20_encrypt)
 
 foreign cipher : {a, w} (a >= 1, 2 >= a, w <= 2^^70) => [16*a][8] -> [8][8] -> [w][8] -> [w][8]
-cipher key nonce inbuf = Salsa20_encrypt (key, nonce, inbuf)
+cipher = Salsa20_encrypt