Pinned alloc_addresses/mod.rs:110–198,225–233. Native external-address selection runs on the actual machine, reading canonical allocation kinds and owners. Only compiler signature queries and actual libffi closure construction remain supplied; there is no whole-allocation-address oracle or invented frame.

@[reducible, inline]

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

Equations

• Miri.Interpreter.NativeAddressSource.State = Miri.Interpreter.MachineAddress.State

@[reducible, inline]

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

Equations

• Miri.Interpreter.NativeAddressSource.M = Miri.Interpreter.MachineAddress.M

structure Miri.Interpreter.NativeAddressSource.Compiler (K U C : Type) : Type

• queries : NativeAbi.Queries (State K U) C
• functionSignature : C → Memory.AllocId → M K U (Array MIR.TyId × MIR.TyId)

  Actual instantiate_bound_regions_with_erased(fn_sig(instance)) query on this compiler GlobalAlloc::Function. Missing evidence is an error; it must not choose the non-instance dummy-allocation branch.

structure Miri.Interpreter.NativeAddressSource.Effects (K U C : Type) : Type

• backing : NativeAllocationLifecycle.Backing (State K U)
• compiler : Compiler K U C
• closure : NativeAbi.ClosureHost (State K U) C Nat
• closuresEnabled : Bool

  Source cfg(all(feature="native-lib", unix)), not guest target guessing.

• queryBudget : Nat

def Miri.Interpreter.NativeAddressSource.externalAddress {K U C : Type} (effects : Effects K U C) (choice : C) (id : Memory.AllocId) (_sourceInfo : Memory.AllocAddresses.AllocationAddressInfo) : M K U UInt64

Actual source native branch. The surrounding MachineAddress engine owns TypeId zero, first-use caching and post-effect address state.

Equations

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

def Miri.Interpreter.NativeAddressSource.hooks {K U C : Type} (runtime : ABI.RuntimeTargetDataLayout) (classify : Memory.AllocAddresses.AddressStateError → StepError) (effects : Effects K U C) (choice : C) : MachineAddress.Hooks K U

Construct the native machine address dictionary from genuine leaves.

Equations

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

def Miri.Interpreter.NativeAddressSource.globalBytes {K U C : Type} (choices : ExecutionChoices.Access (State K U)) (h : MachineAddress.Hooks K U) (effects : Effects K U C) : GlobalAllocationMachine.Bytes K (PointerMachine.User U)

Source get_global_alloc_bytes shares both the actual address engine and its prepared-owner store; self-references observe the cached address before compiler pointer relocation begins.

Equations

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