def Hex.ZMod64.mulWord (p : Nat) [Bounds p] (a b : UInt64) : UInt64

Overflow-safe modular product of two raw words, reconstructing residues and delegating to the (extern-backed) ZMod64.mul. Defined so that mulWord p x.val y.val = (x * y).val.

Equations

• Hex.ZMod64.mulWord p a b = ((Hex.ZMod64.ofNat p a.toNat).mul (Hex.ZMod64.ofNat p b.toNat)).val

def Hex.ZMod64.subWord (p : Nat) [Bounds p] (a b : UInt64) : UInt64

Overflow-safe modular difference of two raw words, reconstructing residues and delegating to ZMod64.sub. Defined so that subWord p x.val y.val = (x - y).val.

Equations

• Hex.ZMod64.subWord p a b = ((Hex.ZMod64.ofNat p a.toNat).sub (Hex.ZMod64.ofNat p b.toNat)).val

@[simp]

theorem Hex.ZMod64.val_zero {p : Nat} [Bounds p] : Zero.zero.val = 0

The backing word of the zero residue is the zero word.

theorem Hex.ZMod64.val_eq_zero_iff {p : Nat} [Bounds p] (x : ZMod64 p) : x.val = 0 ↔ x = Zero.zero

A residue's backing word is zero exactly when the residue is zero.

theorem Hex.ZMod64.mulWord_val {p : Nat} [Bounds p] (x y : ZMod64 p) : mulWord p x.val y.val = (x * y).val

The word multiply agrees with the residue product read off in words.

theorem Hex.ZMod64.subWord_val {p : Nat} [Bounds p] (x y : ZMod64 p) : subWord p x.val y.val = (x - y).val

The word subtract agrees with the residue difference read off in words.

def Hex.FpPoly.toWords {p : Nat} [ZMod64.Bounds p] (a : Array (ZMod64 p)) : Array UInt64

Pack a residue coefficient array into its backing words.

Equations

• Hex.FpPoly.toWords a = Array.map (fun (x : Hex.ZMod64 p) => x.val) a

def Hex.FpPoly.ofWords (p : Nat) [ZMod64.Bounds p] (a : Array UInt64) : Array (ZMod64 p)

Reconstruct a residue coefficient array from raw words.

Equations

• Hex.FpPoly.ofWords p a = Array.map (fun (w : UInt64) => Hex.ZMod64.ofNat p w.toNat) a

@[simp]

theorem Hex.FpPoly.toWords_size {p : Nat} [ZMod64.Bounds p] (a : Array (ZMod64 p)) : (toWords a).size = a.size

theorem Hex.FpPoly.toWords_getD {p : Nat} [ZMod64.Bounds p] (a : Array (ZMod64 p)) (i : Nat) : (toWords a).getD i 0 = (a.getD i Zero.zero).val

Reading a packed word with default 0 is the residue coefficient read with default 0, packed.

theorem Hex.FpPoly.toWords_set! {p : Nat} [ZMod64.Bounds p] (a : Array (ZMod64 p)) (i : Nat) (v : ZMod64 p) : (toWords a).set! i v.val = toWords (a.set! i v)

Writing a residue then packing equals packing then writing the word.

theorem Hex.FpPoly.toWords_replicate {p : Nat} [ZMod64.Bounds p] (n : Nat) : toWords (Array.replicate n Zero.zero) = Array.replicate n 0

Packing a zero-filled array gives a zero-word-filled array.

theorem Hex.FpPoly.ofWords_toWords {p : Nat} [ZMod64.Bounds p] (a : Array (ZMod64 p)) : ofWords p (toWords a) = a

Reconstructing the words of a residue array recovers the original array.

def Hex.FpPoly.arrayDegreeAuxPacked (coeffs : Array UInt64) : Nat → Option Nat

Packed downward degree scan: the highest index below fuel with a nonzero word, mirroring DensePoly.arrayDegreeAux.

Equations

• Hex.FpPoly.arrayDegreeAuxPacked coeffs 0 = none
• Hex.FpPoly.arrayDegreeAuxPacked coeffs fuel.succ = if coeffs.getD fuel 0 = 0 then Hex.FpPoly.arrayDegreeAuxPacked coeffs fuel else some fuel

def Hex.FpPoly.arrayDegreePacked? (coeffs : Array UInt64) : Option Nat

Packed degree: the highest index of a nonzero word, mirroring DensePoly.arrayDegree?.

Equations

• Hex.FpPoly.arrayDegreePacked? coeffs = Hex.FpPoly.arrayDegreeAuxPacked coeffs coeffs.size

def Hex.FpPoly.subtractScaledShiftStepPacked (p : Nat) [ZMod64.Bounds p] (q : Array UInt64) (shift : Nat) (coeff : UInt64) (next : Array UInt64) (j : Nat) : Array UInt64

One packed elimination coefficient write, mirroring DensePoly.subtractScaledShiftStep with overflow-safe word arithmetic.

