HOL Light: Prove correctness of AVX2 `poly_compress_d{4,5,10,11}` by mkannwischer · Pull Request #1545 · pq-code-package/mlkem-native

mkannwischer · 2026-02-04T11:21:19Z

No description provided.

oqs-bot

Mac Mini (M1, 2020) benchmarks

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`12320` cycles	`12321` cycles	`1.00`
`ML-KEM-512 encaps`	`14997` cycles	`14998` cycles	`1.00`
`ML-KEM-512 decaps`	`19552` cycles	`19558` cycles	`1.00`
`ML-KEM-768 keypair`	`21085` cycles	`21085` cycles	`1`
`ML-KEM-768 encaps`	`23871` cycles	`23871` cycles	`1`
`ML-KEM-768 decaps`	`30413` cycles	`30414` cycles	`1.00`
`ML-KEM-1024 keypair`	`30331` cycles	`30332` cycles	`1.00`
`ML-KEM-1024 encaps`	`34576` cycles	`34576` cycles	`1`
`ML-KEM-1024 decaps`	`44183` cycles	`44186` cycles	`1.00`

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

oqs-bot

ppc64le (POWER10) benchmarks

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`59347` cycles	`59750` cycles	`0.99`
`ML-KEM-512 encaps`	`71831` cycles	`72459` cycles	`0.99`
`ML-KEM-512 decaps`	`91670` cycles	`92376` cycles	`0.99`
`ML-KEM-768 keypair`	`99543` cycles	`98711` cycles	`1.01`
`ML-KEM-768 encaps`	`116314` cycles	`115024` cycles	`1.01`
`ML-KEM-768 decaps`	`142257` cycles	`140921` cycles	`1.01`
`ML-KEM-1024 keypair`	`148861` cycles	`150328` cycles	`0.99`
`ML-KEM-1024 encaps`	`167254` cycles	`168943` cycles	`0.99`
`ML-KEM-1024 decaps`	`198649` cycles	`200353` cycles	`0.99`

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

oqs-bot

Arm Cortex-A76 (Raspberry Pi 5) benchmarks

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`28266` cycles	`28233` cycles	`1.00`
`ML-KEM-512 encaps`	`34111` cycles	`34106` cycles	`1.00`
`ML-KEM-512 decaps`	`44383` cycles	`44329` cycles	`1.00`
`ML-KEM-768 keypair`	`47678` cycles	`47626` cycles	`1.00`
`ML-KEM-768 encaps`	`53935` cycles	`53954` cycles	`1.00`
`ML-KEM-768 decaps`	`68367` cycles	`68377` cycles	`1.00`
`ML-KEM-1024 keypair`	`70328` cycles	`70254` cycles	`1.00`
`ML-KEM-1024 encaps`	`78732` cycles	`78807` cycles	`1.00`
`ML-KEM-1024 decaps`	`98431` cycles	`98438` 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 'ppc64le (POWER10) benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `3656b1a`	Previous: `09c31cb`	Ratio
`ML-KEM-768 keypair`	`102020` cycles	`98898` cycles	`1.03`
`ML-KEM-768 encaps`	`119213` cycles	`115162` cycles	`1.04`
`ML-KEM-768 decaps`	`145398` cycles	`140953` cycles	`1.03`
`ML-KEM-1024 encaps`	`172323` cycles	`167223` cycles	`1.03`

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

oqs-bot

Intel Xeon 4th gen (c7i)

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`9729` cycles	`9523` cycles	`1.02`
`ML-KEM-512 encaps`	`11253` cycles	`11346` cycles	`0.99`
`ML-KEM-512 decaps`	`15412` cycles	`15424` cycles	`1.00`
`ML-KEM-768 keypair`	`16159` cycles	`16308` cycles	`0.99`
`ML-KEM-768 encaps`	`17686` cycles	`17956` cycles	`0.98`
`ML-KEM-768 decaps`	`23300` cycles	`23550` cycles	`0.99`
`ML-KEM-1024 keypair`	`22328` cycles	`22080` cycles	`1.01`
`ML-KEM-1024 encaps`	`24724` cycles	`24538` cycles	`1.01`
`ML-KEM-1024 decaps`	`32167` cycles	`32304` 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: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`59739` cycles	`59741` cycles	`1.00`
`ML-KEM-512 encaps`	`67387` cycles	`67378` cycles	`1.00`
`ML-KEM-512 decaps`	`86118` cycles	`86085` cycles	`1.00`
`ML-KEM-768 keypair`	`97313` cycles	`97361` cycles	`1.00`
`ML-KEM-768 encaps`	`110826` cycles	`110891` cycles	`1.00`
`ML-KEM-768 decaps`	`137504` cycles	`138131` cycles	`1.00`
`ML-KEM-1024 keypair`	`154503` cycles	`154743` cycles	`1.00`
`ML-KEM-1024 encaps`	`171090` cycles	`171946` cycles	`1.00`
`ML-KEM-1024 decaps`	`207552` cycles	`208210` cycles	`1.00`

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

oqs-bot

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

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`28228` cycles	`28177` cycles	`1.00`
`ML-KEM-512 encaps`	`36504` cycles	`36564` cycles	`1.00`
`ML-KEM-512 decaps`	`45112` cycles	`45038` cycles	`1.00`
`ML-KEM-768 keypair`	`46171` cycles	`46259` cycles	`1.00`
`ML-KEM-768 encaps`	`55570` cycles	`55708` cycles	`1.00`
`ML-KEM-768 decaps`	`69905` cycles	`69786` cycles	`1.00`
`ML-KEM-1024 keypair`	`70418` cycles	`70313` cycles	`1.00`
`ML-KEM-1024 encaps`	`82573` cycles	`82568` cycles	`1.00`
`ML-KEM-1024 decaps`	`98950` cycles	`99391` cycles	`1.00`

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

oqs-bot

