Reservation identity is the erased concrete type, predicates and runtime salt. A compiler CTFE salt-zero probe is not a witness for an arbitrary runtime cast: pinned Miri chooses among 32 salts. Dense export IDs are not observable raw AllocIds. Prepared catalogs certify the post-export TyCtxt continuation only; missing keys must keep their Unsupported result.

Source traits.rs symbolic vtable reservations. Vtables are not data bytes: raw dereference is rejected by canonical MemoryState.getGlobalAlloc.

structure Miri.Interpreter.VTableMachine.Entry : Type

• typeId : MIR.TyId
• dynamicType : Nat
• salt : Fin 32
• allocation : Memory.AllocId

structure Miri.Interpreter.VTableMachine.Registry : Type

• entries : Array Entry

def Miri.Interpreter.VTableMachine.Registry.empty : Registry

Equations

• Miri.Interpreter.VTableMachine.Registry.empty = { entries := #[] }

def Miri.Interpreter.VTableMachine.Registry.mergePersistent (fresh live : Registry) : Except String Registry

Merge the source-TCX symbolic vtable reservations into a fresh EvalWorld. The key is the already erased/anonymized compiler type and dynamic predicate identity together with Miri's allocation salt.

Equations

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

def Miri.Interpreter.VTableMachine.Registry.ensureDisjointFromFunctions {Other : Type} (vtables : Registry) (functions : FunctionPointers.Registry Other) : Except String Unit

A source AllocId cannot denote both a symbolic vtable and either kind of function pointer stored by FunctionPointers.

Equations

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

def Miri.Interpreter.VTableMachine.Registry.restoreGlobals {P E K : Type} (vtables : Registry) (fresh live : Memory.MemoryState P E K) : Except String (Memory.MemoryState P E K)

Restore the symbolic global metadata associated with persistent runtime vtable identities. Existing fresh-world globals must be one well-formed vtable; otherwise the same ID is already occupied by an incompatible allocation.

Equations

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

structure Miri.Interpreter.VTableMachine.Hooks (K User Other : Type) : Type

• functions : FunctionPointers.Hooks K User Other
• registry : User → Registry
• putRegistry : User → Registry → User
• target : ABI.RuntimeTargetDataLayout
• importedVTable : Memory.AllocId → MachineHooks.M K User (Option (MIR.TyId × Nat))

def Miri.Interpreter.VTableMachine.reserve {K User Other : Type} (h : Hooks K User Other) (ty : MIR.TyId) (dynType : Nat) (salt : Fin 32) : MachineHooks.M K User Memory.AllocId

Source reserve_and_set_vtable_alloc key includes salt and both erased compiler identities. Metadata uses source pointer alignment and size zero.

Equations

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

def Miri.Interpreter.VTableMachine.globalVTable {K User Other : Type} (h : Hooks K User Other) (id : Memory.AllocId) : MachineHooks.M K User (Option (MIR.TyId × Nat))

Equations

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

def Miri.Interpreter.VTableMachine.hooks {K User Other C ABI : Type} (h : Hooks K User Other) (base : VTableHooks Memory.Provenance (MachineHooks.State K User) C CallInstance ABI) : VTableHooks Memory.Provenance (MachineHooks.State K User) C CallInstance ABI

Compiler erase/monomorphic/predicate/method queries stay in base; all symbolic allocation, provenance, salt and address operations are real state.

Equations

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