Source whole-machine provenance visitor composition. Views project actual runtime records, not caller-chosen root lists. No machine read, retag, callback, host operation or descriptor drop is executed while collecting roots.

structure Miri.Interpreter.MachineGCRoots.EntryPointers : Type

Exact machine.rs saved pointer fields. Their absent state is represented by None only when the corresponding source machine field is absent.

• mainReturn : Option (MPlaceTy Memory.Provenance)
• argc : Option (Memory.Pointer Memory.Provenance)
• argv : Option (Memory.Pointer Memory.Provenance)
• commandLine : Option (Memory.Pointer Memory.Provenance)

structure Miri.Interpreter.MachineGCRoots.Views (User Os ReadDir Payload Handle Directory Other : Type) : Type

Required actual storage projections. There is intentionally no generic "remaining roots" callback or empty default for unported runtime fields. FDs are included to make their source-empty visitor an explicit operation.

• stacks : User → ThreadStacks.Registry
• tls : User → ThreadTlsMachine.Data
• errnoPlaces : User → Array (Memory.AllocId × MPlaceTy Memory.Provenance)
• unwindPayloads : User → Unwind.PayloadStore
• extras : User → MemoryExtras.Registry Payload
• environment : User → EnvVars.State (Option Memory.Provenance) Os
• directories : User → UnixDirectories.Table ReadDir
• descriptors : User → Files.Table (Files.Description Handle Directory Other)
• ownership : User → FileOwnership.Registry (Files.Description Handle Directory Other)
• entry : User → EntryPointers
• externStatics : User → ExternStatic.State

def Miri.Interpreter.MachineGCRoots.visitFiles {H D O : Type} (roots : ProvenanceGC.Roots) (_table : Files.Table (Files.Description H D O)) (_ownership : FileOwnership.Registry (Files.Description H D O)) : ProvenanceGC.Roots

files.rs:101–105,584–588 explicitly assumes all source FileDescription instances carry no provenance. Numeric FD identities and host/peer handles do not become allocation roots. This does not license arbitrary new extensions with provenance-bearing description fields to omit their own source visitor.

Equations

• Miri.Interpreter.MachineGCRoots.visitFiles roots _table _ownership = roots

def Miri.Interpreter.MachineGCRoots.visitDirectories {R : Type} (roots : ProvenanceGC.Roots) (table : UnixDirectories.Table R) : ProvenanceGC.Roots

unix/fs.rs:228–236 visits stream.entry only, not the host ReadDir, FD number/identity, next-id counter, or special-entry strings.

Equations

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

def Miri.Interpreter.MachineGCRoots.visitErrno (roots : ProvenanceGC.Roots) (manager : Concurrency.ThreadManager) (storage : Array (Memory.AllocId × MPlaceTy Memory.Provenance)) : Except StepError ProvenanceGC.Roots

Thread.visit visits last_error even for terminated retained records. Unused side-table entries are not source-owned errno places and are not roots.

Equations

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

def Miri.Interpreter.MachineGCRoots.visit {User Os R Payload H D O K : Type} (views : Views User Os R Payload H D O) (state : MachineHooks.State K User) (initial : ProvenanceGC.Roots) : Except StepError ProvenanceGC.Roots

Full user portion of machine.rs:1093–1110, plus actual inactive-thread stacks and allocation-local weak-buffer visitors. The active stack and live allocation bytes/tree tags are visited by ProvenanceGC.run itself.

Equations

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

def Miri.Interpreter.MachineGCRoots.hooks {User Os R Payload H D O AddressPayload K : Type} (views : Views User Os R Payload H D O) (addresses : FunctionPointers.AddressLens User AddressPayload) : ProvenanceGC.Hooks K User

The lawful address lens points at the SAME canonical address and symbolic alignment maps used by function pointers, casts and alignment checks. GC never creates a parallel cache or reconstructs addresses from allocation identity.

Equations

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

