Skip to content

CBMC: Refine bounds for input and output of base multiplication #906

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

hanno-becker
Copy link
Contributor

@hanno-becker hanno-becker commented Mar 24, 2025

Previously, the base multiplication would assume that one of its inputs is bound by 4096 in absolute value, but make no assumptions about the other input ("b-input" henceforth) and its mulcache.

This commit refines the bounds slightly, as follows:

  • The b-input is assumed to be bound by MLK_NTT_BOUND in absolute value. This comes for free since all values for b are results of the NTT.
  • The b-cache-input is assumed to be bound by MLKEM_Q in absolute value.

With those additional bounds in place, it can be showed that the result of the base multiplication is below INT16_MAX/2 in absolute value. Accordingly, this can be added as a precondition for the inverse NTT.

For the native AVX2 backend, the new output bound for the mulcache forces an explicit zeroization of the mulcache. This is not ideal since the cache is in fact entirely unused, but the performance penalty should be marginal (if the compiler can't eliminate the zeroization in the first place).

@hanno-becker hanno-becker added enhancement New feature or request CBMC labels Mar 24, 2025
@hanno-becker hanno-becker force-pushed the refine_bounds branch 4 times, most recently from 1326e42 to f9b25ee Compare March 24, 2025 11:12
@hanno-becker hanno-becker marked this pull request as ready for review March 24, 2025 12:56
@hanno-becker hanno-becker requested a review from a team as a code owner March 24, 2025 12:56
@hanno-becker hanno-becker added the benchmark this PR should be benchmarked in CI label Mar 24, 2025
Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Mac Mini (M1, 2020) benchmarks

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 12257 cycles 12254 cycles 1.00
ML-KEM-512 encaps 14848 cycles 14846 cycles 1.00
ML-KEM-512 decaps 19725 cycles 19721 cycles 1.00
ML-KEM-768 keypair 21048 cycles 21051 cycles 1.00
ML-KEM-768 encaps 23677 cycles 23679 cycles 1.00
ML-KEM-768 decaps 30515 cycles 30515 cycles 1
ML-KEM-1024 keypair 29977 cycles 29978 cycles 1.00
ML-KEM-1024 encaps 34479 cycles 34478 cycles 1.00
ML-KEM-1024 decaps 43430 cycles 43442 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Intel Xeon 4th gen (c7i)

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 9597 cycles 9477 cycles 1.01
ML-KEM-512 encaps 11103 cycles 11217 cycles 0.99
ML-KEM-512 decaps 15370 cycles 15166 cycles 1.01
ML-KEM-768 keypair 16376 cycles 16303 cycles 1.00
ML-KEM-768 encaps 17765 cycles 17790 cycles 1.00
ML-KEM-768 decaps 23604 cycles 23444 cycles 1.01
ML-KEM-1024 keypair 22063 cycles 22001 cycles 1.00
ML-KEM-1024 encaps 24180 cycles 24012 cycles 1.01
ML-KEM-1024 decaps 31927 cycles 31587 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Intel Xeon 4th gen (c7i) (no-opt)

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 30097 cycles 30164 cycles 1.00
ML-KEM-512 encaps 35523 cycles 35677 cycles 1.00
ML-KEM-512 decaps 44923 cycles 45084 cycles 1.00
ML-KEM-768 keypair 48474 cycles 48448 cycles 1.00
ML-KEM-768 encaps 55666 cycles 55690 cycles 1.00
ML-KEM-768 decaps 68997 cycles 68876 cycles 1.00
ML-KEM-1024 keypair 74954 cycles 74942 cycles 1.00
ML-KEM-1024 encaps 83393 cycles 83410 cycles 1.00
ML-KEM-1024 decaps 99713 cycles 99614 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Arm Cortex-A55 (Snapdragon 888) benchmarks

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 59336 cycles 59330 cycles 1.00
ML-KEM-512 encaps 66928 cycles 66920 cycles 1.00
ML-KEM-512 decaps 86001 cycles 86014 cycles 1.00
ML-KEM-768 keypair 101044 cycles 101087 cycles 1.00
ML-KEM-768 encaps 112086 cycles 112317 cycles 1.00
ML-KEM-768 decaps 139218 cycles 139358 cycles 1.00
ML-KEM-1024 keypair 153559 cycles 153471 cycles 1.00
ML-KEM-1024 encaps 172905 cycles 170285 cycles 1.02
ML-KEM-1024 decaps 210032 cycles 207958 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

AMD EPYC 4th gen (c7a)

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 11636 cycles 11702 cycles 0.99
ML-KEM-512 encaps 13259 cycles 13439 cycles 0.99
ML-KEM-512 decaps 18151 cycles 18310 cycles 0.99
ML-KEM-768 keypair 20132 cycles 20125 cycles 1.00
ML-KEM-768 encaps 21192 cycles 21112 cycles 1.00
ML-KEM-768 decaps 28294 cycles 28224 cycles 1.00
ML-KEM-1024 keypair 27080 cycles 27067 cycles 1.00
ML-KEM-1024 encaps 29207 cycles 29123 cycles 1.00
ML-KEM-1024 decaps 38665 cycles 38639 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

AMD EPYC 3rd gen (c6a)

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 17167 cycles 17264 cycles 0.99
ML-KEM-512 encaps 18926 cycles 19057 cycles 0.99
ML-KEM-512 decaps 24408 cycles 24513 cycles 1.00
ML-KEM-768 keypair 29445 cycles 29552 cycles 1.00
ML-KEM-768 encaps 30852 cycles 30875 cycles 1.00
ML-KEM-768 decaps 38787 cycles 38640 cycles 1.00
ML-KEM-1024 keypair 42726 cycles 42962 cycles 0.99
ML-KEM-1024 encaps 45290 cycles 45604 cycles 0.99
ML-KEM-1024 decaps 55637 cycles 55827 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Intel Xeon 3rd gen (c6i)

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 16123 cycles 16149 cycles 1.00
ML-KEM-512 encaps 18258 cycles 18247 cycles 1.00
ML-KEM-512 decaps 24788 cycles 24723 cycles 1.00
ML-KEM-768 keypair 27724 cycles 27803 cycles 1.00
ML-KEM-768 encaps 29501 cycles 29387 cycles 1.00
ML-KEM-768 decaps 38979 cycles 38836 cycles 1.00
ML-KEM-1024 keypair 37668 cycles 37578 cycles 1.00
ML-KEM-1024 encaps 40643 cycles 40554 cycles 1.00
ML-KEM-1024 decaps 53079 cycles 53168 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Intel Xeon 3rd gen (c6i)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite Current: f9b25ee Previous: 8dba13b Ratio
ML-KEM-768 encaps 30902 cycles 29387 cycles 1.05

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

AMD EPYC 4th gen (c7a) (no-opt)

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 36353 cycles 36358 cycles 1.00
ML-KEM-512 encaps 42971 cycles 42959 cycles 1.00
ML-KEM-512 decaps 55977 cycles 55963 cycles 1.00
ML-KEM-768 keypair 59342 cycles 59249 cycles 1.00
ML-KEM-768 encaps 67754 cycles 67706 cycles 1.00
ML-KEM-768 decaps 84988 cycles 84932 cycles 1.00
ML-KEM-1024 keypair 87597 cycles 87560 cycles 1.00
ML-KEM-1024 encaps 98261 cycles 98317 cycles 1.00
ML-KEM-1024 decaps 120160 cycles 120104 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

AMD EPYC 3rd gen (c6a) (no-opt)

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 39011 cycles 39026 cycles 1.00
ML-KEM-512 encaps 47090 cycles 47097 cycles 1.00
ML-KEM-512 decaps 60662 cycles 60745 cycles 1.00
ML-KEM-768 keypair 63305 cycles 63315 cycles 1.00
ML-KEM-768 encaps 74013 cycles 73946 cycles 1.00
ML-KEM-768 decaps 91862 cycles 91861 cycles 1.00
ML-KEM-1024 keypair 94066 cycles 94031 cycles 1.00
ML-KEM-1024 encaps 107373 cycles 107041 cycles 1.00
ML-KEM-1024 decaps 129368 cycles 129724 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Graviton4

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 17808 cycles 17771 cycles 1.00
ML-KEM-512 encaps 21034 cycles 21026 cycles 1.00
ML-KEM-512 decaps 27670 cycles 27696 cycles 1.00
ML-KEM-768 keypair 30684 cycles 30710 cycles 1.00
ML-KEM-768 encaps 33605 cycles 33580 cycles 1.00
ML-KEM-768 decaps 43197 cycles 43195 cycles 1.00
ML-KEM-1024 keypair 44319 cycles 44315 cycles 1.00
ML-KEM-1024 encaps 49573 cycles 49591 cycles 1.00
ML-KEM-1024 decaps 62550 cycles 62497 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Intel Xeon 3rd gen (c6i) (no-opt)

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 47469 cycles 47466 cycles 1.00
ML-KEM-512 encaps 55355 cycles 55344 cycles 1.00
ML-KEM-512 decaps 71584 cycles 71556 cycles 1.00
ML-KEM-768 keypair 77391 cycles 77538 cycles 1.00
ML-KEM-768 encaps 87479 cycles 87559 cycles 1.00
ML-KEM-768 decaps 108019 cycles 108276 cycles 1.00
ML-KEM-1024 keypair 113202 cycles 113314 cycles 1.00
ML-KEM-1024 encaps 126336 cycles 126306 cycles 1.00
ML-KEM-1024 decaps 152907 cycles 152929 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Graviton4 (no-opt)

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 35922 cycles 35918 cycles 1.00
ML-KEM-512 encaps 40862 cycles 40842 cycles 1.00
ML-KEM-512 decaps 52270 cycles 52306 cycles 1.00
ML-KEM-768 keypair 60047 cycles 60759 cycles 0.99
ML-KEM-768 encaps 66957 cycles 67536 cycles 0.99
ML-KEM-768 decaps 81391 cycles 81425 cycles 1.00
ML-KEM-1024 keypair 89042 cycles 89028 cycles 1.00
ML-KEM-1024 encaps 98838 cycles 98877 cycles 1.00
ML-KEM-1024 decaps 117682 cycles 117716 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Graviton3

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 18864 cycles 18877 cycles 1.00
ML-KEM-512 encaps 22344 cycles 22358 cycles 1.00
ML-KEM-512 decaps 29577 cycles 29566 cycles 1.00
ML-KEM-768 keypair 32236 cycles 32250 cycles 1.00
ML-KEM-768 encaps 35628 cycles 35598 cycles 1.00
ML-KEM-768 decaps 45941 cycles 45965 cycles 1.00
ML-KEM-1024 keypair 46491 cycles 46487 cycles 1.00
ML-KEM-1024 encaps 52069 cycles 52080 cycles 1.00
ML-KEM-1024 decaps 65916 cycles 65962 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Graviton2

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 29410 cycles 29444 cycles 1.00
ML-KEM-512 encaps 34613 cycles 34680 cycles 1.00
ML-KEM-512 decaps 45213 cycles 45279 cycles 1.00
ML-KEM-768 keypair 50051 cycles 50139 cycles 1.00
ML-KEM-768 encaps 55328 cycles 55224 cycles 1.00
ML-KEM-768 decaps 70158 cycles 70096 cycles 1.00
ML-KEM-1024 keypair 73082 cycles 73098 cycles 1.00
ML-KEM-1024 encaps 81472 cycles 81514 cycles 1.00
ML-KEM-1024 decaps 101379 cycles 101471 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Graviton3 (no-opt)

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 38966 cycles 39685 cycles 0.98
ML-KEM-512 encaps 44939 cycles 44864 cycles 1.00
ML-KEM-512 decaps 56734 cycles 56842 cycles 1.00
ML-KEM-768 keypair 64234 cycles 64182 cycles 1.00
ML-KEM-768 encaps 72031 cycles 72669 cycles 0.99
ML-KEM-768 decaps 88070 cycles 88056 cycles 1.00
ML-KEM-1024 keypair 96228 cycles 96095 cycles 1.00
ML-KEM-1024 encaps 106307 cycles 106211 cycles 1.00
ML-KEM-1024 decaps 127120 cycles 127057 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

SpacemiT K1 8 (Banana Pi F3) benchmarks

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 225601 cycles 225593 cycles 1.00
ML-KEM-512 encaps 271839 cycles 271821 cycles 1.00
ML-KEM-512 decaps 346406 cycles 346326 cycles 1.00
ML-KEM-768 keypair 374348 cycles 374216 cycles 1.00
ML-KEM-768 encaps 433877 cycles 433736 cycles 1.00
ML-KEM-768 decaps 532770 cycles 532650 cycles 1.00
ML-KEM-1024 keypair 554398 cycles 554463 cycles 1.00
ML-KEM-1024 encaps 632515 cycles 632521 cycles 1.00
ML-KEM-1024 decaps 754467 cycles 754358 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Arm Cortex-A72 (Raspberry Pi 4) benchmarks

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 52821 cycles 53196 cycles 0.99
ML-KEM-512 encaps 60537 cycles 61239 cycles 0.99
ML-KEM-512 decaps 77877 cycles 77578 cycles 1.00
ML-KEM-768 keypair 89670 cycles 89929 cycles 1.00
ML-KEM-768 encaps 97185 cycles 98860 cycles 0.98
ML-KEM-768 decaps 121486 cycles 123436 cycles 0.98
ML-KEM-1024 keypair 135647 cycles 134458 cycles 1.01
ML-KEM-1024 encaps 148998 cycles 147089 cycles 1.01
ML-KEM-1024 decaps 180865 cycles 180649 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Graviton2 (no-opt)

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 59326 cycles 59431 cycles 1.00
ML-KEM-512 encaps 68033 cycles 68011 cycles 1.00
ML-KEM-512 decaps 86704 cycles 86649 cycles 1.00
ML-KEM-768 keypair 98815 cycles 98924 cycles 1.00
ML-KEM-768 encaps 110974 cycles 110402 cycles 1.01
ML-KEM-768 decaps 134574 cycles 134811 cycles 1.00
ML-KEM-1024 keypair 148680 cycles 148822 cycles 1.00
ML-KEM-1024 encaps 163724 cycles 163875 cycles 1.00
ML-KEM-1024 decaps 195449 cycles 195498 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Copy link

@oqs-bot oqs-bot left a comment

Choose a reason for hiding this comment

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

Arm Cortex-A76 (Raspberry Pi 5) benchmarks

Benchmark suite Current: ee52c4e Previous: 8dba13b Ratio
ML-KEM-512 keypair 29409 cycles 29440 cycles 1.00
ML-KEM-512 encaps 34618 cycles 34675 cycles 1.00
ML-KEM-512 decaps 45210 cycles 45264 cycles 1.00
ML-KEM-768 keypair 50053 cycles 50138 cycles 1.00
ML-KEM-768 encaps 55322 cycles 55220 cycles 1.00
ML-KEM-768 decaps 70154 cycles 70075 cycles 1.00
ML-KEM-1024 keypair 73076 cycles 73079 cycles 1.00
ML-KEM-1024 encaps 81445 cycles 81517 cycles 1.00
ML-KEM-1024 decaps 101376 cycles 101473 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@hanno-becker hanno-becker removed the benchmark this PR should be benchmarked in CI label Mar 24, 2025
@hanno-becker hanno-becker added the benchmark this PR should be benchmarked in CI label Mar 24, 2025
@hanno-becker hanno-becker added benchmark this PR should be benchmarked in CI and removed benchmark this PR should be benchmarked in CI labels Mar 25, 2025
@rod-chapman rod-chapman self-requested a review March 25, 2025 10:44
Copy link
Contributor

@mkannwischer mkannwischer left a comment

Choose a reason for hiding this comment

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

LGTM.

Copy link
Contributor

@mkannwischer mkannwischer left a comment

Choose a reason for hiding this comment

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

Something must have broke when rebasing - CBMC is not happy and it looks to me like it's correct.

@rod-chapman
Copy link
Contributor

Looks good to me.

rod-chapman
rod-chapman previously approved these changes Mar 25, 2025
Copy link
Contributor

@rod-chapman rod-chapman left a comment

Choose a reason for hiding this comment

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

Looks good to me. All proofs OK.

@hanno-becker
Copy link
Contributor Author

The combination of this and #895 seems to have a bad effect on CBMC performance. It's too slow to be merged at present.

@hanno-becker hanno-becker force-pushed the refine_bounds branch 5 times, most recently from b6cd5ee to 053d0e2 Compare March 27, 2025 20:00
@hanno-becker hanno-becker dismissed rod-chapman’s stale review April 4, 2025 13:50

PR is too slow to be merged in this form

Previously, the base multiplication would assume that one of its inputs
is bound by 4096 in absolute value, but make no assumptions about the
other input ("b-input" henceforth) and its mulcache.

This commit refines the bounds slightly, as follows:
- The b-input is assumed to be bound by MLK_NTT_BOUND in absolute value.
  This comes for free since all values for b _are_ results of the NTT.
- The b-cache-input is assumed to be bound by MLKEM_Q in absolute value.

With those additional bounds in place, it can be showed that the result
of the base multiplication is below INT16_MAX/2 in absolute value.
Accordingly, this can be added as a precondition for the inverse NTT.

Those refined bounds can help in subsequent commits to improve the
reduction strategy inside the inverse NTT.

For the native AVX2 backend, the new output bound for the mulcache
forces an explicit zeroization of the mulcache. This is not ideal
since the cache is in fact entirely unused, but the performance
penalty should be marginal (if the compiler can't eliminate the
zeroization in the first place).

Signed-off-by: Hanno Becker <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
benchmark this PR should be benchmarked in CI CBMC enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants