Source main/root calls and scheduled MIR steps share one physical execution configuration. This is the connected runtime adapter, not a replacement for constructing the remaining compiler/host leaves of ExecutionMachine.Config.

@[reducible, inline]

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

Equations

• Miri.Input.EvalExecutable.W = Miri.Input.EvalWorld.World

@[reducible, inline]

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

Equations

• Miri.Input.EvalExecutable.U Os R P H D O Aff B Host = Miri.Interpreter.ValidityMachine.UserState (Miri.Input.EvalExecutable.W Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalExecutable.Core (Os R P H D O Aff B Host C ClockHost : Type) : Type 1

Equations

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

def Miri.Input.EvalExecutable.mainCalls {Os R P H D O Aff B Host C ClockHost : Type} (config : Core Os R P H D O Aff B Host C ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (main : Interpreter.MainMachine.Hooks (U Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P) : Interpreter.MainMachine.Hooks (U Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P

Main, constructors and TLS root calls receive the same fully assembled call engine as MIR call terminators: real argument copies, FnEntry retags, frame identities, return copies, protector release and cleanup are preserved.

Equations

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

def Miri.Input.EvalExecutable.loop {C Os R P H D O Aff B Host ClockHost : Type} (configs : C → Core Os R P H D O Aff B Host C ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (main : Interpreter.MainMachine.Hooks (U Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P) (base : Interpreter.RunLoopHooks (EvalWorld.State Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (U Os R P H D O Aff B Host)) : Interpreter.RunLoopHooks (EvalWorld.State Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback

Runtime source choice events stay inside their actual dictionaries. A configuration may depend on the current operation context, but no caller core step replaces the existing interpreter: coreStep is fixed here. Main callback capture, checked restore, actual termination and stack scheduling are mandatory.

Equations

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

def Miri.Input.EvalExecutable.loopChecked {C Os R P H D O Aff B Host ClockHost : Type} (configs : C → Except Interpreter.StepError (Core Os R P H D O Aff B Host C ClockHost)) (limits : Interpreter.ExecutionMachine.Limits) (main : Interpreter.MainMachine.Hooks (U Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P) (base : Interpreter.RunLoopHooks (EvalWorld.State Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (U Os R P H D O Aff B Host)) : Interpreter.RunLoopHooks (EvalWorld.State Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback

Fallible source configuration loop. Source Core construction can depend on the selected scheduler choice and may report a compiler/metadata error. Keep that error at the chosen step with its current state; never synthesize a fallback Core or eagerly reject configurations for choices that are not run.

Equations

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

def Miri.Input.EvalExecutable.fixedCorePrefixLoop {C Os R P H D O Aff B Host ClockHost : Type} (configs : C → Core Os R P H D O Aff B Host C ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (base : Interpreter.RunLoopHooks (EvalWorld.State Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (U Os R P H D O Aff B Host)) : Interpreter.RunLoopHooks (EvalWorld.State Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback

Ready-state finite prefixes use the same fixed Config step and actual local thread-stack scheduler while leaving stack-empty callback/termination behavior as explicit source hooks. This is for a caller that has already initialized a real frame and stops before requesting an unavailable callback.

Equations

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

def Miri.Input.EvalExecutable.ubFreedom {C Os R P H D O Aff B Host ClockHost : Type} (configs : C → Core Os R P H D O Aff B Host C ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (main : Interpreter.MainMachine.Hooks (U Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P) (base : Interpreter.RunLoopHooks (EvalWorld.State Os R P H D O Aff B Host) C Interpreter.MainMachine.Callback) (scheduler : C → Interpreter.ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind (U Os R P H D O Aff B Host)) (allowed : EvalWorld.State Os R P H D O Aff B Host → C → Prop) (initial : EvalWorld.State Os R P H D O Aff B Host → Prop) : Prop

The specification ranges over every permitted finite execution prefix; resource-bounded execution is not used as its safety definition.

Equations

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