Merge pull request #262 from pq-code-package/mlkem

Rename Kyber -> ML-KEM

.github/actions/cbmc/action.yml

@@ -45,7 +45,7 @@ runs:
         run: |
           cd cbmc/proofs;
           echo "::group::cbmc"
-          KYBER_K=2 ./run-cbmc-proofs.py --summarize;
-          KYBER_K=3 ./run-cbmc-proofs.py --summarize;
-          KYBER_K=4 ./run-cbmc-proofs.py --summarize;
+          MLKEM_K=2 ./run-cbmc-proofs.py --summarize;
+          MLKEM_K=3 ./run-cbmc-proofs.py --summarize;
+          MLKEM_K=4 ./run-cbmc-proofs.py --summarize;
           echo "::endgroup::"

Makefile

@@ -26,31 +26,31 @@ quickcheck:
 
 	$(Q)echo "  Everything builds fine!"
         # Run basic functionality checks
-	$(MLKEM512_DIR)/bin/test_kyber512
-	$(MLKEM768_DIR)/bin/test_kyber768
-	$(MLKEM1024_DIR)/bin/test_kyber1024
+	$(MLKEM512_DIR)/bin/test_mlkem512
+	$(MLKEM768_DIR)/bin/test_mlkem768
+	$(MLKEM1024_DIR)/bin/test_mlkem1024
 	python3 ./test/acvp_client.py
 	$(Q)echo "  Functionality and ACVP tests passed!"
 
 mlkem: \
-  $(MLKEM512_DIR)/bin/test_kyber512 \
-  $(MLKEM768_DIR)/bin/test_kyber768 \
-  $(MLKEM1024_DIR)/bin/test_kyber1024
+  $(MLKEM512_DIR)/bin/test_mlkem512 \
+  $(MLKEM768_DIR)/bin/test_mlkem768 \
+  $(MLKEM1024_DIR)/bin/test_mlkem1024
 
 bench: \
-	$(MLKEM512_DIR)/bin/bench_kyber512 \
-	$(MLKEM768_DIR)/bin/bench_kyber768 \
-	$(MLKEM1024_DIR)/bin/bench_kyber1024
+	$(MLKEM512_DIR)/bin/bench_mlkem512 \
+	$(MLKEM768_DIR)/bin/bench_mlkem768 \
+	$(MLKEM1024_DIR)/bin/bench_mlkem1024
 
 acvp: \
-	$(MLKEM512_DIR)/bin/acvp_kyber512 \
-	$(MLKEM768_DIR)/bin/acvp_kyber768 \
-	$(MLKEM1024_DIR)/bin/acvp_kyber1024
+	$(MLKEM512_DIR)/bin/acvp_mlkem512 \
+	$(MLKEM768_DIR)/bin/acvp_mlkem768 \
+	$(MLKEM1024_DIR)/bin/acvp_mlkem1024
 
 bench_components: \
-	$(MLKEM512_DIR)/bin/bench_components_kyber512 \
-	$(MLKEM768_DIR)/bin/bench_components_kyber768 \
-	$(MLKEM1024_DIR)/bin/bench_components_kyber1024
+	$(MLKEM512_DIR)/bin/bench_components_mlkem512 \
+	$(MLKEM768_DIR)/bin/bench_components_mlkem768 \
+	$(MLKEM1024_DIR)/bin/bench_components_mlkem1024
 
 nistkat: \
 	$(MLKEM512_DIR)/bin/gen_NISTKAT512 \

cbmc/proofs/Makefile.common

@@ -528,11 +528,11 @@ DEFINES += -DCBMC=1
 DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)
 DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))"
 
-ifndef KYBER_K
-    $(error KYBER_K not set)
+ifndef MLKEM_K
+    $(error MLKEM_K not set)
 endif
 
-DEFINES += -DKYBER_K=$(KYBER_K)
+DEFINES += -DMLKEM_K=$(MLKEM_K)
 
 # CI currently assumes cbmc invocation has at most one --unwindset
 

