[alex]

Part of #991. Stacked on #2870 (and #2867).

ECDH's window and verify's public NAF both use P-384's allocated doubling (#2867, #2870). It had 16 modular additions and subtractions, each with its own conditional reduction. Following s2n-bignum's p384_montjdouble_alt, it now computes the same point with five of them and three linear combinations, each reduced once:

• d = 12 x y² - 9 m²
• x' = 4 x y² - d
• y' = 3 d m - 8 y⁴

The squares and products are unchanged: 5 squares and 3 products.

Changes

Implementation

• Impl/P384/Linear.lean adds lin o a b c d, which computes [o] = c [a] - d [b] mod p with one reduction, as s2n-bignum's cmsub_p384 does:
  • It forms p - [b] from the modulus's slot, multiplies it by d (rowInit), and adds c [a] (row). The sum is V < (c + d) p, exactly, in seven words.
  • It estimates the quotient as q, the top word plus one, and adds q (2^384 - p) to the low words. Where that doesn't carry, it adds p back under a mask, giving V - q p or V - q p + p, which is in [0, p).
  • The words of q (2^384 - p) and of the masked p are computed from registers, as the allocator follows only loads, movz and register operations.
  • It reuses the proven rowInit, row and P384Mul.addsIn. One generic proof covers all three shapes.
• Impl/P384/EcdhDouble.lean. The raw doubling follows s2n-bignum's order: ops1, lin, ops2, lin, lin. The allocation Impl/P384/EcdhAllocatedCode.lean is regenerated by lean/GenerateP384Ecdh.lean.

Proofs

• Proof/P384/Linear.lean.
  • lin_ok: lin stores (c A + d (p - B)) mod p for A, B < p and c, d < 2^16, changing only clobX and o (OpKeepX).
  • The quotient's arithmetic is reduce_arith, a statement about natural numbers.
  • linOp_ok is the same on the window's slots: o comes to stand for c E_a - d E_b, by toM_lin.
• Proof/P384/EcdhDouble/Vals.lean. raw_vals: the new order computes dblJF, by P-256's values_eq.
• Proof/P384/EcdhDouble/Raw.lean. raw_ok is restated for the new order. Its slot conditions (RawSlots) are decided for each direction.
• Proof/P384/EcdhDouble/Verified.lean. Unchanged in substance. The certificates check the new allocation; each still takes a few seconds in the kernel.

No changes to TCB/ or Spec/.

Speed

Neoverse N2, run 39279849367, compared with #2870's head (8b6dc87):

Benchmark	Base	Head	Change
ecdh_p384	174.76 µs	169.48 µs	−3.0%
ecdsa_p384_sha384_verify 64 B / 1 KiB / 16 KiB	194.60 / 196.43 / 207.72 µs	190.26 / 192.18 / 203.37 µs	−2.2 / −2.2 / −2.1%
ecdsa_p384_sha384_sign 64 B / 1 KiB / 16 KiB	50.37 / 51.10 / 62.32 µs	50.60 / 51.36 / 62.57 µs	+0.4 to +0.5%
ec_p384_public_key	44.90 µs	44.88 µs	0.0%

• With VG_CPU_FEATURES=none: ECDH −3.1%, verify −1.9 to −2.2%, sign +0.2 to +0.3%.
• Sign's code doesn't change; it is emitted into the same file as verify.
• Across the three PRs, P-384 ECDH on N2 goes from 188.9 µs to 169.5 µs (−10.3%). It is now ahead of aws-lc-rs's 186.6 µs.

Checks

These pass locally:

• full lake build
• the emitter (only src/asm/aarch64/ecdh_p384.rs and ecdsa_p384.rs change)
• check_lean_imports, check_lean_modules, check_registrations, check_lean_speed, check_vectors, check_arch_gates, check_variants, check_mcdt, cpu_tests.py lint
• algorithms_table.py --check
• the P-384 tests on aarch64 under qemu, Wycheproof's included

---

Generated by Claude Code