CBMC: Refine bounds for input and output of base multiplication by hanno-becker · Pull Request #906 · pq-code-package/mlkem-native

hanno-becker · 2025-03-24T04:42:14Z

Builds on: Switch mlk_polyvec and mlk_polymat to struct wrappers #1115

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).

oqs-bot

Mac Mini (M1, 2020) benchmarks

Details

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.

oqs-bot

Intel Xeon 4th gen (c7i)

Details

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.

oqs-bot

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

Details

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.

oqs-bot

Arm Cortex-A55 (Snapdragon 888) benchmarks

Details

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.

oqs-bot

AMD EPYC 4th gen (c7a)

Details

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.

oqs-bot

AMD EPYC 3rd gen (c6a)

Details

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.

oqs-bot

Intel Xeon 3rd gen (c6i)

Details

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.

oqs-bot

⚠️ 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.

oqs-bot

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

Details

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.

oqs-bot

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

Details

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.

oqs-bot

Graviton4

Details

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.

oqs-bot

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

Details

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.

oqs-bot

Graviton4 (no-opt)

Details

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.

oqs-bot

Graviton3

Details

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.

oqs-bot

Graviton2

Details

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.

oqs-bot

Graviton3 (no-opt)

Details

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.

oqs-bot

SpacemiT K1 8 (Banana Pi F3) benchmarks

Details

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.

oqs-bot

Arm Cortex-A72 (Raspberry Pi 4) benchmarks

Details

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.

oqs-bot

Graviton2 (no-opt)

Details

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.

oqs-bot

Arm Cortex-A76 (Raspberry Pi 5) benchmarks

Details

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 · 2026-01-01T05:39:40Z

@dkostic Now that you have done all the proofs including the basemul. How much work would you expect it to be to adjust the basemul to use a (slightly) lazy reduction strategy? That is, only reduce after computing each polynomial product, but before accumulation.

hanno-becker · 2026-05-03T07:00:30Z

@dkostic Would you (and Claude) have time to do this, and at the same time resolve #1421?

rod-chapman · 2026-05-04T10:20:27Z

I hope that CBMC 6.9.0 will unblock progress on this one. I will rebase the branch first and see if the proofs complete OK.

hanno-becker · 2026-05-04T10:46:37Z

Thanks @rod-chapman! But this also needs significant work on the x86_64 backend.

rod-chapman · 2026-05-04T11:12:07Z

Oh yes... the x86 back-end has to brought into line with the AArch64 and C back-ends to produce tighter bounds on the output of basemul, right?

I have re-based and re-running proofs now on the C stuff.

oqs-bot · 2026-05-04T11:13:06Z

CBMC Results (ML-KEM-512)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2003s	1531s	+30.8%
`mlk_indcpa_dec`	⚠️	25s	13s	+92%
`mlk_indcpa_keypair_derand`	⚠️	439s	213s	+106%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	⚠️	180s	51s	+253%
`polyvec_basemul_acc_montgomery_cached_native`	⚠️	84s	8s	+950%
`rej_uniform_native_aarch64`	⚠️	53s	33s	+61%

