One compilation-local provider assembly. Source queries are the pinned step.rs/call.rs/operand.rs/stack.rs/traits.rs query sites documented by the constituent adapters. Preparation is ordered state threading, not independent local ID allocation followed by merging. Every earlier view is rebound to the final tables; source failures remain failures, not execution-readiness claims.

structure Miri.Input.CompilerProviders.Prepared : Type

• program : LoweredProgram
• lowering : Option (LowerContext.Bound self.program.input)

  Prepared lowering indices certified for this provider's exact input. Publicly assembled providers may omit the cache; their accessor preserves the historical behavior by deriving from program.input.

• runtime : RuntimeMetadata
• primitiveQueries : Option (CompilerPrimitiveFacts.Bound self.runtime)

  Direct source primitive references prepared for this exact runtime. Publicly assembled providers may omit it and retain the linear query path.

• sourceEquality : RuntimeMetadata.JsonReflexivity self.runtime.source.raw

  Reflexive-comparison certificate created once by the shared call pipeline and retained for every provider check against this source document.

• lifecycle : CompilerLifecyclePipeline.Prepared
• functions : CompilerFunctionFacts.Prepared
• main : CompilerMain.Prepared
• intrinsics : CompilerIntrinsicFacts.Prepared
• constants : CompilerConstantQueries.Prepared
• constantBinding : CompilerConstantQueries.Binding self.constants self.runtime

  Exact compatibility computed once from the values above. Keeping the indices dependent makes later record updates unable to reuse a stale result.

• namedConstants : CompilerNamedConstants.Prepared
• namedGlobals : CompilerNamedGlobals.Prepared
• externStatics : CompilerExternStatic.Prepared
• pointers : CompilerFunctionPointers.Prepared
• vtables : CompilerVTableMachine.Prepared
• namedAbi : CompilerNamedShimAbi.Prepared
• foreignSymbols : Except String CompilerForeignSymbolTables.Prepared

  Immutable compiler export table. Errors remain stored so source consumers retain their original demand-local failure boundary.

• covarianceIndex : CompilerQueryIndices.Covariance self.program.input.raw

  Source-ordered exact lookup index. Global row parse errors remain stored and are reported only when a non-reflexive covariance query is demanded.

• signatureAbiIndex : CompilerQueryIndices.SignatureAbi self.runtime self.program.input.raw

  Parsed helper-signature keys and exact duplicate rows, retaining the first malformed source row for demand-time error ordering.

• initialArrays : Except String RuntimeArrayTypes.World

  Initial persistent interner. Runtime execution must thread its updated World.

• tls : Except String (Array CompilerThreadLocal.Entry)

def Miri.Input.CompilerProviders.Prepared.loweringContext (p : Prepared) : LowerContext

Reuse lowering indices only when certified for this provider's own source document. This remains correct for manually assembled records whose nested fact context happens to refer to a different program.

Equations

• p.loweringContext = match p.lowering with | some prepared => prepared.value | none => Miri.Input.LowerContext.ofDocument p.program.input

def Miri.Input.CompilerProviders.Prepared.primitiveLayout (p : Prepared) (key : String) : Except String (ABI.TyAndLayout TypeId)

Demand one exact compiler primitive using the provider-owned cache when available; manual providers retain the original query path.

Equations

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

def Miri.Input.CompilerProviders.Prepared.orderingLayout (p : Prepared) : Except String (ABI.TyAndLayout TypeId)

Equations

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

def Miri.Input.CompilerProviders.Prepared.callerLocationType (p : Prepared) : Except String TypeId

Equations

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

def Miri.Input.CompilerProviders.prepareProfiled (profile : Lean.Options) (input : LoweredProgram) : Except String Prepared

All identity-appending adapters run on the immediately preceding program. Predicate tokens are established exactly once by CompilerCallPipeline's shared FactAdapters preparation, then consumed by vtable adapters without re-interning.

Equations

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

def Miri.Input.CompilerProviders.prepare (input : LoweredProgram) : Except String Prepared

Equations

• Miri.Input.CompilerProviders.prepare input = Miri.Input.CompilerProviders.prepareProfiled ∅ input

def Miri.Input.CompilerProviders.predicates (p : Prepared) : Array Lean.Json

The canonical predicate table belonging to all prepared vtable/cast facts.

Equations

• Miri.Input.CompilerProviders.predicates p = p.lifecycle.calls.symbols.facts.dynamicPredicates

def Miri.Input.CompilerProviders.resolveCurrent {K User : Type} (p : Prepared) (definition : MIR.DefId) (args : Array MIR.GenericArg) : Interpreter.MachineHooks.M K User Interpreter.CallInstance

Resolve the exact compiler FnDef request at the current canonical source terminator. Original request identity is distinct from the resolved method/shim identity; trait methods may resolve to an implementation with a different DefId.

Equations

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

def Miri.Input.CompilerProviders.executionHooks {K User Other C Host : Type} (p : Prepared) (image : AllocationImage.Imported) (vtableEngine : Interpreter.VTableMachine.Hooks K User Other) (userRelevantCrates : Array Nat) (base : Interpreter.ExecutionMachine.Config K User C Other ABI.ExternAbi Host) : Interpreter.ExecutionMachine.Config K User C Other ABI.ExternAbi Host

Concrete ExternAbi keeps source ABI/unwind identity separate from FnAbi's canonical target convention. All full-callee hooks use the final shared tables. The explicit base config retains physical memory/host/platform capabilities.

Equations

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