Internal compiler-metadata bridge, not the public import API. Successful conversion supplies records and queries; it does not establish execution readiness, machine-hook adequacy, or Rust UB freedom. Original source nodes remain available beside every canonical layout result.

inductive Miri.Input.RuntimeMetadataError : Type

• missing (path : String) : RuntimeMetadataError
• unsupported (path : String) : RuntimeMetadataError
• invalid (path message : String) : RuntimeMetadataError
• duplicateType (id : TypeId) : RuntimeMetadataError
• unknownType (id : TypeId) : RuntimeMetadataError

def Miri.Input.instDecidableEqRuntimeMetadataError.decEq (x✝ x✝¹ : RuntimeMetadataError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.missing a) (Miri.Input.RuntimeMetadataError.missing b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.missing path) (Miri.Input.RuntimeMetadataError.unsupported path_1) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.missing path) (Miri.Input.RuntimeMetadataError.invalid path_1 message) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.missing path) (Miri.Input.RuntimeMetadataError.duplicateType id) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.missing path) (Miri.Input.RuntimeMetadataError.unknownType id) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.unsupported path) (Miri.Input.RuntimeMetadataError.missing path_1) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.unsupported path) (Miri.Input.RuntimeMetadataError.invalid path_1 message) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.unsupported path) (Miri.Input.RuntimeMetadataError.duplicateType id) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.unsupported path) (Miri.Input.RuntimeMetadataError.unknownType id) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.invalid path message) (Miri.Input.RuntimeMetadataError.missing path_1) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.invalid path message) (Miri.Input.RuntimeMetadataError.unsupported path_1) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.invalid path message) (Miri.Input.RuntimeMetadataError.duplicateType id) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.invalid path message) (Miri.Input.RuntimeMetadataError.unknownType id) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.duplicateType id) (Miri.Input.RuntimeMetadataError.missing path) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.duplicateType id) (Miri.Input.RuntimeMetadataError.unsupported path) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.duplicateType id) (Miri.Input.RuntimeMetadataError.invalid path message) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.duplicateType id) (Miri.Input.RuntimeMetadataError.unknownType id_1) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.unknownType id) (Miri.Input.RuntimeMetadataError.missing path) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.unknownType id) (Miri.Input.RuntimeMetadataError.unsupported path) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.unknownType id) (Miri.Input.RuntimeMetadataError.invalid path message) = isFalse ⋯
• Miri.Input.instDecidableEqRuntimeMetadataError.decEq (Miri.Input.RuntimeMetadataError.unknownType id) (Miri.Input.RuntimeMetadataError.duplicateType id_1) = isFalse ⋯

@[instance_reducible]

instance Miri.Input.instDecidableEqRuntimeMetadataError : DecidableEq RuntimeMetadataError

Equations

• Miri.Input.instDecidableEqRuntimeMetadataError = Miri.Input.instDecidableEqRuntimeMetadataError.decEq

def Miri.Input.instReprRuntimeMetadataError.repr : RuntimeMetadataError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Input.instReprRuntimeMetadataError : Repr RuntimeMetadataError

Equations

• Miri.Input.instReprRuntimeMetadataError = { reprPrec := Miri.Input.instReprRuntimeMetadataError.repr }

@[instance_reducible]

instance Miri.Input.instToStringRuntimeMetadataError : ToString RuntimeMetadataError

Equations

• Miri.Input.instToStringRuntimeMetadataError = { toString := fun (e : Miri.Input.RuntimeMetadataError) => reprStr e }

structure Miri.Input.RuntimeMetadata.JsonReflexivity (left : Lean.Json) : Type

A private, checked certificate that one immutable JSON tree compares equal to itself. JSON's BEq is not assumed lawful: a malformed tree may fail this test, in which case comparisons must retain their ordinary recursive path.

• reflexive : Option (PLift ((left == left) = true))

def Miri.Input.RuntimeMetadata.JsonReflexivity.prepare {left : Lean.Json} : JsonReflexivity left

Equations

• Miri.Input.RuntimeMetadata.JsonReflexivity.prepare = { reflexive := if h : (left == left) = true then some { down := h } else none }

def Miri.Input.RuntimeMetadata.JsonReflexivity.matchesRight {left : Lean.Json} (certificate : JsonReflexivity left) (candidate : Lean.Json) : Bool

Compare in the source-left orientation, preserving left == candidate.

Equations

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

def Miri.Input.RuntimeMetadata.JsonReflexivity.matchesLeft {left : Lean.Json} (certificate : JsonReflexivity left) (candidate : Lean.Json) : Bool

