Actual source socket/FileDescription operation selection. Transient finish functions never enter storage; exact data environments select the portable source callback interpreter. Generic option ownership uses the same typed arena.

@[reducible, inline]

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

Equations

• Miri.Interpreter.OwnedSocketOperations.State = Miri.Interpreter.TypedSyncMachine.State

@[reducible, inline]

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

Equations

• Miri.Interpreter.OwnedSocketOperations.M = Miri.Interpreter.TypedSyncMachine.M

def Miri.Interpreter.OwnedSocketOperations.operations {U FH D O K E I R L T P H : Type} (v : OwnedSocketMachine.Views U (Files.Ref (Files.Description FH D O))) (descriptor : SocketMachine.Descriptor O) (virt : OwnedVirtualSocket.Hooks (State K U) (Files.Ref (Files.Description FH D O)) E I) (tcp : OwnedTcpSocket.Hooks (State K U) (Files.Ref (Files.Description FH D O)) R L T E P H I) (options : SocketOptions.Hooks (State K U) (Files.Ref (Files.Description FH D O)) E I) (resource : Nat) : Socket.Operations (State K U) (Files.Ref (Files.Description FH D O)) E

Equations

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

def Miri.Interpreter.OwnedSocketOperations.files {O K U FH D E I R L T P H Meta : Type} (descriptor : SocketMachine.Descriptor O) (virt : OwnedVirtualSocket.Hooks (State K U) (Files.Ref (Files.Description FH D O)) E I) (tcp : OwnedTcpSocket.Hooks (State K U) (Files.Ref (Files.Description FH D O)) R L T E P H I) (resource : Nat) (base : Files.Hooks (State K U) FH D O E Meta) : Files.Hooks (State K U) FH D O E Meta

Equations

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