Connected pinned interpret/cast.rs dispatcher and recursive unsizing. Compiler-owned type descriptions are metadata queries, not a program IR. Machine provenance, memory access/copy and compiler resolution are explicit stateful leaves; none is replaced by successful approximation.

inductive Miri.Interpreter.CastTypeInfo : Type

• integer (kind : MIR.IntegerKind) : CastTypeInfo
• floating (format : FloatFormat) : CastTypeInfo
• boolean : CastTypeInfo
• character : CastTypeInfo
• rawPointer (pointee : MIR.TyId) : CastTypeInfo
• reference (pointee : MIR.TyId) : CastTypeInfo
• fnPointer : CastTypeInfo
• fnDefinition (definition : MIR.DefId) (args : Array MIR.GenericArg) : CastTypeInfo
• closure (definition : MIR.DefId) (args : Array MIR.GenericArg) (upvarCount : Nat) : CastTypeInfo
• pattern (inner : MIR.TyId) (patternId : Nat) : CastTypeInfo
• adt (definition : MIR.DefId) : CastTypeInfo
• array (element : MIR.TyId) (length : UInt64) : CastTypeInfo
• slice (element : MIR.TyId) : CastTypeInfo
• dynamic (predicates : Nat) : CastTypeInfo

def Miri.Interpreter.instDecidableEqCastTypeInfo.decEq (x✝ x✝¹ : CastTypeInfo) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqCastTypeInfo : DecidableEq CastTypeInfo

Equations

• Miri.Interpreter.instDecidableEqCastTypeInfo = Miri.Interpreter.instDecidableEqCastTypeInfo.decEq

@[instance_reducible]

instance Miri.Interpreter.instReprCastTypeInfo : Repr CastTypeInfo

Equations

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

def Miri.Interpreter.instReprCastTypeInfo.repr : CastTypeInfo → Nat → Std.Format

Equations

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

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

• target : ABI.TargetDataLayout
• typeInfo : C → MIR.TyId → RvalueM S CastTypeInfo
• layoutOf : C → MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)
• destLayout : V → ABI.TyAndLayout MIR.TyId
• readImmediate : C → OpTy P → RvalueM S (RvalueImmTy P)
• writeImmediate : C → Immediate P → V → RvalueM S Unit
• writePointer : C → Memory.Pointer (Option P) → V → RvalueM S Unit
• enforceValidity : C → ABI.TyAndLayout MIR.TyId → RvalueM S Bool
• enforceValidityRecursively : C → ABI.TyAndLayout MIR.TyId → RvalueM S Bool
• validatePlace : C → V → Bool → Bool → RvalueM S Unit
• derefPointer : C → OpTy P → RvalueM S Unit
• checkFunctionPointer : C → Memory.Pointer (Option P) → RvalueM S Unit
• exposeProvenance : C → P → RvalueM S Unit
• pointerFromExposedAddress : C → UInt64 → RvalueM S (Memory.Pointer (Option P))
• usizeLayout : C → RvalueM S (ABI.TyAndLayout MIR.TyId)
• floatOps : FloatOpsHooks P S C
• ensureMonomorphic : C → MIR.TyId → RvalueM S Unit
• requireNoBoundVars : C → Array MIR.GenericArg → RvalueM S Unit
• resolveFunction : C → MIR.DefId → Array MIR.GenericArg → RvalueM S (Option CallInstance)
• resolveClosureFnOnce : C → MIR.DefId → Array MIR.GenericArg → RvalueM S CallInstance
• functionPointer : C → CallInstance → RvalueM S (Memory.Pointer (Option P))
• builtinDeref : C → MIR.TyId → Bool → RvalueM S (Option MIR.TyId)
• boxLayout : C → MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)
• validateImmediateABI : Immediate P → ABI.LayoutData → Except StepError Unit
• copyAllowTransmute : C → OpTy P → V → RvalueM S Unit
• copyNoValidate : C → OpTy P → V → Bool → RvalueM S Unit
• projectRead : C → OpTy P → Nat → RvalueM S (OpTy P)
• projectWrite : C → V → Nat → RvalueM S V
• fieldLayout : C → ABI.TyAndLayout MIR.TyId → Nat → RvalueM S (ABI.TyAndLayout MIR.TyId)
• lockstepTails : C → MIR.TyId → MIR.TyId → RvalueM S (MIR.TyId × MIR.TyId)
• vtableType : C → Memory.Pointer (Option P) → Option Nat → RvalueM S MIR.TyId
• vtablePointer : C → MIR.TyId → Nat → RvalueM S (Memory.Pointer (Option P))
• principal : C → Nat → RvalueM S (Option Nat)
• vtableEntries : C → Option Nat → MIR.TyId → RvalueM S (Array (VTableEntry CallInstance))
• supertraitSlot : C → MIR.TyId → MIR.TyId → RvalueM S (Option Nat)
• eraseSelfTraitRef : C → Nat → RvalueM S Nat
• normalizePrincipal : C → Nat → RvalueM S (Option Nat)

