Update tests for AEAD change

Ascon.cry

@@ -1,55 +1,110 @@
-/**
-
-Implementation of Ascon-Based Lightweight Cryptography
-
-Reference:
-
-Meltem Sönmez Turan, Kerry A. McKay, Donghoon Chang, Jinkeon Kang,
-John Kelsey (2025) Ascon-Based Lightweight Cryptography Standards
-for Constrained Devices. (National Institute of Standards and Technology,
-Gaithersburg, MD), NIST Special Publication (SP) NIST SP 800-232.
-https://doi.org/10.6028/NIST.SP.800-232
-
-*/
+/** Ascon-Based Lightweight Cryptography
+ *
+ * Author: Eric Mertens <emertens@gmail.com>
+ * License: ISC
+ *
+ * Key algorithms:
+ * - AEAD128_encrypt/decrypt: Authenticated encryption
+ * - Hash256: Cryptographic hash function
+ * - XOF128: Extendable output function
+ * - CXOF128: Customizable extendable output function
+ *
+ * Reference:
+ *
+ * Meltem Sönmez Turan, Kerry A. McKay, Donghoon Chang, Jinkeon Kang,
+ * John Kelsey (2025) Ascon-Based Lightweight Cryptography Standards
+ * for Constrained Devices. (National Institute of Standards and Technology,
+ * Gaithersburg, MD), NIST Special Publication (SP) NIST SP 800-232.
+ * https://doi.org/10.6028/NIST.SP.800-232
+ */
 module Ascon where
 
-// 2.1. Auxiliary Functions
+private
+  // 2.1. Auxiliary Functions
 
