Source provenance_gc.rs, machine.rs::VisitProvenance, thread.rs frame visitors. This collects provenance as ghost data: it performs no Rust memory read, initialization check, race access or retag. Missing user-state visitors remain required operations; arbitrary empty roots are not a closed interpreter.

structure Miri.Interpreter.ProvenanceGC.Roots : Type

• allocations : Array Memory.AllocId
• tags : Array Memory.BorTag

def Miri.Interpreter.ProvenanceGC.Roots.add (roots : Roots) (id : Option Memory.AllocId) (tag : Option Memory.BorTag) : Roots

Equations

• One or more equations did not get rendered due to their size.
• roots.add (some id_2) none = { allocations := if roots.allocations.contains id_2 = true then roots.allocations else roots.allocations.push id_2, tags := roots.tags }
• roots.add none (some tag_2) = { allocations := roots.allocations, tags := if roots.tags.contains tag_2 = true then roots.tags else roots.tags.push tag_2 }
• roots.add none none = { allocations := roots.allocations, tags := roots.tags }

def Miri.Interpreter.ProvenanceGC.Roots.provenance (roots : Roots) : Memory.Provenance → Roots

Equations

• roots.provenance (Miri.Memory.Provenance.concrete id tag) = roots.add (some id) (some tag)
• roots.provenance Miri.Memory.Provenance.wildcard = roots

def Miri.Interpreter.ProvenanceGC.Roots.pointer (roots : Roots) (pointer : Memory.Pointer (Option Memory.Provenance)) : Roots

Equations

• roots.pointer pointer = match pointer.provenance with | none => roots | some value => roots.provenance value

def Miri.Interpreter.ProvenanceGC.Roots.strictPointer (roots : Roots) (pointer : Memory.Pointer Memory.Provenance) : Roots

Equations

• roots.strictPointer pointer = roots.provenance pointer.provenance

def Miri.Interpreter.ProvenanceGC.Roots.scalar (roots : Roots) (value : Memory.Scalar Memory.Provenance) : Except StepError Roots

Equations

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

def Miri.Interpreter.ProvenanceGC.Roots.immediate (roots : Roots) : Immediate Memory.Provenance → Except StepError Roots

Equations

• roots.immediate (Miri.Interpreter.Immediate.scalar value) = roots.scalar value
• roots.immediate (Miri.Interpreter.Immediate.scalarPair first second) = do let __do_lift ← roots.scalar first __do_lift.scalar second
• roots.immediate Miri.Interpreter.Immediate.uninit = Except.ok roots

def Miri.Interpreter.ProvenanceGC.Roots.metadata (roots : Roots) : MemPlaceMeta Memory.Provenance → Except StepError Roots

Equations

• roots.metadata (Miri.Interpreter.MemPlaceMeta.metadata value) = roots.scalar value
• roots.metadata Miri.Interpreter.MemPlaceMeta.none = Except.ok roots

def Miri.Interpreter.ProvenanceGC.Roots.memPlace (roots : Roots) (place : MemPlace Memory.Provenance) : Except StepError Roots

Equations

• roots.memPlace place = (roots.pointer place.ptr).metadata place.metadata

def Miri.Interpreter.ProvenanceGC.Roots.operand (roots : Roots) : Operand Memory.Provenance → Except StepError Roots

Equations

• roots.operand (Miri.Interpreter.Operand.immediate value) = roots.immediate value
• roots.operand (Miri.Interpreter.Operand.indirect place) = roots.memPlace place

def Miri.Interpreter.ProvenanceGC.Roots.runtimePlace (roots : Roots) (place : RuntimeStackPlace Memory.Provenance) : Except StepError Roots

Equations

• roots.runtimePlace (Miri.Interpreter.RuntimeStackPlace.memory value) = roots.memPlace value.mplace
• roots.runtimePlace (Miri.Interpreter.RuntimeStackPlace.frameLocal frameIndex localId offset layout localsIdentity) = Except.ok roots

def Miri.Interpreter.ProvenanceGC.Roots.frame (roots : Roots) (frame : Frame Memory.Provenance LocalLayout MachineHooks.FrameExtra) : Except StepError Roots

Equations

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

def Miri.Interpreter.ProvenanceGC.Roots.stack (roots : Roots) (stack : ThreadStacks.ActualStack) : Except StepError Roots

Equations

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

def Miri.Interpreter.ProvenanceGC.Roots.allocation (roots : Roots) (borrowTracking : Bool) (allocation : Memory.Allocation Memory.Provenance TreeBorrows.BorrowTree) : Roots

Allocation bytes include partial pointer fragments. Tree roots/exposed tags are visited even for allocations with no reachable pointer; allocation IDs of live entries themselves are deliberately not added to the collected set.

Equations

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

def Miri.Interpreter.ProvenanceGC.Roots.storeBuffer (roots : Roots) (allocation : Concurrency.StoreBufferAlloc (Memory.Scalar Memory.Provenance)) : Except StepError Roots

Equations

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

def Miri.Interpreter.ProvenanceGC.Roots.unwindPayloads (roots : Roots) (manager : Concurrency.ThreadManager) (store : Unwind.PayloadStore) : Except StepError Roots

The arena is only a representation of the actual per-thread payload vectors: visit exactly referenced entries, and reject missing/ambiguous tokens. Unused arena slots are not roots.

Equations

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

structure Miri.Interpreter.ProvenanceGC.Hooks (K User : Type) : Type

Concrete visitors for user-embedded state must cover inactive stacks, unwind payloads, last-error storage, thread-local allocations, TLS, env/dirs/fds, weak store buffers, entry pointers and extern statics. Do not use a callback that ignores a field merely because its source module has not been ported. Machine alloc-address/TB/VClock globals intentionally carry no GC roots.

• visitUser : MachineHooks.State K User → Roots → Except StepError Roots
• addresses : User → Memory.AllocAddresses.GlobalAddressState
• setAddresses : Memory.AllocAddresses.GlobalAddressState → User → User
• symbolicAlignment : User → Array (Memory.AllocId × ABI.Size × ABI.Align)
• setSymbolicAlignment : Array (Memory.AllocId × ABI.Size × ABI.Align) → User → User

def Miri.Interpreter.ProvenanceGC.run {K User : Type} [DecidableEq K] (h : Hooks K User) : MachineHooks.M K User Unit

Full source collection and pruning order. All live bytes are scanned, including leaked allocations. Global compiler allocations count as live via MemoryState.isAllocLive but are not prematurely materialized by collection.

Equations

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