nix: Add HOL-Light cross shells #1441

hanno-becker · 2025-12-31T05:25:18Z

As a first step towards developing and checking HOL-Light proofs for architectures different from the host architecture, this commit adds new nix shells for HOL-Light + cross toolchains.

As a first step towards developing and checking HOL-Light proofs for architectures different from the host architecture, this commit adds new nix shells for HOL-Light + cross toolchains. Signed-off-by: Hanno Becker <[email protected]>

mkannwischer

Thanks! I tested that I can enter the hol_light-cross-aarch64 shell on x86 Linux and run hol.sh there without any issues.
Have not tried to run it on MacOS / AArch64.

oqs-bot

Mac Mini (M1, 2020) benchmarks

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`12327` cycles	`12315` cycles	`1.00`
`ML-KEM-512 encaps`	`15032` cycles	`14989` cycles	`1.00`
`ML-KEM-512 decaps`	`19609` cycles	`19558` cycles	`1.00`
`ML-KEM-768 keypair`	`21395` cycles	`21085` cycles	`1.01`
`ML-KEM-768 encaps`	`24009` cycles	`23869` cycles	`1.01`
`ML-KEM-768 decaps`	`30579` cycles	`30436` cycles	`1.00`
`ML-KEM-1024 keypair`	`30376` cycles	`30381` cycles	`1.00`
`ML-KEM-1024 encaps`	`34644` cycles	`34656` cycles	`1.00`
`ML-KEM-1024 decaps`	`44269` cycles	`44268` cycles	`1.00`

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

oqs-bot

ppc64le (POWER10) benchmarks

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`60518` cycles	`58673` cycles	`1.03`
`ML-KEM-512 encaps`	`72637` cycles	`71511` cycles	`1.02`
`ML-KEM-512 decaps`	`92572` cycles	`91342` cycles	`1.01`
`ML-KEM-768 keypair`	`102386` cycles	`95704` cycles	`1.07`
`ML-KEM-768 encaps`	`117564` cycles	`111480` cycles	`1.05`
`ML-KEM-768 decaps`	`144292` cycles	`136907` cycles	`1.05`
`ML-KEM-1024 keypair`	`152871` cycles	`155480` cycles	`0.98`
`ML-KEM-1024 encaps`	`172228` cycles	`174085` cycles	`0.99`
`ML-KEM-1024 decaps`	`204033` cycles	`205560` cycles	`0.99`

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: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`60518` cycles	`58673` cycles	`1.03`
`ML-KEM-768 keypair`	`102386` cycles	`95704` cycles	`1.07`
`ML-KEM-768 encaps`	`117564` cycles	`111480` cycles	`1.05`
`ML-KEM-768 decaps`	`144292` cycles	`136907` cycles	`1.05`

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

oqs-bot

Intel Xeon 4th gen (c7i)

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`9748` cycles	`9628` cycles	`1.01`
`ML-KEM-512 encaps`	`11426` cycles	`11272` cycles	`1.01`
`ML-KEM-512 decaps`	`15620` cycles	`15154` cycles	`1.03`
`ML-KEM-768 keypair`	`16606` cycles	`16416` cycles	`1.01`
`ML-KEM-768 encaps`	`18171` cycles	`17900` cycles	`1.02`
`ML-KEM-768 decaps`	`23691` cycles	`23504` cycles	`1.01`
`ML-KEM-1024 keypair`	`22465` cycles	`22416` cycles	`1.00`
`ML-KEM-1024 encaps`	`24553` cycles	`24531` cycles	`1.00`
`ML-KEM-1024 decaps`	`32121` cycles	`32315` cycles	`0.99`

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

oqs-bot

