All socket.rs generic/IP/TCP option helpers. Host options are typed effects; absence of a SockRef produces Unsupported, never an accepted option.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.SocketOptions.HostOption : Type

• reuse : HostOption
• linger : HostOption
• keepalive : HostOption
• ttl : HostOption
• nodelay : HostOption

@[instance_reducible]

instance Miri.Interpreter.SocketOptions.instDecidableEqHostOption : DecidableEq HostOption

Equations

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

def Miri.Interpreter.SocketOptions.instReprHostOption.repr : HostOption → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.SocketOptions.instReprHostOption : Repr HostOption

Equations

• Miri.Interpreter.SocketOptions.instReprHostOption = { reprPrec := Miri.Interpreter.SocketOptions.instReprHostOption.repr }

inductive Miri.Interpreter.SocketOptions.Value : Type

• boolean (value : Bool) : Value
• linger (value : Option Clock.Duration) : Value
• ttl (value : UInt32) : Value

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

• address : SocketAddress.Hooks S E I
• os : String
• i32Layout : M S LocalLayout
• u32Layout : M S LocalLayout
• readI32 : MPlaceTy Memory.Provenance → M S Int32
• readTimeval : MPlaceTy Memory.Provenance → M S (Option Clock.Duration)
• setTimeout : F → Bool → Option Clock.Duration → M S Unit
• getTimeout : F → Bool → M S (Option Clock.Duration)
• takeError : F → M S (Option (IoError.HostError E))
• setHost : F → HostOption → Value → M S (Option (Except (IoError.HostError E) Unit))
• getHost : F → HostOption → M S (Option (Except (IoError.HostError E) Value))

def Miri.Interpreter.SocketOptions.setGeneric {S F E I : Type} (h : Hooks S F E I) (socket : F) (option : Int32) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : UInt64) : M S (Files.Result E Unit)

Equations

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

def Miri.Interpreter.SocketOptions.setIp {S F E I : Type} (h : Hooks S F E I) (socket : F) (option : Int32) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : UInt64) : M S (Files.Result E Unit)

Equations

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

def Miri.Interpreter.SocketOptions.setTcp {S F E I : Type} (h : Hooks S F E I) (socket : F) (option : Int32) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : UInt64) : M S (Files.Result E Unit)

Equations

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

def Miri.Interpreter.SocketOptions.getGeneric {S F E I : Type} (h : Hooks S F E I) (socket : F) (option : Int32) : M S (Files.Result E (MPlaceTy Memory.Provenance))

Equations

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

def Miri.Interpreter.SocketOptions.getIp {S F E I : Type} (h : Hooks S F E I) (socket : F) (option : Int32) : M S (Files.Result E (MPlaceTy Memory.Provenance))

Equations

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

def Miri.Interpreter.SocketOptions.getTcp {S F E I : Type} (h : Hooks S F E I) (socket : F) (option : Int32) : M S (Files.Result E (MPlaceTy Memory.Provenance))

Equations

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