From b502362c68423dbcdcafcc7a6599c66df8f77922 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Tue, 3 Dec 2024 09:09:49 +0800 Subject: [PATCH 1/4] remove trailing whitespace Signed-off-by: Matthias J. Kannwischer --- fips202/native/aarch64/common.i | 2 +- fips202/native/x86_64/xkcp/KeccakP-1600-unrolling.macros | 2 +- mlkem/native/aarch64/poly_clean.S | 2 +- mlkem/native/aarch64/poly_opt.S | 2 +- mlkem/native/aarch64/polyvec_clean.S | 2 +- mlkem/native/aarch64/polyvec_opt.S | 2 +- mlkem/native/aarch64/rej_uniform_asm_clean.S | 2 +- mlkem/native/x86_64/fq.S | 2 +- mlkem/native/x86_64/shuffle.S | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) diff --git a/fips202/native/aarch64/common.i b/fips202/native/aarch64/common.i index 0b4da0783..3795784ca 100644 --- a/fips202/native/aarch64/common.i +++ b/fips202/native/aarch64/common.i @@ -1,7 +1,7 @@ /* * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: MIT - */ + */ #if __APPLE__ #define ASM_LOAD(dst, symbol) \ diff --git a/fips202/native/x86_64/xkcp/KeccakP-1600-unrolling.macros b/fips202/native/x86_64/xkcp/KeccakP-1600-unrolling.macros index 486960866..3dbe94a47 100644 --- a/fips202/native/x86_64/xkcp/KeccakP-1600-unrolling.macros +++ b/fips202/native/x86_64/xkcp/KeccakP-1600-unrolling.macros @@ -1,7 +1,7 @@ /* * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 - */ + */ /* Implementation by the Keccak, Keyak and Ketje Teams, namely, Guido Bertoni, diff --git a/mlkem/native/aarch64/poly_clean.S b/mlkem/native/aarch64/poly_clean.S index 550bdc1c2..86e4e494a 100644 --- a/mlkem/native/aarch64/poly_clean.S +++ b/mlkem/native/aarch64/poly_clean.S @@ -1,7 +1,7 @@ /* * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 - */ + */ #include "config.h" #if defined(MLKEM_USE_NATIVE_AARCH64) diff --git a/mlkem/native/aarch64/poly_opt.S b/mlkem/native/aarch64/poly_opt.S index 57c904493..d86595059 100644 --- a/mlkem/native/aarch64/poly_opt.S +++ b/mlkem/native/aarch64/poly_opt.S @@ -1,7 +1,7 @@ /* * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 - */ + */ #include "config.h" #if defined(MLKEM_USE_NATIVE_AARCH64) diff --git a/mlkem/native/aarch64/polyvec_clean.S b/mlkem/native/aarch64/polyvec_clean.S index 0bbac1fef..9504d3d1c 100644 --- a/mlkem/native/aarch64/polyvec_clean.S +++ b/mlkem/native/aarch64/polyvec_clean.S @@ -1,7 +1,7 @@ /* * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 - */ + */ // // AArch64 re-implementation of the asymmetric base multiplication from: // diff --git a/mlkem/native/aarch64/polyvec_opt.S b/mlkem/native/aarch64/polyvec_opt.S index af49fadf3..9ae035639 100644 --- a/mlkem/native/aarch64/polyvec_opt.S +++ b/mlkem/native/aarch64/polyvec_opt.S @@ -1,7 +1,7 @@ /* * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 - */ + */ // AArch64 re-implementation of the asymmetric base multiplication from: diff --git a/mlkem/native/aarch64/rej_uniform_asm_clean.S b/mlkem/native/aarch64/rej_uniform_asm_clean.S index 63a877b75..00332ec65 100644 --- a/mlkem/native/aarch64/rej_uniform_asm_clean.S +++ b/mlkem/native/aarch64/rej_uniform_asm_clean.S @@ -1,7 +1,7 @@ /* * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 - */ + */ /************************************************* * Name: rej_uniform_asm_clean diff --git a/mlkem/native/x86_64/fq.S b/mlkem/native/x86_64/fq.S index 533437df8..00fb093c5 100644 --- a/mlkem/native/x86_64/fq.S +++ b/mlkem/native/x86_64/fq.S @@ -1,7 +1,7 @@ /* * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 - */ + */ // Implementation based on Kyber reference repository // https://github.com/pq-crystals/kyber/blob/main/avx2 diff --git a/mlkem/native/x86_64/shuffle.S b/mlkem/native/x86_64/shuffle.S index d0456b44f..dd1243121 100644 --- a/mlkem/native/x86_64/shuffle.S +++ b/mlkem/native/x86_64/shuffle.S @@ -1,7 +1,7 @@ /* * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 - */ + */ // Implementation from Kyber reference repository // https://github.com/pq-crystals/kyber/blob/main/avx2 From 404269c892cc76e47cdd1b70267797b8afea3d0d Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Tue, 3 Dec 2024 09:13:06 +0800 Subject: [PATCH 2/4] clean-up Makefiles Use constant indentation using tabs rather than spaces. Signed-off-by: Matthias J. Kannwischer --- Makefile | 8 ++++---- mk/config.mk | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Makefile b/Makefile index ff2feb4ff..1721b79ef 100644 --- a/Makefile +++ b/Makefile @@ -14,7 +14,7 @@ buildall: mlkem nistkat kat acvp $(Q)echo " Everything builds fine!" quickcheck: buildall - # Run basic functionality checks + # Run basic functionality checks $(MLKEM512_DIR)/bin/test_mlkem512 $(MLKEM768_DIR)/bin/test_mlkem768 $(MLKEM1024_DIR)/bin/test_mlkem1024 @@ -47,9 +47,9 @@ nistkat: \ $(MLKEM1024_DIR)/bin/gen_NISTKAT1024 kat: \ - $(MLKEM512_DIR)/bin/gen_KAT512 \ - $(MLKEM768_DIR)/bin/gen_KAT768 \ - $(MLKEM1024_DIR)/bin/gen_KAT1024 + $(MLKEM512_DIR)/bin/gen_KAT512 \ + $(MLKEM768_DIR)/bin/gen_KAT768 \ + $(MLKEM1024_DIR)/bin/gen_KAT1024 # emulate ARM64 binary on x86_64 machine emulate: diff --git a/mk/config.mk b/mk/config.mk index 061eedf60..ba7a70ecb 100644 --- a/mk/config.mk +++ b/mk/config.mk @@ -34,10 +34,10 @@ CFLAGS += \ -Wpointer-arith \ -Wno-long-long \ -Wno-unknown-pragmas \ - -Wno-unused-command-line-argument \ + -Wno-unused-command-line-argument \ -O3 \ -fomit-frame-pointer \ - -std=c99 \ + -std=c99 \ -pedantic \ -MMD \ $(CPPFLAGS) From 0db5e3f147f6c21c66ec364bb2e015ad20726ca3 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Tue, 3 Dec 2024 09:20:16 +0800 Subject: [PATCH 3/4] remove namspacing from static scalar_* functions Signed-off-by: Matthias J. Kannwischer --- cbmc/proofs/poly_compress_du/Makefile | 4 ++-- cbmc/proofs/poly_compress_dv/Makefile | 4 ++-- cbmc/proofs/poly_decompress_du/Makefile | 4 ++-- cbmc/proofs/poly_decompress_dv/Makefile | 4 ++-- cbmc/proofs/poly_reduce/Makefile | 2 +- cbmc/proofs/scalar_compress_d1/Makefile | 2 +- cbmc/proofs/scalar_compress_d10/Makefile | 2 +- cbmc/proofs/scalar_compress_d11/Makefile | 2 +- cbmc/proofs/scalar_compress_d4/Makefile | 2 +- cbmc/proofs/scalar_compress_d5/Makefile | 2 +- cbmc/proofs/scalar_decompress_d10/Makefile | 2 +- cbmc/proofs/scalar_decompress_d11/Makefile | 2 +- cbmc/proofs/scalar_decompress_d4/Makefile | 2 +- cbmc/proofs/scalar_decompress_d5/Makefile | 2 +- cbmc/proofs/scalar_signed_to_unsigned_q/Makefile | 2 +- mlkem/poly.h | 11 ----------- 16 files changed, 19 insertions(+), 30 deletions(-) diff --git a/cbmc/proofs/poly_compress_du/Makefile b/cbmc/proofs/poly_compress_du/Makefile index cdb450aab..e8cde2638 100644 --- a/cbmc/proofs/poly_compress_du/Makefile +++ b/cbmc/proofs/poly_compress_du/Makefile @@ -21,9 +21,9 @@ PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_du # For K = 2 or 3, the code calls scalar_compress_d10, so ifeq ($(MLKEM_K),4) -USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_compress_d11 +USE_FUNCTION_CONTRACTS = scalar_compress_d11 else -USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_compress_d10 +USE_FUNCTION_CONTRACTS = scalar_compress_d10 endif APPLY_LOOP_CONTRACTS=on diff --git a/cbmc/proofs/poly_compress_dv/Makefile b/cbmc/proofs/poly_compress_dv/Makefile index 9cc1378f1..26f1b1a6b 100644 --- a/cbmc/proofs/poly_compress_dv/Makefile +++ b/cbmc/proofs/poly_compress_dv/Makefile @@ -20,9 +20,9 @@ PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_dv ifeq ($(MLKEM_K),4) -USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_compress_d5 +USE_FUNCTION_CONTRACTS = scalar_compress_d5 else -USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_compress_d4 +USE_FUNCTION_CONTRACTS = scalar_compress_d4 endif APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/poly_decompress_du/Makefile b/cbmc/proofs/poly_decompress_du/Makefile index e4d98e174..5aca83ccc 100644 --- a/cbmc/proofs/poly_decompress_du/Makefile +++ b/cbmc/proofs/poly_decompress_du/Makefile @@ -22,9 +22,9 @@ CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_du # For K = 2 or 3, the code calls scalar_decompress_d10, so ifeq ($(MLKEM_K),4) -USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_d11 +USE_FUNCTION_CONTRACTS = scalar_decompress_d11 else -USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_d10 +USE_FUNCTION_CONTRACTS = scalar_decompress_d10 endif APPLY_LOOP_CONTRACTS=on diff --git a/cbmc/proofs/poly_decompress_dv/Makefile b/cbmc/proofs/poly_decompress_dv/Makefile index 025ff60d0..b378be1bb 100644 --- a/cbmc/proofs/poly_decompress_dv/Makefile +++ b/cbmc/proofs/poly_decompress_dv/Makefile @@ -22,9 +22,9 @@ CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_dv # For K = 2 or 3, the code calls scalar_decompress_d4, so ifeq ($(MLKEM_K),4) -USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_d5 +USE_FUNCTION_CONTRACTS = scalar_decompress_d5 else -USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_d4 +USE_FUNCTION_CONTRACTS = scalar_decompress_d4 endif APPLY_LOOP_CONTRACTS=on diff --git a/cbmc/proofs/poly_reduce/Makefile b/cbmc/proofs/poly_reduce/Makefile index 66bddb5e0..778ee24dc 100644 --- a/cbmc/proofs/poly_reduce/Makefile +++ b/cbmc/proofs/poly_reduce/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_reduce -USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_signed_to_unsigned_q $(MLKEM_NAMESPACE)barrett_reduce +USE_FUNCTION_CONTRACTS=scalar_signed_to_unsigned_q $(MLKEM_NAMESPACE)barrett_reduce APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/scalar_compress_d1/Makefile b/cbmc/proofs/scalar_compress_d1/Makefile index 32a1e6977..60750eb77 100644 --- a/cbmc/proofs/scalar_compress_d1/Makefile +++ b/cbmc/proofs/scalar_compress_d1/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d1 +CHECK_FUNCTION_CONTRACTS=scalar_compress_d1 USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/scalar_compress_d10/Makefile b/cbmc/proofs/scalar_compress_d10/Makefile index ec15ccfe4..b28bfd90c 100644 --- a/cbmc/proofs/scalar_compress_d10/Makefile +++ b/cbmc/proofs/scalar_compress_d10/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d10 +CHECK_FUNCTION_CONTRACTS= scalar_compress_d10 USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/scalar_compress_d11/Makefile b/cbmc/proofs/scalar_compress_d11/Makefile index 86076358b..1fa590bbf 100644 --- a/cbmc/proofs/scalar_compress_d11/Makefile +++ b/cbmc/proofs/scalar_compress_d11/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d11 +CHECK_FUNCTION_CONTRACTS= scalar_compress_d11 USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/scalar_compress_d4/Makefile b/cbmc/proofs/scalar_compress_d4/Makefile index 906c8f2b6..1c9c3e146 100644 --- a/cbmc/proofs/scalar_compress_d4/Makefile +++ b/cbmc/proofs/scalar_compress_d4/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d4 +CHECK_FUNCTION_CONTRACTS=scalar_compress_d4 USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/scalar_compress_d5/Makefile b/cbmc/proofs/scalar_compress_d5/Makefile index c843a70a9..d5bc8f8e5 100644 --- a/cbmc/proofs/scalar_compress_d5/Makefile +++ b/cbmc/proofs/scalar_compress_d5/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d5 +CHECK_FUNCTION_CONTRACTS=scalar_compress_d5 USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/scalar_decompress_d10/Makefile b/cbmc/proofs/scalar_decompress_d10/Makefile index 413ac3d8e..90190659d 100644 --- a/cbmc/proofs/scalar_decompress_d10/Makefile +++ b/cbmc/proofs/scalar_decompress_d10/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_d10 +CHECK_FUNCTION_CONTRACTS=scalar_decompress_d10 USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/scalar_decompress_d11/Makefile b/cbmc/proofs/scalar_decompress_d11/Makefile index f92eeb34a..62b68f0b2 100644 --- a/cbmc/proofs/scalar_decompress_d11/Makefile +++ b/cbmc/proofs/scalar_decompress_d11/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_d11 +CHECK_FUNCTION_CONTRACTS=scalar_decompress_d11 USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/scalar_decompress_d4/Makefile b/cbmc/proofs/scalar_decompress_d4/Makefile index c3dae80c2..ad5ccdc76 100644 --- a/cbmc/proofs/scalar_decompress_d4/Makefile +++ b/cbmc/proofs/scalar_decompress_d4/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_d4 +CHECK_FUNCTION_CONTRACTS=scalar_decompress_d4 USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/scalar_decompress_d5/Makefile b/cbmc/proofs/scalar_decompress_d5/Makefile index ecd943651..a7a23480c 100644 --- a/cbmc/proofs/scalar_decompress_d5/Makefile +++ b/cbmc/proofs/scalar_decompress_d5/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_d5 +CHECK_FUNCTION_CONTRACTS=scalar_decompress_d5 USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/scalar_signed_to_unsigned_q/Makefile b/cbmc/proofs/scalar_signed_to_unsigned_q/Makefile index 9bb6f8b8b..86f1e9d5b 100644 --- a/cbmc/proofs/scalar_signed_to_unsigned_q/Makefile +++ b/cbmc/proofs/scalar_signed_to_unsigned_q/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_signed_to_unsigned_q +CHECK_FUNCTION_CONTRACTS=scalar_signed_to_unsigned_q USE_FUNCTION_CONTRACTS=ct_sel_int16 ct_cmask_neg_i16 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/mlkem/poly.h b/mlkem/poly.h index 843a9c956..290776416 100644 --- a/mlkem/poly.h +++ b/mlkem/poly.h @@ -40,17 +40,6 @@ typedef struct int16_t coeffs[MLKEM_N >> 1]; } poly_mulcache; -#define scalar_compress_d1 MLKEM_NAMESPACE(scalar_compress_d1) -#define scalar_compress_d4 MLKEM_NAMESPACE(scalar_compress_d4) -#define scalar_compress_d5 MLKEM_NAMESPACE(scalar_compress_d5) -#define scalar_compress_d10 MLKEM_NAMESPACE(scalar_compress_d10) -#define scalar_compress_d11 MLKEM_NAMESPACE(scalar_compress_d11) -#define scalar_decompress_d4 MLKEM_NAMESPACE(scalar_decompress_d4) -#define scalar_decompress_d5 MLKEM_NAMESPACE(scalar_decompress_d5) -#define scalar_decompress_d10 MLKEM_NAMESPACE(scalar_decompress_d10) -#define scalar_decompress_d11 MLKEM_NAMESPACE(scalar_decompress_d11) -#define scalar_signed_to_unsigned_q MLKEM_NAMESPACE(scalar_signed_to_unsigned_q) - /************************************************************ * Name: scalar_compress_d1 * From 980cbbeee410ac07d97d8fbd6613fe992b72926b Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Tue, 3 Dec 2024 09:24:17 +0800 Subject: [PATCH 4/4] remove namspacing from static verify.h functions Signed-off-by: Matthias J. Kannwischer --- cbmc/proofs/crypto_kem_dec/Makefile | 2 +- cbmc/proofs/ct_cmov_zero/Makefile | 4 ++-- cbmc/proofs/ct_memcmp/Makefile | 4 ++-- mlkem/verify.h | 2 -- 4 files changed, 5 insertions(+), 7 deletions(-) diff --git a/cbmc/proofs/crypto_kem_dec/Makefile b/cbmc/proofs/crypto_kem_dec/Makefile index f883ca965..cad79622a 100644 --- a/cbmc/proofs/crypto_kem_dec/Makefile +++ b/cbmc/proofs/crypto_kem_dec/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)dec -USE_FUNCTION_CONTRACTS= $(FIPS202_NAMESPACE)sha3_512 $(FIPS202_NAMESPACE)sha3_256 $(MLKEM_NAMESPACE)indcpa_enc $(MLKEM_NAMESPACE)indcpa_dec $(MLKEM_NAMESPACE)mlkem_shake256_rkprf $(MLKEM_NAMESPACE)ct_memcmp $(MLKEM_NAMESPACE)ct_cmov_zero memcmp +USE_FUNCTION_CONTRACTS= $(FIPS202_NAMESPACE)sha3_512 $(FIPS202_NAMESPACE)sha3_256 $(MLKEM_NAMESPACE)indcpa_enc $(MLKEM_NAMESPACE)indcpa_dec $(MLKEM_NAMESPACE)mlkem_shake256_rkprf ct_memcmp ct_cmov_zero memcmp APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/ct_cmov_zero/Makefile b/cbmc/proofs/ct_cmov_zero/Makefile index 06f1b2f3c..847cb2405 100644 --- a/cbmc/proofs/ct_cmov_zero/Makefile +++ b/cbmc/proofs/ct_cmov_zero/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c # Dummy source -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ct_cmov_zero +CHECK_FUNCTION_CONTRACTS=ct_cmov_zero USE_FUNCTION_CONTRACTS=ct_sel_uint8 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = $(MLKEM_NAMESPACE)ct_cmov_zero +FUNCTION_NAME = ct_cmov_zero # 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 diff --git a/cbmc/proofs/ct_memcmp/Makefile b/cbmc/proofs/ct_memcmp/Makefile index 452701127..917c49db1 100644 --- a/cbmc/proofs/ct_memcmp/Makefile +++ b/cbmc/proofs/ct_memcmp/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ct_memcmp +CHECK_FUNCTION_CONTRACTS=ct_memcmp USE_FUNCTION_CONTRACTS=value_barrier_u8 ct_cmask_nonzero_u8 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(MLKEM_NAMESPACE)ct_memcmp +FUNCTION_NAME = ct_memcmp # 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 diff --git a/mlkem/verify.h b/mlkem/verify.h index 99d6e5f63..5c62223c3 100644 --- a/mlkem/verify.h +++ b/mlkem/verify.h @@ -225,7 +225,6 @@ __contract__(ensures(return_value == (cond ? a : b))) return b ^ (ct_cmask_nonzero_u8(cond) & (a ^ b)); } -#define ct_memcmp MLKEM_NAMESPACE(ct_memcmp) /************************************************* * Name: ct_memcmp * @@ -275,7 +274,6 @@ __contract__( return (value_barrier_u8(ct_cmask_nonzero_u8(r) ^ s) ^ s); } -#define ct_cmov_zero MLKEM_NAMESPACE(ct_cmov_zero) /************************************************* * Name: ct_cmov_zero *