Compare in the candidate-left orientation, preserving candidate == left.

Equations

• certificate.matchesLeft candidate = match certificate.reflexive with | none => candidate == left | some { down := reflexive } => withPtrEq candidate left (fun (x : Unit) => candidate == left) ⋯

def Miri.Input.RuntimeMetadata.JsonReflexivity.matchesRightOr {left : Lean.Json} (certificate : Option (JsonReflexivity left)) (candidate : Lean.Json) : Bool

Optional-cache entry point for callers that keep their historical API.

Equations

• Miri.Input.RuntimeMetadata.JsonReflexivity.matchesRightOr none candidate = (left == candidate)
• Miri.Input.RuntimeMetadata.JsonReflexivity.matchesRightOr (some certificate_2) candidate = certificate_2.matchesRight candidate

theorem Miri.Input.RuntimeMetadata.JsonReflexivity.matchesRight_eq {left : Lean.Json} (certificate : JsonReflexivity left) (candidate : Lean.Json) : certificate.matchesRight candidate = (left == candidate)

theorem Miri.Input.RuntimeMetadata.JsonReflexivity.matchesLeft_eq {left : Lean.Json} (certificate : JsonReflexivity left) (candidate : Lean.Json) : certificate.matchesLeft candidate = (candidate == left)

theorem Miri.Input.RuntimeMetadata.JsonReflexivity.matchesRightOr_eq {left : Lean.Json} (certificate : Option (JsonReflexivity left)) (candidate : Lean.Json) : matchesRightOr certificate candidate = (left == candidate)

@[reducible, inline]

abbrev Miri.Input.RuntimeMetadata.Result (α : Type u_1) : Type u_1

Equations

• Miri.Input.RuntimeMetadata.Result = Except Miri.Input.RuntimeMetadataError

def Miri.Input.RuntimeMetadata.require {A : Type u_1} (value : Option A) (path : String) : Result A

Equations

• Miri.Input.RuntimeMetadata.require (some value_2) path = pure value_2
• Miri.Input.RuntimeMetadata.require none path = throw (Miri.Input.RuntimeMetadataError.missing path)

def Miri.Input.RuntimeMetadata.jsonField (j : Lean.Json) (name : String) : Result Lean.Json

Equations

• Miri.Input.RuntimeMetadata.jsonField j name = Miri.Input.RuntimeMetadata.convert✝ name (j.getObjVal? name)

def Miri.Input.RuntimeMetadata.number (j : Lean.Json) (name : String) : Result Nat

Equations

• Miri.Input.RuntimeMetadata.number j name = do let __do_lift ← Miri.Input.RuntimeMetadata.jsonField j name Miri.Input.RuntimeMetadata.convert✝ name __do_lift.getNat?

def Miri.Input.RuntimeMetadata.u128Number (j : Lean.Json) (name : String) : Result Nat

Full-width rustc u128 JSON endpoints, with backward numeric encoding.

Equations

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

def Miri.Input.RuntimeMetadata.truth (j : Lean.Json) (name : String) : Result Bool

Equations

• Miri.Input.RuntimeMetadata.truth j name = do let __do_lift ← Miri.Input.RuntimeMetadata.jsonField j name Miri.Input.RuntimeMetadata.convert✝ name __do_lift.getBool?

def Miri.Input.RuntimeMetadata.text (j : Lean.Json) (name : String) : Result String

Equations

• Miri.Input.RuntimeMetadata.text j name = do let __do_lift ← Miri.Input.RuntimeMetadata.jsonField j name Miri.Input.RuntimeMetadata.convert✝ name __do_lift.getStr?

def Miri.Input.RuntimeMetadata.array (j : Lean.Json) (name : String) : Result (Array Lean.Json)

Equations

• Miri.Input.RuntimeMetadata.array j name = do let __do_lift ← Miri.Input.RuntimeMetadata.jsonField j name Miri.Input.RuntimeMetadata.convert✝ name __do_lift.getArr?

def Miri.Input.RuntimeMetadata.u64 (n : Nat) (path : String) : Result UInt64

Equations

• Miri.Input.RuntimeMetadata.u64 n path = if n < 2 ^ 64 then pure (UInt64.ofNat n) else throw (Miri.Input.RuntimeMetadataError.invalid path "u64 overflow")

def Miri.Input.RuntimeMetadata.u32 (n : Nat) (path : String) : Result UInt32

Equations

