Merge pull request #115 from GaloisInc/110-sha2-parse

Add preprocessing for SHA2

Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry

@@ -0,0 +1,17 @@
+/**
+ * Secure hash algorithm SHA256.
+ *
+ * @copyright Galois, Inc
+ * @author Marcella Hastings <marcella@galois.com>
+ */
+module Primitive::Keyless::Hash::SHA2::Instantiations::SHA =
+    Primitive::Keyless::Hash::SHA2::Specification
+where
+    type w = 32
+
+    // Per [FIPS-180-4], these are the first 32 bits of the fractional
+    // parts of the square roots of the first 8 prime numbers.
+    H0 = [
+        0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a,
+        0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19
+    ]

Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry

@@ -0,0 +1,19 @@
+/**
+ * Secure hash algorithm SHA384.
+ *
+ * @copyright Galois, Inc
+ * @author Marcella Hastings <marcella@galois.com>
+ */
+module Primitive::Keyless::Hash::SHA2::Instantiations::SHA384 =
+    Primitive::Keyless::Hash::SHA2::Specification
+where
+    type w = 64
+
+    // Per [FIPS-180-4], these are the the first sixty-four bits of the
+    // fractional parts of the square roots of the 9th - 16th prime numbers.
+    H0 = [
+        0xcbbb9d5dc1059ed8, 0x629a292a367cd507,
+        0x9159015a3070dd17, 0x152fecd8f70e5939,
+        0x67332667ffc00b31, 0x8eb44a8768581511,
+        0xdb0c2e0d64f98fa7, 0x47b5481dbefa4fa4
+    ]

Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry

@@ -0,0 +1,19 @@
+/**
+ * Secure hash algorithm SHA512.
+ *
+ * @copyright Galois, Inc
+ * @author Marcella Hastings <marcella@galois.com>
+ */
+module Primitive::Keyless::Hash::SHA2::Instantiations::SHA512 =
+    Primitive::Keyless::Hash::SHA2::Specification
+where
+    type w = 64
+
+    // Per [FIPS-180-4], these are the the first sixty-four bits of the
+    // fractional parts of the square roots of the first 8 prime numbers.
+    H0 = [
+        0x6a09e667f3bcc908, 0xbb67ae8584caa73b,
+        0x3c6ef372fe94f82b, 0xa54ff53a5f1d36f1,
+        0x510e527fade682d1, 0x9b05688c2b3e6c1f,
+        0x1f83d9abfb41bd6b, 0x5be0cd19137e2179
+    ]

Primitive/Keyless/Hash/SHA2/Specification.cry

@@ -31,7 +31,26 @@ parameter
     type w : #
     type constraint (w % 32 == 0, 32 <= w, 64 >= w)
 
+    /**
+     * Initial hash value.
+     * These are defined in [FIPS-180-4] Section 5.3.
+     */
+    H0 : [8][w]
+
+/**
+ * Upper bound on the width of messages that can be processed.
+ * [FIPS-180-4] Section 1, Figure 1.
+ */
+type MaxMessageWidth = 2 * w
+type constraint ValidMessageLength L = width L < MaxMessageWidth
+
 private
+    /**
+     * Size of blocks of data used in hashing; denoted `m` in the spec.
+     * [FIPS-180-4] Section 1, Figure 1.
+     */
+    type BlockSize = 16 * w
+
     /**
      * Circular rotate left operation.
      * [FIPS-180-4] Section 2.2.2 and Section 3.2 #5.
@@ -193,3 +212,47 @@ private
         0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b,
         0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c,
         0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817]
+
+
+    /**
+     * Number of bits used to encode the length of the message for padding.
+     * [FIPS-180-4] Section 5.1.
+     */
+    type LengthBits = 2 * w
+    /**
+     * Number of blocks needed to hold the padded version of a message of length L.
+     * [FIPS-180-4] Section 5.1.
+     */
+    type NumBlocks L = (L + 1 + LengthBits) /^ BlockSize
+
+    /**
+     * Deterministically pad a message to a multiple of the block size.
+     *
+     * [FIPS-180-4] Section 5.1.1 and 5.1.2.
+     *
+     * The constraint is not explicitly noted in Section 5.1, but all
+     * messages to be hashed must not exceed the valid message length.
+     */
+    pad : {L} (ValidMessageLength L) => [L] -> [NumBlocks L * BlockSize]
+    pad M = M # 0b1 # zero # (`L : [LengthBits])
+
+    /**
+     * The example used to demonstrate padding in the spec works.
+     * [FIPS-180-4] Section 5.1.1 and Section 5.1.2.
+     * ```repl
+     * :prove paddingExampleWorks
+     * ```
+     */
+    paddingExampleWorks : Bool
+    paddingExampleWorks
+        | w == 32 => pad (join "abc") == (0b01100001 # 0b01100010 # 0b01100011
+            # 0b1 # (zero : [423]) # (zero : [59]) # 0b11000)
+        | w == 64 => pad (join "abc") == (0b01100001 # 0b01100010 # 0b01100011
+            # 0b1 # (zero : [871]) # (zero : [123]) # 0b11000)
+
+    /**
+     * The message and its padding must be parsed into `N` blocks.
+     * [FIPS-180-4] Section 5.2.
+     */
+    parse : {N} () => [N * BlockSize] -> [N][BlockSize]
+    parse M = split M