Complete windows/fs.rs policy. Reuses shared FileDescription and host open infrastructure; target constants and real host resources remain mandatory.

@[reducible, inline]

abbrev Miri.Interpreter.WindowsFiles.M (σ α : Type) : Type

Equations

• Miri.Interpreter.WindowsFiles.M = EStateM Miri.Interpreter.StepError

inductive Miri.Interpreter.WindowsFiles.Disposition : Type

• createAlways : Disposition
• createNew : Disposition
• openAlways : Disposition
• openExisting : Disposition
• truncateExisting : Disposition

@[instance_reducible]

instance Miri.Interpreter.WindowsFiles.instDecidableEqDisposition : DecidableEq Disposition

Equations

• Miri.Interpreter.WindowsFiles.instDecidableEqDisposition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.WindowsFiles.instReprDisposition : Repr Disposition

Equations

• Miri.Interpreter.WindowsFiles.instReprDisposition = { reprPrec := Miri.Interpreter.WindowsFiles.instReprDisposition.repr }

def Miri.Interpreter.WindowsFiles.instReprDisposition.repr : Disposition → Nat → Std.Format

Equations

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

structure Miri.Interpreter.WindowsFiles.Attributes : Type

• normal : Bool
• backup : Bool
• reparse : Bool

structure Miri.Interpreter.WindowsFiles.File (H : Type) : Type

• handle : H
• writable : Bool

structure Miri.Interpreter.WindowsFiles.Hooks (S F H D P HM Time E : Type) : Type

• handles : WindowsHandles.Hooks S F
• errors : IoError.Hooks S E
• os : String
• communicate : Bool
• noIsolation : String → M S Unit
• constant : String → M S UInt32
• readUsize : OpTy Memory.Provenance → M S UInt64
• readI64 : OpTy Memory.Provenance → M S Int64
• readWidePath : Memory.Pointer (Option Memory.Provenance) → M S P
• pathExists : P → M S Bool
• openFileOrDir : P → UnixOpen.Options → M S (Except (IoError.HostError E) (UnixOpen.Opened H D))

  Actual shared open_file_or_dir(None,path,options), including host workaround.

• dropFile : H → M S Unit
• dropDirectory : D → M S Unit
• insertFile : H → Bool → Bool → M S Int32
• insertDirectory : D → P → M S Int32
• asFile : F → Option (File H)
• metadata : F → M S (Except (IoError.HostError E) HM ⊕ String)
• length : HM → UInt64
• fileType : HM → UnixFsMetadata.FileType
• time : HM → UnixFsMetadata.TimeField → M S (Except (IoError.HostError E) Time)
• windowsTicks : Time → M S UInt64

  system_time_since_windows_epoch then windows_ticks_for (checked u64).

• fileLength : H → M S (Except (IoError.HostError E) UInt64)
• setLength : H → UInt64 → M S (Except (IoError.HostError E) Unit)
• syncAll : H → M S (Except (IoError.HostError E) Unit)
• rename : P → P → M S (Except (IoError.HostError E) Unit)
• removeFile : P → M S (Except (IoError.HostError E) Unit)
• derefAs : OpTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• ptrToPlace : Memory.Pointer (Option Memory.Provenance) → String → M S (MPlaceTy Memory.Provenance)
• derefI64 : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• checkAccess : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S Unit
• field : MPlaceTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• readFieldI64 : MPlaceTy Memory.Provenance → M S Int64
• writeFields : Array (String × Int) → MPlaceTy Memory.Provenance → M S Unit
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• seek : F → Bool → Files.SeekFrom → M S (Except (IoError.Error E) UInt64)
• readWrite : F → Bool → Bool → Memory.Pointer (Option Memory.Provenance) → Nat → Files.Finish S E → M S Unit

  Consumes owned FD reference, including asynchronous completion. Real Files read/write provides the immediate/file route and custom typed pending callbacks.

def Miri.Interpreter.WindowsFiles.disposition {S F H D P HM T E : Type} (h : Hooks S F H D P HM T E) (value : UInt32) : M S Disposition

Equations

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

def Miri.Interpreter.WindowsFiles.attributes {S F H D P HM T E : Type} (h : Hooks S F H D P HM T E) (value : UInt32) : M S Attributes

Equations

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

def Miri.Interpreter.WindowsFiles.create {S F H D P HM T E : Type} (h : Hooks S F H D P HM T E) (name access share security disp flags template : OpTy Memory.Provenance) : M S WindowsHandles.Handle

Equations

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

def Miri.Interpreter.WindowsFiles.getInformation {S F H D P HM T E : Type} (h : Hooks S F H D P HM T E) (file info : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.WindowsFiles.setInformation {S F H D P HM T E : Type} (h : Hooks S F H D P HM T E) (file infoClass info size : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.WindowsFiles.flush {S F H D P HM T E : Type} (h : Hooks S F H D P HM T E) (operand : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.WindowsFiles.moveFile {S F H D P HM T E : Type} (h : Hooks S F H D P HM T E) (old new flags : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.WindowsFiles.deleteFile {S F H D P HM T E : Type} (h : Hooks S F H D P HM T E) (operand : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.WindowsFiles.ntReadWrite {S F H D P HM T E : Type} (h : Hooks S F H D P HM T E) (write : Bool) (handle event routine context status buffer count offset key : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Read/write intentionally differ in whether status projection precedes FD validation, including upstream's NtWriteFile diagnostic in the read branch.

Equations

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

def Miri.Interpreter.WindowsFiles.setPointer {S F H D P HM T E : Type} (h : Hooks S F H D P HM T E) (operand distance newPointer method : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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