From 402be4c15b76ba8b9a53213ce2e38886f78186a3 Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@gmail.com>
Date: Sat, 20 Sep 2025 11:16:37 -0700
Subject: [PATCH] Add decryption spec to saw script

---
 ref-verification/aead.saw   | 113 +++++++++++++++++++++++++++++-------
 ref-verification/common.saw |   2 +-
 2 files changed, 92 insertions(+), 23 deletions(-)

diff --git a/ref-verification/aead.saw b/ref-verification/aead.saw
index 305a486..2ed948a 100644
--- a/ref-verification/aead.saw
+++ b/ref-verification/aead.saw
@@ -5,7 +5,16 @@ include "common.saw";
 thm_P8 <- mk_P8;
 thm_P12 <- mk_P12;
 
-let verify_aead P_len A_len = do {
+let N_len = 16;
+let N_type = llvm_array N_len i8;
+
+let K_len = 16;
+let K_type = llvm_array K_len i8;
+
+let T_len = 16;
+let T_type = llvm_array T_len i8;
+
+let verify_encrypt A_len P_len = do {
   llvm_verify
   m "crypto_aead_encrypt"
   [thm_P12, thm_P8]
@@ -13,28 +22,24 @@ let verify_aead P_len A_len = do {
   do {
     // Inputs
 
-    let P_type = llvm_array P_len i8;
-    (P, P_ptr) <- fresh_alloc_readonly "P" P_type;
-
     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;
     (A, A_ptr) <- fresh_alloc_readonly "A" A_type;
-
-    let N_type = llvm_array 16 i8;
     (N, N_ptr) <- fresh_alloc_readonly "N" N_type;
-
-    let K_type = llvm_array 16 i8;
     (K, K_ptr) <- fresh_alloc_readonly "K" K_type;
 
     // Outputs
 
-    let C_len = eval_size {| P_len + 16 |};
-    let C_type = llvm_array C_len i8;
-    C_ptr <- llvm_alloc C_type;
-
-    CLEN_ptr <- llvm_alloc i64;
+    CT_ptr <- llvm_alloc CT_type;
+    CTLEN_ptr <- llvm_alloc i64;
 
     llvm_execute_func
-      [ C_ptr, CLEN_ptr
+      [ CT_ptr, CTLEN_ptr
       , P_ptr, llvm_term {{ `P_len:[64] }}
       , A_ptr, llvm_term {{ `A_len:[64] }}
       , llvm_null
@@ -42,16 +47,80 @@ let verify_aead P_len A_len = do {
       , K_ptr
       ];
 
-    llvm_points_to CLEN_ptr (llvm_term {{ `C_len : [64] }});
-    llvm_points_to C_ptr (llvm_term {{ C # T where (C,T) = AEAD128_encrypt_bytes K N A P }});
+    llvm_points_to CTLEN_ptr (llvm_term {{ `CT_len : [64] }});
+    llvm_points_to CT_ptr (llvm_term {{ C # T where (C,T) = AEAD128_encrypt_bytes K N A P }});
     llvm_return (llvm_term {{ 0 : [32] }});
   }
   (unint_yices ["Ascon::Ascon_p"]);
 };
 
-verify_aead 0 0;
-verify_aead 0 1;
-verify_aead 1 0;
-verify_aead 10 10;
-verify_aead 20 20;
-verify_aead 33 100;
\ No newline at end of file
+let verify_decrypt A_len P_len = do {
+  llvm_verify
+  m "crypto_aead_decrypt"
+  [thm_P12, thm_P8]
+  false
+  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;
+    
+    // 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 }});
+
+    (A, A_ptr) <- fresh_alloc_readonly "A" A_type;
+    (N, N_ptr) <- fresh_alloc_readonly "N" N_type;
+    (K, K_ptr) <- fresh_alloc_readonly "K" K_type;
+
+    // Outputs
+    P_ptr <- llvm_alloc P_type;
+    PLEN_ptr <- llvm_alloc i64;
+
+    llvm_execute_func
+      [ P_ptr, PLEN_ptr
+      , llvm_null
+      , CT_ptr, llvm_term {{ `CT_len:[64] }}
+      , A_ptr, llvm_term {{ `A_len:[64] }}
+      , N_ptr
+      , K_ptr
+      ];
+
+    // Compute the expected plaintext and tag
+    let PT = {{ AEAD128_decrypt_raw (wordsToBits K) (wordsToBits N) (wordsToBits A) (wordsToBits C) }};
+
+    // Update the plaintext length
+    llvm_points_to PLEN_ptr (llvm_term {{ `P_len : [64] }});
+
+    if eval_bool {{ `P_len > (0 : Integer) }}
+      then llvm_points_to P_ptr (llvm_term {{ bitsToWords PT.0 : [P_len][8] }})
+      else return (); // Reading a 0-length array out of uninitialized memory doesn't work (and isn't needed)
+
+    // Returns 0 on success, -1 on error
+    llvm_return (llvm_term {{ if bitsToWords PT.1 == T then 0 else ~0 : [32] }});
+  }
+  (unint_yices ["Ascon::Ascon_p"]);
+};
+
+// Additional Data incorporation is independent of
+// plain/cipher text processing. Check multiple sizes
+// of AD first and then check multiple sizes of P/C
+
+for [0,1,10,16,100] (\A_len ->
+  for [1] (\P_len -> do {
+    verify_encrypt A_len P_len;
+    verify_decrypt A_len P_len;
+  })
+);
+
+for [0,1] (\A_len ->
+  for [0,1,2,10,15,16,17,100] (\P_len -> do {
+    verify_encrypt A_len P_len;
+    verify_decrypt A_len P_len;
+  })
+);
diff --git a/ref-verification/common.saw b/ref-verification/common.saw
index 84e27b5..5256a76 100644
--- a/ref-verification/common.saw
+++ b/ref-verification/common.saw
@@ -1,4 +1,4 @@
-import "/Users/emertens/Source/ascon/Ascon.cry";
+import "../Ascon.cry";
 
 let i8 = llvm_int 8;
 let i64 = llvm_int 64;