unix/socket.rs syscall protocol. Descriptor operations consume owned refs; concrete TCP/virtual implementations provide real state transitions/callbacks.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.Socket.Family : Type

• ipv4 : Family
• ipv6 : Family

@[instance_reducible]

instance Miri.Interpreter.Socket.instDecidableEqFamily : DecidableEq Family

Equations

• Miri.Interpreter.Socket.instDecidableEqFamily x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.Socket.instReprFamily.repr : Family → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Socket.instReprFamily : Repr Family

Equations

• Miri.Interpreter.Socket.instReprFamily = { reprPrec := Miri.Interpreter.Socket.instReprFamily.repr }

inductive Miri.Interpreter.Socket.Shutdown : Type

• read : Shutdown
• write : Shutdown
• both : Shutdown

@[instance_reducible]

instance Miri.Interpreter.Socket.instDecidableEqShutdown : DecidableEq Shutdown

Equations

• Miri.Interpreter.Socket.instDecidableEqShutdown x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.Socket.instReprShutdown : Repr Shutdown

Equations

• Miri.Interpreter.Socket.instReprShutdown = { reprPrec := Miri.Interpreter.Socket.instReprShutdown.repr }

def Miri.Interpreter.Socket.instReprShutdown.repr : Shutdown → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev Miri.Interpreter.Socket.Finish (S E A : Type) : Type

Equations

• Miri.Interpreter.Socket.Finish = Miri.Interpreter.OwnedSocketCompletion.Finish

structure Miri.Interpreter.Socket.Operations (S F E : Type) : Type

• bind : F → Bool → SocketAddress.Address → M S (Files.Result E Unit)
• listen : F → Bool → Int32 → M S (Files.Result E Unit)
• accept : F → Bool → Bool → Finish S E (Int32 × SocketAddress.Address) → M S Unit
• connect : F → Bool → SocketAddress.Address → Finish S E Unit → M S Unit
• send : F → Bool → Memory.Pointer (Option Memory.Provenance) → Nat → Bool → Finish S E Nat → M S Unit
• recv : F → Bool → Memory.Pointer (Option Memory.Provenance) → Nat → Bool → Bool → Finish S E Nat → M S Unit
• setOption : F → Int32 → Int32 → Memory.Pointer (Option Memory.Provenance) → UInt64 → M S (Files.Result E Unit)
• getOption : F → Int32 → Int32 → M S (Files.Result E (MPlaceTy Memory.Provenance))
• localName : F → Bool → M S (Files.Result E SocketAddress.Address)
• peerName : F → Bool → Finish S E SocketAddress.Address → M S Unit
• shutdown : F → Bool → Shutdown → M S (Files.Result E Unit)

structure Miri.Interpreter.Socket.Hooks (S F E I : Type) : Type

• address : SocketAddress.Hooks S E I
• operations : Operations S F E
• os : String
• communicate : Bool
• isolationReject : String → M S Bool
• readI32 : OpTy Memory.Provenance → M S Int32
• readSizeT : OpTy Memory.Provenance → M S Nat
• lookupFd : Int32 → M S (Option F)
• asSocket : F → M S Bool

  as_unix then checked as_socket, preserving actual same owned description.

• dropFd : F → M S Unit
• newTcp : Family → Bool → M S (Except (IoError.HostError E) F)
• insert : F → M S Int32
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• readLengthPlace : MPlaceTy Memory.Provenance → M S Nat

def Miri.Interpreter.Socket.create {S F E I : Type} (h : Hooks S F E I) (domain kind protocol : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.Socket.bind {S F E I : Type} (h : Hooks S F E I) (number address length : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.Socket.listen {S F E I : Type} (h : Hooks S F E I) (number backlog : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.Socket.accept4 {S F E I : Type} (h : Hooks S F E I) (number address length : OpTy Memory.Provenance) (flags : Option (OpTy Memory.Provenance)) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.Socket.connect {S F E I : Type} (h : Hooks S F E I) (number address length : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.Socket.sendRecv {S F E I : Type} (h : Hooks S F E I) (send : Bool) (number buffer length flags : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.Socket.setOption {S F E I : Type} (h : Hooks S F E I) (number level option value length : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.Socket.getOption {S F E I : Type} (h : Hooks S F E I) (number level option value length : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.Socket.localName {S F E I : Type} (h : Hooks S F E I) (number address length : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.Socket.peerName {S F E I : Type} (h : Hooks S F E I) (number address length : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.Socket.shutdown {S F E I : Type} (h : Hooks S F E I) (number how : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.Socket.unsupportedOperations {F S E : Type} (drop : F → M S Unit) : Operations S F E

Trait default implementations reject every operation. In particular a virtual socket does not inherit successful TCP options, bind or shutdown.

Equations

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