4.1. Erasure-Code Definitions🔗

Definition4.1.1

Group: Erasure Codes. (3)

Group member previews

Preview

Definition 4.1.2

Loading preview

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

uses 0

Used by 13

Reverse dependency previews

Preview

Definition 4.1.2

Loading preview

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

✓L∃∀N

\todo

scheme

structure ErasureCode (Sym : Type) where
  /-- Number of valid encoded-chunk positions; valid indices are `0, …, N - 1`. -/
  N : ℕ
  /-- At least one encoded-chunk position is available. -/
  N_pos : 0 < N
  /-- Number of source symbols and distinct encoded chunks needed for recovery. -/
  nchunk : ℕ
  /-- At least one distinct encoded chunk is required for recovery. -/
  nchunk_pos : 0 < nchunk
  /-- The message fits within the codeword. -/
  nchunk_le_N : nchunk ≤ N
  /-- `Encode(M, i)`: the chunk encoding of message `M` at index `i`. -/
  encode : (Fin nchunk → Sym) → Fin N → Sym
  /-- `Decode(L)`: recover the message from a chunk set, or fail (`none`). -/
  decode : Finset (Fin N × Sym) → Option (Fin nchunk → Sym)

decodability predicate

def Decodable {N : ℕ} (nchunk : ℕ) (chunks : Finset (Fin N × Sym)) : Prop :=
  nchunk ≤ chunks.card ∧ Set.InjOn Prod.fst (chunks : Set (Fin N × Sym))

github #190

Lean code for Definition4.1.1●2 definitions

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

complete

structure ErasureCode (Sym : Type) : Type

structure ErasureCode (Sym : Type) : Type

An erasure code over an alphabet `Sym` (Definition A.6 of [SCKA]).

- `Sym`: the alphabet Σ of symbols;
- `N`: the number of valid encoded-chunk positions; valid indices are
  `0, …, N - 1`;
- `nchunk`: the number of source symbols and the number of distinct encoded
  chunks required to recover the message;
- `nchunk > 0`: at least one distinct encoded chunk is required for recovery;
- `encode M i`: the chunk encoding of message `M` at index `i`;
- `decode L`: recovers a message from a chunk set `L`, or fails (`none`).

Fields

N : ℕ

Number of valid encoded-chunk positions; valid indices are `0, …, N - 1`.

N_pos : 0 < self.N

At least one encoded-chunk position is available.

nchunk : ℕ

Number of source symbols and distinct encoded chunks needed for recovery.

nchunk_pos : 0 < self.nchunk

At least one distinct encoded chunk is required for recovery.

nchunk_le_N : self.nchunk ≤ self.N

The message fits within the codeword.

encode : (Fin self.nchunk → Sym) → Fin self.N → Sym

`Encode(M, i)`: the chunk encoding of message `M` at index `i`.

decode : Finset (Fin self.N × Sym) → Option (Fin self.nchunk → Sym)

`Decode(L)`: recover the message from a chunk set, or fail (`none`).

defdefined in SecureMessaging/ErasureCode/Defs.lean

complete

def ErasureCode.Decodable {Sym : Type} {N : ℕ} (nchunk : ℕ)
  (chunks : Finset (Fin N × Sym)) : Prop

def ErasureCode.Decodable {Sym : Type} {N : ℕ}
  (nchunk : ℕ)
  (chunks : Finset (Fin N × Sym)) : Prop

A received chunk set is *decodable* for threshold `nchunk` when it contains
at least `nchunk` chunks at pairwise distinct positions.

Definition4.1.2

Group: Erasure Codes. (3)

Group member previews

Preview

Definition 4.1.1

Loading preview

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

uses 1

Used by 2

Reverse dependency previews

Preview

Definition 4.1.3

Loading preview

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

✓L∃∀N

\todo

payload serialization and parsing

