From 646da2a6c5686f2a6d58fc53abcdbcb80f649d69 Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@000674-loaner.local>
Date: Tue, 15 Oct 2024 11:14:44 -0400
Subject: [PATCH] mlkem: test "implicit rejection" mechansim #146

Adds a test case for the implict reject case that uses the `J` hash
function in decaps.
---
 .../Cipher/ML_KEM/Tests/ML_KEM512.cry         | 30 ++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry
index d994c3df..467758ee 100644
--- a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry
+++ b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry
@@ -20,6 +20,7 @@ property t0 = keygenWorks && encapsWorks && decapsWorks where
     keygenWorks = ML_KEM::ML_KEM_KeyGen (z, d) == (pk, sk)
     encapsWorks = ML_KEM::ML_KEM_Encaps (pk, msg) == (ss, ct)
     decapsWorks = ML_KEM::ML_KEM_Decaps (ct, sk) == ss
+    decapsFailsCorrectly = ML_KEM::ML_KEM_Decaps (ct_n, sk) == ss_n
 
     z = split 0xf696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68
     d = split 0x6dbbc4375136df3b07f7c70e639e223e177e7fd53b161b3f4d57791794f12624
@@ -137,4 +138,31 @@ property t0 = keygenWorks && encapsWorks && decapsWorks where
         0x72e6dab0edf7e3b08ed1316acf857254b6c1fbf64ce582f2990ccecf9505fd7e,
         0x8517998aaf583be1aa641e9b54dbb91ca9d0700913967fb0349201b5d679b32d
     ])
-    ss = split 0x2b5c52ee72946331983ba050be0f435055c0547901e03559b356517889ea27c5
\ No newline at end of file
+    ss = split 0x2b5c52ee72946331983ba050be0f435055c0547901e03559b356517889ea27c5
+    ct_n = split (join [
+        0x96ac6243c9b1272be77b975a4048bf00ff2c48f94a3483362449273880d45e54,
+        0xbda15729682bf591a74382a708beb78118cab29ad74ac2f405ba720076dfb571,
+        0x88dc168487cd20081f6bf412f257dea03406b23a6a752e478ba4ef9c7c0f4810,
+        0x921fa32545be64dc5d9f18d4e1320efc6508154cda35ab912d059e0291a1150a,
+        0xe0a10da5e3d7bd221a851c598df4d0b18daa920976556099d1c0de4e222d5304,
+        0xd44fa9cb9bd4ffe15769dd6c4793fa809f5264cf0febca4b5975ba287639783a,
+        0xa1f4b645ff7a00d46ee7b19fec17b3e83bcaf4361d5349e30ceab60c386b6b0d,
+        0x1b90d8b336ee6a627ad2a38670cb5113b0fb4ac2ddc4250097483fefd182670e,
+        0xa40f0f45cce90b9ed58dafaef657d64e25fd6692a69721994e7d00b4949205eb,
+        0xe4c4f9c46ee5a1018b220a26d80ae2d2b486372e974d75b20a005b1616ad1e13,
+        0xd162915cc24f274670d1e5e8bd345874a7e7c9759c8e43ff33689200739a6133,
+        0x95f7ae78d73c6a7b90f65ab511f0df3c5dca85d0b9430b4e97098715ff823b61,
+        0x7321799aea0ab9c72234780339ec7b541d5e6f8c1551146c24a65411811b2367,
+        0x4c26123356cf233351382c3994cba5dc6c25a07e1ba9af33eca18bba3e97935e,
+        0x3abdf07e9fa32cecf241e7cafc6592db4ee487ff2b98a4a47805dee17fd93448,
+        0xdc98457b753ed4995ee6b1bfa9ff1d386c91f396ca8f48cab5b09a782ec3b616,
+        0xa87a6448a96236c4655413af755323d36a8db2e16509454489e6ec83629130cd,
+        0x2a54817918af362c83183494b4b590dbaf69cf399d3e2dc3e9c0c1224f148e65,
+        0xef68287341ab72ad58adfc69b28e27e91ebbf830fac53b94f762f01cc9b1561a,
+        0xe35f16edabf51ff164c1309d1fdb52cd2bfedb5a492eb65cb9fc86b8f05ed26d,
+        0x13233fb0a3eb33a9dce2cf98e6516cee42fbe1e97e20ab6c9965f58a377dc73e,
+        0x530667ab8f45e6a70b23db50f0df411732d8acdabe50c51adb886c0e5a5296d4,
+        0xaa1b13a336f0c17812f79fc69418a7d8901c568f410eff2af74baaeb8336f46c,
+        0xa17e14e060ce2d45cdb376286eec8b8befa5ab8025802720a1e7393af579db13
+    ])
+    ss_n = split 0x6e5c522a6d19b86c61bd983b56a0bef351c5ce716f021b49bdecd7bdfd5ed55a