Canonical machine binding of descriptor tables and ownership. Pending I/O must retain/transfer actual references via these same operations. Host resource close and readiness destruction remain explicit last-drop effects.

structure Miri.Interpreter.FileMachine.Hooks (K U H D O : Type) : Type

• table : U → Files.Table (Files.Description H D O)
• setTable : Files.Table (Files.Description H D O) → U → U
• ownership : U → FileOwnership.Registry (Files.Description H D O)
• setOwnership : FileOwnership.Registry (Files.Description H D O) → U → U
• hostUsizeBits : Nat
• referenceBudget : Nat
• onLastDrop : Files.Description H D O → MachineHooks.M K U Unit

def Miri.Interpreter.FileMachine.newReference {K U H D O : Type} (h : Hooks K U H D O) (value : Files.Description H D O) : MachineHooks.M K U (Files.Ref (Files.Description H D O))

Equations

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

def Miri.Interpreter.FileMachine.cloneReference {K U H D O : Type} (h : Hooks K U H D O) (ref : Files.Ref (Files.Description H D O)) : MachineHooks.M K U (Files.Ref (Files.Description H D O))

Equations

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

def Miri.Interpreter.FileMachine.dropReference {K U H D O : Type} (h : Hooks K U H D O) (ref : Files.Ref (Files.Description H D O)) : MachineHooks.M K U Unit

Equations

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

def Miri.Interpreter.FileMachine.upgradeWeak {K U H D O : Type} (h : Hooks K U H D O) (weak : Files.WeakRef) : MachineHooks.M K U (Option (Files.Ref (Files.Description H D O)))

Equations

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

def Miri.Interpreter.FileMachine.bind {K U H D O E Meta : Type} (h : Hooks K U H D O) (base : UnixFd.Hooks (MachineHooks.State K U) H D O E Meta) : UnixFd.Hooks (MachineHooks.State K U) H D O E Meta

Equations

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

def Miri.Interpreter.FileMachine.init {K U H D O : Type} (h : Hooks K U H D O) (mute : Bool) : MachineHooks.M K U Unit

Equations

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