address comments

Signed-off-by: h2parson <h2parson@uwaterloo.ca>

Author: h2parson

proofs/cbmc/sha3_init/Makefile

@@ -24,7 +24,7 @@ USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--bitwuzla
+CBMCFLAGS=--smt2
 
 FUNCTION_NAME = sha3_init
 

sha3_api.c

@@ -5,6 +5,7 @@
 
 /* === FIPS 202: SHA-3 hash and SHAKE eXtensible Output Functions (XOF) */
 
+#include <string.h>
 #include "sha3_api.h"
 #include "cbmc.h"
 
@@ -13,18 +14,8 @@
 
 void sha3_init(sha3_var_t *c, size_t md_sz)
 {
-  size_t i;
-
-  for (i = 0; i < 25; i++)
-  __loop__(
-    assigns(i, object_whole(c->st.d))
-    invariant(i <= 25)
-    invariant(forall(j, 0, i, c->st.d[j] == 0))
-    decreases(25 - i)
-  )
-  {
-    c->st.d[i] = 0;
-  }
+  memset(c->st.d, 0, 25*sizeof(uint64_t));
+  
   c->md_sz = md_sz; /* in SHAKE; if 0, padding done */
   c->r_sz = 200 - 2 * md_sz;
   c->pt = 0;

sha3_api.h

@@ -37,11 +37,6 @@ extern "C"
     requires(memory_no_alias(c, sizeof(sha3_var_t)))
     requires(md_sz <= 49)
     assigns(object_whole(c))
-    ensures(forall(i, 0, 25, c->st.d[i] == 0))
-    ensures(c->md_sz <= 49)
-    ensures(c->r_sz <= 200)
-    ensures(c->r_sz >= 0)
-    ensures(c->pt == 0)
   );
 
   void sha3_update(sha3_var_t *c, const void *data, size_t data_sz);