Canonical constant-operand machine binding. Compiler CTFE pointer IDs remain allocation IDs until actual root-tag/address adjustment; they are never used directly as absolute guest addresses.

structure Miri.Interpreter.ConstantMachine.Context (K User : Type) : Type

• state : MachineHooks.State K User
• pendingError : Option StepError

@[reducible, inline]

abbrev Miri.Interpreter.ConstantMachine.Queries (K User : Type) : Type

Equations

• Miri.Interpreter.ConstantMachine.Queries K User = Miri.Interpreter.ConstantQueries Miri.Memory.Provenance Miri.TreeBorrows.BorrowTree K (Miri.Interpreter.ConstantMachine.Context K User)

def Miri.Interpreter.ConstantMachine.queries {K User Other : Type} (functions : FunctionPointers.Hooks K User Other) (arithmetic : Memory.PointerArithmetic) (externStatic : MIR.DefId → MachineHooks.M K User (Memory.Pointer Memory.Provenance)) (compiler : Queries K User) : Queries K User

Source constantGlobalRootPointer performs TLS/extern classification first. Miri ignores the CTFE immutable flag; the original offset is retained after actual root provenance and absolute base-address assignment.

Equations

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

def Miri.Interpreter.ConstantMachine.fromCompiler {K User Other : Type} (functions : FunctionPointers.Hooks K User Other) (arithmetic : Memory.PointerArithmetic) (externStatic : MIR.DefId → MachineHooks.M K User (Memory.Pointer Memory.Provenance)) (normalize : CallInstance → MIR.MirConst → Except ConstantError MIR.MirConst) (evaluate : CallInstance → MIR.MirConst → MIR.SpanRef → Except ConstantError MIR.ConstValue) : Queries K User

Construct the whole dictionary from actual compiler evidence and machine operations. No unbound placeholder dictionary is required by production.

Equations

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

def Miri.Interpreter.ConstantMachine.evalOperandWithLayout {K User : Type} (runtime : Input.RuntimeMetadata) (compiler : Queries K User) (classifyConstantError : ConstantError → StepError) (constant : MIR.ConstOperand) (known : Option LocalLayout) (checkKnown : Option (LocalLayout → LocalLayout → MachineHooks.M K User Bool)) : MachineHooks.M K User (OpTy Memory.Provenance)

Lift the existing source interpreter without losing post-error machine updates. Error categories from actual machine operations are preserved exactly; compiler/constant subsystem errors use the required source classifier.

Equations

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

def Miri.Interpreter.ConstantMachine.evalOperand {K User : Type} (runtime : Input.RuntimeMetadata) (compiler : Queries K User) (classifyConstantError : ConstantError → StepError) (constant : MIR.ConstOperand) : MachineHooks.M K User (OpTy Memory.Provenance)

Equations

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

def Miri.Interpreter.ConstantMachine.evalValueWithLayout {K User Other : Type} (runtime : Input.RuntimeMetadata) (functions : FunctionPointers.Hooks K User Other) (arithmetic : Memory.PointerArithmetic) (externStatic : MIR.DefId → MachineHooks.M K User (Memory.Pointer Memory.Provenance)) (classifyConstantError : ConstantError → StepError) (value : MIR.ConstValue) (ty : MIR.TyId) (known : Option LocalLayout) (checkKnown : Option (LocalLayout → LocalLayout → MachineHooks.M K User Bool)) : MachineHooks.M K User (OpTy Memory.Provenance)

Direct compiler ConstValue conversion. No synthetic MIR operand, source span, normalization callback or evaluation callback is introduced. Machine effects preceding conversion failure are retained exactly as in operand eval.

Equations

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