NetworkArchitecture

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

definition
legend
layered-architecture
NetworkArchitecture (Address PortNumber SocketId : Type) [Nonempty Address] [Norm Address]
  [Nonempty PortNumber] [Norm PortNumber] [Nonempty SocketId] [Norm SocketId] (poly : List Bool)
  (n : ℕ) : Type 1
Show details 
| NetworkArchitecture.mk : {Address PortNumber SocketId : Type} →
  [inst : Nonempty Address] →
    [inst_1 : Norm Address] →
      [inst_2 : Nonempty PortNumber] →
        [inst_3 : Norm PortNumber] →
          [inst_4 : Nonempty SocketId] →
            [inst_5 : Norm SocketId] →
              {poly : List Bool} →
                {n : ℕ} → Topology → NetworkArchitecture Address PortNumber SocketId poly n

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

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 
fun {Address PortNumber SocketId} [Nonempty Address] [Norm Address] [Nonempty PortNumber]
    [Norm PortNumber] [Nonempty SocketId] [Norm SocketId] {poly} {n} x =>
  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

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 
fun {Address PortNumber SocketId} [Nonempty Address] [Norm Address] [Nonempty PortNumber]
    [Norm PortNumber] [Nonempty SocketId] [Norm SocketId] {poly} {n} x =>
  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)

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 
fun {Address PortNumber SocketId} [Nonempty Address] [Norm Address] [Nonempty PortNumber]
    [Norm PortNumber] [Nonempty SocketId] [Norm SocketId] {poly} {n} x =>
  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)

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 
fun {Address PortNumber SocketId} [Nonempty Address] [Norm Address] [Nonempty PortNumber]
    [Norm PortNumber] [Nonempty SocketId] [Norm SocketId] {poly} {n} x =>
  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

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 
fun {Address PortNumber SocketId} [Nonempty Address] [Norm Address] [Nonempty PortNumber]
    [Norm PortNumber] [Nonempty SocketId] [Norm SocketId] {poly} {n} NA =>
  (((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