Full Results (191 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2003s	1531s	+30.8%
`mlk_indcpa_keypair_derand`	⚠️	439s	213s	+106%
`mlk_indcpa_enc`	✅	255s	255s	+0%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	⚠️	180s	51s	+253%
`mlk_poly_rej_uniform`	✅	136s	135s	+1%
`mlk_rej_uniform_c`	✅	103s	112s	-8%
`polyvec_basemul_acc_montgomery_cached_native`	⚠️	84s	8s	+950%
`rej_uniform_native_x86_64`	✅	54s	55s	-2%
`rej_uniform_native_aarch64`	⚠️	53s	33s	+61%
`poly_ntt_native`	✅	38s	33s	+15%
`mlk_poly_reduce_native`	✅	37s	32s	+16%
`mlk_ntt_layer`	✅	31s	27s	+15%
`mlk_indcpa_dec`	⚠️	25s	13s	+92%
`mlk_keccak_squeezeblocks_x4`	✅	23s	26s	-12%
`keccakf1600x4_permute_native_x4`	✅	17s	17s	+0%
`mlk_poly_decompress_d4_native`	✅	16s	13s	+23%
`mlk_poly_decompress_d10_native`	✅	15s	12s	+25%
`mlk_poly_frommsg`	✅	10s	11s	-9%
`mlk_poly_frombytes_native`	✅	9s	9s	+0%
`mlk_polyvec_add`	✅	9s	11s	-18%
`mlk_keccak_squeeze_once`	✅	8s	8s	+0%
`mlk_keccak_squeezeblocks`	✅	8s	8s	+0%
`mlk_poly_sub`	✅	8s	8s	+0%
`mlk_ntt_butterfly_block`	✅	7s	8s	-12%
`mlk_poly_getnoise_eta1_4x`	✅	7s	2s	+250%
`mlk_matvec_mul`	✅	6s	1s	+500%
`mlk_poly_ntt`	✅	6s	6s	+0%
`mlk_poly_rej_uniform_x4`	✅	6s	5s	+20%
`mlk_check_pct`	✅	5s	1s	+400%
`mlk_invntt_layer`	✅	5s	5s	+0%
`mlk_keccak_absorb_once_x4`	✅	5s	6s	-17%
`mlk_keccakf1600_permute_c`	✅	5s	5s	+0%
`mlk_poly_frombytes_c`	✅	5s	5s	+0%
`mlk_polymat_permute_bitrev_to_custom`	✅	5s	2s	+150%
`mlk_shake256x4`	✅	5s	5s	+0%
`poly_frombytes_native_x86_64`	✅	5s	6s	-17%
`kem_dec`	✅	4s	3s	+33%
`kem_enc`	✅	4s	2s	+100%
`kem_enc_derand`	✅	4s	3s	+33%
`mlk_ct_cmov_zero`	✅	4s	2s	+100%
`mlk_fqmul`	✅	4s	15s	-73%
`mlk_keccak_absorb_once`	✅	4s	3s	+33%
`mlk_keypair_getnoise_eta1`	✅	4s	2s	+100%
`mlk_poly_add`	✅	4s	4s	+0%
`mlk_poly_compress_d10_c`	✅	4s	5s	-20%
`mlk_poly_compress_d4_c`	✅	4s	5s	-20%
`mlk_poly_compress_d5_native`	✅	4s	2s	+100%
`mlk_poly_compress_du`	✅	4s	3s	+33%
`mlk_poly_decompress_d5`	✅	4s	2s	+100%
`mlk_poly_decompress_du`	✅	4s	2s	+100%
`mlk_poly_getnoise_eta1122_4x`	✅	4s	1s	+300%
`mlk_polyvec_mulcache_compute`	✅	4s	2s	+100%
`mlk_polyvec_tomont`	✅	4s	3s	+33%
`mlk_scalar_compress_d1`	✅	4s	4s	+0%
`mlk_scalar_compress_d4`	✅	4s	2s	+100%
`mlk_value_barrier_u8`	✅	4s	2s	+100%
`poly_decompress_d10_native_x86_64`	✅	4s	3s	+33%
`poly_decompress_d4_native_x86_64`	✅	4s	5s	-20%
`poly_invntt_tomont_native`	✅	4s	1s	+300%
`poly_mulcache_compute_native_aarch64`	✅	4s	2s	+100%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	4s	4s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	3s	2s	+50%
`kem_check_pk`	✅	3s	2s	+50%
`kem_keypair_derand`	✅	3s	5s	-40%
`mlk_ct_cmask_neg_i16`	✅	3s	1s	+200%
`mlk_ct_cmask_nonzero_u8`	✅	3s	5s	-40%
`mlk_keccakf1600_extract_bytes`	✅	3s	2s	+50%
`mlk_keccakf1600_permute`	✅	3s	1s	+200%
`mlk_keccakf1600_xor_bytes`	✅	3s	2s	+50%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	3s	3s	+0%
`mlk_keccakf1600x4_extract_bytes_c`	✅	3s	1s	+200%
`mlk_keccakf1600x4_permute`	✅	3s	1s	+200%
`mlk_montgomery_reduce`	✅	3s	1s	+200%
`mlk_poly_cbd_eta1`	✅	3s	2s	+50%
`mlk_poly_compress_d11_c`	✅	3s	2s	+50%
`mlk_poly_compress_d11_native`	✅	3s	2s	+50%
`mlk_poly_compress_d4_native`	✅	3s	5s	-40%
`mlk_poly_decompress_d10_c`	✅	3s	2s	+50%
`mlk_poly_decompress_d11_c`	✅	3s	1s	+200%
`mlk_poly_decompress_d4`	✅	3s	2s	+50%
`mlk_poly_frombytes`	✅	3s	2s	+50%
`mlk_poly_mulcache_compute`	✅	3s	2s	+50%
`mlk_poly_tomont`	✅	3s	2s	+50%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	3s	2s	+50%
`mlk_polyvec_permute_bitrev_to_custom`	✅	3s	1s	+200%
`mlk_scalar_decompress_d10`	✅	3s	3s	+0%
`mlk_sha3_512`	✅	3s	1s	+200%
`mlk_shake128_squeezeblocks`	✅	3s	2s	+50%
`mlk_shake128x4_squeezeblocks`	✅	3s	4s	-25%
`mlk_value_barrier_u32`	✅	3s	2s	+50%
`ntt_native_x86_64`	✅	3s	1s	+200%
`nttunpack_native_x86_64`	✅	3s	3s	+0%
`poly_compress_d11_native_x86_64`	✅	3s	3s	+0%
`poly_compress_d4_native_x86_64`	✅	3s	2s	+50%
`poly_decompress_d11_native_x86_64`	✅	3s	3s	+0%
`poly_reduce_native_x86_64`	✅	3s	4s	-25%
`poly_tomont_native_x86_64`	✅	3s	3s	+0%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	✅	3s	3s	+0%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	✅	3s	2s	+50%
`intt_native_aarch64`	✅	2s	3s	-33%
`intt_native_x86_64`	✅	2s	4s	-50%
`keccak_f1600_x1_native_aarch64`	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	✅	2s	1s	+100%
`keccakf1600_permute_native`	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes_native`	✅	2s	3s	-33%
`keccakf1600x4_xor_bytes_native`	✅	2s	2s	+0%
`kem_keypair`	✅	2s	3s	-33%
`mlk_barrett_reduce`	✅	2s	3s	-33%
`mlk_ct_cmask_nonzero_u16`	✅	2s	4s	-50%
`mlk_ct_get_optblocker_u32`	✅	2s	1s	+100%
`mlk_ct_get_optblocker_u8`	✅	2s	2s	+0%
`mlk_ct_sel_int16`	✅	2s	1s	+100%
`mlk_ct_sel_uint8`	✅	2s	2s	+0%
`mlk_enc_getnoise_eta1_eta2`	✅	2s	2s	+0%
`mlk_gen_matrix`	✅	2s	3s	-33%
`mlk_gen_matrix_serial`	✅	2s	2s	+0%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	2s	1s	+100%
`mlk_keccakf1600x4_extract_bytes`	✅	2s	3s	-33%
`mlk_keccakf1600x4_xor_bytes`	✅	2s	1s	+100%
`mlk_poly_cbd_eta2`	✅	2s	2s	+0%
`mlk_poly_compress_d10`	✅	2s	5s	-60%
`mlk_poly_compress_d4`	✅	2s	2s	+0%
`mlk_poly_compress_d5`	✅	2s	1s	+100%
`mlk_poly_compress_dv`	✅	2s	1s	+100%
`mlk_poly_decompress_d11`	✅	2s	2s	+0%
`mlk_poly_decompress_d4_c`	✅	2s	4s	-50%
`mlk_poly_decompress_d5_c`	✅	2s	1s	+100%
`mlk_poly_decompress_dv`	✅	2s	4s	-50%
`mlk_poly_getnoise_eta2`	✅	2s	3s	-33%
`mlk_poly_invntt_tomont`	✅	2s	2s	+0%
`mlk_poly_invntt_tomont_c`	✅	2s	3s	-33%
`mlk_poly_mulcache_compute_c`	✅	2s	3s	-33%
`mlk_poly_reduce`	✅	2s	2s	+0%
`mlk_poly_tobytes`	✅	2s	3s	-33%
`mlk_poly_tobytes_c`	✅	2s	2s	+0%
`mlk_poly_tobytes_native`	✅	2s	3s	-33%
`mlk_poly_tomont_c`	✅	2s	3s	-33%
`mlk_poly_tomont_native`	✅	2s	3s	-33%
`mlk_polyvec_compress_du`	✅	2s	3s	-33%
`mlk_polyvec_frombytes`	✅	2s	2s	+0%
`mlk_polyvec_invntt_tomont`	✅	2s	4s	-50%
`mlk_rej_uniform`	✅	2s	1s	+100%
`mlk_scalar_compress_d10`	✅	2s	2s	+0%
`mlk_scalar_compress_d11`	✅	2s	1s	+100%
`mlk_scalar_compress_d5`	✅	2s	4s	-50%
`mlk_scalar_decompress_d4`	✅	2s	4s	-50%
`mlk_scalar_decompress_d5`	✅	2s	4s	-50%
`mlk_scalar_signed_to_unsigned_q`	✅	2s	4s	-50%
`mlk_sha3_256`	✅	2s	2s	+0%
`mlk_shake128_absorb_once`	✅	2s	3s	-33%
`mlk_shake128x4_absorb_once`	✅	2s	3s	-33%
`mlk_value_barrier_i32`	✅	2s	1s	+100%
`ntt_native_aarch64`	✅	2s	1s	+100%
`poly_compress_d10_native_x86_64`	✅	2s	5s	-60%
`poly_decompress_d5_native_x86_64`	✅	2s	2s	+0%
`poly_mulcache_compute_native_x86_64`	✅	2s	2s	+0%
`poly_reduce_native_aarch64`	✅	2s	2s	+0%
`poly_tobytes_native_aarch64`	✅	2s	2s	+0%
`poly_tomont_native_aarch64`	✅	2s	1s	+100%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	2s	2s	+0%
`rej_uniform_native`	✅	2s	2s	+0%
`sys_check_capability`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	2s	-50%
`kem_check_sk`	✅	1s	2s	-50%
`mlk_ct_get_optblocker_i32`	✅	1s	2s	-50%
`mlk_ct_memcmp`	✅	1s	1s	+0%
`mlk_keccakf1600x4_xor_bytes_c`	✅	1s	2s	-50%
`mlk_poly_compress_d10_native`	✅	1s	2s	-50%
`mlk_poly_compress_d11`	✅	1s	1s	+0%
`mlk_poly_compress_d5_c`	✅	1s	3s	-67%
`mlk_poly_decompress_d10`	✅	1s	5s	-80%
`mlk_poly_decompress_d11_native`	✅	1s	2s	-50%
`mlk_poly_decompress_d5_native`	✅	1s	2s	-50%
`mlk_poly_getnoise_eta1_4x_native`	✅	1s	4s	-75%
`mlk_poly_mulcache_compute_native`	✅	1s	2s	-50%
`mlk_poly_ntt_c`	✅	1s	2s	-50%
`mlk_poly_reduce_c`	✅	1s	1s	+0%
`mlk_poly_tomsg`	✅	1s	2s	-50%
`mlk_polyvec_decompress_du`	✅	1s	2s	-50%
`mlk_polyvec_ntt`	✅	1s	1s	+0%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	1s	1s	+0%
`mlk_polyvec_reduce`	✅	1s	1s	+0%
`mlk_polyvec_tobytes`	✅	1s	3s	-67%
`mlk_scalar_decompress_d11`	✅	1s	4s	-75%
`mlk_shake256`	✅	1s	2s	-50%
`poly_compress_d5_native_x86_64`	✅	1s	2s	-50%
`poly_getnoise_eta1122_4x_native`	✅	1s	2s	-50%
`poly_tobytes_native_x86_64`	✅	1s	2s	-50%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	1s	2s	-50%

oqs-bot · 2026-05-04T11:35:41Z

CBMC Results (ML-KEM-768)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`mlk_polyvec_basemul_acc_montgomery_cached_c`	⚠️	113s	47s	+140%
`polyvec_basemul_acc_montgomery_cached_native`	⚠️	144s	14s	+929%

Full Results (191 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1692s	1640s	+3.2%
`mlk_indcpa_enc`	✅	291s	249s	+17%
`polyvec_basemul_acc_montgomery_cached_native`	⚠️	144s	14s	+929%
`mlk_poly_rej_uniform`	✅	140s	127s	+10%
`mlk_indcpa_keypair_derand`	✅	129s	302s	-57%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	⚠️	113s	47s	+140%
`mlk_rej_uniform_c`	✅	95s	113s	-16%
`rej_uniform_native_x86_64`	✅	58s	53s	+9%
`rej_uniform_native_aarch64`	✅	52s	35s	+49%
`poly_ntt_native`	✅	39s	38s	+3%
`mlk_poly_reduce_native`	✅	35s	34s	+3%
`mlk_ntt_layer`	✅	30s	29s	+3%
`mlk_keccak_squeezeblocks_x4`	✅	24s	24s	+0%
`keccakf1600x4_permute_native_x4`	✅	16s	18s	-11%
`mlk_poly_decompress_d4_native`	✅	14s	12s	+17%
`mlk_indcpa_dec`	✅	13s	11s	+18%
`mlk_poly_decompress_d10_native`	✅	12s	12s	+0%
`mlk_polyvec_add`	✅	12s	10s	+20%
`mlk_poly_frommsg`	✅	11s	9s	+22%
`mlk_keccak_absorb_once_x4`	✅	8s	7s	+14%
`mlk_keccak_squeezeblocks`	✅	8s	8s	+0%
`mlk_ntt_butterfly_block`	✅	8s	6s	+33%
`mlk_poly_frombytes_native`	✅	8s	7s	+14%
`mlk_poly_sub`	✅	8s	6s	+33%
`mlk_poly_ntt`	✅	7s	7s	+0%
`kem_dec`	✅	6s	5s	+20%
`mlk_fqmul`	✅	6s	17s	-65%
`mlk_keccak_squeeze_once`	✅	6s	7s	-14%
`mlk_keccakf1600_permute_c`	✅	6s	5s	+20%
`mlk_keypair_getnoise_eta1`	✅	6s	2s	+200%
`keccak_f1600_x4_native_aarch64_v84a`	✅	5s	2s	+150%
`mlk_barrett_reduce`	✅	5s	1s	+400%
`mlk_poly_add`	✅	5s	4s	+25%
`mlk_poly_getnoise_eta1122_4x`	✅	5s	1s	+400%
`mlk_poly_rej_uniform_x4`	✅	5s	6s	-17%
`poly_decompress_d4_native_x86_64`	✅	5s	5s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	4s	2s	+100%
`mlk_ct_cmov_zero`	✅	4s	2s	+100%
`mlk_gen_matrix`	✅	4s	3s	+33%
`mlk_invntt_layer`	✅	4s	4s	+0%
`mlk_matvec_mul`	✅	4s	4s	+0%
`mlk_poly_compress_d10_native`	✅	4s	2s	+100%
`mlk_poly_compress_d4_c`	✅	4s	3s	+33%
`mlk_poly_compress_d5_native`	✅	4s	3s	+33%
`mlk_poly_decompress_du`	✅	4s	3s	+33%
`mlk_poly_frombytes_c`	✅	4s	7s	-43%
`mlk_poly_getnoise_eta1_4x`	✅	4s	1s	+300%
`mlk_polyvec_compress_du`	✅	4s	4s	+0%
`mlk_polyvec_frombytes`	✅	4s	3s	+33%
`mlk_polyvec_ntt`	✅	4s	6s	-33%
`mlk_shake256`	✅	4s	2s	+100%
`poly_decompress_d10_native_x86_64`	✅	4s	2s	+100%
`poly_frombytes_native_x86_64`	✅	4s	6s	-33%
`poly_getnoise_eta1122_4x_native`	✅	4s	1s	+300%
`poly_reduce_native_x86_64`	✅	4s	2s	+100%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	✅	4s	1s	+300%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	4s	1s	+300%
`keccak_f1600_x1_native_aarch64_v84a`	✅	3s	1s	+200%
`kem_check_pk`	✅	3s	3s	+0%
`kem_keypair_derand`	✅	3s	3s	+0%
`mlk_ct_cmask_nonzero_u8`	✅	3s	1s	+200%
`mlk_ct_get_optblocker_i32`	✅	3s	2s	+50%
`mlk_ct_sel_uint8`	✅	3s	2s	+50%
`mlk_keccak_absorb_once`	✅	3s	3s	+0%
`mlk_keccakf1600x4_permute`	✅	3s	1s	+200%
`mlk_keccakf1600x4_xor_bytes_c`	✅	3s	2s	+50%
`mlk_poly_cbd_eta1`	✅	3s	2s	+50%
`mlk_poly_cbd_eta2`	✅	3s	1s	+200%
`mlk_poly_compress_d4_native`	✅	3s	2s	+50%
`mlk_poly_decompress_d11`	✅	3s	5s	-40%
`mlk_poly_decompress_d4_c`	✅	3s	5s	-40%
`mlk_poly_decompress_d5_c`	✅	3s	2s	+50%
`mlk_poly_invntt_tomont_c`	✅	3s	1s	+200%
`mlk_poly_mulcache_compute`	✅	3s	3s	+0%
`mlk_poly_ntt_c`	✅	3s	3s	+0%
`mlk_poly_tobytes_native`	✅	3s	3s	+0%
`mlk_polyvec_mulcache_compute`	✅	3s	2s	+50%
`mlk_polyvec_tobytes`	✅	3s	4s	-25%
`mlk_scalar_compress_d1`	✅	3s	2s	+50%
`mlk_scalar_compress_d10`	✅	3s	2s	+50%
`mlk_scalar_compress_d4`	✅	3s	3s	+0%
`mlk_scalar_decompress_d10`	✅	3s	2s	+50%
`mlk_scalar_decompress_d11`	✅	3s	2s	+50%
`mlk_shake128x4_absorb_once`	✅	3s	4s	-25%
`mlk_shake256x4`	✅	3s	5s	-40%
`ntt_native_x86_64`	✅	3s	1s	+200%
`nttunpack_native_x86_64`	✅	3s	2s	+50%
`poly_reduce_native_aarch64`	✅	3s	4s	-25%
`poly_tobytes_native_x86_64`	✅	3s	3s	+0%
`poly_tomont_native_x86_64`	✅	3s	4s	-25%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	3s	2s	+50%
`intt_native_aarch64`	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	2s	+0%
`keccakf1600_permute_native`	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes_native`	✅	2s	5s	-60%
`kem_check_sk`	✅	2s	2s	+0%
`kem_enc`	✅	2s	4s	-50%
`kem_enc_derand`	✅	2s	3s	-33%
`kem_keypair`	✅	2s	2s	+0%
`mlk_check_pct`	✅	2s	2s	+0%
`mlk_ct_cmask_neg_i16`	✅	2s	2s	+0%
`mlk_ct_cmask_nonzero_u16`	✅	2s	2s	+0%
`mlk_ct_get_optblocker_u8`	✅	2s	2s	+0%
`mlk_gen_matrix_serial`	✅	2s	4s	-50%
`mlk_keccakf1600_extract_bytes`	✅	2s	3s	-33%
`mlk_keccakf1600_xor_bytes`	✅	2s	3s	-33%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	2s	6s	-67%
`mlk_keccakf1600x4_extract_bytes`	✅	2s	3s	-33%
`mlk_keccakf1600x4_extract_bytes_c`	✅	2s	1s	+100%
`mlk_keccakf1600x4_xor_bytes`	✅	2s	2s	+0%
`mlk_poly_compress_d10`	✅	2s	2s	+0%
`mlk_poly_compress_d10_c`	✅	2s	2s	+0%
`mlk_poly_compress_d11_c`	✅	2s	1s	+100%
`mlk_poly_compress_d4`	✅	2s	1s	+100%
`mlk_poly_compress_d5`	✅	2s	2s	+0%
`mlk_poly_compress_du`	✅	2s	3s	-33%
`mlk_poly_decompress_d10_c`	✅	2s	3s	-33%
`mlk_poly_decompress_d11_c`	✅	2s	1s	+100%
`mlk_poly_decompress_d11_native`	✅	2s	1s	+100%
`mlk_poly_decompress_d4`	✅	2s	2s	+0%
`mlk_poly_decompress_d5`	✅	2s	2s	+0%
`mlk_poly_decompress_d5_native`	✅	2s	3s	-33%
`mlk_poly_decompress_dv`	✅	2s	3s	-33%
`mlk_poly_getnoise_eta2`	✅	2s	3s	-33%
`mlk_poly_invntt_tomont`	✅	2s	2s	+0%
`mlk_poly_mulcache_compute_c`	✅	2s	2s	+0%
`mlk_poly_mulcache_compute_native`	✅	2s	1s	+100%
`mlk_poly_reduce`	✅	2s	3s	-33%
`mlk_poly_reduce_c`	✅	2s	3s	-33%
`mlk_poly_tobytes`	✅	2s	2s	+0%
`mlk_poly_tomont`	✅	2s	7s	-71%
`mlk_poly_tomont_native`	✅	2s	2s	+0%
`mlk_poly_tomsg`	✅	2s	4s	-50%
`mlk_polymat_permute_bitrev_to_custom`	✅	2s	3s	-33%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	2s	2s	+0%
`mlk_polyvec_decompress_du`	✅	2s	2s	+0%
`mlk_polyvec_permute_bitrev_to_custom`	✅	2s	2s	+0%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	2s	2s	+0%
`mlk_polyvec_reduce`	✅	2s	1s	+100%
`mlk_rej_uniform`	✅	2s	4s	-50%
`mlk_scalar_compress_d11`	✅	2s	5s	-60%
`mlk_scalar_decompress_d4`	✅	2s	3s	-33%
`mlk_scalar_decompress_d5`	✅	2s	3s	-33%
`mlk_shake128_squeezeblocks`	✅	2s	2s	+0%
`mlk_shake128x4_squeezeblocks`	✅	2s	1s	+100%
`mlk_value_barrier_u32`	✅	2s	2s	+0%
`ntt_native_aarch64`	✅	2s	3s	-33%
`poly_compress_d10_native_x86_64`	✅	2s	2s	+0%
`poly_compress_d11_native_x86_64`	✅	2s	3s	-33%
`poly_compress_d4_native_x86_64`	✅	2s	2s	+0%
`poly_compress_d5_native_x86_64`	✅	2s	2s	+0%
`poly_decompress_d5_native_x86_64`	✅	2s	2s	+0%
`poly_invntt_tomont_native`	✅	2s	4s	-50%
`poly_mulcache_compute_native_aarch64`	✅	2s	3s	-33%
`poly_tobytes_native_aarch64`	✅	2s	1s	+100%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	✅	2s	4s	-50%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	✅	2s	3s	-33%
`rej_uniform_native`	✅	2s	4s	-50%
`sys_check_capability`	✅	2s	2s	+0%
`intt_native_x86_64`	✅	1s	2s	-50%
`keccak_f1600_x4_native_avx2`	✅	1s	1s	+0%
`keccakf1600x4_xor_bytes_native`	✅	1s	2s	-50%
`mlk_ct_get_optblocker_u32`	✅	1s	4s	-75%
`mlk_ct_memcmp`	✅	1s	3s	-67%
`mlk_ct_sel_int16`	✅	1s	3s	-67%
`mlk_enc_getnoise_eta1_eta2`	✅	1s	1s	+0%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	1s	2s	-50%
`mlk_keccakf1600_permute`	✅	1s	2s	-50%
`mlk_montgomery_reduce`	✅	1s	2s	-50%
`mlk_poly_compress_d11`	✅	1s	2s	-50%
`mlk_poly_compress_d11_native`	✅	1s	3s	-67%
`mlk_poly_compress_d5_c`	✅	1s	2s	-50%
`mlk_poly_compress_dv`	✅	1s	4s	-75%
`mlk_poly_decompress_d10`	✅	1s	2s	-50%
`mlk_poly_frombytes`	✅	1s	4s	-75%
`mlk_poly_getnoise_eta1_4x_native`	✅	1s	3s	-67%
`mlk_poly_tobytes_c`	✅	1s	2s	-50%
`mlk_poly_tomont_c`	✅	1s	2s	-50%
`mlk_polyvec_invntt_tomont`	✅	1s	3s	-67%
`mlk_polyvec_tomont`	✅	1s	1s	+0%
`mlk_scalar_compress_d5`	✅	1s	5s	-80%
`mlk_scalar_signed_to_unsigned_q`	✅	1s	3s	-67%
`mlk_sha3_256`	✅	1s	3s	-67%
`mlk_sha3_512`	✅	1s	4s	-75%
`mlk_shake128_absorb_once`	✅	1s	2s	-50%
`mlk_value_barrier_i32`	✅	1s	3s	-67%
`mlk_value_barrier_u8`	✅	1s	3s	-67%
`poly_decompress_d11_native_x86_64`	✅	1s	2s	-50%
`poly_mulcache_compute_native_x86_64`	✅	1s	2s	-50%
`poly_tomont_native_aarch64`	✅	1s	5s	-80%

oqs-bot · 2026-05-04T11:36:46Z

CBMC Results (ML-KEM-1024)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2110s	1673s	+26.1%
`mlk_indcpa_dec`	⚠️	21s	11s	+91%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	⚠️	118s	65s	+82%
`polyvec_basemul_acc_montgomery_cached_native`	⚠️	374s	28s	+1236%
`rej_uniform_native_aarch64`	⚠️	54s	34s	+59%

Full Results (191 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2110s	1673s	+26.1%
`mlk_indcpa_enc`	✅	382s	381s	+0%
`polyvec_basemul_acc_montgomery_cached_native`	⚠️	374s	28s	+1236%
`mlk_indcpa_keypair_derand`	✅	183s	160s	+14%
`mlk_poly_rej_uniform`	✅	133s	133s	+0%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	⚠️	118s	65s	+82%
`mlk_rej_uniform_c`	✅	96s	112s	-14%
`rej_uniform_native_x86_64`	✅	56s	58s	-3%
`rej_uniform_native_aarch64`	⚠️	54s	34s	+59%
`poly_ntt_native`	✅	37s	35s	+6%
`mlk_poly_reduce_native`	✅	34s	34s	+0%
`mlk_ntt_layer`	✅	30s	28s	+7%
`mlk_keccak_squeezeblocks_x4`	✅	26s	26s	+0%
`mlk_indcpa_dec`	⚠️	21s	11s	+91%
`keccakf1600x4_permute_native_x4`	✅	18s	15s	+20%
`mlk_polyvec_add`	✅	16s	17s	-6%
`mlk_poly_decompress_d11_native`	✅	15s	13s	+15%
`mlk_poly_decompress_d5_native`	✅	13s	13s	+0%
`mlk_poly_frommsg`	✅	12s	8s	+50%
`mlk_polymat_permute_bitrev_to_custom`	✅	12s	4s	+200%
`mlk_ntt_butterfly_block`	✅	9s	6s	+50%
`mlk_poly_frombytes_native`	✅	9s	9s	+0%
`mlk_keccak_squeeze_once`	✅	8s	7s	+14%
`mlk_keccak_squeezeblocks`	✅	8s	9s	-11%
`mlk_poly_add`	✅	8s	6s	+33%
`poly_decompress_d11_native_x86_64`	✅	8s	4s	+100%
`mlk_poly_ntt`	✅	7s	6s	+17%
`kem_dec`	✅	6s	4s	+50%
`mlk_keccak_absorb_once`	✅	6s	3s	+100%
`mlk_keccak_absorb_once_x4`	✅	6s	7s	-14%
`poly_frombytes_native_x86_64`	✅	6s	6s	+0%
`mlk_fqmul`	✅	5s	17s	-71%
`mlk_invntt_layer`	✅	5s	9s	-44%
`mlk_keccakf1600_permute_c`	✅	5s	4s	+25%
`mlk_poly_getnoise_eta2`	✅	5s	3s	+67%
`mlk_poly_ntt_c`	✅	5s	3s	+67%
`mlk_poly_rej_uniform_x4`	✅	5s	6s	-17%
`mlk_poly_sub`	✅	5s	7s	-29%
`mlk_polyvec_invntt_tomont`	✅	5s	1s	+400%
`mlk_scalar_compress_d5`	✅	5s	3s	+67%
`poly_decompress_d10_native_x86_64`	✅	5s	3s	+67%
`keccakf1600x4_xor_bytes_native`	✅	4s	1s	+300%
`kem_enc`	✅	4s	3s	+33%
`mlk_check_pct`	✅	4s	3s	+33%
`mlk_gen_matrix`	✅	4s	2s	+100%
`mlk_gen_matrix_serial`	✅	4s	7s	-43%
`mlk_keccakf1600_permute`	✅	4s	1s	+300%
`mlk_keccakf1600x4_extract_bytes`	✅	4s	4s	+0%
`mlk_matvec_mul`	✅	4s	3s	+33%
`mlk_poly_compress_d5_c`	✅	4s	1s	+300%
`mlk_poly_decompress_d10_c`	✅	4s	1s	+300%
`mlk_poly_frombytes_c`	✅	4s	6s	-33%
`mlk_poly_tomsg`	✅	4s	2s	+100%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	4s	2s	+100%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	4s	4s	+0%
`mlk_polyvec_reduce`	✅	4s	1s	+300%
`mlk_polyvec_tomont`	✅	4s	4s	+0%
`mlk_scalar_compress_d11`	✅	4s	1s	+300%
`mlk_scalar_decompress_d5`	✅	4s	3s	+33%
`mlk_value_barrier_u32`	✅	4s	2s	+100%
`poly_reduce_native_x86_64`	✅	4s	2s	+100%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	✅	4s	3s	+33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	2s	+50%
`kem_check_pk`	✅	3s	3s	+0%
`mlk_ct_cmask_neg_i16`	✅	3s	3s	+0%
`mlk_ct_cmask_nonzero_u8`	✅	3s	4s	-25%
`mlk_ct_cmov_zero`	✅	3s	2s	+50%
`mlk_keccakf1600x4_xor_bytes_c`	✅	3s	3s	+0%
`mlk_poly_compress_d10`	✅	3s	2s	+50%
`mlk_poly_compress_d10_c`	✅	3s	2s	+50%
`mlk_poly_compress_d11_c`	✅	3s	4s	-25%
`mlk_poly_compress_du`	✅	3s	3s	+0%
`mlk_poly_decompress_d10_native`	✅	3s	2s	+50%
`mlk_poly_decompress_d11`	✅	3s	2s	+50%
`mlk_poly_decompress_d4`	✅	3s	2s	+50%
`mlk_poly_decompress_d5`	✅	3s	3s	+0%
`mlk_poly_decompress_dv`	✅	3s	4s	-25%
`mlk_poly_getnoise_eta1_4x`	✅	3s	3s	+0%
`mlk_poly_getnoise_eta1_4x_native`	✅	3s	5s	-40%
`mlk_poly_mulcache_compute`	✅	3s	2s	+50%
`mlk_poly_mulcache_compute_c`	✅	3s	1s	+200%
`mlk_poly_tobytes_native`	✅	3s	2s	+50%
`mlk_poly_tomont_c`	✅	3s	2s	+50%
`mlk_polyvec_frombytes`	✅	3s	5s	-40%
`mlk_scalar_decompress_d4`	✅	3s	4s	-25%
`mlk_shake128_absorb_once`	✅	3s	3s	+0%
`poly_compress_d10_native_x86_64`	✅	3s	4s	-25%
`poly_compress_d5_native_x86_64`	✅	3s	3s	+0%
`poly_decompress_d4_native_x86_64`	✅	3s	2s	+50%
`poly_decompress_d5_native_x86_64`	✅	3s	3s	+0%
`poly_getnoise_eta1122_4x_native`	✅	3s	3s	+0%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	3s	2s	+50%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	✅	3s	2s	+50%
`rej_uniform_native`	✅	3s	1s	+200%
`sys_check_capability`	✅	3s	4s	-25%
`intt_native_x86_64`	✅	2s	4s	-50%
`keccak_f1600_x1_native_aarch64`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	2s	+0%
`keccakf1600_permute_native`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	✅	2s	2s	+0%
`kem_enc_derand`	✅	2s	3s	-33%
`kem_keypair`	✅	2s	3s	-33%
`kem_keypair_derand`	✅	2s	1s	+100%
`mlk_ct_cmask_nonzero_u16`	✅	2s	1s	+100%
`mlk_ct_get_optblocker_i32`	✅	2s	2s	+0%
`mlk_ct_get_optblocker_u32`	✅	2s	1s	+100%
`mlk_ct_memcmp`	✅	2s	3s	-33%
`mlk_ct_sel_int16`	✅	2s	1s	+100%
`mlk_enc_getnoise_eta1_eta2`	✅	2s	1s	+100%
`mlk_keccakf1600_extract_bytes`	✅	2s	3s	-33%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	2s	2s	+0%
`mlk_keccakf1600_xor_bytes`	✅	2s	2s	+0%
`mlk_keccakf1600x4_extract_bytes_c`	✅	2s	3s	-33%
`mlk_keccakf1600x4_permute`	✅	2s	2s	+0%
`mlk_poly_cbd_eta1`	✅	2s	3s	-33%
`mlk_poly_cbd_eta2`	✅	2s	2s	+0%
`mlk_poly_compress_d10_native`	✅	2s	2s	+0%
`mlk_poly_compress_d11_native`	✅	2s	2s	+0%
`mlk_poly_compress_d4`	✅	2s	2s	+0%
`mlk_poly_compress_d4_c`	✅	2s	3s	-33%
`mlk_poly_compress_d4_native`	✅	2s	3s	-33%
`mlk_poly_compress_d5_native`	✅	2s	2s	+0%
`mlk_poly_compress_dv`	✅	2s	3s	-33%
`mlk_poly_decompress_d10`	✅	2s	2s	+0%
`mlk_poly_decompress_d11_c`	✅	2s	2s	+0%
`mlk_poly_decompress_d4_c`	✅	2s	3s	-33%
`mlk_poly_decompress_d4_native`	✅	2s	2s	+0%
`mlk_poly_decompress_d5_c`	✅	2s	1s	+100%
`mlk_poly_getnoise_eta1122_4x`	✅	2s	4s	-50%
`mlk_poly_invntt_tomont_c`	✅	2s	2s	+0%
`mlk_poly_mulcache_compute_native`	✅	2s	3s	-33%
`mlk_poly_reduce_c`	✅	2s	3s	-33%
`mlk_poly_tobytes`	✅	2s	2s	+0%
`mlk_poly_tobytes_c`	✅	2s	2s	+0%
`mlk_poly_tomont`	✅	2s	1s	+100%
`mlk_poly_tomont_native`	✅	2s	2s	+0%
`mlk_polyvec_compress_du`	✅	2s	3s	-33%
`mlk_polyvec_decompress_du`	✅	2s	3s	-33%
`mlk_polyvec_mulcache_compute`	✅	2s	4s	-50%
`mlk_polyvec_ntt`	✅	2s	9s	-78%
`mlk_polyvec_permute_bitrev_to_custom`	✅	2s	1s	+100%
`mlk_polyvec_tobytes`	✅	2s	3s	-33%
`mlk_scalar_compress_d1`	✅	2s	2s	+0%
`mlk_scalar_compress_d10`	✅	2s	4s	-50%
`mlk_scalar_compress_d4`	✅	2s	2s	+0%
`mlk_scalar_signed_to_unsigned_q`	✅	2s	3s	-33%
`mlk_shake128x4_absorb_once`	✅	2s	1s	+100%
`mlk_shake128x4_squeezeblocks`	✅	2s	4s	-50%
`mlk_shake256`	✅	2s	1s	+100%
`mlk_shake256x4`	✅	2s	3s	-33%
`mlk_value_barrier_i32`	✅	2s	3s	-33%
`mlk_value_barrier_u8`	✅	2s	2s	+0%
`nttunpack_native_x86_64`	✅	2s	6s	-67%
`poly_compress_d11_native_x86_64`	✅	2s	3s	-33%
`poly_compress_d4_native_x86_64`	✅	2s	2s	+0%
`poly_mulcache_compute_native_aarch64`	✅	2s	1s	+100%
`poly_mulcache_compute_native_x86_64`	✅	2s	4s	-50%
`poly_tobytes_native_x86_64`	✅	2s	3s	-33%
`poly_tomont_native_x86_64`	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	2s	1s	+100%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	✅	2s	3s	-33%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	2s	4s	-50%
`intt_native_aarch64`	✅	1s	1s	+0%
`keccak_f1600_x4_native_avx2`	✅	1s	1s	+0%
`kem_check_sk`	✅	1s	1s	+0%
`mlk_barrett_reduce`	✅	1s	2s	-50%
`mlk_ct_get_optblocker_u8`	✅	1s	2s	-50%
`mlk_ct_sel_uint8`	✅	1s	2s	-50%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	1s	2s	-50%
`mlk_keccakf1600x4_xor_bytes`	✅	1s	2s	-50%
`mlk_keypair_getnoise_eta1`	✅	1s	3s	-67%
`mlk_montgomery_reduce`	✅	1s	1s	+0%
`mlk_poly_compress_d11`	✅	1s	3s	-67%
`mlk_poly_compress_d5`	✅	1s	3s	-67%
`mlk_poly_decompress_du`	✅	1s	1s	+0%
`mlk_poly_frombytes`	✅	1s	2s	-50%
`mlk_poly_invntt_tomont`	✅	1s	1s	+0%
`mlk_poly_reduce`	✅	1s	2s	-50%
`mlk_rej_uniform`	✅	1s	1s	+0%
`mlk_scalar_decompress_d10`	✅	1s	2s	-50%
`mlk_scalar_decompress_d11`	✅	1s	1s	+0%
`mlk_sha3_256`	✅	1s	2s	-50%
`mlk_sha3_512`	✅	1s	4s	-75%
`mlk_shake128_squeezeblocks`	✅	1s	1s	+0%
`ntt_native_aarch64`	✅	1s	2s	-50%
`ntt_native_x86_64`	✅	1s	3s	-67%
`poly_invntt_tomont_native`	✅	1s	5s	-80%
`poly_reduce_native_aarch64`	✅	1s	1s	+0%
`poly_tobytes_native_aarch64`	✅	1s	1s	+0%
`poly_tomont_native_aarch64`	✅	1s	4s	-75%

rod-chapman · 2026-05-08T11:09:11Z

Update. I am having trouble getting one proof to work - it's polvec_basemul_acc_montgomery_cached_native().
The problem is the need to carry the stronger pre- and post-conditions across the call to the native back-end in a way that they "survive" so that, if the first call to the native backend responds with "FALLBACK", they are still true for the second call to the C backend. The problem is that the native backend changes representation of the types (e.g. from polyvec * to int16_t b[MLKEM_K * MLKEM_N which makes the reasoning sufficiently complex to defeat Z3.

rod-chapman · 2026-05-09T05:24:35Z

C Proofs are OK now. I found a Z3 tactic that was effective. @dkostic The next move is to prove that the bounds on the outputs of the AArch64 native implementation of basemul are as expected, and as given by the specification of those 3 functions in native/aarch64/src/arith_native_aarch64.h on the refine_bounds branch. The CBMC spec of that for K=2 is here:

mlkem-native/mlkem/src/native/aarch64/src/arith_native_aarch64.h

Line 134 in 8d39977

ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))

The critical contract is ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))

