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 is with a + (k - 1) * b ≤ D for each of its monomials X ^ a * Y ^ b, that vanishes at the n points (α i, w i) (Cslib.Code.Sudan.IsInterpolant). Such a Q is a nonzero solution of n linear equations in its coefficients, so it exists as soon as there are more than n monomials of weighted degree at most D (Cslib.Code.Sudan.exists_isInterpolant); for k ≥ 2 there are at least (D + 1) * (D + 2) / (2 * (k - 1)) of them (Cslib.Code.Sudan.add_one_mul_add_two_le_two_mul_mul_card_monomials). 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 an interpolant Q that have degree less than k and agree with w at more than D points. With distinct points and more than n monomials, its list consists of exactly those polynomials (Cslib.Code.mem_sudan_iff), and its length L always satisfies L * (k - 1) ≤ D (Cslib.Code.card_sudan_mul_le). 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 chooses an interpolant noncomputably and takes its roots, which in the literature are found by solving a linear system and factoring bivariate polynomials in polynomial time; no running time is formalized.

Main definitions

• Cslib.Code.Sudan.monomials: the monomials of bounded weighted degree.
• Cslib.Code.Sudan.bivariateOf: the bivariate polynomial with given coefficients on a set of monomials.
• Cslib.Code.Sudan.IsInterpolant: the bivariate interpolants of a received word.
• Cslib.Code.sudan: Sudan's list decoder.

Main results

• Cslib.Code.Sudan.exists_isInterpolant: interpolants exist when there are more than n monomials.
• Cslib.Code.Sudan.add_one_mul_add_two_le_two_mul_mul_card_monomials: counting the monomials.
• Cslib.Code.Sudan.IsInterpolant.eval_eq_zero, Cslib.Code.Sudan.IsInterpolant.X_sub_C_dvd: root containment, the polynomials with large agreement are roots of every interpolant.
• Cslib.Code.Sudan.IsInterpolant.natDegree_mul_sub_one_le: the Y-degree of an interpolant.
• 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]

def Cslib.Code.Sudan.monomials (w D : ℕ) : Finset (ℕ × ℕ)

The exponents (a, b) with a, b ≤ D of the monomials X ^ a * Y ^ b of (1, w)-weighted degree a + w * b at most D. For w ≥ 1 the bound b ≤ D holds for all of them.

theorem Cslib.Code.Sudan.mem_monomials {w D : ℕ} {ab : ℕ × ℕ} : ab ∈ monomials w D ↔ ab.1 ≤ D ∧ ab.2 ≤ D ∧ ab.1 + w * ab.2 ≤ D

(a, b) is in monomials w D exactly when a ≤ D, b ≤ D and a + w * b ≤ D.

theorem Cslib.Code.Sudan.add_one_mul_add_two_le_two_mul_mul_card_monomials {w : ℕ} (hw : 1 ≤ w) (D : ℕ) : (D + 1) * (D + 2) ≤ 2 * w * (monomials w D).card

Counting monomials. For w ≥ 1 there are at least (D + 1) * (D + 2) / (2 * w) monomials of (1, w)-weighted degree at most D: for each j ≤ D there are j / w + 1 ≥ (j + 1) / w of weighted degree exactly j.

structure Cslib.Code.Sudan.IsInterpolant {F : Type u_1} {ι : Type u_2} [Field F] (α w : ι → F) (k D : ℕ) (Q : Polynomial (Polynomial F)) : Prop

Q is a Sudan interpolant for the received word w with evaluation points α, dimension k and weighted degree D: a nonzero bivariate polynomial of (1, k - 1)-weighted degree at most D that vanishes at the points (α i, w i).

• ne_zero : Q ≠ 0

  The interpolant is nonzero.

• weightedDegree_le (a b : ℕ) : (Q.coeff b).coeff a ≠ 0 → a + (k - 1) * b ≤ D

  Every monomial X ^ a * Y ^ b of Q has (1, k - 1)-weighted degree a + (k - 1) * b at most D.

• evalEval_eq_zero (i : ι) : Polynomial.evalEval (α i) (w i) Q = 0

  The interpolant vanishes at the points (α i, w i).

noncomputable def Cslib.Code.Sudan.bivariateOf {F : Type u_1} [Field F] (M : Finset (ℕ × ℕ)) (c : ℕ × ℕ → F) : Polynomial (Polynomial F)

The bivariate polynomial with coefficient c m at X ^ m.1 * Y ^ m.2 for m ∈ M.

@[simp]

theorem Cslib.Code.Sudan.coeff_coeff_bivariateOf {F : Type u_1} [Field F] (M : Finset (ℕ × ℕ)) (c : ℕ × ℕ → F) (a b : ℕ) : ((bivariateOf M c).coeff b).coeff a = if (a, b) ∈ M then c (a, b) else 0

