From c4716ed46127fb9e5564049ed09aefbbc2fb450a Mon Sep 17 00:00:00 2001
From: Andreas Rumpf <rumpf_a@web.de>
Date: Mon, 20 Jul 2026 08:38:54 +0200
Subject: [PATCH] YRC: use a side-table for topology (#26022)

- Much better locking scheme
- Run concurrently with the mutators
- Thread local collections
- Tarjan's algorithm for cycle collection
---
 lib/system/seqs_v2.nim           |   59 +-
 lib/system/threadimpl.nim        |    4 +
 lib/system/yrc.nim               | 1472 +++++++++++++++++++++++-------
 lib/system/yrc_proof.lean        |  863 +++++++++++++-----
 lib/system/yrc_tarjan_proof.lean |  594 ++++++++++++
 tests/arc/torcbench.nim          |    2 +-
 6 files changed, 2410 insertions(+), 584 deletions(-)
 create mode 100644 lib/system/yrc_tarjan_proof.lean

diff --git a/lib/system/seqs_v2.nim b/lib/system/seqs_v2.nim
index 511bb87d82..fc4a7a7a3b 100644
--- a/lib/system/seqs_v2.nim
+++ b/lib/system/seqs_v2.nim
@@ -25,31 +25,55 @@ when defined(gcYrc):
       HasCollectorLock
       Collecting
 
-    AlignedRwLock = object
-      ## One RwLock per cache line. {.align: 64.} causes the compiler to round
-      ## the struct size up to 64 bytes, so consecutive array elements never
-      ## share a cache line (sizeof(RwLock) = 56 on Linux x86_64 → 8 byte pad).
-      lock {.align: 64.}: RwLock
+    AlignedCounter = object
+      ## one counter per cache line to avoid false sharing between stripes
+      c {.align: 64.}: int
 
+  # Asymmetric two-class exclusion: seq structure mutations and collections
+  # exclude each other, but seq ops run concurrently with seq ops and
+  # collections run concurrently with collections. This replaces the old
+  # RwLock scheme (which allowed only ONE collector, serializing parallel
+  # collection) and also sidesteps POSIX's requirement that a rwlock be
+  # unlocked by its acquiring thread.
   var
-    gYrcLocks: array[NumLockStripes, AlignedRwLock]
+    gSeqActive: array[NumLockStripes, AlignedCounter]  # in-flight seq ops
+    gGcActive: int                                     # active collections
   var
     lockState {.threadvar.}: YrcLockState
 
   proc getYrcStripe(): int {.inline.} =
-    ## Map this thread to one of the NumLockStripes RwLock stripes.
+    ## Map this thread to one of the NumLockStripes counter stripes.
     ## getThreadId() is already cached thread-locally in threadids.nim.
     getThreadId() and (NumLockStripes - 1)
 
   proc acquireMutatorLock() {.compilerRtl, inl.} =
     if lockState == HasNoLock:
-      acquireRead gYrcLocks[getYrcStripe()].lock
+      let s = getYrcStripe()
+      while true:
+        # SEQ_CST inc-then-check pairs with the collector's SEQ_CST
+        # inc-then-drain (Dekker-style store/load ordering)
+        discard atomicFetchAdd(addr gSeqActive[s].c, 1, ATOMIC_SEQ_CST)
+        if atomicLoadN(addr gGcActive, ATOMIC_SEQ_CST) == 0: break
+        discard atomicFetchSub(addr gSeqActive[s].c, 1, ATOMIC_SEQ_CST)
+        while atomicLoadN(addr gGcActive, ATOMIC_ACQUIRE) != 0:
+          discard
       lockState = HasMutatorLock
 
   proc releaseMutatorLock() {.compilerRtl, inl.} =
     if lockState == HasMutatorLock:
       lockState = HasNoLock
-      releaseRead gYrcLocks[getYrcStripe()].lock
+      discard atomicFetchSub(addr gSeqActive[getYrcStripe()].c, 1, ATOMIC_SEQ_CST)
+
+  proc yrcGcFenceEnter() =
+    ## A collection announces itself and waits for in-flight seq structure
+    ## mutations to drain. Multiple collections may hold the fence at once.
+    discard atomicFetchAdd(addr gGcActive, 1, ATOMIC_SEQ_CST)
+    for s in 0 ..< NumLockStripes:
+      while atomicLoadN(addr gSeqActive[s].c, ATOMIC_SEQ_CST) > 0:
+        discard
+
+  proc yrcGcFenceExit() =
+    discard atomicFetchSub(addr gGcActive, 1, ATOMIC_SEQ_CST)
 
   template yrcMutatorLock*(t: typedesc; body: untyped) =
     {.noSideEffect.}:
@@ -71,23 +95,6 @@ when defined(gcYrc):
         {.noSideEffect.}:
           releaseMutatorLock()
 
-  template yrcCollectorLock(body: untyped) =
-    if lockState == HasMutatorLock: releaseMutatorLock()
-    let prevState = lockState
-    let hadToAcquire = prevState < HasCollectorLock
-    if hadToAcquire:
-      # Acquire all stripes in ascending order — the only thread ever holding
-      # multiple write locks is the collector, so there is no lock-order cycle.
-      for yrcI in 0..<NumLockStripes:
-        acquireWrite(gYrcLocks[yrcI].lock)
-      lockState = HasCollectorLock
-    try:
-      body
-    finally:
-      if hadToAcquire:
-        for yrcI in 0..<NumLockStripes:
-          releaseWrite(gYrcLocks[yrcI].lock)
-      lockState = prevState
 
 else:
   template yrcMutatorLock*(t: typedesc; body: untyped) =
diff --git a/lib/system/threadimpl.nim b/lib/system/threadimpl.nim
index dcd1b267a0..e35378db0e 100644
--- a/lib/system/threadimpl.nim
+++ b/lib/system/threadimpl.nim
@@ -27,6 +27,10 @@ else:
 template afterThreadRuns() =
   for i in countdown(nimThreadDestructionHandlers.len-1, 0):
     nimThreadDestructionHandlers[i]()
+  when declared(nimYrcThreadTeardown):
+    # YRC: spill this thread's candidate roots so its garbage remains
+    # collectible after the thread is gone
+    nimYrcThreadTeardown()
 
 proc onThreadDestruction*(handler: proc () {.closure, gcsafe, raises: [].}) =
   ## Registers a *thread local* handler that is called at the thread's
diff --git a/lib/system/yrc.nim b/lib/system/yrc.nim
index 29b6f70ef4..3138a42aae 100644
--- a/lib/system/yrc.nim
+++ b/lib/system/yrc.nim
@@ -1,52 +1,134 @@
 #
 # YRC: Thread-safe ORC (concurrent cycle collector).
-# Same API as orc.nim but with the global mutator/collector RWLock for safety.
-# Destructors for refs run at collection time, not immediately on last decRef.
-# See yrc_proof.lean for a Lean 4 proof of safety and deadlock freedom.
+# Same API as orc.nim. Destructors for refs run at collection time, not
+# immediately on the last decRef.
+# See yrc_proof.lean for a machine-checked (Lean 4) proof of the core
+# invariants — garbage stability, validation soundness, capture partition
+# disjointness, grace periods, fence mutual exclusion, deadlock freedom —
+# and yrc_tarjan_proof.lean for soundness AND completeness of the SCC
+# deadness algorithm.
 #
-# ## Locking Protocol
+# ## Synchronization at a Glance
 #
-# ALL topology-changing operations — heap-field writes (`nimAsgnYrc`,
-# `nimSinkYrc`) and seq mutations that resize internal buffers — hold the
-# global mutator read lock (`gYrcGlobalLock` via `acquireMutatorLock`).
-# Multiple mutators may hold this read lock simultaneously.
+# Ref-field writes (`nimAsgnYrc`, `nimSinkYrc`) are LOCK-FREE: an atomic
+# incRef of the new value, an atomic exchange of the slot, a deferred
+# decRef of the old value enqueued into a stripe queue. The stripe queues
+# have LOCK-FREE PRODUCERS — reserve a slot by fetch-add, then publish it
+# (see the Stripe declaration for the inc/dec publication asymmetry); the
+# per-stripe consumerLock only serializes drains against each other.
 #
-# The cycle collector acquires the exclusive write lock for the entire
-# mark/scan/collect phase. This means the heap topology is *completely
-# frozen* during collection: no `nimAsgnYrc` or seq operation can mutate
-# any pointer field while the three passes run. This gives the Bacon
-# algorithm the stable subgraph it requires without full write barriers.
+# Candidate roots are THREAD-LOCAL (gLocalRoots): draining a thread's
+# stripe registers candidates locally, and the thread's own collections
+# steal that buffer as their root slice — the common path from
+# "suspicious dec" to "freed" never crosses a thread. Exiting threads
+# spill their buffer to a global orphan list, adopted by the next
+# collection anywhere. A cell sits in at most one buffer, guarded by an
+# atomic test-and-set of inRootsFlag; buffered cells are forced live.
 #
-# Consequence for incRef in `nimAsgnYrc`:
-#   Because the collector is blocked, the incRef can be a direct atomic
-#   increment on the RefHeader (`increment head(src)`) rather than going
-#   through the `toInc` stripe queue. The collector will see the updated
-#   RC immediately when it next acquires the write lock. Only decrements
-#   (`yrcDec`) still use the `toDec` stripe queue so that objects whose RC
-#   might reach zero are handled by the collector's cycle-detection logic.
+# Up to MaxPar collections run CONCURRENTLY — with the mutators and with
+# each other — each capturing a disjoint partition of the heap by CAS-ing
+# a claim tag into the rootIdx header word. gMergeLock covers only the
+# tag-slot claim and orphan adoption. All waiting (for a free slot, for a
+# solo capture, for a grace period) is a bounded spin, then parking on
+# gWaitCond.
 #
-# ## Why No Write Barrier Is Needed
+# Seq mutations that change container structure (add/grow/setLen/shrink)
+# announce themselves in the striped gSeqActive counters (seqs_v2.nim); a
+# starting collection waits for those to drain (yrcGcFenceEnter) so its
+# traversal never sees a torn len/payload pair or a freed payload. This
+# fence is the only point where mutators delay a collector.
 #
-# The classic concurrent-GC hazard is the "lost object" problem: during
-# collection the mutator executes `A.field = B` where A is already scanned
-# (black), B is reachable only through an unscanned (gray) object C, and then
-# C's reference to B is removed. The collector never discovers B and frees it
-# while A still points to it. Traditional concurrent collectors need write
-# barriers to prevent this.
+# ## The Write Barrier
 #
-# This problem structurally cannot arise in YRC for two reasons:
+# A concurrent trial-deletion collector needs a snapshot-at-the-beginning
+# (Yuasa) barrier: every reference-set change since the collection started
+# must be observable at commit time. YRC gets this FOR FREE from its
+# deferred RC machinery:
 #
-# 1. The mutator lock freezes the topology during all three passes, so no
-#    concurrent field write can race with markGray/scan/collectWhite.
+# * Removing an edge enqueues the old value into `toDec` — and because the
+#   dec is deferred, the rc word keeps counting the removed reference until
+#   the *next* collection's merge: deletions can only make the captured
+#   graph look MORE alive, never less.
+# * Stack copies enqueue into `toInc` (buffered incs).
+# * Direct rc mutations (`nimAsgnYrc`'s incRef, queue drains, overflow
+#   incs) are atomic RMWs — globally visible when they retire, which the
+#   commit-time rc validation relies on.
 #
-# 2. Even without the lock, the cycle collector only frees *closed cycles* —
-#    subgraphs where every reference to every member comes from within the
-#    group, with zero external references. To execute `A.field = B` the
-#    mutator must hold a reference to A (external ref), which `scan` would
-#    rescue. The two conditions are mutually exclusive.
+# So the commit-time validation is:
+#   1. Any cell sitting in a `toInc`/`toDec` queue had its reference set
+#      changed during capture: its SCC is "dirty" and must not be freed
+#      this round (the entries stay queued; the next merge re-registers
+#      them as candidate roots).
+#   2. Any dead-classified member whose rc word changed since capture saw a
+#      direct incRef: a mutator published a new reference to it. Abort.
+# Everything else was garbage when the collection started, and garbage is
+# stable: nothing can reach it, so nothing can resurrect or mutate it.
+# Aborted SCCs cost nothing (capture never writes to the heap) and are
+# re-registered for the next round.
 #
-# In practice reason (1) makes reason (2) a belt-and-suspenders safety
-# argument rather than the primary mechanism.
+# ## The Collection Algorithm
+#
+# Instead of the classic trial-deletion three-pass dance (markGray / scan /
+# collectWhite) which mutates the rc words in place, collection is split
+# into three phases that leave the heap untouched until the outcome is
+# decided:
+#
+# 1. Capture: one Tarjan SCC traversal over everything reachable from the
+#    candidate roots. Node -> dense index lookup is O(1) without hashing:
+#    the spare `rootIdx` header word is CAS-claimed with the collection's
+#    tag packed with the discovery index; stale tags of retired
+#    collections never need clearing. Everything else lives in side
+#    arrays (SoA layout).
+#
+# 2. Deadness: pure array work on the captured SCC condensation, no heap
+#    access. An SCC is garbage iff it has no references beyond its internal
+#    ones and no live SCC points to it:
+#       external(S) = sum(refcounts of members) - internal edges - edges
+#                     from garbage SCCs
+#    Tarjan emits SCCs sinks-first, so one linear scan in reverse emission
+#    order settles every SCC (sources before their targets).
+#
+# 3. Validate & commit: after validation (dirty peek + rc recheck, with
+#    demotions propagated to captured cross targets) and a grace period
+#    (foreign captures may still hold stale slot snapshots), only members
+#    of dead SCCs are touched. Every slot of a dead member is nil'ed;
+#    slots pointing at survivors decrement the survivor's rc for real
+#    (edges inside the dead group die with the group). Then the members
+#    are destroyed and freed — the slots are nil by the time destructors
+#    run, so destructors cannot re-enter the decRef machinery for the
+#    already-processed edges. When everything captured died and no
+#    cross-collection or pruned edge was seen, nil+free fuse into a
+#    single pass.
+#
+# This structure visits each edge at most twice (capture + commit of the
+# dead subset) instead of up to three times, and — because the outcome is
+# decided on captured data and the heap is only written in commit —
+# capture runs OPTIMISTICALLY, concurrent with mutators and with other
+# collections, with the validation above as the safety net.
+#
+# ## Generational Epoch Stamps
+#
+# Commit re-stamps the cells it PROVED live with the current epoch and
+# their survival age (same rootIdx word, in a namespace disjoint from the
+# claim tags). Within that epoch, captures treat a stamped DESCENDANT of
+# promoted age as an opaque live external and do not descend: long-lived
+# structures are traced once per epoch instead of once per collection,
+# while die-young data — never promoted — is never deferred. Roots always
+# bypass stamps (every death has a dec-witness that gets registered, and
+# registered cells are always scanned as roots), and explicit full
+# collects advance the epoch first, staying exhaustive. The price is
+# floating garbage bounded by ~2 epochs.
+#
+# ## Why No Lost Objects
+#
+# The collector only frees *closed cycles* — subgraphs where every
+# reference to every member comes from within the group, with zero external
+# references. To mutate the graph a mutator must hold a reference to some
+# object; every way of obtaining or dropping such a reference leaves a
+# trace the commit validation observes: a direct atomic incRef (rc-delta
+# check), a buffered inc/dec in the stripe queues (dirty check), or a heap
+# edge that capture traversed (classified live). Snapshot-garbage is
+# unreachable, leaves no such traces, and is freed on the first attempt.
 
 {.push raises: [].}
 
@@ -56,12 +138,10 @@ import std/locks
 
 const
   NumStripes = 64
-  QueueSize = 128
-  RootsThreshold = 10
+  QueueSize {.intdefine.} = 128   # override with -d:QueueSize=N
 
-  colBlack = 0b000
-  colGray = 0b001
-  colWhite = 0b010
+  # rc-word flag bits, layout shared with ORC. YRC does no tricolor
+  # marking; colorMask survives only for the debug printout.
   maybeCycle = 0b100
   inRootsFlag = 0b1000
   colorMask = 0b011
@@ -69,18 +149,14 @@ const
 
 type
   TraceProc = proc (p, env: pointer) {.nimcall, gcsafe, raises: [].}
-  DisposeProc = proc (p: pointer) {.nimcall, gcsafe, raises: [].}
 
-when defined(nimYrcAtomicIncs):
+# With lock-free ref assignments, rc words are mutated concurrently with the
+# collector (direct atomic incRefs), so all collector-side rc accesses must
+# be atomic whenever threads exist.
+const useAtomicRc = defined(nimYrcAtomicIncs) or hasThreadSupport
+
+when useAtomicRc:
   template color(c): untyped = atomicLoadN(addr c.rc, ATOMIC_ACQUIRE) and colorMask
-  template setColor(c, col) =
-    block:
-      var expected = atomicLoadN(addr c.rc, ATOMIC_RELAXED)
-      while true:
-        let desired = (expected and not colorMask) or col
-        if atomicCompareExchangeN(addr c.rc, addr expected, desired, true,
-                                   ATOMIC_ACQ_REL, ATOMIC_RELAXED):
-          break
   template loadRc(c): int = atomicLoadN(addr c.rc, ATOMIC_ACQUIRE)
   template trialDec(c) =
     discard atomicFetchAdd(addr c.rc, -rcIncrement, ATOMIC_ACQ_REL)
@@ -94,65 +170,303 @@ when defined(nimYrcAtomicIncs):
         if atomicCompareExchangeN(addr c.rc, addr expected, desired, true,
                                    ATOMIC_ACQ_REL, ATOMIC_RELAXED):
           break
-  template rcSetFlag(c, flag) =
+  template rcTestSetFlag(c, flag): bool =
+    ## Atomically set `flag`; evaluates to true iff THIS call set it (it
+    ## was clear). Candidate registration must win this race so that a
+    ## cell sits in at most one candidate buffer.
     block:
       var expected = atomicLoadN(addr c.rc, ATOMIC_RELAXED)
-      while true:
-        let desired = expected or flag
-        if atomicCompareExchangeN(addr c.rc, addr expected, desired, true,
-                                   ATOMIC_ACQ_REL, ATOMIC_RELAXED):
+      var won = false
+      while (expected and flag) == 0:
+        if atomicCompareExchangeN(addr c.rc, addr expected, expected or flag,
+                                   true, ATOMIC_ACQ_REL, ATOMIC_RELAXED):
+          won = true
           break
+      won
 else:
   template color(c): untyped = c.rc and colorMask
-  template setColor(c, col) =
-    when col == colBlack:
-      c.rc = c.rc and not colorMask
-    else:
-      c.rc = c.rc and not colorMask or col
   template loadRc(c): int = c.rc
   template trialDec(c) = c.rc = c.rc -% rcIncrement
   template trialInc(c) = c.rc = c.rc +% rcIncrement
   template rcClearFlag(c, flag) = c.rc = c.rc and not flag
-  template rcSetFlag(c, flag) = c.rc = c.rc or flag
+  template rcTestSetFlag(c, flag): bool =
+    block:
+      let won = (c.rc and flag) == 0
+      if won: c.rc = c.rc or flag
+      won
 
 const
   optimizedOrc = false
-  useJumpStack = false
+
+# ---------------- side structure for capture ----------------
 
 type
+  RawSeq[T] = object
+    ## growable array of plain scalars, allocation idiom as in CellSeq
+    len, cap: int
+    d: ptr UncheckedArray[T]
+
+proc resize[T](s: var RawSeq[T]; minCap: int) =
+  s.cap = max(minCap, s.cap div 2 +% s.cap)
+  let newSize = s.cap *% sizeof(T)
+  when compileOption("threads"):
+    s.d = cast[ptr UncheckedArray[T]](reallocShared(s.d, cast[Natural](newSize)))
+  else:
+    s.d = cast[ptr UncheckedArray[T]](realloc(s.d, cast[Natural](newSize)))
+
+proc add[T](s: var RawSeq[T]; v: T) {.inline.} =
+  if s.len >= s.cap: resize(s, s.len +% 1)
+  s.d[s.len] = v
+  s.len = s.len +% 1
+
+proc pop[T](s: var RawSeq[T]): T {.inline.} =
+  s.len = s.len -% 1
+  result = s.d[s.len]
+
+proc init[T](s: var RawSeq[T]; cap: int = 256) =
+  s.len = 0
+  s.cap = cap
+  when compileOption("threads"):
+    s.d = cast[ptr UncheckedArray[T]](allocShared(cast[Natural](s.cap *% sizeof(T))))
+  else:
+    s.d = cast[ptr UncheckedArray[T]](alloc(cast[Natural](s.cap *% sizeof(T))))
+
+proc deinit[T](s: var RawSeq[T]) =
+  if s.d != nil:
+    when compileOption("threads"):
+      deallocShared(s.d)
+    else:
+      dealloc(s.d)
+    s.d = nil
+  s.len = 0
+  s.cap = 0
+
+proc setLenZeroed[T](s: var RawSeq[T]; n: int) =
+  if s.cap < n: resize(s, n)
+  s.len = n
+  zeroMem(s.d, n *% sizeof(T))
+
+proc setLenUninit[T](s: var RawSeq[T]; n: int) =
+  if s.cap < n: resize(s, n)
+  s.len = n
+
+type
+  TraceEntry = object
+    ## (slot, value) snapshot taken at trace time. The value is read exactly
+    ## once: `nimTraceRefDyn` derives the type descriptor from it, so using
+    ## the snapshot everywhere guarantees descriptor and value always match
+    ## even when a mutator concurrently overwrites the slot.
+    slot: ptr pointer
+    val: pointer
+
+  TarjanFrame = object
+    u: int32     # dense index of the cell this frame belongs to
+    base: int    # traceStack.len before this cell's trace ran
+
+  CaptureRec = object
+    ## per captured cell, position == Tarjan discovery index; one record so
+    ## a node costs a single append during the DFS
+    cell: Cell
+    desc: PNimTypeV2
+    rcWord: int               # rc word as captured
+    lowlink: int32
+    sccOf: int32              # -1 while the cell is on the Tarjan stack
+
+  CaptureBufs = object
+    ## side structure of a collection; per collector thread (gCap is a
+    ## threadvar) and persistent across collections, so that frequent
+    ## small collections don't pay per-collection allocations
+    recs: RawSeq[CaptureRec]
+    tstack: RawSeq[int32]
+    frames: RawSeq[TarjanFrame]
+    edges: RawSeq[int64]      # (u shl 32) or v, dense indices
+    sccMemStart: RawSeq[int32]
+    sccMembers: RawSeq[int32]
+    sumRefs: RawSeq[int]      # per SCC: sum of member reference counts
+    internal: RawSeq[int]     # per SCC: number of intra-SCC edges
+    deadIn: RawSeq[int]       # per SCC: number of edges from dead SCCs
+    sccFlags: RawSeq[uint8]
+    crossOff: RawSeq[int32]   # condensation cross edges, bucketed by source
+    crossTgt: RawSeq[int32]
+    crossCursor: RawSeq[int32]
+    crossPend: CellSeq[Cell]  # edge targets owned by other active collections
+    prunedSrc: RawSeq[int32]  # dense indices of cells with pruned out-edges
+    ages: RawSeq[int32]       # per captured cell: captures survived so far
+
   GcEnv = object
-    traceStack: CellSeq[ptr pointer]
-    when useJumpStack:
-      jumpStack: CellSeq[ptr pointer]
+    traceStack: CellSeq[TraceEntry]
     toFree: CellSeq[Cell]
-    freed, touched, edges, rcSum: int
+    nScc: int
+    nDeadScc: int
+    nAborted: int
+    freed, touched: int
     keepThreshold: bool
 
+var gCap {.threadvar.}: CaptureBufs
+
+const
+  flagDead = 1'u8
+  flagForcedLive = 2'u8
+  flagDirty = 4'u8   # a member's reference set changed during capture
+  flagPruned = 8'u8  # an out-edge was pruned via an epoch stamp: a "live"
+                     # verdict may lean on stale stamps, keep it examinable
+
 proc trace(s: Cell; desc: PNimTypeV2; j: var GcEnv) {.inline.} =
   if desc.traceImpl != nil:
     var p = s +! sizeof(RefHeader)
     cast[TraceProc](desc.traceImpl)(p, addr(j))
 
+# The spare rootIdx header word (unused by YRC's root registration, which
+# relies on inRootsFlag) doubles as the capture claim: it packs the owning
+# collection's tag with the cell's dense discovery index. Up to MaxPar
+# collections run CONCURRENTLY, each capturing a disjoint partition of the
+# heap: the first collection to CAS its tag into a cell owns it; everyone
+# else treats the cell as an opaque survivor. Stale tags (from retired
+# collections) never need clearing, they are simply reclaimable.
+#
+# The word does double duty a second time: commit re-stamps proven-live
+# cells with the current EPOCH (high-word namespace disjoint from tags, so
+# the claim protocol is unchanged). Within the same epoch a capture treats
+# a stamped DESCENDANT as an opaque live external and does not descend —
+# long-lived live structures are traced once per epoch instead of once per
+# collection. Roots always bypass the stamp: every death has a dec-witness
+# that gets registered, and registered cells are always scanned as roots.
+const MaxPar {.intdefine.} = 8    # max concurrent collections
+
+when sizeof(int) == 8:
+  const ParSlots = MaxPar
+else:
+  const ParSlots = 1              # no room to pack tags: single collector
+
+var
+  gMergeLock: Lock                       # protects the tag slots + orphaned roots
+  gActiveTags: array[ParSlots, int]      # 0 = free slot
+  gSlotPhase: array[ParSlots, int]       # 0 idle, 1 capturing, 2 committing
+  gSoloCapture: int                      # a solo collection is in its capture phase
+  gTagCounter: int
+  gMyTag {.threadvar.}: int
+  gMySlot {.threadvar.}: int
+  gAmSolo {.threadvar.}: bool
+  gEpoch: int                            # advanced every YrcEpochLen collections
+  gCollectionCounter: int
+  gMyEpochStamp {.threadvar.}: int       # this collection's epoch, as a stamp word
+  gWaitLock: Lock                        # pairs gWaitCond's wait/broadcast; leaf
+  gWaitCond: Cond                        # signaled on capture-end and collection-finish
+
+const
+  SpinBeforePark = 4000
+  YrcEpochLen {.intdefine.} = 64  # collections per epoch; bounds how long a
+                                  # stale "proven live" stamp defers rescans.
+                                  # Short epochs resonate badly with the
+                                  # adaptive threshold: pruned collections
+                                  # are cheap, so collections speed up — and
+                                  # with them the epoch clock, forcing full
+                                  # re-traces MORE often than no stamps at
+                                  # all. (A work-based clock would fix this
+                                  # properly.)
+  YrcPromoteAge {.intdefine.} = 3 # captures a cell must survive before its
+                                  # stamp prunes. Die-young data must never
+                                  # be deferred: torcbench-style lists are
+                                  # traced ~2x per lifetime (the second trace
+                                  # is usually the last), so promoting at 2
+                                  # doubles worker maxMem via death floats;
+                                  # at 3 the floats vanish while long-lived
+                                  # webs (traced >> 3x) keep the full win
+  epochBase = 0x40000000          # stamp namespace: tags stay below this
+  epochMask = 0x3FFFFFFF
+
+# stamp layout: high word = epochBase|epoch, low word = survival age
+template epochStamp(e: int): int = (epochBase or (e and epochMask)) shl 32
+template stampAge(w: int): int = w and 0xFFFFFFFF
+template isEpochStamp(w: int): bool = (w shr 32) >= epochBase
+
+template parkUntil(cond: untyped) =
+  ## Bounded spin (collections transition in microseconds when the system is
+  ## healthy), then block on gWaitCond. `cond` must only read atomics, and
+  ## every write that can make it true is followed by collectorEvent().
+  var spins {.inject.} = 0
+  while not (cond):
+    inc spins
+    if spins >= SpinBeforePark:
+      acquire gWaitLock
+      while not (cond):
+        wait(gWaitCond, gWaitLock)
+      release gWaitLock
+      break
+
+proc collectorEvent() {.inline.} =
+  ## Wake every parked collector after a slot/phase/solo transition. The
+  ## broadcast happens under gWaitLock so that a waiter that saw the old
+  ## state is already inside wait() by the time we broadcast.
+  acquire gWaitLock
+  broadcast gWaitCond
+  release gWaitLock
+
+proc anySlotFree(): bool {.inline.} =
+  result = false
+  for sl in 0 ..< ParSlots:
+    if atomicLoadN(addr gActiveTags[sl], ATOMIC_ACQUIRE) == 0:
+      return true
+
+when sizeof(int) == 8:
+  template isStamped(c: Cell): bool =
+    # "stamped" means: claimed by THIS collection. A relaxed load suffices:
+    # only this thread ever stores gMyTag, and any stale read of a foreign
+    # value routes into claimCell which re-validates with acquire + CAS.
+    (atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED) shr 32) == gMyTag
+  template denseIdx(c: Cell): int32 =
+    int32(atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED) and 0xFFFFFFFF)
+
+  proc isActiveTag(t: int): bool {.inline.} =
+    result = false
+    if t != 0:
+      for s in 0 ..< ParSlots:
+        if atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) == t:
+          return true
+else:
+  template isStamped(c: Cell): bool = c.rootIdx != 0
+  template denseIdx(c: Cell): int32 = int32(c.rootIdx -% 1)
+
 type
   Stripe = object
