CBMC: Add contracts to native backends

mlkem/fips202/native/api.h

@@ -32,13 +32,22 @@
  */
 
 #if defined(MLKEM_USE_FIPS202_X1_NATIVE)
-static INLINE void keccak_f1600_x1_native(uint64_t *state);
+static INLINE void keccak_f1600_x1_native(uint64_t *state)
+__contract__(
+  requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1))
+  assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1)));
 #endif
 #if defined(MLKEM_USE_FIPS202_X2_NATIVE)
-static INLINE void keccak_f1600_x2_native(uint64_t *state);
+static INLINE void keccak_f1600_x2_native(uint64_t *state)
+__contract__(
+  requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 2))
+  assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2)));
 #endif
 #if defined(MLKEM_USE_FIPS202_X4_NATIVE)
-static INLINE void keccak_f1600_x4_native(uint64_t *state);
+static INLINE void keccak_f1600_x4_native(uint64_t *state)
+__contract__(
+  requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
+  assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)));
 #endif
 
 #endif /* MLKEM_NATIVE_FIPS202_NATIVE_API_H */

mlkem/native/api.h

@@ -23,8 +23,21 @@
 #define MLKEM_NATIVE_ARITH_NATIVE_API_H
 
 #include <stdint.h>
+#include "../cbmc.h"
 #include "../common.h"
 
+/* Absolute exclusive upper bound for the output of the inverse NTT
+ *
+ * NOTE: This is the same bound as in poly.h and has to be kept
+ * in sync. */
+#define INVNTT_BOUND (8 * MLKEM_Q)
+
+/* Absolute exclusive upper bound for the output of the forward NTT
+ *
+ * NOTE: This is the same bound as in poly.h and has to be kept
+ * in sync. */
+#define NTT_BOUND (8 * MLKEM_Q)
+
 /*
  * This is the C<->native interface allowing for the drop-in of
  * native code for performance critical arithmetic components of ML-KEM.
@@ -66,7 +79,13 @@
  *
  * Arguments:   - int16_t p[MLKEM_N]: pointer to in/output polynomial
  **************************************************/
