Unify into a single implementation file

Ascon.cry

@@ -48,11 +48,11 @@ type constraint ValidRnd rnd = rnd <= 16
 
 /// Core permutation function parameterized by a round count.
 Ascon_p : {rnd} (ValidRnd rnd) => State -> State
-Ascon_p S = foldl p`{rnd} S (drop`{back=rnd} Const)
+Ascon_p S = foldl round S (drop`{back=rnd} Const)
 
 /// Single round of the Ascon-p permutation.
-p : {rnd} (ValidRnd rnd) => State -> [64] -> State
-p S ci = pL (pS (pC S ci))
+round : State -> [64] -> State
+round S ci = pL (pS (pC S ci))
 
 // 3.1. Internal State
 
@@ -149,3 +149,151 @@ wordsToBits M = join (map reverse M)
 
 bitsToWords : {w,n} (fin w) => [w*n] -> [n][w]
 bitsToWords M = map reverse (split M)
+
+// 4. Authenticated Encryption Schema: Ascon-AEAD128
+
+/// Encryption using Ascon-AEAD128
+///
+/// Parameters:
+/// - Key
+/// - Nonce
+/// - Additional data
+/// - Plaintext
+///
+/// Returns:
+/// - Authenticated ciphertext
+AEAD128_encrypt : {a, p} (fin a, fin p) => [128] -> [128] -> [a] -> [p] -> [p + 128]
+AEAD128_encrypt K N A P = C # T
+  where
+    // key and nonce as two 64-bit integers
+    [K0,K1] = bitsToWords K
+    [N0,N1] = bitsToWords N
+
+    S0 = Ascon_p`{12} [Ascon_AEAD128_IV, K0, K1, N0, N1] ^ [0, 0, 0, K0, K1]
+    SA = AddAD S0 A
+
+    SCs = [XorBlock s p | s <- [SA] # map Ascon_p`{8} SCs | p <- toBlocks P]
+
+    C = take (join (map ExtractC SCs))
+
+    ST = Ascon_p`{12} (last SCs ^ [0, 0, K0, K1, 0])
+    T = ExtractT ST ^ K
+
+/// Decryption using Ascon-AEAD128
+///
+/// Parameters:
+/// - Key
+/// - Nonce
+/// - Additional data
+/// - Ciphertext
+///
+/// Returns:
+/// - Some plaintext on success
+/// - None when message authentication fails
+AEAD128_decrypt : {a, p} (fin a, fin p) => [128] -> [128] -> [a] -> [p + 128] -> Option [p]
+AEAD128_decrypt K N A (Cs_ # Cl # T) =
+  if T == T' then Some P else trace "P" P None
+  where
+    // key and nonce as two 64-bit integers
+    [K0,K1] = bitsToWords K
+    [N0,N1] = bitsToWords N
+
+    S0 = Ascon_p`{12} [Ascon_AEAD128_IV, K0, K1, N0, N1] ^ [0, 0, 0, K0, K1]
+    SA = AddAD S0 A
+
+    Cs = split`{p/128, 128} Cs_
+
+    SCs # [SCl] = [SA] # [Ascon_p`{8} (AssignC s c) | s <- SCs | c <- Cs]
+
+    Plmask # SCl' = ExtractC SCl
+    Sl' = AssignC SCl (Cl # (0b1#0 ^ SCl'))
+
+    Ps = zipWith (\x y -> ExtractC x ^ y) SCs Cs
+    Pl = Plmask ^ Cl
+    P = join Ps # Pl
+
+    ST = Ascon_p`{12} (Sl' ^ [0, 0, K0, K1, 0])
+    T' = ExtractT ST ^ K
+
+AEAD128_encrypt_bytes : {a, p} (fin a, fin p) => [16][8] -> [16][8] -> [a][8] -> [p][8] -> [p + 16][8]
+AEAD128_encrypt_bytes K N A P =
+  bitsToWords (AEAD128_encrypt (wordsToBits K) (wordsToBits N) (wordsToBits A) (wordsToBits P))
+
+AEAD128_decrypt_bytes : {a, p} (fin a, fin p) => [16][8] -> [16][8] -> [a][8] -> [p + 16][8] -> Option ([p][8])
+AEAD128_decrypt_bytes K N A C =
+  case AEAD128_decrypt (wordsToBits K) (wordsToBits N) (wordsToBits A) (wordsToBits C) of
+    None -> None
+    Some p -> Some (bitsToWords p)
+
+AddAD : {a} (fin a) => State -> [a] -> State
+AddAD S A
+    | a == 0 => DomainSep S
+    | a > 0  => DomainSep (foldl AbsorbBlock128 S (toBlocks A))
+
+DomainSep : State -> State
+DomainSep [s0, s1, s2, s3, s4] = [s0, s1, s2, s3, s4 ^ 0b1 # 0]
+
+AbsorbBlock128 : State -> [128] -> State
+AbsorbBlock128 S X = Ascon_p`{8} (XorBlock S X)
+
+XorBlock : State -> [128] -> State
+XorBlock [s0, s1, s2, s3, s4] (xhi # xlo) = [s0 ^ xlo, s1 ^ xhi, s2, s3, s4]
+
+ExtractC : State -> [128]
+ExtractC [s0, s1, _, _, _] = wordsToBits [s0, s1]
+
+AssignC : State -> [128] -> State
+AssignC [_, _, s2, s3, s4] C = bitsToWords C # [s2, s3, s4]
+
+ExtractT : State -> [128]
+ExtractT [_, _, _, s3, s4] = wordsToBits [s3, s4]
+
+Ascon_AEAD128_IV : [64]
+Ascon_AEAD128_IV = 0x00001000808c0001
+
+// 5. Hash and eXtendable-Output Functions (XOFs)
+
+hashBlocks : {n} (fin n) => [64] -> [n][64] -> [inf]
+hashBlocks IV Ms = wordsToBits [head S | S <- iterate Ascon_p`{12} Sn]
+    where
+    S0 = Ascon_p`{12} [IV, 0, 0, 0, 0]
+    Sn = foldl AbsorbBlock64 S0 Ms
+
+AbsorbBlock64 : State -> [64] -> State
+AbsorbBlock64 [s0, s1, s2, s3, s4] X = Ascon_p`{12} [X ^ s0, s1, s2, s3, s4]
+
+/// 5.1. Specification of Ascon-Hash256
+Hash256 : {n} (fin n) => [n] -> [256]
+Hash256 M = take (hashBlocks Hash256_IV (toBlocks M))
+
+Hash256_bytes : {n} (fin n) => [n][8] -> [32][8]
+Hash256_bytes M = bitsToWords (Hash256 (wordsToBits M))
+
+Hash256_IV : [64]
+Hash256_IV = 0x0000080100cc0002
+
+// 5.2. Specification of Ascon-XOF128
+
+XOF128 : {r, n} (fin n, fin r) => [n] -> [r]
+XOF128 M = take (hashBlocks XOF128_IV (toBlocks M))
+
+XOF128_bytes : {r, n} (fin n, fin r) => [n][8] -> [r][8]
+XOF128_bytes M = bitsToWords (XOF128 (wordsToBits M))
+
+XOF128_IV : [64]
+XOF128_IV = 0x0000080000cc0003
+
+// 5.3. Specification of Ascon-CXOF128
+
+CXOF128 : {r, c, n} (fin n, fin r, fin c, 64 >= width c) => [c] -> [n] -> [r]
+CXOF128 Z M = take (hashBlocks CXOF128_IV Ms)
+  where
+    Ms = [`c]
+       # toBlocks Z
+       # toBlocks M
+
+CXOF128_bytes : {r, z, n} (fin n, fin r, 61 >= width z) => [z][8] -> [n][8] -> [r][8]
+CXOF128_bytes Z M = bitsToWords (CXOF128 (wordsToBits Z) (wordsToBits M))
+
+CXOF128_IV : [64]
+CXOF128_IV = 0x0000080000cc0004