Shared canonical FD/Readiness/BlockingIo bindings for socket descriptions. Registries store real protocol state under actual allocation identities.

@[reducible, inline]

abbrev Miri.Interpreter.SocketMachine.Ref (H D O : Type) : Type

Equations

• Miri.Interpreter.SocketMachine.Ref H D O = Miri.Interpreter.Files.Ref (Miri.Interpreter.Files.Description H D O)

inductive Miri.Interpreter.SocketMachine.Kind : Type

• virtual : Kind
• tcp : Kind

@[instance_reducible]

instance Miri.Interpreter.SocketMachine.instDecidableEqKind : DecidableEq Kind

Equations

• Miri.Interpreter.SocketMachine.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.SocketMachine.instReprKind.repr : Kind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Miri.Interpreter.SocketMachine.instReprKind : Repr Kind

Equations

• Miri.Interpreter.SocketMachine.instReprKind = { reprPrec := Miri.Interpreter.SocketMachine.instReprKind.repr }

structure Miri.Interpreter.SocketMachine.Registry (R L T E : Type) : Type

• virtual : Array (Files.FdId × VirtualSocket.State)
• tcp : Array (Files.FdId × TcpSocket.State R L T E)

structure Miri.Interpreter.SocketMachine.Store (U R L T E : Type) : Type

• get : U → Except StepError (Registry R L T E)
• put : Registry R L T E → U → Except StepError U

structure Miri.Interpreter.SocketMachine.Descriptor (O : Type) : Type

• inject : Kind → Files.FdId → O
• project : O → Option (Kind × Files.FdId)

def Miri.Interpreter.SocketMachine.kind {O H D : Type} (descriptor : Descriptor O) (ref : Ref H D O) : Option Kind

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.bindVirtual {K U H D O R L T E : Type} (h : ReadinessMachine.Hooks K U H D O) (descriptor : Descriptor O) (store : Store U R L T E) (base : VirtualSocket.Hooks (MachineHooks.State K U) (Ref H D O) E) : VirtualSocket.Hooks (MachineHooks.State K U) (Ref H D O) E

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.dropSocket {K U H D O R L T E : Type} (h : ReadinessMachine.Hooks K U H D O) (descriptor : Descriptor O) (store : Store U R L T E) (virtual : VirtualSocket.Hooks (MachineHooks.State K U) (Ref H D O) E) (hostDrop : TcpSocket.SocketState R L T → MachineHooks.M K U Unit) (ref : Ref H D O) : MachineHooks.M K U Bool

Installed on the descriptor's actual last-drop route. TCP host state drops before ReadinessWatched (struct field order). Virtual peer notification precedes watched-field drop; it transfers a real upgraded ref to the delayed queue.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.bindReadiness {K U H D O R L T E : Type} (h : ReadinessMachine.Hooks K U H D O) (descriptor : Descriptor O) (store : Store U R L T E) (virtual : VirtualSocket.Hooks (MachineHooks.State K U) (Ref H D O) E) (base : Readiness.Hooks (MachineHooks.State K U) (Ref H D O)) : Readiness.Hooks (MachineHooks.State K U) (Ref H D O)

Descriptor readiness is protocol state, not an unconditional host-ready bit.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.bindTcp {K U H D O R L T E Poll Host : Type} (h : ReadinessMachine.Hooks K U H D O) (descriptor : Descriptor O) (store : Store U R L T E) (readiness : Readiness.Hooks (MachineHooks.State K U) (Ref H D O)) (blocking : ReadinessMachine.BlockingStore U Poll) (base : TcpSocket.Hooks (MachineHooks.State K U) (Ref H D O) R L T E Poll Host) : TcpSocket.Hooks (MachineHooks.State K U) (Ref H D O) R L T E Poll Host

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.edgeBackend (hostOs : String) : Bool

