Pinned operand.rs::const_val_to_op and eval_context.rs::eval_mir_constant, including operand.rs's current-frame normalization boundary. Compiler query results are reusable exact-key evidence; no Rust trait or constant solver is implemented here. Global root conversion retains memory.rs classification and its TLS/extern distinction. Required machine hooks remain stateful and fallible.

inductive Miri.Interpreter.ConstantError : Type

• metadata (message : String) : ConstantError
• query (message : String) : ConstantError
• scalar (error : Memory.ScalarError) : ConstantError
• immediate (error : ImmediateError) : ConstantError
• globalAccess (error : Memory.GlobalAccessError) : ConstantError
• memoryAccess (error : Memory.MemoryAccessError) : ConstantError
• tlsConstantPointer (id : Memory.AllocId) : ConstantError
• invariant (message : String) : ConstantError

@[instance_reducible]

instance Miri.Interpreter.instReprConstantError : Repr ConstantError

Equations

• Miri.Interpreter.instReprConstantError = { reprPrec := Miri.Interpreter.instReprConstantError.repr }

def Miri.Interpreter.instReprConstantError.repr : ConstantError → Nat → Std.Format

Equations

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

structure Miri.Interpreter.ConstantState (P E K H : Type) : Type

• memory : Memory.MemoryState P E K
• hooks : H
• currentInstance : CallInstance

def Miri.Interpreter.ConstantState.fromFrame {P E K H L F : Type} (memory : Memory.MemoryState P E K) (hooks : H) (frame : Frame P L F) : ConstantState P E K H

Initialize the subsystem view from the actual current stack frame, retaining its instance kind and complete generic arguments.

Equations

• Miri.Interpreter.ConstantState.fromFrame memory hooks frame = { memory := memory, hooks := hooks, currentInstance := frame.functionInstance }

@[reducible, inline]

abbrev Miri.Interpreter.ConstantM (P E K H A : Type) : Type

Equations

• Miri.Interpreter.ConstantM P E K H A = EStateM Miri.Interpreter.ConstantError (Miri.Interpreter.ConstantState P E K H) A

structure Miri.Interpreter.ConstantValueQueries (P E K H : Type) : Type

Source ConstValue conversion needs only allocation root/extern queries; normalization and Const::eval belong to the separate MIR-constant path.

• adjustGlobalRootPointer : Memory.Pointer Memory.CtfeProvenance → ConstantM P E K H (Memory.Pointer P)
• externStaticPointer : MIR.DefId → ConstantM P E K H (Memory.Pointer P)

structure Miri.Interpreter.ConstantQueries (P E K H : Type) : Type

• instantiateAndNormalize : CallInstance → MIR.MirConst → ConstantM P E K H MIR.MirConst

  Source instantiate_from_current_frame_and_normalize_erasing_regions. The full current InstanceArgs and shared compiler tables must be used.

• evaluate : CallInstance → MIR.MirConst → MIR.SpanRef → ConstantM P E K H MIR.ConstValue

  Source Const::eval. Receives the normalized source constant and span; absent/TooGeneric/failed compiler evidence is an error, not a value.

• adjustGlobalRootPointer : Memory.Pointer Memory.CtfeProvenance → ConstantM P E K H (Memory.Pointer P)

  Source M::adjust_alloc_root_pointer; implements machine provenance, address allocation, borrow tags and all required global-pointer effects.

• externStaticPointer : MIR.DefId → ConstantM P E K H (Memory.Pointer P)

  Source M::extern_static_pointer; the argument is the shared dense DefId.

def Miri.Interpreter.ConstantQueries.valueQueries {P E K H : Type} (queries : ConstantQueries P E K H) : ConstantValueQueries P E K H

Equations

• queries.valueQueries = { adjustGlobalRootPointer := queries.adjustGlobalRootPointer, externStaticPointer := queries.externStaticPointer }

structure Miri.Interpreter.CompilerConstantEvidence : Type

• fnInstance : CallInstance
• original : MIR.MirConst
• normalized : MIR.MirConst
• span : MIR.SpanRef
• value : MIR.ConstValue

def Miri.Interpreter.instReprCompilerConstantEvidence.repr : CompilerConstantEvidence → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprCompilerConstantEvidence : Repr CompilerConstantEvidence

Equations

• Miri.Interpreter.instReprCompilerConstantEvidence = { reprPrec := Miri.Interpreter.instReprCompilerConstantEvidence.repr }

def Miri.Interpreter.normalizationFromEvidence (evidence : Array CompilerConstantEvidence) (fnInstance : CallInstance) (original : MIR.MirConst) : Except ConstantError MIR.MirConst

Exact compiler query reuse. This checks instance arguments, source form, normalized form and span; it never substitutes a result from another instance.

Equations

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

def Miri.Interpreter.evaluationFromEvidence (evidence : Array CompilerConstantEvidence) (fnInstance : CallInstance) (normalized : MIR.MirConst) (span : MIR.SpanRef) : Except ConstantError MIR.ConstValue

