Skip to content

Conversation

@mkannwischer
Copy link
Contributor

No description provided.

hanno-becker and others added 12 commits December 17, 2025 16:42
- Add mld_polymat_get_row() to retrieve matrix row pointer
- Update mld_polyvec_matrix_pointwise_montgomery() to use helper

Addresses #738 (steps 2-3 of #736)

Signed-off-by: Hanno Becker <[email protected]>
crypto_sign_verify_internal stack:

before: 26928/37232/49776
after: 22784/31040/41536

Signed-off-by: Matthias J. Kannwischer <[email protected]>
crypto_sign_verify_internal stack: 21743/30016/40515

Signed-off-by: Matthias J. Kannwischer <[email protected]>
crypto_sign_verify_internal stack: 17664/24864/33312

Signed-off-by: Matthias J. Kannwischer <[email protected]>
crypto_sign_verify_internal stack: 14592/19744/26144

Signed-off-by: Matthias J. Kannwischer <[email protected]>
crypto_sign_verify_internal stack: 13568/18720/25120

Signed-off-by: Matthias J. Kannwischer <[email protected]>
71168 -> 64000

Signed-off-by: Matthias J. Kannwischer <[email protected]>
64000 -> 55808

Signed-off-by: Matthias J. Kannwischer <[email protected]>
55808 -> 40448

Signed-off-by: Matthias J. Kannwischer <[email protected]>
40448 -> 34304

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 30, 2025
Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 30, 2025
Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 30, 2025
Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 30, 2025
Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 30, 2025
Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 30, 2025
Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 31, 2025
Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 31, 2025
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 31, 2025
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 31, 2025
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
The computation of z is moved into a separate function (compute_pack_z) to
vastly speed up the CBMC proofs.

De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 31, 2025
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 31, 2025
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Dec 31, 2025
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
The computation of z is moved into a separate function (compute_pack_z) to
vastly speed up the CBMC proofs.

De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Jan 3, 2026
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Jan 3, 2026
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
The computation of z is moved into a separate function (compute_pack_z) to
vastly speed up the CBMC proofs.

De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Jan 3, 2026
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
The computation of z is moved into a separate function (compute_pack_z) to
vastly speed up the CBMC proofs.

De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Jan 3, 2026
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Jan 3, 2026
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
The computation of z is moved into a separate function (compute_pack_z) to
vastly speed up the CBMC proofs.

De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Jan 3, 2026
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Jan 5, 2026
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
The computation of z is moved into a separate function (compute_pack_z) to
vastly speed up the CBMC proofs.

De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Jan 5, 2026
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Jan 7, 2026
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
The computation of z is moved into a separate function (compute_pack_z) to
vastly speed up the CBMC proofs.

De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
hanno-becker pushed a commit that referenced this pull request Jan 8, 2026
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
The computation of z is moved into a separate function (compute_pack_z) to
vastly speed up the CBMC proofs.

De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Jan 8, 2026
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
The computation of z is moved into a separate function (compute_pack_z) to
vastly speed up the CBMC proofs.

De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this pull request Jan 8, 2026
This commit reduces the stack usage of signing by computing z = y + s1*cp
incrementally (one polynomial at a time) allowing to eliminate the polyvecl
z (at to cost of a single poly z).
The computation of z is moved into a separate function (compute_pack_z) to
vastly speed up the CBMC proofs.

De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM.

Practically, the same buffer was used early in the function too. Here we
instead introduce a new polyvecl buffer tmp, but that can be placed in a union
together with w1.
Unfortuantely, with the current struct workaround for
diffblue/cbmc#8813, this results in an increase in
stack space by L KB.
This gets eliminated when MLD_CONFIG_REDUCE_RAM is set.

Hoisted out from #791

Signed-off-by: Matthias J. Kannwischer <[email protected]>
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