Add proofs of ML-KEM-Braid supporting functions.

Adds proof Makefiles and harnesses for
  serialize_epp
  deserialize_epp
  serialize_polyvec_16le
  deserialize_polyvec_16le

Adds and correct contracts for those functions in kem.c

Signed-off-by: Rod Chapman <rodchap@amazon.com>

Author: rod-chapman

mlkem/src/kem.c

@@ -380,6 +380,12 @@ int mlk_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
  * Coefficients in [-ETA2, ETA2] are stored as (ETA2 - x), fitting in 4 bits.
  * Two coefficients per byte (low nibble first). */
 static void mlk_serialize_epp(uint8_t out[MLKEM_EPP_BYTES], const mlk_poly *p)
+__contract__(
+  requires(memory_no_alias(out, MLKEM_EPP_BYTES))
+  requires(memory_no_alias(p, sizeof(mlk_poly)))
+  requires(array_abs_bound(p->coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1))
+  assigns(memory_slice(out, MLKEM_EPP_BYTES))
+)
 {
   unsigned j;
   for (j = 0; j < MLKEM_N / 2; j++)
@@ -395,6 +401,11 @@ static void mlk_serialize_epp(uint8_t out[MLKEM_EPP_BYTES], const mlk_poly *p)
 }
 
 static void mlk_deserialize_epp(mlk_poly *p, const uint8_t in[MLKEM_EPP_BYTES])
