Interface

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

definition theorem
legend
inductive NetworkLayer.Protocol : Type
  • data : NetworkLayer.Protocol
  • icmp : NetworkLayer.Protocol
Show details

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, Nat.ble, PULift, cond, noConfusionEnum, noConfusionTypeEnum

Used by: NetworkLayer.forwards, Packet, instNonemptyPacket, instNonemptyProtocol, instNormPacket, instNormProtocol

instance instNonemptyProtocol : Nonempty NetworkLayer.Protocol
Show details 
Nonempty.intro NetworkLayer.Protocol.data

Complexity: 5 (size of the value term)

Outer dependencies: NetworkLayer.Protocol

Lean core dependencies: Nonempty

Used by: instNonemptyPacket

instance instNormProtocol : Norm NetworkLayer.Protocol
Show details 
| instNormProtocol = { norm := fun x => 1 }

Complexity: 17 (size of the value term)

Outer dependencies: NetworkLayer.Protocol

Mathlib dependencies: Norm, Real

Used by: instNormPacket

icmp
inductive Icmp : Type
  • echoRequest : Icmp
  • echoReply : Icmp
  • destinationUnreachable : Icmp
  • timeExceeded : Icmp
Show details

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, Nat.ble, PULift, cond, noConfusionEnum, noConfusionTypeEnum

Used by: NetworkLayer.forwards, Packet, instNonemptyIcmp, instNonemptyPacket, instNormIcmp, instNormPacket

instance instNonemptyIcmp : Nonempty Icmp
Show details 
Nonempty.intro Icmp.echoRequest

Complexity: 5 (size of the value term)

Outer dependencies: Icmp

Lean core dependencies: Nonempty

Used by: instNonemptyPacket

instance instNormIcmp : Norm Icmp
Show details 
| instNormIcmp = { norm := fun x => 1 }

Complexity: 17 (size of the value term)

Outer dependencies: Icmp

Mathlib dependencies: Norm, Real

Used by: instNormPacket

structure Packet (Address Payload : Type) : Type
  • source : Address
  • dest : Address
  • next : Address
  • protocol : NetworkLayer.Protocol
  • icmp : Icmp
  • ttl : ℕ
  • payload : Payload
Show details

Outer dependencies: (none)

Inner dependencies: Icmp, NetworkLayer.Protocol

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

Used by: DataLinkLayer.network, NetworkLayer.forwards, NetworkLayer.interface, NetworkLayer.resolves, NetworkLayer.transport, instNonemptyPacket, instNormPacket

instance instNonemptyPacket {Address Payload : Type} [Nonempty Address] [Nonempty Payload] :
  Nonempty (Packet Address Payload)
Show details 
fun {Address Payload} [inst : Nonempty Address] [inst_1 : Nonempty Payload] =>
  Nonempty.intro
    { source := Classical.choice inst, dest := Classical.choice inst, next := Classical.choice inst,
      protocol := Classical.choice inferInstance, icmp := Classical.choice inferInstance, ttl := 0,
      payload := Classical.choice inst_1 }

Complexity: 83 (size of the value term)

Outer dependencies: Packet

Inner dependencies: Icmp, NetworkLayer.Protocol, instNonemptyIcmp, instNonemptyProtocol

Lean core dependencies: Nat, Nonempty, inferInstance

Used by: NetworkLayer.interface

instance instNormPacket {Address Payload : Type} [Norm Address] [Norm Payload] :
  Norm (Packet Address Payload)
Show details 
| instNormPacket =
  {
    norm := fun p =>
      ‖p.source‖ + ‖p.dest‖ + ‖p.next‖ + ‖p.protocol‖ + ‖p.icmp‖ + ↑p.ttl + ‖p.payload‖ }

Complexity: 207 (size of the value term)

Outer dependencies: Packet

Inner dependencies: Icmp, NetworkLayer.Protocol, instNormIcmp, instNormProtocol

