@[reducible, inline]

abbrev Miri.Input.EvalCallbackSocketConstruction.FD (H D O : Type) : Type

Equations

• Miri.Input.EvalCallbackSocketConstruction.FD H D O = Miri.Interpreter.Files.Ref (Miri.Interpreter.Files.Description H D O)

@[reducible, inline]

abbrev Miri.Input.EvalCallbackSocketConstruction.Other (Raw Listener TcpStream Error : Type) : Type

Equations

• Miri.Input.EvalCallbackSocketConstruction.Other Raw Listener TcpStream Error = Miri.Input.EvalUnixSourceConstruction.Other Raw Listener TcpStream Error

@[reducible, inline]

abbrev Miri.Input.EvalCallbackSocketConstruction.User (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalCallbackSocketConstruction.State (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalCallbackSocketConstruction.RegistryUser (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

The minimal file-description route for source event/socket operations.

structure Miri.Input.EvalCallbackSocketConstruction.SocketFileEffects (S H D O Error : Type) : Type

• read : FD H D O → Bool → Memory.Pointer (Option Memory.Provenance) → Nat → Interpreter.Files.Finish S Error → EStateM Interpreter.StepError S Unit
• write : FD H D O → Bool → Memory.Pointer (Option Memory.Provenance) → Nat → Interpreter.Files.Finish S Error → EStateM Interpreter.StepError S Unit
• readiness : O → EStateM Interpreter.StepError S (Option Interpreter.Files.Readiness)

structure Miri.Input.EvalCallbackSocketConstruction.HostEffects (S H D O Raw Listener TcpStream Error Poll AddrIter : Type) : Type 1

• newRaw : Interpreter.Socket.Family → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) Raw)

  Host socket creation and ownership transitions.

• nonblocking : Raw → Bool → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) Unit)
• dropRaw : Raw → EStateM Interpreter.StepError S Unit
• rawToListener : Raw → EStateM Interpreter.StepError S Listener
• rawToStream : Raw → EStateM Interpreter.StepError S TcpStream
• hostBind : Interpreter.TcpSocket.SocketState Raw Listener TcpStream → Interpreter.SocketAddress.Address → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) Unit)

  Host network operations. Address/state policy remains in TcpSocket.

• hostListen : Interpreter.TcpSocket.SocketState Raw Listener TcpStream → Int32 → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) Unit)
• hostConnect : Raw → Interpreter.SocketAddress.Address → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) Unit)
• hostAccept : Listener → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) (TcpStream × Interpreter.SocketAddress.Address))
• hostSend : TcpStream → ByteArray → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) Nat)
• hostRecv : TcpStream → Nat → Bool → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) ByteArray)
• hostLocal : Interpreter.TcpSocket.SocketState Raw Listener TcpStream → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) Interpreter.SocketAddress.Address)
• hostPeer : TcpStream → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) Interpreter.SocketAddress.Address)
• hostShutdown : TcpStream → Interpreter.Socket.Shutdown → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) Unit)
• hostTakeError : Interpreter.TcpSocket.SocketState Raw Listener TcpStream → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) (Option (Interpreter.IoError.HostError Error)))
• setHostOption : FD H D O → Interpreter.SocketOptions.HostOption → Interpreter.SocketOptions.Value → EStateM Interpreter.StepError S (Option (Except (Interpreter.IoError.HostError Error) Unit))

  Actual host option access. Timeout and SO_ERROR state transitions are built from the canonical TCP store and are intentionally absent here.

• getHostOption : FD H D O → Interpreter.SocketOptions.HostOption → EStateM Interpreter.StepError S (Option (Except (Interpreter.IoError.HostError Error) Interpreter.SocketOptions.Value))
• resolve : String → UInt16 → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) AddrIter)

  Host ToSocketAddrs iterator operations used by getaddrinfo.

• nextAddress : AddrIter → EStateM Interpreter.StepError S (Option (Interpreter.SocketAddress.Address × AddrIter))
• dropIterator : AddrIter → EStateM Interpreter.StepError S Unit
• resolutionDiagnostic : Interpreter.IoError.HostError Error → EStateM Interpreter.StepError S Unit
• deadline {ThreadDeadline : Type} : Option Interpreter.Clock.Duration → EStateM Interpreter.StepError S ThreadDeadline

  Host clock and one-time diagnostic capabilities used by TcpSocket.

• connectingNameWarningOnce : EStateM Interpreter.StepError S Unit
• edgeBackend : Bool

  Host profile fact from the selected runtime, independent of guest target.

• newPoll : EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) Poll)

  Raw host mio::Poll lifecycle. BlockingIo source/manager state is built from the canonical readiness and HostRuntime stores by the source binder.

• dropPoll : Poll → EStateM Interpreter.StepError S Unit
• registerHostSource : Poll → FD H D O → Interpreter.Files.FdId → Interpreter.BlockingIo.Interest → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) Unit)
• pollHost : Poll → Option Interpreter.Clock.Duration → Nat → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError Error) (Array Interpreter.BlockingIo.Event))

structure Miri.Input.EvalCallbackSocketConstruction.RegistrySeed (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

• files : Interpreter.FileMachine.Hooks Memory.MiriMemoryKind (RegistryUser Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)
• readiness : Interpreter.ReadinessMachine.Hooks Memory.MiriMemoryKind (RegistryUser Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)