From 4f5dab582202d273cf10523d7406e3caaca66718 Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Wed, 15 Jan 2025 14:42:40 -0500
Subject: [PATCH] sha3: instantiate `HashInterface` for SHA3 #98

Adds a `fin` constraint to the interface to support truly arbitrary
message lengths in SHA3.
---
 Primitive/Keyless/Hash/HashInterface.cry |  2 +-
 Primitive/Keyless/Hash/SHA3/SHA3.cry     | 21 +++++++++++++++++++++
 2 files changed, 22 insertions(+), 1 deletion(-)

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.