From 5130412f6f695174f640db606e247b59be2ffa09 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Wed, 19 Nov 2025 23:41:29 +0000 Subject: [PATCH 1/4] Strengthen preconditions on polyveck_add() and polyvecl_add() Adds explicit bounds constraints on the inputs to these two functions. These significantly reduce the state space of the inputs, and therefore reduce the space that CBMC/Z3 has to search to find a proof. Calling functions (attempt_signature_generataion() and crypto_sign_keypair_internal() ) re-prove OK with these pre-conditions in place. Signed-off-by: Rod Chapman --- mldsa/src/polyvec.h | 34 ++++++++++++++++++++-------------- 1 file changed, 20 insertions(+), 14 deletions(-) diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h index 06f1174ec..69e2cb772 100644 --- a/mldsa/src/polyvec.h +++ b/mldsa/src/polyvec.h @@ -81,21 +81,24 @@ __contract__( * No modular reduction is performed. * * Arguments: - mld_polyveck *u: pointer to input-output vector of polynomials - *to be added to + * to be added to * - const mld_polyveck *v: pointer to second input vector of - * polynomials + * polynomials **************************************************/ MLD_INTERNAL_API void mld_polyvecl_add(mld_polyvecl *u, const mld_polyvecl *v) __contract__( requires(memory_no_alias(u, sizeof(mld_polyvecl))) requires(memory_no_alias(v, sizeof(mld_polyvecl))) - requires(forall(k0, 0, MLDSA_L, forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] < REDUCE32_DOMAIN_MAX))) - requires(forall(k2, 0, MLDSA_L, forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN))) + requires(forall(p0, 0, MLDSA_L, array_abs_bound(u->vec[p0].coeffs, 0 , MLDSA_N, MLD_INTT_BOUND))) + requires(forall(p1, 0, MLDSA_L, + array_bound(v->vec[p1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) + requires(forall(p2, 0, MLDSA_L, forall(p3, 0, MLDSA_N, (int64_t) u->vec[p2].coeffs[p3] + v->vec[p2].coeffs[p3] < REDUCE32_DOMAIN_MAX))) + requires(forall(p4, 0, MLDSA_L, forall(p5, 0, MLDSA_N, (int64_t) u->vec[p4].coeffs[p5] + v->vec[p4].coeffs[p5] >= INT32_MIN))) assigns(object_whole(u)) - ensures(forall(k4, 0, MLDSA_L, forall(k5, 0, MLDSA_N, u->vec[k4].coeffs[k5] == old(*u).vec[k4].coeffs[k5] + v->vec[k4].coeffs[k5]))) - ensures(forall(k6, 0, MLDSA_L, - array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX))) + ensures(forall(q0, 0, MLDSA_L, forall(q1, 0, MLDSA_N, u->vec[q0].coeffs[q1] == old(*u).vec[q0].coeffs[q1] + v->vec[q0].coeffs[q1]))) + ensures(forall(q2, 0, MLDSA_L, + array_bound(u->vec[q2].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX))) ); #define mld_polyvecl_ntt MLD_NAMESPACE_KL(polyvecl_ntt) @@ -279,21 +282,24 @@ __contract__( * No modular reduction is performed. * * Arguments: - mld_polyveck *u: pointer to input-output vector of polynomials - *to be added to + * to be added to * - const mld_polyveck *v: pointer to second input vector of - * polynomials + * polynomials **************************************************/ MLD_INTERNAL_API void mld_polyveck_add(mld_polyveck *u, const mld_polyveck *v) __contract__( requires(memory_no_alias(u, sizeof(mld_polyveck))) requires(memory_no_alias(v, sizeof(mld_polyveck))) - requires(forall(k0, 0, MLDSA_K, forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] < REDUCE32_DOMAIN_MAX))) - requires(forall(k2, 0, MLDSA_K, forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN))) + requires(forall(p0, 0, MLDSA_K, array_abs_bound(u->vec[p0].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))) + requires(forall(p1, 0, MLDSA_K, + array_bound(v->vec[p1].coeffs, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX))) + requires(forall(p2, 0, MLDSA_K, forall(p3, 0, MLDSA_N, (int64_t) u->vec[p2].coeffs[p3] + v->vec[p2].coeffs[p3] < REDUCE32_DOMAIN_MAX))) + requires(forall(p4, 0, MLDSA_K, forall(p5, 0, MLDSA_N, (int64_t) u->vec[p4].coeffs[p5] + v->vec[p4].coeffs[p5] >= INT32_MIN))) assigns(object_whole(u)) - ensures(forall(k4, 0, MLDSA_K, forall(k5, 0, MLDSA_N, u->vec[k4].coeffs[k5] == old(*u).vec[k4].coeffs[k5] + v->vec[k4].coeffs[k5]))) - ensures(forall(k6, 0, MLDSA_L, - array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX))) + ensures(forall(q0, 0, MLDSA_K, forall(q1, 0, MLDSA_N, u->vec[q0].coeffs[q1] == old(*u).vec[q0].coeffs[q1] + v->vec[q0].coeffs[q1]))) + ensures(forall(q2, 0, MLDSA_L, + array_bound(u->vec[q2].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX))) ); #define mld_polyveck_sub MLD_NAMESPACE_KL(polyveck_sub) From 390c3e054711ddd836d591ed7ec6dfb1264e7d41 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Thu, 20 Nov 2025 12:54:24 +0000 Subject: [PATCH 2/4] Remove now-redundant preconditions Signed-off-by: Rod Chapman --- mldsa/src/polyvec.h | 4 ---- 1 file changed, 4 deletions(-) diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h index 69e2cb772..7bc88468c 100644 --- a/mldsa/src/polyvec.h +++ b/mldsa/src/polyvec.h @@ -93,8 +93,6 @@ __contract__( requires(forall(p0, 0, MLDSA_L, array_abs_bound(u->vec[p0].coeffs, 0 , MLDSA_N, MLD_INTT_BOUND))) requires(forall(p1, 0, MLDSA_L, array_bound(v->vec[p1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) - requires(forall(p2, 0, MLDSA_L, forall(p3, 0, MLDSA_N, (int64_t) u->vec[p2].coeffs[p3] + v->vec[p2].coeffs[p3] < REDUCE32_DOMAIN_MAX))) - requires(forall(p4, 0, MLDSA_L, forall(p5, 0, MLDSA_N, (int64_t) u->vec[p4].coeffs[p5] + v->vec[p4].coeffs[p5] >= INT32_MIN))) assigns(object_whole(u)) ensures(forall(q0, 0, MLDSA_L, forall(q1, 0, MLDSA_N, u->vec[q0].coeffs[q1] == old(*u).vec[q0].coeffs[q1] + v->vec[q0].coeffs[q1]))) ensures(forall(q2, 0, MLDSA_L, @@ -294,8 +292,6 @@ __contract__( requires(forall(p0, 0, MLDSA_K, array_abs_bound(u->vec[p0].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))) requires(forall(p1, 0, MLDSA_K, array_bound(v->vec[p1].coeffs, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX))) - requires(forall(p2, 0, MLDSA_K, forall(p3, 0, MLDSA_N, (int64_t) u->vec[p2].coeffs[p3] + v->vec[p2].coeffs[p3] < REDUCE32_DOMAIN_MAX))) - requires(forall(p4, 0, MLDSA_K, forall(p5, 0, MLDSA_N, (int64_t) u->vec[p4].coeffs[p5] + v->vec[p4].coeffs[p5] >= INT32_MIN))) assigns(object_whole(u)) ensures(forall(q0, 0, MLDSA_K, forall(q1, 0, MLDSA_N, u->vec[q0].coeffs[q1] == old(*u).vec[q0].coeffs[q1] + v->vec[q0].coeffs[q1]))) ensures(forall(q2, 0, MLDSA_L, From a5b4dcd03931149625fa34a64ea9763dff62c1f1 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Fri, 21 Nov 2025 15:13:26 +0000 Subject: [PATCH 3/4] Weaken post-condition and invariant of polyvecl_add() Signed-off-by: Rod Chapman --- mldsa/src/polyvec.c | 1 - mldsa/src/polyvec.h | 1 - 2 files changed, 2 deletions(-) diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index f4c8d7567..25b07e7ef 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -256,7 +256,6 @@ void mld_polyvecl_add(mld_polyvecl *u, const mld_polyvecl *v) invariant(i <= MLDSA_L) invariant(forall(k0, i, MLDSA_L, forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1]))) - invariant(forall(k4, 0, i, forall(k5, 0, MLDSA_N, u->vec[k4].coeffs[k5] == loop_entry(*u).vec[k4].coeffs[k5] + v->vec[k4].coeffs[k5]))) invariant(forall(k6, 0, i, array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX))) ) { diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h index 7bc88468c..a58717a7c 100644 --- a/mldsa/src/polyvec.h +++ b/mldsa/src/polyvec.h @@ -94,7 +94,6 @@ __contract__( requires(forall(p1, 0, MLDSA_L, array_bound(v->vec[p1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) assigns(object_whole(u)) - ensures(forall(q0, 0, MLDSA_L, forall(q1, 0, MLDSA_N, u->vec[q0].coeffs[q1] == old(*u).vec[q0].coeffs[q1] + v->vec[q0].coeffs[q1]))) ensures(forall(q2, 0, MLDSA_L, array_bound(u->vec[q2].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX))) ); From 3606284c59be6a9a7dcc3e7d4e708a216f378d75 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Sun, 23 Nov 2025 15:04:32 +0000 Subject: [PATCH 4/4] Correct postcondition and invariant of polyveck_add() Signed-off-by: Rod Chapman --- mldsa/src/polyvec.c | 1 - mldsa/src/polyvec.h | 3 +-- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index 25b07e7ef..a2e07c6ff 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -495,7 +495,6 @@ void mld_polyveck_add(mld_polyveck *u, const mld_polyveck *v) invariant(i <= MLDSA_K) invariant(forall(k0, i, MLDSA_K, forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1]))) - invariant(forall(k4, 0, i, forall(k5, 0, MLDSA_N, u->vec[k4].coeffs[k5] == loop_entry(*u).vec[k4].coeffs[k5] + v->vec[k4].coeffs[k5]))) invariant(forall(k6, 0, i, array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX))) ) { diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h index a58717a7c..8f2c7f92e 100644 --- a/mldsa/src/polyvec.h +++ b/mldsa/src/polyvec.h @@ -292,8 +292,7 @@ __contract__( requires(forall(p1, 0, MLDSA_K, array_bound(v->vec[p1].coeffs, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX))) assigns(object_whole(u)) - ensures(forall(q0, 0, MLDSA_K, forall(q1, 0, MLDSA_N, u->vec[q0].coeffs[q1] == old(*u).vec[q0].coeffs[q1] + v->vec[q0].coeffs[q1]))) - ensures(forall(q2, 0, MLDSA_L, + ensures(forall(q2, 0, MLDSA_K, array_bound(u->vec[q2].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX))) );