Authoritative readiness state embedded in the existing canonical machine User, sharing actual FileOwnership references and complete thread-stack views.

structure Miri.Interpreter.ReadinessMachine.WatcherEntry : Type

• id : Nat
• strong : Nat
• value : Readiness.Watcher

structure Miri.Interpreter.ReadinessMachine.Registry (F : Type) : Type

• nextWatcher : Nat
• watchers : Array WatcherEntry
• watched : Array (Files.FdId × Readiness.Watched)
• delayed : Array F

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

• files : FileMachine.Hooks K U H D O
• registry : U → Registry (Files.Ref (Files.Description H D O))
• setRegistry : Registry (Files.Ref (Files.Description H D O)) → U → U
• watcherReferenceBudget : Nat
• onLastDrop : Files.Ref (Files.Description H D O) → MachineHooks.M K U Unit

  Actual description destructor with ID retained. It must run watched-field cleanup at that source type's field-drop point, then actual host/resource destruction; separate FD types may have additional delayed updates.

def Miri.Interpreter.ReadinessMachine.newWatcher {K U H D O : Type} (h : Hooks K U H D O) : MachineHooks.M K U Nat

Equations

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

def Miri.Interpreter.ReadinessMachine.upgradeWatcher {K U H D O : Type} (h : Hooks K U H D O) (id : Nat) : MachineHooks.M K U Bool

Equations

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

def Miri.Interpreter.ReadinessMachine.dropFd {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

ID-aware release for source ReadinessWatched::drop. Weak liveness is updated first, so the destructor sees this description as closed.

Equations

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

def Miri.Interpreter.ReadinessMachine.dropWatcher {K U H D O : Type} (h : Hooks K U H D O) (base : Readiness.Hooks (MachineHooks.State K U) (Files.Ref (Files.Description H D O))) (id : Nat) : MachineHooks.M K U Unit

Equations

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

def Miri.Interpreter.ReadinessMachine.bind {K U H D O : Type} (h : Hooks K U H D O) (base : Readiness.Hooks (MachineHooks.State K U) (Files.Ref (Files.Description H D O))) : Readiness.Hooks (MachineHooks.State 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.ReadinessMachine.initWatched {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

Called when a description containing ReadinessWatched is constructed. Absent metadata is never silently treated as an empty, valid watch set.

Equations

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

def Miri.Interpreter.ReadinessMachine.bindThreadStacks {K U F : Type} (base : Readiness.Hooks (ThreadStacks.State K U) F) : Readiness.Hooks (ThreadStacks.State K U) F

The true source ThreadStacks switch wraps actual typed callback execution; SyncRuntime's token registry is not used as a successful acknowledgment.

Equations

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

structure Miri.Interpreter.ReadinessMachine.BlockingStore (U Poll : Type) : Type

• get : U → BlockingIo.Manager Poll
• put : BlockingIo.Manager Poll → U → U

def Miri.Interpreter.ReadinessMachine.bindBlocking {K U H D O Poll Host : Type} (h : Hooks K U H D O) (store : BlockingStore U Poll) (base : BlockingIo.Hooks (MachineHooks.State K U) (Files.Ref (Files.Description H D O)) Poll Host) : BlockingIo.Hooks (MachineHooks.State K U) (Files.Ref (Files.Description H D O)) Poll Host

Equations

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

def Miri.Interpreter.ReadinessMachine.bindBlockingThreadStacks {K U F Poll Host : Type} (base : BlockingIo.Hooks (ThreadStacks.State K U) F Poll Host) : BlockingIo.Hooks (ThreadStacks.State K U) F Poll Host

Equations

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

def Miri.Interpreter.ReadinessMachine.bindScheduling {K U F Poll Host : Type} (budget : Nat) (io : BlockingIo.Hooks (ThreadStacks.State K U) F Poll Host) (base : ThreadStacks.LocalSchedulerHooks K U) : ThreadStacks.LocalSchedulerHooks K U

Equations

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

def Miri.Interpreter.ReadinessMachine.destroyWatched {K U H D O : Type} (h : Hooks K U H D O) (base : Readiness.Hooks (MachineHooks.State K U) (Files.Ref (Files.Description H D O))) (ref : Files.Ref (Files.Description H D O)) : MachineHooks.M K U Unit

Call at the actual ReadinessWatched field-drop point of a description. The ID-aware outer release has already made weak FD upgrades fail.

Equations

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

def Miri.Interpreter.ReadinessMachine.cloneWatcher {K U H D O : Type} (h : Hooks K U H D O) (id : Nat) : MachineHooks.M K U Unit

Equations

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

def Miri.Interpreter.ReadinessMachine.newFd {K U H D O : Type} (h : Hooks K U H D O) (supportsWatching : Files.Description H D O → Bool) (description : 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.ReadinessMachine.bindFiles {K U H D O E Meta : Type} (h : Hooks K U H D O) (readiness : Readiness.Hooks (MachineHooks.State K U) (Files.Ref (Files.Description 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.ReadinessMachine.bindUnixDispatch {K U F Poll Host H D O E Meta Path : Type} (budget : Nat) (io : BlockingIo.Hooks (MachineHooks.State K U) F Poll Host) (base : UnixFdDispatch.Hooks (MachineHooks.State K U) H D O E Meta Path) : UnixFdDispatch.Hooks (MachineHooks.State K U) H D O E Meta Path

Equations

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