sha2: add instantiations + tests for 384, 512 #112

- fixes a bug in the truncation (came from the wrong end)

Primitive/Keyless/Hash/SHA2/Specification.cry

@@ -290,7 +290,7 @@ private
     type LetterVars = ([w], [w], [w], [w], [w], [w], [w], [w])
 
 hash: {l} (ValidMessageLength l) => [l] -> [DigestSize]
-hash M = drop (join (digest ! 0)) where
+hash M = take (join (digest ! 0)) where
     digest = [H0] # [Hi
         where
             // Step 1. Prepare the message schedule.

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

@@ -0,0 +1,48 @@
+import Primitive::Keyless::Hash::SHA2::Instantiations::SHA384 as SHA384
+
+/**
+ * ```repl
+ * :prove abcWorks
+ * ```
+ */
+property abcWorks = SHA384::hash (join "abc") == output where
+    output = join [
+        0xcb00753f45a35e8b, 0xb5a03d699ac65007, 0x272c32ab0eded163,
+        0x1a8b605a43ff5bed, 0x8086072ba1e7cc23, 0x58baeca134c825a7
+    ]
+
+
+/**
+ * ```repl
+ * :prove emptyStringWorks
+ * ```
+ */
+property emptyStringWorks = SHA384::hash [] == output where
+    output = join [
+        0x38b060a751ac9638, 0x4cd9327eb1b1e36a, 0x21fdb71114be0743,
+        0x4c0cc7bf63f6e1da, 0x274edebfe76f65fb, 0xd51ad2f14898b95b
+    ]
+
+/**
+ * ```repl
+ * :prove alphabet448
+ * ```
+ */
+property alphabet448 = SHA384::hash input == output where
+    input = join "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
+    output = join [
+        0x3391fdddfc8dc739, 0x3707a65b1b470939, 0x7cf8b1d162af05ab,
+        0xfe8f450de5f36bc6, 0xb0455a8520bc4e6f, 0x5fe95b1fe3c8452b
+    ]
+
+/**
+ * ```repl
+ * :prove alphabet896
+ * ```
+ */
+property alphabet896 = SHA384::hash input == output where
+    input = join "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
+    output = join [
+        0x09330c33f71147e8, 0x3d192fc782cd1b47, 0x53111b173b3b05d2,
+        0x2fa08086e3b0f712, 0xfcc7c71a557e2db9, 0x66c3e9fa91746039
+    ]

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

@@ -0,0 +1,52 @@
+import Primitive::Keyless::Hash::SHA2::Instantiations::SHA512 as SHA512
+
+/**
+ * ```repl
+ * :prove abcWorks
+ * ```
+ */
+property abcWorks = SHA512::hash (join "abc") == output where
+    output = join [
+        0xddaf35a193617aba, 0xcc417349ae204131, 0x12e6fa4e89a97ea2,
+        0x0a9eeee64b55d39a, 0x2192992a274fc1a8, 0x36ba3c23a3feebbd,
+        0x454d4423643ce80e, 0x2a9ac94fa54ca49f
+    ]
+
+
+/**
+ * ```repl
+ * :prove emptyStringWorks
+ * ```
+ */
+property emptyStringWorks = SHA512::hash [] == output where
+    output = join [
+        0xcf83e1357eefb8bd, 0xf1542850d66d8007, 0xd620e4050b5715dc,
+        0x83f4a921d36ce9ce, 0x47d0d13c5d85f2b0, 0xff8318d2877eec2f,
+        0x63b931bd47417a81, 0xa538327af927da3e
+    ]
+
+/**
+ * ```repl
+ * :prove alphabet448
+ * ```
+ */
+property alphabet448 = SHA512::hash input == output where
+    input = join "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
+    output = join [
+        0x204a8fc6dda82f0a, 0x0ced7beb8e08a416, 0x57c16ef468b228a8,
+        0x279be331a703c335, 0x96fd15c13b1b07f9, 0xaa1d3bea57789ca0,
+        0x31ad85c7a71dd703, 0x54ec631238ca3445
+    ]
+
+/**
+ * ```repl
+ * :prove alphabet896
+ * ```
+ */
+property alphabet896 = SHA512::hash input == output where
+    input = join "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
+    output = join [
+        0x8e959b75dae313da, 0x8cf4f72814fc143f, 0x8f7779c6eb9f7fa1,
+        0x7299aeadb6889018, 0x501d289e4900f7e4, 0x331b99dec4b5433a,
+        0xc7d329eeb6dd2654, 0x5e96e55b874be909
+    ]