Horner evaluation of flat binary coefficient blocks

Block j consists of at most width bits beginning at j*width, with absent bits interpreted as zero by the polynomial codec. Blocks occur in increasing polynomial degree. The count-list fold processes them from highest to lowest using the index total - tail.length - 1.

Every state has the modulus degree in bits. A zero modulus explicitly gives an empty state, and a zero count starts from the zero polynomial. The encoded evaluator reads pair (pair (pair coeffs widthWord) (pair seed modulus)) count; width and count are the lengths of their runtime words.

def Complexity.BitPolynomial.coefficientBlock (coeffs : List Bool) (width j : ℕ) : List Bool

A coefficient block, with missing high coefficients implicitly equal to zero.

Equations

• Complexity.BitPolynomial.coefficientBlock coeffs width j = List.take width (List.drop (j * width) coeffs)

def Complexity.BitPolynomial.blockEvalStep (coefficient seed modulus state : List Bool) : List Bool

One Horner step, guarded to return the empty list for a zero modulus.

Equations

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

def Complexity.BitPolynomial.blockEvalScan (coeffs : List Bool) (width : ℕ) (seed modulus : List Bool) (total : ℕ) : List Bool → List Bool

A tail-first fold visiting coefficient indices total-1, total-2, and so on. The partial-fold semantic invariant requires the count length to be at most total.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BitPolynomial.blockEvalScan coeffs width seed modulus total [] = List.replicate (Complexity.BitPolynomial.significantLength modulus - 1) false

def Complexity.BitPolynomial.blockEvalBits (coeffs : List Bool) (width : ℕ) (seed modulus count : List Bool) : List Bool

Evaluate exactly as many coefficient blocks as there are bits in count.

Equations

• Complexity.BitPolynomial.blockEvalBits coeffs width seed modulus count = Complexity.BitPolynomial.blockEvalScan coeffs width seed modulus count.length count

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

The total paired-input evaluator for a flat sequence of binary coefficient blocks.

Equations

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