Native mod.rs:367–435/444–490 direct ABI and closure preparation. Compiler queries are separated from memory operations; building a host trampoline never requires fabricated NativeHooks read/write callbacks.

structure Miri.Interpreter.NativeAbi.Queries (S C : Type) : Type

• typeShape : C → LocalLayout → RvalueM S Native.TypeShape
• layoutOf : C → MIR.TyId → RvalueM S (Except Unit LocalLayout)

def Miri.Interpreter.NativeAbi.ffiType {S C : Type} (q : Queries S C) (choice : C) : Nat → LocalLayout → RvalueM S Native.FfiType

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.NativeAbi.ffiType q choice 0 x✝ = throw (Miri.Interpreter.StepError.resourceExhaustion "native FFI recursive compiler query budget exhausted")

structure Miri.Interpreter.NativeAbi.ClosureHost (S C Code : Type) : Type

• build : C → Option (Array Native.FfiType × Native.FfiType) → Bool → RvalueM S Code

  Actual libffi Builder/closure/code pointer. Source intentionally leaks both data and closure until process exit, retaining its context interchange. For unsupported signatures the builder receives no descriptors and must install the source diagnostic-and-exit trampoline, not reject construction.

def Miri.Interpreter.NativeAbi.buildClosure {S C Code : Type} (queries : Queries S C) (host : ClosureHost S C Code) (choice : C) (fuel : Nat) (inputs : Array MIR.TyId) (output : MIR.TyId) : RvalueM S Code

Only source unsupported-signature errors choose the aborting descriptor. Missing compiler evidence, resource limits and machine failures propagate.

Equations

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