Direct pointer source construction. Global relocation adjustment runs on actual machine state and never synthesizes a stack. Only external allocation addresses and extern-static resolution remain genuine external capabilities; managed address generation, salt choices and borrow root tags are source code. Human-facing int-to-pointer diagnostics are omitted under the project scope.

def Miri.Interpreter.PointerSource.addressError : Memory.AllocAddresses.AddressStateError → StepError

These are internal address invariants/resource stops, never Rust UB.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.PointerSource.addressError Miri.Memory.AllocAddresses.AddressStateError.strictIntegerToPointerCast = Miri.Interpreter.StepError.machineStop "Int2PtrWithStrictProvenance"
• Miri.Interpreter.PointerSource.addressError Miri.Memory.AllocAddresses.AddressStateError.strictAddressLookup = Miri.Interpreter.StepError.machineStop "Int2PtrWithStrictProvenance"
• Miri.Interpreter.PointerSource.addressError x✝ = Miri.Interpreter.StepError.invalidProgram (toString "allocation address invariant: " ++ toString (toString x✝))

def Miri.Interpreter.PointerSource.addressHooks {K U : Type} (runtime : ABI.RuntimeTargetDataLayout) (externalAddress : Memory.AllocId → Memory.AllocAddresses.AllocationAddressInfo → MachineAddress.M K U UInt64) : MachineAddress.Hooks K U

Equations

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

def Miri.Interpreter.PointerSource.pointers {K U : Type} [DecidableEq K] (globalKind : K) (h : MachineAddress.Hooks K U) (globals : Memory.GlobalAllocationHooks Memory.Provenance TreeBorrows.BorrowTree K (PlaceMachine.AccessState K (PointerMachine.User U))) : PointerMachine.Hooks K U

Actual lazy materialization is used for exposure; it is not a successful empty-tree callback. All address operations retain the same canonical maps.

Equations

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

def Miri.Interpreter.PointerSource.globalRootPointer {K U : Type} (choices : ExecutionChoices.Access (MachineAddress.State K U)) (h : MachineAddress.Hooks K U) (externStatic : MIR.DefId → MachineAddress.M K U (Memory.Pointer Memory.Provenance)) (pointer : Memory.Pointer Memory.CtfeProvenance) : MachineAddress.M K U (Memory.Pointer Memory.Provenance)

memory.rs global_root_pointer checks TLS/extern before the machine root adjustment. Extern statics return their source pointer directly. Root tags are installed before address assignment, retaining that prefix if assignment fails.

Equations

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