CBMC: Add proof and contract for crypto_sign_keypair_internal #269
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
|
Work in progress |
jakemas
commented
May 22, 2025
Comment on lines
+32
to
33
| shake256(seedbuf, 2 * MLDSA_SEEDBYTES + MLDSA_CRHBYTES, inbuf, | ||
| MLDSA_SEEDBYTES + 2); |
There was a problem hiding this comment.
CBMC disliked the shared use of seedbuf as both in and out here.
jakemas
force-pushed
the
crypto_sign_keypair_internal
branch
from
8ffcfca to
ae1870d
Compare
mkannwischer
force-pushed
the
crypto_sign_keypair_internal
branch
from
ae1870d to
8c4946f
Compare
jakemas
force-pushed
the
crypto_sign_keypair_internal
branch
from
8c4946f to
f6b4738
Compare
Comment on lines
+23
to
+29
| USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256 $(MLD_NAMESPACE)polyvec_matrix_expand \ | ||
| $(MLD_NAMESPACE)poly_uniform_eta_4x $(MLD_NAMESPACE)polyvecl_ntt \ | ||
| $(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery \ | ||
| $(MLD_NAMESPACE)polyveck_reduce $(MLD_NAMESPACE)polyveck_invntt_tomont \ | ||
| $(MLD_NAMESPACE)polyveck_add $(MLD_NAMESPACE)polyveck_caddq \ | ||
| $(MLD_NAMESPACE)polyveck_power2round $(MLD_NAMESPACE)pack_pk \ | ||
| $(MLD_NAMESPACE)pack_sk |
There was a problem hiding this comment.
I find it a bit easier to parse to use
USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_expand
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)poly_uniform_eta_4x
Signed-off-by: Jake Massimo <[email protected]>
mkannwischer
force-pushed
the
crypto_sign_keypair_internal
branch
from
f6b4738 to
0af3d30
Compare
|
is still problematic. I think, you can change the contract of (and change poly_power2round accordingly). There is only one call site so this should be okay. |
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.
crypto_sign_keypair_internal#255Depends on #267 and #280