Sudan's list decoder for Reed–Solomon codes

Let w : ι → F be a received word and let α be distinct evaluation points. Sudan's algorithm [Sud97], [GRS19] lists the polynomials P of degree less than k whose values agree with w at more than D points, for a parameter D. It interpolates: it finds a nonzero bivariate polynomial Q(X, Y) of (1, k - 1)-weighted degree at most D that vanishes at the n points (α i, w i) (Cslib.Code.Sudan.IsInterpolant, Cslib.Code.Sudan.interpolant). If P has degree less than k, then Q(X, P(X)) has degree at most D and vanishes at every point where P agrees with w; when there are more than D of them it is zero, so Y - P(X) divides Q(X, Y) (Cslib.Code.Sudan.IsInterpolant.X_sub_C_dvd): P is a root of Q viewed as a polynomial in Y over F[X]. The number of such roots is at most the Y-degree of Q, which is at most D / (k - 1) for k ≥ 2.

The decoder Cslib.Code.sudan returns the roots P of the elimination interpolant Cslib.Code.Sudan.interpolant α w (k - 1) D that have degree less than k and agree with w at more than D points. Because Cslib.Code.Sudan.interpolant searches Y-degrees up to D / (k - 1), completeness (Cslib.Code.mem_sudan_iff) requires positive weight k - 1 ≥ 1, that is k ≥ 2: with distinct points, k ≥ 2 and more than n monomials, its list consists of exactly those polynomials (Cslib.Code.mem_sudan_iff), while soundness (Cslib.Code.degree_lt_and_lt_card_of_mem_sudan) and the list-size bound L * (k - 1) ≤ D (Cslib.Code.card_sudan_mul_le) hold for all k. For k ≥ 2 and 2 * (k - 1) * n < (D + 1) * (D + 2), this list decodes the Reed–Solomon code of dimension k from agreement D + 1 ≈ √(2 * (k - 1) * n) (Cslib.Code.mem_sudan_iff_of_lt), and at most D / (k - 1) codewords have that agreement with any word (Cslib.Code.ncard_sep_reedSolomon_mul_le). Unique decoding needs agreement (n + k) / 2, so this goes beyond half the minimum distance when the rate k / n is small: asymptotically, below 3 - 2 * √2 ≈ 0.17.

This module proves the correctness of the decoder only: Cslib.Code.sudan computes the interpolant by elimination (Cslib.Code.Sudan.interpolant) and takes its roots in F[X][Y] noncomputably (Polynomial.roots), which in the literature are found in polynomial time by factoring bivariate polynomials; no running time is formalized here.

Main definitions

• Cslib.Code.sudan: Sudan's list decoder, built from the explicit elimination interpolant Cslib.Code.Sudan.interpolant.

Main results

• Cslib.Code.degree_lt_and_lt_card_of_mem_sudan: soundness of the listed polynomials.
• Cslib.Code.mem_sudan_iff, Cslib.Code.mem_sudan_iff_of_lt: the decoder lists exactly the polynomials with large agreement.
• Cslib.Code.card_sudan_mul_le: the decoder lists at most D / (k - 1) polynomials.
• Cslib.Code.exists_mem_sudan_of_mem_reedSolomon: list decoding of Reed–Solomon codes.
• Cslib.Code.ncard_sep_reedSolomon_mul_le: few Reed–Solomon codewords have large agreement with a word.

References

• M. Sudan, Decoding of Reed Solomon codes beyond the error-correction bound
• [V. Guruswami, A. Rudra, M. Sudan, Essential Coding Theory] [GRS19]

noncomputable def Cslib.Code.sudan {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] (α w : ι → F) (k D : ℕ) : Finset (Polynomial F)

Sudan's list decoder for dimension k and weighted degree D with evaluation points α: the roots P of the least-Y-degree Sudan interpolant Sudan.interpolant α w (k - 1) D for the received word w, as a polynomial in Y, that have degree less than k and agree with w at more than D points. Completeness (mem_sudan_iff) assumes k ≥ 2 so that the weight k - 1 is positive; the roots are taken noncomputably via Polynomial.roots.

