From 51dbdbf415584b88bab5b38c5840052c6dd609c3 Mon Sep 17 00:00:00 2001
From: Eric Mertens <emertens@gmail.com>
Date: Thu, 4 Sep 2025 14:55:46 -0700
Subject: [PATCH] Documentation and improved bit-order treatment

---
 Ascon.cry            | 67 ++++++++++++++++++++++++++++++++++++++------
 AsconCipher.cry      | 32 +++++++++++++--------
 AsconHash.cry        | 12 ++++----
 Makefile             | 17 +++++++++++
 TestAsconAEAD128.cry |  3 +-
 TestAsconCXOF128.cry |  2 +-
 TestAsconHash256.cry |  2 +-
 TestAsconXOF128.cry  |  2 +-
 8 files changed, 105 insertions(+), 32 deletions(-)
 create mode 100644 Makefile

diff --git a/Ascon.cry b/Ascon.cry
index 710b9e7..5a1d609 100644
--- a/Ascon.cry
+++ b/Ascon.cry
@@ -16,38 +16,74 @@ module Ascon where
 // 2.1. Auxiliary Functions
 
 /// Parse function.
-parse : {r, n} (fin n, fin r, 0 < r) => [n] -> ([n/r][r], [n%r])
+///
+/// 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, n} (fin n, fin r, r >= 1) => [n] -> ([n/r][r], [n%r])
 parse (M_ # Ml) = (split M_, Ml)
 
 /// Padding rule.
+///
+/// The function pad(𝑋, 𝑟) appends the bit 1 to the bitstring 𝑋, followed
+/// bythe 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, n} (n < r, fin r) => [n] -> [r]
 pad M = M # 0b1 # 0
 
+/// Combination of parse and pad that splits a bitstring into a sequence
+/// of integers using Cryptol's native big-endian representation.
 toBlocks : {r, n} (r >= 1, fin r, fin n) => [n] -> [n / r + 1][r]
-toBlocks M = M1 # [pad M2]
+toBlocks M = map reverse (M1 # [pad M2])
   where
     (M1, M2) = parse M
 
 // 3. Ascon Permutations
 
-type constraint ValidRnd rnd = (1 <= rnd, rnd <= 16)
+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)
 
+/// Single round of the Ascon-p permutation.
 p : {rnd} (ValidRnd rnd) => State -> [64] -> State
 p S ci = pL (pS (pC S ci))
 
 // 3.1. Internal State
 
+/// 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
 
+/// 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. 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
+/// Table 5. The constants constᵢ to derive round constants of the Ascon
+/// permutations
 Const : [16][64]
 Const =
     [ 0x000000000000003c
@@ -80,10 +116,20 @@ SBox i = SBoxTable@i
 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
     ]
 
+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
+
 // 3.4. Linear Diffusion Layer pL
 
 pL : State -> State
@@ -98,5 +144,8 @@ pL [S0, S1, S2, S3, S4] =
         sigma : [64] -> [6] -> [6] -> [64]
         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))
+wordsToBits : {w,n} (fin w) => [n][w] -> [w*n]
+wordsToBits M = join (map reverse M)
+
+bitsToWords : {w,n} (fin w) => [w*n] -> [n][w]
+bitsToWords M = map reverse (split M)
diff --git a/AsconCipher.cry b/AsconCipher.cry
index befa7bc..2dfafaa 100644
--- a/AsconCipher.cry
+++ b/AsconCipher.cry
@@ -5,25 +5,27 @@ 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
+Ascon_AEAD128 K N A P = C # T
   where
-    Khi = reverse Khi_
-    Klo = reverse Klo_
-    Nhi = reverse Nhi_
-    Nlo = reverse Nlo_
+    // key and nonce as two 64-bit integers
+    [K0,K1] = bitsToWords K
+    [N0,N1] = bitsToWords N
 
-    S0 = Ascon_p`{12} [Ascon_AEAD128_IV, Khi, Klo, Nhi, Nlo]
-       ^ [0, 0, 0, Khi, Klo]
+    S0 = Ascon_p`{12} [Ascon_AEAD128_IV, K0, K1, N0, N1]
+       ^ [0, 0, 0, K0, K1]
     
     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])
+    C = take (join (map ExtractC SCs))
 
-    ST = Ascon_p`{12} (last SCs ^ [0, 0, Khi, Klo, 0])
-    T = ST@(4:[3]) # ST@(3:[3])
-      ^ Klo # Khi
+    ST = Ascon_p`{12} (last SCs ^ [0, 0, K0, K1, 0])
+    T = ExtractT ST ^ K
+
+Ascon_AEAD128_bytes : {a, p} (fin a, fin p) => [16][8] -> [16][8] -> [a][8] -> [p][8] -> [p + 16][8]
+Ascon_AEAD128_bytes K N A P =
+  bitsToWords (Ascon_AEAD128 (wordsToBits K) (wordsToBits N) (wordsToBits A) (wordsToBits P))
 
 AddAD : {a} (fin a) => State -> [a] -> State
 AddAD S A
