Binary coefficient lists and carryless multiplication

A list of bits represents a polynomial over ZMod 2, with its constant coefficient first. Trailing false bits are high zero coefficients and may be retained. mulBits computes every output coefficient as the parity of the number of contributing pairs of true input coefficients.

The output has length a.length + b.length, including when one operand is empty. For two nonempty inputs this leaves one high zero beyond the largest possible nonzero product coefficient. This fixed length avoids trimming and is convenient for subsequent bounded polynomial arithmetic.

This coefficient representation differs from the fixed natural-polynomial Horner programs in TM.binaryPolynomialEvalTM: here both binary polynomials are runtime inputs, and addition of coefficients is modulo two.

def Complexity.BitPolynomial.ofBits (bits : List Bool) : Polynomial (ZMod 2)

Interpret a coefficient list over ZMod 2, with the constant coefficient first.

Equations

• Complexity.BitPolynomial.ofBits bits = (Polynomial.ofFn bits.length) fun (i : Fin bits.length) => ↑bits[i].toNat

def Complexity.BitPolynomial.mulBits (a b : List Bool) : List Bool

Carryless multiplication, padded to the sum of the input lengths.

Equations

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

def Complexity.BitPolynomial.mulEval (z : List Bool) : List Bool

Multiply two coefficient lists supplied through the standard pairing codec.

Equations

• Complexity.BitPolynomial.mulEval z = Complexity.BitPolynomial.mulBits (Complexity.pairFst z) (Complexity.pairSnd z)