Source tcp_socket.rs typed connect/send/receive/accept/peer callbacks. Host socket effects remain the exact typed source leaves in TcpSocket.Hooks. Callback data, ownership, retries, clock/readiness/order policy execute here.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.OwnedTcpSocket.Action (F : Type) : Type

• connect {F : Type} (fd : F) (finish : OwnedSocketCompletion.Connect) : Action F
• io {F : Type} (fd : F) (send : Bool) (deadline : Option Concurrency.ThreadDeadline) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (peek nonblock : Bool) (finish : OwnedSocketCompletion.Bytes) : Action F
• peer {F : Type} (fd : F) (finish : OwnedSocketCompletion.Peer) : Action F

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

• accept {F : Type} (fd : F) (nonblock : Bool) (finish : OwnedSocketCompletion.Accept) : Capture F
• io {F : Type} (fd : F) (send : Bool) (deadline : Option Concurrency.ThreadDeadline) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (peek : Bool) (finish : OwnedSocketCompletion.Bytes) : Capture F
• ensure {F : Type} (fd : F) (name : String) (action : Action F) : Capture F

structure Miri.Interpreter.OwnedTcpSocket.Hooks (S F R L T E P H I : Type) : Type

• source : TcpSocket.Hooks S F R L T E P H
• completion : OwnedSocketCompletion.Hooks S E I
• register : Capture F → M S Nat
• take : Nat → M S (Capture F)

def Miri.Interpreter.OwnedTcpSocket.dropAction {S F R L T E P H I : Type} (h : Hooks S F R L T E P H I) : Action F → M S Unit

Equations

• Miri.Interpreter.OwnedTcpSocket.dropAction h (Miri.Interpreter.OwnedTcpSocket.Action.connect fd finish) = Miri.Interpreter.OwnedTcpSocket.drop✝ h.source fd
• Miri.Interpreter.OwnedTcpSocket.dropAction h (Miri.Interpreter.OwnedTcpSocket.Action.io fd send deadline pointer length peek nonblock finish) = Miri.Interpreter.OwnedTcpSocket.drop✝ h.source fd
• Miri.Interpreter.OwnedTcpSocket.dropAction h (Miri.Interpreter.OwnedTcpSocket.Action.peer fd finish) = Miri.Interpreter.OwnedTcpSocket.drop✝ h.source fd

def Miri.Interpreter.OwnedTcpSocket.dropCapture {S F R L T E P H I : Type} (h : Hooks S F R L T E P H I) : Capture F → M S Unit

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.OwnedTcpSocket.dropCapture h (Miri.Interpreter.OwnedTcpSocket.Capture.accept fd nonblock finish) = Miri.Interpreter.OwnedTcpSocket.drop✝ h.source fd
• Miri.Interpreter.OwnedTcpSocket.dropCapture h (Miri.Interpreter.OwnedTcpSocket.Capture.io fd send deadline pointer length peek finish) = Miri.Interpreter.OwnedTcpSocket.drop✝ h.source fd

def Miri.Interpreter.OwnedTcpSocket.invoke {S F R L T E P H I : Type} : Nat → Hooks S F R L T E P H I → Capture F → Concurrency.UnblockKind → M S Unit

Equations

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

def Miri.Interpreter.OwnedTcpSocket.wait {S F R L T E P H I : Type} : Nat → Hooks S F R L T E P H I → Capture F → BlockingIo.Interest → Option Concurrency.ThreadDeadline → M S Unit

Equations

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

def Miri.Interpreter.OwnedTcpSocket.runAction {S F R L T E P H I : Type} : Nat → Hooks S F R L T E P H I → Action F → Bool → M S Unit

Equations

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

def Miri.Interpreter.OwnedTcpSocket.ensure {S F R L T E P H I : Type} : Nat → Hooks S F R L T E P H I → F → Option Concurrency.ThreadDeadline → String → Action F → M S Unit

Equations

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

def Miri.Interpreter.OwnedTcpSocket.accept {S F R L T E P H I : Type} (fuel : Nat) (h : Hooks S F R L T E P H I) (fd : F) (communicate nonblock : Bool) (finish : OwnedSocketCompletion.Accept) : M S Unit

Equations

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

def Miri.Interpreter.OwnedTcpSocket.connect {S F R L T E P H I : Type} (fuel : Nat) (h : Hooks S F R L T E P H I) (fd : F) (communicate : Bool) (address : SocketAddress.Address) (finish : OwnedSocketCompletion.Connect) : M S Unit

Equations

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

def Miri.Interpreter.OwnedTcpSocket.sendRecv {S F R L T E P H I : Type} (fuel : Nat) (h : Hooks S F R L T E P H I) (fd : F) (communicate send : Bool) (ptr : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (peek nonblock : Bool) (finish : OwnedSocketCompletion.Bytes) : M S Unit

Equations

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

def Miri.Interpreter.OwnedTcpSocket.peerName {S F R L T E P H I : Type} (fuel : Nat) (h : Hooks S F R L T E P H I) (fd : F) (communicate : Bool) (finish : OwnedSocketCompletion.Peer) : M S Unit

Equations

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