AMD EPYC 4th gen (c7a)

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`11718` cycles	`11789` cycles	`0.99`
`ML-KEM-512 encaps`	`13192` cycles	`13239` cycles	`1.00`
`ML-KEM-512 decaps`	`18077` cycles	`17987` cycles	`1.01`
`ML-KEM-768 keypair`	`20535` cycles	`20555` cycles	`1.00`
`ML-KEM-768 encaps`	`21202` cycles	`21567` cycles	`0.98`
`ML-KEM-768 decaps`	`28659` cycles	`28570` cycles	`1.00`
`ML-KEM-1024 keypair`	`27469` cycles	`27727` cycles	`0.99`
`ML-KEM-1024 encaps`	`29515` cycles	`29561` cycles	`1.00`
`ML-KEM-1024 decaps`	`38943` cycles	`39002` 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 'AMD EPYC 4th gen (c7a)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `3656b1a`	Previous: `ab4cead`	Ratio
`ML-KEM-512 encaps`	`13628` cycles	`13179` cycles	`1.03`

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

oqs-bot

AMD EPYC 3rd gen (c6a)

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`16869` cycles	`16917` cycles	`1.00`
`ML-KEM-512 encaps`	`18563` cycles	`18577` cycles	`1.00`
`ML-KEM-512 decaps`	`24072` cycles	`24112` cycles	`1.00`
`ML-KEM-768 keypair`	`28441` cycles	`28537` cycles	`1.00`
`ML-KEM-768 encaps`	`29595` cycles	`29608` cycles	`1.00`
`ML-KEM-768 decaps`	`37495` cycles	`37585` cycles	`1.00`
`ML-KEM-1024 keypair`	`41277` cycles	`41664` cycles	`0.99`
`ML-KEM-1024 encaps`	`43642` cycles	`44061` cycles	`0.99`
`ML-KEM-1024 decaps`	`54086` cycles	`54503` cycles	`0.99`

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

oqs-bot

Intel Xeon 3rd gen (c6i)

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`16205` cycles	`16153` cycles	`1.00`
`ML-KEM-512 encaps`	`18499` cycles	`18553` cycles	`1.00`
`ML-KEM-512 decaps`	`25069` cycles	`25091` cycles	`1.00`
`ML-KEM-768 keypair`	`28068` cycles	`27480` cycles	`1.02`
`ML-KEM-768 encaps`	`28904` cycles	`29770` cycles	`0.97`
`ML-KEM-768 decaps`	`39260` cycles	`39310` cycles	`1.00`
`ML-KEM-1024 keypair`	`37414` cycles	`37426` cycles	`1.00`
`ML-KEM-1024 encaps`	`40747` cycles	`40378` cycles	`1.01`
`ML-KEM-1024 decaps`	`55628` cycles	`54074` cycles	`1.03`

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

oqs-bot

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

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`36703` cycles	`36593` cycles	`1.00`
`ML-KEM-512 encaps`	`43046` cycles	`43062` cycles	`1.00`
`ML-KEM-512 decaps`	`55682` cycles	`55696` cycles	`1.00`
`ML-KEM-768 keypair`	`58587` cycles	`58622` cycles	`1.00`
`ML-KEM-768 encaps`	`67459` cycles	`67562` cycles	`1.00`
`ML-KEM-768 decaps`	`84385` cycles	`84375` cycles	`1.00`
`ML-KEM-1024 keypair`	`88903` cycles	`88935` cycles	`1.00`
`ML-KEM-1024 encaps`	`99096` cycles	`99124` cycles	`1.00`
`ML-KEM-1024 decaps`	`120572` cycles	`120521` cycles	`1.00`

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

oqs-bot

Graviton4

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`17676` cycles	`17657` cycles	`1.00`
`ML-KEM-512 encaps`	`20595` cycles	`20643` cycles	`1.00`
`ML-KEM-512 decaps`	`27072` cycles	`27057` cycles	`1.00`
`ML-KEM-768 keypair`	`29929` cycles	`29931` cycles	`1.00`
`ML-KEM-768 encaps`	`32733` cycles	`32801` cycles	`1.00`
`ML-KEM-768 decaps`	`41981` cycles	`41976` cycles	`1.00`
`ML-KEM-1024 keypair`	`43755` cycles	`43750` cycles	`1.00`
`ML-KEM-1024 encaps`	`48731` cycles	`48657` cycles	`1.00`
`ML-KEM-1024 decaps`	`61388` cycles	`61393` 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: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`40167` cycles	`40245` cycles	`1.00`
`ML-KEM-512 encaps`	`48363` cycles	`48414` cycles	`1.00`
`ML-KEM-512 decaps`	`62462` cycles	`62512` cycles	`1.00`
`ML-KEM-768 keypair`	`63791` cycles	`63653` cycles	`1.00`
`ML-KEM-768 encaps`	`74835` cycles	`74828` cycles	`1.00`
`ML-KEM-768 decaps`	`93545` cycles	`93492` cycles	`1.00`
`ML-KEM-1024 keypair`	`95086` cycles	`95144` cycles	`1.00`
`ML-KEM-1024 encaps`	`109123` cycles	`109324` cycles	`1.00`
`ML-KEM-1024 decaps`	`131844` cycles	`132082` cycles	`1.00`

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

oqs-bot

Graviton3

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`18659` cycles	`18662` cycles	`1.00`
`ML-KEM-512 encaps`	`21885` cycles	`21886` cycles	`1.00`
`ML-KEM-512 decaps`	`28878` cycles	`28869` cycles	`1.00`
`ML-KEM-768 keypair`	`31590` cycles	`31571` cycles	`1.00`
`ML-KEM-768 encaps`	`34743` cycles	`34808` cycles	`1.00`
`ML-KEM-768 decaps`	`44810` cycles	`44796` cycles	`1.00`
`ML-KEM-1024 keypair`	`46072` cycles	`46156` cycles	`1.00`
`ML-KEM-1024 encaps`	`51506` cycles	`51415` cycles	`1.00`
`ML-KEM-1024 decaps`	`65017` cycles	`65009` 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: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`45677` cycles	`45683` cycles	`1.00`
`ML-KEM-512 encaps`	`54449` cycles	`54200` cycles	`1.00`
`ML-KEM-512 decaps`	`69776` cycles	`69776` cycles	`1`
`ML-KEM-768 keypair`	`74187` cycles	`74192` cycles	`1.00`
`ML-KEM-768 encaps`	`86051` cycles	`86015` cycles	`1.00`
`ML-KEM-768 decaps`	`106633` cycles	`106640` cycles	`1.00`
`ML-KEM-1024 keypair`	`112097` cycles	`112026` cycles	`1.00`
`ML-KEM-1024 encaps`	`124606` cycles	`124528` cycles	`1.00`
`ML-KEM-1024 decaps`	`150640` cycles	`150656` cycles	`1.00`

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