-/// Parse function.
-parse : {r, n} (fin n, fin r, 0 < r) => [n] -> ([n/r][r], [n%r])
-parse (M_ # Ml) = (split M_, Ml)
+  /** Parse function.
+   *
+   * The parse(𝑋, 𝑟) function parses the input bitstring 𝑋 into a sequence
+   * of blocks 𝑋₀, 𝑋₁, …, 𝑋͠ℓ, where 𝓁 ← ⌊|𝑋|/𝑟⌋ (i.e., 𝑋 ← 𝑋₀ ∥ 𝑋₁ ∥ … ∥ 𝑋͠ℓ).
+   * The 𝑋ᵢ blocks for 0 ≤ i ≤ 𝓁 − 1 each have a bit length 𝑟, whereas
+   * 0 ≤ |𝑋͠ℓ| ≤ 𝑟 − 1 (see Algorithm 1). When |𝑋| mod 𝑟 = 0, the final
+   * block is empty (i.e., |𝑋͠ℓ| = 0).
+   */
+  parse : {r, m} (fin m, fin r, r >= 1) => [m] -> ([m / r][r], [m % r])
+  parse (M # Ml) = (split M, Ml)
 
-/// Padding rule.
-pad : {r, n} (n < r, fin r) => [n] -> [r]
-pad M = M # 0b1 # 0
+  /** Padding rule.
+   *
+   * The function pad(𝑋, 𝑟) appends the bit 1 to the bitstring 𝑋, followed
+   * by the bitstring 0ʲ, where 𝑗 is equal to (−|𝑋|−1) mod 𝑟. The length of
+   * the output bitstring is a multiple of 𝑟 (see Algorithm 2). For examples
+   * of padding when representing the data as 64-bit unsigned integers, see
+   * Appendix A.2.
+   */
+  pad : {r, m} (m < r, fin r) => [m] -> [r]
+  pad M = M # 0b1 # 0
 
-toBlocks : {r, n} (r >= 1, fin r, fin n) => [n] -> [n / r + 1][r]
-toBlocks M = M1 # [pad M2]
-  where
-    (M1, M2) = parse M
+  /**
+   * Combination of parse and pad that splits a bitstring into a sequence
+   * of integers using Cryptol's native big-endian representation.
+   */
+  toBlocks : {r, m} (r >= 1, fin r, fin m) => [m] -> [m / r + 1][r]
+  toBlocks M = bitsToWords (M # 0b1 # 0)
 
-// 3. Ascon Permutations
+  // 3. Ascon Permutations
 
-type constraint ValidRnd rnd = (1 <= rnd, rnd <= 16)
+  /** Predicate on valid round counts. */
+  type constraint ValidRnd rnd = rnd <= 16
 
-Ascon_p : {rnd} (ValidRnd rnd) => State -> State
-Ascon_p S = foldl p`{rnd} S (drop`{back=rnd} Const)
+  /** Core permutation function parameterized by a round count. */
+  Ascon_p : {rnd} (ValidRnd rnd) => State -> State
+  Ascon_p S = foldl round S (drop`{back=rnd} Const)
 
-p : {rnd} (ValidRnd rnd) => State -> [64] -> State
-p S ci = pL (pS (pC S ci))
+  /**
+  * Single round of the Ascon-p permutation parameterized by the round
+  * constant.
+  */
+  round : State -> [64] -> State
+  round S ci = pL (pS (pC S ci))
 
-// 3.1. Internal State
+  // 3.1. Internal State
 
-type State = [5][64]
+  /**
+  * The permutations operate on the 320-bit state 𝑆, which is represented
+  * as five 64-bit words denoted as 𝑆ᵢ for 0 ≤ 𝑖 ≤ 4:
+  *
+  *     𝑆 = 𝑆₀ ‖ 𝑆₁ ‖ 𝑆₂ ‖ 𝑆₃ ‖ 𝑆₄
+  *
+  * Let 𝑠ᵢⱼ represent the 𝑗th bit of 𝑆ᵢ, 0 ≤ 𝑗 < 64. In this specification
+  * of the Ascon permutation, each state word represents a 64-bit unsigned
+  * integer, where the least significant bit is the rightmost bit. Details
+  * on other representations of the state can be found in Appendix A.
+  */
+  type State = [5][64]
 
-// 3.2. Constant-Addition Layer pC 
+  // 3.2. Constant-Addition Layer pC
 
-pC : State -> [64] -> State
-pC [S0, S1, S2, S3, S4] ci = [S0, S1, S2 ^ ci, S3, S4]
+  // The constant cᵢ of round 𝑖 of the Ascon permutation Ascon-p[𝑟𝑛𝑑]
+  // (instantiated with 𝑟𝑛𝑑 rounds) for 𝑟𝑛𝑑 ≤ 16 and 0 ≤ 𝑖 < 𝑟𝑛𝑑 − 1
+  // is defined as
+  //
+  //     cᵢ = const[16 − 𝑟𝑛𝑑 + 𝑖]
+  //
+  // where const[0],…,const[15] are defined in Table 5.
 
-/// Table 5. The constants constᵢ to derive round constants of the Ascon permutations
-Const : [16][64]
-Const =
+  /**
+  * The constant-addition layer 𝑃𝑐 adds a 64-bit round constant cᵢ to 𝑆₂
+  * in round 𝑖, for i ≥ 0, 𝑆₂ = 𝑆₂ ⊕ cᵢ.
+  */
+  pC : State -> [64] -> State
+  pC [S0, S1, S2, S3, S4] ci = [S0, S1, S2 ^ ci, S3, S4]
+
+  /**
+  * Table 5. The constants constᵢ to derive round constants of the Ascon
+  * permutations
+  */
+  Const : [16][64]
+  Const =
       [ 0x000000000000003c
       , 0x000000000000002d
       , 0x000000000000001e
@@ -68,26 +123,46 @@ Const =
       , 0x000000000000004b
       ]
 
-// 3.3. Substitution Layer pS
+  // 3.3. Substitution Layer pS
 
-pS : State -> State
-pS S = transpose (map SBox (transpose S))
+  /**
+   * The substitution layer 𝑝𝑆 updates the state S with 64 parallel
+   * applications of the 5-bit substitution box SBOX
+   */
+  pS : State -> State
+  pS S = transpose (map SBox (transpose S))
 
-SBox : [5] -> [5]
-SBox i = SBoxTable@i
+  /** 5-bit substitution used in pS. */
+  SBox : [5] -> [5]
+  SBox i = SBoxTable@i
 
-/// Table 6.
-SBoxTable : [32][5]
-SBoxTable =
+  /** Table 6. Lookup table for SBox */
+  SBoxTable : [32][5]
+  SBoxTable =
       map drop
-    [ 0x04, 0x0b, 0x1f, 0x14, 0x1a, 0x15, 0x09, 0x02, 0x1b, 0x05, 0x08, 0x12, 0x1d, 0x03, 0x06, 0x1c
-    , 0x1e, 0x13, 0x07, 0x0e, 0x00, 0x0d, 0x11, 0x18, 0x10, 0x0c, 0x01, 0x19, 0x16, 0x0a, 0x0f, 0x17
+      [ 0x04, 0x0b, 0x1f, 0x14, 0x1a, 0x15, 0x09, 0x02
+      , 0x1b, 0x05, 0x08, 0x12, 0x1d, 0x03, 0x06, 0x1c
+      , 0x1e, 0x13, 0x07, 0x0e, 0x00, 0x0d, 0x11, 0x18
+      , 0x10, 0x0c, 0x01, 0x19, 0x16, 0x0a, 0x0f, 0x17
       ]
 
-// 3.4. Linear Diffusion Layer pL
+  property
+    SBoxCorrect x0 x1 x2 x3 x4 =
+      [y0, y1, y2, y3, y4] == SBox [x0, x1, x2, x3, x4]
+      where
+        y0 = x4&&x1 ^ x3 ^ x2&&x1 ^ x2 ^ x1&&x0 ^ x1 ^ x0
+        y1 = x4 ^ x3&&x2 ^ x3&&x1 ^ x3 ^ x2&&x1 ^ x2 ^ x1 ^ x0
+        y2 = x4&&x3 ^ x4 ^ x2 ^ x1 ^ 1
+        y3 = x4&&x0 ^ x4 ^ x3&&x0 ^ x3 ^ x2 ^ x1 ^ x0
+        y4 = x4&&x1 ^ x4 ^ x3 ^ x1&&x0 ^ x1
 
-pL : State -> State
-pL [S0, S1, S2, S3, S4] =
+  // 3.4. Linear Diffusion Layer pL
+
+  /** The linear diffusion layer 𝑝𝐿 provides diffusion within each 64-bit
+   * word 𝑆𝑖.
+   */
+  pL : State -> State
+  pL [S0, S1, S2, S3, S4] =
       [ sigma S0 19 28
       , sigma S1 61 39
       , sigma S2  1  6
@@ -96,7 +171,411 @@ pL [S0, S1, S2, S3, S4] =
       ]
       where
           sigma : [64] -> [6] -> [6] -> [64]
-        sigma x i j = x ^ (x >>> i) ^ (x >>> j)
+          sigma x i j = x ^ x>>>i ^ x>>>j
 
-little_bytes : {n} (fin n) => [8*n] -> [8*n]
-little_bytes M = join (map reverse (groupBy`{8} M))
+  /** Concatenate a sequence of integers into a little-endian bitstream. */
+  wordsToBits : {w, n} (fin w) => [n][w] -> [w*n]
+  wordsToBits M = join (map reverse M)
+
+  /** Split a little-endian bitstream in to a sequence of integers. */
+  bitsToWords : {w, n} (fin w) => [w*n] -> [n][w]
+  bitsToWords M = map reverse (split M)
+
+// 4. Authenticated Encryption Schema: Ascon-AEAD128
+
+/** Ascon-AEAD128 encryption algorithm on bitstreams
+ *
+ * Type parameters:
+ * - a: Bit-length of associated data
+ * - p: Bit-length of plaintext
+ *
+ * Parameters:
+ * - K: Key
+ * - N: Nonce
+ * - A: Associated data
+ * - P: Plaintext
+ *
+ * Returns:
+ * - Ciphertext
+ * - Tag
+ */
+AEAD128_encrypt :
+  {a, p} (fin a, fin p) =>
+  [128] -> [128] -> [a] -> [p] -> ([p], [128])
+AEAD128_encrypt K N A P = (C, T)
+  where
+    [K0, K1] = bitsToWords K
+    [N0, N1] = bitsToWords N
+
+    // 𝑆 ← 𝐼𝑉 ‖ 𝐾 ‖ 𝑁                            (15)
+    // 𝑆 ← Ascon-p[12](𝑆)                        (16)
+    // 𝑆 ← 𝑆 ⊕ (0¹⁹² ‖ 𝐾)                        (17)
+    S0 = Ascon_p`{12} [AEAD128_IV, K0, K1, N0, N1] ^ [0, 0, 0, K0, K1]
+
+    SA = AddAD S0 A
+
+    // 𝑃₀, 𝑃₁, …, 𝑃ₙ₋₁, 𝑃͠ₙ ← parse(𝑃,128)        (23)
+    // For each 𝑃ᵢ, 0 ≤ 𝑖 ≤ 𝑛−1
+    //     𝑆[0:127] ← 𝑆[0:127] ⊕ 𝑃ᵢ              (24)
+    //     𝐶ᵢ ← 𝑆[0:127]                         (25)
+    //     𝑆 ← Ascon-p[8](𝑆)                     (26)
+    // For the last block 𝑃͠ₙ
+    //     𝑆[0:127] ← 𝑆[0:127] ⊕ pad(𝑃͠ₙ,128)     (27)
+    //     𝐶͠ₙ ← 𝑆[0:ℓ−1]                         (28)
+    SCs = [XorBlock s p | s <- [SA] # map Ascon_p`{8} SCs | p <- toBlocks P]
+
+    // 𝐶 ← 𝐶₀ ‖ … ‖ 𝐶ₙ₋₁ ‖ 𝐶͠ₙ                    (29)
+    C = take (join (map ExtractC SCs))
+
+    // 𝑆 ← 𝑆 ⊕ (0¹²⁸ ‖ 𝐾 ‖ 0⁶⁴)                  (30)
+    // 𝑆 ← Ascon-p[12](𝑆)                        (31)
+    // 𝑇 ← 𝑆[192:319] ⊕ 𝐾                        (32)
+    ST = Ascon_p`{12} (last SCs ^ [0, 0, K0, K1, 0])
+    T = ExtractT ST ^ K
+
+/** Ascon-AEAD128 decryption algorithm on bitstreams.
+ *
+ * Type parameters:
+ * - a: Bit-length of associated data
+ * - p: Bit-length of plaintext
+ *
+ * Parameters:
+ * - K: Key
+ * - N: Nonce
+ * - A: Associated data
+ * - C: Ciphertext
+ * - T: Tag
+ *
+ * Returns:
+ * - Some plaintext on authentication success
+ * - None on authentication failure
+ */
+AEAD128_decrypt :
+  {a, p} (fin a, fin p) =>
+  [128] -> [128] -> [a] -> [p] -> [128] -> Option [p]
+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])
+AEAD128_decrypt_raw K N A C = (P, T)
+  where
+    // key and nonce as two 64-bit integers
+    [K0, K1] = bitsToWords K
+    [N0, N1] = bitsToWords N
+
+    S0 = Ascon_p`{12} [AEAD128_IV, K0, K1, N0, N1] ^ [0, 0, 0, K0, K1]
+    SA = AddAD S0 A
+
+    (Cs, Cl1) = parse C
+    SCs = [SA] # [Ascon_p`{8} (AssignC s c) | s <- SCs | c <- Cs]
+
+    Mask # Cl2 = join (map ExtractC SCs)
+    P = Mask ^ C
+
+    Cl = Cl1 # (0b1#0 ^ Cl2) // xor toggles the padding bit
+    ST1 = AssignC (last SCs) Cl
+    ST2 = Ascon_p`{12} (ST1 ^ [0, 0, K0, K1, 0])
+    T = ExtractT ST2 ^ K
+
+/** Ascon-AEAD128 encryption algorithm on bytes.
+ *
+ * Type parameters:
+ * - a: Byte-length of associated data
+ * - p: Byte-length of plaintext
+ *
+ * Parameters:
+ * - K: Key
+ * - N: Nonce
+ * - A: Associated data
+ * - P: Plaintext
+ *
+ * Returns:
+ * - C: Ciphertext
+ * - T: Tag
+ */
+AEAD128_encrypt_bytes :
+  {a, p} (fin a, fin p) =>
+  [16][8] -> [16][8] -> [a][8] -> [p][8] -> ([p][8], [16][8])
+AEAD128_encrypt_bytes K N A P = (bitsToWords C, bitsToWords T)
+  where
+    (C, T) = AEAD128_encrypt K' N' A' P'
+    K' = wordsToBits K
+    N' = wordsToBits N
+    A' = wordsToBits A
+    P' = wordsToBits P
+
+/** Ascon-AEAD128 decryption algorithm on bytes.
+ *
+ * Type parameters:
+ * - a: Byte-length of associated data
+ * - p: Byte-length of plaintext
+ *
+ * Parameters:
+ * - K: Key
+ * - N: Nonce
+ * - A: Associated data
+ * - C: Ciphertext
+ * - T: Tag
+ *
+ * Returns:
+ * - Some plaintext on authentication success
+ * - None on authentication failure
+ */
+AEAD128_decrypt_bytes :
+  {a, p} (fin a, fin p) =>
+  [16][8] -> [16][8] -> [a][8] -> [p][8] -> [16][8] -> Option ([p][8])
+AEAD128_decrypt_bytes K N A C T =
+  case AEAD128_decrypt K' N' A' C' T' of
+    None -> None
+    Some p -> Some (bitsToWords p)
+  where
+    K' = wordsToBits K
+    N' = wordsToBits N
+    A' = wordsToBits A
+    C' = wordsToBits C
+    T' = wordsToBits T
+
+private
+  /** Absorb all of the associated data into the permutation state. */
+  AddAD : {a} (fin a) => State -> [a] -> State
+  AddAD S A
+
+      /* If the AD is non-empty (i.e., |𝐴| > 0):
+       *    𝐴₀, 𝐴₁, …, 𝐴ₘ₋₁, 𝐴͠ₘ ← parse(𝐴,128)   (18)
+       *    𝐴ₘ ← pad(𝐴͠ₘ,128)                     (19)
+       */
+      | a > 0  => DomainSep (foldl AbsorbADBlock S (toBlocks A))
+
+      /* If the AD is empty (i.e., |𝐴| = 0): Only the final step
+       * described in (22) is applied.
+       */
+      | a == 0 => DomainSep S
+
+  /* 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)
+
+  /** Toggle the domain separation bit indicating end of associated data.
+   *    𝑆 ← 𝑆 ⊕ (0³¹⁹ ‖ 1)             (22)
+   */
+  DomainSep : State -> State
+  DomainSep [s0, s1, s2, s3, s4] = [s0, s1, s2, s3, s4 ^ 0b1#0]
+
+  /** Add a single block of data into the permutation state. */
+  XorBlock : State -> [128] -> State
+  XorBlock [s0, s1, s2, s3, s4] (xhi # xlo) =
+    [s0 ^ xlo, s1 ^ xhi, s2, s3, s4]
+
+  /** Extracts the first two words of permutation state as a bitstream. */
+  ExtractC : State -> [128]
+  ExtractC [s0, s1, _, _, _] = wordsToBits [s0, s1]
+
+  /** Assigns a bitstream into the first two words of permutation state. */
+  AssignC : State -> [128] -> State
+  AssignC [_, _, s2, s3, s4] C = bitsToWords C # [s2, s3, s4]
+
+  /** Extracts the last two words of permutation state as a bitstream. */
+  ExtractT : State -> [128]
+  ExtractT [_, _, _, s3, s4] = wordsToBits [s3, s4]
+
+  /** Ascon-AEAD128 initialization vector */
+  AEAD128_IV : [64]
+  AEAD128_IV = 0x00001000808c0001
+
+// 5. Hash and eXtendable-Output Functions (XOFs)
+
+private
+  /** Hash function construction
+   *
+   * All three of the modes in Ascon use the same message
+   * absorbtion and 
+   *
+   * Parameters:
+   * - Initialization vector
+   * - List of blocks as integers
+   *
+   * Returns:
+   * - Infinite message digest bitstream to be truncated by caller
+   */
+  hashBlocks : {n} (fin n) => [64] -> [n][64] -> [inf]
+  hashBlocks IV Ms = H
+      where
+      // 𝑆 ← Ascon-p[12](𝐼𝑉 ‖ 0²⁵⁶)              (54)
+      S0 = Ascon_p`{12} [IV, 0, 0, 0, 0]
+
+      // Each message block 𝑀ᵢ is XORed with the state as
+      //     𝑆[0:63] ← 𝑆[0:63] ⊕ 𝑀ᵢ              (57)
+      //     𝑆 ← Ascon-p[12](𝑆)                  (58)
+      Sn = foldl AbsorbBlock64 S0 Ms
+
+      // Each output hash block is computed as
+      //     𝐻ᵢ ← 𝑆[0:63]                        (60)
+      //     𝑆 ← Ascon-p[12](𝑆)                  (61)
+      // 𝐻ᵢ ← 𝐻₀ ‖ 𝐻₁ ‖ …
+      H = wordsToBits [head S | S <- iterate Ascon_p`{12} Sn]
+
+  /** Absorb a block of hash input into the permutation state. */
+  AbsorbBlock64 : State -> [64] -> State
+  AbsorbBlock64 [s0, s1, s2, s3, s4] Mi = Ascon_p`{12} [s0 ^ Mi, s1, s2, s3, s4]
+
+// 5.1. Specification of Ascon-Hash256
+
+/** Ascon-Hash256 implementation on bitstreams.
+ *
+ * Type parameters:
+ * - m: Bit-length of message
+ *
+ * Parameters:
+ * - M: Message
+ *
+ * Returns:
+ * - Message digest
+ */
+Hash256 : {m} (fin m) => [m] -> [256]
+Hash256 M = take (hashBlocks Hash256_IV (toBlocks M))
+
+/** Ascon-Hash256 implementation on bytes.
+ *
+ * Type parameters:
+ * - m: Byte-length of message
+ *
+ * Parameters:
+ * - M: Message
+ *
+ * Returns:
+ * - Message digest
+ */
+Hash256_bytes : {m} (fin m) => [m][8] -> [32][8]
+Hash256_bytes M = bitsToWords (Hash256 (wordsToBits M))
+
+/** Ascon-Hash256 initialization vector */
+Hash256_IV : [64]
+private Hash256_IV = 0x0000080100cc0002
+
+// 5.2. Specification of Ascon-XOF128
+
+/** Ascon-XOF256 implementation on bitstreams.
+ *
+ * Type parameters:
+ * - r: Bit-length of digest
+ * - m: Bit-length of message
+ *
+ * Parameters:
+ * - M: Message
+ *
+ * Returns:
+ * - Variable-length message digest
+ */
+XOF128 : {r, m} (fin m, fin r) => [m] -> [r]
+XOF128 M = take (hashBlocks XOF128_IV (toBlocks M))
+
+/** Ascon-XOF256 implementation on bytes.
+ *
+ * Type parameters:
+ * - r: Byte-length of digest
+ * - m: Byte-length of message
+ *
+ * Parameters:
+ * - M: Message
+ *
+ * Returns:
+ * - Variable-length message digest
+ */
+XOF128_bytes : {r, n} (fin n, fin r) => [n][8] -> [r][8]
+XOF128_bytes M = bitsToWords (XOF128 (wordsToBits M))
+
+/** Ascon-XOF128 initialization vector */
+XOF128_IV : [64]
+private XOF128_IV = 0x0000080000cc0003
+
+// 5.3. Specification of Ascon-CXOF128
+
+/** Ascon-CXOF256 implementation on bitstreams.
+ *
+ * Type parameters:
+ * - r: Bit-length of digest
+ * - c: Bit-length of customization string
+ * - m: Bit-length of message
+ *
+ * Parameters:
+ * - Z: User-defined customization string
+ * - M: Message
+ *
+ * Returns:
+ * - Variable-length message digest
+ */
+CXOF128 :
+  {r, z, m} (fin m, fin r, 64 >= width z) =>
+  [z] -> [m] -> [r]
+CXOF128 Z M = take (hashBlocks CXOF128_IV Ms)
+  where
+    Ms = [`z]
+       # toBlocks Z
+       # toBlocks M
+
+/** Ascon-CXOF256 implementation on bytes.
+ *
+ * Type parameters:
+ * - r: Byte-length of digest
+ * - z: Byte-length of customization string
+ * - m: Byte-length of message
+ *
+ * Parameters:
+ * - Z: User-defined customization string
+ * - M: Message
+ *
+ * Returns:
+ * - Variable-length message digest
+ */
+CXOF128_bytes :
+  {r, z, m} (fin m, fin r, 61 >= width z) =>
+  [z][8] -> [m][8] -> [r][8]
+CXOF128_bytes Z M = bitsToWords (CXOF128 (wordsToBits Z) (wordsToBits M))
+
+/** Ascon-CXOF128 initialization vector */
+CXOF128_IV : [64]
+private CXOF128_IV = 0x0000080000cc0004
+
+// Appendix B. Determination of the Initial Values
+
+private
+  computeIV : [8] -> [4] -> [4] -> [16] -> [8] -> [64]
+  computeIV v a b t r =
+    // 𝐼𝑉 = 𝑣 ‖ 0⁸ ‖ 𝑎 ‖ 𝑏 ‖ 𝑡 ‖ 𝑟/8 ‖ 0¹⁶
+    reverse ( reverse v // is a unique identifier for the algorithm
+            # (0:[8])
+            # reverse a // is the number of rounds during initialization and finalization
+            # reverse b // is the number of rounds during the processing of AD, P, C, M
+            # reverse t // is 128 for AEAD128, 256 for Hash256, and 0 for XOF128/CXOF128
+            # reverse r // is the number of input bytes processed per permutation invocation
+            # (0:[16]))
+
+  property check_AEAD128_IV = AEAD128_IV == computeIV 1 12 8  128 16
+  property check_Hash256_IV = Hash256_IV == computeIV 2 12 12 256  8
+  property check_XOF128_IV  = XOF128_IV  == computeIV 3 12 12   0  8
+  property check_CXOF128_IV = CXOF128_IV == computeIV 4 12 12   0  8

AsconCipher.cry

@@ -1,43 +0,0 @@
-module AsconCipher where
-
-import Ascon
-
-// 4. Authenticated Encryption Schema: Ascon-AEAD128
-
-Ascon_AEAD128 : {a, p} (fin a, fin p) => [128] -> [128] -> [a] -> [p] -> [p + 128]
-Ascon_AEAD128 (Khi_ # Klo_) (Nhi_ # Nlo_) A P = C # reverse T
-  where
-    Khi = reverse Khi_
-    Klo = reverse Klo_
-    Nhi = reverse Nhi_
-    Nlo = reverse Nlo_
-
-    S0 = Ascon_p`{12} [Ascon_AEAD128_IV, Khi, Klo, Nhi, Nlo]
-       ^ [0, 0, 0, Khi, Klo]
-    
-    SA = AddAD S0 A
-  
-    SCs = zipWith XorBlock (take ([SA] # map Ascon_p`{8} SCs)) (toBlocks P)
-
-    C = take (join [reverse s0 # reverse s1 | [s0, s1, _, _, _] <- SCs])
-
-    ST = Ascon_p`{12} (last SCs ^ [0, 0, Khi, Klo, 0])
-    T = ST@(4:[3]) # ST@(3:[3])
-      ^ Klo # Khi
-
-AddAD : {a} (fin a) => State -> [a] -> State
-AddAD S A
-  | a == 0 => DomainSep S
-  | a > 0  => DomainSep (foldl AbsorbBlock S (toBlocks A))
-
-XorBlock : State -> [128] -> State
-XorBlock [s0, s1, s2, s3, s4] (x0 # x1) = [s0 ^ reverse x0, s1 ^ reverse x1, s2, s3, s4]
-
-AbsorbBlock : State -> [128] -> State
-AbsorbBlock S X = Ascon_p`{8} (XorBlock S X)
-
-DomainSep : State -> State
-DomainSep [s0, s1, s2, s3, s4] = [s0, s1, s2, s3, s4 ^ 0b1 # 0]
-
-Ascon_AEAD128_IV : [64]
-Ascon_AEAD128_IV = 0x00001000808c0001

AsconHash.cry

@@ -1,56 +0,0 @@
-module AsconHash where
-
-import Ascon
-
-// 5. Hash and eXtendable-Output Functions (XOFs)
-
-Ascon_Digest : {n} (fin n) => [64] -> [n][64] -> [inf]
-Ascon_Digest IV Ms = join [reverse (head S) | S <- iterate Ascon_p`{12} Sn]
-    where
-    S0 = Ascon_p`{12} [IV, 0, 0, 0, 0]
-    Sn = foldl AbsorbBlock S0 Ms
-
-AbsorbBlock : State -> [64] -> State
-AbsorbBlock [s0, s1, s2, s3, s4] X = Ascon_p`{12} [reverse X ^ s0, s1, s2, s3, s4]
-
-/// 5.1. Specification of Ascon-Hash256
-Ascon_Hash256 : {n} (fin n) => [n] -> [256]
-Ascon_Hash256 M = take (Ascon_Digest Ascon_Hash256_IV (toBlocks M))
-
-Ascon_Hash256_IV : [64]
-Ascon_Hash256_IV = 0x0000080100cc0002
-
-Ascon_Hash256_bytes : {n} (fin n) => [n][8] -> [32][8]
-Ascon_Hash256_bytes M = map reverse (split (Ascon_Hash256 (join (map reverse M))))
-
-property
-  initial_value_works =
-    Ascon_p`{12} ([Ascon_Hash256_IV] # zero)
-      ==
-      [0x9b1e5494e934d681, 0x4bc3a01e333751d2, 0xae65396c6b34b81a, 0x3c7fd4a4d56a4db3, 0x1a5c464906c5976d]
-
-// 5.2. Specification of Ascon-XOF128
-
-Ascon_XOF128 : {r, n} (fin n, fin r) => [n] -> [r]
-Ascon_XOF128 M = take (Ascon_Digest Ascon_XOF128_IV (toBlocks M))
-
-Ascon_XOF128_IV : [64]
-Ascon_XOF128_IV = 0x0000080000cc0003
-
-Ascon_XOF128_bytes : {r, n} (fin n, fin r) => [n][8] -> [r][8]
-Ascon_XOF128_bytes M = map reverse (split (Ascon_XOF128 (join (map reverse M))))
-
-// 5.3. Specification of Ascon-CXOF128
-
-Ascon_CXOF128 : {r, c, n} (fin n, fin r, fin c, 64 >= width c) => [c] -> [n] -> [r]
-Ascon_CXOF128 Z M = take (Ascon_Digest Ascon_CXOF128_IV Ms)
-  where
-    Ms = [reverse `c]
-       # toBlocks Z
-       # toBlocks M
-
-Ascon_CXOF128_bytes : {r, z, n} (fin n, fin r, 61 >= width z) => [z][8] -> [n][8] -> [r][8]
-Ascon_CXOF128_bytes Z M = map reverse (split (Ascon_CXOF128 (join (map reverse Z)) (join (map reverse M))))
-
-Ascon_CXOF128_IV : [64]
-Ascon_CXOF128_IV = 0x0000080000cc0004

LICENSE

@@ -0,0 +1,13 @@
+Copyright 2025 Eric Mertens
+
+Permission to use, copy, modify, and/or distribute this software for any
+purpose with or without fee is hereby granted, provided that the above
+copyright notice and this permission notice appear in all copies.
+
+THE SOFTWARE IS PROVIDED “AS IS” AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *

Makefile

@@ -0,0 +1,21 @@
+.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
+
+test-hash256:
+	$(CRYPTOL) -c :exhaust TestAsconHash256.cry
+
+test-xof128:
+	$(CRYPTOL) -c :exhaust TestAsconXOF128.cry
+
+test-cxof128:
+	$(CRYPTOL) -c :exhaust TestAsconCXOF128.cry
+
+test-aead128:
+	$(CRYPTOL) -c :exhaust TestAsconAEAD128.cry
+
+saw-proofs:
+	$(SAW) verify.saw

TestAsconAEAD128.cry

@@ -1,12 +1,14 @@
 module TestAsconAEAD128 where
 
 import Ascon
-import AsconCipher
 
 testcase : {n, m} (fin m, fin n) => [128] -> [128] -> [8 * m] -> [8 * n] -> [8 * (m + 16)] -> Bit
-testcase K N P A C =
-    Ascon_AEAD128 (little_bytes K) (little_bytes N) (little_bytes A) (little_bytes P)
-    == little_bytes C
+testcase K N P A (C # T) =
+    AEAD128_encrypt_bytes (split K) (split N) (split A) (split P) == (split C, split T)
+    /\
+    case AEAD128_decrypt_bytes (split K) (split N) (split A) (split C) (split T) of
+      None -> False
+      Some p -> p == split P
 
 property
   test1 = testcase 0x000102030405060708090A0B0C0D0E0F 0x101112131415161718191A1B1C1D1E1F [] 0x 0x4F9C278211BEC9316BF68F46EE8B2EC6

TestAsconCXOF128.cry

@@ -1,9 +1,9 @@
 module TestAsconCXOF128 where
 
-import AsconHash
+import Ascon
 
 testcase : {r, z, n} (fin n, fin r, 61 >= width z) => [8*n] -> [8*z] -> [8*r] -> Bool
-testcase M Z D = join (Ascon_CXOF128_bytes (split Z) (split M)) == D
+testcase M Z D = CXOF128_bytes (split Z) (split M) == split D
 
 property
   test1 = testcase [] [] 0x4F50159EF70BB3DAD8807E034EAEBD44C4FA2CBBC8CF1F05511AB66CDCC529905CA12083FC186AD899B270B1473DC5F7EC88D1052082DCDFE69FB75D269E7B74

TestAsconHash256.cry

@@ -1,9 +1,9 @@
 module TestAsconHash256 where
 
-import AsconHash
+import Ascon
 
 testcase : {n} (fin n) => [8*n] -> [256] -> Bool
-testcase M D = join (Ascon_Hash256_bytes (split M)) == D
+testcase M D = Hash256_bytes (split M) == split D
 
 property
   test1 = testcase [] 0x0B3BE5850F2F6B98CAF29F8FDEA89B64A1FA70AA249B8F839BD53BAA304D92B2

TestAsconXOF128.cry

@@ -1,9 +1,9 @@
 module TestAsconXOF128 where
 
-import AsconHash
+import Ascon
 
 testcase : {r, n} (fin n, fin r) => [8*n] -> [8*r] -> Bool
-testcase M D = join (Ascon_XOF128_bytes (split M)) == D
+testcase M D = XOF128_bytes (split M) == split D
 
 property
   test1 = testcase [] 0x473D5E6164F58B39DFD84AACDB8AE42EC2D91FED33388EE0D960D9B3993295C6AD77855A5D3B13FE6AD9E6098988373AF7D0956D05A8F1665D2C67D1A3AD10FF

verify.saw

@@ -0,0 +1,13 @@
+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 : [0]) (P : [128]) ->
+        (T == T'
+        where
+        (C, T) = AEAD128_encrypt K N A P
+        (P', T') = AEAD128_decrypt_raw K N A C)
+    }};
+}));