-    when not defined(yrcAtomics):
-      lockInc: Lock
-    toIncLen: int
+    consumerLock: Lock
+      ## consumers (drains) exclude each other; producers and the
+      ## validation peek are lock-free
+    toIncLen: int     # reservation counters; may exceed QueueSize under
+    toDecLen: int     # overflow — reservations past QueueSize never write
     toInc: array[QueueSize, Cell]
-    lockDec: Lock
-    toDecLen: int
+      ## produced lock-free: reserve via fetch-add, publish the cell with
+      ## an atomic EXCHANGE (non-nil = ready; globals start zeroed and the
+      ## consumer nils consumed slots). The publish must be an RMW, not a
+      ## release store: a queued inc means the rc word UNDER-counts a live
+      ## reference, so the validation peek must reliably observe every
+      ## entry of a completed barrier — an RMW is globally ordered when it
+      ## retires, a release store could still sit in a store buffer.
     toDec: array[QueueSize, (Cell, PNimTypeV2)]
+      ## produced lock-free: reserve via fetch-add, store the cell, then
+      ## publish by storing the desc with release order (desc != nil =
+      ## ready). A plain release suffices here: a pending dec leaves the
+      ## target's rc with an unexplained surplus that forces it live even
+      ## if a peek misses the entry.
 
 type
   PreventThreadFromCollectProc* = proc(): bool {.nimcall, gcsafe, raises: [].}
     ## Callback run before this thread runs the cycle collector.
     ## Return `true` to allow collection, `false` to skip (e.g. real-time thread).
-    ## Invoked while holding the global lock; must not call back into YRC.
+    ## Invoked lock-free before this thread would start a collection;
+    ## must not call back into YRC.
 
 var
-  roots: CellSeq[Cell]  # merged roots, used under global lock
+  roots: CellSeq[Cell]  # ORPHANED candidates only: spilled by exiting
+                        # threads, adopted by the next collection on any
+                        # thread. Guarded by gMergeLock.
+  gLocalRoots {.threadvar.}: CellSeq[Cell]
+    ## This thread's candidate roots. Only the owning thread touches it:
+    ## draining this thread's stripe queue registers candidates here, and
+    ## this thread's collections steal it as their slice — no lock, and
+    ## collections keep the cache locality of thread-local data.
   stripes: array[NumStripes, Stripe]
-  rootsThreshold: int = 128
+  rootsThreshold: int = 128   # shared adaptive heuristic; races are benign
   defaultThreshold = when defined(nimFixedOrc): 10_000 else: 128
   gPreventThreadFromCollectProc: PreventThreadFromCollectProc = nil
 
@@ -196,67 +510,123 @@ proc nimIncRefCyclic(p: pointer; cyclic: bool) {.compilerRtl, inl.} =
     if cyclic: h.rc = h.rc or maybeCycle
   when defined(nimYrcAtomicIncs):
     discard atomicFetchAdd(addr h.rc, rcIncrement, ATOMIC_ACQ_REL)
-  elif defined(yrcAtomics):
-    let s = getStripeIdx()
-    let slot = atomicFetchAdd(addr stripes[s].toIncLen, 1, ATOMIC_ACQ_REL)
-    if slot < QueueSize:
-      atomicStoreN(addr stripes[s].toInc[slot], h, ATOMIC_RELEASE)
-    else:
-      yrcCollectorLock:
-        h.rc = h.rc +% rcIncrement
-        for i in 0..<NumStripes:
-          let len = atomicExchangeN(addr stripes[i].toIncLen, 0, ATOMIC_ACQUIRE)
-          for j in 0..<min(len, QueueSize):
-            let x = atomicLoadN(addr stripes[i].toInc[j], ATOMIC_ACQUIRE)
-            x.rc = x.rc +% rcIncrement
   else:
+    # LOCK-FREE producer: reserve, then publish with an atomic exchange
+    # (see the Stripe declaration for why an RMW and not a release store)
     let idx = getStripeIdx()
-    while true:
-      var overflow = false
-      withLock stripes[idx].lockInc:
-        if stripes[idx].toIncLen < QueueSize:
-          stripes[idx].toInc[stripes[idx].toIncLen] = h
-          stripes[idx].toIncLen += 1
-        else:
-          overflow = true
-      if overflow:
-        yrcCollectorLock:
-          for i in 0..<NumStripes:
-            withLock stripes[i].lockInc:
-              for j in 0..<stripes[i].toIncLen:
-                let x = stripes[i].toInc[j]
-                x.rc = x.rc +% rcIncrement
-              stripes[i].toIncLen = 0
-      else:
-        break
+    let slot = atomicFetchAdd(addr stripes[idx].toIncLen, 1, ATOMIC_ACQ_REL)
+    if slot < QueueSize:
+      discard atomicExchangeN(addr stripes[idx].toInc[slot], h, ATOMIC_ACQ_REL)
+    else:
+      # queue full: apply the inc directly — it is atomic, so a running
+      # collection observes it through the commit-time rc validation.
+      # Buffering resumes once the next drain resets the queue.
+      trialInc(h)
 
-proc mergePendingRoots() =
-  # Merge buffered RC operations. Note: Unlike truly concurrent collectors,
-  # we don't need to set color to black on incRef because collection runs
-  # under the global lock, so no concurrent mutations happen during collection.
-  for i in 0..<NumStripes:
+when defined(nimOrcStats):
+  var
+    gStatRegFresh: int    # registrations of never-captured cells
+    gStatRegRepeat: int   # re-registrations of cells that already survived a capture
+    gStatRegCross: int    # registrations of cells claimed by a foreign ACTIVE collection
+    gStatRegSelf: int     # re-registrations by the collection that holds the cell (demotions)
+    gStatCapTotal: int    # cells claimed into captures (traced by the Tarjan DFS)
+    gStatCapRepeat: int   # ...that had already been captured (and survived) before
+    gStatCapPruned: int   # edges pruned via a current-epoch stamp
+
+  template bumpStat(x: untyped) =
+    discard atomicAddFetch(addr x, 1, ATOMIC_RELAXED)
+
+proc registerLocal(c: Cell; desc: PNimTypeV2) {.inline.} =
+  ## Register a candidate in THIS thread's buffer. The atomic test-and-set
+  ## keeps the invariant that a cell sits in at most one candidate buffer:
+  ## whoever wins the flag owns the registration. Buffered cells are forced
+  ## live by every collection (deadness checks the flag), so no buffer
+  ## entry can ever dangle.
+  if rcTestSetFlag(c, inRootsFlag):
+    when defined(nimOrcStats) and sizeof(int) == 8:
+      let st = atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED)
+      if st == 0: bumpStat gStatRegFresh
+      elif gMyTag != 0 and (st shr 32) == gMyTag: bumpStat gStatRegSelf
+      elif isActiveTag(st shr 32): bumpStat gStatRegCross
+      else: bumpStat gStatRegRepeat
+    if gLocalRoots.d == nil: init(gLocalRoots)
+    add(gLocalRoots, c, desc)
+
+proc drainStripe(i: int) =
+  ## Apply the pending RC operations of one stripe queue; freshly
+  ## dead-looking cells become THIS thread's candidates. rc mutations are
+  ## atomic, so no global lock is needed: a running collection observes
+  ## them through its commit-time validation (rc recheck / dirty peek).
+  ## The consumerLock excludes other drains; producers run free. Each
+  ## queue is consumed the same way: process published entries, wait out
+  ## the (two-instruction) publication window of in-flight reservers,
+  ## then close the batch with a CAS — a plain reset could orphan a slot
+  ## a producer is publishing into. Reservations past QueueSize never
+  ## wrote anything, so an overflowed counter is hard-reset.
+  withLock stripes[i].consumerLock:
     when not defined(nimYrcAtomicIncs):
-      # Inc buffers only exist when increfs are buffered (not atomic)
-      when defined(yrcAtomics):
-        let incLen = atomicExchangeN(addr stripes[i].toIncLen, 0, ATOMIC_ACQUIRE)
-        for j in 0..<min(incLen, QueueSize):
-          let x = atomicLoadN(addr stripes[i].toInc[j], ATOMIC_ACQUIRE)
-          x.rc = x.rc +% rcIncrement
-      else:
-        withLock stripes[i].lockInc:
-          for j in 0..<stripes[i].toIncLen:
-            let x = stripes[i].toInc[j]
-            x.rc = x.rc +% rcIncrement
-          stripes[i].toIncLen = 0
-    withLock stripes[i].lockDec:
-      for j in 0..<stripes[i].toDecLen:
-        let (c, desc) = stripes[i].toDec[j]
+      # apply pending incs FIRST: an inc entry means the rc word
+      # under-counts, so its cell must be raised before decs can free
+      var consumedInc = 0
+      while true:
+        let reserved = atomicLoadN(addr stripes[i].toIncLen, ATOMIC_ACQUIRE)
+        let n = min(reserved, QueueSize)
+        for j in consumedInc ..< n:
+          var c = atomicLoadN(addr stripes[i].toInc[j], ATOMIC_ACQUIRE)
+          while c == nil:
+            c = atomicLoadN(addr stripes[i].toInc[j], ATOMIC_ACQUIRE)
+          trialInc(c)
+          atomicStoreN(addr stripes[i].toInc[j], cast[Cell](nil),
+                       ATOMIC_RELAXED)
+        consumedInc = n
+        if reserved >= QueueSize:
+          discard atomicExchangeN(addr stripes[i].toIncLen, 0, ATOMIC_ACQ_REL)
+          break
+        else:
+          var cur = reserved
+          if atomicCompareExchangeN(addr stripes[i].toIncLen, addr cur, 0,
+                                     false, ATOMIC_ACQ_REL, ATOMIC_RELAXED):
+            break
+    var consumed = 0
+    while true:
+      let reserved = atomicLoadN(addr stripes[i].toDecLen, ATOMIC_ACQUIRE)
+      let n = min(reserved, QueueSize)
+      for j in consumed ..< n:
+        var desc = atomicLoadN(addr stripes[i].toDec[j][1], ATOMIC_ACQUIRE)
+        while desc == nil:
+          desc = atomicLoadN(addr stripes[i].toDec[j][1], ATOMIC_ACQUIRE)
+        let c = stripes[i].toDec[j][0]
         trialDec(c)
-        if (loadRc(c) and inRootsFlag) == 0:
-          rcSetFlag(c, inRootsFlag)
-          if roots.d == nil: init(roots)
-          add(roots, c, desc)
-      stripes[i].toDecLen = 0
+        registerLocal(c, desc)
+        atomicStoreN(addr stripes[i].toDec[j][1], cast[PNimTypeV2](nil),
+                     ATOMIC_RELAXED)
+      consumed = n
+      if reserved >= QueueSize:
+        discard atomicExchangeN(addr stripes[i].toDecLen, 0, ATOMIC_ACQ_REL)
+        break
+      else:
+        var cur = reserved
+        if atomicCompareExchangeN(addr stripes[i].toDecLen, addr cur, 0, false,
+                                   ATOMIC_ACQ_REL, ATOMIC_RELAXED):
+          break
+        # new reservations arrived during processing: consume them too
+
+proc drainAllStripes() =
+  ## Full-collect path: apply every pending RC operation; every resulting
+  ## candidate is adopted by the calling thread.
+  for i in 0..<NumStripes:
+    drainStripe(i)
+
+proc adoptOrphans() =
+  ## Adopt candidates spilled by exited threads. The cells stay flagged;
+  ## they merely change buffers, so the one-buffer invariant holds.
+  if roots.len > 0:               # racy peek; exact under the lock
+    acquire gMergeLock
+    if gLocalRoots.d == nil: init(gLocalRoots)
+    for i in 0 ..< roots.len:
+      add(gLocalRoots, roots.d[i][0], roots.d[i][1])
+    roots.len = 0
+    release gMergeLock
 
 proc collectCycles()
 
@@ -289,125 +659,561 @@ template orcAssert(cond, msg) =
 
 proc nimTraceRef(q: pointer; desc: PNimTypeV2; env: pointer) {.compilerRtl, inl.} =
   let p = cast[ptr pointer](q)
-  if p[] != nil:
+  # read the slot exactly once: mutators may exchange it concurrently.
+  # Aligned pointer loads do not tear on supported targets.
+  let v = p[]
+  if v != nil:
     var j = cast[ptr GcEnv](env)
