Windows callback routing over the canonical Main state. Windows exit callbacks reuse Main/TLS, while FnOnce wake callbacks are selected from the single ThreadMachine token supply and dispatched to typed synchronization. Unix descriptor, futex-registry and socket callback records do not participate.

@[reducible, inline]

abbrev Miri.Input.EvalWindowsCallbackSourceConstruction.Payload (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalWindowsCallbackSourceConstruction.Payload Os R P H D O Aff B Host = Miri.Input.EvalWindowsFileConstruction.Payload Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalWindowsCallbackSourceConstruction.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalWindowsCallbackSourceConstruction.State Os R P H D O Aff B Host = Miri.Input.EvalWindowsFileConstruction.State Os R P H D O Aff B Host

@[reducible, inline]

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

structure Miri.Input.EvalWindowsCallbackSourceConstruction.Product (Os R P H D O Aff B Poll Instant System Native Profiler C X F A : Type) : Type 1

• main : Interpreter.MainMachine.Hooks (Payload Os R P H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler)) C O X F A Aff Interpreter.ProgramExitPoll
• exit : Interpreter.WindowsExitMachine.Hooks (User Os R P H D O Aff B Poll Instant System Native Profiler) C O X F A Aff Interpreter.ProgramExitPoll
• invoke : C → Nat → Concurrency.UnblockKind → EStateM Interpreter.StepError (State Os R P H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler)) Unit
• discard : Nat → EStateM Interpreter.StepError (State Os R P H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler)) Unit

def Miri.Input.EvalWindowsCallbackSourceConstruction.fromSource {Os TyId : Type} [DecidableEq Os] {R P H D O Aff B Poll Instant System Native Profiler C : Type} (main : Interpreter.MainMachine.Hooks (Payload Os R P H D O Aff B (HostRuntime.Storage Poll Instant System H D O Native Profiler)) C O ABI.ExternAbi (ABI.FnAbi TyId) (ABI.ArgAbi TyId) Aff Interpreter.ProgramExitPoll) (effects : Interpreter.TypedSyncMachine.Effects (EvalTypedSyncMachine.State Os R P H D O Aff B Poll Instant System Native Profiler)) : Except Interpreter.StepError (Product Os R P H D O Aff B Poll Instant System Native Profiler C ABI.ExternAbi (ABI.FnAbi TyId) (ABI.ArgAbi TyId))

Construct Main/TLS and ExitCalled callbacks and the FnOnce dispatcher from the actual Main hooks and typed synchronization effects. Callback storage and token ownership remain in their canonical World fields.

Equations

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