Source construction for Unix socket address memory operations. Compiler layouts/constants, pointer access, allocation, projection, byte IO, and provenance-aware copies come from one canonical EnvironmentMemory bundle. The only residual effects are host address resolution and its iterator lifecycle.

@[reducible, inline]

abbrev Miri.Input.EvalSocketAddressConstruction.RuntimeState (U : Type) : Type

Equations

• Miri.Input.EvalSocketAddressConstruction.RuntimeState U = Miri.Input.EvalHostRuntimeConstruction.RuntimeState U

@[reducible, inline]

abbrev Miri.Input.EvalSocketAddressConstruction.RuntimeM (U A : Type) : Type

Equations

• Miri.Input.EvalSocketAddressConstruction.RuntimeM U A = Miri.Input.EvalHostRuntimeConstruction.RuntimeM U A

structure Miri.Input.EvalSocketAddressConstruction.HostEffects (S E Iterator : Type) : Type

• resolve : String → UInt16 → EStateM Interpreter.StepError S (Except (Interpreter.IoError.HostError E) Iterator)
• nextAddress : Iterator → EStateM Interpreter.StepError S (Option (Interpreter.SocketAddress.Address × Iterator))
• dropIterator : Iterator → EStateM Interpreter.StepError S Unit
• resolutionDiagnostic : Interpreter.IoError.HostError E → EStateM Interpreter.StepError S Unit
• listBudget : Nat

def Miri.Input.EvalSocketAddressConstruction.fromSource {Stored C Payload E Iterator : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (Interpreter.ValidityMachine.Control Stored) C Payload) (errors : Interpreter.IoError.Hooks (RuntimeState (Interpreter.ValidityMachine.Control Stored)) E) (host : HostEffects (RuntimeState (Interpreter.ValidityMachine.Control Stored)) E Iterator) : Except Interpreter.StepError (Interpreter.SocketAddress.Hooks (RuntimeState (Interpreter.ValidityMachine.Control Stored)) E Iterator)

Build all guest-side address operations from the selected execution's canonical memory. errors is the already-built errno machine belonging to the same callback state; resolver effects are the only host-specific inputs.

Equations

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

def Miri.Input.EvalSocketAddressConstruction.callbackFromSource {Os R H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler C AddrIter : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored Os R EvalSyncObjectAccess.Payload H D (EvalSocketStorage.Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (EvalSocketStorage.Other Raw Listener TcpStream Error) Native Profiler))) C EvalSyncObjectAccess.Payload) (errors : Interpreter.IoError.Hooks (EvalSocketStorage.State Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error) (host : HostEffects (EvalSocketStorage.State Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error AddrIter) : Except Interpreter.StepError (Interpreter.SocketAddress.Hooks (EvalSocketStorage.State Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error AddrIter)

Build socket-address hooks for callback IO from the same EvalWorld memory bundle used by Core. The explicit Stored specialization is important: RuntimeState (Control (Stored ...)) reduces to the callback's canonical inner state, so pointer provenance, allocation effects, and partially updated error states are already in the required state representation. No alternate memory lens or synthetic transport state is introduced.

Equations

• Miri.Input.EvalSocketAddressConstruction.callbackFromSource p memory errors host = Miri.Input.EvalSocketAddressConstruction.fromSource p memory errors host