Actual native byte ownership on the canonical Allocation/MemoryState. Backing is allocated before AllocId reservation; failed insertion drops only uninserted backing. Deallocation drops the detached allocation on every return, including source validation/hook failures, as Rust's local ownership requires.

structure Miri.Interpreter.NativeAllocationLifecycle.Backing (S : Type) : Type

• isolated : Bool
• zeroed : ABI.Size → ABI.Align → EStateM StepError S (Option NativeAllocBytes.Buffer)
• fromBytes : Array UInt8 → ABI.Align → EStateM StepError S NativeAllocBytes.Buffer
• copyInto : NativeAllocBytes.Buffer → Array UInt8 → EStateM StepError S Unit
• snapshot : NativeAllocBytes.Buffer → EStateM StepError S (Array UInt8)
• release : NativeAllocBytes.Buffer → EStateM StepError S Unit

def Miri.Interpreter.NativeAllocationLifecycle.liftMachineAction {K U A : Type} (action : EStateM StepError (MachineHooks.MachineState K U) A) : EStateM StepError (MachineHooks.State K U) A

Lift the one canonical machine-owned allocator into the full interpreter state, retaining its current stack and all machine mutations on errors.

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.liftBacking {K U : Type} (backing : Backing (MachineHooks.MachineState K U)) : Backing (MachineHooks.State K U)

Equations

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

structure Miri.Interpreter.NativeAllocationLifecycle.Access (S Prov Extra K H : Type) : Type

• memory : S → Memory.MemoryState Prov Extra K
• hooks : S → H
• synchronizeMemory : Memory.MemoryState Prov Extra K → H → H
• put : S → Memory.MemoryState Prov Extra K → H → S

def Miri.Interpreter.NativeAllocationLifecycle.buffer {Prov Extra : Type} (allocation : Memory.Allocation Prov Extra) : Option NativeAllocBytes.Buffer

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.address {Prov Extra : Type} (allocation : Memory.Allocation Prov Extra) : Except String Nat

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.prepareBytes {S : Type} (backing : Backing S) (bytes : Array UInt8) (align : ABI.Align) : EStateM StepError S (Array UInt8 × Option Memory.NativeBufferOwnership)

Fresh from_bytes ownership for ordinary cloning/global-allocator mode. Native compiler globals must instead take their already prepared buffer from source prepared_alloc_bytes; they must not select this fresh allocator.

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.alignmentBytes {S : Type} (align : ABI.Align) : EStateM StepError S Nat

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.commitBytes {S : Type} (backing : Backing S) (owner : Memory.NativeBufferOwnership) (bytes : Array UInt8) (align : ABI.Align) : EStateM StepError S Unit

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.releaseBytes {S : Type} (backing : Backing S) (owner : Memory.NativeBufferOwnership) (_size : ABI.Size) (_align : ABI.Align) : EStateM StepError S Unit

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.createZeroed {S Prov : Type} (backing : Backing S) (size : ABI.Size) (align : ABI.Align) (init : Memory.AllocInit) : EStateM StepError S (Except Memory.AllocError (Memory.Allocation Prov))

Actual native Allocation::try_new; host null leaves the ID supply intact. The zero snapshot validates the external storage contract before reservation.

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.cloneBytes {S Prov Extra : Type} (backing : Backing S) (allocation : Memory.Allocation Prov Extra) : EStateM StepError S (Memory.Allocation Prov Extra)

Ordinary owned-byte clone preserves mask/provenance/extras and receives fresh ownership. Native compiler globals use source prepared buffers instead.

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.releaseAllocation {S Prov Extra : Type} (backing : Backing S) (allocation : Memory.Allocation Prov Extra) : EStateM StepError S Unit

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.allocate {K S Prov Extra H : Type} [DecidableEq K] (access : Access S Prov Extra K H) (backing : Backing S) (size : ABI.Size) (align : ABI.Align) (kind : Memory.MemoryKind K) (init : Memory.AllocInit) (maximum : ABI.Size) (globalKind : Option (Memory.MemoryKind K)) (initExtra : Memory.MemoryState Prov Extra K → H → Memory.AllocId → Memory.MemoryKind K → ABI.Size → ABI.Align → Memory.MemoryStateHookResult Prov Extra K H Extra) (adjustRoot : Memory.MemoryState Prov Extra K → H → Memory.AllocId → Memory.MemoryKind K → Memory.MemoryStateHookResult Prov Extra K H (Memory.Pointer Prov)) : EStateM StepError S (Except Memory.MemoryLifecycleError (Memory.Pointer Prov))

Direct source allocation lifecycle; no FFI-time materialization.

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.deallocate {K S Prov Extra H PE : Type} [DecidableEq K] (access : Access S Prov Extra K H) (backing : Backing S) (pointer : Memory.Pointer (Option Prov)) (oldLayout : Option (ABI.Size × ABI.Align)) (kind : Memory.MemoryKind K) (hooks : Memory.MemoryLifecycleHooks Prov Extra K H PE) : EStateM StepError S (Except Memory.MemoryLifecycleError Unit)

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.bindAllocation {K U : Type} (backing : Backing (MachineHooks.State K U)) (config : PlaceMachine.AllocationConfig K U) : PlaceMachine.AllocationConfig K U

Canonical stack/temporary creation selects native source storage, retaining existing diagnostic/TB/race/address operations and their order.

Equations

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

def Miri.Interpreter.NativeAllocationLifecycle.bindDeallocation {K U P : Type} (backing : Backing (MachineHooks.State K U)) (hooks : AllocationMachine.DeallocationHooks K U P) : AllocationMachine.DeallocationHooks K U P

Equations

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