Descriptor identities/table and portable FileDescription behavior from pinned shims/files.rs. Host handles remain real external resources; no virtual filesystem or readiness-success environment is manufactured.

@[reducible, inline]

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

Equations

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

def Miri.Interpreter.Files.withDrop {S A : Type} (action : M S A) (cleanup : M S Unit) : M S A

Rust scope drop, including errors. A failing required destructor remains explicit and keeps its effects; it cannot be silently discarded.

Equations

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

structure Miri.Interpreter.Files.FdId : Type

• value : Nat

def Miri.Interpreter.Files.instDecidableEqFdId.decEq (x✝ x✝¹ : FdId) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.Files.instDecidableEqFdId.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.Files.instDecidableEqFdId : DecidableEq FdId

Equations

• Miri.Interpreter.Files.instDecidableEqFdId = Miri.Interpreter.Files.instDecidableEqFdId.decEq

def Miri.Interpreter.Files.instReprFdId.repr : FdId → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Files.instReprFdId : Repr FdId

Equations

• Miri.Interpreter.Files.instReprFdId = { reprPrec := Miri.Interpreter.Files.instReprFdId.repr }

inductive Miri.Interpreter.Files.Description (Handle Directory Other : Type) : Type

• stdin {Handle Directory Other : Type} : Description Handle Directory Other
• stdout {Handle Directory Other : Type} : Description Handle Directory Other
• stderr {Handle Directory Other : Type} : Description Handle Directory Other
• nullOutput {Handle Directory Other : Type} : Description Handle Directory Other
• file {Handle Directory Other : Type} (handle : Handle) (readable writable : Bool) : Description Handle Directory Other
• directory {Handle Directory Other : Type} (handle : Directory) : Description Handle Directory Other
• other {Handle Directory Other : Type} (payload : Other) : Description Handle Directory Other

structure Miri.Interpreter.Files.Ref (Description : Type) : Type

• id : FdId
• value : Description

@[instance_reducible]

instance Miri.Interpreter.Files.instBEqRef {D : Type} : BEq (Ref D)

Equations

• Miri.Interpreter.Files.instBEqRef = { beq := fun (left right : Miri.Interpreter.Files.Ref D) => left.id == right.id }

structure Miri.Interpreter.Files.WeakRef : Type

• id : FdId

structure Miri.Interpreter.Files.Table (Description : Type) : Type

• fds : Array (Int32 × Ref Description)
• nextId : Nat

def Miri.Interpreter.Files.Table.newRef {D : Type} (table : Table D) (description : D) (hostUsizeBits : Nat) : Except StepError (Table D × Ref D)

Equations

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

def Miri.Interpreter.Files.Table.insertWithMin {D : Type} (table : Table D) (ref : Ref D) (minimum : Int32) : Except StepError (Table D × Int32)

Equations

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

def Miri.Interpreter.Files.Table.insert {D : Type} (table : Table D) (ref : Ref D) : Except StepError (Table D × Int32)

Equations

• table.insert ref = table.insertWithMin ref 0

def Miri.Interpreter.Files.Table.insertNew {D : Type} (table : Table D) (value : D) (hostUsizeBits : Nat) : Except StepError (Table D × Int32)

Equations

• table.insertNew value hostUsizeBits = do let __x ← table.newRef value hostUsizeBits match __x with | (table, ref) => table.insert ref

def Miri.Interpreter.Files.Table.get {D : Type} (table : Table D) (fd : Int32) : Option (Ref D)

The runtime must retain the returned strong reference (including in pending callbacks). Table.remove transfers its strong reference rather than duplicating.

Equations

• table.get fd = Option.map (fun (x : Int32 × Miri.Interpreter.Files.Ref D) => x.snd) (Array.find? (fun (x : Int32 × Miri.Interpreter.Files.Ref D) => x.fst == fd) table.fds)

def Miri.Interpreter.Files.Table.remove {D : Type} (table : Table D) (fd : Int32) : Table D × Option (Ref D)

Equations

• table.remove fd = ({ fds := Array.filter (fun (x : Int32 × Miri.Interpreter.Files.Ref D) => x.fst != fd) table.fds, nextId := table.nextId }, table.get fd)

