Pinned interpret/call.rs:74–385: trivial ABI, transparent/NPO unfolding, C structural equality and argument compatibility. Compiler type queries are required fallible operations; no unknown predicate becomes false or true. A depth budget makes recursive compiler queries executable and reports resource exhaustion explicitly. The budget is not a bound on Rust execution semantics.

inductive Miri.Interpreter.LayoutCompat.AdtKind : Type

• Struct : AdtKind
• Union : AdtKind
• Enum : AdtKind

@[instance_reducible]

instance Miri.Interpreter.LayoutCompat.instDecidableEqAdtKind : DecidableEq AdtKind

Equations

• Miri.Interpreter.LayoutCompat.instDecidableEqAdtKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.LayoutCompat.instReprAdtKind.repr : AdtKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.LayoutCompat.instReprAdtKind : Repr AdtKind

Equations

• Miri.Interpreter.LayoutCompat.instReprAdtKind = { reprPrec := Miri.Interpreter.LayoutCompat.instReprAdtKind.repr }

structure Miri.Interpreter.LayoutCompat.Field (Ty : Type) : Type

• name : String
• ty : Ty

def Miri.Interpreter.LayoutCompat.instReprField.repr {Ty✝ : Type} [Repr Ty✝] : Field Ty✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.LayoutCompat.instReprField {Ty✝ : Type} [Repr Ty✝] : Repr (Field Ty✝)

Equations

• Miri.Interpreter.LayoutCompat.instReprField = { reprPrec := Miri.Interpreter.LayoutCompat.instReprField.repr }

structure Miri.Interpreter.LayoutCompat.AdtInfo (Ty : Type) : Type

• kind : AdtKind
• transparent : Bool
• reprC : Bool
• reprRust : Bool
• variants : Array (Array (Field Ty))

  Field types are instantiated with the queried type's complete arguments; normalization is requested separately at the source sites that require it.

inductive Miri.Interpreter.LayoutCompat.TypeKind (Ty : Type) : Type

• tuple {Ty : Type} : TypeKind Ty
• never {Ty : Type} : TypeKind Ty
• functionDefinition {Ty : Type} : TypeKind Ty
• closure {Ty : Type} : TypeKind Ty
• coroutine {Ty : Type} : TypeKind Ty
• coroutineClosure {Ty : Type} : TypeKind Ty
• array {Ty : Type} (element : Ty) : TypeKind Ty
• adt {Ty : Type} : TypeKind Ty
• pattern {Ty : Type} (base : Ty) : TypeKind Ty
• unsafeBinder {Ty : Type} : TypeKind Ty
• alias {Ty : Type} : TypeKind Ty
• reference {Ty : Type} (pointee : Ty) : TypeKind Ty
• rawPointer {Ty : Type} (pointee : Ty) : TypeKind Ty
• functionPointer {Ty : Type} : TypeKind Ty
• integer {Ty : Type} (kind : MIR.IntegerKind) : TypeKind Ty
• char {Ty : Type} : TypeKind Ty
• other {Ty : Type} : TypeKind Ty

def Miri.Interpreter.LayoutCompat.instReprTypeKind.repr {Ty✝ : Type} [Repr Ty✝] : TypeKind Ty✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.LayoutCompat.instReprTypeKind {Ty✝ : Type} [Repr Ty✝] : Repr (TypeKind Ty✝)

Equations

• Miri.Interpreter.LayoutCompat.instReprTypeKind = { reprPrec := Miri.Interpreter.LayoutCompat.instReprTypeKind.repr }

@[reducible, inline]

abbrev Miri.Interpreter.LayoutCompat.M (S A : Type) : Type

Equations

• Miri.Interpreter.LayoutCompat.M S A = EStateM Miri.Interpreter.StepError S A

structure Miri.Interpreter.LayoutCompat.Queries (Ty S : Type) : Type

• target : ABI.RuntimeTargetDataLayout
• kind : Ty → M S (TypeKind Ty)
• adt : Ty → M S (AdtInfo Ty)
• field : ABI.TyAndLayout Ty → Nat → M S (ABI.TyAndLayout Ty)
• layoutOf : Ty → M S (ABI.TyAndLayout Ty)
• unitLayout : M S (ABI.TyAndLayout Ty)
• eraseUnsafeBinder : Ty → M S Ty
• normalize : Ty → M S Ty
• reprEqualUpToSeed : Ty → Ty → M S Bool
• itemName : Ty → M S String
• nonnullOptimizationGuaranteed : Ty → M S Bool
• isGlobalBox : Ty → M S Bool
• boxedType : Ty → M S Ty
• pointerMetadataType : Ty → M S Ty

  ptr_metadata_ty must normalize projected unsized-tail types, exactly as the source closure does, rather than comparing only top-level pointees.

def Miri.Interpreter.LayoutCompat.hasTrivialAbi {Ty S : Type} (q : Queries Ty S) : Nat → ABI.TyAndLayout Ty → M S Bool

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.LayoutCompat.hasTrivialAbi q 0 x✝ = Miri.Interpreter.LayoutCompat.exhausted✝

inductive Miri.Interpreter.LayoutCompat.UnfoldPolicy : Type

The three source may_unfold closures, represented without a second IR.

• All : UnfoldPolicy
• Structs : UnfoldPolicy
• StructsUntilNpo : UnfoldPolicy

@[instance_reducible]

instance Miri.Interpreter.LayoutCompat.instDecidableEqUnfoldPolicy : DecidableEq UnfoldPolicy

Equations

• Miri.Interpreter.LayoutCompat.instDecidableEqUnfoldPolicy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.LayoutCompat.instReprUnfoldPolicy.repr : UnfoldPolicy → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.LayoutCompat.instReprUnfoldPolicy : Repr UnfoldPolicy

Equations

• Miri.Interpreter.LayoutCompat.instReprUnfoldPolicy = { reprPrec := Miri.Interpreter.LayoutCompat.instReprUnfoldPolicy.repr }

def Miri.Interpreter.LayoutCompat.unfoldTransparent {Ty S : Type} (q : Queries Ty S) (policy : UnfoldPolicy) : Nat → ABI.TyAndLayout Ty → M S (ABI.TyAndLayout Ty)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.LayoutCompat.unfoldTransparent q policy 0 x✝ = Miri.Interpreter.LayoutCompat.exhausted✝

def Miri.Interpreter.LayoutCompat.unfoldNpo {Ty S : Type} (q : Queries Ty S) (fuel : Nat) (layout : ABI.TyAndLayout Ty) : M S (ABI.TyAndLayout Ty)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.LayoutCompat.unfoldNpo q 0 layout = Miri.Interpreter.LayoutCompat.exhausted✝

def Miri.Interpreter.LayoutCompat.identicalCTypes {Ty S : Type} [DecidableEq Ty] (q : Queries Ty S) : Nat → Ty → Ty → M S Bool

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.LayoutCompat.identicalCTypes q 0 x✝¹ x✝ = Miri.Interpreter.LayoutCompat.exhausted✝

def Miri.Interpreter.LayoutCompat.layoutCompat {Ty S : Type} [DecidableEq Ty] (q : Queries Ty S) (fuel : Nat) (caller callee : ABI.TyAndLayout Ty) : M S Bool

Equations

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

def Miri.Interpreter.LayoutCompat.checkArgumentCompat {Ty S : Type} [DecidableEq Ty] (q : Queries Ty S) (fuel : Nat) (caller callee : ABI.ArgAbi Ty) : M S Bool

Equations

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