One canonical MIR small-step assembly. Records below supply compiler/host queries and platform dispatch; core operations are replaced by source drivers. Resource limits govern concrete execution only, not the permitted MIR relation.

@[reducible, inline]

abbrev Miri.Interpreter.ExecutionMachine.Value : Type

Equations

• Miri.Interpreter.ExecutionMachine.Value = Miri.Interpreter.RuntimePlace Miri.Memory.Provenance

@[reducible, inline]

abbrev Miri.Interpreter.ExecutionMachine.Calls (K U C O X : Type) : Type 1

Equations

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

structure Miri.Interpreter.ExecutionMachine.Limits : Type

• callDispatch : Nat
• casts : Nat
• retag : Nat
• validation : Nat

structure Miri.Interpreter.ExecutionMachine.Config (K User C Other Extern Host : Type) : Type 1

• access : PlaceMachine.AccessConfig K User
• allocation : PlaceMachine.AllocationConfig K User
• compiler : PlaceMachine.CompilerHooks K User C
• projection : PlaceProjectionHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra
• operands : ExecutionLeaves.Operand (MachineHooks.State K User) C
• copy : PlaceCopyHooks Memory.Provenance (MachineHooks.State K User) C
• retag : TypedRetag.Hooks K User
• validity : ValidityVisitor.Hooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra (FnVal Other) (ABI.FnAbi MIR.TyId) ValidityMemory.PaddingHandle
• validationRecursive : C → LocalLayout → MachineHooks.M K User Bool
• lifecycle : CallMachine.Lifecycle K User C
• functions : FunctionPointers.Hooks K User Other
• calls : ExecutionCallLeaves.Hooks (MachineHooks.State K User) C Other Extern
• virtual : ExecutionCallLeaves.Virtual K User C
• helpers : ExecutionCallLeaves.Helpers (MachineHooks.State K User) C Extern
• control : ExecutionLeaves.Control Memory.Provenance LocalLayout MachineHooks.FrameExtra
• panic : Panic.Hooks K User C Other
• unwindTerminateFunction : C → MIR.UnwindTerminateReason → MachineHooks.M K User CallInstance
• ignoreOptionalOverflowChecks : Bool
• rvalues : ExecutionLeaves.Rvalue (MachineHooks.State K User) C
• discriminant : ExecutionLeaves.Discriminant (MachineHooks.State K User) C
• scalar : ExecutionScalar.Leaves (MachineHooks.State K User) C
• floats : FloatOpsHooks Memory.Provenance (MachineHooks.State K User) C
• casts : ExecutionCast.Leaves (MachineHooks.State K User) C
• backend : IntrinsicBackend.Dispatcher (MachineHooks.State K User) C Value
• atomics : AtomicAccessHooks Memory.Provenance (MachineHooks.State K User) C Value
• varArgs : IntrinsicVarArgsHooks Memory.Provenance (MachineHooks.State K User) C Value
• intrinsics : CallInstance → IntrinsicHooks Memory.Provenance (MachineHooks.State K User) C Value
• intrinsicName : CallInstance → MachineHooks.M K User String
• intrinsicMustOverride : CallInstance → MachineHooks.M K User Bool
• intrinsicFallbackIsSpec : CallInstance → MachineHooks.M K User Bool
• addresses : User → Memory.AllocAddresses.GlobalAddressState
• arithmetic : Memory.PointerArithmetic
• isRawPointer : C → MIR.TyId → MachineHooks.M K User Bool
• usizeLayout : C → MachineHooks.M K User LocalLayout
• pointeeLayout : C → MIR.TyId → MachineHooks.M K User LocalLayout
• terminators : TerminatorMachine.Hooks K User Host
• preemptionChoice : C → MachineHooks.M K User Bool

def Miri.Interpreter.ExecutionMachine.scalarHooks {K U C O X Host : Type} (h : Config K U C O X Host) : ScalarOpsHooks Memory.Provenance (MachineHooks.State K U) C

Equations

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

def Miri.Interpreter.ExecutionMachine.withValidation {K U C O X Host : Type} [DecidableEq K] (h : Config K U C O X Host) (limits : Limits) : Config K U C O X Host

Close raw reads, dynamically sized physical copies, and validation with actual source implementations before constructing any expression dictionary.

Equations

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

def Miri.Interpreter.ExecutionMachine.projectionHooks {K U C O X Host : Type} [DecidableEq K] (h : Config K U C O X Host) : PlaceProjectionHooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra

Equations

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

def Miri.Interpreter.ExecutionMachine.operandHooks {K U C O X Host : Type} [DecidableEq K] (h : Config K U C O X Host) : OperandMachine.Hooks K U C

Projection/place/operand dictionaries share actual frame-local clocks, canonical layouts and source typed dereference; no read forces allocation.

Equations

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

def Miri.Interpreter.ExecutionMachine.discriminantHooks {K U C O X Host : Type} [DecidableEq K] (h : Config K U C O X Host) : DiscriminantHooks Memory.Provenance (MachineHooks.State K U) C Value

Equations

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

def Miri.Interpreter.ExecutionMachine.castHooks {K U C O X Host : Type} [DecidableEq K] (h : Config K U C O X Host) (limits : Limits) : CastHooks Memory.Provenance (MachineHooks.State K U) C Value

Equations

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

def Miri.Interpreter.ExecutionMachine.rvalueHooks {K U C O X Host : Type} [DecidableEq K] (h : Config K U C O X Host) (limits : Limits) : RvalueHooks Memory.Provenance (MachineHooks.State K U) C Value

Core expression dictionaries. Genuine compiler type/layout predicates and host/platform leaves in base records survive; operational actions are replaced.

Equations

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

def Miri.Interpreter.ExecutionMachine.callHooks {K U C O X Host : Type} [DecidableEq K] (h : Config K U C O X Host) (limits : Limits) : Calls K U C O X

Core call expression/terminator adapters share the actual lifecycle and source intrinsic fallback policy, retaining platform/foreign dispatch leaves.

Equations

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

def Miri.Interpreter.ExecutionMachine.stepHooks {K U C O X Host : Type} [DecidableEq K] (h : Config K U C O X Host) (limits : Limits) : StepHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K U) C Value

The same existing small-step Step.step executes the assembled hooks.

Equations

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

def Miri.Interpreter.ExecutionMachine.step {K U C O X Host : Type} [DecidableEq K] (h : Config K U C O X Host) (limits : Limits) (c : C) (state : MachineHooks.State K U) : StepResult (MachineHooks.State K U) Bool

Equations

• Miri.Interpreter.ExecutionMachine.step h limits c state = Miri.Interpreter.Step.step (Miri.Interpreter.ExecutionMachine.stepHooks h limits) c state

def Miri.Interpreter.ExecutionMachine.AllowedStep {K U C O X Host : Type} [DecidableEq K] (h : Config K U C O X Host) (allowed : MachineHooks.State K U → C → Prop) (before after : MachineHooks.State K U) (outcome : Except StepError Bool) : Prop

Quantify runner resources as well as source choices. A bounded successful run alone establishes no unrestricted UB-freedom claim.

Equations

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