Interface

Difficulty: easy — 3 definitions, 0 abbreviations, 0 lemmas, 2 theorems, 0 examples.

definition theorem
legend
structure Segment (Port Payload : Type) : Type
  • sourcePort : Port
  • destPort : Port
  • payload : Payload
Show details

Outer dependencies: (none)

Lean core dependencies: Eq, HEq, Nat, SizeOf, eq_of_heq

Used by: NetworkLayer.transport, TransportLayer.application, TransportLayer.interface, instNonemptySegment, instNormSegment

instance instNonemptySegment {Port Payload : Type} [Nonempty Port] [Nonempty Payload] :
  Nonempty (Segment Port Payload)
Show details 
fun {Port Payload} [inst : Nonempty Port] [inst_1 : Nonempty Payload] =>
  Nonempty.intro
    { sourcePort := Classical.choice inst, destPort := Classical.choice inst,
      payload := Classical.choice inst_1 }

Complexity: 43 (size of the value term)

Outer dependencies: Segment

Lean core dependencies: Nonempty

Used by: TransportLayer.interface

instance instNormSegment {Port Payload : Type} [Norm Port] [Norm Payload] : Norm (Segment Port Payload)
Show details 
| instNormSegment = { norm := fun s => ‖s.sourcePort‖ + ‖s.destPort‖ + ‖s.payload‖ }

Complexity: 95 (size of the value term)

Outer dependencies: Segment

Mathlib dependencies: Norm, Real

Used by: NetworkLayer.transport, TransportLayer.application, TransportLayer.interface

transport-layer
def TransportLayer.interface (Port : Type) [Nonempty Port] [Norm Port] (n : ℕ) : InterfaceOld
Show details 
| TransportLayer.interface Port n = InterfaceOld.single (Segment Port (BitSequence n))

Complexity: 47 (size of the value term)

Outer dependencies: InterfaceOld

Inner dependencies: Bit, BitSequence, InterfaceOld.single, Segment, instNonemptySegment, instNormBit, instNormForallFin_computerNetworks, instNormSegment

Mathlib dependencies: Norm

Lean core dependencies: Fin, Nat, Nonempty

Used by: NetworkArchitecture.stack, NetworkArchitecture.transport, NetworkLayer.transport, TransportLayer.application

def NetworkLayer.transport (Address Port : Type) [Nonempty Address] [Norm Address] [Nonempty Port]
  [Norm Port] (n : ℕ) : Layer (NetworkLayer.interface Address n) (TransportLayer.interface Port n)
Show details 
| NetworkLayer.transport Address Port n v =
  match v.left.observe, v.right.observe with
  | none, none => True
  | some p, some s => p.payload = s.payload
  | x, x_1 => False

Complexity: 263 (size of the value term)

Outer dependencies: Layer, NetworkLayer.interface, TransportLayer.interface

Inner dependencies: Bit, BitSequence, InterfaceOld.Value, InterfaceOld.Value.left, InterfaceOld.Value.observe, InterfaceOld.Value.right, InterfaceOld.tensor, Packet, Segment, instNormBit, instNormForallFin_computerNetworks, instNormPacket, instNormSegment

Mathlib dependencies: Norm

Lean core dependencies: Bool, Eq, False, Nat, Nat.hasNotBit, Nat.land, Nat.ne_of_beq_eq_false, Nat.shiftRight, Nonempty, Option, True, Unit, Unit.unit

Used by: NetworkArchitecture.stack

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.

definitiontheoremdeclared elsewheredependencyproof dependency
legend