Runtime symbolic-vtable rules from pinned interpret/traits.rs and memory.rs. The selected tree has no interpret/vtable.rs. Global allocation identity, compiler predicates and function ABI checking are required leaves.

structure Miri.Interpreter.VTablePredicate : Type

• id : Nat
• stableKey : Nat
• autoTrait : Bool

def Miri.Interpreter.instDecidableEqVTablePredicate.decEq (x✝ x✝¹ : VTablePredicate) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqVTablePredicate : DecidableEq VTablePredicate

Equations

• Miri.Interpreter.instDecidableEqVTablePredicate = Miri.Interpreter.instDecidableEqVTablePredicate.decEq

@[instance_reducible]

instance Miri.Interpreter.instReprVTablePredicate : Repr VTablePredicate

Equations

• Miri.Interpreter.instReprVTablePredicate = { reprPrec := Miri.Interpreter.instReprVTablePredicate.repr }

def Miri.Interpreter.instReprVTablePredicate.repr : VTablePredicate → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.VTablePointerError : Type

• danglingInteger : VTablePointerError
• other (error : StepError) : VTablePointerError

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqVTablePointerError : DecidableEq VTablePointerError

Equations

• Miri.Interpreter.instDecidableEqVTablePointerError = Miri.Interpreter.instDecidableEqVTablePointerError.decEq

def Miri.Interpreter.instDecidableEqVTablePointerError.decEq (x✝ x✝¹ : VTablePointerError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqVTablePointerError.decEq Miri.Interpreter.VTablePointerError.danglingInteger Miri.Interpreter.VTablePointerError.danglingInteger = isTrue ⋯
• Miri.Interpreter.instDecidableEqVTablePointerError.decEq Miri.Interpreter.VTablePointerError.danglingInteger (Miri.Interpreter.VTablePointerError.other error) = isFalse ⋯
• Miri.Interpreter.instDecidableEqVTablePointerError.decEq (Miri.Interpreter.VTablePointerError.other error) Miri.Interpreter.VTablePointerError.danglingInteger = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprVTablePointerError : Repr VTablePointerError

Equations

• Miri.Interpreter.instReprVTablePointerError = { reprPrec := Miri.Interpreter.instReprVTablePointerError.repr }

def Miri.Interpreter.instReprVTablePointerError.repr : VTablePointerError → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.VTableEntry (F : Type) : Type

• dropInPlace {F : Type} : VTableEntry F
• size {F : Type} : VTableEntry F
• align {F : Type} : VTableEntry F
• vacant {F : Type} : VTableEntry F
• method {F : Type} (function : F) : VTableEntry F
• traitVPtr {F : Type} (traitRef : Nat) : VTableEntry F

structure Miri.Interpreter.VTableHooks (P S C F ABI : Type) : Type

• target : Miri.ABI.TargetDataLayout
• isDynamic : C → MIR.TyId → RvalueM S Bool
• memoryOffset : C → MemPlace P → Miri.ABI.Size → OffsetMode → MemPlaceMeta P → RvalueM S (MemPlace P)
• resolvePointer : C → Memory.Pointer (Option P) → RvalueM S (Except VTablePointerError (Memory.AllocId × Miri.ABI.Size))
• globalVTable : C → Memory.AllocId → RvalueM S (Option (MIR.TyId × Nat))
• globalFunction : C → Memory.AllocId → RvalueM S (Option F)
• predicates : C → Nat → RvalueM S (Array VTablePredicate)
• normalizePredicate : C → VTablePredicate → RvalueM S Nat
• layoutOf : C → MIR.TyId → RvalueM S (Miri.ABI.TyAndLayout MIR.TyId)
• eraseAndAnonymize : C → MIR.TyId → Nat → RvalueM S (MIR.TyId × Nat)
• ensureMonomorphicType : C → MIR.TyId → RvalueM S Unit
• ensureMonomorphicDyn : C → Nat → RvalueM S Unit
• globalSalt : C → RvalueM S Nat
• reserveVTable : C → MIR.TyId → Nat → Nat → RvalueM S Memory.AllocId
• globalRootPointer : C → Memory.AllocId → RvalueM S (Memory.Pointer (Option P))
• entries : C → Option Nat → MIR.TyId → RvalueM S (Array (VTableEntry F))
• assertVirtualInstanceMatches : C → MIR.TyId → MIR.DefId → F → F → RvalueM S Unit

structure Miri.Interpreter.VTableReadHooks (P S C : Type) : Type

Source symbolic reads separated from reservation and virtual calls, so machine-level dynamic layout needs no placeholder operational dictionary.

• resolvePointer : C → Memory.Pointer (Option P) → RvalueM S (Except VTablePointerError (Memory.AllocId × ABI.Size))
• globalVTable : C → Memory.AllocId → RvalueM S (Option (MIR.TyId × Nat))
• predicates : C → Nat → RvalueM S (Array VTablePredicate)
• normalizePredicate : C → VTablePredicate → RvalueM S Nat
• layoutOf : C → MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)

def Miri.Interpreter.VTableHooks.readHooks {P S C F A : Type} (h : VTableHooks P S C F A) : VTableReadHooks P S C

Equations