cbmc/proofs/Makefile_params.common

@@ -1,17 +1,17 @@
 # SPDX-License-Identifier: Apache-2.0
 
-ifndef KYBER_K
-       $(warning KYBER_K not set -- defaulting to KYBER_K=3)
+ifndef MLKEM_K
+       $(warning MLKEM_K not set -- defaulting to MLKEM_K=3)
 endif
 
-KYBER_K ?= 3
+MLKEM_K ?= 3
 
-ifeq ($(KYBER_K),2)
-     KYBER_NAMESPACE = pqcrystals_kyber512_ref_
-else ifeq ($(KYBER_K),3)
-     KYBER_NAMESPACE=pqcrystals_kyber768_ref_
-else ifeq ($(KYBER_K),4)
-     KYBER_NAMESPACE=pqcrystals_kyber1024_ref_
+ifeq ($(MLKEM_K),2)
+     MLKEM_NAMESPACE = pqcrystals_mlkem512_ref_
+else ifeq ($(MLKEM_K),3)
+     MLKEM_NAMESPACE=pqcrystals_mlkem768_ref_
+else ifeq ($(MLKEM_K),4)
+     MLKEM_NAMESPACE=pqcrystals_mlkem1024_ref_
 else
-     $(error Invalid value of KYBER_K)
+     $(error Invalid value of MLKEM_K)
 endif

cbmc/proofs/README.md

@@ -19,7 +19,7 @@ To run all proofs, print a summary at the end and reflect overall
 success/failure in the error code, use
 
 ```
-KYBER_K={2,3,4} run-cbmc-proofs.py --summarize
+MLKEM_K={2,3,4} run-cbmc-proofs.py --summarize
 ```
 
 If `GITHUB_STEP_SUMMARY` is set, the proof summary will be appended to it.

cbmc/proofs/barrett_reduce/Makefile

@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/reduce.c
 
-CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)barrett_reduce
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)barrett_reduce
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = $(KYBER_NAMESPACE)barrett_reduce
+FUNCTION_NAME = $(MLKEM_NAMESPACE)barrett_reduce
 
 # 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

cbmc/proofs/fqmul/Makefile

@@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/reduce.c
 
 CHECK_FUNCTION_CONTRACTS=fqmul
-USE_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)montgomery_reduce
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)montgomery_reduce
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 

cbmc/proofs/montgomery_reduce/Makefile

@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/reduce.c
 
-CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)montgomery_reduce
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)montgomery_reduce
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = $(KYBER_NAMESPACE)montgomery_reduce
+FUNCTION_NAME = $(MLKEM_NAMESPACE)montgomery_reduce
 
 # 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

cbmc/proofs/poly_compress/Makefile

@@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c
 
-CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)poly_compress
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = $(KYBER_NAMESPACE)poly_compress
+FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_compress
 
 # 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

cbmc/proofs/poly_compress/poly_compress_harness.c

@@ -23,7 +23,7 @@
  */
 void harness(void) {
   poly r;
-  uint8_t a[KYBER_POLYCOMPRESSEDBYTES];
+  uint8_t a[MLKEM_POLYCOMPRESSEDBYTES];
 
   poly_compress(a, &r);
 }

cbmc/proofs/poly_decompress/Makefile

@@ -19,13 +19,13 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c
 
-CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)poly_decompress
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress
 
 # For K = 2 or 3, the code calls scalar_decompress_q_16, so
-ifeq ($(KYBER_K),4)
-USE_FUNCTION_CONTRACTS = $(KYBER_NAMESPACE)scalar_decompress_q_32
+ifeq ($(MLKEM_K),4)
+USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_q_32
 else
-USE_FUNCTION_CONTRACTS = $(KYBER_NAMESPACE)scalar_decompress_q_16
+USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_q_16
 endif
 
 APPLY_LOOP_CONTRACTS=on
