Frobenius and trace in the effective Shoup field

@[instance_reducible]

noncomputable instance MIPRE.SAT.shoupBinField_algebra (k : ℕ) (hk : 1 ≤ k) : Algebra (ZMod 2) (shoupBinField k hk).carrier

Equations

• MIPRE.SAT.shoupBinField_algebra k hk = id inferInstance

theorem MIPRE.SAT.shoupBinField_finrank (k : ℕ) (hk : 1 ≤ k) : Module.finrank (ZMod 2) (shoupBinField k hk).carrier = k

The effective quotient field has the stated extension degree over the binary field.

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

Construct the field and perform a unary-specified number of Frobenius steps.

Equations

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

theorem MIPRE.SAT.shoupFrobeniusTraceProg_frobenius (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) (u : Cost.Unary) : (shoupFrobeniusTraceProg.toFun (Cost.unary k, (shoupBinField k hk).toBits a, u)).1 = (shoupBinField k hk).toBits (a ^ 2 ^ List.length u)

Canonical coordinates of the Frobenius iterate are computed uniformly.

theorem MIPRE.SAT.shoupFrobeniusTraceProg_period (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) : (shoupFrobeniusTraceProg.toFun (Cost.unary k, (shoupBinField k hk).toBits a, Cost.unary k)).1 = (shoupBinField k hk).toBits a

Computing k successive squarings gives the identity on the degree-k field.

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

The trace sum, returned as canonical coordinates in the extension field.

Equations

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

theorem MIPRE.SAT.shoupTraceProg_correct (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) : shoupTraceProg.toFun (Cost.unary k, (shoupBinField k hk).toBits a) = (shoupBinField k hk).toBits ((algebraMap (ZMod 2) (shoupBinField k hk).carrier) ((Algebra.trace (ZMod 2) (shoupBinField k hk).carrier) a))

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

Trace computation, including field construction, has polynomial runtime in k.