Skip to content

Avoid mismatched comparison and fix error in forall/exists macros #1690

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
nmouha wants to merge 6 commits into
base: main
Choose a base branch
from
Open

Avoid mismatched comparison and fix error in forall/exists macros #1690

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
bf5b5af
Avoid mismatched comparison (suggested code improvement, not a bug!)
nmouha May 12, 2026
82e4dc9
cbmc.h: fix forall/exists to quantize over all indices
nmouha May 12, 2026
1229cc1
verify.h: relax bound on len
nmouha May 12, 2026
7a03a4d
cbmc.h: fix spaces
nmouha May 12, 2026
0bc7711
proofs/cbmc/ct_memcmp/Makefile: use cvc5 instead of bitwuzla
nmouha May 12, 2026
3eda479
add cvc5 to Nix config, fix all timeouts
nmouha May 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions flake.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down
4 changes: 2 additions & 2 deletions mlkem/src/cbmc.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand Down
7 changes: 3 additions & 4 deletions mlkem/src/verify.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -317,23 +317,22 @@ __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.
*/
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__(
Expand Down
2 changes: 2 additions & 0 deletions nix/cbmc/default.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
{ buildEnv
, cbmc
, cvc5
, fetchFromGitHub
, callPackage
, bitwuzla
Expand Down Expand Up @@ -37,6 +38,7 @@ buildEnv {

inherit
bitwuzla# 0.8.2
cvc5# 1.3.2
ninja; # 1.13.2
};
}
4 changes: 2 additions & 2 deletions nix/util.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand Down Expand Up @@ -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 { };
Expand Down
2 changes: 1 addition & 1 deletion proofs/cbmc/ct_memcmp/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion proofs/cbmc/indcpa_dec/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion proofs/cbmc/indcpa_enc/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion proofs/cbmc/indcpa_keypair_derand/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion proofs/cbmc/keccak_squeeze_once/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion proofs/cbmc/nttunpack_native_x86_64/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion proofs/cbmc/poly_ntt_native/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion proofs/cbmc/poly_reduce_native/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading