From d3472254a106eb44601ac0b59ef2967a17786087 Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@galois.com>
Date: Mon, 6 Oct 2025 15:03:01 -0700
Subject: [PATCH] Allow hashDigest to generate inf stream

---
 Ascon.cry | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/Ascon.cry b/Ascon.cry
index 6a0ac64..08c6776 100644
--- a/Ascon.cry
+++ b/Ascon.cry
@@ -357,10 +357,10 @@ private
        */
       | a == 0 => DomainSep S
 
-  /* Absorb a block in input into the state.
+  /** Absorb a block in input into the state.
    *     𝑆[0:127] ← 𝑆[0:127] ⊕ 𝐴ᵢ      (20)
    *     𝑆 ← Ascon-p[8](𝑆)             (21)
-   **/
+   */
   AbsorbADBlock : State -> [128] -> State
   AbsorbADBlock S Ai = Ascon_p`{8} (XorBlock S Ai)
 
@@ -474,8 +474,8 @@ private Hash256_IV = 0x0000080100cc0002
  * Returns:
  * - Variable-length message digest
  */
-XOF128 : {r, m} (fin m, fin r) => [m] -> [r]
-XOF128 M = take (hashBlocks XOF128_IV (toBlocks M))
+XOF128 : {r, m} (fin m) => [m] -> [r]
+XOF128 M = take`{back=inf} (hashBlocks XOF128_IV (toBlocks M))
 
 /** Ascon-XOF256 implementation on bytes.
  *
@@ -489,7 +489,7 @@ XOF128 M = take (hashBlocks XOF128_IV (toBlocks M))
  * Returns:
  * - Variable-length message digest
  */
-XOF128_bytes : {r, n} (fin n, fin r) => [n][8] -> [r][8]
+XOF128_bytes : {r, n} (fin n) => [n][8] -> [r][8]
 XOF128_bytes M = bitsToWords (XOF128 (wordsToBits M))
 
 /** Ascon-XOF128 initialization vector */
@@ -513,9 +513,9 @@ private XOF128_IV = 0x0000080000cc0003
  * - Variable-length message digest
  */
 CXOF128 :
-  {r, z, m} (fin m, fin r, 64 >= width z) =>
+  {r, z, m} (fin m, 64 >= width z) =>
   [z] -> [m] -> [r]
-CXOF128 Z M = take (hashBlocks CXOF128_IV Ms)
+CXOF128 Z M = take`{back=inf} (hashBlocks CXOF128_IV Ms)
   where
     Ms = [`z]
        # toBlocks Z
@@ -536,7 +536,7 @@ CXOF128 Z M = take (hashBlocks CXOF128_IV Ms)
  * - Variable-length message digest
  */
 CXOF128_bytes :
-  {r, z, m} (fin m, fin r, 61 >= width z) =>
+  {r, z, m} (fin m, 61 >= width z) =>
   [z][8] -> [m][8] -> [r][8]
 CXOF128_bytes Z M = bitsToWords (CXOF128 (wordsToBits Z) (wordsToBits M))