Checked reuse of real rustc normalization and Const::eval query results. Sources: ty/instance.rs::try_instantiate_mir_and_normalize_erasing_regions; mir/consts.rs::Const::eval; Miri operand.rs::eval_const_to_op. A query key contains the complete instance, source body, MIR location and structural operand path. A source span alone is never an identity. Failed or absent compiler queries remain obligations and fail when requested.

inductive Miri.Input.CompilerConstantQueries.PathElement : Type

• field (name : String) : PathElement
• index (value : Nat) : PathElement

@[instance_reducible]

instance Miri.Input.CompilerConstantQueries.instReprPathElement : Repr PathElement

Equations

• Miri.Input.CompilerConstantQueries.instReprPathElement = { reprPrec := Miri.Input.CompilerConstantQueries.instReprPathElement.repr }

def Miri.Input.CompilerConstantQueries.instReprPathElement.repr : PathElement → Nat → Std.Format

Equations

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

def Miri.Input.CompilerConstantQueries.instDecidableEqPathElement.decEq (x✝ x✝¹ : PathElement) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Input.CompilerConstantQueries.instDecidableEqPathElement : DecidableEq PathElement

Equations

• Miri.Input.CompilerConstantQueries.instDecidableEqPathElement = Miri.Input.CompilerConstantQueries.instDecidableEqPathElement.decEq

structure Miri.Input.CompilerConstantQueries.Site : Type

• bodyIndex : Nat
• location : MIR.Location
• path : Array PathElement

@[instance_reducible]

instance Miri.Input.CompilerConstantQueries.instReprSite : Repr Site

Equations

• Miri.Input.CompilerConstantQueries.instReprSite = { reprPrec := Miri.Input.CompilerConstantQueries.instReprSite.repr }

def Miri.Input.CompilerConstantQueries.instReprSite.repr : Site → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Input.CompilerConstantQueries.instDecidableEqSite : DecidableEq Site

Equations

• Miri.Input.CompilerConstantQueries.instDecidableEqSite = Miri.Input.CompilerConstantQueries.instDecidableEqSite.decEq

def Miri.Input.CompilerConstantQueries.instDecidableEqSite.decEq (x✝ x✝¹ : Site) : Decidable (x✝ = x✝¹)

Equations

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

structure Miri.Input.CompilerConstantQueries.Evidence : Type

• site : Site
• query : Interpreter.CompilerConstantEvidence
• sourcePayload : Lean.Json
• normalizedPayload : Lean.Json

structure Miri.Input.CompilerConstantQueries.Prepared : Type

• program : LoweredProgram
• evidence : Array Evidence
• obligations : Array Obligation

A source compatibility check is deep over JSON. Production preparation does it once, then carries this binding with the exact values it checked. The private constructor and dependent indices prevent a caller from supplying an arbitrary cached Boolean or reusing it for different metadata.

structure Miri.Input.CompilerConstantQueries.Binding (prepared : Prepared) (runtime : RuntimeMetadata) : Type

• compatible : Bool
• correct : self.compatible = (runtime.source.raw == prepared.program.input.raw)

def Miri.Input.CompilerConstantQueries.bind (prepared : Prepared) (runtime : RuntimeMetadata) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw) := none) : Binding prepared runtime

Equations

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

def Miri.Input.CompilerConstantQueries.prepareProfiled (profile : Lean.Options) (input : LoweredProgram) : Except String Prepared

Build only from explicit exporter compiler-query context. In particular, monomorphic-looking syntax is never taken as evidence of normalization.

Equations

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

def Miri.Input.CompilerConstantQueries.prepare (input : LoweredProgram) : Except String Prepared

Equations

• Miri.Input.CompilerConstantQueries.prepare input = Miri.Input.CompilerConstantQueries.prepareProfiled ∅ input

def Miri.Input.CompilerConstantQueries.queriesAt {P E K H : Type} (prepared : Prepared) (site : Site) (machine : Interpreter.ConstantQueries P E K H) : Interpreter.ConstantQueries P E K H

Bind the exact interpreter source site before evaluation. All machine provenance/extern-static leaves retain their stateful failure behavior.

Equations

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