HOL-Light: Add HOL Light proof and CBMC contracts for x86 poly_caddq

[jakemas]

Resolves #492

Summary

• Created x86 AVX2 poly_caddq HOL Light formal proof. Had to unroll loop, verified no performance changes.
• Add CBMC contract for mld_poly_caddq_avx2 and new poly_caddq_native_x86_64 CBMC proof
• Fix MAP_UNTIL_TARGET_PC in x86_64 mldsa_utils.ml (was matching eventually arm instead of eventually x86)
• both CORRECT and SAFE proofs

Depends on: s2n-bignum #397 (VPCMPGTD instruction model)

HOL-Light / x86_64 HOL Light proof for poly_caddq_avx2_asm.S (pull_request)Successful in 10m

[jakemas]

Benchmark: unrolled vs looped poly_caddq (rdtsc, best of 20 × 100k reps)

Version	Cycles/call
Unrolled (this PR)	37
Looped (original)	37

No performance difference — function is memory-bound. Code size: 876 bytes (unrolled) vs 115 bytes (looped).

[github-actions]

Mac Mini (M1, 2020) benchmarks (opt)

Details

Benchmark suite	Current: 83c172c	Previous: 1b47ba6	Ratio
ML-DSA-44 keypair	46536 cycles	46536 cycles	1
ML-DSA-44 sign	131052 cycles	131050 cycles	1.00
ML-DSA-44 verify	47346 cycles	47346 cycles	1
ML-DSA-65 keypair	81691 cycles	81700 cycles	1.00
ML-DSA-65 sign	215419 cycles	215395 cycles	1.00
ML-DSA-65 verify	79305 cycles	79307 cycles	1.00
ML-DSA-87 keypair	132416 cycles	132417 cycles	1.00
ML-DSA-87 sign	277558 cycles	277443 cycles	1.00
ML-DSA-87 verify	134239 cycles	134252 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: 83c172c	Previous: 1b47ba6	Ratio
ML-DSA-44 keypair	112847 cycles	112799 cycles	1.00
ML-DSA-44 sign	401127 cycles	400982 cycles	1.00
ML-DSA-44 verify	120177 cycles	120122 cycles	1.00
ML-DSA-65 keypair	192913 cycles	192868 cycles	1.00
ML-DSA-65 sign	649933 cycles	649945 cycles	1.00
ML-DSA-65 verify	192945 cycles	192948 cycles	1.00
ML-DSA-87 keypair	318764 cycles	318776 cycles	1.00
ML-DSA-87 sign	828766 cycles	828806 cycles	1.00
ML-DSA-87 verify	326656 cycles	326675 cycles	1.00

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

[oqs-bot]

Intel Xeon 4th gen (c7i)

Details

Benchmark suite	Current: 83c172c	Previous: 1b47ba6	Ratio
ML-DSA-44 keypair	45341 cycles	45511 cycles	1.00
ML-DSA-44 sign	136181 cycles	136341 cycles	1.00
ML-DSA-44 verify	47302 cycles	47440 cycles	1.00
ML-DSA-65 keypair	78737 cycles	79043 cycles	1.00
ML-DSA-65 sign	222332 cycles	222551 cycles	1.00
ML-DSA-65 verify	78083 cycles	77883 cycles	1.00
ML-DSA-87 keypair	125052 cycles	124670 cycles	1.00
ML-DSA-87 sign	276747 cycles	276052 cycles	1.00
ML-DSA-87 verify	122413 cycles	122354 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: 83c172c	Previous: 1b47ba6	Ratio
ML-DSA-44 keypair	94218 cycles	94105 cycles	1.00
ML-DSA-44 sign	329909 cycles	329634 cycles	1.00
ML-DSA-44 verify	98793 cycles	98714 cycles	1.00
ML-DSA-65 keypair	161733 cycles	161653 cycles	1.00
ML-DSA-65 sign	538654 cycles	539237 cycles	1.00
ML-DSA-65 verify	160327 cycles	160249 cycles	1.00
ML-DSA-87 keypair	263770 cycles	264627 cycles	1.00
ML-DSA-87 sign	694878 cycles	695291 cycles	1.00
ML-DSA-87 verify	265915 cycles	265870 cycles	1.00

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

[hanno-becker]

@jakemas We should only have one 'core' spec. Either with just the functional description, or with functional description and bounds. We should have exactly one subroutine spec, with both functional description and bounds -- because that's what we want to be eyeball close to the CBMC spec.

Can you please adjust MLDSA_CADDQ_SUBROUTINE_CORRECT to include bounds? And preferably, not necessarily, also consolidate xx_CORRECT xx_CORRECT_BOUND?

[jakemas]

@jakemas We should only have one 'core' spec. Either with just the functional description, or with functional description and bounds. We should have exactly one subroutine spec, with both functional description and bounds -- because that's what we want to be eyeball close to the CBMC spec.

Can you please adjust MLDSA_CADDQ_SUBROUTINE_CORRECT to include bounds? And preferably, not necessarily, also consolidate xx_CORRECT xx_CORRECT_BOUND?

Ok done. Take a look and see what you think.

[hanno-becker]

Thanks @jakemas, the specs look good now. Two smaller issues remain that should be trivial to address.

[hanno-becker]

Please also adjust the README

[jakemas]

Please also adjust the README

added ty!

[hanno-becker]

Please remove the now-duplicate lemmas from the proof script and use their effective copies from mldsa_specs.ml

[jakemas]

Please remove the now-duplicate lemmas from the proof script and use their effective copies from mldsa_specs.ml

done! thanks!

[hanno-becker]

LGTM if CI passes.