Runtime canonical array constructors, including OsStr and argv arrays. Sources: rustc_middle ty/sty.rs::Ty::new_array, rustc_type_ir sty/consts.rs ::from_target_usize, rustc_abi layout.rs::layout_of_array_like (182–207). Runtime IDs are allocations in this explicit interner, never compiler IDs borrowed by equal layout. Keep one World for the lifetime of an interpreter.

inductive Miri.Input.RuntimeArrayTypes.Element : Type

• u8 : Element
• u16 : Element
• compiler (id : TypeId) : Element

def Miri.Input.RuntimeArrayTypes.instDecidableEqElement.decEq (x✝ x✝¹ : Element) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.RuntimeArrayTypes.instDecidableEqElement.decEq Miri.Input.RuntimeArrayTypes.Element.u8 Miri.Input.RuntimeArrayTypes.Element.u8 = isTrue ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqElement.decEq Miri.Input.RuntimeArrayTypes.Element.u8 (Miri.Input.RuntimeArrayTypes.Element.compiler id) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqElement.decEq Miri.Input.RuntimeArrayTypes.Element.u16 Miri.Input.RuntimeArrayTypes.Element.u16 = isTrue ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqElement.decEq Miri.Input.RuntimeArrayTypes.Element.u16 (Miri.Input.RuntimeArrayTypes.Element.compiler id) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqElement.decEq (Miri.Input.RuntimeArrayTypes.Element.compiler id) Miri.Input.RuntimeArrayTypes.Element.u8 = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqElement.decEq (Miri.Input.RuntimeArrayTypes.Element.compiler id) Miri.Input.RuntimeArrayTypes.Element.u16 = isFalse ⋯

@[instance_reducible]

instance Miri.Input.RuntimeArrayTypes.instDecidableEqElement : DecidableEq Element

Equations

• Miri.Input.RuntimeArrayTypes.instDecidableEqElement = Miri.Input.RuntimeArrayTypes.instDecidableEqElement.decEq

@[instance_reducible]

instance Miri.Input.RuntimeArrayTypes.instReprElement : Repr Element

Equations

• Miri.Input.RuntimeArrayTypes.instReprElement = { reprPrec := Miri.Input.RuntimeArrayTypes.instReprElement.repr }

def Miri.Input.RuntimeArrayTypes.instReprElement.repr : Element → Nat → Std.Format

Equations

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

structure Miri.Input.RuntimeArrayTypes.Key : Type

• element : Element
• count : UInt64

def Miri.Input.RuntimeArrayTypes.instDecidableEqKey.decEq (x✝ x✝¹ : Key) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Input.RuntimeArrayTypes.instDecidableEqKey : DecidableEq Key

Equations

• Miri.Input.RuntimeArrayTypes.instDecidableEqKey = Miri.Input.RuntimeArrayTypes.instDecidableEqKey.decEq

def Miri.Input.RuntimeArrayTypes.instReprKey.repr : Key → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Input.RuntimeArrayTypes.instReprKey : Repr Key

Equations

• Miri.Input.RuntimeArrayTypes.instReprKey = { reprPrec := Miri.Input.RuntimeArrayTypes.instReprKey.repr }

inductive Miri.Input.RuntimeArrayTypes.Origin : Type

• compiler (id : TypeId) : Origin
• runtimeConstructor : Origin

@[instance_reducible]

instance Miri.Input.RuntimeArrayTypes.instDecidableEqOrigin : DecidableEq Origin

Equations

• Miri.Input.RuntimeArrayTypes.instDecidableEqOrigin = Miri.Input.RuntimeArrayTypes.instDecidableEqOrigin.decEq

def Miri.Input.RuntimeArrayTypes.instDecidableEqOrigin.decEq (x✝ x✝¹ : Origin) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.RuntimeArrayTypes.instDecidableEqOrigin.decEq (Miri.Input.RuntimeArrayTypes.Origin.compiler id) Miri.Input.RuntimeArrayTypes.Origin.runtimeConstructor = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqOrigin.decEq Miri.Input.RuntimeArrayTypes.Origin.runtimeConstructor (Miri.Input.RuntimeArrayTypes.Origin.compiler id) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqOrigin.decEq Miri.Input.RuntimeArrayTypes.Origin.runtimeConstructor Miri.Input.RuntimeArrayTypes.Origin.runtimeConstructor = isTrue ⋯

