The pointer-sized and byte-fragment representation from rustc's pinned allocation/provenance_map.rs. Read operations preserve the distinction between no provenance, wildcard provenance, and a partial CTFE pointer error. The checked construction below enforces sorted unique map keys. It does not replace the allocation's bounds/initialization/aliasing checks.

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

• idx : UInt8
• prov : Prov
• bytes : Vector UInt8 8

@[instance_reducible]

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

Equations

• Miri.Memory.instDecidableEqPointerFrag = Miri.Memory.instDecidableEqPointerFrag.decEq

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

inductive Miri.Memory.ProvenanceMapError : Type

• memory (reason : MemoryError) : ProvenanceMapError
• pointerSizeZero : ProvenanceMapError
• unsortedOrDuplicateKeys : ProvenanceMapError
• readPartialPointer (offset : ABI.Size) : ProvenanceMapError
• missingWildcard : ProvenanceMapError
• pointerSizedProvenanceAtByte (offset : ABI.Size) : ProvenanceMapError
• insertOverlapsExistingProvenance : ProvenanceMapError
• pointerSizeExceedsFragmentStorage (bytes : UInt64) : ProvenanceMapError
• fragmentSliceOutOfBounds (start size : ABI.Size) (available : Nat) : ProvenanceMapError
• copyEntryCountOverflow : ProvenanceMapError

@[instance_reducible]

instance Miri.Memory.instDecidableEqProvenanceMapError : DecidableEq ProvenanceMapError

Equations

• Miri.Memory.instDecidableEqProvenanceMapError = Miri.Memory.instDecidableEqProvenanceMapError.decEq

