Shared preparation and actual compiler-leaf wiring for virtual/drop/caller calls. All adapters retain one final compilation-local identity table; none selects a body, type or instance by name or structural resemblance.

@[reducible, inline]

abbrev Miri.Input.CompilerCallPipeline.Result (α : Type u_1) : Type u_1

Equations

• Miri.Input.CompilerCallPipeline.Result = Except String

structure Miri.Input.CompilerCallPipeline.Prepared : Type

• scopes : CompilerScopes.Prepared
• runtime : CompilerRuntimeQueries.Prepared
• symbols : CompilerVTableRuntime.Prepared
• calls : CallResolution.Prepared
• sourceEquality : RuntimeMetadata.JsonReflexivity self.calls.runtime.source.raw

def Miri.Input.CompilerCallPipeline.prepareProfiled (profile : Lean.Options) (program : LoweredProgram) : Result Prepared

Each stage appends identities without moving existing indices. Rebind all views to the final table so full shim instances, inline spans, const arguments and executable body identities remain compilation-local and consistent.

Equations

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

def Miri.Input.CompilerCallPipeline.prepare (program : LoweredProgram) : Result Prepared

Equations

• Miri.Input.CompilerCallPipeline.prepare program = Miri.Input.CompilerCallPipeline.prepareProfiled ∅ program

def Miri.Input.CompilerCallPipeline.compilerHooks {S C : Type} (prepared : Prepared) (base : Interpreter.VirtualCalls.CompilerHooks S C) : Interpreter.VirtualCalls.CompilerHooks S C

Equations

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

def Miri.Input.CompilerCallPipeline.vtableHooks {S P E K C : Type} (prepared : Prepared) (image : AllocationImage.Imported) (memory : S → Memory.MemoryState P E K) (base : Interpreter.VTableHooks P S C Interpreter.CallInstance (ABI.FnAbi MIR.TyId)) : Interpreter.VTableHooks P S C Interpreter.CallInstance (ABI.FnAbi MIR.TyId)

Equations

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

def Miri.Input.CompilerCallPipeline.runtimeHooks {S P Extra K C E : Type} (prepared : Prepared) (image : AllocationImage.Imported) (memory : S → Memory.MemoryState P Extra K) (base : Interpreter.VirtualCalls.Hooks P S C E) : Interpreter.VirtualCalls.Hooks P S C E

Runtime reads/projections/pointer alignment remain actual machine actions. Every replaced compiler/symbolic leaf uses the exact imported query evidence.

Equations

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

def Miri.Input.CompilerCallPipeline.loadMir {S : Type} (prepared : Prepared) (fnInstance : Interpreter.CallInstance) : EStateM Interpreter.StepError S Interpreter.LoadedBody

Source load_mir returns the exact body-table key with executable MIR. Missing or ambiguous instance bodies, failed substitutions and templates are errors.

Equations

• Miri.Input.CompilerCallPipeline.loadMir prepared fnInstance = Miri.Input.CompilerCallPipeline.lift✝ (Miri.Input.CallResolution.loadedBodyOfInstance prepared.calls fnInstance)

def Miri.Input.CompilerCallPipeline.bindFunctionCalls {P S C E Other Extern FnABI ArgABI : Type} (prepared : Prepared) (base : Interpreter.FunctionCalls.Hooks P S C E Other Extern FnABI ArgABI) : Interpreter.FunctionCalls.Hooks P S C E Other Extern FnABI ArgABI

Equations

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