def Hex.powLtWordAux (p : Nat) : Nat → Nat → Option Nat

Accumulating helper for powLtWord?: multiply acc by p, n times, with early exit if any partial product reaches 2^64.

Equations

• Hex.powLtWordAux p 0 x✝ = some x✝
• Hex.powLtWordAux p n.succ x✝ = if x✝ * p < UInt64.word then Hex.powLtWordAux p n (x✝ * p) else none

def Hex.powLtWord? (p a : Nat) : Option Nat

some (p^a) if p^a < 2^64, computed with early exit so a huge exponent never materialises a bignum.

Equations

• Hex.powLtWord? p a = Hex.powLtWordAux p a 1

def Hex.cldQuotientModWord? (f g : ZPoly) (p a : Nat) : Option ZPoly

Word-sized CLD quotient (f · g') / g mod p^a for monic g, computed over WordMod when the guard Odd (p^a) ∧ p^a < 2^64 holds (p odd prime ⇒ p^a odd). Returns none when the guard fails, so the caller keeps the bignum path.

Equations

• One or more equations did not get rendered due to their size.