theorem Hex.foldl_add_toNat_mod {p : Nat} [ZMod64.Bounds p] (L : List Nat) (P : Nat → Prop) [DecidablePred P] (f : Nat → ZMod64 p) (g : Nat → Nat) (hfg : ∀ (i : Nat), (f i).toNat = g i % p) (init : ZMod64 p) (initN : Nat) (hinit : init.toNat = initN % p) : (List.foldl (fun (c : ZMod64 p) (i : Nat) => if P i then c + f i else c) init L).toNat = List.foldl (fun (c i : Nat) => if P i then c + g i else c) initN L % p

Fold homomorphism: a ZMod64 conditional-add fold and the matching Nat conditional-add fold agree modulo p on their toNat values. This is what lets a lazily-accumulated (reduce-once) sum equal the per-term-reduced ZMod64 sum.

def Hex.FpPoly.mulPacked {p : Nat} [ZMod64.Bounds p] (a b : FpPoly p) : FpPoly p

Packed lazy-reduction multiply: pack both operands to backing words, convolve natively, reduce once per output coefficient, unpack. The FpPoly coefficients are reduced residues below p < 2^31, so the internal fpConvolve extern is always called within its contract.

Equations

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

theorem Hex.FpPoly.ofWords_getD {p : Nat} [ZMod64.Bounds p] (W : Array UInt64) (k : Nat) : (ofWords p W).getD k Zero.zero = ZMod64.ofNat p (W.getD k 0).toNat

Reading ofWords with default 0 unpacks the word read with default 0.

theorem Hex.FpPoly.mulPacked_eq {p : Nat} [ZMod64.Bounds p] (a b : FpPoly p) : a.mulPacked b = a * b

The packed lazy multiply computes the same polynomial as the reference *.

def Hex.FpPoly.packedCutoff : Nat

Shorter-size threshold below which generic schoolbook multiplication beats the packed lazy-reduction setup. The forced F_257 and F_65537 ladders both cross between 8 and 16 coefficients per operand.

Equations

• Hex.FpPoly.packedCutoff = 16

def Hex.FpPoly.mulPackedFast {p : Nat} [ZMod64.Bounds p] (left right : FpPoly p) : FpPoly p

Total finite-field multiplication for the published consumers: generic schoolbook multiplication below packedCutoff coefficients in the shorter operand, the packed lazy-reduction kernel above it. This is the mulFast dispatcher without its auxiliary-prime NTT and Karatsuba tail, which lives in HexPolyFp.NttMul and depends on libraries that are not yet published; every measured consumer size sits below that tail's 8192-coefficient crossover.

Equations

• left.mulPackedFast right = if min (Hex.DensePoly.size left) (Hex.DensePoly.size right) < Hex.FpPoly.packedCutoff then left * right else left.mulPacked right

theorem Hex.FpPoly.mulPackedFast_eq {p : Nat} [ZMod64.Bounds p] (left right : FpPoly p) : left.mulPackedFast right = left * right

The published dispatcher agrees with schoolbook multiplication.