⚠️ Performance Alert ⚠️

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

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 decaps`	`15620` cycles	`15154` 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: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`16881` cycles	`16914` cycles	`1.00`
`ML-KEM-512 encaps`	`18623` cycles	`18601` cycles	`1.00`
`ML-KEM-512 decaps`	`24024` cycles	`24047` cycles	`1.00`
`ML-KEM-768 keypair`	`28708` cycles	`28516` cycles	`1.01`
`ML-KEM-768 encaps`	`29892` cycles	`29604` cycles	`1.01`
`ML-KEM-768 decaps`	`37766` cycles	`37428` cycles	`1.01`
`ML-KEM-1024 keypair`	`41431` cycles	`42781` cycles	`0.97`
`ML-KEM-1024 encaps`	`43455` cycles	`44067` cycles	`0.99`
`ML-KEM-1024 decaps`	`53995` cycles	`54556` cycles	`0.99`

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

oqs-bot

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

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`28948` cycles	`29235` cycles	`0.99`
`ML-KEM-512 encaps`	`35793` cycles	`36624` cycles	`0.98`
`ML-KEM-512 decaps`	`44826` cycles	`45150` cycles	`0.99`
`ML-KEM-768 keypair`	`47762` cycles	`45945` cycles	`1.04`
`ML-KEM-768 encaps`	`57519` cycles	`55632` cycles	`1.03`
`ML-KEM-768 decaps`	`70711` cycles	`69438` cycles	`1.02`
`ML-KEM-1024 keypair`	`72128` cycles	`72921` cycles	`0.99`
`ML-KEM-1024 encaps`	`84596` cycles	`84816` cycles	`1.00`
`ML-KEM-1024 decaps`	`101848` cycles	`102882` cycles	`0.99`

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

oqs-bot

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Intel Xeon 4th gen (c7i) (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-768 keypair`	`47762` cycles	`45945` cycles	`1.04`
`ML-KEM-768 encaps`	`57519` cycles	`55632` cycles	`1.03`

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

oqs-bot

Intel Xeon 3rd gen (c6i)

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`16367` cycles	`16258` cycles	`1.01`
`ML-KEM-512 encaps`	`18660` cycles	`18596` cycles	`1.00`
`ML-KEM-512 decaps`	`25332` cycles	`25262` cycles	`1.00`
`ML-KEM-768 keypair`	`28100` cycles	`28085` cycles	`1.00`
`ML-KEM-768 encaps`	`30118` cycles	`32039` cycles	`0.94`
`ML-KEM-768 decaps`	`39600` cycles	`39402` cycles	`1.01`
`ML-KEM-1024 keypair`	`38115` cycles	`37718` cycles	`1.01`
`ML-KEM-1024 encaps`	`40627` cycles	`40501` cycles	`1.00`
`ML-KEM-1024 decaps`	`54306` cycles	`54286` 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: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`11686` cycles	`11923` cycles	`0.98`
`ML-KEM-512 encaps`	`13150` cycles	`13466` cycles	`0.98`
`ML-KEM-512 decaps`	`18047` cycles	`18400` cycles	`0.98`
`ML-KEM-768 keypair`	`20741` cycles	`20330` cycles	`1.02`
`ML-KEM-768 encaps`	`21552` cycles	`21357` cycles	`1.01`
`ML-KEM-768 decaps`	`28743` cycles	`28411` cycles	`1.01`
`ML-KEM-1024 keypair`	`28063` cycles	`27660` cycles	`1.01`
`ML-KEM-1024 encaps`	`30217` cycles	`29469` cycles	`1.03`
`ML-KEM-1024 decaps`	`39807` cycles	`38947` cycles	`1.02`

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

oqs-bot

Graviton4

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`17670` cycles	`17667` cycles	`1.00`
`ML-KEM-512 encaps`	`20669` cycles	`20530` cycles	`1.01`
`ML-KEM-512 decaps`	`27104` cycles	`26961` cycles	`1.01`
`ML-KEM-768 keypair`	`30278` cycles	`29973` cycles	`1.01`
`ML-KEM-768 encaps`	`33019` cycles	`32764` cycles	`1.01`
`ML-KEM-768 decaps`	`42212` cycles	`41949` cycles	`1.01`
`ML-KEM-1024 keypair`	`43911` cycles	`43863` cycles	`1.00`
`ML-KEM-1024 encaps`	`48916` cycles	`48796` cycles	`1.00`
`ML-KEM-1024 decaps`	`61546` cycles	`61314` cycles	`1.00`

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

oqs-bot

