From a3d978a4b3aab08dbba2dcfaa19e9d5c402ae40c Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@galois.com>
Date: Mon, 8 Sep 2025 11:08:52 -0700
Subject: [PATCH] Fixup documentation for tag change

---
 Ascon.cry | 27 +++++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

diff --git a/Ascon.cry b/Ascon.cry
index 4ba78e8..f66fd1b 100644
--- a/Ascon.cry
+++ b/Ascon.cry
@@ -196,7 +196,8 @@ private
  * - P: Plaintext
  *
  * Returns:
- * - Authenticated ciphertext
+ * - Ciphertext
+ * - Tag
  */
 AEAD128_encrypt :
   {a, p} (fin a, fin p) =>
@@ -243,6 +244,7 @@ AEAD128_encrypt K N A P = (C, T)
  * - N: Nonce
  * - A: Associated data
  * - C: Ciphertext
+ * - T: Tag
  *
  * Returns:
  * - Some plaintext on authentication success
@@ -255,6 +257,25 @@ AEAD128_decrypt K N A C T1 = if T1 == T2 then Some P else None
   where
    (P, T2) = AEAD128_decrypt_raw K N A C
 
+/** Raw Ascon-AEAD128 decryption algorithm on bitstreams.
+ *
+ * The tag returned by this function should be compared to the
+ * tag on the associated ciphertext to authenticate it.
+ *
+ * Type parameters:
+ * - a: Bit-length of associated data
+ * - p: Bit-length of plaintext
+ *
+ * Parameters:
+ * - K: Key
+ * - N: Nonce
+ * - A: Associated data
+ * - C: Ciphertext
+ *
+ * Returns:
+ * - P: Plaintext
+ * - T: Computed tag
+ */
 AEAD128_decrypt_raw :
   {a, p} (fin a, fin p) =>
   [128] -> [128] -> [a] -> [p] -> ([p], [128])
@@ -291,7 +312,8 @@ AEAD128_decrypt_raw K N A C = (P, T)
  * - P: Plaintext
  *
  * Returns:
- * - Authenticated ciphertext
+ * - C: Ciphertext
+ * - T: Tag
  */
 AEAD128_encrypt_bytes :
   {a, p} (fin a, fin p) =>
@@ -315,6 +337,7 @@ AEAD128_encrypt_bytes K N A P = (bitsToWords C, bitsToWords T)
  * - N: Nonce
  * - A: Associated data
  * - C: Ciphertext
+ * - T: Tag
  *
  * Returns:
  * - Some plaintext on authentication success