Source fast paths in rustc_middle/ty/util.rs::is_trivially_freeze and is_trivially_unpin (1191–1267). A true structural fast path justifies Freeze, Unpin and UnsafeUnpin; false does not justify a negative trait result. Nontrivial runtime arrays still require genuine compiler trait resolution evidence.

def Miri.Input.RuntimeArrayFacts.boolean (context : CompilerFacts.Context) (world : RuntimeArrayTypes.World) (ty : MIR.TyId) (key : String) : Except String Bool

Equations

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

def Miri.Input.RuntimeArrayFacts.opsemInhabited (context : CompilerFacts.Context) (world : RuntimeArrayTypes.World) (ty : MIR.TyId) : Nat → Except String Bool

rustc_middle/ty/inhabitedness/mod.rs:312–314: an array is opsem inhabited exactly when its evaluated length is zero or its element is inhabited. Compiler-owned elements retain their actual normalized query result.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.RuntimeArrayFacts.opsemInhabited context world ty 0 = throw "runtime array inhabitedness query budget exhausted"

def Miri.Input.RuntimeArrayFacts.retagHooks {K U : Type} (access : RuntimeArrayQueries.Access (Interpreter.MachineHooks.State K U)) (context : CompilerFacts.Context) (base : Interpreter.TypedRetag.Hooks K U) : Interpreter.TypedRetag.Hooks K U

Equations

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