def Miri.Input.EvalCallbackSocketConstruction.otherFileEffects {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type} (seed : RegistrySeed Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (event : Interpreter.EventFd.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))) (socket : Option (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)) (retryBudget : Nat) (errorFromKind : Interpreter.IoError.ErrorKind → EStateM Interpreter.StepError (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.IoError.Error Error)) : EvalUnixIoConstruction.OtherFileEffects (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

Bind source OtherFileEffects after the canonical registry and eventfd callback have been created. Eventfd uses the real event store, retry and async finish semantics. The optional socket route must itself come from the source socket constructor; absent routes fail only when a tagged socket operation is requested. Other payloads retain the source's nonblocking/nonterminal defaults.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.otherPositionalEffects {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type} (seed : RegistrySeed Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) : EvalUnixNativeFdConstruction.OtherPositionalEffects (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

Pinned UnixFileDescription's default pread/pwrite arms throw Unsupported. The source currently has no implementations for eventfd or sockets, so retain that operation-local behavior.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.socketDescriptor (Raw Listener TcpStream Error : Type) : Interpreter.SocketMachine.Descriptor (Other Raw Listener TcpStream Error)

Canonical source tags; these remain valid even while optional socket operations are unavailable.

Equations

• Miri.Input.EvalCallbackSocketConstruction.socketDescriptor Raw Listener TcpStream Error = Miri.Interpreter.SourceOther.sockets

def Miri.Input.EvalCallbackSocketConstruction.eventPhysicalFromSeed {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C : Type} (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))) (wakeBudget : Nat) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (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) (choice : C) (libcI32 : String → EStateM Interpreter.StepError (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Int32) (u64Layout : EStateM Interpreter.StepError (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Interpreter.LocalLayout) : Interpreter.EventFd.PhysicalHooks (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))

Construct eventfd's physical hooks directly from the pre-poll registry seed. The passed physicalReadiness is the poll/readiness operation object being assembled for this same source call; descriptor ownership and event state still use the seed's canonical registries.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.blockingFromSeed {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error AddrIter : Type} (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) : 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 around the same early readiness seed. physicalReadiness is supplied only after the caller has constructed the current poll readiness operations; all persistent tables and TCP readiness state remain canonical.

Equations

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

def Miri.Input.EvalCallbackSocketConstruction.registrySeed {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type} (hostUsizeBits fileReferenceBudget watcherReferenceBudget : Nat) (resources : EvalUnixIoConstruction.FileResourceEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)) : RegistrySeed Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error

Build the one canonical descriptor/ownership/readiness registry before poll and source OtherFileEffects exist. The seed is only the persistent registry plus its real last-drop cleanup; it creates no partial Files or readiness operation dictionary. Core can later attach physical readiness and source event/socket methods to these same views.

Equations

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