Graviton3

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`18721` cycles	`18721` cycles	`1`
`ML-KEM-512 encaps`	`22014` cycles	`21988` cycles	`1.00`
`ML-KEM-512 decaps`	`29045` cycles	`28923` cycles	`1.00`
`ML-KEM-768 keypair`	`31965` cycles	`31697` cycles	`1.01`
`ML-KEM-768 encaps`	`35063` cycles	`34905` cycles	`1.00`
`ML-KEM-768 decaps`	`45073` cycles	`44910` cycles	`1.00`
`ML-KEM-1024 keypair`	`46364` cycles	`46309` cycles	`1.00`
`ML-KEM-1024 encaps`	`51705` cycles	`51632` cycles	`1.00`
`ML-KEM-1024 decaps`	`65230` cycles	`65063` 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: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`59796` cycles	`59463` cycles	`1.01`
`ML-KEM-512 encaps`	`67434` cycles	`67187` cycles	`1.00`
`ML-KEM-512 decaps`	`86101` cycles	`86027` cycles	`1.00`
`ML-KEM-768 keypair`	`101986` cycles	`96957` cycles	`1.05`
`ML-KEM-768 encaps`	`113385` cycles	`110301` cycles	`1.03`
`ML-KEM-768 decaps`	`140424` cycles	`137318` cycles	`1.02`
`ML-KEM-1024 keypair`	`155073` cycles	`153918` cycles	`1.01`
`ML-KEM-1024 encaps`	`172974` cycles	`173219` cycles	`1.00`
`ML-KEM-1024 decaps`	`209124` cycles	`210030` 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 'Arm Cortex-A55 (Snapdragon 888) benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-768 keypair`	`101986` cycles	`96957` cycles	`1.05`

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

oqs-bot

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

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`40362` cycles	`40103` cycles	`1.01`
`ML-KEM-512 encaps`	`48611` cycles	`48452` cycles	`1.00`
`ML-KEM-512 decaps`	`62831` cycles	`62695` cycles	`1.00`
`ML-KEM-768 keypair`	`65443` cycles	`63586` cycles	`1.03`
`ML-KEM-768 encaps`	`75684` cycles	`74808` cycles	`1.01`
`ML-KEM-768 decaps`	`94248` cycles	`93418` cycles	`1.01`
`ML-KEM-1024 keypair`	`96040` cycles	`95201` cycles	`1.01`
`ML-KEM-1024 encaps`	`110552` cycles	`109402` cycles	`1.01`
`ML-KEM-1024 decaps`	`133018` cycles	`132405` 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: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`36703` cycles	`36858` cycles	`1.00`
`ML-KEM-512 encaps`	`43123` cycles	`43435` cycles	`0.99`
`ML-KEM-512 decaps`	`55812` cycles	`56449` cycles	`0.99`
`ML-KEM-768 keypair`	`60087` cycles	`58948` cycles	`1.02`
`ML-KEM-768 encaps`	`68320` cycles	`67978` cycles	`1.01`
`ML-KEM-768 decaps`	`85262` cycles	`85323` cycles	`1.00`
`ML-KEM-1024 keypair`	`88825` cycles	`89213` cycles	`1.00`
`ML-KEM-1024 encaps`	`98968` cycles	`99538` cycles	`0.99`
`ML-KEM-1024 decaps`	`120542` cycles	`121730` cycles	`0.99`

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

oqs-bot

Graviton4 (no-opt)

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`35457` cycles	`35454` cycles	`1.00`
`ML-KEM-512 encaps`	`40224` cycles	`40517` cycles	`0.99`
`ML-KEM-512 decaps`	`51282` cycles	`51293` cycles	`1.00`
`ML-KEM-768 keypair`	`58912` cycles	`57158` cycles	`1.03`
`ML-KEM-768 encaps`	`65496` cycles	`65304` cycles	`1.00`
`ML-KEM-768 decaps`	`79803` cycles	`79761` cycles	`1.00`
`ML-KEM-1024 keypair`	`87998` cycles	`88019` cycles	`1.00`
`ML-KEM-1024 encaps`	`97153` cycles	`97623` cycles	`1.00`
`ML-KEM-1024 decaps`	`116170` cycles	`116469` 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 'Graviton4 (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-768 keypair`	`58912` cycles	`57158` cycles	`1.03`

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

oqs-bot

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

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`46480` cycles	`47209` cycles	`0.98`
`ML-KEM-512 encaps`	`55482` cycles	`55680` cycles	`1.00`
`ML-KEM-512 decaps`	`70750` cycles	`71125` cycles	`0.99`
`ML-KEM-768 keypair`	`76808` cycles	`73294` cycles	`1.05`
`ML-KEM-768 encaps`	`87749` cycles	`85193` cycles	`1.03`
`ML-KEM-768 decaps`	`107756` cycles	`105454` cycles	`1.02`
`ML-KEM-1024 keypair`	`112578` cycles	`112701` cycles	`1.00`
`ML-KEM-1024 encaps`	`126257` cycles	`125609` cycles	`1.01`
`ML-KEM-1024 decaps`	`152440` cycles	`151800` cycles	`1.00`

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

