From 8c9c3562203923240ffcb637bf9fede3e3666706 Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@gmail.com>
Date: Sun, 7 Sep 2025 10:41:52 -0700
Subject: [PATCH] Add saw proof for AEAD inversion

---
 Makefile   |  6 +++++-
 verify.saw | 12 ++++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 verify.saw

diff --git a/Makefile b/Makefile
index fb007e3..ad9e18b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,7 @@
-.PHONY: test test-hash256 test-xof128 test-cxof128 test-aead128
+.PHONY: test test-hash256 test-xof128 test-cxof128 test-aead128 saw-proofs
 
 CRYPTOL ?= cryptol
+SAW ?= saw
 
 test: test-hash256 test-xof128 test-cxof128 test-aead128
 
@@ -15,3 +16,6 @@ test-cxof128:
 
 test-aead128:
 	$(CRYPTOL) -c :exhaust TestAsconAEAD128.cry
+
+saw-proofs:
+	$(SAW) verify.saw
\ No newline at end of file
diff --git a/verify.saw b/verify.saw
new file mode 100644
index 0000000..e541c6c
--- /dev/null
+++ b/verify.saw
@@ -0,0 +1,12 @@
+import "Ascon.cry";
+
+for [0,1,2,16,63,64,65,127,128,129,255,256] (\a ->
+for [0,1,2,16,63,64,65,127,128,129,255,256] (\p -> do {
+    print ("decrypt_encrypt",a,p);
+    prove_print (unint_yices ["Ascon::Ascon_p"]) {{
+        \K N (A : [a]) (P : [p]) ->
+        case AEAD128_decrypt K N A (AEAD128_encrypt K N A P) of
+            None -> False
+            Some p' -> p' == P
+    }};
+}));