• h.readHooks = { resolvePointer := h.resolvePointer, globalVTable := h.globalVTable, predicates := h.predicates, normalizePredicate := h.normalizePredicate, layoutOf := h.layoutOf }

def Miri.Interpreter.VTable.checkForTypeRead {P S C : Type} (h : VTableReadHooks P S C) (choice : C) (actual expected : Nat) : RvalueM S Unit

Source ignores auto traits, sorts by compiler stable comparison, removes identical predicates, then normalizes each paired predicate before equality.

Equations

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

def Miri.Interpreter.VTable.getPtrVTableTypeRead {P S C : Type} (h : VTableReadHooks P S C) (choice : C) (ptr : Memory.Pointer (Option P)) (expectedTrait : Option Nat) : RvalueM S MIR.TyId

Equations

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

def Miri.Interpreter.VTable.getSizeAndAlignRead {P S C : Type} (h : VTableReadHooks P S C) (choice : C) (ptr : Memory.Pointer (Option P)) (expectedTrait : Option Nat) : RvalueM S (ABI.Size × ABI.Align)

The interpreter consults the symbolic VTable allocation's type and layout; it does not trust or load the raw size/alignment words of arbitrary memory.

Equations

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

def Miri.Interpreter.VTable.checkForType {P S C F A : Type} (h : VTableHooks P S C F A) (choice : C) (actual expected : Nat) : RvalueM S Unit

Equations

• Miri.Interpreter.VTable.checkForType h choice actual expected = Miri.Interpreter.VTable.checkForTypeRead h.readHooks choice actual expected

def Miri.Interpreter.VTable.getPtrVTableType {P S C F A : Type} (h : VTableHooks P S C F A) (choice : C) (ptr : Memory.Pointer (Option P)) (expectedTrait : Option Nat) : RvalueM S MIR.TyId

Equations

• Miri.Interpreter.VTable.getPtrVTableType h choice ptr expectedTrait = Miri.Interpreter.VTable.getPtrVTableTypeRead h.readHooks choice ptr expectedTrait

def Miri.Interpreter.VTable.getSizeAndAlign {P S C F A : Type} (h : VTableHooks P S C F A) (choice : C) (ptr : Memory.Pointer (Option P)) (expectedTrait : Option Nat) : RvalueM S (ABI.Size × ABI.Align)

Equations

• Miri.Interpreter.VTable.getSizeAndAlign h choice ptr expectedTrait = Miri.Interpreter.VTable.getSizeAndAlignRead h.readHooks choice ptr expectedTrait

def Miri.Interpreter.VTable.getPointer {P S C F A : Type} (h : VTableHooks P S C F A) (choice : C) (ty : MIR.TyId) (dynType : Nat) : RvalueM S (Memory.Pointer (Option P))

Equations

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

def Miri.Interpreter.VTable.getPtrFn {P S C F A : Type} (h : VTableHooks P S C F A) (choice : C) (ptr : Memory.Pointer (Option P)) : RvalueM S F

This resolves allocation identity only, as memory.rs::get_ptr_fn does. Calling it requires ABI/type validation at the actual Call pipeline stage.

Equations

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

def Miri.Interpreter.VTable.getCallableFunction {P S C F A : Type} (h : VTableHooks P S C F A) (validateABI : C → F → A → RvalueM S Unit) (choice : C) (ptr : Memory.Pointer (Option P)) (expectedABI : A) : RvalueM S F

Equations

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

def Miri.Interpreter.VTable.getMethod {P S C F A : Type} (h : VTableHooks P S C F A) (validateABI : C → F → A → RvalueM S Unit) (choice : C) (ptr : Memory.Pointer (Option P)) (expectedTrait : Nat) (principal : Option Nat) (index : Nat) (definition : MIR.DefId) (virtualInstance : F) (expectedABI : A) : RvalueM S F

Explicit checked utility for virtual method resolution. This extra ABI validation is caller-selected; production call.rs validates at frame initialization. Wrong/vacant/header/supertrait entries are UB, never callable functions.

Equations

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

def Miri.Interpreter.VTable.unpackDynTrait {P S C F A : Type} [Memory.PointerProvenance P] (h : VTableHooks P S C F A) (choice : C) (op : OpTy P) (expectedTrait : Nat) : RvalueM S (OpTy P)

Source unpack_dyn_trait operates only on an indirect dynamic place, then changes its layout at zero wrapping offset while clearing the metadata.

Equations

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

def Miri.Interpreter.VTable.readMemoryScalar {K P E H PE : Type} [DecidableEq K] [DecidableEq P] [Memory.PointerProvenance P] (memory : Memory.MemoryState P E K) (state : H) (place : MemPlace P) (layout : ABI.TyAndLayout MIR.TyId) (runtime : ABI.RuntimeTargetDataLayout) (ghostMode : Bool) (globalKind : Option K) (globalHooks : Memory.GlobalAllocationHooks P E K H) (accessHooks : Memory.AllocationAccessHooks P E K H PE) (dynamicLayout : DynamicLayoutResolver P E K H) : MemoryOperandResult P E K H (Memory.Scalar P)

When a consumer actually loads a scalar field, retain the existing typed memory-read pipeline and all access/provenance hooks. Symbolic size/alignment lookup above deliberately does not call this helper.

Equations

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