Source-owned local scheduler/run-loop construction from the live World. The local scheduling policy, readiness service, deadlines, clock, active-stack callbacks and MIR step are assembled here; callers do not supply complete RunLoopHooks or LocalSchedulerHooks records. Only process interrupt observation and abnormal host cleanup remain explicit host operations.

@[reducible, inline]

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

Equations

• Miri.Input.EvalRunConstruction.W = Miri.Input.EvalCallbackMachine.World

@[reducible, inline]

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

Equations

• Miri.Input.EvalRunConstruction.User Os R P H D O Aff B Poll Instant System Native Profiler = Miri.Input.EvalCallbackMachine.ThreadUser Os R P H D O Aff B Poll Instant System Native Profiler

@[reducible, inline]

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

Equations

• Miri.Input.EvalRunConstruction.State Os R P H D O Aff B Poll Instant System Native Profiler = Miri.Input.EvalCallbackMachine.State Os R P H D O Aff B Poll Instant System Native Profiler

@[reducible, inline]

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

Equations

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

CTRL_C_RECEIVED is process-global in Rust, and abnormal profiler cleanup is an environment operation. Keep only these narrow residuals explicit.

structure Miri.Input.EvalRunConstruction.ProcessEffects (S : Type) : Type

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

Build the exact local scheduler branch. communicate is read from the same HostRuntime configuration used at startup. The routed IO hook, deadline registry, ThreadManager and ThreadStacks are all the live World instances.

def Miri.Input.EvalRunConstruction.scheduler {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} (configuration : HostRuntime.Configuration) (callbacks : 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) (choiceAccess : Interpreter.ExecutionChoices.Access (Interpreter.ThreadStacks.State Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler))) (clock : Interpreter.Clock.HostHooks Instant System (State Os R P H D O Aff B Poll Instant System Native Profiler)) (systemDurationSince : System → System → M Os R P H D O Aff B Poll Instant System Native Profiler (Option Interpreter.Clock.Duration)) : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler)

Equations

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

Construct a complete source loop. Main/TLS stack-empty callbacks, thread termination and MIR stepping use their established source machines; ThreadStacks.bindRunLoop adds source stack-switch synchronization. A finite choice tape is still a caller-side execution bound and must remain pending when exhausted; this hook record itself makes no completion claim.

def Miri.Input.EvalRunConstruction.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} (configuration : HostRuntime.Configuration) (callbacks : 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) (main : Interpreter.MainMachine.Hooks (User Os R P H D O Aff B Poll Instant System Native Profiler) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P) (configs : C → EvalExecutable.Core Os R P H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler) C Instant) (limits : Interpreter.ExecutionMachine.Limits) (choiceAccess : Interpreter.ExecutionChoices.Access (Interpreter.ThreadStacks.State Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler))) (clock : Interpreter.Clock.HostHooks Instant System (State Os R P H D O Aff B Poll Instant System Native Profiler)) (systemDurationSince : System → System → M Os R P H D O Aff B Poll Instant System Native Profiler (Option Interpreter.Clock.Duration)) (process : ProcessEffects (State Os R P H D O Aff B Poll Instant System Native Profiler)) : Interpreter.RunLoopHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) C Interpreter.MainMachine.Callback

Equations

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

Source Core construction is fallible because compiler and host facts are queried while building each choice-specific configuration. Preserve those failures at the step boundary; do not turn them into an arbitrary default ExecutionMachine.Config.

def Miri.Input.EvalRunConstruction.hooksFromSourceParts {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} (configuration : HostRuntime.Configuration) (callbacks : 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) (main : Interpreter.MainMachine.Hooks (User Os R P H D O Aff B Poll Instant System Native Profiler) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P) (configs : C → Except Interpreter.StepError (EvalExecutable.Core Os R P H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler) C Instant)) (limits : Interpreter.ExecutionMachine.Limits) (choiceAccess : Interpreter.ExecutionChoices.Access (Interpreter.ThreadStacks.State Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler))) (clock : Interpreter.Clock.HostHooks Instant System (State Os R P H D O Aff B Poll Instant System Native Profiler)) (systemDurationSince : System → System → M Os R P H D O Aff B Poll Instant System Native Profiler (Option Interpreter.Clock.Duration)) (process : ProcessEffects (State Os R P H D O Aff B Poll Instant System Native Profiler)) : Interpreter.RunLoopHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) C Interpreter.MainMachine.Callback × (C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler))

Equations

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

