Single canonical owned-IO store and token supply for TCP and virtual socket callbacks. Every take consumes source FnOnce data before invoking its body.

@[reducible, inline]

abbrev Miri.Interpreter.OwnedSocketMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.OwnedSocketMachine.State = Miri.Interpreter.TypedSyncMachine.State

@[reducible, inline]

abbrev Miri.Interpreter.OwnedSocketMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.OwnedSocketMachine.M = Miri.Interpreter.TypedSyncMachine.M

structure Miri.Interpreter.OwnedSocketMachine.Views (U F : Type) : Type

• storage : U → OwnedIoStore.Storage F
• putStorage : U → OwnedIoStore.Storage F → U
• nextCallback : U → Nat
• putNextCallback : U → Nat → U

def Miri.Interpreter.OwnedSocketMachine.register {U F K : Type} (v : Views U F) (capture : OwnedIoStore.Capture F) : M K U Nat

Equations

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

def Miri.Interpreter.OwnedSocketMachine.lookup {U F K : Type} (v : Views U F) (token : Nat) : M K U (Option (OwnedIoStore.Capture F))

Equations

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

def Miri.Interpreter.OwnedSocketMachine.take {U F K : Type} (v : Views U F) (token : Nat) : M K U (OwnedIoStore.Capture F)

Equations

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

def Miri.Interpreter.OwnedSocketMachine.virtual {U F K E I : Type} (v : Views U F) (source : VirtualSocket.Hooks (State K U) F E) (completion : OwnedSocketCompletion.Hooks (State K U) E I) : OwnedVirtualSocket.Hooks (State K U) F E I

Equations

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

def Miri.Interpreter.OwnedSocketMachine.tcp {U F K R L T E P H I : Type} (v : Views U F) (source : TcpSocket.Hooks (State K U) F R L T E P H) (completion : OwnedSocketCompletion.Hooks (State K U) E I) : OwnedTcpSocket.Hooks (State K U) F R L T E P H I

Equations

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

def Miri.Interpreter.OwnedSocketMachine.invoke {U F K E I R L T P H : Type} (v : Views U F) (virt : OwnedVirtualSocket.Hooks (State K U) F E I) (tcp : OwnedTcpSocket.Hooks (State K U) F R L T E P H I) (resource token : Nat) (kind : Concurrency.UnblockKind) : M K U Bool

None means this token belongs to another actual source family. IO callbacks are not treated as synchronization callbacks and are never silently completed.

Equations

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