Final source-owned call-foreign assembly for the currently constructed Unix chain. The callback is an effectful factory, so the canonical Core is created from the live state at the call boundary. No caller supplies a completed ForeignItems.Hooks record. Unsupported portable arms remain demand-local; the Unix dispatcher retains its exact source order/fallback.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalCallDispatchConstruction.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.EvalCallDispatchConstruction.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.EvalCallDispatchConstruction.SourceUser (Os R 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.EvalCallDispatchConstruction.M (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error A : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalCallDispatchConstruction.HostSeed (Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path AddrIter : Type) : Type 1

Typed subsystem source input for EvalConfigurationCore. The platform components are already source-built component records, never a completed ForeignItems/UnixForeign hook. Core constructs Common and the ordered final resolver at the actual call state.

Equations

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

structure Miri.Input.EvalCallDispatchConstruction.SourceInput (Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path AddrIter : Type) : Type 1

• host : HostSeed Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path AddrIter

  Raw host capabilities only. Compiler-derived dispatch and state-owned Unix components are assembled at the live Core call boundary.

• geometry : InitialMachine.Geometry
• alignment : Interpreter.ValidityMachine.AlignmentCheck
• stringScanBudget : Nat
• pollBudget : Nat
• fileReferenceBudget : Nat
• watcherReferenceBudget : Nat
• shortFdOperations : Bool

  Selected Miri setting; this controls source short-I/O behavior and is not inferred from compiler target facts.

• varArgsBudget : Nat

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

• nativeFd : EvalUnixNativeFdConstruction.Components Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path Place C ClockHost I Interpreter.LoadedBody

  The final source-built descriptor/files/readiness operations used by both foreign dispatch and the ordinary callback runtime.

• registry : EvalCallbackSocketConstruction.RegistrySeed Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error
• virtual : Interpreter.VirtualSocket.Hooks (State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.Files.Ref (Interpreter.Files.Description H D (Other Raw Listener TcpStream Error))) Error
• tcp : Interpreter.TcpSocket.Hooks (State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.Files.Ref (Interpreter.Files.Description H D (Other Raw Listener TcpStream Error))) Raw Listener TcpStream Error Poll Error
• syncEffects : Interpreter.TypedSyncMachine.Effects (State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)
• errors : Interpreter.IoError.Hooks (State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Error
• readinessRoute : EvalUnixFdConstruction.ReadinessRoute (State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)

structure Miri.Input.EvalCallDispatchConstruction.SourceAssembly (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C : Type) (CallbackSeed : Type := Unit) : Type

• foreign : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance
• dispatchers : Interpreter.UnixForeign.SourceDispatchers (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)
• environment : Option (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)
• memory : Option (EvalHostRuntimeConstruction.EnvironmentMemory (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored Os R P H D (Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler))) C P)
• registry : Option (EvalCallbackSocketConstruction.RegistrySeed Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)
• threadTls : Option (EvalUnixThreadTlsConstruction.Components (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.MPlaceTy Memory.Provenance) B Interpreter.CallInstance)
• callbackSeed : Option CallbackSeed

def Miri.Input.EvalCallDispatchConstruction.fromEnvironmentStdOnlyPackage {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C : Type} (p : CompilerProviders.Prepared) (common : EvalForeignConstruction.Common (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (spans : Interpreter.AllocationDriver.SpanHooks) (mathHooks : Interpreter.Math.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (Interpreter.RuntimePlace Memory.Provenance)) (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) (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) Interpreter.LoadedBody Interpreter.CallInstance) (communicate : Bool) (choice : C) (CallbackSeed : Type := Unit) : M Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error (SourceAssembly Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C CallbackSeed)

Connect only the source environment and std-only components while the remaining Unix subsystems are under construction. The dispatcher itself keeps the pinned order and uses exact target-aware demand-local Unsupported arms.

Equations

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

def Miri.Input.EvalCallDispatchConstruction.fromEnvironmentStdOnlySource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C : Type} (p : CompilerProviders.Prepared) (common : EvalForeignConstruction.Common (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (spans : Interpreter.AllocationDriver.SpanHooks) (mathHooks : Interpreter.Math.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (Interpreter.RuntimePlace Memory.Provenance)) (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) (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) Interpreter.LoadedBody Interpreter.CallInstance) (communicate : Bool) (choice : C) : M Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error (Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance)

Compatibility projection for code that only needs ForeignItems hooks.

Equations

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

def Miri.Input.EvalCallDispatchConstruction.unixFromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path ClockHost I : Type} (p : CompilerProviders.Prepared) (common : EvalForeignConstruction.Common (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (spans : Interpreter.AllocationDriver.SpanHooks) (mathHooks : Interpreter.Math.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (Interpreter.RuntimePlace Memory.Provenance)) (components : EvalUnixSourceConstruction.DispatchComponents Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path MIR.Place C ClockHost I) (choice : C) (pollBudget : Nat) : M Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error (Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance)

Build the ordered Unix call resolver around the actual nonrecursive foreign Core and the source dispatcher components. The exact Unix source resolver is shared with UnixForeign.dispatch; the only currently unported outer portable category is explicitly Unsupported when ForeignItems selects it. Unrecognized names still continue through Unix source fallback and then the compiler symbol resolver.

Equations

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

def Miri.Input.EvalCallDispatchConstruction.fromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path ClockHost I : Type} (p : CompilerProviders.Prepared) (native : EvalForeignConstruction.HostEffects (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalForeignConstruction.Stored Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B (EvalSyncMachine.Host Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native Profiler))) (allocation : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (EvalForeignConstruction.User Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B (EvalSyncMachine.Host Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native Profiler))) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (EvalForeignConstruction.User Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B (EvalSyncMachine.Host Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native Profiler)) P) (deallocationDiagnostic : Memory.AllocId → Interpreter.PlaceMachine.MachineM Memory.MiriMemoryKind (EvalForeignConstruction.User Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B (EvalSyncMachine.Host Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native Profiler)) Unit) (nativeDrop : Option (Memory.Allocation Memory.Provenance TreeBorrows.BorrowTree → Interpreter.MachineHooks.M Memory.MiriMemoryKind (EvalForeignConstruction.User Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B (EvalSyncMachine.Host Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native Profiler)) Unit)) (pointer : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalForeignConstruction.Stored Os R P H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B (EvalSyncMachine.Host Poll Instant System H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Native Profiler)))) (spans : Interpreter.AllocationDriver.SpanHooks) (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) (callFunction : C → Interpreter.CallInstance → Array (Interpreter.RvalueImmTy Memory.Provenance) → Interpreter.ReturnContinuation → M Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Unit) (choice : C) (mathHooks : Interpreter.Math.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (Interpreter.RuntimePlace Memory.Provenance)) (components : EvalUnixSourceConstruction.DispatchComponents Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path MIR.Place C ClockHost I) (compatibilityBudget pollBudget : Nat) (debugAssertions : Bool) : M Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error (Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance)

