Binary exponentiation in a polynomial-basis field

The exponent remains a little-endian bit string. The loop performs one squaring and at most one multiplication per bit and keeps fixed-width coefficient vectors. Its polynomial bound also holds for malformed inputs.

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryPolynomial.PowerState : Type

Equations

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

def MIPRE.LowDegree.BinaryPolynomial.powerStep (s : PowerState) (b : Bool) : PowerState

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.powerStep_width (s : PowerState) (b : Bool) : (powerStep s b).1 = s.1 ∧ List.length (powerStep s b).2.1 ≤ List.length s.2.1 ∧ List.length (powerStep s b).2.2 ≤ List.length s.2.2

theorem MIPRE.LowDegree.BinaryPolynomial.fold_powerStep_width (l : Cost.BitStr) (s : PowerState) : (List.foldl powerStep s l).1 = s.1 ∧ List.length (List.foldl powerStep s l).2.1 ≤ List.length s.2.1 ∧ List.length (List.foldl powerStep s l).2.2 ≤ List.length s.2.2

theorem MIPRE.LowDegree.BinaryPolynomial.fold_powerStep_length (l p a c : Cost.BitStr) (ha : List.length a = List.length p) (hc : List.length c = List.length p) : List.length (List.foldl powerStep (p, a, c) l).2.2 = List.length p

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

Repeated squaring with a binary exponent.

Equations

• MIPRE.LowDegree.BinaryPolynomial.powerBits p a e = (List.foldl MIPRE.LowDegree.BinaryPolynomial.powerStep (p, a, MIPRE.LowDegree.BinaryPolynomial.oneBits p) e).2.2

theorem MIPRE.LowDegree.BinaryPolynomial.length_powerBits (p a e : Cost.BitStr) (ha : List.length a = List.length p) : List.length (powerBits p a e) = List.length p

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_fold_powerStep {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a c e : Cost.BitStr) (hroot : z ^ List.length p = evalBits z p) (ha : List.length a = List.length p) (hc : List.length c = List.length p) : evalBits z (List.foldl powerStep (p, a, c) e).2.2 = evalBits z c * evalBits z a ^ Cost.bitsVal e

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_powerBits {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p a e : Cost.BitStr) (hp : p ≠ []) (hroot : z ^ List.length p = evalBits z p) (ha : List.length a = List.length p) : evalBits z (powerBits p a e) = evalBits z a ^ Cost.bitsVal e

Correctness for every characteristic-two ring containing a root of the modulus.

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

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.powerStep_bounded : powerStepProg.FoldBounded (9 * Polynomial.X + 9)

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

One uniform ambient program for exponentiation with binary exponent input.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.powerBitsProg_apply (p a e : Cost.BitStr) : powerBitsProg.toFun (p, a, e) = powerBits p a e