def Miri.Input.EvalRunConstruction.hooksFromSource {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} (configuration : HostRuntime.Configuration) (callbacks : 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) (main : Interpreter.MainMachine.Hooks (User Os R P H D O Aff B Poll Instant System Native Profiler) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P) (configs : C → Except Interpreter.StepError (EvalExecutable.Core Os R P H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler) C Instant)) (limits : Interpreter.ExecutionMachine.Limits) (choiceAccess : Interpreter.ExecutionChoices.Access (Interpreter.ThreadStacks.State Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler))) (clock : Interpreter.Clock.HostHooks Instant System (State Os R P H D O Aff B Poll Instant System Native Profiler)) (systemDurationSince : System → System → M Os R P H D O Aff B Poll Instant System Native Profiler (Option Interpreter.Clock.Duration)) (process : ProcessEffects (State Os R P H D O Aff B Poll Instant System Native Profiler)) : Interpreter.RunLoopHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) C Interpreter.WindowsExitMachine.Callback

Equations

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

Source startup can run main before constructing the optional callback protocol. This scheduler preserves the source's cheap branches: an enabled active thread returns before host polling, empty delayed/readiness and blocking registries take their actual empty branches, and no-deadline states do not read a clock. If execution reaches a branch that needs an unconnected physical poll, delayed readiness update, timed deadline, or host-source query, it returns Unsupported. It never treats a missing callback dictionary as an empty successful result.

def Miri.Input.EvalRunConstruction.hooksFromSourceWithoutCallbacks {Os R P H D O Aff B Poll Instant System Native Profiler C : Type} (configuration : HostRuntime.Configuration) (main : Interpreter.MainMachine.Hooks (User Os R P H D O Aff B Poll Instant System Native Profiler) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P) (configs : C → Except Interpreter.StepError (EvalExecutable.Core Os R P H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler) C Instant)) (limits : Interpreter.ExecutionMachine.Limits) (choiceAccess : Interpreter.ExecutionChoices.Access (Interpreter.ThreadStacks.State Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler))) (clock : Interpreter.Clock.HostHooks Instant System (State Os R P H D O Aff B Poll Instant System Native Profiler)) (systemDurationSince : System → System → M Os R P H D O Aff B Poll Instant System Native Profiler (Option Interpreter.Clock.Duration)) (process : ProcessEffects (State Os R P H D O Aff B Poll Instant System Native Profiler)) : Interpreter.RunLoopHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) C Interpreter.MainMachine.Callback

Equations

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

inductive Miri.Input.EvalRunConstruction.PendingCause : Type

• outerChoicesExhausted (iterations : Nat) : PendingCause
• iterationFuelExhausted (iterations : Nat) : PendingCause
• choiceTapeExhausted (iterations : Nat) : PendingCause
• sourceResourceExhausted (iterations : Nat) (error : Interpreter.StepError) : PendingCause

@[instance_reducible]

instance Miri.Input.EvalRunConstruction.instReprPendingCause : Repr PendingCause

Equations

• Miri.Input.EvalRunConstruction.instReprPendingCause = { reprPrec := Miri.Input.EvalRunConstruction.instReprPendingCause.repr }

def Miri.Input.EvalRunConstruction.instReprPendingCause.repr : PendingCause → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Input.EvalRunConstruction.instDecidableEqPendingCause : DecidableEq PendingCause

Equations

• Miri.Input.EvalRunConstruction.instDecidableEqPendingCause = Miri.Input.EvalRunConstruction.instDecidableEqPendingCause.decEq

def Miri.Input.EvalRunConstruction.instDecidableEqPendingCause.decEq (x✝ x✝¹ : PendingCause) : Decidable (x✝ = x✝¹)

Equations

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

A bounded process driver returns a status only for a source terminal outcome. Exhausting either external bound is explicitly pending/unknown.

inductive Miri.Input.EvalRunConstruction.RunResult (S : Type) : Type

• exited {S : Type} (state : S) (code : Int) (leakCheck : Bool) : RunResult S
• undefinedBehavior {S : Type} (state : S) (error : Interpreter.StepError) : RunResult S
• unsupported {S : Type} (state : S) (error : Interpreter.StepError) : RunResult S
• failed {S : Type} (state : S) (error : Interpreter.StepError) : RunResult S
• pending {S : Type} (state : S) (cause : PendingCause) : RunResult S

def Miri.Input.EvalRunConstruction.instReprRunResult.repr {S✝ : Type} [Repr S✝] : RunResult S✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Input.EvalRunConstruction.instReprRunResult {S✝ : Type} [Repr S✝] : Repr (RunResult S✝)