End-to-end Unix foreign call factory. It obtains symbol tables, target identity, allocator policy, common source bodies and ordered dispatchers from the prepared compiler plus the actual execution machine components. The only effects left as arguments are native-library host calls and the already source-constructed Unix component bundle.

Equations

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

def Miri.Input.EvalCallDispatchConstruction.fromSeedEnvironment {Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C ErrorHost Meta Path AddrIter : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (nativeLibraryPaths : State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error → Array String) (callNative : String → Interpreter.MPlaceTy Memory.Provenance → Array (Interpreter.OpTy Memory.Provenance) → M Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Bool) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalForeignConstruction.Stored Os R EvalSyncPayload.Payload H D (Other Raw Listener TcpStream Error) Aff B (EvalSyncMachine.Host Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler))) (accessConfig : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (SourceUser Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (allocation : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (SourceUser Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) (compiler : Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind (SourceUser Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (SourceUser Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) EvalSyncPayload.Payload) (deallocationDiagnostic : Memory.AllocId → Interpreter.PlaceMachine.MachineM Memory.MiriMemoryKind (SourceUser Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit) (nativeDrop : Option (Memory.Allocation Memory.Provenance TreeBorrows.BorrowTree → Interpreter.MachineHooks.M Memory.MiriMemoryKind (SourceUser Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Unit)) (pointer : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalForeignConstruction.Stored Os R EvalSyncPayload.Payload H D (Other Raw Listener TcpStream Error) Aff B (EvalSyncMachine.Host Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler)))) (spans : Interpreter.AllocationDriver.SpanHooks) (functions : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (SourceUser Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Other Raw Listener TcpStream Error)) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (callFunction : C → Interpreter.CallInstance → Array (Interpreter.RvalueImmTy Memory.Provenance) → Interpreter.ReturnContinuation → M Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Unit) (choice : C) (mathHooks : Interpreter.Math.Hooks Memory.Provenance (State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C (Interpreter.RuntimePlace Memory.Provenance)) (threadFunctions : Unit → Except Interpreter.StepError (Interpreter.FunctionCalls.Hooks Memory.Provenance (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (EvalCoreMachine.World Os R EvalSyncPayload.Payload H D (Other Raw Listener TcpStream Error) Aff B (EvalSyncMachine.Host Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler)))) C Interpreter.MachineHooks.FrameExtra (Other Raw Listener TcpStream Error) ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId))) (host : HostSeed Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path AddrIter) (hostConfiguration : HostRuntime.Configuration) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (Interpreter.ValidityMachine.Control (EvalCoreMachine.Stored Os R EvalSyncPayload.Payload H D (Other Raw Listener TcpStream Error) Aff B (HostRuntime.Storage Poll Instant System H D (Other Raw Listener TcpStream Error) Native Profiler))) C EvalSyncPayload.Payload) (bytes : CompilerGlobalBytes.Prepared) (geometry : InitialMachine.Geometry) (userRelevantCrates : Array Nat) (compatibilityBudget fileReferenceBudget watcherReferenceBudget : Nat) (debugAssertions : Bool) (hostUsizeBits stringScanBudget : Nat) (shortFdOperations : Bool) (varArgsBudget : Nat) : M Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error (SourceAssembly Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C (SourceCallbackSeed Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error Meta Path MIR.Place C (Interpreter.Clock.HostHooks Instant System (State Os R EvalSyncPayload.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)) Interpreter.CallInstance AddrIter))

Production source entry for the currently connected Unix families. It derives environment and std-only hooks from the typed host seed and the exact live Core memory/function providers. All other recognized Unix operations are kept in the ordered resolver as explicit demand-local Unsupported arms.

Equations

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