Actual compiler ValueNS path resolution and const_eval_instance evidence for helpers.rs::eval_path_scalar/eval_libc. Original full constant identity, query environment, type, value and raw payload remain available. Allocation values use the canonical Constant pipeline, preserving graph provenance.

structure Miri.Input.CompilerNamedConstants.Value : Type

• sourceInstance : Interpreter.CallInstance
• ty : MIR.TyId
• value : MIR.ConstValue

structure Miri.Input.CompilerNamedConstants.Entry : Type

• name : String
• result : Except String Value
• payload : Lean.Json

structure Miri.Input.CompilerNamedConstants.Prepared : Type

• program : LoweredProgram
• runtime : RuntimeMetadata
• entries : Array Entry

def Miri.Input.CompilerNamedConstants.prepare (runtime : RuntimeMetadata) (program : LoweredProgram) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw) := none) : Except String Prepared

Equations

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

def Miri.Input.CompilerNamedConstants.value (prepared : Prepared) (name : String) : Except String Value

Equations

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

def Miri.Input.CompilerNamedConstants.scalar {P : Type} (prepared : Prepared) (name : String) : Except String (Memory.Scalar P)

Scalar-only fast path preserves the actual bits and byte width. Allocation pointers/slices/indirect values require toOp and actual global memory hooks.

Equations

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

def Miri.Input.CompilerNamedConstants.i32 (prepared : Prepared) (name : String) : Except String Int32

Equations

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

def Miri.Input.CompilerNamedConstants.toOp {K P E H : Type} [DecidableEq K] (prepared : Prepared) (queries : Interpreter.ConstantQueries P E K H) (name : String) : Interpreter.ConstantM P E K H (Interpreter.OpTy P)

Equations

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