4.2. Reed-Solomon Erasure Code🔗

Definition4.2.1

groupuses 1

Used by 2

Reverse dependency previews

Preview

Theorem 4.2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

\todo

Reed–Solomon parameters

structure Parameters (F : Type) [Field F] where
  /-- Number of codeword positions. -/
  N : ℕ
  /-- The codeword has at least one position. -/
  N_pos : 0 < N
  /-- Number of message symbols and reconstruction threshold. -/
  k : ℕ
  /-- At least one message symbol is required for reconstruction. -/
  k_pos : 0 < k
  /-- The message fits in the codeword. -/
  k_le_N : k ≤ N
  /-- Evaluation point `xⱼ` of each position `j`. -/
  point : Fin N → F
  /-- The evaluation points are pairwise distinct. -/
  point_injective : Function.Injective point

source positions and evaluation points

/-- The inclusion `{0, …, k-1} ↪ {0, …, N-1}`, `i ↦ i`: a message index as a
codeword position. -/
def sourceIndex (params : Parameters F) (i : Fin params.k) : Fin params.N :=
  Fin.castLE params.k_le_N i

/-- The evaluation-point mapping `point : j ↦ xⱼ` restricted to the message
positions `{0, …, k-1}`: `i ↦ xᵢ`. -/
def sourcePoint (params : Parameters F) (i : Fin params.k) : F :=
  params.point (params.sourceIndex i)

/-- The points `x₀, …, x_(k-1)` are pairwise distinct: the restriction of an
injective mapping is itself injective. -/
theorem sourcePoint_injective (params : Parameters F) :
    Function.Injective params.sourcePoint :=
  params.point_injective.comp (Fin.castLE_injective params.k_le_N)

encoding polynomial

def encodingPolynomial (params : Parameters F) (message : Fin params.k → F) : F[X] :=
  Lagrange.interpolate Finset.univ params.sourcePoint message

encode

def encode (params : Parameters F) (message : Fin params.k → F) (i : Fin params.N) : F :=
  (params.encodingPolynomial message).eval (params.point i)

decoding polynomial

noncomputable def decodingPolynomial (params : Parameters F)
    (chunks : Finset (Fin params.N × F)) : F[X] :=
  letI : DecidableEq F := Classical.decEq F
  Lagrange.interpolate chunks (fun (j, _) => params.point j) (fun (_, y) => y)

decode

noncomputable def decode (params : Parameters F)
    (chunks : Finset (Fin params.N × F)) : Option (Fin params.k → F) :=
  letI : Decidable (ErasureCode.Decodable params.k chunks) := Classical.propDecidable _
  if _h : ErasureCode.Decodable params.k chunks then
    some fun i => (params.decodingPolynomial chunks).eval (params.sourcePoint i)
  else
    none

ErasureCode instance

def erasureCode (params : Parameters F) : ErasureCode F where
  N := params.N
  N_pos := params.N_pos
  nchunk := params.k
  nchunk_pos := params.k_pos
  nchunk_le_N := params.k_le_N
  encode := params.encode
  decode := params.decode

uses Definition 4.1.1 · github #198

Lean code for Definition4.2.1●8 definitions

structure(7 fields)defined in SecureMessaging/ErasureCode/ReedSolomon/Construction.lean

complete

structure ErasureCode.ReedSolomon.Parameters (F : Type) [Field F] : Type

structure ErasureCode.ReedSolomon.Parameters
  (F : Type) [Field F] : Type

Valid parameters for a Reed–Solomon code over `F`: positions `0, …, N-1`,
message size `k ≤ N`, and pairwise distinct evaluation points `xⱼ = point j`.

Fields

N : ℕ

Number of codeword positions.

N_pos : 0 < self.N

The codeword has at least one position.

k : ℕ

Number of message symbols and reconstruction threshold.

k_pos : 0 < self.k

At least one message symbol is required for reconstruction.

k_le_N : self.k ≤ self.N

The message fits in the codeword.

point : Fin self.N → F

Evaluation point `xⱼ` of each position `j`.

point_injective : Function.Injective self.point

The evaluation points are pairwise distinct.

defdefined in SecureMessaging/ErasureCode/ReedSolomon/Construction.lean

complete

def ErasureCode.ReedSolomon.Parameters.sourceIndex {F : Type} [Field F]
  (params : ErasureCode.ReedSolomon.Parameters F) (i : Fin params.k) :
  Fin params.N

def ErasureCode.ReedSolomon.Parameters.sourceIndex
  {F : Type} [Field F]
  (params :
    ErasureCode.ReedSolomon.Parameters F)
  (i : Fin params.k) : Fin params.N

The inclusion `{0, …, k-1} ↪ {0, …, N-1}`, `i ↦ i`: a message index as a
codeword position.

defdefined in SecureMessaging/ErasureCode/ReedSolomon/Construction.lean

complete

def ErasureCode.ReedSolomon.Parameters.sourcePoint {F : Type} [Field F]
  (params : ErasureCode.ReedSolomon.Parameters F) (i : Fin params.k) : F

def ErasureCode.ReedSolomon.Parameters.sourcePoint
  {F : Type} [Field F]
  (params :
    ErasureCode.ReedSolomon.Parameters F)
  (i : Fin params.k) : F

