One concrete source FnOnce dispatcher. Scheduling and deadline wrappers select the actual target thread before invoking this interpreter. Main/TLS are FnMut stack-empty callbacks and use MainMachine.take/invoke/restore instead. No missing-token fallback or function-valued registry is accepted here.

@[reducible, inline]

abbrev Miri.Input.EvalCallbackMachine.World (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

• Miri.Input.EvalCallbackMachine.World = Miri.Input.EvalOwnedIoMachine.World

@[reducible, inline]

abbrev Miri.Input.EvalCallbackMachine.State (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

• Miri.Input.EvalCallbackMachine.State = Miri.Input.EvalForeignIoMachine.State

@[reducible, inline]

abbrev Miri.Input.EvalCallbackMachine.Inner (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

• Miri.Input.EvalCallbackMachine.Inner = Miri.Input.EvalOwnedIoMachine.State

@[reducible, inline]

abbrev Miri.Input.EvalCallbackMachine.ThreadUser (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

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

@[reducible, inline]

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

Equations

• Miri.Input.EvalCallbackMachine.FD = Miri.Input.EvalOwnedIoMachine.FD

structure Miri.Input.EvalCallbackMachine.Hooks (Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter : Type) : Type 1

• thread : Interpreter.ThreadMachine.Hooks Memory.MiriMemoryKind (ThreadUser Os R P H D O Aff B Poll Instant System Native Profiler) C O X F A Aff
• futex : Option (Interpreter.LinuxFutexMachine.Hooks Memory.MiriMemoryKind (World Os R P H D O Aff B Poll Instant System Native Profiler) C P O B Instant System Z T E)
• io : EvalOwnedIoMachine.Bindings (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Iter
• socket : EvalOwnedIoMachine.SocketBindings (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E Raw Listener TcpStream Poll Host AddrIter
• descriptor : Interpreter.SocketMachine.Descriptor O
• options : Interpreter.SocketOptions.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E AddrIter
• wakeBudget : Nat
• nestedCapacity : Nat
• synchronousResource : Nat
• deadlineRegistry : Interpreter.ThreadStacks.Storage (ThreadUser Os R P H D O Aff B Poll Instant System Native Profiler) → Interpreter.DeadlineMachine.Registry Instant System

  Registry projections let callback execution suppress pruning until its complete nested callback chain has returned.

• setDeadlineRegistry : Interpreter.DeadlineMachine.Registry Instant System → Interpreter.ThreadStacks.Storage (ThreadUser Os R P H D O Aff B Poll Instant System Native Profiler) → Interpreter.ThreadStacks.Storage (ThreadUser Os R P H D O Aff B Poll Instant System Native Profiler)

def Miri.Input.EvalCallbackMachine.prepare {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter : Type} (h : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter

Concrete source-owned final dictionary factory. Nested execution capacity belongs only to this transient execution dictionary, never deferred source data. All event/poll/epoll/socket bodies are reconstructed after routing readiness.

Equations

• Miri.Input.EvalCallbackMachine.prepare h choice = Miri.Input.EvalCallbackMachine.routeSource✝ h (Miri.Input.EvalCallbackMachine.runWithin✝ h.nestedCapacity h choice)

def Miri.Input.EvalCallbackMachine.blockingIoGc {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter : Type} (h : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Unit

Source blocking-I/O weak-source GC reads the prepared canonical manager; callbacks are not extra provenance roots in the pinned thread visitor.

Equations

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

def Miri.Input.EvalCallbackMachine.invoke {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter : Type} (h : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) (token : Nat) (kind : Concurrency.UnblockKind) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Unit

Equations

• Miri.Input.EvalCallbackMachine.invoke h choice token kind = Miri.Input.EvalCallbackMachine.runWithin✝ h.nestedCapacity h choice token kind

def Miri.Input.EvalCallbackMachine.invokeInner {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter : Type} (h : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) (token : Nat) (kind : Concurrency.UnblockKind) : EStateM Interpreter.StepError (Inner Os R P H D O Aff B Poll Instant System Native Profiler) Unit

Equations

• Miri.Input.EvalCallbackMachine.invokeInner h choice token kind = Miri.Interpreter.ExecutionStateTransport.reverseAction (Miri.Input.EvalCallbackMachine.invoke h choice token kind)

def Miri.Input.EvalCallbackMachine.innerReadiness {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter Fd : Type} (h : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) (base : Interpreter.Readiness.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) Fd) : EStateM Interpreter.StepError (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (Interpreter.Readiness.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) Fd)

Source physical IO dictionaries are constructed on Inner; wake callbacks still perform the complete outer ThreadStacks switch on the same state.

Equations

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

def Miri.Input.EvalCallbackMachine.runtime {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter Ref V Dest : Type} (h : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) (base : Concurrency.SyncRuntime.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Ref V Dest) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Concurrency.SyncRuntime.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Ref V Dest)

Registration/cancellation retain their exact source arena; execution of a selected token uses the full dispatcher, including IO callbacks. Production factories call this on their already typed runtime before binding wake helpers.

Equations

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

def Miri.Input.EvalCallbackMachine.readiness {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter Fd : Type} (h : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) (base : Interpreter.Readiness.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Fd) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Interpreter.Readiness.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Fd)

Uses the full ThreadStacks switch and restores only after successful source callback execution. A callback error retains the selected target and prefix.

Equations

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

def Miri.Input.EvalCallbackMachine.event {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter Fd : Type} (h : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) (wakeBudget : Nat) (ready : Interpreter.Readiness.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Fd) (base : Interpreter.EventFd.PhysicalHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Fd) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Interpreter.EventFd.PhysicalHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Fd)

Canonical source eventfd physical effects close over the routed readiness view, including readiness wakes caused from another callback.

Equations

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

def Miri.Input.EvalCallbackMachine.blocking {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter Fd HostEffect : Type} (h : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) (base : Interpreter.BlockingIo.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Fd Poll HostEffect) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Interpreter.BlockingIo.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Fd Poll HostEffect)

Equations

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

def Miri.Input.EvalCallbackMachine.scheduling {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter Fd HostEffect : Type} (h : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) (wakeBudget : Nat) (io : Interpreter.BlockingIo.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Fd Poll HostEffect) (base : Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (ThreadUser Os R P H D O Aff B Poll Instant System Native Profiler)) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (ThreadUser Os R P H D O Aff B Poll Instant System Native Profiler))

The RunLoop scheduler's delayed readiness and host polling use the same routed wake operation as deadlines and synchronous descriptor operations.

Equations

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

def Miri.Input.EvalCallbackMachine.deadlines {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter : Type} (h : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) (clock : Interpreter.Clock.HostHooks Instant System (State Os R P H D O Aff B Poll Instant System Native Profiler)) (communicate : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Bool) (durationSince : System → System → EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Option Interpreter.Clock.Duration)) : Interpreter.DeadlineMachine.Hooks Memory.MiriMemoryKind (EvalHostMachine.User Os R P H D O Aff B Poll Instant System Native Profiler) Instant System

Deadline execution uses the same terminal dispatcher; no separate timeout callback table, token supply, host clock or thread selection is introduced.

Equations

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

def Miri.Input.EvalCallbackMachine.unix {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter HM Place Time Kind ReadDir DirEntry Duration TZ Timestamp Block Instance : Type} (prepared : CompilerProviders.Prepared) (callbacks : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) (tag : Interpreter.Files.FdId → O) (untag : O → Option Interpreter.Files.FdId) (sourceFiles : Interpreter.Files.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) H D O E HM) (objects : Interpreter.ForeignSyncMachine.Objects (State Os R P H D O Aff B Poll Instant System Native Profiler)) (foreign : Interpreter.UnixForeign.Hooks (State Os R P H D O Aff B Poll Instant System Native Profiler) Place H D O Os HM Time E Kind ReadDir DirEntry Concurrency.TypedSyncRuntime.Ref Duration Iter AddrIter Instant System TZ Timestamp Block Instance) (base : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Poll Instant System Native Profiler) Place Concurrency.TypedSyncRuntime.Dest (Memory.Pointer (Option Memory.Provenance)) Block Instance) : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Interpreter.ForeignItems.Hooks Memory.Provenance (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (EvalSyncMachine.World Os R P H D O Aff B Poll Instant System Native Profiler))) Place (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Block Instance)

