Source-shaped stack-frame state and local storage operations from pinned rustc_const_eval/src/interpret/stack.rs. Interpreter callbacks remain explicit for layout queries, machine hooks, allocation, and deallocation.

inductive Miri.Interpreter.FrameLocation : Type

• mir (location : MIR.Location) : FrameLocation
• unwinding (span : MIR.SpanRef) : FrameLocation

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqFrameLocation : DecidableEq FrameLocation

Equations

• Miri.Interpreter.instDecidableEqFrameLocation = Miri.Interpreter.instDecidableEqFrameLocation.decEq

def Miri.Interpreter.instDecidableEqFrameLocation.decEq (x✝ x✝¹ : FrameLocation) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.instDecidableEqFrameLocation.decEq (Miri.Interpreter.FrameLocation.mir a) (Miri.Interpreter.FrameLocation.mir b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqFrameLocation.decEq (Miri.Interpreter.FrameLocation.mir location) (Miri.Interpreter.FrameLocation.unwinding span) = isFalse ⋯
• Miri.Interpreter.instDecidableEqFrameLocation.decEq (Miri.Interpreter.FrameLocation.unwinding span) (Miri.Interpreter.FrameLocation.mir location) = isFalse ⋯
• Miri.Interpreter.instDecidableEqFrameLocation.decEq (Miri.Interpreter.FrameLocation.unwinding a) (Miri.Interpreter.FrameLocation.unwinding b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprFrameLocation : Repr FrameLocation

Equations

• Miri.Interpreter.instReprFrameLocation = { reprPrec := Miri.Interpreter.instReprFrameLocation.repr }

def Miri.Interpreter.instReprFrameLocation.repr : FrameLocation → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev Miri.Interpreter.FrameInstance : Type

Frames and call dispatch share the complete canonical instance identity.

Equations

• Miri.Interpreter.FrameInstance = Miri.Interpreter.CallInstance

inductive Miri.Interpreter.ReturnContinuation : Type

• goto (ret : Option MIR.BasicBlockId) (unwind : MIR.UnwindAction) : ReturnContinuation
• stop (cleanup : Bool) : ReturnContinuation

def Miri.Interpreter.instDecidableEqReturnContinuation.decEq (x✝ x✝¹ : ReturnContinuation) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqReturnContinuation.decEq (Miri.Interpreter.ReturnContinuation.goto ret unwind) (Miri.Interpreter.ReturnContinuation.stop cleanup) = isFalse ⋯
• Miri.Interpreter.instDecidableEqReturnContinuation.decEq (Miri.Interpreter.ReturnContinuation.stop cleanup) (Miri.Interpreter.ReturnContinuation.goto ret unwind) = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqReturnContinuation : DecidableEq ReturnContinuation

Equations

• Miri.Interpreter.instDecidableEqReturnContinuation = Miri.Interpreter.instDecidableEqReturnContinuation.decEq

@[instance_reducible]

instance Miri.Interpreter.instReprReturnContinuation : Repr ReturnContinuation

Equations

• Miri.Interpreter.instReprReturnContinuation = { reprPrec := Miri.Interpreter.instReprReturnContinuation.repr }

def Miri.Interpreter.instReprReturnContinuation.repr : ReturnContinuation → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.ReturnAction : Type

• normal : ReturnAction
• noJump : ReturnAction
• noCleanup : ReturnAction

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqReturnAction : DecidableEq ReturnAction

Equations

• Miri.Interpreter.instDecidableEqReturnAction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.instReprReturnAction.repr : ReturnAction → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprReturnAction : Repr ReturnAction

Equations

• Miri.Interpreter.instReprReturnAction = { reprPrec := Miri.Interpreter.instReprReturnAction.repr }

inductive Miri.Interpreter.StackError : Type

• emptyStack : StackError
• rootFrameCondition (stackWasEmpty continuationIsStop : Bool) : StackError
• invalidLocal (localId : MIR.LocalId) (localCount : Nat) : StackError
• invalidLocation (location : MIR.Location) : StackError
• cannotMakeReturnPlaceDead : StackError
• localExpectedLive (localId : MIR.LocalId) : StackError
• missingLocalType (localId : MIR.LocalId) : StackError
• unsupportedUnexpectedLocalType (localId : MIR.LocalId) (ty : MIR.TyId) : StackError
• unsizedLocalMissingMetadata (localId : MIR.LocalId) : StackError
• metadataForSizedLocal (localId : MIR.LocalId) : StackError
• machineHookFailure (message : String) : StackError
• layoutFailure (message : String) : StackError
• allocationFailure (message : String) : StackError
• deallocationFailure (message : String) : StackError
• localHasNoAllocationProvenance (localId : MIR.LocalId) : StackError

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqStackError : DecidableEq StackError

Equations

• Miri.Interpreter.instDecidableEqStackError = Miri.Interpreter.instDecidableEqStackError.decEq

def Miri.Interpreter.instDecidableEqStackError.decEq (x✝ x✝¹ : StackError) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Interpreter.instReprStackError.repr : StackError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprStackError : Repr StackError

Equations

• Miri.Interpreter.instReprStackError = { reprPrec := Miri.Interpreter.instReprStackError.repr }

@[instance_reducible]

instance Miri.Interpreter.instToStringStackError : ToString StackError

Equations

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

structure Miri.Interpreter.Frame (Prov Layout Extra : Type) : Type

• body : MIR.Body
• bodyIdentity : BodyIdentity
• functionInstance : FrameInstance
• extra : Extra
• returnContinuation : ReturnContinuation
• returnPlace : RuntimeStackPlace Prov
• localsIdentity : LocalsIdentity
• locals : Array (LocalState Prov Layout)
• vaList : Array (MemoryOperandPlace Prov)
• trackCallerArg : Option MIR.SpanRef
• location : FrameLocation

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqFrame {Prov✝ Layout✝ Extra✝ : Type} [DecidableEq Prov✝] [DecidableEq Layout✝] [DecidableEq Extra✝] : DecidableEq (Frame Prov✝ Layout✝ Extra✝)

Equations

• Miri.Interpreter.instDecidableEqFrame = Miri.Interpreter.instDecidableEqFrame.decEq

def Miri.Interpreter.instDecidableEqFrame.decEq {Prov✝ Layout✝ Extra✝ : Type} [DecidableEq Prov✝] [DecidableEq Layout✝] [DecidableEq Extra✝] (x✝ x✝¹ : Frame Prov✝ Layout✝ Extra✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprFrame {Prov✝ Layout✝ Extra✝ : Type} [Repr Prov✝] [Repr Layout✝] [Repr Extra✝] : Repr (Frame Prov✝ Layout✝ Extra✝)

Equations

• Miri.Interpreter.instReprFrame = { reprPrec := Miri.Interpreter.instReprFrame.repr }

def Miri.Interpreter.instReprFrame.repr {Prov✝ Layout✝ Extra✝ : Type} [Repr Prov✝] [Repr Layout✝] [Repr Extra✝] : Frame Prov✝ Layout✝ Extra✝ → Nat → Std.Format

Equations

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

def Miri.Interpreter.Frame.create {Prov Layout Extra : Type} (loadedBody : LoadedBody) (functionInstance : FrameInstance) (extra : Extra) (returnContinuation : ReturnContinuation) (returnPlace : RuntimeStackPlace Prov) (initialSpan : MIR.SpanRef) (localsIdentity : LocalsIdentity) : Frame Prov Layout Extra

The source push_stack_frame_raw initialization: one dead, uncached local state for each MIR local declaration. The other frame fields are required inputs; no body, return place, instance, or machine extra is invented here.

Equations

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

def Miri.Interpreter.Frame.currentLoc {Prov Layout Extra : Type} (self : Frame Prov Layout Extra) : FrameLocation

Equations

• self.currentLoc = self.location

def Miri.Interpreter.Frame.getLocal {Prov Layout Extra : Type} (self : Frame Prov Layout Extra) (localId : MIR.LocalId) : Except StackError (LocalState Prov Layout)

Equations

• self.getLocal localId = if h : localId < self.locals.size then pure self.locals[localId] else throw (Miri.Interpreter.StackError.invalidLocal localId self.locals.size)

def Miri.Interpreter.Frame.getLocalOperand {Prov Layout Extra : Type} (self : Frame Prov Layout Extra) (localId : MIR.LocalId) : Except StackError (Operand Prov)

Equations

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

def Miri.Interpreter.Frame.replaceLocalValue {Prov Layout Extra : Type} (self : Frame Prov Layout Extra) (localId : MIR.LocalId) (value : LocalValue Prov) : Except StackError (Frame Prov Layout Extra)

Replace only the LocalValue, preserving rustc's memoized layout.

Equations

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

def Miri.Interpreter.Frame.setLocalOperand {Prov Layout Extra : Type} (self : Frame Prov Layout Extra) (localId : MIR.LocalId) (value : Operand Prov) : Except StackError (Frame Prov Layout Extra)

access_mut-style update: dead locals fail, and the cached layout is retained exactly. Callers performing actual writes must run their hooks first.

Equations

• self.setLocalOperand localId value = do let _ ← self.getLocalOperand localId self.replaceLocalValue localId (Miri.Interpreter.LocalValue.live value)

def Miri.Interpreter.Frame.getLocalLayout {Prov Layout Extra : Type} (self : Frame Prov Layout Extra) (localId : MIR.LocalId) : Except StackError (Option Layout)

Equations

• self.getLocalLayout localId = do let __do_lift ← self.getLocal localId pure __do_lift.layout

def Miri.Interpreter.Frame.getOrCacheLocalLayout {Prov Layout Extra : Type} (self : Frame Prov Layout Extra) (localId : MIR.LocalId) (computed : Layout) : Except StackError (Frame Prov Layout Extra × Layout)

Cache the source-computed layout only if no layout was already memoized. The returned layout is the cached one when present, matching layout_of_local.

Equations

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

def Miri.Interpreter.Frame.setLocation {Prov Layout Extra : Type} (self : Frame Prov Layout Extra) (location : FrameLocation) : Except StackError (Frame Prov Layout Extra)

Equations

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

structure Miri.Interpreter.Stack (Prov Layout Extra : Type) : Type

• frames : Array (Frame Prov Layout Extra)

def Miri.Interpreter.instDecidableEqStack.decEq {Prov✝ Layout✝ Extra✝ : Type} [DecidableEq Prov✝] [DecidableEq Layout✝] [DecidableEq Extra✝] (x✝ x✝¹ : Stack Prov✝ Layout✝ Extra✝) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.instDecidableEqStack.decEq { frames := a } { frames := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqStack {Prov✝ Layout✝ Extra✝ : Type} [DecidableEq Prov✝] [DecidableEq Layout✝] [DecidableEq Extra✝] : DecidableEq (Stack Prov✝ Layout✝ Extra✝)

Equations

• Miri.Interpreter.instDecidableEqStack = Miri.Interpreter.instDecidableEqStack.decEq

def Miri.Interpreter.instReprStack.repr {Prov✝ Layout✝ Extra✝ : Type} [Repr Prov✝] [Repr Layout✝] [Repr Extra✝] : Stack Prov✝ Layout✝ Extra✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprStack {Prov✝ Layout✝ Extra✝ : Type} [Repr Prov✝] [Repr Layout✝] [Repr Extra✝] : Repr (Stack Prov✝ Layout✝ Extra✝)

Equations

• Miri.Interpreter.instReprStack = { reprPrec := Miri.Interpreter.instReprStack.repr }

def Miri.Interpreter.Stack.empty {Prov Layout Extra : Type} : Stack Prov Layout Extra

Equations

• Miri.Interpreter.Stack.empty = { frames := #[] }

def Miri.Interpreter.Stack.currentFrame? {Prov Layout Extra : Type} (self : Stack Prov Layout Extra) : Option (Frame Prov Layout Extra)

Equations

• self.currentFrame? = self.frames.back?

def Miri.Interpreter.Stack.frameIndex {Prov Layout Extra : Type} (self : Stack Prov Layout Extra) : Except StackError Nat

Equations

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

def Miri.Interpreter.Stack.pushFrame {Prov Layout Extra : Type} (self : Stack Prov Layout Extra) (frame : Frame Prov Layout Extra) : Except StackError (Stack Prov Layout Extra)

Equations

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

def Miri.Interpreter.Stack.popFrame {Prov Layout Extra : Type} (self : Stack Prov Layout Extra) : Except StackError (Stack Prov Layout Extra × Frame Prov Layout Extra)

Equations

• self.popFrame = match self.frames.back? with | none => throw Miri.Interpreter.StackError.emptyStack | some frame => pure ({ frames := self.frames.pop }, frame)

def Miri.Interpreter.Stack.updateCurrentLocation {Prov Layout Extra : Type} (self : Stack Prov Layout Extra) (location : FrameLocation) : Except StackError (Stack Prov Layout Extra)

Equations

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

def Miri.Interpreter.Stack.getLocal {Prov Layout Extra : Type} (self : Stack Prov Layout Extra) (localId : MIR.LocalId) : Except StackError (LocalState Prov Layout)

Equations

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

def Miri.Interpreter.Stack.getLocalOperand {Prov Layout Extra : Type} (self : Stack Prov Layout Extra) (localId : MIR.LocalId) : Except StackError (Operand Prov)

Equations

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

structure Miri.Interpreter.StackEffect (State α : Type) : Type

Stateful callback result: effects before an error are never rolled back.

• state : State
• outcome : Except StackError α

structure Miri.Interpreter.LocalStorageHooks (Prov Layout Extra State : Type) : Type

Required compiler and machine operations. veryTriviallySized must implement source's recursive type-kind classifier; layout includes normalization and from_known_layout. Allocation/deallocation use stack memory kind.

• veryTriviallySized : MIR.TyId → Except StackError Bool
• layout : State → Frame Prov Layout Extra → MIR.LocalId → StackEffect State Layout
• isSized : Layout → Bool
• afterLocalWrite : State → MIR.LocalId → Bool → StackEffect State Unit
• allocateDyn : State → Layout → MemPlaceMeta Prov → StackEffect State (MemPlace Prov)
• deallocateStack : State → Memory.Pointer (Option Prov) → StackEffect State Unit

structure Miri.Interpreter.LocalStorageResult (Prov Layout Extra State : Type) : Type

• frame : Frame Prov Layout Extra
• state : State
• outcome : Except StackError Unit

def Miri.Interpreter.Frame.deallocateLocal {Prov Layout Extra State : Type} (hooks : LocalStorageHooks Prov Layout Extra State) (state : State) (value : LocalValue Prov) : StackEffect State Unit

Source deallocate_local: only indirect live locals own an allocation. The required deallocator validates provenance and allocation identity.

Equations

• Miri.Interpreter.Frame.deallocateLocal hooks state (Miri.Interpreter.LocalValue.live (Miri.Interpreter.Operand.indirect place)) = hooks.deallocateStack state place.ptr
• Miri.Interpreter.Frame.deallocateLocal hooks state value = { state := state, outcome := Except.ok () }

def Miri.Interpreter.Frame.storageDead {Prov Layout Extra State : Type} (self : Frame Prov Layout Extra) (state : State) (hooks : LocalStorageHooks Prov Layout Extra State) (localId : MIR.LocalId) : LocalStorageResult Prov Layout Extra State

Source storage_dead replaces the value before attempting deallocation.

Equations

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

def Miri.Interpreter.Frame.storageLiveDyn {Prov Layout Extra State : Type} (self : Frame Prov Layout Extra) (state : State) (hooks : LocalStorageHooks Prov Layout Extra State) (localId : MIR.LocalId) (metadata : MemPlaceMeta Prov) : LocalStorageResult Prov Layout Extra State

Source storage_live_dyn, including lazy layout caching, allocation or write hook before replacement, and replacement before old-value deallocation.

Equations

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

def Miri.Interpreter.Frame.storageLive {Prov Layout Extra State : Type} (self : Frame Prov Layout Extra) (state : State) (hooks : LocalStorageHooks Prov Layout Extra State) (localId : MIR.LocalId) : LocalStorageResult Prov Layout Extra State

Equations

• self.storageLive state hooks localId = self.storageLiveDyn state hooks localId Miri.Interpreter.MemPlaceMeta.none

structure Miri.Interpreter.StackRunResult (Prov Layout Extra State α : Type) : Type

Whole-stack effects keep mutations made by a machine hook even on failure.

• stack : Stack Prov Layout Extra
• state : State
• outcome : Except StackError α

structure Miri.Interpreter.StackLifecycleHooks (Prov Layout Extra State : Type) : Type

Compiler-dependent and machine-dependent stages required by the source frame lifecycle. Required constants and always-live analysis are explicit obligations because MIR.Body does not store their compiler query results.

• storage : LocalStorageHooks Prov Layout Extra State
• freshLocalsIdentity : State → State × LocalsIdentity

  Total ghost instrumentation at locals-buffer creation, not a source machine callback.

• initFrame : State → Frame Prov Layout Unit → StackEffect State (Frame Prov Layout Extra)
• requiredConstants : Stack Prov Layout Extra → State → StackRunResult Prov Layout Extra State Unit
• afterPush : Stack Prov Layout Extra → State → StackRunResult Prov Layout Extra State Unit
• beforePop : Stack Prov Layout Extra → State → StackRunResult Prov Layout Extra State Unit
• afterPop : Stack Prov Layout Extra → State → Frame Prov Layout Extra → Bool → StackRunResult Prov Layout Extra State ReturnAction
• alwaysLiveVarsAndTemps : MIR.Body → Except StackError (Array MIR.LocalId)
• deallocateVararg : State → MemoryOperandPlace Prov → StackEffect State Unit

def Miri.Interpreter.Stack.pushStackFrameRaw {Prov Layout Extra State : Type} (self : Stack Prov Layout Extra) (state : State) (hooks : StackLifecycleHooks Prov Layout Extra State) (body : LoadedBody) (functionInstance : FrameInstance) (returnContinuation : ReturnContinuation) (returnPlace : RuntimeStackPlace Prov) (initialSpan : MIR.SpanRef) : StackRunResult Prov Layout Extra State Unit

Source push_stack_frame_raw: init precedes insertion, while required constant checks and after-push run with the new frame already on the stack.

Equations

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

def Miri.Interpreter.Stack.popStackFrameRaw {Prov Layout Extra State : Type} (self : Stack Prov Layout Extra) (state : State) (hooks : StackLifecycleHooks Prov Layout Extra State) : StackRunResult Prov Layout Extra State (Frame Prov Layout Extra)

Source pop_stack_frame_raw: before-pop effects precede removal.

Equations

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

def Miri.Interpreter.Stack.cleanupStackFrame {Prov Layout Extra State : Type} (self : Stack Prov Layout Extra) (state : State) (hooks : StackLifecycleHooks Prov Layout Extra State) (unwinding : Bool) (frame : Frame Prov Layout Extra) : StackRunResult Prov Layout Extra State ReturnAction

Source cleanup_stack_frame: locals, then varargs, then machine after-pop. Stop-without-cleanup skips both deallocation and the machine hook.

Equations

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

def Miri.Interpreter.Stack.pushStackFrameDone {Prov Layout Extra State : Type} (self : Stack Prov Layout Extra) (state : State) (hooks : StackLifecycleHooks Prov Layout Extra State) : StackRunResult Prov Layout Extra State Unit

Source push_stack_frame_done: make return storage and always-live vars live in source order, preserving each successful update on later failure.

Equations

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