@[reducible, inline]

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

Equations

• Miri.Input.EvalRuntimeConstruction.W = Miri.Input.EvalEntryMachine.W

@[reducible, inline]

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

Equations

• Miri.Input.EvalRuntimeConstruction.EntryUser 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.EvalRuntimeConstruction.EntryOuter (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalRuntimeConstruction.EntryOuter Os R P H D O Aff B Host = Miri.Interpreter.ExecutionStateTransport.Outer (Miri.Input.EvalRuntimeConstruction.W Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalRuntimeConstruction.EntryState (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.EvalRuntimeConstruction.outerPlaceHooks {Os R P H D O Aff B Host C : Type} (hooks : Interpreter.PlaceHooks Memory.Provenance (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Inner (W Os R P H D O Aff B Host))) C Interpreter.MachineHooks.FrameExtra) : Interpreter.PlaceHooks Memory.Provenance (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (W Os R P H D O Aff B Host))) C Interpreter.MachineHooks.FrameExtra

Internal source-platform bridge preserving every place operation.

Equations

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

def Miri.Input.EvalRuntimeConstruction.outerProjection {Os R P H D O Aff B Host C : Type} (hooks : Interpreter.PlaceProjectionHooks Memory.Provenance (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Inner (W Os R P H D O Aff B Host))) C Interpreter.MachineHooks.FrameExtra) : Interpreter.PlaceProjectionHooks Memory.Provenance (EntryState Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra

Internal source-platform bridge on the same live runtime world.

Equations

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

Build argv allocation and projection from the same fixed source Config. Only the sysroot sentinel query remains a concrete compiler capability; its failure is demanded only when the actual target is not no_core.

def Miri.Input.EvalRuntimeConstruction.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) (noCore : Bool) (coreSentinelMirAvailable : Interpreter.MachineHooks.M Memory.MiriMemoryKind (EntryOuter Os R P H D O Aff B Host) Bool) : 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 (W Os R P H D O Aff B Host))) P C)

Equations

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

def Miri.Input.EvalRuntimeConstruction.bootstrapHooks {U AddressPayload Payload C O X F A Aff Os : Type} (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) : EvalBootstrap.Hooks U C O X F A Aff Payload AddressPayload Os

Collect the separately source-built startup components into the exact late-init record. This keeps compiler registries and platform/host effects visible as distinct capabilities while avoiding caller replacement of the main callback with a baseline dictionary.

Equations

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