-static INLINE void ntt_native(int16_t p[MLKEM_N]);
+static INLINE void ntt_native(int16_t p[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
+  requires(array_abs_bound(p, 0, MLKEM_N, MLKEM_Q))
+  assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
+  ensures(array_abs_bound(p, 0, MLKEM_N, NTT_BOUND))
+);
 #endif /* MLKEM_USE_NATIVE_NTT */
 
 #if defined(MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER)
@@ -98,7 +117,14 @@ and to/from bytes conversions."
  * Arguments:   - int16_t p[MLKEM_N]: pointer to in/output polynomial
  *
  **************************************************/
-static INLINE void poly_permute_bitrev_to_custom(int16_t p[MLKEM_N]);
+static INLINE void poly_permute_bitrev_to_custom(int16_t p[MLKEM_N])
+__contract__(
+  /* We don't specify that this should be a permutation, but only
+   * that it does not change the bound established at the end of gen_matrix. */
+  requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
+  requires(array_bound(p, 0, MLKEM_N, 0, MLKEM_Q))
+  assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
+  ensures(array_bound(p, 0, MLKEM_N, 0, MLKEM_Q)));
 #endif /* MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER */
 
 #if defined(MLKEM_USE_NATIVE_INTT)
@@ -116,7 +142,12 @@ static INLINE void poly_permute_bitrev_to_custom(int16_t p[MLKEM_N]);
  *
  * Arguments:   - uint16_t *a: pointer to in/output polynomial
  **************************************************/
-static INLINE void intt_native(int16_t p[MLKEM_N]);
+static INLINE void intt_native(int16_t p[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
+  assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
+  ensures(array_abs_bound(p, 0, MLKEM_N, INVNTT_BOUND))
+);
 #endif /* MLKEM_USE_NATIVE_INTT */
 
 #if defined(MLKEM_USE_NATIVE_POLY_REDUCE)
@@ -127,7 +158,12 @@ static INLINE void intt_native(int16_t p[MLKEM_N]);
  *
  * Arguments:   - int16_t r[MLKEM_N]: pointer to input/output polynomial
  **************************************************/
-static INLINE void poly_reduce_native(int16_t p[MLKEM_N]);
+static INLINE void poly_reduce_native(int16_t p[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
+  assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
+  ensures(array_bound(p, 0, MLKEM_N, 0, MLKEM_Q))
+);
 #endif /* MLKEM_USE_NATIVE_POLY_REDUCE */
 
 #if defined(MLKEM_USE_NATIVE_POLY_TOMONT)
@@ -139,7 +175,12 @@ static INLINE void poly_reduce_native(int16_t p[MLKEM_N]);
  *
  * Arguments:   - int16_t r[MLKEM_N]: pointer to input/output polynomial
  **************************************************/
-static INLINE void poly_tomont_native(int16_t p[MLKEM_N]);
+static INLINE void poly_tomont_native(int16_t p[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
+  assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
+  ensures(array_abs_bound(p, 0, MLKEM_N, MLKEM_Q))
+);
 #endif /* MLKEM_USE_NATIVE_POLY_TOMONT */
 
 #if defined(MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE)
@@ -165,7 +206,12 @@ static INLINE void poly_tomont_native(int16_t p[MLKEM_N]);
  *              - cache: pointer to multiplication cache
  **************************************************/
 static INLINE void poly_mulcache_compute_native(int16_t cache[MLKEM_N / 2],
-                                                const int16_t poly[MLKEM_N]);
+                                                const int16_t poly[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(cache, sizeof(int16_t) * (MLKEM_N / 2)))
+  requires(memory_no_alias(poly, sizeof(int16_t) * MLKEM_N))
+  assigns(object_whole(cache))
+);
 #endif /* MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE */
 
 #if defined(MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED)
@@ -190,7 +236,25 @@ static INLINE void poly_mulcache_compute_native(int16_t cache[MLKEM_N / 2],
 static INLINE void polyvec_basemul_acc_montgomery_cached_native(
     int16_t r[MLKEM_N], const int16_t a[MLKEM_K * MLKEM_N],
     const int16_t b[MLKEM_K * MLKEM_N],
-    const int16_t b_cache[MLKEM_K * (MLKEM_N / 2)]);
+    const int16_t b_cache[MLKEM_K * (MLKEM_N / 2)])
+__contract__(
+  requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
+  requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_K * MLKEM_N))
+  requires(memory_no_alias(b, sizeof(int16_t) * MLKEM_K * MLKEM_N))
+  requires(memory_no_alias(b_cache, sizeof(int16_t) * MLKEM_K * (MLKEM_N / 2)))
+  /* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
+   * just use a single flattened array_bound(...) here.
+   *
+   * Once fixed, change to:
+   * ```
+   * requires(array_bound(a, 0, MLKEM_K * MLKEM_N, 0, UINT12_LIMIT))
+   * ```
+   */
+  requires(forall(kN, 0, MLKEM_K,					  \
+              array_bound(&((int16_t(*)[MLKEM_N])(a))[kN][0], 0, MLKEM_N, \
+			  0, UINT12_LIMIT)))
+  assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+);
 #endif
 
 #if defined(MLKEM_USE_NATIVE_POLY_TOBYTES)
@@ -209,7 +273,13 @@ static INLINE void polyvec_basemul_acc_montgomery_cached_native(
  *                   (of MLKEM_POLYBYTES bytes)
  **************************************************/
 static INLINE void poly_tobytes_native(uint8_t r[MLKEM_POLYBYTES],
-                                       const int16_t a[MLKEM_N]);
+                                       const int16_t a[MLKEM_N])
+__contract__(
+  requires(memory_no_alias(r, MLKEM_POLYBYTES))
+  requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
+  requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
+  assigns(object_whole(r))
+);
 #endif /* MLKEM_USE_NATIVE_POLY_TOBYTES */
 
 #if defined(MLKEM_USE_NATIVE_POLY_FROMBYTES)
@@ -227,7 +297,13 @@ static INLINE void poly_tobytes_native(uint8_t r[MLKEM_POLYBYTES],
  *                   (of MLKEM_POLYBYTES bytes)
  **************************************************/
 static INLINE void poly_frombytes_native(int16_t a[MLKEM_N],
-                                         const uint8_t r[MLKEM_POLYBYTES]);
+                                         const uint8_t r[MLKEM_POLYBYTES])
+__contract__(
+  requires(memory_no_alias(r, MLKEM_POLYBYTES))
+  requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
+  assigns(memory_slice(a, sizeof(int16_t) * MLKEM_N))
+  ensures(array_bound(a, 0, MLKEM_N, 0, UINT12_LIMIT))
+);
 #endif /* MLKEM_USE_NATIVE_POLY_FROMBYTES */
 
 #if defined(MLKEM_USE_NATIVE_REJ_UNIFORM)
@@ -249,7 +325,15 @@ static INLINE void poly_frombytes_native(int16_t a[MLKEM_N],
  * len).
  **************************************************/
 static INLINE int rej_uniform_native(int16_t *r, unsigned int len,
-                                     const uint8_t *buf, unsigned int buflen);
+                                     const uint8_t *buf, unsigned int buflen)
+__contract__(
+  requires(len <= 4096 && buflen <= 4096 && buflen % 3 == 0)
+  requires(memory_no_alias(r, sizeof(int16_t) * len))
+  requires(memory_no_alias(buf, buflen))
+  assigns(memory_slice(r, sizeof(int16_t) * len))
+  ensures(return_value == -1 || (0 <= return_value && return_value <= len))
+  ensures(return_value != -1 ==> array_bound(r, 0, (unsigned) return_value, 0, MLKEM_Q))
+);
 #endif /* MLKEM_USE_NATIVE_REJ_UNIFORM */
 
 #endif /* MLKEM_NATIVE_ARITH_NATIVE_API_H */