structure ErasureCodePayload (M Sym : Type) where
  /-- The erasure code used for this payload type. -/
  ec : ErasureCode Sym
  /-- Serialize a payload as the `nchunk`-symbol message consumed by `ec.encode`. -/
  serialize : M → Fin ec.nchunk → Sym
  /-- Parse a decoded `nchunk`-symbol message as a payload, or fail. -/
  parse : (Fin ec.nchunk → Sym) → Option M
  /-- Parsing a serialized payload recovers the original payload. -/
  parse_serialize : ∀ payload, parse (serialize payload) = some payload

uses Definition 4.1.1 · github #251

Lean code for Definition4.1.2●1 definition

structure(4 fields)defined in SecureMessaging/ErasureCode/Defs.lean

complete

structure ErasureCodePayload (M Sym : Type) : Type

structure ErasureCodePayload (M Sym : Type) : Type

An erasure code over `Sym` equipped with serialization for payloads of type `M`.

Fields

ec : ErasureCode Sym

The erasure code used for this payload type.

serialize : M → Fin self.ec.nchunk → Sym

Serialize a payload as the `nchunk`-symbol message consumed by `ec.encode`.

parse : (Fin self.ec.nchunk → Sym) → Option M

Parse a decoded `nchunk`-symbol message as a payload, or fail.

parse_serialize : ∀ (payload : M), self.parse (self.serialize payload) = some payload

Parsing a serialized payload recovers the original payload.

Definition4.1.3

Group: Erasure Codes. (3)

Group member previews

Preview

Definition 4.1.1

Loading preview

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

uses 1used by 1✓L∃∀N

\todo

configured endpoint states

/-- Encoder state for one erasure-coded payload stream. It stores the erasure-code
payload scheme, the payload being encoded, and the counter for the next chunk. -/
structure EncoderState (M Sym : Type) where
  /-- The erasure-code payload scheme used to encode this stream. -/
  ecp : ErasureCodePayload M Sym
  /-- The fixed payload encoded by this stream. -/
  payload : M
  /-- The natural-number counter used for the next emitted chunk. -/
  nextIndex : ℕ

/-- Decoder state for one erasure-coded payload stream. It stores the erasure-code
payload scheme and the indexed chunks received so far. -/
structure DecoderState (M Sym : Type) where
  /-- The erasure-code payload scheme used to decode this stream. -/
  ecp : ErasureCodePayload M Sym
  /-- Indexed chunks retained by the decoder, with at most one symbol per index for
  states reachable from `empty` through `addChunk`. -/
  chunks : Finset (ℕ × Sym)

encoder operations

/-- Initialize an encoder before emitting its first chunk. -/
def init (ecp : ErasureCodePayload M Sym) (payload : M) : EncoderState M Sym :=
  { ecp, payload, nextIndex := 0 }

/-- Emit the chunk at the current counter and advance the counter by one. -/
def nextChunk (state : EncoderState M Sym) :
    (ℕ × Sym) × EncoderState M Sym :=
  (state.ecp.encode state.payload state.nextIndex,
    { state with nextIndex := state.nextIndex + 1 })

decoder operations

/-- The decoder already contains a chunk at `index`. -/
def HasIndex (state : DecoderState M Sym) (index : ℕ) : Prop :=
  ∃ chunk ∈ state.chunks, chunk.1 = index

/-- Whether the decoder contains a chunk at a given index is decidable. -/
instance (state : DecoderState M Sym) (index : ℕ) :
    Decidable (state.HasIndex index) := byM:TypeSym:Typestate:DecoderState M Symindex:ℕ⊢ Decidable (state.HasIndex index)
  unfold HasIndexM:TypeSym:Typestate:DecoderState M Symindex:ℕ⊢ Decidable (∃ chunk ∈ state.chunks, chunk.1 = index)
  infer_instanceAll goals completed! 🐙

/-- Stored chunks have pairwise distinct indices. -/
def IndexUnique (state : DecoderState M Sym) : Prop :=
  Set.InjOn Prod.fst (state.chunks : Set (ℕ × Sym))

/-- Initialize a decoder with no received chunks. -/
def empty (ecp : ErasureCodePayload M Sym) : DecoderState M Sym :=
  { ecp, chunks := ∅ }

