Skip to content

sign mem: reuse w/w0 buffer#792

Closed
mkannwischer wants to merge 1 commit intomainfrom
sign-stack-1
Closed

sign mem: reuse w/w0 buffer#792
mkannwischer wants to merge 1 commit intomainfrom
sign-stack-1

Conversation

@mkannwischer
Copy link
Contributor

@mkannwischer mkannwischer commented Dec 15, 2025 •
edited
Loading

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.

-fstack-usage of signature_internal of ML-DSA-86 reduces from 129616 to 121536 (aarch64, -Os, gcc14).

@mkannwischer
sign mem: reuse w/w0 buffer
87c2bcf 
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>
@mkannwischer mkannwischer marked this pull request as ready for review December 15, 2025 02:46
@mkannwischer mkannwischer requested a review from a team as a code owner December 15, 2025 02:46
@jakemas
Copy link
Contributor

jakemas commented Dec 15, 2025

Looks good to me! Confirmed CBMC passes locally with these changes.

hanno-becker
hanno-becker reviewed Dec 16, 2025
View reviewed changes
mldsa/src/polyvec.h
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)))
Copy link
Contributor

@hanno-becker hanno-becker Dec 16, 2025

Choose a reason for hiding this comment

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

Is it worth keeping the non-aliased version, or can we rewrite the code so it uses the aliased version everywhere?

hanno-becker
hanno-becker reviewed Dec 16, 2025
View reviewed changes
Copy link
Contributor

@hanno-becker hanno-becker left a comment

Choose a reason for hiding this comment

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

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.

@hanno-becker
Copy link
Contributor

hanno-becker commented Dec 16, 2025

The culprit is mld_attempt_signature_generation, which now takes 1041s in CI for ML-DSA-87.

hanno-becker
hanno-becker requested changes Dec 16, 2025
View reviewed changes
Copy link
Contributor

@hanno-becker hanno-becker left a comment

Choose a reason for hiding this comment

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

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
@mkannwischer
decompose: Remove separate input argument
29137ad 
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
@mkannwischer
decompose: Remove separate input argument
4527809 
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 mkannwischer mentioned this pull request Dec 17, 2025
Merged
@mkannwischer mkannwischer marked this pull request as draft December 17, 2025 01:04
@mkannwischer
Copy link
Contributor Author

mkannwischer commented Dec 17, 2025

I've rewritten polyveck_decompose to a 2-argument function in #798.
That achieves the same stack reduction and leads to simpler CBMC contracts and proofs.

mkannwischer added a commit that referenced this pull request Dec 17, 2025
@mkannwischer
decompose: Remove separate input argument
5b19c6d 
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
@mkannwischer
decompose: Remove separate input argument
6ae80c8 
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
@mkannwischer
decompose: Remove separate input argument
bbf00d0 
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
@mkannwischer @hanno-becker
decompose: Remove separate input argument
86496ce 
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

Reviewers

@hanno-becker hanno-becker hanno-becker requested changes

@jakemas jakemas jakemas 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.

3 participants

@mkannwischer @jakemas @hanno-becker