Final Unix dictionary is assembled from the prepared source-owned IO and socket bodies. Runtime replacement happens before UnixForeign.bind captures any handler, and entry polling uses the exact routed BlockingIo source body.

Equations

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

def Miri.Input.EvalCallbackMachine.factory {Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter : Type} (prepared : CompilerProviders.Prepared) (h : Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter) (choice : C) (clock : Interpreter.Clock.HostHooks Instant System (State Os R P H D O Aff B Poll Instant System Native Profiler)) (communicate : EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) Bool) (durationSince : System → System → EStateM Interpreter.StepError (State Os R P H D O Aff B Poll Instant System Native Profiler) (Option Interpreter.Clock.Duration)) (base : Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (ThreadUser Os R P H D O Aff B Poll Instant System Native Profiler)) : Except Interpreter.StepError (Hooks Os R P H D O Aff B Poll Instant System Native Profiler C X F A Z T E Iter Raw Listener TcpStream Host AddrIter × Interpreter.DeadlineMachine.Hooks Memory.MiriMemoryKind (EvalHostMachine.User Os R P H D O Aff B Poll Instant System Native Profiler) Instant System × Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (ThreadUser Os R P H D O Aff B Poll Instant System Native Profiler))

Source-owned final execution assembly. The genuine host clock and choice leaves stay explicit; no caller callback dispatcher or baseline wake execution is accepted. Scheduling, deadlines and the exported callback dictionaries all refer to the same finite nested-execution interpreter.

Equations

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