Source-built TCP, socket-option, virtual socket, and socket syscall policy over the canonical callback registry and EvalWorld context.

def Miri.Input.EvalCallbackSocketConstruction.virtualFromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (seed : RegistrySeed Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (physicalReadiness : Interpreter.Readiness.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error))) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (arithmetic : Memory.PointerArithmetic) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (choice : C) (errors : Interpreter.IoError.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error) (wakeBudget : Nat) : Except Interpreter.StepError (Interpreter.VirtualSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Error)

Source-backed virtual socket/pipe policy. State, descriptor allocation, readiness registration, guest bytes, target constants, and pointer projections are all taken from the selected compiler and final EvalWorld. The ioctl vararg is intentionally a demand-local residual until ForeignContext exposes the actual call-site varargs.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.virtualFileEffects {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type} (budget : Nat) (virtual : Interpreter.VirtualSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Error) : SocketFileEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error

Exact FileDescription read/write/readiness route for the source virtual socketpair and pipe family. TCP references remain Unsupported until their host-backed state builder is attached.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.tcpFromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error AddrIter : Type} (p : CompilerProviders.Prepared) (seed : RegistrySeed Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (physicalReadiness : Interpreter.Readiness.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error))) (blocking : Interpreter.BlockingIo.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Poll Error) (host : HostEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Raw Listener TcpStream Error Poll AddrIter) (errors : Interpreter.IoError.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error) (hostWindows : Bool) (virtual : Interpreter.VirtualSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Error) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (arithmetic : Memory.PointerArithmetic) (wakeBudget : Nat) : Except Interpreter.StepError (Interpreter.TcpSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Raw Listener TcpStream Error Poll Error)

Construct TCP protocol hooks from the canonical file/readiness registry, blocking source manager, compiler target and real host socket operations. The host profile fact hostWindows comes from the runtime host configuration; target OS remains the prepared compiler fact.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.protocolsFromSeed {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error AddrIter C : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (seed : RegistrySeed Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (physicalReadiness : Interpreter.Readiness.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error))) (blocking : Interpreter.BlockingIo.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Poll Error) (host : HostEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Raw Listener TcpStream Error Poll AddrIter) (errors : Interpreter.IoError.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error) (hostWindows : Bool) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (arithmetic : Memory.PointerArithmetic) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (choice : C) (wakeBudget : Nat) : Except Interpreter.StepError (Interpreter.VirtualSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Error × Interpreter.TcpSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Raw Listener TcpStream Error Poll Error)

Construct the two source-owned socket protocols together, preventing a caller from pairing TCP state with a virtual/readiness view from another EvalWorld.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.socketFileEffects {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type} (budget : Nat) (virtual : Interpreter.VirtualSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Error) (tcp : Interpreter.TcpSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Raw Listener TcpStream Error Poll Error) : SocketFileEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error

FileDescription operation hooks for both source socket protocols. The TCP route retains communicate and async finish; virtual pipes/socketpairs use their owned buffer callback path.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.completionFromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Metadata AddrIter : Type} (vector : Interpreter.UnixVectored.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Metadata) (address : Interpreter.SocketAddress.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error AddrIter) (pointerSize : ABI.Size) : Interpreter.OwnedSocketCompletion.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error AddrIter

Source completion rules reuse the canonical vectored-file completion operations and the same compiler-backed socket address hooks.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.optionsFromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error AddrIter : Type} (p : CompilerProviders.Prepared) (address : Interpreter.SocketAddress.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error AddrIter) (host : HostEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Raw Listener TcpStream Error Poll AddrIter) (tcp : Interpreter.TcpSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Raw Listener TcpStream Error Poll Error) : Except Interpreter.StepError (Interpreter.SocketOptions.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Error AddrIter)

Construct socket-option operations from compiler libc layouts, the same source address-memory hooks, TCP-owned timeout/SO_ERROR state, and true host SockRef option effects.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.socketFromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error AddrIter : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (seed : RegistrySeed Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (virtual : Interpreter.VirtualSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Error) (tcp : Interpreter.TcpSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Raw Listener TcpStream Error Poll Error) (options : Interpreter.SocketOptions.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Error AddrIter) (address : Interpreter.SocketAddress.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error AddrIter) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (asUnix : FD H D (Other Raw Listener TcpStream Error) → EStateM Interpreter.StepError (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit) (communicate : Bool) (isolationReject : String → EStateM Interpreter.StepError (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Bool) (budget : Nat) : Except Interpreter.StepError (Interpreter.Socket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Error AddrIter)

Full Unix socket syscall hooks from the source-owned virtual/TCP protocols, options, canonical descriptor ownership, and address-memory constructor.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.socketOperationsFromProtocols {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error AddrIter Metadata : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (seed : RegistrySeed Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (virtual : Interpreter.VirtualSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Error) (tcp : Interpreter.TcpSocket.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Raw Listener TcpStream Error Poll Error) (host : HostEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Raw Listener TcpStream Error Poll AddrIter) (address : Interpreter.SocketAddress.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error AddrIter) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (asUnix : FD H D (Other Raw Listener TcpStream Error) → EStateM Interpreter.StepError (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit) (communicate : Bool) (isolationReject : String → EStateM Interpreter.StepError (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Bool) (budget : Nat) (vector : Interpreter.UnixVectored.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Metadata) : Except Interpreter.StepError (EvalCallbackSourceConstruction.SocketOperations Os R P H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Error AddrIter)

Assemble final socket operations around protocols already built from the canonical registry. This separates protocol construction from the vectored completion dependency so a caller can reuse one protocol/store instance while obtaining completion hooks from the native-FD source constructor. No socket registry or host socket state is allocated here.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.sourceSocketOperations {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error AddrIter C Metadata : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (seed : RegistrySeed Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (physicalReadiness : Interpreter.Readiness.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error))) (host : HostEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Raw Listener TcpStream Error Poll AddrIter) (errors : Interpreter.IoError.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error) (hostWindows : Bool) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (arithmetic : Memory.PointerArithmetic) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (choice : C) (wakeBudget socketBudget : Nat) (address : Interpreter.SocketAddress.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error AddrIter) (asUnix : FD H D (Other Raw Listener TcpStream Error) → EStateM Interpreter.StepError (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit) (communicate : Bool) (isolationReject : String → EStateM Interpreter.StepError (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Bool) (vector : Interpreter.UnixVectored.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Metadata) : Except Interpreter.StepError (EvalCallbackSourceConstruction.SocketOperations Os R P H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Error AddrIter)

Build the callback's complete socket operations from one source context. This is the handoff constructor for the ordinary callback assembly: no SocketOperations, VirtualSocket.Hooks, TcpSocket.Hooks, SocketOptions, or Socket.Hooks record is caller-selected.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.blockingFromDispatch {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path Place C ClockHost I AddrIter : Type} (dispatch : EvalUnixSourceConstruction.DispatchComponents Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path Place C ClockHost I) (host : HostEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Raw Listener TcpStream Error Poll AddrIter) : Interpreter.BlockingIo.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Poll Error

Build BlockingIo over the same readiness registry and file ownership as the Unix FD dispatcher. The source readiness cell belongs to canonical TCP socket state; it is read and updated by descriptor identity, never by a second caller-supplied table.

Equations

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