[alex]

Part of #991.

On N2, P-384 ECDH was the only rustls primitive where we trailed aws-lc-rs (0.99×). This is the first PR of a series that register-allocates P-384's ECDH, following P-256's.

Before this PR, every field operation in the window's doublings was an out-of-line call to vg_p384_mul_mod_p or vg_p384_sqr_mod_p, with its operands in memory. Each doubling is now one straight-line block, allocated into registers and checked by a certificate, the way P-256's are.

Changes

Implementation

• Impl/P384/Ops.lean. P-384's field operations inline on the working space at x0:
  • The _alt product and square cores (P384Mul, P384Sqr, adapted from s2n-bignum) load their operands from slots, not through the functions' pointers.
  • The reduction constants come from the modulus's slot, since the allocator follows only loads and register operations.
• Impl/P384/EcdhDouble.lean. The window's doubling (dblJ) as a straight line of those operations, in both directions (R→D, D→R).
• Allocation. The existing untrusted allocator (Impl/P256/VerifyRegisters.lean) allocates them, run by lean/GenerateP384Ecdh.lean; its output is the literal Impl/P384/EcdhAllocatedCode.lean.
  • Registers: x1–x17 and x21–x25. ECDH already saves x21–x25 on entry and restores them on exit.
  • Spills go to slots the window doesn't read during its doublings: the entry E, the addition's temporaries, and tmp.
• Wiring. WinCfg.windowJ (and quadJ, stepJ, stepLast) take an optional pair of doubling blocks in place of fprogB of double. vg_ecdh_p384 passes the allocated ones.
• Allocator. VerifyRegisters.allocate takes its spill slots as a parameter. The default is P-256's area, so P-256's literals are unchanged.

Proofs

• Proof/P384/Ops.lean. The inline product and square are correct and change only clobX, i.e. clob 6 plus x21–x25. They reuse P384Mul.prod_ok and P384Sqr.sq_ok, generalized to any base register and offset (prodAt_ok, sqAt_ok); the functions' code and proofs are instances of those.
• Proof/P384/EcdhDouble/Raw.lean. The raw doubling meets what winN_ok says of the call-based one.
• Proof/P384/EcdhDouble/Certificate.lean. For each direction, the allocated block agrees with the raw one on every slot except the spills (Forward kernel, decide +kernel, about 4 s each). It changes only regs and its output and spill slots, and is constant-time.
• Proof/P384/EcdhDouble/Verified.lean. The allocated blocks meet the window's new DblSpec. WinJStep, WinJLoop and MulJ4 take the blocks with DblsOk; the default fprogB doubling meets it too (dblN_spec).
• combClob 6 (the window's and comb's register frame, proof only) now includes x21–x25 (winSaved). The ECDH and ECDSA entry code saves and restores them; no emitted code changes.

No changes to TCB/ or Spec/.

Speed

Neoverse N2, run 39261068075, compared with main (e5ec778):

Benchmark	Base	Head	Change
ecdh_p384	188.92 µs	174.75 µs	−7.5%
ec_p384_public_key	44.88 µs	44.85 µs	−0.1%
ecdsa_p384_sha384_sign 64 B / 1 KiB / 16 KiB	50.50 / 51.22 / 62.46 µs	50.36 / 51.13 / 62.35 µs	−0.2% to −0.3%
ecdsa_p384_sha384_verify 64 B / 1 KiB / 16 KiB	208.37 / 210.28 / 221.57 µs	208.58 / 210.46 / 221.81 µs	+0.1%

• ECDH P-384 is now about 1.07× aws-lc-rs's (186.6 µs on N2).
• Sign and verify don't use this code; their changes are noise.
• Next in the series: the window's mixed addition and selection, allocated the same way.

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, including P-384's CAVP and Wycheproof tests

---

Generated by Claude Code

[reaperhulk]

rebase this stack and handle the new visibility rules

[alex]

Done: I rebased the whole stack (#2867 → #2870 → #2872 → #2874) onto main at 6135dd5 and force-pushed it.

Each PR now ends with a commit that adapts its own files to the private-import rules: import for what is used only in proofs, public import of the defining module where a statement needs it (NafDblOk, RawSlots, Unch, Inputs, dblJF).

For each PR on its own base, all of these pass locally:

• a full lake build
• Emit.lean --check (src/asm unchanged)
• check_lean_public_imports.py --base <PR base> on the PR's modules
• the other check_lean_* scripts

---

Generated by Claude Code