-    j.traceStack.add(p, desc)
+    j.traceStack.add(TraceEntry(slot: p, val: v), desc)
 
 proc nimTraceRefDyn(q: pointer; env: pointer) {.compilerRtl, inl.} =
   let p = cast[ptr pointer](q)
-  if p[] != nil:
+  let v = p[]
+  if v != nil:
     var j = cast[ptr GcEnv](env)
-    j.traceStack.add(p, cast[ptr PNimTypeV2](p[])[])
+    j.traceStack.add(TraceEntry(slot: p, val: v), cast[ptr PNimTypeV2](v)[])
 
-proc scanBlack(s: Cell; desc: PNimTypeV2; j: var GcEnv) =
-  s.setColor colBlack
-  let until = j.traceStack.len
-  trace(s, desc, j)
-  when logOrc: writeCell("root still alive", s, desc)
-  while j.traceStack.len > until:
-    let (entry, desc) = j.traceStack.pop()
-    let t = head entry[]
-    trialInc(t)
-    if t.color != colBlack:
-      t.setColor colBlack
-      trace(t, desc, j)
-      when logOrc: writeCell("child still alive", t, desc)
+# ---------------- phase 1: capture ----------------
 
-proc markGray(s: Cell; desc: PNimTypeV2; j: var GcEnv) =
-  if s.color != colGray:
-    s.setColor colGray
-    j.touched = j.touched +% 1
-    j.rcSum = j.rcSum +% (loadRc(s) shr rcShift) +% 1
-    orcAssert(j.traceStack.len == 0, "markGray: trace stack not empty")
-    trace(s, desc, j)
-    while j.traceStack.len > 0:
-      let (entry, desc) = j.traceStack.pop()
-      let t = head entry[]
-      trialDec(t)
-      j.edges = j.edges +% 1
-      if t.color != colGray:
-        t.setColor colGray
-        j.touched = j.touched +% 1
-        j.rcSum = j.rcSum +% (loadRc(t) shr rcShift) +% 2
-        trace(t, desc, j)
-
-proc scan(s: Cell; desc: PNimTypeV2; j: var GcEnv) =
-  if s.color == colGray:
-    if (loadRc(s) shr rcShift) >= 0:
-      scanBlack(s, desc, j)
-    else:
-      orcAssert(j.traceStack.len == 0, "scan: trace stack not empty")
-      s.setColor(colWhite)
-      trace(s, desc, j)
-      while j.traceStack.len > 0:
-        let (entry, desc) = j.traceStack.pop()
-        let t = head entry[]
-        if t.color == colGray:
-          if (loadRc(t) shr rcShift) >= 0:
-            scanBlack(t, desc, j)
-          else:
-            t.setColor(colWhite)
-            trace(t, desc, j)
-
-proc collectColor(s: Cell; desc: PNimTypeV2; col: int; j: var GcEnv) =
-  if s.color == col and (loadRc(s) and inRootsFlag) == 0:
-    orcAssert(j.traceStack.len == 0, "collectWhite: trace stack not empty")
-    s.setColor(colBlack)
-    j.toFree.add(s, desc)
-    trace(s, desc, j)
-    while j.traceStack.len > 0:
-      let (entry, desc) = j.traceStack.pop()
-      let t = head entry[]
-      entry[] = nil
-      if t.color == col and (loadRc(t) and inRootsFlag) == 0:
-        j.toFree.add(t, desc)
-        t.setColor(colBlack)
-        trace(t, desc, j)
-
-proc collectCyclesBacon(j: var GcEnv; lowMark: int) =
-  # YRC defers all destruction to collection time - process ALL roots through Bacon's algorithm
-  # This is different from ORC which handles immediate garbage (rc == 0) directly
-  if lockState == Collecting:
-    return
-  lockState = Collecting
-  let last = roots.len -% 1
-  when logOrc:
-    for i in countdown(last, lowMark):
-      writeCell("root", roots.d[i][0], roots.d[i][1])
-
-  # Process all roots through markGray (Bacon's algorithm)
-  for i in countdown(last, lowMark):
-    markGray(roots.d[i][0], roots.d[i][1], j)
-
-  var colToCollect = colWhite
-  if j.rcSum == j.edges:
-    # Short-cut: we know everything is garbage
-    colToCollect = colGray
-    j.keepThreshold = true
+proc prepareCapture() =
+  if gCap.recs.d == nil:
+    init gCap.recs
+    init gCap.tstack
+    init gCap.frames
+    init gCap.edges
+    init gCap.sccMemStart
+    init gCap.sccMembers
+    init gCap.sumRefs
+    init gCap.internal
+    init gCap.deadIn
+    init gCap.sccFlags
+    init gCap.crossOff
+    init gCap.crossTgt
+    init gCap.crossCursor
+    init gCap.crossPend
+    init gCap.prunedSrc
+    init gCap.ages
   else:
-    # Normal scan phase
-    for i in countdown(last, lowMark):
-      scan(roots.d[i][0], roots.d[i][1], j)
+    gCap.recs.len = 0
+    gCap.tstack.len = 0
+    gCap.frames.len = 0
+    gCap.edges.len = 0
+    gCap.sccMemStart.len = 0
+    gCap.sccMembers.len = 0
+    gCap.sumRefs.len = 0
+    gCap.crossPend.len = 0
+    gCap.prunedSrc.len = 0
+    gCap.ages.len = 0
 
