Arp

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

definition
legend
structure AddressResolution (Address : Type) (k : ℕ) : Type
  • resolve : Address → Option (Fin k)
Show details

Outer dependencies: (none)

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

Used by: NetworkLayer.resolves

def NetworkLayer.resolves (Address : Type) [Nonempty Address] [Norm Address] {k : ℕ}
  (table : AddressResolution Address k) (poly : List Bool) (n : ℕ) :
  Layer (NetworkLayer.interface Address n) (DataLinkLayer.links poly n k)
Show details 
| NetworkLayer.resolves Address table poly n v =
  match v.left.observe with
  | none => v.right.fired = ∅
  | some p =>
    match table.resolve p.next with
    | none => v.right.fired = ∅
    | some link =>
      ∃ (h : link ∈ v.right.fired),
        v.right.fired = {link} ∧ (v.right.value ⟨link, h⟩).payload = p.payload

Complexity: 751 (size of the value term)

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

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

Mathlib dependencies: Finset, Norm

Lean core dependencies: And, Bool, Eq, Exists, Fin, List, List.length, Nat, Nonempty, Option, Unit, Unit.unit

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.

definitiondeclared elsewheredependencyproof dependency
legend