We need to know that's true for the assembly language versions (3 times for K=2,3,4), so that means amending the HOL-Light proof to explicitly state that post-condition. For K=2, that's here or thereabouts:

mlkem-native/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm.ml

Line 328 in 8d39977

==> (ival(read(memory :> bytes16(word_add dst (word (4 * i)))) s) ==

Does that make sense?

Tighten the base-multiplication output bounds across the CBMC and HOL Light proofs by constraining the second operand and its multiplication cache. AArch64: - HOL Light: prove output bounds for poly_basemul_acc_montgomery_cached k2/k3/k4 under |b| < 8*MLKEM_Q and |b_cache| < MLKEM_Q, giving abs(r) <= 8323 / 11652 / 14981 respectively (previously the looser 9857 / 13953 / 18049 under unconstrained b/b_cache). - Add matching CBMC input/output bound contracts to the basemul declarations. x86_64: - Append a Barrett-reduction sweep to the AVX2 basemul kernels so every output coefficient is bounded by abs(r) < 2*MLKEM_Q regardless of k (previously grew to ~8*Q at k=4). - HOL Light: update the basemul proofs for the Barrett reduction (refresh bytecode, fold barred_x86, hoist input bound assumptions) and strengthen the postconditions with abs(r) <= 6657. - Add matching input/output bound CBMC contracts. Also includes the earlier CBMC base-multiplication bound refinements and the cassert()->mlk_assert() correction. Signed-off-by: Dusan Kostic <dkostic@amazon.com>

dkostic · 2026-06-22T16:10:49Z

Before and after performance measured on m8i EC2 instance with Intel(R) Xeon(R) 6975P-C:

  ┌──────────────┬──────────────────┬────────┬────────┬──────────────────┬────────┬────────┬───────────────────┬─────────┬─────────┐
  │              │ mlkem512 keypair │ encaps │ decaps │ mlkem768 keypair │ encaps │ decaps │ mlkem1024 keypair │ encaps  │ decaps  │
  ├──────────────┼──────────────────┼────────┼────────┼──────────────────┼────────┼────────┼───────────────────┼─────────┼─────────┤
  │ no Barrett   │ 37 359           │ 43 892 │ 55 961 │ 60 371           │ 68 916 │ 84 209 │ 90 615            │ 104 190 │ 122 639 │
  ├──────────────┼──────────────────┼────────┼────────┼──────────────────┼────────┼────────┼───────────────────┼─────────┼─────────┤
  │ with Barrett │ 37 345           │ 43 784 │ 55 847 │ 60 867           │ 69 213 │ 84 345 │ 90 648            │ 104 279 │ 122 820 │
  ├──────────────┼──────────────────┼────────┼────────┼──────────────────┼────────┼────────┼───────────────────┼─────────┼─────────┤
  │ Δ cycles     │ −14              │ −108   │ −114   │ +496             │ +297   │ +136   │ +33               │ +89     │ +181    │
  ├──────────────┼──────────────────┼────────┼────────┼──────────────────┼────────┼────────┼───────────────────┼─────────┼─────────┤
  │ Δ %          │ −0.04%           │ −0.25% │ −0.20% │ +0.82%           │ +0.43% │ +0.16% │ +0.04%            │ +0.09%  │ +0.15%  │
  └──────────────┴──────────────────┴────────┴────────┴──────────────────┴────────┴────────┴───────────────────┴─────────┴─────────┘

hanno-becker added enhancement New feature or request CBMC labels Mar 24, 2025

hanno-becker force-pushed the refine_bounds branch 4 times, most recently from 1326e42 to f9b25ee Compare March 24, 2025 11:12

hanno-becker marked this pull request as ready for review March 24, 2025 12:56

hanno-becker requested a review from a team as a code owner March 24, 2025 12:56

hanno-becker added the benchmark this PR should be benchmarked in CI label Mar 24, 2025

oqs-bot reviewed Mar 24, 2025

View reviewed changes

hanno-becker removed the benchmark this PR should be benchmarked in CI label Mar 24, 2025

rod-chapman force-pushed the refine_bounds branch 2 times, most recently from 65200d7 to dca2a1f Compare October 13, 2025 06:30

rod-chapman force-pushed the refine_bounds branch from dca2a1f to 44ba045 Compare November 3, 2025 04:32

rod-chapman force-pushed the refine_bounds branch from bdd712e to 5298417 Compare December 17, 2025 11:12

rod-chapman force-pushed the refine_bounds branch from 1a12828 to 1de0ae8 Compare January 13, 2026 12:22

rod-chapman force-pushed the refine_bounds branch from 1de0ae8 to 978b31c Compare March 10, 2026 15:16

rod-chapman force-pushed the refine_bounds branch from 978b31c to 7cd3fa0 Compare March 23, 2026 17:40

rod-chapman force-pushed the refine_bounds branch from 7cd3fa0 to abf2390 Compare May 4, 2026 10:47

rod-chapman force-pushed the refine_bounds branch 2 times, most recently from 9e4db99 to 7f2d2bc Compare May 8, 2026 14:43

rod-chapman force-pushed the refine_bounds branch 2 times, most recently from 085d1f0 to 999f564 Compare May 18, 2026 07:45

rod-chapman force-pushed the refine_bounds branch from 999f564 to 0495fe6 Compare May 19, 2026 09:00

dkostic force-pushed the refine_bounds branch 4 times, most recently from 457c655 to bc59d2d Compare June 12, 2026 19:04

dkostic force-pushed the refine_bounds branch from bc59d2d to 4b8afa5 Compare June 22, 2026 14:03

Uh oh!

Conversation

hanno-becker commented Mar 24, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Mac Mini (M1, 2020) benchmarks

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Intel Xeon 4th gen (c7i)

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

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

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Arm Cortex-A55 (Snapdragon 888) benchmarks

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

AMD EPYC 4th gen (c7a)

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

AMD EPYC 3rd gen (c6a)

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Intel Xeon 3rd gen (c6i)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

⚠️ Performance Alert ⚠️

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

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

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

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

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Graviton4

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

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

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Graviton4 (no-opt)

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Graviton3

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Graviton2

Uh oh!

oqs-bot left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

hanno-becker commented Mar 24, 2025 •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot commented May 4, 2026 •

edited

Loading

oqs-bot commented May 4, 2026 •

edited

Loading

oqs-bot commented May 4, 2026 •

edited

Loading