Source eval_context.rs::size_and_align_from_meta/size_and_align_of_val. Recursive compiler type traversal has explicit execution fuel; exhaustion is an error and never a fabricated dynamic size.

inductive Miri.Interpreter.DynamicTypeKind : Type

• adt (isSimd : Bool) : DynamicTypeKind
• tuple (isSimd : Bool) : DynamicTypeKind
• dynamic (expectedTrait : Nat) : DynamicTypeKind
• slice : DynamicTypeKind
• str : DynamicTypeKind
• foreign : DynamicTypeKind

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqDynamicTypeKind : DecidableEq DynamicTypeKind

Equations

• Miri.Interpreter.instDecidableEqDynamicTypeKind = Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq

def Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (x✝ x✝¹ : DynamicTypeKind) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.adt a) (Miri.Interpreter.DynamicTypeKind.adt b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.adt isSimd) (Miri.Interpreter.DynamicTypeKind.tuple isSimd_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.adt isSimd) (Miri.Interpreter.DynamicTypeKind.dynamic expectedTrait) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.adt isSimd) Miri.Interpreter.DynamicTypeKind.slice = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.adt isSimd) Miri.Interpreter.DynamicTypeKind.str = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.adt isSimd) Miri.Interpreter.DynamicTypeKind.foreign = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.tuple isSimd) (Miri.Interpreter.DynamicTypeKind.adt isSimd_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.tuple a) (Miri.Interpreter.DynamicTypeKind.tuple b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.tuple isSimd) (Miri.Interpreter.DynamicTypeKind.dynamic expectedTrait) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.tuple isSimd) Miri.Interpreter.DynamicTypeKind.slice = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.tuple isSimd) Miri.Interpreter.DynamicTypeKind.str = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.tuple isSimd) Miri.Interpreter.DynamicTypeKind.foreign = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.dynamic expectedTrait) (Miri.Interpreter.DynamicTypeKind.adt isSimd) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.dynamic expectedTrait) (Miri.Interpreter.DynamicTypeKind.tuple isSimd) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.dynamic a) (Miri.Interpreter.DynamicTypeKind.dynamic b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.dynamic expectedTrait) Miri.Interpreter.DynamicTypeKind.slice = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.dynamic expectedTrait) Miri.Interpreter.DynamicTypeKind.str = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq (Miri.Interpreter.DynamicTypeKind.dynamic expectedTrait) Miri.Interpreter.DynamicTypeKind.foreign = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq Miri.Interpreter.DynamicTypeKind.slice (Miri.Interpreter.DynamicTypeKind.adt isSimd) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq Miri.Interpreter.DynamicTypeKind.slice (Miri.Interpreter.DynamicTypeKind.tuple isSimd) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq Miri.Interpreter.DynamicTypeKind.slice (Miri.Interpreter.DynamicTypeKind.dynamic expectedTrait) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq Miri.Interpreter.DynamicTypeKind.slice Miri.Interpreter.DynamicTypeKind.slice = isTrue ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq Miri.Interpreter.DynamicTypeKind.str (Miri.Interpreter.DynamicTypeKind.adt isSimd) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq Miri.Interpreter.DynamicTypeKind.str (Miri.Interpreter.DynamicTypeKind.tuple isSimd) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq Miri.Interpreter.DynamicTypeKind.str (Miri.Interpreter.DynamicTypeKind.dynamic expectedTrait) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq Miri.Interpreter.DynamicTypeKind.str Miri.Interpreter.DynamicTypeKind.str = isTrue ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq Miri.Interpreter.DynamicTypeKind.foreign (Miri.Interpreter.DynamicTypeKind.adt isSimd) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq Miri.Interpreter.DynamicTypeKind.foreign (Miri.Interpreter.DynamicTypeKind.tuple isSimd) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq Miri.Interpreter.DynamicTypeKind.foreign (Miri.Interpreter.DynamicTypeKind.dynamic expectedTrait) = isFalse ⋯
• Miri.Interpreter.instDecidableEqDynamicTypeKind.decEq Miri.Interpreter.DynamicTypeKind.foreign Miri.Interpreter.DynamicTypeKind.foreign = isTrue ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprDynamicTypeKind : Repr DynamicTypeKind

Equations

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

def Miri.Interpreter.instReprDynamicTypeKind.repr : DynamicTypeKind → Nat → Std.Format

Equations

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

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

• target : ABI.TargetDataLayout
• maxSizeOfVal : ABI.Size
• classify : C → MIR.TyId → RvalueM S DynamicTypeKind
• field : C → ABI.TyAndLayout MIR.TyId → Nat → RvalueM S (ABI.TyAndLayout MIR.TyId)
• packedAlign : C → MIR.TyId → RvalueM S (Option ABI.Align)
• vtableSizeAndAlign : C → Memory.Pointer (Option P) → Option Nat → RvalueM S (ABI.Size × ABI.Align)

def Miri.Interpreter.DynamicLayout.sizeAndAlignFromMeta {P S C : Type} [Memory.PointerProvenance P] (h : DynamicLayoutHooks P S C) (choice : C) (fuel : Nat) (metadata : MemPlaceMeta P) (layout : ABI.TyAndLayout MIR.TyId) : RvalueM S (Option (ABI.Size × ABI.Align))

Exact sized fast path and all selected source unsized arms. Type IDs and canonical layouts remain paired through recursive field queries.

Equations

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

def Miri.Interpreter.DynamicLayout.sizeAndAlignOfVal {P S C : Type} [Memory.PointerProvenance P] (h : DynamicLayoutHooks P S C) (choice : C) (fuel : Nat) (value : OpTy P) : RvalueM S (Option (ABI.Size × ABI.Align))

Equations

• Miri.Interpreter.DynamicLayout.sizeAndAlignOfVal h choice fuel value = Miri.Interpreter.DynamicLayout.sizeAndAlignFromMeta h choice fuel value.metadata value.layout

def Miri.Interpreter.DynamicLayout.alignmentFromMeta {P S C : Type} [Memory.PointerProvenance P] (h : DynamicLayoutHooks P S C) (choice : C) (fuel : Nat) (metadata : MemPlaceMeta P) (layout : ABI.TyAndLayout MIR.TyId) : RvalueM S (Option ABI.Align)

Concrete adapter for ProjectionCx.dynamicAlign. The effectful state is retained in RvalueM; callers should not erase effects to fabricate a pure query.

Equations

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

def Miri.Interpreter.DynamicLayout.memoryResolver {P E K H C : Type} [Memory.PointerProvenance P] (h : DynamicLayoutHooks P (Memory.MemoryState P E K × H) C) (choice : C) (fuel : Nat) (recoverLayout : MemoryOperandPlace P → Except StepError (ABI.TyAndLayout MIR.TyId)) : DynamicLayoutResolver P E K H

Recovering canonical type identity is mandatory because the memory operand view intentionally stores only size/alignment/ABI. Resolver errors preserve the updated memory and hook state; none is the genuine Foreign result.

Equations

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