Actual native loaded-library binding on the canonical World.host vector. Process-global tracing/FFI effects remain required external capabilities; no second native handle table or source-safe result is manufactured.

@[reducible, inline]

abbrev Miri.Input.EvalNativeMachine.Host (Poll Instant System H D O Native Profiler : Type) : Type

Equations

• Miri.Input.EvalNativeMachine.Host = Miri.Input.HostRuntime.Storage

@[reducible, inline]

abbrev Miri.Input.EvalNativeMachine.W (Os R P H D O Aff B Poll Instant System N Profiler : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalNativeMachine.U (Os R P H D O Aff B Poll Instant System N Profiler : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalNativeMachine.S (Os R P H D O Aff B Poll Instant System N Profiler : Type) : Type

Equations

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

structure Miri.Input.EvalNativeMachine.Effects (U C N Code : Type) : Type

Genuine compiler/native process/host effects. Symbol lookup receives the actual loaded handle, and must perform source dlsym+dladdr/path conversion.

• hostBits : Nat
• typeShape : C → Interpreter.LocalLayout → Interpreter.NativeMachine.M Memory.MiriMemoryKind U Interpreter.Native.TypeShape
• layoutOf : C → MIR.TyId → Interpreter.NativeMachine.M Memory.MiriMemoryKind U (Except Unit Interpreter.LocalLayout)
• lookupSymbol : C → N → String → Interpreter.NativeMachine.M Memory.MiriMemoryKind U (Option (Interpreter.Native.SymbolInfo Code))
• tracingEnabled : Interpreter.NativeMachine.State Memory.MiriMemoryKind U → Bool
• backingAddress : Memory.AllocId → Interpreter.NativeMachine.Data → Interpreter.NativeMachine.M Memory.MiriMemoryKind U Nat
• exposePhysical : Memory.AllocId → Bool → Interpreter.NativeMachine.M Memory.MiriMemoryKind U Unit
• warningEmitted : Interpreter.NativeMachine.State Memory.MiriMemoryKind U → Bool
• setWarningEmitted : Interpreter.NativeMachine.State Memory.MiriMemoryKind U → Bool → Interpreter.NativeMachine.State Memory.MiriMemoryKind U
• diagnosticSharedMemory : C → Bool → Interpreter.NativeMachine.M Memory.MiriMemoryKind U Unit
• execute : (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 × Option (Array Interpreter.Native.AccessEvent))

def Miri.Input.EvalNativeMachine.host {Os R P H D O Aff B Poll Instant System N Profiler C Code : Type} (effects : Effects (U Os R P H D O Aff B Poll Instant System N Profiler) C N Code) : Interpreter.NativeMachine.Host Memory.MiriMemoryKind (U Os R P H D O Aff B Poll Instant System N Profiler) C Code

Equations

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

def Miri.Input.EvalNativeMachine.call {Os R P H D O Aff B Poll Instant System N Profiler C Code F A Pad : Type} (effects : Effects (U Os R P H D O Aff B Poll Instant System N Profiler) C N Code) (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (U Os R P H D O Aff B Poll Instant System N Profiler)) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (U Os R P H D O Aff B Poll Instant System N Profiler))) (validity : Interpreter.ValidityVisitor.Hooks Memory.Provenance (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) (dest : Interpreter.RuntimePlace Memory.Provenance) (args : Array (Interpreter.FnArg Memory.Provenance)) : Interpreter.NativeMachine.M Memory.MiriMemoryKind (U Os R P H D O Aff B Poll Instant System N Profiler) Bool

Native calls share the same physical access, address/exposure map, typed validity visitor and loaded host handles as ordinary instruction execution.

Equations

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