mirrors/Nim
1
0
Fork 0
mirror of https://github.com/nim-lang/Nim.git synced 2026-08-02 05:29:01 +00:00
Code Issues Packages Projects Releases Wiki Activity

final tweaks and documentation update

Browse Source
This commit is contained in:
Araq
2026-07-19 14:29:47 +02:00
parent 6322b7b230
commit 8a268b578e
2 changed files with 824 additions and 165 deletions
Download Patch File Download Diff File Expand all files Collapse all files

395
lib/system/yrc.nim
View File

@@ -1,23 +1,42 @@
#
# 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
#
# Ref-field writes (`nimAsgnYrc`, `nimSinkYrc`) are LOCK-FREE: an atomic
# incRef of the new value, an atomic exchange of the slot, and a deferred
# decRef of the old value through the `toDec` stripe queues. Collection runs
# concurrently with them (see "The Write Barrier" below).
# 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.
#
# Seq mutations that change the container structure (add/grow/shrink/setLen)
# still hold the mutator read lock, and the collector still acquires all
# write locks for the duration of a collection. Since ref assignments no
# longer contend on that lock, its only remaining jobs are: freezing seq
# len/payload pairs against the collector's traversal (so no deferred buffer
# frees and no torn len/pointer reads are possible), and collector-vs-
# collector exclusion.
# 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.
#
# 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.
#
# 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 Write Barrier
#
@@ -31,7 +50,9 @@
# the *next* collection's merge: deletions can only make the captured
# graph look MORE alive, never less.
# * Stack copies enqueue into `toInc` (buffered incs).
# * Only `nimAsgnYrc`'s incRef mutates rc words directly (atomically).
# * 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.
#
# So the commit-time validation is:
# 1. Any cell sitting in a `toInc`/`toDec` queue had its reference set
@@ -54,9 +75,10 @@
#
# 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 (unused by YRC otherwise) is stamped
# with an epoch-tagged discovery index, so stale stamps never need
# clearing. Everything else lives in side arrays (SoA layout).
# 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
@@ -66,20 +88,36 @@
# Tarjan emits SCCs sinks-first, so one linear scan in reverse emission
# order settles every SCC (sources before their targets).
#
# 3. Commit: 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. Because the slots are nil by the time
# destructors run, destructors cannot re-enter the decRef machinery for
# the already-processed edges.
# 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 — it is
# the stepping stone towards optimistic, lock-free collection: replace the
# frozen-heap invariant with a SATB write barrier plus commit-time
# validation (rc word unchanged since capture, no barrier hit on a member)
# and the same three phases run concurrently with mutators.
# 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
#
@@ -101,11 +139,9 @@ import std/locks
const
NumStripes = 64
QueueSize {.intdefine.} = 128 # override with -d:QueueSize=N
RootsThreshold = 10
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
@@ -113,7 +149,6 @@ const
type
TraceProc = proc (p, env: pointer) {.nimcall, gcsafe, raises: [].}
DisposeProc = proc (p: pointer) {.nimcall, gcsafe, raises: [].}
# With lock-free ref assignments, rc words are mutated concurrently with the
# collector (direct atomic incRefs), so all collector-side rc accesses must
@@ -135,14 +170,6 @@ when useAtomicRc:
if atomicCompareExchangeN(addr c.rc, addr expected, desired, true,
ATOMIC_ACQ_REL, ATOMIC_RELAXED):
break
template rcSetFlag(c, flag) =
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):
break
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
@@ -162,7 +189,6 @@ else:
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
@@ -247,9 +273,9 @@ type
sccOf: int32 # -1 while the cell is on the Tarjan stack
CaptureBufs = object
## side structure of a collection; persistent across collections (only
## the collector, under the global write lock, ever touches it) so that
## frequent small collections don't pay per-collection allocations
## 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]
@@ -403,19 +429,32 @@ else:
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] # ORPHANED candidates only: spilled by exiting
@@ -471,39 +510,18 @@ 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:
trialInc(h)
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)
trialInc(x)
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:
# flush the inc queues directly: incs are atomic, so this is safe
# concurrently with running collections (whose commit-time rc
# validation observes the change)
for i in 0..<NumStripes:
withLock stripes[i].lockInc:
for j in 0..<stripes[i].toIncLen:
trialInc(stripes[i].toInc[j])
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)
when defined(nimOrcStats):
var
@@ -539,24 +557,59 @@ proc drainStripe(i: int) =
## 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).
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)
trialInc(x)
else:
withLock stripes[i].lockInc:
for j in 0..<stripes[i].toIncLen:
trialInc(stripes[i].toInc[j])
stripes[i].toIncLen = 0
withLock stripes[i].lockDec:
for j in 0..<stripes[i].toDecLen:
let (c, desc) = stripes[i].toDec[j]
trialDec(c)
registerLocal(c, desc)
stripes[i].toDecLen = 0
## 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):
# 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)
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
@@ -863,32 +916,36 @@ proc markDirtyFromQueues(j: var GcEnv; cap: ptr CaptureBufs) =
cap.sccFlags.d[s] = cap.sccFlags.d[s] or flagDirty
for i in 0..<NumStripes:
when not defined(nimYrcAtomicIncs):
when defined(yrcAtomics):
let incLen = min(atomicLoadN(addr stripes[i].toIncLen, ATOMIC_ACQUIRE), QueueSize)
for k in 0..<incLen:
taint atomicLoadN(addr stripes[i].toInc[k], ATOMIC_ACQUIRE)
else:
withLock stripes[i].lockInc:
for k in 0..<stripes[i].toIncLen:
taint stripes[i].toInc[k]
withLock stripes[i].lockDec:
for k in 0..<stripes[i].toDecLen:
# 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 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.
markDirtyFromQueues(j, cap)
# 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 very loop.
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
@@ -914,6 +971,25 @@ proc validateDead(j: var GcEnv; cap: ptr CaptureBufs) =
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
@@ -1145,14 +1221,15 @@ when defined(nimOrcStats):
proc collectCycles() =
when logOrc:
cfprintf(cstderr, "[collectCycles] begin\n")
if lockState == Collecting: return
if lockState == HasMutatorLock:
# We are inside a seq critical section (element destructors running
# under yrcMutatorLock, e.g. shrink or a seq's =destroy): becoming a
# collector here would fence-wait on our own gSeqActive counter —
# self-deadlock. Just make room in the overflowing queue; the next
# dec outside the critical section triggers the actual collection.
# (The pre-fence design instead released the mutator lock here.)
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]
@@ -1265,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)
@@ -1290,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
@@ -1349,8 +1416,6 @@ 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.}

594
lib/system/yrc_tarjan_proof.lean Normal file
View File

@@ -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).
-/