Compiler-backed assembly of the canonical startup runner. This closes the startup facts, argv allocation, platform constant lookup, Main/TLS policy, late-init hooks, and fixed-config run loop around one prepared compiler input. Host environment and extern-static effects remain explicit source capabilities.

@[reducible, inline]

abbrev Miri.Input.EvalStartupAssembly.W (Os R Payload H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalStartupAssembly.W = Miri.Input.EvalEntryMachine.W

@[reducible, inline]

abbrev Miri.Input.EvalStartupAssembly.User (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalStartupAssembly.User Os R P H D O Aff B Host = Miri.Input.EvalExecutable.U Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalStartupAssembly.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalStartupAssembly.State Os R P H D O Aff B Host = Miri.Input.EvalRuntimeConstruction.EntryState Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalStartupAssembly.InnerState (Os R P H D O Aff B Host : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalStartupAssembly.InnerControl (Os R P H D O Aff B Host : Type) : Type

Equations

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

def Miri.Input.EvalStartupAssembly.environmentLens {Os R P H D O Aff B Host : Type} : EvalHostRuntimeConstruction.EnvironmentLens (InnerControl Os R P H D O Aff B Host) Os

The inner pointer-machine lens for the single environment root in EvalWorld. Reads go through the registered canonical root view; writes update that same runtime field and preserve every surrounding world field.

Equations

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

def Miri.Input.EvalStartupAssembly.externStaticLens {Os R P H D O Aff B Host : Type} : EvalHostRuntimeConstruction.ExternStaticLens (InnerControl Os R P H D O Aff B Host)

The ExternStatic registry is another field of the same machine runtime, and must be updated through that field so GC and symbol resolution observe the exact state changed by late initialization.

Equations

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

@[simp]

theorem Miri.Input.EvalStartupAssembly.environmentLens_get_set {Os R P H D O Aff B Host : Type} (user : Interpreter.PointerMachine.User (InnerControl Os R P H D O Aff B Host)) (value : Interpreter.EnvVars.State (Option Memory.Provenance) Os) : environmentLens.get (environmentLens.set user value) = value

@[simp]

theorem Miri.Input.EvalStartupAssembly.environmentLens_set_get {Os R P H D O Aff B Host : Type} (user : Interpreter.PointerMachine.User (InnerControl Os R P H D O Aff B Host)) : environmentLens.set user (environmentLens.get user) = user

def Miri.Input.EvalStartupAssembly.outerEnvironmentHooks {Os R P H D O Aff B Host : Type} (hooks : Interpreter.EnvVars.Hooks (Option Memory.Provenance) Os (InnerState Os R P H D O Aff B Host)) : Interpreter.EnvVars.Hooks (Option Memory.Provenance) Os (State Os R P H D O Aff B Host)

Carry host-environment operations built on the inner canonical pointer machine into late-init's outer thread-storage view. This is only the lossless state reassociation; all memory, roots and environment updates remain in the same machine.

Equations

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

def Miri.Input.EvalStartupAssembly.environmentFromSource {Os R P H D O Aff B Host C : Type} [DecidableEq Memory.MiriMemoryKind] (host : EvalHostRuntimeConstruction.OsHostEffects Os) (hostEffects : EvalHostRuntimeConstruction.EnvironmentHostEffects (InnerControl Os R P H D O Aff B Host)) (family : Interpreter.ForeignItems.Family) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (InnerControl Os R P H D O Aff B Host) C P) : Interpreter.EnvVars.Hooks (Option Memory.Provenance) Os (State Os R P H D O Aff B Host)

Close the host constructor's source-shaped environment effects over the actual World environment root, then transport those effects losslessly into late-init's outer state. Only host OsStr conversions and OS error effects are provided by the embedding.

Equations

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

def Miri.Input.EvalStartupAssembly.externStaticsFromSource {Os R P H D O Aff B Host C : Type} [DecidableEq Memory.MiriMemoryKind] (target : EvalHostRuntimeConstruction.ExternStaticTarget) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (InnerControl Os R P H D O Aff B Host) C P) (functions : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (EvalEntryMachine.InnerUser Os R P H D O Aff B Host) O) (dynamicValue : String → O) (u8Layout usizeLayout : Interpreter.LocalLayout) : Interpreter.ExternStatic.InitHooks (State Os R P H D O Aff B Host)

Build extern-static initialization from the canonical runtime memory, environment root and function-pointer registry. target and dynamicValue are the exact target/platform and Other-symbol encoding selected by the embedding; all allocation, scalar writes, symbol checks and pointer lookup come from source machines.

Equations

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

def Miri.Input.EvalStartupAssembly.vtableRuntimeFromExecution {Os R P H D O Aff B Host C ClockHost : Type} (prepared : EvalPreparation.Prepared) (execution : EvalExecutable.Core Os R P H D O Aff B Host C ClockHost) : Interpreter.VTableMachine.Hooks Memory.MiriMemoryKind (Interpreter.ThreadStacks.Storage (User Os R P H D O Aff B Host)) O

Reassociate the vtable adapter from the fixed execution view to the outer late-init view. Registries and memory queries still address the same canonical world and allocation memory.

Equations

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

def Miri.Input.EvalStartupAssembly.startFromCompilerExecutionPrefix {Os C R P H D O Aff B Host ClockHost : Type} [DecidableEq Os] (prepared : EvalPreparation.Prepared) (configs : C → EvalExecutable.Core Os R P H D O Aff B Host C ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (deallocationError : Memory.MemoryLifecycleError → Interpreter.StepError) (deallocate : Memory.Pointer (Option Memory.Provenance) → Option (ABI.Size × ABI.Align) → Memory.MemoryKind Memory.MiriMemoryKind → Interpreter.MachineHooks.M Memory.MiriMemoryKind (EvalEntryMachine.InnerUser Os R P H D O Aff B Host) Unit) (choice : C) (spans : Interpreter.AllocationDriver.SpanHooks) (platform : Interpreter.TlsPlatform) (format : Interpreter.ConstructorBinaryFormat) (externStatic : MIR.DefId → Interpreter.MachineHooks.M Memory.MiriMemoryKind (EvalRuntimeConstruction.EntryOuter Os R P H D O Aff B Host) (Memory.Pointer Memory.Provenance)) (environment : Interpreter.EnvVars.Hooks (Option Memory.Provenance) Os (State Os R P H D O Aff B Host)) (externStatics : Interpreter.ExternStatic.InitHooks (State Os R P H D O Aff B Host)) (configuration : EvalBootstrap.Configuration Os) (base : Interpreter.RunLoopHooks (State Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host)) (stop : State Os R P H D O Aff B Host → Bool) (choices : List C) (initial : State Os R P H D O Aff B Host) : Interpreter.StepResult (State Os R P H D O Aff B Host) Unit

Run source late-init and a finite scheduler prefix using compiler-derived startup facts, argument layouts, and exact Windows constants. configs choice is the same fixed execution configuration used by Main/TLS construction and argv allocation; scheduled choices continue through the supplied config function and the fixed EvalExecutable.loop core step.

Equations

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

def Miri.Input.EvalStartupAssembly.startFromSourceExecutionPrefix {Os C R P H D O Aff B Host ClockHost : Type} [DecidableEq Os] [DecidableEq Memory.MiriMemoryKind] (prepared : EvalPreparation.Prepared) (configs : C → EvalExecutable.Core Os R P H D O Aff B Host C ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (choice : C) (spans : Interpreter.AllocationDriver.SpanHooks) (host : EvalHostRuntimeConstruction.OsHostEffects Os) (hostEffects : EvalHostRuntimeConstruction.EnvironmentHostEffects (InnerControl Os R P H D O Aff B Host)) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (InnerControl Os R P H D O Aff B Host) C P) (dynamicValue : String → O) (u8Layout usizeLayout : Interpreter.LocalLayout) (configuration : EvalBootstrap.Configuration Os) (base : Interpreter.RunLoopHooks (State Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host)) (stop : State Os R P H D O Aff B Host → Bool) (choices : List C) (initial : State Os R P H D O Aff B Host) : Interpreter.StepResult (State Os R P H D O Aff B Host) Unit

Fully source-wired startup entrypoint. The execution Config selected by configs choice supplies the function-pointer registry to extern-static initialization; the same choice/config closure drives Main/TLS and every MIR step. Environment and weak-symbol storage operate on the canonical runtime roots through the source host constructor.

Equations

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