Exact SourceScopeData evidence for Body::caller_location_span (mir/mod.rs). Body indices are explicit source identities; structural Body equality is never used to discover an identity. Legacy absent inline metadata fails closed.

structure Miri.Input.CompilerScopes.Entry : Type

• scope : Interpreter.VirtualCalls.CallerScope
• trackCaller : Option Bool

structure Miri.Input.CompilerScopes.Prepared : Type

• program : LoweredProgram
• scopes : Array (Array (Except String Entry))

def Miri.Input.CompilerScopes.prepare (program : LoweredProgram) : Prepared

Equations

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

def Miri.Input.CompilerScopes.sourceScope (prepared : Prepared) (bodyIndex scopeIndex : Nat) : Except String Interpreter.VirtualCalls.CallerScope

The caller supplies the canonical body index from its frame identity map. No fallback chooses a root, promoted body, or template by structural equality.

Equations

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

def Miri.Input.CompilerScopes.inlineRequiresCallerLocation (prepared : Prepared) (fnInstance : Interpreter.CallInstance) : Except String Bool

Full inlinecallee instances are the keys, including every generic argument.

Equations

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