Explicit polynomial-time Frobenius-stride traces

def MIPRE.LowDegree.BinaryQuotient.squareFuel (s : SquareState) : Unit → SquareState

Repeat squaring once per unary stride bit.

Equations

• MIPRE.LowDegree.BinaryQuotient.squareFuel s x✝ = MIPRE.LowDegree.BinaryQuotient.squareStep s

theorem MIPRE.LowDegree.BinaryQuotient.fold_squareFuel (u : Cost.Unary) (s : SquareState) : List.foldl squareFuel s u = squareStep^[List.length u] s

noncomputable def MIPRE.LowDegree.BinaryQuotient.squareFuelProg : Cost.PolyTimeFun (SquareState × Unit) SquareState

Equations

• MIPRE.LowDegree.BinaryQuotient.squareFuelProg = (MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.fst).pair (MIPRE.LowDegree.BinaryQuotient.squareProg.comp MIPRE.Cost.PolyTimeFun.fst)

theorem MIPRE.LowDegree.BinaryQuotient.squareFuel_bounded : squareFuelProg.FoldBounded (5 * Polynomial.X + 5)

def MIPRE.LowDegree.BinaryQuotient.frobeniusBits (u : Cost.Unary) (p a : Cost.BitStr) : Cost.BitStr

A supplied unary number of squarings in the explicit binary quotient.

Equations

• MIPRE.LowDegree.BinaryQuotient.frobeniusBits u p a = (MIPRE.LowDegree.BinaryQuotient.squareStep^[List.length u] (p, a)).2

noncomputable def MIPRE.LowDegree.BinaryQuotient.frobeniusBitsProg : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr × Cost.BitStr) Cost.BitStr

The stride Frobenius program is globally polynomially bounded.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.frobeniusBitsProg_apply (u : Cost.Unary) (p a : Cost.BitStr) : frobeniusBitsProg.toFun (u, p, a) = frobeniusBits u p a

theorem MIPRE.LowDegree.BinaryQuotient.frobeniusBits_width_le (u : Cost.Unary) (p a : Cost.BitStr) : List.length (frobeniusBits u p a) ≤ List.length a

Repeated squaring never increases even a malformed coefficient width.

theorem MIPRE.LowDegree.BinaryQuotient.frobeniusBits_width (u : Cost.Unary) (p a : Cost.BitStr) (ha : List.length a = List.length p) : List.length (frobeniusBits u p a) = List.length p

The modulus width is preserved on valid quotient elements.

theorem MIPRE.LowDegree.BinaryQuotient.evalBits_frobeniusBits {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (u : Cost.Unary) (p a : Cost.BitStr) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (ha : List.length a = List.length p) : BinaryPolynomial.evalBits z (frobeniusBits u p a) = BinaryPolynomial.evalBits z a ^ 2 ^ List.length u

The supplied stride is the exponent of the Frobenius iterate.

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryQuotient.TraceState : Type

Stride, modulus, accumulated sum, and the current Frobenius conjugate.

Equations

• MIPRE.LowDegree.BinaryQuotient.TraceState = (MIPRE.Cost.Unary × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

def MIPRE.LowDegree.BinaryQuotient.traceStep (s : TraceState) : Unit → TraceState

Add the current conjugate and advance by the fixed Frobenius stride.

Equations

• MIPRE.LowDegree.BinaryQuotient.traceStep s x✝ = (s.1, s.2.1, MIPRE.LowDegree.BinaryPolynomial.xorBits s.2.2.1 s.2.2.2, MIPRE.LowDegree.BinaryQuotient.frobeniusBits s.1 s.2.1 s.2.2.2)

theorem MIPRE.LowDegree.BinaryQuotient.fold_traceStep_shape (u : Cost.Unary) (s : TraceState) : (List.foldl traceStep s u).1 = s.1 ∧ (List.foldl traceStep s u).2.1 = s.2.1 ∧ List.length (List.foldl traceStep s u).2.2.1 ≤ List.length s.2.2.1 ∧ List.length (List.foldl traceStep s u).2.2.2 ≤ List.length s.2.2.2

All runtime state widths stay below their initial widths.

theorem MIPRE.LowDegree.BinaryQuotient.fold_traceStep_width (u r : Cost.Unary) (p c a : Cost.BitStr) (hc : List.length c = List.length p) (ha : List.length a = List.length p) : List.length (List.foldl traceStep (r, p, c, a) u).2.2.1 = List.length p ∧ List.length (List.foldl traceStep (r, p, c, a) u).2.2.2 = List.length p

Both active coefficient vectors retain the modulus width.

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

The loop computes the trace-shaped sum, with the supplied initial accumulator.

noncomputable def MIPRE.LowDegree.BinaryQuotient.traceStepProg : Cost.PolyTimeFun (TraceState × Unit) TraceState

Equations

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

theorem MIPRE.LowDegree.BinaryQuotient.traceStep_bounded : traceStepProg.FoldBounded (10 * Polynomial.X + 10)

def MIPRE.LowDegree.BinaryQuotient.traceBits (m r : Cost.Unary) (p a : Cost.BitStr) : Cost.BitStr

The binary vector for the sum of the requested Frobenius-stride conjugates.

Equations

• MIPRE.LowDegree.BinaryQuotient.traceBits m r p a = (List.foldl MIPRE.LowDegree.BinaryQuotient.traceStep (r, p, MIPRE.LowDegree.BinaryPolynomial.zeroBits p, a) m).2.2.1

noncomputable def MIPRE.LowDegree.BinaryQuotient.traceBitsProg : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.BitStr × Cost.BitStr) Cost.BitStr

One globally polynomial-time program computes every such modular trace sum.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.traceBitsProg_apply (m r : Cost.Unary) (p a : Cost.BitStr) : traceBitsProg.toFun (m, r, p, a) = traceBits m r p a

theorem MIPRE.LowDegree.BinaryQuotient.traceBits_width (m r : Cost.Unary) (p a : Cost.BitStr) (ha : List.length a = List.length p) : List.length (traceBits m r p a) = List.length p

The modular trace output has exactly the field representation width.

theorem MIPRE.LowDegree.BinaryQuotient.evalBits_traceBits {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (m r : Cost.Unary) (p a : Cost.BitStr) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (ha : List.length a = List.length p) : BinaryPolynomial.evalBits z (traceBits m r p a) = ∑ i ∈ Finset.range (List.length m), BinaryPolynomial.evalBits z a ^ 2 ^ (List.length r * i)

The program's semantics are the finite sum used in Shoup's trace construction.