def Miri.Interpreter.MachineGCRoots.run {K User Os R Payload H D O AddressPayload : Type} [DecidableEq K] (views : Views User Os R Payload H D O) (addresses : FunctionPointers.AddressLens User AddressPayload) : MachineHooks.M K User Unit

Actual source collection and TB/dead/address metadata pruning in one machine action. Root extraction has no memory-access hooks or initialization checks, and source error prefixes are retained by ProvenanceGC.run.

Equations

• Miri.Interpreter.MachineGCRoots.run views addresses = Miri.Interpreter.ProvenanceGC.run (Miri.Interpreter.MachineGCRoots.hooks views addresses)

def Miri.Interpreter.MachineGCRoots.bindMiri {User Os R Payload H D O AddressPayload K Dest MD B I HostPath : Type} (views : Views User Os R Payload H D O) (addresses : FunctionPointers.AddressLens User AddressPayload) (base : MiriShims.Hooks Memory.Provenance (MachineHooks.State K User) Dest MD B I HostPath) [DecidableEq K] : MiriShims.Hooks Memory.Provenance (MachineHooks.State K User) Dest MD B I HostPath

Bind the actual miri_provenance_gc foreign arm to this whole-machine walk.

Equations

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

structure Miri.Interpreter.MachineGCRoots.Storage (Os R Payload H D O Aff : Type) : Type

Concrete root-bearing source storage. Runtime state adapters can directly use these fields rather than maintaining GC-only shadow copies. Callbacks are real thread-runtime state, deliberately excluded by the pinned thread visitor.

• threads : ThreadMachine.Runtime Aff
• tls : ThreadTlsMachine.Data
• errnoPlaces : Array (Memory.AllocId × MPlaceTy Memory.Provenance)
• unwindPayloads : Unwind.PayloadStore
• extras : MemoryExtras.Registry Payload
• environment : EnvVars.State (Option Memory.Provenance) Os
• directories : UnixDirectories.Table R
• descriptors : Files.Table (Files.Description H D O)
• ownership : FileOwnership.Registry (Files.Description H D O)
• entry : EntryPointers
• externStatics : ExternStatic.State

@[reducible, inline]

abbrev Miri.Interpreter.MachineGCRoots.StoredUser (Os R Payload H D O Aff : Type) : Type

Equations

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

def Miri.Interpreter.MachineGCRoots.storedViews {Os R Payload H D O Aff : Type} : Views (StoredUser Os R Payload H D O Aff) Os R Payload H D O

The active stack is StepState.stack and inactive stacks are the actual ThreadStacks registry. Address state exists once, in the nested PointerMachine user. All other projections read the source runtime fields above directly.

Equations

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

def Miri.Interpreter.MachineGCRoots.storedAddresses {Os R Payload H D O Aff : Type} : FunctionPointers.AddressLens (StoredUser Os R Payload H D O Aff) (Storage Os R Payload H D O Aff)

Equations

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

def Miri.Interpreter.MachineGCRoots.runStored {K Os R Payload H D O Aff : Type} [DecidableEq K] : MachineHooks.M K (StoredUser Os R Payload H D O Aff) Unit

Entire source GC operation for this concrete runtime composition.

Equations

• Miri.Interpreter.MachineGCRoots.runStored = Miri.Interpreter.MachineGCRoots.run Miri.Interpreter.MachineGCRoots.storedViews Miri.Interpreter.MachineGCRoots.storedAddresses

def Miri.Interpreter.MachineGCRoots.bindStoredMiri {K Os R Payload H D O Aff Dest MD B I HostPath : Type} [DecidableEq K] (base : MiriShims.Hooks Memory.Provenance (MachineHooks.State K (StoredUser Os R Payload H D O Aff)) Dest MD B I HostPath) : MiriShims.Hooks Memory.Provenance (MachineHooks.State K (StoredUser Os R Payload H D O Aff)) Dest MD B I HostPath

Equations

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