Skip to content
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

Jump to bottom

CBMC: Add spec + proof for polyvec_basemul_acc_montgomery_cached + poly_add #306

Merged
merged 2 commits into from
Nov 5, 2024
Merged

CBMC: Add spec + proof for polyvec_basemul_acc_montgomery_cached + poly_add #306

merged 2 commits into from
Nov 5, 2024

Conversation

hanno-becker
Copy link
Contributor

No description provided.

@hanno-becker hanno-becker marked this pull request as ready for review November 2, 2024 05:36
@hanno-becker
Copy link
Contributor Author

@rod-chapman Something strange is happening here: The aliasing-precondition r==a in the poly_add() contracts seems to be contradictory to CBMC -- you can even put 0==1 in the post-condition, and the proof will go through. But, the contract can be used by the caller polyvec_basemul_acc_montgomery_cached(). This seems worrying to me. Can you explain what's going on?

@hanno-becker
Copy link
Contributor Author

I used SAME_OBJECT + POINTER_OFFSET to express pointer equality for now, which seems to work better. Still, the aliasing issue needs investigating.

@hanno-becker hanno-becker mentioned this pull request Nov 2, 2024
Closed
@hanno-becker hanno-becker force-pushed the polyvec_add branch 2 times, most recently from 7adc7e8 to 2374e95 Compare November 2, 2024 17:25
mkannwischer
mkannwischer requested changes Nov 4, 2024
View reviewed changes
Copy link
Contributor

@mkannwischer mkannwischer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @hanno-becker! The pre- and post-conditions are looking good. Some small suggestions.

Also could you add to the PR title that this also proves poly_add?

mlkem/poly.h Outdated Show resolved Hide resolved
mlkem/poly.h Outdated Show resolved Hide resolved
mlkem/poly.h Outdated Show resolved Hide resolved
mlkem/polyvec.h Outdated Show resolved Hide resolved
mlkem/polyvec.c Outdated Show resolved Hide resolved
@hanno-becker hanno-becker changed the title CBMC: Add spec + proof for polyvec_basemul_acc_montgomery_cached CBMC: Add spec + proof for polyvec_basemul_acc_montgomery_cached + poly_add Nov 4, 2024
@hanno-becker hanno-becker mentioned this pull request Nov 4, 2024
Closed
2 tasks
@hanno-becker hanno-becker mentioned this pull request Nov 4, 2024
Closed
3 tasks
@hanno-becker
Copy link
Contributor Author

hanno-becker commented Nov 4, 2024 •
edited
Loading

Opened #325 to discuss the right shape of harness

@hanno-becker
Copy link
Contributor Author

@mkannwischer @rod-chapman The reasoning about aliasing in poly_add() posed significant verification challenges that are ultimately unnecessary because poly_add() is always used in the aliased form.

I have thus specialized poly_add() to the accumulator-form, which rendered all proofs straightforward.

@hanno-becker hanno-becker force-pushed the polyvec_add branch 3 times, most recently from 63c0aee to 86e1d93 Compare November 4, 2024 12:51
mkannwischer
mkannwischer approved these changes Nov 5, 2024
View reviewed changes
Copy link
Contributor

@mkannwischer mkannwischer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! One typo in a comment - rest looks good to me now.

mlkem/polyvec.c Outdated Show resolved Hide resolved
mkannwischer
mkannwischer reviewed Nov 5, 2024
View reviewed changes
mlkem/poly.h Outdated Show resolved Hide resolved
mkannwischer
mkannwischer reviewed Nov 5, 2024
View reviewed changes
mlkem/polyvec.h Outdated Show resolved Hide resolved
@mkannwischer mkannwischer mentioned this pull request Nov 5, 2024
Merged
@hanno-becker hanno-becker force-pushed the polyvec_add branch 3 times, most recently from 3f93523 to b8e6d76 Compare November 5, 2024 05:44
mkannwischer
mkannwischer approved these changes Nov 5, 2024
View reviewed changes
Copy link
Contributor

@mkannwischer mkannwischer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for addressing my comments. Looks good now.

@hanno-becker
CBMC: Add spec + proof for poly_add()
d4fb3a7 
This commit adds a CBMC spec and proof for `poly_add()`.

Previously, poly_add() had the signature (r[out], a[in], b[in]), allowing
the output polynomial to be separate from the two input polynomials.
Yet, uses of `poly_add()` always have the form `poly_add(r,r,b)`,
aliasing the first and second parameters, and thereby accumulating `b`
onto `r`.

Since aliasing poses additional verification challenges, and the
non-aliased version of `poly_add()` is never used, this commit firstly
modifies the signature of `poly_add()` to only take two inputs,
accumulating the second onto the first.

With that done, the spec and proof in CBMC are straightforward, taking
care to use `OLD(...)` and `LOOP_ENTY(...)` in spec and loop invariants
to refer to the original values of memory.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
CBMC: Add spec + proof for polyvec_basemul_acc_montgomery_cached
af5daa9 
The proof is less trivial than the ones before since one has to use
the output bounds of the lower level functions to show that the
accumulation loop does not overflow.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@mkannwischer mkannwischer merged commit 183855e into main Nov 5, 2024
2 checks passed
@mkannwischer mkannwischer deleted the polyvec_add branch November 5, 2024 05:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mkannwischer mkannwischer mkannwischer approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@hanno-becker @mkannwischer