Pinned shims/unwind.rs: handle_miri_start_unwind, handle_catch_unwind, handle_stack_pop_unwind; machine.rs::after_stack_pop (profiling omitted). Payload tokens are an internal representation of Thread::unwind_payloads: actual typed immediates live in the arena and are removed when popped. They are neither addresses nor allocation identities. Compiler/function-call and memory operations remain required source operations.

structure Miri.Interpreter.Unwind.PayloadStore : Type

• nextToken : Nat
• values : Array (Nat × RvalueImmTy Memory.Provenance)

def Miri.Interpreter.Unwind.PayloadStore.empty : PayloadStore

Exact initial empty payload vector representation.

Equations

• Miri.Interpreter.Unwind.PayloadStore.empty = { nextToken := 0, values := #[] }

structure Miri.Interpreter.Unwind.User (Extra : Type) : Type

• payloads : PayloadStore
• extra : Extra

structure Miri.Interpreter.Unwind.Hooks (K Extra C Other : Type) : Type

• payloads : Extra → PayloadStore
• setPayloads : PayloadStore → Extra → Extra
• readImmediate : C → OpTy Memory.Provenance → MachineHooks.M K Extra (RvalueImmTy Memory.Provenance)
• readPointer : C → OpTy Memory.Provenance → MachineHooks.M K Extra (Memory.Pointer (Option Memory.Provenance))
• forceAllocation : C → RuntimePlace Memory.Provenance → MachineHooks.M K Extra (MPlaceTy Memory.Provenance)
• getPtrFn : C → Memory.Pointer (Option Memory.Provenance) → MachineHooks.M K Extra (FnVal Other)
• callFunction : C → CallInstance → Array (RvalueImmTy Memory.Provenance) → ReturnContinuation → MachineHooks.M K Extra Unit

  Source call_function uses Rust ABI, None destination, and these exact immediates/continuation. Bind to the canonical function-call implementation.

• writeNull : C → MPlaceTy Memory.Provenance → MachineHooks.M K Extra Unit
• writeScalar : C → Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → MachineHooks.M K Extra Unit
• panicUnwinds : Bool

def Miri.Interpreter.Unwind.pushPayload {K Extra C Other : Type} (h : Hooks K Extra C Other) (payload : RvalueImmTy Memory.Provenance) : MachineHooks.M K Extra Unit

Push after reading the complete typed immediate. Source fields in the active thread and the arena are committed together.

Equations

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

def Miri.Interpreter.Unwind.popPayload {K Extra C Other : Type} (h : Hooks K Extra C Other) : MachineHooks.M K Extra (RvalueImmTy Memory.Provenance)

Pop before resolving the catch function, as in the source. Missing or ambiguous arena data is a representation obligation, never a fake payload.

Equations

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

def Miri.Interpreter.Unwind.handleStartUnwind {K Extra C Other : Type} (h : Hooks K Extra C Other) (choice : C) (payload : OpTy Memory.Provenance) : MachineHooks.M K Extra Unit

This operation only stores the payload. Its caller's unwind continuation initiates unwinding; there is no invented jump here.

Equations

• Miri.Interpreter.Unwind.handleStartUnwind h choice payload = do let value ← h.readImmediate choice payload Miri.Interpreter.Unwind.pushPayload h value

def Miri.Interpreter.Unwind.handleCatchUnwind {K Extra C Other : Type} (h : Hooks K Extra C Other) (choice : C) (tryFn data catchFn : OpTy Memory.Provenance) (dest : RuntimePlace Memory.Provenance) (ret : Option MIR.BasicBlockId) : MachineHooks.M K Extra Unit

Source argument order, forced destination before calls, and post-call zero write are retained. The metadata is installed on the frame active after the try call, only for PanicStrategy::Unwind.

Equations

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

def Miri.Interpreter.Unwind.afterStackPop {K Extra C Other : Type} (h : Hooks K Extra C Other) (choice : C) (extra : MachineHooks.FrameExtra) (unwinding : Bool) : MachineHooks.M K Extra ReturnAction

Source after-pop hook. The true return value is written before the payload is popped. A pushed catch frame returns NoJump, preventing the old frame's continuation from being followed by ControlFlow.

Equations

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

def Miri.Interpreter.Unwind.userHooks {K Extra C Other : Type} (base : Hooks K (User Extra) C Other) : Hooks K (User Extra) C Other

The default concrete user-extension lens for payload storage.

Equations

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