Allocation and borrow identities from the pinned rustc/Miri sources. AllocId is a nonzero u64 (mir/interpret/mod.rs); BorTag is a distinct nonzero u64 (borrow_tracker/mod.rs). No address or validity is inferred from either identity. Allocation liveness belongs to the allocation state.

structure Miri.Memory.AllocId : Type

• value : UInt64
• nonzero : self.value ≠ 0

@[instance_reducible]

instance Miri.Memory.instDecidableEqAllocId : DecidableEq AllocId

Equations

• Miri.Memory.instDecidableEqAllocId = Miri.Memory.instDecidableEqAllocId.decEq

def Miri.Memory.instDecidableEqAllocId.decEq (x✝ x✝¹ : AllocId) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Memory.instReprAllocId.repr : AllocId → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprAllocId : Repr AllocId

Equations

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

def Miri.Memory.AllocId.ofUInt64 (value : UInt64) : Option AllocId

Equations

• Miri.Memory.AllocId.ofUInt64 value = if h : value = 0 then none else some { value := value, nonzero := h }

theorem Miri.Memory.AllocId.zero_is_rejected : ofUInt64 0 = none

theorem Miri.Memory.AllocId.constructed_value {value : UInt64} {id : AllocId} (h : ofUInt64 value = some id) : id.value = value

structure Miri.Memory.BorTag : Type

• value : UInt64
• nonzero : self.value ≠ 0

def Miri.Memory.instDecidableEqBorTag.decEq (x✝ x✝¹ : BorTag) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instDecidableEqBorTag : DecidableEq BorTag

Equations

• Miri.Memory.instDecidableEqBorTag = Miri.Memory.instDecidableEqBorTag.decEq

def Miri.Memory.instReprBorTag.repr : BorTag → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprBorTag : Repr BorTag

Equations

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

def Miri.Memory.BorTag.ofUInt64 (value : UInt64) : Option BorTag

Equations

• Miri.Memory.BorTag.ofUInt64 value = if h : value = 0 then none else some { value := value, nonzero := h }

def Miri.Memory.BorTag.one : BorTag

Equations

• Miri.Memory.BorTag.one = { value := 1, nonzero := Miri.Memory.BorTag.one._proof_1 }

@[instance_reducible]

instance Miri.Memory.BorTag.instInhabited : Inhabited BorTag

Equations

• Miri.Memory.BorTag.instInhabited = { default := Miri.Memory.BorTag.one }

def Miri.Memory.BorTag.succ (tag : BorTag) : Option BorTag

Source NonZero<u64>::checked_add(1) preserves overflow as None.

Equations

• tag.succ = if tag.value = 18446744073709551615 then none else Miri.Memory.BorTag.ofUInt64 (tag.value + 1)

theorem Miri.Memory.BorTag.zero_is_rejected : ofUInt64 0 = none

theorem Miri.Memory.BorTag.max_has_no_successor {tag : BorTag} (h : tag.value = 18446744073709551615) : tag.succ = none

inductive Miri.Memory.Provenance : Type

Pinned Miri machine::Provenance. Wildcard is distinct from no provenance.

• concrete (allocId : AllocId) (tag : BorTag) : Provenance
• wildcard : Provenance

@[instance_reducible]

instance Miri.Memory.instDecidableEqProvenance : DecidableEq Provenance

Equations

• Miri.Memory.instDecidableEqProvenance = Miri.Memory.instDecidableEqProvenance.decEq

def Miri.Memory.instDecidableEqProvenance.decEq (x✝ x✝¹ : Provenance) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqProvenance.decEq (Miri.Memory.Provenance.concrete allocId tag) Miri.Memory.Provenance.wildcard = isFalse ⋯
• Miri.Memory.instDecidableEqProvenance.decEq Miri.Memory.Provenance.wildcard (Miri.Memory.Provenance.concrete allocId tag) = isFalse ⋯
• Miri.Memory.instDecidableEqProvenance.decEq Miri.Memory.Provenance.wildcard Miri.Memory.Provenance.wildcard = isTrue ⋯

