Optimize x86-64 P-256 ECDH table construction and finalization

[reaperhulk]

Closed as superseded by #1260. A fresh comparison against main 131275570 showed no useful remaining performance advantage: native ECDH was effectively tied (0.17% lower wall time), and baseline was 0.87% slower in this run. The earlier results below compare against the older main commit and no longer describe the remaining benefit.

Optimize x86-64 P-256 ECDH's five-bit Jacobian path: build even peer-table entries by doubling and odd entries by mixed addition, initialize the accumulator directly from the leading digit, and finish with only the x-coordinate. Keep cached Z²/Z³ in the 16-entry table and use AVX2 selection on ADX or SSE2 on baseline. Align the existing 8192-byte Rust scratch allocation to 64 bytes on x86-64.

Main now contains a separate five-bit Jacobian implementation from #1256. This PR retains the additional table-building, accumulator-initialization, and x-only-finalization changes described above.

The peer-order and digit-bound proofs exclude equal nonzero inputs to the incomplete addition for valid scalars; masks handle infinity and the proofs cover opposite points and invalid scalar inputs. Both backends satisfy the existing ECDH contract, including constant time, memory safety, and ABI preservation. The new peer-order proof is supplied through a separate artifact interface to keep heavy algebra out of the machine proofs. No Spec or TCB changes.

Wall-clock performance

Compared with current main 33b414efc (including #1256) on an Intel Xeon E5-2696 v4, pinned to CPU 2. Medians of 14 native samples per library and 28 baseline samples, 500 ms per sample, alternating library order and reversing main/candidate order between processes, using 256 distinct private keys and peer keys. No local builds ran during measurement. AWS-LC is aws-lc-rs 1.18.1; both builds use matching dependency locks.

ECDH configuration	Main	This PR	Less wall time than main	AWS-LC
Native BMI2/ADX/AVX2	47.814 µs	46.192 µs	3.39%	48.240 µs
Baseline (VG_CPU_FEATURES=none)	73.244 µs	71.348 µs	2.59%	—

Native ECDH takes 4.24% less wall time than AWS-LC. The baseline row disables optional CPU features in both verified-garbage builds, not in AWS-LC. Baseline results were noisier between processes (main process medians 72.275–76.085 µs; PR 70.616–76.382 µs), so its small improvement should be treated accordingly. These replace the earlier measurements against pre-#1256 main f12e4c8b7.

Validation

• Full cached Lean build after rebasing onto 33b414efc: 10,999 jobs passed; standard-axiom, compiler, and specification-origin audits passed.
• Full assembly emission and Emit.lean --check passed. Only src/asm/x86_64/ecdh_p256.rs changes among generated files.
• 424 native Rust tests and 14 forced-baseline P-256 tests passed, including CAVP/Wycheproof.
• 12,288 differential ECDH cases against AWS-LC passed on each backend, including small scalars, scalars close to the group order, randomized scalars, and invalid-scalar checks.
• Clippy, formatting, Lean import/proof-speed checks, vectors, architecture gates, variant coverage, MCDT, CPU-test lint, and algorithm-table checks passed.

CI compatibility fix

Rebased onto main 33b414efc and updated the cached-addition, point-transfer, field-program, and table-copy proof calls for the generalized interfaces merged in #1241/#1250. The registration now accepts the extended P-256 law interface from #1256. Full cached Lean build, emission/audits, emitter consistency check, Clippy, static checks, 424 native Rust tests, and 14 baseline P-256 tests passed again. The emitted ECDH file is byte-for-byte identical to the original PR head 1aa042abf; this fix does not change the measured implementation.

[alex]

CI is failing

[alex]

merge conflicts