Narrow source-runner host residuals. This module contains host operations only: it does not accept a Core, compiler-derived dispatch, Main hooks, guest memory policy, or completed callback dictionaries. Source algorithms and canonical state projections are assembled by the invocation-time Core.

structure Miri.Input.EvalSourceHostEffects.Native (S : Type) : Type

Only the true native-library and OS-error host effects are retained here. The active native-library path list is read from HostRuntime by Core.

• call : String → Interpreter.MPlaceTy Memory.Provenance → Array (Interpreter.OpTy Memory.Provenance) → EStateM Interpreter.StepError S Bool

structure Miri.Input.EvalSourceHostEffects.Process (S : Type) : Type

Process-global interrupt and abnormal-cleanup capabilities used by the source loop. Kept local so this seed does not import the runner.

• interrupted : S → Bool
• handleAbnormalTermination : S → S

structure Miri.Input.EvalSourceHostEffects.Filesystem (Os SourceState H D O Path Meta System Error R : Type) : Type 1

Optional raw host filesystem operations for the pinned Unix source family. The directory iterator entry type is existential and remains a transient host value; the actual rooted directory table uses the existing runtime R.

• Entry : Type
• pathFromOs : Os → Path

  Convert the host OS-string representation to the host path carrier used by the raw filesystem leaves.

• osFromPath : Path → Os
• effects : EvalUnixFsConstruction.HostEffects SourceState H D O Path Meta System Error R self.Entry
• absolute : Option (Path → EStateM Interpreter.StepError SourceState (Except (Interpreter.IoError.HostError Error) Path))

  Raw std::path::absolute result for host paths. Windows file shims need this for GetFullPathNameW; when absent, that operation remains demand-local Unsupported. This is deliberately not synthesized from cwd or canonicalization.

structure Miri.Input.EvalSourceHostEffects.TimeSource (Os SourceState : Type) : Type 1

Raw host chrono/database operations for the pinned time shims. Timezone selection still comes from the guest environment; timezoneString is only the host's OsString::into_string conversion. Zone and timestamp types are packed existentially so source packages can carry the real host representation.

• Zone : Type
• Timestamp : Type
• timezoneString : Os → Except Unit String
• effects : EvalTimeConstruction.HostEffects SourceState self.Zone self.Timestamp

structure Miri.Input.EvalSourceHostEffects.Seed (Os R EnvControl SourceState H D O Aff B Raw Listener TcpStream Error ErrorHost Meta Path Poll AddrIter Instant System NativeHandle Profiler RunState : Type) : Type 1

Host-residual seed shared by the source Core, startup, Unix dispatch, and runner. The independent state parameters are unified by Core at the final callsite; this record does not snapshot or manufacture those states.

• hostOverflowChecks : Bool

  Whether this Miri host build enables Rust overflow checks for ordinary additions in iovec length accumulation. This is a native build-profile fact, not a guest target property: callers provide it for the pinned Miri executable/profile. The repository's reference target/debug/miri is built with Cargo's development profile, whose default enables overflow checks; pinned cargo-miri/src/setup.rs also explicitly keeps them enabled for the Miri sysroot with -Coverflow-checks=on. Other host builds must pass their actual profile setting.

• os : EvalHostRuntimeConstruction.OsHostEffects Os
• environment : EvalHostRuntimeConstruction.EnvironmentHostEffects EnvControl
• unixConfig : EvalUnixConstruction.HostConfigEffects SourceState Os Error
• ioError : EvalUnixConstruction.IoHostEffects SourceState Error
• native : Native SourceState
• openFiles : EvalUnixNativeFdConstruction.OpenHostEffects SourceState H D Error Meta Path Os
• fileResources : EvalUnixIoConstruction.FileResourceEffects SourceState H D O
• hostFiles : EvalUnixIoConstruction.HostFileEffects SourceState H D O Error Meta
• getrandom : Option (Nat → EStateM Interpreter.StepError SourceState (Except String ByteArray))

  Raw host getrandom::fill result used only when Miri communicates with its host. Isolated execution continues to draw bytes from the guest choice tape. Absence remains a demand-local Unsupported result at the random shim.

• fileLocks : EvalUnixIoConstruction.FileLockEffects SourceState H Error
• positional : EvalUnixNativeFdConstruction.OtherPositionalEffects SourceState H D O Error
• control : EvalUnixIoConstruction.ControlSourceEffects SourceState
• filesystem : Option (Filesystem Os SourceState H D O Path Meta System Error R)

  Absent host filesystem support leaves Unix filesystem names as explicit demand-local Unsupported results.

• time : Option (TimeSource Os SourceState)

  Absent chrono/database support remains an explicit demand-local gap.

• socket : EvalCallbackSocketConstruction.HostEffects SourceState H D O Raw Listener TcpStream Error Poll AddrIter
• sync : EvalCallbackSyncConstruction.HostEffects Os R H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B Poll Instant System NativeHandle Profiler ErrorHost
• clock : Interpreter.Clock.HostHooks Instant System RunState
• systemDurationSince : System → System → EStateM Interpreter.StepError RunState (Option Interpreter.Clock.Duration)
• process : Process RunState