• Miri.Input.RuntimeMetadata.u32 n path = if n < 2 ^ 32 then pure (UInt32.ofNat n) else throw (Miri.Input.RuntimeMetadataError.invalid path "u32 overflow")

def Miri.Input.RuntimeMetadata.u128 (n : Nat) (path : String) : Result ABI.U128

Equations

• Miri.Input.RuntimeMetadata.u128 n path = if n < 2 ^ 128 then pure (BitVec.ofNat 128 n) else throw (Miri.Input.RuntimeMetadataError.invalid path "u128 overflow")

def Miri.Input.RuntimeMetadata.size (n : Nat) : Result ABI.Size

Equations

• Miri.Input.RuntimeMetadata.size n = Miri.ABI.Size.ofBytes <$> Miri.Input.RuntimeMetadata.u64 n "size"

def Miri.Input.RuntimeMetadata.alignment (n : Nat) : Result ABI.Align

Equations

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

def Miri.Input.RuntimeMetadata.integer : MIR.IntegerKind → Result ABI.Integer

Equations

• Miri.Input.RuntimeMetadata.integer Miri.MIR.IntegerKind.i8 = pure Miri.ABI.Integer.I8
• Miri.Input.RuntimeMetadata.integer Miri.MIR.IntegerKind.u8 = pure Miri.ABI.Integer.I8
• Miri.Input.RuntimeMetadata.integer Miri.MIR.IntegerKind.i16 = pure Miri.ABI.Integer.I16
• Miri.Input.RuntimeMetadata.integer Miri.MIR.IntegerKind.u16 = pure Miri.ABI.Integer.I16
• Miri.Input.RuntimeMetadata.integer Miri.MIR.IntegerKind.i32 = pure Miri.ABI.Integer.I32
• Miri.Input.RuntimeMetadata.integer Miri.MIR.IntegerKind.u32 = pure Miri.ABI.Integer.I32
• Miri.Input.RuntimeMetadata.integer Miri.MIR.IntegerKind.i64 = pure Miri.ABI.Integer.I64
• Miri.Input.RuntimeMetadata.integer Miri.MIR.IntegerKind.u64 = pure Miri.ABI.Integer.I64
• Miri.Input.RuntimeMetadata.integer Miri.MIR.IntegerKind.i128 = pure Miri.ABI.Integer.I128
• Miri.Input.RuntimeMetadata.integer Miri.MIR.IntegerKind.u128 = pure Miri.ABI.Integer.I128
• Miri.Input.RuntimeMetadata.integer Miri.MIR.IntegerKind.isize = throw (Miri.Input.RuntimeMetadataError.unsupported "pointer-sized integer primitive tag")
• Miri.Input.RuntimeMetadata.integer Miri.MIR.IntegerKind.usize = throw (Miri.Input.RuntimeMetadataError.unsupported "pointer-sized integer primitive tag")

def Miri.Input.RuntimeMetadata.float : FloatTypeTag → Result ABI.Float

Equations

• Miri.Input.RuntimeMetadata.float Miri.Input.FloatTypeTag.f16 = pure Miri.ABI.Float.F16
• Miri.Input.RuntimeMetadata.float Miri.Input.FloatTypeTag.f16b = pure Miri.ABI.Float.F16B
• Miri.Input.RuntimeMetadata.float Miri.Input.FloatTypeTag.f32 = pure Miri.ABI.Float.F32
• Miri.Input.RuntimeMetadata.float Miri.Input.FloatTypeTag.f64 = pure Miri.ABI.Float.F64
• Miri.Input.RuntimeMetadata.float Miri.Input.FloatTypeTag.f128 = pure Miri.ABI.Float.F128
• Miri.Input.RuntimeMetadata.float Miri.Input.FloatTypeTag.ppcf128 = pure Miri.ABI.Float.PpcF128
• Miri.Input.RuntimeMetadata.float (Miri.Input.FloatTypeTag.unknown value) = throw (Miri.Input.RuntimeMetadataError.unsupported "float tag")

def Miri.Input.RuntimeMetadata.primitive (target : ABI.RuntimeTargetDataLayout) (source : PrimitiveLayout) : Result ABI.Primitive

Equations

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

def Miri.Input.RuntimeMetadata.scalar (target : ABI.RuntimeTargetDataLayout) (source : ScalarLayout) : Result ABI.Scalar

Equations

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

def Miri.Input.RuntimeMetadata.backend (target : ABI.RuntimeTargetDataLayout) (source : BackendRepr) : Result ABI.BackendRepr

Equations

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

def Miri.Input.RuntimeMetadata.fields (source : FieldShape) : Result ABI.FieldsShape

