Canonical stack.rs frame/local/instruction queries. The body index is the identity key; body contents only check consistency. Local layouts consume exact full-instance body-normalization evidence, never template type substitution.

@[reducible, inline]

abbrev Miri.Input.CompilerFrameContext.ActualFrame : Type

Equations

• Miri.Input.CompilerFrameContext.ActualFrame = Miri.Interpreter.Frame Miri.Memory.Provenance Miri.Interpreter.LocalLayout Miri.Interpreter.MachineHooks.FrameExtra

def Miri.Input.CompilerFrameContext.bodyOfFrame (p : CompilerProviders.Prepared) (frame : ActualFrame) : Except String LoweredBody

Resolve by canonical identity and validate the complete instance/body pair. Structural equality is an assertion, not a body-selection algorithm.

Equations

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

def Miri.Input.CompilerFrameContext.currentBody {K User : Type} (p : CompilerProviders.Prepared) : Interpreter.MachineHooks.M K User LoweredBody

Equations

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

def Miri.Input.CompilerFrameContext.normalizedBody (p : CompilerProviders.Prepared) (frame : ActualFrame) : Except String Lean.Json

Equations

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

def Miri.Input.CompilerFrameContext.normalizedLocalType (p : CompilerProviders.Prepared) (frame : ActualFrame) (id : MIR.LocalId) : Except String MIR.TyId

The recorded normalization ran rustc's instantiate-MIR-and-normalize query with this exact full instance and body's typing environment.

Equations

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

def Miri.Input.CompilerFrameContext.normalizeCastTarget {K User : Type} (p : CompilerProviders.Prepared) (requested : MIR.TyId) : Interpreter.MachineHooks.M K User MIR.TyId

Source step.rs Cast target normalization at the exact current statement. The requested original type must be the actual Cast target. No type-ID-only substitution table is shared across distinct full instantiations.

Equations

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

def Miri.Input.CompilerFrameContext.computeLocalLayout {K User : Type} (p : CompilerProviders.Prepared) (id : MIR.LocalId) : Interpreter.MachineHooks.M K User Interpreter.LocalLayout

The uncached compiler leaf used by the canonical local-layout cache.

Equations

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

def Miri.Input.CompilerFrameContext.layoutOfLocal {K User : Type} (p : CompilerProviders.Prepared) (debugAssertions : Bool) (compatible : Interpreter.LocalLayout → Interpreter.LocalLayout → Except Interpreter.StepError Bool) (id : MIR.LocalId) (known : Option Interpreter.LocalLayout) : Interpreter.MachineHooks.M K User Interpreter.LocalLayout

Complete source layout_of_local for the actual current frame: a cached layout bypasses normalization; debug compatibility runs before cache mutation.

Equations

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

def Miri.Input.CompilerFrameContext.localSpan {K User : Type} (p : CompilerProviders.Prepared) (supplied : MIR.Body) (id : MIR.LocalId) : Interpreter.MachineHooks.M K User MIR.SpanRef

The passed body is checked against the current identity, never searched.

Equations

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

def Miri.Input.CompilerFrameContext.instruction {K User : Type} (p : CompilerProviders.Prepared) : Interpreter.MachineHooks.M K User (Option (MIR.Statement ⊕ MIR.Terminator))

Return the actual existing MIR node; no second executable instruction IR.

Equations

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

def Miri.Input.CompilerFrameContext.sourceInfo {K User : Type} (p : CompilerProviders.Prepared) : Interpreter.MachineHooks.M K User (Option MIR.SourceInfo)

Equations

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

def Miri.Input.CompilerFrameContext.currentSpan {K User : Type} (p : CompilerProviders.Prepared) : Interpreter.MachineHooks.M K User MIR.SpanRef

Equations

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

def Miri.Input.CompilerFrameContext.curSpan {K User : Type} (p : CompilerProviders.Prepared) (contextSpan : MIR.SpanRef) : Interpreter.MachineHooks.M K User MIR.SpanRef

Source InterpCx::cur_span retains the actual enclosing compiler span for an empty stack. The caller supplies that source context; no dummy is invented.

Equations

