CTFE's packed provenance from pinned rustc mir/interpret/pointer.rs. The representation is decoded into the same allocation ID and two flags; the constructor enforces the source's 62-bit ID and immutable⇒shared invariant. packed reconstructs the original u64, including both high bits. This is separate from Miri's concrete/wildcard provenance, not a substitute for it.

inductive Miri.Memory.CtfeProvenanceError : Type

• allocationIdUsesFlagBits : CtfeProvenanceError

@[instance_reducible]

instance Miri.Memory.instDecidableEqCtfeProvenanceError : DecidableEq CtfeProvenanceError

Equations

• Miri.Memory.instDecidableEqCtfeProvenanceError x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instReprCtfeProvenanceError : Repr CtfeProvenanceError

Equations

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

def Miri.Memory.instReprCtfeProvenanceError.repr : CtfeProvenanceError → Nat → Std.Format

Equations

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

structure Miri.Memory.CtfeProvenance : Type

• allocId : AllocId
• allocIdFits : self.allocId.value < 4611686018427387904
• immutable : Bool
• sharedRef : Bool
• immutableImpliesShared : self.immutable = true → self.sharedRef = true

def Miri.Memory.instDecidableEqCtfeProvenance.decEq (x✝ x✝¹ : CtfeProvenance) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instDecidableEqCtfeProvenance : DecidableEq CtfeProvenance

Equations

• Miri.Memory.instDecidableEqCtfeProvenance = Miri.Memory.instDecidableEqCtfeProvenance.decEq

@[instance_reducible]

instance Miri.Memory.instReprCtfeProvenance : Repr CtfeProvenance

Equations

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

def Miri.Memory.instReprCtfeProvenance.repr : CtfeProvenance → Nat → Std.Format

Equations

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

def Miri.Memory.CtfeProvenance.fromAllocId (id : AllocId) : Except CtfeProvenanceError CtfeProvenance

Equations

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

def Miri.Memory.CtfeProvenance.asImmutable (prov : CtfeProvenance) : CtfeProvenance

Equations

• prov.asImmutable = { allocId := prov.allocId, allocIdFits := ⋯, immutable := true, sharedRef := true, immutableImpliesShared := Miri.Memory.CtfeProvenance.asImmutable._proof_1 }

def Miri.Memory.CtfeProvenance.asSharedRef (prov : CtfeProvenance) : CtfeProvenance

Equations

• prov.asSharedRef = { allocId := prov.allocId, allocIdFits := ⋯, immutable := prov.immutable, sharedRef := true, immutableImpliesShared := ⋯ }

def Miri.Memory.CtfeProvenance.intoParts (prov : CtfeProvenance) : AllocId × Bool × Bool

Equations

• prov.intoParts = (prov.allocId, prov.immutable, prov.sharedRef)

def Miri.Memory.CtfeProvenance.fromParts (parts : AllocId × Bool × Bool) : Except CtfeProvenanceError CtfeProvenance

Equations

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

def Miri.Memory.CtfeProvenance.packed (prov : CtfeProvenance) : UInt64

The exact two high-bit masks from the source representation.

Equations

• prov.packed = (prov.allocId.value ||| if prov.immutable = true then 9223372036854775808 else 0) ||| if prov.sharedRef = true then 4611686018427387904 else 0

theorem Miri.Memory.CtfeProvenance.packed_allocation_bits (prov : CtfeProvenance) : prov.packed &&& 4611686018427387903 = prov.allocId.value

Decoding the allocation bits recovers exactly the stored identity. This uses kernel-checked bitwise lemmas; no native-decide certificate axiom.

theorem Miri.Memory.CtfeProvenance.packed_immutable_bit (prov : CtfeProvenance) : prov.packed &&& 9223372036854775808 ≠ 0 ↔ prov.immutable = true

theorem Miri.Memory.CtfeProvenance.packed_shared_bit (prov : CtfeProvenance) : prov.packed &&& 4611686018427387904 ≠ 0 ↔ prov.sharedRef = true

theorem Miri.Memory.CtfeProvenance.packed_nonzero (prov : CtfeProvenance) : prov.packed ≠ 0

theorem Miri.Memory.CtfeProvenance.immutable_is_shared (prov : CtfeProvenance) (h : prov.immutable = true) : prov.sharedRef = true

theorem Miri.Memory.CtfeProvenance.asImmutable_sets_both (prov : CtfeProvenance) : prov.asImmutable.immutable = true ∧ prov.asImmutable.sharedRef = true

theorem Miri.Memory.CtfeProvenance.asImmutable_retains_allocation (prov : CtfeProvenance) : prov.asImmutable.allocId = prov.allocId

theorem Miri.Memory.CtfeProvenance.asSharedRef_retains_allocation (prov : CtfeProvenance) : prov.asSharedRef.allocId = prov.allocId

@[instance_reducible]

instance Miri.Memory.instPointerProvenanceCtfeProvenance : PointerProvenance CtfeProvenance

Equations

• Miri.Memory.instPointerProvenanceCtfeProvenance = { offsetIsAddr := false, wildcard := none, getAllocId := fun (prov : Miri.Memory.CtfeProvenance) => some prov.allocId }

def Miri.Memory.Pointer.provAndRelativeOffset (ptr : Pointer CtfeProvenance) : CtfeProvenance × ABI.Size

Equations

• ptr.provAndRelativeOffset = ptr.intoRawParts

def Miri.Memory.Pointer.fromCtfeProvenance (prov : CtfeProvenance) : Pointer CtfeProvenance

Equations

• Miri.Memory.Pointer.fromCtfeProvenance prov = Miri.Memory.Pointer.new prov Miri.ABI.Size.ZERO

def Miri.Memory.Pointer.fromAllocId (id : AllocId) : Except CtfeProvenanceError (Pointer CtfeProvenance)

Equations

• Miri.Memory.Pointer.fromAllocId id = do let __do_lift ← Miri.Memory.CtfeProvenance.fromAllocId id pure (Miri.Memory.Pointer.fromCtfeProvenance __do_lift)