remove namspacing from static verify.h functions

Signed-off-by: Matthias J. Kannwischer <[email protected]>
pq-code-package · Dec 3, 2024 · 980cbbe · 980cbbe
1 parent 0db5e3f
commit 980cbbe
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
  *