The generic engine pointer from pinned rustc mir/interpret/pointer.rs and the concrete Miri provenance from machine.rs are kept separate. In Miri the offset field is an absolute address; with CTFE provenance it is relative. None of these constructors or wrapping operations establishes dereference validity, liveness, alignment, permission, or initialization.

structure Miri.Memory.Pointer (Prov : Type u) : Type u

• offset : ABI.Size
• provenance : Prov

def Miri.Memory.instDecidableEqPointer.decEq {Prov✝ : Type u_1} [DecidableEq Prov✝] (x✝ x✝¹ : Pointer Prov✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instDecidableEqPointer {Prov✝ : Type u_1} [DecidableEq Prov✝] : DecidableEq (Pointer Prov✝)

Equations

• Miri.Memory.instDecidableEqPointer = Miri.Memory.instDecidableEqPointer.decEq

def Miri.Memory.instReprPointer.repr {Prov✝ : Type u_1} [Repr Prov✝] : Pointer Prov✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprPointer {Prov✝ : Type u_1} [Repr Prov✝] : Repr (Pointer Prov✝)

Equations

• Miri.Memory.instReprPointer = { reprPrec := Miri.Memory.instReprPointer.repr }

inductive Miri.Memory.PointerError : Type

Errors corresponding to source assertion/try_into failures, not UB.

• sourceSizeError (reason : ABI.SizeError) : PointerError
• unsignedConversionOverflow : PointerError
• signedConversionOverflow : PointerError
• relativeProvenanceHasNoAbsoluteAddress : PointerError

def Miri.Memory.instDecidableEqPointerError.decEq (x✝ x✝¹ : PointerError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqPointerError.decEq (Miri.Memory.PointerError.sourceSizeError a) (Miri.Memory.PointerError.sourceSizeError b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqPointerError.decEq (Miri.Memory.PointerError.sourceSizeError reason) Miri.Memory.PointerError.unsignedConversionOverflow = isFalse ⋯
• Miri.Memory.instDecidableEqPointerError.decEq (Miri.Memory.PointerError.sourceSizeError reason) Miri.Memory.PointerError.signedConversionOverflow = isFalse ⋯
• Miri.Memory.instDecidableEqPointerError.decEq (Miri.Memory.PointerError.sourceSizeError reason) Miri.Memory.PointerError.relativeProvenanceHasNoAbsoluteAddress = isFalse ⋯
• Miri.Memory.instDecidableEqPointerError.decEq Miri.Memory.PointerError.unsignedConversionOverflow (Miri.Memory.PointerError.sourceSizeError reason) = isFalse ⋯
• Miri.Memory.instDecidableEqPointerError.decEq Miri.Memory.PointerError.unsignedConversionOverflow Miri.Memory.PointerError.unsignedConversionOverflow = isTrue ⋯
• Miri.Memory.instDecidableEqPointerError.decEq Miri.Memory.PointerError.signedConversionOverflow (Miri.Memory.PointerError.sourceSizeError reason) = isFalse ⋯
• Miri.Memory.instDecidableEqPointerError.decEq Miri.Memory.PointerError.signedConversionOverflow Miri.Memory.PointerError.signedConversionOverflow = isTrue ⋯
• Miri.Memory.instDecidableEqPointerError.decEq Miri.Memory.PointerError.relativeProvenanceHasNoAbsoluteAddress (Miri.Memory.PointerError.sourceSizeError reason) = isFalse ⋯
• Miri.Memory.instDecidableEqPointerError.decEq Miri.Memory.PointerError.relativeProvenanceHasNoAbsoluteAddress Miri.Memory.PointerError.relativeProvenanceHasNoAbsoluteAddress = isTrue ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqPointerError : DecidableEq PointerError

Equations

• Miri.Memory.instDecidableEqPointerError = Miri.Memory.instDecidableEqPointerError.decEq

def Miri.Memory.instReprPointerError.repr : PointerError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprPointerError : Repr PointerError

Equations

• Miri.Memory.instReprPointerError = { reprPrec := Miri.Memory.instReprPointerError.repr }

structure Miri.Memory.PointerArithmetic : Type

Target-size operations from PointerArithmetic. Assertions and narrowing conversion failures remain explicit. No target triple is selected here.

• pointerSize : ABI.Size

def Miri.Memory.instDecidableEqPointerArithmetic.decEq (x✝ x✝¹ : PointerArithmetic) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqPointerArithmetic.decEq { pointerSize := a } { pointerSize := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqPointerArithmetic : DecidableEq PointerArithmetic

Equations

• Miri.Memory.instDecidableEqPointerArithmetic = Miri.Memory.instDecidableEqPointerArithmetic.decEq

@[instance_reducible]

instance Miri.Memory.instReprPointerArithmetic : Repr PointerArithmetic

Equations

• Miri.Memory.instReprPointerArithmetic = { reprPrec := Miri.Memory.instReprPointerArithmetic.repr }

def Miri.Memory.instReprPointerArithmetic.repr : PointerArithmetic → Nat → Std.Format

Equations

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

def Miri.Memory.PointerArithmetic.targetUsizeMax (cx : PointerArithmetic) : Except PointerError UInt64

Equations

• cx.targetUsizeMax = do let __do_lift ← Miri.Memory.PointerArithmetic.sizeResult✝ cx.pointerSize.unsignedIntMax Miri.Memory.PointerArithmetic.toUInt64Checked✝ __do_lift

def Miri.Memory.PointerArithmetic.truncateToTargetUsize (cx : PointerArithmetic) (value : UInt64) : Except PointerError UInt64

Equations

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

def Miri.Memory.PointerArithmetic.signExtendToTargetIsize (cx : PointerArithmetic) (value : UInt64) : Except PointerError Int64

Equations

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

def Miri.Memory.PointerArithmetic.targetIsizeMax (cx : PointerArithmetic) : Except PointerError Int64

Equations

• cx.targetIsizeMax = do let __do_lift ← Miri.Memory.PointerArithmetic.sizeResult✝ cx.pointerSize.signedIntMax Miri.Memory.PointerArithmetic.toInt64Checked✝ __do_lift

def Miri.Memory.PointerArithmetic.targetIsizeMin (cx : PointerArithmetic) : Except PointerError Int64

Equations

• cx.targetIsizeMin = do let __do_lift ← Miri.Memory.PointerArithmetic.sizeResult✝ cx.pointerSize.signedIntMin Miri.Memory.PointerArithmetic.toInt64Checked✝ __do_lift

def Miri.Memory.PointerArithmetic.maxSizeOfVal (cx : PointerArithmetic) : Except PointerError ABI.Size

Pinned PointerArithmetic::max_size_of_val, independent of the ABI object-size bound (which is smaller for 64-bit LLVM layouts).

Equations

• cx.maxSizeOfVal = do let maximum ← cx.targetIsizeMax pure (Miri.ABI.Size.ofBytes (UInt64.ofNat maximum.toInt.toNat))

def Miri.Memory.Pointer.new {Prov : Type u_1} (provenance : Prov) (offset : ABI.Size) : Pointer Prov

Equations

• Miri.Memory.Pointer.new provenance offset = { offset := offset, provenance := provenance }

def Miri.Memory.Pointer.intoRawParts {Prov : Type u_1} (ptr : Pointer Prov) : Prov × ABI.Size

Equations

• ptr.intoRawParts = (ptr.provenance, ptr.offset)

def Miri.Memory.Pointer.mapProvenance {Prov : Type u_1} (ptr : Pointer Prov) (f : Prov → Prov) : Pointer Prov

Equations

• ptr.mapProvenance f = { offset := ptr.offset, provenance := f ptr.provenance }

def Miri.Memory.Pointer.withOptionalProvenance {Prov : Type u_1} (ptr : Pointer Prov) : Pointer (Option Prov)

Equations

• ptr.withOptionalProvenance = { offset := ptr.offset, provenance := some ptr.provenance }

def Miri.Memory.Pointer.withoutProvenance {Prov : Type u_1} (addr : UInt64) : Pointer (Option Prov)

Equations

• Miri.Memory.Pointer.withoutProvenance addr = { offset := Miri.ABI.Size.ofBytes addr, provenance := none }

def Miri.Memory.Pointer.null {Prov : Type u_1} : Pointer (Option Prov)

Equations

• Miri.Memory.Pointer.null = Miri.Memory.Pointer.withoutProvenance 0

def Miri.Memory.Pointer.intoPointerOrAddr {Prov : Type u_1} (ptr : Pointer (Option Prov)) : Except ABI.Size (Pointer Prov)

Rust Result<Pointer<Prov>, Size>: an address without provenance goes through the error branch, not a fabricated allocation.

Equations

• ptr.intoPointerOrAddr = match ptr.provenance with | some prov => Except.ok (Miri.Memory.Pointer.new prov ptr.offset) | none => Except.error ptr.offset

def Miri.Memory.Pointer.addr {Prov : Type u_1} [PointerProvenance Prov] (ptr : Pointer (Option Prov)) : Except PointerError ABI.Size

Source addr assertion depends on the provenance representation.

Equations

• ptr.addr = if Miri.Memory.PointerProvenance.offsetIsAddr Prov = true then Except.ok ptr.offset else Except.error Miri.Memory.PointerError.relativeProvenanceHasNoAbsoluteAddress

def Miri.Memory.Pointer.wrappingOffset {Prov : Type} (ptr : Pointer Prov) (offset : ABI.Size) (cx : PointerArithmetic) : Except PointerError (Pointer Prov)

Source wraps u64 addition before truncating to the target pointer size.

Equations

• ptr.wrappingOffset offset cx = do let result ← cx.truncateToTargetUsize (ptr.offset.bytes + offset.bytes) pure { offset := Miri.ABI.Size.ofBytes result, provenance := ptr.provenance }

def Miri.Memory.Pointer.wrappingSignedOffset {Prov : Type} (ptr : Pointer Prov) (offset : Int64) (cx : PointerArithmetic) : Except PointerError (Pointer Prov)

Equations

• ptr.wrappingSignedOffset offset cx = ptr.wrappingOffset (Miri.ABI.Size.ofBytes offset.toUInt64) cx

theorem Miri.Memory.Pointer.map_preserves_offset {Prov : Type u_1} (ptr : Pointer Prov) (f : Prov → Prov) : (ptr.mapProvenance f).offset = ptr.offset

theorem Miri.Memory.Pointer.no_provenance_is_address {Prov : Type u_1} (value : UInt64) : (withoutProvenance value).intoPointerOrAddr = Except.error (ABI.Size.ofBytes value)

theorem Miri.Memory.Pointer.wrappingOffset_preserves_provenance {Prov : Type} (ptr : Pointer Prov) (offset : ABI.Size) (cx : PointerArithmetic) (next : Pointer Prov) (h : ptr.wrappingOffset offset cx = Except.ok next) : next.provenance = ptr.provenance

@[reducible, inline]

abbrev Miri.Memory.MiriPointer : Type

Equations

• Miri.Memory.MiriPointer = Miri.Memory.Pointer (Option Miri.Memory.Provenance)

@[reducible, inline]

abbrev Miri.Memory.StrictPointer : Type

Equations

• Miri.Memory.StrictPointer = Miri.Memory.Pointer Miri.Memory.Provenance