-  # Collect phase: free all garbage objects
-  init j.toFree
-  for i in 0 ..< roots.len:
-    let s = roots.d[i][0]
-    rcClearFlag(s, inRootsFlag)
-    collectColor(s, roots.d[i][1], colToCollect, j)
+# rc is captured without the flag bits: the collector itself toggles
+# inRootsFlag between capture and commit, which must not look like a
+# mutation to the commit-time rc validation.
+when sizeof(int) == 8:
+  proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs;
+                 pruneLive: bool): int32 =
+    ## Dense index if this collection owns `c` (claiming and registering it
+    ## if it was unclaimed), -1 if another ACTIVE collection owns it, or
+    ## -2 if `pruneLive` and the cell was proven live in the current epoch
+    ## (treat as an opaque live external, don't descend).
+    if gAmSolo:
+      # no other collection is (or can start) capturing: plain stores.
+      # This recovers the sequential capture speed of the single-collector
+      # design whenever collections do not actually overlap.
+      let old = c.rootIdx
+      if (old shr 32) == gMyTag:
+        return int32(old and 0xFFFFFFFF)
+      if pruneLive and (old shr 32) == (gMyEpochStamp shr 32) and
+          stampAge(old) >= YrcPromoteAge:
+        return -2
+      let idx = cap.recs.len
+      c.rootIdx = (gMyTag shl 32) or idx
+      when defined(nimOrcStats):
+        bumpStat gStatCapTotal
+        if old != 0: bumpStat gStatCapRepeat
+      cap.recs.add CaptureRec(cell: c, desc: desc,
+                               rcWord: loadRc(c) and not rcMask,
+                               lowlink: int32(idx), sccOf: -1'i32)
+      cap.ages.add int32(if isEpochStamp(old): min(stampAge(old), 1000) else: 0)
+      cap.tstack.add int32(idx)
+      return int32(idx)
+    while true:
+      var old = atomicLoadN(addr c.rootIdx, ATOMIC_ACQUIRE)
+      if (old shr 32) == gMyTag:
+        return int32(old and 0xFFFFFFFF)
+      if pruneLive and (old shr 32) == (gMyEpochStamp shr 32) and
+          stampAge(old) >= YrcPromoteAge:
+        return -2
+      if isActiveTag(old shr 32):
+        return -1
+      let idx = cap.recs.len
+      if atomicCompareExchangeN(addr c.rootIdx, addr old,
+                                 (gMyTag shl 32) or idx, false,
+                                 ATOMIC_ACQ_REL, ATOMIC_RELAXED):
+        when defined(nimOrcStats):
+          bumpStat gStatCapTotal
+          if old != 0: bumpStat gStatCapRepeat
+        cap.recs.add CaptureRec(cell: c, desc: desc,
+                                 rcWord: loadRc(c) and not rcMask,
+                                 lowlink: int32(idx), sccOf: -1'i32)
+        cap.ages.add int32(if isEpochStamp(old): min(stampAge(old), 1000) else: 0)
+        cap.tstack.add int32(idx)
+        return int32(idx)
+else:
+  proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs;
+                 pruneLive: bool): int32 =
+    # no room to pack epoch stamps on 32 bit: pruneLive is ignored
+    if c.rootIdx != 0:
+      result = int32(c.rootIdx -% 1)
+    else:
+      result = int32(cap.recs.len)
+      c.rootIdx = cap.recs.len +% 1
+      cap.recs.add CaptureRec(cell: c, desc: desc,
+                               rcWord: loadRc(c) and not rcMask,
+                               lowlink: result, sccOf: -1'i32)
+      cap.tstack.add result
 
-  # Clear roots before freeing to prevent nested collectCycles() from accessing freed cells
-  roots.len = 0
+proc capture(s: Cell; desc: PNimTypeV2; j: var GcEnv; cap: ptr CaptureBufs) =
+  ## Iterative Tarjan SCC over everything reachable from `s`. A frame's
+  ## pending out-edges are the traceStack entries above frame.base; a child
+  ## pushes and drains its own segment above ours, so when the child's frame
+  ## pops, the stack is back at our segment and we resume popping our edges.
+  if isStamped(s): return
+  orcAssert(j.traceStack.len == 0, "capture: trace stack not empty")
+  # roots never prune: a dec-witnessed suspicion overrides any epoch stamp
+  let root = claimCell(s, desc, cap, pruneLive = false)
+  if root < 0:
+    return   # another active collection owns this candidate; it handles it
+  trace(s, desc, j)
+  cap.frames.add TarjanFrame(u: root, base: 0)
+  while cap.frames.len > 0:
+    let u = cap.frames.d[cap.frames.len -% 1].u
+    let base = cap.frames.d[cap.frames.len -% 1].base
+    if j.traceStack.len > base:
+      let (entry, tdesc) = j.traceStack.pop()
+      let t = head(entry.val)
+      if isStamped(t):
+        let v = denseIdx(t)
+        cap.edges.add (int64(u) shl 32) or int64(v)
+        if cap.recs.d[v].sccOf < 0 and v < cap.recs.d[u].lowlink:
+          cap.recs.d[u].lowlink = v
+      else:
+        let childBase = j.traceStack.len
+        let v = claimCell(t, tdesc, cap, pruneLive = true)
+        if v == -1:
+          # cross-collection edge: the owner sees our reference in the rc
+          # word and classifies the target live; we re-register it as a
+          # candidate before our commit so it is re-examined later
+          cap.crossPend.add(t, tdesc)
+        elif v == -2:
+          # target proven live this epoch: opaque live external, no descent.
+          # Taint u's SCC — its own "live" verdict may lean on the stamp.
+          cap.prunedSrc.add u
+          when defined(nimOrcStats):
+            bumpStat gStatCapPruned
+        else:
+          cap.edges.add (int64(u) shl 32) or int64(v)
+          trace(t, tdesc, j)
+          cap.frames.add TarjanFrame(u: v, base: childBase)
+    else:
+      cap.frames.len = cap.frames.len -% 1
+      if cap.frames.len > 0:
+        let pu = cap.frames.d[cap.frames.len -% 1].u
+        if cap.recs.d[u].lowlink < cap.recs.d[pu].lowlink:
+          cap.recs.d[pu].lowlink = cap.recs.d[u].lowlink
+      if cap.recs.d[u].lowlink == u:
+        # u is the root of an SCC: pop the members off the Tarjan stack
+        cap.sccMemStart.add int32(cap.sccMembers.len)
+        var sum = 0
+        while true:
+          let w = cap.tstack.pop()
+          cap.recs.d[w].sccOf = int32(j.nScc)
+          cap.sccMembers.add w
+          sum = sum +% (cap.recs.d[w].rcWord shr rcShift) +% 1
+          if w == u: break
+        cap.sumRefs.add sum
+        inc j.nScc
 
-  # Free all collected objects
-  # Destructors must not call nimDecRefIsLastCyclicStatic (add to toDec) during this phase
-  for i in 0 ..< j.toFree.len:
-    let s = j.toFree.d[i][0]
-    when orcLeakDetector:
-      writeCell("CYCLIC OBJECT FREED", s, j.toFree.d[i][1])
-    free(s, j.toFree.d[i][1])
-  j.freed = j.freed +% j.toFree.len
-  deinit j.toFree
+# ---------------- phase 2: deadness, side arrays only ----------------
+
+proc computeDeadness(j: var GcEnv; cap: ptr CaptureBufs) =
+  let nScc = j.nScc
+  setLenZeroed cap.internal, nScc
+  setLenZeroed cap.deadIn, nScc
+  setLenZeroed cap.sccFlags, nScc
+  setLenZeroed cap.crossOff, nScc + 1
+  setLenUninit cap.crossCursor, nScc
+  # classify captured edges: internal to an SCC vs condensation cross edges
+  var nCross = 0
+  for i in 0 ..< cap.edges.len:
+    let e = cap.edges.d[i]
+    let su = cap.recs.d[int32(e shr 32)].sccOf
+    let sv = cap.recs.d[int32(e and 0xFFFFFFFF'i64)].sccOf
+    if su == sv:
+      inc cap.internal.d[su]
+    else:
+      inc cap.crossOff.d[su]
+      inc nCross
+  var total = 0'i32
+  for s in 0 ..< nScc:
+    let c = cap.crossOff.d[s]
+    cap.crossOff.d[s] = total
+    cap.crossCursor.d[s] = total
+    total = total +% c
+  cap.crossOff.d[nScc] = total
+  setLenUninit cap.crossTgt, nCross
+  for i in 0 ..< cap.edges.len:
+    let e = cap.edges.d[i]
+    let su = cap.recs.d[int32(e shr 32)].sccOf
+    let sv = cap.recs.d[int32(e and 0xFFFFFFFF'i64)].sccOf
+    if su != sv:
+      cap.crossTgt.d[cap.crossCursor.d[su]] = sv
+      inc cap.crossCursor.d[su]
+  # pruned out-edges taint the source SCC: pruning cannot cause a false
+  # "dead" (an untraced target only ever ADDS unexplained external refs),
+  # but a "live" verdict may lean on a stamp that went stale within the
+  # epoch, so validate re-registers surviving pruned SCCs
+  for i in 0 ..< cap.prunedSrc.len:
+    let s = cap.recs.d[cap.prunedSrc.d[i]].sccOf
+    cap.sccFlags.d[s] = cap.sccFlags.d[s] or flagPruned
+  # cells that stay registered as roots (partial collection) count as
+  # externally referenced: the roots buffer itself points at them
+  for mi in 0 ..< cap.sccMembers.len:
+    let m = cap.sccMembers.d[mi]
+    if (loadRc(cap.recs.d[m].cell) and inRootsFlag) != 0:
+      let s = cap.recs.d[m].sccOf
+      cap.sccFlags.d[s] = cap.sccFlags.d[s] or flagForcedLive
+  # deadness over the condensation. Tarjan emits sinks first, so higher SCC
+  # ids are sources and every cross edge goes from a higher id to a lower
+  # one: one reverse scan settles everything.
+  for s in countdown(nScc - 1, 0):
+    let ext = cap.sumRefs.d[s] -% cap.internal.d[s] -% cap.deadIn.d[s]
+    when logOrc:
+      cfprintf(cstderr, "[scc %ld] members %ld sumRefs %ld internal %ld deadIn %ld ext %ld forced %ld\n",
+        s, cap.sccMemStart.d[s+1] - cap.sccMemStart.d[s], cap.sumRefs.d[s],
+        cap.internal.d[s], cap.deadIn.d[s], ext, int(cap.sccFlags.d[s]))
+    if (cap.sccFlags.d[s] and flagForcedLive) == 0 and ext == 0:
+      cap.sccFlags.d[s] = cap.sccFlags.d[s] or flagDead
+      inc j.nDeadScc
+      for k in cap.crossOff.d[s] ..< cap.crossOff.d[s+1]:
+        inc cap.deadIn.d[cap.crossTgt.d[k]]
+    else:
+      # a live SCC keeps everything it points to alive
+      for k in cap.crossOff.d[s] ..< cap.crossOff.d[s+1]:
+        let t = cap.crossTgt.d[k]
+        cap.sccFlags.d[t] = cap.sccFlags.d[t] or flagForcedLive
+
+# ---------------- phase 3: validate & commit ----------------
+
+proc markDirtyFromQueues(j: var GcEnv; cap: ptr CaptureBufs) =
+  ## The SATB half of the design: any cell with an inc or dec enqueued since
+  ## the last drain had its reference set changed during capture. Peek
+  ## (don't drain!) the stripe queues and taint the affected SCCs; the
+  ## entries stay queued and the next merge re-registers them as candidates.
+  template taint(cp: Cell) =
+    let c = cp
+    if isStamped(c):
+      let s = cap.recs.d[denseIdx(c)].sccOf
+      cap.sccFlags.d[s] = cap.sccFlags.d[s] or flagDirty
+  for i in 0..<NumStripes:
+    when not defined(nimYrcAtomicIncs):
+      # lock-free peek. This one is LOAD-BEARING (an inc entry means the
+      # rc word under-counts a live reference), which is why the producer
+      # publishes with an RMW: every completed barrier's entry is globally
+      # visible here. A nil slot is a barrier mid-publication — at most one
+      # per thread, and the chain of custody for how that thread OBTAINED
+      # the reference is older, completed and therefore observable.
+      let incLen = min(atomicLoadN(addr stripes[i].toIncLen, ATOMIC_ACQUIRE),
+                       QueueSize)
+      for k in 0..<incLen:
+        let c = atomicLoadN(addr stripes[i].toInc[k], ATOMIC_ACQUIRE)
+        if c != nil: taint c
+    # lock-free peek: skip slots whose publish has not landed yet. Sound:
+    # a pending deferred dec leaves the target's rc counting a ref whose
+    # edge the capture no longer traverses — an unexplained +1 that forces
+    # the target live no matter what (deletions only make the captured
+    # graph look MORE alive). The taint here is belt and braces.
+    let decLen = min(atomicLoadN(addr stripes[i].toDecLen, ATOMIC_ACQUIRE),
+                     QueueSize)
+    for k in 0..<decLen:
+      if atomicLoadN(addr stripes[i].toDec[k][1], ATOMIC_ACQUIRE) != nil:
+        taint stripes[i].toDec[k][0]
+
+proc demoteTouchedDead(j: var GcEnv; cap: ptr CaptureBufs) =
+  ## One descending demotion pass. Descending ids = the deadness scan's
+  ## order (sources before sinks): a demotion must propagate to the SCC's
+  ## dead cross targets, whose deadIn had explained the edges away only
+  ## under the assumption that this SCC dies with them. The demoted SCC
+  ## survives with its slots intact, so any target left dead would be
+  ## freed under a surviving reference. Targets have lower ids, so
+  ## tainting them here demotes them (transitively) later in this loop.
+  for s in countdown(j.nScc - 1, 0):
+    if (cap.sccFlags.d[s] and flagDead) != 0:
+      var ok = (cap.sccFlags.d[s] and flagDirty) == 0
+      if ok:
+        for mi in cap.sccMemStart.d[s] ..< cap.sccMemStart.d[s+1]:
+          let m = cap.sccMembers.d[mi]
+          if (loadRc(cap.recs.d[m].cell) and not rcMask) != cap.recs.d[m].rcWord:
+            ok = false
+            break
+      if not ok:
+        cap.sccFlags.d[s] = cap.sccFlags.d[s] and not flagDead
+        inc j.nAborted
+        for k in cap.crossOff.d[s] ..< cap.crossOff.d[s+1]:
+          let t = cap.crossTgt.d[k]
+          if (cap.sccFlags.d[t] and flagDead) != 0:
+            cap.sccFlags.d[t] = cap.sccFlags.d[t] or flagDirty
+        let m = cap.sccMembers.d[cap.sccMemStart.d[s]]
+        registerLocal(cap.recs.d[m].cell, cap.recs.d[m].desc)
+    elif (cap.sccFlags.d[s] and flagPruned) != 0:
+      # survives, but its liveness may rest on a stale epoch stamp: keep
+      # one member registered so the verdict is retried (fully re-examined
+      # once the epoch advances)
+      let m = cap.sccMembers.d[cap.sccMemStart.d[s]]
+      registerLocal(cap.recs.d[m].cell, cap.recs.d[m].desc)
+
+proc validateDead(j: var GcEnv; cap: ptr CaptureBufs) =
+  ## Demote every dead SCC that a mutator touched during capture: dirty via
+  ## the queues, or a direct incRef visible as a changed rc word. Demoted
+  ## SCCs become ordinary survivors (so committed neighbors decrement into
+  ## them correctly) and one member is re-registered as a candidate root so
+  ## the SCC is re-examined by the next collection.
+  ##
+  ## ONE peek before the rc rechecks suffices; there is no peek→commit
+  ## TOCTOU. To enqueue an op on X a mutator must HOLD X, and its chain of
+  ## custody regresses to evidence this validation already checks: a ref
+  ## counted at capture (X was never classified dead), a direct incRef
+  ## since capture (rc-word recheck, which runs AFTER the peek), or a
+  ## buffered stack inc — still queued (this peek saw it) or drained
+  ## (rc word changed before the recheck). New entries after the peek
+  ## carry no new information about X's deadness. See "Why No Lost
+  ## Objects" above and yrc_proof.lean §3–§4.
+  markDirtyFromQueues(j, cap)
+  demoteTouchedDead(j, cap)
+
+proc commitDead(j: var GcEnv; cap: ptr CaptureBufs) =
+  validateDead(j, cap)
+  # publish cross-collection edge targets as candidate roots BEFORE any of
+  # our commit decs could make them collectible: they are owner-live this
+  # round, and the registration keeps them examinable in a later round
+  for i in 0 ..< cap.crossPend.len:
+    registerLocal(cap.crossPend.d[i][0], cap.crossPend.d[i][1])
+  template deadCell(t: Cell): bool =
+    isStamped(t) and (cap.sccFlags.d[cap.recs.d[denseIdx(t)].sccOf] and flagDead) != 0
+  template graceWait() =
+    # Grace period: another collection still in its CAPTURE phase may hold
+    # stale (slot, value) snapshots referencing our dead cells; disposing
+    # them now could hand reused memory to its traversal. Captures are
+    # bounded and never wait on us. New captures cannot reach our dead
+    # cells: they are unreachable, and our tag stays active until after
+    # the frees.
+    when sizeof(int) == 8:
+      for s in 0 ..< ParSlots:
+        if s != gMySlot:
+          let tg = atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE)
+          if tg != 0:
+            parkUntil(atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) != tg or
+                      atomicLoadN(addr gSlotPhase[s], ATOMIC_ACQUIRE) != 1)
+  # A dead cell's reference to another active collection's cell must still
+  # be decremented (the target survives this round), so the all-dead fast
+  # path additionally requires that no cross-collection edge was seen.
+  # pruned edges also disable the fused path: its nil-without-dec would
+  # leak rc on the stamped targets (and skip their re-registration)
+  let allDead = j.nDeadScc == j.nScc and j.nAborted == 0 and
+                cap.crossPend.len == 0 and cap.prunedSrc.len == 0
+  if allDead:
+    # Everything captured dies and no slot can point outside the dead set:
+    # nil the slots and free in ONE pass over the cells — they went cold
+    # since capture, a second sweep would miss cache all over again.
+    # Freeing cell A before nil-ing a later cell B's slot that points at A
+    # is fine: nobody reads B's slots in between (mutators cannot reach the
+    # closed dead set, foreign captures never traverse our tagged cells,
+    # and the grace wait has retired stale snapshots before the first free).
+    graceWait()
+    for m in 0 ..< cap.recs.len:
+      let cell = cap.recs.d[m].cell
+      let desc = cap.recs.d[m].desc
+      orcAssert(j.traceStack.len == 0, "commitDead: trace stack not empty")
+      trace(cell, desc, j)
+      while j.traceStack.len > 0:
+        let (entry, _) = j.traceStack.pop()
+        entry.slot[] = nil
+      when sizeof(int) != 8:
+        cell.rootIdx = 0    # no epoch in the stamp: clear before the free
+      when orcLeakDetector:
+        writeCell("CYCLIC OBJECT FREED", cell, desc)
+      free(cell, desc)
+    j.freed = cap.recs.len
+  else:
+    init j.toFree
+    for s in 0 ..< j.nScc:
+      if (cap.sccFlags.d[s] and flagDead) != 0:
+        for mi in cap.sccMemStart.d[s] ..< cap.sccMemStart.d[s+1]:
+          let m = cap.sccMembers.d[mi]
+          let cell = cap.recs.d[m].cell
+          let desc = cap.recs.d[m].desc
+          j.toFree.add(cell, desc)
+          # nil every slot so the destructor cannot dec these edges again;
+          # references to survivors are decremented for real, references into
+          # the dead group die with the group (already accounted by deadIn).
+          # The dead cells must all outlive this pass: deadCell reads the
+          # TARGET's header, so no fusing with the free loop here.
+          orcAssert(j.traceStack.len == 0, "commitDead: trace stack not empty")
+          trace(cell, desc, j)
+          while j.traceStack.len > 0:
+            let (entry, tdesc) = j.traceStack.pop()
+            let t = head(entry.val)
+            entry.slot[] = nil
+            if not deadCell(t):
+              trialDec(t)
+              when sizeof(int) == 8:
+                # a stamped target was not analyzed by THIS collection, so
+                # this dec may be the death blow: keep the cell examinable
+                if isEpochStamp(atomicLoadN(addr t.rootIdx, ATOMIC_RELAXED)):
+                  registerLocal(t, tdesc)
+    when sizeof(int) == 8:
+      # epoch-stamp what this collection PROVED live, carrying the cell's
+      # survival age: only cells that keep surviving get promoted to ages
+      # where captures prune them, so die-young data is never deferred.
+      # Demoted (dirty) and pruned SCCs stay unproven — leave their stale
+      # tags claimable. Our tag is still active, so no foreign claim can
+      # race these stores.
+      for s in 0 ..< j.nScc:
+        if (cap.sccFlags.d[s] and (flagDead or flagDirty or flagPruned)) == 0:
+          for mi in cap.sccMemStart.d[s] ..< cap.sccMemStart.d[s+1]:
+            let m = cap.sccMembers.d[mi]
+            atomicStoreN(addr cap.recs.d[m].cell.rootIdx,
+                         gMyEpochStamp or (int(cap.ages.d[m]) +% 1),
+                         ATOMIC_RELAXED)
+    else:
+      # no epoch in the stamp: clear them while all cells are still alive
+      for i in 0 ..< cap.recs.len:
+        cap.recs.d[i].cell.rootIdx = 0
+    graceWait()
+    for i in 0 ..< j.toFree.len:
+      when orcLeakDetector:
+        writeCell("CYCLIC OBJECT FREED", j.toFree.d[i][0], j.toFree.d[i][1])
+      free(j.toFree.d[i][0], j.toFree.d[i][1])
+    j.freed = j.toFree.len
+    deinit j.toFree
+
+proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell];
+                     wait: bool; drainAll = false): bool =
+  ## Drain pending RC operations (own stripe; all stripes for a full
+  ## collect) and try to become a collector over THIS THREAD's candidates:
+  ## claim a tag slot — the only step still under gMergeLock — and steal
+  ## the thread-local buffer as this collection's slice, lock-free. When
+  ## there is enough work but all ParSlots collections are running, `wait`
+  ## decides between parking until a slot frees (backpressure for
+  ## overflowing mutators) and giving up. Either way the drain happened,
+  ## so the caller's overflowing queue has room again.
+  result = false
+  if drainAll: drainAllStripes()
+  else: drainStripe(getStripeIdx())
+  adoptOrphans()
+  while gLocalRoots.len >= minRoots and gLocalRoots.len > keepBelow and
+      mayRunCycleCollect():
+    acquire gMergeLock
+    var slot = -1
+    for sl in 0 ..< ParSlots:
+      if atomicLoadN(addr gActiveTags[sl], ATOMIC_RELAXED) == 0:
+        slot = sl
+        break
+    if slot < 0:
+      release gMergeLock
+      if not wait: break
+      # backpressure: all ParSlots collections are running; park until one
+      # finishes (finishCollection broadcasts) instead of burning a core
+      parkUntil(anySlotFree())
+      drainStripe(getStripeIdx())   # the world moved while we waited
+      adoptOrphans()
+    else:
+      gTagCounter = (gTagCounter +% 1) and (epochBase - 1)  # tags below the stamp namespace
+      if gTagCounter == 0: gTagCounter = 1
+      gMyTag = gTagCounter
+      gMySlot = slot
+      gMyEpochStamp = epochStamp(atomicLoadN(addr gEpoch, ATOMIC_RELAXED))
+      var othersActive = false
+      for sl in 0 ..< ParSlots:
+        if sl != slot and atomicLoadN(addr gActiveTags[sl], ATOMIC_RELAXED) != 0:
+          othersActive = true
+      gAmSolo = not othersActive
+      if gAmSolo:
+        atomicStoreN(addr gSoloCapture, 1, ATOMIC_RELEASE)
+      atomicStoreN(addr gSlotPhase[slot], 1, ATOMIC_RELEASE)
+      atomicStoreN(addr gActiveTags[slot], gMyTag, ATOMIC_SEQ_CST)
+      release gMergeLock
+      # our buffer, our slice: no lock needed
+      if keepBelow == 0:
+        slice = gLocalRoots     # steal the whole buffer
+        init(gLocalRoots)
+      else:
+        init(slice, max(gLocalRoots.len - keepBelow, 8))
+        for i in keepBelow ..< gLocalRoots.len:
+          slice.add(gLocalRoots.d[i][0], gLocalRoots.d[i][1])
+        gLocalRoots.len = keepBelow
+      result = true
+      break
+
+proc finishCollection() =
+  if atomicAddFetch(addr gCollectionCounter, 1, ATOMIC_RELAXED) mod YrcEpochLen == 0:
+    discard atomicAddFetch(addr gEpoch, 1, ATOMIC_RELAXED)
+  atomicStoreN(addr gActiveTags[gMySlot], 0, ATOMIC_SEQ_CST)
+  atomicStoreN(addr gSlotPhase[gMySlot], 0, ATOMIC_RELEASE)
+  gMyTag = 0
+  gAmSolo = false
+  collectorEvent()   # wake backpressure and grace waiters
+
+proc collectCyclesImpl(j: var GcEnv; slice: var CellSeq[Cell]) =
+  # All destruction is deferred to collection time: plain rc==0 garbage in
+  # the roots buffer forms singleton SCCs with external count 0 and is freed
+  # by the same machinery as the cycles.
+  let last = slice.len -% 1
+  when logOrc:
+    for i in countdown(last, 0):
+      writeCell("root", slice.d[i][0], slice.d[i][1])
+
+  init j.traceStack
+  prepareCapture()
+  let cap = addr gCap   # hoist the TLS lookup out of the hot loops
+  j.nScc = 0
+
+  for i in countdown(last, 0):
+    capture(slice.d[i][0], slice.d[i][1], j, cap)
+  cap.sccMemStart.add int32(cap.sccMembers.len)   # sentinel
+  j.touched = cap.recs.len
+  atomicStoreN(addr gSlotPhase[gMySlot], 2, ATOMIC_RELEASE)  # capture done
+  if gAmSolo:
+    atomicStoreN(addr gSoloCapture, 0, ATOMIC_RELEASE)
+  collectorEvent()   # wake solo-gate and grace waiters
+
+  # Unregister the processed candidates before computing deadness: only
+  # cells that STAY registered count as externally referenced by the roots
+  # buffer. Doing this before freeing anything also ensures a nested
+  # collectCycles() (triggered from a destructor) cannot access freed cells.
+  for i in 0 ..< slice.len:
+    rcClearFlag(slice.d[i][0], inRootsFlag)
+
+  computeDeadness(j, cap)
+  commitDead(j, cap)
+  j.keepThreshold = j.freed == j.touched and j.touched > 0
+
+  deinit j.traceStack
+
+proc runCollection(j: var GcEnv; slice: var CellSeq[Cell]) =
+  ## Runs one collection over the stolen slice, concurrently with mutators
+  ## AND with up to ParSlots-1 other collections over disjoint partitions.
+  yrcGcFenceEnter()      # freeze seq structure mutations, not ref writes
+  if not gAmSolo:
+    # a solo collection claims with plain stores; nobody else may claim
+    # cells until its capture phase is over
+    parkUntil(atomicLoadN(addr gSoloCapture, ATOMIC_ACQUIRE) == 0)
+  let prev = lockState
+  lockState = Collecting
+  collectCyclesImpl(j, slice)
+  lockState = prev
+  yrcGcFenceExit()
+  finishCollection()
+  deinit slice
 
 when defined(nimOrcStats):
   var freedCyclicObjects {.threadvar.}: int
@@ -415,15 +1221,23 @@ when defined(nimOrcStats):
 proc collectCycles() =
   when logOrc:
     cfprintf(cstderr, "[collectCycles] begin\n")
-  yrcCollectorLock:
-    mergePendingRoots()
-    if roots.len >= rootsThreshold and mayRunCycleCollect():
-      let nRoots = roots.len
-      var j: GcEnv
-      init j.traceStack
-      collectCyclesBacon(j, 0)
-      if roots.len == 0 and roots.d != nil:
-        deinit roots
+  if lockState == Collecting or lockState == HasMutatorLock:
+    # Cannot start a nested collection:
+    #   Collecting — destructor-driven decs during free can fill the
+    #     stripe; re-entering would corrupt collector state. Returning
+    #     without draining used to livelock the enqueue spin.
+    #   HasMutatorLock — becoming a collector would fence-wait on our
+    #     own gSeqActive counter (self-deadlock).
+    # Just make room in the overflowing queue; a later dec outside this
+    # context triggers the actual collection.
+    drainStripe(getStripeIdx())
+    return
+  var slice: CellSeq[Cell]
+  if startCollection(rootsThreshold, 0, slice, wait = true):
+    let nRoots = slice.len
+    var j: GcEnv
+    runCollection(j, slice)
+    block:
       when not defined(nimStressOrc):
         if j.keepThreshold:
           discard
@@ -444,25 +1258,37 @@ proc collectCycles() =
         cfprintf(cstderr, "[collectCycles] end; freed %ld new threshold %ld\n", j.freed, rootsThreshold)
       when defined(nimOrcStats):
         inc freedCyclicObjects, j.freed
-      deinit j.traceStack
 
 when defined(nimOrcStats):
   type
     OrcStats* = object
       freedCyclicObjects*: int
+      regFresh*, regRepeat*, regCross*, regSelf*: int
+      capTotal*, capRepeat*, capPruned*: int
   proc GC_orcStats*(): OrcStats =
-    result = OrcStats(freedCyclicObjects: freedCyclicObjects)
+    # freedCyclicObjects is per-thread; the registration/capture counters
+    # are process-global (instrumentation for the epoch-stamp decision)
+    result = OrcStats(freedCyclicObjects: freedCyclicObjects,
+      regFresh: atomicLoadN(addr gStatRegFresh, ATOMIC_RELAXED),
+      regRepeat: atomicLoadN(addr gStatRegRepeat, ATOMIC_RELAXED),
+      regCross: atomicLoadN(addr gStatRegCross, ATOMIC_RELAXED),
+      regSelf: atomicLoadN(addr gStatRegSelf, ATOMIC_RELAXED),
+      capTotal: atomicLoadN(addr gStatCapTotal, ATOMIC_RELAXED),
+      capRepeat: atomicLoadN(addr gStatCapRepeat, ATOMIC_RELAXED),
+      capPruned: atomicLoadN(addr gStatCapPruned, ATOMIC_RELAXED))
 
 proc GC_runOrc* =
-  yrcCollectorLock:
-    mergePendingRoots()
-    if roots.len > 0 and mayRunCycleCollect():
-      var j: GcEnv
-      init j.traceStack
-      collectCyclesBacon(j, 0)
-      deinit j.traceStack
-      roots.len = 0
-  when logOrc: orcAssert roots.len == 0, "roots not empty!"
+  if lockState == Collecting: return
+  # an explicit collect must be exhaustive: age out every liveness stamp
+  # so nothing is pruned
+  discard atomicAddFetch(addr gEpoch, 1, ATOMIC_RELAXED)
+  var slice: CellSeq[Cell]
+  if startCollection(1, 0, slice, wait = true, drainAll = true):
+    var j: GcEnv
+    runCollection(j, slice)
+  # note: aborted SCCs and cross-collection targets legitimately leave
+  # re-registered roots behind; other RUNNING threads' local candidates
+  # are theirs to collect (exiting threads spill to the orphan buffer)
 
 proc GC_enableOrc*() =
   when not defined(nimStressOrc):
@@ -473,23 +1299,37 @@ proc GC_disableOrc*() =
     rootsThreshold = high(int)
 
 proc GC_prepareOrc*(): int {.inline.} =
-  yrcCollectorLock:
-    mergePendingRoots()
-    result = roots.len
+  drainAllStripes()
+  adoptOrphans()
+  result = gLocalRoots.len
 
 proc GC_partialCollect*(limit: int) =
-  yrcCollectorLock:
-    mergePendingRoots()
-    if roots.len > limit and mayRunCycleCollect():
-      var j: GcEnv
-      init j.traceStack
-      collectCyclesBacon(j, limit)
-      deinit j.traceStack
-      roots.len = limit
+  if lockState == Collecting: return
+  var slice: CellSeq[Cell]
+  if startCollection(limit + 1, limit, slice, wait = true):
+    var j: GcEnv
+    runCollection(j, slice)
 
 proc GC_fullCollect* =
   GC_runOrc()
 
+proc nimYrcThreadTeardown() =
+  ## Called when a thread exits (threadimpl): drain our stripe so nothing
+  ## of ours is stranded in a queue no other thread hashes to, then spill
+  ## our candidate buffer to the global orphan buffer, where the next
+  ## collection on any thread adopts it.
+  drainStripe(getStripeIdx())
+  if gLocalRoots.len > 0:
+    acquire gMergeLock
+    if roots.d == nil: init(roots)
+    for i in 0 ..< gLocalRoots.len:
+      add(roots, gLocalRoots.d[i][0], gLocalRoots.d[i][1])
+    release gMergeLock
+  if gLocalRoots.d != nil:
+    deinit(gLocalRoots)
+    gLocalRoots.d = nil
+    gLocalRoots.len = 0
+
 proc GC_enableMarkAndSweep*() = GC_enableOrc()
 proc GC_disableMarkAndSweep*() = GC_disableOrc()
 
@@ -502,24 +1342,27 @@ else:
   template markedAsCyclic(s: Cell; desc: PNimTypeV2): bool =
     (desc.flags and acyclicFlag) == 0
 
+proc enqueueDec(cell: Cell; desc: PNimTypeV2) {.inline.} =
+  ## LOCK-FREE producer for the deferred-dec queue: reserve a slot with a
+  ## fetch-add, store the cell, then publish by storing the desc (release;
+  ## desc != nil is the ready marker consumers wait for/skip). A reservation
+  ## past QueueSize never writes anything — the reserver makes room by
+  ## draining (collectCycles always at least drains our own stripe, even
+  ## when nested in a collection or a seq critical section) and retries
+  ## with a fresh reservation.
+  let idx = getStripeIdx()
+  while true:
+    let slot = atomicFetchAdd(addr stripes[idx].toDecLen, 1, ATOMIC_ACQ_REL)
+    if slot < QueueSize:
+      stripes[idx].toDec[slot][0] = cell
+      atomicStoreN(addr stripes[idx].toDec[slot][1], desc, ATOMIC_RELEASE)
+      break
+    collectCycles()
+
 proc nimDecRefIsLastCyclicDyn(p: pointer): bool {.compilerRtl, inl.} =
   result = false
   if p != nil:
-    let cell = head(p)
-    let desc = cast[ptr PNimTypeV2](p)[]
-    let idx = getStripeIdx()
-    while true:
-      var overflow = false
-      withLock stripes[idx].lockDec:
-        if stripes[idx].toDecLen < QueueSize:
-          stripes[idx].toDec[stripes[idx].toDecLen] = (cell, desc)
-          stripes[idx].toDecLen += 1
-        else:
-          overflow = true
-      if overflow:
-        collectCycles()
-      else:
-        break
+    enqueueDec(head(p), cast[ptr PNimTypeV2](p)[])
 
 proc nimDecRefIsLastDyn(p: pointer): bool {.compilerRtl, inl.} =
   nimDecRefIsLastCyclicDyn(p)
@@ -527,20 +1370,7 @@ proc nimDecRefIsLastDyn(p: pointer): bool {.compilerRtl, inl.} =
 proc nimDecRefIsLastCyclicStatic(p: pointer; desc: PNimTypeV2): bool {.compilerRtl, inl.} =
   result = false
   if p != nil:
-    let cell = head(p)
-    let idx = getStripeIdx()
-    while true:
-      var overflow = false
-      withLock stripes[idx].lockDec:
-        if stripes[idx].toDecLen < QueueSize:
-          stripes[idx].toDec[stripes[idx].toDecLen] = (cell, desc)
-          stripes[idx].toDecLen += 1
-        else:
-          overflow = true
-      if overflow:
-        collectCycles()
-      else:
-        break
+    enqueueDec(head(p), desc)
 
 proc unsureAsgnRef(dest: ptr pointer, src: pointer) {.inline.} =
   dest[] = src
@@ -553,25 +1383,27 @@ proc yrcDec(tmp: pointer; desc: PNimTypeV2) {.inline.} =
     discard nimDecRefIsLastCyclicDyn(tmp)
 
 proc nimAsgnYrc(dest: ptr pointer; src: pointer; desc: PNimTypeV2) {.compilerRtl.} =
-  ## YRC write barrier for ref copy assignment.
-  ## Holds the mutator read lock for the entire operation so the collector
-  ## cannot run between the incRef and decRef, closing the stale-decRef
-  ## bug. Direct atomic incRef replaces the toInc stripe queue: the
-  ## collector is blocked, so the RC update is immediately visible and correct.
-  acquireMutatorLock()
-  if src != nil: increment head(src)   # direct atomic: no toInc queue needed
-  let tmp = dest[]
-  dest[] = src
-  if tmp != nil: yrcDec(tmp, desc)     # still deferred via toDec for cycle detection
-  releaseMutatorLock()
+  ## YRC write barrier for ref copy assignment. LOCK-FREE: the deferred dec
+  ## of the old value doubles as the snapshot-at-the-beginning log (the
+  ## collector peeks the toDec queues at commit time), and the direct atomic
+  ## incRef of the new value is exactly the rc mutation the collector's
+  ## commit-time rc validation observes.
+  if src != nil: increment head(src)
+  when hasThreadSupport:
+    let tmp = atomicExchangeN(dest, src, ATOMIC_ACQ_REL)
+  else:
+    let tmp = dest[]
+    dest[] = src
+  if tmp != nil: yrcDec(tmp, desc)
 
 proc nimSinkYrc(dest: ptr pointer; src: pointer; desc: PNimTypeV2) {.compilerRtl.} =
   ## YRC write barrier for ref sink (move). No incRef on source.
-  acquireMutatorLock()
-  let tmp = dest[]
-  dest[] = src
+  when hasThreadSupport:
+    let tmp = atomicExchangeN(dest, src, ATOMIC_ACQ_REL)
+  else:
+    let tmp = dest[]
+    dest[] = src
   if tmp != nil: yrcDec(tmp, desc)
-  releaseMutatorLock()
 
 proc nimMarkCyclic(p: pointer) {.compilerRtl, inl.} =
   when optimizedOrc:
@@ -580,12 +1412,10 @@ proc nimMarkCyclic(p: pointer) {.compilerRtl, inl.} =
       h.rc = h.rc or maybeCycle
 
 # Initialize locks at module load.
-# RwLock stripes live in seqs_v2 (gYrcLocks); NumLockStripes is exported from there.
-for i in 0..<NumLockStripes:
-  initRwLock(gYrcLocks[i].lock)
+initLock(gMergeLock)
+initLock(gWaitLock)
+initCond(gWaitCond)
 for i in 0..<NumStripes:
-  when not defined(yrcAtomics) and not defined(nimYrcAtomicIncs):
-    initLock(stripes[i].lockInc)
-  initLock(stripes[i].lockDec)
+  initLock(stripes[i].consumerLock)
 
 {.pop.}
diff --git a/lib/system/yrc_proof.lean b/lib/system/yrc_proof.lean
index 2189f6ddab..e54fd66bec 100644
--- a/lib/system/yrc_proof.lean
+++ b/lib/system/yrc_proof.lean
@@ -1,56 +1,83 @@
 /-
-  YRC Safety Proof (self-contained, no Mathlib)
-  ==============================================
-  Formal model of YRC's key invariant: the cycle collector never frees
-  an object that any mutator thread can reach.
+  YRC Safety Proof — lock-free SATB collector with parallel collections
+  =====================================================================
+  Self-contained, no Mathlib. Checked with Lean 4 (v4.32.0).
 
-  ## Model overview
+  Formal model of the safety arguments behind lib/system/yrc.nim in its
+  current form: lock-free write barrier, optimistic capture / validate /
+  commit, and up to `MaxPar` concurrent collections over disjoint
+  CAS-claimed partitions.
 
-  We model the heap as a set of objects with directed edges (ref fields).
-  Each thread owns a set of *stack roots* — objects reachable from local variables.
-  The write barrier (nimAsgnYrc) does:
-    1. atomic store  dest ← src          (graph is immediately current)
-    2. buffer inc(src)                    (deferred)
-    3. buffer dec(old)                    (deferred)
+  ## What the implementation does (the things we model)
 
-  The collector (under global lock) does:
-    1. Merge all buffered inc/dec into merged RCs
-    2. Trial deletion (markGray): subtract internal edges from merged RCs
-    3. scan: objects with RC ≥ 0 after trial deletion are rescued (scanBlack)
-    4. Free objects that remain white (closed cycles with zero external refs)
+  Write barrier `nimAsgnYrc(dest, src)`:
+    1. direct ATOMIC incRef of src        (rc word mutation, visible to all)
+    2. atomicExchange dest ← src          (graph is immediately current;
+                                           old value read atomically)
+    3. buffer dec(old) in a striped queue (deferred — this queue IS the
+                                           snapshot-at-the-beginning log)
+
+  A collection (any mutator thread can become a collector):
+    1. merge queues into rc words, steal candidate roots  (under gMergeLock)
+    2. CAPTURE: Tarjan SCC traversal; each visited cell is claimed by
+       CAS-ing a collection tag into its spare header word (claimCell);
+       cells claimed by another ACTIVE collection are not traversed
+       (claimCell → -1, deferred via crossPend)
+    3. compute deadness per SCC: ext(S) = sumRefs − internal − deadIn
+    4. VALIDATE at commit: an SCC is freed only if no queue entry mentions
+       a member (dirty check) and every member's rc word is unchanged
+       since capture (recheck) — validateDead
+    5. COMMIT: nil all slots of dead cells, trialDec edges to survivors,
+       wait out concurrent captures (grace period), then free — commitDead
+
+  ## Proof structure
+
+  §1  Heap model, reachability, the core safety theorem.
+  §2  Write barrier: no lost objects.
+  §3  Mutator operational semantics and GARBAGE STABILITY: a closed
+      (externally unreferenced) set stays closed under every mutator step,
+      allocation, and foreign frees. This is why optimistic
+      capture/validate/commit is sound and why aborts cost nothing.
+  §4  Commit validation arithmetic: validated ext(D) = 0 implies D is
+      closed; corollary CROSS-TARGET LIVENESS — a cell referenced from
+      outside a collection's partition is never freed by that collection.
+  §5  Tag uniqueness and partition disjointness for parallel collections.
+  §6  Grace period: no capture ever dereferences a freed cell.
+  §7  The asymmetric seq/GC fence (seqs_v2.nim): Dekker-style mutual
+      exclusion between seq structure mutations and collections.
+  §8  Deadlock freedom for the remaining locks (gMergeLock + stripes) and
+      the spin-wait ordering argument.
 -/
 
 -- Objects and threads are just natural numbers for simplicity.
 abbrev Obj := Nat
 abbrev Thread := Nat
 
-/-! ### State -/
+/-! ## §1 Heap model and reachability -/
 
-/-- The state of the heap and collector at a point in time. -/
+/-- The state of the heap at a point in time. -/
 structure State where
-  /-- Physical heap edges: `edges x y` means object `x` has a ref field pointing to `y`.
-      Always up-to-date (atomic stores). -/
+  /-- Physical heap edges: `edges x y` means object `x` has a ref field
+      pointing to `y`. Always up-to-date (atomic stores/exchanges). -/
   edges : Obj → Obj → Prop
-  /-- Stack roots per thread. `roots t x` means thread `t` has a local variable pointing to `x`. -/
+  /-- Stack roots per thread: local variables and the shared candidate
+      roots buffer (both are "external" to any captured subgraph). -/
   roots : Thread → Obj → Prop
-  /-- Pending buffered increments (not yet merged). -/
-  pendingInc : Obj → Nat
-  /-- Pending buffered decrements (not yet merged). -/
-  pendingDec : Obj → Nat
+  /-- Live allocations. The allocator hands out only unallocated objects;
+      captured cells stay allocated until their collection frees them. -/
+  allocated : Obj → Prop
 
-/-! ### Reachability -/
-
-/-- An object is *reachable* if some thread can reach it via stack roots + heap edges. -/
+/-- An object is *reachable* if some thread can reach it via stack roots
+    plus heap edges. -/
 inductive Reachable (s : State) : Obj → Prop where
   | root (t : Thread) (x : Obj) : s.roots t x → Reachable s x
   | step (x y : Obj) : Reachable s x → s.edges x y → Reachable s y
 
-/-- Directed reachability between heap objects (following physical edges only). -/
+/-- Directed reachability following physical heap edges only. -/
 inductive HeapReachable (s : State) : Obj → Obj → Prop where
   | refl (x : Obj) : HeapReachable s x x
   | step (x y z : Obj) : HeapReachable s x y → s.edges y z → HeapReachable s x z
 
-/-- If a root reaches `r` and `r` heap-reaches `x`, then `x` is Reachable. -/
 theorem heapReachable_of_reachable (s : State) (r x : Obj)
     (hr : Reachable s r) (hp : HeapReachable s r x) :
     Reachable s x := by
@@ -58,70 +85,62 @@ theorem heapReachable_of_reachable (s : State) (r x : Obj)
   | refl => exact hr
   | step _ _ _ hedge ih => exact Reachable.step _ _ ih hedge
 
-/-! ### What the collector frees -/
-
-/-- An object has an *external reference* if some thread's stack roots point to it. -/
+/-- An object has an *external reference* if some thread points to it. -/
 def hasExternalRef (s : State) (x : Obj) : Prop :=
   ∃ t, s.roots t x
 
-/-- An object is *externally anchored* if it is heap-reachable from some
-    object that has an external reference. This is what scanBlack computes:
-    it starts from objects with trialRC ≥ 0 (= has external refs) and traces
-    the current physical graph. -/
+/-- Externally anchored: heap-reachable from an externally referenced
+    object. This is what deadness computation + survivor rescue computes. -/
 def anchored (s : State) (x : Obj) : Prop :=
   ∃ r, hasExternalRef s r ∧ HeapReachable s r x
 
-/-- The collector frees `x` only if `x` is *not anchored*:
-    no external ref, and not reachable from any externally-referenced object.
-    This models: after trial deletion, x remained white, and scanBlack
-    didn't rescue it. -/
+/-- The collector frees `x` only if `x` is not anchored. -/
 def collectorFrees (s : State) (x : Obj) : Prop :=
   ¬ anchored s x
 
-/-! ### Main safety theorem -/
-
-/-- **Lemma**: Every reachable object is anchored.
-    If thread `t` reaches `x`, then there is a chain from a stack root
-    (which has an external ref) through heap edges to `x`. -/
+/-- Every reachable object is anchored. -/
 theorem reachable_is_anchored (s : State) (x : Obj)
     (h : Reachable s x) : anchored s x := by
   induction h with
   | root t x hroot =>
     exact ⟨x, ⟨t, hroot⟩, HeapReachable.refl x⟩
-  | step a b h_reach_a h_edge ih =>
+  | step a b _ h_edge ih =>
     obtain ⟨r, h_ext_r, h_path_r_a⟩ := ih
     exact ⟨r, h_ext_r, HeapReachable.step r a b h_path_r_a h_edge⟩
 
-/-- **Main Safety Theorem**: If the collector frees `x`, then no thread
-    can reach `x`. Freed objects are unreachable.
-
-    This is the contrapositive of `reachable_is_anchored`. -/
+/-- **Core Safety Theorem**: freed objects are unreachable. -/
 theorem yrc_safety (s : State) (x : Obj)
     (h_freed : collectorFrees s x) : ¬ Reachable s x := by
   intro h_reach
   exact h_freed (reachable_is_anchored s x h_reach)
 
-/-! ### The write barrier preserves reachability -/
+/-! ## §2 The write barrier
 
-/-- Model of `nimAsgnYrc(dest_field_of_a, src)`:
-    Object `a` had a field pointing to `old`, now points to `src`.
-    Graph update is immediate. The new edge takes priority (handles src = old). -/
+  `nimAsgnYrc` performs the atomic inc of `src` BEFORE the exchange, so
+  there is no instant at which the edge `a → src` exists without src's rc
+  accounting for it; and the exchange reads `old` atomically, so two
+  racing barriers on the same slot can never both dec the same old value.
+  The dec of `old` is deferred: until the next merge, old's rc is merely
+  inflated — always conservative. -/
+
+/-- Model of `nimAsgnYrc(field a, src)`: `a`'s field pointed to `old`,
+    now points to `src`. The graph update is immediate (atomicExchange). -/
 def writeBarrier (s : State) (a old src : Obj) : State :=
   { s with
     edges := fun x y =>
       if x = a ∧ y = src then True
       else if x = a ∧ y = old then False
-      else s.edges x y
-    pendingInc := fun x => if x = src then s.pendingInc x + 1 else s.pendingInc x
-    pendingDec := fun x => if x = old then s.pendingDec x + 1 else s.pendingDec x }
+      else s.edges x y }
 
-/-- **No Lost Object Theorem**: If thread `t` holds a stack ref to `a` and
-    executes `a.field = b` (replacing old), then `b` is reachable afterward.
+/-- Overwriting a slot with nil: only removes an edge. -/
+def storeNil (s : State) (a old : Obj) : State :=
+  { s with
+    edges := fun x y =>
+      if x = a ∧ y = old then False else s.edges x y }
 
-    This is why the "lost object" problem from concurrent GC literature
-    doesn't arise in YRC: the atomic store makes `a→b` visible immediately,
-    and `a` is anchored (thread `t` holds it), so scanBlack traces `a→b`
-    and rescues `b`. -/
+/-- **No Lost Object**: if thread `t` holds `a` and stores `a.f = b`,
+    then `b` is reachable afterwards — the exchange publishes the edge
+    atomically, so a concurrent collection's survivor rescue traces it. -/
 theorem no_lost_object (s : State) (t : Thread) (a old b : Obj)
     (h_root_a : s.roots t a) :
     Reachable (writeBarrier s a old b) b := by
@@ -129,225 +148,597 @@ theorem no_lost_object (s : State) (t : Thread) (a old b : Obj)
   · exact Reachable.root t a h_root_a
   · simp [writeBarrier]
 
-/-! ### Non-atomic write barrier window safety
+/-! ## §3 Mutator semantics and garbage stability
 
-  The write barrier does three steps non-atomically:
-    1. atomicStore(dest, src)     — graph update
-    2. buffer inc(src)            — deferred
-    3. buffer dec(old)            — deferred
+  The heart of optimistic capture/validate/commit is the *garbage
+  stability theorem*: a set with no external references cannot acquire
+  one later, because mutators can only copy references they can reach.
+  Hence a dead set that VALIDATES at commit time stays dead through the
+  grace window and until the actual `free` calls — no re-validation is
+  needed, and an aborted (dirty) capture merely wasted its own work.
 
-  If the collector runs between steps 1 and 2 (inc not yet buffered):
-  - src has a new incoming heap edge not yet reflected in RCs
-  - But src is reachable from the mutator's stack (mutator held a ref to store it)
-  - So src has an external ref → trialRC ≥ 1 → scanBlack rescues src ✓
+  Every constructor's precondition encodes the fundamental capability
+  restriction: to use a reference you must hold it. `P` is the set of
+  cells protected from foreign frees (in yrc: cells stamped with an
+  active tag are never freed by another collection — §5). -/
 
-  If the collector runs between steps 2 and 3 (dec not yet buffered):
-  - old's RC is inflated by 1 (the dec hasn't arrived)
-  - This is conservative: old appears to have more refs than it does
-  - Trial deletion won't spuriously free it ✓
--/
+def addRoot (s : State) (t : Thread) (x : Obj) : State :=
+  { s with roots := fun t' y => (t' = t ∧ y = x) ∨ s.roots t' y }
 
