The stages of local list decoding as De Morgan circuits

Reconstructing a worst-case hard function from a predictor for its encoding [STV01] runs three decoders in sequence, each of which queries the previous one at computed points: Goldreich–Levin decoding of the inner Hadamard code (Cslib.Circuits.Boolean.glPredictor), local list decoding of the outer Reed–Muller code along lines with advice (Cslib.Code.lineListDecode), and self-correction by interpolation and majority trees (Cslib.Code.lagrangeDecode, Cslib.majTree). This module bounds the De Morgan circuit size of each stage given the circuit size of the previous one.

A field element is represented by w bits through an encoding enc : F ≃ BitString w, and a function G : (Fin m → F) → F is bit-synthesizable with cost gates (Cslib.Circuits.Boolean.BitSynthesis) if, whenever the bits of the coordinates of a point are available, the bits of the value of G at that point can be made available with cost further gates. The arithmetic between queries runs over the full binary basis of the field and is bit-blasted (Cslib.Circuits.Synthesis.bitBlast_synthesis), at bitBlastCost w gates per field operation.

• The Goldreich–Levin stage costs glCost w K s for a predictor of size s and K masks (Cslib.Circuits.Boolean.bitSynthesis_glPredictor).
• The line stage costs lineCost for a field of size q, in terms of the cost of its oracle (Cslib.Circuits.Boolean.BitSynthesis.lineListDecode).
• The self-correction stage costs selfCorrectCost in terms of the cost of its oracle (Cslib.Circuits.Boolean.BitSynthesis.selfCorrect).

Main definitions

• Cslib.Circuits.Boolean.BitSynthesis: bit-synthesizable functions.
• Cslib.Circuits.Boolean.glPredictor, Cslib.Circuits.Boolean.glCost: the Goldreich–Levin decoder of the inner code and its gate budget.

Main results

• Cslib.Circuits.Boolean.bitSynthesis_glPredictor, Cslib.Circuits.Boolean.BitSynthesis.lineListDecode, Cslib.Circuits.Boolean.BitSynthesis.selfCorrect: the costs of the three stages.

References

• [M. Sudan, L. Trevisan, S. Vadhan, Pseudorandom generators without the XOR lemma] [STV01]
• O. Goldreich, L. Levin, A Hard-Core Predicate for All One-Way Functions

Bit-synthesizable functions

def Cslib.Circuits.Boolean.BitSynthesis {F : Type u_1} {w m : ℕ} (enc : F ≃ BitString w) (G : (Fin m → F) → F) (cost : ℕ) : Prop

G is bit-synthesizable with cost gates: whenever the bits of the coordinates of a point are available, the bits of the value of G at the point can be made available with cost further De Morgan gates.

theorem Cslib.Circuits.Boolean.BitSynthesis.mono {F : Type u_1} {w m : ℕ} {enc : F ≃ BitString w} {G : (Fin m → F) → F} {a b : ℕ} (h : BitSynthesis enc G a) (hab : a ≤ b) : BitSynthesis enc G b

A bit synthesis with a gates is one with any larger budget.

The Goldreich–Levin stage

def Cslib.Circuits.Boolean.glPredictor {F : Type u_1} {w m : ℕ} (enc : F ≃ BitString w) (C : BooleanFunction (m * w + w)) {K : ℕ} (masks : Fin K → BitString w) (guess : BitString K) : (Fin m → F) → F

The Goldreich–Levin decoder of the inner code. At a point x, the corrected-majority candidate of the predictor r ↦ C (bits of x, r) with fixed masks and guess, read as a field element.

def Cslib.Circuits.Boolean.glCost (w K s : ℕ) : ℕ

The gate budget of the Goldreich–Levin stage: two constants, and for each output bit, 2 ^ K - 1 copies of the predictor, each with at most one negation, and a strict majority.

theorem Cslib.Circuits.Boolean.bitSynthesis_glPredictor {F : Type u_1} {w m : ℕ} (enc : F ≃ BitString w) {C : BooleanFunction (m * w + w)} {sC : ℕ} (hC : complexity interpretation (single C) ≤ sC) {K : ℕ} (masks : Fin K → BitString w) (guess : BitString K) : BitSynthesis enc (glPredictor enc C masks guess) (glCost w K sC)

The Goldreich–Levin stage. If the predictor C has a De Morgan circuit with at most s gates, the Goldreich–Levin decoder with masks masks and guess guess is bit-synthesizable with glCost w K s gates.

The line stage

def Cslib.Circuits.Boolean.lineCost (w q m M ℓ d SG : ℕ) : ℕ

The gate budget of the line stage over a field with q elements, for points in m variables, M monomials, Y-degrees up to ℓ, degree d and an oracle of cost SG: the points of the line and the decoding with a hint are bit-blasted, and the oracle is queried at the q points of the line.

theorem Cslib.Circuits.Boolean.BitSynthesis.lineListDecode {F : Type u_1} {w m : ℕ} [Field F] [Fintype F] [DecidableEq F] {enc : F ≃ BitString w} {G : (Fin m → F) → F} {SG : ℕ} (hG : BitSynthesis enc G SG) (d D : ℕ) (z : Fin m → F) (a : F) : BitSynthesis enc (Code.lineListDecode G d D z a) (lineCost w (Fintype.card F) m (Code.Sudan.monomials d D).card (D / d) d SG)

The line stage. If G is bit-synthesizable with SG gates, then the local list decoder lineListDecode G d D z a is bit-synthesizable with lineCost gates.

The self-correction stage

def Cslib.Circuits.Boolean.selfCorrectCost (w m d L S1 : ℕ) : ℕ

The gate budget of the self-correction stage, for points in m variables, d + 1 nodes, a majority tree of depth L and an oracle of cost S1: the points of the lines and the interpolation and majorities are bit-blasted, and the oracle is queried at 3 ^ L * (d + 1) points.

theorem Cslib.Circuits.Boolean.BitSynthesis.selfCorrect {F : Type u_1} {w m : ℕ} [Field F] [DecidableEq F] {enc : F ≃ BitString w} {C1 : (Fin m → F) → F} {S1 : ℕ} (hC1 : BitSynthesis enc C1 S1) {d : ℕ} (ν : Fin (d + 1) ↪ F) {L : ℕ} (V : Fin (3 ^ L) → Fin m → F) : BitSynthesis enc (fun (x : Fin m → F) => majTree L fun (τ : Fin (3 ^ L)) => Code.lagrangeDecode ν C1 x (V τ)) (selfCorrectCost w m d L S1)

The self-correction stage. If C1 is bit-synthesizable with S1 gates, then the majority tree of depth L of the interpolations of C1 along the lines through x in the directions V τ is bit-synthesizable with selfCorrectCost gates.