Uniform polynomial-time products of Frobenius translates

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryQuotient.NormState : Type

Modulus, binary polynomial to translate, and accumulating coefficient list.

Equations

• MIPRE.LowDegree.BinaryQuotient.NormState = (MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr)

def MIPRE.LowDegree.BinaryQuotient.normStep (s : NormState) (a : Cost.BitStr) : NormState

Multiply the accumulator by one translated copy of the binary polynomial.

Equations

• MIPRE.LowDegree.BinaryQuotient.normStep s a = (s.1, s.2.1, MIPRE.LowDegree.BinaryQuotient.mulCoeffLists s.1 (MIPRE.LowDegree.BinaryQuotient.translateBits s.1 a s.2.1) s.2.2)

theorem MIPRE.LowDegree.BinaryQuotient.fold_normStep_shape (pre : List Cost.BitStr) (p g : Cost.BitStr) (cs : List Cost.BitStr) : (List.foldl normStep (p, g, cs) pre).1 = p ∧ (List.foldl normStep (p, g, cs) pre).2.1 = g ∧ (List.foldl normStep (p, g, cs) pre).2.2.length ≤ cs.length + pre.length * List.length g

theorem MIPRE.LowDegree.BinaryQuotient.fold_normStep_width_le (pre : List Cost.BitStr) (p g : Cost.BitStr) (cs : List Cost.BitStr) (N : ℕ) (hp : List.length p ≤ N) (hc : ∀ c ∈ cs, List.length c ≤ N) (c : Cost.BitStr) : c ∈ (List.foldl normStep (p, g, cs) pre).2.2 → List.length c ≤ N

theorem MIPRE.LowDegree.BinaryQuotient.fold_normStep_width (pre : List Cost.BitStr) (p g : Cost.BitStr) (cs : List Cost.BitStr) (ha : ∀ a ∈ pre, List.length a = List.length p) (hc : ∀ c ∈ cs, List.length c = List.length p) (c : Cost.BitStr) : c ∈ (List.foldl normStep (p, g, cs) pre).2.2 → List.length c = List.length p

Valid quotient widths are preserved by the translate-product loop.

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_fold_normStep {R : Type u_1} [CommRing R] [CharP R 2] [Algebra (ZMod 2) R] (z : R) (pre : List Cost.BitStr) (p g : Cost.BitStr) (cs : List Cost.BitStr) (hp : p ≠ []) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (ha : ∀ a ∈ pre, List.length a = List.length p) : coeffPolynomial z (List.foldl normStep (p, g, cs) pre).2.2 = (List.map (fun (a : Cost.BitStr) => translatedPolynomial (polyOfBits g) (BinaryPolynomial.evalBits z a)) pre).prod * coeffPolynomial z cs

The loop computes precisely the product of the specified translated polynomials.

def MIPRE.LowDegree.BinaryQuotient.normProductBits (p g : Cost.BitStr) (as : List Cost.BitStr) : List Cost.BitStr

Product of the translates specified by a list of quotient elements.

Equations

• MIPRE.LowDegree.BinaryQuotient.normProductBits p g as = (List.foldl MIPRE.LowDegree.BinaryQuotient.normStep (p, g, [MIPRE.LowDegree.BinaryPolynomial.oneBits p]) as).2.2

theorem MIPRE.LowDegree.BinaryQuotient.coeffPolynomial_normProductBits {R : Type u_1} [CommRing R] [CharP R 2] [Algebra (ZMod 2) R] (z : R) (p g : Cost.BitStr) (as : List Cost.BitStr) (hp : p ≠ []) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) (ha : ∀ a ∈ as, List.length a = List.length p) : coeffPolynomial z (normProductBits p g as) = (List.map (fun (a : Cost.BitStr) => translatedPolynomial (polyOfBits g) (BinaryPolynomial.evalBits z a)) as).prod

The printed coefficient list represents the prescribed translate product.

noncomputable def MIPRE.LowDegree.BinaryQuotient.normStepProg : Cost.PolyTimeFun (NormState × Cost.BitStr) NormState

Equations

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

theorem MIPRE.LowDegree.BinaryQuotient.normStep_bounded : normStepProg.FoldBounded (30 * Polynomial.X ^ 3 + 30 * Polynomial.X ^ 2 + 30 * Polynomial.X + 30)

noncomputable def MIPRE.LowDegree.BinaryQuotient.normProductBitsProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

One globally polynomial-time program for a supplied list of polynomial translates.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.normProductBitsProg_apply (p g : Cost.BitStr) (as : List Cost.BitStr) : normProductBitsProg.toFun (p, g, as) = normProductBits p g as

def MIPRE.LowDegree.BinaryQuotient.rootBits (p : Cost.BitStr) : Cost.BitStr

A fixed-width encoding of the canonical quotient root, also valid in degree one.

Equations

• MIPRE.LowDegree.BinaryQuotient.rootBits p = MIPRE.LowDegree.BinaryPolynomial.shiftReduce p (MIPRE.LowDegree.BinaryPolynomial.oneBits p)

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.length_rootBits (p : Cost.BitStr) : List.length (rootBits p) = List.length p

theorem MIPRE.LowDegree.BinaryQuotient.evalBits_rootBits {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p : Cost.BitStr) (hp : p ≠ []) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) : BinaryPolynomial.evalBits z (rootBits p) = z

noncomputable def MIPRE.LowDegree.BinaryQuotient.rootBitsProg : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.rootBitsProg_apply (p : Cost.BitStr) : rootBitsProg.toFun p = rootBits p

def MIPRE.LowDegree.BinaryQuotient.composedSumBits (p g : Cost.BitStr) : Cost.BitStr

Binary output of the composed-sum construction for the supplied monic modulus and polynomial.

Equations

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

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

The composed-sum constructor is polynomial-time on every pair of raw lists.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.composedSumBitsProg_apply (p g : Cost.BitStr) : composedSumBitsProg.toFun (p, g) = composedSumBits p g