@@ -31,7 +33,7 @@ AddAD S A
   | 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]
+XorBlock [s0, s1, s2, s3, s4] (xhi # xlo) = [s0 ^ xlo, s1 ^ xhi, s2, s3, s4]
 
 AbsorbBlock : State -> [128] -> State
 AbsorbBlock S X = Ascon_p`{8} (XorBlock S X)
@@ -39,5 +41,11 @@ 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]
 
+ExtractC : State -> [128]
+ExtractC [s0, s1, _, _, _] = wordsToBits [s0, s1]
+
+ExtractT : State -> [128]
+ExtractT [_, _, _, s3, s4] = wordsToBits [s3, s4]
+
 Ascon_AEAD128_IV : [64]
 Ascon_AEAD128_IV = 0x00001000808c0001
diff --git a/AsconHash.cry b/AsconHash.cry
index 8fcb264..23698d6 100644
--- a/AsconHash.cry
+++ b/AsconHash.cry
@@ -5,13 +5,13 @@ 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]
+Ascon_Digest IV Ms = wordsToBits [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]
+AbsorbBlock [s0, s1, s2, s3, s4] X = Ascon_p`{12} [X ^ s0, s1, s2, s3, s4]
 
 /// 5.1. Specification of Ascon-Hash256
 Ascon_Hash256 : {n} (fin n) => [n] -> [256]
@@ -21,7 +21,7 @@ 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))))
+Ascon_Hash256_bytes M = bitsToWords (Ascon_Hash256 (wordsToBits M))
 
 property
   initial_value_works =
@@ -38,19 +38,19 @@ 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))))
+Ascon_XOF128_bytes M = bitsToWords (Ascon_XOF128 (wordsToBits 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]
+    Ms = [`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_bytes Z M = bitsToWords (Ascon_CXOF128 (wordsToBits Z) (wordsToBits M))
 
 Ascon_CXOF128_IV : [64]
 Ascon_CXOF128_IV = 0x0000080000cc0004
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..fb007e3
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,17 @@
+.PHONY: test test-hash256 test-xof128 test-cxof128 test-aead128
+
+CRYPTOL ?= cryptol
+
+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
diff --git a/TestAsconAEAD128.cry b/TestAsconAEAD128.cry
index 6bcdb2e..68cc5bc 100644
--- a/TestAsconAEAD128.cry
+++ b/TestAsconAEAD128.cry
@@ -5,8 +5,7 @@ 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
+    Ascon_AEAD128_bytes (split K) (split N) (split A) (split P) == split C
 
 property
   test1 = testcase 0x000102030405060708090A0B0C0D0E0F 0x101112131415161718191A1B1C1D1E1F [] 0x 0x4F9C278211BEC9316BF68F46EE8B2EC6
diff --git a/TestAsconCXOF128.cry b/TestAsconCXOF128.cry
index 74ab4ab..2cda2ed 100644
--- a/TestAsconCXOF128.cry
+++ b/TestAsconCXOF128.cry
@@ -3,7 +3,7 @@ module TestAsconCXOF128 where
 import AsconHash
 
 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 = Ascon_CXOF128_bytes (split Z) (split M) == split D
 
 property
   test1 = testcase [] [] 0x4F50159EF70BB3DAD8807E034EAEBD44C4FA2CBBC8CF1F05511AB66CDCC529905CA12083FC186AD899B270B1473DC5F7EC88D1052082DCDFE69FB75D269E7B74
diff --git a/TestAsconHash256.cry b/TestAsconHash256.cry
index 6bb6e33..cff9f46 100644
--- a/TestAsconHash256.cry
+++ b/TestAsconHash256.cry
@@ -3,7 +3,7 @@ module TestAsconHash256 where
 import AsconHash
 
 testcase : {n} (fin n) => [8*n] -> [256] -> Bool
-testcase M D = join (Ascon_Hash256_bytes (split M)) == D
+testcase M D = Ascon_Hash256_bytes (split M) == split D
 
 property
   test1 = testcase [] 0x0B3BE5850F2F6B98CAF29F8FDEA89B64A1FA70AA249B8F839BD53BAA304D92B2
diff --git a/TestAsconXOF128.cry b/TestAsconXOF128.cry
index c8cba17..25aa5a0 100644
--- a/TestAsconXOF128.cry
+++ b/TestAsconXOF128.cry
@@ -3,7 +3,7 @@ module TestAsconXOF128 where
 import AsconHash
 
 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 = Ascon_XOF128_bytes (split M) == split D
 
 property
   test1 = testcase [] 0x473D5E6164F58B39DFD84AACDB8AE42EC2D91FED33388EE0D960D9B3993295C6AD77855A5D3B13FE6AD9E6098988373AF7D0956D05A8F1665D2C67D1A3AD10FF