def Miri.Interpreter.Files.Table.isFdNum {D : Type} (table : Table D) (fd : Int32) : Bool

Equations

• table.isFdNum fd = table.fds.any fun (x : Int32 × Miri.Interpreter.Files.Ref D) => x.fst == fd

def Miri.Interpreter.Files.Table.init {H D O : Type} (mute : Bool) (hostUsizeBits : Nat) : Except StepError (Table (Description H D O))

Equations

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

structure Miri.Interpreter.Files.Readiness : Type

• readable : Bool
• writable : Bool
• readClosed : Bool
• writeClosed : Bool
• error : Bool

def Miri.Interpreter.Files.instDecidableEqReadiness.decEq (x✝ x✝¹ : Readiness) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Files.instDecidableEqReadiness : DecidableEq Readiness

Equations

• Miri.Interpreter.Files.instDecidableEqReadiness = Miri.Interpreter.Files.instDecidableEqReadiness.decEq

def Miri.Interpreter.Files.instReprReadiness.repr : Readiness → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Files.instReprReadiness : Repr Readiness

Equations

• Miri.Interpreter.Files.instReprReadiness = { reprPrec := Miri.Interpreter.Files.instReprReadiness.repr }

inductive Miri.Interpreter.Files.SeekFrom : Type

• start (offset : UInt64) : SeekFrom
• current (offset : Int64) : SeekFrom
• finish (offset : Int64) : SeekFrom

@[reducible, inline]

abbrev Miri.Interpreter.Files.Result (Host A : Type) : Type

Equations

• Miri.Interpreter.Files.Result Host A = Except (Miri.Interpreter.IoError.Error Host) A

@[reducible, inline]

abbrev Miri.Interpreter.Files.Finish (S Host : Type) : Type

Equations

• Miri.Interpreter.Files.Finish S Host = Miri.Interpreter.IoCompletionData.Finish S (Miri.Interpreter.IoError.Error Host)

structure Miri.Interpreter.Files.Hooks (S Handle Directory Other Host Metadata : Type) : Type

• family : ForeignItems.Family
• hostRead : Description Handle Directory Other → ByteArray → M S (Except (IoError.HostError Host) (Nat × ByteArray))
• hostWrite : Description Handle Directory Other → ByteArray → M S (Except (IoError.HostError Host) Nat)
• hostFlushStdout : M S Unit
• hostSeek : Handle → SeekFrom → M S (Except (IoError.HostError Host) UInt64)
• hostMetadata : Description Handle Directory Other → M S (Except (IoError.HostError Host) Metadata)
• hostIsTerminal : Description Handle Directory Other → M S Bool
• readBytes : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S ByteArray
• writeBytes : Memory.Pointer (Option Memory.Provenance) → ByteArray → M S Unit
• permissionDenied : M S (IoError.HostError Host)
• otherRead : Ref (Description Handle Directory Other) → Bool → Memory.Pointer (Option Memory.Provenance) → Nat → Finish S Host → M S Unit

  Socket/pipe/event descriptions may block and invoke finish only later. Their real readiness/blocking implementation must retain captured strong refs.

• otherWrite : Ref (Description Handle Directory Other) → Bool → Memory.Pointer (Option Memory.Provenance) → Nat → Finish S Host → M S Unit
• otherShortOperations : Other → Bool
• otherReadiness : Other → M S (Option Readiness)
• otherHasReadinessWatched : Other → Bool
• otherIsTerminal : Other → Bool → M S Bool

