Pinned interpret/validity.rs::aggregate_field_path_elem (371-452) and visit_variant (1277-1290). Paths are diagnostics only. Field names come from actual compiler definitions; dyn paths require the actual projected child type. Captured-variable numeric names are used only after explicit capture-name query evidence reports no binding name, as in the source fallback.

@[reducible, inline]

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

Equations

• Miri.Input.CompilerPaths.Result = Except String

def Miri.Input.CompilerPaths.variantPath (context : CompilerFacts.Context) (layout : ABI.TyAndLayout TypeId) (index : Nat) : Result Memory.PathElem

Equations

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

def Miri.Input.CompilerPaths.fieldPath (context : CompilerFacts.Context) (layout : ABI.TyAndLayout TypeId) (index : Nat) (childType : TypeId) : Result Memory.PathElem

Equations

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

def Miri.Input.CompilerPaths.validityHooks {P S C E Fn Abi Pad : Type} (prepared : CompilerFactAdapters.Prepared) (machine : Interpreter.ValidityVisitor.Hooks P S C E Fn Abi Pad) : Interpreter.ValidityVisitor.Hooks P S C E Fn Abi Pad

Bind diagnostic paths using the actual projected child type supplied by the visitor, including dynamically unpacked values and Box allocator projections.

Equations

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