Skip to content

Conversation

@mkannwischer
Copy link
Contributor

@mkannwischer mkannwischer commented Dec 17, 2025

This commit is the second commit working towards bringing down the memory consumption of signature_internal. It combines the y and h buffer as those lifetime does not overlap.

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

@mkannwischer
Copy link
Contributor Author

CBMC runtime for ML-DSA-87 increases from 11 minutes to 25 minutes :(

@hanno-becker
Copy link
Contributor

@mkannwischer To double-check: Can you try adding a helper function which takes the pointers to the helper structures (incl. y and h) as arguments, and simply asserting that y and h be the same? I wonder if that would lead to a different handling of read/writes than when y and h are visibly (to CBMC) members of a union.

@mkannwischer mkannwischer force-pushed the sign-stack-yh branch 4 times, most recently from 283b8b5 to d725be5 Compare December 24, 2025 13:29
Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
mkannwischer and others added 3 commits December 25, 2025 05:00
This commit is the second commit working towards bringing down the memory
consumption of signature_internal. It combines the y and h buffer as those
lifetime does not overlap.

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@mkannwischer
Copy link
Contributor Author

We merged #818 instead.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants