Add XOF mode

AsconHash256.cry

@@ -2,23 +2,26 @@ module AsconHash256 where
 
 import Ascon
 
-/// 5.1. Specification of Ascon-Hash256
-Ascon_Hash256 : {n} (fin n) => [n] -> [256]
-Ascon_Hash256 M = join [reverse (head S) | S <- take (iterate Ascon_p`{12} Sn)]
+// 5. Hash and eXtendable-Output Functions (XOFs)
+
+Ascon_Digest : {n} (fin n) => [64] -> [n] -> [inf]
+Ascon_Digest IV M = join [reverse (head S) | S <- iterate Ascon_p`{12} Sn]
     where
     (M1, M2) = parse M
     M' = map reverse (M1 # [pad M2])
 
     AddBlock [s0, s1, s2, s3, s4] X = Ascon_p`{12} [X ^ s0, s1, s2, s3, s4]
-    S0 = Ascon_p`{12} [Ascon_Hash256_IV, 0, 0, 0, 0]
+    S0 = Ascon_p`{12} [IV, 0, 0, 0, 0]
     Sn = foldl AddBlock S0 M'
 
+
+/// 5.1. Specification of Ascon-Hash256
+Ascon_Hash256 : {n} (fin n) => [n] -> [256]
+Ascon_Hash256 M = take (Ascon_Digest Ascon_Hash256_IV M)
+
 Ascon_Hash256_IV : [64]
 Ascon_Hash256_IV = 0x0000080100cc0002
 
-little_bytes : {n} (fin n) => [8*n] -> [8*n]
-little_bytes M = join (map reverse (groupBy`{8} M))
-
 Ascon_Hash256_bytes : {n} (fin n) => [n][8] -> [32][8]
 Ascon_Hash256_bytes M = map reverse (split (Ascon_Hash256 (join (map reverse M))))
 
@@ -27,3 +30,21 @@ property
     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 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_IV : [64]
+Ascon_CXOF128_IV = 0x0000080000cc0004
+
+little_bytes : {n} (fin n) => [8*n] -> [8*n]
+little_bytes M = join (map reverse (groupBy`{8} M))