Imported rustc GlobalAlloc::TypeId nodes seed the actual intrinsic symbol registry before runtime reserve_and_set_type_id_alloc. Input allocation IDs and runtime allocation IDs are connected only by the imported memory map.

def Miri.Input.CompilerIntrinsicSymbols.typeHash (p : CompilerProviders.Prepared) (ty : MIR.TyId) : Except String ABI.U128

Equations

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

def Miri.Input.CompilerIntrinsicSymbols.importedTypeId {P E K : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (memory : Memory.MemoryState P E K) (id : Memory.AllocId) : Except String (Option MIR.TyId)

Equations

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

def Miri.Input.CompilerIntrinsicSymbols.seedImported {P E K : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (memory : Memory.MemoryState P E K) (initial : Interpreter.IntrinsicSymbolsMachine.Registry) : Except String Interpreter.IntrinsicSymbolsMachine.Registry

Equations

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

def Miri.Input.CompilerIntrinsicSymbols.attachProfiled {U K : Type} (profile : Lean.Options) (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (registry : Interpreter.IntrinsicSymbolsMachine.Access U) : Interpreter.MachineHooks.M K U Unit

Equations

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

def Miri.Input.CompilerIntrinsicSymbols.attach {U K : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (registry : Interpreter.IntrinsicSymbolsMachine.Access U) : Interpreter.MachineHooks.M K U Unit

Equations

• Miri.Input.CompilerIntrinsicSymbols.attach p image registry = Miri.Input.CompilerIntrinsicSymbols.attachProfiled ∅ p image registry

theorem Miri.Input.CompilerIntrinsicSymbols.attach_profile_identity {K U : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (registry : Interpreter.IntrinsicSymbolsMachine.Access U) : attach p image registry = attachProfiled ∅ p image registry

def Miri.Input.CompilerIntrinsicSymbols.typeIdLeaves {K U C : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) : Interpreter.IntrinsicSymbolsMachine.TypeIdLeaves K U C

Missing hash/region compiler metadata remains a source query failure. The registry preparation above must execute before the first dynamic reservation.

Equations

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