CBMC: Add proof for poly_permute_bitrev_to_custom_harness

Dull since this is a no-op in the C backend, but still needed
for completeness.

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

Author: hanno-becker

proofs/cbmc/ct_get_optblocker_i32/ct_get_optblocker_i32_harness.c

@@ -4,4 +4,4 @@
 
 #include "verify.h"
 
-void harness(void) { uint8_t x = mlk_ct_get_optblocker_u8(); }
+void harness(void) { int32_t x = mlk_ct_get_optblocker_i32(); }

proofs/cbmc/poly_permute_bitrev_to_custom/Makefile

@@ -0,0 +1,64 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = poly_permute_bitrev_to_custom_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_poly_permute_bitrev_to_custom
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c
+
+CHECK_FUNCTION_CONTRACTS=mlk_poly_permute_bitrev_to_custom
+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
+
+# For this proof we tell CBMC to
+#  1. not decompose arrays into their individual cells
+#  2. to model arrays directly as SMT-lib arrays
+#  3. to slice constraints that are not in the cone of influence of the proof obligations
+# These options simplify them modelling of arrays and produce much more compact
+# SMT files, leaving all array-type reasoning to the SMT solver.
+#
+# For functions that use large and multi-dimensional arrays, this yields
+# a substantial improvement in proof performance.
+CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
+
+FUNCTION_NAME = mlk_poly_permute_bitrev_to_custom
+
+# 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/poly_permute_bitrev_to_custom/poly_permute_bitrev_to_custom_harness.c

@@ -0,0 +1,14 @@
+// Copyright (c) 2024-2025 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <stdint.h>
+#include "params.h"
+
+void mlk_poly_permute_bitrev_to_custom(int16_t data[MLKEM_N]);
+
+void harness(void)
+{
+  int16_t data[MLKEM_N];
+  mlk_poly_permute_bitrev_to_custom(data);
+}