Persistent before_terminator state in the single actual World.host. Source Control is only a transient view: setter writes both persistent counters and the existing monotonic clock, preserving every other runtime field.

@[reducible, inline]

abbrev Miri.Input.EvalTerminatorMachine.Host (Poll Instant System H D O Native Profiler : Type) : Type

Equations

• Miri.Input.EvalTerminatorMachine.Host = Miri.Input.HostRuntime.Storage

@[reducible, inline]

abbrev Miri.Input.EvalTerminatorMachine.User (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalTerminatorMachine.State (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

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

structure Miri.Input.EvalTerminatorMachine.ControlAccess (H Clock : Type) : Type

Storage access for an opaque real host payload. Production HostRuntime uses the concrete accessor below; provenance/root traversal is never supplied by the host accessor.

• get : H → Interpreter.TerminatorMachine.Control Clock
• put : Interpreter.TerminatorMachine.Control Clock → H → H

structure Miri.Input.EvalTerminatorMachine.IoSourcesAccess (HostPayload : Type) : Type

• get : HostPayload → Array (Interpreter.Files.FdId × Interpreter.BlockingIo.Source)
• put : HostPayload → Array (Interpreter.Files.FdId × Interpreter.BlockingIo.Source) → HostPayload

def Miri.Input.EvalTerminatorMachine.ioGc {HostPayload Os R P H D O Aff B : Type} (sources : IoSourcesAccess HostPayload) : Interpreter.MachineHooks.M Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D O Aff B HostPayload) Unit

blocking_io.rs::run_gc retains exactly weak descriptions that are not closed. Liveness comes from the canonical ownership registry, not table slots or an independently supplied success callback.

Equations

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

def Miri.Input.EvalTerminatorMachine.genericHooks {HostPayload Clock Os R P H D O Aff B : Type} (control : ControlAccess HostPayload Clock) (blockingIoGc : Interpreter.MachineHooks.M Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D O Aff B HostPayload) Unit) : Interpreter.TerminatorMachine.Hooks Memory.MiriMemoryKind (EvalCoreMachine.User Os R P H D O Aff B HostPayload) Clock

Equations

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

def Miri.Input.EvalTerminatorMachine.getControl {Os R P H D O Aff B Poll Instant System Native Profiler : Type} (u : User Os R P H D O Aff B Poll Instant System Native Profiler) : Interpreter.TerminatorMachine.Control Instant

Equations

• Miri.Input.EvalTerminatorMachine.getControl u = Miri.Interpreter.TerminatorControl.view u.payload.payload.user.host.control u.payload.payload.user.host.clock

def Miri.Input.EvalTerminatorMachine.setControl {Instant Os R P H D O Aff B Poll System Native Profiler : Type} (control : Interpreter.TerminatorMachine.Control Instant) (u : User Os R P H D O Aff B Poll Instant System Native Profiler) : User Os R P H D O Aff B Poll Instant System Native Profiler

Equations

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

@[simp]

theorem Miri.Input.EvalTerminatorMachine.get_set {Instant Os R P H D O Aff B Poll System Native Profiler : Type} (control : Interpreter.TerminatorMachine.Control Instant) (u : User Os R P H D O Aff B Poll Instant System Native Profiler) : getControl (setControl control u) = control

def Miri.Input.EvalTerminatorMachine.controlAccess {Poll Instant System H D O Native Profiler : Type} : ControlAccess (Host Poll Instant System H D O Native Profiler) Instant

Equations

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

def Miri.Input.EvalTerminatorMachine.ioSourcesAccess {Poll Instant System H D O Native Profiler : Type} : IoSourcesAccess (Host Poll Instant System H D O Native Profiler)

Equations

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

def Miri.Input.EvalTerminatorMachine.hooks {Os R P H D O Aff B Poll Instant System Native Profiler : Type} (blockingIoGc : Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Unit) : Interpreter.TerminatorMachine.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Instant

Equations

• Miri.Input.EvalTerminatorMachine.hooks blockingIoGc = Miri.Input.EvalTerminatorMachine.genericHooks Miri.Input.EvalTerminatorMachine.controlAccess blockingIoGc

def Miri.Input.EvalTerminatorMachine.bind {Os R P H D O Aff B Poll Instant System Native Profiler C X : Type} (blockingIoGc : Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Unit) (base : Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) C O X Instant) : Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) C O X Instant

Production binding replaces all control storage callbacks with the actual source host state. The sole surviving operation is real blocking-I/O GC.

Equations

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