[alex]

Decapsulation's decryption on AArch64 now runs with 16-bit coefficients, as keygen, encaps and the re-encryption already do. It uses #3046's vg_mlkem16_ntt, and it deletes the u32 decrypt path, which nothing else used.

What changes

• Optimized.decryptM:
  • Each row of u is decoded and decompressed into PP with 32 bits, as before.
  • A new inline pass, Narrow16.narrow, narrows the row to 16 bits at yOff i. Per eight coefficients it does two ldr q, one uzp1 .8h and one str q, in 32 iterations.
  • The row is then transformed by a call of vg_mlkem16_ntt.
  • ŝ is decoded with 16 bits (Codec12W) into the consumed first matrix row.
  • The rest uses the 16-bit pieces encapsulation already uses: the fused dot product (DotW), the inverse transform (invW), then a widen into PP for the subtraction from v and the compression of m'.
• New module Ops16: the small 16-bit helpers (addWAt, widenAt, dec12WAt, enc12WAt, dotAt, plus the new narrowAt) move here from Kem16, so that Optimized can use them without an import cycle. No names change.
• Deleted (now unused):
  • Impl: ReadonlyDecrypt, and the inline u32 readonly transforms Readonly.fwd/inv with their nttAt/nttInvAt/nttAtWith/nttInvAtWith wrappers.
  • Proofs of those transforms:
    • Ntt16/Readonly Fwd/Inv/Contract, nttAtWith_ok, KemReadonlyTransform;
    • NttR.fwd_run/inv_run with their checks and literals.
  • The u32 dot product's proofs (Dot/Core, Loop, Setup, LoopInput, KemDot).
  • The u32 decode (KemDecode, decoded_ready, DecryptU) and the old decrypt proofs (DecryptReadonlyU/Tail).
  • What stays: the out-of-line u32 vg_mlkem_ntt/vg_mlkem_inv_ntt and the tops' table constants, which other code still uses.

Proofs

• Narrow16.narrow_ok (mirrors Widen16.widen_ok): lanes_load and vhalf_perm_h8 give the low halfwords, and CoeffsInW.write16 the stores.
• KEM-level wrappers: Kem.narrowW_ok, and Kem.nttW_ok for the call of vg_mlkem16_ntt from offsets of x28.
• Optimized/DecryptW.lean:
  • DInvW, the 16-bit counterpart of DInv;
  • uW_step/uW_all for the rows of û';
  • m_tailW for the tail: inverse NTT, widen, decode-decompress of v, sub, compress.
• fused_m_ok keeps its statement: it is re-proven by uW_all, decode_stepW, decoded_readyW, fusedW_ok and m_tailW, so DecryptStart and everything above it are unchanged.
• Optimized/Taints.lean: the deStart taint checks list VG_MLKEM16_NTT_ZETAS, since decryption now calls vg_mlkem16_ntt. TopTiming's restSymbols already lists it.

Benchmarks

Gate (set by the coordinating session): decaps at least 1% faster on its own and at least 2% faster together with #3046; keygen and encaps no slower than 0.7%.

Run 39693821950 on N2 (arches=aarch64, cpu_features=-, modules=mlkem768 mlkem1024), against #3046's head 7040c17. It ran on this commit before its restack onto main (fef1e5a). The restack only brought in #3025 and #3029, which do not touch AArch64 ML-KEM. Fastest of 8 copies per side; spread ≤ 0.2%.

Benchmark	Base	Head	Change
mlkem768_keygen	12.28 µs	12.28 µs	0.0%
mlkem768_encaps	12.78 µs	12.78 µs	0.0%
mlkem768_encaps_from_bytes	12.99 µs	12.98 µs	0.0%
mlkem768_decaps	14.76 µs	14.48 µs	1.9% faster
mlkem1024_keygen	19.43 µs	19.42 µs	0.0%
mlkem1024_encaps	19.58 µs	19.59 µs	0.0%
mlkem1024_encaps_from_bytes	19.86 µs	19.85 µs	0.0%
mlkem1024_decaps	22.31 µs	21.93 µs	1.7% faster

Together with #3046's 1.3% on decaps, that is about 3.2% (768) and 3.0% (1024). The gate is met.

Checks

• Full lake build and Emit.lean --check pass on the restacked commit. src/asm/aarch64/mlkem768.rs and mlkem1024.rs are regenerated, about 3,000 fewer lines net.
• cargo test for aarch64-unknown-linux-gnu under qemu-aarch64 -cpu max, with Wycheproof: all ML-KEM tests pass, both by default and with VG_CPU_FEATURES=none.
• The Python checks pass:
  • check_lean_imports, check_lean_modules and check_lean_public_imports (with its suggested fixes applied);
  • check_registrations and check_lean_speed;
  • check_vectors and check_arch_gates;
  • check_variants and check_mcdt.
• cargo fmt --check passes.

---

Generated by Claude Code

[alex]

The benched commit fef1e5a and this head 16ca5f1 generate the same AArch64 code: git diff fef1e5a 16ca5f1 -- src/asm/aarch64 is empty. Everything else the restack changed comes from main (#3025, #3029) and touches neither AArch64 nor ML-KEM. So run 39693821950 measured exactly this PR's code.

---

Generated by Claude Code