Internal reuse of actual rustc instance-resolution and FnAbi query results. Complete instance arguments and shared definition/type-constant tables are kept. Missing/ambiguous/conflicting queries remain errors. This is not a compiler instance solver or Miri's foreign-function/shim dispatcher.

@[reducible, inline]

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

Equations

• Miri.Input.CallResolution.Result = Except String

def Miri.Input.CallResolution.convention (source : CanonicalAbi) : Result ABI.CanonAbi

Equations

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

def Miri.Input.CallResolution.functionAbi (runtime : RuntimeMetadata) (source : FunctionAbi) : Result (ABI.FnAbi TypeId)

Equations

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

structure Miri.Input.CallResolution.FunctionAbiCache (runtime : RuntimeMetadata) : Type

Immutable conversion memo tied to the exact runtime value and its exact shared-graph inputs. Its sole constructor proves the entries equal a fresh build, so callers cannot install fabricated ABI results.

• entries : Std.HashMap Lean.Json (Except String (Miri.ABI.FnAbi Miri.Input.TypeId))
• exact : entries self = buildFunctionAbiCache runtime

def Miri.Input.CallResolution.prepareFunctionAbiCacheProfiled (profile : Lean.Options) (runtime : RuntimeMetadata) : FunctionAbiCache runtime

Prepare the memo for all shared-graph FnAbi candidates in this runtime.

Equations

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

def Miri.Input.CallResolution.prepareFunctionAbiCache (runtime : RuntimeMetadata) : FunctionAbiCache runtime

Prepare the memo for all shared-graph FnAbi candidates in this runtime.

Equations

• Miri.Input.CallResolution.prepareFunctionAbiCache runtime = Miri.Input.CallResolution.prepareFunctionAbiCacheProfiled ∅ runtime

def Miri.Input.CallResolution.functionAbiJson (runtime : RuntimeMetadata) (raw : Lean.Json) (cache : Option (FunctionAbiCache runtime) := none) : Result (ABI.FnAbi TypeId)

Decode and convert a raw compiler FnAbi through the checked shared cache. Without a cache, retain the direct decoder/converter path for manually constructed runtime contexts.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.CallResolution.functionAbiJson runtime raw = do let __do_lift ← Miri.Input.CallResolution.decodeFunctionAbiJson✝ raw Miri.Input.CallResolution.functionAbi runtime __do_lift

structure Miri.Input.CallResolution.Site : Type

• bodyIndex : Nat
• block : MIR.BasicBlockId

@[instance_reducible]

instance Miri.Input.CallResolution.instDecidableEqSite : DecidableEq Site

Equations

• Miri.Input.CallResolution.instDecidableEqSite = Miri.Input.CallResolution.instDecidableEqSite.decEq

def Miri.Input.CallResolution.instDecidableEqSite.decEq (x✝ x✝¹ : Site) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Input.CallResolution.instReprSite : Repr Site

Equations

• Miri.Input.CallResolution.instReprSite = { reprPrec := Miri.Input.CallResolution.instReprSite.repr }

def Miri.Input.CallResolution.instReprSite.repr : Site → Nat → Std.Format

Equations

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

structure Miri.Input.CallResolution.Resolution : Type

• callee : Interpreter.CallInstance
• sourceInstanceId : InstanceId
• function : MIR.Operand
• abi : Except String (ABI.FnAbi TypeId)
• source : Lean.Json

structure Miri.Input.CallResolution.Entry : Type

• site : Site
• outcome : Except String Resolution

structure Miri.Input.CallResolution.InstanceBody : Type

• fnInstance : Interpreter.CallInstance
• sourceInstanceId : InstanceId
• bodyIndex : Nat

structure Miri.Input.CallResolution.Indirect : Type

• site : Site
• function : MIR.Operand
• functionType : MIR.TyId
• abi : ABI.FnAbi TypeId
• source : Lean.Json

structure Miri.Input.CallResolution.Prepared : Type

• program : LoweredProgram
• runtime : RuntimeMetadata
• functionAbiCache : FunctionAbiCache self.runtime
• unitLayoutCache : Option (CallCompatibility.UnitLayoutCache self.runtime)

  Strict source unit-layout scan cached as a deferred outcome for ABI compatibility calls. Manual records retain the linear compatibility path.

• sourceEquality : RuntimeMetadata.JsonReflexivity self.runtime.source.raw
• entries : Array Entry
• bodies : Array InstanceBody
• obligations : Array Obligation
• indirect : Array Indirect

def Miri.Input.CallResolution.prepareWithRuntimeProfiled (profile : Lean.Options) (runtime : RuntimeMetadata) (program : LoweredProgram) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw) := none) : Result Prepared

Prepare call-resolution tables using the already validated immutable runtime metadata for this program's unchanged ImportDocument. Compiler tables may grow during preparation, but CompilerGlobals.prepareProgram changes only the lowered bundle and leaves that document untouched.

Equations

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

def Miri.Input.CallResolution.prepareWithRuntime (runtime : RuntimeMetadata) (program : LoweredProgram) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw) := none) : Result Prepared

Prepare call-resolution tables using validated runtime metadata.

Equations

• Miri.Input.CallResolution.prepareWithRuntime runtime program sourceEquality = Miri.Input.CallResolution.prepareWithRuntimeProfiled ∅ runtime program sourceEquality

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

Standalone compatibility path: validate RuntimeMetadata before resolving instances or call-site queries, preserving the historical error order.

Equations

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

def Miri.Input.CallResolution.atSite (prepared : Prepared) (site : Site) : Result Resolution

Equations

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

def Miri.Input.CallResolution.resolveAt (prepared : Prepared) (site : Site) (function : MIR.Operand) : Result Interpreter.CallInstance

Function operand identity is checked in addition to body and block. Source sites are compiler-table indices, never diagnostic span matches.

Equations

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

def Miri.Input.CallResolution.abiOfInstance (prepared : Prepared) (fnInstance : Interpreter.CallInstance) (extraArgs : Array TypeId) : Result (ABI.FnAbi TypeId)

Equations

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

def Miri.Input.CallResolution.loadedBodyOfInstance (prepared : Prepared) (fnInstance : Interpreter.CallInstance) : Result Interpreter.LoadedBody

A loaded body carries the exact source table key. Equal MIR syntax does not make distinct root/template/promoted/instance body identities interchangeable.

Equations

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

def Miri.Input.CallResolution.bodyOfInstance (prepared : Prepared) (fnInstance : Interpreter.CallInstance) : Result MIR.Body

Compatibility syntax-only view of the exact loaded body. It retains the same unique-key and instantiation checks; equal bodies are not merged.

Equations

• Miri.Input.CallResolution.bodyOfInstance prepared fnInstance = do let __do_lift ← Miri.Input.CallResolution.loadedBodyOfInstance prepared fnInstance pure __do_lift.body

def Miri.Input.CallResolution.bindAbi {S P C E Other Extern : Type} (prepared : Prepared) (compatibility : CallCompatibility.Evidence S) (budget : Nat) (base : Interpreter.CallHooks P S C E Other Extern (ABI.FnAbi TypeId) (ABI.ArgAbi TypeId)) : Interpreter.CallHooks P S C E Other Extern (ABI.FnAbi TypeId) (ABI.ArgAbi TypeId)

Replace only ABI leaves with complete compiler records and source layout compatibility. Machine dispatch, target features, caller locations, pointer resolution and actual body interception remain required in the supplied hooks.

Equations

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