/-- Add a chunk unless its index is already present. The first symbol received at an
index is retained, so exact duplicates are harmless and later conflicts are ignored.
Streaming guarantees here are erasure-only and assume honest, in-range chunk indices. -/
def addChunk [DecidableEq Sym] (state : DecoderState M Sym) (chunk : ℕ × Sym) :
    DecoderState M Sym :=
  if state.HasIndex chunk.1 then state
  else { state with chunks := insert chunk state.chunks }

/-- Attempt to decode the chunks accumulated by the decoder. -/
def decodedPayload (state : DecoderState M Sym) : Option M :=
  state.ecp.decode state.chunks

/-- Whether the accumulated chunks currently decode to a payload. -/
def hasMessage (state : DecoderState M Sym) : Bool :=
  state.decodedPayload.isSome

uses Definition 4.1.2 · github #251

Lean code for Definition4.1.3●8 definitions

structure(3 fields)defined in SecureMessaging/ErasureCode/Streaming.lean

complete

structure ErasureCodePayload.Streaming.EncoderState (M Sym : Type) : Type

structure ErasureCodePayload.Streaming.EncoderState
  (M Sym : Type) : Type

Encoder state for one erasure-coded payload stream. It stores the erasure-code
payload scheme, the payload being encoded, and the counter for the next chunk.

Fields

ecp : ErasureCodePayload M Sym

The erasure-code payload scheme used to encode this stream.

payload : M

The fixed payload encoded by this stream.

nextIndex : ℕ

The natural-number counter used for the next emitted chunk.

defdefined in SecureMessaging/ErasureCode/Streaming.lean

complete

def ErasureCodePayload.Streaming.EncoderState.init {M Sym : Type}
  (ecp : ErasureCodePayload M Sym) (payload : M) :
  ErasureCodePayload.Streaming.EncoderState M Sym

def ErasureCodePayload.Streaming.EncoderState.init
  {M Sym : Type}
  (ecp : ErasureCodePayload M Sym)
  (payload : M) :
  ErasureCodePayload.Streaming.EncoderState
    M Sym

Initialize an encoder before emitting its first chunk.

defdefined in SecureMessaging/ErasureCode/Streaming.lean

complete

def ErasureCodePayload.Streaming.EncoderState.nextChunk {M Sym : Type}
  (state : ErasureCodePayload.Streaming.EncoderState M Sym) :
  (ℕ × Sym) × ErasureCodePayload.Streaming.EncoderState M Sym

def ErasureCodePayload.Streaming.EncoderState.nextChunk
  {M Sym : Type}
  (state :
    ErasureCodePayload.Streaming.EncoderState
      M Sym) :
  (ℕ × Sym) ×
    ErasureCodePayload.Streaming.EncoderState
      M Sym

Emit the chunk at the current counter and advance the counter by one.

structure(2 fields)defined in SecureMessaging/ErasureCode/Streaming.lean

complete

structure ErasureCodePayload.Streaming.DecoderState (M Sym : Type) : Type

structure ErasureCodePayload.Streaming.DecoderState
  (M Sym : Type) : Type

Decoder state for one erasure-coded payload stream. It stores the erasure-code
payload scheme and the indexed chunks received so far.

Fields

ecp : ErasureCodePayload M Sym

The erasure-code payload scheme used to decode this stream.

chunks : Finset (ℕ × Sym)

Indexed chunks retained by the decoder, with at most one symbol per index for
states reachable from `empty` through `addChunk`.

defdefined in SecureMessaging/ErasureCode/Streaming.lean

complete

def ErasureCodePayload.Streaming.DecoderState.empty {M Sym : Type}
  (ecp : ErasureCodePayload M Sym) :
  ErasureCodePayload.Streaming.DecoderState M Sym

def ErasureCodePayload.Streaming.DecoderState.empty
  {M Sym : Type}
  (ecp : ErasureCodePayload M Sym) :
  ErasureCodePayload.Streaming.DecoderState
    M Sym

Initialize a decoder with no received chunks.

defdefined in SecureMessaging/ErasureCode/Streaming.lean

complete

def ErasureCodePayload.Streaming.DecoderState.addChunk {M Sym : Type}
  [DecidableEq Sym]
  (state : ErasureCodePayload.Streaming.DecoderState M Sym)
  (chunk : ℕ × Sym) : ErasureCodePayload.Streaming.DecoderState M Sym

