Uniform inversion in the Shoup polynomial-basis field

def MIPRE.LowDegree.BinaryPolynomial.inverseExponent (p : Cost.BitStr) : Cost.BitStr

The exponent 2^k - 2, written directly in k bits rather than expanded in unary.

Equations

• MIPRE.LowDegree.BinaryPolynomial.inverseExponent p = false :: List.map (fun (x : Bool) => true) (List.tail p)

theorem MIPRE.LowDegree.BinaryPolynomial.bitsVal_ones (n : ℕ) : Cost.bitsVal (List.replicate n true) + 1 = 2 ^ n

theorem MIPRE.LowDegree.BinaryPolynomial.bitsVal_inverseExponent (p : Cost.BitStr) : Cost.bitsVal (inverseExponent p) = 2 ^ List.length p - 2

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

Inversion by binary exponentiation. Its specification requires a nonzero operand.

Equations

• MIPRE.LowDegree.BinaryPolynomial.inverseBits p a = MIPRE.LowDegree.BinaryPolynomial.powerBits p a (MIPRE.LowDegree.BinaryPolynomial.inverseExponent p)

theorem MIPRE.LowDegree.BinaryPolynomial.length_inverseBits (p a : Cost.BitStr) (ha : List.length a = List.length p) : List.length (inverseBits p a) = List.length p

theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_inverseBits {F : Type u_1} [Field F] [Fintype F] [CharP F 2] (z : F) (p a : Cost.BitStr) (hp : p ≠ []) (hcard : Fintype.card F = 2 ^ List.length p) (hroot : z ^ List.length p = evalBits z p) (ha : List.length a = List.length p) (hne : evalBits z a ≠ 0) : evalBits z (inverseBits p a) = (evalBits z a)⁻¹

Correctness in every finite characteristic-two field of the supplied cardinality.

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

Equations

• MIPRE.LowDegree.BinaryPolynomial.inverseExponentProg = (MIPRE.Cost.PolyTimeFun.const false).cons ((MIPRE.Cost.PolyTimeFun.const true).map.comp MIPRE.Cost.PolyTimeFun.tail)

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.inverseExponentProg_apply (p : Cost.BitStr) : inverseExponentProg.toFun p = inverseExponent p

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

Globally polynomial-time inversion routine, uniform in the supplied modulus.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.inverseBitsProg_apply (p a : Cost.BitStr) : inverseBitsProg.toFun (p, a) = inverseBits p a

noncomputable def MIPRE.SAT.shoupInvProg : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr) Cost.BitStr

Construct the Shoup modulus and invert a nonzero field element in its power basis.

Equations

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

theorem MIPRE.SAT.shoupInvProg_correct (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) (ha : a ≠ 0) : shoupInvProg.toFun (Cost.unary k, (shoupBinField k hk).toBits a) = (shoupBinField k hk).toBits a⁻¹

theorem MIPRE.SAT.shoupInvProg_time_le : ∃ (R : Polynomial ℕ), ∀ (k : ℕ) (a : Cost.BitStr), List.length a = k → ∃ t ≤ Polynomial.eval k R, shoupInvProg.code.Runs (Cost.encode (Cost.unary k, a)) (Cost.encode (shoupInvProg.toFun (Cost.unary k, a))) t

Including construction of the modulus, inversion takes polynomial time in the degree.