4.3. SPQR Erasure Code🔗

Definition4.3.1

Group: The 16-coordinate parallel Reed–Solomon construction and its SPQR specialization. (3)

Group member previews

Preview

Definition 4.3.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.1

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Definition 4.3.2

Loading preview

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

✓L∃∀N

\todo

16-coordinate chunk

abbrev Chunk (F : Type) := Fin 16 → F

encode

def encode (params : ReedSolomon.Parameters F) (message : Fin params.k → Chunk F)
    (index : Fin params.N) : Chunk F :=
  fun coordinate => params.encode (fun i => message i coordinate) index

coordinate chunks

def coordinateChunks (params : ReedSolomon.Parameters F)
    (chunks : Finset (Fin params.N × Chunk F)) (coordinate : Fin 16) :
    Finset (Fin params.N × F) := byF:Typeinst✝:Field Fparams:ReedSolomon.Parameters Fchunks:Finset (Fin params.N × Chunk F)coordinate:Fin 16⊢ Finset (Fin params.N × F)
  classical
  exact chunks.image fun (j, y) => (j, y coordinate)All goals completed! 🐙

decode

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

ErasureCode instance

def parallelErasureCode (params : ReedSolomon.Parameters F) : ErasureCode (Chunk 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 := encode params
  decode := decode params

uses Definition 4.2.1 · Definition 4.1.1

Lean code for Definition4.3.1●5 definitions

abbrevdefined in SecureMessaging/ErasureCode/SPQRReedSolomon/Construction.lean

complete

abbrev ErasureCode.SPQRReedSolomon.Chunk (F : Type) : Type

abbrev ErasureCode.SPQRReedSolomon.Chunk
  (F : Type) : Type

A chunk of 16 field elements. For `F = GF(2^16)`, it represents 32 bytes after
choosing a two-byte representation of field elements.

defdefined in SecureMessaging/ErasureCode/SPQRReedSolomon/Construction.lean

complete

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

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

Encode a chunk message at position `j` by applying the Reed–Solomon encoder
independently to each of its 16 coordinates:
`Encode(m, j) = (P₀(xⱼ), …, P₁₅(xⱼ))`.

defdefined in SecureMessaging/ErasureCode/SPQRReedSolomon/Construction.lean

complete

def ErasureCode.SPQRReedSolomon.coordinateChunks {F : Type} [Field F]
  (params : ErasureCode.ReedSolomon.Parameters F)
  (chunks : Finset (Fin params.N × ErasureCode.SPQRReedSolomon.Chunk F))
  (coordinate : Fin 16) : Finset (Fin params.N × F)

def ErasureCode.SPQRReedSolomon.coordinateChunks
  {F : Type} [Field F]
  (params :
    ErasureCode.ReedSolomon.Parameters F)
  (chunks :
    Finset
      (Fin params.N ×
        ErasureCode.SPQRReedSolomon.Chunk
          F))
  (coordinate : Fin 16) :
  Finset (Fin params.N × F)

Project each received chunk `(j, y)` to its `c`-th coordinate `(j, y[c])`.

defdefined in SecureMessaging/ErasureCode/SPQRReedSolomon/Construction.lean

complete

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

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

Decode a received chunk set coordinatewise. For a decodable set, coordinate `c`
is reconstructed from `Q_c` at the `k` source points; otherwise decoding returns
`none`.

defdefined in SecureMessaging/ErasureCode/SPQRReedSolomon/Construction.lean

complete

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

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

Lift a Reed–Solomon code to an erasure code whose symbols are 16-coordinate
chunks. It retains block length `N` and threshold `k`.

Definition4.3.2

Group: The 16-coordinate parallel Reed–Solomon construction and its SPQR specialization. (3)

Group member previews

Preview

Definition 4.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

\todo

galois field

abbrev GF16 := GaloisField 2 16

evaluation points

def spqrEvaluationPoints : Fin (2 ^ 16) ≃ GF16 :=
  (Finite.equivFinOfCardEq gf16_card).symm

Reed–Solomon parameters

def spqrParameters (k : ℕ) (hk : k ≤ 2 ^ 16) (hk_pos : 0 < k) :
    ReedSolomon.Parameters GF16
    where
  N := 2 ^ 16
  N_pos := byF:Typeinst✝:Field Fk:ℕhk:k ≤ 2 ^ 16hk_pos:0 < k⊢ 0 < 2 ^ 16 norm_numAll goals completed! 🐙
  k := k
  k_pos := hk_pos
  k_le_N := hk
  point := spqrEvaluationPoints
  point_injective := spqrEvaluationPoints.injective

ErasureCode instance

def erasureCode (k : ℕ) (hk : k ≤ 2 ^ 16) (hk_pos : 0 < k) : ErasureCode (Chunk GF16) :=
  parallelErasureCode (spqrParameters k hk hk_pos)

uses Definition 4.3.1

Lean code for Definition4.3.2●4 definitions

abbrevdefined in SecureMessaging/ErasureCode/SPQRReedSolomon/Construction.lean

complete

abbrev ErasureCode.SPQRReedSolomon.GF16 : Type

abbrev ErasureCode.SPQRReedSolomon.GF16 : Type

An abstract finite field with `2^16` elements for the SPQR specialization.

defdefined in SecureMessaging/ErasureCode/SPQRReedSolomon/Construction.lean

complete

def ErasureCode.SPQRReedSolomon.spqrEvaluationPoints :
  Fin (2 ^ 16) ≃ ErasureCode.SPQRReedSolomon.GF16

def ErasureCode.SPQRReedSolomon.spqrEvaluationPoints :
  Fin (2 ^ 16) ≃
    ErasureCode.SPQRReedSolomon.GF16

The chosen bijection `x : {0, …, 2^16-1} ≃ GF16`, whose values `xⱼ` are the
Reed–Solomon evaluation points.

defdefined in SecureMessaging/ErasureCode/SPQRReedSolomon/Construction.lean

complete

def ErasureCode.SPQRReedSolomon.spqrParameters (k : ℕ) (hk : k ≤ 2 ^ 16)
  (hk_pos : 0 < k) :
  ErasureCode.ReedSolomon.Parameters ErasureCode.SPQRReedSolomon.GF16

def ErasureCode.SPQRReedSolomon.spqrParameters
  (k : ℕ) (hk : k ≤ 2 ^ 16)
  (hk_pos : 0 < k) :
  ErasureCode.ReedSolomon.Parameters
    ErasureCode.SPQRReedSolomon.GF16

The single-coordinate Reed–Solomon parameters shared by all 16 coordinates:
threshold `k`, block length `2^16`, and evaluation points given by
`spqrEvaluationPoints`.

defdefined in SecureMessaging/ErasureCode/SPQRReedSolomon/Construction.lean

complete

def ErasureCode.SPQRReedSolomon.erasureCode (k : ℕ) (hk : k ≤ 2 ^ 16)
  (hk_pos : 0 < k) :
  ErasureCode
    (ErasureCode.SPQRReedSolomon.Chunk ErasureCode.SPQRReedSolomon.GF16)

def ErasureCode.SPQRReedSolomon.erasureCode
  (k : ℕ) (hk : k ≤ 2 ^ 16)
  (hk_pos : 0 < k) :
  ErasureCode
    (ErasureCode.SPQRReedSolomon.Chunk
      ErasureCode.SPQRReedSolomon.GF16)

The abstract SPQR erasure code at threshold `k`: the 16-coordinate parallel code
specialized to `GF16`, with one chunk at each codeword position.

Theorem4.3.3

Group: The 16-coordinate parallel Reed–Solomon construction and its SPQR specialization. (3)

Group member previews

Preview

Definition 4.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

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

parallel correctness

theorem parallelErasureCode_correct (params : ReedSolomon.Parameters F) :
    (parallelErasureCode params).Correct

uses Definition 4.3.1 · Theorem 4.2.2 · Definition 4.1.4

Lean code for Theorem4.3.3●1 theorem

theoremdefined in SecureMessaging/ErasureCode/SPQRReedSolomon/Correctness.lean

complete

theorem ErasureCode.SPQRReedSolomon.parallelErasureCode_correct {F : Type}
  [Field F] (params : ErasureCode.ReedSolomon.Parameters F) :
  (ErasureCode.SPQRReedSolomon.parallelErasureCode params).Correct

theorem ErasureCode.SPQRReedSolomon.parallelErasureCode_correct
  {F : Type} [Field F]
  (params :
    ErasureCode.ReedSolomon.Parameters
      F) :
  (ErasureCode.SPQRReedSolomon.parallelErasureCode
      params).Correct

Correctness of the parallel construction: for every message and position
set `I`, decoding honest chunks returns the message when `k ≤ |I|` and returns `none`
when `|I| < k`.

Theorem4.3.4

Group: The 16-coordinate parallel Reed–Solomon construction and its SPQR specialization. (3)

Group member previews

Preview

Definition 4.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 4.3.2

Loading preview

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

used by 0✓L∃∀N

\todo

SPQR correctness

theorem erasureCode_correct (k : ℕ) (hk : k ≤ 2 ^ 16) (hk_pos : 0 < k) :
    (erasureCode k hk hk_pos).Correct

uses Definition 4.3.2 · Theorem 4.3.3

Lean code for Theorem4.3.4●1 theorem

theoremdefined in SecureMessaging/ErasureCode/SPQRReedSolomon/Correctness.lean

complete

theorem ErasureCode.SPQRReedSolomon.erasureCode_correct (k : ℕ)
  (hk : k ≤ 2 ^ 16) (hk_pos : 0 < k) :
  (ErasureCode.SPQRReedSolomon.erasureCode k hk hk_pos).Correct

theorem ErasureCode.SPQRReedSolomon.erasureCode_correct
  (k : ℕ) (hk : k ≤ 2 ^ 16)
  (hk_pos : 0 < k) :
  (ErasureCode.SPQRReedSolomon.erasureCode
      k hk hk_pos).Correct

Correctness of the abstract SPQR specialization for every threshold
`0 < k ≤ 2^16`.

References:

Signal (2025)
Signal (2025)