Canonical host-state projections used by deadlines/time shims. The actual host clock and callback dispatcher remain supplied effects; storage, thread selection and all source deadline transitions use one actual World.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalHostMachine.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.EvalHostMachine.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.

def Miri.Input.EvalHostMachine.deadlines {Instant System Os R P H D O Aff B Poll Native Profiler : Type} (clock : Interpreter.Clock.HostHooks Instant System (State Os R P H D O Aff B Poll Instant System Native Profiler)) (communicate : Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Bool) (systemDurationSince : System → System → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) (Option Interpreter.Clock.Duration)) (invokeCallback : Nat → Concurrency.UnblockKind → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Unit) : Interpreter.DeadlineMachine.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Poll Instant System Native Profiler) Instant System

Equations

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