Binary fields represented in the polynomial power basis

Unlike an arbitrary basis of a Galois field, the power basis of F₂[X]/(f) connects directly to the uniform coefficient-list programs. This is the field representation needed for the classical PCP's arithmetic. A self-dual normal representation and its change-of-basis algorithm remain separate constructions.

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

def MIPRE.SAT.bitOfCoeff (z : ZMod 2) : Bool

Equations

• MIPRE.SAT.bitOfCoeff z = decide (z = 1)

theorem MIPRE.SAT.ofBool_bitOfCoeff (z : ZMod 2) : LowDegree.ofBool (bitOfCoeff z) = z

theorem MIPRE.SAT.bitOfCoeff_ofBool (b : Bool) : bitOfCoeff (LowDegree.ofBool b) = b

theorem MIPRE.SAT.instCharPAdjoinRootZModOfNatNat_mIPRE (f : Polynomial (ZMod 2)) [Fact (Irreducible f)] : CharP (AdjoinRoot f) 2

noncomputable def MIPRE.SAT.quotientBinField (f : Polynomial (ZMod 2)) (hf : f.Monic) [Fact (Irreducible f)] : BinField f.natDegree

A binary field with coefficient bits in the power basis of a monic irreducible polynomial. The basis is specified, rather than chosen by abstract finite-field existence.

Equations

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

theorem MIPRE.SAT.quotientBinField_toBits_ofBits (f : Polynomial (ZMod 2)) (hf : f.Monic) [Fact (Irreducible f)] (l : Cost.BitStr) (hlen : List.length l = f.natDegree) : (quotientBinField f hf).toBits ((quotientBinField f hf).ofBits l) = l

Every correctly sized bit string is the canonical representation of its decoded field element. In particular, raw equality tests are faithful.

theorem MIPRE.SAT.quotientBinField_ofBits (f : Polynomial (ZMod 2)) (hf : f.Monic) [Fact (Irreducible f)] (l : Cost.BitStr) (hlen : List.length l = f.natDegree) : (quotientBinField f hf).ofBits l = LowDegree.BinaryPolynomial.evalBits (AdjoinRoot.root f) l

Correct-width coefficient decoding is evaluation at the quotient's root.

theorem MIPRE.SAT.quotient_evalBits_eq_iff (f : Polynomial (ZMod 2)) (hf : f.Monic) [Fact (Irreducible f)] (a b : Cost.BitStr) (ha : List.length a = f.natDegree) (hb : List.length b = f.natDegree) : LowDegree.BinaryPolynomial.evalBits (AdjoinRoot.root f) a = LowDegree.BinaryPolynomial.evalBits (AdjoinRoot.root f) b ↔ a = b

Equality of correctly sized coefficient vectors is equivalent to equality of their evaluations at the irreducible quotient's root.

theorem MIPRE.SAT.quotient_root_eq (f : Polynomial (ZMod 2)) [Fact (Irreducible f)] (p : Cost.BitStr) (hpoly : f = LowDegree.polyOfBits (p ++ [true])) : AdjoinRoot.root f ^ List.length p = LowDegree.BinaryPolynomial.evalBits (AdjoinRoot.root f) p

A coefficient vector defining the lower part of the modulus satisfies the root equation consumed by the arithmetic programs.

theorem MIPRE.SAT.quotientBinField_add (f : Polynomial (ZMod 2)) (hf : f.Monic) [Fact (Irreducible f)] (a b : Cost.BitStr) (ha : List.length a = f.natDegree) (hb : List.length b = f.natDegree) : (quotientBinField f hf).ofBits (LowDegree.BinaryPolynomial.xorBitsProg.toFun (a, b)) = (quotientBinField f hf).ofBits a + (quotientBinField f hf).ofBits b

The uniform XOR program implements field addition on correctly sized inputs.

theorem MIPRE.SAT.quotientBinField_mul (f : Polynomial (ZMod 2)) (hf : f.Monic) [Fact (Irreducible f)] (p a b : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = LowDegree.polyOfBits (p ++ [true])) (ha : List.length a = f.natDegree) (hb : List.length b = f.natDegree) : (quotientBinField f hf).ofBits (LowDegree.BinaryPolynomial.mulReduceProg.toFun (p, a, b)) = (quotientBinField f hf).ofBits a * (quotientBinField f hf).ofBits b