Equations

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

def Miri.Input.RuntimeMetadata.niche (target : ABI.RuntimeTargetDataLayout) (j : Lean.Json) : Result (Option ABI.Niche)

Equations

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

def Miri.Input.RuntimeMetadata.encoding (source : TagEncoding) : Result ABI.TagEncoding

Equations

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

def Miri.Input.RuntimeMetadata.variants (target : ABI.RuntimeTargetDataLayout) (source : VariantsLayout) : Result ABI.Variants

Equations

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

def Miri.Input.RuntimeMetadata.layout (target : ABI.RuntimeTargetDataLayout) (source : Layout) : Result ABI.LayoutData

Equations

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

def Miri.Input.RuntimeMetadata.importTarget (j : Lean.Json) : Result ABI.RuntimeTargetDataLayout

Every canonical target field is required. LLVM's original layout string and address-space bounds stay in the enclosing source document as evidence.

Equations

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

structure Miri.Input.RuntimeNodeLookupCache (nodes : Array TypeNode) : Type

A prepared type-node table is tied to the exact source array it summarizes, and its table must equal the canonical first-row-wins map for that array.

• entries : Std.HashMap TypeId TypeNode
• exact : self.entries = Miri.Input.canonicalNodeLookup✝ nodes

def Miri.Input.RuntimeNodeLookupCache.build (nodes : Array TypeNode) : RuntimeNodeLookupCache nodes

Build a first-row-wins index, matching Array.find? on nodes.

Equations

• Miri.Input.RuntimeNodeLookupCache.build nodes = { entries := Miri.Input.canonicalNodeLookup✝ nodes, exact := ⋯ }

structure Miri.Input.RuntimeLayoutLookupCache (layouts : Array (TypeId × Except RuntimeMetadataError (ABI.TyAndLayout TypeId))) : Type

A prepared layout table indexed by the exact layout array it summarizes. Its entries equal the canonical first-row-wins map, retaining first-row errors.

• entries : Std.HashMap TypeId (Except RuntimeMetadataError (ABI.TyAndLayout TypeId))
• exact : self.entries = Miri.Input.canonicalLayoutLookup✝ layouts

def Miri.Input.RuntimeLayoutLookupCache.build (layouts : Array (TypeId × Except RuntimeMetadataError (ABI.TyAndLayout TypeId))) : RuntimeLayoutLookupCache layouts

Build a first-row-wins index, matching Array.find? on layouts.

Equations

• Miri.Input.RuntimeLayoutLookupCache.build layouts = { entries := Miri.Input.canonicalLayoutLookup✝ layouts, exact := ⋯ }

structure Miri.Input.RuntimeMetadata : Type

Internal metadata cache. A failed type-layout conversion remains a stored obligation; successful import never marks the document execution-ready.

• source : ImportDocumentCore
• target : ABI.RuntimeTargetDataLayout
• layouts : Array (TypeId × Except RuntimeMetadataError (ABI.TyAndLayout TypeId))
• nodeCache : Option (RuntimeNodeLookupCache self.source.types)
• layoutCache : Option (RuntimeLayoutLookupCache self.layouts)

structure Miri.Input.RuntimeMetadata.Indexedextends Miri.Input.RuntimeMetadata : Type

Preparation-only immutable lookup view. The public base record remains an array-backed value, so existing direct construction and record updates retain their old semantics. The index is constructed from one fixed metadata value; its first-entry policy matches the base .find? lookups for manually built records that contain duplicate keys.

• source : ImportDocumentCore
• target : ABI.RuntimeTargetDataLayout
• layouts : Array (TypeId × Except RuntimeMetadataError (ABI.TyAndLayout TypeId))
• nodeCache : Option (RuntimeNodeLookupCache self.source.types)
• layoutCache : Option (RuntimeLayoutLookupCache self.layouts)
• nodeIndex : Std.HashMap TypeId TypeNode
• layoutIndex : Std.HashMap TypeId (Except RuntimeMetadataError (ABI.TyAndLayout TypeId))
• rawReflexivity : JsonReflexivity self.source.raw

  A checked fast-path certificate for reflexive source-document equality. JSON equality is not assumed lawful: malformed trees may fail even raw == raw. When absent, consumers must run the original full comparator.

def Miri.Input.RuntimeMetadata.Indexed.ofMetadata (metadata : RuntimeMetadata) (sourceEquality : Option (JsonReflexivity metadata.source.raw) := none) : Indexed

