LayeredArchitecture

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

definition abbreviation theorem
legend

A layer is a piece of a bigger system that only ever talks to its own neighbours: the layer directly above it, and the layer directly below it. It never talks straight to a layer further away. A layer really has two neighbours to answer to at once, though: whatever its neighbour above hands it, and whatever its neighbour below hands it. In one step it reacts to both, and answers both back: something to send up, and something to send down.

Two layers can only sit next to each other when they agree on exactly what crosses the boundary between them. What one layer calls “what I hand down” has to be exactly what the layer below it calls “what I receive from above”: the very same values, on the very same ports.

As an example, here are the five layers a computer network is commonly built from, listed from the top (closest to the program sending something) down to the bottom (closest to the wire):

Six boundaries separate these five layers: one above the application layer, one below the physical layer, and one between every pair of neighbouring layers in between.

noncomputable instance (I : Interface) : Nonempty I.Value :=

Outer dependencies: Interface, Interface.Value

Lean core dependencies: Fin, Nonempty

Used by: Layer

A layer sits between the interface it shares with its neighbour above (up) and the one it shares with its neighbour below (down). In one step it reacts to whatever both neighbours hand it at once, an input from above and an input from below, and answers both at once, an output to above and an output to below.

def Layer (State : Type) [Nonempty State] [Norm State] (up down : Interface) :=
  InformationSystem State (up.Value × down.Value) (up.Value × down.Value)

Outer dependencies: Interface

Mathlib dependencies: Norm

Lean core dependencies: Nonempty, Prod

A layered architecture of n layers. interface k names the boundary directly above layer k (there are n + 1 boundaries in total for n layers: one above the very first layer, and one below every layer including the last). Consecutive layers automatically agree on what crosses the boundary between them, since they both refer to the very same interface value there.

layered-architecture
structure LayeredArchitecture (n : Nat) (interface : Fin (n + 1)  Interface)
    (State : Fin n  Type) [ k, Nonempty (State k)] [ k, Norm (State k)] where
  /-- The layer at position `k`, between the interface directly above it and the one directly
  below it. -/
  layer : (k : Fin n)  Layer (State k) (interface k.castSucc) (interface k.succ)

Outer dependencies: Interface

Inner dependencies: Layer

Mathlib dependencies: Norm

Lean core dependencies: Eq, Fin, Fin.castSucc, Fin.succ, HEq, Nat, Nonempty, SizeOf, eq_of_heq

The six boundaries of a computer network’s five layers, from the one above the application layer down to the one below the physical layer.

def NetworkBoundary (Data Message Segment Packet Frame Signal : Interface) : Fin 6  Interface
  | 0 => Data
  | 1 => Message
  | 2 => Segment
  | 3 => Packet
  | 4 => Frame
  | 5 => Signal

Outer dependencies: Interface

A computer network’s own layered architecture: exactly the five layers described in this file’s own introduction, an instance of the general LayeredArchitecture above.

abbrev NetworkArchitecture (Data Message Segment Packet Frame Signal : Interface)
    (State : Fin 5  Type) [ k, Nonempty (State k)] [ k, Norm (State k)] :=
  LayeredArchitecture 5 (NetworkBoundary Data Message Segment Packet Frame Signal) State

Outer dependencies: Interface

Inner dependencies: LayeredArchitecture, NetworkBoundary

Mathlib dependencies: Norm

Lean core dependencies: Fin, Nat, Nonempty

Used by: (none)

Dependency diagram

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

definitionabbreviationtheoremdeclared elsewheredependencyproof dependency
legend