Equations

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

def Miri.Interpreter.valueGlobalRootPointer {P E K H : Type} (queries : ConstantValueQueries P E K H) (pointer : Memory.Pointer Memory.CtfeProvenance) : ConstantM P E K H (Memory.Pointer P)

Source global_root_pointer classification happens before the machine root pointer adjustment. Constants cannot point to TLS; foreign statics require the extern-static hook instead of normal root adjustment.

Equations

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

def Miri.Interpreter.valueToOpWithLayout {P E K H : Type} (runtime : Input.RuntimeMetadata) (queries : ConstantValueQueries P E K H) (value : MIR.ConstValue) (ty : MIR.TyId) (known : Option LocalLayout) (checkKnown : Option (LocalLayout → LocalLayout → ConstantM P E K H Bool)) : ConstantM P E K H (OpTy P)

Source const_val_to_op. Indirect and slice constants carry immutable/shared CTFE roots; scalar pointers retain their own exported flags. Constructing an indirect operand does not dereference it or trigger a global initializer.

Equations

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

def Miri.Interpreter.constantGlobalRootPointer {P E K H : Type} (queries : ConstantQueries P E K H) (pointer : Memory.Pointer Memory.CtfeProvenance) : ConstantM P E K H (Memory.Pointer P)

Compatibility projection for the full MIR-constant dictionary.

Equations

• Miri.Interpreter.constantGlobalRootPointer queries pointer = Miri.Interpreter.valueGlobalRootPointer queries.valueQueries pointer

def Miri.Interpreter.constValueToOpWithLayout {P E K H : Type} (runtime : Input.RuntimeMetadata) (queries : ConstantQueries P E K H) (value : MIR.ConstValue) (ty : MIR.TyId) (known : Option LocalLayout) (checkKnown : Option (LocalLayout → LocalLayout → ConstantM P E K H Bool)) : ConstantM P E K H (OpTy P)

Equations

• Miri.Interpreter.constValueToOpWithLayout runtime queries value ty known checkKnown = Miri.Interpreter.valueToOpWithLayout runtime queries.valueQueries value ty known checkKnown

def Miri.Interpreter.evalMirConstantWithLayout {P E K H : Type} (runtime : Input.RuntimeMetadata) (queries : ConstantQueries P E K H) (constant : MIR.MirConst) (span : MIR.SpanRef) (known : Option LocalLayout) (checkKnown : Option (LocalLayout → LocalLayout → ConstantM P E K H Bool)) : ConstantM P E K H (OpTy P)

The evaluator receives the original source form through normalization; only source Const::Val bypasses a compiler evaluation query.

Equations

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

def Miri.Interpreter.evalConstOperandWithLayout {P E K H : Type} (runtime : Input.RuntimeMetadata) (queries : ConstantQueries P E K H) (constant : MIR.ConstOperand) (known : Option LocalLayout) (checkKnown : Option (LocalLayout → LocalLayout → ConstantM P E K H Bool)) : ConstantM P E K H (OpTy P)

Connected eval_operand(Constant): instantiate/substitute current frame arguments, normalize, then evaluate; no missing parameter becomes a default.

Equations

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

def Miri.Interpreter.constValueToOp {P E K H : Type} (runtime : Input.RuntimeMetadata) (queries : ConstantQueries P E K H) (value : MIR.ConstValue) (ty : MIR.TyId) : ConstantM P E K H (OpTy P)

Compatibility entry points without a known-layout hint.

Equations

• Miri.Interpreter.constValueToOp runtime queries value ty = Miri.Interpreter.constValueToOpWithLayout runtime queries value ty none none

def Miri.Interpreter.evalMirConstant {P E K H : Type} (runtime : Input.RuntimeMetadata) (queries : ConstantQueries P E K H) (constant : MIR.MirConst) (span : MIR.SpanRef) : ConstantM P E K H (OpTy P)

Equations

• Miri.Interpreter.evalMirConstant runtime queries constant span = Miri.Interpreter.evalMirConstantWithLayout runtime queries constant span none none

def Miri.Interpreter.evalConstOperand {P E K H : Type} (runtime : Input.RuntimeMetadata) (queries : ConstantQueries P E K H) (constant : MIR.ConstOperand) : ConstantM P E K H (OpTy P)

Equations

• Miri.Interpreter.evalConstOperand runtime queries constant = Miri.Interpreter.evalConstOperandWithLayout runtime queries constant none none

def Miri.Interpreter.constantGetAllocRaw {K P E H : Type} [DecidableEq K] (id : Memory.AllocId) (globalKind : Option K) (hooks : Memory.GlobalAllocationHooks P E K H) : ConstantM P E K H (Memory.Allocation P E)

Connect subsequent memory access to source get_global_alloc/get_alloc_raw including initializer→before_access_global→adjust hooks and owned-only caching.

Equations

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