@@ -35,7 +35,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-FUNCTION_NAME = $(KYBER_NAMESPACE)poly_decompress
+FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_decompress
 
 # 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

cbmc/proofs/poly_decompress/poly_decompress_harness.c

@@ -23,7 +23,7 @@
  */
 void harness(void) {
   poly r;
-  uint8_t a[KYBER_POLYCOMPRESSEDBYTES];
+  uint8_t a[MLKEM_POLYCOMPRESSEDBYTES];
 
   poly_decompress(&r, a);
 }

cbmc/proofs/poly_tobytes/Makefile

@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)poly_tobytes
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_tobytes
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-FUNCTION_NAME = $(KYBER_NAMESPACE)poly_tobytes
+FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_tobytes
 
 # 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

cbmc/proofs/poly_tobytes/poly_tobytes_harness.c

@@ -23,7 +23,7 @@
  */
 void harness(void) {
   poly a;
-  uint8_t r[KYBER_POLYBYTES];
+  uint8_t r[MLKEM_POLYBYTES];
 
   /* Contracts for this function are in poly.h */
   poly_tobytes(r, &a);

cbmc/proofs/scalar_compress_q_16/Makefile

@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)scalar_compress_q_16
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_q_16
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

cbmc/proofs/scalar_compress_q_32/Makefile

@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)scalar_compress_q_32
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_q_32
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

cbmc/proofs/scalar_decompress_q_16/Makefile

@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)scalar_decompress_q_16
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_q_16
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

cbmc/proofs/scalar_decompress_q_32/Makefile

@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)scalar_decompress_q_32
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_q_32
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile

@@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c
 
-CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)scalar_signed_to_unsigned_q_16
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_signed_to_unsigned_q_16
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

mk/schemes.mk

@@ -6,17 +6,17 @@ ifeq ($(OPT),1)
 endif
 
 CPPFLAGS += -Imlkem -Imlkem/sys -Imlkem/native -Imlkem/native/aarch64 -Imlkem/native/x86_64
-TESTS = test_kyber acvp_kyber bench_kyber bench_components_kyber gen_NISTKAT gen_KAT
+TESTS = test_mlkem acvp_mlkem bench_mlkem bench_components_mlkem gen_NISTKAT gen_KAT
 
 MLKEM512_DIR = $(BUILD_DIR)/mlkem512
 MLKEM768_DIR = $(BUILD_DIR)/mlkem768
 MLKEM1024_DIR = $(BUILD_DIR)/mlkem1024
 
-$(MLKEM512_DIR)/bin/%: CPPFLAGS += -DKYBER_K=2
+$(MLKEM512_DIR)/bin/%: CPPFLAGS += -DMLKEM_K=2
 $(TESTS:%=$(MLKEM512_DIR)/bin/%512):$(MLKEM512_DIR)/bin/%512: $(MLKEM512_DIR)/test/%.c.o $(call MAKE_OBJS,$(MLKEM512_DIR),$(SOURCES))
 
-$(MLKEM768_DIR)/bin/%: CPPFLAGS += -DKYBER_K=3
+$(MLKEM768_DIR)/bin/%: CPPFLAGS += -DMLKEM_K=3
 $(TESTS:%=$(MLKEM768_DIR)/bin/%768):$(MLKEM768_DIR)/bin/%768: $(MLKEM768_DIR)/test/%.c.o $(call MAKE_OBJS,$(MLKEM768_DIR),$(SOURCES))
 
-$(MLKEM1024_DIR)/bin/%: CPPFLAGS += -DKYBER_K=4
+$(MLKEM1024_DIR)/bin/%: CPPFLAGS += -DMLKEM_K=4
 $(TESTS:%=$(MLKEM1024_DIR)/bin/%1024):$(MLKEM1024_DIR)/bin/%1024: $(MLKEM1024_DIR)/test/%.c.o  $(call MAKE_OBJS,$(MLKEM1024_DIR),$(SOURCES))