[POC] Bench: Add Dabao (Baochip-1x) benchmarks by mkannwischer · Pull Request #1448 · pq-code-package/mldsa-native

mkannwischer · 2026-09-27T08:39:39Z

Add a test platform for the Dabao board (Baochip-1x, RV32IMAC at 350 MHz) and run the benchmarks on it in CI.

Test binaries are built with a soft-float RV32IMAC newlib toolchain (new .#dabao dev shell) and linked into the xous-core baremetal image, which provides the USB serial console. link.py builds and signs that image with a pinned, patched xous-core; exec_wrapper.py flashes it through the boot1 console, runs the test and reports its exit code.

Warning

Nowhere near ready to be merged.

Add a test platform for the Dabao board (Baochip-1x, RV32IMAC at 350 MHz) and run the benchmarks on it in CI. Test binaries are built with a soft-float RV32IMAC newlib toolchain (new `.#dabao` dev shell) and linked into the xous-core `baremetal` image, which provides the USB serial console. link.py builds and signs that image with a pinned, patched xous-core; exec_wrapper.py flashes it through the boot1 console, runs the test and reports its exit code. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

github-actions

Mac Mini (M1, 2020) benchmarks (opt)

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`46491` cycles	`46494` cycles	`1.00`
`ML-DSA-44 sign`	`131379` cycles	`131434` cycles	`1.00`
`ML-DSA-44 verify`	`47328` cycles	`47376` cycles	`1.00`
`ML-DSA-65 keypair`	`81700` cycles	`81719` cycles	`1.00`
`ML-DSA-65 sign`	`215297` cycles	`215302` cycles	`1.00`
`ML-DSA-65 verify`	`79317` cycles	`79322` cycles	`1.00`
`ML-DSA-87 keypair`	`132366` cycles	`132372` cycles	`1.00`
`ML-DSA-87 sign`	`277449` cycles	`277416` cycles	`1.00`
`ML-DSA-87 verify`	`137025` cycles	`136996` cycles	`1.00`

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

github-actions

Mac Mini (M1, 2020) benchmarks (no-opt)

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`113520` cycles	`112841` cycles	`1.01`
`ML-DSA-44 sign`	`405441` cycles	`402663` cycles	`1.01`
`ML-DSA-44 verify`	`120169` cycles	`119436` cycles	`1.01`
`ML-DSA-65 keypair`	`193745` cycles	`193013` cycles	`1.00`
`ML-DSA-65 sign`	`654209` cycles	`651616` cycles	`1.00`
`ML-DSA-65 verify`	`193705` cycles	`192988` cycles	`1.00`
`ML-DSA-87 keypair`	`318890` cycles	`318884` cycles	`1.00`
`ML-DSA-87 sign`	`831198` cycles	`831107` cycles	`1.00`
`ML-DSA-87 verify`	`325785` cycles	`325770` cycles	`1.00`

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

github-actions

Arm Cortex-A76 (Raspberry Pi 5) benchmarks (opt)

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`112268` cycles	`112281` cycles	`1.00`
`ML-DSA-44 sign`	`354108` cycles	`354075` cycles	`1.00`
`ML-DSA-44 verify`	`117045` cycles	`117165` cycles	`1.00`
`ML-DSA-65 keypair`	`194692` cycles	`194672` cycles	`1.00`
`ML-DSA-65 sign`	`583444` cycles	`583313` cycles	`1.00`
`ML-DSA-65 verify`	`192940` cycles	`193133` cycles	`1.00`
`ML-DSA-87 keypair`	`320562` cycles	`321007` cycles	`1.00`
`ML-DSA-87 sign`	`747067` cycles	`747555` cycles	`1.00`
`ML-DSA-87 verify`	`318257` cycles	`318676` cycles	`1.00`

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

github-actions

Arm Cortex-A76 (Raspberry Pi 5) benchmarks (no-opt)

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`211931` cycles	`212004` cycles	`1.00`
`ML-DSA-44 sign`	`760430` cycles	`760098` cycles	`1.00`
`ML-DSA-44 verify`	`229710` cycles	`229440` cycles	`1.00`
`ML-DSA-65 keypair`	`375838` cycles	`376081` cycles	`1.00`
`ML-DSA-65 sign`	`1245711` cycles	`1245097` cycles	`1.00`
`ML-DSA-65 verify`	`371812` cycles	`371792` cycles	`1.00`
`ML-DSA-87 keypair`	`601673` cycles	`601811` cycles	`1.00`
`ML-DSA-87 sign`	`1585077` cycles	`1583956` cycles	`1.00`
`ML-DSA-87 verify`	`617440` cycles	`617448` cycles	`1.00`

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

github-actions

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`218382` cycles	`215465` cycles	`1.01`
`ML-DSA-44 sign`	`600412` cycles	`599960` cycles	`1.00`
`ML-DSA-44 verify`	`215741` cycles	`215886` cycles	`1.00`
`ML-DSA-65 keypair`	`383044` cycles	`380665` cycles	`1.01`
`ML-DSA-65 sign`	`991660` cycles	`995589` cycles	`1.00`
`ML-DSA-65 verify`	`367305` cycles	`365798` cycles	`1.00`
`ML-DSA-87 keypair`	`646829` cycles	`642746` cycles	`1.01`
`ML-DSA-87 sign`	`1329897` cycles	`1328306` cycles	`1.00`
`ML-DSA-87 verify`	`628922` cycles	`623047` cycles	`1.01`

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

oqs-bot

Intel Xeon 4th gen (c7i)

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`43340` cycles	`43335` cycles	`1.00`
`ML-DSA-44 sign`	`130247` cycles	`130054` cycles	`1.00`
`ML-DSA-44 verify`	`45253` cycles	`45274` cycles	`1.00`
`ML-DSA-65 keypair`	`75857` cycles	`76106` cycles	`1.00`
`ML-DSA-65 sign`	`213779` cycles	`213867` cycles	`1.00`
`ML-DSA-65 verify`	`74904` cycles	`74645` cycles	`1.00`
`ML-DSA-87 keypair`	`123505` cycles	`123276` cycles	`1.00`
`ML-DSA-87 sign`	`270748` cycles	`270714` cycles	`1.00`
`ML-DSA-87 verify`	`120734` cycles	`120652` 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: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`92178` cycles	`92092` cycles	`1.00`
`ML-DSA-44 sign`	`348951` cycles	`348083` cycles	`1.00`
`ML-DSA-44 verify`	`99497` cycles	`99491` cycles	`1.00`
`ML-DSA-65 keypair`	`154055` cycles	`154151` cycles	`1.00`
`ML-DSA-65 sign`	`564933` cycles	`565525` cycles	`1.00`
`ML-DSA-65 verify`	`159268` cycles	`159287` cycles	`1.00`
`ML-DSA-87 keypair`	`255997` cycles	`255425` cycles	`1.00`
`ML-DSA-87 sign`	`724691` cycles	`724512` cycles	`1.00`
`ML-DSA-87 verify`	`264060` cycles	`263806` 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: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`47641` cycles	`47153` cycles	`1.01`
`ML-DSA-44 sign`	`139565` cycles	`140214` cycles	`1.00`
`ML-DSA-44 verify`	`49662` cycles	`50124` cycles	`0.99`
`ML-DSA-65 keypair`	`81945` cycles	`82197` cycles	`1.00`
`ML-DSA-65 sign`	`228505` cycles	`229690` cycles	`0.99`
`ML-DSA-65 verify`	`82565` cycles	`84336` cycles	`0.98`
`ML-DSA-87 keypair`	`130664` cycles	`130415` cycles	`1.00`
`ML-DSA-87 sign`	`280357` cycles	`280238` cycles	`1.00`
`ML-DSA-87 verify`	`128424` cycles	`128337` cycles	`1.00`

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

oqs-bot

Graviton5

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`51447` cycles	`51544` cycles	`1.00`
`ML-DSA-44 sign`	`162190` cycles	`162240` cycles	`1.00`
`ML-DSA-44 verify`	`54804` cycles	`54695` cycles	`1.00`
`ML-DSA-65 keypair`	`90193` cycles	`90158` cycles	`1.00`
`ML-DSA-65 sign`	`266245` cycles	`266210` cycles	`1.00`
`ML-DSA-65 verify`	`89984` cycles	`89808` cycles	`1.00`
`ML-DSA-87 keypair`	`145990` cycles	`145901` cycles	`1.00`
`ML-DSA-87 sign`	`334511` cycles	`335555` cycles	`1.00`
`ML-DSA-87 verify`	`144887` cycles	`145479` cycles	`1.00`

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

oqs-bot

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

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`118934` cycles	`119113` cycles	`1.00`
`ML-DSA-44 sign`	`458308` cycles	`459803` cycles	`1.00`
`ML-DSA-44 verify`	`131602` cycles	`131354` cycles	`1.00`
`ML-DSA-65 keypair`	`201101` cycles	`201239` cycles	`1.00`
`ML-DSA-65 sign`	`747563` cycles	`742008` cycles	`1.01`
`ML-DSA-65 verify`	`210192` cycles	`210141` cycles	`1.00`
`ML-DSA-87 keypair`	`331258` cycles	`332735` cycles	`1.00`
`ML-DSA-87 sign`	`941447` cycles	`943014` cycles	`1.00`
`ML-DSA-87 verify`	`344794` cycles	`346024` 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: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`52235` cycles	`52012` cycles	`1.00`
`ML-DSA-44 sign`	`156653` cycles	`155876` cycles	`1.00`
`ML-DSA-44 verify`	`54462` cycles	`54350` cycles	`1.00`
`ML-DSA-65 keypair`	`89985` cycles	`89686` cycles	`1.00`
`ML-DSA-65 sign`	`253797` cycles	`253118` cycles	`1.00`
`ML-DSA-65 verify`	`90323` cycles	`89910` cycles	`1.00`
`ML-DSA-87 keypair`	`143615` cycles	`143380` cycles	`1.00`
`ML-DSA-87 sign`	`310837` cycles	`309922` cycles	`1.00`
`ML-DSA-87 verify`	`138829` cycles	`138722` cycles	`1.00`

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

oqs-bot

Graviton5 (no-opt)

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`100210` cycles	`99994` cycles	`1.00`
`ML-DSA-44 sign`	`369798` cycles	`369411` cycles	`1.00`
`ML-DSA-44 verify`	`110532` cycles	`110169` cycles	`1.00`
`ML-DSA-65 keypair`	`175570` cycles	`176078` cycles	`1.00`
`ML-DSA-65 sign`	`595149` cycles	`596508` cycles	`1.00`
`ML-DSA-65 verify`	`177598` cycles	`177442` cycles	`1.00`
`ML-DSA-87 keypair`	`285023` cycles	`286625` cycles	`0.99`
`ML-DSA-87 sign`	`757785` cycles	`757839` cycles	`1.00`
`ML-DSA-87 verify`	`296702` cycles	`295774` 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: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`133760` cycles	`133339` cycles	`1.00`
`ML-DSA-44 sign`	`521437` cycles	`519956` cycles	`1.00`
`ML-DSA-44 verify`	`147050` cycles	`146742` cycles	`1.00`
`ML-DSA-65 keypair`	`224336` cycles	`224146` cycles	`1.00`
`ML-DSA-65 sign`	`848581` cycles	`847357` cycles	`1.00`
`ML-DSA-65 verify`	`235579` cycles	`234420` cycles	`1.00`
`ML-DSA-87 keypair`	`369081` cycles	`367973` cycles	`1.00`
`ML-DSA-87 sign`	`1065583` cycles	`1064638` cycles	`1.00`
`ML-DSA-87 verify`	`382215` cycles	`381485` 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: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`61780` cycles	`61663` cycles	`1.00`
`ML-DSA-44 sign`	`188687` cycles	`188790` cycles	`1.00`
`ML-DSA-44 verify`	`66126` cycles	`66187` cycles	`1.00`
`ML-DSA-65 keypair`	`108095` cycles	`108346` cycles	`1.00`
`ML-DSA-65 sign`	`311306` cycles	`311940` cycles	`1.00`
`ML-DSA-65 verify`	`108586` cycles	`109108` cycles	`1.00`
`ML-DSA-87 keypair`	`170515` cycles	`172400` cycles	`0.99`
`ML-DSA-87 sign`	`378902` cycles	`383035` cycles	`0.99`
`ML-DSA-87 verify`	`170152` cycles	`171307` cycles	`0.99`

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

github-actions

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`300040` cycles	`299209` cycles	`1.00`
`ML-DSA-44 sign`	`1132984` cycles	`1128871` cycles	`1.00`
`ML-DSA-44 verify`	`330605` cycles	`329148` cycles	`1.00`
`ML-DSA-65 keypair`	`549720` cycles	`546676` cycles	`1.01`
`ML-DSA-65 sign`	`1868692` cycles	`1860299` cycles	`1.00`
`ML-DSA-65 verify`	`530524` cycles	`527863` cycles	`1.01`
`ML-DSA-87 keypair`	`851734` cycles	`848296` cycles	`1.00`
`ML-DSA-87 sign`	`2376484` cycles	`2384110` cycles	`1.00`
`ML-DSA-87 verify`	`880414` cycles	`879177` 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: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`153848` cycles	`156139` cycles	`0.99`
`ML-DSA-44 sign`	`588313` cycles	`594995` cycles	`0.99`
`ML-DSA-44 verify`	`169080` cycles	`171509` cycles	`0.99`
`ML-DSA-65 keypair`	`262325` cycles	`262241` cycles	`1.00`
`ML-DSA-65 sign`	`958413` cycles	`964309` cycles	`0.99`
`ML-DSA-65 verify`	`271882` cycles	`272016` cycles	`1.00`
`ML-DSA-87 keypair`	`431233` cycles	`432829` cycles	`1.00`
`ML-DSA-87 sign`	`1210420` cycles	`1213001` cycles	`1.00`
`ML-DSA-87 verify`	`446721` cycles	`447738` cycles	`1.00`

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

oqs-bot

Graviton4

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`67382` cycles	`67188` cycles	`1.00`
`ML-DSA-44 sign`	`198582` cycles	`199058` cycles	`1.00`
`ML-DSA-44 verify`	`70337` cycles	`70294` cycles	`1.00`
`ML-DSA-65 keypair`	`119365` cycles	`119349` cycles	`1.00`
`ML-DSA-65 sign`	`325608` cycles	`325681` cycles	`1.00`
`ML-DSA-65 verify`	`116876` cycles	`117069` cycles	`1.00`
`ML-DSA-87 keypair`	`196651` cycles	`196230` cycles	`1.00`
`ML-DSA-87 sign`	`421761` cycles	`420592` cycles	`1.00`
`ML-DSA-87 verify`	`193332` cycles	`192796` cycles	`1.00`

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

oqs-bot

Graviton3

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`71588` cycles	`71502` cycles	`1.00`
`ML-DSA-44 sign`	`210232` cycles	`210202` cycles	`1.00`
`ML-DSA-44 verify`	`74910` cycles	`74960` cycles	`1.00`
`ML-DSA-65 keypair`	`126070` cycles	`126199` cycles	`1.00`
`ML-DSA-65 sign`	`344764` cycles	`345032` cycles	`1.00`
`ML-DSA-65 verify`	`124137` cycles	`124351` cycles	`1.00`
`ML-DSA-87 keypair`	`206726` cycles	`207013` cycles	`1.00`
`ML-DSA-87 sign`	`439860` cycles	`444604` cycles	`0.99`
`ML-DSA-87 verify`	`204791` cycles	`204509` cycles	`1.00`

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

oqs-bot

Graviton4 (no-opt)

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`127800` cycles	`127847` cycles	`1.00`
`ML-DSA-44 sign`	`441873` cycles	`442380` cycles	`1.00`
`ML-DSA-44 verify`	`136459` cycles	`136598` cycles	`1.00`
`ML-DSA-65 keypair`	`223044` cycles	`223363` cycles	`1.00`
`ML-DSA-65 sign`	`714348` cycles	`714348` cycles	`1`
`ML-DSA-65 verify`	`220910` cycles	`220979` cycles	`1.00`
`ML-DSA-87 keypair`	`365028` cycles	`365561` cycles	`1.00`
`ML-DSA-87 sign`	`916025` cycles	`958782` cycles	`0.96`
`ML-DSA-87 verify`	`371402` cycles	`371548` cycles	`1.00`

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

oqs-bot

Graviton3 (no-opt)

Details

Benchmark suite	Current: `bcba070`	Previous: `14d195a`	Ratio
`ML-DSA-44 keypair`	`138397` cycles	`138360` cycles	`1.00`
`ML-DSA-44 sign`	`488095` cycles	`488372` cycles	`1.00`
`ML-DSA-44 verify`	`149570` cycles	`149676` cycles	`1.00`
`ML-DSA-65 keypair`	`242068` cycles	`242151` cycles	`1.00`
`ML-DSA-65 sign`	`793052` cycles	`792429` cycles	`1.00`
`ML-DSA-65 verify`	`242155` cycles	`241998` cycles	`1.00`
`ML-DSA-87 keypair`	`395952` cycles	`396891` cycles	`1.00`
`ML-DSA-87 sign`	`1014800` cycles	`1060851` cycles	`0.96`
`ML-DSA-87 verify`	`405100` cycles	`404926` cycles	`1.00`

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

oqs-bot · 2026-09-27T09:16:11Z

CBMC Results (ML-DSA-44, REDUCE-RAM)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	28s	12s	+133%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	120s	19s	+532%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	39s	5s	+680%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	154s	49s	+214%

Full Results (229 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1183s	1364s	-13.3%
`caddq`	LP64	z3*	✅	1s	6s	-83%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	28s	12s	+133%
`decompose`	LP64	z3*	✅	2s	3s	-33%
`fqmul`	LP64	bitwuzla*	✅	21s	39s	-46%
`fqscale`	LP64	bitwuzla*	✅	1s	2s	-50%
`intt_native_aarch64`	LP64	z3*	✅	4s	3s	+33%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	1s	-	new
`intt_native_x86_64`	LP64	z3*	✅	1s	2s	-50%
`keccak_absorb`	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	6s	8s	-25%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccak_finalize`	LP64	z3*	✅	1s	2s	-50%
`keccak_init`	LP64	z3*	✅	1s	3s	-67%
`keccak_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccakf1600_extract_bytes (big endian)`	LP64	z3*	✅	2s	4s	-50%
`keccakf1600_permute`	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute_native`	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	6s	-83%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	4s	-75%
`keccakf1600x4_permute`	LP64	z3*	✅	2s	4s	-50%
`keccakf1600x4_permute_native`	LP64	z3*	✅	13s	22s	-41%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	5s	-60%
`make_hint`	LP64	z3*	✅	2s	3s	-33%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	120s	19s	+532%
`mld_check_pct`	LP64	z3*	✅	5s	15s	-67%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	2s	6s	-67%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	3s	3s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	3s	-33%
	ILP32	z3	✅	1s	3s	-67%
	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u8`	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	z3*	✅	1s	4s	-75%
`mld_ct_get_optblocker_u32`	LP64	z3*	✅	3s	2s	+50%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	2s	-50%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	1s	+0%
`mld_ct_sel_int32`	LP64	z3*	✅	1s	3s	-67%
`mld_h`	LP64	z3*	✅	4s	4s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	54s	105s	-49%
`mld_keccakf1600_extract_bytes`	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600_permute_c`	LP64	z3*	✅	5s	7s	-29%
`mld_keccakf1600x4_extract_bytes_c`	LP64	z3*	✅	2s	4s	-50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	z3*	✅	2s	4s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	23s	-52%
`mld_ntt_layer`	LP64	bitwuzla*	✅	26s	41s	-37%
`mld_polymat_expand_entry`	LP64	z3*	✅	1s	2s	-50%
`mld_prepare_domain_separation_prefix`	LP64	z3*	✅	1s	3s	-67%
`mld_sample_s1_s2`	LP64	z3*	✅	2s	1s	+100%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	3s	4s	-25%
`mld_sign_attempt`	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	z3*	✅	3s	-	new
`mld_sign_resume`	LP64	z3*	✅	1s	-	new
`mld_value_barrier_i64`	LP64	z3*	✅	2s	3s	-33%
`mld_value_barrier_u32`	LP64	z3*	✅	3s	1s	+200%
`mld_value_barrier_u8`	LP64	z3*	✅	3s	4s	-25%
`montgomery_reduce`	LP64	z3*	✅	2s	2s	+0%
`ntt_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	1s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	-	new
	LP64	z3	✅	1s	-	new
`ntt_native_x86_64`	LP64	z3*	✅	4s	3s	+33%
`nttunpack_native_x86_64`	LP64	z3*	✅	2s	4s	-50%
`pack_sig_c`	LP64	z3*	✅	2s	5s	-60%
`pack_sig_h`	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
`pack_sig_z`	LP64	z3*	✅	3s	2s	+50%
`pack_sk_rho_key_tr_s2`	LP64	z3*	✅	4s	5s	-20%
`pack_sk_s1`	LP64	z3*	✅	2s	3s	-33%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	6s	-50%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	2s	4s	-50%
`pointwise_native_aarch64`	LP64	z3*	✅	3s	2s	+50%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	3s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	3s	-	new
`pointwise_native_x86_64`	LP64	z3*	✅	2s	4s	-50%
`poly_add`	LP64	z3*	✅	2s	7s	-71%
`poly_caddq`	LP64	z3*	✅	1s	4s	-75%
`poly_caddq_c`	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native`	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native_x86_64`	LP64	z3*	✅	2s	4s	-50%
`poly_challenge`	LP64	z3*	✅	4s	6s	-33%
`poly_chknorm`	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_c`	LP64	z3*	✅	6s	11s	-45%
`poly_chknorm_native`	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`poly_chknorm_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_88_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_c`	LP64	z3*	✅	4s	5s	-20%
`poly_decompose_native`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont`	LP64	z3*	✅	1s	2s	-50%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	4s	11s	-64%
`poly_invntt_tomont_native`	LP64	z3*	✅	2s	3s	-33%
`poly_ntt`	LP64	z3*	✅	3s	3s	+0%
`poly_ntt_c`	LP64	z3_smt_only*	✅	9s	21s	-57%
`poly_ntt_native`	LP64	z3*	✅	4s	3s	+33%
`poly_permute_bitrev_to_custom_optional`	LP64	z3*	✅	3s	5s	-40%
`poly_permute_bitrev_to_custom_optional_native`	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery`	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	64s	112s	-43%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	3s	2s	+50%
`poly_power2round`	LP64	z3*	✅	2s	4s	-50%
`poly_reduce`	LP64	z3*	✅	4s	4s	+0%
`poly_shiftl`	LP64	z3*	✅	5s	4s	+25%
`poly_sub`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_4x`	LP64	z3*	✅	1s	3s	-67%
`poly_uniform_eta`	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_eta_4x`	LP64	z3*	✅	7s	12s	-42%
`poly_uniform_gamma1`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	2s	5s	-60%
`poly_use_hint`	LP64	z3*	✅	4s	2s	+100%
`poly_use_hint_c`	LP64	z3*	✅	4s	5s	-20%
`poly_use_hint_native`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_x86_64`	LP64	z3*	✅	3s	-	new
`polyeta_pack`	LP64	z3*	✅	2s	3s	-33%
`polyeta_unpack`	LP64	z3*	✅	9s	14s	-36%
`polyt0_pack`	LP64	z3*	✅	2s	4s	-50%
`polyt0_unpack`	LP64	z3*	✅	7s	12s	-42%
`polyt1_pack`	LP64	z3*	✅	2s	3s	-33%
`polyt1_unpack`	LP64	z3*	✅	2s	2s	+0%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	2s	4s	-50%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	8s	6s	+33%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	91s	149s	-39%
`polyveck_caddq`	LP64	z3*	✅	2s	3s	-33%
`polyveck_chknorm`	LP64	z3*	✅	4s	67s	-94%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	3s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	4s	5s	-20%
`polyveck_ntt`	LP64	z3*	✅	2s	2s	+0%
`polyveck_pack_eta`	LP64	z3*	✅	3s	4s	-25%
`polyveck_reduce`	LP64	z3*	✅	1s	4s	-75%
`polyveck_unpack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_chknorm`	LP64	z3*	✅	3s	11s	-73%
`polyvecl_ntt`	LP64	z3*	✅	3s	3s	+0%
`polyvecl_pack_eta`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	1s	4s	-75%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	1s	3s	-67%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_eta`	LP64	z3*	✅	3s	4s	-25%
`polyvecl_unpack_z`	LP64	z3*	✅	3s	3s	+0%
`polyw1_pack`	LP64	z3*	✅	3s	4s	-25%
`polyw1_pack_32`	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_88`	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack`	LP64	z3*	✅	2s	-	new
`polyw1_unpack_32`	LP64	z3*	✅	3s	-	new
`polyw1_unpack_88`	LP64	z3*	✅	3s	-	new
`polyz_pack`	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack`	LP64	z3*	✅	4s	3s	+33%
`polyz_unpack_17_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack_c`	LP64	z3*	✅	5s	8s	-38%
`polyz_unpack_native`	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	z3*	✅	3s	2s	+50%
`reduce32`	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	3s	5s	-40%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	4s	-25%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	3s	+0%
`rej_uniform`	LP64	z3*	✅	4s	8s	-50%
`rej_uniform_c`	LP64	z3*	✅	9s	16s	-44%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	4s	3s	+33%
`rej_uniform_eta_native_x86_64`	LP64	z3_smt_only*	✅	3s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	5s	-40%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
`rej_uniform_native_x86_64`	LP64	z3_smt_only*	✅	7s	-	new
`shake128_absorb`	LP64	z3*	✅	3s	3s	+0%
`shake128_finalize`	LP64	z3*	✅	1s	3s	-67%
`shake128_init`	LP64	z3*	✅	1s	2s	-50%
`shake128_release`	LP64	z3*	✅	1s	2s	-50%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	2s	-50%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	2s	-50%
`shake256`	LP64	z3*	✅	2s	1s	+100%
`shake256_absorb`	LP64	z3*	✅	2s	2s	+0%
`shake256_finalize`	LP64	z3*	✅	2s	2s	+0%
`shake256_init`	LP64	z3*	✅	3s	4s	-25%
`shake256_release`	LP64	z3*	✅	1s	1s	+0%
`shake256_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	1s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	2s	-50%
`sig_unpack_hints`	LP64	z3*	✅	12s	2s	+500%
`sign_keypair`	LP64	z3*	✅	5s	5s	+0%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	18s	4s	+350%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	39s	5s	+680%
`sign_signature`	LP64	z3*	✅	4s	6s	-33%
`sign_signature_extmu`	LP64	z3*	✅	3s	4s	-25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	14s	4s	+250%
`sign_signature_pre_hash_internal`	LP64	z3*	✅	3s	4s	-25%
`sign_signature_pre_hash_shake256`	LP64	z3*	✅	4s	4s	+0%
`sign_verify`	LP64	z3*	✅	3s	4s	-25%
`sign_verify_extmu`	LP64	z3*	✅	2s	5s	-60%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	154s	49s	+214%
`sign_verify_pre_hash_internal`	LP64	z3*	✅	6s	5s	+20%
`sign_verify_pre_hash_shake256`	LP64	z3*	✅	2s	5s	-60%
`sk_s1hat_get_poly`	LP64	z3*	✅	3s	2s	+50%
`sk_s2hat_get_poly`	LP64	z3*	✅	3s	5s	-40%
`sk_t0hat_get_poly`	LP64	z3*	✅	2s	1s	+100%
`sys_check_capability`	LP64	z3*	✅	1s	2s	-50%
`unpack_pk_t1`	LP64	z3*	✅	1s	3s	-67%
`unpack_sk`	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_s1hat`	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_s2hat`	LP64	z3*	✅	3s	4s	-25%
`unpack_sk_t0hat`	LP64	z3*	✅	1s	2s	-50%
`use_hint`	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	z3*	✅	1s	3s	-67%
`yvec_init`	LP64	z3*	✅	1s	1s	+0%

oqs-bot · 2026-09-27T09:16:40Z

CBMC Results (ML-DSA-65, REDUCE-RAM)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	31s	7s	+343%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	108s	31s	+248%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	25s	3s	+733%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	56s	5s	+1020%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	176s	71s	+148%

Full Results (229 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1282s	1482s	-13.5%
`caddq`	LP64	z3*	✅	3s	2s	+50%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	31s	7s	+343%
`decompose`	LP64	z3*	✅	1s	4s	-75%
`fqmul`	LP64	bitwuzla*	✅	22s	40s	-45%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
`intt_native_aarch64`	LP64	z3*	✅	4s	2s	+100%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	3s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_x86_64`	LP64	z3*	✅	2s	4s	-50%
`keccak_absorb`	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	10s	-50%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	3s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccak_finalize`	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	z3*	✅	2s	4s	-50%
`keccak_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	4s	-25%
`keccakf1600_extract_bytes (big endian)`	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute`	LP64	z3*	✅	2s	4s	-50%
`keccakf1600_permute_native`	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	3s	4s	-25%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	1s	+0%
`keccakf1600x4_permute`	LP64	z3*	✅	2s	1s	+100%
`keccakf1600x4_permute_native`	LP64	z3*	✅	13s	22s	-41%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	3s	2s	+50%
`make_hint`	LP64	z3*	✅	1s	3s	-67%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	108s	31s	+248%
`mld_check_pct`	LP64	z3*	✅	5s	12s	-58%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	4s	5s	-20%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	4s	6s	-33%
	ILP32	cvc5_arrays_exp	✅	1s	6s	-83%
	ILP32	z3	✅	2s	6s	-67%
	LP64	bitwuzla	✅	1s	6s	-83%
	LP64	cvc5_arrays_exp	✅	1s	6s	-83%
	LP64	z3*	✅	1s	6s	-83%
`mld_ct_cmask_neg_i32`	LP64	z3*	✅	4s	3s	+33%
`mld_ct_cmask_nonzero_u32`	LP64	z3*	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u8`	LP64	z3*	✅	3s	2s	+50%
`mld_ct_get_optblocker_i64`	LP64	z3*	✅	2s	1s	+100%
`mld_ct_get_optblocker_u32`	LP64	z3*	✅	1s	3s	-67%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	4s	-75%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	4s	-75%
`mld_ct_sel_int32`	LP64	z3*	✅	1s	2s	-50%
`mld_h`	LP64	z3*	✅	2s	3s	-33%
`mld_invntt_layer`	LP64	bitwuzla*	✅	55s	108s	-49%
`mld_keccakf1600_extract_bytes`	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600_permute_c`	LP64	z3*	✅	5s	7s	-29%
`mld_keccakf1600x4_extract_bytes_c`	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	z3*	✅	1s	2s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	12s	25s	-52%
`mld_ntt_layer`	LP64	bitwuzla*	✅	22s	43s	-49%
`mld_polymat_expand_entry`	LP64	z3*	✅	2s	3s	-33%
`mld_prepare_domain_separation_prefix`	LP64	z3*	✅	1s	4s	-75%
`mld_sample_s1_s2`	LP64	z3*	✅	4s	6s	-33%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	3s	3s	+0%
`mld_sign_attempt`	LP64	z3*	✅	1s	-	new
`mld_sign_finish`	LP64	z3*	✅	4s	-	new
`mld_sign_resume`	LP64	z3*	✅	4s	-	new
`mld_value_barrier_i64`	LP64	z3*	✅	3s	2s	+50%
`mld_value_barrier_u32`	LP64	z3*	✅	1s	4s	-75%
`mld_value_barrier_u8`	LP64	z3*	✅	2s	1s	+100%
`montgomery_reduce`	LP64	z3*	✅	2s	1s	+100%
`ntt_native_aarch64`	LP64	z3*	✅	1s	3s	-67%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	3s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_x86_64`	LP64	z3*	✅	2s	5s	-60%
`nttunpack_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`pack_sig_c`	LP64	z3*	✅	3s	3s	+0%
`pack_sig_h`	LP64	z3_no_bv_extract*	✅	1s	2s	-50%
`pack_sig_z`	LP64	z3*	✅	2s	1s	+100%
`pack_sk_rho_key_tr_s2`	LP64	z3*	✅	3s	2s	+50%
`pack_sk_s1`	LP64	z3*	✅	2s	3s	-33%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	5s	6s	-17%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	3s	5s	-40%
`pointwise_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	3s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	1s	-	new
`pointwise_native_x86_64`	LP64	z3*	✅	1s	2s	-50%
`poly_add`	LP64	z3*	✅	3s	7s	-57%
`poly_caddq`	LP64	z3*	✅	1s	3s	-67%
`poly_caddq_c`	LP64	z3*	✅	3s	5s	-40%
`poly_caddq_native`	LP64	z3*	✅	1s	4s	-75%
`poly_caddq_native_aarch64`	LP64	z3*	✅	4s	2s	+100%
`poly_caddq_native_x86_64`	LP64	z3*	✅	2s	1s	+100%
`poly_challenge`	LP64	z3*	✅	2s	5s	-60%
`poly_chknorm`	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_c`	LP64	z3*	✅	9s	13s	-31%
`poly_chknorm_native`	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_x86_64`	LP64	z3*	✅	2s	4s	-50%
`poly_decompose`	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`poly_decompose_88_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_c`	LP64	z3*	✅	3s	8s	-62%
`poly_decompose_native`	LP64	z3*	✅	3s	5s	-40%
`poly_decompose_native_x86_64`	LP64	z3*	✅	3s	2s	+50%
`poly_invntt_tomont`	LP64	z3*	✅	2s	5s	-60%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	5s	10s	-50%
`poly_invntt_tomont_native`	LP64	z3*	✅	3s	5s	-40%
`poly_ntt`	LP64	z3*	✅	1s	2s	-50%
`poly_ntt_c`	LP64	z3_smt_only*	✅	9s	22s	-59%
`poly_ntt_native`	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional_native`	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery`	LP64	z3*	✅	3s	2s	+50%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	62s	116s	-47%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	4s	4s	+0%
`poly_power2round`	LP64	z3*	✅	4s	7s	-43%
`poly_reduce`	LP64	z3*	✅	1s	4s	-75%
`poly_shiftl`	LP64	z3*	✅	3s	3s	+0%
`poly_sub`	LP64	z3*	✅	1s	4s	-75%
`poly_uniform`	LP64	z3*	✅	1s	2s	-50%
`poly_uniform_4x`	LP64	z3*	✅	2s	4s	-50%
`poly_uniform_eta`	LP64	z3*	✅	2s	5s	-60%
`poly_uniform_eta_4x`	LP64	z3*	✅	8s	13s	-38%
`poly_uniform_gamma1`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	5s	3s	+67%
`poly_use_hint`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_c`	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native`	LP64	z3*	✅	2s	7s	-71%
`poly_use_hint_native_aarch64`	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint_native_x86_64`	LP64	z3*	✅	4s	-	new
`polyeta_pack`	LP64	z3*	✅	3s	1s	+200%
`polyeta_unpack`	LP64	z3*	✅	2s	4s	-50%
`polyt0_pack`	LP64	z3*	✅	1s	5s	-80%
`polyt0_unpack`	LP64	z3*	✅	9s	13s	-31%
`polyt1_pack`	LP64	z3*	✅	2s	3s	-33%
`polyt1_unpack`	LP64	z3*	✅	4s	3s	+33%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	2s	6s	-67%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	2s	3s	-33%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	3s	8s	-62%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	154s	201s	-23%
`polyveck_caddq`	LP64	z3*	✅	4s	7s	-43%
`polyveck_chknorm`	LP64	z3*	✅	5s	36s	-86%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	5s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	4s	7s	-43%
`polyveck_ntt`	LP64	z3*	✅	1s	4s	-75%
`polyveck_pack_eta`	LP64	z3*	✅	1s	3s	-67%
`polyveck_reduce`	LP64	z3*	✅	4s	6s	-33%
`polyveck_unpack_eta`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_chknorm`	LP64	z3*	✅	5s	43s	-88%
`polyvecl_ntt`	LP64	z3*	✅	2s	7s	-71%
`polyvecl_pack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	1s	4s	-75%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	2s	1s	+100%
`polyvecl_unpack_eta`	LP64	z3*	✅	1s	2s	-50%
`polyvecl_unpack_z`	LP64	z3*	✅	2s	1s	+100%
`polyw1_pack`	LP64	z3*	✅	5s	3s	+67%
`polyw1_pack_32`	LP64	z3*	✅	1s	2s	-50%
`polyw1_pack_88`	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack`	LP64	z3*	✅	5s	-	new
`polyw1_unpack_32`	LP64	z3*	✅	4s	-	new
`polyw1_unpack_88`	LP64	z3*	✅	3s	-	new
`polyz_pack`	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack`	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack_19_native_aarch64`	LP64	z3*	✅	2s	5s	-60%
`polyz_unpack_c`	LP64	z3*	✅	3s	9s	-67%
`polyz_unpack_native`	LP64	z3*	✅	4s	3s	+33%
`polyz_unpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`power2round`	LP64	z3*	✅	1s	2s	-50%
`reduce32`	LP64	z3*	✅	2s	2s	+0%
`rej_eta`	LP64	bitwuzla*	✅	1s	5s	-80%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	4s	-50%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	3s	+0%
`rej_uniform`	LP64	z3*	✅	3s	7s	-57%
`rej_uniform_c`	LP64	z3*	✅	7s	16s	-56%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	5s	-60%
`rej_uniform_eta_native_x86_64`	LP64	z3_smt_only*	✅	1s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	4s	-25%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	5s	-40%
`rej_uniform_native_x86_64`	LP64	z3_smt_only*	✅	6s	-	new
`shake128_absorb`	LP64	z3*	✅	1s	2s	-50%
`shake128_finalize`	LP64	z3*	✅	1s	2s	-50%
`shake128_init`	LP64	z3*	✅	2s	6s	-67%
`shake128_release`	LP64	z3*	✅	2s	2s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	3s	-67%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	4s	2s	+100%
`shake256`	LP64	z3*	✅	1s	2s	-50%
`shake256_absorb`	LP64	z3*	✅	2s	4s	-50%
`shake256_finalize`	LP64	z3*	✅	1s	1s	+0%
`shake256_init`	LP64	z3*	✅	2s	4s	-50%
`shake256_release`	LP64	z3*	✅	1s	3s	-67%
`shake256_squeeze`	LP64	bitwuzla*	✅	1s	4s	-75%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	2s	+50%
`sig_unpack_hints`	LP64	z3*	✅	13s	1s	+1200%
`sign_keypair`	LP64	z3*	✅	6s	4s	+50%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	25s	3s	+733%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	56s	5s	+1020%
`sign_signature`	LP64	z3*	✅	3s	5s	-40%
`sign_signature_extmu`	LP64	z3*	✅	4s	4s	+0%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	11s	6s	+83%
`sign_signature_pre_hash_internal`	LP64	z3*	✅	3s	3s	+0%
`sign_signature_pre_hash_shake256`	LP64	z3*	✅	3s	7s	-57%
`sign_verify`	LP64	z3*	✅	2s	6s	-67%
`sign_verify_extmu`	LP64	z3*	✅	2s	2s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	176s	71s	+148%
`sign_verify_pre_hash_internal`	LP64	z3*	✅	2s	5s	-60%
`sign_verify_pre_hash_shake256`	LP64	z3*	✅	3s	6s	-50%
`sk_s1hat_get_poly`	LP64	z3*	✅	1s	3s	-67%
`sk_s2hat_get_poly`	LP64	z3*	✅	2s	1s	+100%
`sk_t0hat_get_poly`	LP64	z3*	✅	1s	1s	+0%
`sys_check_capability`	LP64	z3*	✅	2s	1s	+100%
`unpack_pk_t1`	LP64	z3*	✅	3s	2s	+50%
`unpack_sk`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	z3*	✅	1s	1s	+0%
`unpack_sk_s2hat`	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_t0hat`	LP64	z3*	✅	3s	4s	-25%
`use_hint`	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	z3*	✅	4s	3s	+33%
`yvec_init`	LP64	z3*	✅	3s	5s	-40%

oqs-bot · 2026-09-27T09:16:46Z

CBMC Results (ML-DSA-87, REDUCE-RAM)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	26s	12s	+117%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	123s	34s	+262%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	34s	6s	+467%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	71s	6s	+1083%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	182s	47s	+287%

Full Results (229 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1260s	1436s	-12.3%
`caddq`	LP64	z3*	✅	1s	3s	-67%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	26s	12s	+117%
`decompose`	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	23s	39s	-41%
`fqscale`	LP64	bitwuzla*	✅	2s	1s	+100%
`intt_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	1s	-	new
`intt_native_x86_64`	LP64	z3*	✅	2s	4s	-50%
`keccak_absorb`	LP64	z3*	✅	5s	4s	+25%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	8s	-38%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	1s	+200%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccak_finalize`	LP64	z3*	✅	1s	1s	+0%
`keccak_init`	LP64	z3*	✅	1s	1s	+0%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	5s	-60%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute`	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_permute_native`	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	3s	1s	+200%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	1s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccakf1600x4_permute`	LP64	z3*	✅	3s	2s	+50%
`keccakf1600x4_permute_native`	LP64	z3*	✅	10s	25s	-60%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	1s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	3s	2s	+50%
`make_hint`	LP64	z3*	✅	1s	2s	-50%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	123s	34s	+262%
`mld_check_pct`	LP64	z3*	✅	4s	15s	-73%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	2s	6s	-67%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	1s	+0%
	ILP32	cvc5_arrays_exp	✅	3s	1s	+200%
	ILP32	z3	✅	3s	1s	+200%
	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_cmask_neg_i32`	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u32`	LP64	z3*	✅	2s	5s	-60%
`mld_ct_cmask_nonzero_u8`	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u32`	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	3s	-67%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	1s	+0%
`mld_ct_sel_int32`	LP64	z3*	✅	1s	2s	-50%
`mld_h`	LP64	z3*	✅	3s	2s	+50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	53s	111s	-52%
`mld_keccakf1600_extract_bytes`	LP64	z3*	✅	2s	1s	+100%
`mld_keccakf1600_permute_c`	LP64	z3*	✅	5s	8s	-38%
`mld_keccakf1600x4_extract_bytes_c`	LP64	z3*	✅	2s	3s	-33%
`mld_keccakf1600x4_xor_bytes_c`	LP64	z3*	✅	1s	1s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	23s	-52%
`mld_ntt_layer`	LP64	bitwuzla*	✅	23s	44s	-48%
`mld_polymat_expand_entry`	LP64	z3*	✅	2s	4s	-50%
`mld_prepare_domain_separation_prefix`	LP64	z3*	✅	3s	3s	+0%
`mld_sample_s1_s2`	LP64	z3*	✅	4s	8s	-50%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	3s	6s	-50%
`mld_sign_attempt`	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	z3*	✅	3s	-	new
`mld_sign_resume`	LP64	z3*	✅	3s	-	new
`mld_value_barrier_i64`	LP64	z3*	✅	1s	2s	-50%
`mld_value_barrier_u32`	LP64	z3*	✅	2s	3s	-33%
`mld_value_barrier_u8`	LP64	z3*	✅	1s	2s	-50%
`montgomery_reduce`	LP64	z3*	✅	1s	2s	-50%
`ntt_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	1s	-	new
`ntt_native_x86_64`	LP64	z3*	✅	3s	2s	+50%
`nttunpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`pack_sig_c`	LP64	z3*	✅	1s	2s	-50%
`pack_sig_h`	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`pack_sig_z`	LP64	z3*	✅	2s	3s	-33%
`pack_sk_rho_key_tr_s2`	LP64	z3*	✅	2s	2s	+0%
`pack_sk_s1`	LP64	z3*	✅	3s	2s	+50%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	2s	5s	-60%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	4s	8s	-50%
`pointwise_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	3s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	1s	-	new
`pointwise_native_x86_64`	LP64	z3*	✅	2s	5s	-60%
`poly_add`	LP64	z3*	✅	3s	8s	-62%
`poly_caddq`	LP64	z3*	✅	2s	5s	-60%
`poly_caddq_c`	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native`	LP64	z3*	✅	4s	3s	+33%
`poly_caddq_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`poly_challenge`	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm`	LP64	z3*	✅	1s	4s	-75%
`poly_chknorm_c`	LP64	z3*	✅	7s	13s	-46%
`poly_chknorm_native`	LP64	z3*	✅	4s	1s	+300%
`poly_chknorm_native_aarch64`	LP64	z3*	✅	4s	5s	-20%
`poly_chknorm_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	4s	3s	+33%
`poly_decompose_88_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_c`	LP64	z3*	✅	4s	6s	-33%
`poly_decompose_native`	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`poly_invntt_tomont`	LP64	z3*	✅	3s	4s	-25%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	7s	9s	-22%
`poly_invntt_tomont_native`	LP64	z3*	✅	2s	2s	+0%
`poly_ntt`	LP64	z3*	✅	1s	2s	-50%
`poly_ntt_c`	LP64	z3_smt_only*	✅	11s	19s	-42%
`poly_ntt_native`	LP64	z3*	✅	3s	4s	-25%
`poly_permute_bitrev_to_custom_optional`	LP64	z3*	✅	1s	2s	-50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery`	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	63s	125s	-50%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	3s	-33%
`poly_power2round`	LP64	z3*	✅	3s	7s	-57%
`poly_reduce`	LP64	z3*	✅	1s	4s	-75%
`poly_shiftl`	LP64	z3*	✅	2s	4s	-50%
`poly_sub`	LP64	z3*	✅	2s	5s	-60%
`poly_uniform`	LP64	z3*	✅	5s	4s	+25%
`poly_uniform_4x`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_eta`	LP64	z3*	✅	3s	5s	-40%
`poly_uniform_eta_4x`	LP64	z3*	✅	7s	12s	-42%
`poly_uniform_gamma1`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	1s	3s	-67%
`poly_use_hint`	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint_c`	LP64	z3*	✅	4s	4s	+0%
`poly_use_hint_native`	LP64	z3*	✅	1s	1s	+0%
`poly_use_hint_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_x86_64`	LP64	z3*	✅	3s	-	new
`polyeta_pack`	LP64	z3*	✅	3s	3s	+0%
`polyeta_unpack`	LP64	z3*	✅	7s	13s	-46%
`polyt0_pack`	LP64	z3*	✅	3s	3s	+0%
`polyt0_unpack`	LP64	z3*	✅	8s	14s	-43%
`polyt1_pack`	LP64	z3*	✅	2s	5s	-60%
`polyt1_unpack`	LP64	z3*	✅	1s	3s	-67%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	1s	3s	-67%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	4s	13s	-69%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	108s	196s	-45%
`polyveck_caddq`	LP64	z3*	✅	4s	8s	-50%
`polyveck_chknorm`	LP64	z3*	✅	3s	9s	-67%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	5s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	2s	4s	-50%
`polyveck_ntt`	LP64	z3*	✅	2s	3s	-33%
`polyveck_pack_eta`	LP64	z3*	✅	3s	5s	-40%
`polyveck_reduce`	LP64	z3*	✅	2s	6s	-67%
`polyveck_unpack_eta`	LP64	z3*	✅	3s	3s	+0%
`polyvecl_chknorm`	LP64	z3*	✅	3s	38s	-92%
`polyvecl_ntt`	LP64	z3*	✅	4s	8s	-50%
`polyvecl_pack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	1s	2s	-50%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	3s	2s	+50%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	1s	3s	-67%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	1s	2s	-50%
`polyvecl_unpack_eta`	LP64	z3*	✅	1s	3s	-67%
`polyvecl_unpack_z`	LP64	z3*	✅	1s	3s	-67%
`polyw1_pack`	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_32`	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_88`	LP64	z3*	✅	1s	2s	-50%
`polyw1_unpack`	LP64	z3*	✅	1s	-	new
`polyw1_unpack_32`	LP64	z3*	✅	2s	-	new
`polyw1_unpack_88`	LP64	z3*	✅	1s	-	new
`polyz_pack`	LP64	z3*	✅	1s	4s	-75%
`polyz_unpack`	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	LP64	z3*	✅	1s	4s	-75%
`polyz_unpack_19_native_aarch64`	LP64	z3*	✅	4s	5s	-20%
`polyz_unpack_c`	LP64	z3*	✅	4s	7s	-43%
`polyz_unpack_native`	LP64	z3*	✅	2s	1s	+100%
`polyz_unpack_native_x86_64`	LP64	z3*	✅	4s	3s	+33%
`power2round`	LP64	z3*	✅	3s	3s	+0%
`reduce32`	LP64	z3*	✅	3s	3s	+0%
`rej_eta`	LP64	bitwuzla*	✅	4s	2s	+100%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	4s	-50%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	4s	-50%
`rej_uniform`	LP64	z3*	✅	4s	7s	-43%
`rej_uniform_c`	LP64	z3*	✅	7s	18s	-61%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
`rej_uniform_eta_native_x86_64`	LP64	z3_smt_only*	✅	1s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	5s	-40%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
`rej_uniform_native_x86_64`	LP64	z3_smt_only*	✅	7s	-	new
`shake128_absorb`	LP64	z3*	✅	1s	2s	-50%
`shake128_finalize`	LP64	z3*	✅	1s	2s	-50%
`shake128_init`	LP64	z3*	✅	1s	2s	-50%
`shake128_release`	LP64	z3*	✅	3s	3s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	1s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	4s	-75%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	1s	+100%
`shake256`	LP64	z3*	✅	2s	3s	-33%
`shake256_absorb`	LP64	z3*	✅	4s	3s	+33%
`shake256_finalize`	LP64	z3*	✅	2s	3s	-33%
`shake256_init`	LP64	z3*	✅	1s	3s	-67%
`shake256_release`	LP64	z3*	✅	2s	5s	-60%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	5s	-80%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	4s	-75%
`sig_unpack_hints`	LP64	z3*	✅	12s	4s	+200%
`sign_keypair`	LP64	z3*	✅	6s	4s	+50%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	34s	6s	+467%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	71s	6s	+1083%
`sign_signature`	LP64	z3*	✅	2s	4s	-50%
`sign_signature_extmu`	LP64	z3*	✅	3s	4s	-25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	17s	3s	+467%
`sign_signature_pre_hash_internal`	LP64	z3*	✅	2s	2s	+0%
`sign_signature_pre_hash_shake256`	LP64	z3*	✅	7s	3s	+133%
`sign_verify`	LP64	z3*	✅	4s	2s	+100%
`sign_verify_extmu`	LP64	z3*	✅	2s	4s	-50%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	182s	47s	+287%
`sign_verify_pre_hash_internal`	LP64	z3*	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	LP64	z3*	✅	2s	7s	-71%
`sk_s1hat_get_poly`	LP64	z3*	✅	1s	3s	-67%
`sk_s2hat_get_poly`	LP64	z3*	✅	1s	2s	-50%
`sk_t0hat_get_poly`	LP64	z3*	✅	2s	3s	-33%
`sys_check_capability`	LP64	z3*	✅	2s	2s	+0%
`unpack_pk_t1`	LP64	z3*	✅	2s	2s	+0%
`unpack_sk`	LP64	z3*	✅	3s	4s	-25%
`unpack_sk_s1hat`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s2hat`	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_t0hat`	LP64	z3*	✅	1s	4s	-75%
`use_hint`	LP64	z3*	✅	3s	3s	+0%
`yvec_get_poly`	LP64	z3*	✅	1s	2s	-50%
`yvec_init`	LP64	z3*	✅	1s	4s	-75%

oqs-bot · 2026-09-27T09:18:05Z

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	90s	50s	+80%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	135s	58s	+133%
`polyveck_chknorm`	LP64	z3*	⚠️	53s	5s	+960%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	35s	5s	+600%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	107s	26s	+312%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	262s	114s	+130%

Full Results (229 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1554s	1514s	+2.6%
`caddq`	LP64	z3*	✅	2s	2s	+0%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	90s	50s	+80%
`decompose`	LP64	z3*	✅	3s	2s	+50%
`fqmul`	LP64	bitwuzla*	✅	22s	39s	-44%
`fqscale`	LP64	bitwuzla*	✅	1s	3s	-67%
`intt_native_aarch64`	LP64	z3*	✅	1s	9s	-89%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_x86_64`	LP64	z3*	✅	3s	4s	-25%
`keccak_absorb`	LP64	z3*	✅	4s	5s	-20%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	4s	9s	-56%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	4s	3s	+33%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccak_finalize`	LP64	z3*	✅	3s	3s	+0%
`keccak_init`	LP64	z3*	✅	2s	3s	-33%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	LP64	z3*	✅	4s	2s	+100%
`keccakf1600_permute`	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_permute_native`	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccakf1600x4_permute`	LP64	z3*	✅	2s	4s	-50%
`keccakf1600x4_permute_native`	LP64	z3*	✅	11s	22s	-50%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	1s	3s	-67%
`make_hint`	LP64	z3*	✅	2s	3s	-33%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	135s	58s	+133%
`mld_check_pct`	LP64	z3*	✅	3s	14s	-79%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	7s	7s	+0%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	1s	2s	-50%
	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_neg_i32`	LP64	z3*	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u32`	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u8`	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_i64`	LP64	z3*	✅	1s	4s	-75%
`mld_ct_get_optblocker_u32`	LP64	z3*	✅	1s	1s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	1s	+200%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	3s	-67%
`mld_ct_sel_int32`	LP64	z3*	✅	2s	2s	+0%
`mld_h`	LP64	z3*	✅	2s	4s	-50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	55s	107s	-49%
`mld_keccakf1600_extract_bytes`	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600_permute_c`	LP64	z3*	✅	3s	8s	-62%
`mld_keccakf1600x4_extract_bytes_c`	LP64	z3*	✅	4s	2s	+100%
`mld_keccakf1600x4_xor_bytes_c`	LP64	z3*	✅	2s	2s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	10s	23s	-57%
`mld_ntt_layer`	LP64	bitwuzla*	✅	19s	42s	-55%
`mld_polymat_expand_entry`	LP64	z3*	✅	2s	3s	-33%
`mld_prepare_domain_separation_prefix`	LP64	z3*	✅	3s	4s	-25%
`mld_sample_s1_s2`	LP64	z3*	✅	4s	4s	+0%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	4s	3s	+33%
`mld_sign_attempt`	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	z3*	✅	3s	-	new
`mld_sign_resume`	LP64	z3*	✅	4s	-	new
`mld_value_barrier_i64`	LP64	z3*	✅	3s	2s	+50%
`mld_value_barrier_u32`	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u8`	LP64	z3*	✅	1s	3s	-67%
`montgomery_reduce`	LP64	z3*	✅	1s	3s	-67%
`ntt_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`nttunpack_native_x86_64`	LP64	z3*	✅	1s	1s	+0%
`pack_sig_c`	LP64	z3*	✅	2s	2s	+0%
`pack_sig_h`	LP64	z3_no_bv_extract*	✅	5s	3s	+67%
`pack_sig_z`	LP64	z3*	✅	1s	4s	-75%
`pack_sk_rho_key_tr_s2`	LP64	z3*	✅	3s	3s	+0%
`pack_sk_s1`	LP64	z3*	✅	2s	2s	+0%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	4s	-25%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	3s	7s	-57%
`pointwise_native_aarch64`	LP64	z3*	✅	3s	5s	-40%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	1s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_x86_64`	LP64	z3*	✅	2s	4s	-50%
`poly_add`	LP64	z3*	✅	3s	7s	-57%
`poly_caddq`	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_c`	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_native`	LP64	z3*	✅	3s	5s	-40%
`poly_caddq_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`poly_caddq_native_x86_64`	LP64	z3*	✅	2s	4s	-50%
`poly_challenge`	LP64	z3*	✅	1s	3s	-67%
`poly_chknorm`	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_c`	LP64	z3*	✅	6s	17s	-65%
`poly_chknorm_native`	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_aarch64`	LP64	z3*	✅	1s	4s	-75%
`poly_chknorm_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_88_native_aarch64`	LP64	z3*	✅	1s	4s	-75%
`poly_decompose_c`	LP64	z3*	✅	1s	4s	-75%
`poly_decompose_native`	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`poly_invntt_tomont`	LP64	z3*	✅	2s	4s	-50%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	6s	11s	-45%
`poly_invntt_tomont_native`	LP64	z3*	✅	3s	4s	-25%
`poly_ntt`	LP64	z3*	✅	2s	3s	-33%
`poly_ntt_c`	LP64	z3_smt_only*	✅	9s	19s	-53%
`poly_ntt_native`	LP64	z3*	✅	2s	5s	-60%
`poly_permute_bitrev_to_custom_optional`	LP64	z3*	✅	5s	2s	+150%
`poly_permute_bitrev_to_custom_optional_native`	LP64	z3*	✅	3s	4s	-25%
`poly_pointwise_montgomery`	LP64	z3*	✅	4s	3s	+33%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	45s	114s	-61%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	1s	2s	-50%
`poly_power2round`	LP64	z3*	✅	3s	4s	-25%
`poly_reduce`	LP64	z3*	✅	2s	3s	-33%
`poly_shiftl`	LP64	z3*	✅	2s	3s	-33%
`poly_sub`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	z3*	✅	2s	6s	-67%
`poly_uniform_4x`	LP64	z3*	✅	8s	14s	-43%
`poly_uniform_eta`	LP64	z3*	✅	1s	5s	-80%
`poly_uniform_eta_4x`	LP64	z3*	✅	8s	11s	-27%
`poly_uniform_gamma1`	LP64	z3*	✅	1s	4s	-75%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	1s	5s	-80%
`poly_use_hint`	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_c`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native`	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`poly_use_hint_native_x86_64`	LP64	z3*	✅	3s	-	new
`polyeta_pack`	LP64	z3*	✅	3s	3s	+0%
`polyeta_unpack`	LP64	z3*	✅	5s	14s	-64%
`polyt0_pack`	LP64	z3*	✅	2s	2s	+0%
`polyt0_unpack`	LP64	z3*	✅	6s	15s	-60%
`polyt1_pack`	LP64	z3*	✅	2s	4s	-50%
`polyt1_unpack`	LP64	z3*	✅	1s	5s	-80%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	18s	28s	-36%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	3s	8s	-62%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	1s	2s	-50%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	12s	15s	-20%
`polyveck_caddq`	LP64	z3*	✅	2s	3s	-33%
`polyveck_chknorm`	LP64	z3*	⚠️	53s	5s	+960%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	2s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	1s	5s	-80%
`polyveck_ntt`	LP64	z3*	✅	2s	5s	-60%
`polyveck_pack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyveck_reduce`	LP64	z3*	✅	3s	5s	-40%
`polyveck_unpack_eta`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_chknorm`	LP64	z3*	✅	2s	10s	-80%
`polyvecl_ntt`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_pack_eta`	LP64	z3*	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	4s	-50%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	138s	131s	+5%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	4s	2s	+100%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_z`	LP64	z3*	✅	3s	2s	+50%
`polyw1_pack`	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_32`	LP64	z3*	✅	1s	2s	-50%
`polyw1_pack_88`	LP64	z3*	✅	2s	1s	+100%
`polyw1_unpack`	LP64	z3*	✅	4s	-	new
`polyw1_unpack_32`	LP64	z3*	✅	1s	-	new
`polyw1_unpack_88`	LP64	z3*	✅	2s	-	new
`polyz_pack`	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack`	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	LP64	z3*	✅	3s	5s	-40%
`polyz_unpack_19_native_aarch64`	LP64	z3*	✅	1s	5s	-80%
`polyz_unpack_c`	LP64	z3*	✅	3s	11s	-73%
`polyz_unpack_native`	LP64	z3*	✅	3s	2s	+50%
`polyz_unpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`power2round`	LP64	z3*	✅	3s	3s	+0%
`reduce32`	LP64	z3*	✅	1s	2s	-50%
`rej_eta`	LP64	bitwuzla*	✅	4s	3s	+33%
`rej_eta_c`	LP64	bitwuzla*	✅	1s	4s	-75%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	6s	-50%
`rej_uniform`	LP64	z3*	✅	10s	18s	-44%
`rej_uniform_c`	LP64	z3*	✅	9s	15s	-40%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
`rej_uniform_eta_native_x86_64`	LP64	z3_smt_only*	✅	3s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	4s	-50%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	1s	5s	-80%
`rej_uniform_native_x86_64`	LP64	z3_smt_only*	✅	7s	-	new
`shake128_absorb`	LP64	z3*	✅	1s	2s	-50%
`shake128_finalize`	LP64	z3*	✅	2s	2s	+0%
`shake128_init`	LP64	z3*	✅	3s	3s	+0%
`shake128_release`	LP64	z3*	✅	4s	1s	+300%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	3s	-67%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	1s	+0%
`shake256`	LP64	z3*	✅	3s	1s	+200%
`shake256_absorb`	LP64	z3*	✅	1s	3s	-67%
`shake256_finalize`	LP64	z3*	✅	3s	2s	+50%
`shake256_init`	LP64	z3*	✅	1s	3s	-67%
`shake256_release`	LP64	z3*	✅	1s	2s	-50%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	3s	3s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	4s	4s	+0%
`sig_unpack_hints`	LP64	z3*	✅	18s	2s	+800%
`sign_keypair`	LP64	z3*	✅	4s	4s	+0%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	15s	4s	+275%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	35s	5s	+600%
`sign_signature`	LP64	z3*	✅	3s	3s	+0%
`sign_signature_extmu`	LP64	z3*	✅	4s	4s	+0%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	107s	26s	+312%
`sign_signature_pre_hash_internal`	LP64	z3*	✅	3s	6s	-50%
`sign_signature_pre_hash_shake256`	LP64	z3*	✅	3s	3s	+0%
`sign_verify`	LP64	z3*	✅	5s	4s	+25%
`sign_verify_extmu`	LP64	z3*	✅	3s	3s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	262s	114s	+130%
`sign_verify_pre_hash_internal`	LP64	z3*	✅	4s	3s	+33%
`sign_verify_pre_hash_shake256`	LP64	z3*	✅	4s	5s	-20%
`sk_s1hat_get_poly`	LP64	z3*	✅	2s	3s	-33%
`sk_s2hat_get_poly`	LP64	z3*	✅	3s	2s	+50%
`sk_t0hat_get_poly`	LP64	z3*	✅	2s	2s	+0%
`sys_check_capability`	LP64	z3*	✅	2s	4s	-50%
`unpack_pk_t1`	LP64	z3*	✅	1s	5s	-80%
`unpack_sk`	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_s1hat`	LP64	z3*	✅	2s	1s	+100%
`unpack_sk_s2hat`	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_t0hat`	LP64	z3*	✅	1s	3s	-67%
`use_hint`	LP64	z3*	✅	1s	2s	-50%
`yvec_get_poly`	LP64	z3*	✅	1s	3s	-67%
`yvec_init`	LP64	z3*	✅	3s	3s	+0%

oqs-bot · 2026-09-27T09:22:02Z

CBMC Results (ML-DSA-65)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	2295s	1784s	+28.6%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	147s	13s	+1031%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	236s	63s	+275%
`sig_unpack_hints`	LP64	z3*	⚠️	33s	2s	+1550%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	30s	5s	+500%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	62s	6s	+933%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	205s	55s	+273%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	479s	177s	+171%

Full Results (229 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	2295s	1784s	+28.6%
`caddq`	LP64	z3*	✅	3s	3s	+0%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	147s	13s	+1031%
`decompose`	LP64	z3*	✅	2s	1s	+100%
`fqmul`	LP64	bitwuzla*	✅	26s	40s	-35%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
`intt_native_aarch64`	LP64	z3*	✅	4s	3s	+33%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	3s	-	new
`intt_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`keccak_absorb`	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	8s	-38%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	4s	-75%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccak_finalize`	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	z3*	✅	2s	1s	+100%
`keccak_squeeze`	LP64	bitwuzla*	✅	4s	4s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	5s	-40%
`keccakf1600_extract_bytes (big endian)`	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute`	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute_native`	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	4s	-75%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	4s	-75%
`keccakf1600x4_permute`	LP64	z3*	✅	1s	4s	-75%
`keccakf1600x4_permute_native`	LP64	z3*	✅	12s	23s	-48%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	3s	-33%
`make_hint`	LP64	z3*	✅	4s	2s	+100%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	236s	63s	+275%
`mld_check_pct`	LP64	z3*	✅	5s	14s	-64%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	5s	7s	-29%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	2s	-50%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	3s	2s	+50%
	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_neg_i32`	LP64	z3*	✅	3s	2s	+50%
`mld_ct_cmask_nonzero_u32`	LP64	z3*	✅	3s	4s	-25%
`mld_ct_cmask_nonzero_u8`	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_i64`	LP64	z3*	✅	3s	2s	+50%
`mld_ct_get_optblocker_u32`	LP64	z3*	✅	1s	3s	-67%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	2s	-50%
`mld_ct_sel_int32`	LP64	z3*	✅	1s	3s	-67%
`mld_h`	LP64	z3*	✅	3s	2s	+50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	72s	109s	-34%
`mld_keccakf1600_extract_bytes`	LP64	z3*	✅	1s	1s	+0%
`mld_keccakf1600_permute_c`	LP64	z3*	✅	3s	6s	-50%
`mld_keccakf1600x4_extract_bytes_c`	LP64	z3*	✅	2s	3s	-33%
`mld_keccakf1600x4_xor_bytes_c`	LP64	z3*	✅	1s	2s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	14s	24s	-42%
`mld_ntt_layer`	LP64	bitwuzla*	✅	29s	41s	-29%
`mld_polymat_expand_entry`	LP64	z3*	✅	1s	4s	-75%
`mld_prepare_domain_separation_prefix`	LP64	z3*	✅	4s	2s	+100%
`mld_sample_s1_s2`	LP64	z3*	✅	2s	6s	-67%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	4s	4s	+0%
`mld_sign_attempt`	LP64	z3*	✅	5s	-	new
`mld_sign_finish`	LP64	z3*	✅	3s	-	new
`mld_sign_resume`	LP64	z3*	✅	3s	-	new
`mld_value_barrier_i64`	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u32`	LP64	z3*	✅	1s	3s	-67%
`mld_value_barrier_u8`	LP64	z3*	✅	1s	3s	-67%
`montgomery_reduce`	LP64	z3*	✅	3s	4s	-25%
`ntt_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`nttunpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`pack_sig_c`	LP64	z3*	✅	2s	5s	-60%
`pack_sig_h`	LP64	z3_no_bv_extract*	✅	2s	5s	-60%
`pack_sig_z`	LP64	z3*	✅	2s	2s	+0%
`pack_sk_rho_key_tr_s2`	LP64	z3*	✅	4s	2s	+100%
`pack_sk_s1`	LP64	z3*	✅	4s	5s	-20%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	4s	6s	-33%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	4s	8s	-50%
`pointwise_native_aarch64`	LP64	z3*	✅	2s	5s	-60%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	3s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`poly_add`	LP64	z3*	✅	2s	9s	-78%
`poly_caddq`	LP64	z3*	✅	4s	2s	+100%
`poly_caddq_c`	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_native`	LP64	z3*	✅	5s	2s	+150%
`poly_caddq_native_aarch64`	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native_x86_64`	LP64	z3*	✅	4s	3s	+33%
`poly_challenge`	LP64	z3*	✅	5s	6s	-17%
`poly_chknorm`	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_c`	LP64	z3*	✅	7s	15s	-53%
`poly_chknorm_native`	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_aarch64`	LP64	z3*	✅	5s	3s	+67%
`poly_chknorm_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`poly_decompose`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_88_native_aarch64`	LP64	z3*	✅	2s	1s	+100%
`poly_decompose_c`	LP64	z3*	✅	4s	5s	-20%
`poly_decompose_native`	LP64	z3*	✅	1s	3s	-67%
`poly_decompose_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`poly_invntt_tomont`	LP64	z3*	✅	1s	3s	-67%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	7s	11s	-36%
`poly_invntt_tomont_native`	LP64	z3*	✅	3s	2s	+50%
`poly_ntt`	LP64	z3*	✅	2s	2s	+0%
`poly_ntt_c`	LP64	z3_smt_only*	✅	11s	19s	-42%
`poly_ntt_native`	LP64	z3*	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional`	LP64	z3*	✅	5s	2s	+150%
`poly_permute_bitrev_to_custom_optional_native`	LP64	z3*	✅	1s	4s	-75%
`poly_pointwise_montgomery`	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	58s	125s	-54%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	3s	-33%
`poly_power2round`	LP64	z3*	✅	2s	4s	-50%
`poly_reduce`	LP64	z3*	✅	2s	3s	-33%
`poly_shiftl`	LP64	z3*	✅	2s	3s	-33%
`poly_sub`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	z3*	✅	6s	4s	+50%
`poly_uniform_4x`	LP64	z3*	✅	8s	13s	-38%
`poly_uniform_eta`	LP64	z3*	✅	3s	4s	-25%
`poly_uniform_eta_4x`	LP64	z3*	✅	8s	14s	-43%
`poly_uniform_gamma1`	LP64	z3*	✅	4s	3s	+33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_c`	LP64	z3*	✅	2s	5s	-60%
`poly_use_hint_native`	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native_x86_64`	LP64	z3*	✅	3s	-	new
`polyeta_pack`	LP64	z3*	✅	2s	3s	-33%
`polyeta_unpack`	LP64	z3*	✅	5s	8s	-38%
`polyt0_pack`	LP64	z3*	✅	4s	3s	+33%
`polyt0_unpack`	LP64	z3*	✅	10s	16s	-38%
`polyt1_pack`	LP64	z3*	✅	3s	3s	+0%
`polyt1_unpack`	LP64	z3*	✅	3s	5s	-40%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	74s	110s	-33%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	14s	27s	-48%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	2s	1s	+100%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	15s	18s	-17%
`polyveck_caddq`	LP64	z3*	✅	4s	6s	-33%
`polyveck_chknorm`	LP64	z3*	✅	3s	6s	-50%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	4s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	4s	8s	-50%
`polyveck_ntt`	LP64	z3*	✅	4s	7s	-43%
`polyveck_pack_eta`	LP64	z3*	✅	3s	4s	-25%
`polyveck_reduce`	LP64	z3*	✅	1s	4s	-75%
`polyveck_unpack_eta`	LP64	z3*	✅	3s	6s	-50%
`polyvecl_chknorm`	LP64	z3*	✅	1s	7s	-86%
`polyvecl_ntt`	LP64	z3*	✅	5s	4s	+25%
`polyvecl_pack_eta`	LP64	z3*	✅	1s	3s	-67%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	222s	210s	+6%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	1s	2s	-50%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_unpack_eta`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_unpack_z`	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	z3*	✅	2s	4s	-50%
`polyw1_pack_32`	LP64	z3*	✅	2s	4s	-50%
`polyw1_pack_88`	LP64	z3*	✅	1s	2s	-50%
`polyw1_unpack`	LP64	z3*	✅	1s	-	new
`polyw1_unpack_32`	LP64	z3*	✅	3s	-	new
`polyw1_unpack_88`	LP64	z3*	✅	4s	-	new
`polyz_pack`	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack`	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_19_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_c`	LP64	z3*	✅	3s	13s	-77%
`polyz_unpack_native`	LP64	z3*	✅	4s	4s	+0%
`polyz_unpack_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	z3*	✅	3s	1s	+200%
`reduce32`	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	1s	2s	-50%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	5s	-60%
`rej_eta_native`	LP64	bitwuzla*	✅	1s	3s	-67%
`rej_uniform`	LP64	z3*	✅	14s	18s	-22%
`rej_uniform_c`	LP64	z3*	✅	13s	14s	-7%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	4s	-50%
`rej_uniform_eta_native_x86_64`	LP64	z3_smt_only*	✅	1s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	4s	-25%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
`rej_uniform_native_x86_64`	LP64	z3_smt_only*	✅	11s	-	new
`shake128_absorb`	LP64	z3*	✅	1s	2s	-50%
`shake128_finalize`	LP64	z3*	✅	3s	1s	+200%
`shake128_init`	LP64	z3*	✅	1s	2s	-50%
`shake128_release`	LP64	z3*	✅	1s	3s	-67%
`shake128_squeeze`	LP64	bitwuzla*	✅	4s	2s	+100%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
`shake256`	LP64	z3*	✅	2s	2s	+0%
`shake256_absorb`	LP64	z3*	✅	3s	2s	+50%
`shake256_finalize`	LP64	z3*	✅	2s	1s	+100%
`shake256_init`	LP64	z3*	✅	4s	2s	+100%
`shake256_release`	LP64	z3*	✅	1s	2s	-50%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	3s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	3s	-33%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
`sig_unpack_hints`	LP64	z3*	⚠️	33s	2s	+1550%
`sign_keypair`	LP64	z3*	✅	5s	3s	+67%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	30s	5s	+500%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	62s	6s	+933%
`sign_signature`	LP64	z3*	✅	3s	6s	-50%
`sign_signature_extmu`	LP64	z3*	✅	2s	2s	+0%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	205s	55s	+273%
`sign_signature_pre_hash_internal`	LP64	z3*	✅	4s	3s	+33%
`sign_signature_pre_hash_shake256`	LP64	z3*	✅	6s	3s	+100%
`sign_verify`	LP64	z3*	✅	3s	3s	+0%
`sign_verify_extmu`	LP64	z3*	✅	3s	3s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	479s	177s	+171%
`sign_verify_pre_hash_internal`	LP64	z3*	✅	2s	5s	-60%
`sign_verify_pre_hash_shake256`	LP64	z3*	✅	4s	5s	-20%
`sk_s1hat_get_poly`	LP64	z3*	✅	2s	6s	-67%
`sk_s2hat_get_poly`	LP64	z3*	✅	2s	2s	+0%
`sk_t0hat_get_poly`	LP64	z3*	✅	2s	2s	+0%
`sys_check_capability`	LP64	z3*	✅	3s	4s	-25%
`unpack_pk_t1`	LP64	z3*	✅	4s	5s	-20%
`unpack_sk`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	z3*	✅	4s	2s	+100%
`unpack_sk_s2hat`	LP64	z3*	✅	1s	4s	-75%
`unpack_sk_t0hat`	LP64	z3*	✅	2s	5s	-60%
`use_hint`	LP64	z3*	✅	2s	2s	+0%
`yvec_get_poly`	LP64	z3*	✅	2s	3s	-33%
`yvec_init`	LP64	z3*	✅	2s	3s	-33%

oqs-bot · 2026-09-27T09:23:33Z

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	184s	19s	+868%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	335s	55s	+509%
`sig_unpack_hints`	LP64	z3*	⚠️	27s	3s	+800%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	43s	6s	+617%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	52s	6s	+767%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	355s	42s	+745%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	594s	97s	+512%

Full Results (229 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	2621s	2151s	+21.9%
`caddq`	LP64	z3*	✅	2s	4s	-50%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	184s	19s	+868%
`decompose`	LP64	z3*	✅	1s	3s	-67%
`fqmul`	LP64	bitwuzla*	✅	22s	43s	-49%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
`intt_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	4s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`keccak_absorb`	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	9s	-44%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	1s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	4s	-25%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	4s	-75%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_finalize`	LP64	z3*	✅	3s	1s	+200%
`keccak_init`	LP64	z3*	✅	2s	3s	-33%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	4s	-25%
`keccakf1600_extract_bytes (big endian)`	LP64	z3*	✅	3s	3s	+0%
`keccakf1600_permute`	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute_native`	LP64	z3*	✅	4s	4s	+0%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	3s	3s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccakf1600x4_permute`	LP64	z3*	✅	3s	3s	+0%
`keccakf1600x4_permute_native`	LP64	z3*	✅	11s	23s	-52%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	1s	3s	-67%
`make_hint`	LP64	z3*	✅	4s	3s	+33%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	335s	55s	+509%
`mld_check_pct`	LP64	z3*	✅	7s	16s	-56%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	6s	8s	-25%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	3s	-33%
	ILP32	cvc5_arrays_exp	✅	3s	3s	+0%
	ILP32	z3	✅	1s	3s	-67%
	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	LP64	z3*	✅	1s	4s	-75%
`mld_ct_cmask_nonzero_u32`	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u8`	LP64	z3*	✅	3s	3s	+0%
`mld_ct_get_optblocker_i64`	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_u32`	LP64	z3*	✅	3s	2s	+50%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	3s	-67%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	3s	-67%
`mld_ct_sel_int32`	LP64	z3*	✅	2s	3s	-33%
`mld_h`	LP64	z3*	✅	2s	3s	-33%
`mld_invntt_layer`	LP64	bitwuzla*	✅	56s	115s	-51%
`mld_keccakf1600_extract_bytes`	LP64	z3*	✅	3s	4s	-25%
`mld_keccakf1600_permute_c`	LP64	z3*	✅	5s	7s	-29%
`mld_keccakf1600x4_extract_bytes_c`	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	z3*	✅	2s	4s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	24s	-54%
`mld_ntt_layer`	LP64	bitwuzla*	✅	21s	45s	-53%
`mld_polymat_expand_entry`	LP64	z3*	✅	1s	3s	-67%
`mld_prepare_domain_separation_prefix`	LP64	z3*	✅	4s	4s	+0%
`mld_sample_s1_s2`	LP64	z3*	✅	4s	6s	-33%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	2s	8s	-75%
`mld_sign_attempt`	LP64	z3*	✅	3s	-	new
`mld_sign_finish`	LP64	z3*	✅	2s	-	new
`mld_sign_resume`	LP64	z3*	✅	3s	-	new
`mld_value_barrier_i64`	LP64	z3*	✅	1s	1s	+0%
`mld_value_barrier_u32`	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u8`	LP64	z3*	✅	2s	3s	-33%
`montgomery_reduce`	LP64	z3*	✅	2s	3s	-33%
`ntt_native_aarch64`	LP64	z3*	✅	2s	6s	-67%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	4s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_x86_64`	LP64	z3*	✅	1s	2s	-50%
`nttunpack_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`pack_sig_c`	LP64	z3*	✅	2s	4s	-50%
`pack_sig_h`	LP64	z3_no_bv_extract*	✅	5s	4s	+25%
`pack_sig_z`	LP64	z3*	✅	1s	5s	-80%
`pack_sk_rho_key_tr_s2`	LP64	z3*	✅	2s	3s	-33%
`pack_sk_s1`	LP64	z3*	✅	2s	1s	+100%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	6s	-50%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	5s	6s	-17%
`pointwise_native_aarch64`	LP64	z3*	✅	3s	5s	-40%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	4s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_add`	LP64	z3*	✅	2s	6s	-67%
`poly_caddq`	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_c`	LP64	z3*	✅	1s	3s	-67%
`poly_caddq_native`	LP64	z3*	✅	3s	4s	-25%
`poly_caddq_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_x86_64`	LP64	z3*	✅	4s	2s	+100%
`poly_challenge`	LP64	z3*	✅	1s	5s	-80%
`poly_chknorm`	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_c`	LP64	z3*	✅	5s	15s	-67%
`poly_chknorm_native`	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_x86_64`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose`	LP64	z3*	✅	1s	3s	-67%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_88_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_c`	LP64	z3*	✅	3s	5s	-40%
`poly_decompose_native`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont`	LP64	z3*	✅	1s	1s	+0%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	5s	12s	-58%
`poly_invntt_tomont_native`	LP64	z3*	✅	1s	5s	-80%
`poly_ntt`	LP64	z3*	✅	1s	3s	-67%
`poly_ntt_c`	LP64	z3_smt_only*	✅	12s	21s	-43%
`poly_ntt_native`	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional`	LP64	z3*	✅	1s	3s	-67%
`poly_permute_bitrev_to_custom_optional_native`	LP64	z3*	✅	2s	5s	-60%
`poly_pointwise_montgomery`	LP64	z3*	✅	3s	4s	-25%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	42s	144s	-71%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	5s	-60%
`poly_power2round`	LP64	z3*	✅	2s	3s	-33%
`poly_reduce`	LP64	z3*	✅	5s	2s	+150%
`poly_shiftl`	LP64	z3*	✅	2s	4s	-50%
`poly_sub`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	z3*	✅	4s	4s	+0%
`poly_uniform_4x`	LP64	z3*	✅	8s	13s	-38%
`poly_uniform_eta`	LP64	z3*	✅	1s	4s	-75%
`poly_uniform_eta_4x`	LP64	z3*	✅	6s	11s	-45%
`poly_uniform_gamma1`	LP64	z3*	✅	1s	4s	-75%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint`	LP64	z3*	✅	1s	1s	+0%
`poly_use_hint_c`	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_x86_64`	LP64	z3*	✅	2s	-	new
`polyeta_pack`	LP64	z3*	✅	1s	4s	-75%
`polyeta_unpack`	LP64	z3*	✅	5s	17s	-71%
`polyt0_pack`	LP64	z3*	✅	3s	4s	-25%
`polyt0_unpack`	LP64	z3*	✅	7s	14s	-50%
`polyt1_pack`	LP64	z3*	✅	2s	3s	-33%
`polyt1_unpack`	LP64	z3*	✅	1s	4s	-75%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	99s	324s	-69%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	15s	38s	-61%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	1s	3s	-67%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	12s	18s	-33%
`polyveck_caddq`	LP64	z3*	✅	7s	8s	-12%
`polyveck_chknorm`	LP64	z3*	✅	3s	3s	+0%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	6s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	6s	9s	-33%
`polyveck_ntt`	LP64	z3*	✅	3s	11s	-73%
`polyveck_pack_eta`	LP64	z3*	✅	6s	6s	+0%
`polyveck_reduce`	LP64	z3*	✅	3s	3s	+0%
`polyveck_unpack_eta`	LP64	z3*	✅	2s	4s	-50%
`polyvecl_chknorm`	LP64	z3*	✅	3s	7s	-57%
`polyvecl_ntt`	LP64	z3*	✅	4s	7s	-43%
`polyvecl_pack_eta`	LP64	z3*	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	5s	-60%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	206s	353s	-42%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	2s	4s	-50%
`polyvecl_unpack_eta`	LP64	z3*	✅	2s	5s	-60%
`polyvecl_unpack_z`	LP64	z3*	✅	3s	4s	-25%
`polyw1_pack`	LP64	z3*	✅	1s	4s	-75%
`polyw1_pack_32`	LP64	z3*	✅	3s	4s	-25%
`polyw1_pack_88`	LP64	z3*	✅	3s	3s	+0%
`polyw1_unpack`	LP64	z3*	✅	2s	-	new
`polyw1_unpack_32`	LP64	z3*	✅	1s	-	new
`polyw1_unpack_88`	LP64	z3*	✅	3s	-	new
`polyz_pack`	LP64	z3*	✅	2s	5s	-60%
`polyz_unpack`	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack_17_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack_c`	LP64	z3*	✅	5s	3s	+67%
`polyz_unpack_native`	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	z3*	✅	1s	4s	-75%
`reduce32`	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	1s	4s	-75%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	5s	-40%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	6s	-50%
`rej_uniform`	LP64	z3*	✅	11s	15s	-27%
`rej_uniform_c`	LP64	z3*	✅	9s	19s	-53%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	1s	5s	-80%
`rej_uniform_eta_native_x86_64`	LP64	z3_smt_only*	✅	1s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	8s	-75%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
`rej_uniform_native_x86_64`	LP64	z3_smt_only*	✅	8s	-	new
`shake128_absorb`	LP64	z3*	✅	3s	4s	-25%
`shake128_finalize`	LP64	z3*	✅	2s	2s	+0%
`shake128_init`	LP64	z3*	✅	1s	1s	+0%
`shake128_release`	LP64	z3*	✅	2s	4s	-50%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	3s	5s	-40%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
`shake256`	LP64	z3*	✅	1s	2s	-50%
`shake256_absorb`	LP64	z3*	✅	5s	2s	+150%
`shake256_finalize`	LP64	z3*	✅	3s	2s	+50%
`shake256_init`	LP64	z3*	✅	3s	2s	+50%
`shake256_release`	LP64	z3*	✅	1s	3s	-67%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	4s	1s	+300%
`sig_unpack_hints`	LP64	z3*	⚠️	27s	3s	+800%
`sign_keypair`	LP64	z3*	✅	7s	4s	+75%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	43s	6s	+617%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	52s	6s	+767%
`sign_signature`	LP64	z3*	✅	5s	5s	+0%
`sign_signature_extmu`	LP64	z3*	✅	3s	4s	-25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	355s	42s	+745%
`sign_signature_pre_hash_internal`	LP64	z3*	✅	3s	5s	-40%
`sign_signature_pre_hash_shake256`	LP64	z3*	✅	4s	6s	-33%
`sign_verify`	LP64	z3*	✅	2s	5s	-60%
`sign_verify_extmu`	LP64	z3*	✅	4s	3s	+33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	594s	97s	+512%
`sign_verify_pre_hash_internal`	LP64	z3*	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	LP64	z3*	✅	3s	3s	+0%
`sk_s1hat_get_poly`	LP64	z3*	✅	1s	3s	-67%
`sk_s2hat_get_poly`	LP64	z3*	✅	2s	3s	-33%
`sk_t0hat_get_poly`	LP64	z3*	✅	2s	4s	-50%
`sys_check_capability`	LP64	z3*	✅	2s	3s	-33%
`unpack_pk_t1`	LP64	z3*	✅	2s	1s	+100%
`unpack_sk`	LP64	z3*	✅	1s	5s	-80%
`unpack_sk_s1hat`	LP64	z3*	✅	1s	2s	-50%
`unpack_sk_s2hat`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_t0hat`	LP64	z3*	✅	2s	7s	-71%
`use_hint`	LP64	z3*	✅	3s	3s	+0%
`yvec_get_poly`	LP64	z3*	✅	2s	4s	-50%
`yvec_init`	LP64	z3*	✅	3s	4s	-25%

mkannwischer added the benchmark label Sep 27, 2026

github-actions Bot reviewed Sep 27, 2026

View reviewed changes

oqs-bot reviewed Sep 27, 2026

View reviewed changes

github-actions Bot reviewed Sep 27, 2026

View reviewed changes

oqs-bot reviewed Sep 27, 2026

View reviewed changes

Conversation

mkannwischer commented Sep 27, 2026

Uh oh!

github-actions Bot left a comment

Choose a reason for hiding this comment

Mac Mini (M1, 2020) benchmarks (opt)

Uh oh!

github-actions Bot left a comment

Choose a reason for hiding this comment

Mac Mini (M1, 2020) benchmarks (no-opt)

Uh oh!

github-actions Bot left a comment

Choose a reason for hiding this comment

Arm Cortex-A76 (Raspberry Pi 5) benchmarks (opt)

Uh oh!

github-actions Bot left a comment

Choose a reason for hiding this comment

Arm Cortex-A76 (Raspberry Pi 5) benchmarks (no-opt)

Uh oh!

github-actions Bot left a comment

Choose a reason for hiding this comment

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Intel Xeon 4th gen (c7i)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

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

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

AMD EPYC 4th gen (c7a)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton5

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

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

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

AMD EPYC 3rd gen (c6a)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton5 (no-opt)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

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

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Intel Xeon 3rd gen (c6i)

Uh oh!

github-actions Bot left a comment

Choose a reason for hiding this comment

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

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

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton4

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton3

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton4 (no-opt)

Uh oh!

oqs-bot left a comment