Rust-side native call staging from pinned shims/native_lib/mod.rs. Required leaves describe concrete compiler, allocation, and external host operations; libffi does not acquire a fabricated pure Lean implementation.

structure Miri.Interpreter.Native.Hooks (P S C V Code : Type) : Type

• target : ABI.TargetDataLayout
• hostBits : Nat
• typeShape : C → ABI.TyAndLayout MIR.TyId → RvalueM S TypeShape
• layoutOf : C → MIR.TyId → RvalueM S (Except Unit (ABI.TyAndLayout MIR.TyId))
• libraries : S → Array Library
• lookupSymbol : C → Library → String → RvalueM S (Option (SymbolInfo Code))
• tracingEnabled : S → Bool
• placeLayout : V → ABI.TyAndLayout MIR.TyId
• placePointer : V → Except StepError (Memory.Pointer (Option P))
• resolve : C → Memory.Pointer (Option P) → Nat → RvalueM S (Memory.AllocId × Nat)
• allocation : C → Memory.AllocId → RvalueM S (RawAllocation P)
• provenanceRange : C → Memory.AllocId → Nat → Nat → RvalueM S (Array P)
• inspectOutsideInterpreter : C → Memory.AllocId → Nat → Nat → RvalueM S (Array UInt8)
• expose : C → P → RvalueM S Unit
• warningEmitted : S → Bool

  Process-wide AtomicBool diagnostic dedup, before exposing provenance.

• setWarningEmitted : S → Bool → S
• diagnosticSharedMemory : C → Bool → RvalueM S Unit
• visitExposed : C → (Memory.AllocId → RvalueM S Unit) → RvalueM S Unit

  Reachability traversal is the canonical allocation visitor (including newly exposed allocations); callback mutations/errors must commit in source order.

• isLiveData : C → Memory.AllocId → RvalueM S Bool
• exposePhysical : C → Memory.AllocId → Bool → RvalueM S Unit
• nativeWrite : C → Memory.AllocId → Option (Nat × Nat) → RvalueM S Unit
• rawCall : C → Code → Array OwnedArg → FfiType → ABI.Size → RvalueM S (Array UInt8 × Option (Array AccessEvent))

  Actual libffi+supervisor operation. OwnedArg descriptors are consumed once.

• writeBytes : C → Memory.Pointer (Option P) → Array UInt8 → RvalueM S Unit
• tryResolve : C → Memory.Pointer (Option P) → Nat → RvalueM S (Option (Memory.AllocId × Nat))
• enforceValidity : C → ABI.TyAndLayout MIR.TyId → RvalueM S Bool
• enforceRecursively : C → ABI.TyAndLayout MIR.TyId → RvalueM S Bool
• validate : C → V → Bool → Bool → RvalueM S Unit
• allocationFromAddress : C → Nat → Nat → RvalueM S (Option Memory.AllocId)

  Exact native address resolver; length is the remaining range after popping its current byte, as in source Range::next followed by Range::len.

def Miri.Interpreter.Native.queryLayout {P S C V Code : Type} (h : Hooks P S C V Code) (choice : C) (ty : MIR.TyId) : RvalueM S (ABI.TyAndLayout MIR.TyId)

A known compiler layout failure is unsupported FFI type; an unavailable compiler query remains an outer RvalueM error and is never converted to success.

Equations

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

def Miri.Interpreter.Native.ffiType {P S C V Code : Type} (h : Hooks P S C V Code) (choice : C) : Nat → ABI.TyAndLayout MIR.TyId → RvalueM S FfiType

Type conversion fails before any operand inspection/exposure. The explicit query fuel is an obligation on recursive compiler metadata, never a success default.

Equations

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

def Miri.Interpreter.Native.argument {P S C V Code : Type} [Memory.PointerProvenance P] (h : Hooks P S C V Code) (choice : C) (fuel : Nat) (tracing : Bool) (value : OpTy P) : RvalueM S OwnedArg

Indirect argument inspection deliberately allows uninit and pointer bytes; it must use the outside-interpreter accessor, not normal Rust memory reads.

Equations

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

def Miri.Interpreter.Native.applyAccesses {P S C V Code : Type} (h : Hooks P S C V Code) (choice : C) (events : Array AccessEvent) : RvalueM S Unit

Equations

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

def Miri.Interpreter.Native.returnToMemory {P S C V Code : Type} (h : Hooks P S C V Code) (choice : C) (bytes : Array UInt8) (dest : V) : RvalueM S Unit

Equations

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

def Miri.Interpreter.Native.findSymbol {P S C V Code : Type} (h : Hooks P S C V Code) (choice : C) (name : String) : RvalueM S (Option Code)

Equations

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

def Miri.Interpreter.Native.call {P S C V Code : Type} [Memory.PointerProvenance P] (h : Hooks P S C V Code) (choice : C) (fuel : Nat) (name : String) (dest : V) (args : Array (OpTy P)) : RvalueM S Bool

Full Rust-side call pipeline: lookup, argument conversion, return ABI query, reachable-memory preparation, host call, trace application, return validation.

Equations

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