Canonical callback assembly over the initialized EvalWorld. Main/TLS owns the thread hook, live backend Effects select the owned IO runtime, and socket bindings are built from their physical/source operations. Callers never supply a completed EvalCallbackMachine.Hooks.

@[reducible, inline]

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

Equations

• Miri.Input.EvalCallbackSourceConstruction.World = Miri.Input.EvalCallbackMachine.World

@[reducible, inline]

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

Equations

• Miri.Input.EvalCallbackSourceConstruction.State = Miri.Input.EvalCallbackMachine.State

@[reducible, inline]

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

Equations

• Miri.Input.EvalCallbackSourceConstruction.Inner = Miri.Input.EvalCallbackMachine.Inner

@[reducible, inline]

abbrev Miri.Input.EvalCallbackSourceConstruction.User (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.EvalCallbackSourceConstruction.FD (H D O : Type) : Type

Equations

• Miri.Input.EvalCallbackSourceConstruction.FD = Miri.Input.EvalCallbackMachine.FD

Physical operations used by the canonical owned event/poll/epoll constructor. Effects are source OS/synchronization writes; no guest-memory access or callback storage is supplied here.

structure Miri.Input.EvalCallbackSourceConstruction.IoOperations (Os R P H D O Aff B Poll Instant System Native Profiler E Iter Meta : Type) : Type

• effects : Interpreter.TypedSyncMachine.Effects (Inner Os R P H D O Aff B Poll Instant System Native Profiler)
• event : Interpreter.EventFd.PhysicalHooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O)
• poll : Interpreter.PollShims.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) Iter
• epoll : Interpreter.EpollShims.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) Iter
• vector : Interpreter.UnixVectored.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) H D O E Meta
• wakeBudget : Nat

Source policy inputs for the owned socket state machine. These are the primitive stores, physical source operations, and protocol semantics consumed by EvalOwnedIoMachine.prepareSockets; the resulting SocketBindings record is never selected by the caller.

structure Miri.Input.EvalCallbackSourceConstruction.SocketOperations (Os R P H D O Aff B Poll Instant System Native Profiler Raw Listener TcpStream Host E AddrIter : Type) : Type

• machine : Interpreter.ReadinessMachine.Hooks Memory.MiriMemoryKind (EvalOwnedIoMachine.User Os R P H D O Aff B Poll Instant System Native Profiler) H D O
• store : Interpreter.SocketMachine.Store (EvalOwnedIoMachine.User Os R P H D O Aff B Poll Instant System Native Profiler) Raw Listener TcpStream E
• blocking : Interpreter.ReadinessMachine.BlockingStore (EvalOwnedIoMachine.User Os R P H D O Aff B Poll Instant System Native Profiler) Poll
• asUnix : FD H D O → EStateM Interpreter.StepError (Inner Os R P H D O Aff B Poll Instant System Native Profiler) Unit
• virtual : Interpreter.VirtualSocket.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E
• tcp : Interpreter.TcpSocket.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) Raw Listener TcpStream E Poll Host
• options : Interpreter.SocketOptions.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E AddrIter
• socket : Interpreter.Socket.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) (FD H D O) E AddrIter
• finish : Interpreter.OwnedSocketCompletion.Hooks (Inner Os R P H D O Aff B Poll Instant System Native Profiler) E AddrIter

structure Miri.Input.EvalCallbackSourceConstruction.Components (Os R P H D O Aff B Poll Instant System Native Profiler C Z T E Iter Meta Raw Listener TcpStream Host AddrIter : Type) : Type

• 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 : IoOperations Os R P H D O Aff B Poll Instant System Native Profiler E Iter Meta
• sockets : SocketOperations Os R P H D O Aff B Poll Instant System Native Profiler Raw Listener TcpStream Host E AddrIter
• descriptor : Interpreter.SocketMachine.Descriptor O
• nestedCapacity : Nat
• synchronousResource : Nat

def Miri.Input.EvalCallbackSourceConstruction.fromSource {Os R P H D O Aff B Poll Instant System Native Profiler C TyId Z T E Iter Meta Raw Listener TcpStream Host AddrIter : Type} (main : Interpreter.MainMachine.Hooks (User Os R P H D O Aff B Poll Instant System Native Profiler) C O ABI.ExternAbi (ABI.FnAbi TyId) (ABI.ArgAbi TyId) Aff P) (components : Components Os R P H D O Aff B Poll Instant System Native Profiler C Z T E Iter Meta Raw Listener TcpStream Host AddrIter) (state : State Os R P H D O Aff B Poll Instant System Native Profiler) : Except (Interpreter.StepError × State Os R P H D O Aff B Poll Instant System Native Profiler) (EvalCallbackMachine.Hooks Os R P H D O Aff B Poll Instant System Native Profiler C ABI.ExternAbi (ABI.FnAbi TyId) (ABI.ArgAbi TyId) Z T E Iter Raw Listener TcpStream Host AddrIter × State Os R P H D O Aff B Poll Instant System Native Profiler)

Build and return source callbacks with the exact post-construction state. EStateM itself cannot carry the higher-universe callback dictionary, so the factory runs the existing IO source constructor explicitly and returns both its real state prefix and the assembled Hooks. On an error the updated state is returned alongside the error, preserving source effects.

Equations

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