Skip to content

Commit 7290e5c

Browse files
tob-joecodex
tob-joe
and
codex
committed
Add CBMC target platform support
Add explicit CBMC target platform selection for the proof infrastructure, including i386 Linux support with an i686 preprocessor and matching CBMC target-model flags. Add target compiler shims for goto-instrument, a target ABI canary proof, and the solver/proof configuration tweaks needed by the 32-bit ML-KEM suite. Do not expose riscv32 as a CBMC target because this CBMC toolchain does not support that architecture model. Verification: git diff --check; python3 -B -m py_compile scripts/tests proofs/cbmc/run-cbmc-proofs.py; ./scripts/tests cbmc --help target list; canary dry-runs for i386-linux, x86_64-linux, aarch64-linux, riscv64-linux, and ppc64le-linux; nix eval --raw .#devShells.aarch64-linux.cbmc32.drvPath. Signed-off-by: Joe Doyle <joseph.doyle@trailofbits.com> Co-authored-by: Codex <codex@openai.com>
1 parent 22fda7f commit 7290e5c

19 files changed

Lines changed: 199 additions & 22 deletions

File tree

‎flake.nix‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,7 @@
8080
packages.toolchains = util.toolchains;
8181
packages.toolchains_native = util.toolchains_native;
8282
packages.toolchain_x86_64 = util.toolchain_x86_64;
83+
packages.toolchain_i686 = util.toolchain_i686;
8384
packages.toolchain_aarch64 = util.toolchain_aarch64;
8485
packages.toolchain_riscv64 = util.toolchain_riscv64;
8586
packages.toolchain_riscv32 = util.toolchain_riscv32;
@@ -130,6 +131,17 @@
130131
devShells.cbmc = util.mkShell {
131132
packages = builtins.attrValues { inherit (config.packages) cbmc toolchains_native; } ++ [ pkgs.gh ];
132133
};
134+
devShells.cbmc32 = util.mkShell {
135+
packages = builtins.attrValues {
136+
inherit (config.packages)
137+
cbmc
138+
toolchain_i686
139+
toolchain_x86_64
140+
toolchain_aarch64
141+
toolchain_riscv64
142+
toolchain_ppc64le;
143+
} ++ [ pkgs.gh ];
144+
};
133145
devShells.slothy = util.mkShell {
134146
packages = builtins.attrValues { inherit (config.packages) slothy linters toolchains_native; };
135147
};

