remove namspacing from static scalar_* functions

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

Hide file tree

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