Canonical source construction for the Windows file/handle dispatch. It reuses the source Files/Readiness tables and actual Main memory; only host path and host file operations remain inputs.

@[reducible, inline]

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

Equations

• Miri.Input.EvalWindowsFileConstruction.Payload Os R P H D O Aff B Host = Miri.Interpreter.ValidityMachine.UserState (Miri.Input.EvalCoreMachine.World Os R P H D O Aff B Host)

@[reducible, inline]

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

Equations

• Miri.Input.EvalWindowsFileConstruction.State Os R P H D O Aff B Host = Miri.Interpreter.MainMachine.State (Miri.Input.EvalWindowsFileConstruction.Payload Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalWindowsFileConstruction.Ref (H D O : Type) : Type

Equations

• Miri.Input.EvalWindowsFileConstruction.Ref H D O = Miri.Interpreter.WindowsFileMachine.Ref H D O

@[reducible, inline]

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

Equations

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

structure Miri.Input.EvalWindowsFileConstruction.HostEffects (Os S Path H D O HM Time E : Type) : Type

• pathFromOs : Os → Path
• osFromPath : Path → Os
• pathExists : Path → M S Bool
• absolute : Option (Path → M S (Except (Interpreter.IoError.HostError E) Path))
• length : HM → UInt64
• fileType : HM → Interpreter.UnixFsMetadata.FileType
• time : HM → Interpreter.UnixFsMetadata.TimeField → M S (Except (Interpreter.IoError.HostError E) Time)
• fileLength : H → M S (Except (Interpreter.IoError.HostError E) UInt64)
• setLength : H → UInt64 → M S (Except (Interpreter.IoError.HostError E) Unit)
• syncAll : H → M S (Except (Interpreter.IoError.HostError E) Unit)
• rename : Path → Path → M S (Except (Interpreter.IoError.HostError E) Unit)
• removeFile : Path → M S (Except (Interpreter.IoError.HostError E) Unit)

def Miri.Input.EvalWindowsFileConstruction.fromSource [DecidableEq Memory.MiriMemoryKind] {Os R P H D O Aff B Host C Error HM Path Instant Time Zone Timestamp : Type} (p : CompilerProviders.Prepared) (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) (environment : Interpreter.WindowsEnvironmentDispatch.Hooks (State Os R P H D O Aff B Host) Os Error Interpreter.EnvVars.Kind) (files : 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) (host : HostEffects Os (State Os R P H D O Aff B Host) Path H D O HM Time Error) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (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) (threadError : Concurrency.ThreadError → Interpreter.StepError) : Except Interpreter.StepError (Interpreter.WindowsFileDispatch.Hooks (State Os R P H D O Aff B Host) (Ref H D O) H D Path HM Time Error Interpreter.EnvVars.Kind)

Assemble all guest-memory, ABI and descriptor behavior for Windows files over one initialized Main state. files, readiness, and sharedOpen are the canonical source components from that same world; they are not guest hook facades. Host filesystem observations stay in host.

Equations

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