sha3: fix types to work with infinite output #132

Specifically, this allows callers of `SHAKE` functions to either specify
a concrete output lengths (if the needed length is known at call time)
or infinite length (if there's some additional processing before
truncating the output).

Primitive/Keyless/Hash/SHAKE/SHAKE128.cry

@@ -26,10 +26,12 @@ import Primitive::Keyless::Hash::utils (toBytes)
  * SHAKE128 extendable-output function.
  * [FIPS-202] Section 6.2.
  *
+ * This supports any output length `d`, including infinite length.
+ *
  * Note that the specification of `c` is above, in the instantiation of the
  * `keccak` module.
  */
-shake128 : {m, d} (fin m, fin d) => [m] -> [d]
+shake128 : {d, m} (fin m) => [m] -> [d]
 shake128 M = Keccak (M # 0b1111)
 
 /**

Primitive/Keyless/Hash/SHAKE/SHAKE256.cry

@@ -26,10 +26,12 @@ import Primitive::Keyless::Hash::utils (toBytes)
  * SHAKE256 extendable-output function.
  * [FIPS-202] Section 6.2.
  *
+ * This supports any output length `d`, including infinite length.
+ *
  * Note that the specification of `c` is above, in the instantiation of the
  * `keccak` module.
  */
-shake256: {m, d} (fin m, fin d) => [m] -> [d]
+shake256: {d, m} (fin m) => [m] -> [d]
 shake256 M = Keccak (M # 0b1111)
 
 /*

Primitive/Keyless/Hash/keccak.cry

@@ -61,9 +61,8 @@ parameter
  * with the specific functions for Keccak (Sec 5.2).
  * [FIPS-202] Section 4, Algorithm 8; instantiated as in Section 5.2.
  */
-Keccak : {m, d}
-    (fin m, fin d) => [m] -> [d]
-Keccak M = take`{d} (extend (Ss ! 0)) where
+Keccak : {d, m} (fin m) => [m] -> [d]
+Keccak M = take`{front=d, back=inf} (extend (Ss ! 0)) where
     // Step 1.
     P = M # pad `{x = r, m = m}
     // Step 2.