Exact host cfg list selecting epoll/kqueue short-I/O readiness clearing.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.operations {O S H D E R L T P Host I : Type} (budget : Nat) (descriptor : Descriptor O) (virtual : VirtualSocket.Hooks S (Ref H D O) E) (tcp : TcpSocket.Hooks S (Ref H D O) R L T E P Host) (options : SocketOptions.Hooks S (Ref H D O) E I) : Socket.Operations S (Ref H D O) E

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.bindOptions {S F R L T E P H I : Type} (tcp : TcpSocket.Hooks S F R L T E P H) (base : SocketOptions.Hooks S F E I) : SocketOptions.Hooks S F E I

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.bindSocket {K U H D O R L T E P Host I : Type} (h : ReadinessMachine.Hooks K U H D O) (descriptor : Descriptor O) (store : Store U R L T E) (budget : Nat) (asUnix : Ref H D O → MachineHooks.M K U Unit) (virtual : VirtualSocket.Hooks (MachineHooks.State K U) (Ref H D O) E) (tcp : TcpSocket.Hooks (MachineHooks.State K U) (Ref H D O) R L T E P Host) (options : SocketOptions.Hooks (MachineHooks.State K U) (Ref H D O) E I) (base : Socket.Hooks (MachineHooks.State K U) (Ref H D O) E I) : Socket.Hooks (MachineHooks.State K U) (Ref H D O) E I

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.bindFiles {O S H D E R L T Poll Host HM : Type} (budget : Nat) (descriptor : Descriptor O) (virtual : VirtualSocket.Hooks S (Ref H D O) E) (tcp : TcpSocket.Hooks S (Ref H D O) R L T E Poll Host) (base : Files.Hooks S H D O E HM) : Files.Hooks S H D O E HM

Source FileDescription::read/write route also supports virtual pipe ends; only send/recv go through checked as_socket. Other payloads delegate unchanged.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.bindDeadline {K U Host System F R L T E Poll Error : Type} (deadline : DeadlineMachine.Hooks K U Host System) (base : TcpSocket.Hooks (MachineHooks.State K U) F R L T E Poll Error) : TcpSocket.Hooks (MachineHooks.State K U) F R L T E Poll Error

Actual monotonic clock and typed registry for nonblocking "now" probes and relative read/write timeouts; no Nat timestamp approximation.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.bindRawMemory {K U F E R L T P H : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K U) (arithmetic : Memory.PointerArithmetic) (virtual : VirtualSocket.Hooks (MachineHooks.State K U) F E) (tcp : TcpSocket.Hooks (MachineHooks.State K U) F R L T E P H) : VirtualSocket.Hooks (MachineHooks.State K U) F E × TcpSocket.Hooks (MachineHooks.State K U) F R L T E P H

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.bind {K U H D O R L T E Poll Host I : Type} (h : ReadinessMachine.Hooks K U H D O) (descriptor : Descriptor O) (store : Store U R L T E) (blocking : ReadinessMachine.BlockingStore U Poll) (budget : Nat) (asUnix : Ref H D O → MachineHooks.M K U Unit) (baseVirtual : VirtualSocket.Hooks (MachineHooks.State K U) (Ref H D O) E) (baseTcp : TcpSocket.Hooks (MachineHooks.State K U) (Ref H D O) R L T E Poll Host) (options : SocketOptions.Hooks (MachineHooks.State K U) (Ref H D O) E I) (socket : Socket.Hooks (MachineHooks.State K U) (Ref H D O) E I) : VirtualSocket.Hooks (MachineHooks.State K U) (Ref H D O) E × TcpSocket.Hooks (MachineHooks.State K U) (Ref H D O) R L T E Poll Host × Socket.Hooks (MachineHooks.State K U) (Ref H D O) E I

Final authoritative registry composition; compiler/memory/host leaves from base remain required. Both socket kinds share the same ownership/readiness view.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.bindFullStacks {K U F E R L T Poll Host : Type} (virtual : VirtualSocket.Hooks (ThreadStacks.State K U) F E) (tcp : TcpSocket.Hooks (ThreadStacks.State K U) F R L T E Poll Host) : VirtualSocket.Hooks (ThreadStacks.State K U) F E × TcpSocket.Hooks (ThreadStacks.State K U) F R L T E Poll Host

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.bindAddress {K U D MD B Inst E I : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K U) (arithmetic : Memory.PointerArithmetic) (memory : MemoryShims.Hooks Memory.Provenance (MachineHooks.State K U) D MD B Inst) (budget : Nat) (base : SocketAddress.Hooks (MachineHooks.State K U) E I) : SocketAddress.Hooks (MachineHooks.State K U) E I

Address byte accesses and temporary-buffer copies reuse actual shared memory operations. Compiler allocation, pointer views and field projections stay typed.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.SocketMachine.bindTimeval {S Host System Zone Stamp F E I : Type} (time : TimeShims.Hooks S Host System Zone Stamp) (base : SocketOptions.Hooks S F E I) : SocketOptions.Hooks S F E I

Equations

• One or more equations did not get rendered due to their size.