From 8732e7527147f1240e303c0ac27425f6624e243d Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@gmail.com>
Date: Tue, 30 Sep 2025 20:39:30 -0700
Subject: [PATCH] Cleanups

---
 ref-verification/aead.saw | 11 +++++------
 ref-verification/hash.saw | 20 ++++++++++----------
 2 files changed, 15 insertions(+), 16 deletions(-)

diff --git a/ref-verification/aead.saw b/ref-verification/aead.saw
index 2ed948a..7b9416f 100644
--- a/ref-verification/aead.saw
+++ b/ref-verification/aead.saw
@@ -22,10 +22,10 @@ let verify_encrypt A_len P_len = do {
   do {
     // Inputs
 
+    let CT_len = eval_size {| P_len + T_len |};
+
     let A_type = llvm_array A_len i8;
     let P_type = llvm_array P_len i8;
-    
-    let CT_len = eval_size {| P_len + T_len |};
     let CT_type = llvm_array CT_len i8;
 
     (P, P_ptr) <- fresh_alloc_readonly "P" P_type;
@@ -62,15 +62,14 @@ let verify_decrypt A_len P_len = do {
   do {
     let CT_len = eval_size {| P_len + T_len |};
 
-    let C_type = llvm_array P_len i8;
-    let CT_type = llvm_array CT_len i8;
     let A_type = llvm_array A_len i8;
     let P_type = llvm_array P_len i8;
-    
+    let C_type = llvm_array P_len i8;
+    let CT_type = llvm_array CT_len i8;
+
     // Inputs
     C <- llvm_fresh_var "C" C_type;
     T <- llvm_fresh_var "T" T_type;
-
     CT_ptr <- llvm_alloc_readonly CT_type;
     llvm_points_to CT_ptr (llvm_term {{ C # T }});
 
diff --git a/ref-verification/hash.saw b/ref-verification/hash.saw
index d941b5c..f01e712 100644
--- a/ref-verification/hash.saw
+++ b/ref-verification/hash.saw
@@ -22,19 +22,19 @@ thm_unfold_iv <- prove_print rme
 
 let verify_hash256 IN_len =
   llvm_verify
-  m "crypto_hash"
-  [thm_P12]
-  true
-  do {
-    let IN_type = llvm_array IN_len (llvm_int 8);
-    (IN, IN_ptr) <- fresh_alloc_readonly "IN" IN_type;
+    m "crypto_hash"
+    [thm_P12]
+    true
+    do {
+      let IN_type = llvm_array IN_len (llvm_int 8);
+      (IN, IN_ptr) <- fresh_alloc_readonly "IN" IN_type;
 
-    let OUT_type = llvm_array 32 (llvm_int 8);
-    OUT_ptr <- llvm_alloc OUT_type;
+      let OUT_type = llvm_array 32 (llvm_int 8);
+      OUT_ptr <- llvm_alloc OUT_type;
 
-    llvm_execute_func [OUT_ptr, IN_ptr, llvm_term {{ `IN_len:[64] }}];
+      llvm_execute_func [OUT_ptr, IN_ptr, llvm_term {{ `IN_len:[64] }}];
 
-    llvm_points_to OUT_ptr (llvm_term {{ Hash256_bytes IN }});
+      llvm_points_to OUT_ptr (llvm_term {{ Hash256_bytes IN }});
       llvm_return (llvm_term {{ 0 : [32] }});
     };