diff --git a/Primitive/Keyless/Hash/HashInterface.cry b/Primitive/Keyless/Hash/HashInterface.cry index 7e36a78..70e027f 100644 --- a/Primitive/Keyless/Hash/HashInterface.cry +++ b/Primitive/Keyless/Hash/HashInterface.cry @@ -39,4 +39,4 @@ interface module Primitive::Keyless::Hash::HashInterface where * Hash function, mapping an arbitrary-length message to a fixed-length * message digest. */ - hash: {m} (width m < MessageUpperBound) => [m] -> [DigestLength] + hash: {m} (fin m, width m < MessageUpperBound) => [m] -> [DigestLength] diff --git a/Primitive/Keyless/Hash/SHA3/SHA3.cry b/Primitive/Keyless/Hash/SHA3/SHA3.cry index 0ad05ab..f060e18 100644 --- a/Primitive/Keyless/Hash/SHA3/SHA3.cry +++ b/Primitive/Keyless/Hash/SHA3/SHA3.cry @@ -30,6 +30,27 @@ parameter type digest : # type constraint (fin digest, digest % 8 == 0, digest >= 224, digest <= 512) +/** + * Length of the hash digest. + * + * This is made public to instantiate the `HashInterface`. + */ +type DigestLength = digest + +/** + * There is no upper bound on the message length for SHA3 hashes. + */ +type MessageUpperBound = inf + +/** + * Security strength (in bits) of the hash function. + * [FIPS-202] Appendix A.1, Table 4. + * @see Hash functions webpage: https://csrc.nist.gov/projects/hash-functions#security-strengths + * + * This is made public to instantiate the `HashInterface`. + */ +type SecurityStrength = DigestLength / 2 + /** * SHA-3 hash function specification. * [FIPS-202] Section 6.1.