def Miri.Memory.instDecidableEqProvenanceMapError.decEq (x✝ x✝¹ : ProvenanceMapError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprProvenanceMapError : Repr ProvenanceMapError

Equations

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

def Miri.Memory.instReprProvenanceMapError.repr : ProvenanceMapError → Nat → Std.Format

Equations

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

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

• ptrs : Array (ABI.Size × Prov)
• byteFragments : Option (Array (ABI.Size × PointerFrag Prov))

@[instance_reducible]

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

Equations

• Miri.Memory.instDecidableEqProvenanceMap = Miri.Memory.instDecidableEqProvenanceMap.decEq

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

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

• ptrs : Array (ABI.Size × Prov)
• byteFragments : Array (ABI.Size × PointerFrag Prov)

@[instance_reducible]

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

Equations

• Miri.Memory.instDecidableEqProvenanceCopy = Miri.Memory.instDecidableEqProvenanceCopy.decEq

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

def Miri.Memory.ProvenanceMap.new {Prov : Type u_1} : ProvenanceMap Prov

Equations

• Miri.Memory.ProvenanceMap.new = { ptrs := #[], byteFragments := none }

def Miri.Memory.ProvenanceMap.fromPresortedPtrs {Prov : Type u_1} (values : Array (ABI.Size × Prov)) : Except ProvenanceMapError (ProvenanceMap Prov)

The source requires sorted, duplicate-free keys at this entry point.

Equations

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

def Miri.Memory.ProvenanceMap.fromParts {Prov : Type u_1} (ptrs : Array (ABI.Size × Prov)) (fragments : Option (Array (ABI.Size × PointerFrag Prov))) : Except ProvenanceMapError (ProvenanceMap Prov)

A fragment-state decoder with the same sorted-map key invariants. It is not a replacement for source prepare_copy/apply_copy/clear operations.

Equations

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

def Miri.Memory.ProvenanceMap.getPtr {Prov : Type u_1} (self : ProvenanceMap Prov) (offset : ABI.Size) : Option Prov

Equations

• self.getPtr offset = Option.map Prod.snd (Array.find? (fun (entry : Miri.ABI.Size × Prov) => entry.fst.bytes == offset.bytes) self.ptrs)

def Miri.Memory.ProvenanceMap.rangePtrs {Prov : Type} (self : ProvenanceMap Prov) (range : AllocRange) (pointerSize : ABI.Size) : Except ProvenanceMapError (Array (ABI.Size × Prov))

Equations

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

def Miri.Memory.ProvenanceMap.rangeBytes {Prov : Type} (self : ProvenanceMap Prov) (range : AllocRange) : Except ProvenanceMapError (Array (ABI.Size × PointerFrag Prov))

Equations

• self.rangeBytes range = do let finish ← Miri.Memory.ProvenanceMap.rangeEnd✝ range pure (Miri.Memory.ProvenanceMap.rangeEntries✝ (self.byteFragments.getD #[]) range.start finish)

def Miri.Memory.ProvenanceMap.rangeEmpty {Prov : Type} (self : ProvenanceMap Prov) (range : AllocRange) (pointerSize : ABI.Size) : Except ProvenanceMapError Bool

Equations

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

def Miri.Memory.ProvenanceMap.getByte {Prov : Type} (self : ProvenanceMap Prov) (offset pointerSize : ABI.Size) : Except ProvenanceMapError (Option (PointerFrag Prov))

Equations

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

def Miri.Memory.ProvenanceMap.getRange {Prov : Type} (self : ProvenanceMap Prov) (range : AllocRange) (pointerSize : ABI.Size) : Except ProvenanceMapError (Array (AllocRange × Prov))

Source get_range yields whole pointer entries first, then byte entries.

Equations

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

def Miri.Memory.ProvenanceMap.provenances {Prov : Type u_1} (self : ProvenanceMap Prov) : Array Prov

Equations

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

def Miri.Memory.ProvenanceMap.readPtr {Prov : Type} [DecidableEq Prov] [PointerProvenance Prov] (self : ProvenanceMap Prov) (offset pointerSize : ABI.Size) : Except ProvenanceMapError (Option Prov)

Equations

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

theorem Miri.Memory.ProvenanceMap.empty_has_no_provenance {Prov : Type u_1} : new.provenances = #[]

theorem Miri.Memory.ProvenanceMap.read_exact_pointer {Prov : Type} [DecidableEq Prov] [PointerProvenance Prov] (self : ProvenanceMap Prov) (offset pointerSize : ABI.Size) (prov : Prov) (h : self.getPtr offset = some prov) : self.readPtr offset pointerSize = Except.ok (some prov)

Mutating source operations keep the updated state even on assertion failure, using the standard library's EStateM result representation.

@[reducible, inline]

abbrev Miri.Memory.ProvenanceMap.Mutation (Prov α : Type) : Type

Equations

• Miri.Memory.ProvenanceMap.Mutation Prov α = EStateM Miri.Memory.ProvenanceMapError (Miri.Memory.ProvenanceMap Prov) α

def Miri.Memory.ProvenanceMap.insertPtr {Prov : Type} (offset : ABI.Size) (prov : Prov) (pointerSize : ABI.Size) : Mutation Prov Unit

Equations

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

def Miri.Memory.ProvenanceMap.clear {Prov : Type} (range : AllocRange) (data : Array UInt8) (pointerSize : ABI.Size) : Mutation Prov Unit

Equations

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

def Miri.Memory.ProvenanceMap.writeWildcards {Prov : Type} [PointerProvenance Prov] (range : AllocRange) (data : Array UInt8) (pointerSize : ABI.Size) : Mutation Prov Unit

Equations

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

def Miri.Memory.ProvenanceMap.mergeBytes {Prov : Type} [DecidableEq Prov] (pointerSize : ABI.Size) : Mutation Prov Bool

Equations

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

def Miri.Memory.ProvenanceMap.prepareCopy {Prov : Type} (self : ProvenanceMap Prov) (range : AllocRange) (data : Array UInt8) (pointerSize : ABI.Size) : Except ProvenanceMapError (ProvenanceCopy Prov)

Equations

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

def Miri.Memory.ProvenanceMap.applyCopy {Prov : Type} (copy : ProvenanceCopy Prov) (range : AllocRange) (repeatCount : UInt64) : Mutation Prov Unit

Source apply_copy requires the affected range to have been cleared. The map insertions retain the source's replacement behavior at existing keys.

Equations

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

theorem Miri.Memory.ProvenanceMap.clear_new {P : Type} (range : AllocRange) (data : Array UInt8) (pointerSize finish : ABI.Size) (positive : pointerSize.bytes ≠ 0) (endEq : range.endExclusive = Except.ok finish) : clear range data pointerSize new = EStateM.Result.ok () new

theorem Miri.Memory.ProvenanceMap.insertPtr_new {P : Type} (offset pointerSize finish : ABI.Size) (provenance : P) (positive : pointerSize.bytes ≠ 0) (endEq : (allocRange offset pointerSize).endExclusive = Except.ok finish) : insertPtr offset provenance pointerSize new = EStateM.Result.ok () { ptrs := #[(offset, provenance)], byteFragments := none }

theorem Miri.Memory.ProvenanceMap.clear_singleton_before {P : Type} (range : AllocRange) (data : Array UInt8) (pointerSize finish : ABI.Size) (provenance : P) (positive : pointerSize.bytes ≠ 0) (before : pointerSize.bytes.toNat ≤ range.start.bytes.toNat) (endEq : range.endExclusive = Except.ok finish) : clear range data pointerSize { ptrs := #[(ABI.Size.ZERO, provenance)], byteFragments := none } = EStateM.Result.ok () { ptrs := #[(ABI.Size.ZERO, provenance)], byteFragments := none }

theorem Miri.Memory.ProvenanceMap.insertPtr_singleton_after {P : Type} (offset pointerSize finish : ABI.Size) (old newProvenance : P) (positive : pointerSize.bytes ≠ 0) (before : pointerSize.bytes.toNat ≤ offset.bytes.toNat) (endEq : (allocRange offset pointerSize).endExclusive = Except.ok finish) : ∃ (updated : ProvenanceMap P), insertPtr offset newProvenance pointerSize { ptrs := #[(ABI.Size.ZERO, old)], byteFragments := none } = EStateM.Result.ok () updated