Pinned unix/tcp_socket.rs. Raw/socket2, mio listener and stream ownership remain separate typed host resources. All portable state/readiness policy is here.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.TcpSocket.SocketState (Raw Listener Stream : Type) : Type

• initial {Raw Listener Stream : Type} (raw : Raw) : SocketState Raw Listener Stream
• listening {Raw Listener Stream : Type} (listener : Listener) : SocketState Raw Listener Stream
• connecting {Raw Listener Stream : Type} (stream : Stream) : SocketState Raw Listener Stream
• connected {Raw Listener Stream : Type} (stream : Stream) : SocketState Raw Listener Stream
• failed {Raw Listener Stream : Type} (stream : Stream) : SocketState Raw Listener Stream
• transition {Raw Listener Stream : Type} : SocketState Raw Listener Stream

structure Miri.Interpreter.TcpSocket.State (R L T E : Type) : Type

• family : Socket.Family
• socket : SocketState R L T
• nonblock : Bool
• bound : Bool
• ready : Files.Readiness
• error : Option (IoError.HostError E)
• readTimeout : Option Clock.Duration
• writeTimeout : Option Clock.Duration

structure Miri.Interpreter.TcpSocket.Hooks (S F R L T E Poll Host : Type) : Type

• io : BlockingIo.Hooks S F Poll Host
• get : F → M S (State R L T E)
• put : F → State R L T E → M S Unit
• cloneFd : F → M S F
• newFd : State R L T E → M S F
• insert : F → M S Int32
• os : String
• hostWindows : Bool
• hostEdgeBackend : Bool
• errors : IoError.Hooks S E
• newRaw : Socket.Family → M S (Except (IoError.HostError E) R)
• nonblocking : R → Bool → M S (Except (IoError.HostError E) Unit)
• dropRaw : R → M S Unit
• rawToListener : R → M S L
• rawToStream : R → M S T
• hostBind : SocketState R L T → SocketAddress.Address → M S (Except (IoError.HostError E) Unit)
• hostListen : SocketState R L T → Int32 → M S (Except (IoError.HostError E) Unit)
• hostConnect : R → SocketAddress.Address → M S (Except (IoError.HostError E) Unit)
• hostAccept : L → M S (Except (IoError.HostError E) (T × SocketAddress.Address))
• hostSend : T → ByteArray → M S (Except (IoError.HostError E) Nat)
• hostRecv : T → Nat → Bool → M S (Except (IoError.HostError E) ByteArray)
• hostLocal : SocketState R L T → M S (Except (IoError.HostError E) SocketAddress.Address)
• hostPeer : T → M S (Except (IoError.HostError E) SocketAddress.Address)
• hostShutdown : T → Socket.Shutdown → M S (Except (IoError.HostError E) Unit)
• hostTakeError : SocketState R L T → M S (Except (IoError.HostError E) (Option (IoError.HostError E)))
• readBytes : Memory.Pointer (Option Memory.Provenance) → Nat → M S ByteArray
• writeBytes : Memory.Pointer (Option Memory.Provenance) → ByteArray → M S Unit
• deadline : Option Clock.Duration → M S Concurrency.ThreadDeadline

  True -> actual monotonic now; false+duration -> now.add_lossy(duration).

• connectingNameWarningOnce : M S Unit
• wakeBudget : Nat

def Miri.Interpreter.TcpSocket.newSocket {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (family : Socket.Family) (nonblock : Bool) : M S (Except (IoError.HostError E) F)

Equations

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

def Miri.Interpreter.TcpSocket.ensureNotFailed {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (name : String) : M S Unit

Equations

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

def Miri.Interpreter.TcpSocket.updateLastError {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) : M S Unit

Equations

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

def Miri.Interpreter.TcpSocket.actionDeadline {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (nonblock : Bool) (timeout : Option Clock.Duration) : M S (Option Concurrency.ThreadDeadline)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.TcpSocket.actionDeadline h nonblock none = if nonblock = true then do let __do_lift ← h.deadline none pure (some __do_lift) else pure none

def Miri.Interpreter.TcpSocket.bind {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (communicate : Bool) (address : SocketAddress.Address) : M S (Files.Result E Unit)

Equations

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

def Miri.Interpreter.TcpSocket.listen {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (communicate : Bool) (backlog : Int32) : M S (Files.Result E Unit)

Equations

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

def Miri.Interpreter.TcpSocket.ensureConnected {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (deadline : Option Concurrency.ThreadDeadline) (name : String) (action : Bool → M S Unit) : M S Unit

Consumes one owner, preserving source's single readiness-based connection probe (no invented peer_addr probe and no spurious-wakeup retry).

Equations

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

def Miri.Interpreter.TcpSocket.accept {S F R L T E P H : Type} (budget : Nat) (h : Hooks S F R L T E P H) (fd : F) (communicate nonblock : Bool) (finish : Socket.Finish S E (Int32 × SocketAddress.Address)) : M S Unit

Equations

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

def Miri.Interpreter.TcpSocket.connect {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (communicate : Bool) (address : SocketAddress.Address) (finish : Socket.Finish S E Unit) : M S Unit

Equations

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

def Miri.Interpreter.TcpSocket.sendRecv {S F R L T E P H : Type} (budget : Nat) (h : Hooks S F R L T E P H) (fd : F) (communicate send : Bool) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (peek nonblock : Bool) (finish : Files.Finish S E) : M S Unit

Equations

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

def Miri.Interpreter.TcpSocket.localName {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (communicate : Bool) : M S (Files.Result E SocketAddress.Address)

Equations

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

def Miri.Interpreter.TcpSocket.peerName {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (communicate : Bool) (finish : Socket.Finish S E SocketAddress.Address) : M S Unit

Equations

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

def Miri.Interpreter.TcpSocket.shutdown {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (communicate : Bool) (how : Socket.Shutdown) : M S (Files.Result E Unit)

Equations

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

def Miri.Interpreter.TcpSocket.setTimeout {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (write : Bool) (timeout : Option Clock.Duration) : M S Unit

Equations

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

def Miri.Interpreter.TcpSocket.getTimeout {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (write : Bool) : M S (Option Clock.Duration)

Equations

• Miri.Interpreter.TcpSocket.getTimeout h fd write = do let value ← h.get fd pure (if write = true then value.writeTimeout else value.readTimeout)

def Miri.Interpreter.TcpSocket.takeError {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) : M S (Option (IoError.HostError E))

Equations

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

def Miri.Interpreter.TcpSocket.sourceState {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) : M S (SocketState R L T)

SourceFileDescription accepts only registered mio-backed socket states.

Equations

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

def Miri.Interpreter.TcpSocket.getFlags {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (libcI32 : String → M S Int32) : M S Int32

Equations

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

def Miri.Interpreter.TcpSocket.setFlags {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (libcI32 : String → M S Int32) (flags : Int32) : M S Int32

Equations

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

def Miri.Interpreter.TcpSocket.ioctl {S F R L T E P H : Type} (h : Hooks S F R L T E P H) (fd : F) (communicate : Bool) (operation : Memory.Scalar Memory.Provenance) (libc : String → M S (Memory.Scalar Memory.Provenance)) (readArgument : M S Int32) : M S Int32

Equations

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

def Miri.Interpreter.TcpSocket.name : String

Equations

• Miri.Interpreter.TcpSocket.name = "socket"

def Miri.Interpreter.TcpSocket.shortFdOperations : Bool

Equations

• Miri.Interpreter.TcpSocket.shortFdOperations = false