Interface

Difficulty: moderate — 4 definitions, 0 abbreviations, 0 lemmas, 0 theorems, 0 examples.

definition
legend
ApplicationLayer.Op : Type
Show details 
| ApplicationLayer.Op.create : ApplicationLayer.Op
| ApplicationLayer.Op.bind : ApplicationLayer.Op
| ApplicationLayer.Op.listen : ApplicationLayer.Op
| ApplicationLayer.Op.connect : ApplicationLayer.Op
| ApplicationLayer.Op.accept : ApplicationLayer.Op
| ApplicationLayer.Op.send : ApplicationLayer.Op
| ApplicationLayer.Op.receive : ApplicationLayer.Op
| ApplicationLayer.Op.close : ApplicationLayer.Op

Outer dependencies: (none)

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

Used by: ApplicationLayer.Value, ApplicationLayer.interface, TransportLayer.application

ApplicationLayer.Value (SocketId Address PortNumber : Type) (n : ℕ) : ApplicationLayer.Op → Type
Show details 
fun SocketId Address PortNumber n x =>
  match x with
  | ApplicationLayer.Op.create => SocketId
  | ApplicationLayer.Op.bind => SocketId × Address × PortNumber
  | ApplicationLayer.Op.listen => SocketId
  | ApplicationLayer.Op.connect => SocketId × Address × PortNumber
  | ApplicationLayer.Op.accept => SocketId × SocketId
  | ApplicationLayer.Op.send => SocketId × BitSequence n
  | ApplicationLayer.Op.receive => SocketId × BitSequence n
  | ApplicationLayer.Op.close => SocketId

Complexity: 81 (size of the value term)

Outer dependencies: ApplicationLayer.Op

Inner dependencies: BitSequence

Lean core dependencies: Nat, Prod, Unit, Unit.unit

Used by: ApplicationLayer.interface

application-layer
ApplicationLayer.interface (SocketId Address PortNumber : Type) [Nonempty SocketId] [Norm SocketId]
  [Nonempty Address] [Norm Address] [Nonempty PortNumber] [Norm PortNumber] (n : ℕ) : InterfaceOld
Show details 
fun SocketId Address PortNumber [Nonempty SocketId] [Norm SocketId] [Nonempty Address]
    [Norm Address] [Nonempty PortNumber] [Norm PortNumber] n =>
  { Ports := ApplicationLayer.Op, Port := ApplicationLayer.Value SocketId Address PortNumber n,
    nonempty := ⋯,
    size := fun op =>
      ApplicationLayer.Op.casesOn (motive := fun t =>
        op = t → Norm (ApplicationLayer.Value SocketId Address PortNumber n op)) op
        (fun h => ⋯ ▸ inferInstance) (fun h => ⋯ ▸ inferInstance) (fun h => ⋯ ▸ inferInstance)
        (fun h => ⋯ ▸ inferInstance) (fun h => ⋯ ▸ inferInstance) (fun h => ⋯ ▸ inferInstance)
        (fun h => ⋯ ▸ inferInstance) (fun h => ⋯ ▸ inferInstance) ⋯,
    Coherent := fun s => s.card ≤ 1, coherent_empty := ApplicationLayer.interface._proof_2,
    coherent_singleton := ApplicationLayer.interface._proof_3,
    coherent_downward := @ApplicationLayer.interface._proof_4 }

Complexity: 689 (size of the value term)

Outer dependencies: InterfaceOld

Inner dependencies: ApplicationLayer.Op, ApplicationLayer.Value, Bit, BitSequence, instNormBit, instNormForallFin_computerNetworks

Mathlib dependencies: Finset, Finset.card, Finset.card_le_card, Finset.card_singleton, Norm, le_trans

Lean core dependencies: Eq, Eq.symm, Eq.trans, Fin, Nat, Nonempty, Prod, True, congrArg, congrFun', inferInstance, of_eq_true

Used by: NetworkArchitecture.application, TransportLayer.application

TransportLayer.application (SocketId Address PortNumber Port : Type) [Nonempty SocketId]
  [Norm SocketId] [Nonempty Address] [Norm Address] [Nonempty PortNumber] [Norm PortNumber]
  [Nonempty Port] [Norm Port] (n : ℕ) :
  Layer (TransportLayer.interface Port n) (ApplicationLayer.interface SocketId Address PortNumber n)
Show details 
fun SocketId Address PortNumber Port [Nonempty SocketId] [Norm SocketId] [Nonempty Address]
    [Norm Address] [Nonempty PortNumber] [Norm PortNumber] [Nonempty Port] [Norm Port] n v =>
  (∀ (h : ApplicationLayer.Op.send ∈ v.right.fired),
      ∃ s, v.left.observe = some s ∧ (v.right.value ⟨ApplicationLayer.Op.send, h⟩).2 = s.payload) ∧
    (∀ (h : ApplicationLayer.Op.receive ∈ v.right.fired),
        ∃ s,
          v.left.observe = some s ∧
            (v.right.value ⟨ApplicationLayer.Op.receive, h⟩).2 = s.payload) ∧
      ((∀ op ∈ v.right.fired, op ≠ ApplicationLayer.Op.send ∧ op ≠ ApplicationLayer.Op.receive) →
        v.left.observe = none)

Complexity: 1685 (size of the value term)

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

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

Mathlib dependencies: Finset, Norm

Lean core dependencies: And, Eq, Exists, Nat, Ne, Nonempty, Option

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.

definitiondeclared elsewheredependencyproof dependency
legend