Interface

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

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

Outer dependencies: (none)

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

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

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

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

Complexity: 17 (size of the value term)

Outer dependencies: NetworkLayer.Protocol

Mathlib dependencies: Norm, Real

Used by: instNormPacket

icmp
Icmp : Type
Show details 
| Icmp.echoRequest : Icmp
| Icmp.echoReply : Icmp
| Icmp.destinationUnreachable : Icmp
| Icmp.timeExceeded : Icmp

Outer dependencies: (none)

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

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

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

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

Complexity: 17 (size of the value term)

Outer dependencies: Icmp

Mathlib dependencies: Norm, Real

Used by: instNormPacket

Packet (Address Payload : Type) : Type
Show details 
| Packet.mk : {Address Payload : Type} →
  Address → Address → Address → NetworkLayer.Protocol → Icmp → ℕ → Payload → Packet Address Payload

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

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

instNormPacket {Address Payload : Type} [Norm Address] [Norm Payload] :
  Norm (Packet Address Payload)
Show details 
fun {Address Payload} [Norm Address] [Norm Payload] =>
  {
    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
NetworkLayer.interface (Address : Type) [Nonempty Address] [Norm Address] (n : ℕ) : InterfaceOld
Show details 
fun Address [Nonempty Address] [Norm 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

DataLinkLayer.network (Address : Type) [Nonempty Address] [Norm Address] (poly : List Bool)
  (n : ℕ) : Layer (DataLinkLayer.interface poly n) (NetworkLayer.interface Address n)
Show details 
fun Address [Nonempty Address] [Norm 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

ForwardingTable (Address : Type) : Type
Show details 
| ForwardingTable.mk : {Address : Type} → (Address → Address → Option Address) → ForwardingTable Address

Outer dependencies: (none)

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

Used by: NetworkLayer.forwards

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 
fun Address [Nonempty Address] [Norm 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