def Miri.Memory.instReprProvenance.repr : Provenance → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprProvenance : Repr Provenance

Equations

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

def Miri.Memory.Provenance.offsetIsAddr : Bool

Equations

• Miri.Memory.Provenance.offsetIsAddr = true

def Miri.Memory.Provenance.wildcardProvenance : Option Provenance

Equations

• Miri.Memory.Provenance.wildcardProvenance = some Miri.Memory.Provenance.wildcard

def Miri.Memory.Provenance.getAllocId : Provenance → Option AllocId

Equations

• (Miri.Memory.Provenance.concrete a a_1).getAllocId = some a
• Miri.Memory.Provenance.wildcard.getAllocId = none

theorem Miri.Memory.Provenance.wildcard_has_no_fixed_allocation : wildcard.getAllocId = none

theorem Miri.Memory.Provenance.concrete_retains_allocation (id : AllocId) (tag : BorTag) : (concrete id tag).getAllocId = some id

class Miri.Memory.PointerProvenance (Prov : Type u) : Type u

The semantic members of rustc's interpret::Provenance trait. The formatting callback is diagnostic-only. Implementations are fixed by the library for each concrete engine provenance type.

• offsetIsAddr : Bool
• wildcard : Option Prov
• getAllocId : Prov → Option AllocId

@[instance_reducible]

instance Miri.Memory.instPointerProvenanceProvenance : PointerProvenance Provenance

Equations

• Miri.Memory.instPointerProvenanceProvenance = { offsetIsAddr := true, wildcard := some Miri.Memory.Provenance.wildcard, getAllocId := Miri.Memory.Provenance.getAllocId }

@[instance_reducible]

instance Miri.Memory.instPointerProvenanceAllocId : PointerProvenance AllocId

Equations

• Miri.Memory.instPointerProvenanceAllocId = { offsetIsAddr := false, wildcard := none, getAllocId := some }

inductive Miri.Memory.ProvenanceExtra : Type

The extra information from Miri's machine::ProvenanceExtra.

• concrete (tag : BorTag) : ProvenanceExtra
• wildcard : ProvenanceExtra

@[instance_reducible]

instance Miri.Memory.instDecidableEqProvenanceExtra : DecidableEq ProvenanceExtra

Equations

• Miri.Memory.instDecidableEqProvenanceExtra = Miri.Memory.instDecidableEqProvenanceExtra.decEq

def Miri.Memory.instDecidableEqProvenanceExtra.decEq (x✝ x✝¹ : ProvenanceExtra) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqProvenanceExtra.decEq (Miri.Memory.ProvenanceExtra.concrete a) (Miri.Memory.ProvenanceExtra.concrete b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqProvenanceExtra.decEq (Miri.Memory.ProvenanceExtra.concrete tag) Miri.Memory.ProvenanceExtra.wildcard = isFalse ⋯
• Miri.Memory.instDecidableEqProvenanceExtra.decEq Miri.Memory.ProvenanceExtra.wildcard (Miri.Memory.ProvenanceExtra.concrete tag) = isFalse ⋯
• Miri.Memory.instDecidableEqProvenanceExtra.decEq Miri.Memory.ProvenanceExtra.wildcard Miri.Memory.ProvenanceExtra.wildcard = isTrue ⋯

@[instance_reducible]

instance Miri.Memory.instReprProvenanceExtra : Repr ProvenanceExtra

Equations

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

def Miri.Memory.instReprProvenanceExtra.repr : ProvenanceExtra → Nat → Std.Format

Equations

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

def Miri.Memory.ProvenanceExtra.andThen {α : Type u_1} (extra : ProvenanceExtra) (f : BorTag → Option α) : Option α

Equations

• (Miri.Memory.ProvenanceExtra.concrete a).andThen f = f a
• Miri.Memory.ProvenanceExtra.wildcard.andThen f = none