[alex]

Part of #991.

On AArch64, vg_ecdsa_p256_verify's joint loop now doubles with Impl.P256.EcdhDouble.program, the doubling vg_ecdh_p256 already uses. It uses five squares and three products, and reduces each linear combination (12a − 9b, 4a − b, 3a − 8b) once. The old unfused doubling used four squares, four products and twelve separately reduced additions and subtractions. ECDH's doubling is in place on the same accumulator slots. Its certificate was already checked against verify's observation set and work regions (VerifyAllocated.observe .doubleRR, VerifyAllocated.work), so it drops in.

Proof

• Generalized raw proof (Proof/P256/EcdhDouble/): weakMul_ok, linearField_ok, linear41Field_ok and inv_keep_unused now take any slot predicate with its Lay and Aligned facts, instead of ECDH's.
  • rawR_ok proves the raw fused doubling from the accumulator alone.
  • raw_ok extends it to any live list holding R; slots it doesn't write are kept, by ProgKeep and the layout.
  • result_of relates the raw result to runOps (operations .doubleRR) on any such live list.
  • ECDH's proofs are these at ECDH's slots.
• Verify (AllocatedArithmetic):
  • double_field_ok and double_ok prove EcdhDouble.program on the joint loop's jointLive with the same postcondition as before, through ECDH's certificate.
  • The timing proof takes ECDH's Certificate.ct (FieldCT) through fieldWP_relCT.
• Dead code removed: the unfused allocated doubling. That's its literal in VerifyAllocatedCode, its certificate (Proof/P256/VerifyAllocated/Double.lean) and its Double_ct, along with its entry in GenerateP256Verify.lean.

No change to TCB/, Spec/ or any contract. Only src/asm/aarch64/ecdsa_p256.rs changes: verify's loop body, and its note in Generic/P256/AArch64/EcdsaP256.lean.

Benchmarks

This PR's Benchmarks check ran on N2 (Neoverse N2, 0xd49), comparing against main.

row	detected	sha3	none
ecdsa_p256_sha256_verify/64	49.27 → 47.37 µs (−3.8%)	−3.8%	−3.8%
ecdsa_p256_sha256_verify/1024	49.83 → 47.93 µs (−3.8%)	−3.6%	−3.6%
ecdsa_p256_sha256_verify/16384	−3.4%	−1.9%	−1.9%
ecdsa_p256_sha384_verify/64	49.54 → 47.64 µs (−3.8%)	−3.8%	−3.8%
ecdsa_p256_sha384_verify/1024	−3.8%	−3.7%	−3.7%
ecdsa_p256_sha384_verify/16384	−3.1%	−3.1%	−2.3%

Every sign row and ec_p256_public_key moves between −0.3% and +0.0%; their code is byte-identical to main (unchanged code / placement). verify/64 against aws-lc-rs's 52.24 µs on N2 goes from 0.94× to 0.91×.

Doubling alone on N2: 256 doublings, timed on a throwaway branch that will never be merged (run 39072614399). The blocks are copied from the generated code.

256 doublings, N2	µs
verify's old doubling	30.47
ECDH's fused doubling (this PR)	28.71 (−5.8%)
s2n-bignum p256_montjdouble_alt (call overhead included)	29.34

llvm-mca, cycles per doubling (200 iterations of each block). This PR can't be benchmarked on Apple, so llvm-mca stands in for it:

CPU model	old	fused
apple-m1	381	361 (−5.2%)
neoverse-n2	248	254 (+2.4%)

llvm-mca's N2 model gets the direction wrong: N2 measured −5.8% on the doubling and −3.8% on verify. So llvm-mca's M1 prediction is supporting evidence only.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ma2fA9rUTPXEEQjYyCMCRw