Protocol

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

definition lemma theorem

legend

A protocol is behaviour: what a sender and a receiver each do, step by step, to move envelopes across a channel that might lose or corrupt them. This file works out the simplest such protocol, “stop-and-wait” retransmission: the sender keeps resending the same envelope until it hears back that the receiver got a valid copy.

The point of the whole protocol: run it for long enough against a channel that isn’t lossy forever (it eventually lets an uncorrupted copy through), and the receiver eventually confirms it got a valid envelope — the payload gets there, even though any individual attempt might not.

NoteSender.State

The sender’s state: the envelope currently “in flight”, and whether it’s still waiting to hear that the receiver got it.

structure Sender.State (poly : List Bool) (n : Nat) where
  pending : Envelope poly n poly.length
  waiting : Bool

Outer dependencies: (none)

Inner dependencies: Envelope

Lean core dependencies: Bool, Eq, HEq, List, List.length, Nat, eq_of_heq

Used by: Sender.step, instNonemptyState, instNormState

ImportantinstNonemptyState

instance {poly : List Bool} {n : Nat} : Nonempty (Sender.State poly n) :=

Outer dependencies: Sender.State

Inner dependencies: Envelope, instNonemptyEnvelope

Lean core dependencies: Bool, List, List.length, Nat, Nonempty, inferInstance

Used by: Sender.step

ImportantinstNormState

instance {poly : List Bool} {n : Nat} : Norm (Sender.State poly n) where
  norm st := ‖st.pending‖

Outer dependencies: Sender.State

Inner dependencies: Envelope, instNormEnvelope

Mathlib dependencies: Norm

Lean core dependencies: Bool, List, List.length, Nat

Used by: Sender.step

NoteSender.step

The sender: on every step it re-sends whatever envelope is pending. Fed true (meaning the receiver confirmed it got a valid copy), it stops waiting; fed false (meaning the receiver reported a bad copy, or nothing has come back yet), it keeps waiting and resends the same envelope next step too.

def Sender.step (poly : List Bool) (n : Nat) :
    InformationSystem (Sender.State poly n) Bool (Envelope poly n poly.length) where
  step st ack := (⟨st.pending, !ack⟩, st.pending)
  conserves := by
    sorry

Outer dependencies: Envelope, InformationSystem, Sender.State, instNonemptyEnvelope, instNonemptyState, instNormBool_computerNetworks, instNormEnvelope, instNormState

Inner dependencies: instNormProd_computerNetworks

Mathlib dependencies: Real

Lean core dependencies: Bool, Bool.not, Eq, Lean.Name, List, List.length, Nat, Prod

Used by: (none)

NoteReceiver.step

The receiver: checks an incoming envelope’s CRC and reports back whether it was valid — the confirmation signal the sender is waiting for. Stateless: it doesn’t need to remember anything between envelopes for this simple protocol.

def Receiver.step (poly : List Bool) (n : Nat) :
    InformationSystem Unit (Envelope poly n poly.length) Bool where
  step _ e := ((), decide (Envelope.valid poly e))
  conserves := by
    sorry

Outer dependencies: Envelope, InformationSystem, instNonemptyEnvelope, instNormBool_computerNetworks, instNormEnvelope, instNormUnit_computerNetworks

Inner dependencies: Bit, Envelope.valid, crc, instNormProd_computerNetworks

Mathlib dependencies: Real

Lean core dependencies: Bool, Decidable.decide, Eq, Fin, Lean.Name, List, List.length, List.ofFn, Nat, Option.getD, Prod, Unit, Unit.unit

Used by: Receiver.step_correct

TipReceiver.step_correct

The receiver reports exactly Envelope.valid: a positive report means the envelope really did arrive uncorrupted, not just that the receiver said so.

theorem Receiver.step_correct (e : Envelope poly n poly.length) :
    ((Receiver.step poly n).step () e).2 = true ↔ Envelope.valid poly e :=

Dependencies: Envelope, Envelope.valid, Receiver.step, instNonemptyEnvelope, instNormBool_computerNetworks, instNormEnvelope, instNormUnit_computerNetworks

Proof dependencies: Bit, crc

Lean core dependencies: Bool, Eq, Fin, Iff, List, List.length, List.ofFn, Nat, Option.getD, Unit, Unit.unit, decide_eq_true_iff

Used by: (none)

Dependency diagram

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

definitionlemmatheoremdeclared elsewheredependencyproof dependency

legend