Binary polynomial arithmetic on coefficient lists

Coefficient lists are little-endian. XOR implements addition, and multiplication by the indeterminate is reduced using the lower coefficients of a monic modulus. The semantic lemmas work in every characteristic-two commutative ring containing a root of that modulus; the programs are uniform in the coefficient lists.

def MIPRE.LowDegree.BinaryPolynomial.evalBits {R : Type u_1} [CommRing R] (z : R) : Cost.BitStr → R

Evaluate a little-endian binary coefficient list by Horner's rule.

Equations

• MIPRE.LowDegree.BinaryPolynomial.evalBits z [] = 0
• MIPRE.LowDegree.BinaryPolynomial.evalBits z (b :: l) = MIPRE.LowDegree.ofBool b + z * MIPRE.LowDegree.BinaryPolynomial.evalBits z l

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_nil {R : Type u_1} [CommRing R] (z : R) : evalBits z [] = 0

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_cons {R : Type u_1} [CommRing R] (z : R) (b : Bool) (l : Cost.BitStr) : evalBits z (b :: l) = ofBool b + z * evalBits z l

theorem MIPRE.LowDegree.BinaryPolynomial.eval₂_polyOfBits {R : Type u_1} [CommRing R] (f : ZMod 2 →+* R) (z : R) (l : Cost.BitStr) : Polynomial.eval₂ f z (polyOfBits l) = evalBits z l

Horner semantics agrees with evaluation of the coefficient polynomial.

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_append {R : Type u_1} [CommRing R] (z : R) (a b : Cost.BitStr) : evalBits z (a ++ b) = evalBits z a + z ^ List.length a * evalBits z b

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_zero {R : Type u_1} [CommRing R] (z : R) (n : ℕ) : evalBits z (List.replicate n false) = 0

def MIPRE.LowDegree.BinaryPolynomial.xorBits (a b : Cost.BitStr) : Cost.BitStr

Fixed-width XOR, used only with equal-width operands in correctness lemmas.

Equations

