Bind only exported, exact compilation-local compiler query evidence to runtime virtual-call drivers. Unexported trait-principal/instance-rebasing/drop queries remain required leaves in the original dictionary.

@[reducible, inline]

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

Equations

• Miri.Input.CompilerVirtualFacts.Result = Except String

def Miri.Input.CompilerVirtualFacts.receiverKind (context : CompilerFacts.Context) (id : TypeId) : Result Interpreter.VirtualCalls.ReceiverKind

Equations

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

def Miri.Input.CompilerVirtualFacts.dynamicData (prepared : CompilerFactAdapters.Prepared) (id : TypeId) : Result (Option Interpreter.VirtualCalls.DynamicData)

The compiler exports predicates.principal() through the same bound existential-predicate interner as trait checking. Missing legacy fields fail.

Equations

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

def Miri.Input.CompilerVirtualFacts.compilerHooks {S C : Type} (prepared : CompilerFactAdapters.Prepared) (base : Interpreter.VirtualCalls.CompilerHooks S C) : Interpreter.VirtualCalls.CompilerHooks S C

Every installed query is backed by an actual fully-monomorphized compiler record or canonical type/layout evidence. This does not solve instances or construct a raw-pointer/ref type by searching for a same-sized layout.

Equations

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

def Miri.Input.CompilerVirtualFacts.inlineAttribute (prepared : CompilerScopes.Prepared) (fnInstance : Interpreter.CallInstance) : Result (Option Bool)

Source inlinecallee attribute evidence is optional only when that full instance does not occur in any inline scope. Conflicts/unresolved entries are errors; they must not be hidden by a fallback query.

Equations

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

def Miri.Input.CompilerVirtualFacts.scopeHooks {S C : Type} (prepared : CompilerScopes.Prepared) (base : Interpreter.VirtualCalls.CompilerHooks S C) : Interpreter.VirtualCalls.CompilerHooks S C

The canonical body key comes directly from the saved frame. Body equality is only a consistency assertion after indexing, never a body lookup strategy. A non-inlined instance's attribute still uses the mandatory base query.

Equations

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

def Miri.Input.CompilerVirtualFacts.runtimeHooks {S C : Type} (prepared : CompilerRuntimeQueries.Prepared) (base : Interpreter.VirtualCalls.CompilerHooks S C) : Interpreter.VirtualCalls.CompilerHooks S C

Actual compiler Ty::new_mut_ptr/new_mut_ref, resolve_drop_glue and requires_caller_location evidence. Missing keys fail; no structural type search or synthetic function/ABI is introduced.

Equations

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

def Miri.Input.CompilerVirtualFacts.hooks {P S C E : Type} (prepared : CompilerFactAdapters.Prepared) (base : Interpreter.VirtualCalls.Hooks P S C E) : Interpreter.VirtualCalls.Hooks P S C E

Both type and vtable trait predicates consume the same compiler predicate array table; no principal identity is synthesized from a diagnostic string.

Equations

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