Windows handles/files connected to canonical FD ownership, machine threads, FileDescription effects, shared host open and source OS strings/time helpers.

@[reducible, inline]

abbrev Miri.Interpreter.WindowsFileMachine.Ref (H D O : Type) : Type

Equations

• Miri.Interpreter.WindowsFileMachine.Ref H D O = Miri.Interpreter.Files.Ref (Miri.Interpreter.Files.Description H D O)

def Miri.Interpreter.WindowsFileMachine.bindHandles {K U H D O : Type} (h : ReadinessMachine.Hooks K U H D O) (target : ABI.RuntimeTargetDataLayout) (threadError : Concurrency.ThreadError → StepError) (base : WindowsHandles.Hooks (MachineHooks.State K U) (Ref H D O)) : WindowsHandles.Hooks (MachineHooks.State K U) (Ref H D O)

Equations

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

def Miri.Interpreter.WindowsFileMachine.readWrite {K U H D O E HM : Type} (h : ReadinessMachine.Hooks K U H D O) (files : Files.Hooks (MachineHooks.State K U) H D O E HM) (ref : Ref H D O) (communicate write : Bool) (pointer : Memory.Pointer (Option Memory.Provenance)) (count : Nat) (finish : Files.Finish (MachineHooks.State K U) E) : MachineHooks.M K U Unit

Default host/file descriptions drop at the call boundary. Custom descriptions own the transferred reference and typed continuation for real blocked I/O.

Equations

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

def Miri.Interpreter.WindowsFileMachine.bind {K U H D O E HM P T Kind : Type} (h : ReadinessMachine.Hooks K U H D O) (target : ABI.RuntimeTargetDataLayout) (threadError : Concurrency.ThreadError → StepError) (files : Files.Hooks (MachineHooks.State K U) H D O E HM) (sharedOpen : UnixOpen.Hooks (MachineHooks.State K U) H D O E HM P) (otherMetadata : O → MachineHooks.M K U (Except (IoError.HostError E) HM ⊕ String)) (prepareDirectory : D → P → MachineHooks.M K U D) (base : WindowsPaths.Hooks (MachineHooks.State K U) (Ref H D O) H D P HM T E Kind) : WindowsPaths.Hooks (MachineHooks.State K U) (Ref H D O) H D P HM T E Kind

Equations

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

def Miri.Interpreter.WindowsFileMachine.bindTime {S Host T Zone Stamp F H D P HM E : Type} (time : TimeShims.Hooks S Host T Zone Stamp) (base : WindowsFiles.Hooks S F H D P HM T E) : WindowsFiles.Hooks S F H D P HM T E

Epoch/tick arithmetic stays canonical TimeShims, including before-epoch and u64 overflow outcomes, rather than a caller-computed time snapshot.

Equations

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