Windows execution loop over the canonical Main and ExitCalled callback product. It reuses the interpreter's step and termination machines, while Windows callback ownership stays in Main/TLS, ExitCalled, typed synchronization state. Host readiness is inspected on demand and reports Unsupported only when an actual host-blocked operation requires absent polling.

@[reducible, inline]

abbrev Miri.Input.EvalWindowsRunConstruction.Payload : Type

Equations

• Miri.Input.EvalWindowsRunConstruction.Payload = Miri.Input.EvalSyncPayload.Payload

@[reducible, inline]

abbrev Miri.Input.EvalWindowsRunConstruction.Other (Raw Listener TcpStream Error : Type) : Type

Equations

• Miri.Input.EvalWindowsRunConstruction.Other Raw Listener TcpStream Error = Miri.Input.EvalSocketStorage.Other Raw Listener TcpStream Error

@[reducible, inline]

abbrev Miri.Input.EvalWindowsRunConstruction.Host (Poll Instant System H D Raw Listener TcpStream Error Native Profiler : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalWindowsRunConstruction.State (Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalWindowsRunConstruction.User (Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalWindowsRunConstruction.World (Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

def Miri.Input.EvalWindowsRunConstruction.needsHostIo {Poll F D : Type} (blocking : Interpreter.BlockingIo.Manager Poll) (readiness : Interpreter.ReadinessMachine.Registry F) (ownership : Interpreter.FileOwnership.Registry D) : Bool

Equations

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

def Miri.Input.EvalWindowsRunConstruction.scheduler {Os R H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler C X F A : Type} (configuration : HostRuntime.Configuration) (callbacks : EvalWindowsCallbackSourceConstruction.Product Os R Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler C X F A) (choiceAccess : Interpreter.ExecutionChoices.Access (Interpreter.ThreadStacks.State Memory.MiriMemoryKind (User Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error))) (clock : Interpreter.Clock.HostHooks Instant System (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (systemDurationSince : System → System → EStateM Interpreter.StepError (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Option Interpreter.Clock.Duration)) : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (User Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)

Build the local source scheduler from real deadline state, host clock and the one Windows callback router. Windows has no host poll binding here, so delayed readiness and blocked host sources stay explicit demand-local gaps.

Equations

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

def Miri.Input.EvalWindowsRunConstruction.hooks {Os R H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler C : Type} (configuration : HostRuntime.Configuration) (callbacks : EvalWindowsCallbackSourceConstruction.Product Os R Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler C ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)) (configs : C → Except Interpreter.StepError (EvalExecutable.Core Os R Payload H D (Other Raw Listener TcpStream Error) Aff B (Host Poll Instant System H D Raw Listener TcpStream Error Native Profiler) C Instant)) (limits : Interpreter.ExecutionMachine.Limits) (choiceAccess : Interpreter.ExecutionChoices.Access (Interpreter.ThreadStacks.State Memory.MiriMemoryKind (User Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error))) (clock : Interpreter.Clock.HostHooks Instant System (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (systemDurationSince : System → System → EStateM Interpreter.StepError (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Option Interpreter.Clock.Duration)) (process : EvalRunConstruction.ProcessEffects (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) : Interpreter.RunLoopHooks (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.WindowsExitMachine.Callback

Construct the Windows Main/TLS/ExitCalled loop with the same execution step, termination, interrupt, process and choice-tape semantics as the loop. Callback execution is exclusively through WindowsExitMachine.

Equations

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

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

Finite-prefix execution preserves the runner's pending and error classification. Only a source termination error returns exited.

Equations

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