Equations

• Hex.FpPoly.subtractScaledShiftStepPacked p q shift coeff next j = next.set! (shift + j) (Hex.ZMod64.subWord p (next.getD (shift + j) 0) (Hex.ZMod64.mulWord p coeff (q.getD j 0)))

def Hex.FpPoly.subtractScaledShiftPacked (p : Nat) [ZMod64.Bounds p] (rem q : Array UInt64) (shift : Nat) (coeff : UInt64) : Array UInt64

One full packed elimination step rem - coeff * xˢʰⁱᶠᵗ * q, mirroring DensePoly.subtractScaledShift.

Equations

• Hex.FpPoly.subtractScaledShiftPacked p rem q shift coeff = List.foldl (Hex.FpPoly.subtractScaledShiftStepPacked p q shift coeff) rem (List.range q.size)

def Hex.FpPoly.divModArrayAuxPacked (p : Nat) [ZMod64.Bounds p] (q : Array UInt64) (qDegree : Nat) (scaleLead : UInt64 → UInt64) (fuel : Nat) (quot rem : Array UInt64) : Array UInt64 × Array UInt64

The packed fuel-bounded long-division loop, mirroring DensePoly.divModArrayAux.

Equations

• One or more equations did not get rendered due to their size.
• Hex.FpPoly.divModArrayAuxPacked p q qDegree scaleLead 0 quot rem = (quot, rem)

def Hex.FpPoly.modByMonicPacked {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) (_hmonic : DensePoly.Monic f) : FpPoly p

Packed monic division remainder, sharing the signature of FpPoly.modByMonic (so a @[csimp] swap would be well-typed, though it is intentionally not registered; see the module docstring). Packs both operand arrays, runs the packed loop with scaleLead = id (the divisor is monic), and reconstructs the remainder.

Equations

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

theorem Hex.FpPoly.arrayDegreeAuxPacked_eq {p : Nat} [ZMod64.Bounds p] (a : Array (ZMod64 p)) (ceil : Nat) : arrayDegreeAuxPacked (toWords a) ceil = DensePoly.arrayDegreeAux a ceil

Packed degree scan agrees with the reference scan on packed input.

theorem Hex.FpPoly.arrayDegreePacked?_eq {p : Nat} [ZMod64.Bounds p] (a : Array (ZMod64 p)) : arrayDegreePacked? (toWords a) = DensePoly.arrayDegree? a

Packed degree agrees with the reference degree on packed input.

theorem Hex.FpPoly.subtractScaledShiftStepPacked_eq {p : Nat} [ZMod64.Bounds p] (q : Array (ZMod64 p)) (shift : Nat) (coeff : ZMod64 p) (rem : Array (ZMod64 p)) (j : Nat) : subtractScaledShiftStepPacked p (toWords q) shift coeff.val (toWords rem) j = toWords (DensePoly.subtractScaledShiftStep q shift coeff rem j)

One packed elimination coefficient write corresponds to the reference write.

theorem Hex.FpPoly.foldl_subtractScaledShiftStepPacked {p : Nat} [ZMod64.Bounds p] (q : Array (ZMod64 p)) (shift : Nat) (coeff : ZMod64 p) (xs : List Nat) (rem : Array (ZMod64 p)) : List.foldl (subtractScaledShiftStepPacked p (toWords q) shift coeff.val) (toWords rem) xs = toWords (List.foldl (DensePoly.subtractScaledShiftStep q shift coeff) rem xs)

Folding the packed step over any index list corresponds to folding the reference step.

theorem Hex.FpPoly.subtractScaledShiftPacked_eq {p : Nat} [ZMod64.Bounds p] (rem q : Array (ZMod64 p)) (shift : Nat) (coeff : ZMod64 p) : subtractScaledShiftPacked p (toWords rem) (toWords q) shift coeff.val = toWords (DensePoly.subtractScaledShift rem q shift coeff)

A full packed elimination step corresponds to the reference step.

theorem Hex.FpPoly.divModArrayAuxPacked_eq {p : Nat} [ZMod64.Bounds p] (q : Array (ZMod64 p)) (qDegree fuel : Nat) (quot rem : Array (ZMod64 p)) : divModArrayAuxPacked p (toWords q) qDegree id fuel (toWords quot) (toWords rem) = (toWords (DensePoly.divModArrayAux q qDegree id fuel quot rem).fst, toWords (DensePoly.divModArrayAux q qDegree id fuel quot rem).snd)

The packed long-division loop corresponds, coordinatewise, to the reference loop with scaleLead = id.

theorem Hex.FpPoly.modByMonicPacked_eq {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) (hmonic : DensePoly.Monic f) : f.modByMonic g hmonic = f.modByMonicPacked g hmonic

Value correspondence. The packed monic-division remainder equals the reference FpPoly.modByMonic for every modulus p (every Bounds p).