Actual compiler call construction; no complete operational CallHooks record is accepted and discarded. Every query key uses the canonical compilation.

def Miri.Input.CompilerCallConstruction.compiler {K U C : Type} (p : CompilerProviders.Prepared) (budget : Nat) : Interpreter.ExecutionCallLeaves.Compiler (Interpreter.MachineHooks.State K U) C ABI.ExternAbi

Canonical full compiler dictionary, including target-feature policy.

Equations

• Miri.Input.CompilerCallConstruction.compiler p budget = Miri.Input.CompilerExecutionCallLeaves.make p budget

def Miri.Input.CompilerCallConstruction.dispatch {K U Other C : Type} (p : CompilerProviders.Prepared) (foreign : Option (Interpreter.MachineHooks.M K U (Interpreter.ForeignItems.Hooks Memory.Provenance (Interpreter.MachineHooks.State K U) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance))) (backend : Interpreter.CallDispatchMachine.Backend (Interpreter.MachineHooks.State K U)) (dynSymName : Other → String) : Interpreter.CallDispatchMachine.Hooks (Interpreter.MachineHooks.State K U) C Other

Foreign emulation and real backend hooks are actual source interpreters; MIR loading is the same exact LoadedBody provider used by helper/root calls.

Equations

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

def Miri.Input.CompilerCallConstruction.leaves {K U Other C : Type} (p : CompilerProviders.Prepared) (compatibilityBudget : Nat) (foreign : Option (Interpreter.MachineHooks.M K U (Interpreter.ForeignItems.Hooks Memory.Provenance (Interpreter.MachineHooks.State K U) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance))) (backend : Interpreter.CallDispatchMachine.Backend (Interpreter.MachineHooks.State K U)) (dynSymName : Other → String) (llvm : Interpreter.CallInstance → Interpreter.MachineHooks.M K U (Interpreter.IntrinsicArchitecture.DispatchHooks Memory.Provenance (Interpreter.MachineHooks.State K U) C (Interpreter.RuntimePlace Memory.Provenance))) : Interpreter.ExecutionCallLeaves.Hooks (Interpreter.MachineHooks.State K U) C Other ABI.ExternAbi

Equations

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

def Miri.Input.CompilerCallConstruction.virtual {K U C : Type} (p : CompilerProviders.Prepared) (vtable : Interpreter.VTableHooks Memory.Provenance (Interpreter.MachineHooks.State K U) C Interpreter.CallInstance (ABI.FnAbi MIR.TyId)) (alignment : Interpreter.PointerPlaceMachine.AlignmentContext U) : Interpreter.ExecutionCallLeaves.Virtual K U C

Shared canonical vtable queries plus the exact compiler virtual leaves; receiver reads, projections and pointer construction are not caller callbacks.

Equations

• Miri.Input.CompilerCallConstruction.virtual p vtable alignment = { compiler := Miri.Input.CompilerVirtualLeaves.make p.lifecycle.calls, vtable := vtable, alignment := alignment }

def Miri.Input.CompilerCallConstruction.lifecycle {K U C Other : Type} (p : CompilerProviders.Prepared) (userRelevantCrates : Array Nat) (storage : Interpreter.MachineHooks.StorageHooks K U) (identity : Interpreter.ExecutionCallLeaves.IdentityAccess U) (unwind : Interpreter.Unwind.Hooks K U C Other) : Interpreter.CallMachine.Lifecycle K U C

Source frame metadata, preamble/checks and after-pop unwind processing. Storage is the actual shared machine allocation context; no raw-push or post-initialization success callback is accepted.

Equations

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

def Miri.Input.CompilerCallConstruction.threadIdentity {U : Type} : Interpreter.ExecutionCallLeaves.IdentityAccess (Interpreter.ThreadStacks.Storage U)

Exact existing shared ThreadStacks supply, without a second counter.

Equations

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

def Miri.Input.CompilerCallConstruction.helpers {C K U : Type} (p : CompilerProviders.Prepared) (dummySpan : MIR.SpanRef) (fnAbiOfSignature : C → Interpreter.FunctionCalls.SignatureRequest ABI.ExternAbi → Interpreter.MachineHooks.M K U (ABI.FnAbi MIR.TyId)) : Except String (Interpreter.ExecutionCallLeaves.Helpers (Interpreter.MachineHooks.State K U) C ABI.ExternAbi)

Actual source helper metadata plus the genuine dummy-signature compiler query. Stack/origin operations are built by ExecutionCalls.helpers.

Equations

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