NetworkArchitecture

Difficulty: hard — 7 definitions, 0 abbreviations, 0 lemmas, 0 theorems, 0 examples.

definition
legend
layered-architecture
structure NetworkArchitecture (Address PortNumber SocketId : Type) [Nonempty Address] [Norm Address]
  [Nonempty PortNumber] [Norm PortNumber] [Nonempty SocketId] [Norm SocketId] (poly : List Bool)
  (n : ℕ) : Type 1
  • topology : Topology
Show details

Outer dependencies: (none)

Inner dependencies: Topology

Mathlib dependencies: Norm

Lean core dependencies: Bool, Eq, HEq, List, Nat, Nonempty, SizeOf, eq_of_heq

Used by: NetworkArchitecture.application, NetworkArchitecture.dataLink, NetworkArchitecture.network, NetworkArchitecture.physical, NetworkArchitecture.stack, NetworkArchitecture.transport

def NetworkArchitecture.physical {Address PortNumber SocketId : Type} [Nonempty Address] [Norm Address]
  [Nonempty PortNumber] [Norm PortNumber] [Nonempty SocketId] [Norm SocketId] {poly : List Bool}
  {n : ℕ} : NetworkArchitecture Address PortNumber SocketId poly n → InterfaceOld
Show details 
| x✝.physical = PhysicalLayer.interface (n + poly.length)

Complexity: 83 (size of the value term)

Outer dependencies: InterfaceOld, NetworkArchitecture

Inner dependencies: PhysicalLayer.interface

Mathlib dependencies: Norm

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

Used by: NetworkArchitecture.stack

def NetworkArchitecture.network {Address PortNumber SocketId : Type} [Nonempty Address] [Norm Address]
  [Nonempty PortNumber] [Norm PortNumber] [Nonempty SocketId] [Norm SocketId] {poly : List Bool}
  {n : ℕ} : NetworkArchitecture Address PortNumber SocketId poly n → InterfaceOld
Show details 
| x✝.network = NetworkLayer.interface Address n

Complexity: 69 (size of the value term)

Outer dependencies: InterfaceOld, NetworkArchitecture

Inner dependencies: NetworkLayer.interface

Mathlib dependencies: Norm

Lean core dependencies: Bool, List, Nat, Nonempty

Used by: (none)

def NetworkArchitecture.transport {Address PortNumber SocketId : Type} [Nonempty Address] [Norm Address]
  [Nonempty PortNumber] [Norm PortNumber] [Nonempty SocketId] [Norm SocketId] {poly : List Bool}
  {n : ℕ} : NetworkArchitecture Address PortNumber SocketId poly n → InterfaceOld
Show details 
| x✝.transport = TransportLayer.interface PortNumber n

Complexity: 69 (size of the value term)

Outer dependencies: InterfaceOld, NetworkArchitecture

Inner dependencies: TransportLayer.interface

Mathlib dependencies: Norm

Lean core dependencies: Bool, List, Nat, Nonempty

Used by: (none)

def NetworkArchitecture.application {Address PortNumber SocketId : Type} [Nonempty Address]
  [Norm Address] [Nonempty PortNumber] [Norm PortNumber] [Nonempty SocketId] [Norm SocketId]
  {poly : List Bool} {n : ℕ} : NetworkArchitecture Address PortNumber SocketId poly n → InterfaceOld
Show details 
| x✝.application = ApplicationLayer.interface SocketId Address PortNumber n

Complexity: 81 (size of the value term)

Outer dependencies: InterfaceOld, NetworkArchitecture

Inner dependencies: ApplicationLayer.interface

Mathlib dependencies: Norm

Lean core dependencies: Bool, List, Nat, Nonempty

Used by: NetworkArchitecture.stack

def NetworkArchitecture.stack {Address PortNumber SocketId : Type} [Nonempty Address] [Norm Address]
  [Nonempty PortNumber] [Norm PortNumber] [Nonempty SocketId] [Norm SocketId] {poly : List Bool}
  {n : ℕ} (NA : NetworkArchitecture Address PortNumber SocketId poly n) :
  Layer NA.physical NA.application
Show details 
| NA.stack =
  (((DataLinkLayer.physical poly n).sequential (DataLinkLayer.network Address poly n)).sequential
        (NetworkLayer.transport Address PortNumber n)).sequential
    (TransportLayer.application SocketId Address PortNumber PortNumber n)

Complexity: 277 (size of the value term)

Outer dependencies: Layer, NetworkArchitecture, NetworkArchitecture.application, NetworkArchitecture.physical

Inner dependencies: DataLinkLayer.interface, DataLinkLayer.network, DataLinkLayer.physical, Layer.sequential, NetworkLayer.interface, NetworkLayer.transport, TransportLayer.application, TransportLayer.interface

Mathlib dependencies: Norm

Lean core dependencies: Bool, List, Nat, Nonempty

Used by: (none)

Dependency diagram

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

definitiondeclared elsewheredependencyproof dependency
legend