Exact compiler startup facts and the small source-owned arguments adapter. These are separate from host environment contents: the latter remain the explicit EvalBootstrap.Configuration supplied by the embedding.

structure Miri.Input.EvalStartupRuntimeConstruction.StartupFacts : Type

• noCore : Except String Bool
• coreEscapeDefault : Except String (DefinitionId × Bool)

def Miri.Input.EvalStartupRuntimeConstruction.prepare (compiler : CompilerProviders.Prepared) : Except String StartupFacts

Prepare source facts from the pinned exporter query table. Failed queries remain stored and are raised only if the corresponding source startup path asks for them. The escape-default identity must already be in the canonical definition table; no path or display-name identity is synthesized here.

Equations

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

def Miri.Input.EvalStartupRuntimeConstruction.argumentsFromExecution {Os R P H D O Aff B Host C ClockHost : Type} (compiler : CompilerProviders.Prepared) (execution : EvalExecutable.Core Os R P H D O Aff B Host C ClockHost) (facts : StartupFacts) : Except String (Interpreter.EntryArguments.Hooks Memory.MiriMemoryKind (Interpreter.ThreadStacks.Storage (EvalExecutable.U Os R P H D O Aff B Host)) (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (EvalRuntimeConstruction.W Os R P H D O Aff B Host))) P C)

Attach exact exporter-derived no_core and sentinel-MIR facts to the argv constructor from the same fixed execution Config. No target knob is supplied by the caller, and failed compiler queries remain demand-time Unknown.

Equations

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