fix several incorrectly-formed repl tests

GaloisInc · Oct 9, 2024 · d441a39 · d441a39
1 parent 277dace
commit d441a39
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 17 deletions.
diff --git a/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry b/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry
@@ -208,6 +208,7 @@ publicKey d = EC::scmul (fromZ d) EC::G
  * [FIPS-186-5] Section 3.3.
  * ```repl
  * :check signAndVerifyIsCorrect`{64}
+ * ```
  */
 signAndVerifyIsCorrect : {m} (fin m, width m < 64) => [m] -> Z EC::n -> Z EC::n -> Bool
 property signAndVerifyIsCorrect M d k = verification

diff --git a/Primitive/Keyless/Hash/SHA3/Tests.cry b/Primitive/Keyless/Hash/SHA3/Tests.cry
@@ -1,4 +1,4 @@
-/*
+/**
  * Tests of the SHA3 hash functions.
  *
  * Test vectors drawn from the NIST Cryptographic Standards and Guidelines
@@ -17,15 +17,15 @@ import Primitive::Keyless::Hash::utils
 submodule SHA3_224 where
   import Primitive::Keyless::Hash::SHA3::SHA3_224
 
-  /*
+  /**
    * ```repl
    * :prove t1
    * ```
    */
   property t1 = join (toBytes (sha3 [])) ==
     0x6b4e03423667dbb73b6e15454f0eb1abd4597f9a1b078e3f5b5a6bc7
 
-  /*
+  /**
    * ```repl
    * :prove t2
    * ```
@@ -36,15 +36,15 @@ submodule SHA3_224 where
   msg1600 : [1600]
   msg1600 = join [ 0b11000101 | _ <- zero : [200] ]
 
-  /*
+  /**
    * ```repl
    * :prove t3
    * ```
    */
   property t3 = join (toBytes (sha3 msg1600)) ==
     0x9376816aba503f72f96ce7eb65ac095deee3be4bf9bbc2a1cb7e11e0
 
-  /*
+  /**
    * ```repl
    * :prove t4
    * ```
@@ -56,23 +56,23 @@ submodule SHA3_224 where
 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
    * ```
@@ -84,15 +84,15 @@ submodule SHA3_256 where
 submodule SHA3_384 where
   import Primitive::Keyless::Hash::SHA3::SHA3_384
 
-  /*
+  /**
    * ```repl
    * :prove t1
    * ```
    */
   property t1 = join (toBytes (sha3 [])) ==
     0x0c63a75b845e4f7d01107d852e4c2485c51a50aaaa94fc61995e71bbee983a2ac3713831264adb47fb6bd1e058d5f004
 
-  /*
+  /**
    * ```repl
    * :prove t2
    * ```
@@ -104,15 +104,15 @@ submodule SHA3_384 where
 submodule SHA3_512 where
   import Primitive::Keyless::Hash::SHA3::SHA3_512
 
-  /*
+  /**
    * ```repl
    * :prove t1
    * ```
    */
   property t1 = join (toBytes (sha3 [])) ==
     0xa69f73cca23a9ac5c8b567dc185a756e97c982164fe25859e0d1dcc1475c80a615b2123af1f5f94c11e3e9402c3ac558f500199d95b6d3e301758586281dcd26
 
-  /*
+  /**
    * ```repl
    * :prove t2
    * ```

diff --git a/Primitive/Keyless/Hash/SHAKE/SHAKE256.cry b/Primitive/Keyless/Hash/SHAKE/SHAKE256.cry
@@ -34,7 +34,7 @@ import Primitive::Keyless::Hash::utils (toBytes)
 shake256: {d, m} (fin m) => [m] -> [d]
 shake256 M = Keccak (M # 0b1111)
 
-/*
+/**
  * ```repl
  * :prove k5
  * ```
@@ -47,7 +47,7 @@ property k5 = join (toBytes (shake256`{512} [])) == expected_result where
         0xfc821c49479ab48640292eacb3b7c4be
     ]
 
-/*
+/**
  * ```repl
  * :prove k6
  * ```
@@ -60,7 +60,7 @@ property k6 = join (toBytes (shake256 0b0)) == expected_result where
         0x55d30410d71b8e275a676545600f1c35
     ]
 
-/*
+/**
  * ```repl
  * :prove k7
  * ```
@@ -73,7 +73,7 @@ property k7 = join (toBytes (shake256 0b11 : [512])) == expected_result where
         0x7c98f3948e6b7959a9b8950ffd6345d5
     ]
 
-/*
+/**
  * ```repl
  * :prove k8
  * ```

diff --git a/Primitive/Symmetric/Cipher/Block/AES_specification.cry b/Primitive/Symmetric/Cipher/Block/AES_specification.cry
@@ -44,7 +44,7 @@ encrypt k = encryptWithSchedule (keyExpansion k)
 decrypt : [KeySize] -> [BlockSize] -> [BlockSize]
 decrypt k = decryptWithSchedule (keyExpansion k)
 
-/*
+/**
  * This property must be true for each instantiation.
  * With high probability, it will be extremely slow to prove.
  *