The coefficient of X ^ a * Y ^ b in bivariateOf M c is c (a, b) when (a, b) ∈ M, and zero otherwise.

theorem Cslib.Code.Sudan.evalEval_bivariateOf {F : Type u_1} [Field F] (M : Finset (ℕ × ℕ)) (c : ℕ × ℕ → F) (x y : F) : Polynomial.evalEval x y (bivariateOf M c) = ∑ m ∈ M, c m * x ^ m.1 * y ^ m.2

The value of bivariateOf M c at (x, y) is ∑ m ∈ M, c m * x ^ m.1 * y ^ m.2.

theorem Polynomial.eval_eval_eq_evalEval {R : Type u_3} [CommSemiring R] (Q : Polynomial (Polynomial R)) (P : Polynomial R) (x : R) : eval x (eval P Q) = evalEval x (eval x P) Q

Evaluating Q(X, P(X)) at x evaluates Q at (x, P(x)).

theorem Cslib.Code.Sudan.natDegree_eval_le_of_weighted {F : Type u_1} [Field F] {d E : ℕ} {S : Polynomial (Polynomial F)} {P : Polynomial F} (hP : P.natDegree ≤ d) (hS : ∀ (a b : ℕ), (S.coeff b).coeff a ≠ 0 → a + d * b ≤ E) : (Polynomial.eval P S).natDegree ≤ E

Substituting Y = P(X), with P of degree at most d, into a bivariate polynomial whose monomials have (1, d)-weighted degree at most E gives a polynomial of degree at most E.

theorem Cslib.Code.Sudan.IsInterpolant.natDegree_mul_sub_one_le {F : Type u_1} {ι : Type u_2} [Field F] {α w : ι → F} {k D : ℕ} {Q : Polynomial (Polynomial F)} (hQ : IsInterpolant α w k D Q) : Q.natDegree * (k - 1) ≤ D

The Y-degree of a Sudan interpolant: deg_Y Q * (k - 1) ≤ D.

theorem Cslib.Code.Sudan.exists_isInterpolant {F : Type u_1} {ι : Type u_2} [Field F] {k D : ℕ} [Fintype ι] (α w : ι → F) (hn : Fintype.card ι < (monomials (k - 1) D).card) : ∃ (Q : Polynomial (Polynomial F)), IsInterpolant α w k D Q

Interpolation. If there are more than n monomials of (1, k - 1)-weighted degree at most D, every received word has a Sudan interpolant: the n conditions Q (α i, w i) = 0 are linear in the coefficients of Q.

theorem Cslib.Code.Sudan.IsInterpolant.eval_eq_zero {F : Type u_1} {ι : Type u_2} [Field F] {α w : ι → F} {k D : ℕ} {Q : Polynomial (Polynomial F)} [Fintype ι] [DecidableEq F] (hα : Function.Injective α) (hQ : IsInterpolant α w k D Q) {P : Polynomial F} (hP : P.degree < ↑k) (hagree : D < {i : ι | Polynomial.eval (α i) P = w i}.card) : Polynomial.eval P Q = 0

Root containment. With distinct points, if P has degree less than k and agrees with the received word at more than D points, then Q(X, P(X)) = 0 for every Sudan interpolant Q.

theorem Cslib.Code.Sudan.IsInterpolant.X_sub_C_dvd {F : Type u_1} {ι : Type u_2} [Field F] {α w : ι → F} {k D : ℕ} {Q : Polynomial (Polynomial F)} [Fintype ι] [DecidableEq F] (hα : Function.Injective α) (hQ : IsInterpolant α w k D Q) {P : Polynomial F} (hP : P.degree < ↑k) (hagree : D < {i : ι | Polynomial.eval (α i) P = w i}.card) : Polynomial.X - Polynomial.C P ∣ Q

Root containment. With distinct points, if P has degree less than k and agrees with the received word at more than D points, then Y - P(X) divides every Sudan interpolant Q(X, Y).

theorem Cslib.Code.Sudan.IsInterpolant.mem_roots {F : Type u_1} {ι : Type u_2} [Field F] {α w : ι → F} {k D : ℕ} {Q : Polynomial (Polynomial F)} [Fintype ι] [DecidableEq F] (hα : Function.Injective α) (hQ : IsInterpolant α w k D Q) {P : Polynomial F} (hP : P.degree < ↑k) (hagree : D < {i : ι | Polynomial.eval (α i) P = w i}.card) : P ∈ Q.roots

With distinct points, a polynomial of degree less than k that agrees with the received word at more than D points is a root of every Sudan interpolant, as a polynomial in Y.

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 a Sudan interpolant Q 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; the empty list when there is no interpolant. The interpolant is chosen noncomputably; this definition makes no claim about how it or its roots are found.

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 α) (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, if there are 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.