Typed source host-owned machine.rs::new state. Host effects are required operations on an actual environment; isolated mode still creates then drops the poll object, while the clock uses the source virtual epoch. No closure arena is embedded recursively in its own machine state.

structure Miri.Input.HostRuntime.Storage (Poll Instant System H D O Native Profiler : Type) : Type

• blocking : Interpreter.BlockingIo.Manager Poll
• clock : Interpreter.Clock.Monotonic Instant
• deadlines : Interpreter.DeadlineMachine.Registry Instant System
• readiness : Interpreter.ReadinessMachine.Registry (Interpreter.Files.Ref (Interpreter.Files.Description H D O))
• futex : Concurrency.FutexRuntime.Storage (Interpreter.MPlaceTy Memory.Provenance)
• sync : Concurrency.TypedSyncRuntime.Storage
• io : Interpreter.OwnedIoStore.Storage (Interpreter.Files.Ref (Interpreter.Files.Description H D O))
• events : Array (Interpreter.Files.FdId × Interpreter.EventFd.Event)
• virtualSockets : Array (Interpreter.Files.FdId × Interpreter.VirtualSocket.State)
• tcpSockets : Array (Interpreter.Files.FdId × O)
• nativeLibraries : Array (String × Native)
• profiler : Option Profiler
• control : Interpreter.TerminatorControl.Counters

structure Miri.Input.HostRuntime.Configuration : Type

• communicate : Bool
• muteOutput : Bool
• hostUsizeBits : Nat
• profileOutput : Option String
• nativeLibraries : Array String
• hostTriple : String
• targetTriple : String
• nativeSupported : Bool
• control : Interpreter.TerminatorControl.Configuration

structure Miri.Input.HostRuntime.Hooks (S Poll Instant System Native Profiler : Type) : Type

• createProfiler : String → EStateM Interpreter.StepError S Profiler
• newPoll : EStateM Interpreter.StepError S Poll
• dropPoll : Poll → EStateM Interpreter.StepError S Unit
• hostClock : Interpreter.Clock.HostHooks Instant System S
• loadNative : String → EStateM Interpreter.StepError S Native
• dropNative : Native → EStateM Interpreter.StepError S Unit
• dropProfiler : Profiler → EStateM Interpreter.StepError S Unit

def Miri.Input.HostRuntime.create {S Poll Instant System Native Profiler H D O : Type} (h : Hooks S Poll Instant System Native Profiler) (config : Configuration) (beforePoll beforeDescriptors : EStateM Interpreter.StepError S Unit) : EStateM Interpreter.StepError S (Storage Poll Instant System H D O Native Profiler × Interpreter.Files.Table (Interpreter.Files.Description H D O) × Interpreter.FileOwnership.Registry (Interpreter.Files.Description H D O))

Equations

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

def Miri.Input.HostRuntime.create.load {S Poll Instant System Native Profiler : Type} (h : Hooks S Poll Instant System Native Profiler) (config : Configuration) (remaining : List String) : EStateM Interpreter.StepError S (Array (String × Native))

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.HostRuntime.create.load h config [] = pure #[]

def Miri.Input.HostRuntime.dispose {S Poll Instant System Native Profiler H D O : Type} (h : Hooks S Poll Instant System Native Profiler) (host : Storage Poll Instant System H D O Native Profiler) : EStateM Interpreter.StepError S Unit

Cleanup for a fully constructed host payload if later machine assembly fails.

Equations

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

def Miri.Input.HostRuntime.protect {S Poll Instant System Native Profiler H D O A : Type} (h : Hooks S Poll Instant System Native Profiler) (host : Storage Poll Instant System H D O Native Profiler) (action : EStateM Interpreter.StepError S A) : EStateM Interpreter.StepError S A

Equations

• Miri.Input.HostRuntime.protect h host action = Miri.Input.HostRuntime.onError✝ action (Miri.Input.HostRuntime.dispose h host)