Full state reassociation for source socket operations. Finish captures retain exact environments, and transient bodies are translated in the inverse direction. No callbacks or additional roots are installed by this transport.
def
Miri.Interpreter.OwnedSocketTransport.socket
{K U F E I : Type}
(h : Socket.Hooks (TypedSyncMachine.State K U) F E I)
(base : Socket.Hooks (MachineHooks.State K (ExecutionStateTransport.Outer U)) F E I)
:
Socket.Hooks (MachineHooks.State K (ExecutionStateTransport.Outer U)) F E I
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.OwnedSocketTransport.readiness
{K U F : Type}
(h : Readiness.Hooks (TypedSyncMachine.State K U) F)
(runtime :
Concurrency.SyncRuntime.Hooks (MachineHooks.State K (ExecutionStateTransport.Outer U)) Nat Int32
(MPlaceTy Memory.Provenance))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.OwnedSocketTransport.virtual
{K U F E : Type}
(h : VirtualSocket.Hooks (TypedSyncMachine.State K U) F E)
(runtime :
Concurrency.SyncRuntime.Hooks (MachineHooks.State K (ExecutionStateTransport.Outer U)) Nat Int32
(MPlaceTy Memory.Provenance))
(base : VirtualSocket.Hooks (MachineHooks.State K (ExecutionStateTransport.Outer U)) F E)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.OwnedSocketTransport.files
{K U H D O E Meta : Type}
(h : Files.Hooks (TypedSyncMachine.State K U) H D O E Meta)
(base : Files.Hooks (MachineHooks.State K (ExecutionStateTransport.Outer U)) H D O E Meta)
:
Files.Hooks (MachineHooks.State K (ExecutionStateTransport.Outer U)) H D O E Meta
Equations
- One or more equations did not get rendered due to their size.