The uniform modular-multiplication program implements field multiplication.

noncomputable def MIPRE.SAT.shoupFieldModel (k : ℕ) (hk : 1 ≤ k) : BinField (LowDegree.polyOfBits (LowDegree.shoupIrreducible.toFun (Cost.unary k))).natDegree

Shoup's concrete quotient model, before transporting the degree equality.

Equations

• MIPRE.SAT.shoupFieldModel k hk = MIPRE.SAT.quotientBinField (MIPRE.LowDegree.polyOfBits (MIPRE.LowDegree.shoupIrreducible.toFun (MIPRE.Cost.unary k))) ⋯

noncomputable def MIPRE.SAT.shoupBinField (k : ℕ) (hk : 1 ≤ k) : BinField k

A field of size 2^k in the polynomial basis supplied by Shoup's algorithm.

Equations

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

instance MIPRE.SAT.shoupBinField_charP (k : ℕ) (hk : 1 ≤ k) : CharP (shoupBinField k hk).carrier 2

The degree metadata does not change the quotient carrier or its arithmetic.

theorem MIPRE.SAT.shoupBinField_toBits_ofBits (k : ℕ) (hk : 1 ≤ k) (l : Cost.BitStr) (hl : List.length l = k) : (shoupBinField k hk).toBits ((shoupBinField k hk).ofBits l) = l

Canonical decoding is unchanged by the explicit degree bookkeeping.

noncomputable def MIPRE.SAT.shoupAdmissibleField (k : ℕ) (hk : Odd k) : BinField k

The admissible field family with exactly the domain required by PcpDecider.fld.

Equations

• MIPRE.SAT.shoupAdmissibleField k hk = MIPRE.SAT.shoupBinField k ⋯

noncomputable def MIPRE.SAT.shoupRoot (k : ℕ) (hk : 1 ≤ k) : (shoupBinField k hk).carrier

The distinguished root in the explicit Shoup field carrier.

Equations

• MIPRE.SAT.shoupRoot k hk = AdjoinRoot.root (MIPRE.LowDegree.polyOfBits (MIPRE.LowDegree.shoupIrreducible.toFun (MIPRE.Cost.unary k)))

theorem MIPRE.SAT.shoupRoot_equation (k : ℕ) (hk : 1 ≤ k) : shoupRoot k hk ^ List.length (LowDegree.BinaryPolynomial.shoupLowerCoeffs.toFun (Cost.unary k)) = LowDegree.BinaryPolynomial.evalBits (shoupRoot k hk) (LowDegree.BinaryPolynomial.shoupLowerCoeffs.toFun (Cost.unary k))

theorem MIPRE.SAT.shoupRoot_eval_toBits (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) : LowDegree.BinaryPolynomial.evalBits (shoupRoot k hk) ((shoupBinField k hk).toBits a) = a

A canonical Shoup coefficient vector evaluates to its original field element.

theorem MIPRE.SAT.shoupRoot_eval_eq_iff (k : ℕ) (hk : 1 ≤ k) (a b : Cost.BitStr) (ha : List.length a = k) (hb : List.length b = k) : LowDegree.BinaryPolynomial.evalBits (shoupRoot k hk) a = LowDegree.BinaryPolynomial.evalBits (shoupRoot k hk) b ↔ a = b

Equality at the Shoup root is faithful on the verifier's fixed-width vectors.

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

Compute the modulus from unary k, then multiply the two coefficient vectors. This is one uniform ambient program, with a polynomial bound in its input size.

Equations

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

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

The uniform multiplication program runs in time polynomial in k on k-bit operands, including construction of the modulus.

theorem MIPRE.SAT.shoupMulProg_correct (k : ℕ) (hk : 1 ≤ k) (a b : Cost.BitStr) (ha : List.length a = k) (hb : List.length b = k) : (shoupFieldModel k hk).ofBits (shoupMulProg.toFun (Cost.unary k, a, b)) = (shoupFieldModel k hk).ofBits a * (shoupFieldModel k hk).ofBits b

Correctness of the uniform field multiplication program on k-bit operands.