Explicit Rc/Weak lifetime state for file descriptions, including references held by pending callbacks. Table slot counts alone never determine liveness.

structure Miri.Interpreter.FileOwnership.Entry (D : Type) : Type

• ref : Files.Ref D
• strong : Nat

structure Miri.Interpreter.FileOwnership.Registry (D : Type) : Type

• entries : Array (Entry D)

def Miri.Interpreter.FileOwnership.register {D : Type} (state : Registry D) (ref : Files.Ref D) : Except StepError (Registry D)

Equations

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

def Miri.Interpreter.FileOwnership.retain {D : Type} (state : Registry D) (id : Files.FdId) (referenceBudget : Nat) : Except StepError (Registry D × Files.Ref D)

Equations

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

def Miri.Interpreter.FileOwnership.release {D : Type} (state : Registry D) (id : Files.FdId) : Except StepError (Registry D × Option D)

Last release returns the real payload for destructor/readiness cleanup. The runtime must execute that cleanup; this function does not fake host close.

Equations

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

def Miri.Interpreter.FileOwnership.upgrade {D : Type} (state : Registry D) (weak : Files.WeakRef) (referenceBudget : Nat) : Except StepError (Registry D × Option (Files.Ref D))

Equations

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

def Miri.Interpreter.FileOwnership.isClosed {D : Type} (state : Registry D) (weak : Files.WeakRef) : Bool

Equations

• Miri.Interpreter.FileOwnership.isClosed state weak = !state.entries.any fun (entry : Miri.Interpreter.FileOwnership.Entry D) => entry.ref.id == weak.id && decide (entry.strong > 0)

def Miri.Interpreter.FileOwnership.downgrade {D : Type} (ref : Files.Ref D) : Files.WeakRef

Equations

• Miri.Interpreter.FileOwnership.downgrade ref = { id := ref.id }