Assemble source-built Unix environment and poll fields over the actual EvalWorld machine. This is a component bundle, not a caller-supplied UnixForeign.Hooks: the environment and poll policies are constructed here, while file/readiness and native blocking-I/O effects remain separate typed boundaries for their own source constructors.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixSourceConstruction.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.EvalUnixSourceConstruction.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.EvalUnixSourceConstruction.Stored (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.EvalUnixSourceConstruction.Control (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.EvalUnixSourceConstruction.FD (H D O : Type) : Type

Equations

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

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

• environment : Interpreter.UnixEnvironmentDispatch.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Os Error Interpreter.EnvVars.Kind
• poll : Interpreter.PollDispatch.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) EvalUnixFdConstruction.ArrayCursor

structure Miri.Input.EvalUnixSourceConstruction.DispatchComponents (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path Place C ClockHost I : Type) : Type

Source-built entry-shim fields assembled from the environment/poll and native FD constructors. Other platform subsystems remain separate components until their source constructors are connected. This is deliberately not a replacement for the full UnixForeign.Hooks dictionary.

• environmentAndPoll : Components Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error
• nativeFd : EvalUnixNativeFdConstruction.Components Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path Place C ClockHost I
• threadTls : EvalUnixThreadTlsConstruction.Components (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.MPlaceTy Memory.Provenance) B I
• linux : Option (EvalUnixLinuxConstruction.Components (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Place H D (Other Raw Listener TcpStream Error) Error Meta Os B I)
• stdOnly : Interpreter.StdOnlyShims.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Place (Interpreter.MPlaceTy Memory.Provenance) B I

def Miri.Input.EvalUnixSourceConstruction.connectDispatch {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path C ClockHost I : Type} (p : CompilerProviders.Prepared) (environmentAndPoll : Components Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (nativeFd : EvalUnixNativeFdConstruction.Components Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path MIR.Place C ClockHost I) (threadTls : EvalUnixThreadTlsConstruction.Components (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.MPlaceTy Memory.Provenance) B I) (linux : Option (EvalUnixLinuxConstruction.Components (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) MIR.Place H D (Other Raw Listener TcpStream Error) Error Meta Os B I)) (stdOnly : Interpreter.StdOnlyShims.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) MIR.Place (Interpreter.MPlaceTy Memory.Provenance) B I) : Except Interpreter.StepError (DispatchComponents Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path MIR.Place C ClockHost I)

Equations

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

def Miri.Input.EvalUnixSourceConstruction.dispatchers {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path C ClockHost I : Type} (p : CompilerProviders.Prepared) (components : DispatchComponents Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path MIR.Place C ClockHost I) (pollBudget : Nat) : Except Interpreter.StepError (Interpreter.UnixForeign.SourceDispatchers (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error))

Build the single ordered Unix dispatcher from runtime-created fields. Environment, FD/control/vector, poll and std-only arms run their source implementations. Every not-yet-constructed source group has an exact target-aware matcher and fails Unsupported only when that recognized name is requested; names outside those groups continue through the outer source resolver.

Equations

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

def Miri.Input.EvalUnixSourceConstruction.bindDispatchers {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path C ClockHost I : Type} (p : CompilerProviders.Prepared) (components : DispatchComponents Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path MIR.Place C ClockHost I) (pollBudget : Nat) (base : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) MIR.Place (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) : Except Interpreter.StepError (Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) MIR.Place (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I)

Replace only the Unix arm of a source-built common foreign dispatcher. The same Core is checked against the one used while constructing StdOnly, so callers cannot substitute a different family/target/allocation policy at the last boundary. Other source foreign-item arms remain owned by the enclosing portable/platform construction.

Equations

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

def Miri.Input.EvalUnixSourceConstruction.fromRuntime {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C Payload Metadata HostEffect : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (userRelevantCrates : Array Nat) (compatibilityBudget : Nat) (host : EvalHostRuntimeConstruction.OsHostEffects Os) (hostEffects : EvalHostRuntimeConstruction.EnvironmentHostEffects (Control Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (hostConfig : EvalUnixConstruction.HostConfigEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Os Error) (ioHost : EvalUnixConstruction.IoHostEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (Control Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Payload) (unitLayout : Interpreter.LocalLayout) (hostUsizeBits fileReferenceBudget watcherReferenceBudget : Nat) (resources : EvalUnixIoConstruction.FileResourceEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error)) (hostFiles : EvalUnixIoConstruction.HostFileEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error Metadata) (otherFiles : EvalUnixIoConstruction.OtherFileEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (Other Raw Listener TcpStream Error) Error) (readinessRoute : EvalUnixFdConstruction.ReadinessRoute (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (deadline : Interpreter.DeadlineMachine.Hooks Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Instant System) (descriptor : Interpreter.PollMachine.DescriptorHooks (Other Raw Listener TcpStream Error)) (communicate : Bool) (entryPollBudget iterationBudget : Nat) (io : Interpreter.BlockingIo.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (FD H D (Other Raw Listener TcpStream Error)) Poll HostEffect) : Except Interpreter.StepError (Components Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)

Construct the Unix environment and outer source poll from the same compiler provider and current EvalWorld state. File memory and descriptor ownership are built here from the narrow host-file/other-description effects; readinessRoute, deadline, and native blocking I/O remain their separately constructed source components.

Equations

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

def Miri.Input.EvalUnixSourceConstruction.stdOnlyFromRuntime {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C I MirBody : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (userRelevantCrates : Array Nat) (accessConfig : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (allocationConfig : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (compilerConfig : Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind (User Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (Stored Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (choice : C) (environment : Interpreter.UnixEnvironmentDispatch.Hooks (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Os Error Interpreter.EnvVars.Kind) (globalBytes : CompilerGlobalBytes.Prepared) (functions : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.UserState (Stored Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (Other Raw Listener TcpStream Error)) (pageSize stackAddress stackSize : UInt64) (foreign : Interpreter.ForeignItems.Core Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) MIR.Place (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) MirBody I) : Except Interpreter.StepError (Interpreter.StdOnlyShims.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) MIR.Place (Interpreter.MPlaceTy Memory.Provenance) MirBody I)

Source-backed std-only fields for the Unix chain. The fallback foreign dispatcher is supplied only at the final chain boundary; compiler layouts, frame identity, physical accesses, target constants, byte-global allocation, isolation policy, and thread-yield state are closed over their canonical providers here. The Unix home-directory string conversion is retained as an explicit host capability because the current StdOnlyShims interface is String-valued.

Equations

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