oqs-bot

⚠️ Performance Alert ⚠️

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

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-768 keypair`	`76808` cycles	`73294` cycles	`1.05`
`ML-KEM-768 encaps`	`87749` cycles	`85193` cycles	`1.03`

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

oqs-bot

Graviton2

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`28389` cycles	`28267` cycles	`1.00`
`ML-KEM-512 encaps`	`34240` cycles	`34164` cycles	`1.00`
`ML-KEM-512 decaps`	`44577` cycles	`44407` cycles	`1.00`
`ML-KEM-768 keypair`	`48318` cycles	`47750` cycles	`1.01`
`ML-KEM-768 encaps`	`54472` cycles	`54106` cycles	`1.01`
`ML-KEM-768 decaps`	`68790` cycles	`68471` cycles	`1.00`
`ML-KEM-1024 keypair`	`70634` cycles	`70507` cycles	`1.00`
`ML-KEM-1024 encaps`	`79098` cycles	`78979` cycles	`1.00`
`ML-KEM-1024 decaps`	`98895` cycles	`98520` cycles	`1.00`

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

oqs-bot

Graviton3 (no-opt)

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`38964` cycles	`39038` cycles	`1.00`
`ML-KEM-512 encaps`	`44630` cycles	`44875` cycles	`0.99`
`ML-KEM-512 decaps`	`56733` cycles	`56825` cycles	`1.00`
`ML-KEM-768 keypair`	`64892` cycles	`62569` cycles	`1.04`
`ML-KEM-768 encaps`	`71966` cycles	`71789` cycles	`1.00`
`ML-KEM-768 decaps`	`87819` cycles	`88170` cycles	`1.00`
`ML-KEM-1024 keypair`	`96246` cycles	`96214` cycles	`1.00`
`ML-KEM-1024 encaps`	`106298` cycles	`106763` cycles	`1.00`
`ML-KEM-1024 decaps`	`126939` cycles	`127072` 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 'Graviton3 (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-768 keypair`	`64892` cycles	`62569` cycles	`1.04`

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

oqs-bot

Graviton2 (no-opt)

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`59244` cycles	`59191` cycles	`1.00`
`ML-KEM-512 encaps`	`68645` cycles	`68509` cycles	`1.00`
`ML-KEM-512 decaps`	`87468` cycles	`87152` cycles	`1.00`
`ML-KEM-768 keypair`	`99102` cycles	`95538` cycles	`1.04`
`ML-KEM-768 encaps`	`111051` cycles	`109386` cycles	`1.02`
`ML-KEM-768 decaps`	`136167` cycles	`134652` cycles	`1.01`
`ML-KEM-1024 keypair`	`148685` cycles	`146689` cycles	`1.01`
`ML-KEM-1024 encaps`	`164519` cycles	`162476` cycles	`1.01`
`ML-KEM-1024 decaps`	`195822` cycles	`193998` cycles	`1.01`

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

