Source-owned IO FnOnce environments. This first connected unit executes all eventfd retry bodies without recursive function-valued state or a retry budget. Poll/epoll environments retain their exact source identities and are reserved for their connected source adapters.

@[reducible, inline]

abbrev Miri.Interpreter.OwnedIoRuntime.M (σ α : Type) : Type

Equations

• Miri.Interpreter.OwnedIoRuntime.M = EStateM Miri.Interpreter.StepError

inductive Miri.Interpreter.OwnedIoRuntime.Capture (F : Type) : Type

• eventRead {F : Type} (fd : F) (buffer : IoCompletion.Dest) (finish : IoCompletion.Capture) : Capture F
• eventWrite {F : Type} (num : UInt64) (fd : F) (buffer : IoCompletion.Dest) (finish : IoCompletion.Capture) : Capture F
• poll {F : Type} (watcher : Nat) (interests : Array (Int32 × IoCompletion.Dest)) (dest : IoCompletion.Dest) : Capture F
• epoll {F : Type} (fd : F) (event dest : IoCompletion.Dest) : Capture F

structure Miri.Interpreter.OwnedIoRuntime.Storage (F : Type) : Type

• callbacks : Array (Nat × Capture F)

structure Miri.Interpreter.OwnedIoRuntime.Hooks (S F E : Type) : Type

• event : EventFd.PhysicalHooks S F
• completion : IoCompletion.Hooks S E
• errorFromKind : IoError.ErrorKind → M S (IoError.Error E)
• register : Capture F → M S Nat
• take : Nat → M S (Capture F)
• dropWatcher : Nat → M S Unit
• pollReady : Nat → Array (Int32 × IoCompletion.Dest) → M S UInt32

  Source write_ready_events, not an arbitrary completion callback.

• writeU32 : UInt32 → IoCompletion.Dest → M S Unit
• epollReady : F → IoCompletion.Dest → IoCompletion.Dest → M S Nat
• epollRemoveBlocked : F → Concurrency.ThreadId → M S Unit

def Miri.Interpreter.OwnedIoRuntime.dropCapture {S F E : Type} (h : Hooks S F E) : Capture F → M S Unit

Equations

• Miri.Interpreter.OwnedIoRuntime.dropCapture h (Miri.Interpreter.OwnedIoRuntime.Capture.eventRead fd buffer finish) = h.event.dropFd fd
• Miri.Interpreter.OwnedIoRuntime.dropCapture h (Miri.Interpreter.OwnedIoRuntime.Capture.eventWrite num fd buffer finish) = h.event.dropFd fd
• Miri.Interpreter.OwnedIoRuntime.dropCapture h (Miri.Interpreter.OwnedIoRuntime.Capture.epoll fd event dest) = h.event.dropFd fd
• Miri.Interpreter.OwnedIoRuntime.dropCapture h (Miri.Interpreter.OwnedIoRuntime.Capture.poll watcher interests dest) = h.dropWatcher watcher

def Miri.Interpreter.OwnedIoRuntime.cancel {S F E : Type} (h : Hooks S F E) (token : Nat) : M S Unit

Equations

• Miri.Interpreter.OwnedIoRuntime.cancel h token = do let __do_lift ← h.take token Miri.Interpreter.OwnedIoRuntime.dropCapture h __do_lift

def Miri.Interpreter.OwnedIoRuntime.block {S F E : Type} (h : Hooks S F E) (capture : Capture F) (reason : Concurrency.BlockReason) (deadline : Option Concurrency.ThreadDeadline) : M S Unit

Equations

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

def Miri.Interpreter.OwnedIoRuntime.readStep {S F E : Type} (h : Hooks S F E) (fd : F) (buffer : IoCompletion.Dest) (completion : IoCompletion.Capture) : M S Unit

Takes source ownership of fd. A deferred callback receives that ownership without a clone/drop detour; immediate completion and failures drop it once.

Equations

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

def Miri.Interpreter.OwnedIoRuntime.writeStep {S F E : Type} (h : Hooks S F E) (fd : F) (buffer : IoCompletion.Dest) (completion : IoCompletion.Capture) : M S Unit

Equations

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

def Miri.Interpreter.OwnedIoRuntime.invoke {S F E : Type} (h : Hooks S F E) (token : Nat) (kind : Concurrency.UnblockKind) : M S Unit

Source call consumes Box<Self> first. Each arm owns its captured strong reference, including every error path; retries transfer it into the next box.

Equations

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