[alex]

Part of #991.

What

AArch64 vg_ecdsa_p256_verify builds the odd multiples Q, 3Q, …, 15Q of the public key by co-Z arithmetic, reusing ECDH's register-allocated DBLU and ZADDU blocks (Impl/P256/EcdhTable.lean):

• DBLU of the affine Q gives 2Q and Q at one Z;
• with 2Q as the co-Z addend, each of seven ZADDU steps adds 2Q, returning the next odd multiple, 2Q rescaled to its Z, and that Z's square and cube.

Each entry and its Z², Z³ are stored as the joint loop expects (Impl/P256/VerifyTable.lean). This replaces the general Jacobian table (seven additions with exceptional-case branches) and the separate pass that computed the cached Z² and Z³ of each entry (P256Allocated.ops.table := VerifyTable.build, cache := .block []). The verify function shrinks from 15861 to 11226 lines of assembly.

No TCB/ or Spec/ changes. The registration file passes h.prime and its notes describe the new table.

Proof

• Proof/P256/VerifyTable/Field.lean: ECDH's allocated DBLU/ZADDU blocks carry their field contract to any slot predicate holding their slots, through their existing certificates on the observed slots.
• Copies, Store, StoreInv, Build: each phase of the build on the field invariant, with the environment after it an explicit function of the one before (buildEnv), and the frame (AllocatedFrame over ECDH's work regions, the table and its cache).
• Env.lean: the algebra. Entry a of buildEnv is (2a−1)Q in Jacobian coordinates, with its cached powers. ZADDU needs (2k+1)Q ≠ ±2Q for k ≤ 6, which follows from PrimeOrder (n > 17). allocatedVerify_verified therefore now also takes the curve's PrimeOrder, which the P256 AArch64 law variant already provides (h.prime in the registration file).
• Timing.lean: every address and the loop count depend on the scratch pointer alone (taint_decide on the copy and store blocks, ECDH's Dblu.ct/Zaddu.ct), so runs from one field environment leak the same. The table is built from the public key only.
• Proof/Ecdsa/Verify/AArch64/AllocatedPoints.lean (the allocated sections moved out of JointPoints.lean, plus the new setup stage) and AllocatedPointsTiming.lean wire it into the verifier's correctness and timing proofs.

Performance

llvm-mca of the changed region (the table and its cache; the preparation and the joint loop are unchanged), straight-line along the common path:

CPU	before	after
Neoverse N2	4134 cycles	2254 cycles
Apple M1	6001 cycles	3392 cycles

Benchmarks: this PR's Benchmarks check (aarch64, ecdsa_p256, the scope ci/bench_arches.py gives); results in its run summary.

Tests

CAVP and Wycheproof P-256 verification (cargo test --target aarch64-unknown-linux-gnu -- ecdsa_p256, under qemu) pass. lake build and Emit.lean --check pass on Lean 4.35.0, as do the ci/check_*.py scripts.

---

Generated by Claude Code