Interface

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

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

Outer dependencies: (none)

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

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

def ApplicationLayer.Value (SocketId Address PortNumber : Type) (n : ℕ) : ApplicationLayer.Op → Type
Show details 
| ApplicationLayer.Value SocketId Address PortNumber n ApplicationLayer.Op.create = SocketId
| ApplicationLayer.Value SocketId Address PortNumber n ApplicationLayer.Op.bind =
  (SocketId × Address × PortNumber)
| ApplicationLayer.Value SocketId Address PortNumber n ApplicationLayer.Op.listen = SocketId
| ApplicationLayer.Value SocketId Address PortNumber n ApplicationLayer.Op.connect =
  (SocketId × Address × PortNumber)
| ApplicationLayer.Value SocketId Address PortNumber n ApplicationLayer.Op.accept =
  (SocketId × SocketId)
| ApplicationLayer.Value SocketId Address PortNumber n ApplicationLayer.Op.send =
  (SocketId × BitSequence n)
| ApplicationLayer.Value SocketId Address PortNumber n ApplicationLayer.Op.receive =
  (SocketId × BitSequence n)
| ApplicationLayer.Value SocketId Address PortNumber 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
def ApplicationLayer.interface (SocketId Address PortNumber : Type) [Nonempty SocketId] [Norm SocketId]
  [Nonempty Address] [Norm Address] [Nonempty PortNumber] [Norm PortNumber] (n : ℕ) : InterfaceOld
Show details 
| ApplicationLayer.interface SocketId Address 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

def 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 
| TransportLayer.application SocketId Address PortNumber 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