Circuits for Reed–Solomon decoding with a hint

Sudan decoding with a hint (Cslib.Code.hintDecode) is an arithmetic computation on the received word, the hint and fixed constants: elimination for the interpolant of least Y-degree, then Newton iteration evaluated on all of F. Over the full binary basis of the field, where every operation on at most two field elements is one gate, it therefore has circuits of size polynomial in |F|, the number of points and the number of monomials. For n points, M monomials of (1, d)-weighted degree at most D, ℓ = D / d and q = |F|:

• the interpolant costs at most interpolantCost n M ℓ gates (Cslib.Circuits.Synthesis.full_interpolantCoeffs), dominated by ℓ + 1 eliminations of kernelVecCost n M gates each;
• Newton iteration to degree d costs at most henselCost q M d gates (Cslib.Circuits.Synthesis.full_henselValue);
• the whole decoder costs at most hintDecodeCost n q M ℓ d, their sum (Cslib.Circuits.Synthesis.full_hintDecode).

The word, the hint position and the hint value may be arbitrary available functions of the circuit's inputs.

Main definitions

• Cslib.Circuits.interpolantCost, Cslib.Circuits.henselStepCost, Cslib.Circuits.henselCost, Cslib.Circuits.hintDecodeCost: the gate budgets.

Main results

• Cslib.Circuits.Synthesis.full_interpolantCoeffs: the interpolant of least Y-degree.
• Cslib.Circuits.Synthesis.full_henselValue: Newton iteration.
• Cslib.Circuits.Synthesis.full_hintDecode: decoding with a hint.

References

• [M. Sudan, L. Trevisan, S. Vadhan, Pseudorandom generators without the XOR lemma] [STV01]
• M. Sudan, Decoding of Reed Solomon codes beyond the error-correction bound

def Cslib.Circuits.interpolantCost (n M ℓ : ℕ) : ℕ

The gate budget of the least-Y-degree interpolant for n points, M monomials and Y-degrees up to ℓ.

def Cslib.Circuits.henselStepCost (q M d : ℕ) : ℕ

The gate budget of one Newton step over a field with q elements, for M monomials and degree at most d.

def Cslib.Circuits.henselCost (q M d : ℕ) : ℕ

The gate budget of Newton iteration to degree d.

def Cslib.Circuits.hintDecodeCost (n q M ℓ d : ℕ) : ℕ

The gate budget of decoding with a hint.

Newton iteration

theorem Cslib.Circuits.Synthesis.full_henselValue {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {N : ℕ} {s : Set ((Fin N → F) → F)} (M : Finset (ℕ × ℕ)) (c : ℕ × ℕ → (Fin N → F) → F) (hc : ∀ m ∈ M, c m ∈ s) {τ a : (Fin N → F) → F} (hτ : τ ∈ s) (ha : a ∈ s) (d : ℕ) : Synthesis fullInterpretation s {fun (x : Fin N → F) => Code.henselValue (Code.Sudan.bivariateOf M fun (m : ℕ × ℕ) => c m x) (τ x) (a x) d} (henselCost (Fintype.card F) M.card d)

Newton iteration by a circuit. Given the coefficients on M of Q, the hint position and the hint value as available functions, henselValue Q τ a d costs at most henselCost q M d gates of the full binary basis.

The interpolant

theorem Cslib.Circuits.Synthesis.full_interpolantCoeffs {F : Type u_1} [Field F] [DecidableEq F] {N : ℕ} {s : Set ((Fin N → F) → F)} {ι : Type u_2} [Fintype ι] (α : ι → F) (w : ι → (Fin N → F) → F) (hw : ∀ (i : ι), w i ∈ s) (d D : ℕ) : Synthesis fullInterpretation s (Set.range fun (m : ↥(Code.Sudan.monomials d D)) (x : Fin N → F) => Code.Sudan.interpolantCoeffs α (fun (i : ι) => w i x) d D ↑m) (interpolantCost (Fintype.card ι) (Code.Sudan.monomials d D).card (D / d))

The least-Y-degree interpolant by a circuit. Given the received word as available functions, its interpolant coefficients on monomials d D cost at most interpolantCost n M (D / d) gates of the full binary basis, for n points and M monomials.

theorem Cslib.Circuits.Synthesis.full_hintDecode {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {N : ℕ} {s : Set ((Fin N → F) → F)} {ι : Type u_2} [Fintype ι] (α : ι → F) (w : ι → (Fin N → F) → F) (hw : ∀ (i : ι), w i ∈ s) {τ a : (Fin N → F) → F} (hτ : τ ∈ s) (ha : a ∈ s) (d D : ℕ) : Synthesis fullInterpretation s {fun (x : Fin N → F) => Code.hintDecode α (fun (i : ι) => w i x) d D (τ x) (a x)} (hintDecodeCost (Fintype.card ι) (Fintype.card F) (Code.Sudan.monomials d D).card (D / d) d)

Decoding with a hint by a circuit. Given the received word, the hint position and the hint value as available functions, hintDecode α w d D τ a costs at most hintDecodeCost n q M (D / d) d gates of the full binary basis, for n points, q = |F| and M monomials of (1, d)-weighted degree at most D.