def Miri.Input.EvalRuntimeConstruction.runReadyConfiguredPrefixUntil {Os C R P H D O Aff B Host ClockHost : Type} [DecidableEq Os] (configs : C → EvalExecutable.Core Os R P H D O Aff B Host C ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (base : Interpreter.RunLoopHooks (EntryState Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (EntryUser Os R P H D O Aff B Host)) (stop : EntryState Os R P H D O Aff B Host → Bool) (choices : List C) (initial : EntryState Os R P H D O Aff B Host) : Interpreter.StepResult (EntryState Os R P H D O Aff B Host) Unit

Run a real initialized frame through the fixed execution Config and actual local thread-stack scheduler. Stack-empty callbacks remain explicit in base; the stop predicate lets a harness capture a completed call frame before a later iteration asks for a main/TLS callback it did not initialize.

Equations

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

def Miri.Input.EvalRuntimeConstruction.runReadyConfiguredPrefixUntil.execute {Os C R P H D O Aff B Host : Type} (stop : EntryState Os R P H D O Aff B Host → Bool) (loop : Interpreter.RunLoopHooks (EvalWorld.State Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (state : EntryState Os R P H D O Aff B Host) : List C → Interpreter.StepResult (EntryState Os R P H D O Aff B Host) Unit

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.EvalRuntimeConstruction.runReadyConfiguredPrefixUntil.execute stop loop state [] = (state, Except.ok ())

def Miri.Input.EvalRuntimeConstruction.runReadyConfiguredPrefix {Os C R P H D O Aff B Host ClockHost : Type} [DecidableEq Os] (configs : C → EvalExecutable.Core Os R P H D O Aff B Host C ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (base : Interpreter.RunLoopHooks (EntryState Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (EntryUser Os R P H D O Aff B Host)) (choices : List C) (initial : EntryState Os R P H D O Aff B Host) : Interpreter.StepResult (EntryState Os R P H D O Aff B Host) Unit

A bounded ready-state source prefix without a caller-defined MIR step.

Equations

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

def Miri.Input.EvalRuntimeConstruction.startAndRunPrefix {Os U C O X F A Aff Payload AddressPayload : Type} [DecidableEq Os] (hooks : EvalBootstrap.Hooks U C O X F A Aff Payload AddressPayload Os) (configuration : EvalBootstrap.Configuration Os) (initialChoice : C) (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

Run real late_init and then a caller-bounded finite run-loop prefix. Initialization errors return the exact state after their source prefix; a successful prefix returns the actual state without claiming process completion.

Equations

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

def Miri.Input.EvalRuntimeConstruction.runConfiguredPrefixUntil {Os R P H D O Aff B Host C ClockHost : Type} [DecidableEq Os] (main : Interpreter.MainMachine.Hooks (EvalExecutable.U Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P) (configs : C → EvalExecutable.Core Os R P H D O Aff B Host C ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (base : Interpreter.RunLoopHooks (EntryState Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (EntryUser Os R P H D O Aff B Host)) (stop : EntryState Os R P H D O Aff B Host → Bool) (choices : List C) (initial : EntryState Os R P H D O Aff B Host) : Interpreter.StepResult (EntryState Os R P H D O Aff B Host) Unit

Executable form: late-init and every scheduled step share the fixed EvalExecutable coreStep. The main hook is expected to come from EvalEntryMachine.mainFromExecution (and may be assembled with bootstrapHooks above); no caller-supplied RunLoop coreStep is used.

Equations

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

def Miri.Input.EvalRuntimeConstruction.runConfiguredPrefixUntil.execute {Os R P H D O Aff B Host C : Type} (stop : EntryState Os R P H D O Aff B Host → Bool) (prefixLoop : Interpreter.RunLoopHooks (EntryState Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (state : EntryState Os R P H D O Aff B Host) : List C → Interpreter.StepResult (EntryState Os R P H D O Aff B Host) Unit

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.EvalRuntimeConstruction.runConfiguredPrefixUntil.execute stop prefixLoop state [] = (state, Except.ok ())

def Miri.Input.EvalRuntimeConstruction.runConfiguredPrefix {Os R P H D O Aff B Host C ClockHost : Type} [DecidableEq Os] (main : Interpreter.MainMachine.Hooks (EvalExecutable.U Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P) (configs : C → EvalExecutable.Core Os R P H D O Aff B Host C ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (base : Interpreter.RunLoopHooks (EntryState Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (EntryUser Os R P H D O Aff B Host)) (choices : List C) (initial : EntryState Os R P H D O Aff B Host) : Interpreter.StepResult (EntryState Os R P H D O Aff B Host) Unit

Run a finite list of scheduler choices from an already initialized source state. This is useful for observing an exact call/return prefix without asking the main callback to run after the target frame has returned.

Equations

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

def Miri.Input.EvalRuntimeConstruction.startAndRunConfiguredPrefixUntil {Os R P H D O Aff B Host C AddressPayload ClockHost : Type} [DecidableEq Os] (hooks : EvalBootstrap.Hooks (EvalExecutable.U Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P AddressPayload Os) (configuration : EvalBootstrap.Configuration Os) (initialChoice : C) (configs : C → EvalExecutable.Core Os R P H D O Aff B Host C ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (base : Interpreter.RunLoopHooks (EntryState Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (EntryUser Os R P H D O Aff B Host)) (stop : EntryState Os R P H D O Aff B Host → Bool) (choices : List C) (initial : EntryState Os R P H D O Aff B Host) : Interpreter.StepResult (EntryState Os R P H D O Aff B Host) Unit

Equations

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

def Miri.Input.EvalRuntimeConstruction.startFromExecutionPrefix {Os R P H D O Aff B Host C ClockHost : Type} [DecidableEq Os] (compiler : CompilerProviders.Prepared) (execution : EvalExecutable.Core Os R P H D O Aff B Host C ClockHost) (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) (layout : EvalEntryMachine.Layouts) (spans : Interpreter.AllocationDriver.SpanHooks) (platform : Interpreter.TlsPlatform) (format : Interpreter.ConstructorBinaryFormat) (externStatic : MIR.DefId → Interpreter.MachineHooks.M Memory.MiriMemoryKind (EntryOuter Os R P H D O Aff B Host) (Memory.Pointer Memory.Provenance)) (evalWindows : String → String → Interpreter.MachineHooks.M Memory.MiriMemoryKind (EntryOuter Os R P H D O Aff B Host) (Memory.Scalar Memory.Provenance)) (arguments : Interpreter.EntryArguments.Hooks Memory.MiriMemoryKind (Interpreter.ThreadStacks.Storage (EntryUser Os R P H D O Aff B Host)) (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (W Os R P H D O Aff B Host))) P C) (environment : Interpreter.EnvVars.Hooks (Option Memory.Provenance) Os (EntryState Os R P H D O Aff B Host)) (externStatics : Interpreter.ExternStatic.InitHooks (EntryState Os R P H D O Aff B Host)) (symbols : Interpreter.IntrinsicSymbolsMachine.Access (Interpreter.ThreadStacks.Storage (EntryUser Os R P H D O Aff B Host))) (image : AllocationImage.Imported) (vtableRuntime : Interpreter.VTableMachine.Hooks Memory.MiriMemoryKind (Interpreter.ThreadStacks.Storage (EntryUser Os R P H D O Aff B Host)) O) (configuration : EvalBootstrap.Configuration Os) (base : Interpreter.RunLoopHooks (EntryState Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (EntryUser Os R P H D O Aff B Host)) (stop : EntryState Os R P H D O Aff B Host → Bool) (choices : List C) (initial : EntryState Os R P H D O Aff B Host) : Interpreter.StepResult (EntryState Os R P H D O Aff B Host) Unit

Equations

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