Exact native callback signature from alloc_addresses/mod.rs:167–174. The catalog records the actual compiler query after full-instance substitution and bound-region erasure, with no normalization or FnAbi reconstruction.

def Miri.Input.CompilerNativeSignatures.query (p : CompilerProviders.Prepared) (callee : Interpreter.CallInstance) : Except String (Array MIR.TyId × MIR.TyId)

Equations

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

def Miri.Input.CompilerNativeSignatures.make {K U Other C : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (arrays : RuntimeArrayQueries.Access (Interpreter.MachineAddress.State K U)) (registry : Interpreter.PointerMachine.User U → Interpreter.FunctionPointers.Registry Other) : Interpreter.NativeAddressSource.Compiler K U C

Equations

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

structure Miri.Input.CompilerNativeSignatures.Host (K U C : Type) : Type

Remaining native capabilities are actual allocator/libffi effects plus source build configuration and a finite compiler traversal budget.

• backing : Interpreter.NativeAllocationLifecycle.Backing (Interpreter.MachineAddress.State K U)
• closure : Interpreter.NativeAbi.ClosureHost (Interpreter.MachineAddress.State K U) C Nat
• closuresEnabled : Bool
• queryBudget : Nat

def Miri.Input.CompilerNativeSignatures.effects {K U Other C : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (arrays : RuntimeArrayQueries.Access (Interpreter.MachineAddress.State K U)) (registry : Interpreter.PointerMachine.User U → Interpreter.FunctionPointers.Registry Other) (host : Host K U C) : Interpreter.NativeAddressSource.Effects K U C

Optional native construction installs the direct compiler catalog adapter; callers cannot supply a substitute whole function-signature query here.

Equations

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

def Miri.Input.CompilerNativeSignatures.optionalEffects {K U Other C : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (arrays : RuntimeArrayQueries.Access (Interpreter.MachineAddress.State K U)) (registry : Interpreter.PointerMachine.User U → Interpreter.FunctionPointers.Registry Other) (host : Option (Host K U C)) : Option (Interpreter.NativeAddressSource.Effects K U C)

Equations

• Miri.Input.CompilerNativeSignatures.optionalEffects p image arrays registry host = Option.map (Miri.Input.CompilerNativeSignatures.effects p image arrays registry) host