Callback operations reused from the canonical Unix source dispatchers. This module owns the structural binding: poll/epoll, vectored IO, descriptor identity, readiness and event storage are taken from one DispatchComponents bundle. Only the backend-selected typed-sync scalar/write effects and resource bound remain supplied by the enclosing source runner.

@[reducible, inline]

abbrev Miri.Input.EvalCallbackOperationConstruction.Other (Raw Listener TcpStream Error : Type) : Type

Equations

• Miri.Input.EvalCallbackOperationConstruction.Other Raw Listener TcpStream Error = Miri.Input.EvalSocketStorage.Other Raw Listener TcpStream Error

@[reducible, inline]

abbrev Miri.Input.EvalCallbackOperationConstruction.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.EvalCallbackOperationConstruction.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.

@[reducible, inline]

abbrev Miri.Input.EvalCallbackOperationConstruction.FD (H D O : Type) : Type

Equations

• Miri.Input.EvalCallbackOperationConstruction.FD H D O = Miri.Interpreter.Files.Ref (Miri.Interpreter.Files.Description H D O)

def Miri.Input.EvalCallbackOperationConstruction.sourceIoOperations {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path C ClockHost I : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (nativeFd : EvalUnixNativeFdConstruction.Components Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path MIR.Place C ClockHost I Interpreter.LoadedBody) (effects : Interpreter.TypedSyncMachine.Effects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalCoreMachine.Stored Os R P H D (Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler))) (accessConfig : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (EvalOwnedIoMachine.User Os R P H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) (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) (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) (unitLayout : Interpreter.LocalLayout) (readinessRoute : EvalUnixFdConstruction.ReadinessRoute (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (hostClock : Interpreter.Clock.HostHooks Instant System (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (errors : Interpreter.IoError.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error) (wakeBudget iterationBudget : Nat) : Except Interpreter.StepError (EvalCallbackSourceConstruction.IoOperations Os R P H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler Error EvalUnixFdConstruction.ArrayCursor Meta)

Assemble callback IO operations from the final source native-FD bundle. This is intentionally separate from the Unix dispatch bundle: callback poll and epoll must share the final Files/readiness registry and the same host deadline state, while their readiness route is the genuine source route.

Equations

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

def Miri.Input.EvalCallbackOperationConstruction.ioOperations {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path C ClockHost I : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (dispatch : EvalUnixSourceConstruction.DispatchComponents Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path MIR.Place C ClockHost I) (effects : Interpreter.TypedSyncMachine.Effects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (EvalOwnedIoMachine.User Os R P H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) (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) (wakeBudget : Nat) : Except Interpreter.StepError (EvalCallbackSourceConstruction.IoOperations Os R P H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler Error EvalUnixFdConstruction.ArrayCursor Meta)

Derive the callback IO primitives from the very same Unix dispatch bundle that Core installs for foreign calls. In particular, this does not accept a second poll or epoll ABI/readiness dictionary, a second vectored-memory dictionary, or an alternate event-FD tag/store. The caller provides only the active-backend-dependent typed-sync scalar effects and the callback resource bound.

Equations

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

def Miri.Input.EvalCallbackOperationConstruction.bindSocketState {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path 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 MIR.Place C ClockHost I) (base : 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) : 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

Replace every socket state/descriptor-owner operation in a socket seed by the canonical final EvalWorld sources. Protocol and genuine host operations remain those built by the socket source constructor; callers cannot install a parallel readiness registry, descriptor table, blocking store, or Unix downcast. The descriptor encoding is also fixed to SourceOther's exact tagged identity.

Equations

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

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

Equations

• Miri.Input.EvalCallbackOperationConstruction.descriptor Raw Listener TcpStream Error = Miri.Interpreter.SourceOther.sockets