Concrete native memory adapter. Source: native_lib/mod.rs:181–360,550–600 and rustc interpret/memory.rs:1104–1134. FFI execution, actual stable native backing pointers, physical exposure and process-global state remain explicit host effects, not fabricated native execution results.

@[reducible, inline]

abbrev Miri.Interpreter.NativeMachine.User (User : Type) : Type

Equations

• Miri.Interpreter.NativeMachine.User = Miri.Interpreter.ValidityMachine.UserState

@[reducible, inline]

abbrev Miri.Interpreter.NativeMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.NativeMachine.State K U = Miri.Interpreter.ValidityMachine.State K U

@[reducible, inline]

abbrev Miri.Interpreter.NativeMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.NativeMachine.M K U = Miri.Interpreter.ValidityMachine.M K U

@[reducible, inline]

abbrev Miri.Interpreter.NativeMachine.Data : Type

Equations

• Miri.Interpreter.NativeMachine.Data = Miri.Memory.Allocation Miri.Memory.Provenance Miri.TreeBorrows.BorrowTree

def Miri.Interpreter.NativeMachine.raw {K U : Type} [DecidableEq K] (access : ValidityMachine.Access K U) (id : Memory.AllocId) (mutable : Bool) : M K U Data

Raw access has no Rust read/write hooks. Global conversion effects and failed mutable materialization are committed before returning its error.

Equations

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

def Miri.Interpreter.NativeMachine.publish {K U : Type} [DecidableEq K] (access : ValidityMachine.Access K U) (id : Memory.AllocId) (bytes : Array UInt8) : M K U Unit

The host publication callback preserves already observed bytes even when its subsequent FFI operation fails. No mask/provenance transition runs here.

Equations

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

def Miri.Interpreter.NativeMachine.processWrite {K U : Type} [DecidableEq K] (access : ValidityMachine.Access K U) (id : Memory.AllocId) (range : Option (Nat × Nat)) : M K U Unit

Equations

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

structure Miri.Interpreter.NativeMachine.Host (K U C Code : Type) : Type

• hostBits : Nat
• typeShape : C → LocalLayout → M K U Native.TypeShape
• layoutOf : C → MIR.TyId → M K U (Except Unit LocalLayout)
• libraries : State K U → Array Native.Library
• lookupSymbol : C → Nat → Native.Library → String → M K U (Option (Native.SymbolInfo Code))

  Index selects the actual loaded handle in the source library vector, including distinct handles with equal configured path strings.

• tracingEnabled : State K U → Bool
• backingAddress : Memory.AllocId → Data → M K U Nat

  Same stable, correctly aligned host storage that the canonical native address provider exposes. May materialize actual host storage, never invent an address or substitute copied storage with a different lifetime.

• exposePhysical : Memory.AllocId → Bool → M K U Unit
• warningEmitted : State K U → Bool
• setWarningEmitted : State K U → Bool → State K U
• diagnosticSharedMemory : C → Bool → M K U Unit
• execute : (Memory.AllocId → Array UInt8 → M K U Unit) → C → Code → Array Native.OwnedArg → Native.FfiType → ABI.Size → M K U (Array UInt8 × Option (Array Native.AccessEvent))

  Actual libffi + supervisor. Publish all changed owned backing snapshots through the supplied callback on every returning outcome, including errors; reports are host observations, not trusted claims of native program safety.

def Miri.Interpreter.NativeMachine.visitReachable {K U : Type} [DecidableEq K] (access : ValidityMachine.Access K U) (callback : Memory.AllocId → M K U Unit) : Nat → List Memory.AllocId → Array Memory.AllocId → M K U Unit

LIFO traversal snapshots children before callback mutation, matching visit_reachable_allocs. Fuel exhaustion is a resource error, not completion.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.NativeMachine.visitReachable access callback x✝¹ [] x✝ = pure ()
• Miri.Interpreter.NativeMachine.visitReachable access callback 0 (head :: tail) x✝ = throw (Miri.Interpreter.StepError.resourceExhaustion "native allocation reachability budget exhausted")

def Miri.Interpreter.NativeMachine.argument {K U C Code : Type} [DecidableEq K] (host : Host K U C Code) (access : ValidityMachine.Access K U) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (engine : Native.Hooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance) Code) (choice : C) (fuel : Nat) (tracing : Bool) (value : OpTy Memory.Provenance) : M K U Native.OwnedArg

Keep one source allocation snapshot across provenance exposure and raw argument inspection. The generic legacy Hook interface is not used to repeat these raw global queries. Immediate conversion reuses the source serializer.

Equations

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

def Miri.Interpreter.NativeMachine.call {K U C Code F A Pad : Type} [DecidableEq K] (host : Host K U C Code) (access : ValidityMachine.Access K U) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) (validity : ValidityVisitor.Hooks Memory.Provenance (State K U) C MachineHooks.FrameExtra F A Pad) (validationBudget reachabilityBudget : Nat) (choice : C) (fuel : Nat) (name : String) (dest : RuntimePlace Memory.Provenance) (args : Array (OpTy Memory.Provenance)) : M K U Bool

Connected native driver, including the source's single-snapshot argument and trace paths and single mutable return query. Native.Hooks remains useful for type conversion; no baseline NativeHooks is a production input.

Equations

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