+__contract__(
+  requires(memory_no_alias(in, MLKEM_EPP_BYTES))
+  requires(memory_no_alias(p, sizeof(mlk_poly)))
+  assigns(memory_slice(p, sizeof(mlk_poly)))
+)
 {
   unsigned j;
   for (j = 0; j < MLKEM_N / 2; j++)
@@ -415,6 +426,11 @@ static void mlk_deserialize_epp(mlk_poly *p, const uint8_t in[MLKEM_EPP_BYTES])
  * Coefficients must be non-negative (e.g., after reduce). */
 static void mlk_serialize_polyvec_16le(uint8_t out[MLKEM_POLYVEC16_BYTES],
                                        const mlk_polyvec *v)
+__contract__(
+  requires(memory_no_alias(out, MLKEM_POLYVEC16_BYTES))
+  requires(memory_no_alias(v, sizeof(mlk_polyvec)))
+  assigns(memory_slice(out, MLKEM_POLYVEC16_BYTES))
+)
 {
   unsigned i, j;
   for (i = 0; i < MLKEM_K; i++)
@@ -427,9 +443,9 @@ static void mlk_serialize_polyvec_16le(uint8_t out[MLKEM_POLYVEC16_BYTES],
     __loop__(
       assigns(j, memory_slice(out, MLKEM_POLYVEC16_BYTES))
       invariant(j <= MLKEM_N)
-      decreases(MLKEM_K - j))
+      decreases(MLKEM_N - j))
     {
-      uint16_t c = (uint16_t)v->vec[i].coeffs[j];
+      uint16_t c = mlk_cast_int16_to_uint16(v->vec[i].coeffs[j]);
       out[i * MLKEM_POLY16_BYTES + 2 * j] = (uint8_t)(c & 0xFF);
       out[i * MLKEM_POLY16_BYTES + 2 * j + 1] = (uint8_t)(c >> 8);
     }
@@ -438,6 +454,11 @@ static void mlk_serialize_polyvec_16le(uint8_t out[MLKEM_POLYVEC16_BYTES],
 
 static void mlk_deserialize_polyvec_16le(
     mlk_polyvec *v, const uint8_t in[MLKEM_POLYVEC16_BYTES])
+__contract__(
+  requires(memory_no_alias(in, MLKEM_POLYVEC16_BYTES))
+  requires(memory_no_alias(v, sizeof(mlk_polyvec)))
+  assigns(memory_slice(v, sizeof(mlk_polyvec)))
+)
 {
   unsigned i, j;
   for (i = 0; i < MLKEM_K; i++)
@@ -450,7 +471,7 @@ static void mlk_deserialize_polyvec_16le(
     __loop__(
       assigns(j, memory_slice(v, sizeof(mlk_polyvec)))
       invariant(j <= MLKEM_N)
-      decreases(MLKEM_K - j))
+      decreases(MLKEM_N - j))
     {
       v->vec[i].coeffs[j] = mlk_cast_uint16_to_int16(
           (uint16_t)((unsigned)in[i * MLKEM_POLY16_BYTES + 2 * j] |

proofs/cbmc/deserialize_epp/Makefile

@@ -0,0 +1,36 @@
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = deserialize_epp_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = mlk_deserialize_epp
+
+DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/src/kem.c
+
+CHECK_FUNCTION_CONTRACTS=mlk_deserialize_epp
+USE_FUNCTION_CONTRACTS =
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = mlk_deserialize_epp
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 12
+
+include ../Makefile.common

proofs/cbmc/deserialize_epp/deserialize_epp_harness.c

@@ -0,0 +1,21 @@
+// Copyright (c) The mlkem-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include <kem.h>
+#include <poly.h>
+
+#define mlk_deserialize_epp MLK_NAMESPACE(deserialize_epp)
+void mlk_deserialize_epp(mlk_poly *p, const uint8_t in[MLKEM_EPP_BYTES]);
+
+void harness(void)
+{
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
+  uint8_t *in;
+  mlk_poly *p;
+
+  mlk_deserialize_epp(p, in);
+}

proofs/cbmc/deserialize_polyvec_16le/Makefile

@@ -0,0 +1,36 @@
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = deserialize_polyvec_16le_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = mlk_deserialize_polyvec_16le
+
+DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/src/kem.c
+
+CHECK_FUNCTION_CONTRACTS=mlk_deserialize_polyvec_16le
+USE_FUNCTION_CONTRACTS =
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = mlk_deserialize_polyvec_16le
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 12
+
+include ../Makefile.common

proofs/cbmc/deserialize_polyvec_16le/deserialize_polyvec_16le_harness.c

@@ -0,0 +1,22 @@
+// Copyright (c) The mlkem-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include <kem.h>
+#include <poly_k.h>
+
+#define mlk_deserialize_polyvec_16le MLK_NAMESPACE(deserialize_polyvec_16le)
+void mlk_deserialize_polyvec_16le(mlk_polyvec *v,
+                                  const uint8_t in[MLKEM_POLYVEC16_BYTES]);
+
+void harness(void)
+{
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
+  uint8_t *in;
+  mlk_polyvec *v;
+
+  mlk_deserialize_polyvec_16le(v, in);
+}

proofs/cbmc/serialize_epp/Makefile

@@ -0,0 +1,36 @@
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = serialize_epp_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = mlk_serialize_epp
+
+DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/src/kem.c
+
+CHECK_FUNCTION_CONTRACTS=mlk_serialize_epp
+USE_FUNCTION_CONTRACTS =
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = mlk_serialize_epp
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 12
+
+include ../Makefile.common

proofs/cbmc/serialize_epp/serialize_epp_harness.c

@@ -0,0 +1,21 @@
+// Copyright (c) The mlkem-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include <kem.h>
+#include <poly.h>
+
+#define mlk_serialize_epp MLK_NAMESPACE(serialize_epp)
+void mlk_serialize_epp(uint8_t out[MLKEM_EPP_BYTES], const mlk_poly *p);
+
+void harness(void)
+{
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
+  uint8_t *out;
+  mlk_poly *p;
+
+  mlk_serialize_epp(out, p);
+}

proofs/cbmc/serialize_polyvec_16le/Makefile

@@ -0,0 +1,36 @@
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = serialize_polyvec_16le_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = mlk_serialize_polyvec_16le
+
+DEFINES += -DMLK_CONFIG_ENABLE_MLKEM_BRAID
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/src/kem.c
+
+CHECK_FUNCTION_CONTRACTS=mlk_serialize_polyvec_16le
+USE_FUNCTION_CONTRACTS =
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = mlk_serialize_polyvec_16le
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 12
+
+include ../Makefile.common

proofs/cbmc/serialize_polyvec_16le/serialize_polyvec_16le_harness.c

@@ -0,0 +1,22 @@
+// Copyright (c) The mlkem-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include <kem.h>
+#include <poly_k.h>
+
+#define mlk_serialize_polyvec_16le MLK_NAMESPACE(serialize_polyvec_16le)
+void mlk_serialize_polyvec_16le(uint8_t out[MLKEM_POLYVEC16_BYTES],
+                                const mlk_polyvec *v);
+
+void harness(void)
+{
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
+  uint8_t *out;
+  mlk_polyvec *v;
+
+  mlk_serialize_polyvec_16le(out, v);
+}