progress

`distinctBase` results in typedesc, so `set[T.distinctBase]` received
`typedesc[range[...]]` as its element type, which `isOrdinalType`
rejects. Strip the wrapper in `semSet` before storing the element type
and checking ordinality.

Also add `tyFromExpr` to the deferred-check set so the error doesn't
fire prematurely inside generic bodies - same pattern already used by
`semArray`.

.github/workflows/ci_packages.yml

@@ -38,7 +38,7 @@ jobs:
           fetch-depth: 2
 
       - name: 'Install node.js'
-        uses: actions/setup-node@v6
+        uses: actions/setup-node@v7
         with:
           node-version: 24
 

.github/workflows/ci_publish.yml

@@ -22,7 +22,7 @@ jobs:
           fetch-depth: 2
 
       - name: 'Install node.js'
-        uses: actions/setup-node@v6
+        uses: actions/setup-node@v7
         with:
           node-version: 24
 

changelog.md

@@ -12,10 +12,6 @@ rounding guarantees (via the
   avoid conflicts with `system.default`, so named argument usage for this
   parameter like `getOrDefault(..., default = ...)` will have to be changed.
 
-- Typedesc field access on object/tuple types (e.g. `Foo[int].val`) is now
-  restricted to `typeof` context. Use `--legacy:typedescFieldAccess` to restore
-  the previous behavior of allowing it outside `typeof`.
-
 - With `-d:nimPreviewCheckedClose`, the `close` function in the `std/syncio` module now raises an IO exception in case of an error.
 
 - Unknown warnings and hints now gives warnings `warnUnknownNotes` instead of

compiler/ast2nif.nim

@@ -118,13 +118,24 @@ proc toClassSymId*(config: ConfigRef; typeId: ItemId): nifstreams.SymId =
 
 type
   LineInfoWriter = object
-    fileK: FileIndex # remember the current pair, even faster than the hash table
+    # `fileK`/`fileV` cache the most recently resolved (FileIndex -> FileId) pair,
+    # faster than the hash table. `fileK` MUST be constructed at an invalid
+    # sentinel (see `newLineInfoWriter`), never zero: `FileIndex(0)` is a real file
+    # index, and `fileV` zero-inits to `FileId(0)` == `NoFile`, so a zero `fileK`
+    # would make the first lookup of the module-at-index-0 falsely hit this cache
+    # and return `NoFile` — silently dropping ALL of that module's line info.
+    fileK: FileIndex
     fileV: FileId
     tab: Table[FileIndex, FileId]
     revTab: Table[FileId, FileIndex] # reverse mapping for oldLineInfo
     man: LineInfoManager
     config: ConfigRef
 
+proc newLineInfoWriter(config: ConfigRef): LineInfoWriter =
+  # `fileK` starts invalid so the one-entry cache never collides with a real
+  # `FileIndex(0)` (see the type's doc comment).
+  LineInfoWriter(config: config, fileK: astli.InvalidFileIdx)
+
 proc get(w: var LineInfoWriter; key: FileIndex): FileId =
   if w.fileK == key:
     result = w.fileV
@@ -211,9 +222,8 @@ type
     decodedFileIndices: HashSet[FileIndex]
     locals: HashSet[ItemId]  # track proc-local symbols
     inProc: int
-    writtenTypes: seq[PType]  # types sealed during this emit; under ideActive
-    writtenSyms: seq[PSym]    # they are reset to Complete afterwards so nimsuggest
-                              # can keep mutating its still-live query targets
+    writtenTypes: seq[PType]  # types sealed during a non-owning emit
+    writtenSyms: seq[PSym]    # reset afterwards so their owner can keep using them
     writtenPackages: HashSet[string]
     depSuffixes: HashSet[string]  # module suffixes already emitted as `(import ...)` deps
     emittedBackendTypes: HashSet[(int32, int32)]  # backend-local types already def'd this
@@ -462,6 +472,9 @@ proc writeNode(w: var Writer; dest: var IcBuilder; n: PNode; forAst = false)
 proc writeType(w: var Writer; dest: var IcBuilder; typ: PType)
 proc writeSym(w: var Writer; dest: var IcBuilder; sym: PSym)
 
+func restoresWrittenState(config: ConfigRef): bool {.inline.} =
+  config.ideActive or optGenBif in config.globalOptions
+
 proc writeLoc(w: var Writer; dest: var IcBuilder; loc: TLoc) =
   dest.addIdent toNifTag(loc.k)
   dest.addIdent toNifTag(loc.storage)
@@ -558,7 +571,7 @@ proc writeType(w: var Writer; dest: var IcBuilder; typ: PType) =
     # module (or nowhere), leaving dangling references (e.g. `symbol has no
     # offset` for a `pointer` type whose itemId.module drifted away).
     typ.state = Sealed
-    if w.infos.config.ideActive: w.writtenTypes.add typ
+    if restoresWrittenState(w.infos.config): w.writtenTypes.add typ
     writeTypeDef(w, dest, typ)
   else:
     dest.addSymUse pool.syms.getOrIncl(nifTypeName(w, typ)), NoLineInfo
@@ -723,7 +736,7 @@ proc writeSym(w: var Writer; dest: var IcBuilder; sym: PSym) =
       dest.addSymUse pool.syms.getOrIncl(w.toNifSymName(sym)), NoLineInfo
   elif shouldWriteSymDef(w, sym):
     sym.state = Sealed
-    if w.infos.config.ideActive: w.writtenSyms.add sym
+    if restoresWrittenState(w.infos.config): w.writtenSyms.add sym
     writeSymDef(w, dest, sym)
   else:
     # NIF has direct support for symbol references so we don't need to use a tag here,
@@ -758,7 +771,7 @@ proc writeSymNode(w: var Writer; dest: var IcBuilder; n: PNode; sym: PSym) =
     else: shouldWriteSymDef(w, sym)
   if wantDef:
     if not sym.itemId.isBackendMinted and not isField: sym.state = Sealed
-    if w.infos.config.ideActive: w.writtenSyms.add sym
+    if restoresWrittenState(w.infos.config): w.writtenSyms.add sym
     if nodeTyp != n.sym.typImpl:
       dest.buildTree hiddenTypeTag, trLineInfo(w, n.info):
         writeType(w, dest, nodeTyp)
@@ -883,6 +896,16 @@ var reexpModTag = registerTag("reexpmod")
 var offerTag = registerTag("offer")
 var typeOfferTag = registerTag("toffer")
 var modulesrcTag = registerTag("modulesrc")
+var expansionTag = registerTag("expansion")
+# `(sig <symUse @src>)*` — signature occurrences (parameter names and the symbols
+# in their type expressions). A semchecked routine's params are dropped from the
+# serialized AST (`skipParams`) and reconstructed from `s.typ`, which holds the
+# RESOLVED type — so the source parameter names and the written type names (e.g.
+# an alias `Stream`, not `StreamObj`) carry no position in the module body. Like
+# the `expansion` records, these are teed into the `deps` side-channel: the loader
+# skips the tag, but `idetools` scans every Symbol token, so goto-def / find-usages
+# work on signatures.
+var sigTag = registerTag("sig")
 # `(unusedid <int>)` — the module's first FREE itemId after the frontend
 # (`.s.bif`) or the lower stage (`.t.bif`). The backend seeds its per-module
 # sym/type counters here so freshly-minted backend ids (closure envs, RTTI
@@ -923,6 +946,51 @@ proc registerNifAstTags*() =
   offerTag = registerTag("offer")
   typeOfferTag = registerTag("toffer")
   modulesrcTag = registerTag("modulesrc")
+  expansionTag = registerTag("expansion")
+  sigTag = registerTag("sig")
+
+proc emitSigOccurrences(w: var Writer; n: PNode) =
+  ## Record every `nkSym` in a routine-signature subtree (parameter names and the
+  ## symbols inside their type expressions, incl. the return type) as a `(sig ...)`
+  ## occurrence in the `deps` side-channel, carrying the SOURCE position. Called on
+  ## the params AST that `skipParams` is about to drop, so tooling keeps a
+  ## positioned token for each signature symbol without changing the module body
+  ## the loader / backend actually consume.
+  if n == nil: return
+  if n.kind == nkSym:
+    w.deps.addParLe sigTag, NoLineInfo
+    w.deps.addSymUse pool.syms.getOrIncl(w.toNifSymName(n.sym)), trLineInfo(w, n.info)
+    w.deps.addParRi
+  else:
+    for i in 0 ..< n.safeLen: emitSigOccurrences(w, n[i])
+
+proc emitFwdDecl(w: var Writer; n: PNode; sym: PSym) =
+  ## A routine's forward declaration (`proc foo(...)` with no body, later followed
+  ## by `proc foo(...) = ...`) is a distinct top-level node, but the routine has a
+  ## SINGLE `sdef`, emitted at the IMPLEMENTATION site (`sym.infoImpl`) — so the
+  ## prototype's own position would otherwise vanish from the `.bif`. Tee it into
+  ## the `deps` side-channel as a POSITIONED `(sig @proto <symDef>)`: the loader
+  ## skips the `sig` tag (processTopLevel), but `idetools.scanDef` finds the
+  ## `SymbolDef` and reports the enclosing tag's line info — so a `--def` on a
+  ## forward-declared proc returns TWO results (prototype + implementation), which
+  ## is desired. Safe against symbol resolution: the loader rebuilds its name->pos
+  ## table from the CONTENT body (`buildPosIndex`, written after `deps`, last write
+  ## wins) so the real `sdef` still resolves; the extra on-disk index entry has no
+  ## resolution consumer. The prototype's signature symbols (param names and the
+  ## symbols in their type expressions) are teed too, positioned at the prototype,
+  ## exactly as `emitSigOccurrences` records them for the implementation.
+  # The `SymbolDef` carries the prototype line info too (not just the enclosing
+  # tag): `scanDef` reads the position from the tag, but pass-1 `findPos` matches
+  # a token by its OWN line info, so this is what makes a query issued AT the
+  # prototype position resolve the symbol.
+  let protoInfo = trLineInfo(w, n[namePos].info)
+  let sid = pool.syms.getOrIncl(w.toNifSymName(sym))
+  w.deps.addParLe sigTag, protoInfo
+  w.deps.addSymDef sid, protoInfo   # scanDef reports this as a def
+  w.deps.addSymUse sid, protoInfo   # findPos (pass 1) / scanUses match a Symbol use
+  w.deps.addParRi
+  if sfFromGeneric notin sym.flagsImpl and paramsPos < n.safeLen:
+    emitSigOccurrences(w, n[paramsPos])
 
 proc writeNode(w: var Writer; dest: var IcBuilder; n: PNode; forAst = false) =
   if n == nil:
@@ -997,7 +1065,16 @@ proc writeNode(w: var Writer; dest: var IcBuilder; n: PNode; forAst = false) =
       # For top-level named routines (not forAst), just write the symbol.
       # The full AST will be stored in the symbol's sdef.
       if not forAst and n[namePos].kind == nkSym:
-        writeSym(w, dest, n[namePos].sym)
+        let s = n[namePos].sym
+        writeSym(w, dest, s)
+        # A forward declaration is a SECOND top-level node for `s` (body-less here;
+        # the real body — and the lone sdef — lands at the implementation). Tee the
+        # prototype's own position so goto-def / find-usages surface it as well.
+        let impl = s.astImpl
+        if n.safeLen > bodyPos and n[bodyPos].kind == nkEmpty and
+           impl != nil and impl != n and
+           impl.safeLen > bodyPos and impl[bodyPos].kind != nkEmpty:
+          emitFwdDecl(w, n, s)
       else:
         # Writing AST inside sdef or anonymous proc: write full structure
         inc w.inProc
@@ -1018,6 +1095,13 @@ proc writeNode(w: var Writer; dest: var IcBuilder; n: PNode; forAst = false) =
         w.withNode dest, ast:
           for i in 0 ..< ast.len:
             if i == paramsPos and skipParams:
+              # The dropped params still hold the source positions and the WRITTEN
+              # type names (before alias/type resolution); tee them into the `deps`
+              # side-channel for goto-def / find-usages (see `emitSigOccurrences`).
+              # Skip generic INSTANCES: their param syms are instance-specific, and
+              # the generic's own signature already records the source occurrences.
+              if sfFromGeneric notin n[namePos].sym.flagsImpl:
+                emitSigOccurrences(w, ast[i])
               # Parameters are redundant with s.typ.n (and re-emitting their syms
               # is dangerous for generic instances — we do not adapt the symbols
               # properly). Emit an `nkEmpty` placeholder rather than a dot token:
@@ -1548,8 +1632,9 @@ proc writeNifModule*(config: ConfigRef; thisModule: int32; n: PNode;
                                               genericParamsCount: int]] = @[];
                      typeOffers: seq[tuple[generic: PSym; inst: PType]] = @[];
                      resolvedImportDeps: seq[FileIndex] = @[];
-                     firstUnusedId: int32 = 0) =
-  var w = Writer(infos: LineInfoWriter(config: config), currentModule: thisModule)
+                     firstUnusedId: int32 = 0;
+                     expansions: seq[(PSym, TLineInfo)] = @[]) =
+  var w = Writer(infos: newLineInfoWriter(config), currentModule: thisModule)
   w.deps = newIcBuilder(64)
   var content = newIcBuilder(300)
 
