Assemble the canonical Windows environment, file and thread foreign-item families over one prepared compiler target and one initialized Main machine. The component constructors own guest memory, process/environment tables, descriptor/handle state and TLS/thread operations. Host interaction remains explicit at the source boundary.

@[reducible, inline]

abbrev Miri.Input.EvalWindowsSourceConstruction.Payload (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalWindowsSourceConstruction.Payload Os R P H D O Aff B Host = Miri.Input.EvalWindowsFileConstruction.Payload Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalWindowsSourceConstruction.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalWindowsSourceConstruction.State Os R P H D O Aff B Host = Miri.Input.EvalWindowsFileConstruction.State Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalWindowsSourceConstruction.FileRef (H D O : Type) : Type

Equations

• Miri.Input.EvalWindowsSourceConstruction.FileRef H D O = Miri.Input.EvalWindowsFileConstruction.Ref H D O

@[reducible, inline]

abbrev Miri.Input.EvalWindowsSourceConstruction.M (S A : Type) : Type

Equations

• Miri.Input.EvalWindowsSourceConstruction.M S A = EStateM Miri.Interpreter.StepError S A

structure Miri.Input.EvalWindowsSourceConstruction.Components (Os R P H D O Aff B Host C Error HM Path Time : Type) : Type

• environment : Interpreter.WindowsEnvironmentDispatch.Hooks (State Os R P H D O Aff B Host) Os Error Interpreter.EnvVars.Kind
• files : Interpreter.WindowsFileDispatch.Hooks (State Os R P H D O Aff B Host) (FileRef H D O) H D Path HM Time Error Interpreter.EnvVars.Kind
• thread : Interpreter.WindowsThreadDispatch.Hooks (State Os R P H D O Aff B Host) (FileRef H D O)
• frameInStd : EStateM Interpreter.StepError (State Os R P H D O Aff B Host) Bool

def Miri.Input.EvalWindowsSourceConstruction.fromSource {Os R P H D O Aff B Host C Error HM Path Instant Time Zone Timestamp : Type} [DecidableEq Memory.MiriMemoryKind] [DecidableEq Os] (p : CompilerProviders.Prepared) (host : EvalHostRuntimeConstruction.OsHostEffects Os) (environmentHost : EvalHostRuntimeConstruction.EnvironmentHostEffects (EvalWindowsEnvironmentConstruction.InnerControl Os R P H D O Aff B Host)) (environmentMemory : EvalWindowsEnvironmentConstruction.Memory Os R P H D O Aff B Host C) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (errors : Interpreter.IoError.Hooks (State Os R P H D O Aff B Host) Error) (environmentHostConfig : EvalWindowsEnvironmentConstruction.HostEffects (State Os R P H D O Aff B Host) Os Error) (main : Interpreter.MainMachine.Hooks (Payload Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff Interpreter.ProgramExitPoll) (fileRegistry : Interpreter.Files.Hooks (State Os R P H D O Aff B Host) H D O Error HM) (readiness : Interpreter.ReadinessMachine.Hooks Memory.MiriMemoryKind (Interpreter.ThreadStacks.Storage (Payload Os R P H D O Aff B Host)) H D O) (sharedOpen : Interpreter.UnixOpen.Hooks (State Os R P H D O Aff B Host) H D O Error HM Path) (prepareDirectory : D → Path → M (State Os R P H D O Aff B Host) D) (otherMetadata : O → M (State Os R P H D O Aff B Host) (Except (Interpreter.IoError.HostError Error) HM ⊕ String)) (timeHooks : Interpreter.TimeShims.Hooks (State Os R P H D O Aff B Host) Instant Time Zone Timestamp) (hostWindowsFiles : EvalWindowsFileConstruction.HostEffects Os (State Os R P H D O Aff B Host) Path H D O HM Time Error) (checkPointerAccess : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M (State Os R P H D O Aff B Host) Unit) (choice : C) (compatibilityBudget : Nat) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (userRelevantCrates : Array Nat) (threadError : Concurrency.ThreadError → Interpreter.StepError) : Except Interpreter.StepError (Components Os R P H D O Aff B Host C Error HM Path Time)

Build the core Windows foreign families from narrow host capabilities and the same source Main, EvalWorld memory and descriptor registry. timeHooks contains source time policy plus the required clock/timezone effects; filesystem calls consume hostFiles and hostWindowsFiles.

Equations

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

def Miri.Input.EvalWindowsSourceConstruction.dispatch {Os R P H D O Aff B Host C Error HM Path Time ClockInstant TZ Timestamp SyncRef I : Type} [DecidableEq Os] {ForeignBody Destination : Type} (components : Components Os R P H D O Aff B Host C Error HM Path Time) (time : Option (Interpreter.TimeShimDispatch.Hooks (State Os R P H D O Aff B Host) ClockInstant Time TZ Timestamp)) (sync : Option (Interpreter.WindowsSyncDispatch.Hooks (State Os R P H D O Aff B Host) SyncRef)) (random : Option (Interpreter.WindowsRandomDispatch.Hooks (State Os R P H D O Aff B Host) Destination ForeignBody I)) (platform : Option (Interpreter.WindowsPlatformDispatch.Hooks (State Os R P H D O Aff B Host) Os Error Interpreter.EnvVars.Kind (FileRef H D O))) (stdOnly : Option (Interpreter.StdOnlyShims.WindowsHooks Memory.Provenance (State Os R P H D O Aff B Host) Destination (Interpreter.MPlaceTy Memory.Provenance) ForeignBody I)) (base : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Host) Destination (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) ForeignBody I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (Interpreter.OpTy Memory.Provenance)) (dest : Interpreter.MPlaceTy Memory.Provenance) : M (State Os R P H D O Aff B Host) Interpreter.ForeignItems.EmulateItemResult

Demand-local assembly for a partially constructed Windows source closure. Environment, files and threads are always real source components from fromSource; the independently ported time/sync/random/platform/std-only families can be attached as they become available. A recognized operation whose family is absent returns Unsupported at the operation boundary, while an unrelated Windows symbol continues through the canonical fallback.

Equations

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

def Miri.Input.EvalWindowsSourceConstruction.dispatchInitial {Os R P H D O Aff B Host Error ClockInstant Time TZ Timestamp SyncRef I : Type} [DecidableEq Os] {ForeignBody Destination : Type} (environment : Interpreter.WindowsEnvironmentDispatch.Hooks (State Os R P H D O Aff B Host) Os Error Interpreter.EnvVars.Kind) (time : Option (Interpreter.TimeShimDispatch.Hooks (State Os R P H D O Aff B Host) ClockInstant Time TZ Timestamp)) (sync : Option (Interpreter.WindowsSyncDispatch.Hooks (State Os R P H D O Aff B Host) SyncRef)) (random : Option (Interpreter.WindowsRandomDispatch.Hooks (State Os R P H D O Aff B Host) Destination ForeignBody I)) (platform : Option (Interpreter.WindowsPlatformDispatch.Hooks (State Os R P H D O Aff B Host) Os Error Interpreter.EnvVars.Kind (FileRef H D O))) (stdOnly : Option (Interpreter.StdOnlyShims.WindowsHooks Memory.Provenance (State Os R P H D O Aff B Host) Destination (Interpreter.MPlaceTy Memory.Provenance) ForeignBody I)) (base : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Host) Destination (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) ForeignBody I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (Interpreter.OpTy Memory.Provenance)) (dest : Interpreter.MPlaceTy Memory.Provenance) : M (State Os R P H D O Aff B Host) Interpreter.ForeignItems.EmulateItemResult