oqs-bot

Graviton4 (no-opt)

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`35447` cycles	`35449` cycles	`1.00`
`ML-KEM-512 encaps`	`40090` cycles	`40183` cycles	`1.00`
`ML-KEM-512 decaps`	`51102` cycles	`51185` cycles	`1.00`
`ML-KEM-768 keypair`	`56747` cycles	`56701` cycles	`1.00`
`ML-KEM-768 encaps`	`64546` cycles	`64956` cycles	`0.99`
`ML-KEM-768 decaps`	`79383` cycles	`79034` cycles	`1.00`
`ML-KEM-1024 keypair`	`88002` cycles	`87863` cycles	`1.00`
`ML-KEM-1024 encaps`	`96984` cycles	`96878` cycles	`1.00`
`ML-KEM-1024 decaps`	`116076` cycles	`115822` cycles	`1.00`

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

oqs-bot

Graviton2

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`28266` cycles	`28304` cycles	`1.00`
`ML-KEM-512 encaps`	`34180` cycles	`34176` cycles	`1.00`
`ML-KEM-512 decaps`	`44384` cycles	`44456` cycles	`1.00`
`ML-KEM-768 keypair`	`47627` cycles	`47692` cycles	`1.00`
`ML-KEM-768 encaps`	`53950` cycles	`54036` cycles	`1.00`
`ML-KEM-768 decaps`	`68359` cycles	`68554` cycles	`1.00`
`ML-KEM-1024 keypair`	`70331` cycles	`70252` cycles	`1.00`
`ML-KEM-1024 encaps`	`78776` cycles	`78788` cycles	`1.00`
`ML-KEM-1024 decaps`	`98509` cycles	`98488` cycles	`1.00`

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

oqs-bot

Graviton3 (no-opt)

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`38940` cycles	`38939` cycles	`1.00`
`ML-KEM-512 encaps`	`44527` cycles	`44634` cycles	`1.00`
`ML-KEM-512 decaps`	`56584` cycles	`56707` cycles	`1.00`
`ML-KEM-768 keypair`	`62337` cycles	`62345` cycles	`1.00`
`ML-KEM-768 encaps`	`71069` cycles	`71769` cycles	`0.99`
`ML-KEM-768 decaps`	`87343` cycles	`87100` cycles	`1.00`
`ML-KEM-1024 keypair`	`96356` cycles	`96161` cycles	`1.00`
`ML-KEM-1024 encaps`	`106137` cycles	`106143` cycles	`1.00`
`ML-KEM-1024 decaps`	`126884` cycles	`126598` cycles	`1.00`

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

oqs-bot

Graviton2 (no-opt)

Details

Benchmark suite	Current: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`59076` cycles	`59084` cycles	`1.00`
`ML-KEM-512 encaps`	`68596` cycles	`68639` cycles	`1.00`
`ML-KEM-512 decaps`	`87335` cycles	`87370` cycles	`1.00`
`ML-KEM-768 keypair`	`95506` cycles	`95804` cycles	`1.00`
`ML-KEM-768 encaps`	`110331` cycles	`109900` cycles	`1.00`
`ML-KEM-768 decaps`	`134533` cycles	`135444` cycles	`0.99`
`ML-KEM-1024 keypair`	`147674` cycles	`147985` cycles	`1.00`
`ML-KEM-1024 encaps`	`163740` cycles	`163868` cycles	`1.00`
`ML-KEM-1024 decaps`	`195321` cycles	`195550` 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: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`155372` cycles	`155465` cycles	`1.00`
`ML-KEM-512 encaps`	`163233` cycles	`163351` cycles	`1.00`
`ML-KEM-512 decaps`	`206469` cycles	`206588` cycles	`1.00`
`ML-KEM-768 keypair`	`249714` cycles	`249883` cycles	`1.00`
`ML-KEM-768 encaps`	`270195` cycles	`270397` cycles	`1.00`
`ML-KEM-768 decaps`	`332474` cycles	`332134` cycles	`1.00`
`ML-KEM-1024 keypair`	`395444` cycles	`395687` cycles	`1.00`
`ML-KEM-1024 encaps`	`423271` cycles	`423463` cycles	`1.00`
`ML-KEM-1024 decaps`	`506841` cycles	`507256` 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: `7d9af85`	Previous: `4e44546`	Ratio
`ML-KEM-512 keypair`	`50770` cycles	`51003` cycles	`1.00`
`ML-KEM-512 encaps`	`59441` cycles	`58881` cycles	`1.01`
`ML-KEM-512 decaps`	`76264` cycles	`75041` cycles	`1.02`
`ML-KEM-768 keypair`	`86971` cycles	`85748` cycles	`1.01`
`ML-KEM-768 encaps`	`96215` cycles	`93667` cycles	`1.03`
`ML-KEM-768 decaps`	`119562` cycles	`117498` cycles	`1.02`
`ML-KEM-1024 keypair`	`130182` cycles	`130677` cycles	`1.00`
`ML-KEM-1024 encaps`	`142627` cycles	`143022` cycles	`1.00`
`ML-KEM-1024 decaps`	`173949` cycles	`173967` cycles	`1.00`

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

oqs-bot · 2026-02-06T05:05:34Z

CBMC Results (ML-KEM-512)

Full Results (185 proofs)

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

oqs-bot · 2026-02-06T05:06:28Z