• MIPRE.LowDegree.BinaryPolynomial.xorBits a b = List.zipWith xor a b

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.length_xorBits (a b : Cost.BitStr) : List.length (xorBits a b) = min (List.length a) (List.length b)

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_xor {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (a b : Cost.BitStr) (hlen : List.length a = List.length b) : evalBits z (xorBits a b) = evalBits z a + evalBits z b

def MIPRE.LowDegree.BinaryPolynomial.shiftLow (a : Cost.BitStr) : Cost.BitStr

Shift by one coefficient and discard the new highest coefficient.

Equations

• MIPRE.LowDegree.BinaryPolynomial.shiftLow a = (false :: a).dropLast

def MIPRE.LowDegree.BinaryPolynomial.shiftReduce (p a : Cost.BitStr) : Cost.BitStr

Multiply by the indeterminate modulo X^k + p, with p represented by exactly k lower coefficients.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.length_shiftLow (a : Cost.BitStr) : List.length (shiftLow a) = List.length a

theorem MIPRE.LowDegree.BinaryPolynomial.length_shiftReduce_le (p a : Cost.BitStr) : List.length (shiftReduce p a) ≤ List.length a

theorem MIPRE.LowDegree.BinaryPolynomial.length_shiftReduce (p a : Cost.BitStr) (h : List.length a = List.length p) : List.length (shiftReduce p a) = List.length p

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_shiftLow {R : Type u_1} [CommRing R] (z : R) (a : Cost.BitStr) : evalBits z (shiftLow a) + z ^ List.length a * ofBool (List.getLastD a false) = z * evalBits z a

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_shiftReduce {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a : Cost.BitStr) (hlen : List.length a = List.length p) (hroot : z ^ List.length p = evalBits z p) : evalBits z (shiftReduce p a) = z * evalBits z a

Reduction is correct whenever the chosen element satisfies the monic modulus.

def MIPRE.LowDegree.BinaryPolynomial.mulReduce (p a b : Cost.BitStr) : Cost.BitStr

Horner multiplication, reducing after every shift.

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.length_mulReduce_le (p a b : Cost.BitStr) : List.length (mulReduce p a b) ≤ List.length a

Even malformed moduli and operands cannot increase the accumulator width.

theorem MIPRE.LowDegree.BinaryPolynomial.length_mulReduce (p a b : Cost.BitStr) (h : List.length a = List.length p) : List.length (mulReduce p a b) = List.length p

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_mulReduce {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a b : Cost.BitStr) (hlen : List.length a = List.length p) (hroot : z ^ List.length p = evalBits z p) : evalBits z (mulReduce p a b) = evalBits z a * evalBits z b

The reduced multiplication algorithm computes multiplication in every characteristic-two algebra in which the specified monic modulus vanishes.

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

Take a unary-specified number of coefficients in polynomial time.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.takeBitsProg_apply (p : Cost.Unary × Cost.BitStr) : takeBitsProg.toFun p = List.take (List.length p.1) p.2

noncomputable def MIPRE.LowDegree.BinaryPolynomial.xorBitProg : Cost.PolyTimeFun (Bool × Bool) Bool

XOR of two bits, as an ambient program.

Equations

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

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

Uniform polynomial-time addition of fixed-width coefficient vectors.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.xorBitsProg_apply (p : Cost.BitStr × Cost.BitStr) : xorBitsProg.toFun p = xorBits p.1 p.2

noncomputable def MIPRE.LowDegree.BinaryPolynomial.headProg : Cost.PolyTimeFun Cost.BitStr Bool

Equations

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

noncomputable def MIPRE.LowDegree.BinaryPolynomial.tailProg : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Equations

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

noncomputable def MIPRE.LowDegree.BinaryPolynomial.shiftLowProg : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Equations

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

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

Uniform polynomial-time multiplication by the indeterminate modulo a binary monic polynomial. The input is the lower-coefficient vector and the operand.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.shiftReduceProg_apply (p : Cost.BitStr × Cost.BitStr) : shiftReduceProg.toFun p = shiftReduce p.1 p.2

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryPolynomial.MulState : Type

Equations

• MIPRE.LowDegree.BinaryPolynomial.MulState = (MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

def MIPRE.LowDegree.BinaryPolynomial.mulStep (s : MulState) (bit : Bool) : MulState

Equations

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

noncomputable def MIPRE.LowDegree.BinaryPolynomial.mulStepProg : Cost.PolyTimeFun (MulState × Bool) MulState

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.mulStepProg_apply (s : MulState) (bit : Bool) : mulStepProg.toFun (s, bit) = mulStep s bit

theorem MIPRE.LowDegree.BinaryPolynomial.mulStep_length (s : MulState) (bit : Bool) : List.length (mulStep s bit).2.2 ≤ List.length s.2.2

theorem MIPRE.LowDegree.BinaryPolynomial.foldl_mulStep (l : Cost.BitStr) (s : MulState) : (List.foldl mulStep s l).1 = s.1 ∧ (List.foldl mulStep s l).2.1 = s.2.1 ∧ List.length (List.foldl mulStep s l).2.2 ≤ List.length s.2.2

theorem MIPRE.LowDegree.BinaryPolynomial.mulStepProg_bounded : mulStepProg.FoldBounded (4 * Polynomial.X + 4)

theorem MIPRE.LowDegree.BinaryPolynomial.foldr_mulStep (l p a acc : Cost.BitStr) : List.foldr (fun (bit : Bool) (s : MulState) => mulStep s bit) (p, a, acc) l = (p, a, List.foldr (fun (bit : Bool) (v : Cost.BitStr) => if bit = true then xorBits (shiftReduce p v) a else shiftReduce p v) acc l)

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

Uniform polynomial-time multiplication modulo a binary monic polynomial. The input carries its lower coefficients and the two operands.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.mulReduceProg_apply (s : Cost.BitStr × Cost.BitStr × Cost.BitStr) : mulReduceProg.toFun s = mulReduce s.1 s.2.1 s.2.2