diff --git a/Primitive/Asymmetric/Signature/RSA_PSS.cry b/Primitive/Asymmetric/Signature/RSA_PSS.cry
index ac3ca891..d6a287b3 100644
--- a/Primitive/Asymmetric/Signature/RSA_PSS.cry
+++ b/Primitive/Asymmetric/Signature/RSA_PSS.cry
@@ -1,16 +1,16 @@
 /*
-   Copyright (c) 2021, Galois Inc.
-   www.cryptol.net
-*/
-
-/* This module implements an RSA signature scheme
-   with the EMSA-PSS encoding method described in 9.1 of
-
-   PKCS #1: RSA Cryptography Specifications Version 2.2
-
-   See also:
-   https://tools.ietf.org/html/rfc8017
-*/
+ * @copyright Galois Inc. 2021
+ * @author Andrei Stefanescu
+ * www.cryptol.net
+ *
+ * This module implements an RSA signature scheme
+ * with the EMSA-PSS encoding method described in 9.1 of
+ *
+ * PKCS #1: RSA Cryptography Specifications Version 2.2
+ *
+ * See also:
+ * https://tools.ietf.org/html/rfc8017
+ */
 module Primitive::Asymmetric::Signature::RSA_PSS where
 
 import Common::utils
@@ -19,10 +19,19 @@ parameter
   type hLen : # // Number of octets returned by chosen hash function
   type constraint (fin hLen, hLen >= 1)
 
-  hash : {n} (fin n) => [n][8] -> [8 * hLen]
+  /**
+   * Some hash functions have an upper bound on the message length they support.
+   *
+   * Most uses of `hash` here are on a fixed input made of 8 bytes of padding
+   * an `hLen`-byte hashed message, and an `hLen`-byte salt. The type constraint
+   * enforces that all such calls are on valid-length inputs.
+   */
+  type MessageUpperBound : #
+  type constraint (width (8 * (hLen + hLen + 8)) < MessageUpperBound)
 
+  hash : {n} (fin n, width (8 * n) < MessageUpperBound) => [n][8] -> [8 * hLen]
 
-MGF1 : {seedLen, maskLen} (fin seedLen, fin maskLen) => [seedLen][8] -> [maskLen][8]
+MGF1 : {seedLen, maskLen} (fin seedLen, fin maskLen, width (8 * seedLen + 32) < MessageUpperBound) => [seedLen][8] -> [maskLen][8]
 MGF1 seed = take (join [ split (hash (seed # (split c))) | c <- [(0 : [32]) ...] ])
 
 
diff --git a/Primitive/Asymmetric/Signature/RSA_PSS_SHA384.cry b/Primitive/Asymmetric/Signature/RSA_PSS_SHA384.cry
index 3d9fd833..0bff9bcd 100644
--- a/Primitive/Asymmetric/Signature/RSA_PSS_SHA384.cry
+++ b/Primitive/Asymmetric/Signature/RSA_PSS_SHA384.cry
@@ -6,8 +6,9 @@
 
 module Primitive::Asymmetric::Signature::RSA_PSS_SHA384 = Primitive::Asymmetric::Signature::RSA_PSS where
 
-import Primitive::Keyless::Hash::SHA2Imperative::SHA384
+import Primitive::Keyless::Hash::SHA2::Instantiations::SHA384 as SHA384
 
 type hLen = 48
-hash = SHAImp
+hash m = join (SHA384::hashBytes m)
+type MessageUpperBound = SHA384::MessageUpperBound
 
diff --git a/Primitive/Keyless/Hash/HMAC.cry b/Primitive/Keyless/Hash/HMAC.cry
index ae7a6617..78a3d749 100644
--- a/Primitive/Keyless/Hash/HMAC.cry
+++ b/Primitive/Keyless/Hash/HMAC.cry
@@ -10,7 +10,7 @@
 
 module Primitive::Keyless::Hash::HMAC where
 
-import Primitive::Keyless::Hash::SHA2Imperative::SHA384
+import Primitive::Keyless::Hash::SHA2Internal::SHA384
 
 // Pad or hash `key`, depending on its length, until it is 128 bytes long
 key_init : {key_size} (fin key_size) => [key_size][8] -> [128][8]
diff --git a/Primitive/Keyless/Hash/README.md b/Primitive/Keyless/Hash/README.md
index ea3edfbc..c5564395 100644
--- a/Primitive/Keyless/Hash/README.md
+++ b/Primitive/Keyless/Hash/README.md
@@ -1,4 +1,4 @@
-Hash functions.
+This directory includes executable specifications for several hash functions.
 
 | Scheme | [Gold standard](https://github.com/GaloisInc/cryptol-specs/wiki/Reviewing-guidelines)? | Literate |
 | --- | --- | --- |
@@ -9,3 +9,17 @@ Hash functions.
 | FNV | | No |
 | MD5 | | Yes |
 | SHA1 |  | No |
+
+## SHA2
+There are two versions of SHA2 here, as defined in [FIPS 180-4](https://doi.org/10.6028/NIST.FIPS.180-4). The [`SHA2`](/Primitive/Keyless/Hash/SHA2/) directory contains the spec-adherent version and should be used for the vast majority of applications.
+
+The [`SHA2Internal`](/Primitive/Keyless/Hash/SHA2Internal/) directory contains an equivalent implementation. It was originally written as part of a proof of correctness for a Java implementation of SHA2. It makes public several internal components of SHA2, like the compression function and the state representation, that are not part of the public interface defined in FIPS 180-4.
+These are used in the implementation of several other algorithms in this repo, like [HMAC](/Primitive/Keyless/Hash/HMAC.cry) and [SHACAL](/Primitive/Symmetric/Cipher/Block/SHACAL.cry). We've kept the two instantiations that these dependencies use and [checked equivalence of the two versions](SHA2Internal/Equivalence.cry) but recommend using the spec-adherent version where possible.
+
+## SHA3
+The SHA3 specification includes one internal algorithm, known as [Keccak](Keccak.cry), and two families of public interfaces: the hash functions [SHA3](SHA3/) and the extendable-output functions [SHAKE](SHAKE/).
+
+One quirk of the Keccak algorithm is that it assumes a particularly unusual bit ordering for the input. In practice, most applications do not want to rearrange inputs to match that bit ordering (indeed, the KATs provided by NIST are not provided with that ordering), so the default `hash` and `xof` functions for the `SHA3` and `SHAKE` algorithms take input in big-endian, or most-significant-bit first, ordering. For applications that have unusual bit-ordering needs, the [KeccakBitOrdering](KeccakBitOrdering.cry) module has helper functions to convert between various representations of bits.
+
+## HashInterface
+Some applications require an arbitrary hash function. The `HashInterface` provided is instantiated by both the `SHA2` and `SHA3` hashes.
diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA224.cry b/Primitive/Keyless/Hash/SHA2Imperative/SHA224.cry
deleted file mode 100644
index adf77f18..00000000
--- a/Primitive/Keyless/Hash/SHA2Imperative/SHA224.cry
+++ /dev/null
@@ -1,34 +0,0 @@
-/*
-   @copyright Galois Inc. 2018
-   @author Sean Weaver
-   @editor Sam Breese
-   www.cryptol.net
-*/
-
-module Primitive::Keyless::Hash::SHA2Imperative::SHA224 = Primitive::Keyless::Hash::SHA2Imperative::SHA where
-
-type wp = 32
-
-type digest_size = 224
-
-type j = 64
-
-H0 = [ 0xc1059ed8, 0x367cd507, 0x3070dd17, 0xf70e5939,
-       0xffc00b31, 0x68581511, 0x64f98fa7, 0xbefa4fa4]
-
-K = [ 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5,
-      0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174,
-      0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da,
-      0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967,
-      0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85,
-      0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070,
-      0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3,
-      0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2]
-
-SIGMA_0 x = (x >>> 2) ^ (x >>> 13) ^ (x >>> 22)
-
-SIGMA_1 x = (x >>> 6) ^ (x >>> 11) ^ (x >>> 25)
-
-sigma_0 x = (x >>> 7) ^ (x >>> 18) ^ (x >> 3)
-
-sigma_1 x = (x >>> 17) ^ (x >>> 19) ^ (x >> 10)
\ No newline at end of file
diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA512.cry b/Primitive/Keyless/Hash/SHA2Imperative/SHA512.cry
deleted file mode 100644
index 7f5dd8ff..00000000
--- a/Primitive/Keyless/Hash/SHA2Imperative/SHA512.cry
+++ /dev/null
@@ -1,47 +0,0 @@
-/*
-   @copyright Galois Inc. 2018
-   @author Sean Weaver
-   @editor Sam Breese
-   www.cryptol.net
-*/
-
-module Primitive::Keyless::Hash::SHA2Imperative::SHA512 = Primitive::Keyless::Hash::SHA2Imperative::SHA where
-
-type wp = 64
-
-type digest_size = 512
-
-type j = 80
-
-H0 = [ 0x6a09e667f3bcc908, 0xbb67ae8584caa73b, 0x3c6ef372fe94f82b, 0xa54ff53a5f1d36f1,
-       0x510e527fade682d1, 0x9b05688c2b3e6c1f, 0x1f83d9abfb41bd6b, 0x5be0cd19137e2179]
-
-K = [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc,
-      0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118,
-      0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2,
-      0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694,
-      0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65,
-      0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5,
-      0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4,
-      0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70,
-      0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df,
-      0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b,
-      0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30,
-      0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8,
-      0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8,
-      0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3,
-      0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec,
-      0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b,
-      0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178,
-      0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b,
-      0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c,
-      0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817]
-
-SIGMA_0 x = (x >>> 28) ^ (x >>> 34) ^ (x >>> 39)
-
-SIGMA_1 x = (x >>> 14) ^ (x >>> 18) ^ (x >>> 41)
-
-sigma_0 x = (x >>> 1) ^ (x >>> 8) ^ (x >> 7)
-
-sigma_1 x = (x >>> 19) ^ (x >>> 61) ^ (x >> 6)
-
diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA512_224.cry b/Primitive/Keyless/Hash/SHA2Imperative/SHA512_224.cry
deleted file mode 100644
index 6e26fe51..00000000
--- a/Primitive/Keyless/Hash/SHA2Imperative/SHA512_224.cry
+++ /dev/null
@@ -1,47 +0,0 @@
-/*
-   @copyright Galois Inc. 2018
-   @author Sean Weaver
-   @editor Sam Breese
-   www.cryptol.net
-*/
-
-module Primitive::Keyless::Hash::SHA2Imperative::SHA512_224 = Primitive::Keyless::Hash::SHA2Imperative::SHA where
-
-type wp = 64
-
-type digest_size = 224
-
-type j = 80
-
-H0 = [ 0x8c3d37c819544da2, 0x73e1996689dcd4d6, 0x1dfab7ae32ff9c82, 0x679dd514582f9fcf,
-       0x0f6d2b697bd44da8, 0x77e36f7304c48942, 0x3f9d85a86a1d36c8, 0x1112e6ad91d692a1]
-
-K = [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc,
-      0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118,
-      0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2,
-      0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694,
-      0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65,
-      0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5,
-      0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4,
-      0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70,
-      0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df,
-      0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b,
-      0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30,
-      0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8,
-      0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8,
-      0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3,
-      0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec,
-      0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b,
-      0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178,
-      0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b,
-      0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c,
-      0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817]
-
-SIGMA_0 x = (x >>> 28) ^ (x >>> 34) ^ (x >>> 39)
-
-SIGMA_1 x = (x >>> 14) ^ (x >>> 18) ^ (x >>> 41)
-
-sigma_0 x = (x >>> 1) ^ (x >>> 8) ^ (x >> 7)
-
-sigma_1 x = (x >>> 19) ^ (x >>> 61) ^ (x >> 6)
-
diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA512_256.cry b/Primitive/Keyless/Hash/SHA2Imperative/SHA512_256.cry
deleted file mode 100644
index ff33291e..00000000
--- a/Primitive/Keyless/Hash/SHA2Imperative/SHA512_256.cry
+++ /dev/null
@@ -1,47 +0,0 @@
-/*
-   @copyright Galois Inc. 2018
-   @author Sean Weaver
-   @editor Sam Breese
-   www.cryptol.net
-*/
-
-module Primitive::Keyless::Hash::SHA2Imperative::SHA512_256 = Primitive::Keyless::Hash::SHA2Imperative::SHA where
-
-type wp = 64
-
-type digest_size = 256
-
-type j = 80
-
-H0 = [ 0x22312194fc2bf72c, 0x9f555fa3c84c64c2, 0x2393b86b6f53b151, 0x963877195940eabd,
-       0x96283ee2a88effe3, 0xbe5e1e2553863992, 0x2b0199fc2c85b8aa, 0x0eb72ddc81c52ca2]
-
-K = [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc,
-      0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118,
-      0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2,
-      0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694,
-      0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65,
-      0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5,
-      0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4,
-      0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70,
-      0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df,
-      0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b,
-      0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30,
-      0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8,
-      0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8,
-      0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3,
-      0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec,
-      0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b,
-      0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178,
-      0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b,
-      0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c,
-      0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817]
-
-SIGMA_0 x = (x >>> 28) ^ (x >>> 34) ^ (x >>> 39)
-
-SIGMA_1 x = (x >>> 14) ^ (x >>> 18) ^ (x >>> 41)
-
-sigma_0 x = (x >>> 1) ^ (x >>> 8) ^ (x >> 7)
-
-sigma_1 x = (x >>> 19) ^ (x >>> 61) ^ (x >> 6)
-
diff --git a/Primitive/Keyless/Hash/SHA2Internal/Equivalence.cry b/Primitive/Keyless/Hash/SHA2Internal/Equivalence.cry
new file mode 100644
index 00000000..f521a958
--- /dev/null
+++ b/Primitive/Keyless/Hash/SHA2Internal/Equivalence.cry
@@ -0,0 +1,52 @@
+/**
+ * Properties demonstrating equivalence of the spec-adherent `SHA2`
+ * implementation and the alternative `SHA2Internal` implementation.
+ *
+ * @copyright Galois, Inc.
+ * @author Marcella Hastings <marcella@galois.com>
+ */
+import Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 as SHA_256
+import Primitive::Keyless::Hash::SHA2Internal::SHA256 as SHAI_256
+
+import Primitive::Keyless::Hash::SHA2::Instantiations::SHA384 as SHA_384
+import Primitive::Keyless::Hash::SHA2Internal::SHA384 as SHAI_384
+
+/**
+ * The `internal` version of SHA256 matches the spec-adherent version.
+ * ```repl
+ * :exhaust sha256ImplsAreEquivalent`{10}
+ * :check sha256ImplsAreEquivalent`{256}
+ * ```
+ */
+sha256ImplsAreEquivalent : {m} (fin m, width m < SHA_256::MessageUpperBound) => [m] -> Bit
+property sha256ImplsAreEquivalent m = SHA_256::hash m == SHAI_256::sha m
+
+/**
+ * The byte-wise APIs for the two SHA256 implementations match.
+ * ```repl
+ * :exhaust sha256BytewiseImplsAreEquivalent`{1}
+ * :check sha256BytewiseImplsAreEquivalent`{256}
+ * ```
+ */
+sha256BytewiseImplsAreEquivalent : {m} (fin m, width (8 * m) < SHA_256::MessageUpperBound) => [m][8] -> Bit
+property sha256BytewiseImplsAreEquivalent m = join (SHA_256::hashBytes m) == SHAI_256::SHAImp m
+
+/**
+ * The `internal` version of SHA384 matches the spec-adherent version.
+ * ```repl
+ * :exhaust sha384ImplsAreEquivalent`{10}
+ * :check sha384ImplsAreEquivalent`{256}
+ * ```
+ */
+sha384ImplsAreEquivalent : {m} (fin m, width m < SHA_384::MessageUpperBound) => [m] -> Bit
+property sha384ImplsAreEquivalent m = SHA_384::hash m == SHAI_384::sha m
+
+/**
+ * The byte-wise APIs for the two SHA384 implementations match.
+ * ```repl
+ * :exhaust sha384BytewiseImplsAreEquivalent`{1}
+ * :check sha384BytewiseImplsAreEquivalent`{256}
+ * ```
+ */
+sha384BytewiseImplsAreEquivalent : {m} (fin m, width (8 * m) < SHA_384::MessageUpperBound) => [m][8] -> Bit
+property sha384BytewiseImplsAreEquivalent m = join (SHA_384::hashBytes m) == SHAI_384::SHAImp m
diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA.cry b/Primitive/Keyless/Hash/SHA2Internal/SHA.cry
similarity index 99%
rename from Primitive/Keyless/Hash/SHA2Imperative/SHA.cry
rename to Primitive/Keyless/Hash/SHA2Internal/SHA.cry
index 01f50e3e..3c0176a4 100644
--- a/Primitive/Keyless/Hash/SHA2Imperative/SHA.cry
+++ b/Primitive/Keyless/Hash/SHA2Internal/SHA.cry
@@ -17,7 +17,7 @@ www.cryptol.net
     @see https://doi.org/10.6028/NIST.SP.800-107r1.
 */
 
-module Primitive::Keyless::Hash::SHA2Imperative::SHA where
+module Primitive::Keyless::Hash::SHA2Internal::SHA where
 
 import Array
 import Common::ByteArray
diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA256.cry b/Primitive/Keyless/Hash/SHA2Internal/SHA256.cry
similarity index 92%
rename from Primitive/Keyless/Hash/SHA2Imperative/SHA256.cry
rename to Primitive/Keyless/Hash/SHA2Internal/SHA256.cry
index 6a95efcb..969af110 100644
--- a/Primitive/Keyless/Hash/SHA2Imperative/SHA256.cry
+++ b/Primitive/Keyless/Hash/SHA2Internal/SHA256.cry
@@ -7,7 +7,7 @@
    www.cryptol.net
 */
 
-module Primitive::Keyless::Hash::SHA2Imperative::SHA256 = Primitive::Keyless::Hash::SHA2Imperative::SHA where
+module Primitive::Keyless::Hash::SHA2Internal::SHA256 = Primitive::Keyless::Hash::SHA2Internal::SHA where
 
 type wp = 32
 
diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA384.cry b/Primitive/Keyless/Hash/SHA2Internal/SHA384.cry
similarity index 95%
rename from Primitive/Keyless/Hash/SHA2Imperative/SHA384.cry
rename to Primitive/Keyless/Hash/SHA2Internal/SHA384.cry
index d572176b..138b286f 100644
--- a/Primitive/Keyless/Hash/SHA2Imperative/SHA384.cry
+++ b/Primitive/Keyless/Hash/SHA2Internal/SHA384.cry
@@ -5,7 +5,7 @@
    www.cryptol.net
 */
 
-module Primitive::Keyless::Hash::SHA2Imperative::SHA384 = Primitive::Keyless::Hash::SHA2Imperative::SHA where
+module Primitive::Keyless::Hash::SHA2Internal::SHA384 = Primitive::Keyless::Hash::SHA2Internal::SHA where
 
 type wp = 64
 
diff --git a/Primitive/Symmetric/Cipher/Block/SHACAL.cry b/Primitive/Symmetric/Cipher/Block/SHACAL.cry
index 6d551318..e52e9812 100644
--- a/Primitive/Symmetric/Cipher/Block/SHACAL.cry
+++ b/Primitive/Symmetric/Cipher/Block/SHACAL.cry
@@ -14,7 +14,7 @@
 
 module Primitive::Symmetric::Cipher::Block::SHACAL where
 
-import Primitive::Keyless::Hash::SHA2Imperative::SHA256
+import Primitive::Keyless::Hash::SHA2Internal::SHA256
 import Primitive::Keyless::Hash::SHA1
 
 /**SHACAL1**/
diff --git a/Primitive/Symmetric/KDF/HKDF.md b/Primitive/Symmetric/KDF/HKDF.md
index 38cb49b3..4c0ab2d1 100644
--- a/Primitive/Symmetric/KDF/HKDF.md
+++ b/Primitive/Symmetric/KDF/HKDF.md
@@ -1,3 +1,7 @@
+<!---
+ - @copyright Galois, Inc.
+ - @author Aaron Tomb
+ --->
 # HMAC-based Extract-and-Expand Key Derivation Function (HKDF)
 
 ## Welcome
@@ -88,7 +92,7 @@ parameter
     type constraint validHMACSizes KeyLen MsgLen =
       ( fin KeyLen, fin MsgLen
           , 32 >= width MsgLen
-          , 64 >= width (8 * KeyLen)
+          , 64 > width (8 * KeyLen)
           , 64 >= width (8 * 64 + MsgLen))
 
 
diff --git a/Primitive/Symmetric/KDF/HKDF256.cry b/Primitive/Symmetric/KDF/HKDF256.cry
index 3e42f16f..724cc09b 100644
--- a/Primitive/Symmetric/KDF/HKDF256.cry
+++ b/Primitive/Symmetric/KDF/HKDF256.cry
@@ -1,12 +1,15 @@
-module Primitive::Symmetric::KDF::HKDF256 = Primitive::Symmetric::KDF::HKDF where
-
-import Primitive::Symmetric::MAC::HMAC
-
-type HashLen = 32
-HMAC = hmacBytes
-
-hmacBytes : {n, m} (64 >= width (8 * (64 + m)),
-                    64 >= width (8 * n), 32 >= width m, fin m, fin n) =>
-              [n][8] -> [m][8] -> [32][8]
-hmacBytes key msg = split (hmacSHA256 key msg)
-
+/**
+ * @copyright Galois, Inc
+ * @author Aaron Tomb
+ */
+module Primitive::Symmetric::KDF::HKDF256 = Primitive::Symmetric::KDF::HKDF where
+
+import Primitive::Symmetric::MAC::HMAC
+
+type HashLen = 32
+HMAC = hmacBytes
+
+hmacBytes : {n, m} (64 >= width (8 * (64 + m)),
+                    64 > width (8 * n), 32 >= width m, fin m, fin n) =>
+            [n][8] -> [m][8] -> [32][8]
+hmacBytes key msg = split (hmacSHA256 key msg)
diff --git a/Primitive/Symmetric/MAC/HMAC.cry b/Primitive/Symmetric/MAC/HMAC.cry
index f4802e3a..80effc5f 100644
--- a/Primitive/Symmetric/MAC/HMAC.cry
+++ b/Primitive/Symmetric/MAC/HMAC.cry
@@ -7,16 +7,16 @@
 
 module Primitive::Symmetric::MAC::HMAC where
 
-import Primitive::Keyless::Hash::SHA2Imperative::SHA256
+import Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 as SHA256
 
 //////// Functional version ////////
 
-sha256Wrap msg = sha (join msg)
+sha256Wrap msg = SHA256::hash (join msg)
 
 hmacSHA256 : {pwBytes, msgBytes}
              (fin pwBytes, fin msgBytes
              , 32 >= width msgBytes
-             , 64 >= width (8*pwBytes)
+             , 64 > width (8*pwBytes)
              , 64 >= width (8 * (64 + msgBytes))
              ) => [pwBytes][8] -> [msgBytes][8] -> [256]
 hmacSHA256 = hmac `{blockLength=64} sha256Wrap sha256Wrap sha256Wrap
@@ -50,7 +50,18 @@ hmac hash hash2 hash3 key message = hash2 (okey # internal)
    ikey = [k ^ 0x36 | k <- ks]
    internal = split (hash (ikey # message))
 
-
+/**
+ * Test vector from NIST's CAVP program.
+ * @see https://csrc.nist.gov/projects/cryptographic-algorithm-validation-program/message-authentication#Testing
+ * ```repl
+ * :prove cavpTest30
+ * ```
+ */
+property cavpTest30 = digest == expected_digest where
+  key = split 0x9779d9120642797f1747025d5b22b7ac607cab08e1758f2f3a46c8be1e25c53b8c6a8f58ffefa176
+  msg = split 0xb1689c2591eaf3c9e66070f8a77954ffb81749f1b00346f9dfe0b2ee905dcc288baf4a92de3f4001dd9f44c468c3d07d6c6ee82faceafc97c2fc0fc0601719d2dcd0aa2aec92d1b0ae933c65eb06a03c9c935c2bad0459810241347ab87e9f11adb30415424c6c7f5f22a003b8ab8de54f6ded0e3ab9245fa79568451dfa258e
+  expected_digest = 0x769f00d3e6a6cc1fb426a14a4f76c6462e6149726e0dee0ec0cf97a16605ac8b
+  digest = hmacSHA256 key msg