CBMC Results (ML-KEM-768)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	1922s	1388s	+38.5%
`mlk_keccak_squeezeblocks_x4`	⚠️	232s	149s	+56%
`mlk_ntt_layer`	⚠️	29s	18s	+61%
`mlk_poly_reduce_native`	⚠️	22s	14s	+57%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	⚠️	87s	52s	+67%
`mlk_rej_uniform_c`	⚠️	125s	69s	+81%

Full Results (185 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	1922s	1388s	+38.5%
`mlk_indcpa_keypair_derand`	✅	315s	244s	+29%
`mlk_indcpa_enc`	✅	252s	195s	+29%
`mlk_keccak_squeezeblocks_x4`	⚠️	232s	149s	+56%
`mlk_rej_uniform_c`	⚠️	125s	69s	+81%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	⚠️	87s	52s	+67%
`polyvec_basemul_acc_montgomery_cached_native`	✅	78s	60s	+30%
`mlk_poly_rej_uniform`	✅	43s	33s	+30%
`mlk_polyvec_add`	✅	37s	28s	+32%
`poly_ntt_native`	✅	36s	29s	+24%
`mlk_ntt_layer`	⚠️	29s	18s	+61%
`keccakf1600x4_permute_native_x4`	✅	22s	17s	+29%
`mlk_indcpa_dec`	✅	22s	15s	+47%
`mlk_poly_reduce_native`	⚠️	22s	14s	+57%
`mlk_poly_decompress_d10_native`	✅	18s	15s	+20%
`mlk_poly_decompress_d4_native`	✅	17s	12s	+42%
`mlk_poly_frombytes_native`	✅	13s	8s	+62%
`mlk_poly_sub`	✅	13s	11s	+18%
`mlk_keccak_absorb_once_x4`	✅	12s	9s	+33%
`mlk_ntt_butterfly_block`	✅	11s	10s	+10%
`mlk_keccak_squeezeblocks`	✅	9s	10s	-10%
`mlk_polymat_permute_bitrev_to_custom`	✅	9s	6s	+50%
`mlk_fqmul`	✅	8s	8s	+0%
`mlk_keccak_squeeze_once`	✅	8s	7s	+14%
`mlk_poly_frommsg`	✅	8s	7s	+14%
`mlk_poly_rej_uniform_x4`	✅	8s	8s	+0%
`kem_dec`	✅	7s	5s	+40%
`mlk_invntt_layer`	✅	7s	4s	+75%
`intt_native_x86_64`	✅	6s	1s	+500%
`keccakf1600_permute_native`	✅	6s	8s	-25%
`mlk_gen_matrix`	✅	6s	4s	+50%
`mlk_gen_matrix_serial`	✅	6s	4s	+50%
`mlk_poly_mulcache_compute_c`	✅	6s	2s	+200%
`mlk_polyvec_tomont`	✅	6s	1s	+500%
`mlk_shake256x4`	✅	6s	3s	+100%
`mlk_ct_sel_uint8`	✅	5s	2s	+150%
`mlk_keccakf1600_permute`	✅	5s	3s	+67%
`mlk_keccakf1600_xor_bytes`	✅	5s	2s	+150%
`mlk_poly_compress_d10_c`	✅	5s	-	new
`mlk_poly_compress_d10_native`	✅	5s	-	new
`mlk_poly_tomsg`	✅	5s	2s	+150%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	5s	3s	+67%
`mlk_polyvec_reduce`	✅	5s	2s	+150%
`mlk_shake128x4_absorb_once`	✅	5s	2s	+150%
`nttunpack_native_x86_64`	✅	5s	3s	+67%
`poly_decompress_d10_native_x86_64`	✅	5s	4s	+25%
`poly_decompress_d4_native_x86_64`	✅	5s	3s	+67%
`poly_frombytes_native_x86_64`	✅	5s	4s	+25%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	✅	5s	1s	+400%
`rej_uniform_native`	✅	5s	3s	+67%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	4s	2s	+100%
`keccakf1600x4_xor_bytes_native`	✅	4s	2s	+100%
`kem_check_pk`	✅	4s	3s	+33%
`mlk_ct_cmask_nonzero_u16`	✅	4s	3s	+33%
`mlk_ct_get_optblocker_u8`	✅	4s	4s	+0%
`mlk_keccak_absorb_once`	✅	4s	5s	-20%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	4s	2s	+100%
`mlk_poly_cbd_eta2`	✅	4s	3s	+33%
`mlk_poly_compress_d11_native`	✅	4s	-	new
`mlk_poly_compress_d5_c`	✅	4s	-	new
`mlk_poly_decompress_d4_c`	✅	4s	3s	+33%
`mlk_poly_getnoise_eta1_4x`	✅	4s	3s	+33%
`mlk_poly_getnoise_eta1_4x_native`	✅	4s	3s	+33%
`mlk_poly_mulcache_compute`	✅	4s	3s	+33%
`mlk_poly_mulcache_compute_native`	✅	4s	2s	+100%
`mlk_poly_reduce_c`	✅	4s	4s	+0%
`mlk_poly_tobytes`	✅	4s	3s	+33%
`mlk_polyvec_frombytes`	✅	4s	1s	+300%
`mlk_polyvec_invntt_tomont`	✅	4s	2s	+100%
`mlk_polyvec_permute_bitrev_to_custom`	✅	4s	3s	+33%
`poly_decompress_d11_native_x86_64`	✅	4s	1s	+300%
`poly_invntt_tomont_native`	✅	4s	3s	+33%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	✅	4s	3s	+33%
`intt_native_aarch64`	✅	3s	4s	-25%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	2s	+50%
`kem_keypair_derand`	✅	3s	3s	+0%
`mlk_barrett_reduce`	✅	3s	2s	+50%
`mlk_check_pct`	✅	3s	2s	+50%
`mlk_ct_cmask_neg_i16`	✅	3s	2s	+50%
`mlk_ct_get_optblocker_i32`	✅	3s	4s	-25%
`mlk_keccakf1600_extract_bytes`	✅	3s	3s	+0%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	3s	3s	+0%
`mlk_montgomery_reduce`	✅	3s	1s	+200%
`mlk_poly_add`	✅	3s	3s	+0%
`mlk_poly_cbd_eta1`	✅	3s	2s	+50%
`mlk_poly_compress_d11`	✅	3s	-	new
`mlk_poly_compress_d4_c`	✅	3s	-	new
`mlk_poly_compress_d4_native`	✅	3s	-	new
`mlk_poly_decompress_d10`	✅	3s	1s	+200%
`mlk_poly_decompress_d11_native`	✅	3s	1s	+200%
`mlk_poly_decompress_d5_native`	✅	3s	2s	+50%
`mlk_poly_decompress_dv`	✅	3s	2s	+50%
`mlk_poly_frombytes`	✅	3s	2s	+50%
`mlk_poly_ntt`	✅	3s	4s	-25%
`mlk_poly_ntt_c`	✅	3s	2s	+50%
`mlk_poly_reduce`	✅	3s	1s	+200%
`mlk_poly_tobytes_native`	✅	3s	2s	+50%
`mlk_poly_tomont_native`	✅	3s	6s	-50%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	3s	2s	+50%
`mlk_polyvec_mulcache_compute`	✅	3s	1s	+200%
`mlk_rej_uniform`	✅	3s	2s	+50%
`mlk_scalar_compress_d10`	✅	3s	2s	+50%
`mlk_scalar_compress_d11`	✅	3s	3s	+0%
`mlk_scalar_decompress_d11`	✅	3s	2s	+50%
`mlk_scalar_decompress_d5`	✅	3s	2s	+50%
`mlk_sha3_256`	✅	3s	1s	+200%
`mlk_sha3_512`	✅	3s	3s	+0%
`mlk_value_barrier_i32`	✅	3s	3s	+0%
`mlk_value_barrier_u8`	✅	3s	3s	+0%
`poly_compress_d11_native_x86_64`	✅	3s	-	new
`poly_compress_d4_native_x86_64`	✅	3s	-	new
`poly_compress_d5_native_x86_64`	✅	3s	-	new
`poly_mulcache_compute_native_aarch64`	✅	3s	3s	+0%
`poly_mulcache_compute_native_x86_64`	✅	3s	2s	+50%
`poly_reduce_native_aarch64`	✅	3s	2s	+50%
`poly_tobytes_native_aarch64`	✅	3s	4s	-25%
`poly_tomont_native_aarch64`	✅	3s	2s	+50%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	✅	3s	2s	+50%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	3s	2s	+50%
`sys_check_capability`	✅	3s	3s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	✅	2s	2s	+0%
`kem_check_sk`	✅	2s	4s	-50%
`kem_enc`	✅	2s	2s	+0%
`kem_enc_derand`	✅	2s	2s	+0%
`kem_keypair`	✅	2s	3s	-33%
`mlk_ct_cmask_nonzero_u8`	✅	2s	1s	+100%
`mlk_ct_cmov_zero`	✅	2s	3s	-33%
`mlk_ct_get_optblocker_u32`	✅	2s	1s	+100%
`mlk_ct_sel_int16`	✅	2s	2s	+0%
`mlk_keccakf1600x4_extract_bytes`	✅	2s	1s	+100%
`mlk_keccakf1600x4_permute`	✅	2s	2s	+0%
`mlk_keccakf1600x4_xor_bytes`	✅	2s	2s	+0%
`mlk_matvec_mul`	✅	2s	2s	+0%
`mlk_poly_compress_d11_c`	✅	2s	-	new
`mlk_poly_compress_d4`	✅	2s	-	new
`mlk_poly_compress_d5`	✅	2s	-	new
`mlk_poly_compress_d5_native`	✅	2s	-	new
`mlk_poly_compress_du`	✅	2s	2s	+0%
`mlk_poly_decompress_d10_c`	✅	2s	2s	+0%
`mlk_poly_decompress_d11`	✅	2s	2s	+0%
`mlk_poly_decompress_d11_c`	✅	2s	3s	-33%
`mlk_poly_decompress_d4`	✅	2s	3s	-33%
`mlk_poly_decompress_d5`	✅	2s	2s	+0%
`mlk_poly_decompress_d5_c`	✅	2s	1s	+100%
`mlk_poly_decompress_du`	✅	2s	3s	-33%
`mlk_poly_getnoise_eta1122_4x`	✅	2s	2s	+0%
`mlk_poly_getnoise_eta2`	✅	2s	3s	-33%
`mlk_poly_invntt_tomont`	✅	2s	2s	+0%
`mlk_poly_invntt_tomont_c`	✅	2s	2s	+0%
`mlk_poly_tobytes_c`	✅	2s	2s	+0%
`mlk_poly_tomont`	✅	2s	2s	+0%
`mlk_poly_tomont_c`	✅	2s	3s	-33%
`mlk_polyvec_compress_du`	✅	2s	3s	-33%
`mlk_polyvec_decompress_du`	✅	2s	3s	-33%
`mlk_polyvec_ntt`	✅	2s	2s	+0%
`mlk_polyvec_tobytes`	✅	2s	2s	+0%
`mlk_scalar_compress_d4`	✅	2s	2s	+0%
`mlk_scalar_compress_d5`	✅	2s	3s	-33%
`mlk_scalar_decompress_d10`	✅	2s	1s	+100%
`mlk_scalar_signed_to_unsigned_q`	✅	2s	1s	+100%
`mlk_shake128_absorb_once`	✅	2s	3s	-33%
`mlk_shake128_squeezeblocks`	✅	2s	2s	+0%
`mlk_shake128x4_squeezeblocks`	✅	2s	3s	-33%
`mlk_shake256`	✅	2s	2s	+0%
`mlk_value_barrier_u32`	✅	2s	3s	-33%
`ntt_native_aarch64`	✅	2s	2s	+0%
`poly_compress_d10_native_x86_64`	✅	2s	-	new
`poly_decompress_d5_native_x86_64`	✅	2s	2s	+0%
`poly_getnoise_eta1122_4x_native`	✅	2s	2s	+0%
`poly_reduce_native_x86_64`	✅	2s	2s	+0%
`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	3s	-33%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	2s	4s	-50%
`rej_uniform_native_aarch64`	✅	2s	2s	+0%
`rej_uniform_native_x86_64`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	1s	1s	+0%
`mlk_ct_memcmp`	✅	1s	2s	-50%
`mlk_poly_compress_d10`	✅	1s	-	new
`mlk_poly_compress_dv`	✅	1s	2s	-50%
`mlk_poly_frombytes_c`	✅	1s	2s	-50%
`mlk_scalar_compress_d1`	✅	1s	2s	-50%
`mlk_scalar_decompress_d4`	✅	1s	1s	+0%
`ntt_native_x86_64`	✅	1s	3s	-67%

oqs-bot · 2026-02-06T05:09:44Z

CBMC Results (ML-KEM-1024)

Full Results (185 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2742s	2706s	+1.3%
`mlk_indcpa_enc`	✅	1321s	1336s	-1%
`mlk_indcpa_keypair_derand`	✅	210s	224s	-6%
`mlk_keccak_squeezeblocks_x4`	✅	181s	162s	+12%
`polyvec_basemul_acc_montgomery_cached_native`	✅	121s	127s	-5%
`mlk_rej_uniform_c`	✅	96s	89s	+8%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	✅	64s	67s	-4%
`poly_ntt_native`	✅	53s	38s	+39%
`mlk_poly_rej_uniform`	✅	34s	37s	-8%
`mlk_ntt_layer`	✅	24s	24s	+0%
`mlk_indcpa_dec`	✅	20s	19s	+5%
`keccakf1600x4_permute_native_x4`	✅	18s	22s	-18%
`mlk_poly_decompress_d11_native`	✅	18s	13s	+38%
`mlk_poly_reduce_native`	✅	16s	14s	+14%
`mlk_poly_decompress_d5_native`	✅	14s	15s	-7%
`mlk_polyvec_ntt`	✅	14s	14s	+0%
`mlk_ntt_butterfly_block`	✅	13s	9s	+44%
`mlk_polyvec_add`	✅	11s	12s	-8%
`mlk_keccak_absorb_once_x4`	✅	10s	13s	-23%
`mlk_poly_sub`	✅	10s	12s	-17%
`mlk_poly_frombytes_native`	✅	9s	8s	+12%
`mlk_poly_rej_uniform_x4`	✅	9s	7s	+29%
`kem_dec`	✅	7s	8s	-12%
`mlk_fqmul`	✅	7s	8s	-12%
`mlk_gen_matrix`	✅	7s	9s	-22%
`mlk_gen_matrix_serial`	✅	7s	4s	+75%
`mlk_keccak_squeezeblocks`	✅	7s	7s	+0%
`mlk_poly_frommsg`	✅	7s	10s	-30%
`mlk_invntt_layer`	✅	6s	9s	-33%
`mlk_keccak_squeeze_once`	✅	6s	7s	-14%
`mlk_poly_compress_d11_c`	✅	6s	-	new
`nttunpack_native_x86_64`	✅	6s	2s	+200%
`kem_check_pk`	✅	5s	6s	-17%
`mlk_ct_get_optblocker_i32`	✅	5s	2s	+150%
`mlk_poly_compress_dv`	✅	5s	2s	+150%
`mlk_poly_getnoise_eta1122_4x`	✅	5s	5s	+0%
`mlk_poly_mulcache_compute_c`	✅	5s	2s	+150%
`mlk_polymat_permute_bitrev_to_custom`	✅	5s	6s	-17%
`mlk_polyvec_permute_bitrev_to_custom`	✅	5s	1s	+400%
`mlk_sha3_512`	✅	5s	2s	+150%
`ntt_native_aarch64`	✅	5s	2s	+150%
`poly_frombytes_native_x86_64`	✅	5s	7s	-29%
`poly_mulcache_compute_native_aarch64`	✅	5s	4s	+25%
`keccak_f1600_x4_native_aarch64_v84a`	✅	4s	3s	+33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	4s	2s	+100%
`keccakf1600_permute_native`	✅	4s	6s	-33%
`keccakf1600x4_extract_bytes_native`	✅	4s	3s	+33%
`kem_enc`	✅	4s	3s	+33%
`kem_keypair`	✅	4s	3s	+33%
`kem_keypair_derand`	✅	4s	2s	+100%
`mlk_keccak_absorb_once`	✅	4s	6s	-33%
`mlk_poly_add`	✅	4s	2s	+100%
`mlk_poly_compress_d11_native`	✅	4s	-	new
`mlk_poly_compress_d4_native`	✅	4s	-	new
`mlk_poly_compress_d5_c`	✅	4s	-	new
`mlk_poly_decompress_d11_c`	✅	4s	2s	+100%
`mlk_poly_decompress_d4_native`	✅	4s	3s	+33%
`mlk_poly_getnoise_eta1_4x_native`	✅	4s	3s	+33%
`mlk_poly_mulcache_compute`	✅	4s	3s	+33%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	4s	4s	+0%
`mlk_scalar_decompress_d5`	✅	4s	3s	+33%
`mlk_shake128x4_absorb_once`	✅	4s	3s	+33%
`mlk_shake256x4`	✅	4s	7s	-43%
`mlk_value_barrier_u8`	✅	4s	3s	+33%
`poly_decompress_d11_native_x86_64`	✅	4s	5s	-20%
`poly_decompress_d5_native_x86_64`	✅	4s	4s	+0%
`poly_reduce_native_aarch64`	✅	4s	5s	-20%
`poly_reduce_native_x86_64`	✅	4s	2s	+100%
`poly_tobytes_native_aarch64`	✅	4s	4s	+0%
`intt_native_x86_64`	✅	3s	4s	-25%
`keccakf1600x4_xor_bytes_native`	✅	3s	3s	+0%
`kem_enc_derand`	✅	3s	5s	-40%
`mlk_check_pct`	✅	3s	3s	+0%
`mlk_ct_get_optblocker_u32`	✅	3s	1s	+200%
`mlk_ct_memcmp`	✅	3s	3s	+0%
`mlk_keccakf1600_permute`	✅	3s	3s	+0%
`mlk_keccakf1600x4_permute`	✅	3s	2s	+50%
`mlk_matvec_mul`	✅	3s	3s	+0%
`mlk_poly_cbd_eta2`	✅	3s	3s	+0%
`mlk_poly_compress_d10`	✅	3s	-	new
`mlk_poly_compress_d10_native`	✅	3s	-	new
`mlk_poly_compress_d4_c`	✅	3s	-	new
`mlk_poly_compress_d5`	✅	3s	-	new
`mlk_poly_decompress_d10_c`	✅	3s	2s	+50%
`mlk_poly_decompress_d4`	✅	3s	1s	+200%
`mlk_poly_frombytes_c`	✅	3s	3s	+0%
`mlk_poly_ntt_c`	✅	3s	2s	+50%
`mlk_poly_tobytes`	✅	3s	4s	-25%
`mlk_poly_tobytes_c`	✅	3s	4s	-25%
`mlk_poly_tomont`	✅	3s	2s	+50%
`mlk_poly_tomsg`	✅	3s	2s	+50%
`mlk_polyvec_compress_du`	✅	3s	2s	+50%
`mlk_polyvec_invntt_tomont`	✅	3s	4s	-25%
`mlk_polyvec_mulcache_compute`	✅	3s	2s	+50%
`mlk_polyvec_tomont`	✅	3s	3s	+0%
`mlk_scalar_compress_d11`	✅	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_shake128_absorb_once`	✅	3s	1s	+200%
`mlk_shake128x4_squeezeblocks`	✅	3s	4s	-25%
`mlk_shake256`	✅	3s	1s	+200%
`poly_compress_d4_native_x86_64`	✅	3s	-	new
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	3s	4s	-25%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	3s	4s	-25%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	✅	3s	2s	+50%
`rej_uniform_native`	✅	3s	4s	-25%
`rej_uniform_native_aarch64`	✅	3s	2s	+50%
`rej_uniform_native_x86_64`	✅	3s	2s	+50%
`intt_native_aarch64`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	2s	+0%
`kem_check_sk`	✅	2s	3s	-33%
`mlk_ct_cmask_neg_i16`	✅	2s	3s	-33%
`mlk_ct_cmask_nonzero_u16`	✅	2s	2s	+0%
`mlk_ct_cmask_nonzero_u8`	✅	2s	2s	+0%
`mlk_ct_get_optblocker_u8`	✅	2s	1s	+100%
`mlk_keccakf1600_extract_bytes`	✅	2s	1s	+100%
`mlk_keccakf1600_xor_bytes`	✅	2s	3s	-33%
`mlk_keccakf1600x4_extract_bytes`	✅	2s	1s	+100%
`mlk_keccakf1600x4_xor_bytes`	✅	2s	3s	-33%
`mlk_poly_cbd_eta1`	✅	2s	3s	-33%
`mlk_poly_compress_d10_c`	✅	2s	-	new
`mlk_poly_compress_d4`	✅	2s	-	new
`mlk_poly_compress_d5_native`	✅	2s	-	new
`mlk_poly_compress_du`	✅	2s	5s	-60%
`mlk_poly_decompress_d10`	✅	2s	3s	-33%
`mlk_poly_decompress_d11`	✅	2s	2s	+0%
`mlk_poly_decompress_d4_c`	✅	2s	1s	+100%
`mlk_poly_decompress_d5_c`	✅	2s	2s	+0%
`mlk_poly_decompress_du`	✅	2s	3s	-33%
`mlk_poly_decompress_dv`	✅	2s	4s	-50%
`mlk_poly_frombytes`	✅	2s	2s	+0%
`mlk_poly_getnoise_eta1_4x`	✅	2s	3s	-33%
`mlk_poly_getnoise_eta2`	✅	2s	3s	-33%
`mlk_poly_invntt_tomont_c`	✅	2s	1s	+100%
`mlk_poly_mulcache_compute_native`	✅	2s	2s	+0%
`mlk_poly_ntt`	✅	2s	3s	-33%
`mlk_poly_reduce`	✅	2s	2s	+0%
`mlk_poly_reduce_c`	✅	2s	3s	-33%
`mlk_poly_tobytes_native`	✅	2s	3s	-33%
`mlk_poly_tomont_native`	✅	2s	3s	-33%
`mlk_polyvec_reduce`	✅	2s	5s	-60%
`mlk_scalar_compress_d1`	✅	2s	2s	+0%
`mlk_scalar_compress_d10`	✅	2s	2s	+0%
`mlk_scalar_compress_d5`	✅	2s	3s	-33%
`mlk_scalar_signed_to_unsigned_q`	✅	2s	3s	-33%
`mlk_sha3_256`	✅	2s	1s	+100%
`mlk_shake128_squeezeblocks`	✅	2s	3s	-33%
`mlk_value_barrier_i32`	✅	2s	1s	+100%
`ntt_native_x86_64`	✅	2s	3s	-33%
`poly_compress_d11_native_x86_64`	✅	2s	-	new
`poly_compress_d5_native_x86_64`	✅	2s	-	new
`poly_decompress_d10_native_x86_64`	✅	2s	2s	+0%
`poly_invntt_tomont_native`	✅	2s	1s	+100%
`poly_mulcache_compute_native_x86_64`	✅	2s	2s	+0%
`poly_tobytes_native_x86_64`	✅	2s	3s	-33%
`poly_tomont_native_aarch64`	✅	2s	2s	+0%
`poly_tomont_native_x86_64`	✅	2s	1s	+100%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	✅	2s	4s	-50%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	2s	2s	+0%
`sys_check_capability`	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64`	✅	1s	3s	-67%
`mlk_barrett_reduce`	✅	1s	2s	-50%
`mlk_ct_cmov_zero`	✅	1s	2s	-50%
`mlk_ct_sel_int16`	✅	1s	2s	-50%
`mlk_ct_sel_uint8`	✅	1s	3s	-67%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	1s	1s	+0%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	1s	1s	+0%
`mlk_montgomery_reduce`	✅	1s	2s	-50%
`mlk_poly_compress_d11`	✅	1s	-	new
`mlk_poly_decompress_d10_native`	✅	1s	2s	-50%
`mlk_poly_decompress_d5`	✅	1s	1s	+0%
`mlk_poly_invntt_tomont`	✅	1s	2s	-50%
`mlk_poly_tomont_c`	✅	1s	2s	-50%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	1s	1s	+0%
`mlk_polyvec_decompress_du`	✅	1s	3s	-67%
`mlk_polyvec_frombytes`	✅	1s	3s	-67%
`mlk_polyvec_tobytes`	✅	1s	2s	-50%
`mlk_rej_uniform`	✅	1s	2s	-50%
`mlk_scalar_decompress_d4`	✅	1s	3s	-67%
`mlk_value_barrier_u32`	✅	1s	4s	-75%
`poly_compress_d10_native_x86_64`	✅	1s	-	new
`poly_decompress_d4_native_x86_64`	✅	1s	4s	-75%
`poly_getnoise_eta1122_4x_native`	✅	1s	3s	-67%

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

…sembly Replace the C intrinsics implementation of the four x86_64 AVX2 poly_compress functions with handwritten assembly, enabling verification in HOL Light. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

Add functional correctness proofs for the four x86_64 AVX2 poly_compress functions. Each proof verifies the assembly against the compress_d specification from FIPS 203. Co-authored-by: Hanno Becker <beckphan@amazon.co.uk> Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Add subroutine-level constant-time proofs for poly_compress_d{4,5,10,11}. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

All x86_64 ML-KEM arithmetic intrinsics have been rewritten in assembly and verified, so update the verification claims accordingly. Note that the x86_64 FIPS-202 (Keccak) backend remains in C intrinsics and is not yet covered by proof. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

hanno-becker

Nice teamwork 😃 LGTM.

mkannwischer changed the title ~~WIP: HOL Light: Add proof skeleton for poly_compress_d{4,5,10,11}~~ WIP: HOL Light: Prove correctness of AVX2 poly_compress_d{4,5,10,11} Feb 5, 2026

hanno-becker reviewed Feb 5, 2026

View reviewed changes

Comment thread dev/x86_64/src/poly_compress_d11.S Outdated

mkannwischer force-pushed the prove-compress branch from e6c882e to 3656b1a Compare February 6, 2026 04:12

mkannwischer added the benchmark this PR should be benchmarked in CI label Feb 6, 2026

oqs-bot reviewed Feb 6, 2026

View reviewed changes

hanno-becker removed the benchmark this PR should be benchmarked in CI label Feb 7, 2026

mkannwischer force-pushed the prove-compress branch 2 times, most recently from 3e666b0 to e67fb4b Compare February 16, 2026 12:45

hanno-becker force-pushed the prove-compress branch from e67fb4b to c6fd37e Compare February 16, 2026 13:47

hanno-becker changed the title ~~WIP: HOL Light: Prove correctness of AVX2 poly_compress_d{4,5,10,11}~~ HOL Light: Prove correctness of AVX2 poly_compress_d{4,5,10,11} Feb 17, 2026

hanno-becker marked this pull request as ready for review February 17, 2026 03:57

hanno-becker requested a review from a team as a code owner February 17, 2026 03:57

mkannwischer mentioned this pull request Feb 18, 2026

Discussion: Release schedule #1519

Open

mkannwischer force-pushed the prove-compress branch from c6fd37e to 56b827d Compare February 25, 2026 08:42

mkannwischer mentioned this pull request Feb 25, 2026

Format: Don't allow tabs #1573

Merged

mkannwischer force-pushed the prove-compress branch from 56b827d to 7d9af85 Compare February 26, 2026 10:38

mkannwischer added benchmark this PR should be benchmarked in CI and removed benchmark this PR should be benchmarked in CI labels Feb 26, 2026

mkannwischer commented Feb 26, 2026

View reviewed changes

Comment thread README.md Outdated

mkannwischer force-pushed the prove-compress branch from 5511a29 to 10d1f9c Compare February 27, 2026 06:41

mkannwischer added the DO-NOT-MERGE label Feb 27, 2026

mkannwischer force-pushed the prove-compress branch 2 times, most recently from b44f1b7 to 3736083 Compare February 27, 2026 08:07

mkannwischer removed the DO-NOT-MERGE label Feb 27, 2026

hanno-becker reviewed Feb 27, 2026

View reviewed changes

Comment thread nix/hol_light/default.nix Outdated

mkannwischer and others added 6 commits February 27, 2026 19:45

nix: Update HOL Light and s2n-bignum

bbcdf0e

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

CBMC/x86_64: Add specs and proofs for compression routines

ea2be98

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

HOL-Light/x86_64: Add constant-time proofs for compression functions

2320d34

Add subroutine-level constant-time proofs for poly_compress_d{4,5,10,11}. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

mkannwischer force-pushed the prove-compress branch from 3736083 to 602e37e Compare February 27, 2026 11:46

hanno-becker approved these changes Feb 27, 2026

View reviewed changes

mkannwischer merged commit 474660e into main Feb 27, 2026
413 checks passed

mkannwischer deleted the prove-compress branch February 27, 2026 14:08

mkannwischer mentioned this pull request Mar 14, 2026

Update mlkem-native to v1.1.0 open-quantum-safe/liboqs#2376

Merged

Conversation

mkannwischer commented Feb 4, 2026

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

ppc64le (POWER10) 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

Arm Cortex-A76 (Raspberry Pi 5) benchmarks

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

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

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

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

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

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

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

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

Graviton3

Uh oh!

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

Uh oh!

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 left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot commented Feb 6, 2026 •

edited

Loading

oqs-bot commented Feb 6, 2026 •

edited

Loading

oqs-bot commented Feb 6, 2026 •

edited

Loading