Skip to content

Strengthen contracts on polyvec_matrix_pointwise_montgomery() and dependents #292

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.

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
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

rod-chapman
Copy link
Contributor

@rod-chapman rod-chapman commented May 27, 2025

Fixes #291

  1. Rename REDUCE_RANGE_MAX to REDUCE32_RANGE_MAX to help differentiate this constant from MONTGOMERY_REDUCE_RANGE_MAX.

  2. Similarly, and for consistency, REDUCE_DOMAIN_MAX is renamed to REDUCE32_DOMAIN_MAX

  3. Strengthen post-conditions and loop invariants of the following functions

montgomery_reduce()
polyvecl_pointwise_acc_montgomery()
polyvec_matrix_pointwise_montgomery()
  1. Tests, proofs, lint all OK.

…e this constant from MONTGOMERY_REDUCE_RANGE_MAX.

2. Similarly, and for consistency, REDUCE_DOMAIN_MAX is renamed to REDUCE32_DOMAIN_MAX

3. Strengthen post-conditions and loop invariants of the following functions

montgomery_reduce()
polyvecl_pointwise_acc_montgomery()
polyvec_matrix_pointwise_montgomery()

Signed-off-by: Rod Chapman <[email protected]>
@rod-chapman rod-chapman requested a review from a team as a code owner May 27, 2025 20:27
@rod-chapman rod-chapman requested a review from jakemas May 27, 2025 20:27
@rod-chapman rod-chapman self-assigned this May 27, 2025
@mkannwischer
Copy link
Contributor

Can we think this a bit further so we don't have to touch it again?
In verification we need the following:

polyvec_matrix_pointwise_montgomery(&w1, mat, &z);
polyveck_pointwise_poly_montgomery(&t1, &cp, &t1);

polyveck_sub(&w1, &t1);
polyveck_reduce(&w1);

This needs an even stricter post-condition on polyvec_matrix_pointwise_montgomery to not overflow the subtraction.

@rod-chapman
Copy link
Contributor Author

I will take a look, but there will be some latency - I am at a big meeting away from home.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

CBMC: strengthen postcondition of polyvec_matrix_pointwise_montgomery()
3 participants