Bump cryptol specs

[andreistefanescu]

Split from #2011, caused by timeout in intTests/test0001/javamd5test.saw.

[RyanGlScott]

Wow. The javamd5test.saw timeout is quite interesting. The following patch suffices to fix the timeout:

diff --git a/intTests/test0001/javamd5test.saw b/intTests/test0001/javamd5test.saw
index 5e49c0a7c..e218ac180 100644
--- a/intTests/test0001/javamd5test.saw
+++ b/intTests/test0001/javamd5test.saw
@@ -38,14 +38,15 @@ r2 <- lemma "(a b c d : Vec 8 Bool) -> EqTrue (bvEq 32 (bvOr 32 (bvOr 32 (bvOr 3
 // 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))";
+r3 <- lemma "EqTrue (bvEq 1 [ecNumber (TCNum 1) Bool PLiteralBit] (bvNat 1 1))";
+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] empty_ss;
+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"];
+    unfolding ["md5", "prepMsg", "processMsg", "pad"];
     simplify ss;
     goal_eval;
     w4;

An explanation as to why each change is necessary:

1. I needed to change the use of [True] to ecNumber (TCNum 1) Bool PLiteralBit in r3. This is because Literate Cryptol specifications cryptol-specs#67 changed a use of [True] to [1] in the Cryptol implementation of the pad function, and [1] desugars to ecNumber (TCNum 1) Bool PLiteralBit in SAWCore.

2. In addition, I needed to prove an additional r4 lemma that states a property about how the convert function interacts with groupBy and join. The convert function was introduced in Literate Cryptol specifications cryptol-specs#67, and it's roughly equivalent to the ntohl/htonl functions in the previous implementation of MD5.

   I'm not entirely sure why SAW has such a hard time with the new convert function, to be honest. As far as I can tell, the most important difference is that convert has nested applications of groupBy and join, which What4 seems to have a harder time reasoning about. The r4 lemma aims to eliminate as many nested uses of groupBy and join as possible.

3. I needed to unfold prepMsg in order to expose the use of [1] (as explained in change (1) above), and I needed to unfold processMsg in order to expose the use of convert (as explained in change (2) above).

[RyanGlScott]

Instead of declaring the r4 lemma (and unfolding processMsg), we could alternatively make the following change in cryptol-specs' MD5.md:

diff --git a/Primitive/Keyless/Hash/MD5.md b/Primitive/Keyless/Hash/MD5.md
index bed83d1..ec4f4b2 100644
--- a/Primitive/Keyless/Hash/MD5.md
+++ b/Primitive/Keyless/Hash/MD5.md
@@ -287,7 +287,7 @@ processMsg M = last abcd'
     where
         abcd0 = initialize
         abcd' = [ abcd0 ]
-              # [ rounds abcd (groupBy`{32} (convert (join X)))
+              # [ rounds abcd (map convert X)
                 | abcd <- abcd' | X <- M ]
 ```
 

[RyanGlScott]

Happily, the CI now passes after pushing the changes from #2012 (comment). It's unclear to me if modifying cryptol-specs upstream (as suggested in #2012 (comment)) would actually be a net positive, so I'll refrain from doing so.

Let's land this.