Actual imported GlobalAlloc::Function/VTable identity leaves. Runtime allocation IDs are resolved through AllocationImage's mapping, never equated with exported IDs. Complete instances share the program's compiler tables.

@[reducible, inline]

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

Equations

• Miri.Input.CompilerVTableRuntime.Result = Except String

structure Miri.Input.CompilerVTableRuntime.InstanceEvidence : Type

• id : InstanceId
• outcome : Result Interpreter.CallInstance

structure Miri.Input.CompilerVTableRuntime.ArrayReflexivity {α : Type} [BEq α] (values : Array α) : Type

• checked : Option (PLift ((values == values) = true))

structure Miri.Input.CompilerVTableRuntime.Prepared : Type

• facts : CompilerFactAdapters.Prepared
• instances : Array InstanceEvidence
• obligations : Array Obligation

def Miri.Input.CompilerVTableRuntime.prepare (facts : CompilerFactAdapters.Prepared) : Prepared

Decode every registered instance, including callable shims without MIR. Body availability is not required to establish the full function identity. Missing identity evidence remains a per-instance error, not a guessed Item.

Equations

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

structure Miri.Input.CompilerVTableRuntime.GlobalLookup (prepared : Prepared) : Type

• instanceRows : Array Miri.Input.CompilerVTableRuntime.InstanceEvidence
• instanceBuckets : Std.HashMap Nat (Array Miri.Input.CompilerVTableRuntime.InstanceEvidence)
• exactInstances : instanceRows self = prepared.instances
• definitionRows : Array Miri.Input.DefinitionId
• definitionIndex : Std.HashMap (Nat × Nat) Nat
• exactDefinitions : definitionRows self = prepared.facts.context.program.compilerTables.definitions
• definitionReflexivity : Miri.Input.CompilerVTableRuntime.ArrayReflexivity (definitionRows self)
• typeConstantRows : Array Miri.MIR.TypeConst
• exactTypeConstants : typeConstantRows self = prepared.facts.context.program.compilerTables.typeConstants
• typeConstantReflexivity : Miri.Input.CompilerVTableRuntime.ArrayReflexivity (typeConstantRows self)

def Miri.Input.CompilerVTableRuntime.GlobalLookup.prepare (prepared : Prepared) : GlobalLookup prepared

Equations

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

def Miri.Input.CompilerVTableRuntime.functionInstanceUsing (prepared : Prepared) (lookup : GlobalLookup prepared) (id : InstanceId) : Result Interpreter.CallInstance

Equations

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

def Miri.Input.CompilerVTableRuntime.functionInstance (prepared : Prepared) (id : InstanceId) : Result Interpreter.CallInstance

Equations

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

def Miri.Input.CompilerVTableRuntime.globalFunctionUsing {P E K : Type} (prepared : Prepared) (lookup : GlobalLookup prepared) (image : AllocationImage.Imported) (memory : Memory.MemoryState P E K) (id : Memory.AllocId) : Result (Option Interpreter.CallInstance)

Equations

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

def Miri.Input.CompilerVTableRuntime.globalFunction {P E K : Type} (prepared : Prepared) (image : AllocationImage.Imported) (memory : Memory.MemoryState P E K) (id : Memory.AllocId) : Result (Option Interpreter.CallInstance)

Equations

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

def Miri.Input.CompilerVTableRuntime.globalVTable {P E K : Type} (prepared : Prepared) (image : AllocationImage.Imported) (memory : Memory.MemoryState P E K) (id : Memory.AllocId) : Result (Option (MIR.TyId × Nat))

Equations

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

def Miri.Input.CompilerVTableRuntime.globalVTableUsing {P E K : Type} (prepared : Prepared) (_lookup : GlobalLookup prepared) (image : AllocationImage.Imported) (memory : Memory.MemoryState P E K) (id : Memory.AllocId) : Result (Option (MIR.TyId × Nat))

Equations

• Miri.Input.CompilerVTableRuntime.globalVTableUsing prepared _lookup image memory id = Miri.Input.CompilerVTableRuntime.globalVTable prepared image memory id

def Miri.Input.CompilerVTableRuntime.queryTargetPrincipal (facts : CompilerFactAdapters.Prepared) (raw : Lean.Json) (sourceType allocationId : Nat) : Result Nat

Resolve a memory-backed vtable through the exact compiler allocation ID recorded for a principal/type query. Query metadata alone is not enough: the source TraitVPtr allocation must equal this ID. Each row must agree with its complete predicate key, while rows sharing the allocation must agree on the allocation's type, compiler-normalized principal, layout, and entries. A named HRTB and its instantiated principal can legitimately share this memory image; their symbolic type/predicate/salt keys remain distinct.

Equations

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

def Miri.Input.CompilerVTableRuntime.supertraitPrincipal (prepared : Prepared) (sourceType : MIR.TyId) (entry : VtableEntry) : Result Nat

Recover the target principal only through the exact serialized compiler allocation identity. A direct .vtable node carries its own type/principal; rustc may instead serialize the same global allocation as memory, in which case the query row's vtable_allocation_id is the required identity join.

Equations

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

def Miri.Input.CompilerVTableRuntime.entriesUsing (prepared : Prepared) (lookup : GlobalLookup prepared) (expectedPrincipal : Option Nat) (ty : MIR.TyId) : Result (Array (Interpreter.VTableEntry Interpreter.CallInstance))

Actual compiler vtable_entries result keyed by its concrete type and exact compiler principal. Repeated symbolic allocations must provide identical query results; allocation-ID coincidence and type-size inference are never keys.

Equations

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

def Miri.Input.CompilerVTableRuntime.entries (prepared : Prepared) (expectedPrincipal : Option Nat) (ty : MIR.TyId) : Result (Array (Interpreter.VTableEntry Interpreter.CallInstance))

Equations

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

def Miri.Input.CompilerVTableRuntime.hooks {S P E K C Abi : Type} (prepared : Prepared) (image : AllocationImage.Imported) (memory : S → Memory.MemoryState P E K) (base : Interpreter.VTableHooks P S C Interpreter.CallInstance Abi) : Interpreter.VTableHooks P S C Interpreter.CallInstance Abi

Install imported symbolic allocation queries with canonical machine memory. Address resolution and vtable-entry/principal queries remain required leaves; this does not manufacture them from the selected pointer's bytes.

Equations

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