‎nix/util.nix‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ rec {
3434
_toolchains = { cross ? true }:
3535
let
3636
x86_64-gcc = wrap-gcc pkgs.pkgsCross.gnu64;
37+
i686-gcc = wrap-gcc pkgs.pkgsCross.gnu32;
3738
aarch64-gcc = wrap-gcc pkgs.pkgsCross.aarch64-multiplatform;
3839
riscv64-gcc = wrap-gcc pkgs.pkgsCross.riscv64;
3940
riscv32-gcc = wrap-gcc pkgs.pkgsCross.riscv32;
@@ -47,7 +48,7 @@ rec {
4748
# and won't just work for now
4849
# - equip all toolchains if cross is explicitly set to true
4950
# - On some machines, `native-gcc` needed to be evaluated lastly (placed as the last element of the toolchain list), or else would result in environment variables (CC, AR, ...) overriding issue.
50-
pkgs.lib.optionals cross [ pkgs.qemu pkgs.gcc-arm-embedded x86_64-gcc aarch64-gcc riscv64-gcc riscv32-gcc ppc64le-gcc ]
51+
pkgs.lib.optionals cross [ pkgs.qemu pkgs.gcc-arm-embedded x86_64-gcc i686-gcc aarch64-gcc riscv64-gcc riscv32-gcc ppc64le-gcc ]
5152
++ pkgs.lib.optionals (cross && pkgs.stdenv.isLinux && pkgs.stdenv.isx86_64) [ aarch64_be-gcc ]
5253
++ pkgs.lib.optionals cross [ native-gcc ]
5354
# git is not available in the nix shell on Darwin. As a workaround we add git as a dependency here.
@@ -143,6 +144,11 @@ rec {
143144
cross_compilers = [ (wrap-gcc pkgs.pkgsCross.gnu64) ];
144145
};
145146

147+
toolchain_i686 = _individual_toolchain {
148+
name = "i686";
149+
cross_compilers = [ (wrap-gcc pkgs.pkgsCross.gnu32) ];
150+
};
151+
146152
toolchain_aarch64 = _individual_toolchain {
147153
name = "aarch64";
148154
cross_compilers = [ (wrap-gcc pkgs.pkgsCross.aarch64-multiplatform) ];

‎proofs/cbmc/Makefile.common‎

Lines changed: 97 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -325,9 +325,91 @@ CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK)
325325
# initialized with unconstrained values.
326326
NONDET_STATIC ?=
327327

328+
# Target platform for CBMC/goto-cc. Leave unset to preserve the historic
329+
# host-default model.
330+
CBMC_TARGET ?=
331+
CBMC_TARGET_CC ?=
332+
CBMC_TARGET_GOTO_FLAGS ?=
333+
CBMC_TARGET_CBMC_FLAGS ?=
334+
CBMC_TARGET_INSTRUMENT_ENV ?=
335+
CBMC_TARGET_GCC_AS_GCC_DIR ?=
336+
CBMC_TARGET_HOST_PATH ?= $(shell printf '%s' "$$PATH")
337+
CBMC_TARGET_POINTER_BYTES ?= 8
338+
CBMC_TARGET_SIZE_T_BYTES ?= 8
339+
CBMC_TARGET_LONG_BYTES ?= 8
340+
341+
ifeq ($(strip $(CBMC_TARGET)),)
342+
ifeq ($(strip $(CBMC_TARGET_CC)),)
343+
CBMC_TARGET_CC = $(CC)
344+
endif
345+
else ifeq ($(CBMC_TARGET),i386-linux)
346+
ifeq ($(strip $(CBMC_TARGET_CC)),)
347+
CBMC_TARGET_CC = i686-unknown-linux-gnu-gcc
348+
endif
349+
CBMC_TARGET_GOTO_FLAGS = --i386-linux
350+
CBMC_TARGET_CBMC_FLAGS = --i386-linux
351+
ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),)
352+
CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/i686-gcc-as-gcc
353+
endif
354+
CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC)
355+
CBMC_TARGET_POINTER_BYTES = 4
356+
CBMC_TARGET_SIZE_T_BYTES = 4
357+
CBMC_TARGET_LONG_BYTES = 4
358+
else ifeq ($(CBMC_TARGET),x86_64-linux)
359+
ifeq ($(strip $(CBMC_TARGET_CC)),)
360+
CBMC_TARGET_CC = x86_64-unknown-linux-gnu-gcc
361+
endif
362+
CBMC_TARGET_CBMC_FLAGS = --arch x86_64 --os linux --LP64
363+
ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),)
364+
CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/x86_64-gcc-as-gcc
365+
endif
366+
CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC)
367+
CBMC_TARGET_POINTER_BYTES = 8
368+
CBMC_TARGET_SIZE_T_BYTES = 8
369+
CBMC_TARGET_LONG_BYTES = 8
370+
else ifeq ($(CBMC_TARGET),aarch64-linux)
371+
ifeq ($(strip $(CBMC_TARGET_CC)),)
372+
CBMC_TARGET_CC = aarch64-unknown-linux-gnu-gcc
373+
endif
374+
CBMC_TARGET_CBMC_FLAGS = --arch arm64 --os linux --LP64
375+
ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),)
376+
CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/aarch64-gcc-as-gcc
377+
endif
378+
CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC)
379+
CBMC_TARGET_POINTER_BYTES = 8
380+
CBMC_TARGET_SIZE_T_BYTES = 8
381+
CBMC_TARGET_LONG_BYTES = 8
382+
else ifeq ($(CBMC_TARGET),riscv64-linux)
383+
ifeq ($(strip $(CBMC_TARGET_CC)),)
384+
CBMC_TARGET_CC = riscv64-unknown-linux-gnu-gcc
385+
endif
386+
CBMC_TARGET_CBMC_FLAGS = --arch riscv64 --os linux --LP64
387+
ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),)
388+
CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/riscv64-gcc-as-gcc
389+
endif
390+
CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC)
391+
CBMC_TARGET_POINTER_BYTES = 8
392+
CBMC_TARGET_SIZE_T_BYTES = 8
393+
CBMC_TARGET_LONG_BYTES = 8
394+
else ifeq ($(CBMC_TARGET),ppc64le-linux)
395+
ifeq ($(strip $(CBMC_TARGET_CC)),)
396+
CBMC_TARGET_CC = powerpc64le-unknown-linux-gnu-gcc
397+
endif
398+
CBMC_TARGET_CBMC_FLAGS = --arch ppc64le --os linux --LP64
399+
ifeq ($(strip $(CBMC_TARGET_GCC_AS_GCC_DIR)),)
400+
CBMC_TARGET_GCC_AS_GCC_DIR = $(PROOF_ROOT)/tools/ppc64le-gcc-as-gcc
401+
endif
402+
CBMC_TARGET_INSTRUMENT_ENV = PATH=$(CBMC_TARGET_GCC_AS_GCC_DIR):$(CBMC_TARGET_HOST_PATH) CC=$(CBMC_TARGET_CC) GCC=$(CBMC_TARGET_CC)
403+
CBMC_TARGET_POINTER_BYTES = 8
404+
CBMC_TARGET_SIZE_T_BYTES = 8
405+
CBMC_TARGET_LONG_BYTES = 8
406+
else
407+
$(error Unsupported CBMC_TARGET '$(CBMC_TARGET)'; expected i386-linux, x86_64-linux, aarch64-linux, riscv64-linux, ppc64le-linux, or unset)
408+
endif
409+
328410
# Flags to pass to goto-cc for compilation and linking
329-
COMPILE_FLAGS ?= -Wall -Werror --native-compiler $(CC)
330-
LINK_FLAGS ?= -Wall -Werror
411+
COMPILE_FLAGS ?= -Wall -Werror $(CBMC_TARGET_GOTO_FLAGS) --native-compiler $(CBMC_TARGET_CC)
412+
LINK_FLAGS ?= -Wall -Werror $(CBMC_TARGET_GOTO_FLAGS)
331413
EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols
332414