• Miri.Input.CompilerFrameContext.curSpan p contextSpan = do let __do_lift ← get if __do_lift.stack.frames.isEmpty = true then pure contextSpan else Miri.Input.CompilerFrameContext.currentSpan p

structure Miri.Input.CompilerFrameContext.CompilerLeaves (K User C : Type) : Type

Remaining capabilities after source-owned local layout/span queries are removed. These concern typed operations, validation and compiler predicates.

• debugAssertions : Bool
• validationInProgress : Interpreter.MachineHooks.M K User Bool
• projection : C → Interpreter.MachineHooks.M K User (Interpreter.ProjectionCx Memory.Provenance)
• deref : C → Interpreter.RuntimePlace Memory.Provenance → Bool → Interpreter.MachineHooks.M K User (Interpreter.RuntimePlace Memory.Provenance)
• checkPlaceType : C → MIR.Place → Interpreter.RuntimePlace Memory.Provenance → Interpreter.MachineHooks.M K User Unit
• memoryOffset : C → Interpreter.MemPlace Memory.Provenance → ABI.Size → Interpreter.OffsetMode → Interpreter.MemPlaceMeta Memory.Provenance → Interpreter.MachineHooks.M K User (Interpreter.MemPlace Memory.Provenance)
• debugAbiCheck : Interpreter.Immediate Memory.Provenance → Interpreter.LocalLayout → Interpreter.MachineHooks.M K User Unit
• enforceValidity : C → Interpreter.LocalLayout → Interpreter.MachineHooks.M K User Bool
• validate : C → Interpreter.RuntimePlace Memory.Provenance → Interpreter.MachineHooks.M K User Unit
• willValidateMemory : Interpreter.MemoryOperandLayout → Bool

def Miri.Input.CompilerFrameContext.compilerFromLeaves {K User C : Type} (p : CompilerProviders.Prepared) (h : CompilerLeaves K User C) : Interpreter.PlaceMachine.CompilerHooks K User C

Equations

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

def Miri.Input.CompilerFrameContext.compilerHooks {K User C : Type} (p : CompilerProviders.Prepared) (base : Interpreter.PlaceMachine.CompilerHooks K User C) : Interpreter.PlaceMachine.CompilerHooks K User C

Equations

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

def Miri.Input.CompilerFrameContext.rvalueLeaves {C K User : Type} (p : CompilerProviders.Prepared) (threadLocalPointer : C → MIR.DefId → Interpreter.MachineHooks.M K User (Memory.Pointer (Option Memory.Provenance))) : Interpreter.ExecutionLeaves.Rvalue (Interpreter.MachineHooks.State K User) C

Only TLS resolution remains a capability of the rvalue leaf record.

Equations

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

def Miri.Input.CompilerFrameContext.executionHooks {K User C Other Extern Host : Type} (p : CompilerProviders.Prepared) (base : Interpreter.ExecutionMachine.Config K User C Other Extern Host) : Interpreter.ExecutionMachine.Config K User C Other Extern Host

Close canonical frame access and local compiler leaves in the same config. The existing operational dictionaries retain physical/validation capabilities.

Equations

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

theorem Miri.Input.CompilerFrameContext.localSpan_known {K U : Type} (p : CompilerProviders.Prepared) (body : Interpreter.LoadedBody) (actual : LoweredBody) (fnInstance : Interpreter.CallInstance) (decl : LocalDecl) (span : MIR.SpanRef) (row : p.program.bundle.bodies[body.identity.index]? = some actual) (contents : actual.body = body.body) (loader : CallResolution.loadedBodyOfInstance p.lifecycle.calls.calls fnInstance = Except.ok body) (declaration : actual.input.locals[0]? = some decl) (indexed : List.idxOf? decl.sourceInfo.span p.program.bundle.spans.toList = some span.id) (frames : Array ActualFrame) (frame : ActualFrame) (machine : Interpreter.MachineHooks.MachineState K U) (identity : frame.bodyIdentity = body.identity) (function : frame.functionInstance = fnInstance) (frameBody : frame.body = body.body) : localSpan p body.body 0 { stack := { frames := frames.push frame }, machine := machine } = EStateM.Result.ok span { stack := { frames := frames.push frame }, machine := machine }