Canonical Windows source startup. The factory builds the fixed MIR configuration and live Windows foreign context from raw source leaves. This unit builds its initial assembly, bootstraps the same Main state, and derives typed-sync and Windows callback routing for the Windows component connector and loop.

@[reducible, inline]

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

Equations

• Miri.Input.EvalWindowsSourceRunConstruction.Other Raw Listener TcpStream Error = Miri.Input.EvalWindowsCallDispatchConstruction.Other Raw Listener TcpStream Error

@[reducible, inline]

abbrev Miri.Input.EvalWindowsSourceRunConstruction.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.EvalWindowsSourceRunConstruction.State (Os R H D 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.EvalWindowsSourceRunConstruction.Assembly (Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path Zone Timestamp : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalWindowsSourceRunConstruction.Context (Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path Zone Timestamp : Type) : Type 1

Equations

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

structure Miri.Input.EvalWindowsSourceRunConstruction.Started (Os R H D B Poll Instant System Native Profiler C Raw Listener TcpStream Error ErrorHost Meta Path : Type) : Type 1

• execution : Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (EvalConfigurationCore.SourceUser Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (Other Raw Listener TcpStream Error) ABI.ExternAbi Instant
• context : Context Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path Unit Unit
• assembly : Assembly Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path Unit Unit
• bootstrap : EvalBootstrap.Configuration Os × EvalBootstrap.Hooks (EvalExecutable.U Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B (Host Poll Instant System H D Raw Listener TcpStream Error Native Profiler)) C (Other Raw Listener TcpStream Error) ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Interpreter.CpuAffinity.Mask EvalSyncObjectAccess.Payload (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (EvalWorld.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B (Host Poll Instant System H D Raw Listener TcpStream Error Native Profiler)))) Os
• main : Interpreter.MainMachine.Hooks (EvalCallbackMachine.ThreadUser Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler) C (Other Raw Listener TcpStream Error) ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Interpreter.CpuAffinity.Mask Interpreter.ProgramExitPoll
• syncEffects : Interpreter.TypedSyncMachine.Effects (Interpreter.MachineHooks.State Memory.MiriMemoryKind (EvalSyncMachine.User Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler))
• callbacks : EvalWindowsCallbackSourceConstruction.Product Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler C ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)
• callbackAssembly : EvalWindowsCallbackAssembly.Product Os R H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error C ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)
• state : State Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error

def Miri.Input.EvalWindowsSourceRunConstruction.startFromInitial {Os R H D B Poll Instant System Native Profiler C Raw Listener TcpStream Error ErrorHost Meta Path AddrIter : Type} [DecidableEq Os] [DecidableEq Memory.MiriMemoryKind] (prepared : EvalPreparation.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : EvalConfigurationCore.Options) (sourceLeaves : EvalConfigurationCore.SourceLeaves Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C Instant Interpreter.CallInstance AddrIter) (windowsHost : EvalWindowsEnvironmentConstruction.HostEffects (State Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error) Os Error) (choice : C) (limits : Interpreter.ExecutionMachine.Limits) (bootstrapConfiguration : EvalBootstrap.Configuration Os) (initial : State Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error) : Except (State Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error × Interpreter.StepError) (Started Os R H D B Poll Instant System Native Profiler C Raw Listener TcpStream Error ErrorHost Meta Path)

Build the Windows execution package, construct its same-world raw foreign assembly, attach bootstrap Main/TLS and source environment state, then derive the backend-specific typed synchronization effects and actual callback router. Every failure after a stateful operation returns the state prefix with error.

Equations

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

def Miri.Input.EvalWindowsSourceRunConstruction.runFromInitial {Os R H D B Poll Instant System Native Profiler C : Type} [DecidableEq Os] [DecidableEq Memory.MiriMemoryKind] {Raw Listener TcpStream Error ErrorHost Meta Path AddrIter : Type} (prepared : EvalPreparation.Prepared) (image : AllocationImage.Imported) (bytes : CompilerGlobalBytes.Prepared) (options : EvalConfigurationCore.Options) (sourceLeaves : EvalConfigurationCore.SourceLeaves Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C Instant Interpreter.CallInstance AddrIter) (windowsHost : EvalWindowsEnvironmentConstruction.HostEffects (State Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error) Os Error) (pathToOs : Path → Os) (choice : C) (initialConfiguration : InitialMachine.Configuration Interpreter.CpuAffinity.Mask B) (bootstrapConfiguration : EvalBootstrap.Configuration Os) (limits : Interpreter.ExecutionMachine.Limits) (capacity iterationFuel : Nat) (outerChoices : List C) (initial : State Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error) : Except Interpreter.StepError (EvalRunConstruction.RunResult (State Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error))

Run an already constructed Windows world from its source-owned startup. Each scheduler choice builds a fresh source configuration and connects its foreign assembly to the same startup Main and callback registries. The Windows loop then handles deadline, exit, join, and synchronization callbacks without Unix descriptor callback seeds.

Equations

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