def ErasureCodePayload.Streaming.DecoderState.addChunk
  {M Sym : Type} [DecidableEq Sym]
  (state :
    ErasureCodePayload.Streaming.DecoderState
      M Sym)
  (chunk : ℕ × Sym) :
  ErasureCodePayload.Streaming.DecoderState
    M Sym

Add a chunk unless its index is already present. The first symbol received at an
index is retained, so exact duplicates are harmless and later conflicts are ignored.
Streaming guarantees here are erasure-only and assume honest, in-range chunk indices.

defdefined in SecureMessaging/ErasureCode/Streaming.lean

complete

def ErasureCodePayload.Streaming.DecoderState.decodedPayload {M Sym : Type}
  (state : ErasureCodePayload.Streaming.DecoderState M Sym) : Option M

def ErasureCodePayload.Streaming.DecoderState.decodedPayload
  {M Sym : Type}
  (state :
    ErasureCodePayload.Streaming.DecoderState
      M Sym) :
  Option M

Attempt to decode the chunks accumulated by the decoder.

defdefined in SecureMessaging/ErasureCode/Streaming.lean

complete

def ErasureCodePayload.Streaming.DecoderState.hasMessage {M Sym : Type}
  (state : ErasureCodePayload.Streaming.DecoderState M Sym) : Bool

def ErasureCodePayload.Streaming.DecoderState.hasMessage
  {M Sym : Type}
  (state :
    ErasureCodePayload.Streaming.DecoderState
      M Sym) :
  Bool

Whether the accumulated chunks currently decode to a payload.

Definition4.1.4

Group: Erasure Codes. (3)

Group member previews

Preview

Definition 4.1.1

Loading preview

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

uses 1

Used by 6

Reverse dependency previews

Preview

Theorem 4.2.2

Loading preview

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

✓L∃∀N

\todo

chunk set L_I = \{(i, \mathsf{Encode}(M, i)) \mid i \in I\}

def encodeChunks (ec : ErasureCode Sym)
    (M : Fin ec.nchunk → Sym) (I : Finset (Fin ec.N)) :
    Finset (Fin ec.N × Sym) :=
  I.map {
    toFun := fun i => (i, ec.encode M i)
    inj' := fun _ _ h => congrArg Prod.fst h
  }

correctness predicate

def Correct (ec : ErasureCode Sym) : Prop :=
  ∀ (M : Fin ec.nchunk → Sym) (I : Finset (Fin ec.N)),
    (ec.nchunk ≤ I.card → ec.decode (ec.encodeChunks M I) = some M) ∧
    (I.card < ec.nchunk → ec.decode (ec.encodeChunks M I) = none)

uses Definition 4.1.1 · github #191

Lean code for Definition4.1.4●2 definitions

defdefined in SecureMessaging/ErasureCode/Defs.lean

complete

def ErasureCode.encodeChunks {Sym : Type} (ec : ErasureCode Sym)
  (M : Fin ec.nchunk → Sym) (I : Finset (Fin ec.N)) :
  Finset (Fin ec.N × Sym)

def ErasureCode.encodeChunks {Sym : Type}
  (ec : ErasureCode Sym)
  (M : Fin ec.nchunk → Sym)
  (I : Finset (Fin ec.N)) :
  Finset (Fin ec.N × Sym)

The honest chunk set of `M` at positions `I`:
`{(i, Encode(M, i)) | i ∈ I}`.

The index is retained in each chunk, so distinct positions remain distinct even
when their encoded symbols are equal.

defdefined in SecureMessaging/ErasureCode/Defs.lean

complete

def ErasureCode.Correct {Sym : Type} (ec : ErasureCode Sym) : Prop

def ErasureCode.Correct {Sym : Type}
  (ec : ErasureCode Sym) : Prop

Correctness: decoding the chunk set `{(i, Encode(M, i)) | i ∈ I}` recovers
`M` when `nchunk ≤ |I|` and fails when `|I| < nchunk`.