One final compilation-local identity table for actual frame lifecycle, full-instance ABI and backtrace source queries. Appending span/definition IDs never invalidates already prepared runtime dictionaries.

structure Miri.Input.CompilerLifecyclePipeline.Prepared : Type

• calls : CompilerCallPipeline.Prepared
• instances : CompilerInstanceAbi.Prepared
• lifecycle : CompilerLifecycle.Prepared
• backtrace : CompilerBacktraceSource.Prepared
• frames : CompilerFrameMetadata.Prepared
• shim : CompilerShimAbi.Prepared

def Miri.Input.CompilerLifecyclePipeline.prepareProfiled (profile : Lean.Options) (calls : CompilerCallPipeline.Prepared) : Except String Prepared

Equations

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

def Miri.Input.CompilerLifecyclePipeline.prepare (calls : CompilerCallPipeline.Prepared) : Except String Prepared

Equations

• Miri.Input.CompilerLifecyclePipeline.prepare calls = Miri.Input.CompilerLifecyclePipeline.prepareProfiled ∅ calls

theorem Miri.Input.CompilerLifecyclePipeline.prepareProfiled_eq_prepare (profile : Lean.Options) (calls : CompilerCallPipeline.Prepared) : prepareProfiled profile calls = prepare calls

Profiling wrappers preserve the lifecycle preparation result exactly.

def Miri.Input.CompilerLifecyclePipeline.lifecycleHooks {K User C : Type} (p : Prepared) (userRelevantCrates : Array Nat) (base : Interpreter.CallMachine.Lifecycle K User C) : Interpreter.CallMachine.Lifecycle K User C

Close all frame compiler leaves with actual exported query results. The remaining fields concern machine memory, ghost identity allocation and unwind.

Equations

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

def Miri.Input.CompilerLifecyclePipeline.backtraceHooks {S P Extra K D MD B I E : Type} (p : Prepared) (image : AllocationImage.Imported) (memory : S → Memory.MemoryState P Extra K) (base : Interpreter.Backtrace.Hooks P S D MD B I E CompilerBacktraceSource.Position) : Interpreter.Backtrace.Hooks P S D MD B I E CompilerBacktraceSource.Position

Source query closure composes with BacktraceMachine's actual memory binding. Actual function allocation/address/provenance lookup remains the machine's job.

Equations

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

def Miri.Input.CompilerLifecyclePipeline.functionHooks {K User C Other Extern : Type} (p : Prepared) (base : Interpreter.FunctionCalls.Hooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.MachineHooks.FrameExtra Other Extern (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)) : Interpreter.FunctionCalls.Hooks Memory.Provenance (Interpreter.MachineHooks.State K User) C Interpreter.MachineHooks.FrameExtra Other Extern (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)

Root/direct/virtual/drop calls share exact full-instance/extra-argument ABI queries and exact LoadedBody identities from this same final table.

Equations

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