Raw host-effect wiring for the Windows file family. WindowsFiles owns the Win32 flag parser; this module supplies the same-world byte access, descriptor ownership, shared open-file-or-directory policy, and genuine host file leaves. UnixOpen's embedded FD dictionary is only used by its Unix open-path entrypoint, which WindowsFiles never calls.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalWindowsIoSourceConstruction.Host (Poll Instant System H D O Native Profiler : Type) : Type

Equations

• Miri.Input.EvalWindowsIoSourceConstruction.Host Poll Instant System H D O Native Profiler = Miri.Input.HostRuntime.Storage Poll Instant System H D O Native Profiler

@[reducible, inline]

abbrev Miri.Input.EvalWindowsIoSourceConstruction.Payload (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.EvalWindowsIoSourceConstruction.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.EvalWindowsIoSourceConstruction.FD (H D O : Type) : Type

Equations

• Miri.Input.EvalWindowsIoSourceConstruction.FD H D O = Miri.Interpreter.Files.Ref (Miri.Interpreter.Files.Description H D O)

@[reducible, inline]

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

Equations

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

structure Miri.Input.EvalWindowsIoSourceConstruction.IoComponents (Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path : Type) : Type

• fileRegistry : Interpreter.Files.Hooks (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Meta
• readiness : Interpreter.ReadinessMachine.Hooks Memory.MiriMemoryKind (Interpreter.ThreadStacks.Storage (Payload Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) H D (Other Raw Listener TcpStream Error)
• sharedOpen : Interpreter.UnixOpen.Hooks (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Meta Path
• prepareDirectory : D → Path → M (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) D
• otherMetadata : Other Raw Listener TcpStream Error → M (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Except (Interpreter.IoError.HostError Error) Meta ⊕ String)
• hostFiles : EvalWindowsFileConstruction.HostEffects Os (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Path H D (Other Raw Listener TcpStream Error) Meta System Error
• checkPointerAccess : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit

def Miri.Input.EvalWindowsIoSourceConstruction.fromSource {Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (sourceSeed : EvalWindowsCallDispatchConstruction.SourceSeed Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C) (main : Interpreter.MainMachine.Hooks (Payload Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (Other Raw Listener TcpStream Error) ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff Interpreter.ProgramExitPoll) (errors : Interpreter.IoError.Hooks (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error) (openHost : EvalUnixNativeFdConstruction.OpenHostEffects (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D Error Meta Path Os) (hostFiles : EvalUnixIoConstruction.HostFileEffects (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Meta) (resources : EvalUnixIoConstruction.FileResourceEffects (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)) (_locks : EvalUnixIoConstruction.FileLockEffects (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H Error) (positional : EvalUnixNativeFdConstruction.OtherPositionalEffects (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error) (filesystem : Option (EvalSourceHostEffects.Filesystem Os (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Path Meta System Error R)) (resourcesBudget watcherBudget hostUsizeBits : Nat) (targetIsizeMax hostIsizeMax : UInt64) (pathToOs : Path → Os) (arithmetic : Memory.PointerArithmetic) : Except Interpreter.StepError (IoComponents Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path)

Build Windows file IO over the live Main access configuration and the raw host residuals. Path-to-OS conversion is an explicit representation codec, separate from optional filesystem syscalls.

Equations

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

def Miri.Input.EvalWindowsIoSourceConstruction.fromInnerSource {Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (sourceSeed : EvalWindowsCallDispatchConstruction.SourceSeed Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C) (main : Interpreter.MainMachine.Hooks (Payload Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (Other Raw Listener TcpStream Error) ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff Interpreter.ProgramExitPoll) (errors : Interpreter.IoError.Hooks (State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error) (openHost : EvalUnixNativeFdConstruction.OpenHostEffects (EvalSocketStorage.State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D Error Meta Path Os) (hostFiles : EvalUnixIoConstruction.HostFileEffects (EvalSocketStorage.State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Meta) (resources : EvalUnixIoConstruction.FileResourceEffects (EvalSocketStorage.State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)) (locks : EvalUnixIoConstruction.FileLockEffects (EvalSocketStorage.State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H Error) (positional : EvalUnixNativeFdConstruction.OtherPositionalEffects (EvalSocketStorage.State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error) (filesystem : Option (EvalSourceHostEffects.Filesystem Os (EvalSocketStorage.State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Path Meta System Error R)) (resourcesBudget watcherBudget hostUsizeBits : Nat) (targetIsizeMax hostIsizeMax : UInt64) (pathToOs : Path → Os) (arithmetic : Memory.PointerArithmetic) : Except Interpreter.StepError (IoComponents Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path)

Adapt the raw source-runner host effects, whose state is the canonical EvalCore inner state, into the outer Main state used by Windows dispatch.

Equations

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