alloc_addresses/mod.rs:139–159,415–445. Real zeroed native backing is reserved before address publication, kept in canonical alloc-address state by AllocId, removed before CTFE byte copy, and transferred into Allocation ownership without a second allocation.

structure Miri.Interpreter.NativePreparedGlobals.Access (S : Type) : Type

• get : S → Memory.AllocAddresses.GlobalAddressState
• put : S → Memory.AllocAddresses.GlobalAddressState → S
• isCompilerGlobal : S → Memory.AllocId → Bool

def Miri.Interpreter.NativePreparedGlobals.machineAccess {K U : Type} : Access (MachineHooks.MachineState K (PointerMachine.User U))

The source store lives in alloc-address state, so raw-global materialization cannot overwrite its ownership transfer when committing a MemoryState result.

Equations

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

def Miri.Interpreter.NativePreparedGlobals.stateAccess {K U : Type} : Access (MachineHooks.State K (PointerMachine.User U))

Equations

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

def Miri.Interpreter.NativePreparedGlobals.reserve {S : Type} (access : Access S) (backing : NativeAllocationLifecycle.Backing S) (id : Memory.AllocId) (size : ABI.Size) (align : ABI.Align) : EStateM StepError S Nat

Called precisely inside first native global address assignment. The source allocates before try_insert, so even duplicate-ID failure follows allocation.

Equations

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

def Miri.Interpreter.NativePreparedGlobals.dummyAddress {S : Type} (backing : NativeAllocationLifecycle.Backing S) : EStateM StepError S Nat

Pinned dummy_alloc: allocate one zero byte with alignment one and leak its real backing for a unique function/vtable/va-list identity until process exit. No ownership entry is inserted and no host address is synthesized.

Equations

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

def Miri.Interpreter.NativePreparedGlobals.address {S : Type} (access : Access S) (id : Memory.AllocId) : EStateM StepError S Nat

Existing prepared backing can be observed without transferring ownership. Address caching owns first-call detection; repeated reserve is an assertion.

Equations

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

def Miri.Interpreter.NativePreparedGlobals.takeAndCopy {S : Type} (access : Access S) (backing : NativeAllocationLifecycle.Backing S) (ensureAddress : Memory.AllocId → EStateM StepError S Nat) (id : Memory.AllocId) (bytes : Array UInt8) (align : ABI.Align) : EStateM StepError S (Array UInt8 × Option Memory.NativeBufferOwnership)

The caller is the canonical address engine; it must be invoked before take, so a self-reference sees the already cached address during pointer conversion.

Equations

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

def Miri.Interpreter.NativePreparedGlobals.bytes {K U : Type} (access : Access (MachineHooks.MachineState K U)) (backing : NativeAllocationLifecycle.Backing (MachineHooks.MachineState K U)) (ensureAddress : Memory.AllocId → PlaceMachine.MachineM K U Nat) : GlobalAllocationMachine.Bytes K U

Direct compiler-global backing dictionary on the same machine memory.

Equations

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