theorem Cslib.Code.degree_lt_and_lt_card_of_mem_sudan {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] {α w : ι → F} {k D : ℕ} {P : Polynomial F} (h : P ∈ sudan α w k D) : P.degree < ↑k ∧ D < {i : ι | Polynomial.eval (α i) P = w i}.card

Every polynomial listed by Sudan's decoder has degree less than k and agrees with the received word at more than D points.

theorem Cslib.Code.card_sudan_mul_le {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] {α w : ι → F} {k D : ℕ} : (sudan α w k D).card * (k - 1) ≤ D

The size of the list. Sudan's decoder lists L polynomials with L * (k - 1) ≤ D: at most D / (k - 1) of them for k ≥ 2.

theorem Cslib.Code.mem_sudan_iff {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] {α w : ι → F} {k D : ℕ} {P : Polynomial F} (hα : Function.Injective α) (hk : 2 ≤ k) (hn : Fintype.card ι < (Sudan.monomials (k - 1) D).card) : P ∈ sudan α w k D ↔ P.degree < ↑k ∧ D < {i : ι | Polynomial.eval (α i) P = w i}.card

Sudan's list decoder lists the polynomials with large agreement. With distinct points, k ≥ 2 and more than n monomials of (1, k - 1)-weighted degree at most D, Sudan's decoder lists exactly the polynomials of degree less than k that agree with the received word at more than D points.

theorem Cslib.Code.mem_sudan_iff_of_lt {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] {α w : ι → F} {k D : ℕ} {P : Polynomial F} (hα : Function.Injective α) (hk : 2 ≤ k) (hn : 2 * (k - 1) * Fintype.card ι < (D + 1) * (D + 2)) : P ∈ sudan α w k D ↔ P.degree < ↑k ∧ D < {i : ι | Polynomial.eval (α i) P = w i}.card

Sudan's list decoding of Reed–Solomon codes [Sud97]. With distinct points, k ≥ 2 and 2 * (k - 1) * n < (D + 1) * (D + 2), Sudan's decoder lists exactly the polynomials of degree less than k that agree with the received word at more than D points; by card_sudan_mul_le there are at most D / (k - 1) of them.

theorem Cslib.Code.exists_mem_sudan_of_mem_reedSolomon {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] {α w : ι → F} {k D : ℕ} (hα : Function.Injective α) (hk : 2 ≤ k) (hn : 2 * (k - 1) * Fintype.card ι < (D + 1) * (D + 2)) {c : ι → F} (hc : c ∈ reedSolomon α k) (hagree : D < {i : ι | c i = w i}.card) : ∃ P ∈ sudan α w k D, (fun (i : ι) => Polynomial.eval (α i) P) = c

List decoding of Reed–Solomon codes. With distinct points, k ≥ 2 and 2 * (k - 1) * n < (D + 1) * (D + 2), every codeword of the Reed–Solomon code of dimension k that agrees with the received word at more than D points is the list of values of a polynomial listed by Sudan's decoder.

theorem Cslib.Code.ncard_sep_reedSolomon_mul_le {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] {α : ι → F} {k D : ℕ} (hα : Function.Injective α) (hk : 2 ≤ k) (hn : 2 * (k - 1) * Fintype.card ι < (D + 1) * (D + 2)) (w : ι → F) : {c : ι → F | c ∈ ↑(reedSolomon α k) ∧ D < {i : ι | c i = w i}.card}.ncard * (k - 1) ≤ D

List size for Reed–Solomon codes. With distinct points, k ≥ 2 and 2 * (k - 1) * n < (D + 1) * (D + 2), the number L of codewords of the Reed–Solomon code of dimension k that agree with a word at more than D points satisfies L * (k - 1) ≤ D.