@@ -1626,6 +1711,17 @@ proc writeNifModule*(config: ConfigRef; thisModule: int32; n: PNode;
   w.deps.addStrLit toFullPath(config, FileIndex(thisModule))
   w.deps.addParRi
 
+  # Template/macro expansions leave no trace in the sem'checked AST, so record
+  # each as `(expansion <symUse @call-site>)`: a `Symbol` use of the expanded
+  # routine carrying the ORIGINAL call-site line info. The loader skips the tag
+  # (processTopLevel), but `idetools` scans every `Symbol` token in the buffer,
+  # so this restores "find usages / goto-def" for templates and macros.
+  for (sym, info) in expansions:
+    if sym == nil: continue
+    w.deps.addParLe expansionTag, NoLineInfo
+    w.deps.addSymUse pool.syms.getOrIncl(w.toNifSymName(sym)), trLineInfo(w, info)
+    w.deps.addParRi
+
   # Generic TYPE-instance OFFERS: the `tyGenericInst` types this module created
   # (e.g. `HashArray[8192, Gwei]`). Non-IC keeps ONE such instance in the global
   # `typeInstCache`, so a structural bound computed at the first instantiation
@@ -1694,17 +1790,15 @@ proc writeNifModule*(config: ConfigRef; thisModule: int32; n: PNode;
       let s = op.sym
       if s.state != Sealed:
         s.state = Sealed
-        if config.ideActive: w.writtenSyms.add s
+        if restoresWrittenState(config): w.writtenSyms.add s
         writeSymDef w, dest, s
 
   dest.addParRi()
 
-  # nimsuggest reuses these symbols/types as live, mutable query targets (sem
-  # re-runs, usage tracking, flag updates). Sealing is only needed for intra-emit
-  # dedup; once the NIF is built, un-seal so suggest can keep mutating them
-  # (matches `loadedState` loading Complete under ideActive). The `Sealed` guard
-  # stays in force for a real `nim m`/`nim nifc` build.
-  if config.ideActive:
+  # Nimsuggest and normal code generation reuse these symbols/types as live,
+  # mutable targets. Sealing is only needed for intra-emit dedup; once the NIF
+  # is built, un-seal them. The guard stays in force for a real `nim m` build.
+  if restoresWrittenState(config):
     for s in w.writtenSyms:
       if s.state == Sealed: s.state = Complete
     for t in w.writtenTypes:
@@ -1824,7 +1918,7 @@ type
 
 proc createDecodeContext*(config: ConfigRef; cache: IdentCache): DecodeContext =
   ## Supposed to be a global variable
-  result = DecodeContext(infos: LineInfoWriter(config: config), cache: cache)
+  result = DecodeContext(infos: newLineInfoWriter(config), cache: cache)
 
 var loadStatsInit {.threadvar.}: int          # 0=unknown 1=on 2=off
 var statsCtxPtr {.threadvar.}: ptr DecodeContext
@@ -3251,6 +3345,14 @@ proc processTopLevel(c: var DecodeContext; cur: var Cursor; flags: set[LoadFlag]
         # self-identification record for the standalone include-graph scanner;
         # not needed by the loader, just skip past it.
         skip cur
+      elif tagIs(cur, "expansion"):
+        # template/macro expansion usage record for tooling (`idetools` scans it
+        # as a `Symbol` use); the loader itself needs nothing from it.
+        skip cur
+      elif tagIs(cur, "sig"):
+        # signature-symbol occurrence record for tooling (`idetools` scans it as a
+        # `Symbol` use); the loader itself needs nothing from it.
+        skip cur
       elif tagIs(cur, "implementation"):
         cont = false
       elif LoadFullAst in flags or tagIs(cur, toNifTag(nkLetSection)) or
@@ -3312,7 +3414,7 @@ proc writeLoweredModule*(c: var DecodeContext; config: ConfigRef;
   # types/globals/params/locals stay Complete and emit real defs (the `.t.nif` is
   # the sole source the cg stage reads — no `.s.nif` fallback for them).
   sealLoadedRoutines(c)
-  var w = Writer(infos: LineInfoWriter(config: config), currentModule: thisModule)
+  var w = Writer(infos: newLineInfoWriter(config), currentModule: thisModule)
   w.deps = newIcBuilder(64)
   w.inProc = 1
   w.lowering = true
@@ -3438,4 +3540,3 @@ when isMainModule:
   echo obj.name, " ", obj.module, " ", obj.count
   let objb = parseSymName("abcdef.0121")
   echo objb.name, " ", objb.module, " ", objb.count
-

compiler/ccgexprs.nim

@@ -3143,6 +3143,12 @@ proc genMagicExpr(p: BProc, e: PNode, d: var TLoc, op: TMagic) =
       localError(p.config, e.info,
         "for --mm:arc|atomicArc|orc 'deepcopy' support has to be enabled with --deepcopy:on")
 
+    let typ = e[1].typ.skipTypes({tyVar, tyRef, tyGenericInst, tyTypeDesc,
+                                   tyAlias, tyInferred, tySink, tyLent, tyOwned})
+    if hasDisabledAsgn(p.module.g.graph, typ):
+      localError(p.config, e.info,
+        "'deepCopy' is not available for type <" & typeToString(typ) & ">")
+
     let x = if e[1].kind in {nkAddr, nkHiddenAddr}: e[1][0] else: e[1]
     var a = initLocExpr(p, x)
     var b = initLocExpr(p, e[2])

compiler/closureiters.nim

@@ -336,9 +336,14 @@ proc collectExceptState(ctx: var Ctx, n: PNode): PNode {.inline.} =
         var cond: PNode = nil
         for i in 0..<c.len - 1:
           assert(c[i].kind == nkType)
+          # Use the :curExc env field (set by the wrapper before entering the
+          # except landing state) instead of calling getCurrentException():
+          # injectdestructors does not process the args of this raw generic
+          # `of` magic call, so an owning getCurrentException() temp would
+          # never be destroyed and the caught exception would leak (#23615).
           let nextCond = newTreeIT(nkCall, c.info, ctx.g.getSysType(c.info, tyBool),
             newSymNode(g.getSysMagic(c.info, "of", mOf)),
-            g.callCodegenProc("getCurrentException"),
+            ctx.newCurExcAccess(),
             c[i])
 
           cond = if cond.isNil: nextCond

compiler/commands.nim

@@ -509,6 +509,7 @@ proc parseCommand*(command: string): Command =
   of "nifc": cmdNifC  # generate C from NIF files
   of "ic": cmdIc  # generate .build.nif for nifmake
   of "icconfig": cmdIcConfig  # produce the precompiled config artifact
+  of "track": cmdTrack  # IDE goto-def / find-usages over `nim ic`'s NIF output
   else: cmdUnknown
 
 proc setCmd*(conf: ConfigRef, cmd: Command) =
@@ -825,6 +826,8 @@ proc processSwitch*(switch, arg: string, pass: TCmdLinePass, info: TLineInfo;
       localError(conf, info, "expected nim|cpp but found " & arg)
   of "compress":
     conf.globalOptions.incl optCompress
+  of "genbif":
+    processOnOffSwitchG(conf, {optGenBif}, arg, pass, info)
   of "g": # alias for --debugger:native
     conf.globalOptions.incl optCDebug
     conf.options.incl optLineDir
@@ -1324,8 +1327,16 @@ proc processArgument*(pass: TCmdLinePass; p: OptParser;
       # support UNIX style filenames everywhere for portable build scripts:
       if config.projectName.len == 0:
         config.projectName = unixToNativePath(p.key)
-      config.arguments = cmdLineRest(p)
-      result = true
+      if config.cmd == cmdTrack:
+        # `nim track PROJ --def:...`: unlike a normal command (where everything
+        # after the project file is passed to the compiled program), `track`
+        # accepts its IDE-query switches AFTER the project — the natural,
+        # nimsuggest-like invocation form. So don't swallow the rest of the line
+        # into `arguments`; keep parsing the remaining tokens as switches.
+        result = false
+      else:
+        config.arguments = cmdLineRest(p)
+        result = true
     else:
       result = false
   inc argsCount

compiler/deps.nim

@@ -590,6 +590,98 @@ proc readDepsFile(c: var DepContext; pair: FilePair; current: Node) =
           elif t.kind == ParRi: dec depth
     t = next(s)
 
+proc collectIncludeNames(depsPath: string; names: var seq[string]) =
+  ## Lightweight scan of a `.deps.nif` prelude: collect the raw path text of
+  ## every entry inside an `(include ...)` node (idents like `semexprs`, string
+  ## literals like `"system/mmdisp"`, and the leaves of `a/b` path infixes).
+  ## Liberal by design — it also picks up entries under a statically-false
+  ## `(when ...)`; that is harmless for the only caller (`includerSbifs`), whose
+  ## over-collection just costs an extra, result-free bif scan downstream.
+  if not fileExists(depsPath): return
+  var s = nifstreams.open(depsPath)
+  defer: nifstreams.close(s)
+  discard processDirectives(s.r)
+  var depth = 0
+  var includeDepth = 0     # the `depth` at which the current `(include` opened; 0 = not inside one
+  var t = next(s)
+  while t.kind != EofToken:
+    case t.kind
+    of ParLe:
+      inc depth
+      if includeDepth == 0 and pool.tags[t.tagId] == "include":
+        includeDepth = depth
+    of ParRi:
+      if includeDepth != 0 and depth == includeDepth:
+        includeDepth = 0
+      dec depth
+    of Ident, StringLit:
+      if includeDepth != 0:
+        names.add pool.strings[t.litId]
+    else: discard
+    t = next(s)
+
+proc entryStemBase(roots: seq[string]; name: string): (string, string) =
+  ## Resolve include entry `name` to (deps-stem, base-name); ("","") if unfound.
+  for r in roots:
+    let p = r / name.addFileExt("nim")
+    if fileExists(p):
+      return (moduleSuffix(p, []), splitFile(p).name)
+  result = ("", "")
+
+proc includerSbifs*(conf: ConfigRef; targetFile: AbsoluteFile): seq[string] =
+  ## For an include file `targetFile`, return the `.s.bif` paths of every module
+  ## that includes it — directly OR transitively (following the include chain
+  ## `module -> incA -> incB -> targetFile`). `nim track` uses this to avoid
+  ## loading and scanning every module bif: an include file has no bif of its
+  ## own, so its type-checked tokens live in the *including* module's bif. Only
+  ## the small `.deps.nif` preludes are read here, never a `.s.bif`.
+  const depsExt = ".deps.nif"
+  let nc = getNimcacheDir(conf).string
+
+  # Candidate roots for resolving an `(include X)` entry to a real file, so its
+  # module suffix (== its own deps-file stem) can be computed. Include entries
+  # carry any sub-path (`system/mmdisp`), so the file's *directory* roots suffice:
+  # the target's own dir, the project dir, and the search paths cover the
+  # compiler, the stdlib and typical single-tree projects.
+  var roots: seq[string] = @[parentDir(targetFile.string)]
+  if conf.projectPath.string.len > 0: roots.add conf.projectPath.string
+  for sp in conf.searchPaths: roots.add sp.string
+
+  # One pass over every prelude builds the reverse include graph, keyed by base
+  # file name: `includedBy[b]` = deps stems whose owner directly `include`s a
+  # file named `b`. `stemBase` maps an include-only file's deps stem back to its
+  # own base name, so the walk can climb through nested includes.
+  var includedBy = initTable[string, seq[string]]()
+  var stemBase = initTable[string, string]()
+  for depsPath in walkFiles(nc / "*" & depsExt):
+    let base = extractFilename(depsPath)
+    if base.endsWith(".p" & depsExt): continue   # `.p.deps.nif` twin
+    let ownerStem = base[0 ..< base.len - depsExt.len]
+    var names: seq[string] = @[]
+    collectIncludeNames(depsPath, names)
+    for n in names:
+      let (childStem, childBase) = entryStemBase(roots, n)
+      if childBase.len == 0: continue
+      includedBy.mgetOrPut(childBase, @[]).add ownerStem
+      stemBase[childStem] = childBase          # this child's stem -> its base name
+
+  # Walk UP from the target: a deps stem that includes the current base name is
+  # either a module (has a `.s.bif` -> collect it) or itself an include file
+  # (recurse via its own base name).
+  result = @[]
+  var seenBase = initHashSet[string]()
+  var work = @[splitFile(targetFile.string).name]
+  while work.len > 0:
+    let b = work.pop()
+    if seenBase.containsOrIncl(b): continue
+    for stem in includedBy.getOrDefault(b):
+      let sbif = nc / stem & ".s.bif"
+      if fileExists(sbif):
+        if sbif notin result: result.add sbif   # module owner
+      else:
+        let ob = stemBase.getOrDefault(stem)     # include-only owner: climb higher
+        if ob.len > 0: work.add ob
+
 proc traverseDeps(c: var DepContext; pair: FilePair; current: Node) =
   ## Process a module: run nifler and read deps
   if not runNifler(c, pair.nimFile):
@@ -1134,8 +1226,12 @@ proc generateBackendBuildFile(c: DepContext; forwardedArgs: seq[string]): string
 
   b.endTree()  # stmts
 
-proc commandIc*(conf: ConfigRef) =
-  ## Main entry point for `nim ic`
+proc commandIc*(conf: ConfigRef; frontendOnly = false) =
+  ## Main entry point for `nim ic`. With `frontendOnly` (used by `nim track` for
+  ## IDE queries) it runs only Phase 1 — the incremental nifler + `nim m`
+  ## frontend that writes every module's `.s.bif` — and skips the whole-program
+  ## backend (`nim nifc` -> C -> link), which a goto-def / find-usages scan does
+  ## not need.
   when not defined(nimKochBootstrap):
     let nifler = findNifler()
     if nifler.len == 0:
@@ -1275,10 +1371,12 @@ proc commandIc*(conf: ConfigRef) =
       if nifmake.len == 0:
         rawMessage(conf, hintSuccess, "run:" & " nifmake run" & parallel & " " & buildFile)
         # without nifmake we can only print the manual commands; emit the
-        # backend's too (best effort — discovery cannot run) and stop.
-        let backendFile = generateBackendBuildFile(c, forwardedArgs)
-        rawMessage(conf, hintSuccess, "generated: " & backendFile)
-        rawMessage(conf, hintSuccess, "run:" & " nifmake run" & parallel & " " & backendFile)
+        # backend's too (best effort — discovery cannot run) and stop. An IDE
+        # query (`frontendOnly`) needs no backend, so skip it there.
+        if not frontendOnly:
+          let backendFile = generateBackendBuildFile(c, forwardedArgs)
+          rawMessage(conf, hintSuccess, "generated: " & backendFile)
+          rawMessage(conf, hintSuccess, "run:" & " nifmake run" & parallel & " " & backendFile)
         return
       let cmd = quoteShell(nifmake) & " run" & parallel & " " & quoteShell(buildFile)
       rawMessage(conf, hintExecuting, cmd)
@@ -1322,7 +1420,9 @@ proc commandIc*(conf: ConfigRef) =
     # Phase 2 — backend (whole-program `nim nifc`), run once over the now-final
     # graph. Kept a separate nifmake run so backend rebuilds are decided purely
     # by nifmake's input mtimes, independent of frontend discovery.
-    if frontendOk:
+    # An IDE query (`frontendOnly`) stops after Phase 1: the `.s.bif` it scans
+    # are all produced by the frontend; codegen + link would be wasted work.
+    if frontendOk and not frontendOnly:
       let backendFile = generateBackendBuildFile(c, forwardedArgs)
       rawMessage(conf, hintSuccess, "generated: " & backendFile)
       let cmd = quoteShell(nifmake) & " run" & parallel & " " & quoteShell(backendFile)

compiler/icconfig.nim

@@ -260,17 +260,26 @@ proc ensureIcConfig*(conf: ConfigRef) =
   if not fileExists(outPath) or sourcesChanged(outPath):
     createDir(cacheDir)
     # Re-invoke ourselves as the config producer: reuse this process's command
-    # line, dropping the command argument (`ic`) in favour of `icconfig` and the
-    # explicit output path, both BEFORE the project file (anything after the
-    # project is swallowed into `config.arguments` by `cmdLineRest`). The
-    # producer re-reads `nim.cfg` itself.
+    # line, dropping the command argument (`ic`/`track`) in favour of `icconfig`
+    # and the explicit output path. Every switch must land BEFORE the project
+    # file, because anything after the project is swallowed into
+    # `config.arguments` by `cmdLineRest` (and a non-empty `arguments` without
+    # `--run` is a hard error). Callers may legitimately put switches after the
+    # project — `nim track PROJ --def:...` — so we re-order rather than replay
+    # verbatim: all `-`-prefixed switches first (in encounter order), then the
+    # non-switch project token(s). The producer re-reads `nim.cfg` itself.
     var pargs = @["icconfig", "--icConfigOut:" & outPath]
+    var rest: seq[string] = @[]
     var droppedCmd = false
     for a in commandLineParams():
-      if not droppedCmd and a.len > 0 and a[0] != '-':
-        droppedCmd = true  # drop the original command token (`ic`)
-      else:
+      if a.len == 0: continue
+      if a[0] == '-':
         pargs.add a
+      elif not droppedCmd:
+        droppedCmd = true  # drop the original command token (`ic`/`track`)
+      else:
+        rest.add a  # project file (and any further non-switch tokens) go last
+    for a in rest: pargs.add a
     let p = startProcess(getAppFilename(), args = pargs,
                          options = {poStdErrToStdOut})
     let outp = p.outputStream.readAll()

compiler/idetools.nim

@@ -0,0 +1,279 @@
+#
+#
+#           The Nim Compiler
+#        (c) Copyright 2026 Andreas Rumpf
+#
+#    See the file "copying.txt", included in this
+#    distribution, for details about the copyright.
+#
+
+## NIF-based goto-definition / find-all-usages for `nim track`.
+##
+## This is the mainline-Nim port of nimony's `idetools.nim`. It answers a
+## `--def:FILE,LINE,COL` / `--usages:FILE,LINE,COL` query by *scanning the
+## `.s.bif` files* (binary NIF, see `dist/nimony/src/lib/bif.nim`) that the
+## preceding `nim ic` frontend (`nim track`) emitted into the nimcache directory
+## — NOT by re-running sem. NIF distinguishes a definition (`SymbolDef` token) from a use
+## (`Symbol` token) syntactically, so goto-def / find-uses become plain token
+## scans over type-checked NIF, which is more reliable than the classic PSym
+## engine because generics and macros are type-checked in the NIF too.
+##
+## Two passes (mirroring nimony's `usages`):
+##  1. Load the queried module's `.s.bif` and find the `Symbol`/`SymbolDef`
+##     token whose line info + identifier length contains `conf.m.trackPos`.
+##     That yields the mangled symbol NAME and whether it is global (>= 2 dots).
+##  2. `--usages`: emit every `Symbol` (use) token; `--def`: every `SymbolDef`.
+##     A global symbol is scanned across every module `.s.bif`; a local one only
+##     within the queried module.
+##
+## IMPORTANT porting note: `bif.load` mints FRESH per-file pools, so a `SymId`
+## from module A's buffer is meaningless in module B's. The cross-module match is
+## therefore by the mangled NAME string, never by `SymId` (nimony can compare ids
+## because it parses every text NIF into one shared global pool; we cannot).
+
+import std / [os, strutils, sets]
+import options, msgs, pathutils
+import lineinfos as astli
+import ast2nif   # toNifFilename
+from deps import includerSbifs   # deps-guided include-file lookup
+import "../dist/nimony/src/lib/nifcore"
+from "../dist/nimony/src/lib" / bif import load, BifModule, containsSym
+
+proc identLen(name: string): int =
+  ## Length of the displayed identifier: the run before the first `.` of a
+  ## mangled NIF name (`ident.disamb[.moduleSuffix]`). Bounds the column match.
+  let d = name.find('.')
+  result = if d < 0: name.len else: d
+
+proc isGlobalName(name: string): bool =
+  ## A global symbol carries `ident.disamb.moduleSuffix` (>= 2 dots); a local at
+  ## most `ident.disamb` (<= 1 dot). `moduleSuffix` is a dot-free hash, so a raw
+  ## dot count is equivalent to nifbuilder's suffix-compressed test for our use.
+  var dots = 0
+  for i in 1 ..< name.len:
+    if name[i] == '.': inc dots
+  result = dots >= 2
+
+proc posMatch(c: Cursor; conf: ConfigRef; target: TLineInfo; tokenLen: int): bool =
+  ## True when `target` (the queried position) falls within the identifier span
+  ## of the Symbol/SymbolDef token at `c`. Mirrors nimony's `lineInfoMatch`; the
+  ## filename is resolved through the loaded buffer's own pool (fresh per file),
+  ## then mapped to a `FileIndex` exactly like `ast2nif.oldLineInfo`.
+  let li = rawLineInfo(c)
+  if not li.isValid: return false
+  if li.line.int != target.line.int: return false
+  let f = fileInfoIdx(conf, AbsoluteFile lineInfoFile(c))
+  if f != target.fileIndex: return false
+  if target.col.int < li.col.int: return false
+  if target.col.int > li.col.int + tokenLen: return false
+  result = true
+
+const sep = '\t'
+
+proc formatSuggest(s: Suggest): string =
+  ## Reproduce `suggest.$Suggest` for the `ideDef`/`ideUse` sections without
+  ## importing `suggest` (which would create an import cycle). Layout:
+  ## `section⭾symkind⭾qualifiedPath⭾forth⭾filePath⭾line⭾column⭾⭾quality`.
+  ## symkind is always `skUnknown` here — the raw NIF scan has no PSym to give a
+  ## real kind (like nimony's `foundSymbol`, which leaves it empty).
+  result = $s.section
+  result.add sep
+  result.add "skUnknown"
+  result.add sep
+  if s.qualifiedPath.len != 0:
+    result.add s.qualifiedPath.join(".")
+  result.add sep
+  result.add s.forth
+  result.add sep
+  result.add s.filePath
+  result.add sep
+  result.add $s.line
+  result.add sep
+  result.add $s.column
+  result.add sep            # empty doc field (docgen is off outside nimsuggest)
+  if s.version == 0 or s.version == 3:
+    result.add sep
+    result.add $s.quality
+
+proc emit(conf: ConfigRef; c: Cursor; section: IdeCmd; name: string;
+          seen: var HashSet[string]) =
+  ## Report one hit as a nimsuggest-compatible result (routed through the
+  ## structured-output hook / `--stdout`). We only have the mangled name + line
+  ## info from the raw NIF, so symkind/type are left empty — like nimony's
+  ## `foundSymbol`. `seen` deduplicates: the same source location can back
+  ## several NIF `Symbol` tokens (e.g. a call argument re-emitted in a lowered
+  ## form), which must surface as one hit.
+  let li = rawLineInfo(c)
+  if not li.isValid: return
+  let key = $section.int & ":" & lineInfoFile(c) & ":" & $li.line.int & ":" & $li.col.int
+  if seen.containsOrIncl(key):
+    return  # already reported this location for this section
+  let s = Suggest(section: section,
+                  qualifiedPath: @[name[0 ..< identLen(name)]],
+                  filePath: lineInfoFile(c),
+                  line: li.line.int,
+                  column: li.col.int,
+                  tokenLen: identLen(name),
+                  forth: "",
+                  symkind: 0'u8,
+                  quality: 100,
+                  version: conf.suggestVersion)
+  if conf.suggestionResultHook != nil:
+    conf.suggestionResultHook(s)
+  else:
+    conf.suggestWriteln(formatSuggest(s))
+
+proc tokenSymId(c: Cursor): SymId {.inline.} =
+  ## SymId (in the cursor's own per-file pool) of a `Symbol`/`SymbolDef` token,
+  ## or `SymId(0)` for an inline-encoded one — which is never our search target:
+  ## a mangled name (`ident.disamb.suffix`) is always longer than
+  ## `StrInlineMaxLen`, so every occurrence of the symbol we look for is stored by
+  ## pool id, decoded here with a shift and no string materialization.
+  if isInlineLit(c): SymId(0) else: SymId(combinedPayload(c) shr 1)
+
+template symMatches(c: Cursor): bool =
+  ## True when the token at `c` is the searched symbol. The fast path is a pure
+  ## integer compare against `targetSym` (the symbol's id in THIS module's pool,
+  ## resolved once per file by the caller). `targetSym == 0` means the name is not
+  ## representable as a pool id (a rare <=3-byte local): fall back to a string
+  ## compare, correct for both inline and pooled encodings.
+  (if targetSym != SymId(0): tokenSymId(c) == targetSym else: symName(c) == targetName)
+
+proc scanUses(conf: ConfigRef; m: var BifModule; targetSym: SymId; targetName: string;
+              seen: var HashSet[string]) =
+  ## `--usages`: report every `Symbol` (use) occurrence with valid line info.
+  if m.buf.len == 0: return
+  var c = m.buf.beginRead()
+  while c.hasMore:
+    if c.kind == Symbol and symMatches(c) and rawLineInfo(c).isValid:
+      emit(conf, c, ideUse, targetName, seen)
+    inc c
+  c.endRead()
+
+proc scanDef(conf: ConfigRef; m: var BifModule; targetSym: SymId; targetName: string;
+             seen: var HashSet[string]) =
+  ## `--def`: report the declaration of the target symbol if this module owns it
+  ## (has its `SymbolDef`). The `SymbolDef` token itself carries no line info; the
+  ## declaration location lives on the *enclosing tag* (e.g. `(sd @file:line:col`,
+  ## like `bif.buildIndex`'s `mostRecentTagPos`). When that tag has no line info
+  ## either, fall back to the declaration-site `Symbol` occurrence — but only in
+  ## the owning module, so a plain user of the symbol is never reported as a def.
+  if m.buf.len == 0: return
+  var c = m.buf.beginRead()
+  var mostRecentTagPos = 0
+  var sawDef = false
+  var emitted = false
+  var fallbackPos = -1
+  while c.hasMore:
+    case c.kind
+    of TagLit:
+      mostRecentTagPos = cursorToPosition(m.buf, c)
+      inc c
+    of SymbolDef:
+      if symMatches(c):
+        sawDef = true
+        var tc = cursorAt(m.buf, mostRecentTagPos)
+        if rawLineInfo(tc).isValid:
+          emit(conf, tc, ideDef, targetName, seen)
+          emitted = true
+        tc.endRead()
+      inc c
+    of Symbol:
+      if fallbackPos < 0 and symMatches(c) and rawLineInfo(c).isValid:
+        fallbackPos = cursorToPosition(m.buf, c)
+      inc c
+    else:
+      inc c
+  c.endRead()
+  if sawDef and not emitted and fallbackPos >= 0:
+    var fc = cursorAt(m.buf, fallbackPos)
+    emit(conf, fc, ideDef, targetName, seen)
+    fc.endRead()
+
+proc scanBuf(conf: ConfigRef; m: var BifModule; section: IdeCmd;
+             targetSym: SymId; targetName: string; seen: var HashSet[string]) =
+  ## Emit hits for the target symbol in `m` per the query kind. `ideDus`
+  ## (`--defusages`) reports both the definition and every usage.
+  if section in {ideDef, ideDus}:
+    scanDef(conf, m, targetSym, targetName, seen)
+  if section in {ideUse, ideDus}:
+    scanUses(conf, m, targetSym, targetName, seen)
+
+proc findPos(conf: ConfigRef; m: var BifModule; target: TLineInfo;
+             foundName: var string): bool =
+  ## Scan `m` for the `Symbol`/`SymbolDef` token covering the queried position
+  ## `target` and set `foundName` to its mangled name. Returns true on a hit.
+  if m.buf.len == 0: return false
+  var c = m.buf.beginRead()
+  result = false
+  while c.hasMore:
+    let k = c.kind
+    if k == Symbol or k == SymbolDef:
+      let nm = symName(c)
+      if posMatch(c, conf, target, identLen(nm)):
+        foundName = nm
+        result = true
+        break
+    inc c
+  c.endRead()
+
+proc runIdeQuery*(conf: ConfigRef) =
+  ## Entry point: called from `main.nim` after `commandCheck` when a
+  ## `--def`/`--usages` query is active. Assumes the check just emitted the
+  ## project's `.s.bif` files into `getNimcacheDir(conf)`.
+  let section = conf.ideCmd
+  if section notin {ideDef, ideUse, ideDus}: return
+  let target = conf.m.trackPos
+  if target.fileIndex.int32 < 0: return
+
+  # Pass 1: position -> symbol. Try the queried file's own module bif first (the
+  # fast path when the position is inside a real module). An include file has no
+  # module bif of its own — its tokens live in the *including* module's bif with
+  # include-file line info — so when the direct lookup misses, consult the
+  # `.deps.nif` preludes (`includerSbifs`) to load only the module(s) that
+  # include the queried file (directly or transitively), never every bif in the
+  # nimcache. `ownerFile` is the bif that owns the hit.
+  let modFile = toNifFilename(conf, target.fileIndex)
+  var foundName = ""
+  var ownerFile = ""
+  if fileExists(modFile):
+    var qm = load(modFile)
+    if findPos(conf, qm, target, foundName):
+      ownerFile = modFile
+  if foundName.len == 0:
+    for cand in includerSbifs(conf, toFullPath(conf, target.fileIndex).AbsoluteFile):
+      if cand == modFile: continue
+      var m = load(cand)
+      if findPos(conf, m, target, foundName):
+        ownerFile = cand
+        break
+  if foundName.len == 0: return
+
+  # Pass 2: emit definition / usages. `seen` spans every module so a location is
+  # reported once even when scanned across the whole nimcache.
+  #
+  # Cross-file matching is by SymId, not by decoding every token's name. Two
+  # filters keep it cheap:
+  #   1. `bif.containsSym` — a sym-table-only probe that reads just the small
+  #      trailing pools, NOT the token block or any `BiTable`. A module that never
+  #      references the symbol is rejected here without a full `load` (no pools
+  #      built, no token block mapped) — so a query whose symbol lives in a few
+  #      modules no longer pays to load the whole nimcache.
+  #   2. For a module that does contain it, `bif.load` mints a fresh per-file pool,
+  #      so the name is resolved to THIS file's SymId once via `getKeyId`; the scan
+  #      then compares integer ids per token instead of materializing a string for
+  #      each (see `symMatches`).
+  var seen = initHashSet[string]()
+  if isGlobalName(foundName):
+    for f in walkFiles((getNimcacheDir(conf).string) / "*.s.bif"):
+      if not containsSym(f, foundName): continue
+      var m = load(f)
+      let tid = m.buf.pool.syms.getKeyId(foundName)
+      if tid != SymId(0):
+        scanBuf(conf, m, section, tid, foundName, seen)
+  else:
+    # Local symbol: its mangled name is not unique across modules, so restrict
+    # the scan to the module it lives in (the one that owns the queried position).
+    var qm = load(ownerFile)
+    let tid = qm.buf.pool.syms.getKeyId(foundName)
+    scanBuf(conf, qm, section, tid, foundName, seen)

compiler/injectdestructors.nim

@@ -24,7 +24,7 @@ import std/[strtabs, tables, strutils, intsets]
 when defined(nimPreviewSlimSystem):
   import std/assertions
 
-from trees import exprStructuralEquivalent, getRoot, whichPragma, getPotentialWrites
+from trees import exprStructuralEquivalent, getRoot, isCursor, whichPragma, getPotentialWrites
 
 type
   Con = object
@@ -180,17 +180,6 @@ proc isFirstWrite(n: PNode; c: var Con): bool =
   let m = skipConvDfa(n)
   result = nfFirstWrite in m.flags
 
-proc isCursor(n: PNode): bool =
-  case n.kind
-  of nkSym:
-    sfCursor in n.sym.flags
-  of nkDotExpr:
-    isCursor(n[1])
-  of nkCheckedFieldExpr:
-    isCursor(n[0])
-  else:
-    false
-
 template isFullyUnpackedTuple(n: PNode): bool =
   ## we move out all elements of unpacked tuples,
   ## hence unpacked tuples themselves don't need to be destroyed

compiler/liftdestructors.nim

@@ -94,11 +94,21 @@ proc defaultOp(c: var TLiftCtx; t: PType; body, x, y: PNode) =
     body.add genBuiltin(c, mWasMoved, "wasMoved", x)
 
 proc genAddr(c: var TLiftCtx; x: PNode): PNode =
-  if x.kind == nkHiddenDeref:
+  # These synthesized addresses are always passed to codegen procs that expect a
+  # genuine pointer (nimAsgnYrc, nimSinkYrc, destructors, ...). `addr(deref x)`
+  # collapses to `x` only when `x` is a real pointer; on the C++ backend a `var`
+  # parameter is a C++ reference, so we must keep the `nkHiddenAddr` to actually
+  # take its address (`&dest`) instead of passing the reference's value. Likewise
+  # `tfVarIsPtr` keeps the C++ backend from lowering the synthesized address back
+  # to a reference and dropping the `&` (e.g. a closure's `tyPointer` env). See
+  # #26026 CI (yrc + cpp).
+  if x.kind == nkHiddenDeref and c.g.config.backend != backendCpp:
     checkSonsLen(x, 1, c.g.config)
     result = x[0]
   else:
-    result = newNodeIT(nkHiddenAddr, x.info, makeVarType(x.typ.owner, x.typ, c.idgen))
+    let addrTyp = makeVarType(x.typ.owner, x.typ, c.idgen)
+    addrTyp.incl tfVarIsPtr
+    result = newNodeIT(nkHiddenAddr, x.info, addrTyp)
     result.add x
 
 proc genWhileLoop(c: var TLiftCtx; i, dest: PNode): PNode =

compiler/main.nim

@@ -34,6 +34,7 @@ from icconfig import produceIcConfig
 when not defined(nimKochBootstrap):
   import nifbackend
   import deps
+  import idetools
 
 when not defined(leanCompiler):
   import docgen
@@ -416,6 +417,20 @@ proc mainCommand*(graph: ModuleGraph) =
       for it in conf.searchPaths: msgWriteln(conf, it.string)
   of cmdCheck:
     commandCheck(graph)
+  of cmdTrack:
+    # `nim track --def:/--usages:/--track:` — IDE goto-definition / find-usages.
+    # Runs `nim ic`'s incremental frontend (nifler + per-module `nim m`, so only
+    # changed modules recompile and each writes a faithful, VM-executed `.s.bif`
+    # — covering stdlib too), then scans those NIF files (idetools.runIdeQuery).
+    # Shares the `nim ic` nimcache dir, so a prior `nim ic` build is reused.
+    setUseIc(true)
+    wantMainModule(conf)
+    setOutFile(conf)
+    when not defined(nimKochBootstrap):
+      commandIc(conf, frontendOnly = true)
+      runIdeQuery(conf)
+    else:
+      rawMessage(conf, errGenerated, "nim track not available in bootstrap build")
   of cmdM:
     # cmdM uses NIF files, not ROD files
     graph.config.symbolFiles = disabledSf

compiler/modulegraphs.nim

@@ -177,6 +177,11 @@ type
 
     procGlobals*: seq[PNode]
     nifReplayActions*: Table[int32, seq[PNode]]  # module position -> replay actions for NIF
+    nifExpansions*: Table[int32, seq[(PSym, TLineInfo)]]
+      # module position -> (template/macro sym, call-site info) for every expansion
+      # in that module. Templates/macros leave no trace in the sem'checked AST, so
+      # this side-channel (written into the `.bif`, see ast2nif) is what lets
+      # `nim track --usages`/`--def` find them. Populated by `rememberExpansion`.
     cachedMods: IntSet
     hookClosure: IntSet # modules whose serialized hooks were already registered
 

compiler/nim.nim

@@ -120,7 +120,7 @@ proc handleCmdLine(cache: IdentCache; conf: ConfigRef) =
   # so `loadConfigs` replays it instead of re-parsing the `nim.cfg` chain — the
   # driver runs on the exact same config its children will. See icconfig.nim.
   when not defined(nimKochBootstrap):
-    if conf.cmd == cmdIc:
+    if conf.cmd in {cmdIc, cmdTrack}:
       ensureIcConfig(conf)
 
   var graph = newModuleGraph(cache, conf)
@@ -134,7 +134,7 @@ proc handleCmdLine(cache: IdentCache; conf: ConfigRef) =
   if conf.selectedGC == gcUnselected:
     if conf.backend in {backendC, backendCpp, backendObjc} or
         (conf.cmd in cmdDocLike and conf.backend != backendJs) or
-        conf.cmd in {cmdGendepend, cmdNifC, cmdIc, cmdM}:
+        conf.cmd in {cmdGendepend, cmdNifC, cmdIc, cmdM, cmdTrack}:
       initOrcDefines(conf)
 
   if conf.selectedStrings == stringSso and

compiler/options.nim

@@ -29,7 +29,7 @@ const
 
   nimEnableCovariance* = defined(nimEnableCovariance)
 
-  icFormatVersion* = "29"
+  icFormatVersion* = "30"
     ## Version of the IC cache format (the sem-NIF module layout written by
     ## ast2nif.nim plus the iface/impl/edges side files). Bump it whenever
     ## that layout changes: `commandIc` wipes a nimcache whose `ic.version`
@@ -140,6 +140,7 @@ type                          # please make sure we have under 32 options
     optDocRaw                 # for documentation: Don't render markdown for JSON output
     optItaniumMangle          # mangling follows the Itanium spec
     optCompress               # turn on AST compression by converting it to NIF
+    optGenBif                 # generate semantic BIF alongside ordinary code generation
     optWithinConfigSystem     # we still compile within the configuration system
 
   TGlobalOptions* = set[TGlobalOption]
@@ -205,6 +206,7 @@ type
     cmdNifC  # generate C code from NIF files
     cmdIc  # generate .build.nif for nifmake
     cmdIcConfig # `nim ic`'s precompiled-config producer (writes ic_config.cfg.nif)
+    cmdTrack # `nim track --def/--usages`: IC frontend build + NIF scan for IDE queries
 
 const
   cmdBackends* = {cmdCompileToC, cmdCompileToCpp, cmdCompileToOC,
@@ -288,9 +290,6 @@ type
     procParamTypeBackendAliases
       ## Keep the old proc type compatibility rules that ignore backend
       ## c type aliases.
-    typedescFieldAccess
-      ## Allow typedesc field access on object/tuple types outside of
-      ## typeof context.
     injectedSymbolRedefinition
       ## Allow a template to inject a symbol *definition* that is then emitted
       ## more than once (e.g. a `typed` argument captured by a `{.dirty.}`

compiler/pipelines.nim

@@ -167,7 +167,8 @@ proc processPipelineModule*(graph: ModuleGraph; module: PSym; idgen: IdGenerator
     s = stream
     graph.interactive = stream.kind == llsStdIn
   var topLevelStmts =
-    if optCompress in graph.config.globalOptions or graph.config.cmd == cmdM:
+    if {optCompress, optGenBif} * graph.config.globalOptions != {} or
+        graph.config.cmd == cmdM:
       newNodeI(nkStmtList, module.info)
     else:
       nil
@@ -255,7 +256,7 @@ proc processPipelineModule*(graph: ModuleGraph; module: PSym; idgen: IdGenerator
         graph.config.cmd == cmdM and graph.config.errorCounter == 0 and
           graph.config.m.fileInfos[module.position].dirtyFile.isEmpty
       else:
-        (optCompress in graph.config.globalOptions) or
+        ({optCompress, optGenBif} * graph.config.globalOptions != {}) or
         (graph.config.cmd == cmdM and
          (sfMainModule in module.flags or
           (graph.config.icGroup.len > 0 and
@@ -317,9 +318,12 @@ proc processPipelineModule*(graph: ModuleGraph; module: PSym; idgen: IdGenerator
       # the backend seeds its id minting ABOVE this so closure envs / RTTI hooks
       # never share a `toId` with a frontend sym/type. See ast2nif `(unusedid)`.
       let firstUnusedId = max(idgen.symId, idgen.typeId)
+      var expansions: seq[(PSym, TLineInfo)] = @[]
+      discard graph.nifExpansions.take(module.position.int32, expansions)
       writeNifModule(graph.config, module.position.int32, topLevelStmts, graph.opsLog,
                      replayActions, implDeps, reexportedModuleSyms(graph, module),
-                     genericOffers, typeOffers, resolvedImportDeps, firstUnusedId)
+                     genericOffers, typeOffers, resolvedImportDeps, firstUnusedId,
+                     expansions)
       # The module's REAL direct imports (incl. macro-generated) for `nim ic`'s
       # graph re-derivation; see ast2nif.writeSemDeps / semdata.addImportFileDep.
       var semDepPaths: seq[string] = @[]

compiler/sem.nim

@@ -288,6 +288,14 @@ proc newSymG*(kind: TSymKind, n: PNode, c: PContext): PSym =
         result = copySym(result)
         result.ast = n.sym.ast
         put(c.p, n.sym, result)
+    if result.state == Sealed:
+      # the symbol was loaded from another module's NIF cache (e.g. a param
+      # symbol spliced out of an imported proc type by a `typed` macro) and is
+      # therefore immutable; the caller re-owns it and assigns its type/flags,
+      # so hand back a fresh, mutable copy owned by the current module instead.
+      let fresh = copySym(result, c.idgen)
+      fresh.ast = result.ast
+      result = fresh
     # when there is a nested proc inside a template, semtmpl
     # will assign a wrong owner during the first pass over the
     # template; we must fix it here: see #909
@@ -576,10 +584,12 @@ const
 
 proc semMacroExpr(c: PContext, n, nOrig: PNode, sym: PSym,
                   flags: TExprFlags = {}; expectedType: PType = nil): PNode =
-  rememberExpansion(c, nOrig.info, sym)
+  let info = getCallLineInfo(n)
+  # the callee identifier's position is the usage site tooling expects (matches
+  # `markUsed` below), not the whole-call `nOrig.info`.
+  rememberExpansion(c, info, sym)
   pushInfoContext(c.config, nOrig.info, sym.detailedInfo)
 
-  let info = getCallLineInfo(n)
   markUsed(c, info, sym)
   onUse(info, sym)
   if sym == c.p.owner:

compiler/semdata.nim

@@ -382,8 +382,9 @@ proc addImportFileDep*(c: PContext; f: FileIndex) =
     if f notin deps[]: deps[].add f
 
 proc addPragmaComputation*(c: PContext; n: PNode) =
-  # Also store for NIF-based IC (cmdM mode or optCompress)
-  if optCompress in c.config.globalOptions or c.config.cmd == cmdM:
+  # Also store whenever the semchecked module is serialized to NIF/BIF.
+  if {optCompress, optGenBif} * c.config.globalOptions != {} or
+      c.config.cmd == cmdM:
     addNifReplayAction(c.graph, c.module.position.int32, n)
 
 proc inclSym(sq: var seq[PSym], s: PSym): bool =
@@ -668,7 +669,15 @@ proc rememberExpansion*(c: PContext; info: TLineInfo; expandedSym: PSym) =
   ## ("find all usages of this template" would not work). We need special
   ## logic to remember macro/template expansions. This is done here and
   ## delegated to the "NIF" file mechanism.
-  discard "XXX To implement"
+  ##
+  ## We only bother when a NIF file is actually going to be written (IC / `nim m`,
+  ## `--compress`, semantic BIF output, or a running suggestion engine); a plain
+  ## `nim c` throws the record away, so recording it would be pure overhead.
+  if info.fileIndex == InvalidFileIdx: return
+  if c.config.cmd == cmdM or
+      {optCompress, optGenBif} * c.config.globalOptions != {} or
+      c.config.ideActive:
+    c.graph.nifExpansions.mgetOrPut(c.module.position.int32, @[]).add (expandedSym, info)
 
 const
   errVarForOutParamNeededX = "for a 'var' type a variable needs to be passed; but '$1' is immutable"

compiler/semexprs.nim

@@ -26,13 +26,15 @@ const
 
 proc semTemplateExpr(c: PContext, n: PNode, s: PSym,
                      flags: TExprFlags = {}; expectedType: PType = nil): PNode =
-  rememberExpansion(c, n.info, s)
+  let info = getCallLineInfo(n)
+  # `info` (the callee identifier's position, not the whole call node) is what
+  # tooling wants to see as the usage site — matches `markUsed` below.
+  rememberExpansion(c, info, s)
   # IC: this expands `s`'s body into the current module's sem, so the module
   # depends on that body — record a NeedsImpl (strong) edge to `s`'s module.
   # The iface cookie hashes only signatures now, so a template body edit moves
   # only the impl cookie, and just the modules that expanded it re-sem.
   recordIcImplDep(c.graph, s)
-  let info = getCallLineInfo(n)
   markUsed(c, info, s)
   onUse(info, s)
   # Note: This is n.info on purpose. It prevents template from creating an info
@@ -1551,8 +1553,7 @@ proc tryReadingTypeField(c: PContext, n: PNode, i: PIdent, ty: PType): PNode =
       markUsed(c, n.info, f)
       onUse(n.info, f)
   of tyObject, tyTuple:
-    if (c.inTypeofContext > 0 or typedescFieldAccess in c.config.legacyFeatures) and
-        ty.n != nil and ty.n.kind == nkRecList:
+    if ty.n != nil and ty.n.kind == nkRecList:
       let field = lookupInRecord(ty.n, i)
       if field != nil:
         n.typ = makeTypeDesc(c, field.typ)

compiler/semmagic.nim

@@ -693,5 +693,10 @@ proc magicsAfterOverloadResolution(c: PContext, n: PNode,
     if n[1].kind in {nkStmtListExpr, nkBlockExpr,
               nkIfExpr, nkCaseStmt, nkTryStmt}:
       localError(c.config, n.info, "Nested expressions cannot be moved: '" & $n[1] & "'")
+  of mMove:
+    result = n
+    if isCursor(n[1]):
+      localError(c.config, n.info, errFailedMove,
+        "cannot move cursor '" & $n[1] & "'; a cursor does not own its value")
   else:
     result = n

compiler/sempass2.nim

@@ -1649,10 +1649,11 @@ proc track(tracked: PEffects, n: PNode) =
       message(tracked.config, n.info, warnPtrToCstringConv,
           $n[1].typ)
 
-    # Check for implicit range conversions
+    # Check for implicit range conversions. Compile-time constants are already
+    # fully known here, so only non-constant values need the downsizing warning.
     if n.kind == nkHiddenStdConv and (not tracked.isArrayIndexing) and
-          n[1].kind notin {nkCharLit..nkUInt64Lit, nkFloatLit..nkFloat128Lit} and
-          shouldWarnRangeConversion(tracked.config, n.info, n.typ, n[1].typ):
+          shouldWarnRangeConversion(tracked.config, n.info, n.typ, n[1].typ) and
+          getConstExpr(tracked.ownerModule, n[1], tracked.c.idgen, tracked.graph) == nil:
       message(tracked.config, n.info, warnImplicitRangeConversion,
               typeToString(n[1].typ) & " -> " & typeToString(n.typ))
 
@@ -1783,13 +1784,18 @@ proc setEffectsForProcType*(g: ModuleGraph; t: PType, n: PNode; s: PSym = nil) =
     elif s != nil and (s.magic != mNone or {sfImportc, sfExportc} * s.flags == {sfImportc}):
       effects[exceptionEffects] = newNodeI(nkArgList, effects.info)
 
+    let forbidsSpec = effectSpec(n, wForbids)
     let tagsSpec = effectSpec(n, wTags)
     if not isNil(tagsSpec):
       effects[tagEffects] = tagsSpec
+    elif not isNil(forbidsSpec):
+      # `.forbids` without `.tags` still declares a known empty tag set.
+      # Leaving this as nil would mean "unknown tags", which later widens
+      # indirect calls to `RootEffect`.
+      effects[tagEffects] = newNodeI(nkArgList, effects.info)
     elif s != nil and (s.magic != mNone or {sfImportc, sfExportc} * s.flags == {sfImportc}):
       effects[tagEffects] = newNodeI(nkArgList, effects.info)
 
-    let forbidsSpec = effectSpec(n, wForbids)
     if not isNil(forbidsSpec):
       effects[forbiddenEffects] = forbidsSpec
     elif s != nil and (s.magic != mNone or {sfImportc, sfExportc} * s.flags == {sfImportc}):

compiler/semstmts.nim

@@ -2892,7 +2892,8 @@ proc incMod(c: PContext, n: PNode, it: PNode, includeStmtResult, resolvedIncStmt
 proc evalInclude(c: PContext, n: PNode): PNode =
   result = newNodeI(nkStmtList, n.info)
   var resolvedIncStmt: PNode = nil
-  if optCompress in c.config.globalOptions or c.config.cmd == cmdM:
+  if {optCompress, optGenBif} * c.config.globalOptions != {} or
+      c.config.cmd == cmdM:
     # New resolve the include filenames to string literals that contain absolute paths,
     # nicer for IC:
     resolvedIncStmt = newNodeI(nkIncludeStmt, n.info)

compiler/semtypes.nim

@@ -219,9 +219,10 @@ proc semSet(c: PContext, n: PNode, prev: PType): PType =
   result = newOrPrevType(tySet, prev, c)
   if n.len == 2 and n[1].kind != nkEmpty:
     var base = semTypeNode(c, n[1], nil)
+    if base.kind == tyTypeDesc: base = base.base  # unwrap from type traits like distinctBase
     addSonSkipIntLit(result, base, c.idgen)
     if base.kind in {tyGenericInst, tyAlias, tySink}: base = skipModifier(base)
-    if base.kind notin {tyGenericParam, tyGenericInvocation}:
+    if base.kind notin {tyGenericParam, tyGenericInvocation, tyFromExpr}:
       if base.kind == tyForward:
         c.forwardTypeUpdates.add (getCurrOwner(c), result, n)
       elif not isOrdinalType(base, allowEnumWithHoles = true):

compiler/semtypinst.nim

@@ -12,7 +12,7 @@
 import std / tables
 
 import ast, astalgo, msgs, types, magicsys, semdata, renderer, options,
-  lineinfos, modulegraphs, layeredtable
+  lineinfos, modulegraphs, layeredtable, typeallowed
 
 when defined(nimPreviewSlimSystem):
   import std/assertions
@@ -296,6 +296,19 @@ proc replaceTypeVarsN(cl: var TReplTypeVars, n: PNode; start=0; expectedType: PT
         replaceTypeVarsS(cl, n.sym, replaceTypeVarsT(cl, n.sym.typ))
     if result.sym.kind == skField and
         (cl.owner == nil or result.sym.owner == cl.owner):
+      let invalidType =
+        if not cl.allowMetaTypes and result.typ != nil and result.typ.isMetaType and
+            result.sym.owner != nil and result.sym.owner.kind == skType:
+          typeAllowed(result.typ, skVar, cl.c, {taProcContextIsNotMacro})
+        else:
+          nil
+      # Constrained types can remain unresolved during overload matching. Only
+      # reject the type-valued storage that can reach code generation (#24848).
+      if invalidType != nil and invalidType.kind == tyTypeDesc:
+        localError(cl.c.config, result.info,
+          "'" & invalidType.typeToString & "' is not a concrete type")
+        result.typ = errorType(cl.c)
+        result.sym.typ = result.typ
       if result.sym.ast != nil:
         # instantiate default value of object/tuple field
         var n = result.sym.ast

compiler/sighashes.nim

@@ -274,6 +274,7 @@ proc hashType(c: var MD5Context, t: PType; flags: set[ConsiderFlag]; conf: Confi
     c.hashTree(t.n, {}, conf)
   of tyTuple:
     c &= char(t.kind)
+    c &= t.len
     if t.n != nil and CoType notin flags:
       for i in 0..<t.n.len:
         assert(t.n[i].kind == nkSym)

compiler/trees.nim

@@ -225,6 +225,17 @@ proc getRoot*(n: PNode): PSym =
     else: result = nil
   else: result = nil
 
+proc isCursor*(n: PNode): bool =
+  case n.kind
+  of nkSym:
+    sfCursor in n.sym.flags
+  of nkDotExpr:
+    isCursor(n[1])
+  of nkCheckedFieldExpr:
+    isCursor(n[0])
+  else:
+    false
+
 proc stupidStmtListExpr*(n: PNode): bool =
   for i in 0..<n.len-1:
     if n[i].kind notin {nkEmpty, nkCommentStmt}: return false

compiler/vmgen.nim

@@ -851,14 +851,26 @@ proc genBinaryStmt(c: PCtx; n: PNode; opc: TOpcode) =
   c.freeTemp(tmp)
   c.freeTemp(dest)
 
+proc genMutatingValue(c: PCtx; n: PNode): TRegister =
+  ## Loads the value of an in-place mutation target while keeping it attached to
+  ## its original storage. Compound lvalues must be resolved through their
+  ## address: a normal value load can return a detached copy (for example, when
+  ## indexing a broadcast default array).
+  if needsAsgnPatch(n):
+    let address = c.genx(n, {gfNodeAddr})
+    result = c.getTemp(n.typ)
+    c.gABC(n, opcLdDeref, result, address)
+    c.freeTemp(address)
+  else:
+    result = c.genx(n)
+
 proc genBinaryStmtVar(c: PCtx; n: PNode; opc: TOpcode) =
   var x = n[1]
   if x.kind in {nkAddr, nkHiddenAddr}: x = x[0]
   let
-    dest = c.genx(x)
+    dest = c.genMutatingValue(x)
     tmp = c.genx(n[2])
   c.gABC(n, opc, dest, tmp, 0)
-  #c.genAsgnPatch(n[1], dest)
   c.freeTemp(tmp)
   c.freeTemp(dest)
 
@@ -1162,7 +1174,7 @@ proc genMagic(c: PCtx; n: PNode; dest: var TDest; flags: TGenFlags = {}, m: TMag
 
   of mIncl, mExcl:
     unused(c, n, dest)
-    var d = c.genx(n[1])
+    var d = c.genMutatingValue(n[1])
     var tmp = c.genx(n[2])
     c.genSetType(n[1], d)
     c.gABC(n, if m == mIncl: opcIncl else: opcExcl, d, tmp)

doc/advopt.txt

@@ -21,6 +21,7 @@ Advanced commands:
                             see also: --dump.format:json (useful with: `| jq`)
   //check                   checks the project for syntax and semantics
                             (can be combined with --defusages)
+  //track                   goto-definition / find-usages via `nim ic`
 
 Runtime checks (see -x):
   --objChecks:on|off        turn obj conversion checks on|off
@@ -33,6 +34,8 @@ Runtime checks (see -x):
   --infChecks:on|off        turn Inf checks on|off
 
 Advanced options:
+  --def:FILE,LINE,COL       find the definition of the symbol at the position
+  --usages:FILE,LINE,COL    find all usages of the symbol at the position
   --defusages:FILE,LINE,COL
                             find the definition and all usages of a symbol
   -o:FILE, --out:FILE       set the output filename
@@ -119,6 +122,7 @@ Advanced options:
   --lineDir:on|off          generation of #line directive on|off
   --embedsrc:on|off         embeds the original source code as comments
                             in the generated output
+  --genBif:on|off           generate per-module semantic BIF metadata in nimcache
   --tlsEmulation:on|off     turn thread local storage emulation on|off
   --implicitStatic:on|off   turn implicit compile time evaluation on|off
   --trmacros:on|off         turn term rewriting macros on|off

doc/ic.md

@@ -39,6 +39,16 @@ debugging a build).
 Artifacts (the NIF zoo)
 =======================
 
+Semantic BIF from regular builds
+--------------------------------
+
+``--genBif:on`` makes a regular compiler invocation write each semantically
+checked module as ``<suffix>.s.bif`` under the build's nimcache directory. This
+reuses the semantic artifact format used by IC without enabling incremental
+compilation or changing how the program is generated and linked. Tools such as
+language servers, debuggers, and binding generators can request these artifacts
+when they need resolved symbols and types from an ordinary build.
+
 Per module ``<suffix>`` (a content hash of the path; see *NIF symbols* below),
 under the nimcache directory:
 

doc/mm.md

@@ -50,9 +50,23 @@ cycle collector's overhead
 but `--mm:orc` also produces more machine code than `--mm:arc`, so if you're on a target
 where code size matters and you know that your code does not produce cycles, you can
 use `--mm:arc`. Notice that the default `async`:idx: implementation produces cycles
-and leaks memory with `--mm:arc`, in other words, for `async` you need to use `--mm:orc`.
+and leaks memory with `--mm:arc`, in other words, for `async` you need to use `--mm:orc`
+or `--mm:yrc`.
 
 
+Atomic ARC/YRC
+--------------
+
+ARC/ORC are not threadsafe if `ref` or other automatically managed types are
+accessed across thread boundaries.
+Moving isolated subgraphs between threads is supported for ARC/ORC and the language has support
+for that in the form of `isolate`. The modes `mm:atomicArc` and `mm:yrc` do offer this thread safety -- at the cost of atomic instructions. Whether that cost is acceptable depends on your program, it hard to give general guidelines. On a modern CPU the potential speedups in the form of increased multi-threading capabilities should outweigh the costs of atomic instructions by far. On an embedded device the atomics would probably only hurt though.
+
+`mm:atomicArc` is a threadsafe variant of ARC: All the optimizations in the form of move semantics etc are still applied. `mm:yrc` is the threadsafe variant of ORC.
+
+YRC is a novel concurrent cycle collection algorithm -- these are beasts to verify
+and to get correct so there are dragons lurking here, use at your own risk.
+
 
 Other MM modes
 --------------
@@ -66,7 +80,7 @@ Other MM modes
   Heaps are thread-local.
 --mm:boehm    Boehm based garbage collector, it offers a shared heap.
 --mm:go    Go's garbage collector, useful for interoperability with Go.
-  Offers a shared heap.
+  Offers a shared heap. Note that `mm:go` has seen little real world use. Use at your own risk.
 
 --mm:none    No memory management strategy nor a garbage collector. Allocated memory is
   simply never freed. You should use `--mm:arc` instead.
@@ -76,6 +90,7 @@ Here is a comparison of the different memory management modes:
 ================== ======== ================= ============== ====== =================== ===================
 Memory Management  Heap     Reference Cycles  Stop-The-World Atomic Valgrind compatible Command line switch
 ================== ======== ================= ============== ====== =================== ===================
+YRC                Shared   Cycle Collector   No             Yes    Yes                 `--mm:yrc`
 ORC                Shared   Cycle Collector   No             No     Yes                 `--mm:orc`
 ARC                Shared   Leak              No             No     Yes                 `--mm:arc`
 Atomic ARC         Shared   Leak              No             Yes    Yes                 `--mm:atomicArc`

koch.nim

@@ -11,16 +11,16 @@
 
 const
   # examples of possible values for repos: Head, ea82b54
-  NimbleStableCommit = "42ef70c2102a942c46f13eb76872326edd525cec"    # 0.22.3
+  NimbleStableCommit = "a399f502dec7ffcd905c1cf54b13274ad990bada"    # 0.24.1
   AtlasStableCommit = "aa6fb162006f3015aa84c4305e15cb4d230f5ad6"     # 0.14.7
   ChecksumsStableCommit = "5c132cd332cce5d64a0da9ac3e4c9664313dccb4" # 0.2.2
   SatStableCommit = "9d52513b3c68bfb929dbd687d4fb2836cfee6936"
 
-  NimonyStableCommit = "6f9ac6655dc6724ae4e5ccb93b8123c18d54391a" # unversioned \
+  NimonyStableCommit = "f831b953d7c21d9a4b11d0042039e7f84d7c8dc9" # unversioned \
     # Note that Nimony uses Nim as a git submodule but we don't want to install
     # Nimony's dependency to Nim as we are Nim. So a `git clone` without --recursive
     # is **required** here.
-    # Commit from 2026-07-03 -- .bif files are memory mapped too
+    # Commit from 2026-07-10 -- stable .bif file format
 
   # examples of possible values for fusion: #head, #ea82b54, 1.2.3
   FusionStableHash = "#562467452b32cb7a97410ea177f083e6d8405734"
@@ -619,7 +619,7 @@ proc runIcTestFile(inp: string) =
 const icSuite = ["thallo", "tconverter", "timp", "tmiscs", "tparseutils",
                  "tcompiletimeglobal", "tsighashstable", "tpureenum", "tgenericoffer",
                  "tconverterreexport", "ttypeoffer", "ttransitiveoffer",
-                 "tmodsymref", "tmethupref", "temit"]
+                 "tmodsymref", "tmethupref", "temit", "ttraitparam"]
 
 proc icTest(args: string) =
   temp("")

lib/pure/asyncdispatch.nim

@@ -269,6 +269,23 @@ proc processPendingCallbacks(p: PDispatcherBase; didSomeWork: var bool) =
     cb()
     didSomeWork = true
 
+proc processTimersBeforePoll(
+  p: PDispatcherBase, didSomeWork: var bool
+): Option[int] {.inline.} =
+  # Do not let an expired timeout overtake completion callbacks which are
+  # already pending. `adjustTimeout` makes the I/O poll non-blocking when the
+  # callback queue is non-empty.
+  if p.callbacks.len == 0:
+    result = processTimers(p, didSomeWork)
+
+proc processCallbacksAndTimers(p: PDispatcherBase; didSomeWork: var bool) =
+  # A completed operation can take multiple queued callbacks to propagate
+  # through its public future. Process the whole chain before expired timers.
+  processPendingCallbacks(p, didSomeWork)
+  discard processTimers(p, didSomeWork)
+  # Timer futures must still propagate within this dispatcher iteration.
+  processPendingCallbacks(p, didSomeWork)
+
 proc adjustTimeout(
   p: PDispatcherBase, pollTimeout: int, nextTimer: Option[int]
 ): int {.inline.} =
@@ -399,7 +416,7 @@ when defined(windows) or defined(nimdoc):
         "No handles or timers registered in dispatcher.")
 
     result = false
-    let nextTimer = processTimers(p, result)
+    let nextTimer = processTimersBeforePoll(p, result)
     let at = adjustTimeout(p, timeout, nextTimer)
     var llTimeout =
       if at == -1: winlean.INFINITE
@@ -450,10 +467,7 @@ when defined(windows) or defined(nimdoc):
           result = false
         else: raiseOSError(errCode)
 
-    # Timer processing.
-    discard processTimers(p, result)
-    # Callback queue processing
-    processPendingCallbacks(p, result)
+    processCallbacksAndTimers(p, result)
 
 
   var acceptEx: WSAPROC_ACCEPTEX
@@ -1404,7 +1418,7 @@ else:
 
     result = false
     var keys: array[64, ReadyKey]
-    let nextTimer = processTimers(p, result)
+    let nextTimer = processTimersBeforePoll(p, result)
     var count =
       p.selector.selectInto(adjustTimeout(p, timeout, nextTimer), keys)
     for i in 0..<count:
@@ -1447,10 +1461,7 @@ else:
         if writeCbListCount > 0: incl(newEvents, Event.Write)
         p.selector.updateHandle(SocketHandle(fd), newEvents)
 
-    # Timer processing.
-    discard processTimers(p, result)
-    # Callback queue processing
-    processPendingCallbacks(p, result)
+    processCallbacksAndTimers(p, result)
 
   proc recv*(socket: AsyncFD, size: int,
              flags = {SocketFlag.SafeDisconn}): owned(Future[string]) =

lib/pure/nimprof.nim

@@ -186,7 +186,7 @@ proc writeProfile() {.noconv.} =
     var perProc = initCountTable[string]()
     for i in 0..entries-1:
       var dups = initHashSet[string]()
-      for ii in 0..high(typeof(StackTrace.lines)):
+      for ii in 0..high(StackTrace.lines):
         let procname = profileData[i].st[ii]
         if isNil(procname): break
         let p = $procname
@@ -201,7 +201,7 @@ proc writeProfile() {.noconv.} =
         writeLine(f, "Entry: ", i+1, "/", entries, " Calls: ",
           profileData[i].total // totalCalls, " [sum: ", sum, "; ",
           sum // totalCalls, "]")
-        for ii in 0..high(typeof(StackTrace.lines)):
+        for ii in 0..high(StackTrace.lines):
           let procname = profileData[i].st[ii]
           let filename = profileData[i].st.files[ii]
           if isNil(procname): break

lib/pure/xmltree.nim

@@ -913,17 +913,14 @@ proc findAll*(n: XmlNode, tag: string, caseInsensitive = false): seq[XmlNode] =
 
 proc xmlConstructor(a: NimNode): NimNode =
   if a.kind == nnkCall:
-    result = newCall("newXmlTree", toStrLit(a[0]))
+    result = newCall("newXmlTree", newStrLitNode($a[0]))
     var attrs = newNimNode(nnkBracket, a)
     var newStringTabCall = newCall(bindSym"newStringTable", attrs,
                                     bindSym"modeCaseSensitive")
     var elements = newNimNode(nnkBracket, a)
     for i in 1..a.len-1:
       if a[i].kind == nnkExprEqExpr:
-        # In order to support attributes like `data-lang` we have to
-        # replace whitespace because `toStrLit` gives `data - lang`.
-        let attrName = toStrLit(a[i][0]).strVal.replace(" ", "")
-        attrs.add(newStrLitNode(attrName))
+        attrs.add(newStrLitNode($a[i][0]))
         attrs.add(a[i][1])
         #echo repr(attrs)
       else:

lib/system/alloc.nim

@@ -804,6 +804,24 @@ when defined(gcDestructors):
     sysAssert c.next == nil, "c.next pointer must be nil"
     atomicPrepend a.sharedFreeListBigChunks, c
 
+  proc takeFromSharedFreeListBigChunks(a: var MemRegion): PBigChunk {.inline.} =
+    when hasThreadSupport:
+      while true:
+        result = atomicLoadN(addr a.sharedFreeListBigChunks, ATOMIC_ACQUIRE)
+        if result == nil:
+          break
+        let next = result.next.loada
+        var expected = result
+        if atomicCompareExchangeN(addr a.sharedFreeListBigChunks, addr expected, next,
+                                  weak = true, ATOMIC_ACQUIRE, ATOMIC_RELAXED):
+          result.next.storea nil
+          break
+    else:
+      result = a.sharedFreeListBigChunks
+      if result != nil:
+        a.sharedFreeListBigChunks = result.next
+        result.next = nil
+
   proc addToSharedFreeList(c: PSmallChunk; f: ptr FreeCell; size: int) {.inline.} =
     atomicPrepend c.owner.sharedFreeLists[size], f
 
@@ -827,21 +845,14 @@ when defined(gcDestructors):
     inc(c.free, total)
     dec(a.occ, total)
 
-  proc freeDeferredObjects(a: var MemRegion; root: PBigChunk) =
-    var it = root
-    var maxIters = MaxSteps # make it time-bounded
-    while true:
-      let rest = it.next.loada
-      it.next.storea nil
-      deallocBigChunk(a, cast[PBigChunk](it))
-      if maxIters == 0:
-        if rest != nil:
-          addToSharedFreeListBigChunks(a, rest)
-          sysAssert a.sharedFreeListBigChunks != nil, "re-enqueing failed"
-        break
-      it = rest
-      dec maxIters
+  proc freeDeferredObjects(a: var MemRegion) =
+    # Pop only as many nodes as we can process. Detaching the entire list and
+    # re-enqueuing its unprocessed tail through atomicPrepend would overwrite
+    # that tail's next pointer and lose the rest of the list.
+    for _ in 0..MaxSteps:
+      let it = takeFromSharedFreeListBigChunks(a)
       if it == nil: break
+      deallocBigChunk(a, it)
 
 when defined(heaptrack):
   const heaptrackLib =
@@ -969,13 +980,7 @@ proc rawAlloc(a: var MemRegion, requestedSize: int, alignment: int = 0): pointer
     trackSize(c.size)
   else:
     when defined(gcDestructors):
-      when hasThreadSupport:
-        let deferredFrees = atomicExchangeN(addr a.sharedFreeListBigChunks, nil, ATOMIC_RELAXED)
-      else:
-        let deferredFrees = a.sharedFreeListBigChunks
-        a.sharedFreeListBigChunks = nil
-      if deferredFrees != nil:
-        freeDeferredObjects(a, deferredFrees)
+      freeDeferredObjects(a)
 
     # For big chunks with custom alignment, allocate extra space.
     # Since chunks are page-aligned, the needed padding is a compile-time
@@ -1397,4 +1402,4 @@ template instantiateForRegion(allocator: untyped) {.dirty.} =
         #sharedMemStatsShared(sharedHeap.currMem - sharedHeap.freeMem)
   {.pop.}
 
-{.pop.}
+{.pop.}

lib/system/arc.nim

@@ -36,7 +36,12 @@ type
     rc: int # the object header is now a single RC field.
             # we could remove it in non-debug builds for the 'owned ref'
             # design but this seems unwise.
-    when defined(gcOrc) or defined(gcYrc):
+    when defined(gcYrc):
+      rootIdx: int64 # the collector's claim word: collection tag or epoch
+                     # stamp packed with the dense capture index. Explicitly
+                     # 64 bit so that 32-bit targets run the same concurrent
+                     # claim and epoch-stamp algorithms
+    elif defined(gcOrc):
       rootIdx: int # thanks to this we can delete potential cycle roots
                    # in O(1) without doubly linked lists
     when defined(nimArcDebug) or defined(nimArcIds):

lib/system/excpt.nim

@@ -207,10 +207,10 @@ when defined(nativeStacktrace) and nativeStackTraceSupported:
       if enabled:
         if dlresult != 0:
           var oldLen = s.len
-          add(s, tempDlInfo.dli_fname)
+          add(s, cstrToStrBuiltin(tempDlInfo.dli_fname))
           if tempDlInfo.dli_sname != nil:
             for k in 1..max(1, 25-(s.len-oldLen)): add(s, ' ')
-            add(s, tempDlInfo.dli_sname)
+            add(s, cstrToStrBuiltin(tempDlInfo.dli_sname))
         else:
           add(s, '?')
         add(s, "\n")

lib/system/gc.nim

@@ -892,9 +892,6 @@ when not defined(useNimRtl):
             "API usage error: GC_enable called but GC is already enabled")
     dec(gch.recGcLock)
 
-  proc GC_setStrategy(strategy: GC_Strategy) =
-    discard
-
   proc GC_enableMarkAndSweep() =
     gch.cycleThreshold = InitialCycleThreshold
 

lib/system/gc_interface.nim

@@ -3,14 +3,6 @@
 when not usesDestructors:
   {.pragma: nodestroy.}
 
-when hasAlloc:
-  type
-    GC_Strategy* = enum  ## The strategy the GC should use for the application.
-      gcThroughput,      ## optimize for throughput
-      gcResponsiveness,  ## optimize for responsiveness (default)
-      gcOptimizeTime,    ## optimize for speed
-      gcOptimizeSpace    ## optimize for memory footprint
-
 when hasAlloc and not defined(js) and not usesDestructors:
   proc GC_disable*() {.rtl, inl, gcsafe, raises: [].}
     ## Disables the GC. If called `n` times, `n` calls to `GC_enable`
@@ -66,9 +58,6 @@ when hasAlloc and defined(js):
   template GC_fullCollect* =
     {.warning: "GC_fullCollect is a no-op in JavaScript".}
 
-  template GC_setStrategy* =
-    {.warning: "GC_setStrategy is a no-op in JavaScript".}
-
   template GC_enableMarkAndSweep* =
     {.warning: "GC_enableMarkAndSweep is a no-op in JavaScript".}
 

lib/system/gc_ms.nim

@@ -491,8 +491,6 @@ when not defined(useNimRtl):
             "API usage error: GC_enable called but GC is already enabled")
     dec(gch.recGcLock)
 
-  proc GC_setStrategy(strategy: GC_Strategy) = discard
-
   proc GC_enableMarkAndSweep() =
     gch.cycleThreshold = InitialThreshold
 

lib/system/gc_regions.nim

@@ -415,7 +415,6 @@ when hasThreadSupport:
 proc GC_disable() = discard
 proc GC_enable() = discard
 proc GC_fullCollect() = discard
-proc GC_setStrategy(strategy: GC_Strategy) = discard
 proc GC_enableMarkAndSweep() = discard
 proc GC_disableMarkAndSweep() = discard
 proc GC_getStatistics(): string = return ""

lib/system/mm/boehm.nim

@@ -76,7 +76,6 @@ when not defined(useNimRtl):
   proc GC_disable() = boehmGC_disable()
   proc GC_enable() = boehmGC_enable()
   proc GC_fullCollect() = boehmGCfullCollect()
-  proc GC_setStrategy(strategy: GC_Strategy) = discard
   proc GC_enableMarkAndSweep() = discard
   proc GC_disableMarkAndSweep() = discard
   proc GC_getStatistics(): string = return ""

lib/system/mm/go.nim

@@ -12,7 +12,6 @@ proc GC_disable() = discard
 proc GC_enable() = discard
 proc go_gc() {.importc: "go_gc", dynlib: goLib.}
 proc GC_fullCollect() = go_gc()
-proc GC_setStrategy(strategy: GC_Strategy) = discard
 proc GC_enableMarkAndSweep() = discard
 proc GC_disableMarkAndSweep() = discard
 

lib/system/mm/malloc.nim

@@ -55,8 +55,6 @@ when not defined(gcOrc) and not defined(gcYrc):
   proc GC_enableMarkAndSweep() = discard
   proc GC_disableMarkAndSweep() = discard
 
-proc GC_setStrategy(strategy: GC_Strategy) = discard
-
 proc getOccupiedMem(): int = discard
 proc getFreeMem(): int = discard
 proc getTotalMem(): int = discard

lib/system/mm/none.nim

@@ -8,7 +8,6 @@ proc initGC() = discard
 proc GC_disable() = discard
 proc GC_enable() = discard
 proc GC_fullCollect() = discard
-proc GC_setStrategy(strategy: GC_Strategy) = discard
 proc GC_enableMarkAndSweep() = discard
 proc GC_disableMarkAndSweep() = discard
 proc GC_getStatistics(): string = return ""

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) =

lib/system/strs_v3.nim

@@ -514,10 +514,25 @@ proc setLengthStr(s: var SmallString; newLen: int; zeroing: bool) =
         s.more.fullLen = newLen
         s.more.data[newLen] = '\0'
       else:
-        # shared or static block: detach and go back to inline
+        # shared or static block: detach from the shared/static buffer.
         if newLen <= 0:
           nimDestroyStrV1(s)
           s.bytes = 0
+        elif newLen > PayloadSize:
+          # Still too long for inline: detach into a fresh unique heap block
+          # rather than overflowing the inline overlay.
+          let old = s.more
+          let p = cast[ptr LongString](alloc(LongStringDataOffset + newLen + 1))
+          p.rc = 1
+          p.fullLen = newLen
+          p.capImpl = newLen
+          copyMem(addr p.data[0], addr old.data[0], newLen)
+          p.data[newLen] = '\0'
+          if slen == HeapSlen and atomicSubFetch(old.rc, 1) == 0:
+            dealloc(old)
+          s.more = p
+          setSSLen(s, HeapSlen)
+          copyMem(inlinePtr(s), addr p.data[0], AlwaysAvail)  # sync hot prefix
         else:
           let old = s.more
           let inl = inlinePtr(s)

lib/system/sysstr.nim

@@ -223,8 +223,9 @@ proc addChar(s: NimString, c: char): NimString =
 proc appendString(dest, src: NimString) {.compilerproc, inline.} =
   ## Raw, does not prepare `dest` space for copying
   if src != nil:
-    copyMem(addr(dest.data[dest.len]), addr(src.data), src.len + 1)
+    copyMem(addr(dest.data[dest.len]), addr(src.data), src.len)
     inc(dest.len, src.len)
+    dest.data[dest.len] = '\0'
 
 proc setLengthStr(s: NimString, newLen: int): NimString {.compilerRtl.} =
   ## Sets the `s` length to `newLen` zeroing memory on growth.

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

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,618 @@ 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  when a collection prunes ANY out-edge, it keeps one member of
+        EVERY surviving SCC registered — not just the SCCs that pruned an
+        edge themselves. This is broader than it first looks and the
+        breadth is load-bearing: a pruned cell is not traced, yet its
+        out-edges still count toward its targets' rc, so a pruned cell
+        that is ITSELF dead (promoted while live, died later this epoch)
+        contributes phantom refs that inflate an UNRELATED SCC's external
+        count and misclassify that genuinely-dead SCC as a plain (non-
+        prune-source) survivor. Registering only prune-source SCCs
+        (the original hook) let such a survivor be re-stamped, dropped
+        from the retry set, and orphaned permanently once its last
+        prune-source neighbour resolved — a real leak the dumpster `fuzz`
+        port surfaced (tests/yrc/tyrc_fuzz_graph.nim: ~1% of allocations
+        lost, ORC-clean, un-recoverable even by repeated GC_fullCollect).
+        Registering every survivor of a pruning collection closes it; the
+        cost is bounded because pruning keeps the captured set small, so
+        "every survivor" is only the handful actually traced;
+    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 (and E2's original narrow form was empirically wrong —
+  see above; the broadened form is validated by the fuzz port across seeds
+  and sizes, not machine-checked). The epoch clock counts collections
+  (YrcEpochLen=64);
+  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 — but 64 sits clear of that. A
+  work-based clock (advance per N cells traced) was measured and lost on
+  long-lived structures: pruning shrinks trace work, so the clock stalls
+  exactly when a stale web should be re-examined, trading float for a
+  resonance the default length already avoids.
 
   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.
 -/

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

nimsuggest/nimsuggest.nim

@@ -1156,13 +1156,14 @@ proc executeNoHooksV3(cmd: IdeCmd, file: AbsoluteFile, dirtyfile: AbsoluteFile,
       graph.suggestResult(s.sym, s.sym.info)
   of ideType:
     let s = graph.findSymData(file, line, col)
-    if not s.isNil:
+    if not s.isNil and s.sym.typ != nil:
       let typeSym = s.sym.typ.sym
       if typeSym != nil:
         graph.suggestResult(typeSym, typeSym.info, ideType)
-      elif s.sym.typ.len != 0:
+      elif s.sym.typ.len != 0 and s.sym.typ[0] != nil:
         let genericType = s.sym.typ[0].sym
-        graph.suggestResult(genericType, genericType.info, ideType)
+        if genericType != nil:
+          graph.suggestResult(genericType, genericType.info, ideType)
   of ideUse, ideDus:
     let symbol = graph.findSymData(file, line, col)
     if not symbol.isNil:

nimsuggest/tests/tv3_typeDefinition.nim

@@ -20,6 +20,13 @@ echo fo#[!]#oGeneric.bar
 # bad type
 echo unde#[!]#fined
 
+# type of a void proc: typ[0] (return type) is nil, must not crash
+var s = ""
+s.a#[!]#dd('x')
+
+# type of a module symbol: typ is nil, must not crash
+import std/str#[!]#utils
+
 discard """
 $nimsuggest --v3 --tester $file
 >type $1
@@ -29,4 +36,6 @@ type	skType	tv3_typeDefinition.Foo2	Foo2	$file	11	2	""	100
 >type $3
 type	skType	tv3_typeDefinition.FooGeneric	FooGeneric	$file	14	2	""	100
 >type $4
+>type $5
+>type $6
 """

testament/categories.nim

@@ -190,8 +190,10 @@ proc ioTests(r: var TResults, cat: Category, options: string) =
 
 # ------------------------- async tests ---------------------------------------
 proc asyncTests(r: var TResults, cat: Category, options: string) =
+  # Run async with yrc instead of the default orc; the CI already runs long
+  # enough that we cannot afford to test both.
   template test(filename: untyped) =
-    testSpec r, makeTest(filename, options, cat)
+    testSpec r, makeTest(filename, options & " --mm:yrc", cat)
   for t in os.walkFiles("tests/async/t*.nim"):
     test(t)
 
@@ -528,6 +530,7 @@ proc mmRaise(kind: TResultEnum, expected, given: string) =
   raise e
 
 proc isMetamorphicIcTest(content: string): bool =
+  result = false
   for line in content.splitLines:
     if line.strip == "#? metamorphic": return true
 
@@ -559,7 +562,7 @@ proc stableBinary(path: string): string =
   ## so two builds seconds apart differ there even with identical codegen. Skipping
   ## a generous fixed window keeps the clean-vs-incremental check about codegen.
   const headerSkip = 4096
-  var f: File
+  var f: File = nil
   if not open(f, path, fmRead):
     raise newException(IOError, "cannot open: " & path)
   defer: close(f)

tests/arc/t26010.nim

@@ -0,0 +1,23 @@
+discard """
+  action: reject
+  matrix: "--mm:orc; --mm:refc"
+  errormsg: "cannot move cursor 'a'; a cursor does not own its value"
+"""
+
+# bug #26010: a cursor is a non-owning alias and cannot transfer ownership.
+
+type Xxx = object
+
+proc `=destroy`(v: var Xxx) =
+  debugEcho "dest"
+
+proc test(v: ref Xxx) =
+  var a {.cursor.} = v
+  var b = move(a)
+  discard
+
+proc main() =
+  var x = new Xxx
+  test(x)
+
+main()

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

tests/async/t23615.nim

@@ -0,0 +1,52 @@
+discard """
+  valgrind: true
+  cmd: '''nim c --mm:orc -d:nimAllocStats -d:useMalloc $file'''
+  output: '''ok'''
+"""
+
+# bug #23615: exceptions caught by a typed except branch in a closure
+# iterator (and thus in any async proc) leaked under ARC/ORC.
+
+import std/[asyncdispatch, importutils]
+
+privateAccess(AllocStats)
+
+block: # pure closure iterator, the minimal form of the bug
+  proc runIter() =
+    iterator it(): int {.closure.} =
+      try:
+        yield 1
+        raise newException(ValueError, "x")
+      except ValueError:
+        discard
+      yield 2
+    var f = it
+    doAssert f() == 1
+    doAssert f() == 2
+  let base = getAllocStats()
+  runIter()
+  GC_fullCollect()
+  let after = getAllocStats()
+  doAssert after.allocCount - after.deallocCount ==
+           base.allocCount - base.deallocCount, $base & " " & $after
+
+block: # the async incarnation from the issue
+  proc err {.async.} =
+    raise newException(ValueError, "err1")
+
+  proc amain {.async.} =
+    await sleepAsync(1)
+    for _ in 0..<50:
+      try:
+        await err()
+      except ValueError:
+        discard
+
+  waitFor amain()
+  doAssert not hasPendingOperations()
+  setGlobalDispatcher(nil)
+  GC_fullCollect()
+
+let stats = getAllocStats()
+doAssert stats.allocCount - stats.deallocCount < 10, $stats
+echo "ok"

tests/async/tasyncclosestall.nim

@@ -4,6 +4,7 @@ discard """
   exitcode: 0
 """
 import asyncdispatch, asyncnet
+import std/strutils
 
 when defined(windows):
   from winlean import ERROR_NETNAME_DELETED
@@ -14,6 +15,7 @@ else:
 # even when the socket is closed.
 const
   timeout = 2000
+  messagePaddingSize = 64 * 1024
 var port = Port(0)
 
 var sent = 0
@@ -31,10 +33,12 @@ proc isExpectedDisconnectionError(errCode: int32): bool =
     errCode == EBADF or errCode == ECONNRESET or errCode == EPIPE
 
 proc keepSendingTo(c: AsyncSocket) {.async.} =
+  let messagePadding = repeat('x', messagePaddingSize)
   while true:
-    # This write will eventually get stuck because the client is not reading
-    # its messages.
-    let sendFut = c.send("Foobar" & $sent & "\n", flags = {})
+    # Larger writes reach socket backpressure quickly even on slow CI machines.
+    # This write will eventually get stuck because the client is not reading.
+    # Keep the padding after the newline so recvLine does not drain it.
+    let sendFut = c.send("Foobar" & $sent & "\n" & messagePadding, flags = {})
     var sendTimedOut = false
     try:
       # On some platforms (notably macOS ARM64), the kernel may return

tests/async/tasyncdispatchordering.nim

@@ -0,0 +1,32 @@
+discard """
+  action: run
+"""
+
+import asyncdispatch, os
+
+proc wrap(fut: Future[void]): Future[void] =
+  result = newFuture[void]("wrap")
+  let retFuture = result
+  fut.addCallback proc () =
+    if fut.failed:
+      retFuture.fail(fut.error)
+    else:
+      retFuture.complete()
+
+block:
+  let root = newFuture[void]("root")
+  let wrapped = wrap(wrap(wrap(root)))
+  let completedBeforeDeadline = withTimeout(wrapped, 20)
+
+  # Completion has happened at the bottom of the future chain, but its
+  # callbacks cannot propagate until control reaches the dispatcher.
+  root.complete()
+  sleep(40)
+
+  doAssert waitFor(completedBeforeDeadline)
+
+block:
+  var callbackRan = false
+  sleepAsync(0).addCallback proc () = callbackRan = true
+  poll(0)
+  doAssert callbackRan

tests/ccgbugs2/t25883_tuple_sighash_collision.nim

@@ -0,0 +1,45 @@
+discard """
+targets: "c cpp"
+output: "13"
+"""
+
+# bug #25883: C codegen assigns same type hash to tuples with different nesting
+# but identical flattened content.
+# ((Int[1], Int[2]), Int[13], Int[14]) and ((Int[1], Int[2], Int[13]), Int[14])
+# must get distinct C type names.
+
+type
+  Int[V: static int] = object
+
+proc main() =
+  var b = ((1, 2), 13, 14)
+  var c = ((1, 2, 13), 14)
+  echo c[0][2]
+
+main()
+
+block:
+  type
+    Int[V: static int] = object
+    Layout[Sh, St] = object
+      shape: Sh
+      stride: St
+  
+  func makeB(): auto =
+    Layout[((Int[2], Int[3]), Int[5], Int[7]), ((Int[1], Int[2]), Int[6], Int[30])](
+      shape: ((Int[2](), Int[3]()), Int[5](), Int[7]()),
+      stride: ((Int[1](), Int[2]()), Int[6](), Int[30]())
+    )
+  
+  func makeC(): auto =
+    Layout[((Int[2], Int[3], Int[5]), Int[7]), ((Int[1], Int[2], Int[6]), Int[30])](
+      shape: ((Int[2](), Int[3](), Int[5]()), Int[7]()),
+      stride: ((Int[1](), Int[2](), Int[6]()), Int[30]())
+    )
+  
+  
+  proc main() =
+    let b = makeB()
+    let c = makeC()
+  
+  main()

tests/codegen/tgenbif.nim

@@ -0,0 +1,14 @@
+discard """
+  output: "ok"
+  targets: "c"
+  matrix: "--genBif:on"
+"""
+
+import std/[compilesettings, os]
+
+let cache = querySetting(nimcacheDir)
+var hasSemanticBif = false
+for path in walkFiles(cache / "*.s.bif"):
+  hasSemanticBif = true
+doAssert hasSemanticBif
+echo "ok"

tests/concepts/tmapconcept.nim

@@ -39,7 +39,7 @@ static:
   ok seq[int] is Enumerable[int]
   ok seq[string] is Enumerable
   ok seq[int] is Enumerable[SomeNumber]
-  ok typeof(SparseSeq.data) is Enumerable
+  ok SparseSeq.data is Enumerable
   no seq[string] is Enumerable[int]
   no int is Enumerable
   no int is Enumerable[int]

tests/effects/tissue25976.nim

@@ -0,0 +1,28 @@
+type
+  NestedPoll = object of RootEffect
+
+  CallbackFunc = proc(arg: pointer) {.gcsafe, raises: [], forbids: [NestedPoll].}
+  TaggedCallbackFunc = proc(arg: pointer) {.gcsafe, raises: [], tags: [], forbids: [NestedPoll].}
+
+  InternalAsyncCallback = object
+    fn: CallbackFunc
+
+  TaggedInternalAsyncCallback = object
+    fn: TaggedCallbackFunc
+
+proc closeSocket(aftercb: CallbackFunc = nil) =
+  proc continuation(udata: pointer) =
+    aftercb(nil)
+
+  let acb = InternalAsyncCallback(fn: continuation)
+  discard acb
+
+proc closeSocketTagged(aftercb: TaggedCallbackFunc = nil) =
+  proc continuation(udata: pointer) =
+    aftercb(nil)
+
+  let acb = TaggedInternalAsyncCallback(fn: continuation)
+  discard acb
+
+closeSocket()
+closeSocketTagged()

tests/generics/t21601.nim

@@ -0,0 +1,12 @@
+discard """
+  errormsg: "'typedesc' is not a concrete type"
+  line: 10
+"""
+
+# issue #21601
+type Person = object
+
+type Builder* = ref object of RootObj
+  class*: typedesc
+
+echo Builder(class: Person).repr

tests/generics/t24848.nim

@@ -0,0 +1,10 @@
+discard """
+  errormsg: "'typedesc[R[system.int]]' is not a concrete type"
+  line: 8
+"""
+
+# issue #24848
+type R[C] = ref object
+  b: C
+
+discard R[[R[int]]]()

tests/ic/mtraitparam.nim

@@ -0,0 +1,34 @@
+import std/macros
+
+type
+  Chunk* = ref object
+    x*: int32
+  ChunkTrait* = distinct tuple[
+    loaded: proc(self: pointer, chunk: Chunk)
+  ]
+
+macro makeVTable*(traitType: typedesc): untyped =
+  ## Splice the param symbols out of an imported proc type into a fresh proc
+  ## type nested in a fresh tuple type. Under `nim ic` the imported trait is
+  ## loaded from a NIF cache, so its param symbols are `Sealed`; re-owning them
+  ## in `semProcTypeNode` used to trip `ast.nim` `s.state != Sealed`.
+  var t = traitType.getTypeInst[1].getTypeImpl
+  if t.kind == nnkDistinctTy: t = t[0]
+  let formalParams = t[0][1][0]
+  var bridgeParams = nnkFormalParams.newTree(formalParams[0].copyNimTree)
+  bridgeParams.add nnkIdentDefs.newTree(ident"p", ident"pointer", newEmptyNode())
+  for j in 2 ..< formalParams.len:
+    bridgeParams.add formalParams[j].copyNimTree
+  let vtType = nnkTupleTy.newTree(
+    nnkIdentDefs.newTree(ident"m0",
+      nnkProcTy.newTree(bridgeParams, nnkPragma.newTree(ident"nimcall")),
+      newEmptyNode()))
+  let vtName = genSym(nskType, "VT")
+  let vtVar = genSym(nskVar, "vt")
+  result = nnkStmtList.newTree(
+    nnkTypeSection.newTree(
+      nnkTypeDef.newTree(vtName, newEmptyNode(), vtType)),
+    nnkVarSection.newTree(
+      nnkIdentDefs.newTree(
+        nnkPragmaExpr.newTree(vtVar, nnkPragma.newTree(ident"used")),
+        vtName, newEmptyNode())))

tests/ic/ttraitparam.nim

@@ -0,0 +1,14 @@
+discard """
+output: '''ok'''
+"""
+
+# Regression test: a `typed` macro in an imported module splices param symbols
+# out of an imported proc type into a freshly semchecked proc type. Under
+# `nim ic` those param symbols are loaded `Sealed` from the NIF cache; reusing
+# them in `newSymG`/`semProcTypeNode` used to fail `ast.nim` `s.state != Sealed`.
+
+import mtraitparam
+
+makeVTable(ChunkTrait)
+
+echo "ok"

tests/metatype/ttypedesc3.nim

@@ -48,6 +48,6 @@ type
   Foo[T] = object
     val: T
 
-var x: typeof(Foo[int].val)
+var x: Foo[int].val
 inc(x)
 echo x

tests/metatype/ttypedesc_field_legacy.nim

@@ -1,11 +0,0 @@
-discard """
-  matrix: "--legacy:typedescFieldAccess"
-  output: "4"
-"""
-
-type
-  Foo[T] = object
-    val: T
-
-var x: Foo[int].val = 4
-echo x

tests/pragmas/tcustom_pragma.nim

@@ -330,7 +330,7 @@ TypeDef
     Baz {.expectedAst(typeAst).} = object
       x: string
 
-  static: doAssert typeof(Baz.x) is string
+  static: doAssert Baz.x is string
 
   const procAst = """
 ProcDef

tests/range/timplicitrangedownsizing.nim

@@ -75,4 +75,31 @@ wf = smallFloatRange  # OK - SmallFloat range fits in WideFloatRange
 proc foo(x: Natural) =
   discard
 
-foo(12)
+foo(12)
+
+block:
+  type
+    E = enum
+      ea, eb
+
+    R = range[eb..eb]
+    I = range[0..3]
+
+  proc accept(r: R) = discard
+  proc accept(i: I) = discard
+
+  var r: R
+  var i: I
+  const enumOk = eb
+  const enumAlias = enumOk
+  const intOk = 1 + 2
+
+  r = eb
+  r = enumOk
+  r = enumAlias
+  accept(eb)
+  accept(enumOk)
+  accept(enumAlias)
+
+  i = intOk
+  accept(intOk)

tests/set/tset_range_trait.nim

@@ -0,0 +1,39 @@
+# Test that set[] accepts range types via typedesc[R], and set[typedesc[R]]
+# must unwrap the typedesc wrapper before checking ordinality.
+
+import std/typetraits
+
+type
+  TestDistinctRange = distinct range[0 .. 63]
+
+block: # explicit range type as set base
+  type S = set[range[0 .. 63]]
+  var s: S = {0, 1}
+  doAssert 0 in s
+
+block: # distinctBase result as set base (non-generic)
+  type S = set[TestDistinctRange.distinctBase]
+  var s: S = {0, 1}
+  doAssert 0 in s
+
+block: # range alias as set base
+  type RangeAlias = range[0 .. 63]
+  type S = set[RangeAlias]
+  var s: S = {0, 1}
+  doAssert 0 in s
+
+block: # set[T.distinctBase] in generic body type position
+  proc test[T: TestDistinctRange]() =
+    var s: set[T.distinctBase]
+    s = {0, 1}
+    doAssert 0 in s
+
+  test[TestDistinctRange]()
+
+block: # passing set[T.distinctBase] to a proc expecting set[0..63]
+  proc accept(x: typedesc[set[0 .. 63]]) = discard
+
+  proc pass[T: TestDistinctRange](p: typedesc[set[T]]) =
+    accept(set[T.distinctBase])
+
+  pass(set[TestDistinctRange])

tests/stdlib/txmltree.nim

@@ -118,3 +118,14 @@ block: #21541
   doAssert temp.text == "Hello!"
   temp.text = "Hola!"
   doAssert temp.text == "Hola!"
+
+block: #26039
+  let tree = <>rss(
+    "xmlns:atom" = "http://www.w3.org/2005/Atom",
+    <>"atom:link"(
+      `data-dummy` = "test",
+    ),
+  )
+  doAssert $tree == """<rss xmlns:atom="http://www.w3.org/2005/Atom">
+  <atom:link data-dummy="test" />
+</rss>"""

tests/system/tdeepcopy_nocopy.nim

@@ -0,0 +1,12 @@
+discard """
+  matrix: "--mm:refc; --mm:orc --deepcopy:on"
+  errormsg: "'deepCopy' is not available for type <NoCopy>"
+  file: "system.nim"
+"""
+
+type NoCopy = object
+
+proc `=copy`(a: var NoCopy; b: NoCopy) {.error.}
+
+var a = new NoCopy
+var b = deepCopy(a)

tests/system/tdeepcopy_nocopy_field.nim

@@ -0,0 +1,15 @@
+discard """
+  matrix: "--mm:refc; --mm:orc --deepcopy:on"
+  errormsg: "'deepCopy' is not available for type <Container>"
+  file: "system.nim"
+"""
+
+type
+  NoCopy = object
+  Container = object
+    value: NoCopy
+
+proc `=copy`(a: var NoCopy; b: NoCopy) {.error.}
+
+var a = new Container
+var b = deepCopy(a)

tests/threads/tsharedfreelistbigchunks.nim

@@ -0,0 +1,40 @@
+discard """
+  matrix: "--mm:arc; --mm:orc"
+"""
+
+import std/[atomics, typedthreads]
+
+const numChunks = 23 # More than the allocator's bounded drain can process.
+
+var
+  pointers: array[numChunks, pointer]
+  allocated: Atomic[bool]
+  continueAllocating: Atomic[bool]
+
+proc allocPointers() {.thread.} =
+  for i in 0..<pointers.len:
+    pointers[i] = allocShared(8192)
+  allocated.store(true, moRelease)
+
+  while not continueAllocating.load(moAcquire):
+    discard
+
+  # The first allocation drains MaxSteps + 1 chunks. The second allocation
+  # must still be able to find and drain the remainder.
+  for _ in 0..1:
+    let p = allocShared(8192)
+    deallocShared(p)
+
+  doAssert getOccupiedMem() == 0
+
+var thread: Thread[void]
+createThread(thread, allocPointers)
+
+while not allocated.load(moAcquire):
+  discard
+
+for p in pointers:
+  deallocShared(p)
+continueAllocating.store(true, moRelease)
+
+joinThread(thread)

tests/vm/tbroadcastarraymutation.nim

@@ -0,0 +1,101 @@
+type
+  Container = object
+    numbers: seq[int]
+    text: string
+    chars: set[char]
+
+  Variant = object
+    case enabled: bool
+    of false:
+      numbers: seq[int]
+    else:
+      discard
+
+  Index = enum
+    index0, index1, index2, index3, index4, index5, index6, index7,
+    index8, index9, index10, index11, index12, index13, index14, index15,
+    index16, index17, index18, index19, index20, index21, index22, index23,
+    index24, index25, index26, index27, index28, index29, index30, index31,
+    index32
+
+  Outer = object
+    values: array[33, seq[int]]
+
+proc directSeq(): array[33, seq[int]] =
+  result[32].add 1
+
+proc directStringChar(): array[33, string] =
+  result[32].add 'a'
+
+proc directStringString(): array[33, string] =
+  result[32].add "ab"
+
+proc directSet(): array[33, set[char]] =
+  result[32].incl 'a'
+
+proc fieldSeq(): array[33, Container] =
+  result[32].numbers.add 1
+
+proc fieldStringChar(): array[33, Container] =
+  result[32].text.add 'a'
+
+proc fieldStringString(): array[33, Container] =
+  result[32].text.add "ab"
+
+proc fieldSet(): array[33, Container] =
+  result[32].chars.incl 'a'
+
+proc nestedSeq(): array[33, array[33, seq[int]]] =
+  result[32][32].add 1
+
+proc checkedFieldSeq(): array[33, Variant] =
+  result[32].numbers.add 1
+
+proc enumIndexSeq(): array[Index, seq[int]] =
+  result[index32].add 1
+
+proc rangeIndexSeq(): array[10..42, seq[int]] =
+  result[42].add 1
+
+proc firstIndexSeq(): array[33, seq[int]] =
+  result[0].add 1
+
+proc middleIndexSeq(): array[33, seq[int]] =
+  result[16].add 1
+
+proc objectArraySeq(): Outer =
+  result.values[32].add 1
+
+proc singleEvaluation(): tuple[values: array[33, seq[int]], evaluations: int] =
+  var evaluations = 0
+  proc index(): int =
+    inc evaluations
+    32
+  result.values[index()].add 1
+  result.evaluations = evaluations
+
+proc test =
+  let direct = directSeq()
+  doAssert direct[0].len == 0
+  doAssert direct[31].len == 0
+  doAssert direct[32] == @[1]
+  doAssert directStringChar()[32] == "a"
+  doAssert directStringString()[32] == "ab"
+  doAssert 'a' in directSet()[32]
+  doAssert fieldSeq()[32].numbers == @[1]
+  doAssert fieldStringChar()[32].text == "a"
+  doAssert fieldStringString()[32].text == "ab"
+  doAssert 'a' in fieldSet()[32].chars
+  doAssert nestedSeq()[32][32] == @[1]
+  doAssert checkedFieldSeq()[32].numbers == @[1]
+  doAssert enumIndexSeq()[index32] == @[1]
+  doAssert rangeIndexSeq()[42] == @[1]
+  doAssert firstIndexSeq()[0] == @[1]
+  doAssert middleIndexSeq()[16] == @[1]
+  doAssert objectArraySeq().values[32] == @[1]
+  let evaluated = singleEvaluation()
+  doAssert evaluated.values[32] == @[1]
+  doAssert evaluated.evaluations == 1
+
+static: test()
+test()

tests/yrc/tyrc_fuzz_graph.nim

@@ -0,0 +1,84 @@
+discard """
+  cmd: "nim c --mm:yrc -d:useMalloc --threads:on $file"
+  output: "ok"
+  disabled: "windows"
+  disabled: "freebsd"
+  disabled: "openbsd"
+"""
+
+# Deterministic port of dumpster's `fuzz` test
+# (https://claytonwramsey.com/blog/dumpster/): drive a mutable object graph
+# through a long random sequence of node/edge inserts and removals, then drop
+# every root and assert that *every allocation ever made is destroyed exactly
+# once* -- no leak (count 0) and no double free (count > 1). The graph grows
+# thick with overlapping and self cycles, so only the cycle collector can wind
+# it down. A fixed LCG seed makes the shape reproducible across runs.
+
+type
+  DropCount = object
+    id: int
+    live: bool          # false in any moved-from temporary -> never miscounts
+  Node = ref object
+    refs: seq[Node]
+    dc: DropCount
+
+var counts: seq[int]    # counts[id] == times allocation `id` was destroyed
+
+proc `=destroy`(x: DropCount) =
+  if x.live: inc counts[x.id]
+
+var nextId = 0
+proc newNode(): Node =
+  counts.add 0
+  result = Node(refs: @[], dc: DropCount(id: nextId, live: true))
+  inc nextId
+
+# `child` is a by-value borrow (dumpster's `Gc::clone`): storing it copies the
+# reference, leaving the caller's root slot still owning. Using `.refs.add`
+# directly would move the root at its last read and change the graph shape.
+proc link(parent, child: Node) = parent.refs.add child
+
+# Small fixed-seed LCG (Numerical Recipes constants) for reproducible shape.
+var rngState: uint32 = 12345
+proc rnd(n: int): int =
+  rngState = rngState * 1664525'u32 + 1013904223'u32
+  int((rngState shr 16) mod uint32(n))
+
+proc run =
+  const N = 20_000
+  var roots: seq[Node]
+  for i in 0 ..< 50: roots.add newNode()
+
+  for _ in 0 ..< N:
+    if roots.len == 0: roots.add newNode()
+    case rnd(4)
+    of 0:                                   # allocate a fresh root
+      roots.add newNode()
+    of 1:                                   # add edge from -> to (may self-loop)
+      let a = rnd(roots.len)
+      let b = rnd(roots.len)
+      link(roots[a], roots[b])
+    of 2:                                   # drop a root handle (swap-remove)
+      let i = rnd(roots.len)
+      roots[i] = roots[roots.high]
+      roots.setLen roots.len - 1
+    else:                                   # drop one outgoing edge of a root
+      let a = rnd(roots.len)
+      if roots[a].refs.len > 0:
+        let j = rnd(roots[a].refs.len)
+        roots[a].refs[j] = roots[a].refs[roots[a].refs.high]
+        roots[a].refs.setLen roots[a].refs.len - 1
+
+  roots.setLen 0                            # release every remaining root
+  GC_fullCollect()
+  GC_fullCollect()
+
+run()
+
+var missing = 0
+for id in 0 ..< nextId:
+  if counts[id] != 1:
+    inc missing
+doAssert missing == 0, "graph not fully reclaimed: " & $missing & " of " &
+  $nextId & " allocations leaked or double-freed"
+echo "ok"

tests/yrc/tyrc_leak.nim

@@ -0,0 +1,33 @@
+discard """
+  cmd: "nim c --mm:yrc -d:useMalloc --threads:on $file"
+  output: "ok"
+  disabled: "windows"
+  disabled: "freebsd"
+  disabled: "openbsd"
+"""
+
+# Memory must stay bounded while creating cyclic garbage forever: the
+# collector has to keep pace with allocation. A leak shows up as unbounded
+# peak occupancy, which the assertion below catches.
+
+type Node = ref object
+  next: Node
+  data: seq[int]
+
+proc mk(n: int) =
+  var h = Node(data: newSeq[int](4))
+  var c = h
+  for i in 1 ..< n:
+    c.next = Node(data: newSeq[int](4))
+    c = c.next
+  c.next = h
+
+var peak = 0
+for round in 0 ..< 30:
+  for i in 0 ..< 10_000:
+    mk(8)
+  let occ = getOccupiedMem()
+  if occ > peak: peak = occ
+doAssert peak < 64 * 1024 * 1024, "memory exploded: leak"
+GC_fullCollect()
+echo "ok"

tests/yrc/tyrc_micro.nim

@@ -0,0 +1,26 @@
+discard """
+  cmd: "nim c --mm:yrc -d:useMalloc --threads:on $file"
+  output: "done"
+  valgrind: "leaks"
+  disabled: "windows"
+  disabled: "freebsd"
+  disabled: "openbsd"
+"""
+
+# Smallest possible cycle: a three-node ring that is dead the instant `mk`
+# returns. GC_fullCollect must reclaim it without touching freed memory.
+
+type Node = ref object
+  next: Node
+
+proc mk =
+  let a = Node()
+  let b = Node()
+  let c = Node()
+  a.next = b
+  b.next = c
+  c.next = a
+
+mk()
+GC_fullCollect()
+echo "done"

tests/yrc/tyrc_parallel_loop.nim

@@ -0,0 +1,74 @@
+discard """
+  cmd: "nim c --mm:yrc -d:useMalloc --threads:on $file"
+  output: "ok"
+  valgrind: "leaks"
+  disabled: "windows"
+  disabled: "freebsd"
+  disabled: "openbsd"
+"""
+
+# The "parallel_loop" complex graph from Clayton Ramsey's `dumpster` collector
+# (https://claytonwramsey.com/blog/dumpster/). Four allocations form a single
+# SCC built from two *overlapping* cycles that share nodes 1 and 4:
+#
+#     1 -> 4        4 -> 2, 4 -> 3        2 -> 1, 3 -> 1
+#
+# so 1->4->2->1 and 1->4->3->1 traverse the same 1 and 4. Every node keeps a
+# nonzero refcount from *inside* the SCC, so plain reference counting can never
+# free any of them; only cycle collection can, and only once the last external
+# handle is gone. We drop the four root handles one at a time and assert that
+# nothing is reclaimed until the final drop, then all four die together -- the
+# exact assertion sequence dumpster's test makes.
+
+type
+  # A field whose destructor bumps a per-node counter when the cell is freed;
+  # `slot` is nil in any moved-from temporary, so those don't miscount.
+  DropCount = object
+    slot: ptr int
+  Node = ref object
+    refs: seq[Node]
+    dc: DropCount
+
+proc `=destroy`(x: DropCount) =
+  if x.slot != nil: inc x.slot[]
+
+# Add an edge parent -> child. `child` is a by-value borrow, so the caller's
+# handle keeps owning its reference -- this is Nim's equivalent of dumpster's
+# `Gc::clone`. Building edges with `g1.refs.add g2` instead would *move* g2 at
+# its last read and silently collapse the graph's root set.
+proc link(parent, child: Node) = parent.refs.add child
+
+# drops[0] is unused; nodes are 1..4 to mirror the blog's gc1..gc4. The four
+# handles live in an array so each stays an independent, still-owning root.
+var drops: array[5, int]
+
+proc scenario =
+  var g: array[1..4, Node]
+  for i in 1..4: g[i] = Node(dc: DropCount(slot: addr drops[i]))
+  link(g[2], g[1])          # 2 -> 1
+  link(g[3], g[1])          # 3 -> 1
+  link(g[4], g[2])          # 4 -> 2
+  link(g[4], g[3])          # 4 -> 3
+  link(g[1], g[4])          # 1 -> 4  (closes both cycles)
+
+  GC_fullCollect()
+  doAssert drops == [0, 0, 0, 0, 0], "nothing dead yet"
+
+  g[1] = nil        # node1 still held by node2 and node3
+  GC_fullCollect()
+  doAssert drops == [0, 0, 0, 0, 0], "dropping root 1 frees nothing"
+
+  g[2] = nil        # node2 still held by node4
+  GC_fullCollect()
+  doAssert drops == [0, 0, 0, 0, 0], "dropping root 2 frees nothing"
+
+  g[3] = nil        # node3 still held by node4
+  GC_fullCollect()
+  doAssert drops == [0, 0, 0, 0, 0], "dropping root 3 frees nothing"
+
+  g[4] = nil        # last external handle gone: the whole SCC is garbage
+  GC_fullCollect()
+  doAssert drops == [0, 1, 1, 1, 1], "the full cycle is reclaimed at once"
+
+scenario()
+echo "ok"

tests/yrc/tyrc_partial.nim

@@ -0,0 +1,33 @@
+discard """
+  cmd: "nim c --mm:yrc -d:useMalloc --threads:on $file"
+  output: "ok"
+  valgrind: "leaks"
+  disabled: "windows"
+  disabled: "freebsd"
+  disabled: "openbsd"
+"""
+
+# Exercise the manual collection API: disable automatic collections, build a
+# batch of dead cycles, then reclaim them in halves via GC_partialCollect and
+# confirm the pending count shrinks accordingly.
+
+type Node = ref object
+  next: Node
+
+proc mk(n: int) =
+  var h = Node()
+  var c = h
+  for i in 1 ..< n: (c.next = Node(); c = c.next)
+  c.next = h
+
+GC_disableOrc()   # no automatic collections; exercise the partial API
+for i in 0 ..< 300: mk(4)
+let pending = GC_prepareOrc()
+doAssert pending > 0
+GC_partialCollect(pending div 2)          # collect only the upper half
+let remaining = GC_prepareOrc()
+doAssert remaining <= pending div 2, $remaining & " vs " & $pending
+GC_partialCollect(0)                      # collect the rest
+doAssert GC_prepareOrc() == 0
+GC_fullCollect()
+echo "ok"

tests/yrc/tyrc_rings.nim

@@ -0,0 +1,60 @@
+discard """
+  cmd: "nim c --mm:yrc -d:useMalloc --threads:on $file"
+  output: "ok"
+  valgrind: "leaks"
+  disabled: "windows"
+  disabled: "freebsd"
+  disabled: "openbsd"
+"""
+
+# Functional test for the Tarjan-based collector: doubly-linked dead rings,
+# self-referential cells, and one surviving ring whose integrity is checked
+# after a full collect.
+
+type
+  Node = ref object
+    next: Node
+    prev: Node
+    data: string
+
+proc makeRing(n: int): Node =
+  result = Node(data: "head")
+  var cur = result
+  for i in 1 ..< n:
+    let x = Node(data: $i)
+    cur.next = x
+    x.prev = cur
+    cur = x
+  cur.next = result
+  result.prev = cur
+
+proc dropRings =
+  for i in 0 ..< 2000:
+    discard makeRing(10)   # dead immediately
+
+proc keepOne: Node =
+  for i in 0 ..< 100:
+    discard makeRing(5)
+  result = makeRing(7)     # survives
+
+proc selfRef =
+  type S = ref object
+    self: S
+    buf: seq[int]
+  for i in 0 ..< 500:
+    let s = S(buf: newSeq[int](8))
+    s.self = s
+
+dropRings()
+selfRef()
+let keep = keepOne()
+GC_fullCollect()
+doAssert keep.data == "head"
+var cnt = 0
+var it = keep
+while true:
+  inc cnt
+  it = it.next
+  if it == keep: break
+doAssert cnt == 7, "live ring corrupted: " & $cnt
+echo "ok"

tests/yrc/tyrc_satb.nim

@@ -0,0 +1,72 @@
+discard """
+  cmd: "nim c --mm:yrc -d:useMalloc --threads:on $file"
+  output: "ok"
+  disabled: "windows"
+  disabled: "freebsd"
+  disabled: "openbsd"
+"""
+
+# Concurrent stress for the lock-free SATB collector: mutator threads rewire
+# live cyclic structures (constant dirty traffic + capture aborts) and churn
+# garbage cycles while a dedicated thread runs back-to-back collections. Live
+# data corruption or a lost object trips a doAssert / a growing residual.
+
+import std/typedthreads
+
+type Node = ref object
+  next: Node        # ring structure, stable
+  payload: Node     # rewired constantly -> candidates + dirty SCCs
+  id: int
+
+const NWorkers = 3
+const Iters = 400_000
+const RingLen = 64
+
+var stopFlag: bool
+var done: array[NWorkers, int]
+
+proc mkRing(tag: int): seq[Node] =
+  result = newSeq[Node](RingLen)
+  for i in 0 ..< RingLen: result[i] = Node(id: tag + i)
+  for i in 0 ..< RingLen:
+    result[i].next = result[(i+1) mod RingLen]
+    result[i].payload = result[(i*13+7) mod RingLen]
+
+proc verify(ring: seq[Node]; tag: int) =
+  for i in 0 ..< RingLen:
+    doAssert ring[i].id == tag + i, "node corrupted"
+    doAssert ring[i].next.id == tag + (i+1) mod RingLen, "ring broken"
+    doAssert ring[i].payload.id >= tag and ring[i].payload.id < tag + RingLen,
+      "payload points outside ring: live data corrupted"
+
+proc worker(tid: int) {.thread.} =
+  var tag = tid * 1_000_000
+  var ring = mkRing(tag)
+  for i in 0 ..< Iters:
+    # lock-free barrier hot path: rewire a payload edge inside the live ring.
+    # decs the old target (rc > 0) -> candidate; collections capture the live
+    # ring concurrently and must rescue or abort, never free it.
+    ring[i mod RingLen].payload = ring[(i * 7 + 3) mod RingLen]
+    if (i and 8191) == 0:
+      verify(ring, tag)
+    if (i and 32767) == 0:
+      inc tag, RingLen
+      ring = mkRing(tag)   # old ring becomes a garbage cycle tangle
+  verify(ring, tag)
+  done[tid] = 1
+
+proc collector() {.thread.} =
+  while not stopFlag:
+    GC_runOrc()
+
+var th: array[NWorkers, Thread[int]]
+var col: Thread[void]
+createThread(col, collector)
+for i in 0 ..< NWorkers: createThread(th[i], worker, i)
+joinThreads(th)
+stopFlag = true
+joinThread(col)
+for i in 0 ..< NWorkers: doAssert done[i] == 1
+GC_fullCollect()
+GC_fullCollect()
+echo "ok"

tests/yrc/tyrc_threads.nim

@@ -0,0 +1,60 @@
+discard """
+  cmd: "nim c --mm:yrc -d:useMalloc --threads:on $file"
+  output: "ok"
+  disabled: "windows"
+  disabled: "freebsd"
+  disabled: "openbsd"
+"""
+
+# N threads each churn garbage cycles while maintaining one live ring that is
+# verified continuously and replaced, plus explicit GC_runOrc collections from
+# every thread. Corruption of live data trips a doAssert.
+
+import std/typedthreads
+
+type Node = ref object
+  next: Node
+  prev: Node
+  id: int
+
+const NThreads = 4
+const Iters = 30_000
+
+proc mkRing(n, tag: int): Node =
+  result = Node(id: tag)
+  var c = result
+  for i in 1 ..< n:
+    let x = Node(id: tag + i)
+    c.next = x
+    x.prev = c
+    c = x
+  c.next = result
+  result.prev = c
+
+proc checkRing(r: Node; n, tag: int) =
+  var c = r
+  for i in 0 ..< n:
+    doAssert c.id == tag + i, "ring corrupted!"
+    c = c.next
+  doAssert c == r, "ring not closed!"
+
+var results: array[NThreads, int]
+
+proc worker(tid: int) {.thread.} =
+  var keep = mkRing(5, tid * 1000)
+  for i in 0 ..< Iters:
+    discard mkRing(3 + (i and 7), 999999)   # garbage
+    if (i and 255) == 0:
+      checkRing(keep, 5, tid * 1000)
+      keep = mkRing(5, tid * 1000)          # old keep becomes garbage
+    if (i and 1023) == 0:
+      GC_runOrc()                            # explicit collections from all threads
+  checkRing(keep, 5, tid * 1000)
+  results[tid] = 1
+
+var th: array[NThreads, Thread[int]]
+for i in 0 ..< NThreads: createThread(th[i], worker, i)
+joinThreads(th)
+for i in 0 ..< NThreads: doAssert results[i] == 1
+GC_fullCollect()
+echo "ok"

tools/deps.nim

@@ -52,7 +52,7 @@ proc updateSubmodules*(dir: string, allowBundled = false) =
     let oldDir = getCurrentDir()
     setCurrentDir(dir)
     try:
-      exec "git submodule update --init"
+      exec "git submodule update --init --recursive"
     finally:
       setCurrentDir(oldDir)
   elif allowBundled: