diff --git a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry
index ab536860..543bf43b 100644
--- a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry
+++ b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry
@@ -1,5 +1,6 @@
 /**
- * Secure hash algorithm SHA-256 as specified in [FIPS-180-4].
+ * Instantiation of the secure hash algorithm SHA-256 as specified in
+ * [FIPS-180-4], Section 5.3.3.
  *
  * @copyright Galois, Inc
  * @author Marcella Hastings <marcella@galois.com>
diff --git a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry
index 4440af4d..2d7c18e9 100644
--- a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry
+++ b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry
@@ -1,5 +1,6 @@
 /**
- * Secure hash algorithm SHA-384 as specified in [FIPS-180-4].
+ * Instantiation of the secure hash algorithm SHA-384 as specified in
+ * [FIPS-180-4], Section 5.3.4.
  *
  * @copyright Galois, Inc
  * @author Marcella Hastings <marcella@galois.com>
diff --git a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry
index 2e90fb6c..788ae712 100644
--- a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry
+++ b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry
@@ -1,5 +1,6 @@
 /**
- * Secure hash algorithm SHA-512 as specified in [FIPS-180-4].
+ * Instantiation of the secure hash algorithm SHA-512 as specified in
+ * [FIPS-180-4], Section 5.3.5.
  *
  * @copyright Galois, Inc
  * @author Marcella Hastings <marcella@galois.com>
diff --git a/Primitive/Keyless/Hash/SHA2/Specification.cry b/Primitive/Keyless/Hash/SHA2/Specification.cry
index db327492..76b39da2 100644
--- a/Primitive/Keyless/Hash/SHA2/Specification.cry
+++ b/Primitive/Keyless/Hash/SHA2/Specification.cry
@@ -26,7 +26,9 @@ parameter
     /**
      * Length of words, in bits, that are used during hashing.
      *
-     * The specification defines words to be either 32 or 64 bits.
+     * The specification defines words to be either 32 bits (for
+     * SHA-224 and SHA-256) or 64 bits (for SHA-384, SHA-512, and
+     * SHA-512/t for any valid `t`).
      * [FIPS-180-4] Section 1, Figure 1.
      */
     type w : #