Pinned intrinsics.rs write_type_id/read_type_id and memory.rs get_ptr_type_id. TypeId hashes remain decorated with compiler-owned provenance; integer equality alone cannot validate a forged TypeId.

structure Miri.Interpreter.IntrinsicTypeIdHooks (P S C V : Type) : Type

• target : ABI.TargetDataLayout
• hasErasableRegions : C → MIR.TyId → RvalueM S Bool
• typeHash : C → MIR.TyId → RvalueM S ABI.U128
• u128Layout : C → RvalueM S (ABI.TyAndLayout MIR.TyId)
• unitLayout : C → RvalueM S (ABI.TyAndLayout MIR.TyId)
• reserveTypeId : C → MIR.TyId → RvalueM S Memory.AllocId
• globalRootPointer : C → Memory.AllocId → ABI.Size → RvalueM S (Memory.Pointer P)
• resolvePointer : C → Memory.Pointer (Option P) → RvalueM S (Memory.AllocId × ABI.Size)
• globalTypeId : C → Memory.AllocId → RvalueM S (Option MIR.TyId)
• placeLayout : V → ABI.TyAndLayout MIR.TyId
• copyAllowTransmute : C → OpTy P → V → RvalueM S Unit
• projectFieldRead : C → OpTy P → Nat → RvalueM S (OpTy P)
• projectFieldWrite : C → V → Nat → RvalueM S V
• elementLayout : C → ABI.TyAndLayout MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)
• offsetRead : C → OpTy P → ABI.Size → OffsetMode → ABI.TyAndLayout MIR.TyId → RvalueM S (OpTy P)
• offsetWrite : C → V → ABI.Size → OffsetMode → ABI.TyAndLayout MIR.TyId → RvalueM S V
• readImmediate : C → OpTy P → RvalueM S (RvalueImmTy P)
• readPlaceScalar : C → V → RvalueM S (Memory.Scalar P)
• writeScalar : C → Memory.Scalar P → V → RvalueM S Unit

def Miri.Interpreter.IntrinsicTypeId.getPointerType {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicTypeIdHooks P S C V) (choice : C) (pointer : Memory.Pointer (Option P)) : RvalueM S (MIR.TyId × UInt64)

Source get_ptr_type_id checks the global allocation kind, retaining the pointer offset as its hash fragment rather than requiring a zero offset.

Equations

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

def Miri.Interpreter.IntrinsicTypeId.write {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicTypeIdHooks P S C V) (choice : C) (ty : MIR.TyId) (dest : V) : RvalueM S Unit

Equations

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

def Miri.Interpreter.IntrinsicTypeId.read {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicTypeIdHooks P S C V) (choice : C) (op : OpTy P) : RvalueM S MIR.TyId

Equations

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