Update MLKEM_NAMESPACE to MLK_NAMESPACE for all new proofs

Signed-off-by: Rod Chapman <rodchap@amazon.com>
pq-code-package · Feb 6, 2025 · 413c9fa · 413c9fa
1 parent b588f60
commit 413c9fa
Show file tree

Hide file tree

Showing 17 changed files with 29 additions and 29 deletions.
diff --git a/proofs/cbmc/invntt_layer321/Makefile b/proofs/cbmc/invntt_layer321/Makefile
@@ -19,16 +19,16 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer321
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul
+CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer321
+USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)fqmul
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)invntt_layer321
+FUNCTION_NAME = $(MLK_NAMESPACE)invntt_layer321
 
 # 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/proofs/cbmc/invntt_layer321/invntt_layer321_harness.c b/proofs/cbmc/invntt_layer321/invntt_layer321_harness.c
@@ -4,7 +4,7 @@
 
 #include <poly.h>
 
-#define invntt_layer321 MLKEM_NAMESPACE(invntt_layer321)
+#define invntt_layer321 MLK_NAMESPACE(invntt_layer321)
 void invntt_layer321(int16_t *r);
 
 /**

diff --git a/proofs/cbmc/invntt_layer54/Makefile b/proofs/cbmc/invntt_layer54/Makefile
@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)invntt_layer54
+FUNCTION_NAME = $(MLK_NAMESPACE)invntt_layer54
 
 # 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/proofs/cbmc/invntt_layer54/invntt_layer54_harness.c b/proofs/cbmc/invntt_layer54/invntt_layer54_harness.c
@@ -4,7 +4,7 @@
 
 #include <poly.h>
 
-#define invntt_layer54 MLKEM_NAMESPACE(invntt_layer54)
+#define invntt_layer54 MLK_NAMESPACE(invntt_layer54)
 void invntt_layer54(int16_t *r);
 
 /**

diff --git a/proofs/cbmc/invntt_layer54_butterfly/Makefile b/proofs/cbmc/invntt_layer54_butterfly/Makefile
@@ -19,16 +19,16 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer54_butterfly
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul $(MLKEM_NAMESPACE)barrett_reduce
+CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer54_butterfly
+USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)fqmul $(MLK_NAMESPACE)barrett_reduce
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)invntt_layer54_butterfly
+FUNCTION_NAME = $(MLK_NAMESPACE)invntt_layer54_butterfly
 
 # 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/proofs/cbmc/invntt_layer54_butterfly/invntt_layer54_butterfly_harness.c b/proofs/cbmc/invntt_layer54_butterfly/invntt_layer54_butterfly_harness.c
@@ -4,7 +4,7 @@
 
 #include <poly.h>
 
-#define invntt_layer54_butterfly MLKEM_NAMESPACE(invntt_layer54_butterfly)
+#define invntt_layer54_butterfly MLK_NAMESPACE(invntt_layer54_butterfly)
 void invntt_layer54_butterfly(int16_t r[MLKEM_N], const unsigned zeta_index,
                               const unsigned start);
 

diff --git a/proofs/cbmc/invntt_layer6/Makefile b/proofs/cbmc/invntt_layer6/Makefile
@@ -19,16 +19,16 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer6
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul
+CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer6
+USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)fqmul
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)invntt_layer6
+FUNCTION_NAME = $(MLK_NAMESPACE)invntt_layer6
 
 # 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/proofs/cbmc/invntt_layer6/invntt_layer6_harness.c b/proofs/cbmc/invntt_layer6/invntt_layer6_harness.c
@@ -4,7 +4,7 @@
 
 #include <poly.h>
 
-#define invntt_layer6 MLKEM_NAMESPACE(invntt_layer6)
+#define invntt_layer6 MLK_NAMESPACE(invntt_layer6)
 void invntt_layer6(int16_t *r);
 
 /**

diff --git a/proofs/cbmc/invntt_layer7_invert/invntt_layer7_invert_harness.c b/proofs/cbmc/invntt_layer7_invert/invntt_layer7_invert_harness.c
@@ -4,7 +4,7 @@
 
 #include <poly.h>
 
-#define invntt_layer7_invert MLKEM_NAMESPACE(invntt_layer7_invert)
+#define invntt_layer7_invert MLK_NAMESPACE(invntt_layer7_invert)
 void invntt_layer7_invert(int16_t *r);
 
 /**

diff --git a/proofs/cbmc/ntt_layer123/Makefile b/proofs/cbmc/ntt_layer123/Makefile
@@ -19,16 +19,16 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer123
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul
+CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)ntt_layer123
+USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)fqmul
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)ntt_layer123
+FUNCTION_NAME = $(MLK_NAMESPACE)ntt_layer123
 
 # 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/proofs/cbmc/ntt_layer123/ntt_layer123_harness.c b/proofs/cbmc/ntt_layer123/ntt_layer123_harness.c
@@ -4,7 +4,7 @@
 
 #include <poly.h>
 
-#define ntt_layer123 MLKEM_NAMESPACE(ntt_layer123)
+#define ntt_layer123 MLK_NAMESPACE(ntt_layer123)
 void ntt_layer123(int16_t *r);
 
 /**

diff --git a/proofs/cbmc/ntt_layer45/Makefile b/proofs/cbmc/ntt_layer45/Makefile
@@ -18,16 +18,16 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer45
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer45_butterfly
+CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)ntt_layer45
+USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)ntt_layer45_butterfly
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)ntt_layer45
+FUNCTION_NAME = $(MLK_NAMESPACE)ntt_layer45
 
 # 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/proofs/cbmc/ntt_layer45/ntt_layer45_harness.c b/proofs/cbmc/ntt_layer45/ntt_layer45_harness.c
@@ -4,7 +4,7 @@
 
 #include <poly.h>
 
-#define ntt_layer45 MLKEM_NAMESPACE(ntt_layer45)
+#define ntt_layer45 MLK_NAMESPACE(ntt_layer45)
 void ntt_layer45(int16_t *r);
 
 /**

diff --git a/proofs/cbmc/ntt_layer45_butterfly/Makefile b/proofs/cbmc/ntt_layer45_butterfly/Makefile
@@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)ntt_layer45_butterfly
+FUNCTION_NAME = $(MLK_NAMESPACE)ntt_layer45_butterfly
 
 # 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/proofs/cbmc/ntt_layer45_butterfly/ntt_layer45_butterfly_harness.c b/proofs/cbmc/ntt_layer45_butterfly/ntt_layer45_butterfly_harness.c
@@ -4,7 +4,7 @@
 
 #include <poly.h>
 
-#define ntt_layer45_butterfly MLKEM_NAMESPACE(ntt_layer45_butterfly)
+#define ntt_layer45_butterfly MLK_NAMESPACE(ntt_layer45_butterfly)
 void ntt_layer45_butterfly(int16_t r[MLKEM_N],
                            const unsigned zeta_subtree_index,
                            const unsigned start);

diff --git a/proofs/cbmc/ntt_layer6/Makefile b/proofs/cbmc/ntt_layer6/Makefile
@@ -19,16 +19,16 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer6
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul
+CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)ntt_layer6
+USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)fqmul
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)ntt_layer6
+FUNCTION_NAME = $(MLK_NAMESPACE)ntt_layer6
 
 # 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/proofs/cbmc/ntt_layer6/ntt_layer6_harness.c b/proofs/cbmc/ntt_layer6/ntt_layer6_harness.c
@@ -4,7 +4,7 @@
 
 #include <poly.h>
 
-#define ntt_layer6 MLKEM_NAMESPACE(ntt_layer6)
+#define ntt_layer6 MLK_NAMESPACE(ntt_layer6)
 void ntt_layer6(int16_t *r);
 
 /**