eval.rs::create_ecx / machine.rs::late_init on an actual initial machine. The caller supplies the fully configured initial context and compiler image; this module neither synthesizes target facts nor substitutes successful host operations. Every failed initialization retains its already executed prefix.

structure Miri.Input.EvalBootstrap.Configuration (Os : Type) : Type

• arguments : Array String
• entry : MIR.DefId
• entryType : Interpreter.MainEntryType
• communicate : Bool
• forwarded : Array Os
• environment : Array (Os × Os)
• overrides : Array (Os × Os)

structure Miri.Input.EvalBootstrap.Hooks (U C O X F A Aff Payload AddressPayload Os : Type) : Type 1

• arguments : Interpreter.EntryArguments.Hooks Memory.MiriMemoryKind (Interpreter.ThreadStacks.Storage U) AddressPayload Payload C
• main : Interpreter.MainMachine.Hooks U C O X F A Aff Payload
• environment : Interpreter.EnvVars.Hooks (Option Memory.Provenance) Os (Interpreter.MainMachine.State U)
• externStatics : Interpreter.ExternStatic.InitHooks (Interpreter.MainMachine.State U)
• compiler : CompilerProviders.Prepared
• symbols : Interpreter.IntrinsicSymbolsMachine.Access (Interpreter.ThreadStacks.Storage U)
• image : AllocationImage.Imported
• vtableRuntime : Interpreter.VTableMachine.Hooks Memory.MiriMemoryKind (Interpreter.ThreadStacks.Storage U) O

def Miri.Input.EvalBootstrap.createContextWithBytesProfiled {Os U C O X F A Aff P AP : Type} [DecidableEq Os] (profile : Lean.Options) (h : Hooks U C O X F A Aff P AP Os) (config : Configuration Os) (choice : C) : Interpreter.MainMachine.M U CompilerGlobalBytes.Prepared

Salt-zero identities are attached to the actual imported image before allocating runtime arguments. Source late_init then initializes environment, extern statics, and finally installs the captured main-thread callback.

Equations

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

def Miri.Input.EvalBootstrap.createContextWithBytes {Os U C O X F A Aff P AP : Type} [DecidableEq Os] (h : Hooks U C O X F A Aff P AP Os) (config : Configuration Os) (choice : C) : Interpreter.MainMachine.M U CompilerGlobalBytes.Prepared

Equations

• Miri.Input.EvalBootstrap.createContextWithBytes h config choice = Miri.Input.EvalBootstrap.createContextWithBytesProfiled ∅ h config choice

theorem Miri.Input.EvalBootstrap.createContextWithBytes_profile_identity {Os U C O X F A Aff P AP : Type} [DecidableEq Os] (h : Hooks U C O X F A Aff P AP Os) (config : Configuration Os) (choice : C) : createContextWithBytes h config choice = createContextWithBytesProfiled ∅ h config choice

def Miri.Input.EvalBootstrap.createContext {Os U C O X F A Aff P AP : Type} [DecidableEq Os] (h : Hooks U C O X F A Aff P AP Os) (config : Configuration Os) (choice : C) : Interpreter.MainMachine.M U Unit

Compatibility entry; initialization still attaches the actual compiler byte pool.

Equations

• Miri.Input.EvalBootstrap.createContext h config choice = do let _ ← Miri.Input.EvalBootstrap.createContextWithBytes h config choice pure ()

def Miri.Input.EvalBootstrap.executePrefix {U C O X F A Aff P : Type} (h : Interpreter.MainMachine.Hooks U C O X F A Aff P) (base : Interpreter.RunLoopHooks (Interpreter.MainMachine.State U) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind U) (choices : List C) (initial : Interpreter.MainMachine.State U) : Interpreter.StepResult (Interpreter.MainMachine.State U) Unit

A finite execution prefix, not successful program completion. Exit remains an actual termination outcome of the source loop; exhausting supplied choices returns the current state so a caller can extend the execution prefix.

Equations

• Miri.Input.EvalBootstrap.executePrefix h base scheduler choices initial = Miri.Input.EvalBootstrap.executePrefix.go (Miri.Interpreter.MainMachine.bindLoop h base scheduler) choices initial

def Miri.Input.EvalBootstrap.executePrefix.go {U C : Type} (loop : Interpreter.RunLoopHooks (Interpreter.MainMachine.State U) C Interpreter.MainMachine.Callback) : List C → Interpreter.MainMachine.State U → Interpreter.StepResult (Interpreter.MainMachine.State U) Unit

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.EvalBootstrap.executePrefix.go loop [] a✝ = (a✝, Except.ok ())