Pinned helpers.rs::call_function and call_thread_root_function. This driver uses the canonical Call.initStackFrame rather than treating a successful call as an opaque foreign effect. The compiler's construction of a dummy-binder function-pointer signature and its ABI query remain explicit query operations.

structure Miri.Interpreter.FunctionCalls.SignatureRequest (Extern : Type) : Type

mk_fn_sig receives these exact input/output types, Safe safety, the given ABI, and the source defaults (not C variadic or splatted). This is a compiler query request, not another executable program representation.

• inputs : Array MIR.TyId
• output : MIR.TyId
• abi : Extern
• safety : MIR.Safety
• cVariadic : Bool
• splatted : Bool

structure Miri.Interpreter.FunctionCalls.Hooks (P S C E Other Extern FnABI ArgABI : Type) : Type 1

• call : CallHooks P S C E Other Extern FnABI ArgABI
• loadMir : C → CallInstance → CallM S LoadedBody

  load_mir(f.def, None), before constructing destination/signature.

• unitLayout : LocalLayout
• fnAbiOfSignature : C → SignatureRequest Extern → CallM S FnABI

  Actual mk_fn_sig + Binder::dummy + fn_abi_of_fn_ptr(..., empty). No existential type/ABI chosen by the proof user is permitted here.

• callerLocationType : CallM S MIR.TyId
• activeStackEmpty : CallM S Bool
• originIsDummy : CallM S Bool

  Compare the actual active thread's origin Span to DUMMY_SP.

• setOrigin : MIR.SpanRef → CallM S Unit

def Miri.Interpreter.FunctionCalls.fakeAllocZst {P : Type} (layout : LocalLayout) : Except StepError (MPlaceTy P)

Source place.rs::fake_alloc_zst. No allocation, borrow/race event, or fresh provenance is introduced. Its absolute address is the ABI alignment in bytes.

Equations

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

def Miri.Interpreter.FunctionCalls.callFunction {P S C E Other Extern FnABI ArgABI : Type} (h : Hooks P S C E Other Extern FnABI ArgABI) (choice : C) (fnInstance : CallInstance) (callerAbi : Extern) (args : Array (RvalueImmTy P)) (destination : Option (MPlaceTy P)) (continuation : ReturnContinuation) : CallM S Unit

Internal helper calls pass immediate copies; track_caller changes the caller signature, not the explicit argument array. initStackFrame supplies the caller-location argument according to the canonical source call pipeline.

Equations

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

def Miri.Interpreter.FunctionCalls.callThreadRootFunction {P S C E Other Extern FnABI ArgABI : Type} (h : Hooks P S C E Other Extern FnABI ArgABI) (choice : C) (fnInstance : CallInstance) (callerAbi : Extern) (args : Array (RvalueImmTy P)) (destination : Option (MPlaceTy P)) (span : MIR.SpanRef) : CallM S Unit

Source assertions are interpreter representation errors, not Rust UB. Origin is assigned before any load_mir/compiler query, and retained if it fails.

Equations

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

def Miri.Interpreter.FunctionCalls.bindUnwind {K User C Other Extern FnABI ArgABI : Type} (base : Unwind.Hooks K User C Other) (h : Hooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra Other Extern FnABI ArgABI) : Unwind.Hooks K User C Other

Install the internal Rust call helper in the panic/unwind driver while retaining all actual memory/function-pointer and payload operations.

Equations

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