Build exact-key tables for repeated source/compiler fact lookups. Duplicate keys in manually constructed records preserve the first source-order entry.

Equations

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

def Miri.Input.RuntimeMetadata.Indexed.matchesSourceLeft (metadata : Indexed) (left : Lean.Json) : Bool

Compare a candidate document using the exact original JSON equality. The checked self-equality certificate permits Lean's safe withPtrEq fast path when the indexed metadata object is reused by the source world.

Equations

• metadata.matchesSourceLeft left = metadata.rawReflexivity.matchesLeft left

theorem Miri.Input.RuntimeMetadata.Indexed.matchesSourceLeft_eq (metadata : Indexed) (left : Lean.Json) : metadata.matchesSourceLeft left = (left == metadata.source.raw)

@[instance_reducible]

instance Miri.Input.RuntimeMetadata.instCoeIndexed : Coe Indexed RuntimeMetadata

Equations

• Miri.Input.RuntimeMetadata.instCoeIndexed = { coe := Miri.Input.RuntimeMetadata.Indexed.toRuntimeMetadata }

def Miri.Input.RuntimeMetadata.ofDocument (document : ImportDocumentCore) : Result RuntimeMetadata

Equations

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

def Miri.Input.RuntimeMetadata.node (metadata : RuntimeMetadata) (id : TypeId) : Result TypeNode

Equations

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

def Miri.Input.RuntimeMetadata.lookup (metadata : RuntimeMetadata) (id : TypeId) : Result (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.RuntimeMetadata.Indexed.node (metadata : Indexed) (id : TypeId) : Result TypeNode

Equations

• metadata.node id = Miri.Input.RuntimeMetadata.require metadata.nodeIndex[id]? (toString "type " ++ toString id)

def Miri.Input.RuntimeMetadata.Indexed.lookup (metadata : Indexed) (id : TypeId) : Result (ABI.TyAndLayout TypeId)

Equations

• metadata.lookup id = do let entry ← Miri.Input.RuntimeMetadata.require metadata.layoutIndex[id]? (toString "layout " ++ toString id) entry

def Miri.Input.RuntimeMetadata.obligations (metadata : RuntimeMetadata) : Array (TypeId × RuntimeMetadataError)

This is an explicit diagnostic inventory, not an execution-readiness test.

Equations

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

def Miri.Input.RuntimeMetadata.findKind (metadata : RuntimeMetadata) (kind : TypeShapeKind) : Result (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.RuntimeMetadata.integerLayout (metadata : RuntimeMetadata) (kind : MIR.IntegerKind) : Result (ABI.TyAndLayout TypeId)

Canonical primitive lookup compares the compiler integer tag, rather than choosing an arbitrary member of the broad int/uint shape category.

Equations

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

def Miri.Input.RuntimeMetadata.tupleLayout (metadata : RuntimeMetadata) (elements : Array TypeId) : Result (ABI.TyAndLayout TypeId)

Source Ty::new_tup identity from the exact ordered compiler element IDs. No size, display spelling, or first-match heuristic establishes a tuple type.

Equations

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

def Miri.Input.RuntimeMetadata.overflowTupleLayout (metadata : RuntimeMetadata) (element : ABI.TyAndLayout TypeId) : Result (ABI.TyAndLayout TypeId)

Equations

• metadata.overflowTupleLayout element = do let boolean ← metadata.findKind Miri.Input.TypeShapeKind.bool metadata.tupleLayout #[element.ty, boolean.ty]

def Miri.Input.RuntimeMetadata.field (metadata : RuntimeMetadata) (parent : ABI.TyAndLayout TypeId) (index : Nat) : Result (ABI.TyAndLayout TypeId)

Source type relationships are read from typed compiler payloads, never from display/debug strings. ADT field selection uses the selected variant.

Equations

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

def Miri.Input.RuntimeMetadata.forVariant (metadata : RuntimeMetadata) (parent : ABI.TyAndLayout TypeId) (index : Nat) : Result (ABI.TyAndLayout TypeId)

Reconstructs precisely LayoutData::for_variant in pinned rustc_abi/layout/simple.rs:158–185. Missing uninhabited-variant compiler queries remain obligations instead of fabricated field metadata.

Equations

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

def Miri.Input.RuntimeMetadata.pointee (metadata : RuntimeMetadata) (parent : ABI.TyAndLayout TypeId) : Result (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.RuntimeMetadata.queries (metadata : RuntimeMetadata) : ABI.LayoutQueries TypeId

Boundary adapter preserves missing compiler metadata as explicit failures.

Equations

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