[alex]

Part of #991.

This follows up #2772 (the NEON codecs for ML-KEM-768) for ML-KEM-1024's widths. On AArch64, vg_mlkem1024_compress_encode and vg_mlkem1024_decode_decompress were scalar loops that handled one coefficient at a time. Both are now vector loops that handle 32 coefficients per iteration, reusing the 768 codecs' loop framework (Proof/MlKem/AArch64/CodecV/).

Changes

Compress (Impl/MlKem1024/AArch64/Compress.lean)

• Compression is (x · mul + add) >> 19 mod 2ᵈ, the same as for 768.
  • Width gains an add field: width5 = ⟨5, 8, 5, 5040, 261888⟩ and width11 = ⟨11, 8, 11, 322542, 261888⟩.
  • Each constant is proven against Compress_d for every x < q by compress1024_eq.
• d = 5: packs pairs of lanes into 10, 20 and 40 bits, as d = 10 does for 768. TBL then gathers the 20 bytes.
• d = 11: packs into two doublewords of 44 bits per 8 lanes, merged into 88-bit groups (merge88). Three TBLs gather the 44 bytes, which are stored as 16 + 16 + 8 + 4 bytes.

Decompress

• d = 5: TBL loads each group's five bytes into a doubleword. These are split into 10-bit values (ddSplit, now shared with 768's d = 10) and then into 5-bit values (dd5Quarter).
• d = 11: TBL loads each group's 11 bytes into a register. USHR/SHL/EXT/ORR/ZIP1 split its 88 bits into two 44-bit doublewords (dd11Group), which ddSplit splits into 11-bit values.

Shared framework (768)

These changes generalize the 768 framework to more widths. 768's generated code is unchanged.

• WOk states compression as (x · mul + add) / 2¹⁹ mod 2ᵈ and allows d ≤ 11.
• cmpV_ok takes the bounds mul ≤ 322542 and add < 2¹⁹.
• The setup frames of vloop_ok and dloop_ok leave room for the extra index and constant registers (v20–v23).
• ddSplit_ok is factored out of Dd10.lean, for b = 10 or 11.

Proofs

• New files in Proof/MlKem1024/AArch64/CodecV/, one iteration per width and direction: Ce5, Ce11, Dd5, Dd11, their *Step files, Dword88 and Widths.
• The top-level files keep their contracts (compressEncodeAArch64, decodeDecompressAArch64) and their theorem names.
• Stream.lean is deleted: only the scalar proofs used it.

No changes to TCB/ or Spec/. The new code uses only instructions already in the AArch64 model.

Speed

Neoverse N2, run 39238659055, compared with main (dbfa7dd), with the fastest of the copies per side:

Benchmark	default / sha3	neon / none
mlkem1024_decaps	29.90 → 29.28 µs (−2.1%)	42.10 → 41.50 µs (−1.4%)
mlkem1024_encaps	23.17 → 22.89 µs (−1.2%)	37.50 → 37.23 µs (−0.7%)
mlkem1024_encaps_from_bytes	23.87 → 23.60 µs (−1.1%)	38.20 → 37.93 µs (−0.7%)
mlkem1024_keygen	24.25 → 24.25 µs (0.0%)	34.98 → 34.99 µs (0.0%)

• No row is slower. Keygen does not call these codecs, and its copies' ranges overlap.
• The gain is smaller than my estimate (~10–17%) from llvm-mca's per-call cycle counts. The scalar codecs were a smaller share of encaps and decaps than that estimate assumed.

Checks

These pass locally:

• full lake build
• the emitter (only src/asm/aarch64/mlkem1024.rs changes)
• check_lean_imports, check_lean_modules, check_registrations, check_lean_speed, check_vectors, check_arch_gates, check_variants, check_mcdt, cpu_tests.py lint
• algorithms_table.py (table unchanged)
• cargo fmt, clippy
• the ML-KEM tests on aarch64 under qemu, including ML-KEM-1024's ACVP and Wycheproof tests

---

Generated by Claude Code