@[instance_reducible]

instance Miri.Input.RuntimeArrayTypes.instReprOrigin : Repr Origin

Equations

• Miri.Input.RuntimeArrayTypes.instReprOrigin = { reprPrec := Miri.Input.RuntimeArrayTypes.instReprOrigin.repr }

def Miri.Input.RuntimeArrayTypes.instReprOrigin.repr : Origin → Nat → Std.Format

Equations

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

structure Miri.Input.RuntimeArrayTypes.Entry : Type

• key : Key
• value : ABI.TyAndLayout TypeId
• origin : Origin

structure Miri.Input.RuntimeArrayTypes.World : Type

• metadata : RuntimeMetadata
• byteLayout : ABI.TyAndLayout TypeId
• wideLayout : ABI.TyAndLayout TypeId
• entries : Array Entry
• nextId : TypeId
• obligations : Array String
• aliases : Array (Key × TypeId)

inductive Miri.Input.RuntimeArrayTypes.Error : Type

• metadata (reason : String) : Error
• targetUsizeOverflow (count : UInt64) : Error
• sizeOverflow : Error
• conflictingCanonicalIdentity : Error
• compilerLayoutMismatch (id : TypeId) : Error
• missingRuntimeType (id : TypeId) : Error
• fieldOutOfBounds (index count : Nat) : Error

@[instance_reducible]

instance Miri.Input.RuntimeArrayTypes.instDecidableEqError : DecidableEq Error

Equations

• Miri.Input.RuntimeArrayTypes.instDecidableEqError = Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq

def Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (x✝ x✝¹ : Error) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.metadata reason) (Miri.Input.RuntimeArrayTypes.Error.targetUsizeOverflow count) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.metadata reason) Miri.Input.RuntimeArrayTypes.Error.sizeOverflow = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.metadata reason) Miri.Input.RuntimeArrayTypes.Error.conflictingCanonicalIdentity = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.metadata reason) (Miri.Input.RuntimeArrayTypes.Error.compilerLayoutMismatch id) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.metadata reason) (Miri.Input.RuntimeArrayTypes.Error.missingRuntimeType id) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.metadata reason) (Miri.Input.RuntimeArrayTypes.Error.fieldOutOfBounds index count) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.targetUsizeOverflow count) (Miri.Input.RuntimeArrayTypes.Error.metadata reason) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.targetUsizeOverflow count) Miri.Input.RuntimeArrayTypes.Error.sizeOverflow = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.targetUsizeOverflow count) (Miri.Input.RuntimeArrayTypes.Error.compilerLayoutMismatch id) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.targetUsizeOverflow count) (Miri.Input.RuntimeArrayTypes.Error.missingRuntimeType id) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq Miri.Input.RuntimeArrayTypes.Error.sizeOverflow (Miri.Input.RuntimeArrayTypes.Error.metadata reason) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq Miri.Input.RuntimeArrayTypes.Error.sizeOverflow (Miri.Input.RuntimeArrayTypes.Error.targetUsizeOverflow count) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq Miri.Input.RuntimeArrayTypes.Error.sizeOverflow Miri.Input.RuntimeArrayTypes.Error.sizeOverflow = isTrue ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq Miri.Input.RuntimeArrayTypes.Error.sizeOverflow (Miri.Input.RuntimeArrayTypes.Error.compilerLayoutMismatch id) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq Miri.Input.RuntimeArrayTypes.Error.sizeOverflow (Miri.Input.RuntimeArrayTypes.Error.missingRuntimeType id) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq Miri.Input.RuntimeArrayTypes.Error.sizeOverflow (Miri.Input.RuntimeArrayTypes.Error.fieldOutOfBounds index count) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq Miri.Input.RuntimeArrayTypes.Error.conflictingCanonicalIdentity (Miri.Input.RuntimeArrayTypes.Error.metadata reason) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq Miri.Input.RuntimeArrayTypes.Error.conflictingCanonicalIdentity (Miri.Input.RuntimeArrayTypes.Error.missingRuntimeType id) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.compilerLayoutMismatch id) (Miri.Input.RuntimeArrayTypes.Error.metadata reason) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.compilerLayoutMismatch id) (Miri.Input.RuntimeArrayTypes.Error.targetUsizeOverflow count) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.compilerLayoutMismatch id) Miri.Input.RuntimeArrayTypes.Error.sizeOverflow = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.compilerLayoutMismatch id) (Miri.Input.RuntimeArrayTypes.Error.missingRuntimeType id_1) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.missingRuntimeType id) (Miri.Input.RuntimeArrayTypes.Error.metadata reason) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.missingRuntimeType id) (Miri.Input.RuntimeArrayTypes.Error.targetUsizeOverflow count) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.missingRuntimeType id) Miri.Input.RuntimeArrayTypes.Error.sizeOverflow = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.missingRuntimeType id) Miri.Input.RuntimeArrayTypes.Error.conflictingCanonicalIdentity = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.missingRuntimeType id) (Miri.Input.RuntimeArrayTypes.Error.compilerLayoutMismatch id_1) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.missingRuntimeType id) (Miri.Input.RuntimeArrayTypes.Error.fieldOutOfBounds index count) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.fieldOutOfBounds index count) (Miri.Input.RuntimeArrayTypes.Error.metadata reason) = isFalse ⋯
• Miri.Input.RuntimeArrayTypes.instDecidableEqError.decEq (Miri.Input.RuntimeArrayTypes.Error.fieldOutOfBounds index count) Miri.Input.RuntimeArrayTypes.Error.sizeOverflow = isFalse ⋯

