Concrete dictionary wiring for canonical Miri pointer provenance. These bindings retain the unrelated compiler, validity, memory and float leaves.

def Miri.Interpreter.PointerMachine.checkAccessSigned {K U : Type} (h : Hooks K U) (pointer : Memory.Pointer (Option Memory.Provenance)) (size : Int64) (message : Memory.CheckInAllocMsg) : M K U Unit

Signed interval checks use canonical memory, preserving the zero-byte fast path and concrete dangling provenance until liveness checking.

Equations

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

def Miri.Interpreter.PointerMachine.offsetInbounds {K U : Type} (h : Hooks K U) (pointer : Memory.Pointer (Option Memory.Provenance)) (offset : Int64) : M K U (Memory.Pointer (Option Memory.Provenance))

Equations

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

def Miri.Interpreter.PointerMachine.binary {K U C : Type} (h : Hooks K U) (target : ABI.TargetDataLayout) (ops : ScalarOpsHooks Memory.Provenance (State K U) C) (isRaw : C → MIR.TyId → M K U Bool) (usize : C → M K U (ABI.TyAndLayout MIR.TyId)) (pointeeLayout : C → MIR.TyId → M K U (ABI.TyAndLayout MIR.TyId)) (choice : C) (op : MIR.BinOp) (left right : RvalueImmTy Memory.Provenance) : M K U (RvalueImmTy Memory.Provenance)

rustc's Offset arm precedes Miri's bitwise/comparison machine fallback. Pointee layout and signedness are compiler facts; arithmetic is concrete.

Equations

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

def Miri.Interpreter.PointerMachine.scalarOps {K U C : Type} (h : Hooks K U) (target : ABI.TargetDataLayout) (ops : ScalarOpsHooks Memory.Provenance (State K U) C) (isRaw : C → MIR.TyId → M K U Bool) (usize : C → M K U (ABI.TyAndLayout MIR.TyId)) (pointeeLayout : C → MIR.TyId → M K U (ABI.TyAndLayout MIR.TyId)) : ScalarOpsHooks Memory.Provenance (State K U) C

Equations

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

def Miri.Interpreter.PointerMachine.castHooks {K U C V : Type} [DecidableEq K] (h : Hooks K U) (base : CastHooks Memory.Provenance (State K U) C V) : CastHooks Memory.Provenance (State K U) C V

Pointer-to-integer exposure preserves the scalar's actual address; only provenance exposure is rebound here. Cast's width/sign conversion is unchanged.

Equations

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

def Miri.Interpreter.PointerMachine.resolvePointer {K U : Type} (h : Hooks K U) (memory : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree K) (state : State K U) (pointer : Memory.Pointer (Option Memory.Provenance)) (size : Int) : Memory.MachineHookResult (State K U) (Except UInt64 (Memory.ResolvedPointer Memory.Provenance))

Memory's resolver distinguishes unresolved integer addresses from missing semantics. Wildcard resolution is performed anew on every access. A concrete pointer's TB tag and a wildcard marker survive in the resolved extra.

Equations

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

def Miri.Interpreter.PointerMachine.allocationAccessHooks {K U : Type} (h : Hooks K U) (base : Memory.AllocationAccessHooks Memory.Provenance TreeBorrows.BorrowTree K (State K U) Memory.Provenance) : Memory.AllocationAccessHooks Memory.Provenance TreeBorrows.BorrowTree K (State K U) Memory.Provenance

Actual AllocationAccess dictionary: all TB/race/sync physical access stages remain in the supplied machine dictionary; only provenance resolution changes.

Equations

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

def Miri.Interpreter.PointerMachine.intrinsicHooks {K U C V : Type} (h : Hooks K U) (base : IntrinsicHooks Memory.Provenance (State K U) C V) : IntrinsicHooks Memory.Provenance (State K U) C V

Bind the already ported full ptr_offset_from pipeline to actual memory resolution and inbounds checks. Errors inside the source deferred check are returned as values so its two-direction error preference remains intact.

Equations

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

def Miri.Interpreter.PointerMachine.checkAlignment {K U : Type} (h : Hooks K U) (symbolic enforce : Bool) (pointer : Memory.Pointer (Option Memory.Provenance)) (required : ABI.Align) : M K U Unit

Symbolic promises override the concrete address check only when source requests that mode and allocation kind. Canonical memory supplies liveness, alignment and allocation kind; wildcard provenance is resolved per call.

Equations

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