Add byte-delimited API for SHA2 and SHA3

Primitive/Asymmetric/KEM/ML_KEM/Specification.cry

@@ -112,53 +112,38 @@ private
     /**
      * Pseudorandom function (PRF).
      * [FIPS-203] Section 4.1, Equations 4.2 and 4.3.
-     *
-     * The SHA3 API operates over bit streams; the `groupBy` and `join` calls
-     * convert to and from our byte arrays.
      */
     PRF : {eta} (2 <= eta, eta <= 3) => [32]Byte -> Byte -> [64 * eta]Byte
-    PRF s b = groupBy`{8} (SHAKE256::xof (join s # b))
+    PRF s b = SHAKE256::xofBytes`{8 * 64 * eta} (s # [b])
 
     /**
      * One of the hash functions used in the protocol.
      * [FIPS-203] Section 4.1, Equation 4.4.
-     *
-     * The SHA3 API operates over bit streams; the `groupBy` and `join` calls
-     * convert to and from our byte arrays.
      */
     H : {hinl} (fin hinl) => [hinl]Byte -> [32]Byte
-    H M = groupBy (SHA3_256::hash (join M))
+    H s = SHA3_256::hashBytes s
 
     /**
      * One of the hash functions used in the protocol.
      * [FIPS-203] Section 4.1, Equation 4.4.
-     *
-     * The SHA3 API operates over bit streams; the `groupBy` and `join` calls
-     * convert to and from our byte arrays.
      */
     J : {hinl} (fin hinl) => [hinl]Byte -> [32]Byte
-    J s = groupBy (SHAKE256::xof (join s))
+    J s = SHAKE256::xofBytes`{8 * 32} s
 
     /**
      * One of the hash functions used in the protocol.
      * [FIPS-203] Section 4.1, Equation 4.5.
-     *
-     * The SHA3 API operates over bit streams; the `groupBy` and `join` calls
-     * convert to and from our byte arrays.
      */
     G : {ginl} (fin ginl) => [ginl]Byte -> ([32]Byte, [32]Byte)
-    G M = (a, b) where
-        [a, b] = split`{2} (groupBy`{8} (SHA3_512::hash (join M)))
+    G c = (a, b) where
+        [a, b] = split (SHA3_512::hashBytes c)
 
     /**
      * eXtendable-Output Function (XOF) wrapper.
      * [FIPS-203] Section 4.1, Equation 4.6.
-     *
-     * The SHA3 API operates over bit streams; the `groupBy` and `join` calls
-     * convert to and from our byte arrays.
      */
     XOF : ([34]Byte) -> [inf]Byte
-    XOF(d) = groupBy (SHAKE128::xof (join d))
+    XOF = SHAKE128::xofBytes
 
     /**
      * Conversion from little-endian bit arrays to byte arrays.

Primitive/Asymmetric/Signature/XMSS/Instantiations/WOTSP_SHA2_256.cry

@@ -27,7 +27,7 @@ module Primitive::Asymmetric::Signature::XMSS::Instantiations::WOTSP_SHA2_256 =
         type n = 32
         type w = 16
 
-        F KEY M = split (SHA256::hash (join ((zero : [32][8]) # KEY # M)))
-        PRF KEY M = split (SHA256::hash (join ((zero : [31][8]) # [(3 : [8])] # KEY # M)))
+        F KEY M = SHA256::hashBytes ((zero : [32][8]) # KEY # M)
+        PRF KEY M = SHA256::hashBytes ((zero : [31][8]) # [(3 : [8])] # KEY # M)
 
 

Primitive/Keyless/Hash/SHA2/Specification.cry

@@ -39,9 +39,13 @@ parameter
      *
      * Allowable values for each word size `w` are defined in [FIPS-180-4]
      * Section 1, Figure 1.
+     *
+     * The spec does not explicitly require that the digest size is a multiple
+     * of 8, but all the allowable sizes are; adding this explicit constraint
+     * allows us to define a hash function that operates over bytes.
      */
     type DigestSize : #
-    type constraint (8 * w >= DigestSize)
+    type constraint (8 * w >= DigestSize, DigestSize % 8 == 0)
 
     /**
      * Initial hash value.
@@ -360,3 +364,13 @@ hash M = take (join (digest ! 0)) where
             c' = b
             b' = a
             a' = T1 + T2
+
+/**
+ * Secure hash function, computed over bytes.
+ *
+ * This is not explicitly part of the spec, but many applications represent
+ * their input and output over byte strings (rather than bit strings as used
+ * in the spec itself).
+ */
+hashBytes: {l} (ValidMessageLength (8 * l)) => [l][8] -> [DigestSize / 8][8]
+hashBytes M = groupBy`{8} (hash (join M))

Primitive/Keyless/Hash/SHA3/SHA3.cry

@@ -19,8 +19,16 @@ import Primitive::Keyless::Hash::Keccak where
     type c = 2 * digest
 
 parameter
-  type digest : #
-  type constraint (fin digest, digest >= 224, digest <= 512)
+    /**
+     * Digest length -- that is, the length of the output of the hash function.
+     *
+     * The spec allows the 5 FIPS-approved digest lengths : 160, 224, 256, 384,
+     * and 512 bits. The constraint here is looser than that requirement; the
+     * restriction that 8 divides the digest length is to allow the byte-wise
+     * `hashBytes` function.
+     */
+    type digest : #
+    type constraint (fin digest, digest % 8 == 0, digest >= 224, digest <= 512)
 
 /**
  * SHA-3 hash function specification.
@@ -48,7 +56,19 @@ sha3 M = Keccak`{d=digest} (M # 0b01)
  * from the bit ordering expected by `Keccak`. If input is provided in the
  * format described in [FIPS-202] Appendix B (a hex string with an even
  * number of digits and an actual length `n`), use the `KOB::truncate` function
- * to get the correct input:
+ * to get the correct input.
  */
 hash : {n} (fin n) => [n] -> [digest]
 hash M = KBO::reverseBitOrdering (Keccak`{d=digest} ((KBO::reverseBitOrdering M) # 0b01))
+
+/**
+ * SHA-3 hash function specification over byte-delimited inputs.
+ *
+ * This expects input and output in MSB order. It handles conversion to and
+ * from the bit ordering expected by `Keccak`. If input is provided in the
+ * format described in [FIPS-202] Appendix B (a hex string with an even
+ * number of digits and an actual length `n`), use the `KOB::truncate` function
+ * to get the correct input.
+ */
+hashBytes : {m} (fin m) => [m][8] -> [digest / 8][8]
+hashBytes M = split (hash (join M))

Primitive/Keyless/Hash/SHA3/Tests.cry

@@ -59,7 +59,10 @@ submodule SHA3_224 where
      * :prove t72
      * ```
      */
-    property t72 = SHA3_224::hash 0xb29373f6f8839bd498 == output where
+    property t72 = hashWorks && hashBytesWorks where
+        hashWorks = SHA3_224::hash input == output
+        hashBytesWorks = SHA3_224::hashBytes (split input) == split output
+        input = 0xb29373f6f8839bd498
         output = 0xe02a13fa4770f824bcd69799284878f19bfdc833ac6d865f28b757d0
 
     /**
@@ -111,15 +114,17 @@ submodule SHA3_256 where
     property t8 = SHA3_256::hash 0x6a ==
         0xf35e560e05de779f2669b9f513c2a7ab81dfeb100e2f4ee1fb17354bfa2740ca
 
-
     /**
      * This is from the bytewise tests.
      * ```repl
      * :prove t72
      * ```
      */
-    property t72 = SHA3_256::hash 0xfb8dfa3a132f9813ac ==
-        0xfd09b3501888445ffc8c3bb95d106440ceee469415fce1474743273094306e2e
+    property t72 = hashWorks && hashBytesWorks where
+        hashWorks = SHA3_256::hash input == output
+        hashBytesWorks = SHA3_256::hashBytes (split input) == split output
+        input = 0xfb8dfa3a132f9813ac
+        output = 0xfd09b3501888445ffc8c3bb95d106440ceee469415fce1474743273094306e2e
 
     /**
      * This is from the bitwise tests.
@@ -174,7 +179,10 @@ submodule SHA3_384 where
      * :prove t72
      * ```
      */
-    property t72 = SHA3_384::hash 0xa36e5a59043b6333d7 == output where
+    property t72 = hashWorks && hashBytesWorks where
+        hashWorks = SHA3_384::hash input == output
+        hashBytesWorks = SHA3_384::hashBytes (split input) == split output
+        input = 0xa36e5a59043b6333d7
         output = join [
             0xbd045661663436d07720ff3c8b6f922066dfe244456a56ca,
             0x46dfb3f7e271116d932107c7b04cc7c60173e08d0c2e107c
@@ -205,7 +213,10 @@ submodule SHA3_512 where
      * :prove t72
      * ```
      */
-    property t72 = SHA3_512::hash 0x3d6093966950abd846 == output where
+    property t72 = hashWorks && hashBytesWorks where
+        hashWorks = SHA3_512::hash input == output
+        hashBytesWorks = SHA3_512::hashBytes (split input) == split output
+        input = 0x3d6093966950abd846
         output = join [
             0x53e30da8b74ae76abf1f65761653ebfbe87882e9ea0ea564addd7cfd5a652457,
             0x8ad6be014d7799799ef5e15c679582b791159add823b95c91e26de62dcb74cfa

Primitive/Keyless/Hash/SHAKE/SHAKE128.cry

@@ -61,6 +61,17 @@ shake128 M = Keccak (M # 0b1111)
 xof : {d, m} (fin m) => [m] -> [d]
 xof M = KBO::reverseBitOrdering (Keccak ((KBO::reverseBitOrdering M) # 0b1111))
 
+/**
+ * SHAKE128 extendable-output function over byte-delimited inputs.
+ *
+ * Note that `d` is specified in _bits_. The `dBytes` parameter allows us to
+ * have infinite output. The alternative approach, requiring `d % 8 == 0`,
+ * is only possible when `d` is finite due to a type constraint on
+ * the mod operation.
+ */
+xofBytes : {d, m, dBytes} (fin m, dBytes * 8 == d) => [m][8] -> [dBytes][8]
+xofBytes M = split (xof (join M))
+
 /**
  * The CAVP test vectors provide input in MSB order as hex strings with an
  * even number of digits; each test is for a specific bit-length input.

Primitive/Keyless/Hash/SHAKE/SHAKE256.cry

@@ -61,6 +61,17 @@ shake256 M = Keccak (M # 0b1111)
 xof : {d, m} (fin m) => [m] -> [d]
 xof M = KBO::reverseBitOrdering (Keccak ((KBO::reverseBitOrdering M) # 0b1111))
 
+/**
+ * SHAKE256 extendable-output function over byte-delimited inputs.
+ *
+ * Note that `d` is specified in _bits_. The `dBytes` parameter allows us to
+ * have infinite output. The alternative approach, requiring `d % 8 == 0`,
+ * is only possible when `d` is finite due to a type constraint on
+ * the mod operation.
+ */
+xofBytes : {d, m, dBytes} (fin m, dBytes * 8 == d) => [m][8] -> [dBytes][8]
+xofBytes M = split (xof (join M))
+
 /**
  * ```repl
  * :prove k5