Mathlib dependencies: Norm, Real

Lean core dependencies: Nat.cast

Used by: DataLinkLayer.network, NetworkLayer.forwards, NetworkLayer.interface, NetworkLayer.resolves, NetworkLayer.transport

network-layer
def NetworkLayer.interface (Address : Type) [Nonempty Address] [Norm Address] (n : ℕ) : InterfaceOld
Show details 
| NetworkLayer.interface Address n = InterfaceOld.single (Packet Address (BitSequence n))

Complexity: 47 (size of the value term)

Outer dependencies: InterfaceOld

Inner dependencies: Bit, BitSequence, InterfaceOld.single, Packet, instNonemptyPacket, instNormBit, instNormForallFin_computerNetworks, instNormPacket

Mathlib dependencies: Norm

Lean core dependencies: Fin, Nat, Nonempty

Used by: DataLinkLayer.network, NetworkArchitecture.network, NetworkArchitecture.stack, NetworkLayer.forwards, NetworkLayer.resolves, NetworkLayer.transport

def DataLinkLayer.network (Address : Type) [Nonempty Address] [Norm Address] (poly : List Bool)
  (n : ℕ) : Layer (DataLinkLayer.interface poly n) (NetworkLayer.interface Address n)
Show details 
| DataLinkLayer.network Address poly n v =
  match v.left.observe, v.right.observe with
  | none, none => True
  | some e, some p => Frame.valid poly e ∧ e.payload = p.payload
  | x, x_1 => False

Complexity: 269 (size of the value term)

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

Inner dependencies: Bit, BitSequence, Frame, Frame.valid, InterfaceOld.Value, InterfaceOld.Value.left, InterfaceOld.Value.observe, InterfaceOld.Value.right, InterfaceOld.tensor, Packet, instNormBit, instNormForallFin_computerNetworks, instNormFrame, instNormPacket

Mathlib dependencies: Norm

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

Used by: NetworkArchitecture.stack

structure ForwardingTable (Address : Type) : Type
  • nextHop : Address → Address → Option Address
Show details

Outer dependencies: (none)

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

Used by: NetworkLayer.forwards

def NetworkLayer.forwards (Address : Type) [Nonempty Address] [Norm Address]
  (table : ForwardingTable Address) (here : Address) (n : ℕ) :
  Layer (NetworkLayer.interface Address n) (NetworkLayer.interface Address n)
Show details 
| NetworkLayer.forwards Address table here n v =
  match v.left.observe, v.right.observe with
  | none, none => True
  | some p, some q =>
    if p.ttl = 0 then
      q.source = here ∧
        q.dest = p.source ∧ q.protocol = NetworkLayer.Protocol.icmp ∧ q.icmp = Icmp.timeExceeded
    else
      match table.nextHop p.dest here with
      | some hop =>
        p.source = q.source ∧
          p.dest = q.dest ∧
            p.protocol = q.protocol ∧ p.payload = q.payload ∧ q.next = hop ∧ q.ttl = p.ttl - 1
      | none =>
        q.source = here ∧
          q.dest = p.source ∧
            q.protocol = NetworkLayer.Protocol.icmp ∧ q.icmp = Icmp.destinationUnreachable
  | x, x_1 => False

Complexity: 641 (size of the value term)

Outer dependencies: ForwardingTable, Layer, NetworkLayer.interface

Inner dependencies: Bit, BitSequence, Icmp, InterfaceOld.Value, InterfaceOld.Value.left, InterfaceOld.Value.observe, InterfaceOld.Value.right, InterfaceOld.tensor, NetworkLayer.Protocol, Packet, instNormBit, instNormForallFin_computerNetworks, instNormPacket

Mathlib dependencies: Norm

Lean core dependencies: And, Eq, False, Nat, Nat.hasNotBit, Nonempty, Option, True, Unit, Unit.unit, ite

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.

definitiontheoremdeclared elsewheredependencyproof dependency
legend