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/mlkem/src/cbmc.h b/mlkem/src/cbmc.h index 80e1a36fc..4d5b7c700 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 */ diff --git a/mlkem/src/verify.h b/mlkem/src/verify.h index 600afa44a..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,14 +325,14 @@ __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)) 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__( 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/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 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