Uniform programs for Frobenius orbits and cyclic operators

theorem MIPRE.SAT.instFactPrimeOfNatNat_mIPRE_5 : Fact (Nat.Prime 2)

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

Equations

• MIPRE.SAT.shoupSquareStateProg = MIPRE.Cost.PolyTimeFun.fst.pair MIPRE.SAT.shoupSquareProg

theorem MIPRE.SAT.shoupSquareProg_length_le (u : Cost.Unary) (v : Cost.BitStr) : List.length (shoupSquareProg.toFun (u, v)) ≤ List.length v

theorem MIPRE.SAT.shoupSquareStateProg_iterate_width (n : ℕ) (s : Cost.Unary × Cost.BitStr) : (shoupSquareStateProg.toFun^[n] s).1 = s.1 ∧ List.length (shoupSquareStateProg.toFun^[n] s).2 ≤ List.length s.2

theorem MIPRE.SAT.shoupSquareStateProg_iterate_size (n : ℕ) (s : Cost.Unary × Cost.BitStr) : Cost.esize (shoupSquareStateProg.toFun^[n] s) ≤ Polynomial.eval (Cost.esize s) (5 * Polynomial.X + 5)

theorem MIPRE.SAT.shoupSquareStateProg_iterate_correct (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) (n : ℕ) : shoupSquareStateProg.toFun^[n] (Cost.unary k, (shoupBinField k hk).toBits a) = (Cost.unary k, (shoupBinField k hk).toBits (a ^ 2 ^ n))

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

Print exactly k successive Frobenius powers of an encoded field element.

Equations

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

theorem MIPRE.SAT.shoupOrbitProg_correct (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) : shoupOrbitProg.toFun (Cost.unary k, (shoupBinField k hk).toBits a) = List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (a ^ 2 ^ ↑i)

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

Evaluate a linearized polynomial from its cyclic coefficient vector.

Equations

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

theorem MIPRE.SAT.shoupActionProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (z : AddMonoidAlgebra (ZMod 2) (Fin k)) (a : (shoupBinField k hk).carrier) : shoupActionProg.toFun (Cost.unary k, LowDegree.BinaryLinear.vectorBits ((LowDegree.BinaryLinear.groupCoordinates k) z), (shoupBinField k hk).toBits a) = (shoupBinField k hk).toBits (((shoupFrobeniusAction k hk) z) a)