Binary coefficient representations

The coefficient interpretation used by the public Shoup contract and by the independent polynomial algorithms. This module does not assume that an irreducible polynomial has already been constructed.

noncomputable def MIPRE.LowDegree.polyOfBits (l : List Bool) : Polynomial (ZMod 2)

The polynomial over 𝔽₂ whose coefficient of Tⁱ is bit i of l, least significant first --- the repository's little-endian bit convention (Cost.bitsVal, bitsOfNat).

Equations

• MIPRE.LowDegree.polyOfBits l = ∑ i ∈ Finset.range l.length, (Polynomial.monomial i) (if l.getD i false = true then 1 else 0)

theorem MIPRE.LowDegree.BinaryPolynomial.coeff_polyOfBits (l : Cost.BitStr) (i : ℕ) : (polyOfBits l).coeff i = ofBool (List.getD l i false)

The polynomial used by Shoup's contract reads the same coefficient bits.

theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_cons (b : Bool) (l : Cost.BitStr) : polyOfBits (b :: l) = Polynomial.C (ofBool b) + Polynomial.X * polyOfBits l

theorem MIPRE.LowDegree.BinaryPolynomial.natDegree_lt_length (l : Cost.BitStr) (h : (polyOfBits l).Monic) : (polyOfBits l).natDegree < List.length l

A monic polynomial's leading coefficient is present in its coefficient list.

theorem MIPRE.LowDegree.BinaryPolynomial.normalize_monic (l : Cost.BitStr) (h : (polyOfBits l).Monic) : polyOfBits (List.take (polyOfBits l).natDegree l ++ [true]) = polyOfBits l

Remove trailing zero coefficients and separate the leading monic coefficient.