[alex]

Part of #991. The AArch64 counterpart of #2746.

What

InvCfg.inv (Impl/Weierstrass/AArch64/Inv.lean), the divstep inversion of the generic AArch64 Weierstrass code, used to reduce a and b fully in every batch. Each batch did one word of Montgomery reduction, then brought the result into [0, p) with three masked passes of p (mredC). Now:

• a and b stay signed in n + 1 words, in (-p, 2p).
• One word of reduction keeps them there, since |u| + |v| ≤ 2^59 (mredS).
• The three passes run once, at the end (normC, factored out of mredC).

The model is Proof/Divstep/TcS.lean's invRunS, from #2746.

The signed batches have slots of their own (sBS, sNFS, sNGS, sTS): f, g, a, b, f' and g' of n + 1 words each, then t. That is 7 n + 8 of the table's 9 n words. The constant goes in f''s place.

Old pieces kept. batch, init, fgUpdate, abUpdate and finish stay as they were, because the P-256 ECDH and verify inversions are built on them. Those are Impl/P256/EcdhInverse.lean and Ecdsa/Verify/AArch64/Allocated.lean, register-allocated copies of the update certified against the generic one. fgUpdate and finish are now fgUpdateAt and finishAt at the old slots, so their code is unchanged. ecdh_p256.rs and P-256 verify's code are byte-identical.

Reach. This reaches every user of inv:

• P-256 signing (both inversions) and its public key (ec_p256);
• every inversion of P-384, P-521, P-224, P-192, secp256k1 and brainpoolP256r1/P384r1/P512r1.

Dynamic instruction counts per inversion (straight-line batches, with normC once at the end):

modulus	batches	abUpdate per batch	inversion, before → after
4 words	10	492 → 372	17210 → 16094 (−6.5%)
6 words (P-384)	15	696 → 520	30735 → 28211 (−8.2%)
9 words (P-521)	23	1002 → 742	58443 → 52627 (−10.0%)

P-256 ECDH and verify, measured and left as they are. I regenerated their allocated updates from the signed update with their generators (GenerateP256Ecdh.lean, GenerateP256Verify.lean, which reproduce today's files byte for byte):

	before	signed
ECDH update, per batch	460	426
verify inverseUpdate, per batch	467	431
whole P-256 ECDH inversion, instructions	13682	13419 (−1.9%)

• The allocator already keeps the three normalization passes in registers, so they cost little.
• The signed lin adds a word to each of its four rows.
• The end's normC adds about 75 instructions.

That is under 0.1% of ECDH or verify, against moving about 1,850 lines of their proofs to the signed invariant, so they keep the old batches.

No TCB/ or Spec/ changes.

Proof

• InvBatch.lean:
  • normC_ok: [t + 8] holding r ∈ (-p, 2p) becomes norm p r, by Divstep.norm_nat.
  • mredS_ok: [dst] ≡ mredRaw p m T, by Divstep.mredRaw_nat. Both are split from mredC_ok's proof.
  • IInvS, the signed batch state.
  • abHalfS_ok, abUpdS_ok, batchS_ok: a batch as Divstep.batchS.
  • fgUpd_ok is generalized to any staging slots (fgUpdAt_ok); the old lemma is a corollary.
  • These live in InvBatch because modules of their own would bring Divstep/Tc.lean and Packed.lean more than 40 importers.
• InvMain.lean:
  • initS_ok.
  • loopS_ok: the invariant invRunS, with a, b in (-p, 2p) by invRunS_range, and d, f, g those of invRun by invRunS_rel.
  • finishS_ok: normC, then finishAt_ok, the old finish_ok generalized over the constant's slot.
  • invPow_ok: the same statement, for the new inv. Its a is norm p of invRunS's, which is invRun's (norm_invRunS).
  • InvSound, the contract every caller uses, is unchanged.

Performance

Benchmarks run 39116706828: Neoverse N2, aarch64, cpu_features='-', against the merge base (31531ad97), modules ecdsa_p256 ec_p256 ecdh_p384 ecdsa_p384 ec_p384 ecdh_p521 ecdsa_p521 ecdh_secp256k1.

	change
P-256 signing	−1.2% to −1.8%
ec_p256_public_key	−1.3%
P-384 signing	−1.1% to −1.4%
P-384, P-521 and secp256k1 ECDH and verify	about 0 (P-521 verify −0.1% to −0.2%)
ecdsa_p521_sha512_sign/64	+0.7%
ecdsa_p521_sha512_sign/1024	+0.9%
ecdsa_p521_sha512_sign/16384	+0.2%
ec_p521_public_key	+1.0%

The P-521 rows are not a regression of this change, in my reading:

• The only P-521 code this PR changes is its inversion (p521_inverse.rs), and that runs 10.0% fewer instructions (58443 → 52627, about 5,800 fewer per call).
• Signing does two inversions and the public key one, so the expected effect is a small speedup, not a slowdown.
• These are FRESH_COPIES groups (P-521's comb table): each side is the best of 8 fresh copies of its binary, and the copies of one side spread by 6–12%. That is page-placement noise ten times the size of these deltas.
• P-521 verify, which runs the same inversion, moved the other way (−0.1% to −0.2%).

P-192, P-224 and the three brainpool curves run the same inv code and were not benchmarked.

Tests

• lake build, Emit.lean --check and the ci/check_*.py scripts pass.
• Wycheproof for P-192, P-224, P-256, P-384, P-521, secp256k1 and brainpool passes under qemu: cargo test --release --target aarch64-unknown-linux-gnu, 61 tests.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ma2fA9rUTPXEEQjYyCMCRw