-/-- Model the state between steps 1-2: graph updated, inc not yet buffered.
-    `src` has new edge but RC doesn't reflect it yet. -/
-def stateAfterStore (s : State) (a old src : Obj) : State :=
+def delRoot (s : State) (t : Thread) (x : Obj) : State :=
+  { s with roots := fun t' y => if t' = t ∧ y = x then False else s.roots t' y }
+
+def allocObj (s : State) (t : Thread) (x : Obj) : State :=
   { s with
-    edges := fun x y =>
-      if x = a ∧ y = src then True
-      else if x = a ∧ y = old then False
-      else s.edges x y }
+    roots := fun t' y => (t' = t ∧ y = x) ∨ s.roots t' y
+    allocated := fun y => y = x ∨ s.allocated y }
 
-/-- Even in the window between atomic store and buffered inc,
-    src is still reachable (from the mutator's stack via a→src). -/
-theorem src_reachable_in_window (s : State) (t : Thread) (a old src : Obj)
-    (h_root_a : s.roots t a) :
-    Reachable (stateAfterStore s a old src) src := by
-  apply Reachable.step a src
-  · exact Reachable.root t a h_root_a
-  · simp [stateAfterStore]
+def freeObj (s : State) (x : Obj) : State :=
+  { s with
+    edges := fun u v => if u = x ∨ v = x then False else s.edges u v
+    allocated := fun y => if y = x then False else s.allocated y }
 
-/-- Therefore src is anchored in the window → collector won't free it. -/
-theorem src_safe_in_window (s : State) (t : Thread) (a old src : Obj)
-    (h_root_a : s.roots t a) :
-    ¬ collectorFrees (stateAfterStore s a old src) src := by
-  intro h_freed
-  exact h_freed (reachable_is_anchored _ _ (src_reachable_in_window s t a old src h_root_a))
+/-- One step of the concurrent system, as seen by a fixed observer
+    protecting the cell set `P`. -/
+inductive MutStep (P : Obj → Prop) (s : State) : State → Prop where
+  /-- `a.f = src`: the mutator must hold refs to `a` and `src`. -/
+  | write (a old src : Obj)
+      (ha : Reachable s a) (hsrc : Reachable s src) :
+      MutStep P s (writeBarrier s a old src)
+  /-- `a.f = nil`. -/
+  | writeNil (a old : Obj) (ha : Reachable s a) :
+      MutStep P s (storeNil s a old)
+  /-- Copy a reachable ref into a local / the roots buffer. -/
+  | rootCopy (t : Thread) (x : Obj) (hx : Reachable s x) :
+      MutStep P s (addRoot s t x)
+  /-- Drop a local ref (scope exit, roots-buffer unregistration). -/
+  | rootDrop (t : Thread) (x : Obj) :
+      MutStep P s (delRoot s t x)
+  /-- Allocate: the allocator returns only unallocated addresses. -/
+  | alloc (t : Thread) (x : Obj) (hfresh : ¬ s.allocated x) :
+      MutStep P s (allocObj s t x)
+  /-- A DIFFERENT collection frees one of its own dead cells: it is
+      unreachable (its own §1 safety) and not protected (§5 partition
+      disjointness: it carries the other collection's tag, not ours). -/
+  | foreignFree (x : Obj) (hunreach : ¬ Reachable s x) (hprot : ¬ P x) :
+      MutStep P s (freeObj s x)
 
-/-! ### Deadlock freedom
+/-- Reflexive-transitive closure: an arbitrary interleaving of steps by
+    all mutators and all other collections. -/
+inductive MutSteps (P : Obj → Prop) (s : State) : State → Prop where
+  | refl : MutSteps P s s
+  | tail {s' s'' : State} :
+      MutSteps P s s' → MutStep P s' s'' → MutSteps P s s''
 
-  YRC uses three classes of locks:
-    • gYrcGlobalLock           (level 0)
-    • stripes[i].lockInc       (level 2*i + 1,  for i in 0..N-1)
-    • stripes[i].lockDec       (level 2*i + 2,  for i in 0..N-1)
+/-- `S` is *closed*: no thread points into it and no heap edge enters it
+    from outside. This is exactly "validated dead set" (§4). -/
+def closed (s : State) (S : Obj → Prop) : Prop :=
+  (∀ t x, S x → ¬ s.roots t x) ∧
+  (∀ u v, S v → s.edges u v → S u)
 
-  Total order:  global < lockInc[0] < lockDec[0] < lockInc[1] < lockDec[1] < ...
+/-- Members of a closed set are unreachable. -/
+theorem closed_unreachable (s : State) (S : Obj → Prop)
+    (h : closed s S) : ∀ x, Reachable s x → ¬ S x := by
+  intro x hr
+  induction hr with
+  | root t x hroot => exact fun hS => h.1 t x hS hroot
+  | step a b _ hedge ih => exact fun hS => ih (h.2 a b hS hedge)
 
-  Every code path in yrc.nim acquires locks in strictly ascending level order:
+/-- The invariant carried through the grace window: `S` closed and all
+    members still allocated (their memory has not been reused). -/
+def DeadInv (s : State) (S : Obj → Prop) : Prop :=
+  closed s S ∧ ∀ x, S x → s.allocated x
 
-  **nimIncRefCyclic** (mutator fast path):
-    acquire lockInc[myStripe] → release → done.
-    Holds exactly one lock. ✓
+/-- **One-step stability**: no single action of any mutator, allocator or
+    other collection can break the invariant of a closed set. -/
+theorem step_preserves_deadInv (s s' : State) (S : Obj → Prop)
+    (hinv : DeadInv s S) (hstep : MutStep S s s') : DeadInv s' S := by
+  obtain ⟨hcl, halloc⟩ := hinv
+  cases hstep with
+  | write a old src ha hsrc =>
+    refine ⟨⟨fun t x hS hroot => hcl.1 t x hS hroot, ?_⟩, fun x hS => halloc x hS⟩
+    intro u v hSv hedge
+    simp only [writeBarrier] at hedge
+    by_cases h1 : u = a ∧ v = src
+    · exact absurd (h1.2 ▸ hSv) (closed_unreachable s S hcl src hsrc)
+    · by_cases h2 : u = a ∧ v = old
+      · -- corner case old = src: the "remove old" branch is overridden
+        -- by the "add src" branch, so the edge survives — but then
+        -- v = old = src is reachable, hence not in S
+        simp [h2] at hedge
+        have hSsrc : S src := by rw [← hedge, ← h2.2]; exact hSv
+        exact absurd hSsrc (closed_unreachable s S hcl src hsrc)
+      · simp [h1, h2] at hedge
+        exact hcl.2 u v hSv hedge
+  | writeNil a old ha =>
+    refine ⟨⟨fun t x hS hroot => hcl.1 t x hS hroot, ?_⟩, fun x hS => halloc x hS⟩
+    intro u v hSv hedge
+    simp only [storeNil] at hedge
+    by_cases h2 : u = a ∧ v = old
+    · simp [h2] at hedge
+    · simp [h2] at hedge
+      exact hcl.2 u v hSv hedge
+  | rootCopy t x hx =>
+    refine ⟨⟨?_, fun u v hSv hedge => hcl.2 u v hSv hedge⟩, fun y hS => halloc y hS⟩
+    intro t' y hSy hroot
+    simp only [addRoot] at hroot
+    cases hroot with
+    | inl h => exact absurd (h.2 ▸ hSy) (closed_unreachable s S hcl x hx)
+    | inr h => exact hcl.1 t' y hSy h
+  | rootDrop t x =>
+    refine ⟨⟨?_, fun u v hSv hedge => hcl.2 u v hSv hedge⟩, fun y hS => halloc y hS⟩
+    intro t' y hSy hroot
+    simp only [delRoot] at hroot
+    by_cases h : t' = t ∧ y = x
+    · simp [h] at hroot
+    · simp [h] at hroot
+      exact hcl.1 t' y hSy hroot
+  | alloc t x hfresh =>
+    refine ⟨⟨?_, fun u v hSv hedge => hcl.2 u v hSv hedge⟩, ?_⟩
+    · intro t' y hSy hroot
+      simp only [allocObj] at hroot
+      cases hroot with
+      | inl h => exact hfresh (h.2 ▸ halloc y hSy)
+      | inr h => exact hcl.1 t' y hSy h
+    · intro y hS
+      simp only [allocObj]
+      exact Or.inr (halloc y hS)
+  | foreignFree x hunreach hprot =>
+    refine ⟨⟨fun t y hSy hroot => hcl.1 t y hSy hroot, ?_⟩, ?_⟩
+    · intro u v hSv hedge
+      simp only [freeObj] at hedge
+      by_cases h : u = x ∨ v = x
+      · simp [h] at hedge
+      · simp [h] at hedge
+        exact hcl.2 u v hSv hedge
+    · intro y hSy
+      simp only [freeObj]
+      have hyx : ¬ y = x := fun he => hprot (he ▸ hSy)
+      simp [hyx]
+      exact halloc y hSy
 
-  **nimIncRefCyclic** (overflow path):
-    acquire gYrcGlobalLock (level 0), then for i=0..N-1: acquire lockInc[i] → release.
-    Ascending: 0 < 1 < 3 < 5 < ... ✓
+/-- **Garbage Stability Theorem**: once a set is closed, it stays closed
+    (and unreusable) under any interleaving of concurrent activity. -/
+theorem deadInv_stable (s s' : State) (S : Obj → Prop)
+    (hinv : DeadInv s S) (hsteps : MutSteps S s s') : DeadInv s' S := by
+  induction hsteps with
+  | refl => exact hinv
+  | tail _ hstep ih => exact step_preserves_deadInv _ _ S ih hstep
 
-  **nimDecRefIsLastCyclic{Dyn,Static}** (fast path):
-    acquire lockDec[myStripe] → release → done.
-    Holds exactly one lock. ✓
+/-- Snapshot garbage cannot be resurrected: members of a set that was
+    closed at commit time are unreachable at every later point. -/
+theorem garbage_stability (s s' : State) (S : Obj → Prop)
+    (hinv : DeadInv s S) (hsteps : MutSteps S s s') :
+    ∀ x, S x → ¬ Reachable s' x := by
+  intro x hS hr
+  exact closed_unreachable s' S (deadInv_stable s s' S hinv hsteps).1 x hr hS
 
-  **nimDecRefIsLastCyclic{Dyn,Static}** (overflow path):
-    calls collectCycles → acquire gYrcGlobalLock (level 0),
-    then mergePendingRoots which for i=0..N-1:
-      acquire lockInc[i] → release, acquire lockDec[i] → release.
-    Ascending: 0 < 1 < 2 < 3 < 4 < ... ✓
+/-- **Commit-then-free safety**: if the dead set validated (was closed)
+    at commit time, then freeing its members after ANY amount of further
+    concurrent activity (the grace window, other collections' frees,
+    destructor-driven mutations) satisfies the §1 free condition. -/
+theorem commit_free_safe (s s' : State) (S : Obj → Prop)
+    (hinv : DeadInv s S) (hsteps : MutSteps S s s') :
+    ∀ x, S x → collectorFrees s' x := by
+  intro x hS hanch
+  obtain ⟨r, ⟨t, hroot⟩, hpath⟩ := hanch
+  have hr : Reachable s' x :=
+    heapReachable_of_reachable s' r x (Reachable.root t r hroot) hpath
+  exact closed_unreachable s' S (deadInv_stable s s' S hinv hsteps).1 x hr hS
 
-  **collectCycles / GC_runOrc** (collector):
-    acquire gYrcGlobalLock (level 0),
-    then mergePendingRoots (same ascending pattern as above). ✓
+/-! ## §4 Commit validation arithmetic
 
-  **nimAsgnYrc / nimSinkYrc** (write barrier):
-    Calls nimIncRefCyclic then nimDecRefIsLastCyclic*.
-    Each call acquires and releases its lock independently.
-    No nesting between the two calls. ✓
+  `computeDeadness` marks an SCC dead when
+      ext(S) = sumRefs(S) − internal(S) − deadIn(S) = 0,
+  i.e. summed over the whole dead set D (union of dead SCCs):
+      Σ_{c∈D} rc(c) = #(edges within D).
+  `validateDead` then establishes that the captured rc words are the
+  COMMIT-TIME rc values (rc recheck) and that no unmerged queue entry
+  mentions a member (dirty check via markDirtyFromQueues — the deferred
+  dec queues double as the SATB log; direct incs are atomic rc mutations
+  caught by the recheck). Under yrc's invariant "rc counts every
+  reference: heap slots, stack refs, and the roots-buffer flag" (the
+  roots-buffer refs are excluded by clearing inRootsFlag on the slice
+  BEFORE computeDeadness — collectCyclesImpl), we get: every member's rc
+  splits into internal references (from D) and external ones, and the
+  totals matching forces every external count to zero. -/
 
-  Since every path follows the total order, deadlock is impossible.
--/
+theorem sum_map_split (l : List Obj) (f g h : Obj → Nat)
+    (hp : ∀ c, c ∈ l → f c = g c + h c) :
+    (l.map f).sum = (l.map g).sum + (l.map h).sum := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    have ha : f a = g a + h a := hp a (by simp)
+    have ih' := ih (fun c hc => hp c (List.mem_cons_of_mem a hc))
+    simp only [List.map_cons, List.sum_cons]
+    omega
 
-/-- Lock levels in YRC. Each lock maps to a unique natural number. -/
+theorem sum_zero_all (l : List Nat) (h : l.sum = 0) :
+    ∀ x, x ∈ l → x = 0 := by
+  induction l with
+  | nil => intro x hx; cases hx
+  | cons a l ih =>
+    simp only [List.sum_cons] at h
+    intro x hx
+    cases List.mem_cons.mp hx with
+    | inl he => subst he; omega
+    | inr hm => exact ih (by omega) x hm
+
+/-- **Validation soundness (arithmetic)**: if every member's commit-time
+    rc splits as internal + external, and the collector's check
+    Σ rc = Σ internal passed, then no member has any external ref. -/
+theorem validated_no_external
+    (members : List Obj) (rc inD extIn : Obj → Nat)
+    (h_exact : ∀ c, c ∈ members → rc c = inD c + extIn c)
+    (h_check : (members.map rc).sum = (members.map inD).sum) :
+    ∀ c, c ∈ members → extIn c = 0 := by
+  have hsplit := sum_map_split members rc inD extIn h_exact
+  have hzero : (members.map extIn).sum = 0 := by omega
+  intro c hc
+  exact sum_zero_all _ hzero (extIn c) (List.mem_map_of_mem hc)
+
+/-- **Validated implies closed**: bridging the counts to the graph. The
+    two counting premises say what `extIn` MEANS: any stack/root ref and
+    any heap edge from a non-member contributes at least one external
+    count (this is the rc-exactness established by merge + validate). -/
+theorem validated_closed (s : State) (D : Obj → Prop)
+    (members : List Obj) (extIn : Obj → Nat)
+    (hmem : ∀ x, D x → x ∈ members)
+    (h_roots_counted : ∀ t c, D c → s.roots t c → 1 ≤ extIn c)
+    (h_edges_counted : ∀ u c, D c → ¬ D u → s.edges u c → 1 ≤ extIn c)
+    (h_zero : ∀ c, c ∈ members → extIn c = 0) :
+    closed s D := by
+  constructor
+  · intro t x hD hroot
+    have h1 := h_roots_counted t x hD hroot
+    have h2 := h_zero x (hmem x hD)
+    omega
+  · intro u v hD hedge
+    by_cases hu : D u
+    · exact hu
+    · have h1 := h_edges_counted u v hD hu hedge
+      have h2 := h_zero v (hmem v hD)
+      omega
+
+/-! ## §5 Parallel collections: tags, partitions, cross-target liveness -/
+
+/-- Tags are issued from a monotonic counter under gMergeLock
+    (startCollection). Distinct issue times give distinct tags, so a
+    stale stamp from a finished collection can never be mistaken for a
+    different active collection's tag. (The implementation wraps the
+    counter at 2³¹; the model assumes no wrap-around while a tag is
+    active — an ABA that would need 2³¹ collections to complete during
+    one collection's lifetime.) -/
+theorem tags_distinct (issue : Nat → Nat)
+    (hmono : ∀ i j, i < j → issue i < issue j) :
+    ∀ i j, issue i = issue j → i = j := by
+  intro i j heq
+  cases Nat.lt_trichotomy i j with
+  | inl h => have := hmono i j h; omega
+  | inr h =>
+    cases h with
+    | inl h => exact h
+    | inr h => have := hmono j i h; omega
+
+/-- Each cell's header stores ONE stamp (claimCell CASes the whole
+    word), so two active collections with distinct tags claim disjoint
+    partitions. -/
+theorem partitions_disjoint (stamp : Obj → Nat) (tagA tagB : Nat)
+    (hne : tagA ≠ tagB) :
+    ∀ x, stamp x = tagA → stamp x = tagB → False := by
+  intro x hA hB
+  exact hne (hA ▸ hB)
+
+/-- **Cross-target liveness**: a cell claimed by collection B but
+    referenced from OUTSIDE B's partition is never in B's dead set.
+    B's internal count for the cell only includes edges from B's dead
+    members; the foreign edge contributes an external count, and
+    validation forces external counts to zero — so the cell's SCC fails
+    the deadness check (equivalently: it is demoted). This is why
+    claimCell may simply refuse foreign-claimed cells (return -1) and
+    crossPend defer them: their owner provably keeps them alive this
+    round, and re-registration makes them candidates for the next. -/
+theorem cross_target_live (D : Obj → Prop) (claimedB : Obj → Prop)
+    (members : List Obj) (extIn : Obj → Nat)
+    (s : State)
+    (hDsub : ∀ x, D x → claimedB x)
+    (hmem : ∀ x, D x → x ∈ members)
+    (h_edges_counted : ∀ u c, D c → ¬ D u → s.edges u c → 1 ≤ extIn c)
+    (h_zero : ∀ c, c ∈ members → extIn c = 0)
+    (u c : Obj) (hedge : s.edges u c) (hu : ¬ claimedB u) :
+    ¬ D c := by
+  intro hDc
+  have hDu : ¬ D u := fun h => hu (hDsub u h)
+  have h1 := h_edges_counted u c hDc hDu hedge
+  have h2 := h_zero c (hmem c hDc)
+  omega
+
+/-! ## §6 The grace period
+
+  A concurrent capture holds raw `(slot, value)` snapshots (TraceEntry);
+  the value pointer is dereferenced later (header read in claimCell). A
+  capture that overlapped our validation may have snapshotted a slot
+  that USED to point into our dead set. commitDead therefore waits, for
+  every other slot that is in capture phase (gSlotPhase == 1), until
+  that capture ends — captures never wait on anyone, so this is bounded.
+
+  Two obligations:
+  (a) captures that started BEFORE our commit are waited out — temporal
+      argument below (`grace_no_use_after_free`);
+  (b) captures that start AT/AFTER our commit never snapshot a dead
+      cell in the first place (`post_commit_snap_misses_dead`): they
+      only read slots of cells they claim; our dead cells carry our
+      still-active tag, so claimCell refuses them (never traversed),
+      and no slot OUTSIDE the dead set points into it (closedness, held
+      through the window by §3 stability). -/
+
+/-- Any snapshot value read by a post-commit capture comes from a slot
+    of a cell that capture claimed; claimed cells are never dead cells
+    of another active collection (§5), and the dead set is closed. -/
+theorem post_commit_snap_misses_dead (s : State)
+    (D claimedC snap : Obj → Prop)
+    (hdisj : ∀ x, claimedC x → ¬ D x)
+    (hclosed : closed s D)
+    (hsnap : ∀ v, snap v → ∃ u, claimedC u ∧ s.edges u v) :
+    ∀ v, D v → ¬ snap v := by
+  intro v hD hs
+  obtain ⟨u, hu, he⟩ := hsnap v hs
+  exact hdisj u hu (hclosed.2 u v hD he)
+
+/-- One concurrent capture, with its interval in a global time order and
+    the set of values it ever snapshots. `derefs x t` = the capture
+    reads x's header at time t (always within its interval, always on a
+    snapshotted value). -/
+structure CaptureWindow where
+  start : Nat
+  finish : Nat
+  snap : Obj → Prop
+  derefs : Obj → Nat → Prop
+
+/-- **Grace safety**: no capture dereferences a dead cell at or after
+    its free time. `commitT` is when the dead set validated; `freeT` is
+    when commitDead's free loop runs. The premises are exactly the
+    protocol: (grace) commitDead's spin means any capture that started
+    before commit has finished before we free; (miss) §6(b) above. -/
+theorem grace_no_use_after_free
+    (C : CaptureWindow) (D : Obj → Prop) (commitT freeT : Nat)
+    (h_deref : ∀ x t, C.derefs x t → C.start ≤ t ∧ t ≤ C.finish ∧ C.snap x)
+    (h_grace : C.start < commitT → C.finish < freeT)
+    (h_miss : commitT ≤ C.start → ∀ x, D x → ¬ C.snap x) :
+    ∀ x t, D x → C.derefs x t → t < freeT := by
+  intro x t hD hd
+  obtain ⟨h1, h2, h3⟩ := h_deref x t hd
+  cases Nat.lt_or_ge C.start commitT with
+  | inl h => have := h_grace h; omega
+  | inr h => exact absurd h3 (h_miss h x hD)
+
+/-! ## §7 The asymmetric seq/GC fence (seqs_v2.nim)
+
+  Seq structure mutations (which may FREE the old buffer on realloc)
+  must not overlap a collection, but seq-vs-seq and collection-vs-
+  collection may run concurrently. The committed fence:
+
+    mutator (acquireMutatorLock):    collector (yrcGcFenceEnter):
+      1. FetchAdd gSeqActive[s] SC     1. FetchAdd gGcActive  SC
+      2. Load gGcActive        SC      2. Load gSeqActive[s]  SC (each s)
+      proceed iff it read 0            proceed when all read 0
+      (else back off: FetchSub, spin, retry)
+
+  Under sequential consistency all four operations occupy positions in
+  one total order. Suppose both sides are in their critical sections
+  simultaneously (neither has executed its matching FetchSub). The
+  mutator read gGcActive = 0 AFTER its own inc: since the collector's
+  inc precedes its critical section and no dec intervened, the
+  collector's inc must be ordered after the mutator's read — and
+  symmetrically for the collector's read. That yields a cycle in the
+  total order: -/
+
+theorem fence_mutual_exclusion
+    (mutInc mutChk gcInc gcChk : Nat)  -- positions in the SC total order
+    (h_mut_po : mutInc < mutChk)       -- program order, mutator
+    (h_gc_po : gcInc < gcChk)          -- program order, collector
+    (h_mut_read0 : mutChk < gcInc)     -- mutator read gGcActive = 0
+    (h_gc_read0 : gcChk < mutInc) :    -- collector read counter = 0
+    False := by omega
+
+/-! ## §8 Deadlock freedom
+
+  ### Locks
+
+  The queue producers went lock-free (reserve a slot by fetch-add, then
+  publish it: incs with an RMW exchange — the validation peek must see
+  every completed inc barrier — decs with a release store of the desc,
+  self-protecting via the unexplained rc surplus). The validation peek
+  is lock-free too. What remains:
+    • gMergeLock                (level 0: tag-slot claim + orphan roots)
+    • stripes[i].consumerLock   (level i + 1,  i in 0..N-1: excludes
+                                 DRAINS of the same stripe against each
+                                 other — drains wait out the two-store
+                                 publication window and close each batch
+                                 with a CAS, so no producer coordination
+                                 is needed)
+    • gWaitLock                 (leaf: pairs gWaitCond's wait/broadcast;
+                                 only ever held around a predicate check,
+                                 a wait(), or a broadcast() — never while
+                                 acquiring any other lock, and no other
+                                 lock is held when it is taken)
+
+  Total order:  gMergeLock < consumerLock[0] < consumerLock[1] < ...
+
+  In fact the current paths never HOLD two of these at once — strictly
+  stronger than the ascending-order requirement the theorem needs:
+
+  **nimIncRefCyclic / nimAsgnYrc / nimSinkYrc / enqueueDec /
+    registerLocal / markDirtyFromQueues**: lock-free, no locks at all;
+    enqueueDec's overflow calls collectCycles with nothing held. ✓
+  **drainStripe**: consumerLock[i] alone; the processing inside
+    (trialDec, registerLocal into the thread-local buffer) takes no
+    lock. drainAllStripes: consumerLock[i] ascending, released between
+    stripes. ✓
+  **startCollection / nimYrcThreadTeardown**: drain first (consumerLock,
+    released), THEN gMergeLock for the slot claim / orphan spill —
+    sequential, never nested. adoptOrphans: gMergeLock alone. ✓
+  **validateDead / commitDead**: no locks (candidate re-registration is
+    the lock-free registerLocal). ✓
+
+  ### Blocking waits (parked on gWaitCond after a bounded spin)
+
+    W1 backpressure (startCollection): waits for a free tag slot —
+       gMergeLock is RELEASED first; slots free when collections finish
+       (finishCollection broadcasts).
+    W2 solo gate (runCollection): a non-solo collection waits for
+       gSoloCapture = 0 — cleared when the solo collection's CAPTURE
+       ends (collectCyclesImpl broadcasts), before its commit.
+    W3 grace (commitDead): waits for other slots to leave capture phase
+       (broadcast at the phase 1→2 transition and at finish).
+    W4 fence (yrcGcFenceEnter): spins for in-flight seq ops — each is a
+       short critical section that never blocks (releaseMutatorLock is
+       a plain FetchSub).
+
+  W1–W3 park on gWaitCond: the waiter re-checks its predicate under
+  gWaitLock before sleeping, and every state transition that can make a
+  predicate true (capture-end, collection-finish) broadcasts under the
+  same lock — so a transition either happens before the re-check (the
+  waiter never sleeps) or after it (the waiter is inside wait() and is
+  woken). No missed wakeups, and the wait-for structure is unchanged.
+
+  No wait cycle exists: order the blocking conditions by what they wait
+  FOR. A capture phase terminates unconditionally (finite traversal, no
+  waits inside — claimCell returns -1 immediately on contention). W2
+  waits only on a capture; W3 waits only on captures; a collection
+  executes W2 BEFORE its own capture and W3 AFTER it, so "X waits (W2)
+  on S's capture" and "S waits (W3) on X's capture" cannot hold
+  simultaneously: S clears gSoloCapture before entering commit, so by
+  the time S is in W3, X has passed W2. W1 waits on full collections,
+  which terminate because W2/W3/W4 do. Formally, the lock part is the
+  same ascending-order argument as before: -/
+
+/-- Lock levels in YRC. -/
 inductive LockId (n : Nat) where
-  | global : LockId n
-  | lockInc (i : Nat) (h : i < n) : LockId n
-  | lockDec (i : Nat) (h : i < n) : LockId n
+  | mergeLock : LockId n
+  | consumerLock (i : Nat) (h : i < n) : LockId n
 
-/-- The level (priority) of each lock in the total order. -/
 def lockLevel {n : Nat} : LockId n → Nat
-  | .global => 0
-  | .lockInc i _ => 2 * i + 1
-  | .lockDec i _ => 2 * i + 2
+  | .mergeLock => 0
+  | .consumerLock i _ => i + 1
 
-/-- All lock levels are distinct (the level function is injective). -/
+/-- All lock levels are distinct (the order is total and well-defined). -/
 theorem lockLevel_injective {n : Nat} (a b : LockId n)
     (h : lockLevel a = lockLevel b) : a = b := by
   cases a with
-  | global =>
+  | mergeLock =>
     cases b with
-    | global => rfl
-    | lockInc j hj => simp [lockLevel] at h
-    | lockDec j hj => simp [lockLevel] at h
-  | lockInc i hi =>
+    | mergeLock => rfl
+    | consumerLock j hj => simp [lockLevel] at h
+  | consumerLock i hi =>
     cases b with
-    | global => simp [lockLevel] at h
-    | lockInc j hj =>
-      have : i = j := by simp [lockLevel] at h; omega
-      subst this; rfl
-    | lockDec j hj => simp [lockLevel] at h; omega
-  | lockDec i hi =>
-    cases b with
-    | global => simp [lockLevel] at h
-    | lockInc j hj => simp [lockLevel] at h; omega
-    | lockDec j hj =>
-      have : i = j := by simp [lockLevel] at h; omega
+    | mergeLock => simp [lockLevel] at h
+    | consumerLock j hj =>
+      have : i = j := by simp [lockLevel] at h; exact h
       subst this; rfl
 
-/-- Helper: stripe lock levels are strictly ascending across stripes. -/
-theorem stripe_levels_ascending (i : Nat) :
-    2 * i + 1 < 2 * i + 2 ∧ 2 * i + 2 < 2 * (i + 1) + 1 := by
-  constructor <;> omega
-
-/-- lockInc levels are strictly ascending with index. -/
-theorem lockInc_level_strict_mono {n : Nat} (i j : Nat) (hi : i < n) (hj : j < n)
-    (hij : i < j) : lockLevel (.lockInc i hi : LockId n) < lockLevel (.lockInc j hj) := by
-  simp [lockLevel]; omega
-
-/-- lockDec levels are strictly ascending with index. -/
-theorem lockDec_level_strict_mono {n : Nat} (i j : Nat) (hi : i < n) (hj : j < n)
-    (hij : i < j) : lockLevel (.lockDec i hi : LockId n) < lockLevel (.lockDec j hj) := by
-  simp [lockLevel]; omega
-
-/-- Global lock has the lowest level (level 0). -/
-theorem global_level_min {n : Nat} (l : LockId n) (h : l ≠ .global) :
-    lockLevel (.global : LockId n) < lockLevel l := by
+/-- gMergeLock has the lowest level. -/
+theorem mergeLock_level_min {n : Nat} (l : LockId n) (h : l ≠ .mergeLock) :
+    lockLevel (.mergeLock : LockId n) < lockLevel l := by
   cases l with
-  | global => exact absurd rfl h
-  | lockInc i hi => simp [lockLevel]
-  | lockDec i hi => simp [lockLevel]
+  | mergeLock => exact absurd rfl h
+  | consumerLock i hi => simp [lockLevel]
 
-/-- **Deadlock Freedom**: Any sequence of lock acquisitions that follows the
-    "acquire in ascending level order" discipline cannot deadlock.
-
-    This is a standard result: a total order on locks with the invariant that
-    every thread acquires locks in strictly ascending order prevents cycles
-    in the wait-for graph, which is necessary and sufficient for deadlock.
-
-    We prove the 2-thread case (the general N-thread case follows by the
-    same transitivity argument on the wait-for cycle). -/
+/-- **Deadlock Freedom** (2-thread wait cycle; N-thread follows by the
+    same transitivity on the wait-for chain): impossible when every
+    thread acquires locks in strictly ascending level order. -/
 theorem no_deadlock_from_total_order {n : Nat}
-    -- Two threads each hold a lock and wait for another
     (held₁ waited₁ held₂ waited₂ : LockId n)
-    -- Thread 1 holds held₁ and wants waited₁ (ascending order)
     (h1 : lockLevel held₁ < lockLevel waited₁)
-    -- Thread 2 holds held₂ and wants waited₂ (ascending order)
     (h2 : lockLevel held₂ < lockLevel waited₂)
-    -- Deadlock requires: thread 1 waits for what thread 2 holds,
-    -- and thread 2 waits for what thread 1 holds
     (h_wait1 : waited₁ = held₂)
     (h_wait2 : waited₂ = held₁) :
     False := by
   subst h_wait1; subst h_wait2
   omega
 
-/-! ### Summary of verified properties (all QED, no sorry)
+/-! ## Summary of verified properties (all QED, no sorry)
 
-  1. `reachable_is_anchored`: Every reachable object is anchored
-     (has a path from an externally-referenced object via heap edges).
+  §1  `yrc_safety` — the collector frees only unanchored objects, which
+      no thread can reach. No use-after-free at the graph level.
+  §2  `no_lost_object` — the atomically published edge is traced.
+  §3  `step_preserves_deadInv`, `deadInv_stable`, `garbage_stability` —
+      a closed set stays closed under every mutator write, root
+      copy/drop, allocation, and foreign free: snapshot garbage cannot
+      be resurrected. `commit_free_safe` — freeing a commit-validated
+      dead set after ANY further concurrent activity is safe.
+  §4  `validated_no_external`, `validated_closed` — the Σrc = Σinternal
+      check plus rc-exactness forces zero external references, i.e. the
+      dead set is closed at commit time (feeding §3).
+  §5  `tags_distinct`, `partitions_disjoint`, `cross_target_live` —
+      concurrent collections own disjoint partitions, and a cell
+      referenced across a partition boundary is never freed by its
+      owner this round (soundness of claimCell's -1 + crossPend).
+  §6  `post_commit_snap_misses_dead`, `grace_no_use_after_free` — with
+      commitDead's grace spin, no capture ever dereferences freed
+      memory.
+  §7  `fence_mutual_exclusion` — the SEQ_CST Dekker pairing in
+      seqs_v2.nim excludes seq structure mutation during collection.
+  §8  `lockLevel_injective`, `mergeLock_level_min`,
+      `no_deadlock_from_total_order` — the remaining locks form a total
+      order acquired ascending; spin-waits form an acyclic wait-for
+      structure (prose above).
 
-  2. `yrc_safety`: The collector only frees unanchored objects,
-     which are unreachable by all threads. **No use-after-free.**
+  ## What is NOT proved
 
-  3. `no_lost_object`: After `a.field = b`, `b` is reachable
-     (atomic store makes the edge visible immediately).
+  • Tarjan/SCC implementation correctness: that `capture` computes the
+    actual SCCs and that computeDeadness's per-SCC sums equal the model's
+    Σrc/Σinternal for the emitted dead set (condensation, sinks-first
+    order, deadIn accounting). §4 takes the counts as given.
+  • rc-exactness mechanics: that merge + the dirty check + the rc-word
+    recheck really imply "commit-time rc = internal + external" (§4's
+    h_exact). The argument: rc is only mutated by atomic direct incs
+    (caught by the recheck), merged queue entries (queues drained at
+    merge; later entries caught by the dirty peek), and the collector's
+    own inRootsFlag toggles (excluded from the compared word — see the
+    comment above claimCell).
+  • The C11 memory model: §7 assumes sequential consistency for the
+    SEQ_CST operations (sound: SEQ_CST ops do form a total order) and
+    the acquire/release reasoning elsewhere is informal.
+  • Liveness/completeness: every dead cycle is EVENTUALLY freed.
+    Aborted (dirty) SCCs and crossPend targets are re-registered as
+    candidates, so they are re-examined; termination of that loop under
+    adversarial mutators is not formalized. Also unproved: termination
+    bounds for the four spin-waits (prose in §8).
+  • Tag wrap-around: 2³¹ collections completing during one collection's
+    lifetime could forge a stale stamp (noted at `tags_distinct`).
 
-  4. `src_safe_in_window`: Even between the atomic store and
-     the buffered inc, the collector cannot free src.
+  ## Epoch stamps (generational pruning)
 
-  5. `lockLevel_injective`: All lock levels are distinct (well-defined total order).
-
-  6. `global_level_min`: The global lock has the lowest level.
-
-  7. `lockInc_level_strict_mono`, `lockDec_level_strict_mono`:
-     Stripe locks are strictly ordered by index.
-
-  8. `no_deadlock_from_total_order`: A 2-thread deadlock cycle is impossible
-     when both threads acquire locks in ascending level order.
-
-  Together these establish that YRC's write barrier protocol
-  (atomic store → buffer inc → buffer dec) is safe under concurrent
-  collection, and the locking discipline prevents deadlock.
-
-  ## What is NOT proved: Completeness (liveness)
-
-  This proof covers **safety** (no use-after-free) and **deadlock-freedom**,
-  but does NOT prove **completeness** — that all garbage cycles are eventually
-  collected.
-
-  Completeness depends on the trial deletion algorithm (Bacon 2001) correctly
-  identifying closed cycles. Specifically it requires proving:
-
-  1. After `mergePendingRoots`, merged RCs equal logical RCs
-     (buffered inc/dec exactly compensate graph changes since last merge).
-  2. `markGray` subtracts exactly the internal (heap→heap) edge count from
-     each node's merged RC, yielding `trialRC(x) = externalRefCount(x)`.
-  3. `scan` correctly partitions: nodes with `trialRC ≥ 0` are rescued by
-     `scanBlack`; nodes with `trialRC < 0` remain white.
-  4. White nodes form closed subgraphs with zero external refs → garbage.
-
-  These properties follow from the well-known Bacon trial-deletion algorithm
-  and are assumed here rather than re-proved. The YRC-specific contribution
-  (buffered RCs, striped queues, concurrent mutators) is what our safety
-  proof covers — showing that concurrency does not break the preconditions
-  that trial deletion relies on (physical graph consistency, eventual RC
-  consistency after merge).
+  Commit re-stamps proven-live cells with (epochBase|epoch, survivalAge)
+  in the claim word; a capture treats a current-epoch stamp of age ≥
+  YrcPromoteAge on a DESCENDANT as an opaque live external and does not
+  descend. Soundness needs no new lemmas: a pruned cell is simply an
+  uncaptured cell, so the captured set shrinks and every §3–§6 statement
+  quantifies over a smaller S. Pruning can only ADD unexplained external
+  refs to captured SCCs (a pruned predecessor's refs are never explained
+  by internal/deadIn), so it can force a false "live", never a false
+  "dead" — the conservative direction. Completeness (bounded float,
+  ≤ ~2 epochs) rests on four hooks, each keeping a dec-witness
+  registered:
+    E1  roots never prune: a registered candidate is always fully
+        root-scanned, stamps notwithstanding;
+    E2  an SCC that pruned an out-edge and survives keeps one member
+        registered (flagPruned) — its "live" verdict may lean on a stamp
+        that went stale within the epoch;
+    E3  a commit-time dec into a stamped cell re-registers the target —
+        the dec may be the death blow to a cell no collection analyzed;
+    E4  explicit full collects advance the epoch first, so all stamps
+        are stale and nothing is pruned.
+  Not formalized. Also noted: the epoch clock counts collections, and
+  short epochs (≲ 4) resonate with the adaptive threshold — pruned
+  collections are cheap, so collections and hence epoch turns speed up,
+  re-tracing MORE than with no stamps; a work-based clock would fix it.
 
   Reference: D.F. Bacon and V.T. Rajan, "Concurrent Cycle Collection in
-  Reference Counted Systems", ECOOP 2001.
+  Reference Counted Systems", ECOOP 2001 — the deadness arithmetic is
+  the condensation form of their trial deletion; the capture/validate/
+  commit structure and the SATB use of the deferred-dec queues are
+  yrc-specific.
 -/
diff --git a/lib/system/yrc_tarjan_proof.lean b/lib/system/yrc_tarjan_proof.lean
new file mode 100644
index 0000000000..68221b1467
--- /dev/null
+++ b/lib/system/yrc_tarjan_proof.lean
@@ -0,0 +1,594 @@
+/-
+  Tarjan-based deadness computation — correctness proof
+  =====================================================
+  Self-contained, no Mathlib. Checked with Lean 4 (v4.32.0).
+
+  Companion to yrc_proof.lean; models the NOVEL part of yrc.nim's
+  collector: cycle detection via a single Tarjan SCC traversal plus one
+  linear reverse scan over the condensation, replacing Bacon-style trial
+  deletion (three traversals: markGray / scan / collectWhite).
+
+  ## The algorithm (capture / computeDeadness in yrc.nim)
+
+  `capture` runs an iterative Tarjan DFS from the candidate roots. Each
+  visited cell is claimed (dense index in the header), its rc word is
+  snapshotted, and every traversed slot contributes one edge record.
+  SCCs are numbered 0, 1, 2, … in POP (completion) order. Tarjan's
+  invariant: when an SCC is completed, every SCC it points to was
+  completed earlier — so every condensation cross edge goes from a
+  HIGHER SCC id to a LOWER one ("sinks first").
+
+  `computeDeadness` then makes ONE pass s = nScc−1 … 0 (sources before
+  sinks, since in-edges come from higher ids):
+
+      ext(s) = sumRefs(s) − internal(s) − deadIn(s)
+      if not forcedLive(s) and ext(s) == 0:
+        s is DEAD;  for each cross edge s → t: deadIn(t) += 1
+      else:
+        s is LIVE;  for each cross edge s → t: forcedLive(t) := true
+
+  where sumRefs(s) = Σ rc over members, internal(s) = # captured edges
+  within s, and forcedLive is seeded from cells still registered in the
+  roots buffer (inRootsFlag).
+
+  ## What we prove
+
+  Fix the SPEC of liveness on the condensation: an SCC is live iff it
+  has an external reference, a roots-buffer seed, or a captured cross
+  edge from a live SCC (`LiveScc`, an inductive definition).
+
+  1. `scan_dead_iff_not_live` — any deadness assignment satisfying the
+     scan's per-SCC equation (well-defined thanks to the sinks-first
+     edge order) marks an SCC dead IFF it is not live. Soundness AND
+     completeness in one theorem: the single reverse scan computes the
+     garbage set EXACTLY on the captured snapshot.
+  2. `impl_fixpoint_is_spec` — the implementation's ARITHMETIC form
+     (ext = sumRefs − internal − deadIn with forcedLive propagation) is
+     the same equation, given rc-exactness (sumRefs = external +
+     internal + cross-in; established by merge + commit validation, see
+     yrc_proof.lean §4).
+  3. Cell-level bridge: `tarjan_sound` — cells of dead SCCs are
+     unreachable in the snapshot; `tarjan_complete` — every captured
+     garbage cell IS marked dead (this needs strong connectivity of the
+     SCCs and exactness of the external counts; Bacon needs his second
+     and third traversals for the same guarantee).
+  4. `demotion_closure_sound` — validate-time demotion (an SCC dropped
+     from the dead set because a mutator dirtied it) must PROPAGATE
+     along captured cross edges: the freed set stays closed only if the
+     demoted set is successor-closed within the dead set. A demoted SCC
+     survives with its out-edges intact, so any still-dead target would
+     be freed while a surviving cell points at it.
+
+  ## What is assumed (and where it is discharged)
+
+  • The sinks-first edge order (`horder`) — Tarjan's classical
+    invariant; the DFS itself is not modeled.
+  • rc-exactness (`hcount`) — discharged operationally by yrc_proof §4
+    (merge + dirty check + rc-word recheck).
+  • That `capture` records exactly the heap edges among captured cells
+    and that SCC members are mutually reachable (`h_edge_resp`,
+    `h_conn`, `h_cross_real`) — properties of the traversal + Tarjan.
+-/
+
+abbrev Obj := Nat
+
+/-! ## §1 Descending induction
+
+  The scan processes higher SCC ids first; every recursive dependency
+  of `dead s` is on some `u > s`. This induction principle is the
+  well-definedness of the whole scheme. -/
+
+theorem descending_induction {n : Nat} (P : Fin n → Prop)
+    (step : ∀ s : Fin n, (∀ u : Fin n, s < u → P u) → P s) :
+    ∀ s, P s := by
+  have key : ∀ k, ∀ s : Fin n, n - s.val ≤ k → P s := by
+    intro k
+    induction k with
+    | zero =>
+      intro s hs
+      have := s.isLt
+      omega
+    | succ k ih =>
+      intro s _
+      apply step
+      intro u hu
+      apply ih
+      have h1 := u.isLt
+      have h2 : s.val < u.val := hu
+      omega
+  intro s
+  exact key n s (by omega)
+
+/-! ## §2 The condensation and the liveness spec
+
+  `edges` are the captured condensation cross edges (with multiplicity:
+  one entry per traversed slot, exactly like cap.edges bucketed into
+  crossTgt). `extRefs s` counts references into SCC `s` from OUTSIDE
+  the capture: stack refs, uncaptured heap cells, other collections'
+  partitions — everything in Σrc not explained by captured edges.
+  `seed s` is the inRootsFlag forcedLive seeding. -/
+
+section Condensation
+
+variable {n : Nat}
+variable (edges : List (Fin n × Fin n))
+variable (extRefs : Fin n → Nat)
+variable (seed : Fin n → Bool)
+
+/-- The SPEC: an SCC is live iff something external anchors it —
+    directly or through a chain of captured cross edges. -/
+inductive LiveScc : Fin n → Prop where
+  | ext (s : Fin n) : 0 < extRefs s → LiveScc s
+  | root (s : Fin n) : seed s = true → LiveScc s
+  | pred (u s : Fin n) : (u, s) ∈ edges → LiveScc u → LiveScc s
+
+/-- The per-SCC equation the reverse scan establishes: dead iff no
+    external refs, no seed, and ALL cross predecessors dead. (The
+    sinks-first order makes this a valid definition: every predecessor
+    has a higher id and is decided first — see `descending_induction`;
+    without that order the "definition" would be circular.) -/
+def ScanEq (dead : Fin n → Bool) : Prop :=
+  ∀ s, dead s = true ↔
+    (extRefs s = 0 ∧ seed s = false ∧
+     ∀ e ∈ edges, e.2 = s → dead e.1 = true)
+
+/-- Live SCCs are never marked dead (soundness direction). -/
+theorem live_not_dead (dead : Fin n → Bool)
+    (hfix : ScanEq edges extRefs seed dead) :
+    ∀ s, LiveScc edges extRefs seed s → dead s ≠ true := by
+  intro s hl
+  induction hl with
+  | ext s h =>
+    intro hd
+    have := ((hfix s).mp hd).1
+    omega
+  | root s h =>
+    intro hd
+    have := ((hfix s).mp hd).2.1
+    rw [h] at this
+    cases this
+  | pred u s hmem _ ih =>
+    intro hd
+    exact ih (((hfix s).mp hd).2.2 (u, s) hmem rfl)
+
+/-- Non-live SCCs are always marked dead (completeness direction) —
+    by descending induction along the scan order. -/
+theorem not_live_dead
+    (horder : ∀ e ∈ edges, e.2 < e.1)
+    (dead : Fin n → Bool)
+    (hfix : ScanEq edges extRefs seed dead) :
+    ∀ s, ¬ LiveScc edges extRefs seed s → dead s = true := by
+  refine descending_induction
+    (fun s => ¬ LiveScc edges extRefs seed s → dead s = true) ?_
+  intro s ihs hnl
+  rw [hfix]
+  refine ⟨?_, ?_, ?_⟩
+  · cases Nat.eq_zero_or_pos (extRefs s) with
+    | inl h => exact h
+    | inr h => exact absurd (LiveScc.ext s h) hnl
+  · cases hsd : seed s with
+    | false => rfl
+    | true => exact absurd (LiveScc.root s hsd) hnl
+  · intro e he hes
+    have hlt : s < e.1 := by
+      have := horder e he
+      rw [hes] at this
+      exact this
+    apply ihs e.1 hlt
+    intro hlu
+    have hmem : (e.1, s) ∈ edges := by
+      rw [← hes]
+      simpa using he
+    exact hnl (LiveScc.pred e.1 s hmem hlu)
+
+/-- **Main condensation theorem**: the single reverse scan computes
+    EXACTLY the non-live SCCs. One Tarjan DFS + one linear scan replace
+    Bacon's three graph traversals, with no loss of precision on the
+    snapshot. -/
+theorem scan_dead_iff_not_live
+    (horder : ∀ e ∈ edges, e.2 < e.1)
+    (dead : Fin n → Bool)
+    (hfix : ScanEq edges extRefs seed dead) :
+    ∀ s, dead s = true ↔ ¬ LiveScc edges extRefs seed s := by
+  intro s
+  constructor
+  · intro hd hl
+    exact live_not_dead edges extRefs seed dead hfix s hl hd
+  · exact not_live_dead edges extRefs seed horder dead hfix s
+
+/-! ## §3 The implementation's arithmetic form
+
+  computeDeadness does not test "all predecessors dead" directly; it
+  maintains ext(s) = sumRefs(s) − internal(s) − deadIn(s) and a
+  forcedLive flag pushed along cross edges of live SCCs. We show this
+  is the same equation, given rc-exactness:
+
+      sumRefs s = extRefs s + internal s + (# cross edges into s).
+
+  ext(s) = 0 then says extRefs s = 0 AND every cross in-edge came from
+  a dead predecessor; ¬forcedLive says no seed and no LIVE predecessor
+  pushed the flag — together exactly `ScanEq`. -/
+
+def inCount (s : Fin n) : Nat :=
+  edges.countP (fun e => e.2 == s)
+
+def deadInCount (dead : Fin n → Bool) (s : Fin n) : Nat :=
+  edges.countP (fun e => e.2 == s && dead e.1)
+
+/-- countP is monotone under pointwise implication. -/
+theorem countP_le_of_imp {α : Type} (l : List α) (p q : α → Bool)
+    (himp : ∀ x ∈ l, p x = true → q x = true) :
+    l.countP p ≤ l.countP q := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    have iht := ih (fun x hx => himp x (List.mem_cons_of_mem a hx))
+    by_cases hpa : p a = true
+    · have hqa := himp a (by simp) hpa
+      simp [hpa, hqa]
+      omega
+    · simp only [List.countP_cons]
+      have : p a = false := by
+        cases h : p a
+        · rfl
+        · exact absurd h hpa
+      simp [this]
+      omega
+
+/-- If a stronger predicate matches as often as a weaker one, they
+    agree on every element. -/
+theorem countP_eq_forces_all {α : Type} (l : List α) (p q : α → Bool)
+    (himp : ∀ x ∈ l, q x = true → p x = true)
+    (heq : l.countP p = l.countP q) :
+    ∀ x ∈ l, p x = true → q x = true := by
+  induction l with
+  | nil => intro x hx; cases hx
+  | cons a l ih =>
+    have himpt : ∀ x ∈ l, q x = true → p x = true :=
+      fun x hx => himp x (List.mem_cons_of_mem a hx)
+    have hmono := countP_le_of_imp l q p himpt
+    intro x hx hpx
+    simp only [List.countP_cons] at heq
+    cases List.mem_cons.mp hx with
+    | inl hxa =>
+      subst hxa
+      cases hqx : q x with
+      | true => rfl
+      | false =>
+        exfalso
+        simp [hpx, hqx] at heq
+        omega
+    | inr hxl =>
+      have hqa_pa : (if q a = true then 1 else 0) ≤ (if p a = true then 1 else 0) := by
+        by_cases hq : q a = true
+        · simp [hq, himp a (by simp) hq]
+        · simp [hq]
+      have heqt : l.countP p = l.countP q := by
+        by_cases hq : q a = true
+        · simp [hq, himp a (by simp) hq] at heq
+          omega
+        · have hqf : q a = false := by
+            cases h : q a
+            · rfl
+            · exact absurd h hq
+          by_cases hp : p a = true
+          · simp [hp, hqf] at heq
+            omega
+          · have hpf : p a = false := by
+              cases h : p a
+              · rfl
+              · exact absurd h hp
+            simp [hpf, hqf] at heq
+            omega
+      exact ih himpt heqt x hxl hpx
+
+/-- If all cross predecessors of `s` are dead, deadIn equals the full
+    in-count (and vice versa). -/
+theorem deadIn_eq_inCount_iff (dead : Fin n → Bool) (s : Fin n) :
+    deadInCount edges dead s = inCount edges s ↔
+    (∀ e ∈ edges, e.2 = s → dead e.1 = true) := by
+  constructor
+  · intro heq e he hes
+    have himp : ∀ x ∈ edges, (fun e => e.2 == s && dead e.1) x = true →
+        (fun e => e.2 == s) x = true := by
+      intro x _ hx
+      simp only [Bool.and_eq_true] at hx
+      exact hx.1
+    have := countP_eq_forces_all edges
+      (fun e => e.2 == s) (fun e => e.2 == s && dead e.1)
+      himp heq.symm e he
+    have hbeq : (e.2 == s) = true := by
+      simp [hes]
+    have := this hbeq
+    simp only [Bool.and_eq_true] at this
+    exact this.2
+  · intro hall
+    unfold deadInCount inCount
+    apply List.countP_congr
+    intro e he
+    by_cases hes : e.2 = s
+    · simp [hes, hall e he hes]
+    · have : (e.2 == s) = false := by
+        simp [hes]
+      simp [this]
+
+/-- The implementation's per-SCC decision, verbatim from
+    computeDeadness: NOT forced (no seed, no live predecessor pushed
+    the flag) and ext = sumRefs − internal − deadIn = 0 (stated
+    subtraction-free). -/
+def ImplEq (sumRefs internal : Fin n → Nat) (dead : Fin n → Bool) : Prop :=
+  ∀ s, dead s = true ↔
+    (¬ (seed s = true ∨ ∃ e ∈ edges, e.2 = s ∧ dead e.1 = false) ∧
+     sumRefs s = internal s + deadInCount edges dead s)
+
+/-- **The arithmetic is the spec**: under rc-exactness, the
+    implementation's equation is `ScanEq`, so `scan_dead_iff_not_live`
+    applies to computeDeadness as written. -/
+theorem impl_fixpoint_is_spec
+    (sumRefs internal : Fin n → Nat) (dead : Fin n → Bool)
+    (hcount : ∀ s, sumRefs s = extRefs s + internal s + inCount edges s)
+    (himpl : ImplEq edges seed sumRefs internal dead) :
+    ScanEq edges extRefs seed dead := by
+  intro s
+  rw [himpl s]
+  constructor
+  · rintro ⟨hnf, harith⟩
+    have hor := hnf
+    rw [not_or] at hor
+    obtain ⟨hseed, hnopred⟩ := hor
+    have hseedf : seed s = false := by
+      cases h : seed s
+      · rfl
+      · exact absurd h hseed
+    have hall : ∀ e ∈ edges, e.2 = s → dead e.1 = true := by
+      intro e he hes
+      cases h : dead e.1 with
+      | true => rfl
+      | false => exact absurd ⟨e, he, hes, h⟩ hnopred
+    have hdc := (deadIn_eq_inCount_iff edges dead s).mpr hall
+    have hc := hcount s
+    refine ⟨by omega, hseedf, hall⟩
+  · rintro ⟨hext, hseedf, hall⟩
+    have hdc := (deadIn_eq_inCount_iff edges dead s).mpr hall
+    refine ⟨?_, ?_⟩
+    · rw [not_or]
+      refine ⟨by simp [hseedf], ?_⟩
+      rintro ⟨e, he, hes, hdf⟩
+      rw [hall e he hes] at hdf
+      cases hdf
+    · have hc := hcount s
+      omega
+
+end Condensation
+
+/-! ## §4 Cell-level correctness
+
+  Bridge from the condensation to the actual heap snapshot. `extRef`
+  covers every reference source outside the capture: mutator stacks,
+  the roots buffer, uncaptured heap cells' slots that the arithmetic
+  cannot explain, and other collections' partitions (cross-collection
+  edges — this is the SCC-side view of `cross_target_live` in
+  yrc_proof.lean §5). -/
+
+structure CellGraph where
+  edge : Obj → Obj → Prop
+  extRef : Obj → Prop
+
+/-- A cell is live iff an external reference anchors it through heap
+    edges (the cell-level ground truth; `anchored` of yrc_proof.lean). -/
+inductive CellLive (g : CellGraph) : Obj → Prop where
+  | ext (x : Obj) : g.extRef x → CellLive g x
+  | step (x y : Obj) : CellLive g x → g.edge x y → CellLive g y
+
+/-- Paths through heap edges, used to move liveness around inside an
+    SCC (Tarjan guarantees SCC members are mutually reachable). -/
+inductive EdgePath (g : CellGraph) : Obj → Obj → Prop where
+  | refl (x : Obj) : EdgePath g x x
+  | step (x y z : Obj) : EdgePath g x y → g.edge y z → EdgePath g x z
+
+theorem cellLive_along_path (g : CellGraph) (u v : Obj)
+    (hl : CellLive g u) (hp : EdgePath g u v) : CellLive g v := by
+  induction hp with
+  | refl => exact hl
+  | step _ _ _ hedge ih => exact CellLive.step _ _ ih hedge
+
+section CellBridge
+
+variable {n : Nat}
+variable (g : CellGraph)
+variable (edges : List (Fin n × Fin n))
+variable (extRefs : Fin n → Nat)
+variable (seed : Fin n → Bool)
+variable (captured : Obj → Prop)
+variable (scc : Obj → Fin n)
+
+/-- Any live captured cell sits in a live SCC.
+    Premises are properties of `capture`:
+    * `h_edge_resp` — every heap edge between captured cells was
+      recorded (same SCC → internal; different → cross edge);
+    * `h_closed` — an edge from an UNCAPTURED cell is unexplained by
+      the captured arithmetic, so it lands in extRefs;
+    * `h_ext` — direct external refs (stacks, roots buffer, foreign
+      partitions) are counted in extRefs. -/
+theorem captured_live_scc
+    (h_edge_resp : ∀ u v, captured u → captured v → g.edge u v →
+        scc u = scc v ∨ (scc u, scc v) ∈ edges)
+    (h_closed : ∀ u v, captured v → g.edge u v → ¬ captured u →
+        0 < extRefs (scc v))
+    (h_ext : ∀ v, captured v → g.extRef v → 0 < extRefs (scc v)) :
+    ∀ x, CellLive g x → captured x →
+      LiveScc edges extRefs seed (scc x) := by
+  intro x hl
+  induction hl with
+  | ext x h =>
+    intro hc
+    exact LiveScc.ext _ (h_ext x hc h)
+  | step u v hu hedge ih =>
+    intro hcv
+    by_cases hcu : captured u
+    · cases h_edge_resp u v hcu hcv hedge with
+      | inl heq => rw [← heq]; exact ih hcu
+      | inr hmem => exact LiveScc.pred _ _ hmem (ih hcu)
+    · exact LiveScc.ext _ (h_closed u v hcv hedge hcu)
+
+/-- **Soundness**: every cell of a dead SCC is unanchored in the
+    snapshot — freeing it is justified by yrc_proof.lean §1
+    (`yrc_safety`) + §3 (stability through the commit window). -/
+theorem tarjan_sound
+    (dead : Fin n → Bool)
+    (hfix : ScanEq edges extRefs seed dead)
+    (h_edge_resp : ∀ u v, captured u → captured v → g.edge u v →
+        scc u = scc v ∨ (scc u, scc v) ∈ edges)
+    (h_closed : ∀ u v, captured v → g.edge u v → ¬ captured u →
+        0 < extRefs (scc v))
+    (h_ext : ∀ v, captured v → g.extRef v → 0 < extRefs (scc v)) :
+    ∀ x, captured x → dead (scc x) = true → ¬ CellLive g x := by
+  intro x hc hd hl
+  exact live_not_dead edges extRefs seed dead hfix (scc x)
+    (captured_live_scc g edges extRefs seed captured scc
+      h_edge_resp h_closed h_ext x hl hc) hd
+
+/-- Every cell of a live SCC is genuinely live. Needs the converse
+    premises: external counts are EXACT (no phantom refs — deferred
+    decs inflate rc, so in the running system this holds only after
+    the merge; overcounts delay collection by a round, they never
+    cause a wrong free), cross edges are real edges, and SCC members
+    are mutually reachable (Tarjan). -/
+theorem live_scc_cells_live
+    (h_ext_exact : ∀ s : Fin n, 0 < extRefs s →
+        ∃ v, captured v ∧ scc v = s ∧ g.extRef v)
+    (h_seed_exact : ∀ s : Fin n, seed s = true →
+        ∃ v, captured v ∧ scc v = s ∧ g.extRef v)
+    (h_cross_real : ∀ (u s : Fin n), (u, s) ∈ edges →
+        ∃ cu cv, captured cu ∧ captured cv ∧ scc cu = u ∧ scc cv = s ∧
+          g.edge cu cv)
+    (h_conn : ∀ u v, captured u → captured v → scc u = scc v →
+        EdgePath g u v) :
+    ∀ s, LiveScc edges extRefs seed s →
+      ∀ x, captured x → scc x = s → CellLive g x := by
+  intro s hl
+  induction hl with
+  | ext s h =>
+    intro x hc hs
+    obtain ⟨v, hcv, hsv, hev⟩ := h_ext_exact s h
+    exact cellLive_along_path g v x (CellLive.ext v hev)
+      (h_conn v x hcv hc (by rw [hsv, hs]))
+  | root s h =>
+    intro x hc hs
+    obtain ⟨v, hcv, hsv, hev⟩ := h_seed_exact s h
+    exact cellLive_along_path g v x (CellLive.ext v hev)
+      (h_conn v x hcv hc (by rw [hsv, hs]))
+  | pred u s hmem _ ih =>
+    intro x hc hs
+    obtain ⟨cu, cv, hccu, hccv, hscu, hscv, he⟩ := h_cross_real u s hmem
+    have hculive : CellLive g cu := ih cu hccu hscu
+    exact cellLive_along_path g cv x (CellLive.step cu cv hculive he)
+      (h_conn cv x hccv hc (by rw [hscv, hs]))
+
+/-- **Completeness**: every captured garbage cell is marked dead — the
+    scan collects ALL cycles reachable from the candidate set in one
+    round (on the snapshot; concurrent inflation only defers). -/
+theorem tarjan_complete
+    (horder : ∀ e ∈ edges, e.2 < e.1)
+    (dead : Fin n → Bool)
+    (hfix : ScanEq edges extRefs seed dead)
+    (h_ext_exact : ∀ s : Fin n, 0 < extRefs s →
+        ∃ v, captured v ∧ scc v = s ∧ g.extRef v)
+    (h_seed_exact : ∀ s : Fin n, seed s = true →
+        ∃ v, captured v ∧ scc v = s ∧ g.extRef v)
+    (h_cross_real : ∀ (u s : Fin n), (u, s) ∈ edges →
+        ∃ cu cv, captured cu ∧ captured cv ∧ scc cu = u ∧ scc cv = s ∧
+          g.edge cu cv)
+    (h_conn : ∀ u v, captured u → captured v → scc u = scc v →
+        EdgePath g u v) :
+    ∀ x, captured x → ¬ CellLive g x → dead (scc x) = true := by
+  intro x hc hnl
+  apply not_live_dead edges extRefs seed horder dead hfix
+  intro hl
+  exact hnl (live_scc_cells_live g edges extRefs seed captured scc
+    h_ext_exact h_seed_exact h_cross_real h_conn (scc x) hl x hc rfl)
+
+end CellBridge
+
+/-! ## §5 Validate-time demotion must propagate
+
+  validateDead demotes a dead SCC when a mutator dirtied it (queue
+  entry or changed rc word). A demoted SCC becomes a survivor: its
+  slots are NOT nil'd at commit, so its captured out-edges remain in
+  the heap. If a cross target of a demoted SCC stayed in the dead set,
+  the commit would free a cell that a surviving cell still points to —
+  deadIn had explained that edge away under the assumption that the
+  predecessor dies too.
+
+  Minimal instance of the hazard: two SCCs, one edge 1 → 0, both
+  computed dead (ext = 0 for both; SCC 0's only reference comes from
+  SCC 1, subtracted as deadIn). Demote SCC 1 alone, and the freed set
+  {0} has a live in-edge from the surviving SCC 1.
+
+  The theorem below states the repair: if the demoted set `K` is
+  successor-closed within the dead set (demoting s also demotes every
+  dead t with a captured edge s → t, transitively — one countdown pass
+  suffices because edges go from higher to lower ids), then the freed
+  set F = dead ∖ K is predecessor-closed: every captured edge into F
+  comes from F. Combined with extRefs = 0 and no seed (ScanEq) this
+  makes F closed in the sense of yrc_proof.lean §3, so freeing F is
+  covered by `commit_free_safe` there. -/
+
+theorem demotion_closure_sound {n : Nat}
+    (edges : List (Fin n × Fin n))
+    (extRefs : Fin n → Nat) (seed : Fin n → Bool)
+    (dead : Fin n → Bool)
+    (hfix : ScanEq edges extRefs seed dead)
+    (K : Fin n → Prop)                       -- the demoted SCCs
+    (hK_closed : ∀ e ∈ edges, K e.1 → dead e.2 = true → K e.2) :
+    -- every captured edge into the freed set comes from the freed set
+    ∀ e ∈ edges, (dead e.2 = true ∧ ¬ K e.2) →
+      (dead e.1 = true ∧ ¬ K e.1) := by
+  intro e he ⟨hd2, hk2⟩
+  have hd1 : dead e.1 = true :=
+    ((hfix e.2).mp hd2).2.2 e he rfl
+  refine ⟨hd1, ?_⟩
+  intro hk1
+  exact hk2 (hK_closed e he hk1 hd2)
+
+/-- Without successor-closure the guarantee genuinely fails: in the
+    two-SCC instance above, demoting only SCC 1 leaves the freed set
+    {0} with an in-edge from a survivor. (Concrete witness, checked by
+    `decide`-style evaluation.) -/
+example :
+    let edges : List (Fin 2 × Fin 2) := [(1, 0)]
+    let dead : Fin 2 → Bool := fun _ => true
+    let K : Fin 2 → Prop := fun s => s = 1     -- demote only SCC 1
+    -- ScanEq holds for `dead` (both SCCs legitimately computed dead) …
+    ScanEq edges (fun _ => 0) (fun _ => false) dead ∧
+    -- … yet the freed set {0} has an in-edge from surviving SCC 1:
+    ((1, 0) ∈ edges ∧ dead 0 = true ∧ ¬ K 0 ∧ K 1) := by
+  refine ⟨?_, ?_⟩
+  · intro s
+    simp
+  · refine ⟨by simp, rfl, by simp, rfl⟩
+
+/-! ## Summary (all QED, no sorry)
+
+  * `descending_induction` — the sinks-first SCC numbering makes the
+    reverse scan a well-founded definition.
+  * `scan_dead_iff_not_live` — the scan marks an SCC dead iff it is
+    not externally anchored: exact garbage identification in ONE
+    linear pass over the condensation.
+  * `impl_fixpoint_is_spec` — the implementation's arithmetic
+    (ext = sumRefs − internal − deadIn, forcedLive propagation) is
+    that same equation under rc-exactness.
+  * `tarjan_sound` / `tarjan_complete` — at the cell level: dead cells
+    are unanchored (frees are safe) and unanchored captured cells are
+    freed (nothing is missed on the snapshot).
+  * `demotion_closure_sound` + counterexample — demotion is sound iff
+    it propagates along captured cross edges to still-dead targets;
+    a lone demotion can leave the freed set with a surviving
+    predecessor.
+
+  Not modeled: the Tarjan DFS itself (its two classical invariants —
+  SCC partition and sinks-first emission — enter as premises), the
+  iterative traceStack encoding, crossPend (cross-collection edges are
+  folded into `extRefs`, justified by yrc_proof.lean §5), and the
+  temporal validity of rc-exactness (yrc_proof.lean §4).
+-/
diff --git a/tests/arc/torcbench.nim b/tests/arc/torcbench.nim
index e54537883a..a010b229c2 100644
--- a/tests/arc/torcbench.nim
+++ b/tests/arc/torcbench.nim
@@ -36,4 +36,4 @@ proc main() =
 main()
 GC_fullCollect()
 when not defined(useMalloc):
-  echo getOccupiedMem() < 10 * 1024 * 1024, " peak memory: ", getMaxMem() < 10 * 1024 * 1024
+  echo getOccupiedMem() < 10 * 1024 * 1024, " peak memory: ", getMaxMem() < 12 * 1024 * 1024