Canonical final SourceOther representation and actual HostRuntime socket state. Decoder checks are explicit: malformed state tags are never silently filtered away. The final factory does not accept a replaceable Any embedding.

@[reducible, inline]

abbrev Miri.Input.EvalSocketStorage.Other (Raw Listener Stream Error : Type) : Type

Equations

• Miri.Input.EvalSocketStorage.Other = Miri.Interpreter.SourceOther.Value

@[reducible, inline]

abbrev Miri.Input.EvalSocketStorage.World (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalSocketStorage.User (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalSocketStorage.State (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

def Miri.Input.EvalSocketStorage.sockets {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type} : Interpreter.SocketMachine.Store (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Raw Listener TcpStream Error

Equations

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

def Miri.Input.EvalSocketStorage.blocking {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type} : Interpreter.ReadinessMachine.BlockingStore (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Poll

Equations

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

def Miri.Input.EvalSocketStorage.files {H D Raw Listener TcpStream Error Os R P Aff B Poll Instant System Native Profiler : Type} (hostUsizeBits referenceBudget : Nat) (onLastDrop : Interpreter.Files.Description H D (Other Raw Listener TcpStream Error) → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit) : Interpreter.FileMachine.Hooks Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)

Actual source FD table and strong ownership, without a duplicate table.

Equations

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

def Miri.Input.EvalSocketStorage.readiness {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type} (files : Interpreter.FileMachine.Hooks Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)) (watcherReferenceBudget : Nat) (onLastDrop : Interpreter.Files.Ref (Interpreter.Files.Description H D (Other Raw Listener TcpStream Error)) → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit) : Interpreter.ReadinessMachine.Hooks Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)

Equations

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