From 6b80fb49b0a087cc02b6104a44433006e07a613d Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Fri, 8 Nov 2024 11:42:36 +0000 Subject: [PATCH] Improve speed of polyvec_add() proof. Removes detailed ENSURES clause for polyvec_add() since this is not required for proof of type-safety of calling units. Add comment explaining why a strong ENSURES clause on polyvec_add() is NOT required for proof of type-safety. Signed-off-by: Rod Chapman --- mlkem/polyvec.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/mlkem/polyvec.h b/mlkem/polyvec.h index 88a3c11d9..d139487ff 100644 --- a/mlkem/polyvec.h +++ b/mlkem/polyvec.h @@ -237,13 +237,16 @@ ENSURES(FORALL(int, k0, 0, MLKEM_K - 1, * * Description: Add vectors of polynomials * - * Arguments: - polyvec *r: pointer to input-output vector of polynomials to be - *added to + * Arguments: - polyvec *r: pointer to input-output vector of polynomials to be + * added to * - const polyvec *b: pointer to second input vector of polynomials * * The coefficients of r and b must be so that the addition does * not overflow. Otherwise, the behaviour of this function is undefined. * + * The coefficients returned in *r are in int16_t which is sufficient + * to prove type-safety of calling units. Therefore, no stronger + * ENSURES clause is required on this function. **************************************************/ void polyvec_add(polyvec *r, const polyvec *b) // clang-format off REQUIRES(IS_FRESH(r, sizeof(polyvec))) @@ -254,9 +257,6 @@ REQUIRES(FORALL(int, j0, 0, MLKEM_K - 1, REQUIRES(FORALL(int, j1, 0, MLKEM_K - 1, FORALL(int, k1, 0, MLKEM_N - 1, (int32_t)r->vec[j1].coeffs[k1] + b->vec[j1].coeffs[k1] >= INT16_MIN))) -ENSURES(FORALL(int, j, 0, MLKEM_K - 1, - FORALL(int, k, 0, MLKEM_N - 1, - r->vec[j].coeffs[k] == OLD(*r).vec[j].coeffs[k] + b->vec[j].coeffs[k]))) ASSIGNS(OBJECT_WHOLE(r)); // clang-format on