[alex]

Part of #991.

What

AArch64 vg_ecdsa_p384_verify builds the public NAF's table of the key's odd multiples Q, 3Q, …, 15Q by co-Z arithmetic (Impl/Weierstrass/CoZ.lean, Impl/Weierstrass/AArch64/PubNaf.lean):

• DBLU of the affine Q (its z is one) gives 2Q and Q at one Z. Its slots are renamed (dbluσ) so that 2Q lands in E and Q in R, exactly where ZADDU reads them, so no copies follow.
• Seven ZADDU steps (coZσ) each add 2Q. Each returns the next odd multiple and 2Q rescaled to that multiple's Z, and the multiple is stored into the next entry.

This replaces a general doubling and seven complete Jacobian additions, with their exceptional-case branches. The table's field products drop from 120 to 55; each is a call of vg_p384_mul_mod_p or vg_p384_sqr_mod_p. The only generated file that changes is src/asm/aarch64/ecdsa_p384.rs (+687/−1743 lines). The selection, the doublings and the additions of the main loop are unchanged.

No TCB/ or Spec/ changes. The registration file (Generic/P384/AArch64/EcdsaP384.lean) now passes h.prime, as P-256's verify already does, and its notes describe the new table.

Proof

• Proof/Weierstrass/CoZTable.lean (algebra, target-independent):
  • dblu_pts: DBLU of an affine P gives 2P and P at one nonzero Z.
  • zaddu_pts: ZADDU of 2P and (2k+1)P gives (2k+3)P, and 2P at its new Z. It needs (2k+1)P ≠ ±2P for k ≤ 6 (coz_x), which follows from PrimeOrder with n ≥ 17.
• PubNaf/CoZField.lean: a renaming (Ren) of a co-Z program's slots onto the window method's carries the generic field-program contract (fprogB_ok) over to the numbered program's values (coZ_ok).
• PubNaf/TableCoZ.lean: table_ok covers the initial copy and store (coZInit_ok), DBLU (dbluStep_ok) and the counted ZADDU loop (coZStep_ok). It replaces the general table's steps in PubNaf/Table.lean.
• PubNaf/TableTiming.lean: table_relCT.
  • The co-Z programs are branch-free (coZ_relCT).
  • The stores' addresses depend only on x20, and the loop count only on x19.
• window_ok/window_relCT and the verifier's proofs (PubNafMul, PubNafPoints, PubNafMain, PubNafTiming, P384/Verified) now take three more facts: the curve's PrimeOrder, 17 ≤ n, and that the prepared Q's z is one. P384/Checks discharges the new taint checks.

Performance

Benchmarks run 39092210388, against 02fa10ae2. Its scope is aarch64, cpu_features='- none', modules=ecdsa_p384, the one ci/bench_arches.py gives.

Benchmark	default	VG_CPU_FEATURES=none
ecdsa_p384_sha384_verify/64	215.16 → 212.82 µs (−1.1%)	215.29 → 212.86 µs (−1.1%)
ecdsa_p384_sha384_verify/1024	217.16 → 214.83 µs (−1.1%)	218.51 → 216.27 µs (−1.0%)
ecdsa_p384_sha384_verify/16384	228.42 → 226.18 µs (−1.0%)	250.11 → 247.76 µs (−0.9%)

Sign and ec_p384_public_key, whose code is unchanged, moved by at most 0.1%.

llvm-mca of the table's construction, along its common path with the multiply and square callees inlined:

CPU	before	after
Neoverse N2	9515 cycles	4671 cycles
Apple M1	17920 cycles	8633 cycles

Tests

lake build, Emit.lean --check and the ci/check_*.py scripts pass. Wycheproof and RFC 6979 P-384 verification (cargo test --release --target aarch64-unknown-linux-gnu -- p384, under qemu) pass.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ma2fA9rUTPXEEQjYyCMCRw

[alex]

why draft?

[alex]

It was a draft only until the benchmark run it links had finished. That run is in now: verify is 0.9–1.1% faster on aarch64, and the unchanged rows are flat. I've added the results to the description and marked the PR ready.

---

Generated by Claude Code