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
  *