Eight-limb inversion: runtime definitions (Mathlib-free)

The Pornin binary-GCD inverse candidate over Limbs8 and its checked wrapper (invGcdRaw), Mathlib-free for precompileModules consumers. The proof side is Montgomery/Native64x8Inv.

Per-field schedule

class Montgomery.Native64x8.GcdData (modulus : Nat) : Type

Per-field schedule of the binary-GCD inverse candidate; every obligation defaults to decide.

• finalRounds : Nat

  Divsteps in the final word-sized phase: 2·bits(p) - 2 - 15·31.

• initU : Limbs8

  Initial u: the power of two that keeps the candidate in Montgomery form.

• initU_bounded : (initU modulus).Bounded
• initU_toNat : (initU modulus).toNat = 2 ^ (591 - finalRounds modulus) % modulus
• finalRounds_le : finalRounds modulus ≤ 62

  Final-phase chunks stay at mac width.

Word-sized divstep loop

@[inline]

def Montgomery.Native64x8.gcdBitLen (x : UInt64) : Nat

Bit length of a word.

def Montgomery.Native64x8.gcdInner (rounds : Nat) (a b : UInt64) (f0 g0 f1 g1 : Int) : UInt64 × UInt64 × Int × Int × Int × Int

The word-sized divstep loop, accumulating the transition matrix; b must be odd.

Approximation: 64-bit windows over 32-bit limbs

@[inline]

def Montgomery.Native64x8.gcdLimb (v : Limbs8) : Nat → UInt64

Read limb i (out-of-range indices read the top limb).

@[inline]

def Montgomery.Native64x8.gcdNumBits (a b : Limbs8) : Nat × Nat

Highest nonzero limb index among limbs 1-7 of a ||| b and its bit length; (1, 0) when all are zero.

@[inline]

def Montgomery.Native64x8.gcdApprox (val : Limbs8) (limbIdx bits : Nat) : UInt64

One-word approximation: top 33 bits (at the shared bit length) above the bottom 31; exact once both values fit one 64-bit word.

Nine-limb linear combinations over the native macs

@[inline]

def Montgomery.Native64x8.gcdAdd9 (p q : State9) : State9

9-limb ripple-carry add (top carry discarded).

@[inline]

def Montgomery.Native64x8.gcdSub9 (p q : State9) : State9 × UInt64

9-limb subtract with borrow; the wrapped difference and the final borrow.

@[inline]

def Montgomery.Native64x8.gcdLinearCombDiv (a b : Limbs8) (f g : Int) : Limbs8 × Int

(f·a + g·b) / 2^31 as magnitude and sign. Requires |f| + |g| ≤ 2^31.

@[inline]

def Montgomery.Native64x8.gcdLinearCombMontyRed (q : Limbs8) (negInv : UInt64) (a b : Limbs8) (f g : Int) : Limbs8

f·a + g·b folded through one Montgomery reduction step. Requires |f| + |g| ≤ 2^31.

Main loop and candidate

def Montgomery.Native64x8.gcdMainLoop (q : Limbs8) (negInv : UInt64) (rounds : Nat) (a u b v : Limbs8) : Limbs8 × Limbs8 × Limbs8 × Limbs8

The outer rounds: 31 divsteps on one-word approximations, then the transition matrix applied to both tracks.

def Montgomery.Native64x8.gcdFinalChunks (q : Limbs8) (negInv : UInt64) (finalRounds : Nat) (a u b v : Limbs8) : Limbs8

The final divsteps as two mac-width chunks, folding the Montgomery pair.

def Montgomery.Native64x8.gcdInvCandidate (modulus : Nat) [P : GcdData modulus] (q : Limbs8) (negInv : UInt64) (x : Limbs8) : Limbs8

Pornin binary-GCD candidate for the Montgomery inverse, canonical nonzero x·R mod p to x⁻¹·R mod p; proof-free, callers verify.

Checked inversion over raw limbs

@[irreducible]

def Montgomery.Native64x8.montPow (q : Limbs8) (negInv : UInt64) (acc x : Limbs8) (n : Nat) : Limbs8

acc · x^n in Montgomery form by binary powering.

def Montgomery.Native64x8.invGcdRaw (modulus : Nat) [GcdData modulus] (q : Limbs8) (negInv : UInt64) (rMod x : Limbs8) : Limbs8

The GCD candidate, accepted only if it verifies (z · x = 1); else Fermat montPow.