Uniform sums and products of coefficient vectors

def MIPRE.LowDegree.BinaryPolynomial.arithmeticStep (mul : Bool) (s : Cost.BitStr × Cost.BitStr) (b : Cost.BitStr) : Cost.BitStr × Cost.BitStr

Equations

• MIPRE.LowDegree.BinaryPolynomial.arithmeticStep mul s b = (s.1, if mul = true then MIPRE.LowDegree.BinaryPolynomial.mulReduce s.1 s.2 b else MIPRE.LowDegree.BinaryPolynomial.xorBits s.2 b)

theorem MIPRE.LowDegree.BinaryPolynomial.arithmeticStep_width (mul : Bool) (s : Cost.BitStr × Cost.BitStr) (b : Cost.BitStr) : List.length (arithmeticStep mul s b).2 ≤ List.length s.2

theorem MIPRE.LowDegree.BinaryPolynomial.fold_arithmeticStep (mul : Bool) (l : List Cost.BitStr) (s : Cost.BitStr × Cost.BitStr) : (List.foldl (arithmeticStep mul) s l).1 = s.1 ∧ List.length (List.foldl (arithmeticStep mul) s l).2 ≤ List.length s.2

def MIPRE.LowDegree.BinaryPolynomial.arithmeticFold (mul : Bool) (p a : Cost.BitStr) (l : List Cost.BitStr) : Cost.BitStr

Sum or product, starting from a supplied coefficient vector.

Equations

• MIPRE.LowDegree.BinaryPolynomial.arithmeticFold mul p a l = (List.foldl (MIPRE.LowDegree.BinaryPolynomial.arithmeticStep mul) (p, a) l).2

theorem MIPRE.LowDegree.BinaryPolynomial.arithmeticFold_cons (mul : Bool) (p a b : Cost.BitStr) (l : List Cost.BitStr) : arithmeticFold mul p a (b :: l) = arithmeticFold mul p (if mul = true then mulReduce p a b else xorBits a b) l

theorem MIPRE.LowDegree.BinaryPolynomial.arithmeticFold_add_width (p a : Cost.BitStr) (l : List Cost.BitStr) (ha : List.length a = List.length p) (hl : ∀ b ∈ l, List.length b = List.length p) : List.length (arithmeticFold false p a l) = List.length p

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_arithmeticFold_mul {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a : Cost.BitStr) (l : List Cost.BitStr) (ha : List.length a = List.length p) (hroot : z ^ List.length p = evalBits z p) : evalBits z (arithmeticFold true p a l) = evalBits z a * (List.map (evalBits z) l).prod

A modular product fold computes the product of all decoded operands.

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_arithmeticFold_add {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a : Cost.BitStr) (l : List Cost.BitStr) (ha : List.length a = List.length p) (hl : ∀ b ∈ l, List.length b = List.length p) : evalBits z (arithmeticFold false p a l) = evalBits z a + (List.map (evalBits z) l).sum

A fixed-width XOR fold computes the sum of all decoded operands.

noncomputable def MIPRE.LowDegree.BinaryPolynomial.arithmeticStepProg (mul : Bool) : Cost.PolyTimeFun ((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.LowDegree.BinaryPolynomial.arithmeticStep_bounded (mul : Bool) : (arithmeticStepProg mul).FoldBounded (5 * Polynomial.X + 5)

noncomputable def MIPRE.LowDegree.BinaryPolynomial.arithmeticFoldProg (mul : Bool) : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × List Cost.BitStr) Cost.BitStr

Globally polynomial-time summation or multiplication of coefficient vectors. The modulus and initial accumulator are explicit inputs.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.arithmeticFoldProg_apply (mul : Bool) (p a : Cost.BitStr) (l : List Cost.BitStr) : (arithmeticFoldProg mul).toFun (p, a, l) = arithmeticFold mul p a l