Initial Windows dispatch before Main-bound file/thread callbacks exist. Environment, random, and std-only operations are still source-built on the canonical startup state. File, thread, time, sync, and platform names fail closed only when requested; unrelated names continue through the Core fallback.

Equations

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

def Miri.Input.EvalWindowsSourceConstruction.bind {Os R P H D O Aff B Host C Error HM Path Time ClockInstant TZ Timestamp SyncRef I : Type} [DecidableEq Os] {ForeignBody Destination : Type} (components : Components Os R P H D O Aff B Host C Error HM Path Time) (time : Option (Interpreter.TimeShimDispatch.Hooks (State Os R P H D O Aff B Host) ClockInstant Time TZ Timestamp)) (sync : Option (Interpreter.WindowsSyncDispatch.Hooks (State Os R P H D O Aff B Host) SyncRef)) (random : Option (Interpreter.WindowsRandomDispatch.Hooks (State Os R P H D O Aff B Host) Destination ForeignBody I)) (platform : Option (Interpreter.WindowsPlatformDispatch.Hooks (State Os R P H D O Aff B Host) Os Error Interpreter.EnvVars.Kind (FileRef H D O))) (stdOnly : Option (Interpreter.StdOnlyShims.WindowsHooks Memory.Provenance (State Os R P H D O Aff B Host) Destination (Interpreter.MPlaceTy Memory.Provenance) ForeignBody I)) (base : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Host) Destination (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) ForeignBody I) : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Host) Destination (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) ForeignBody I

Bind the demand-local source dispatcher into the common foreign-item chain. Missing component families stay explicit and fail only after their exact names reach the dispatcher.

Equations

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