CBMC: Add contracts and proofs for more polyvec functions #169
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mkannwischer
force-pushed
the
cbmc-polyvec-proofs-slow
branch
from
e28b543 to
6407e51
Compare
|
Aha, it looks like we were working on the same functions at the same time! |
That's unfortunate. I usually create issues and assign myself to them to avoid this (I have done so for these functions in this case). If you can please assign yourself to issues you are working on/plan to work on then we can avoid race conditions like this in the future. |
mkannwischer
force-pushed
the
cbmc-polyvec-proofs-slow
branch
2 times, most recently
from
000e87b to
b241026
Compare
hanno-becker
force-pushed
the
cbmc-polyvec-proofs-slow
branch
from
b241026 to
2565882
Compare
mkannwischer
force-pushed
the
cbmc-polyvec-proofs-slow
branch
from
2565882 to
9e4e501
Compare
jakemas
approved these changes
Apr 24, 2025
jakemas
reviewed
Apr 24, 2025
CBMC: Add contract and proof for polyveck_caddq CBMC: Add contract and proof for polyvecl_ntt CBMC: Add contract and proof for polyveck_ntt Resolves #125 Resolves #133 Resolves #118 Resolves #129 Signed-off-by: Matthias J. Kannwischer <[email protected]>
rod-chapman
force-pushed
the
cbmc-polyvec-proofs-slow
branch
from
9e4e501 to
d67b68b
Compare
|
Looks good to me. All proofs, lint and tests OK. I will squash and merge. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
polyvecl_ntt#118polyveck_ntt#129polyveck_caddq#125polyveck_power2round#133I moved the slow proofs from #151 out, so we can work on them separately.
Update: I used the workaround from #92 to make the four proofs fast using a temporary polynomial. That's a temporary workaround for diffblue/cbmc#8617. I added the functions to #102, so that we can remove the workaround later.