Source virtual_socket.rs read/write retry execution with exact data captures. Uses the existing canonical socket buffers, clock policies and readiness state. Future retries are queued environments, not recursive closure calls or fuel.

@[reducible, inline]

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

Equations

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

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

• read {F : Type} (socket : F) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (nonblock : Bool) (finish : OwnedSocketCompletion.Bytes) : Capture F
• write {F : Type} (socket : F) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (nonblock : Bool) (finish : OwnedSocketCompletion.Bytes) : Capture F

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

• source : VirtualSocket.Hooks S F E
• completion : OwnedSocketCompletion.Hooks S E Iter
• register : Capture F → M S Nat
• take : Nat → M S (Capture F)

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

Equations

• Miri.Interpreter.OwnedVirtualSocket.dropCapture h (Miri.Interpreter.OwnedVirtualSocket.Capture.read fd pointer length nonblock finish) = h.source.readiness.dropFd fd
• Miri.Interpreter.OwnedVirtualSocket.dropCapture h (Miri.Interpreter.OwnedVirtualSocket.Capture.write fd pointer length nonblock finish) = h.source.readiness.dropFd fd

def Miri.Interpreter.OwnedVirtualSocket.write {S F E I : Type} (h : Hooks S F E I) (socket : F) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (nonblock : Bool) (finish : OwnedSocketCompletion.Bytes) : M S Unit

Equations

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

def Miri.Interpreter.OwnedVirtualSocket.read {S F E I : Type} (h : Hooks S F E I) (socket : F) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (nonblock : Bool) (finish : OwnedSocketCompletion.Bytes) : M S Unit

Equations

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

def Miri.Interpreter.OwnedVirtualSocket.invoke {S F E I : Type} (h : Hooks S F E I) (capture : Capture F) (reason : Concurrency.UnblockKind) : M S Unit

The canonical dispatcher has already consumed Box<Self> before this call.

Equations

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