One positive source callback sum for all owned IO families. Old source IO adapters use a filtered value view, whose setter preserves every other family from the current canonical store. No shadow store or counter is allocated. Callback lookup/take is by unique token; array order is not observed.

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

• io {F : Type} (value : OwnedIoRuntime.Capture F) : Capture F
• virtual {F : Type} (value : OwnedVirtualSocket.Capture F) : Capture F
• tcp {F : Type} (value : OwnedTcpSocket.Capture F) : Capture F
• owner {F : Type} (fd : F) : Capture F

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

• callbacks : Array (Nat × Capture F)

def Miri.Interpreter.OwnedIoStore.base {F : Type} (s : Storage F) : OwnedIoRuntime.Storage F

Equations

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

def Miri.Interpreter.OwnedIoStore.putBase {F : Type} (s : Storage F) (value : OwnedIoRuntime.Storage F) : Storage F

Equations

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