diff --git a/ref-verification/hash.saw b/ref-verification/hash.saw
index 97b9c20..d941b5c 100644
--- a/ref-verification/hash.saw
+++ b/ref-verification/hash.saw
@@ -6,16 +6,19 @@ thm_P12 <- mk_P12;
 
 let ss0 = cryptol_ss ();
 
+thm_null_input <- prove_print rme
+  (rewrite ss0
+    {{ \(x : [0][8]) -> Hash256_bytes x ==
+       [0x0b, 0x3b, 0xe5, 0x85, 0x0f, 0x2f, 0x6b, 0x98,
+        0xca, 0xf2, 0x9f, 0x8f, 0xde, 0xa8, 0x9b, 0x64,
+        0xa1, 0xfa, 0x70, 0xaa, 0x24, 0x9b, 0x8f, 0x83,
+        0x9b, 0xd5, 0x3b, 0xaa, 0x30, 0x4d, 0x92, 0xb2] }});
+
 thm_unfold_iv <- prove_print rme
   (rewrite ss0
-    {{ Ascon_p`{12} [Hash256_IV, 0, 0, 0, 0]
-       ==
-       [0x9b1e5494e934d681,
-        0x4bc3a01e333751d2,
-        0xae65396c6b34b81a,
-        0x3c7fd4a4d56a4db3,
-        0x1a5c464906c5976d]
-    }});
+    {{ Ascon_p`{12} [Hash256_IV, 0, 0, 0, 0] ==
+       [0x9b1e5494e934d681, 0x4bc3a01e333751d2, 0xae65396c6b34b81a,
+        0x3c7fd4a4d56a4db3, 0x1a5c464906c5976d] }});
 
 let verify_hash256 IN_len =
   llvm_verify
@@ -34,26 +37,29 @@ let verify_hash256 IN_len =
     llvm_points_to OUT_ptr (llvm_term {{ Hash256_bytes IN }});
       llvm_return (llvm_term {{ 0 : [32] }});
     };
-    
+
 // What4 will have completely evaluated the term from symbolic evaluation
 // so don't try to keep Ascon_p uninterpreted at all.
-verify_hash256 0 rme;
+// verify_hash256 0 rme;
 
-for [      1,  2,  3,  4,  5,  6,  7,
+for [  0,  1,  2,  3,  4,  5,  6,  7,
        8,  9, 10, 11, 12, 13, 14, 15,
       16, 17, 18, 19, 20, 21, 22, 23,
       24, 25, 26, 27, 28, 29, 30, 31,
       32, 33] (\IN_len -> do {
-  
+
   print ("Verifying for size", IN_len);
   verify_hash256 IN_len
-  do { 
-      // What4 will have simplified away the application of
-      // Ascon_p to the IV, so simplify that away before
-      // holding all other Ascon_p occurences uninterpreted.
+  do {
+      // Handle zero case that completely evaluated away
+      simplify (addsimp thm_null_input ss0);
 
+      // Expose (Ascon_p [IV,0,0,0,0])
       unfolding ["Hash256_bytes", "Hash256", "hashBlocks"];
+
+      // Handle non-zero case where W4 simplified the IV permutation
       simplify (addsimp thm_unfold_iv ss0);
+
       w4_unint_rme ["Ascon_p"];
     };
 });