sha3: add copyright notices #132

Primitive/Asymmetric/Signature/DSA/p2048_q224.cry

@@ -1,3 +1,10 @@
+/*
+ * DSA instantiated with SHA-1 and SHA-3.
+ *
+ * @copyright Galois, Inc
+ * @author Ajay Kumar Eeralla
+ *
+ */
 module Primitive::Asymmetric::Signature::DSA::p2048_q224=
     Primitive::Asymmetric::Signature::DSA::DSA where
 import Common::utils

Primitive/Keyless/Hash/SHA3/SHA3.cry

@@ -1,3 +1,16 @@
+/*
+ * SHA-3 hash function, as specified in [FIPS-202].
+ *
+ * [FIPS-202]: National Institute of Standards and Technology. SHA-3 Standard:
+ *     Permutation-Based Hash and Extendable-Output Functions. (Department of
+ *     Commerce, Washington, D.C.), Federal Information Processing Standards
+ *     Publication (FIPS) NIST FIPS 202. August 2015.
+ *     @see https://dx.doi.org/10.6028/NIST.FIPS.202
+ *
+ * @copyright Galois, Inc.
+ * @author Ajay Kumar Eeralla
+ * @editor Marcella Hastings <[email protected]>
+ */
 module Primitive::Keyless::Hash::SHA3::SHA3 where
 import Primitive::Keyless::Hash::keccak where
     type b = 1600
@@ -8,5 +21,12 @@ parameter
   type digest : #
   type constraint (fin digest, digest >= 224, digest <= 512)
 
