Stateful bindings of pinned miri/src/alloc_addresses/mod.rs to the canonical interpreter machine. Random outcomes are inputs, never fixed seeds. Native allocation and compiler-global materialization are external effects.

structure Miri.Interpreter.PointerMachine.User (U : Type) : Type

• addresses : Memory.AllocAddresses.GlobalAddressState
• payload : U
• symbolicAlignment : Array (Memory.AllocId × ABI.Size × ABI.Align)

@[reducible, inline]

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

Equations

• Miri.Interpreter.PointerMachine.State K U = Miri.Interpreter.MachineHooks.State K (Miri.Interpreter.PointerMachine.User U)

@[reducible, inline]

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

Equations

• Miri.Interpreter.PointerMachine.M K U A = Miri.Interpreter.MachineHooks.M K (Miri.Interpreter.PointerMachine.User U) A

structure Miri.Interpreter.PointerMachine.Hooks (K U : Type) : Type

• arithmetic : Memory.PointerArithmetic
• externalAddress : Memory.AllocId → Memory.AllocAddresses.AllocationAddressInfo → M K U UInt64
• ensureTreeExtra : Memory.AllocId → M K U Unit

  Compiler globals may require allocation before Tree Borrows has an extra.

• diagnosticIntToPtr : M K U Unit
• strictIntToPtr : StepError

  Strict provenance is a machine termination, not Rust UB.

• classifyAddressError : Memory.AllocAddresses.AddressStateError → StepError

def Miri.Interpreter.PointerMachine.addrFromAllocId {K U : Type} (h : Hooks K U) (id : Memory.AllocId) (kind : Option Memory.AllocAddresses.AddressMemoryKind) (choice : Memory.AllocAddresses.AddressRandomChoices) : M K U UInt64

The cached path performs no metadata lookup, thread lookup or external call.

Equations

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

def Miri.Interpreter.PointerMachine.exposeProvenance {K U : Type} [DecidableEq K] (h : Hooks K U) (provenance : Memory.Provenance) : M K U Unit

Exposure commits set membership before materializing globals or mutating TB. All per-range tree mutations are retained even when exposure fails.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.PointerMachine.exposeProvenance h provenance = pure ()

def Miri.Interpreter.PointerMachine.pointerFromExposedAddress {K U : Type} (h : Hooks K U) (address : UInt64) : M K U (Memory.Pointer (Option Memory.Provenance))

Integer casts create wildcard provenance without allocation resolution.

Equations

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

def Miri.Interpreter.PointerMachine.ptrGetAlloc {K U : Type} (h : Hooks K U) (pointer : Memory.Pointer Memory.Provenance) (size : Int64) : M K U (Option (Memory.AllocId × ABI.Size))

Allocation resolution uses actual canonical memory liveness and sizes; dead concrete provenance is intentionally returned for later UAF checking.

Equations

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

def Miri.Interpreter.PointerMachine.adjustAllocRootPointer {K U : Type} (h : Hooks K U) (id : Memory.AllocId) (tag : Memory.BorTag) (offset : ABI.Size) (kind : Memory.AllocAddresses.AddressMemoryKind) (choice : Memory.AllocAddresses.AddressRandomChoices) : M K U (Memory.Pointer Memory.Provenance)

Relative compiler root pointers become absolute without losing identity/tag.

Equations

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

def Miri.Interpreter.PointerMachine.freeAllocId {K U : Type} (h : Hooks K U) (id : Memory.AllocId) (size : ABI.Size) (align : ABI.Align) (kind : Memory.AllocAddresses.AddressMemoryKind) (choice : Bool) : M K U Unit

Source removal precedes pool choice, clock release and pool insertion. The old vector clock is stored while the canonical active clock increments.

Equations

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

def Miri.Interpreter.PointerMachine.removeUnreachableAllocs {K U : Type} (live : Array Memory.AllocId) : M K U Unit

Source GC only drops id-to-base entries after the collector has proved unreachability; inverse/exposed entries are removed by deallocation.

Equations

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

structure Miri.Interpreter.PointerMachine.GlobalBytesHooks (K U : Type) : Type

Native memory ownership and native call trampolines cannot be represented by synthetic addresses. The external provider must consume prepared bytes, check host alignment/length, and copy the supplied contents in source order.

• nativeEnabled : Bool
• nativePreparedBytes : Memory.AllocId → Array UInt8 → ABI.Align → M K U (Array UInt8)

def Miri.Interpreter.PointerMachine.getGlobalAllocBytes {K U : Type} (h : Hooks K U) (bytesHooks : GlobalBytesHooks K U) (id : Memory.AllocId) (bytes : Array UInt8) (align : ABI.Align) (choice : Memory.AllocAddresses.AddressRandomChoices) : M K U (Array UInt8)

Equations

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

def Miri.Interpreter.PointerMachine.symbolicAlignment (symbolic : Bool) (kind : Memory.AllocationKind) (allocationAlign : ABI.Align) (promise : Option (ABI.Size × ABI.Align)) (offset : ABI.Size) (required : ABI.Align) : Except ABI.AlignError (Option Memory.Misalignment)

Source symbolic alignment override. Non-live and non-symbolic cases defer only the ordinary concrete alignment check to the existing memory engine.

Equations

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