Source owned IO dictionaries on the actual outer ThreadStacks machine. Only the already proved full-state reassociation changes record nesting.

def Miri.Interpreter.OwnedIoTransport.event {U F K E : Type} (sync : TypedSyncMachine.Views U) (io : OwnedIoMachine.Views U F) (e : TypedSyncMachine.Effects (TypedSyncMachine.State K U)) (h : OwnedIoMachine.Operations (TypedSyncMachine.State K U) F E) : EventFd.Hooks (MachineHooks.State K (ExecutionStateTransport.Outer U)) F

Equations

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

def Miri.Interpreter.OwnedIoTransport.store {U O : Type} (h : EventFdMachine.Store (ExecutionStateTransport.Inner U) O) : EventFdMachine.Store (ExecutionStateTransport.Outer U) O

Equations

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