Source-owned assembly of native calls. Compiler ABI metadata is queried from the prepared image and the live runtime-array registry. The remaining inputs are narrow host operations: real symbol/address lookup, stable backing, process-global tracing state, and the source supervisor/libffi boundary. The resulting call always runs NativeMachine's canonical argument, exposure, Tree Borrows, trace, return-write, and validity pipeline.

These are external native operations, not a replacement String → Bool foreign shim. In particular, execute retains the source interchange and supervisor protocol and delegates only real libffi/process operations.

structure Miri.Input.EvalNativeSourceConstruction.RawHost (U C N Code : Type) : Type

• exposePhysical : Memory.AllocId → Bool → Interpreter.NativeMachine.M Memory.MiriMemoryKind U Unit
• process : EvalNativeConstruction.Process U C
• lookupSymbol : C → N → String → Interpreter.NativeMachine.M Memory.MiriMemoryKind U (Option (Interpreter.Native.SymbolInfo Code))
• supervisor : Interpreter.Native.Trace.ChildHooks (Interpreter.NativeMachine.State Memory.MiriMemoryKind U) C
• ffi : (Memory.AllocId → Array UInt8 → Interpreter.NativeMachine.M Memory.MiriMemoryKind U Unit) → C → Code → Array Interpreter.Native.OwnedArg → Interpreter.Native.FfiType → ABI.Size → Interpreter.NativeMachine.M Memory.MiriMemoryKind U (Array UInt8)

The array accessor must address the same EvalWorld.World carried by the native-call state. It is supplied by the canonical Core configuration (for source execution, EvalProjectionMachine.arrays).

def Miri.Input.EvalNativeSourceConstruction.effects {U C N Code : Type} (hostBits : Nat) (lifecycleBacking : Option (Interpreter.NativeAllocationLifecycle.Backing (Interpreter.NativeMachine.State Memory.MiriMemoryKind U))) (p : CompilerProviders.Prepared) (arrays : RuntimeArrayQueries.Access (Interpreter.NativeMachine.State Memory.MiriMemoryKind U)) (raw : RawHost U C N Code) : EvalNativeMachine.Effects U C N Code

Equations

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

Build the actual native call action over the caller's canonical memory and validity providers. NativeMachine.call first searches the live loaded-library vector, so an empty vector returns the source false result without demanding symbol lookup, libffi, or tracing capabilities.

def Miri.Input.EvalNativeSourceConstruction.call {Os R P H D O Aff B Poll Instant System N Profiler C Code F A Pad : Type} (hostBits : Nat) (lifecycleBacking : Option (Interpreter.NativeAllocationLifecycle.Backing (Interpreter.NativeMachine.State Memory.MiriMemoryKind (EvalNativeMachine.U Os R P H D O Aff B Poll Instant System N Profiler)))) (p : CompilerProviders.Prepared) (arrays : RuntimeArrayQueries.Access (Interpreter.NativeMachine.State Memory.MiriMemoryKind (EvalNativeMachine.U Os R P H D O Aff B Poll Instant System N Profiler))) (raw : Option (RawHost (EvalNativeMachine.U Os R P H D O Aff B Poll Instant System N Profiler) C N Code)) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalNativeMachine.U Os R P H D O Aff B Poll Instant System N Profiler)) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (EvalNativeMachine.U Os R P H D O Aff B Poll Instant System N Profiler))) (validity : Interpreter.ValidityVisitor.Hooks Memory.Provenance (EvalNativeMachine.S Os R P H D O Aff B Poll Instant System N Profiler) C Interpreter.MachineHooks.FrameExtra F A Pad) (validationBudget reachabilityBudget : Nat) (choice : C) (fuel : Nat) (name : String) (destination : Interpreter.RuntimePlace Memory.Provenance) (arguments : Array (Interpreter.OpTy Memory.Provenance)) : Interpreter.NativeMachine.M Memory.MiriMemoryKind (EvalNativeMachine.U Os R P H D O Aff B Poll Instant System N Profiler) Bool

Equations

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