Effective Frobenius iteration and trace

A fixed-width loop squares its current field element and adds it to a trace accumulator. The loop count is unary, so k Frobenius operations take poly(k) time even though the represented exponent is 2^k.

def MIPRE.LowDegree.BinaryPolynomial.traceStep (s : PowerState) : Unit → PowerState

Equations

• MIPRE.LowDegree.BinaryPolynomial.traceStep s x✝ = (s.1, MIPRE.LowDegree.BinaryPolynomial.mulReduce s.1 s.2.1 s.2.1, MIPRE.LowDegree.BinaryPolynomial.xorBits s.2.2 s.2.1)

theorem MIPRE.LowDegree.BinaryPolynomial.traceStep_width (s : PowerState) (u : Unit) : (traceStep s u).1 = s.1 ∧ List.length (traceStep s u).2.1 ≤ List.length s.2.1 ∧ List.length (traceStep s u).2.2 ≤ List.length s.2.2

theorem MIPRE.LowDegree.BinaryPolynomial.fold_traceStep_width (u : Cost.Unary) (s : PowerState) : (List.foldl traceStep s u).1 = s.1 ∧ List.length (List.foldl traceStep s u).2.1 ≤ List.length s.2.1 ∧ List.length (List.foldl traceStep s u).2.2 ≤ List.length s.2.2

theorem MIPRE.LowDegree.BinaryPolynomial.fold_traceStep_length (u : Cost.Unary) (p a c : Cost.BitStr) (ha : List.length a = List.length p) (hc : List.length c = List.length p) : List.length (List.foldl traceStep (p, a, c) u).2.1 = List.length p ∧ List.length (List.foldl traceStep (p, a, c) u).2.2 = List.length p

def MIPRE.LowDegree.BinaryPolynomial.frobeniusTrace (p a : Cost.BitStr) (u : Cost.Unary) : Cost.BitStr × Cost.BitStr

Both the final Frobenius iterate and the sum of the preceding iterates.

Equations

• MIPRE.LowDegree.BinaryPolynomial.frobeniusTrace p a u = (List.foldl MIPRE.LowDegree.BinaryPolynomial.traceStep (p, a, MIPRE.LowDegree.BinaryPolynomial.zeroBits p) u).2

theorem MIPRE.LowDegree.BinaryPolynomial.length_frobeniusTrace (p a : Cost.BitStr) (u : Cost.Unary) (ha : List.length a = List.length p) : List.length (frobeniusTrace p a u).1 = List.length p ∧ List.length (frobeniusTrace p a u).2 = List.length p

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_fold_traceStep {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a c : Cost.BitStr) (u : Cost.Unary) (hroot : z ^ List.length p = evalBits z p) (ha : List.length a = List.length p) (hc : List.length c = List.length p) : evalBits z (List.foldl traceStep (p, a, c) u).2.1 = evalBits z a ^ 2 ^ List.length u ∧ evalBits z (List.foldl traceStep (p, a, c) u).2.2 = evalBits z c + ∑ i ∈ Finset.range (List.length u), evalBits z a ^ 2 ^ i

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_frobeniusTrace {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a : Cost.BitStr) (u : Cost.Unary) (hroot : z ^ List.length p = evalBits z p) (ha : List.length a = List.length p) : evalBits z (frobeniusTrace p a u).1 = evalBits z a ^ 2 ^ List.length u ∧ evalBits z (frobeniusTrace p a u).2 = ∑ i ∈ Finset.range (List.length u), evalBits z a ^ 2 ^ i

Squaring and accumulating computes the Frobenius orbit and its trace sum.

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_frobeniusTrace_trace {F : Type u_2} [Field F] [Finite F] [CharP F 2] [Algebra (ZMod 2) F] (z : F) (p a : Cost.BitStr) (hdegree : Module.finrank (ZMod 2) F = List.length p) (hroot : z ^ List.length p = evalBits z p) (ha : List.length a = List.length p) : evalBits z (frobeniusTrace p a (Cost.unary (List.length p))).2 = (algebraMap (ZMod 2) F) ((Algebra.trace (ZMod 2) F) (evalBits z a))

The accumulated sum is the algebraic trace, embedded into the extension field.

noncomputable def MIPRE.LowDegree.BinaryPolynomial.traceStepProg : Cost.PolyTimeFun (PowerState × Unit) PowerState

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.traceStep_bounded : traceStepProg.FoldBounded (9 * Polynomial.X + 9)

noncomputable def MIPRE.LowDegree.BinaryPolynomial.frobeniusTraceProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.Unary) (Cost.BitStr × Cost.BitStr)

Uniform computation of Frobenius iteration and the associated trace sum.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.frobeniusTraceProg_apply (p a : Cost.BitStr) (u : Cost.Unary) : frobeniusTraceProg.toFun (p, a, u) = frobeniusTrace p a u