The explicit affine disperser as a computable function

The explicit disperser on N bits works in the field 𝔽_{2 ^ n}, n = p₁ ⋯ pₖ, with the monomial basis ∏ᵢ αᵢ ^ Jᵢ in roots αᵢ of the least-code irreducible polynomials gᵢ of the prime degrees pᵢ. Its multiplication table depends only on the gᵢ: coordinate M of the product of the monomials J and K is the product over i of the coefficient of X ^ Mᵢ in the remainder of X ^ (Jᵢ + Kᵢ) modulo gᵢ (Cslib.prodPowBasis_mul_prodPowBasis). With the monomials numbered in the mixed radix (p₁, …, pₖ) (Cslib.AffineDisperser.mixedDigit), the table is computed from the remainders of the powers of X (Cslib.AffineDisperser.monomialTable, Cslib.AffineDisperser.isMulTable_monomialTable), and the polynomials gᵢ by exhaustive search with trial division among the codes below 2 ^ (4 L + 1).

The function Cslib.AffineDisperser.explicitDisperserProgram, a plain Lean function on bit lists (not a FreeM program), reads N from the length of its input, computes the parameters, the irreducible polynomials, the remainders and the multiplication table, and evaluates traceSym 1 r t in coordinates. It computes the explicit disperser (Cslib.AffineDisperser.explicitDisperserProgram_eq). Since the computation does not involve the roots, every choice of roots gives the same function (Cslib.AffineDisperser.traceSymBits_rootBasis_eq_explicitDisperser): the root chosen in Cslib.AffineDisperser.binaryRoot does not matter.

Main definitions

• Cslib.AffineDisperser.monomialTable: the multiplication table of a monomial basis.
• Cslib.AffineDisperser.explicitTable: the multiplication table of the explicit field.
• Cslib.AffineDisperser.rootBasis: the monomial basis in any roots of the irreducible polynomials.
• Cslib.AffineDisperser.explicitDisperserProgram: the explicit disperser, as a computable function on bit lists.

Main results

• Cslib.AffineDisperser.isMulTable_monomialTable: the monomial table is a multiplication table.
• Cslib.AffineDisperser.traceSymCoords_explicitTable: the coordinate computation with the explicit table is the explicit disperser.
• Cslib.AffineDisperser.traceSymBits_rootBasis_eq_explicitDisperser: independence of the roots.
• Cslib.AffineDisperser.explicitDisperserProgram_eq: the function computes the explicit disperser.

References

• E. Ben-Sasson, S. Kopparty, Affine dispersers from subspace polynomials

The multiplication table of a monomial basis

def Cslib.AffineDisperser.mixedDigit (ms : List ℕ) (u i : ℕ) : ℕ

Digit i of u in the mixed radix ms, least significant digit first.

def Cslib.AffineDisperser.monomialBit (ms : List ℕ) (R : List (List (List Bool))) (u w v : ℕ) : Bool

Coordinate v of the product of the monomials u and w (numbered in the mixed radix ms): the product over the factors i of the coefficient of X ^ vᵢ in the remainder of X ^ (uᵢ + wᵢ), read from the table R i of remainders of powers.

def Cslib.AffineDisperser.monomialTable (ms : List ℕ) (R : List (List (List Bool))) : List (List (List Bool))

The multiplication table of the monomial basis with mixed radix ms and tables of remainders of powers R.

theorem Cslib.AffineDisperser.isMulTable_monomialTable {F : Type u_1} [Field F] [Algebra (ZMod 2) F] [FiniteDimensional (ZMod 2) F] (ms : List ℕ) (R : List (List (List Bool))) {α : Fin ms.length → F} (hm : Pairwise (Function.onFun Nat.Coprime ms.get)) (hE : Module.finrank (ZMod 2) F = ∏ i : Fin ms.length, ms.get i) (hα : ∀ (i : Fin ms.length), (minpoly (ZMod 2) (α i)).natDegree = ms.get i) (hR : ∀ (i : Fin ms.length), ∀ e < 2 * ms.get i, α i ^ e = ∑ d ∈ Finset.range (ms.get i), BitString.bitEquiv.symm (((R.getD ↑i []).getD e []).getD d false) • α i ^ d) : IsMulTable ((prodPowBasis hm hE hα).reindex finPiFinEquiv) (monomialTable ms R)

