perf(bz): ZMod64 inverse in word arithmetic, removing the Int.extGcd/gmp round-trip

[kim-em]

Context. Deliverable 4 of #8630. Deliverables 1 and 2 landed in that issue's PR. This carves out the word-arithmetic modular inverse.

Measurement. ZMod64.inv (HexModArith/Basic.lean:542) routes through HexArith.Int.extGcd (gmp), showing up as lean_int_extgcd_fallback + gmp on the modular-inverse path in the deg-24 profile. It is called once per field division step (O(deg) per gcd), so smaller than the O(deg²) elimination win from deliverable 2, but still on the hot path (every division in gcdPacked/divModRemainderPacked and, later, nullspace pivoting).

Deliverable. Compute the ZMod64 inverse in word arithmetic, eliminating the Int.extGcd/gmp round-trip per inverse.

Design notes / gotchas.

• A global @[csimp] @ZMod64.inv = @invImpl must hold for every Bounds p and every input, including non-prime p and non-coprime a, where inv currently returns the Int.extGcd-derived Bezout residue ofNat p (Int.toNat (s % p)). So Fermat powering a^(p-2) is not a valid global swap (it only matches for prime p, coprime a).
• HexArith.UInt64.extGcd (HexArith/ExtGcd.lean:499) does not help on its own: it still calls Int.extGcd internally for the cofactors. A genuine win needs a binary/extended GCD implemented in UInt64 (wrapping/widening) arithmetic, proved equal to the current inv residue for all Bounds p (the extGcd_bezout/extGcd_fst certificates are a starting point). Alternatively an @[extern] C kernel (trusted) matching the exact residue convention.

Verification. @[csimp]-backed equality (or extern with a matching-residue argument); FLINT conformance byte-identical; bench targets show the win.

[kim-em]

Reframing note: the packed/de-boxing premise from #8630 did not hold (see #8633 — the real cost was a per-multiply bignum allocation, now removed, ~1.6-2.3x). A word-arithmetic ZMod64.inv may still help since inv still routes through Int.extGcd/gmp, but it is O(deg) per gcd (one leading-coefficient inverse per division step), not the O(deg^2) hot loop, so it is lower priority than #8633/#8637. Worth measuring the inverse's share after #8633 before investing.

[kim-em]

Closing per the reframing comment above: O(deg) per gcd (one leading-coefficient inverse per division step), lower priority than the landed #8633 and the pending #8639, and worth investing in only if its share is still material afterwards. That measurement is tracked in #8647.

🤖 Prepared with Claude Code