Existing IO hooks use Nat for source host synchronization references. This lawful representation view uses the same arena indices, not a second object or callback store. Dynamic source object kinds remain checked by that arena.

def Miri.Interpreter.TypedSyncNat.runtime {U K : Type} (v : TypedSyncMachine.Views U) (e : TypedSyncMachine.Effects (TypedSyncMachine.State K U)) : Concurrency.SyncRuntime.Hooks (TypedSyncMachine.State K U) Nat Int32 Concurrency.TypedSyncRuntime.Dest

Equations

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

def Miri.Interpreter.TypedSyncNat.routed {U K : Type} (v : TypedSyncMachine.Views U) (e : TypedSyncMachine.Effects (TypedSyncMachine.State K U)) (run : Nat → Concurrency.UnblockKind → TypedSyncMachine.M K U Unit) : Concurrency.SyncRuntime.Hooks (TypedSyncMachine.State K U) Nat Int32 Concurrency.TypedSyncRuntime.Dest

Canonical Nat representation with the terminal source dispatcher installed before any wake closure captures it. Registration/cancellation stay in the one typed sync arena; no legacy branch is inspected or inherited.

Equations

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

def Miri.Interpreter.TypedSyncNat.outward {U K : Type} (v : TypedSyncMachine.Views U) (e : TypedSyncMachine.Effects (TypedSyncMachine.State K U)) : Concurrency.SyncRuntime.Hooks (MachineHooks.State K (ExecutionStateTransport.Outer U)) Nat Int32 Concurrency.TypedSyncRuntime.Dest

Equations

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