CBMC: Add spec + proof for poly_add()

Restrict the spec to the case `poly_add(r,r,x)` for now, which is the
only one used throughout the codebase.

I am unsure about the idiomatic way to capture aliasing of the
r and a parameters. It seems that `IS_FRESH(r) && r == a` is
contradictory to CBMC, so for now the commit uses `SAME_OBJECT(r,a)`
and `POINTER_OFFSET(r) == POINTER_OFFSET(a)`.

Care needs to be taken in the spec and loop invariants to account for
the fact that `a` is overwritten in the loop. To access the original
values, the `LOOP_ENTRY` and `OLD` wrappers are needed.

Signed-off-by: Hanno Becker <[email protected]>

The docstring for poly_add has been moved to poly.h. This commit
removes it from poly.h.

Signed-off-by: Hanno Becker <[email protected]>

Author: hanno-becker

cbmc/proofs/poly_add/Makefile

@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = poly_add_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 = poly_add
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_add
+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 = poly_add
+
+# 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

cbmc/proofs/poly_add/cbmc-proof.txt

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

cbmc/proofs/poly_add/poly_add_harness.c

@@ -0,0 +1,27 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0 AND Apache-2.0
+
+/*
+ * Insert copyright notice
+ */
+
+/**
+ * @file poly_add_harness.c
+ * @brief Implements the proof harness for basemul_cached function.
+ */
+#include "poly.h"
+
+/*
+ * Insert project header files that
+ *   - include the declaration of the function
+ *   - include the types needed to declare function arguments
+ */
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void) {
+  poly r, b;
+  poly_add(&r, &r, &b);
+}

mlkem/cbmc.h

@@ -14,6 +14,7 @@
 #define INVARIANT(...)
 #define ASSERT(...)
 #define ASSUME(...)
+#define SAME_OBJECT(...)
 
 #else  // CBMC _is_ defined, therefore we're doing proof
 
@@ -34,6 +35,8 @@
 #define ASSERT(...) __CPROVER_assert(__VA_ARGS__)
 #define ASSUME(...) __CPROVER_assume(__VA_ARGS__)
 
+#define SAME_OBJECT(...) __CPROVER_same_object(__VA_ARGS__)
+
 ///////////////////////////////////////////////////
 // Macros for "expression" forms that may appear
 // _inside_ top-level contracts.

mlkem/poly.c

@@ -555,20 +555,19 @@ void poly_reduce(poly *r) {
 }
 #endif /* MLKEM_USE_NATIVE_POLY_REDUCE */
 
-/*************************************************
- * Name:        poly_add
- *
- * Description: Add two polynomials; no modular reduction is performed
- *
- * Arguments: - poly *r: pointer to output polynomial
- *            - const poly *a: pointer to first input polynomial
- *            - const poly *b: pointer to second input polynomial
- **************************************************/
 void poly_add(poly *r, const poly *a, const poly *b) {
-  unsigned int i;
-  for (i = 0; i < MLKEM_N; i++) {
-    r->coeffs[i] = a->coeffs[i] + b->coeffs[i];
-  }
+  int i;
+  for (i = 0; i < MLKEM_N; i++)
+      // clang-format off
+    ASSIGNS(i, OBJECT_WHOLE(r))
+    INVARIANT(i >= 0 && i <= MLKEM_N)
+    INVARIANT(FORALL(int, k0, i, MLKEM_N - 1, r->coeffs[k0] == LOOP_ENTRY(*r).coeffs[k0]))
+    INVARIANT(FORALL(int, k1, 0, i - 1, r->coeffs[k1] == LOOP_ENTRY(*a).coeffs[k1] + b->coeffs[k1]))
+    DECREASES(MLKEM_N - i)
+    // clang-format on
+    {
+      r->coeffs[i] = a->coeffs[i] + b->coeffs[i];
+    }
 }
 
 /*************************************************

mlkem/poly.h

@@ -304,7 +304,36 @@ ASSIGNS(OBJECT_WHOLE(x));
 void poly_reduce(poly *r);
 
 #define poly_add MLKEM_NAMESPACE(poly_add)
-void poly_add(poly *r, const poly *a, const poly *b);
+/************************************************************
+ * Name: poly_add
+ *
+ * Description: Computes the coefficient-wise addition of two polynomials
+ *
+ * Arguments: - r: Pointer to output polynomial
+ *            - a: Pointer to first input polynomial. Must be the same as r.
+ *            - b: Pointer to second input polynomial. Must be disjoint from a
+ *                 and r.
+ *
+ * The coefficients of a and b must be so that the addition does
+ * not overflow. Otherwise, the behaviour of this function is undefined.
+ *
+ * NOTE: The restriction r == a is not needed, but we currently only
+ *       prove a CBMC spec under that assumption.
+ *
+ ************************************************************/
+void poly_add(poly *r, const poly *a, const poly *b)
+    // clang-format off
+// So far, poly_add is only used with r == a, so restrict proof to this case
+// TODO: Is this the right way to capture the aliasing constraint a==r?
+REQUIRES(SAME_OBJECT(r,a))
+REQUIRES(__CPROVER_POINTER_OFFSET(r)==__CPROVER_POINTER_OFFSET(a))
+REQUIRES(b != NULL && IS_FRESH(b, sizeof(poly)))
+REQUIRES(FORALL(int, k0, 0, MLKEM_N - 1, (int32_t) r->coeffs[k0] + b->coeffs[k0] <= INT16_MAX))
+REQUIRES(FORALL(int, k1, 0, MLKEM_N - 1, (int32_t) r->coeffs[k1] + b->coeffs[k1] >= INT16_MIN))
+ENSURES(FORALL(int, k, 0, MLKEM_N - 1, r->coeffs[k] == OLD(*a).coeffs[k] + b->coeffs[k]))
+ASSIGNS(OBJECT_WHOLE(r));
+// clang-format on
+
 #define poly_sub MLKEM_NAMESPACE(poly_sub)
 void poly_sub(poly *r, const poly *a, const poly *b);