Envelope

Difficulty: moderate — 3 definitions, 1 abbreviations, 1 lemmas, 3 theorems.

definition abbreviation lemma theorem
legend

An envelope wraps up a payload together with a check value, computed by a cyclic redundancy check (CRC), that lets a receiver tell whether the payload arrived corrupted. Its payload and check are made of Bits (see Information), not Bools: each one stands for an actual observation, so it genuinely carries information.

A short list of bits (a “check”) computed from a longer list of bits (bits), following a fixed rule (poly) that stays the same for every envelope. Two different inputs almost never produce the same check; in particular, changing even a single bit of bits always changes it (see crc_detects_single_bit_flip below) — that’s what makes it useful for catching corruption.

def crc (poly : List Bool) (bits : List Bool) : List Bool :=
  let k := poly.length
  bits.foldl
    (fun reg bit =>
      let top := reg.headD false
      let shifted := reg.tail ++ [bit]
      if top then List.zipWith xor shifted poly else shifted)
    (List.replicate k false)

Outer dependencies: (none)

Lean core dependencies: Bool, Bool.xor, Eq, List, List.foldl, List.headD, List.length, List.replicate, List.tail, List.zipWith, Nat, ite

Used by: Envelope.make, Envelope.valid, Receiver.step, Receiver.step_correct, crc_detects_single_bit_flip

An envelope: a payload of n bits, plus a k-bit CRC check computed from it under generator poly.

structure Envelope (poly : List Bool) (n k : Nat) where
  payload : Fin n → Bit
  check : Fin k → Bit

Outer dependencies: (none)

Inner dependencies: Bit

Lean core dependencies: Bool, Eq, Fin, HEq, List, Nat, eq_of_heq

Used by: Envelope.make, Envelope.valid, Receiver.step, Receiver.step_correct, Sender.State, Sender.step, instNonemptyEnvelope, instNonemptyState, instNormEnvelope, instNormState

instance {poly : List Bool} {n k : Nat} : Nonempty (Envelope poly n k) :=

Outer dependencies: Envelope

Inner dependencies: Bit

Lean core dependencies: Bool, Fin, List, Nat, Nonempty, inferInstance

Used by: Receiver.step, Receiver.step_correct, Sender.step, instNonemptyState

instance {poly : List Bool} {n k : Nat} : Norm (Envelope poly n k) where
  norm e := ‖e.payload‖ + ‖e.check‖

Outer dependencies: Envelope

Inner dependencies: Bit, instNormBit, instNormForallFin_computerNetworks

Mathlib dependencies: Norm, Real

Lean core dependencies: Bool, Fin, List, Nat

Used by: Receiver.step, Receiver.step_correct, Sender.step, instNormState

Build an envelope from a payload, filling in its check value via crc.

def Envelope.make (poly : List Bool) (n : Nat) (payload : Fin n → Bit) :
    Envelope poly n poly.length :=
  { payload
    check := fun i => (crc poly (List.ofFn (fun j => (payload j : Bool))))[(i : Nat)]?.getD false }

Outer dependencies: Bit, Envelope

Inner dependencies: crc

Lean core dependencies: Bool, Fin, List, List.length, List.ofFn, Nat, Option.getD

Used by: Envelope.make_valid

An envelope is valid exactly when its check value matches what crc recomputes from its payload — a receiver holding a corrupted envelope can tell, as long as the corruption actually changes the check (see crc_detects_single_bit_flip below).

abbrev Envelope.valid (poly : List Bool) {n : Nat} (e : Envelope poly n poly.length) : Prop :=
  ∀ i, e.check i = (crc poly (List.ofFn (fun j => (e.payload j : Bool))))[(i : Nat)]?.getD false

Outer dependencies: Envelope

Inner dependencies: Bit, crc

Lean core dependencies: Bool, Eq, Fin, List, List.length, List.ofFn, Nat, Option.getD

Used by: Envelope.make_valid, Receiver.step, Receiver.step_correct

An envelope built by Envelope.make is always valid: the check is computed directly from the payload it accompanies, no corruption possible before it’s even sent.

theorem Envelope.make_valid (poly : List Bool) (n : Nat) (payload : Fin n → Bit) :
    Envelope.valid poly (Envelope.make poly n payload) := by

Dependencies: Bit, Envelope.make, Envelope.valid

Lean core dependencies: Bool, Fin, Lean.Name, List, Nat

Used by: (none)

The main point of a CRC: flipping exactly one bit of the payload changes the check value it should have, for any nonzero generator polynomial — so a receiver comparing the check it got against the check it recomputes will notice a single-bit corruption.

theorem crc_detects_single_bit_flip (poly : List Bool) (hpoly : poly.any id)
    (bits : List Bool) (i : Fin bits.length) :
    crc poly (bits.set i (!bits[i])) ≠ crc poly bits := by

Dependencies: crc

Lean core dependencies: Bool, Bool.not, Decidable.byContradiction, Decidable.decide, Eq, Eq.symm, Eq.trans, Fin, Int, Int.add_one_le_of_lt, Int.sub_nonneg_of_le, Lean.Name, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.tidy_sat, List, List.any, List.length, List.set, Nat, Nat.cast, Nat.le_of_not_lt, Ne, Not, id, le_of_le_of_eq, of_decide_eq_true

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll) to zoom, click a node to jump to it.

definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency
legend