mlkem/sampling.c

@@ -29,10 +29,10 @@ __contract__(
   requires(offset <= target && target <= 4096 && buflen <= 4096 && buflen % 3 == 0)
   requires(memory_no_alias(r, sizeof(int16_t) * target))
   requires(memory_no_alias(buf, buflen))
-  requires(offset > 0 ==> array_bound(r, 0, offset, 0, MLKEM_Q))
+  requires(array_bound(r, 0, offset, 0, MLKEM_Q))
   assigns(memory_slice(r, sizeof(int16_t) * target))
   ensures(offset <= return_value && return_value <= target)
-  ensures(return_value > 0 ==> array_bound(r, 0, return_value, 0, MLKEM_Q))
+  ensures(array_bound(r, 0, return_value, 0, MLKEM_Q))
 )
 {
   unsigned int ctr, pos;
@@ -66,7 +66,6 @@ __contract__(
   return ctr;
 }
 
-#if !defined(MLKEM_USE_NATIVE_REJ_UNIFORM)
 /*************************************************
  * Name:        rej_uniform
  *
@@ -87,7 +86,7 @@ __contract__(
  *                                     Must be a multiple of 3.
  *
  * Note: Strictly speaking, only a few values of buflen near UINT_MAX need
- * excluding. The limit of 4096 is somewhat arbitary but sufficient for all
+ * excluding. The limit of 128 is somewhat arbitary but sufficient for all
  * uses of this function. Similarly, the actual limit for target is UINT_MAX/2.
  *
  * Returns the new offset of sampled 16-bit integers, at most target,
@@ -110,33 +109,27 @@ __contract__(
   requires(offset <= target && target <= 4096 && buflen <= 4096 && buflen % 3 == 0)
   requires(memory_no_alias(r, sizeof(int16_t) * target))
   requires(memory_no_alias(buf, buflen))
-  requires(offset > 0 ==> array_bound(r, 0, offset, 0, MLKEM_Q))
+  requires(array_bound(r, 0, offset, 0, MLKEM_Q))
   assigns(memory_slice(r, sizeof(int16_t) * target))
   ensures(offset <= return_value && return_value <= target)
-  ensures(return_value > 0 ==> array_bound(r, 0, return_value, 0, MLKEM_Q))
+  ensures(array_bound(r, 0, return_value, 0, MLKEM_Q))
 )
 {
-  return rej_uniform_scalar(r, target, offset, buf, buflen);
-}
-#else  /* MLKEM_USE_NATIVE_REJ_UNIFORM */
-static unsigned int rej_uniform(int16_t *r, unsigned int target,
-                                unsigned int offset, const uint8_t *buf,
-                                unsigned int buflen)
-{
-  int ret;
-
-  /* Sample from large buffer with full lane as much as possible. */
-  ret = rej_uniform_native(r + offset, target - offset, buf, buflen);
-  if (ret != -1)
+#if defined(MLKEM_USE_NATIVE_REJ_UNIFORM)
+  if (offset == 0)
   {
-    unsigned res = offset + (unsigned)ret;
-    debug_assert_bound(r, res, 0, MLKEM_Q);
-    return res;
+    int ret = rej_uniform_native(r, target, buf, buflen);
+    if (ret != -1)
+    {
+      unsigned res = (unsigned)ret;
+      debug_assert_bound(r, res, 0, MLKEM_Q);
+      return res;
+    }
   }
+#endif /* MLKEM_USE_NATIVE_REJ_UNIFORM */
 
   return rej_uniform_scalar(r, target, offset, buf, buflen);
 }
-#endif /* MLKEM_USE_NATIVE_REJ_UNIFORM */
 
 #ifndef MLKEM_GEN_MATRIX_NBLOCKS
 #define MLKEM_GEN_MATRIX_NBLOCKS \

proofs/cbmc/KeccakF1600_StatePermute_native/KeccakF1600_StatePermute_native_harness.c

@@ -0,0 +1,11 @@
+// Copyright (c) 2024 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <keccakf1600.h>
+
+void harness(void)
+{
+  uint64_t *s;
+  KeccakF1600_StatePermute(s);
+}

proofs/cbmc/KeccakF1600_StatePermute_native/Makefile

@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = KeccakF1600_StatePermute_native_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 = KeccakF1600_StatePermute_native
+
+DEFINES += -DMLKEM_USE_NATIVE_BACKEND_FIPS202 -DMLKEM_NATIVE_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x1.h\""
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StatePermute
+USE_FUNCTION_CONTRACTS=keccak_f1600_x1_native
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--bitwuzla
+
+FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600_StatePermute_native
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 8
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

proofs/cbmc/KeccakF1600_StatePermute_native/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/KeccakF1600x4_StatePermute_native_x2_harness.c

@@ -0,0 +1,11 @@
+// Copyright (c) 2024 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <keccakf1600.h>
+
+void harness(void)
+{
+  uint64_t *s;
+  KeccakF1600x4_StatePermute(s);
+}