Equations

• Miri.Input.EvalRunConstruction.instReprRunResult = { reprPrec := Miri.Input.EvalRunConstruction.instReprRunResult.repr }

def Miri.Input.EvalRunConstruction.classifyError {S : Type} (state : S) (error : Interpreter.StepError) : RunResult S

Equations

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

def Miri.Input.EvalRunConstruction.observeProgress {Os R P H D O Aff B Poll Instant System Native Profiler : Type} (profile : Lean.Options) (boundary : String) (iteration : Nat) (state : State Os R P H D O Aff B Poll Instant System Native Profiler) : State Os R P H D O Aff B Poll Instant System Native Profiler

Profiling is an identity on the state, including failed prefixes. Log the first 64 iterations, then every 64th; the count is outer scheduler iterations, not MIR instructions. Labels are evaluated only with profiling enabled.

Equations

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

theorem Miri.Input.EvalRunConstruction.observeProgress_eq {Os R P H D O Aff B Poll Instant System Native Profiler : Type} (profile : Lean.Options) (boundary : String) (iteration : Nat) (state : State Os R P H D O Aff B Poll Instant System Native Profiler) : observeProgress profile boundary iteration state = state

def Miri.Input.EvalRunConstruction.iterationProfiled {Os R P H D O Aff B Poll Instant System Native Profiler C Callback : Type} (profile : Lean.Options) (loop : Interpreter.RunLoopHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) C Callback) (choice : C) (iteration : Nat) (state : State Os R P H D O Aff B Poll Instant System Native Profiler) : Interpreter.StepResult (State Os R P H D O Aff B Poll Instant System Native Profiler) Unit

Time complete scheduler iterations, retaining their starting frame identity. Only profiling emits spans; the local threshold defaults to 10ms to avoid printing every fast iteration. A span includes scheduling and callbacks, not just the MIR instruction at its starting location.

Equations

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

theorem Miri.Input.EvalRunConstruction.iterationProfiled_eq {Os R P H D O Aff B Poll Instant System Native Profiler C Callback : Type} (profile : Lean.Options) (loop : Interpreter.RunLoopHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) C Callback) (choice : C) (iteration : Nat) (state : State Os R P H D O Aff B Poll Instant System Native Profiler) : iterationProfiled profile loop choice iteration state = Interpreter.RunLoop.iteration loop choice state

This reuses RunLoop.iteration directly. No stop predicate can turn a prefix boundary into process success, and no callback is permitted to claim completion. A source TerminationInfo::Exit is the only successful process result represented here.

def Miri.Input.EvalRunConstruction.runUntilTerminalProfiled {Os R P H D O Aff B Poll Instant System Native Profiler C : Type} (profile : Lean.Options) {Callback : Type} (loop : Interpreter.RunLoopHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) C Callback) (iterationFuel : Nat) (outerChoices : List C) (initial : State Os R P H D O Aff B Poll Instant System Native Profiler) : RunResult (State Os R P H D O Aff B Poll Instant System Native Profiler)

Equations

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

def Miri.Input.EvalRunConstruction.runUntilTerminal {Os R P H D O Aff B Poll Instant System Native Profiler C Callback : Type} (loop : Interpreter.RunLoopHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) C Callback) (iterationFuel : Nat) (outerChoices : List C) (initial : State Os R P H D O Aff B Poll Instant System Native Profiler) : RunResult (State Os R P H D O Aff B Poll Instant System Native Profiler)

Original API, with observation disabled.

Equations

• Miri.Input.EvalRunConstruction.runUntilTerminal loop iterationFuel outerChoices initial = Miri.Input.EvalRunConstruction.runUntilTerminalProfiled ∅ loop iterationFuel outerChoices initial

theorem Miri.Input.EvalRunConstruction.runUntilTerminalProfiled_eq_runUntilTerminal {Os R P H D O Aff B Poll Instant System Native Profiler C Callback : Type} (profile : Lean.Options) (loop : Interpreter.RunLoopHooks (State Os R P H D O Aff B Poll Instant System Native Profiler) C Callback) (fuel : Nat) (choices : List C) (initial : State Os R P H D O Aff B Poll Instant System Native Profiler) : runUntilTerminalProfiled profile loop fuel choices initial = runUntilTerminal loop fuel choices initial

Every choice, state mutation and terminal/error/pending result is preserved for arbitrary profiling options, hooks, bounds and initial states.