sign mem: reuse w/w0 buffer #792
Closed
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
This is the first of a series of commit bringing down the memory consumption of signature_internal. Memory consumption is reduced by placing buffers whose lifetime does not overlap into a union starting with thw w and w0 buffer. CBMC contracts and proofs are adjusted where necessary. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Contributor
|
Looks good to me! Confirmed CBMC passes locally with these changes. |
jakemas
approved these changes
Dec 15, 2025
| requires(memory_no_alias(v1, sizeof(mld_polyveck))) | ||
| requires(memory_no_alias(v0, sizeof(mld_polyveck))) | ||
| requires(memory_no_alias(v, sizeof(mld_polyveck))) | ||
| requires(v0 == v || memory_no_alias(v, sizeof(mld_polyveck))) |
Contributor
There was a problem hiding this comment.
Is it worth keeping the non-aliased version, or can we rewrite the code so it uses the aliased version everywhere?
Contributor
hanno-becker
left a comment
hanno-becker
left a comment
There was a problem hiding this comment.
It looks like the CBMC runtime got quite a lot worse, from 7/7/11 to 11/15/21.
We can of course just hope for the best and merge this, but seeing that this is only the very beginning of a series of changes, I am wary that it's not going to work for long.
Contributor
|
The culprit is |
hanno-becker
requested changes
Dec 16, 2025
Contributor
hanno-becker
left a comment
hanno-becker
left a comment
There was a problem hiding this comment.
Rather than ignoring the CBMC slowdown, I'd prefer if we could spend more time in this toy-example to understand what, if anything, we can do to keep the CBMC runtime largely where it was.
@tautschnig told me that if we never use unions for data-presentation changes and set --slice-formula, it should not matter (Michael, chime in if I mispresent anything), but this example does not seem to confirm it:
CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3
CBMCFLAGS += --slice-formula
CBMCFLAGS += --no-array-field-sensitivity
mkannwischer
added a commit
that referenced
this pull request
Dec 17, 2025
To reduce stack usage, polyveck_decompose should be able to operate on one of the outputs aliasing the input. This is already fully supported but wasn't used to ease CBMC proofs/contracts at a cost of requiring additional stack space which is undesirable. This commit is an alternative to #792 which extended the CBMC contracts to allow aliasing. This commit instead, changes the signature of the decompose functions to take 2 arguments instead of 3, where the second output also acts as and input. The corresponding poly_ and native functions are adjusted accordingly. CBMC contracts/proofs and unit tests are adjusted to the new signature. The single callsite of polyveck_decompose is adjusted. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
mkannwischer
added a commit
that referenced
this pull request
Dec 17, 2025
To reduce stack usage, polyveck_decompose should be able to operate on one of the outputs aliasing the input. This is already fully supported but wasn't used to ease CBMC proofs/contracts at a cost of requiring additional stack space which is undesirable. This commit is an alternative to #792 which extended the CBMC contracts to allow aliasing. This commit instead, changes the signature of the decompose functions to take 2 arguments instead of 3, where the second output also acts as and input. The corresponding poly_ and native functions are adjusted accordingly. CBMC contracts/proofs and unit tests are adjusted to the new signature. The single callsite of polyveck_decompose is adjusted. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Contributor
Author
|
I've rewritten |
mkannwischer
added a commit
that referenced
this pull request
Dec 17, 2025
To reduce stack usage, polyveck_decompose should be able to operate on one of the outputs aliasing the input. This is already fully supported but wasn't used to ease CBMC proofs/contracts at a cost of requiring additional stack space which is undesirable. This commit is an alternative to #792 which extended the CBMC contracts to allow aliasing. This commit instead, changes the signature of the decompose functions to take 2 arguments instead of 3, where the second output also acts as and input. The corresponding poly_ and native functions are adjusted accordingly. CBMC contracts/proofs and unit tests are adjusted to the new signature. The single callsite of polyveck_decompose is adjusted. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
mkannwischer
added a commit
that referenced
this pull request
Dec 17, 2025
To reduce stack usage, polyveck_decompose should be able to operate on one of the outputs aliasing the input. This is already fully supported but wasn't used to ease CBMC proofs/contracts at a cost of requiring additional stack space which is undesirable. This commit is an alternative to #792 which extended the CBMC contracts to allow aliasing. This commit instead, changes the signature of the decompose functions to take 2 arguments instead of 3, where the second output also acts as and input. The corresponding poly_ and native functions are adjusted accordingly. CBMC contracts/proofs and unit tests are adjusted to the new signature. The single callsite of polyveck_decompose is adjusted. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
mkannwischer
added a commit
that referenced
this pull request
Dec 17, 2025
To reduce stack usage, polyveck_decompose should be able to operate on one of the outputs aliasing the input. This is already fully supported but wasn't used to ease CBMC proofs/contracts at a cost of requiring additional stack space which is undesirable. This commit is an alternative to #792 which extended the CBMC contracts to allow aliasing. This commit instead, changes the signature of the decompose functions to take 2 arguments instead of 3, where the second output also acts as and input. The corresponding poly_ and native functions are adjusted accordingly. CBMC contracts/proofs and unit tests are adjusted to the new signature. The single callsite of polyveck_decompose is adjusted. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
hanno-becker
pushed a commit
that referenced
this pull request
Dec 17, 2025
To reduce stack usage, polyveck_decompose should be able to operate on one of the outputs aliasing the input. This is already fully supported but wasn't used to ease CBMC proofs/contracts at a cost of requiring additional stack space which is undesirable. This commit is an alternative to #792 which extended the CBMC contracts to allow aliasing. This commit instead, changes the signature of the decompose functions to take 2 arguments instead of 3, where the second output also acts as and input. The corresponding poly_ and native functions are adjusted accordingly. CBMC contracts/proofs and unit tests are adjusted to the new signature. The single callsite of polyveck_decompose is adjusted. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
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.
This is the first of a series of commit bringing down the memory consumption of signature_internal.
Memory consumption is reduced by placing buffers whose lifetime does not overlap into a union starting with thw w and w0 buffer. CBMC contracts and proofs are adjusted where necessary.
crypto_sign_signature_internalstack usage #791-fstack-usageofsignature_internalof ML-DSA-86 reduces from 129616 to 121536 (aarch64, -Os, gcc14).