From bf5b5af99f8bbc74354ac7a652950f23029616f9 Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Mon, 11 May 2026 20:22:17 -0400 Subject: [PATCH 1/6] Avoid mismatched comparison (suggested code improvement, not a bug!) Signed-off-by: Nicky Mouha --- mlkem/src/verify.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mlkem/src/verify.h b/mlkem/src/verify.h index 600afa44a..0911a46b8 100644 --- a/mlkem/src/verify.h +++ b/mlkem/src/verify.h @@ -333,7 +333,7 @@ __contract__( ensures((return_value == 0) == forall(i, 0, len, (a[i] == b[i])))) { uint8_t r = 0, s = 0; - unsigned i; + size_t i; for (i = 0; i < len; i++) __loop__( From 82e4dc9425bb4521649f4fc777081fae5c0ba33b Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 12:24:21 -0400 Subject: [PATCH 2/6] cbmc.h: fix forall/exists to quantize over all indices Signed-off-by: Nicky Mouha --- mlkem/src/cbmc.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mlkem/src/cbmc.h b/mlkem/src/cbmc.h index 80e1a36fc..07fcf13de 100644 --- a/mlkem/src/cbmc.h +++ b/mlkem/src/cbmc.h @@ -89,14 +89,14 @@ #define forall(qvar, qvar_lb, qvar_ub, predicate) \ __CPROVER_forall \ { \ - unsigned qvar; \ + size_t qvar; \ ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> (predicate) \ } #define exists(qvar, qvar_lb, qvar_ub, predicate) \ __CPROVER_exists \ { \ - unsigned qvar; \ + size_t qvar; \ ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) && (predicate) \ } /* clang-format on */ From 1229cc13f4e0f3bfcc8392b36c259cf6705591bc Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 12:25:31 -0400 Subject: [PATCH 3/6] verify.h: relax bound on len Signed-off-by: Nicky Mouha --- mlkem/src/verify.h | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/mlkem/src/verify.h b/mlkem/src/verify.h index 0911a46b8..d8fbf30f6 100644 --- a/mlkem/src/verify.h +++ b/mlkem/src/verify.h @@ -317,8 +317,7 @@ __contract__(ensures(return_value == (cond ? a : b))) * * @param[in] a First byte array. * @param[in] b Second byte array. - * @param len Length of the byte arrays, upper-bounded to UINT16_MAX to - * control proof complexity only. + * @param len Length of the byte arrays. * * @retval 0 The byte arrays are equal. * @retval 0xFF The byte arrays are not equal. @@ -326,7 +325,7 @@ __contract__(ensures(return_value == (cond ? a : b))) static MLK_INLINE uint8_t mlk_ct_memcmp(const uint8_t *a, const uint8_t *b, const size_t len) __contract__( - requires(len <= UINT16_MAX) + requires(len <= MLK_MAX_BUFFER_SIZE) requires(memory_no_alias(a, len)) requires(memory_no_alias(b, len)) ensures((return_value == 0) || (return_value == 0xFF)) From 7a03a4d43ce7843a7ece01bda04ae1e18191d3a4 Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 12:35:30 -0400 Subject: [PATCH 4/6] cbmc.h: fix spaces Signed-off-by: Nicky Mouha --- mlkem/src/cbmc.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mlkem/src/cbmc.h b/mlkem/src/cbmc.h index 07fcf13de..4d5b7c700 100644 --- a/mlkem/src/cbmc.h +++ b/mlkem/src/cbmc.h @@ -96,7 +96,7 @@ #define exists(qvar, qvar_lb, qvar_ub, predicate) \ __CPROVER_exists \ { \ - size_t qvar; \ + size_t qvar; \ ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) && (predicate) \ } /* clang-format on */ From 0bc7711a9cc1d9d28102207edb13713ceebd8985 Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 17:02:52 -0400 Subject: [PATCH 5/6] proofs/cbmc/ct_memcmp/Makefile: use cvc5 instead of bitwuzla Signed-off-by: Nicky Mouha --- proofs/cbmc/ct_memcmp/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/cbmc/ct_memcmp/Makefile b/proofs/cbmc/ct_memcmp/Makefile index 7b7c1ce1f..51c060096 100644 --- a/proofs/cbmc/ct_memcmp/Makefile +++ b/proofs/cbmc/ct_memcmp/Makefile @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--bitwuzla +CBMCFLAGS=--cvc5 FUNCTION_NAME = mlk_ct_memcmp From 3eda479f8004cebc6b99cb3e3912cafecd8c2c77 Mon Sep 17 00:00:00 2001 From: Nicky Mouha Date: Tue, 12 May 2026 20:13:47 -0400 Subject: [PATCH 6/6] add cvc5 to Nix config, fix all timeouts Signed-off-by: Nicky Mouha --- flake.nix | 4 ++-- nix/cbmc/default.nix | 2 ++ nix/util.nix | 4 ++-- proofs/cbmc/indcpa_dec/Makefile | 2 +- proofs/cbmc/indcpa_enc/Makefile | 2 +- proofs/cbmc/indcpa_keypair_derand/Makefile | 2 +- proofs/cbmc/keccak_squeeze_once/Makefile | 2 +- proofs/cbmc/nttunpack_native_x86_64/Makefile | 2 +- proofs/cbmc/poly_ntt_native/Makefile | 2 +- proofs/cbmc/poly_reduce_native/Makefile | 2 +- 10 files changed, 13 insertions(+), 11 deletions(-) diff --git a/flake.nix b/flake.nix index 31483560a..be16a6adf 100644 --- a/flake.nix +++ b/flake.nix @@ -25,7 +25,7 @@ pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.${system}; pkgs-2405 = inputs.nixpkgs-2405.legacyPackages.${system}; util = pkgs.callPackage ./nix/util.nix { - inherit (pkgs) bitwuzla z3; + inherit (pkgs) bitwuzla cvc5 z3; inherit (pkgs-unstable) cbmc; # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11 python3-for-slothy = pkgs-unstable.python3; @@ -237,7 +237,7 @@ pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.x86_64-linux; util = pkgs.callPackage ./nix/util.nix { inherit pkgs; - inherit (pkgs) bitwuzla z3; + inherit (pkgs) bitwuzla cvc5 z3; inherit (pkgs-unstable) cbmc; # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11 python3-for-slothy = pkgs-unstable.python3; diff --git a/nix/cbmc/default.nix b/nix/cbmc/default.nix index 58e21c796..e33f885f0 100644 --- a/nix/cbmc/default.nix +++ b/nix/cbmc/default.nix @@ -3,6 +3,7 @@ # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT { buildEnv , cbmc +, cvc5 , fetchFromGitHub , callPackage , bitwuzla @@ -37,6 +38,7 @@ buildEnv { inherit bitwuzla# 0.8.2 + cvc5# 1.3.2 ninja; # 1.13.2 }; } diff --git a/nix/util.nix b/nix/util.nix index c63835721..c67116933 100644 --- a/nix/util.nix +++ b/nix/util.nix @@ -2,7 +2,7 @@ # Copyright (c) The mldsa-native project authors # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -{ pkgs, cbmc, bitwuzla, z3, python3-for-slothy }: +{ pkgs, cbmc, bitwuzla, cvc5, z3, python3-for-slothy }: rec { glibc-join = p: p.buildPackages.symlinkJoin { name = "glibc-join"; @@ -96,7 +96,7 @@ rec { }; }; - cbmc_pkgs = pkgs.callPackage ./cbmc { inherit cbmc bitwuzla z3; }; + cbmc_pkgs = pkgs.callPackage ./cbmc { inherit cbmc bitwuzla cvc5 z3; }; valgrind_varlat = pkgs.callPackage ./valgrind { }; hol_light' = pkgs.callPackage ./hol_light { }; diff --git a/proofs/cbmc/indcpa_dec/Makefile b/proofs/cbmc/indcpa_dec/Makefile index 0233f0b81..27c8af140 100644 --- a/proofs/cbmc/indcpa_dec/Makefile +++ b/proofs/cbmc/indcpa_dec/Makefile @@ -37,7 +37,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--cvc5 --refine-arrays FUNCTION_NAME = mlk_indcpa_dec diff --git a/proofs/cbmc/indcpa_enc/Makefile b/proofs/cbmc/indcpa_enc/Makefile index e9ac63b84..ddc2a955c 100644 --- a/proofs/cbmc/indcpa_enc/Makefile +++ b/proofs/cbmc/indcpa_enc/Makefile @@ -43,7 +43,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_smt_only --z3 +CBMCFLAGS=--cvc5 --refine-arrays FUNCTION_NAME = mlk_indcpa_enc diff --git a/proofs/cbmc/indcpa_keypair_derand/Makefile b/proofs/cbmc/indcpa_keypair_derand/Makefile index 115e78769..51bd35025 100644 --- a/proofs/cbmc/indcpa_keypair_derand/Makefile +++ b/proofs/cbmc/indcpa_keypair_derand/Makefile @@ -36,7 +36,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--cvc5 --refine-arrays FUNCTION_NAME = mlk_indcpa_keypair_derand diff --git a/proofs/cbmc/keccak_squeeze_once/Makefile b/proofs/cbmc/keccak_squeeze_once/Makefile index afa7ade38..90cf523f3 100644 --- a/proofs/cbmc/keccak_squeeze_once/Makefile +++ b/proofs/cbmc/keccak_squeeze_once/Makefile @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--bitwuzla +CBMCFLAGS=--z3 FUNCTION_NAME = mlk_keccak_squeeze_once diff --git a/proofs/cbmc/nttunpack_native_x86_64/Makefile b/proofs/cbmc/nttunpack_native_x86_64/Makefile index f54a2ce0b..d865e27a7 100644 --- a/proofs/cbmc/nttunpack_native_x86_64/Makefile +++ b/proofs/cbmc/nttunpack_native_x86_64/Makefile @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--cvc5 --refine-arrays FUNCTION_NAME = nttunpack_native_x86_64 diff --git a/proofs/cbmc/poly_ntt_native/Makefile b/proofs/cbmc/poly_ntt_native/Makefile index fb2924e5f..50981df71 100644 --- a/proofs/cbmc/poly_ntt_native/Makefile +++ b/proofs/cbmc/poly_ntt_native/Makefile @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--bitwuzla +CBMCFLAGS=--cvc5 --refine-arrays FUNCTION_NAME = mlk_poly_ntt diff --git a/proofs/cbmc/poly_reduce_native/Makefile b/proofs/cbmc/poly_reduce_native/Makefile index 8a1202b90..e85b86916 100644 --- a/proofs/cbmc/poly_reduce_native/Makefile +++ b/proofs/cbmc/poly_reduce_native/Makefile @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--bitwuzla +CBMCFLAGS=--cvc5 --refine-arrays FUNCTION_NAME = mlk_poly_reduce_native