Exact get_vtable_ptr compiler stage from interpret/traits.rs: erase and anonymize the complete (type,predicate-list) pair, then source has_param checks. Symbolic allocation salt/reservation/root-pointer effects remain runtime actions.

structure Miri.Input.CompilerVTableQueries.Entry : Type

• inputType : TypeId
• inputPredicates : Nat
• outputType : TypeId
• outputPredicates : Nat
• typeMonomorphic : Bool
• predicatesMonomorphic : Bool
• diagnosticQueryId : Option Nat

structure Miri.Input.CompilerVTableQueries.Prepared : Type

• facts : CompilerFactAdapters.Prepared
• entries : Array Entry
• traceQueries : Bool

def Miri.Input.CompilerVTableQueries.prepare (facts : CompilerFactAdapters.Prepared) : Except String Prepared

Equations

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

def Miri.Input.CompilerVTableQueries.eraseAndAnonymize (prepared : Prepared) (ty : TypeId) (predicates : Nat) : Except String (TypeId × Nat)

Equations

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

theorem Miri.Input.CompilerVTableQueries.eraseAndAnonymize_trace_identity (prepared : Prepared) (ty : TypeId) (predicates : Nat) : eraseAndAnonymize { facts := prepared.facts, entries := prepared.entries, traceQueries := true } ty predicates = eraseAndAnonymize { facts := prepared.facts, entries := prepared.entries } ty predicates

Diagnostic output preserves the exact lookup, including missing-key errors.

def Miri.Input.CompilerVTableQueries.ensureMonomorphicType (prepared : Prepared) (ty : TypeId) : Except String Unit

Equations

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

def Miri.Input.CompilerVTableQueries.ensureMonomorphicDyn (prepared : Prepared) (predicates : Nat) : Except String Unit

Equations

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

def Miri.Input.CompilerVTableQueries.hooks {P S C Fn Abi : Type} (prepared : Prepared) (base : Interpreter.VTableHooks P S C Fn Abi) : Interpreter.VTableHooks P S C Fn Abi

Equations

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