+/**
+ * SHA-3 hash function specification.
+ * [FIPS-202] Section 6.1.
+ *
+ * Note that the specification of `c` is above, in the instantiation of the
+ * `keccak` module.
+ */
 sha3 : {n} (fin n) => [n] -> [digest]
 sha3 M = Keccak`{d=digest} (M # 0b01)

Primitive/Keyless/Hash/SHA3/SHA3_224.cry

@@ -1,10 +1,9 @@
+/**
+ * Instantiation of SHA3-224.
+ *
+ * @copyright Galois Inc.
+ * @author Ajay Kumar Eeralla
+ */
 module Primitive::Keyless::Hash::SHA3::SHA3_224 =
-       Primitive::Keyless::Hash::SHA3::SHA3
-where
-
-type digest = 224
-
-
-
-
-
+    Primitive::Keyless::Hash::SHA3::SHA3 where
+        type digest = 224

Primitive/Keyless/Hash/SHA3/SHA3_256.cry

@@ -1,6 +1,9 @@
+/**
+ * Instantiation of SHA3-256.
+ *
+ * @copyright Galois Inc.
+ * @author Ajay Kumar Eeralla
+ */
 module Primitive::Keyless::Hash::SHA3::SHA3_256 =
-       Primitive::Keyless::Hash::SHA3::SHA3
-where
-  type digest = 256
-
-
+    Primitive::Keyless::Hash::SHA3::SHA3 where
+        type digest = 256

Primitive/Keyless/Hash/SHA3/SHA3_384.cry

@@ -1,8 +1,9 @@
+/**
+ * Instantiation of SHA3-384.
+ *
+ * @copyright Galois Inc.
+ * @author Ajay Kumar Eeralla
+ */
 module Primitive::Keyless::Hash::SHA3::SHA3_384 =
-       Primitive::Keyless::Hash::SHA3::SHA3
-where
-
-type digest = 384
-
-
-
+    Primitive::Keyless::Hash::SHA3::SHA3 where
+        type digest = 384

Primitive/Keyless/Hash/SHA3/SHA3_512.cry

@@ -1,7 +1,9 @@
+/**
+ * Instantiation of SHA3-512.
+ *
+ * @copyright Galois Inc.
+ * @author Ajay Kumar Eeralla
+ */
 module Primitive::Keyless::Hash::SHA3::SHA3_512 =
-       Primitive::Keyless::Hash::SHA3::SHA3
-  where
-
-type digest = 512
-
-
+    Primitive::Keyless::Hash::SHA3::SHA3 where
+        type digest = 512

Primitive/Keyless/Hash/SHA3/Tests.cry

@@ -1,59 +1,122 @@
+/*
+ * Tests of the SHA3 hash functions.
+ *
+ * Test vectors drawn from the NIST Cryptographic Standards and Guidelines
+ * example values.
+ * https://csrc.nist.gov/projects/cryptographic-standards-and-guidelines/example-values
+ *
+ * @copyright Galois Inc.
+ * @author Ajay Kumar Eeralla
+ * @editor Iavor Diatchki <[email protected]>
+ * @editor Marcella Hastings <[email protected]>
+ */
 module Primitive::Keyless::Hash::SHA3::Tests where
 
 import Primitive::Keyless::Hash::utils
 
-// Test vectors from
-// https://csrc.nist.gov/projects/cryptographic-standards-and-guidelines/example-values#aHashing
-
-
 submodule SHA3_224 where
   import Primitive::Keyless::Hash::SHA3::SHA3_224
 
+  /*
+   * ```repl
+   * :prove t1
+   * ```
+   */
   property t1 = join (toBytes (sha3 [])) ==
     0x6b4e03423667dbb73b6e15454f0eb1abd4597f9a1b078e3f5b5a6bc7
 
+  /*
+   * ```repl
+   * :prove t2
+   * ```
+   */
   property t2 = join (toBytes (sha3 0b11001)) ==
     0xffbad5da96bad71789330206dc6768ecaeb1b32dca6b3301489674ab
 
   msg1600 : [1600]
   msg1600 = join [ 0b11000101 | _ <- zero : [200] ]
 
+  /*
+   * ```repl
+   * :prove t3
+   * ```
+   */
   property t3 = join (toBytes (sha3 msg1600)) ==
     0x9376816aba503f72f96ce7eb65ac095deee3be4bf9bbc2a1cb7e11e0
 
+  /*
+   * ```repl
+   * :prove t4
+   * ```
+   */
   property t4 = join (toBytes (sha3 (msg1600 # 0b11000))) ==
     0x22d2f7bb0b173fd8c19686f9173166e3ee62738047d7eadd69efb228
 
 
 submodule SHA3_256 where
   import Primitive::Keyless::Hash::SHA3::SHA3_256
 
+  /*
+   * ```repl
+   * :prove t1
+   * ```
+   */
   property t1 = join (toBytes (sha3 [])) ==
     0xa7ffc6f8bf1ed76651c14756a061d662f580ff4de43b49fa82d80a4b80f8434a
 
+  /*
+   * ```repl
+   * :prove t2
+   * ```
+   */
   property t2 = join (toBytes (sha3 0b11001)) ==
     0x7b0047cf5a456882363cbf0fb05322cf65f4b7059a46365e830132e3b5d957af
 
+  /*
+   * ```repl
+   * :prove t3
+   * ```
+   */
   property t3 = join (toBytes (sha3 0b110010100001101011011110100110)) ==
       0xc8242fef409e5ae9d1f1c857ae4dc624b92b19809f62aa8c07411c54a078b1d0
 
 
 submodule SHA3_384 where
   import Primitive::Keyless::Hash::SHA3::SHA3_384
 
+  /*
+   * ```repl
+   * :prove t1
+   * ```
+   */
   property t1 = join (toBytes (sha3 [])) ==
     0x0c63a75b845e4f7d01107d852e4c2485c51a50aaaa94fc61995e71bbee983a2ac3713831264adb47fb6bd1e058d5f004
 
+  /*
+   * ```repl
+   * :prove t2
+   * ```
+   */
   property t2 = join (toBytes (sha3 0b11001)) ==
    0x737c9b491885e9bf7428e792741a7bf8dca9653471c3e148473f2c236b6a0a6455eb1dce9f779b4b6b237fef171b1c64
 
 
 submodule SHA3_512 where
   import Primitive::Keyless::Hash::SHA3::SHA3_512
 
+  /*
+   * ```repl
+   * :prove t1
+   * ```
+   */
   property t1 = join (toBytes (sha3 [])) ==
     0xa69f73cca23a9ac5c8b567dc185a756e97c982164fe25859e0d1dcc1475c80a615b2123af1f5f94c11e3e9402c3ac558f500199d95b6d3e301758586281dcd26
 
+  /*
+   * ```repl
+   * :prove t2
+   * ```
+   */
   property t2 = join (toBytes (sha3 0b11001)) ==
     0xa13e01494114c09800622a70288c432121ce70039d753cadd2e006e4d961cb27544c1481e5814bdceb53be6733d5e099795e5e81918addb058e22a9f24883f37
 

Primitive/Keyless/Hash/SHAKE/SHAKE128.cry

@@ -1,3 +1,18 @@
+/*
+ * Instantiation of SHAKE128, a SHA-3 extendable-output function, as specified
+ * in [FIPS-202].
+ *
+ * [FIPS-202]: National Institute of Standards and Technology. SHA-3 Standard:
+ *     Permutation-Based Hash and Extendable-Output Functions. (Department of
+ *     Commerce, Washington, D.C.), Federal Information Processing Standards
+ *     Publication (FIPS) NIST FIPS 202. August 2015.
+ *     @see https://dx.doi.org/10.6028/NIST.FIPS.202
+ *
+ * @copyright Galois, Inc.
+ * @author Ajay Kumar Eeralla
+ * @editor Marcella Hastings <[email protected]>
+ *
+ */
 module Primitive::Keyless::Hash::SHAKE::SHAKE128 where
 import Primitive::Keyless::Hash::keccak where
     type b = 1600
@@ -7,6 +22,13 @@ import Primitive::Keyless::Hash::keccak where
     type c = 256
 import Primitive::Keyless::Hash::utils (toBytes)
 
+/**
+ * SHAKE128 extendable-output function.
+ * [FIPS-202] Section 6.2.
+ *
+ * Note that the specification of `c` is above, in the instantiation of the
+ * `keccak` module.
+ */
 shake128 : {m, d} (fin m, fin d) => [m] -> [d]
 shake128 M = Keccak (M # 0b1111)
 

Primitive/Keyless/Hash/SHAKE/SHAKE256.cry

@@ -1,3 +1,18 @@
+/*
+ * Instantiation of SHAKE256, a SHA-3 extendable-output function, as specified
+ * in [FIPS-202].
+ *
+ * [FIPS-202]: National Institute of Standards and Technology. SHA-3 Standard:
+ *     Permutation-Based Hash and Extendable-Output Functions. (Department of
+ *     Commerce, Washington, D.C.), Federal Information Processing Standards
+ *     Publication (FIPS) NIST FIPS 202. August 2015.
+ *     @see https://dx.doi.org/10.6028/NIST.FIPS.202
+ *
+ * @copyright Galois, Inc.
+ * @author Ajay Kumar Eeralla
+ * @editor Marcella Hastings <[email protected]>
+ *
+ */
 module Primitive::Keyless::Hash::SHAKE::SHAKE256 where
 import Primitive::Keyless::Hash::keccak where
     type b = 1600
@@ -7,8 +22,13 @@ import Primitive::Keyless::Hash::keccak where
     type c = 512
 import Primitive::Keyless::Hash::utils (toBytes)
 
-type secBits = 256
-
+/**
+ * SHAKE256 extendable-output function.
+ * [FIPS-202] Section 6.2.
+ *
+ * Note that the specification of `c` is above, in the instantiation of the
+ * `keccak` module.
+ */
 shake256: {m, d} (fin m, fin d) => [m] -> [d]
 shake256 M = Keccak (M # 0b1111)
 
@@ -62,4 +82,4 @@ property k8 = join (toBytes (shake256 (reverse 0b110))) == expected_result where
         0xbddbe2cbd3a9a3ba3914da88e5853e70,
         0x83630e6d51d7a009017d8176c3067329,
         0xbec8e5f65591d65c5894c40132f1a2ab
-    ]
+                                                                             ]