Build the existing Solarish foreign-item machine from compiler facts and the active Unix memory/environment products. The Solarish shim semantics stay in SolarishForeign; this module supplies their exact target layouts, constants, physical place operations, and canonical event/epoll machines.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• Miri.Input.EvalUnixSolarishConstruction.FD H D O = Miri.Input.EvalUnixSourceConstruction.FD H D O

def Miri.Input.EvalUnixSolarishConstruction.fromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (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) (foreign : Interpreter.ForeignItems.Core Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (Stored Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (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) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (choice : C) (epoll : Interpreter.EpollShims.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) (event : Interpreter.EventFd.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))) (pollBudget : Nat) (stackAddress stackSize : UInt64) : Except Interpreter.StepError (Interpreter.SolarishForeign.CoreHooks (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 (Interpreter.RuntimePlace Memory.Provenance) Error Interpreter.LoadedBody Interpreter.CallInstance)

Construct every Solarish foreign-item hook from the live Unix environment, compiler layout/constant tables, and canonical memory/event state. Only the already source-constructed foreign core and event/epoll operation machines cross this boundary; no operation callback is supplied individually.

Equations

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