@[instance_reducible]

instance Miri.Input.RuntimeArrayTypes.instReprError : Repr Error

Equations

• Miri.Input.RuntimeArrayTypes.instReprError = { reprPrec := Miri.Input.RuntimeArrayTypes.instReprError.repr }

def Miri.Input.RuntimeArrayTypes.instReprError.repr : Error → Nat → Std.Format

Equations

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

def Miri.Input.RuntimeArrayTypes.calculate (target : ABI.RuntimeTargetDataLayout) (element : ABI.LayoutData) (count : UInt64) : Except Error ABI.LayoutData

Exact source layout calculator, including exclusive object-size bound, first-element niche retention, alignment and wrapping randomization seed.

Equations

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

def Miri.Input.RuntimeArrayTypes.create (runtime : RuntimeMetadata) : Except Error World

Seed exact constructor aliases before computing any layouts. Layout failures in unrelated compiler catalog entries do not turn World creation into execution of those types; requesting their constructors still fails explicitly.

Equations

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

def Miri.Input.RuntimeArrayTypes.intern (world : World) (element : Element) (count : UInt64) : Except Error (ABI.TyAndLayout TypeId × World)

Intern source Ty::new_array(compiler primitive, target-usize value). The updated World is mandatory: dropping it drops the canonical identity map.

Equations

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

def Miri.Input.RuntimeArrayTypes.internElement (world : World) (element : TypeId) (count : UInt64) : Except Error (ABI.TyAndLayout TypeId × World)

General source array constructor for an actual compiler/runtime element ID. No supplied layout establishes identity: lookup uses the canonical element ID.

Equations

• Miri.Input.RuntimeArrayTypes.internElement world element count = Miri.Input.RuntimeArrayTypes.intern world (Miri.Input.RuntimeArrayTypes.elementOfId✝ world element) count

def Miri.Input.RuntimeArrayTypes.osStringArray (world : World) (wide : Bool) (count : UInt64) : Except Error (ABI.TyAndLayout TypeId × World)

Equations

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

def Miri.Input.RuntimeArrayTypes.lookup (world : World) (id : TypeId) : Except Error (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.RuntimeArrayTypes.arrayInfo (world : World) (id : TypeId) : Except Error (Key × ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.RuntimeArrayTypes.fieldLayout (world : World) (id index : Nat) : Except Error (ABI.TyAndLayout TypeId)

Equations

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