The monomial table is a multiplication table: for roots αᵢ whose powers αᵢ ^ e, e < 2 mᵢ, have the coordinates R i e in the power basis, monomialTable ms R is the multiplication table of the monomial basis, numbered by finPiFinEquiv.

The explicit field

def Cslib.AffineDisperser.codeBound (N : ℕ) : ℕ

The codes searched for the irreducible polynomials on N bits: those below 2 ^ (4 L + 1), which contain the codes of all polynomials of degree at most 4 L.

def Cslib.AffineDisperser.explicitPowerTables (N : ℕ) : List (List (List Bool))

The tables of remainders of powers of X modulo the least-code irreducible polynomials of the prime degrees on N bits.

def Cslib.AffineDisperser.explicitTable (N : ℕ) : List (List (List Bool))

The multiplication table of the monomial basis of the explicit field on N bits.

theorem Cslib.AffineDisperser.coprime_degreePrime (N : ℕ) : Pairwise (Function.onFun Nat.Coprime (Explicit.degreePrime N))

theorem Cslib.AffineDisperser.natDegree_minpoly_of_aeval_eq_zero {N : ℕ} {j : Fin (Explicit.degreePrimes N).length} {a : ExplicitField N} (ha : (Polynomial.aeval a) (leastIrreducible (Explicit.degreePrime N j)) = 0) : (minpoly (ZMod 2) a).natDegree = Explicit.degreePrime N j

noncomputable def Cslib.AffineDisperser.rootBasis (N : ℕ) (α : Fin (Explicit.degreePrimes N).length → ExplicitField N) (hα : ∀ (j : Fin (Explicit.degreePrimes N).length), (Polynomial.aeval (α j)) (leastIrreducible (Explicit.degreePrime N j)) = 0) : Module.Basis (ExplicitMonomial N) (ZMod 2) (ExplicitField N)

The monomial basis of ExplicitField N in any roots α j of the least-code irreducible polynomials of the prime degrees.

theorem Cslib.AffineDisperser.aeval_binaryRoot_degreePrime (N : ℕ) (j : Fin (Explicit.degreePrimes N).length) : (Polynomial.aeval (binaryRoot (Explicit.degreePrime N j) (Explicit.fieldDegree N))) (leastIrreducible (Explicit.degreePrime N j)) = 0

The computable function

theorem Cslib.AffineDisperser.traceSymCoords_explicitTable (N : ℕ) (x : List Bool) : traceSymCoords (explicitTable N) (Explicit.numBlocks N) (Explicit.symDegree N) x = explicitDisperser N (BitString.ofList N x)

The coordinate computation with the explicit table is the explicit disperser on the first N bits of x (missing bits are zero).

theorem Cslib.AffineDisperser.traceSymBits_rootBasis_eq_explicitDisperser (N : ℕ) (α : Fin (Explicit.degreePrimes N).length → ExplicitField N) (hα : ∀ (j : Fin (Explicit.degreePrimes N).length), (Polynomial.aeval (α j)) (leastIrreducible (Explicit.degreePrime N j)) = 0) : traceSymBits 1 (Explicit.numBlocks N) (Explicit.symDegree N) (rootBasis N α hα) (explicitPos N) = explicitDisperser N

The choice of roots does not matter: the monomial basis in any roots of the least-code irreducible polynomials gives the explicit disperser. In particular the root chosen by binaryRoot is immaterial.

def Cslib.AffineDisperser.explicitDisperserProgram (x : List Bool) : Bool

The explicit disperser as a computable function on bit lists: the input length N fixes the parameters, and the function finds the irreducible polynomials, builds the multiplication table and evaluates traceSym 1 r t in coordinates.

theorem Cslib.AffineDisperser.explicitDisperserProgram_eq (x : List Bool) : explicitDisperserProgram x = explicitDisperser x.length (BitString.ofList x.length x)

The computable function is the explicit disperser.