Source interpret/traits.rs::check_vtable_for_type (67-103): complete-binder predicate identities, real compiler stable_cmp ranks, and exact normalized identity after late-bound-region erasure. The same shared predicate-array table serves dyn types and exported symbolic vtables. No Debug string is a key.

@[reducible, inline]

abbrev Miri.Input.CompilerVTableFacts.Result (α : Type u_1) : Type u_1

Equations

• Miri.Input.CompilerVTableFacts.Result = Except String

def Miri.Input.CompilerVTableFacts.predicates (prepared : CompilerFactAdapters.Prepared) (token : Nat) : Result (Array Interpreter.VTablePredicate)

Equations

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

def Miri.Input.CompilerVTableFacts.normalizePredicate (prepared : CompilerFactAdapters.Prepared) (predicate : Interpreter.VTablePredicate) : Result Nat

Equations

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

def Miri.Input.CompilerVTableFacts.exportedArrayToken (prepared : CompilerFactAdapters.Prepared) (payload : Lean.Json) : Result Nat

Resolve an exported global-vtable predicate array through the shared table. Allocation source IDs are resolved by AllocationImage, separately from these compiler predicate-array identities.

Equations

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

def Miri.Input.CompilerVTableFacts.hooks {P S C Fn Abi : Type} (prepared : CompilerFactAdapters.Prepared) (machine : 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.