Internal connection from compiler input records to the source ABI compatibility port. Missing compiler predicates/normalization are mandatory query obligations, never heuristic equivalence based on size or debug strings.

@[reducible, inline]

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

Equations

• Miri.Input.CallCompatibility.Result = Except Miri.Input.RuntimeMetadataError

def Miri.Input.CallCompatibility.attributes (source : AbiAttributes) : Result ABI.ArgAttributes

Equations

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

def Miri.Input.CallCompatibility.register (source : AbiRegister) : Result ABI.Reg

Equations

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

def Miri.Input.CallCompatibility.castTarget (source : AbiCastTarget) : Result ABI.CastTarget

Equations

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

def Miri.Input.CallCompatibility.passMode (source : AbiPassMode) : Result ABI.PassMode

Equations

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

def Miri.Input.CallCompatibility.argument (runtime : RuntimeMetadata) (source : AbiArgument) : Result (ABI.ArgAbi TypeId)

Equations

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

structure Miri.Input.CallCompatibility.Evidence (S : Type) : Type

These source compiler queries are absent or only partially represented by the exporter. Each consumer must supply exact-key evidence or explicit errors. In particular, item names are not reconstructed from diagnostic def paths.

• eraseUnsafeBinder : TypeId → Interpreter.LayoutCompat.M S TypeId
• normalize : TypeId → Interpreter.LayoutCompat.M S TypeId
• reprEqualUpToSeed : TypeId → TypeId → Interpreter.LayoutCompat.M S Bool
• itemName : TypeId → Interpreter.LayoutCompat.M S String
• nonnullOptimizationGuaranteed : TypeId → Interpreter.LayoutCompat.M S Bool
• isGlobalBox : TypeId → Interpreter.LayoutCompat.M S Bool
• boxedType : TypeId → Interpreter.LayoutCompat.M S TypeId
• pointerMetadataType : TypeId → Interpreter.LayoutCompat.M S TypeId

def Miri.Input.CallCompatibility.kind (runtime : RuntimeMetadata) (id : TypeId) : Result (Interpreter.LayoutCompat.TypeKind TypeId)

Equations

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

def Miri.Input.CallCompatibility.adt (runtime : RuntimeMetadata) (id : TypeId) : Result (Interpreter.LayoutCompat.AdtInfo TypeId)

Equations

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

structure Miri.Input.CallCompatibility.UnitLayoutCache (runtime : RuntimeMetadata) : Type

The strict unit query used by source ABI compatibility. Its result retains the exact scan outcome, including duplicate and malformed metadata failures.

• value : Result (ABI.TyAndLayout TypeId)
• exact : self.value = Miri.Input.CallCompatibility.unitLayout✝ runtime

def Miri.Input.CallCompatibility.bindUnitLayout (runtime : RuntimeMetadata) : UnitLayoutCache runtime

Equations

• Miri.Input.CallCompatibility.bindUnitLayout runtime = { value := Miri.Input.CallCompatibility.unitLayout✝ runtime, exact := ⋯ }

def Miri.Input.CallCompatibility.queries {S : Type} (runtime : RuntimeMetadata) (evidence : Evidence S) (unitCache : Option (UnitLayoutCache runtime) := none) : Interpreter.LayoutCompat.Queries TypeId S

Connect the source algorithm to canonical records while keeping every missing compiler query explicit and preserving the caller's effect state.

Equations

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

def Miri.Input.CallCompatibility.checkArgumentCompat {S : Type} (runtime : RuntimeMetadata) (evidence : Evidence S) (fuel : Nat) (caller callee : AbiArgument) : Interpreter.LayoutCompat.M S Bool

Equations

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