def Miri.Interpreter.Cast.intLikeValue {P S C V : Type} [Memory.PointerProvenance P] (h : CastHooks P S C V) (choice : C) (scalar : Memory.Scalar P) (source : ABI.TyAndLayout MIR.TyId) : RvalueM S (ABI.U128 × Bool)

Source cast_from_int_like's u128 intermediate, after typed validity conversion. Pointer inputs use the existing provenance-aware Scalar conversion; no pointer address approximation or provenance clearing occurs here.

Equations

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

def Miri.Interpreter.Cast.castFromIntLike {P S C V : Type} [Memory.PointerProvenance P] (h : CastHooks P S C V) (choice : C) (scalar : Memory.Scalar P) (source target : ABI.TyAndLayout MIR.TyId) : RvalueM S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.Cast.ptrToPtr {P S C V : Type} [Memory.PointerProvenance P] (h : CastHooks P S C V) (choice : C) (source : RvalueImmTy P) (target : ABI.TyAndLayout MIR.TyId) : RvalueM S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.Cast.pointerExposeProvenance {P S C V : Type} [Memory.PointerProvenance P] (h : CastHooks P S C V) (choice : C) (source : RvalueImmTy P) (target : ABI.TyAndLayout MIR.TyId) : RvalueM S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.Cast.pointerWithExposedProvenance {P S C V : Type} [Memory.PointerProvenance P] (h : CastHooks P S C V) (choice : C) (source : RvalueImmTy P) (target : ABI.TyAndLayout MIR.TyId) : RvalueM S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.Cast.unsizeIntoPointer {P S C V : Type} [Memory.PointerProvenance P] (h : CastHooks P S C V) (choice : C) (source : OpTy P) (dest : V) (sourceTy targetTy : MIR.TyId) : RvalueM S Unit

Source unsize_into_ptr, including dynamic upcast slot/prefix assertions.

Equations

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

def Miri.Interpreter.Cast.unsizeInto {P S C V : Type} [Memory.PointerProvenance P] (h : CastHooks P S C V) (choice : C) (fuel : Nat) (source : OpTy P) (target : ABI.TyAndLayout MIR.TyId) (dest : V) : RvalueM S Unit

Recursive source aggregate unsizing. Earlier field copies stay committed when a later field fails, including the second-changing-field invariant.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.Cast.unsizeInto h choice 0 source target dest = throw (Miri.Interpreter.StepError.resourceExhaustion "cast unsizing recursion fuel")

def Miri.Interpreter.Cast.cast {P S C V : Type} [Memory.PointerProvenance P] (h : CastHooks P S C V) (choice : C) (fuel : Nat) (source : OpTy P) (kind : MIR.CastKind) (castTy : MIR.TyId) (dest : V) : RvalueM S Unit

Full source cast dispatch. Cast layout resolution precedes source validity, which is skipped exactly for transmute/subtype/box-deref and unsizing.

Equations

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