[alex]

Part of #991. Stacked on #2867.

P-384 ECDSA verification's [v]Q (the public width-five NAF, PubNaf.window) doubles with the same window slots as ECDH. So it can use #2867's register-allocated R→D doubling as it is. Before this PR, each of its 385 doublings was eight out-of-line calls to vg_p384_mul_mod_p or vg_p384_sqr_mod_p and 16 additions or subtractions through memory.

Changes

Implementation

• PubNaf.window (Impl/Weierstrass/AArch64/PubNaf.lean) takes an optional doubling. The default none keeps the field program's.
  • stepD K d is an iteration with the doubling d, and stepOf K dd chooses between the two.
  • pubNafPoints and pubNafVerify pass the doubling through.
  • Every other user, P-521's included, is unchanged.
• verifyP384 passes some (.block EcdhAllocatedCode.doubleRD).

Proofs

• Proof/Weierstrass/AArch64/PubNaf/StepD.lean. stepD_ok is step_ok with the doubling given by AArch64 P-384 ECDH: register-allocated doublings in the window #2867's DblSpec (from Inv on dblVR), and stepOf_ok covers either case.
• PubNaf/StepDTiming.lean. stepDRaw_relCT is the relational timing of such an iteration:
  • The doubling is constant-time given x0.
  • It leaves both runs' D at the same values, because DblSpec fixes them from the shared values of R.
  • It writes only the loop's slots, so the read-only slots and the table keep their values (ro_unch).
• Threading. window_ok, pubNafMul_ok, pubNafPoints_ok, pubNafVerify_ok, loop_relCT, window_relCT and pubNafVerify_public_ct take the doubling, with NafDblOk (correctness) and NafDblCT (timing). P-521's packed NAF passes none.
• Proof/Ecdsa/Verify/AArch64/P384/Verified.lean. Supplies the doubling's correctness from P384.EcdhDouble.dblsOk and its timing from Certificate.ctRD.

No changes to TCB/ or Spec/.

Speed

Neoverse N2, run 39270255193, compared with #2867's head (62ccb5c):

Benchmark	Base	Head	Change
ecdsa_p384_sha384_verify 64 B / 1 KiB / 16 KiB	208.53 / 210.33 / 221.55 µs	194.60 / 196.51 / 207.75 µs	−6.7 / −6.6 / −6.2%
ecdh_p384	174.76 µs	174.78 µs	0.0%
ecdsa_p384_sha384_sign 64 B / 1 KiB / 16 KiB	50.42 / 51.15 / 62.36 µs	50.69 / 51.39 / 62.66 µs	+0.5 to +0.6%
ec_p384_public_key	44.88 µs	45.01 µs	+0.3%

• With VG_CPU_FEATURES=none, verify is 5.7–6.6% faster and every other row is within 0.0%.
• Sign's code doesn't change. Its +0.5% with the default features is within the gate, and it is 0.0% without them.

Checks

These pass locally:

• full lake build
• the emitter (only src/asm/aarch64/ecdsa_p384.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 --check
• the P-384 tests on aarch64 under qemu, Wycheproof's included

---

Generated by Claude Code