def Miri.Interpreter.Files.readFromHost {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (description : Description H D O) (len : Nat) (pointer : Memory.Pointer (Option Memory.Provenance)) : M S (Result E Nat)

Equations

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

def Miri.Interpreter.Files.writeToHost {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (description : Description H D O) (len : Nat) (pointer : Memory.Pointer (Option Memory.Provenance)) : M S (Result E Nat)

Equations

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

def Miri.Interpreter.Files.read {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (ref : Ref (Description H D O)) (communicate : Bool) (pointer : Memory.Pointer (Option Memory.Provenance)) (len : Nat) (finish : Finish S E) : M S Unit

Equations

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

def Miri.Interpreter.Files.write {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (ref : Ref (Description H D O)) (communicate : Bool) (pointer : Memory.Pointer (Option Memory.Provenance)) (len : Nat) (finish : Finish S E) : M S Unit

Equations

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

def Miri.Interpreter.Files.shortOperations {S H D O E Meta : Type} (h : Hooks S H D O E Meta) : Description H D O → Bool

Equations

• Miri.Interpreter.Files.shortOperations h (Miri.Interpreter.Files.Description.file handle readable writable) = true
• Miri.Interpreter.Files.shortOperations h (Miri.Interpreter.Files.Description.other value) = h.otherShortOperations value
• Miri.Interpreter.Files.shortOperations h x✝ = false

def Miri.Interpreter.Files.readiness {S H D O E Meta : Type} (h : Hooks S H D O E Meta) : Description H D O → M S (Option Readiness)

Equations

• Miri.Interpreter.Files.readiness h Miri.Interpreter.Files.Description.stdin = pure (some { readable := true, writable := true })
• Miri.Interpreter.Files.readiness h Miri.Interpreter.Files.Description.stdout = pure (some { writable := true })
• Miri.Interpreter.Files.readiness h Miri.Interpreter.Files.Description.stderr = pure (some { writable := true })
• Miri.Interpreter.Files.readiness h Miri.Interpreter.Files.Description.nullOutput = pure (some { writable := true })
• Miri.Interpreter.Files.readiness h (Miri.Interpreter.Files.Description.file handle readable writable) = pure none
• Miri.Interpreter.Files.readiness h (Miri.Interpreter.Files.Description.directory handle) = pure none
• Miri.Interpreter.Files.readiness h (Miri.Interpreter.Files.Description.other value) = h.otherReadiness value

def Miri.Interpreter.Files.hasReadinessWatched {S H D O E Meta : Type} (h : Hooks S H D O E Meta) : Description H D O → Bool

Equations

• Miri.Interpreter.Files.hasReadinessWatched h Miri.Interpreter.Files.Description.stdin = true
• Miri.Interpreter.Files.hasReadinessWatched h Miri.Interpreter.Files.Description.stdout = true
• Miri.Interpreter.Files.hasReadinessWatched h Miri.Interpreter.Files.Description.stderr = true
• Miri.Interpreter.Files.hasReadinessWatched h Miri.Interpreter.Files.Description.nullOutput = true
• Miri.Interpreter.Files.hasReadinessWatched h (Miri.Interpreter.Files.Description.file handle readable writable) = false
• Miri.Interpreter.Files.hasReadinessWatched h (Miri.Interpreter.Files.Description.directory handle) = false
• Miri.Interpreter.Files.hasReadinessWatched h (Miri.Interpreter.Files.Description.other value) = h.otherHasReadinessWatched value

def Miri.Interpreter.Files.isTty {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (communicate : Bool) (description : Description H D O) : M S Bool

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.Files.isTty h communicate Miri.Interpreter.Files.Description.stdin = if communicate = true then h.hostIsTerminal Miri.Interpreter.Files.Description.stdin else pure false
• Miri.Interpreter.Files.isTty h communicate Miri.Interpreter.Files.Description.stdout = if communicate = true then h.hostIsTerminal Miri.Interpreter.Files.Description.stdout else pure false
• Miri.Interpreter.Files.isTty h communicate Miri.Interpreter.Files.Description.stderr = if communicate = true then h.hostIsTerminal Miri.Interpreter.Files.Description.stderr else pure false
• Miri.Interpreter.Files.isTty h communicate (Miri.Interpreter.Files.Description.other value) = h.otherIsTerminal value communicate
• Miri.Interpreter.Files.isTty h communicate description = pure false

def Miri.Interpreter.Files.seek {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (communicate : Bool) (description : Description H D O) (offset : SeekFrom) : M S (Result E UInt64)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.Files.seek h communicate description offset = throw (Miri.Interpreter.StepError.unsupported "cannot seek this file description")