Uniform evaluation of field coefficient vectors

Coefficients are listed in increasing degree order. The program constructs the field modulus once, then uses Horner's rule. Its ambient polynomial bound also holds on malformed inputs: every step preserves the modulus and evaluation point, and the accumulator's bit length can only decrease.

This file does not parse answers or claim correctness of the Pauli decider. It supplies the arithmetic operation needed by its two line tests.

def MIPRE.Introspection.FieldPolynomialProgram.evalCoeffs {R : Type u_1} [Semiring R] (x : R) (coeffs : List R) : R

Evaluation of a coefficient list in increasing degree order.

Equations

• MIPRE.Introspection.FieldPolynomialProgram.evalCoeffs x coeffs = List.foldr (fun (c a : R) => a * x + c) 0 coeffs

@[simp]

theorem MIPRE.Introspection.FieldPolynomialProgram.evalCoeffs_nil {R : Type u_1} [Semiring R] (x : R) : evalCoeffs x [] = 0

@[simp]

theorem MIPRE.Introspection.FieldPolynomialProgram.evalCoeffs_cons {R : Type u_1} [Semiring R] (x c : R) (coeffs : List R) : evalCoeffs x (c :: coeffs) = evalCoeffs x coeffs * x + c

theorem MIPRE.Introspection.FieldPolynomialProgram.evalCoeffs_ofFn {R : Type u_1} [CommSemiring R] (x : R) {n : ℕ} (f : Fin n → R) : evalCoeffs x (List.ofFn f) = ∑ i : Fin n, f i * x ^ ↑i

This is the coefficient-vector evaluation used by the line-test semantics.

def MIPRE.Introspection.FieldPolynomialProgram.hornerStep (s : Cost.BitStr × Cost.BitStr × Cost.BitStr) (c : Cost.BitStr) : Cost.BitStr × Cost.BitStr × Cost.BitStr

Equations

• MIPRE.Introspection.FieldPolynomialProgram.hornerStep s c = (s.1, s.2.1, MIPRE.LowDegree.BinaryPolynomial.xorBits (MIPRE.LowDegree.BinaryPolynomial.mulReduce s.1 s.2.2 s.2.1) c)

theorem MIPRE.Introspection.FieldPolynomialProgram.hornerStep_width (s : Cost.BitStr × Cost.BitStr × Cost.BitStr) (c : Cost.BitStr) : List.length (hornerStep s c).2.2 ≤ List.length s.2.2

theorem MIPRE.Introspection.FieldPolynomialProgram.fold_hornerStep (l : List Cost.BitStr) (s : Cost.BitStr × Cost.BitStr × Cost.BitStr) : (List.foldl hornerStep s l).1 = s.1 ∧ (List.foldl hornerStep s l).2.1 = s.2.1 ∧ List.length (List.foldl hornerStep s l).2.2 ≤ List.length s.2.2

theorem MIPRE.Introspection.FieldPolynomialProgram.fold_hornerStep_acc (l : List Cost.BitStr) (p x a : Cost.BitStr) : (List.foldl hornerStep (p, x, a) l).2.2 = List.foldl (fun (a c : Cost.BitStr) => LowDegree.BinaryPolynomial.xorBits (LowDegree.BinaryPolynomial.mulReduce p a x) c) a l

noncomputable def MIPRE.Introspection.FieldPolynomialProgram.hornerStepProg : Cost.PolyTimeFun ((Cost.BitStr × Cost.BitStr × Cost.BitStr) × Cost.BitStr) (Cost.BitStr × Cost.BitStr × Cost.BitStr)

Equations

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

theorem MIPRE.Introspection.FieldPolynomialProgram.hornerStep_bounded : hornerStepProg.FoldBounded (5 * Polynomial.X + 5)

noncomputable def MIPRE.Introspection.FieldPolynomialProgram.hornerFoldProg : Cost.PolyTimeFun (List Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) Cost.BitStr

Horner evaluation with an explicit modulus, point and initial accumulator. The initial accumulator is useful for the correctness induction; ordinary polynomial evaluation initializes it to the field's zero vector.

Equations

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

noncomputable def MIPRE.Introspection.FieldPolynomialProgram.shoupHornerProg : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr × List Cost.BitStr) Cost.BitStr

One ambient program, uniform in both field width and coefficient count.

Equations

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

theorem MIPRE.Introspection.FieldPolynomialProgram.shoupHornerProg_correct (k : ℕ) (hk : 1 ≤ k) (x : (SAT.shoupBinField k hk).carrier) (coeffs : List (SAT.shoupBinField k hk).carrier) : shoupHornerProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).toBits x, List.map (SAT.shoupBinField k hk).toBits coeffs) = (SAT.shoupBinField k hk).toBits (evalCoeffs x coeffs)

theorem MIPRE.Introspection.FieldPolynomialProgram.shoupHornerProg_ofFn (k : ℕ) (hk : 1 ≤ k) {n : ℕ} (x : (SAT.shoupBinField k hk).carrier) (f : Fin n → (SAT.shoupBinField k hk).carrier) : shoupHornerProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).toBits x, (SAT.shoupBinField k hk).vecBits f) = (SAT.shoupBinField k hk).toBits (∑ i : Fin n, f i * x ^ ↑i)

Canonical fixed-length vectors evaluate to the expected power sum.