333415
# During instrumentation, it adds models of C library functions
@@ -555,6 +637,7 @@ endif
555637
################################################################
556638
# CBMC flags common to all proofs
557639
CBMCFLAGS += $(CBMC_FLAG_FLUSH)
640+
CBMCFLAGS += $(CBMC_TARGET_CBMC_FLAGS)
558641
CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
559642
CBMCFLAGS += --slice-formula
560643

@@ -563,6 +646,9 @@ CBMCFLAGS += --slice-formula
563646
DEFINES += -DCBMC=1
564647
DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)
565648
DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))"
649+
DEFINES += -DCBMC_TARGET_POINTER_BYTES=$(CBMC_TARGET_POINTER_BYTES)
650+
DEFINES += -DCBMC_TARGET_SIZE_T_BYTES=$(CBMC_TARGET_SIZE_T_BYTES)
651+
DEFINES += -DCBMC_TARGET_LONG_BYTES=$(CBMC_TARGET_LONG_BYTES)
566652

567653

568654
ifndef MLKEM_K
@@ -719,7 +805,7 @@ $(PROOF_GOTO)0100.goto: $(PROOF_SOURCES)
719805
$(PROJECT_GOTO)0200.goto: $(PROJECT_GOTO)0100.goto
720806
$(LITANI) add-job \
721807
--command \
722-
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
808+
'$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
723809
--inputs $^ \
724810
--outputs $@ \
725811
--stdout-file $(LOGDIR)/remove_function_body-log.txt \
@@ -742,7 +828,7 @@ $(HARNESS_GOTO)0100.goto: $(PROOF_GOTO)0100.goto $(PROJECT_GOTO)0200.goto
742828
$(HARNESS_GOTO)0200.goto: $(HARNESS_GOTO)0100.goto
743829
$(LITANI) add-job \
744830
--command \
745-
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \
831+
'$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \
746832
--inputs $^ \
747833
--outputs $@ \
748834
--stdout-file $(LOGDIR)/restrict_function_pointer-log.txt \
@@ -764,7 +850,7 @@ ifneq ($(strip $(CODE_CONTRACTS)),)
764850
else
765851
$(LITANI) add-job \
766852
--command \
767-
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \
853+
'$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \
768854
--inputs $^ \
769855
--outputs $@ \
770856
--stdout-file $(LOGDIR)/nondet_static-log.txt \
@@ -778,7 +864,7 @@ $(HARNESS_GOTO)0400.goto: $(HARNESS_GOTO)0300.goto
778864
ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
779865
$(LITANI) add-job \
780866
--command \
781-
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(ADD_LIBRARY_FLAG) $(CBMC_OPT_CONFIG_LIBRARY) $^ $@' \
867+
'$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(ADD_LIBRARY_FLAG) $(CBMC_OPT_CONFIG_LIBRARY) $^ $@' \
782868
--inputs $^ \
783869
--outputs $@ \
784870
--stdout-file $(LOGDIR)/linking-library-models-log.txt \
@@ -801,7 +887,7 @@ $(HARNESS_GOTO)0500.goto: $(HARNESS_GOTO)0400.goto
801887
ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
802888
$(LITANI) add-job \
803889
--command \
804-
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \
890+
'$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \
805891
--inputs $^ \
806892
--outputs $@ \
807893
--stdout-file $(LOGDIR)/unwind_loops-log.txt \
@@ -811,7 +897,7 @@ ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
811897
else ifneq ($(strip $(CODE_CONTRACTS)),)
812898
$(LITANI) add-job \
813899
--command \
814-
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
900+
'$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
815901
--inputs $^ \
816902
--outputs $@ \
817903
--stdout-file $(LOGDIR)/unwind_loops-log.txt \
@@ -833,7 +919,7 @@ endif
833919
$(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto
834920
$(LITANI) add-job \
835921
--command \
836-
'$(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
922+
'$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
837923
--inputs $^ \
838924
--outputs $@ \
839925
--stdout-file $(LOGDIR)/check_function_contracts-log.txt \
@@ -845,7 +931,7 @@ $(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto
845931
$(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto
846932
$(LITANI) add-job \
847933
--command \
848-
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
934+
'$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
849935
--inputs $^ \
850936
--outputs $@ \
851937
--stdout-file $(LOGDIR)/slice_global_inits-log.txt \
@@ -857,7 +943,7 @@ $(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto
857943
$(HARNESS_GOTO)0800.goto: $(HARNESS_GOTO)0700.goto
858944
$(LITANI) add-job \
859945
--command \
860-
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
946+
'$(CBMC_TARGET_INSTRUMENT_ENV) $(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
861947
--inputs $^ \
862948
--outputs $@ \
863949
--stdout-file $(LOGDIR)/drop_unused_functions-log.txt \

‎proofs/cbmc/cbmc_target_model/Makefile‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
# Copyright (c) The mlkem-native project authors
2+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
include ../Makefile_params.common
5+
6+
HARNESS_ENTRY = harness
7+
HARNESS_FILE = cbmc_target_model_harness
8+
9+
PROOF_UID = mlk_cbmc_target_model
10+
11+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
12+
PROJECT_SOURCES += $(PROOFDIR)/cbmc_target_model_project.c
13+
14+
EXTERNAL_SAT_SOLVER=
15+
CBMCFLAGS=--smt2
16+
17+
FUNCTION_NAME = harness
18+
19+
CBMC_OBJECT_BITS = 8
20+
21+
include ../Makefile.common

‎proofs/cbmc/cbmc_target_model/cbmc_target_model_harness.c‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// Copyright (c) The mlkem-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include <stddef.h>
5+
#include <stdint.h>
6+
7+
void __CPROVER_assert(_Bool, const char *);
8+
9+
void harness(void)
10+
{
11+
__CPROVER_assert(sizeof(void *) == CBMC_TARGET_POINTER_BYTES,
12+
"CBMC target pointer width matches selected model");
13+
__CPROVER_assert(sizeof(size_t) == CBMC_TARGET_SIZE_T_BYTES,
14+
"CBMC target size_t width matches selected model");
15+
__CPROVER_assert(sizeof(long) == CBMC_TARGET_LONG_BYTES,
16+
"CBMC target long width matches selected model");
17+
__CPROVER_assert(sizeof(uint64_t) == 8,
18+
"CBMC target uint64_t width is 8 bytes");
19+
}

‎proofs/cbmc/cbmc_target_model/cbmc_target_model_project.c‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
// Copyright (c) The mlkem-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
int cbmc_target_model_project_anchor;

‎proofs/cbmc/ntt_butterfly_block/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ USE_DYNAMIC_FRAMES=1
2626

2727
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
2828
EXTERNAL_SAT_SOLVER=
29-
CBMCFLAGS=--bitwuzla
29+
CBMCFLAGS=--smt2
3030

3131
FUNCTION_NAME = mlk_ntt_butterfly_block
3232

‎proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_aarch64/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ PROOF_UID = polyvec_basemul_acc_montgomery_cached_k2_native_aarch64
1212

1313
# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be
1414
# included, which contains the CBMC specifications.
15-
DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/aarch64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
15+
DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/aarch64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_BUILD -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
1616
INCLUDES +=
1717

1818
REMOVE_FUNCTION_BODY +=

‎proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ PROOF_UID = polyvec_basemul_acc_montgomery_cached_k2_native_x86_64
1212

1313
# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be
1414
# included, which contains the CBMC specifications.
15-
DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
15+
DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_BUILD -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
1616
INCLUDES +=
1717

1818
REMOVE_FUNCTION_BODY +=

‎proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_aarch64/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ PROOF_UID = polyvec_basemul_acc_montgomery_cached_k3_native_aarch64
1212

1313
# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be
1414
# included, which contains the CBMC specifications.
15-
DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/aarch64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
15+
DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/aarch64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_BUILD -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
1616
INCLUDES +=
1717

1818
REMOVE_FUNCTION_BODY +=

0 commit comments

Comments
 (0)