[alex]

Part of #991. Stacked on #2872 (itself on #2870 and #2867); review only the last two commits.

Until now, the P-384 ECDH window's mixed addition R + E called out of line to vg_p384_mul_mod_p and vg_p384_sqr_mod_p, through fprogB of maddJ (8 products and 3 squares). It now runs as one straight-line block of Ops.op field operations, the same inline cores the allocated doublings use.

Changes

Implementation

• Impl/Weierstrass/AArch64/WindowJ.lean. sumJ (and stepJ, windowJ) take an optional block for the mixed addition (maddRD), in place of fprogB of maddJ, the same way they take the doublings. Cfg.mulJ4 and exchangeJ4 pass it through. Every other caller keeps the default, none, so their code is unchanged.
• Impl/P384/EcdhMadd.lean. madd := (maddJ K.S K.R K.E K.D).flatMap Ops.op. It uses x1–x17 and x21–x25; ECDH already saves x21–x25.
• vg_ecdh_p384 passes madd.

Proofs

• Proof/Weierstrass/AArch64/WinJStep.lean.
  • MaddSpec is what a window's mixed addition must do: keep the registers outside clob ++ winSaved and the memory outside the loop's slots, and leave D holding maddJF of R and E.
  • MaddOk lifts it to the optional block.
  • sumJ_ok takes a block with MaddOk; the default fprogB program meets it through winN_ok.
  • winStepJ_ok, windowJ_ok and mulJ4_ok pass it on.
• Proof/P384/EcdhMadd.lean. madd_ok is ofN_ok's argument with Ops.fprog_ok in place of fprogB_ok: the same slots, frame and values (ofN_run, maddJN_run).

No certificate: the block is not register-allocated. llvm-mca (N2) puts the allocator's output at 856 cycles against 822 for the inline block, so allocation would cost time here, unlike the doubling.

No changes to TCB/ or Spec/.

Speed

Neoverse N2, run 39288463032, against #2872's head (73332c3):

Benchmark	default	VG_CPU_FEATURES=none
ecdh_p384	−1.3% (169.48 → 167.25 µs)	−1.3%
ec_p384_public_key	+0.2%	+0.1%
ecdsa_p384_sha384_sign 64 B / 1 KiB / 16 KiB	−0.1% / 0.0% / +0.1%	+0.1% / +0.1% / 0.0%
ecdsa_p384_sha384_verify 64 B / 1 KiB / 16 KiB	−0.1%	−0.1%

Sign and verify don't use this code; their changes are noise.

The whole stack against main (da70d00), run 39288468635:

• ECDH: −11.3% (188.64 → 167.31 µs), about 0.90× aws-lc-rs's 186.6 µs.
• Verify: −8.1% to −8.7%.
• Sign: within ±0.1%.

Checks

These pass locally:

• full lake build
• the emitter (only src/asm/aarch64/ecdh_p384.rs changes)
• check_lean_imports, check_lean_modules, check_registrations, check_lean_speed, check_vectors, check_arch_gates, check_variants, check_mcdt
• algorithms_table.py (table unchanged)
• the ECDH and P-384 tests on aarch64 under qemu, Wycheproof included

---

Generated by Claude Code