oqs-bot

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Graviton2 (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-768 keypair`	`99102` cycles	`95538` cycles	`1.04`

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

oqs-bot

Arm Cortex-A76 (Raspberry Pi 5) benchmarks

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`28319` cycles	`28270` cycles	`1.00`
`ML-KEM-512 encaps`	`34294` cycles	`34171` cycles	`1.00`
`ML-KEM-512 decaps`	`44519` cycles	`44383` cycles	`1.00`
`ML-KEM-768 keypair`	`48341` cycles	`47760` cycles	`1.01`
`ML-KEM-768 encaps`	`54298` cycles	`54098` cycles	`1.00`
`ML-KEM-768 decaps`	`68826` cycles	`68450` cycles	`1.01`
`ML-KEM-1024 keypair`	`70573` cycles	`70463` cycles	`1.00`
`ML-KEM-1024 encaps`	`79156` cycles	`78939` cycles	`1.00`
`ML-KEM-1024 decaps`	`98847` cycles	`98534` 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: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`52019` cycles	`50772` cycles	`1.02`
`ML-KEM-512 encaps`	`60850` cycles	`58932` cycles	`1.03`
`ML-KEM-512 decaps`	`77590` cycles	`75200` cycles	`1.03`
`ML-KEM-768 keypair`	`87303` cycles	`87254` cycles	`1.00`
`ML-KEM-768 encaps`	`95147` cycles	`96237` cycles	`0.99`
`ML-KEM-768 decaps`	`117799` cycles	`118896` cycles	`0.99`
`ML-KEM-1024 keypair`	`131871` cycles	`131021` cycles	`1.01`
`ML-KEM-1024 encaps`	`143755` cycles	`143815` cycles	`1.00`
`ML-KEM-1024 decaps`	`174260` cycles	`175209` cycles	`0.99`

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

oqs-bot

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Arm Cortex-A72 (Raspberry Pi 4) benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 encaps`	`60850` cycles	`58932` cycles	`1.03`
`ML-KEM-512 decaps`	`77590` cycles	`75200` cycles	`1.03`

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

oqs-bot

SpacemiT K1 8 (Banana Pi F3) benchmarks

Details

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-512 keypair`	`155062` cycles	`154986` cycles	`1.00`
`ML-KEM-512 encaps`	`163322` cycles	`162984` cycles	`1.00`
`ML-KEM-512 decaps`	`206583` cycles	`206175` cycles	`1.00`
`ML-KEM-768 keypair`	`260790` cycles	`249927` cycles	`1.04`
`ML-KEM-768 encaps`	`275737` cycles	`269261` cycles	`1.02`
`ML-KEM-768 decaps`	`337769` cycles	`332637` cycles	`1.02`
`ML-KEM-1024 keypair`	`395373` cycles	`395350` cycles	`1.00`
`ML-KEM-1024 encaps`	`422318` cycles	`423249` cycles	`1.00`
`ML-KEM-1024 decaps`	`507278` cycles	`505626` 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 'SpacemiT K1 8 (Banana Pi F3) benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `9cb9ec9`	Previous: `e379df7`	Ratio
`ML-KEM-768 keypair`	`260790` cycles	`249927` cycles	`1.04`

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

- Ported from pq-code-package/mlkem-native#1441 Signed-off-by: Liam Fisher <[email protected]>

hanno-becker requested a review from a team as a code owner December 31, 2025 05:25

hanno-becker added enhancement New feature or request hol-light nix labels Dec 31, 2025

hanno-becker force-pushed the hol_light_cross_shell branch from 461bee7 to 59338ef Compare December 31, 2025 05:27

hanno-becker requested a review from mkannwischer December 31, 2025 05:31

nix: Add HOL-Light cross shells

9cb9ec9

As a first step towards developing and checking HOL-Light proofs for architectures different from the host architecture, this commit adds new nix shells for HOL-Light + cross toolchains. Signed-off-by: Hanno Becker <[email protected]>

hanno-becker force-pushed the hol_light_cross_shell branch from 59338ef to 9cb9ec9 Compare December 31, 2025 05:35

mkannwischer approved these changes Dec 31, 2025

View reviewed changes

hanno-becker merged commit 0c6c7e6 into main Dec 31, 2025
424 checks passed

hanno-becker deleted the hol_light_cross_shell branch December 31, 2025 07:19

mkannwischer added the needs-mldsa-native-port label Jan 2, 2026

oqs-bot reviewed Jan 2, 2026

View reviewed changes

mkannwischer mentioned this pull request Jan 5, 2026

Port cross-compilation support for HOL-Light pq-code-package/mldsa-native#840

Closed

mkannwischer removed the needs-mldsa-native-port label Jan 7, 2026

This was referenced Jan 11, 2026

Port cross-compilation support for HOL-Light from mlkem pq-code-package/mldsa-native#871

Closed

HOL-Light: Allow cross-generation of byte code pq-code-package/mldsa-native#872

Merged

mkannwischer pushed a commit to pq-code-package/mldsa-native that referenced this pull request Jan 12, 2026

nix: Add HOL-Light cross shells

d1304ec

- Ported from pq-code-package/mlkem-native#1441 Signed-off-by: Liam Fisher <[email protected]>

nix: Add HOL-Light cross shells #1441

nix: Add HOL-Light cross shells #1441

Uh oh!

Conversation

hanno-becker commented Dec 31, 2025

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Mac Mini (M1, 2020) benchmarks

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

ppc64le (POWER10) benchmarks

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

⚠️ Performance Alert ⚠️

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

⚠️ Performance Alert ⚠️

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

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

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

⚠️ Performance Alert ⚠️

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Intel Xeon 3rd gen (c6i)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

AMD EPYC 4th gen (c7a)

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

Arm Cortex-A55 (Snapdragon 888) benchmarks

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

⚠️ Performance Alert ⚠️

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

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

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton4 (no-opt)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment