get the endianness working

Ascon.cry

@@ -13,6 +13,16 @@ https://doi.org/10.6028/NIST.SP.800-232
 */
 module Ascon where
 
+// 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)
+
+/// Padding rule.
+pad : {r, n} (n < r, fin r) => [n] -> [r]
+pad M = M # 0b1 # 0
+
 // 3. Ascon Permutations
 
 type constraint ValidRnd rnd = (1 <= rnd, rnd <= 16)

AsconHash256.cry

@@ -2,30 +2,28 @@ module AsconHash256 where
 
 import Ascon
 
-parse : {r, n} (fin n, fin r, 0 < r) => [n] -> ([n/r][r], [n%r])
-parse (M_ # Ml) = (split M_, Ml)
-
-pad : {n} (n < 64) => [n] -> [64]
-pad M = bs # b # zero
-  where
-    bs : [n/8*8]
-    b_ : [n%8]
-    bs # b_ = M
-    b : [8]
-    b = zext`{8} (0b1 # b_)
-
 /// 5.1. Specification of Ascon-Hash256
 Ascon_Hash256 : {n} (fin n) => [n] -> [256]
-Ascon_Hash256 M =
+Ascon_Hash256 M = join [reverse (head S) | S <- take (iterate Ascon_p`{12} Sn)]
-    join [LE (head S) | S <- take (iterate Ascon_p`{12} Sn)]
     where
     (M1, M2) = parse M
-    M2' = pad M2
+    M' = map reverse (M1 # [pad M2])
-    M' = M1 # [pad M2]
 
-    AddBlock [s0, s1, s2, s3, s4] X = Ascon_p`{12} [LE X ^ s0, s1, s2, s3, s4]
+    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]
     Sn = foldl AddBlock S0 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))))
+
+property
+  initial_value_works =
+    Ascon_p`{12} ([Ascon_Hash256_IV] # zero)
+      ==
+      [0x9b1e5494e934d681, 0x4bc3a01e333751d2, 0xae65396c6b34b81a, 0x3c7fd4a4d56a4db3, 0x1a5c464906c5976d]