[alex]

Part of #991. Follows #2729.

What

AArch64 vg_ecdsa_p384_verify's public NAF multiplication keeps each table entry's Z² and Z³ (cache, Impl/Weierstrass/AArch64/PubNaf.lean). They are computed once, after the co-Z table, into 128·6 bytes of scratch above the table. Each addition of an entry then reads them instead of computing them (addC, the Jacobian addition with the head CachedJac.headAt).

• The cache costs 16 field products: one square and one multiplication per entry.
• Each addition saves 2: the first digit's addition and every one in the loop.
• With about 64 additions per verify, that is roughly 110 fewer products.

The only generated file that changes is src/asm/aarch64/ecdsa_p384.rs (+443/−29 lines). The cache is unrolled for the eight entries. P-256's code, which shares CachedJac, is unchanged.

No TCB/ or Spec/ changes. Impl/Weierstrass/CachedJac.lean generalizes head to headAt, which reads Z² and Z³ from any two slots, and head is now headAt at P-256's slots. The registration file's notes describe the cache.

Proof

• PubNaf/CacheBuild.lean: cacheTo_ok. The Z² and Z³ of each of the 8 entries are stored at cacheAt, with the table, the scalar and every other slot of the window kept.
• PubNaf/Cache.lean:
  • CacheOk (the cache's words are Z², Z³ of each table entry).
  • Its framing through the loop (CacheOk.unch, away_loopW).
  • NafFixed.rebase, which moves the loop's fixed facts to the state after the cache.
• PubNaf/AddC.lean: addCB_ok. It is jacAddB_ok's contract given slots holding Z² and Z³ of q. PubNaf/AddCTiming.lean gives its timing.
• PubNaf/Digit.lean, DigitTiming.lean:
  • The entry's selection also loads its cached words into R.y, R.z (entry_ok, entryFields_ok).
  • The loop invariant carries CacheOk.
  • The addresses of the cache loads depend only on the digit.
• PubNaf/Window.lean, WindowTiming.lean: the cache between the table and the loop, branch-free (cache_relCT).
• The verifier (PubNafMul, PubNafPoints) places the cache above the table (cacheLayQ) and adds its range to the frame of words the multiplication writes.

Performance

Benchmarks run 39094784345, against #2729's head (1d5a8df9). Its scope is aarch64, cpu_features='- none', modules=ecdsa_p384.

Benchmark	default	VG_CPU_FEATURES=none
ecdsa_p384_sha384_verify/64	212.62 → 209.03 µs (−1.7%)	212.92 → 209.19 µs (−1.8%)
ecdsa_p384_sha384_verify/1024	214.67 → 210.86 µs (−1.8%)	216.29 → 212.38 µs (−1.8%)
ecdsa_p384_sha384_verify/16384	225.69 → 222.24 µs (−1.5%)	247.82 → 243.96 µs (−1.6%)

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

llvm-mca, with the multiply and square callees inlined (cycles):

	Neoverse N2	Apple M1
loop addition's head, before → after	386 → 247	718 → 455
first addition's head, before → after	611 → 472	1162 → 899
the cache (once)	1236	2260

So the cache pays for itself after about 9 additions.

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