The evaluation-point mapping `point : j ↦ xⱼ` restricted to the message
positions `{0, …, k-1}`: `i ↦ xᵢ`.

defdefined in SecureMessaging/ErasureCode/ReedSolomon/Construction.lean

complete

def ErasureCode.ReedSolomon.Parameters.encodingPolynomial {F : Type}
  [Field F] (params : ErasureCode.ReedSolomon.Parameters F)
  (message : Fin params.k → F) : Polynomial F

def ErasureCode.ReedSolomon.Parameters.encodingPolynomial
  {F : Type} [Field F]
  (params :
    ErasureCode.ReedSolomon.Parameters F)
  (message : Fin params.k → F) :
  Polynomial F

The *encoding polynomial* `Pₘ` of a message `m`: the unique polynomial with
`deg Pₘ < k` and `Pₘ(xᵢ) = mᵢ` for `i < k`, by Lagrange interpolation at the points
`x₀, …, x_(k-1)`.

defdefined in SecureMessaging/ErasureCode/ReedSolomon/Construction.lean

complete

def ErasureCode.ReedSolomon.Parameters.encode {F : Type} [Field F]
  (params : ErasureCode.ReedSolomon.Parameters F)
  (message : Fin params.k → F) (i : Fin params.N) : F

def ErasureCode.ReedSolomon.Parameters.encode
  {F : Type} [Field F]
  (params :
    ErasureCode.ReedSolomon.Parameters F)
  (message : Fin params.k → F)
  (i : Fin params.N) : F

`Encode(m, j) = Pₘ(xⱼ)`: the codeword symbol of message `m` at position `j`.

defdefined in SecureMessaging/ErasureCode/ReedSolomon/Construction.lean

complete

def ErasureCode.ReedSolomon.Parameters.decodingPolynomial {F : Type}
  [Field F] (params : ErasureCode.ReedSolomon.Parameters F)
  (chunks : Finset (Fin params.N × F)) : Polynomial F

def ErasureCode.ReedSolomon.Parameters.decodingPolynomial
  {F : Type} [Field F]
  (params :
    ErasureCode.ReedSolomon.Parameters F)
  (chunks : Finset (Fin params.N × F)) :
  Polynomial F

The interpolant `Q` through the pairs `{(xⱼ, y) | (j, y) ∈ L}` of a received
chunk set `L`. For honest chunks `y = Pₘ(xⱼ)` at `n ≥ k` distinct positions,
`Q = Pₘ`.

defdefined in SecureMessaging/ErasureCode/ReedSolomon/Construction.lean

complete

def ErasureCode.ReedSolomon.Parameters.decode {F : Type} [Field F]
  (params : ErasureCode.ReedSolomon.Parameters F)
  (chunks : Finset (Fin params.N × F)) : Option (Fin params.k → F)

def ErasureCode.ReedSolomon.Parameters.decode
  {F : Type} [Field F]
  (params :
    ErasureCode.ReedSolomon.Parameters F)
  (chunks : Finset (Fin params.N × F)) :
  Option (Fin params.k → F)

`Decode(L) = (Q(x₀), …, Q(x_(k-1)))` when `L` is decodable, and `⊥` (`none`)
otherwise.

Conflicting chunks `(j, y₁), (j, y₂)` with `y₁ ≠ y₂` are rejected because they share
the position `j`. Chunks with distinct positions but corrupted values are
outside the erasure-only correctness claim.

defdefined in SecureMessaging/ErasureCode/ReedSolomon/Construction.lean

complete

def ErasureCode.ReedSolomon.Parameters.erasureCode {F : Type} [Field F]
  (params : ErasureCode.ReedSolomon.Parameters F) : ErasureCode F

def ErasureCode.ReedSolomon.Parameters.erasureCode
  {F : Type} [Field F]
  (params :
    ErasureCode.ReedSolomon.Parameters
      F) :
  ErasureCode F

The erasure code `(N, nchunk = k, Encode, Decode)` induced by a Reed–Solomon
code.

Theorem4.2.2

group

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

\todo

erasure-code correctness

theorem erasureCode_correct (params : Parameters F) : params.erasureCode.Correct

uses Definition 4.2.1 · Definition 4.1.4 · github #199

Lean code for Theorem4.2.2●1 theorem

theoremdefined in SecureMessaging/ErasureCode/ReedSolomon/Correctness.lean

complete

theorem ErasureCode.ReedSolomon.Parameters.erasureCode_correct {F : Type}
  [Field F] (params : ErasureCode.ReedSolomon.Parameters F) :
  params.erasureCode.Correct

theorem ErasureCode.ReedSolomon.Parameters.erasureCode_correct
  {F : Type} [Field F]
  (params :
    ErasureCode.ReedSolomon.Parameters
      F) :
  params.erasureCode.Correct

The Reed–Solomon erasure code is correct (`ErasureCode.Correct`, [SCKA] Def.
A.6): for every message `m` and position set `I`, `Decode(L_I) = m` if `k ≤ |I|`,
and `Decode(L_I) = ⊥` if `|I| < k`.

References: