Preparation-time lookup indices for exact covariance and generated-call ABI queries. The indices retain source row order and the first malformed global row; consumers still decide query-specific matches and error precedence.

structure Miri.Input.CompilerQueryIndices.CovarianceData : Type

• headerError : Option String
• firstRowError : Option (Nat × String)
• rows : Std.HashMap String (Array (Nat × Lean.Json))

structure Miri.Input.CompilerQueryIndices.Covariance (raw : Lean.Json) : Type

• data : CovarianceData
• exact : self.data = Miri.Input.CompilerQueryIndices.buildCovariance✝ raw

def Miri.Input.CompilerQueryIndices.covariance (raw : Lean.Json) : Covariance raw

Equations

• Miri.Input.CompilerQueryIndices.covariance raw = { data := Miri.Input.CompilerQueryIndices.buildCovariance✝ raw, exact := ⋯ }

structure Miri.Input.CompilerQueryIndices.SignatureAbiRow : Type

A helper-signature row's raw query value and its demand-time ABI result. The Excepts retain malformed/unsupported row outcomes without making an unused query fail during index construction.

• index : Nat
• record : Lean.Json
• abiQuery : Except String Lean.Json
• parsedAbi : Except String (ABI.FnAbi MIR.TyId)

structure Miri.Input.CompilerQueryIndices.SignatureAbiData : Type

• headerError : Option String
• firstRowError : Option (Nat × String)
• rows : Std.HashMap String (Array SignatureAbiRow)

structure Miri.Input.CompilerQueryIndices.SignatureAbi (runtime : RuntimeMetadata) (raw : Lean.Json) : Type

• abiCache : Option (CallResolution.FunctionAbiCache runtime)
• data : SignatureAbiData
• exact : self.data = Miri.Input.CompilerQueryIndices.buildSignatureAbi✝ runtime self.abiCache raw

def Miri.Input.CompilerQueryIndices.signatureAbi (runtime : RuntimeMetadata) (raw : Lean.Json) (abiCache : Option (CallResolution.FunctionAbiCache runtime) := none) : SignatureAbi runtime raw

Equations

• Miri.Input.CompilerQueryIndices.signatureAbi runtime raw abiCache = { abiCache := abiCache, data := Miri.Input.CompilerQueryIndices.buildSignatureAbi✝ runtime abiCache raw, exact := ⋯ }

def Miri.Input.CompilerQueryIndices.covarianceRows {raw : Lean.Json} (index : Covariance raw) (source target : Nat) : Array (Nat × Lean.Json)

Equations

• Miri.Input.CompilerQueryIndices.covarianceRows index source target = index.data.rows.getD (Miri.Input.CompilerQueryIndices.covarianceKey✝ source target) #[]

def Miri.Input.CompilerQueryIndices.signatureRows {runtime : RuntimeMetadata} {raw : Lean.Json} (index : SignatureAbi runtime raw) (key : String) : Array (Nat × Lean.Json)

Equations

• Miri.Input.CompilerQueryIndices.signatureRows index key = Array.map (fun (row : Miri.Input.CompilerQueryIndices.SignatureAbiRow) => (row.index, row.record)) (index.data.rows.getD key #[])

def Miri.Input.CompilerQueryIndices.signatureAbiRows {runtime : RuntimeMetadata} {raw : Lean.Json} (index : SignatureAbi runtime raw) (key : String) : Array SignatureAbiRow

Internal query path selecting predecoded ABI outcomes while retaining each source row's index and raw record for exact duplicate checks.

Equations

• Miri.Input.CompilerQueryIndices.signatureAbiRows index key = index.data.rows.getD key #[]

def Miri.Input.CompilerQueryIndices.signatureRequestKey (inputs : Array MIR.TyId) (output : MIR.TyId) (abi : ABI.ExternAbi) (safety : MIR.Safety) (cVariadic splatted : Bool) : String

Equations

• Miri.Input.CompilerQueryIndices.signatureRequestKey inputs output abi safety cVariadic splatted = Miri.Input.CompilerQueryIndices.signatureKey✝ inputs output abi safety cVariadic splatted