Actual memory.rs TypeId globals and va_list_map. The maps start empty; allocation IDs come from the same MemoryState reserve supply as every other allocation. No Rust memory is allocated for symbolic TypeId/VaList entries. provenance_gc.rs::VisitProvenance(MiriInterpCx) visits alloc_map and machine, not rustc memory.va_list_map: these maps deliberately add no GC roots.

structure Miri.Interpreter.IntrinsicSymbolsMachine.Registry : Type

• typeIds : Array (Memory.AllocId × MIR.TyId)
• vaLists : Array (Memory.AllocId × List (RuntimePlace Memory.Provenance))

def Miri.Interpreter.IntrinsicSymbolsMachine.Registry.empty : Registry

Equations

• Miri.Interpreter.IntrinsicSymbolsMachine.Registry.empty = { typeIds := #[], vaLists := #[] }

structure Miri.Interpreter.IntrinsicSymbolsMachine.Access (U : Type) : Type

• get : U → Registry
• put : U → Registry → U

def Miri.Interpreter.IntrinsicSymbolsMachine.reserveTypeId {U K : Type} (registry : Access U) (ty : MIR.TyId) : MachineHooks.M K U Memory.AllocId

Equations

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

def Miri.Interpreter.IntrinsicSymbolsMachine.globalTypeId {U K : Type} (registry : Access U) (imported : Memory.AllocId → MachineHooks.M K U (Option MIR.TyId)) (id : Memory.AllocId) : MachineHooks.M K U (Option MIR.TyId)

Equations

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

structure Miri.Interpreter.IntrinsicSymbolsMachine.TypeIdLeaves (K U C : Type) : Type

• hasErasableRegions : C → MIR.TyId → MachineHooks.M K U Bool
• typeHash : C → MIR.TyId → MachineHooks.M K U ABI.U128
• u128Layout : C → MachineHooks.M K U LocalLayout
• unitLayout : C → MachineHooks.M K U LocalLayout
• importedTypeId : Memory.AllocId → MachineHooks.M K U (Option MIR.TyId)

def Miri.Interpreter.IntrinsicSymbolsMachine.typeId {K U C O : Type} [DecidableEq K] (leaves : TypeIdLeaves K U C) (registry : Access U) (access : PlaceMachine.AccessConfig K U) (functions : FunctionPointers.Hooks K U O) (operands : OperandMachine.Hooks K U C) (copy : PlaceCopyHooks Memory.Provenance (MachineHooks.State K U) C) : IntrinsicTypeIdHooks Memory.Provenance (MachineHooks.State K U) C (RuntimePlace Memory.Provenance)

Root-pointer tag/address effects execute before the hash-fragment offset is restored. TypeId allocations have source special address zero.

Equations

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

structure Miri.Interpreter.IntrinsicSymbolsMachine.VarArgsLeaves (K U C : Type) : Type

• layoutOf : C → MIR.TyId → MachineHooks.M K U LocalLayout
• typeInfo : C → MIR.TyId → MachineHooks.M K U VaTypeInfo
• identicalCTypes : C → MIR.TyId → MIR.TyId → MachineHooks.M K U Bool
• isCVoid : C → MIR.TyId → MachineHooks.M K U Bool
• vaListFields : C → MIR.TyId → MachineHooks.M K U (Array MIR.TyId)
• isRawPointer : C → MIR.TyId → MachineHooks.M K U Bool

def Miri.Interpreter.IntrinsicSymbolsMachine.varArgs {K U C O : Type} [DecidableEq K] (leaves : VarArgsLeaves K U C) (registry : Access U) (access : PlaceMachine.AccessConfig K U) (arithmetic : Memory.PointerArithmetic) (functions : FunctionPointers.Hooks K U O) (operands : OperandMachine.Hooks K U C) (copy : PlaceCopyHooks Memory.Provenance (MachineHooks.State K U) C) : IntrinsicVarArgsHooks Memory.Provenance (MachineHooks.State K U) C (RuntimePlace Memory.Provenance)

Equations

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