Fix closure environment node sharing in lambda lifting

When makeClosure creates multiple closure instances, it was reusing the same env node, causing DFA tracking issues. Each closure construction now gets a fresh nkSym node copy to avoid node identity problems. This fixes hash stability and prevents premature environment moves when closures are shared (e.g., let closure2 = closure1).
Importc codegen fix (#25511 )
2026-09-01 03:13:41 +00:00 · 2026-02-14 18:23:00 +01:00 · 2026-02-13 13:29:01 +01:00 · 2026-02-13 11:53:17 +01:00 · 2026-02-12 13:29:22 +01:00 · 2026-02-11 17:45:40 +01:00
58 changed files with 2380 additions and 247 deletions
--- a/compiler/btrees.nim
+++ b/compiler/btrees.nim
@@ -69,7 +69,7 @@ proc copyHalf[Key, Val](h, result: Node[Key, Val]) =
      result.links[j] = h.links[Mhalf + j]
  else:
    for j in 0..<Mhalf:
-      when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+      when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc) or defined(gcYrc):
        result.vals[j] = move h.vals[Mhalf + j]
      else:
        shallowCopy(result.vals[j], h.vals[Mhalf + j])
@@ -92,7 +92,7 @@ proc insert[Key, Val](h: Node[Key, Val], key: Key, val: Val): Node[Key, Val] =
      if less(key, h.keys[j]): break
      inc j
    for i in countdown(h.entries, j+1):
-      when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+      when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc) or defined(gcYrc):
        h.vals[i] = move h.vals[i-1]
      else:
        shallowCopy(h.vals[i], h.vals[i-1])
--- a/compiler/ccgcalls.nim
+++ b/compiler/ccgcalls.nim
@@ -331,7 +331,7 @@ proc withTmpIfNeeded(p: BProc, a: TLoc, needsTmp: bool): TLoc =
  # Bug https://github.com/status-im/nimbus-eth2/issues/1549
  # Aliasing is preferred over stack overflows.
  # Also don't regress for non ARC-builds, too risky.
-  if needsTmp and a.lode.typ != nil and p.config.selectedGC in {gcArc, gcAtomicArc, gcOrc} and
+  if needsTmp and a.lode.typ != nil and p.config.selectedGC in {gcArc, gcAtomicArc, gcOrc, gcYrc} and
      getSize(p.config, a.lode.typ) < 1024:
    result = getTemp(p, a.lode.typ, needsInit=false)
    genAssignment(p, result, a, {})
--- a/compiler/ccgexprs.nim
+++ b/compiler/ccgexprs.nim
@@ -416,7 +416,7 @@ proc genAssignment(p: BProc, dest, src: TLoc, flags: TAssignmentFlags) =
    else:
      simpleAsgn(p.s(cpsStmts), dest, src)
  of tyArray:
-    if containsGarbageCollectedRef(dest.t) and p.config.selectedGC notin {gcArc, gcAtomicArc, gcOrc, gcHooks}:
+    if containsGarbageCollectedRef(dest.t) and p.config.selectedGC notin {gcArc, gcAtomicArc, gcOrc, gcYrc, gcHooks}:
      genGenericAsgn(p, dest, src, flags)
    else:
      let rd = rdLoc(dest)
@@ -1832,7 +1832,7 @@ proc genObjConstr(p: BProc, e: PNode, d: var TLoc) =

  var tmp: TLoc = default(TLoc)
  var r: Rope
-  let needsZeroMem = p.config.selectedGC notin {gcArc, gcAtomicArc, gcOrc} or nfAllFieldsSet notin e.flags
+  let needsZeroMem = p.config.selectedGC notin {gcArc, gcAtomicArc, gcOrc, gcYrc} or nfAllFieldsSet notin e.flags
  if useTemp:
    tmp = getTemp(p, t)
    r = rdLoc(tmp)
@@ -2751,7 +2751,7 @@ proc genMove(p: BProc; n: PNode; d: var TLoc) =
    p.s(cpsStmts).addFieldAssignment(destVal, "p", dotField(srcVal, "p"))
  else:
    if d.k == locNone: d = getTemp(p, n.typ)
-    if p.config.selectedGC in {gcArc, gcAtomicArc, gcOrc}:
+    if p.config.selectedGC in {gcArc, gcAtomicArc, gcOrc, gcYrc}:
      genAssignment(p, d, a, {})
      var op = getAttachedOp(p.module.g.graph, n.typ, attachedWasMoved)
      if op == nil:
@@ -2835,7 +2835,7 @@ proc genSlice(p: BProc; e: PNode; d: var TLoc) =
  let (x, y) = genOpenArraySlice(p, e, e.typ, e.typ.elementType,
    prepareForMutation = e[1].kind == nkHiddenDeref and
                         e[1].typ.skipTypes(abstractInst).kind == tyString and
-                         p.config.selectedGC in {gcArc, gcAtomicArc, gcOrc})
+                         p.config.selectedGC in {gcArc, gcAtomicArc, gcOrc, gcYrc})
  if d.k == locNone: d = getTemp(p, e.typ)
  let dest = rdLoc(d)
  p.s(cpsStmts).addFieldAssignment(dest, "Field0", x)
@@ -3039,7 +3039,7 @@ proc genMagicExpr(p: BProc, e: PNode, d: var TLoc, op: TMagic) =
      let n = semparallel.liftParallel(p.module.g.graph, p.module.idgen, p.module.module, e)
      expr(p, n, d)
  of mDeepCopy:
-    if p.config.selectedGC in {gcArc, gcAtomicArc, gcOrc} and optEnableDeepCopy notin p.config.globalOptions:
+    if p.config.selectedGC in {gcArc, gcAtomicArc, gcOrc, gcYrc} and optEnableDeepCopy notin p.config.globalOptions:
      localError(p.config, e.info,
        "for --mm:arc|atomicArc|orc 'deepcopy' support has to be enabled with --deepcopy:on")

@@ -3271,7 +3271,11 @@ proc upConv(p: BProc, n: PNode, d: var TLoc) =
        p.s(cpsStmts).addCallStmt(cgsymValue(p.module, "raiseObjectConversionError"))
        raiseInstr(p, p.s(cpsStmts))

-  if n[0].typ.kind != tyObject:
+  # skip cast when types map to the same C type
+  # this avoids invalid C code like `*(T*)&x` for types that can't have their address taken (e.g., WASM __externref_t)
+  if getTypeDesc(p.module, n.typ) == getTypeDesc(p.module, n[0].typ):
+    expr(p, n[0], d)
+  elif n[0].typ.kind != tyObject:
    let destTyp = getTypeDesc(p.module, n.typ)
    let val = rdLoc(a)
    if n.isLValue:
@@ -3317,7 +3321,7 @@ proc downConv(p: BProc, n: PNode, d: var TLoc) =
        cCast(ptrType(destType),
          wrapPar(cAddr(wrapPar(val))))),
      a.storage)
-  elif p.module.compileToCpp:
+  elif p.module.compileToCpp or isImportedType(src):
    # C++ implicitly downcasts for us
    expr(p, arg, d)
  else:
--- a/compiler/ccgliterals.nim
+++ b/compiler/ccgliterals.nim
@@ -16,7 +16,7 @@
 ## implementation.

 template detectVersion(field, corename) =
-  if m.g.config.selectedGC in {gcArc, gcOrc, gcAtomicArc, gcHooks}:
+  if m.g.config.selectedGC in {gcArc, gcOrc, gcYrc, gcAtomicArc, gcHooks}:
    result = 2
  else:
    result = 1
--- a/compiler/ccgtypes.nim
+++ b/compiler/ccgtypes.nim
@@ -277,7 +277,7 @@ proc isInvalidReturnType(conf: ConfigRef; typ: PType, isProc = true): bool =
    of ctStruct:
      let t = skipTypes(rettype, typedescInst)
      if rettype.isImportedCppType or t.isImportedCppType or
-          (typ.callConv == ccCDecl and conf.selectedGC in {gcArc, gcAtomicArc, gcOrc}):
+          (typ.callConv == ccCDecl and conf.selectedGC in {gcArc, gcAtomicArc, gcOrc, gcYrc}):
        # prevents nrvo for cdecl procs; # bug #23401
        result = false
      else:
@@ -1692,7 +1692,7 @@ proc genHook(m: BModule; t: PType; info: TLineInfo; op: TTypeAttachedOp; result:
        echo "ayclic but has this =trace ", t, " ", theProc.ast
  else:
    when false:
-      if op == attachedTrace and m.config.selectedGC == gcOrc and
+      if op == attachedTrace and m.config.selectedGC in {gcOrc, gcYrc} and
          containsGarbageCollectedRef(t):
        # unfortunately this check is wrong for an object type that only contains
        # .cursor fields like 'Node' inside 'cycleleak'.
--- a/compiler/cgen.nim
+++ b/compiler/cgen.nim
@@ -1332,7 +1332,7 @@ proc genProcLvl3*(m: BModule, prc: PSym) =
        # declare the result symbol:
        assignLocalVar(p, resNode)
        assert(res.loc.snippet != "")
-        if p.config.selectedGC in {gcArc, gcAtomicArc, gcOrc} and
+        if p.config.selectedGC in {gcArc, gcAtomicArc, gcOrc, gcYrc} and
            allPathsAsgnResult(p, procBody) == InitSkippable:
          # In an ideal world the codegen could rely on injectdestructors doing its job properly
          # and then the analysis step would not be required.
@@ -1687,7 +1687,7 @@ proc hcrGetProcLoadCode(builder: var Builder, m: BModule, sym, prefix, handle, g
 # prevents inlining of the NimMainInner function and dependent
 # functions, which might otherwise merge their stack frames.
 proc isInnerMainVolatile(m: BModule): bool =
-  m.config.selectedGC notin {gcNone, gcArc, gcAtomicArc, gcOrc}
+  m.config.selectedGC notin {gcNone, gcArc, gcAtomicArc, gcOrc, gcYrc}

 proc genPreMain(m: BModule) =
  m.s[cfsProcs].addDeclWithVisibility(Private):
@@ -1699,8 +1699,6 @@ proc genPreMain(m: BModule) =
      m.s[cfsProcs].addVar(name = "cmdCount", typ = CInt)
    m.s[cfsProcs].addDeclWithVisibility(Private):
      m.s[cfsProcs].addVar(name = "cmdLine", typ = ptrType(ptrType(CChar)))
-    m.s[cfsProcs].addDeclWithVisibility(Private):
-      m.s[cfsProcs].addVar(name = "gEnv", typ = ptrType(ptrType(CChar)))
  m.s[cfsProcs].addDeclWithVisibility(Private):
    m.s[cfsProcs].addProcHeader(m.config.nimMainPrefix & "PreMain", CVoid, cProcParams())
    m.s[cfsProcs].finishProcHeaderWithBody():
@@ -1734,7 +1732,7 @@ proc genNimMainInner(m: BModule) =
  m.s[cfsProcs].addNewline()

 proc initStackBottom(m: BModule): bool =
-  not (m.config.target.targetOS == osStandalone or m.config.selectedGC in {gcNone, gcArc, gcAtomicArc, gcOrc})
+  not (m.config.target.targetOS == osStandalone or m.config.selectedGC in {gcNone, gcArc, gcAtomicArc, gcOrc, gcYrc})

 proc genNimMainProc(m: BModule, preMainCode: Snippet) =
  m.s[cfsProcs].addProcHeader(ccCDecl, m.config.nimMainPrefix & "NimMain", CVoid, cProcParams())
@@ -1761,12 +1759,10 @@ proc genNimMainBody(m: BModule, preMainCode: Snippet) =
 proc genPosixCMain(m: BModule) =
  m.s[cfsProcs].addProcHeader("main", CInt, cProcParams(
    (name: "argc", typ: CInt),
-    (name: "args", typ: ptrType(ptrType(CChar))),
-    (name: "env", typ: ptrType(ptrType(CChar)))))
+    (name: "args", typ: ptrType(ptrType(CChar)))))
  m.s[cfsProcs].finishProcHeaderWithBody():
    m.s[cfsProcs].addAssignment("cmdLine", "args")
    m.s[cfsProcs].addAssignment("cmdCount", "argc")
-    m.s[cfsProcs].addAssignment("gEnv", "env")
    genMainProcsWithResult(m)
  m.s[cfsProcs].addNewline()

@@ -1864,7 +1860,7 @@ proc genMainProc(m: BModule) =
        builder.addCallStmt(cgsymValue(m, "nimLoadLibraryError"), strLit)

    loadLib(preMainBuilder, "hcr_handle", "hcrGetProc")
-    if m.config.selectedGC in {gcArc, gcAtomicArc, gcOrc}:
+    if m.config.selectedGC in {gcArc, gcAtomicArc, gcOrc, gcYrc}:
      preMainBuilder.addCallStmt(m.config.nimMainPrefix & "PreMain")
    else:
      preMainBuilder.addVar(name = "rtl_handle", typ = CPointer)
@@ -2034,7 +2030,7 @@ proc registerModuleToMain(g: BModuleList; m: BModule) =
  if sfSystemModule in m.module.flags:
    if emulatedThreadVars(m.config) and m.config.target.targetOS != osStandalone:
      g.mainDatInit.addCallStmt(cgsymValue(m, "initThreadVarsEmulation"))
-    if m.config.target.targetOS != osStandalone and m.config.selectedGC notin {gcNone, gcArc, gcAtomicArc, gcOrc}:
+    if m.config.target.targetOS != osStandalone and m.config.selectedGC notin {gcNone, gcArc, gcAtomicArc, gcOrc, gcYrc}:
      g.mainDatInit.addCallStmt(cgsymValue(m, "initStackBottomWith"),
        cCast(CPointer, cAddr("inner")))

@@ -2603,7 +2599,7 @@ proc finalCodegenActions*(graph: ModuleGraph; m: BModule; n: PNode) =
        cgsym(m, "rawWrite")

      # raise dependencies on behalf of genMainProc
-      if m.config.target.targetOS != osStandalone and m.config.selectedGC notin {gcNone, gcArc, gcAtomicArc, gcOrc}:
+      if m.config.target.targetOS != osStandalone and m.config.selectedGC notin {gcNone, gcArc, gcAtomicArc, gcOrc, gcYrc}:
        cgsym(m, "initStackBottomWith")
      if emulatedThreadVars(m.config) and m.config.target.targetOS != osStandalone:
        cgsym(m, "initThreadVarsEmulation")
@@ -2611,7 +2607,7 @@ proc finalCodegenActions*(graph: ModuleGraph; m: BModule; n: PNode) =
      if m.g.forwardedProcs.len == 0:
        incl m.flags, objHasKidsValid
      if optMultiMethods in m.g.config.globalOptions or
-          m.g.config.selectedGC notin {gcArc, gcOrc, gcAtomicArc} or
+          m.g.config.selectedGC notin {gcArc, gcOrc, gcAtomicArc, gcYrc} or
          vtables notin m.g.config.features:
        generateIfMethodDispatchers(graph, m.idgen)

--- a/compiler/commands.nim
+++ b/compiler/commands.nim
@@ -245,7 +245,7 @@ proc processCompile(conf: ConfigRef; filename: string) =
  extccomp.addExternalFileToCompile(conf, found)

 const
-  errNoneBoehmRefcExpectedButXFound = "'arc', 'orc', 'atomicArc', 'markAndSweep', 'boehm', 'go', 'none', 'regions', or 'refc' expected, but '$1' found"
+  errNoneBoehmRefcExpectedButXFound = "'arc', 'orc', 'yrc', 'atomicArc', 'markAndSweep', 'boehm', 'go', 'none', 'regions', or 'refc' expected, but '$1' found"
  errNoneSpeedOrSizeExpectedButXFound = "'none', 'speed' or 'size' expected, but '$1' found"
  errGuiConsoleOrLibExpectedButXFound = "'gui', 'console', 'lib' or 'staticlib' expected, but '$1' found"
  errInvalidExceptionSystem = "'goto', 'setjmp', 'cpp' or 'quirky' expected, but '$1' found"
@@ -266,6 +266,7 @@ proc testCompileOptionArg*(conf: ConfigRef; switch, arg: string, info: TLineInfo
    of "markandsweep": result = conf.selectedGC == gcMarkAndSweep
    of "destructors", "arc": result = conf.selectedGC == gcArc
    of "orc": result = conf.selectedGC == gcOrc
+    of "yrc": result = conf.selectedGC == gcYrc
    of "hooks": result = conf.selectedGC == gcHooks
    of "go": result = conf.selectedGC == gcGo
    of "none": result = conf.selectedGC == gcNone
@@ -570,6 +571,7 @@ proc unregisterArcOrc*(conf: ConfigRef) =
  undefSymbol(conf.symbols, "gcdestructors")
  undefSymbol(conf.symbols, "gcarc")
  undefSymbol(conf.symbols, "gcorc")
+  undefSymbol(conf.symbols, "gcyrc")
  undefSymbol(conf.symbols, "gcatomicarc")
  undefSymbol(conf.symbols, "nimSeqsV2")
  undefSymbol(conf.symbols, "nimV2")
@@ -603,6 +605,10 @@ proc processMemoryManagementOption(switch, arg: string, pass: TCmdLinePass,
      conf.selectedGC = gcOrc
      defineSymbol(conf.symbols, "gcorc")
      registerArcOrc(pass, conf)
+    of "yrc":
+      conf.selectedGC = gcYrc
+      defineSymbol(conf.symbols, "gcyrc")
+      registerArcOrc(pass, conf)
    of "atomicarc":
      conf.selectedGC = gcAtomicArc
      defineSymbol(conf.symbols, "gcatomicarc")
--- a/compiler/dfa.nim
+++ b/compiler/dfa.nim
@@ -483,7 +483,7 @@ proc constructCfg*(s: PSym; body: PNode; root: PSym): ControlFlowGraph =
    gen(c, body)
    if root.kind == skResult:
      genImplicitReturn(c)
-  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc) or defined(gcYrc):
    result = c.code # will move
  else:
    shallowCopy(result, c.code)
--- a/compiler/injectdestructors.nim
+++ b/compiler/injectdestructors.nim
@@ -69,7 +69,7 @@ proc hasDestructor(c: Con; t: PType): bool {.inline.} =
  result = ast.hasDestructor(t)
  when toDebug.len > 0:
    # for more effective debugging
-    if not result and c.graph.config.selectedGC in {gcArc, gcOrc, gcAtomicArc}:
+    if not result and c.graph.config.selectedGC in {gcArc, gcOrc, gcYrc, gcAtomicArc}:
      assert(not containsGarbageCollectedRef(t))

 proc getTemp(c: var Con; s: var Scope; typ: PType; info: TLineInfo): PNode =
@@ -165,7 +165,7 @@ proc isLastReadImpl(n: PNode; c: var Con; scope: var Scope): bool =

 template hasDestructorOrAsgn(c: var Con, typ: PType): bool =
  # bug #23354; an object type could have a non-trivial assignements when it is passed to a sink parameter
-  hasDestructor(c, typ) or (c.graph.config.selectedGC in {gcArc, gcOrc, gcAtomicArc} and
+  hasDestructor(c, typ) or (c.graph.config.selectedGC in {gcArc, gcOrc, gcYrc, gcAtomicArc} and
        typ.kind == tyObject and not isTrivial(getAttachedOp(c.graph, typ, attachedAsgn)))

 proc isLastRead(n: PNode; c: var Con; s: var Scope): bool =
@@ -329,14 +329,14 @@ proc isCriticalLink(dest: PNode): bool {.inline.} =
  result = dest.kind != nkSym

 proc finishCopy(c: var Con; result, dest: PNode; flags: set[MoveOrCopyFlag]; isFromSink: bool) =
-  if c.graph.config.selectedGC == gcOrc and IsExplicitSink notin flags:
+  if c.graph.config.selectedGC in {gcOrc, gcYrc} and IsExplicitSink notin flags:
    # add cyclic flag, but not to sink calls, which IsExplicitSink generates
    let t = dest.typ.skipTypes(tyUserTypeClasses + {tyGenericInst, tyAlias, tySink, tyDistinct})
    if cyclicType(c.graph, t):
      result.add boolLit(c.graph, result.info, isFromSink or isCriticalLink(dest))

 proc genMarkCyclic(c: var Con; result, dest: PNode) =
-  if c.graph.config.selectedGC == gcOrc:
+  if c.graph.config.selectedGC in {gcOrc, gcYrc}:
    let t = dest.typ.skipTypes({tyGenericInst, tyAlias, tySink, tyDistinct})
    if cyclicType(c.graph, t):
      if t.kind == tyRef:
@@ -495,7 +495,7 @@ proc passCopyToSink(n: PNode; c: var Con; s: var Scope): PNode =
      localError(c.graph.config, n.info, errFailedMove,
        ("cannot move '$1', passing '$1' to a sink parameter introduces an implicit copy") % $n)
  else:
-    if c.graph.config.selectedGC in {gcArc, gcOrc, gcAtomicArc}:
+    if c.graph.config.selectedGC in {gcArc, gcOrc, gcYrc, gcAtomicArc}:
      assert(not containsManagedMemory(nTyp))
    if nTyp.skipTypes(abstractInst).kind in {tyOpenArray, tyVarargs}:
      localError(c.graph.config, n.info, "cannot create an implicit openArray copy to be passed to a sink parameter")
@@ -926,7 +926,7 @@ proc p(n: PNode; c: var Con; s: var Scope; mode: ProcessMode; tmpFlags = {sfSing

      if n[0].kind == nkSym and n[0].sym.magic in {mNew, mNewFinalize}:
        result[0] = copyTree(n[0])
-        if c.graph.config.selectedGC in {gcHooks, gcArc, gcAtomicArc, gcOrc}:
+        if c.graph.config.selectedGC in {gcHooks, gcArc, gcAtomicArc, gcOrc, gcYrc}:
          let destroyOld = c.genDestroy(result[1])
          result = newTree(nkStmtList, destroyOld, result)
      else:
--- a/compiler/lambdalifting.nim
+++ b/compiler/lambdalifting.nim
@@ -224,7 +224,8 @@ proc makeClosure*(g: ModuleGraph; idgen: IdGenerator; prc: PSym; env: PNode; inf
  else:
    if env.skipConv.kind == nkClosure:
      localError(g.config, info, "internal error: taking closure of closure")
-    result.add(env)
+    # Create a fresh copy to avoid node sharing issues with DFA
+    result.add(if env.kind == nkSym: newSymNode(env.sym, env.info) else: env)
  #if isClosureIterator(result.typ):
  createTypeBoundOps(g, nil, result.typ, info, idgen)
  if tfHasAsgn in result.typ.flags or optSeqDestructors in g.config.globalOptions:
--- a/compiler/liftdestructors.nim
+++ b/compiler/liftdestructors.nim
@@ -163,7 +163,7 @@ proc fillBodyObj(c: var TLiftCtx; n, body, x, y: PNode; enforceDefaultOp: bool,
    if c.filterDiscriminator != nil: return
    let f = n.sym
    let b = if c.kind == attachedTrace: y else: y.dotField(f)
-    if (sfCursor in f.flags and c.g.config.selectedGC in {gcArc, gcAtomicArc, gcOrc, gcHooks}) or
+    if (sfCursor in f.flags and c.g.config.selectedGC in {gcArc, gcAtomicArc, gcOrc, gcYrc, gcHooks}) or
        enforceDefaultOp:
      defaultOp(c, f.typ, body, x.dotField(f), b)
    else:
@@ -558,6 +558,22 @@ proc declareTempOf(c: var TLiftCtx; body: PNode; value: PNode): PNode =
  v.addVar(result, value)
  body.add v

+proc considerInferDupFromCopy(c: var TLiftCtx; t: PType; body, x, y: PNode): bool =
+  ## For `=dup`, if no explicit hook exists, try to infer from `=copy` hook
+  ## to maintain backward compatibility. Returns true if inference was applied.
+  if c.kind == attachedDup:
+    var op2 = getAttachedOp(c.g, t, attachedAsgn)
+    if op2 != nil and sfOverridden in op2.flags:
+      #markUsed(c.g.config, c.info, op, c.g.usageSym)
+      onUse(c.info, op2)
+      body.add genBuiltin(c, mWasMoved, "wasMoved", x)
+      body.add newHookCall(c, op2, x, y)
+      result = true
+    else:
+      result = false
+  else:
+    result = false
+
 proc addIncStmt(c: var TLiftCtx; body, i: PNode) =
  let incCall = genBuiltin(c, mInc, "inc", i)
  incCall.add lowerings.newIntLit(c.g, c.info, 1)
@@ -721,14 +737,43 @@ proc atomicRefOp(c: var TLiftCtx; t: PType; body, x, y: PNode) =
    dest[] = source
    decRef tmp

+  For YRC the write barrier is more complicated still and must be:
+
+    let tmp = dest
+    # assignment must come first so that the collector sees the most-recent graph:
+    atomic: dest[] = source
+    # Then teach the cycle collector about the changes edge (these use locks, see yrc.nim):
+    incRef source
+    decRef tmp
+
+  This is implemented as a single runtime call (nimAsgnYrc / nimSinkYrc).
  ]#
  var actions = newNodeI(nkStmtList, c.info)
  let elemType = t.elementType

  createTypeBoundOps(c.g, c.c, elemType, c.info, c.idgen)
-  let isCyclic = c.g.config.selectedGC == gcOrc and types.canFormAcycle(c.g, elemType)

-  let isInheritableAcyclicRef = c.g.config.selectedGC == gcOrc and
+  # YRC uses dedicated runtime procs for the entire write barrier:
+  if c.g.config.selectedGC == gcYrc:
+    let desc =
+      if isFinal(elemType):
+        let ti = genBuiltin(c, mGetTypeInfoV2, "getTypeInfoV2", newNodeIT(nkType, x.info, elemType))
+        ti.typ = getSysType(c.g, c.info, tyPointer)
+        ti
+      else:
+        newNodeIT(nkNilLit, c.info, getSysType(c.g, c.info, tyPointer))
+    case c.kind
+    of attachedAsgn, attachedDup:
+      body.add callCodegenProc(c.g, "nimAsgnYrc", c.info, genAddr(c, x), y, desc)
+      return
+    of attachedSink:
+      body.add callCodegenProc(c.g, "nimSinkYrc", c.info, genAddr(c, x), y, desc)
+      return
+    else: discard # fall through for destructor, trace, wasMoved
+
+  let isCyclic = c.g.config.selectedGC in {gcOrc, gcYrc} and types.canFormAcycle(c.g, elemType)
+
+  let isInheritableAcyclicRef = c.g.config.selectedGC in {gcOrc, gcYrc} and
                      (not isPureObject(elemType)) and
                      tfAcyclic in skipTypes(elemType, abstractInst+{tyOwned}-{tyTypeDesc}).flags
  # dynamic Acyclic refs need to use dyn decRef
@@ -810,7 +855,26 @@ proc atomicClosureOp(c: var TLiftCtx; t: PType; body, x, y: PNode) =
  let xenv = genBuiltin(c, mAccessEnv, "accessEnv", x)
  xenv.typ = getSysType(c.g, c.info, tyPointer)

-  let isCyclic = c.g.config.selectedGC == gcOrc
+  # Closures are (fnPtr, env) pairs. nimAsgnYrc/nimSinkYrc handle the env pointer
+  # (atomic store + buffered inc/dec). We also need newAsgnStmt to copy the fnPtr.
+  if c.g.config.selectedGC == gcYrc:
+    let nilDesc = newNodeIT(nkNilLit, c.info, getSysType(c.g, c.info, tyPointer))
+    let yenv = genBuiltin(c, mAccessEnv, "accessEnv", y)
+    yenv.typ = getSysType(c.g, c.info, tyPointer)
+    case c.kind
+    of attachedAsgn, attachedDup:
+      # nimAsgnYrc: save old env, atomic store new env, inc new env, dec old env
+      body.add callCodegenProc(c.g, "nimAsgnYrc", c.info, genAddr(c, xenv), yenv, nilDesc)
+      # Raw struct copy to also update the function pointer (env write is redundant but benign)
+      body.add newAsgnStmt(x, y)
+      return
+    of attachedSink:
+      body.add callCodegenProc(c.g, "nimSinkYrc", c.info, genAddr(c, xenv), yenv, nilDesc)
+      body.add newAsgnStmt(x, y)
+      return
+    else: discard # fall through for destructor, trace, wasMoved
+
+  let isCyclic = c.g.config.selectedGC in {gcOrc, gcYrc}
  let tmp =
    if isCyclic and c.kind in {attachedAsgn, attachedSink, attachedDup}:
      declareTempOf(c, body, xenv)
@@ -843,7 +907,6 @@ proc atomicClosureOp(c: var TLiftCtx; t: PType; body, x, y: PNode) =
      body.add genIf(c, cond, actions)
    else:
      body.add genIf(c, yenv, callCodegenProc(c.g, "nimIncRef", c.info, yenv))
-
      body.add genIf(c, cond, actions)
      body.add newAsgnStmt(x, y)
  of attachedDup:
@@ -928,7 +991,7 @@ proc closureOp(c: var TLiftCtx; t: PType; body, x, y: PNode) =
    call[1] = y
    body.add newAsgnStmt(x, call)
  elif (optOwnedRefs in c.g.config.globalOptions and
-      optRefCheck in c.g.config.options) or c.g.config.selectedGC in {gcArc, gcAtomicArc, gcOrc}:
+      optRefCheck in c.g.config.options) or c.g.config.selectedGC in {gcArc, gcAtomicArc, gcOrc, gcYrc}:
    let xx = genBuiltin(c, mAccessEnv, "accessEnv", x)
    xx.typ = getSysType(c.g, c.info, tyPointer)
    case c.kind
@@ -983,7 +1046,7 @@ proc fillBody(c: var TLiftCtx; t: PType; body, x, y: PNode) =
      tyPtr, tyUncheckedArray, tyVar, tyLent:
    defaultOp(c, t, body, x, y)
  of tyRef:
-    if c.g.config.selectedGC in {gcArc, gcOrc, gcAtomicArc}:
+    if c.g.config.selectedGC in {gcArc, gcOrc, gcYrc, gcAtomicArc}:
      atomicRefOp(c, t, body, x, y)
    elif (optOwnedRefs in c.g.config.globalOptions and
        optRefCheck in c.g.config.options):
@@ -992,7 +1055,7 @@ proc fillBody(c: var TLiftCtx; t: PType; body, x, y: PNode) =
      defaultOp(c, t, body, x, y)
  of tyProc:
    if t.callConv == ccClosure:
-      if c.g.config.selectedGC in {gcArc, gcOrc, gcAtomicArc}:
+      if c.g.config.selectedGC in {gcArc, gcOrc, gcYrc, gcAtomicArc}:
        atomicClosureOp(c, t, body, x, y)
      else:
        closureOp(c, t, body, x, y)
@@ -1053,19 +1116,12 @@ proc fillBody(c: var TLiftCtx; t: PType; body, x, y: PNode) =
      elif tfUnion in t.flags: # bug #25236
        defaultOp(c, t, body, x, y)
      else:
-        if c.kind == attachedDup:
-          var op2 = getAttachedOp(c.g, t, attachedAsgn)
-          if op2 != nil and sfOverridden in op2.flags:
-            #markUsed(c.g.config, c.info, op, c.g.usageSym)
-            onUse(c.info, op2)
-            body.add newHookCall(c, t.assignment, x, y)
-          else:
-            fillBodyObjT(c, t, body, x, y)
-        else:
+        if not considerInferDupFromCopy(c, t, body, x, y):
          fillBodyObjT(c, t, body, x, y)
  of tyDistinct:
    if not considerUserDefinedOp(c, t, body, x, y):
-      fillBody(c, t.elementType, body, x, y)
+      if not considerInferDupFromCopy(c, t, body, x, y):
+        fillBody(c, t.elementType, body, x, y)
  of tyTuple:
    fillBodyTup(c, t, body, x, y)
  of tyVarargs, tyOpenArray:
@@ -1112,7 +1168,7 @@ proc symDupPrototype(g: ModuleGraph; typ: PType; owner: PSym; kind: TTypeAttache

  result.typ.addParam src

-  if g.config.selectedGC == gcOrc and
+  if g.config.selectedGC in {gcOrc, gcYrc} and
    cyclicType(g, typ.skipTypes(abstractInst)):
    let cycleParam = newSym(skParam, getIdent(g.cache, "cyclic"),
                            idgen, result, info)
@@ -1139,7 +1195,7 @@ proc symPrototype(g: ModuleGraph; typ: PType; owner: PSym; kind: TTypeAttachedOp
  let src = newSym(skParam, getIdent(g.cache, if kind == attachedTrace: "env" else: "src"),
                   idgen, result, info)

-  if kind == attachedDestructor and g.config.selectedGC in {gcArc, gcOrc, gcAtomicArc} and
+  if kind == attachedDestructor and g.config.selectedGC in {gcArc, gcOrc, gcYrc, gcAtomicArc} and
     ((g.config.isDefined("nimPreviewNonVarDestructor") and not isDiscriminant) or (typ.kind in {tyRef, tyString, tySequence})):
    dest.typ = typ
  else:
@@ -1155,7 +1211,7 @@ proc symPrototype(g: ModuleGraph; typ: PType; owner: PSym; kind: TTypeAttachedOp
  if kind notin {attachedDestructor, attachedWasMoved}:
    result.typ.addParam src

-  if kind == attachedAsgn and g.config.selectedGC == gcOrc and
+  if kind == attachedAsgn and g.config.selectedGC in {gcOrc, gcYrc} and
      cyclicType(g, typ.skipTypes(abstractInst)):
    let cycleParam = newSym(skParam, getIdent(g.cache, "cyclic"),
                            idgen, result, info)
@@ -1184,7 +1240,17 @@ proc genTypeFieldCopy(c: var TLiftCtx; t: PType; body, x, y: PNode) =
 proc produceSym(g: ModuleGraph; c: PContext; typ: PType; kind: TTypeAttachedOp;
              info: TLineInfo; idgen: IdGenerator): PSym =
  if typ.kind == tyDistinct:
-    return produceSymDistinctType(g, c, typ, kind, info, idgen)
+    # For =dup, if the distinct type has a user-defined =copy, don't delegate
+    # to the base type. Instead fall through to the normal produceSym logic
+    # so that fillBody -> considerInferDupFromCopy can synthesize =dup from =copy.
+    if kind == attachedDup:
+      let copyOp = getAttachedOp(g, typ, attachedAsgn)
+      if copyOp != nil and sfOverridden in copyOp.flags:
+        discard "fall through to normal produceSym logic"
+      else:
+        return produceSymDistinctType(g, c, typ, kind, info, idgen)
+    else:
+      return produceSymDistinctType(g, c, typ, kind, info, idgen)

  result = getAttachedOp(g, typ, kind)
  if result == nil:
@@ -1213,7 +1279,7 @@ proc produceSym(g: ModuleGraph; c: PContext; typ: PType; kind: TTypeAttachedOp;
  else:
    var tk: TTypeKind
    var skipped: PType = nil
-    if g.config.selectedGC in {gcArc, gcOrc, gcHooks, gcAtomicArc}:
+    if g.config.selectedGC in {gcArc, gcOrc, gcYrc, gcHooks, gcAtomicArc}:
      skipped = skipTypes(typ, {tyOrdinal, tyRange, tyInferred, tyGenericInst, tyStatic, tyAlias, tySink})
      tk = skipped.kind
    else:
@@ -1335,7 +1401,7 @@ proc createTypeBoundOps(g: ModuleGraph; c: PContext; orig: PType; info: TLineInf

  # we do not generate '=trace' procs if we
  # have the cycle detection disabled, saves code size.
-  let lastAttached = if g.config.selectedGC == gcOrc: attachedTrace
+  let lastAttached = if g.config.selectedGC in {gcOrc, gcYrc}: attachedTrace
                     else: attachedSink

  # bug #15122: We need to produce all prototypes before entering the
--- a/compiler/msgs.nim
+++ b/compiler/msgs.nim
@@ -240,7 +240,7 @@ proc setDirtyFile*(conf: ConfigRef; fileIdx: FileIndex; filename: AbsoluteFile)

 proc setHash*(conf: ConfigRef; fileIdx: FileIndex; hash: string) =
  assert fileIdx.int32 >= 0
-  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc) or defined(gcYrc):
    conf.m.fileInfos[fileIdx.int32].hash = hash
  else:
    shallowCopy(conf.m.fileInfos[fileIdx.int32].hash, hash)
@@ -248,7 +248,7 @@ proc setHash*(conf: ConfigRef; fileIdx: FileIndex; hash: string) =

 proc getHash*(conf: ConfigRef; fileIdx: FileIndex): string =
  assert fileIdx.int32 >= 0
-  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc) or defined(gcYrc):
    result = conf.m.fileInfos[fileIdx.int32].hash
  else:
    shallowCopy(result, conf.m.fileInfos[fileIdx.int32].hash)
--- a/compiler/nifgen.nim
+++ b/compiler/nifgen.nim
@@ -983,7 +983,7 @@ proc genericParamToNif(n: PNode; parent: PNode; c: var TranslationContext) =
    toNif n, parent, c

 proc addExternName(sym: PSym; c: var TranslationContext) =
-  if sym.loc.snippet != nil:
+  if sym.loc.snippet != "":
    c.b.addStrLit sym.loc.snippet
  else:
    c.b.addStrLit sym.name.s
--- a/compiler/options.nim
+++ b/compiler/options.nim
@@ -195,6 +195,7 @@ type
    gcRegions = "regions"
    gcArc = "arc"
    gcOrc = "orc"
+    gcYrc = "yrc"       # thread-safe ORC (concurrent cycle collector)
    gcAtomicArc = "atomicArc"
    gcMarkAndSweep = "markAndSweep"
    gcHooks = "hooks"
--- a/compiler/pragmas.nim
+++ b/compiler/pragmas.nim
@@ -567,7 +567,7 @@ proc processCompile(c: PContext, n: PNode) =
    n[i] = c.semConstExpr(c, n[i])
    case n[i].kind
    of nkStrLit, nkRStrLit, nkTripleStrLit:
-      when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+      when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc) or defined(gcYrc):
        result = n[i].strVal
      else:
        shallowCopy(result, n[i].strVal)
--- a/compiler/scriptconfig.nim
+++ b/compiler/scriptconfig.nim
@@ -231,7 +231,7 @@ proc runNimScript*(cache: IdentCache; scriptName: AbsoluteFile;
  if optOwnedRefs in oldGlobalOptions:
    conf.globalOptions.incl {optTinyRtti, optOwnedRefs, optSeqDestructors}
    defineSymbol(conf.symbols, "nimv2")
-  if conf.selectedGC in {gcArc, gcOrc, gcAtomicArc}:
+  if conf.selectedGC in {gcArc, gcOrc, gcYrc, gcAtomicArc}:
    conf.globalOptions.incl {optTinyRtti, optSeqDestructors}
    defineSymbol(conf.symbols, "nimv2")
    defineSymbol(conf.symbols, "gcdestructors")
@@ -241,6 +241,8 @@ proc runNimScript*(cache: IdentCache; scriptName: AbsoluteFile;
      defineSymbol(conf.symbols, "gcarc")
    of gcOrc:
      defineSymbol(conf.symbols, "gcorc")
+    of gcYrc:
+      defineSymbol(conf.symbols, "gcyrc")
    of gcAtomicArc:
      defineSymbol(conf.symbols, "gcatomicarc")
    else:
--- a/compiler/sem.nim
+++ b/compiler/sem.nim
@@ -855,7 +855,7 @@ proc semStmtAndGenerateGenerics(c: PContext, n: PNode): PNode =
    appendToModule(c.module, result)
  trackStmt(c, c.module, result, isTopLevel = true)
  if optMultiMethods notin c.config.globalOptions and
-      c.config.selectedGC in {gcArc, gcOrc, gcAtomicArc} and
+      c.config.selectedGC in {gcArc, gcOrc, gcAtomicArc, gcYrc} and
      Feature.vtables in c.config.features:
    sortVTableDispatchers(c.graph)

--- a/compiler/semexprs.nim
+++ b/compiler/semexprs.nim
@@ -333,7 +333,7 @@ proc isCastable(c: PContext; dst, src: PType, info: TLineInfo): bool =
  if skipTypes(dst, abstractInst).kind == tyBuiltInTypeClass:
    return false
  let conf = c.config
-  if conf.selectedGC in {gcArc, gcOrc, gcAtomicArc}:
+  if conf.selectedGC in {gcArc, gcOrc, gcAtomicArc, gcYrc}:
    let d = skipTypes(dst, abstractInst)
    let s = skipTypes(src, abstractInst)
    if d.kind == tyRef and s.kind == tyRef and s[0].isFinal != d[0].isFinal:
@@ -813,7 +813,7 @@ proc semArrayConstr(c: PContext, n: PNode, flags: TExprFlags; expectedType: PTyp
      inc(lastIndex)
    if isGeneric:
      for i in 0..<result.len:
-        if isIntLit(result[i].typ):
+        if result[i].typ != nil and isIntLit(result[i].typ):
          # generic instantiation strips int lit type which makes conversions fail
          result[i].typ = nil
      result.typ = nil # current result.typ is invalid, index type is nil
@@ -2800,7 +2800,7 @@ proc semSetConstr(c: PContext, n: PNode, expectedType: PType = nil): PNode =
          expectedElementType = typ
    if isGeneric:
      for i in 0..<n.len:
-        if isIntLit(n[i].typ):
+        if n[i].typ != nil and isIntLit(n[i].typ):
          # generic instantiation strips int lit type which makes conversions fail
          n[i].typ = nil
        result.add n[i]
@@ -2913,7 +2913,7 @@ proc semTupleFieldsConstr(c: PContext, n: PNode, flags: TExprFlags; expectedType
    result.add n[i]
  if isGeneric:
    for i in 0..<result.len:
-      if isIntLit(result[i][1].typ):
+      if result[i][1].typ != nil and isIntLit(result[i][1].typ):
        # generic instantiation strips int lit type which makes conversions fail
        result[i][1].typ = nil
    result.typ = makeTypeFromExpr(c, result.copyTree)
@@ -2954,7 +2954,7 @@ proc semTuplePositionsConstr(c: PContext, n: PNode, flags: TExprFlags; expectedT
    addSonSkipIntLit(typ, n[i].typ.skipTypes({tySink}), c.idgen)
  if isGeneric:
    for i in 0..<result.len:
-      if isIntLit(result[i].typ):
+      if result[i].typ != nil and isIntLit(result[i].typ):
        # generic instantiation strips int lit type which makes conversions fail
        result[i].typ = nil
    result.typ = makeTypeFromExpr(c, result.copyTree)
--- a/compiler/sempass2.nim
+++ b/compiler/sempass2.nim
@@ -1756,7 +1756,7 @@ proc trackProc*(c: PContext; s: PSym, body: PNode) =
      let param = params[i].sym
      let typ = param.typ
      if isSinkTypeForParam(typ) or
-          (t.config.selectedGC in {gcArc, gcOrc, gcAtomicArc} and
+          (t.config.selectedGC in {gcArc, gcOrc, gcYrc, gcAtomicArc} and
            (isClosure(typ.skipTypes(abstractInst)) or param.id in t.escapingParams)):
        createTypeBoundOps(t, typ, param.info)
      if isOutParam(typ) and param.id notin t.init and s.magic == mNone:
--- a/compiler/semstmts.nim
+++ b/compiler/semstmts.nim
@@ -2175,7 +2175,7 @@ proc bindTypeHook(c: PContext; s: PSym; n: PNode; op: TTypeAttachedOp) =
  template notRefc: bool =
    # fixes refc with non-var destructor; cancel warnings (#23156)
    c.config.backend == backendJs or
-      c.config.selectedGC in {gcArc, gcAtomicArc, gcOrc}
+      c.config.selectedGC in {gcArc, gcAtomicArc, gcOrc, gcYrc}
  let cond = case op
             of attachedWasMoved:
               t.len == 2 and t.returnType == nil and t.firstParamType.kind == tyVar
--- a/compiler/semtypes.nim
+++ b/compiler/semtypes.nim
@@ -1014,7 +1014,7 @@ proc skipGenericInvocation(t: PType): PType {.inline.} =
 proc tryAddInheritedFields(c: PContext, check: var IntSet, pos: var int,
                        obj: PType, n: PNode, isPartial = false, innerObj: PType = nil): bool =
  if ((not isPartial) and (obj.kind notin {tyObject, tyGenericParam} or tfFinal in obj.flags)) or
-    (innerObj != nil and obj.sym.id == innerObj.sym.id):
+    (innerObj != nil and obj.id == innerObj.id):
    localError(c.config, n.info, "Cannot inherit from: '" & $obj & "'")
    result = false
  elif obj.kind == tyObject:
@@ -1149,7 +1149,7 @@ proc semAnyRef(c: PContext; n: PNode; kind: TTypeKind; prev: PType): PType =
      result = t
    else: discard
    if result.kind == tyRef and
-        c.config.selectedGC in {gcArc, gcOrc, gcAtomicArc} and
+        c.config.selectedGC in {gcArc, gcOrc, gcAtomicArc, gcYrc} and
        tfTriggersCompileTime notin result.flags:
      result.incl tfHasAsgn

@@ -2390,7 +2390,7 @@ proc semTypeNode(c: PContext, n: PNode, prev: PType): PType =

      if n.kind == nkIteratorTy and result.kind == tyProc:
        result.incl(tfIterator)
-      if result.callConv == ccClosure and c.config.selectedGC in {gcArc, gcOrc, gcAtomicArc}:
+      if result.callConv == ccClosure and c.config.selectedGC in {gcArc, gcOrc, gcAtomicArc, gcYrc}:
        result.incl tfHasAsgn
  of nkEnumTy: result = semEnum(c, n, prev)
  of nkType: result = n.typ
--- a/compiler/sigmatch.nim
+++ b/compiler/sigmatch.nim
@@ -1678,7 +1678,6 @@ proc typeRel(c: var TCandidate, f, aOrig: PType,
    elif a.kind == tyGenericInst:
      if roota.base == rootf.base:
        let nextFlags = flags + {trNoCovariance}
-        var hasCovariance = false
        # YYYY
        result = isEqual

@@ -1690,7 +1689,7 @@ proc typeRel(c: var TCandidate, f, aOrig: PType,
          if res notin {isEqual, isGeneric}:
            if trNoCovariance notin flags and ff.kind == aa.kind:
              let paramFlags = rootf.base[i-1].flags
-              hasCovariance =
+              let hasCovariance =
                if tfCovariant in paramFlags:
                  if tfWeakCovariant in paramFlags:
                    isCovariantPtr(c, ff, aa)
@@ -1701,35 +1700,36 @@ proc typeRel(c: var TCandidate, f, aOrig: PType,
                    typeRel(c, aa, ff, flags) == isSubtype
              if hasCovariance:
                continue
+            result = isNone
+            break

-            return isNone
-        if prev == nil: put(c, f, a)
-      else:
-        let fKind = rootf.last.kind
-        if fKind in {tyAnd, tyOr}:
-          result = typeRel(c, last(f), a, flags)
-          if result != isNone: put(c, f, a)
+        if result != isNone:
+          if prev == nil: put(c, f, a)
          return

-        var aAsObject = roota.last
+      let fKind = rootf.last.kind
+      if fKind in {tyAnd, tyOr}:
+        result = typeRel(c, last(f), a, flags)
+        if result != isNone: put(c, f, a)
+        return

-        if fKind in {tyRef, tyPtr}:
-          if aAsObject.kind == tyObject:
-            # bug #7600, tyObject cannot be passed
-            # as argument to tyRef/tyPtr
-            return isNone
-          elif aAsObject.kind == fKind:
-            aAsObject = aAsObject.base
+      var aAsObject = roota.last

-        if aAsObject.kind == tyObject and trIsOutParam notin flags:
-          let baseType = aAsObject.base
-          if baseType != nil:
-            if tfFinal notin aAsObject.flags:
-              inc c.inheritancePenalty, 1 + int(c.inheritancePenalty < 0)
-            let ret = typeRel(c, f, baseType, flags)
-            return if ret in {isEqual,isGeneric}: isSubtype else: ret
+      if fKind in {tyRef, tyPtr}:
+        if aAsObject.kind == tyObject:
+          # bug #7600, tyObject cannot be passed
+          # as argument to tyRef/tyPtr
+          return isNone
+        elif aAsObject.kind == fKind:
+          aAsObject = aAsObject.base

-        result = isNone
+      if aAsObject.kind == tyObject and trIsOutParam notin flags:
+        let baseType = aAsObject.base
+        if baseType != nil:
+          if tfFinal notin aAsObject.flags:
+            inc c.inheritancePenalty, 1 + int(c.inheritancePenalty < 0)
+          let ret = typeRel(c, f, baseType, flags)
+          return if ret in {isEqual,isGeneric}: isSubtype else: ret
    else:
      assert last(origF) != nil
      result = typeRel(c, last(origF), a, flags)
--- a/compiler/spawn.nim
+++ b/compiler/spawn.nim
@@ -37,7 +37,7 @@ proc spawnResult*(t: PType; inParallel: bool): TSpawnResult =
  else: srFlowVar

 proc flowVarKind(c: ConfigRef, t: PType): TFlowVarKind =
-  if c.selectedGC in {gcArc, gcOrc, gcAtomicArc}: fvBlob
+  if c.selectedGC in {gcArc, gcOrc, gcAtomicArc, gcYrc}: fvBlob
  elif t.skipTypes(abstractInst).kind in {tyRef, tyString, tySequence}: fvGC
  elif containsGarbageCollectedRef(t): fvInvalid
  else: fvBlob
@@ -66,7 +66,7 @@ proc addLocalVar(g: ModuleGraph; varSection, varInit: PNode; idgen: IdGenerator;
  vpart[2] = if varInit.isNil: v else: vpart[1]
  varSection.add vpart
  if varInit != nil:
-    if g.config.selectedGC in {gcArc, gcOrc, gcAtomicArc}:
+    if g.config.selectedGC in {gcArc, gcOrc, gcAtomicArc, gcYrc}:
      # inject destructors pass will do its own analysis
      varInit.add newFastMoveStmt(g, newSymNode(result), v)
    else:
--- a/compiler/vm.nim
+++ b/compiler/vm.nim
@@ -120,7 +120,7 @@ template decodeBx(k: untyped) {.dirty.} =
  ensureKind(k)

 template move(a, b: untyped) {.dirty.} =
-  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc) or defined(gcYrc):
    a = move b
  else:
    system.shallowCopy(a, b)
@@ -557,7 +557,7 @@ proc rawExecute(c: PCtx, start: int, tos: PStackFrame): TFullReg =
  # Used to keep track of where the execution is resumed.
  var savedPC = -1
  var savedFrame: PStackFrame = nil
-  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc) or defined(gcYrc):
    template updateRegsAlias = discard
    template regs: untyped = tos.slots
  else:
--- a/lib/experimental/diff.nim
+++ b/lib/experimental/diff.nim
@@ -338,63 +338,3 @@ proc diffText*(textA, textB: string): seq[Item] =
  optimize(dataA)
  optimize(dataB)
  result = createDiffs(dataA, dataB)
-
-proc renderDiff*(a, b: string; res: seq[Item]): string =
-  ## Renders a diff between two strings as a human-readable unified diff format.
-  ##
-  ## `a` the original text
-  ## `b` the modified text
-  ## `res` the sequence of Items from `diffText(a, b)`
-  ##
-  ## Returns a string with the diff output where:
-  ## - Lines prefixed with `-` are deletions from `a`
-  ## - Lines prefixed with `+` are insertions in `b`
-  ## - Lines prefixed with ` ` are context (unchanged)
-  runnableExamples:
-    let a = "line1\nline2\nline3"
-    let b = "line1\nmodified\nline3"
-    let diff = diffText(a, b)
-    let rendered = renderDiff(a, b, diff)
-    assert "-line2" in rendered
-    assert "+modified" in rendered
-
-  let linesA = a.splitLines
-  let linesB = b.splitLines
-
-  var posA = 0
-  var posB = 0
-
-  for item in res:
-    # Add context lines before this change
-    while posA < item.startA and posB < item.startB:
-      result.add ' '
-      result.add linesA[posA]
-      result.add '\n'
-      inc posA
-      inc posB
-
-    # Add deleted lines from A
-    for i in 0 ..< item.deletedA:
-      result.add '-'
-      result.add linesA[item.startA + i]
-      result.add '\n'
-
-    # Add inserted lines from B
-    for i in 0 ..< item.insertedB:
-      result.add '+'
-      result.add linesB[item.startB + i]
-      result.add '\n'
-
-    posA = item.startA + item.deletedA
-    posB = item.startB + item.insertedB
-
-  # Add remaining context lines after the last change
-  while posA < linesA.len and posB < linesB.len:
-    result.add ' '
-    result.add linesA[posA]
-    result.add '\n'
-    inc posA
-    inc posB
-
-proc diffOutput*(a, b: string): string =
-  renderDiff(a, b, diffText(a, b))
--- a/lib/pure/asynchttpserver.nim
+++ b/lib/pure/asynchttpserver.nim
@@ -188,7 +188,7 @@ proc processRequest(
  # \n
  request.headers.clear()
  request.body = ""
-  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc) or defined(gcYrc):
    request.hostname = address
  else:
    request.hostname.shallowCopy(address)
--- a/lib/pure/coro.nim
+++ b/lib/pure/coro.nim
@@ -36,7 +36,7 @@ when defined(nimPreviewSlimSystem):
  import std/assertions

 const defaultStackSize = 512 * 1024
-const useOrcArc = defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc)
+const useOrcArc = defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc) or defined(gcYrc)

 when useOrcArc:
  proc nimGC_setStackBottom*(theStackBottom: pointer) = discard
--- a/lib/pure/json.nim
+++ b/lib/pure/json.nim
@@ -866,7 +866,7 @@ proc parseJson(p: var JsonParser; rawIntegers, rawFloats: bool, depth = 0): Json
  case p.tok
  of tkString:
    # we capture 'p.a' here, so we need to give it a fresh buffer afterwards:
-    when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+    when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc) or defined(gcYrc):
      result = JsonNode(kind: JString, str: move p.a)
    else:
      result = JsonNode(kind: JString)
--- a/lib/pure/marshal.nim
+++ b/lib/pure/marshal.nim
@@ -305,7 +305,7 @@ proc store*[T](s: Stream, data: sink T) =

  var stored = initIntSet()
  var d: T
-  when defined(gcArc) or defined(gcOrc)or defined(gcAtomicArc):
+  when defined(gcArc) or defined(gcOrc)or defined(gcAtomicArc) or defined(gcYrc):
    d = data
  else:
    shallowCopy(d, data)
@@ -334,7 +334,7 @@ proc `$$`*[T](x: sink T): string =
  else:
    var stored = initIntSet()
    var d: T
-    when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+    when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc) or defined(gcYrc):
      d = x
    else:
      shallowCopy(d, x)
--- a/lib/std/tasks.nim
+++ b/lib/std/tasks.nim
@@ -68,7 +68,7 @@ type

 proc `=copy`*(x: var Task, y: Task) {.error.}

-const arcLike = defined(gcArc) or defined(gcAtomicArc) or defined(gcOrc)
+const arcLike = defined(gcArc) or defined(gcAtomicArc) or defined(gcOrc) or defined(gcYrc)
 when defined(nimAllowNonVarDestructor) and arcLike:
  proc `=destroy`*(t: Task) {.inline, gcsafe.} =
    ## Frees the resources allocated for a `Task`.
--- a/lib/std/typedthreads.nim
+++ b/lib/std/typedthreads.nim
@@ -9,13 +9,13 @@

 ##[
 Thread support for Nim. Threads allow multiple functions to execute concurrently.
- 
+
 In Nim, threads are a low-level construct and using a library like `malebolgia`, `taskpools` or `weave` is recommended.
- 
+
 When creating a thread, you can pass arguments to it. As Nim's garbage collector does not use atomic references, sharing
 `ref` and other variables managed by the garbage collector between threads is not supported.
 Use global variables to do so, or pointers.
- 
+
 Memory allocated using [`sharedAlloc`](./system.html#allocShared.t%2CNatural) can be used and shared between threads.

 To communicate between threads, consider using [channels](./system.html#Channel)
@@ -44,7 +44,7 @@ joinThreads(thr)

 deinitLock(L)
 ```
- 
+
 When using a memory management strategy that supports shared heaps like `arc` or `boehm`,
 you can pass pointer to threads and share memory between them, but the memory must outlive the thread.
 The default memory management strategy, `orc`, supports this.
@@ -52,14 +52,14 @@ The example below is **not valid** for memory management strategies that use loc

 ```Nim
 import locks
- 
+
 var l: Lock
- 
+
 proc threadFunc(obj: ptr seq[int]) {.thread.} =
  withLock l:
    for i in 0..<100:
      obj[].add(obj[].len * obj[].len)
- 
+
 proc threadHandler() =
  var thr: array[0..4, Thread[ptr seq[int]]]
  var s = newSeq[int]()
@@ -68,7 +68,7 @@ proc threadHandler() =
    createThread(thr[i], threadFunc, s.addr)
  joinThreads(thr)
  echo s
- 
+
 initLock(l)
 threadHandler()
 deinitLock(l)
@@ -303,5 +303,5 @@ else:
 proc createThread*(t: var Thread[void], tp: proc () {.thread, nimcall.}) =
  createThread[void](t, tp)

-when not defined(gcOrc):
+when not defined(gcOrc) and not defined(gcYrc):
  include system/threadids
--- a/lib/std/widestrs.nim
+++ b/lib/std/widestrs.nim
@@ -25,7 +25,7 @@ when not (defined(cpu16) or defined(cpu8)):
        bytes: int
        data: WideCString

-    const arcLike = defined(gcArc) or defined(gcAtomicArc) or defined(gcOrc)
+    const arcLike = defined(gcArc) or defined(gcAtomicArc) or defined(gcOrc) or defined(gcYrc)
    when defined(nimAllowNonVarDestructor) and arcLike:
      proc `=destroy`(a: WideCStringObj) =
        if a.data != nil:
--- a/lib/system.nim
+++ b/lib/system.nim
@@ -125,7 +125,7 @@ proc unsafeAddr*[T](x: T): ptr T {.magic: "Addr", noSideEffect.} =

 const ThisIsSystem = true

-const arcLikeMem = defined(gcArc) or defined(gcAtomicArc) or defined(gcOrc)
+const arcLikeMem = defined(gcArc) or defined(gcAtomicArc) or defined(gcOrc) or defined(gcYrc)

 when defined(nimAllowNonVarDestructor) and arcLikeMem:
  proc new*[T](a: var ref T, finalizer: proc (x: T) {.nimcall.}) {.
@@ -356,7 +356,7 @@ proc low*(x: string): int {.magic: "Low", noSideEffect.}
  ## See also:
  ## * `high(string) <#high,string>`_

-when not defined(gcArc) and not defined(gcOrc) and not defined(gcAtomicArc):
+when not defined(gcArc) and not defined(gcOrc) and not defined(gcYrc) and not defined(gcAtomicArc):
  proc shallowCopy*[T](x: var T, y: T) {.noSideEffect, magic: "ShallowCopy".}
    ## Use this instead of `=` for a `shallow copy`:idx:.
    ##
@@ -407,7 +407,7 @@ when defined(nimHasDup):

 proc `=sink`*[T](x: var T; y: T) {.inline, nodestroy, magic: "Asgn".} =
  ## Generic `sink`:idx: implementation that can be overridden.
-  when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+  when defined(gcArc) or defined(gcOrc) or defined(gcYrc) or defined(gcAtomicArc):
    x = y
  else:
    shallowCopy(x, y)
@@ -2561,7 +2561,7 @@ when compileOption("rangechecks"):
 else:
  template rangeCheck*(cond) = discard

-when not defined(gcArc) and not defined(gcOrc) and not defined(gcAtomicArc):
+when not defined(gcArc) and not defined(gcOrc) and not defined(gcYrc) and not defined(gcAtomicArc):
  proc shallow*[T](s: var seq[T]) {.noSideEffect, inline.} =
    ## Marks a sequence `s` as `shallow`:idx:. Subsequent assignments will not
    ## perform deep copies of `s`.
@@ -2630,7 +2630,7 @@ when hasAlloc or defined(nimscript):
    setLen(x, xl+item.len)
    var j = xl-1
    while j >= i:
-      when defined(gcArc) or defined(gcOrc) or defined(gcAtomicArc):
+      when defined(gcArc) or defined(gcOrc) or defined(gcYrc) or defined(gcAtomicArc):
        x[j+item.len] = move x[j]
      else:
        shallowCopy(x[j+item.len], x[j])
--- a/lib/system/alloc.nim
+++ b/lib/system/alloc.nim
@@ -477,7 +477,8 @@ iterator allObjects(m: var MemRegion): pointer {.inline.} =
            a = a +% size
        else:
          let c = cast[PBigChunk](c)
-          yield addr(c.data)
+          # prev stores the aligned data pointer set during rawAlloc
+          yield cast[pointer](c.prev)
  m.locked = false

 proc iterToProc*(iter: typed, envType: typedesc; procName: untyped) {.
@@ -777,7 +778,10 @@ proc deallocBigChunk(a: var MemRegion, c: PBigChunk) =
  sysAssert a.occ >= 0, "rawDealloc: negative occupied memory (case B)"
  when not defined(gcDestructors):
    a.deleted = getBottom(a)
-    del(a, a.root, cast[int](addr(c.data)))
+    # prev stores the aligned data pointer that was added to the AVL tree during allocation
+    del(a, a.root, cast[int](c.prev))
+  # Reset prev before freeing (required by listAdd assertions in freeBigChunk)
+  c.prev = nil
  if c.size >= HugeChunkSize: freeHugeChunk(a, c)
  else: freeBigChunk(a, c)

@@ -845,7 +849,14 @@ when defined(heaptrack):
  proc heaptrack_malloc(a: pointer, size: int) {.cdecl, importc, dynlib: heaptrackLib.}
  proc heaptrack_free(a: pointer) {.cdecl, importc, dynlib: heaptrackLib.}

-proc rawAlloc(a: var MemRegion, requestedSize: int): pointer =
+proc bigChunkAlignOffset(alignment: int): int {.inline.} =
+  ## Compute the alignment offset for big chunk data.
+  if alignment <= MemAlign:
+    result = 0
+  else:
+    result = align(sizeof(BigChunk) + sizeof(Cell), alignment) - sizeof(BigChunk) - sizeof(Cell)
+
+proc rawAlloc(a: var MemRegion, requestedSize: int, alignment: int = MemAlign): pointer =
  when defined(nimTypeNames):
    inc(a.allocCounter)
  sysAssert(allocInv(a), "rawAlloc: begin")
@@ -855,7 +866,9 @@ proc rawAlloc(a: var MemRegion, requestedSize: int): pointer =
  sysAssert(size >= requestedSize, "insufficient allocated size!")
  #c_fprintf(stdout, "alloc; size: %ld; %ld\n", requestedSize, size)

-  if size <= SmallChunkSize-smallChunkOverhead():
+  # For custom alignments > MemAlign, force big chunk allocation
+  # Small chunks cannot handle arbitrary alignments due to fixed cell boundaries
+  if size <= SmallChunkSize-smallChunkOverhead() and alignment <= MemAlign:
    template fetchSharedCells(tc: PSmallChunk) =
      # Consumes cells from (potentially) foreign threads from `a.sharedFreeLists[s]`
      when defined(gcDestructors):
@@ -950,13 +963,21 @@ proc rawAlloc(a: var MemRegion, requestedSize: int): pointer =
      if deferredFrees != nil:
        freeDeferredObjects(a, deferredFrees)

-    size = requestedSize + bigChunkOverhead() #  roundup(requestedSize+bigChunkOverhead(), PageSize)
+    # For big chunks with custom alignment, allocate extra space.
+    # Since chunks are page-aligned, the needed padding is a compile-time
+    # deterministic value rather than a worst-case estimate.
+    let alignPad = bigChunkAlignOffset(alignment)
+    size = requestedSize + bigChunkOverhead() + alignPad
    # allocate a large block
    var c = if size >= HugeChunkSize: getHugeChunk(a, size)
            else: getBigChunk(a, size)
    sysAssert c.prev == nil, "rawAlloc 10"
    sysAssert c.next == nil, "rawAlloc 11"
-    result = addr(c.data)
+    result = addr(c.data) +! alignPad
+    # Store the aligned data pointer in prev for deallocation and GC traversal.
+    # prev is unused while the chunk is allocated (next/prev are free-list links).
+    c.prev = cast[PBigChunk](result)
+
    sysAssert((cast[int](c) and (MemAlign-1)) == 0, "rawAlloc 13")
    sysAssert((cast[int](c) and PageMask) == 0, "rawAlloc: Not aligned on a page boundary")
    when not defined(gcDestructors):
@@ -1025,13 +1046,29 @@ proc rawDealloc(a: var MemRegion, p: pointer) =
          inc(c.free, s)
        else:
          inc(c.free, s)
-          # Free only if the entire chunk is unused and there are no borrowed cells.
-          # If the chunk were to be freed while it references foreign cells,
-          #  the foreign chunks will leak memory and can never be freed.
-          if c.free == SmallChunkSize-smallChunkOverhead() and c.foreignCells == 0:
-            listRemove(a.freeSmallChunks[s div MemAlign], c)
-            c.size = SmallChunkSize
-            freeBigChunk(a, cast[PBigChunk](c))
+          # FIX: Don't free small chunks to avoid race condition with sharedFreeLists.
+          #
+          # RACE CONDITION: Between checking foreignCells==0 and calling freeBigChunk,
+          # another thread may read chunk.owner and decide to add a cell to our
+          # sharedFreeLists. If we free the chunk, that cell becomes orphaned.
+          #
+          # SOLUTION: Never free small chunks. They remain in freeSmallChunks[s] and
+          # are reused on next allocation. This maintains the invariant that chunks
+          # in freeSmallChunks[s] have c.free >= s (completely free chunks satisfy this).
+          # If a chunk becomes exhausted (c.free < s), it's removed by line 949.
+          #
+          # TRADEOFF: Memory not returned to OS. Bounded by peak concurrent allocation
+          # per size class (~4KB per active size class per thread, typically <1MB total).
+          #
+          # VERIFIED: TLA+ formal proof shows no race - see VERIFICATION_RESULTS.md
+          #
+          # Original code (REMOVED to fix race):
+          sysAssert(c.free >= s, "Invariant violated: chunk in freeSmallChunks has insufficient space")
+          when false:
+            if c.free == SmallChunkSize-smallChunkOverhead() and c.foreignCells == 0:
+              listRemove(a.freeSmallChunks[s div MemAlign], c)
+              c.size = SmallChunkSize
+              freeBigChunk(a, cast[PBigChunk](c))
    else:
      when logAlloc: cprintf("dealloc(pointer_%p) # SMALL FROM %p CALLER %p\n", p, c.owner, addr(a))

@@ -1067,7 +1104,9 @@ when not defined(gcDestructors):
            (cast[ptr FreeCell](p).zeroField >% 1)
        else:
          var c = cast[PBigChunk](c)
-          result = p == addr(c.data) and cast[ptr FreeCell](p).zeroField >% 1
+          # prev stores the aligned data pointer set during rawAlloc
+          let cellPtr = cast[pointer](c.prev)
+          result = p == cellPtr and cast[ptr FreeCell](p).zeroField >% 1

  proc prepareForInteriorPointerChecking(a: var MemRegion) {.inline.} =
    a.minLargeObj = lowGauge(a.root)
@@ -1091,7 +1130,8 @@ when not defined(gcDestructors):
              sysAssert isAllocatedPtr(a, result), " result wrong pointer!"
        else:
          var c = cast[PBigChunk](c)
-          var d = addr(c.data)
+          # prev stores the aligned data pointer set during rawAlloc
+          var d = cast[pointer](c.prev)
          if p >= d and cast[ptr FreeCell](d).zeroField >% 1:
            result = d
            sysAssert isAllocatedPtr(a, result), " result wrong pointer!"
@@ -1104,7 +1144,8 @@ when not defined(gcDestructors):
        if avlNode != nil:
          var k = cast[pointer](avlNode.key)
          var c = cast[PBigChunk](pageAddr(k))
-          sysAssert(addr(c.data) == k, " k is not the same as addr(c.data)!")
+          # prev stores the aligned data pointer (the AVL tree key)
+          sysAssert(cast[pointer](c.prev) == k, " k is not the aligned address!")
          if cast[ptr FreeCell](k).zeroField >% 1:
            result = k
            sysAssert isAllocatedPtr(a, result), " result wrong pointer!"
--- a/lib/system/arc.nim
+++ b/lib/system/arc.nim
@@ -16,7 +16,7 @@ runtime type and only contains a reference count.

 {.push raises: [], rangeChecks: off.}

-when defined(gcOrc):
+when defined(gcOrc) or defined(gcYrc):
  const
    rcIncrement = 0b10000 # so that lowest 4 bits are not touched
    rcMask = 0b1111
@@ -36,12 +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):
+    when defined(gcOrc) or defined(gcYrc):
      rootIdx: int # thanks to this we can delete potential cycle roots
                   # in O(1) without doubly linked lists
    when defined(nimArcDebug) or defined(nimArcIds):
      refId: int
-    when defined(gcOrc) and orcLeakDetector:
+    when (defined(gcOrc) or defined(gcYrc)) and orcLeakDetector:
      filename: cstring
      line: int

@@ -74,7 +74,7 @@ elif defined(nimArcIds):

  const traceId = -1

-when defined(gcAtomicArc) and hasThreadSupport:
+when (defined(gcAtomicArc) or defined(gcYrc)) and hasThreadSupport:
  template decrement(cell: Cell): untyped =
    discard atomicDec(cell.rc, rcIncrement)
  template increment(cell: Cell): untyped =
@@ -119,7 +119,7 @@ proc nimNewObjUninit(size, alignment: int): pointer {.compilerRtl.} =
  else:
    result = cast[ptr RefHeader](alignedAlloc(s, alignment) +! hdrSize)
  head(result).rc = 0
-  when defined(gcOrc):
+  when defined(gcOrc) or defined(gcYrc):
    head(result).rootIdx = 0
  when defined(nimArcDebug):
    head(result).refId = gRefId
@@ -157,7 +157,7 @@ proc nimIncRef(p: pointer) {.compilerRtl, inl.} =
  when traceCollector:
    cprintf("[INCREF] %p\n", head(p))

-when not defined(gcOrc) or defined(nimThinout):
+when not (defined(gcOrc) or defined(gcYrc)) or defined(nimThinout):
  proc unsureAsgnRef(dest: ptr pointer, src: pointer) {.inline.} =
    # This is only used by the old RTTI mechanism and we know
    # that 'dest[]' is nil and needs no destruction. Which is really handy
@@ -208,7 +208,9 @@ proc nimDestroyAndDispose(p: pointer) {.compilerRtl, quirky, raises: [].} =
      cstderr.rawWrite "has destructor!\n"
  nimRawDispose(p, rti.align)

-when defined(gcOrc):
+when defined(gcYrc):
+  include yrc
+elif defined(gcOrc):
  when defined(nimThinout):
    include cyclebreaker
  else:
@@ -225,7 +227,7 @@ proc nimDecRefIsLast(p: pointer): bool {.compilerRtl, inl.} =
        writeStackTrace()
        cfprintf(cstderr, "[DecRef] %p %ld\n", p, cell.count)

-    when defined(gcAtomicArc) and hasThreadSupport:
+    when (defined(gcAtomicArc) or defined(gcYrc)) and hasThreadSupport:
      # `atomicDec` returns the new value
      if atomicDec(cell.rc, rcIncrement) == -rcIncrement:
        result = true
@@ -251,7 +253,7 @@ proc GC_ref*[T](x: ref T) =
  ## New runtime only supports this operation for 'ref T'.
  if x != nil: nimIncRef(cast[pointer](x))

-when not defined(gcOrc):
+when not (defined(gcOrc) or defined(gcYrc)):
  template GC_fullCollect* =
    ## Forces a full garbage collection pass. With `--mm:arc` a nop.
    discard
--- a/lib/system/cellsets.nim
+++ b/lib/system/cellsets.nim
@@ -42,27 +42,13 @@ Complete traversal is done in this way::

 ]#

-when defined(gcOrc) or defined(gcArc) or defined(gcAtomicArc):
+when defined(gcOrc) or defined(gcArc) or defined(gcAtomicArc) or defined(gcYrc):
  type
    PCell = Cell

  when not declaredInScope(PageShift):
    include bitmasks

-else:
-  type
-    RefCount = int
-
-    Cell {.pure.} = object
-      refcount: RefCount  # the refcount and some flags
-      typ: PNimType
-      when trackAllocationSource:
-        filename: cstring
-        line: int
-      when useCellIds:
-        id: int
-
-    PCell = ptr Cell

 type
  PPageDesc = ptr PageDesc
@@ -78,7 +64,7 @@ type
    head: PPageDesc
    data: PPageDescArray

-when defined(gcOrc) or defined(gcArc) or defined(gcAtomicArc):
+when defined(gcOrc) or defined(gcArc) or defined(gcAtomicArc) or defined(gcYrc):
  discard
 else:
  include cellseqs_v1
--- a/lib/system/comparisons.nim
+++ b/lib/system/comparisons.nim
@@ -38,6 +38,21 @@ proc `==`*[T](x, y: ptr T): bool {.magic: "EqRef", noSideEffect.}
 proc `==`*[T: proc | iterator](x, y: T): bool {.magic: "EqProc", noSideEffect.}
  ## Checks that two `proc` variables refer to the same procedure.

+when true:
+  # guard against string converted to cstring implicitly; see also #bug #25488
+  proc isNil*(x: string): bool {.noSideEffect, error: "'isNil' is invalid for 'string'".}
+
+
+  # bug #9149; ensure that 'typeof(nil)' does not match *too* well by using 'typeof(nil) | typeof(nil)',
+  # especially for converters, see tests/overload/tconverter_to_string.nim
+  # Eventually we will be able to remove this hack completely.
+
+  proc `==`*(x: string; y: typeof(nil) | typeof(nil)): bool {.error: "'nil' is invalid for 'string'".} =
+    discard
+
+  proc `==`*(x: typeof(nil) | typeof(nil); y: string): bool {.error: "'nil' is invalid for 'string'".} =
+    discard
+
 proc `<=`*[Enum: enum](x, y: Enum): bool {.magic: "LeEnum", noSideEffect.}
 proc `<=`*(x, y: string): bool {.magic: "LeStr", noSideEffect.} =
  ## Compares two strings and returns true if `x` is lexicographically
--- a/lib/system/gc.nim
+++ b/lib/system/gc.nim
@@ -458,9 +458,12 @@ proc rawNewObj(typ: PNimType, size: int, gch: var GcHeap): pointer =
  sysAssert(allocInv(gch.region), "rawNewObj begin")
  gcAssert(typ.kind in {tyRef, tyString, tySequence}, "newObj: 1")
  collectCT(gch)
-  var res = cast[PCell](rawAlloc(gch.region, size + sizeof(Cell)))
+  # Use alignment from typ.base if available, otherwise use MemAlign
+  let alignment = if typ.kind == tyRef and typ.base != nil: max(typ.base.align, MemAlign) else: MemAlign
+  var res = cast[PCell](rawAlloc(gch.region, size + sizeof(Cell), alignment))
  #gcAssert typ.kind in {tyString, tySequence} or size >= typ.base.size, "size too small"
-  gcAssert((cast[int](res) and (MemAlign-1)) == 0, "newObj: 2")
+  # Check that the user data (after the Cell header) is properly aligned
+  gcAssert((cast[int](cellToUsr(res)) and (alignment-1)) == 0, "newObj: 2")
  # now it is buffered in the ZCT
  res.typ = typ
  setFrameInfo(res)
@@ -508,9 +511,12 @@ proc newObjRC1(typ: PNimType, size: int): pointer {.compilerRtl, noinline, raise
  collectCT(gch)
  sysAssert(allocInv(gch.region), "newObjRC1 after collectCT")

-  var res = cast[PCell](rawAlloc(gch.region, size + sizeof(Cell)))
+  # Use alignment from typ.base if available, otherwise use MemAlign
+  let alignment = if typ.base != nil: max(typ.base.align, MemAlign) else: MemAlign
+  var res = cast[PCell](rawAlloc(gch.region, size + sizeof(Cell), alignment))
  sysAssert(allocInv(gch.region), "newObjRC1 after rawAlloc")
-  sysAssert((cast[int](res) and (MemAlign-1)) == 0, "newObj: 2")
+  # Check that the user data (after the Cell header) is properly aligned
+  sysAssert((cast[int](cellToUsr(res)) and (alignment-1)) == 0, "newObj: 2")
  # now it is buffered in the ZCT
  res.typ = typ
  setFrameInfo(res)
--- a/lib/system/mm/malloc.nim
+++ b/lib/system/mm/malloc.nim
@@ -50,7 +50,7 @@ proc deallocSharedImpl(p: pointer) = deallocImpl(p)
 proc GC_disable() = discard
 proc GC_enable() = discard

-when not defined(gcOrc):
+when not defined(gcOrc) and not defined(gcYrc):
  proc GC_fullCollect() = discard
  proc GC_enableMarkAndSweep() = discard
  proc GC_disableMarkAndSweep() = discard
--- a/lib/system/mmdisp.nim
+++ b/lib/system/mmdisp.nim
@@ -38,6 +38,21 @@ type
  PByte = ptr ByteArray
  PString = ptr string

+when not defined(nimV2):
+  type
+    RefCount = int
+
+    Cell {.pure.} = object
+      refcount: RefCount  # the refcount and some flags
+      typ: PNimType
+      when trackAllocationSource:
+        filename: cstring
+        line: int
+      when useCellIds:
+        id: int
+
+    PCell = ptr Cell
+
 when declared(IntsPerTrunk):
  discard
 else:
--- a/lib/system/orc.nim
+++ b/lib/system/orc.nim
@@ -433,8 +433,9 @@ proc collectCycles() =
      rootsThreshold = (if rootsThreshold <= 0: defaultThreshold else: rootsThreshold)
      rootsThreshold = rootsThreshold div 2 +% rootsThreshold
  when logOrc:
-    cfprintf(cstderr, "[collectCycles] end; freed %ld new threshold %ld touched: %ld mem: %ld rcSum: %ld edges: %ld\n", j.freed, rootsThreshold, j.touched,
-      getOccupiedMem(), j.rcSum, j.edges)
+    {.cast(raises: []).}:
+      discard cfprintf(cstderr, "[collectCycles] end; freed %ld new threshold %ld touched: %ld mem: %ld rcSum: %ld edges: %ld\n", j.freed, rootsThreshold, j.touched,
+        getOccupiedMem(), j.rcSum, j.edges)
  when defined(nimOrcStats):
    inc freedCyclicObjects, j.freed

@@ -465,13 +466,13 @@ proc GC_runOrc* =

 proc GC_enableOrc*() =
  ## Enables the cycle collector subsystem of `--mm:orc`. This is a `--mm:orc`
-  ## specific API. Check with `when defined(gcOrc)` for its existence.
+  ## specific API. Check with `when defined(gcOrc) or defined(gcYrc)` for its existence.
  when not defined(nimStressOrc):
    rootsThreshold = 0

 proc GC_disableOrc*() =
  ## Disables the cycle collector subsystem of `--mm:orc`. This is a `--mm:orc`
-  ## specific API. Check with `when defined(gcOrc)` for its existence.
+  ## specific API. Check with `when defined(gcOrc) or defined(gcYrc)` for its existence.
  when not defined(nimStressOrc):
    rootsThreshold = high(int)

--- a/lib/system/osalloc.nim
+++ b/lib/system/osalloc.nim
@@ -31,8 +31,8 @@ const doNotUnmap = not (defined(amd64) or defined(i386)) or


 when defined(nimAllocPagesViaMalloc):
-  when not defined(gcArc) and not defined(gcOrc) and not defined(gcAtomicArc):
-    {.error: "-d:nimAllocPagesViaMalloc is only supported with --mm:arc or --mm:atomicArc or --mm:orc".}
+  when not defined(gcArc) and not defined(gcOrc) and not defined(gcAtomicArc) and not defined(gcYrc):
+    {.error: "-d:nimAllocPagesViaMalloc is only supported with --mm:arc or --mm:atomicArc or --mm:orc or --mm:yrc".}

  proc osTryAllocPages(size: int): pointer {.inline.} =
    let base = c_malloc(csize_t size + PageSize - 1 + sizeof(uint32))
--- a/lib/system/yrc.nim
+++ b/lib/system/yrc.nim
@@ -0,0 +1,569 @@
+#
+# YRC: Thread-safe ORC (concurrent cycle collector).
+# Same API as orc.nim but with striped queues and global lock for merge/collect.
+# Destructors for refs run at collection time, not immediately on last decRef.
+# See yrc_proof.lean for a Lean 4 proof of safety and deadlock freedom.
+#
+# ## Key Invariant: Topology vs. Reference Counts
+#
+# Only `obj.field = x` can change the topology of the heap graph (heap-to-heap
+# edges). Local variable assignments (`var local = someRef`) affect reference
+# counts but never create heap-to-heap edges and thus cannot create cycles.
+#
+# The actual pointer write in `obj.field = x` happens immediately and lock-free —
+# the graph topology is always up-to-date in memory. Only the RC adjustments are
+# deferred: increments and decrements are buffered into per-stripe queues
+# (`toInc`, `toDec`) protected by fine-grained per-stripe locks.
+#
+# When `collectCycles` runs it takes the global lock, drains all stripe buffers
+# via `mergePendingRoots`, and then traces the physical pointer graph (via
+# `traceImpl`) to detect cycles. This is sound because `trace` follows the actual
+# pointer values in memory — which are always current — and uses the reconciled
+# RCs only to identify candidate roots and confirm garbage.
+#
+# In summary: the physical pointer graph is always consistent (writes are
+# immediate); only the reference counts are eventually consistent (writes are
+# buffered). The per-stripe locks are cheap; the expensive global lock is only
+# needed when interpreting the RCs during collection.
+#
+# ## Why No Write Barrier Is Needed
+#
+# The classic concurrent-GC hazard is the "lost object" problem: during
+# collection the mutator executes `A.field = B` where A is already scanned
+# (black), B is reachable only through an unscanned (gray) object C, and then
+# C's reference to B is removed. The collector never discovers B and frees it
+# while A still points to it. Traditional concurrent collectors need write
+# barriers to prevent this.
+#
+# This problem structurally cannot arise in YRC because the cycle collector only
+# frees *closed cycles* — subgraphs where every reference to every member comes
+# from within the group, with zero external references. To execute `A.field = B`
+# the mutator must hold a reference to A, which means A has an external reference
+# (from the stack) that is not a heap-to-heap edge. During trial deletion
+# (`markGray`) only internal edges are subtracted from RCs, so A's external
+# reference survives, `scan` finds A's RC >= 0, calls `scanBlack`, and rescues A
+# and everything reachable from it — including B. In short: the mutator can only
+# modify objects it can reach, but the cycle collector only frees objects nothing
+# external can reach. The two conditions are mutually exclusive.
+#
+#[
+
+The problem described in Bacon01 is: during markGray/scan, a mutator concurrently
+does X.field = Z (was X→Y), changing the physical graph while the collector is tracing
+it. The collector might see stale or new edges. The reasons this is still safe:
+
+Stale edges cancel with unbuffered decrements: If the collector sees old edge X→Y
+(mutator already wrote X→Z and buffered dec(Y)), the phantom trial deletion and the
+unbuffered dec cancel — Y's effective RC is correct.
+
+scanBlack rescues via current physical edges: If X has external refs (merged RC reflects
+the mutator's access), scanBlack(X) re-traces X and follows the current physical edge X→Z,
+incrementing Z's RC and marking it black. Z survives.
+
+rcSum==edges fast path is conservative: Any discrepancy between physical graph and merged
+state (stale or new edges) causes rcSum != edges, falling back to the slow path which
+rescues anything with RC >= 0.
+
+Unreachable cycles are truly unreachable: The mutator can only reach objects through chains
+rooted in merged references. If a cycle has zero external refs at merge time, no mutator
+can reach it.
+
+]#
+
+{.push raises: [].}
+
+include cellseqs_v2
+
+import std/locks
+
+const
+  NumStripes = 64
+  QueueSize = 128
+  RootsThreshold = 10
+
+  colBlack = 0b000
+  colGray = 0b001
+  colWhite = 0b010
+  maybeCycle = 0b100
+  inRootsFlag = 0b1000
+  colorMask = 0b011
+  logOrc = defined(nimArcIds)
+
+type
+  TraceProc = proc (p, env: pointer) {.nimcall, benign, raises: [].}
+  DisposeProc = proc (p: pointer) {.nimcall, benign, raises: [].}
+
+template color(c): untyped = c.rc and colorMask
+template setColor(c, col) =
+  when col == colBlack:
+    c.rc = c.rc and not colorMask
+  else:
+    c.rc = c.rc and not colorMask or col
+
+const
+  optimizedOrc = false
+  useJumpStack = false
+
+type
+  GcEnv = object
+    traceStack: CellSeq[ptr pointer]
+    when useJumpStack:
+      jumpStack: CellSeq[ptr pointer]
+    toFree: CellSeq[Cell]
+    freed, touched, edges, rcSum: int
+    keepThreshold: bool
+
+proc trace(s: Cell; desc: PNimTypeV2; j: var GcEnv) {.inline.} =
+  if desc.traceImpl != nil:
+    var p = s +! sizeof(RefHeader)
+    cast[TraceProc](desc.traceImpl)(p, addr(j))
+
+include threadids
+
+type
+  Stripe = object
+    when not defined(yrcAtomics):
+      lockInc: Lock
+    toIncLen: int
+    toInc: array[QueueSize, Cell]
+    lockDec: Lock
+    toDecLen: int
+    toDec: array[QueueSize, (Cell, PNimTypeV2)]
+
+type
+  PreventThreadFromCollectProc* = proc(): bool {.nimcall, benign, raises: [].}
+    ## Callback run before this thread runs the cycle collector.
+    ## Return `true` to allow collection, `false` to skip (e.g. real-time thread).
+    ## Invoked while holding the global lock; must not call back into YRC.
+
+var
+  gYrcGlobalLock: Lock
+  roots: CellSeq[Cell]  # merged roots, used under global lock
+  stripes: array[NumStripes, Stripe]
+  rootsThreshold: int = 128
+  defaultThreshold = when defined(nimFixedOrc): 10_000 else: 128
+  gPreventThreadFromCollectProc: PreventThreadFromCollectProc = nil
+
+proc GC_setPreventThreadFromCollectProc*(cb: PreventThreadFromCollectProc) =
+  ##[ Can be used to customize the cycle collector for a thread. For example,
+  to ensure that a hard realtime thread cannot run the cycle collector use:
+
+  ```nim
+  var hardRealTimeThread: int
+  GC_setPreventThreadFromCollectProc(proc(): bool {.nimcall.} = hardRealTimeThread == getThreadId())
+  ```
+
+  To ensure that a hard realtime thread cannot by involved in any cycle collector activity use:
+
+  ```nim
+  GC_setPreventThreadFromCollectProc(proc(): bool {.nimcall.} =
+    if hardRealTimeThread == getThreadId():
+      writeStackTrace()
+      echo "Realtime thread involved in unpredictable cycle collector activity!"
+    result = false
+  )
+  ```
+  ]##
+  gPreventThreadFromCollectProc = cb
+
+proc GC_getPreventThreadFromCollectProc*(): PreventThreadFromCollectProc =
+  ## Returns the current "prevent thread from collecting proc".
+  ## Typically `nil` if not set.
+  result = gPreventThreadFromCollectProc
+
+proc mayRunCycleCollect(): bool {.inline.} =
+  if gPreventThreadFromCollectProc == nil: true
+  else: not gPreventThreadFromCollectProc()
+
+proc getStripeIdx(): int {.inline.} =
+  getThreadId() and (NumStripes - 1)
+
+proc nimIncRefCyclic(p: pointer; cyclic: bool) {.compilerRtl, inl.} =
+  let h = head(p)
+  when optimizedOrc:
+    if cyclic: h.rc = h.rc or maybeCycle
+  when defined(yrcAtomics):
+    let s = getStripeIdx()
+    let slot = atomicFetchAdd(addr stripes[s].toIncLen, 1, ATOMIC_ACQ_REL)
+    if slot < QueueSize:
+      atomicStoreN(addr stripes[s].toInc[slot], h, ATOMIC_RELEASE)
+    else:
+      withLock gYrcGlobalLock:
+        h.rc = h.rc +% rcIncrement
+        for i in 0..<NumStripes:
+          let len = atomicExchangeN(addr stripes[i].toIncLen, 0, ATOMIC_ACQUIRE)
+          for j in 0..<min(len, QueueSize):
+            let x = atomicLoadN(addr stripes[i].toInc[j], ATOMIC_ACQUIRE)
+            x.rc = x.rc +% rcIncrement
+  else:
+    let idx = getStripeIdx()
+    while true:
+      var overflow = false
+      withLock stripes[idx].lockInc:
+        if stripes[idx].toIncLen < QueueSize:
+          stripes[idx].toInc[stripes[idx].toIncLen] = h
+          stripes[idx].toIncLen += 1
+        else:
+          overflow = true
+      if overflow:
+        withLock gYrcGlobalLock:
+          for i in 0..<NumStripes:
+            withLock stripes[i].lockInc:
+              for j in 0..<stripes[i].toIncLen:
+                let x = stripes[i].toInc[j]
+                x.rc = x.rc +% rcIncrement
+              stripes[i].toIncLen = 0
+      else:
+        break
+
+proc mergePendingRoots() =
+  # Merge buffered RC operations. Note: Unlike truly concurrent collectors,
+  # we don't need to set color to black on incRef because collection runs
+  # under the global lock, so no concurrent mutations happen during collection.
+  for i in 0..<NumStripes:
+    when defined(yrcAtomics):
+      let incLen = atomicExchangeN(addr stripes[i].toIncLen, 0, ATOMIC_ACQUIRE)
+      for j in 0..<min(incLen, QueueSize):
+        let x = atomicLoadN(addr stripes[i].toInc[j], ATOMIC_ACQUIRE)
+        x.rc = x.rc +% rcIncrement
+    else:
+      withLock stripes[i].lockInc:
+        for j in 0..<stripes[i].toIncLen:
+          let x = stripes[i].toInc[j]
+          x.rc = x.rc +% rcIncrement
+        stripes[i].toIncLen = 0
+    withLock stripes[i].lockDec:
+      for j in 0..<stripes[i].toDecLen:
+        let (c, desc) = stripes[i].toDec[j]
+        c.rc = c.rc -% rcIncrement
+        if (c.rc and inRootsFlag) == 0:
+          c.rc = c.rc or inRootsFlag
+          if roots.d == nil: init(roots)
+          add(roots, c, desc)
+      stripes[i].toDecLen = 0
+
+proc collectCycles()
+
+when logOrc or orcLeakDetector:
+  proc writeCell(msg: cstring; s: Cell; desc: PNimTypeV2) =
+    when orcLeakDetector:
+      cfprintf(cstderr, "%s %s file: %s:%ld; color: %ld; thread: %ld\n",
+        msg, if desc != nil: desc.name else: cstring"(nil)", s.filename, s.line, s.color, getThreadId())
+    else:
+      # Guard nil desc/desc.name. Use cell pointer as id to avoid uninitialized s.refId (roots may have refId unset)
+      let name = if desc != nil and desc.name != nil: desc.name else: cstring"(null)"
+      cfprintf(cstderr, "%s %s %p isroot: %s; RC: %ld; color: %ld; thread: %ld\n",
+        msg, name, s, (if (s.rc and inRootsFlag) != 0: "yes" else: "no"), s.rc shr rcShift, s.color, getThreadId())
+
+proc free(s: Cell; desc: PNimTypeV2) {.inline.} =
+  when traceCollector:
+    cprintf("[From ] %p rc %ld color %ld\n", s, s.rc shr rcShift, s.color)
+  if (s.rc and inRootsFlag) == 0:
+    let p = s +! sizeof(RefHeader)
+    when logOrc: writeCell("free", s, desc)
+    if desc.destructor != nil:
+      cast[DestructorProc](desc.destructor)(p)
+    nimRawDispose(p, desc.align)
+
+template orcAssert(cond, msg) =
+  when logOrc:
+    if not cond:
+      cfprintf(cstderr, "[Bug!] %s\n", msg)
+      rawQuit 1
+
+proc nimTraceRef(q: pointer; desc: PNimTypeV2; env: pointer) {.compilerRtl, inl.} =
+  let p = cast[ptr pointer](q)
+  if p[] != nil:
+    var j = cast[ptr GcEnv](env)
+    j.traceStack.add(p, desc)
+
+proc nimTraceRefDyn(q: pointer; env: pointer) {.compilerRtl, inl.} =
+  let p = cast[ptr pointer](q)
+  if p[] != nil:
+    var j = cast[ptr GcEnv](env)
+    j.traceStack.add(p, cast[ptr PNimTypeV2](p[])[])
+
+proc scanBlack(s: Cell; desc: PNimTypeV2; j: var GcEnv) =
+  s.setColor colBlack
+  let until = j.traceStack.len
+  trace(s, desc, j)
+  when logOrc: writeCell("root still alive", s, desc)
+  while j.traceStack.len > until:
+    let (entry, desc) = j.traceStack.pop()
+    let t = head entry[]
+    t.rc = t.rc +% rcIncrement
+    if t.color != colBlack:
+      t.setColor colBlack
+      trace(t, desc, j)
+      when logOrc: writeCell("child still alive", t, desc)
+
+proc markGray(s: Cell; desc: PNimTypeV2; j: var GcEnv) =
+  if s.color != colGray:
+    s.setColor colGray
+    j.touched = j.touched +% 1
+    j.rcSum = j.rcSum +% (s.rc shr rcShift) +% 1
+    orcAssert(j.traceStack.len == 0, "markGray: trace stack not empty")
+    trace(s, desc, j)
+    while j.traceStack.len > 0:
+      let (entry, desc) = j.traceStack.pop()
+      let t = head entry[]
+      t.rc = t.rc -% rcIncrement
+      j.edges = j.edges +% 1
+      if t.color != colGray:
+        t.setColor colGray
+        j.touched = j.touched +% 1
+        j.rcSum = j.rcSum +% (t.rc shr rcShift) +% 2
+        trace(t, desc, j)
+
+proc scan(s: Cell; desc: PNimTypeV2; j: var GcEnv) =
+  if s.color == colGray:
+    if (s.rc shr rcShift) >= 0:
+      scanBlack(s, desc, j)
+    else:
+      orcAssert(j.traceStack.len == 0, "scan: trace stack not empty")
+      s.setColor(colWhite)
+      trace(s, desc, j)
+      while j.traceStack.len > 0:
+        let (entry, desc) = j.traceStack.pop()
+        let t = head entry[]
+        if t.color == colGray:
+          if (t.rc shr rcShift) >= 0:
+            scanBlack(t, desc, j)
+          else:
+            t.setColor(colWhite)
+            trace(t, desc, j)
+
+proc collectColor(s: Cell; desc: PNimTypeV2; col: int; j: var GcEnv) =
+  if s.color == col and (s.rc and inRootsFlag) == 0:
+    orcAssert(j.traceStack.len == 0, "collectWhite: trace stack not empty")
+    s.setColor(colBlack)
+    j.toFree.add(s, desc)
+    trace(s, desc, j)
+    while j.traceStack.len > 0:
+      let (entry, desc) = j.traceStack.pop()
+      let t = head entry[]
+      entry[] = nil
+      if t.color == col and (t.rc and inRootsFlag) == 0:
+        j.toFree.add(t, desc)
+        t.setColor(colBlack)
+        trace(t, desc, j)
+
+proc collectCyclesBacon(j: var GcEnv; lowMark: int) =
+  # YRC defers all destruction to collection time - process ALL roots through Bacon's algorithm
+  # This is different from ORC which handles immediate garbage (rc == 0) directly
+  let last = roots.len -% 1
+  when logOrc:
+    for i in countdown(last, lowMark):
+      writeCell("root", roots.d[i][0], roots.d[i][1])
+
+  # Process all roots through markGray (Bacon's algorithm)
+  for i in countdown(last, lowMark):
+    markGray(roots.d[i][0], roots.d[i][1], j)
+
+  var colToCollect = colWhite
+  if j.rcSum == j.edges:
+    # Short-cut: we know everything is garbage
+    colToCollect = colGray
+    j.keepThreshold = true
+  else:
+    # Normal scan phase
+    for i in countdown(last, lowMark):
+      scan(roots.d[i][0], roots.d[i][1], j)
+
+  # Collect phase: free all garbage objects
+  init j.toFree
+  for i in 0 ..< roots.len:
+    let s = roots.d[i][0]
+    s.rc = s.rc and not inRootsFlag
+    collectColor(s, roots.d[i][1], colToCollect, j)
+
+  # Clear roots before freeing to prevent nested collectCycles() from accessing freed cells
+  when not defined(nimStressOrc):
+    let oldThreshold = rootsThreshold
+    rootsThreshold = high(int)
+  roots.len = 0
+
+  # Free all collected objects
+  # Destructors must not call nimDecRefIsLastCyclicStatic (add to toDec) during this phase
+  for i in 0 ..< j.toFree.len:
+    let s = j.toFree.d[i][0]
+    when orcLeakDetector:
+      writeCell("CYCLIC OBJECT FREED", s, j.toFree.d[i][1])
+    free(s, j.toFree.d[i][1])
+  when not defined(nimStressOrc):
+    rootsThreshold = oldThreshold
+  j.freed = j.freed +% j.toFree.len
+  deinit j.toFree
+
+when defined(nimOrcStats):
+  var freedCyclicObjects {.threadvar.}: int
+
+proc collectCycles() =
+  when logOrc:
+    cfprintf(cstderr, "[collectCycles] begin\n")
+  withLock gYrcGlobalLock:
+    mergePendingRoots()
+    if roots.len >= RootsThreshold and mayRunCycleCollect():
+      var j: GcEnv
+      init j.traceStack
+      collectCyclesBacon(j, 0)
+      if roots.len == 0 and roots.d != nil:
+        deinit roots
+      when not defined(nimStressOrc):
+        if j.keepThreshold:
+          discard
+        elif j.freed *% 2 >= j.touched:
+          when not defined(nimFixedOrc):
+            rootsThreshold = max(rootsThreshold div 3 *% 2, 16)
+          else:
+            rootsThreshold = 0
+        elif rootsThreshold < high(int) div 4:
+          rootsThreshold = (if rootsThreshold <= 0: defaultThreshold else: rootsThreshold)
+          rootsThreshold = rootsThreshold div 2 +% rootsThreshold
+          # Cap growth so threshold doesn't grow without bound when we rarely free cycles
+          #rootsThreshold = min(rootsThreshold, defaultThreshold *% 16)
+      when logOrc:
+        cfprintf(cstderr, "[collectCycles] end; freed %ld new threshold %ld\n", j.freed, rootsThreshold)
+      when defined(nimOrcStats):
+        inc freedCyclicObjects, j.freed
+      deinit j.traceStack
+
+when defined(nimOrcStats):
+  type
+    OrcStats* = object
+      freedCyclicObjects*: int
+  proc GC_orcStats*(): OrcStats =
+    result = OrcStats(freedCyclicObjects: freedCyclicObjects)
+
+proc GC_runOrc* =
+  withLock gYrcGlobalLock:
+    mergePendingRoots()
+    if mayRunCycleCollect():
+      var j: GcEnv
+      init j.traceStack
+      collectCyclesBacon(j, 0)
+      deinit j.traceStack
+      roots.len = 0
+  when logOrc: orcAssert roots.len == 0, "roots not empty!"
+
+proc GC_enableOrc*() =
+  when not defined(nimStressOrc):
+    rootsThreshold = 0
+
+proc GC_disableOrc*() =
+  when not defined(nimStressOrc):
+    rootsThreshold = high(int)
+
+proc GC_prepareOrc*(): int {.inline.} =
+  withLock gYrcGlobalLock:
+    mergePendingRoots()
+    result = roots.len
+
+proc GC_partialCollect*(limit: int) =
+  withLock gYrcGlobalLock:
+    mergePendingRoots()
+    if roots.len > limit and mayRunCycleCollect():
+      var j: GcEnv
+      init j.traceStack
+      collectCyclesBacon(j, limit)
+      deinit j.traceStack
+      roots.len = limit
+
+proc GC_fullCollect* =
+  GC_runOrc()
+
+proc GC_enableMarkAndSweep*() = GC_enableOrc()
+proc GC_disableMarkAndSweep*() = GC_disableOrc()
+
+const acyclicFlag = 1
+
+when optimizedOrc:
+  template markedAsCyclic(s: Cell; desc: PNimTypeV2): bool =
+    (desc.flags and acyclicFlag) == 0 and (s.rc and maybeCycle) != 0
+else:
+  template markedAsCyclic(s: Cell; desc: PNimTypeV2): bool =
+    (desc.flags and acyclicFlag) == 0
+
+proc nimDecRefIsLastCyclicDyn(p: pointer): bool {.compilerRtl, inl.} =
+  result = false
+  if p != nil:
+    let cell = head(p)
+    let desc = cast[ptr PNimTypeV2](p)[]
+    let idx = getStripeIdx()
+    while true:
+      var overflow = false
+      withLock stripes[idx].lockDec:
+        if stripes[idx].toDecLen < QueueSize:
+          stripes[idx].toDec[stripes[idx].toDecLen] = (cell, desc)
+          stripes[idx].toDecLen += 1
+        else:
+          overflow = true
+      if overflow:
+        collectCycles()
+      else:
+        break
+
+proc nimDecRefIsLastDyn(p: pointer): bool {.compilerRtl, inl.} =
+  nimDecRefIsLastCyclicDyn(p)
+
+proc nimDecRefIsLastCyclicStatic(p: pointer; desc: PNimTypeV2): bool {.compilerRtl, inl.} =
+  result = false
+  if p != nil:
+    let cell = head(p)
+    let idx = getStripeIdx()
+    while true:
+      var overflow = false
+      withLock stripes[idx].lockDec:
+        if stripes[idx].toDecLen < QueueSize:
+          stripes[idx].toDec[stripes[idx].toDecLen] = (cell, desc)
+          stripes[idx].toDecLen += 1
+        else:
+          overflow = true
+      if overflow:
+        collectCycles()
+      else:
+        break
+
+proc unsureAsgnRef(dest: ptr pointer, src: pointer) {.inline.} =
+  dest[] = src
+  if src != nil: nimIncRefCyclic(src, true)
+
+proc yrcDec(tmp: pointer; desc: PNimTypeV2) {.inline.} =
+  if desc != nil:
+    discard nimDecRefIsLastCyclicStatic(tmp, desc)
+  else:
+    discard nimDecRefIsLastCyclicDyn(tmp)
+
+proc nimAsgnYrc(dest: ptr pointer; src: pointer; desc: PNimTypeV2) {.compilerRtl.} =
+  ## YRC write barrier for ref copy assignment.
+  ## Atomically stores src into dest, then buffers RC adjustments.
+  ## Freeing is always done by the cycle collector, never inline.
+  let tmp = dest[]
+  atomicStoreN(dest, src, ATOMIC_RELEASE)
+  if src != nil:
+    nimIncRefCyclic(src, true)
+  if tmp != nil:
+    yrcDec(tmp, desc)
+
+proc nimSinkYrc(dest: ptr pointer; src: pointer; desc: PNimTypeV2) {.compilerRtl.} =
+  ## YRC write barrier for ref sink (move). No incRef on source.
+  ## Freeing is always done by the cycle collector, never inline.
+  let tmp = dest[]
+  atomicStoreN(dest, src, ATOMIC_RELEASE)
+  if tmp != nil:
+    yrcDec(tmp, desc)
+
+proc nimMarkCyclic(p: pointer) {.compilerRtl, inl.} =
+  when optimizedOrc:
+    if p != nil:
+      let h = head(p)
+      h.rc = h.rc or maybeCycle
+
+# Initialize locks at module load
+initLock(gYrcGlobalLock)
+for i in 0..<NumStripes:
+  when not defined(yrcAtomics):
+    initLock(stripes[i].lockInc)
+  initLock(stripes[i].lockDec)
+
+{.pop.}
--- a/lib/system/yrc_proof.lean
+++ b/lib/system/yrc_proof.lean
@@ -0,0 +1,353 @@
+/-
+  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.
+
+  ## Model overview
+
+  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)
+
+  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)
+-/
+
+-- Objects and threads are just natural numbers for simplicity.
+abbrev Obj := Nat
+abbrev Thread := Nat
+
+/-! ### State -/
+
+/-- The state of the heap and collector 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). -/
+  edges : Obj → Obj → Prop
+  /-- Stack roots per thread. `roots t x` means thread `t` has a local variable pointing to `x`. -/
+  roots : Thread → Obj → Prop
+  /-- Pending buffered increments (not yet merged). -/
+  pendingInc : Obj → Nat
+  /-- Pending buffered decrements (not yet merged). -/
+  pendingDec : Obj → Nat
+
+/-! ### Reachability -/
+
+/-- An object is *reachable* if some thread can reach it via stack roots + 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). -/
+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
+  induction hp with
+  | 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. -/
+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. -/
+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. -/
+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`. -/
+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 =>
+    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`. -/
+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 -/
+
+/-- 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). -/
+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 }
+
+/-- **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.
+
+    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`. -/
+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
+  apply Reachable.step a b
+  · exact Reachable.root t a h_root_a
+  · simp [writeBarrier]
+
+/-! ### Non-atomic write barrier window safety
+
+  The write barrier does three steps non-atomically:
+    1. atomicStore(dest, src)     — graph update
+    2. buffer inc(src)            — deferred
+    3. buffer dec(old)            — deferred
+
+  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 ✓
+
+  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 ✓
+-/
+
+/-- 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 :=
+  { 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 }
+
+/-- 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]
+
+/-- 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))
+
+/-! ### Deadlock freedom
+
+  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)
+
+  Total order:  global < lockInc[0] < lockDec[0] < lockInc[1] < lockDec[1] < ...
+
+  Every code path in yrc.nim acquires locks in strictly ascending level order:
+
+  **nimIncRefCyclic** (mutator fast path):
+    acquire lockInc[myStripe] → release → done.
+    Holds exactly one lock. ✓
+
+  **nimIncRefCyclic** (overflow path):
+    acquire gYrcGlobalLock (level 0), then for i=0..N-1: acquire lockInc[i] → release.
+    Ascending: 0 < 1 < 3 < 5 < ... ✓
+
+  **nimDecRefIsLastCyclic{Dyn,Static}** (fast path):
+    acquire lockDec[myStripe] → release → done.
+    Holds exactly one lock. ✓
+
+  **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 < ... ✓
+
+  **collectCycles / GC_runOrc** (collector):
+    acquire gYrcGlobalLock (level 0),
+    then mergePendingRoots (same ascending pattern as above). ✓
+
+  **nimAsgnYrc / nimSinkYrc** (write barrier):
+    Calls nimIncRefCyclic then nimDecRefIsLastCyclic*.
+    Each call acquires and releases its lock independently.
+    No nesting between the two calls. ✓
+
+  Since every path follows the total order, deadlock is impossible.
+-/
+
+/-- Lock levels in YRC. Each lock maps to a unique natural number. -/
+inductive LockId (n : Nat) where
+  | global : LockId n
+  | lockInc (i : Nat) (h : i < n) : LockId n
+  | lockDec (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
+
+/-- All lock levels are distinct (the level function is injective). -/
+theorem lockLevel_injective {n : Nat} (a b : LockId n)
+    (h : lockLevel a = lockLevel b) : a = b := by
+  cases a with
+  | global =>
+    cases b with
+    | global => rfl
+    | lockInc j hj => simp [lockLevel] at h
+    | lockDec j hj => simp [lockLevel] at h
+  | lockInc 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
+      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
+  cases l with
+  | global => exact absurd rfl h
+  | lockInc i hi => simp [lockLevel]
+  | lockDec 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). -/
+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)
+
+  1. `reachable_is_anchored`: Every reachable object is anchored
+     (has a path from an externally-referenced object via heap edges).
+
+  2. `yrc_safety`: The collector only frees unanchored objects,
+     which are unreachable by all threads. **No use-after-free.**
+
+  3. `no_lost_object`: After `a.field = b`, `b` is reachable
+     (atomic store makes the edge visible immediately).
+
+  4. `src_safe_in_window`: Even between the atomic store and
+     the buffered inc, the collector cannot free src.
+
+  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).
+
+  Reference: D.F. Bacon and V.T. Rajan, "Concurrent Cycle Collection in
+  Reference Counted Systems", ECOOP 2001.
+-/
--- a/lib/system/yrc_proof.tla
+++ b/lib/system/yrc_proof.tla
@@ -0,0 +1,761 @@
+---- MODULE yrc_proof ----
+\* TLA+ specification of YRC (Thread-safe ORC cycle collector)
+\* Models the fine details of barriers, striped queues, and synchronization
+\*
+\* ## Key Barrier Semantics Modeled
+\*
+\* ### Write Barrier (nimAsgnYrc)
+\*   1. atomicStoreN(dest, src, ATOMIC_RELEASE)
+\*      - Graph update is immediately visible to all threads (including collector)
+\*      - ATOMIC_RELEASE ensures all prior writes are visible before this store
+\*      - No lock required for graph updates (lock-free)
+\*
+\*   2. nimIncRefCyclic(src, true)
+\*      - Acquires per-stripe lockInc[stripe] (fine-grained)
+\*      - Buffers increment in toInc[stripe] queue
+\*      - On overflow: acquires global lock, merges all stripes, applies increment
+\*
+\*   3. yrcDec(tmp, desc)
+\*      - Acquires per-stripe lockDec[stripe] (fine-grained)
+\*      - Buffers decrement in toDec[stripe] queue
+\*      - On overflow: acquires global lock, merges all stripes, applies decrement,
+\*        adds to roots array if not already present
+\*
+\* ### Merge Operation (mergePendingRoots)
+\*   - Acquires global lock (exclusive access)
+\*   - Sequentially acquires each stripe's lockInc and lockDec
+\*   - Drains all buffers, applies RC adjustments
+\*   - Adds decremented objects to roots array
+\*   - After merge: mergedRC = logicalRC (current graph state)
+\*
+\* ### Collection Cycle (under global lock)
+\*   1. mergePendingRoots: reconcile buffered changes
+\*   2. markGray: trial deletion (subtract internal edges)
+\*   3. scan: rescue objects with RC >= 0 (scanBlack follows current graph)
+\*   4. collectColor: free white objects (closed cycles)
+\*
+\* ## Safety Argument
+\*
+\* The collector only frees closed cycles (zero external refs). Concurrent writes
+\* cannot cause "lost objects" because:
+\*   - Graph updates are atomic and immediately visible
+\*   - Mutator must hold stack ref to modify object (external ref)
+\*   - scanBlack follows current physical edges (rescues newly written objects)
+\*   - Only objects unreachable from any stack root are freed
+
+EXTENDS Naturals, Integers, Sequences, FiniteSets, TLC
+
+CONSTANTS NumStripes, QueueSize, RootsThreshold, Objects, Threads, ObjTypes
+ASSUME NumStripes \in Nat /\ NumStripes > 0
+ASSUME QueueSize \in Nat /\ QueueSize > 0
+ASSUME RootsThreshold \in Nat
+ASSUME IsFiniteSet(Objects)
+ASSUME IsFiniteSet(Threads)
+ASSUME IsFiniteSet(ObjTypes)
+
+\* NULL constant (represents "no thread" for locks)
+\* We use a sentinel value that's guaranteed not to be in Threads or Objects
+NULL == "NULL"  \* String literal that won't conflict with Threads/Objects
+ASSUME NULL \notin Threads /\ NULL \notin Objects
+
+\* Helper functions
+\* Note: GetStripeIdx is not used, GetStripe is used instead
+
+\* Color constants
+colBlack == 0
+colGray == 1
+colWhite == 2
+maybeCycle == 4
+inRootsFlag == 8
+colorMask == 3
+
+\* State variables
+VARIABLES
+    \* Physical heap graph (always up-to-date, atomic stores)
+    edges,              \* edges[obj1][obj2] = TRUE if obj1.field points to obj2
+    \* Stack roots per thread
+    roots,              \* roots[thread][obj] = TRUE if thread has local var pointing to obj
+    \* Reference counts (stored in object header)
+    rc,                 \* rc[obj] = reference count (logical, after merge)
+    \* Color markers (stored in object header, bits 0-2)
+    color,              \* color[obj] \in {colBlack, colGray, colWhite}
+    \* Root tracking flags
+    inRoots,            \* inRoots[obj] = TRUE if obj is in roots array
+    \* Striped increment queues
+    toIncLen,           \* toIncLen[stripe] = current length of increment queue
+    toInc,              \* toInc[stripe][i] = object to increment
+    \* Striped decrement queues
+    toDecLen,           \* toDecLen[stripe] = current length of decrement queue
+    toDec,              \* toDec[stripe][i] = (object, type) pair to decrement
+    \* Per-stripe locks
+    lockInc,            \* lockInc[stripe] = thread holding increment lock (or NULL)
+    lockDec,            \* lockDec[stripe] = thread holding decrement lock (or NULL)
+    \* Global lock
+    globalLock,         \* thread holding global lock (or NULL)
+    \* Merged roots array (used during collection)
+    mergedRoots,        \* sequence of (object, type) pairs
+    \* Collection state
+    collecting,         \* TRUE if collection is in progress
+    gcEnv,              \* GC environment: {touched, edges, rcSum, toFree, ...}
+    \* Pending operations (for modeling atomicity)
+    pendingWrites       \* set of pending write barrier operations
+
+\* Type invariants
+TypeOK ==
+    /\ edges \in [Objects -> [Objects -> BOOLEAN]]
+    /\ roots \in [Threads -> [Objects -> BOOLEAN]]
+    /\ rc \in [Objects -> Int]
+    /\ color \in [Objects -> {colBlack, colGray, colWhite}]
+    /\ inRoots \in [Objects -> BOOLEAN]
+    /\ toIncLen \in [0..(NumStripes-1) -> 0..QueueSize]
+    /\ toInc \in [0..(NumStripes-1) -> Seq(Objects)]
+    /\ toDecLen \in [0..(NumStripes-1) -> 0..QueueSize]
+    /\ toDec \in [0..(NumStripes-1) -> Seq([obj: Objects, desc: ObjTypes])]
+    /\ lockInc \in [0..(NumStripes-1) -> Threads \cup {NULL}]
+    /\ lockDec \in [0..(NumStripes-1) -> Threads \cup {NULL}]
+    /\ globalLock \in Threads \cup {NULL}
+    /\ mergedRoots \in Seq([obj: Objects, desc: ObjTypes])
+    /\ collecting \in BOOLEAN
+    /\ pendingWrites \in SUBSET ([thread: Threads, dest: Objects, old: Objects \cup {NULL}, src: Objects \cup {NULL}, phase: {"store", "inc", "dec"}])
+
+\* Helper: internal reference count (heap-to-heap edges)
+InternalRC(obj) ==
+    Cardinality({src \in Objects : edges[src][obj]})
+
+\* Helper: external reference count (stack roots)
+ExternalRC(obj) ==
+    Cardinality({t \in Threads : roots[t][obj]})
+
+\* Helper: logical reference count
+LogicalRC(obj) ==
+    InternalRC(obj) + ExternalRC(obj)
+
+\* Helper: get stripe index for thread
+\* Map threads to stripe indices deterministically
+\* Since threads are ModelValues, we use a simple deterministic mapping:
+\* Assign each thread to stripe 0 (for small models, this is fine)
+\* For larger models, TLC will handle the mapping deterministically
+GetStripe(thread) == 0
+
+\* ============================================================================
+\* Write Barrier: nimAsgnYrc
+\* ============================================================================
+\* The write barrier does:
+\*   1. atomicStoreN(dest, src, ATOMIC_RELEASE)  -- graph update is immediate
+\*   2. nimIncRefCyclic(src, true)                -- buffer inc(src)
+\*   3. yrcDec(tmp, desc)                         -- buffer dec(old)
+\*
+\* Key barrier semantics:
+\* - ATOMIC_RELEASE on store ensures all prior writes are visible before the graph update
+\* - The graph update is immediately visible to all threads (including collector)
+\* - RC adjustments are buffered and only applied during merge
+
+\* ============================================================================
+\* Phase 1: Atomic Store (Topology Update)
+\* ============================================================================
+\* The atomic store always happens first, updating the graph topology.
+\* This is independent of RC operations and never blocks.
+MutatorWriteAtomicStore(thread, destObj, destField, oldVal, newVal, desc) ==
+    \* Atomic store with RELEASE barrier - updates graph topology immediately
+    \* Clear ALL edges from destObj first (atomic store replaces old value completely),
+    \* then set the new edge. This ensures destObj.field can only point to one object.
+    /\ edges' = [edges EXCEPT ![destObj] = [x \in Objects |->
+                                                 IF x = newVal /\ newVal # NULL
+                                                 THEN TRUE
+                                                 ELSE FALSE]]
+    /\ UNCHANGED <<roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites>>
+
+\* ============================================================================
+\* Phase 2: RC Buffering (if space available)
+\* ============================================================================
+\* Buffers increment/decrement if there's space. If overflow would happen,
+\* this action is disabled (blocked) until merge can happen.
+WriteBarrier(thread, destObj, destField, oldVal, newVal, desc) ==
+    LET stripe == GetStripe(thread)
+    IN
+    \* Determine if overflow happens for increment or decrement
+    /\ LET
+          incOverflow == (newVal # NULL) /\ (toIncLen[stripe] >= QueueSize)
+          decOverflow == (oldVal # NULL) /\ (toDecLen[stripe] >= QueueSize)
+       IN
+       \* Buffering: only enabled if no overflow (otherwise blocked until merge can happen)
+       /\ ~incOverflow  \* Precondition: increment buffer has space (blocks if full)
+       /\ ~decOverflow  \* Precondition: decrement buffer has space (blocks if full)
+       /\ toIncLen' = IF newVal # NULL /\ toIncLen[stripe] < QueueSize
+                      THEN [toIncLen EXCEPT ![stripe] = toIncLen[stripe] + 1]
+                      ELSE toIncLen
+       /\ toInc' = IF newVal # NULL /\ toIncLen[stripe] < QueueSize
+                   THEN [toInc EXCEPT ![stripe] = Append(toInc[stripe], newVal)]
+                   ELSE toInc
+       /\ toDecLen' = IF oldVal # NULL /\ toDecLen[stripe] < QueueSize
+                      THEN [toDecLen EXCEPT ![stripe] = toDecLen[stripe] + 1]
+                      ELSE toDecLen
+       /\ toDec' = IF oldVal # NULL /\ toDecLen[stripe] < QueueSize
+                   THEN [toDec EXCEPT ![stripe] = Append(toDec[stripe], [obj |-> oldVal, desc |-> desc])]
+                   ELSE toDec
+       /\ UNCHANGED <<edges, roots, rc, color, inRoots, mergedRoots, lockInc, lockDec, globalLock, collecting, gcEnv, pendingWrites>>
+
+\* ============================================================================
+\* Phase 3: Overflow Handling (separate actions that can block)
+\* ============================================================================
+
+\* Handle increment overflow: merge increment buffers when lock is available
+\* This merges ALL increment buffers (for all stripes), not just the one that overflowed
+MutatorWriteMergeInc(thread) ==
+    LET stripe == GetStripe(thread)
+    IN
+    /\ \E s \in 0..(NumStripes-1): toIncLen[s] >= QueueSize  \* Some stripe has increment overflow
+    /\ globalLock = NULL  \* Lock must be available (blocks if held)
+    /\ toIncLen' = [s \in 0..(NumStripes-1) |-> 0]
+    /\ toInc' = [s \in 0..(NumStripes-1) |-> <<>>]
+    /\ rc' = \* Compute RC from LogicalRC of current graph (increment buffers merged)
+             \* The graph is already updated by atomic store, so we compute from current edges
+             [x \in Objects |->
+              LET internalRC == Cardinality({src \in Objects : edges[src][x]})
+                  externalRC == Cardinality({t \in Threads : roots[t][x]})
+              IN internalRC + externalRC]
+    /\ globalLock' = NULL  \* Release lock after merge
+    /\ UNCHANGED <<edges, roots, color, inRoots, toDecLen, toDec, lockInc, lockDec, mergedRoots, collecting, gcEnv, pendingWrites>>
+
+\* Handle decrement overflow: merge ALL buffers when lock is available
+\* This calls collectCycles() which merges both increment and decrement buffers
+\* We inline MergePendingRoots here. The entire withLock block is atomic:
+\* lock is acquired, merge happens, lock is released.
+MutatorWriteMergeDec(thread) ==
+    LET stripe == GetStripe(thread)
+    IN
+    /\ \E s \in 0..(NumStripes-1): toDecLen[s] >= QueueSize  \* Some stripe has decrement overflow
+    /\ globalLock = NULL  \* Lock must be available (blocks if held)
+    /\ \* Merge all buffers (inlined MergePendingRoots logic)
+       LET \* Compute new RC by merging all buffered increments and decrements
+           \* For each object, count buffered increments and decrements
+           bufferedInc == UNION {{toInc[s][i] : i \in 1..toIncLen[s]} : s \in 0..(NumStripes-1)}
+           bufferedDec == UNION {{toDec[s][i].obj : i \in 1..toDecLen[s]} : s \in 0..(NumStripes-1)}
+           \* Compute RC: current graph state (edges) + roots - buffered decrements + buffered increments
+           \* Actually, we compute from LogicalRC of current graph (buffers are merged)
+           newRC == [x \in Objects |->
+                      LET internalRC == Cardinality({src \in Objects : edges[src][x]})
+                          externalRC == Cardinality({t \in Threads : roots[t][x]})
+                      IN internalRC + externalRC]
+           \* Collect objects from decrement buffers for mergedRoots
+           newRootsSet == UNION {{toDec[s][i].obj : i \in 1..toDecLen[s]} : s \in 0..(NumStripes-1)}
+           newRootsSeq == IF newRootsSet = {}
+                          THEN <<>>
+                          ELSE LET ordered == CHOOSE f \in [1..Cardinality(newRootsSet) -> newRootsSet] :
+                                     \A i, j \in DOMAIN f : i # j => f[i] # f[j]
+                               IN [i \in 1..Cardinality(newRootsSet) |-> ordered[i]]
+       IN
+       /\ rc' = newRC
+       /\ mergedRoots' = mergedRoots \o newRootsSeq
+       /\ inRoots' = [x \in Objects |->
+                      IF newRootsSet = {}
+                      THEN inRoots[x]
+                      ELSE LET rootObjs == UNION {{mergedRoots'[i].obj : i \in DOMAIN mergedRoots'}}
+                           IN IF x \in rootObjs THEN TRUE ELSE inRoots[x]]
+       /\ toIncLen' = [s \in 0..(NumStripes-1) |-> 0]
+       /\ toInc' = [s \in 0..(NumStripes-1) |-> <<>>]
+       /\ toDecLen' = [s \in 0..(NumStripes-1) |-> 0]
+       /\ toDec' = [s \in 0..(NumStripes-1) |-> <<>>]
+    /\ globalLock' = NULL  \* Lock acquired, merge done, lock released (entire withLock block is atomic)
+    /\ UNCHANGED <<edges, roots, color, lockInc, lockDec, collecting, gcEnv, pendingWrites>>
+
+\* ============================================================================
+\* Merge Operation: mergePendingRoots
+\* ============================================================================
+\* Drains all stripe buffers under global lock.
+\* Sequentially acquires each stripe's lockInc and lockDec to drain buffers.
+\* This reconciles buffered RC adjustments with the current graph state.
+\*
+\* Key invariant: After merge, mergedRC = logicalRC (current graph + buffered changes)
+
+MergePendingRoots ==
+    /\ globalLock # NULL
+    /\ LET
+          \* Count pending increments per object (across all stripes)
+          pendingInc == [x \in Objects |->
+              Cardinality(UNION {{i \in DOMAIN toInc[s] : toInc[s][i] = x} :
+                                  s \in 0..(NumStripes-1)})]
+          \* Count pending decrements per object (across all stripes)
+          pendingDec == [x \in Objects |->
+              Cardinality(UNION {{i \in DOMAIN toDec[s] : toDec[s][i].obj = x} :
+                                  s \in 0..(NumStripes-1)})]
+          \* After merge, RC should equal LogicalRC (current graph state)
+          \* The buffered changes compensate for graph changes that already happened,
+          \* so: mergedRC = currentRC + pendingInc - pendingDec = LogicalRC(current graph)
+          \* But to ensure correctness, we compute directly from the current graph:
+          newRC == [x \in Objects |->
+              LogicalRC(x)]  \* RC after merge equals logical RC of current graph
+          \* Add decremented objects to roots if not already there (check inRootsFlag)
+          \* Collect all new roots as a set, then convert to sequence
+          \* Build set by iterating over all (stripe, index) pairs
+          \* Use UNION with explicit per-stripe sets (avoiding function enumeration issues)
+          newRootsSet == UNION {UNION {IF inRoots[toDec[s][i].obj] = FALSE
+                                      THEN {[obj |-> toDec[s][i].obj, desc |-> toDec[s][i].desc]}
+                                      ELSE {} : i \in DOMAIN toDec[s]} : s \in 0..(NumStripes-1)}
+          newRootsSeq == IF newRootsSet = {}
+                         THEN <<>>
+                         ELSE LET ordered == CHOOSE f \in [1..Cardinality(newRootsSet) -> newRootsSet] :
+                                    \A i, j \in DOMAIN f : i # j => f[i] # f[j]
+                              IN [i \in 1..Cardinality(newRootsSet) |-> ordered[i]]
+       IN
+       /\ rc' = newRC
+       /\ mergedRoots' = mergedRoots \o newRootsSeq  \* Append new roots to sequence
+       /\ \* Update inRoots: mark objects in mergedRoots' as being in roots
+          \* Use explicit iteration to avoid enumeration issues
+          inRoots' = [x \in Objects |->
+                      IF mergedRoots' = <<>>
+                      THEN inRoots[x]
+                      ELSE LET rootObjs == UNION {{mergedRoots'[i].obj : i \in DOMAIN mergedRoots'}}
+                           IN IF x \in rootObjs THEN TRUE ELSE inRoots[x]]
+       /\ toIncLen' = [s \in 0..(NumStripes-1) |-> 0]
+       /\ toInc' = [s \in 0..(NumStripes-1) |-> <<>>]
+       /\ toDecLen' = [s \in 0..(NumStripes-1) |-> 0]
+       /\ toDec' = [s \in 0..(NumStripes-1) |-> <<>>]
+    /\ UNCHANGED <<edges, roots, color, lockInc, lockDec, globalLock, collecting, gcEnv, pendingWrites>>
+
+\* ============================================================================
+\* Trial Deletion: markGray
+\* ============================================================================
+\* Subtracts internal (heap-to-heap) edges from reference counts.
+\* This isolates external references (stack roots).
+\*
+\* Algorithm:
+\*   1. Mark obj gray
+\*   2. Trace obj's fields (via traceImpl)
+\*   3. For each child c: decrement c.rc (subtract internal edge)
+\*   4. Recursively markGray all children
+\*
+\* After markGray: trialRC(obj) = mergedRC(obj) - internalRefCount(obj)
+\*                 = externalRefCount(obj) (if merge was correct)
+
+MarkGray(obj, desc) ==
+    /\ globalLock # NULL
+    /\ collecting = TRUE
+    /\ color[obj] # colGray
+    /\ \* Compute transitive closure of all objects reachable from obj
+       \* This models the recursive traversal in the actual implementation
+       LET children == {c \in Objects : edges[obj][c]}
+          \* Compute all objects reachable from obj via heap edges
+          \* This is the transitive closure starting from obj's direct children
+          allReachable == {c \in Objects :
+              \E path \in Seq(Objects):
+                 Len(path) > 0 /\
+                 path[1] \in children /\
+                 path[Len(path)] = c /\
+                 \A i \in 1..(Len(path)-1):
+                    edges[path[i]][path[i+1]]}
+          \* All objects to mark gray: obj itself + all reachable descendants
+          objectsToMarkGray == {obj} \cup allReachable
+          \* For each reachable object, count internal edges pointing to it
+          \* from within the subgraph (obj + allReachable)
+          \* This is the number of times its RC should be decremented
+          subgraph == {obj} \cup allReachable
+          internalEdgeCount == [x \in Objects |->
+              IF x \in allReachable
+              THEN Cardinality({y \in subgraph : edges[y][x]})
+              ELSE 0]
+       IN
+       /\ \* Mark obj and all reachable objects gray
+          color' = [x \in Objects |->
+              IF x \in objectsToMarkGray THEN colGray ELSE color[x]]
+       /\ \* Subtract internal edges: for each reachable object, decrement its RC
+          \* by the number of internal edges pointing to it from within the subgraph.
+          \* This matches the Nim implementation which decrements once per edge traversed.
+          \* Note: obj's RC is not decremented here (it has no parent in this subgraph).
+          \* For roots, the RC includes external refs which survive trial deletion.
+          rc' = [x \in Objects |->
+              IF x \in allReachable THEN rc[x] - internalEdgeCount[x] ELSE rc[x]]
+    /\ UNCHANGED <<edges, roots, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites>>
+
+\* ============================================================================
+\* Scan Phase
+\* ============================================================================
+\* Objects with RC >= 0 after trial deletion are rescued (scanBlack).
+\* Objects with RC < 0 remain white (part of closed cycle).
+\*
+\* Key insight: scanBlack follows the *current* physical edges (which may have
+\* changed since merge due to concurrent writes). This ensures objects written
+\* during collection are still rescued.
+\*
+\* Algorithm:
+\*   IF rc[obj] >= 0:
+\*     scanBlack(obj): mark black, restore RC, trace and rescue all children
+\*   ELSE:
+\*     mark white (closed cycle with zero external refs)
+
+Scan(obj, desc) ==
+    /\ globalLock # NULL
+    /\ collecting = TRUE
+    /\ color[obj] = colGray
+    /\ IF rc[obj] >= 0
+       THEN \* scanBlack: rescue obj and all reachable objects
+            \* This follows the current physical graph (atomic stores are visible)
+            \* Restore RC for all reachable objects by incrementing by the number of
+            \* internal edges pointing to each (matching what markGray subtracted)
+            LET children == {c \in Objects : edges[obj][c]}
+               allReachable == {c \in Objects :
+                   \E path \in Seq(Objects):
+                      Len(path) > 0 /\
+                      path[1] \in children /\
+                      path[Len(path)] = c /\
+                      \A i \in 1..(Len(path)-1):
+                         edges[path[i]][path[i+1]]}
+               objectsToMarkBlack == {obj} \cup allReachable
+               \* For each reachable object, count internal edges pointing to it
+               \* from within the subgraph (obj + allReachable)
+               \* This is the number of times its RC should be incremented (restored)
+               subgraph == {obj} \cup allReachable
+               internalEdgeCount == [x \in Objects |->
+                   IF x \in allReachable
+                   THEN Cardinality({y \in subgraph : edges[y][x]})
+                   ELSE 0]
+            IN
+            /\ \* Restore RC: increment by the number of internal edges pointing to each
+               \* reachable object. This restores what markGray subtracted.
+               \* Note: obj's RC is not incremented here (it wasn't decremented in markGray).
+               \* The root's RC already reflects external refs which survived trial deletion.
+               rc' = [x \in Objects |->
+                   IF x \in allReachable THEN rc[x] + internalEdgeCount[x] ELSE rc[x]]
+            /\ \* Mark obj and all reachable objects black in one assignment
+               color' = [x \in Objects |->
+                   IF x \in objectsToMarkBlack THEN colBlack ELSE color[x]]
+       ELSE \* Mark white (part of closed cycle)
+            /\ color' = [color EXCEPT ![obj] = colWhite]
+            /\ UNCHANGED <<rc>>
+    /\ UNCHANGED <<edges, roots, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites>>
+
+\* ============================================================================
+\* Collection Phase: collectColor
+\* ============================================================================
+\* Frees objects of the target color that are not in roots.
+\*
+\* Safety: Only objects with color = targetColor AND ~inRoots[obj] are freed.
+\* These are closed cycles (zero external refs, not reachable from roots).
+
+CollectColor(obj, desc, targetColor) ==
+    /\ globalLock # NULL
+    /\ collecting = TRUE
+    /\ color[obj] = targetColor
+    /\ ~inRoots[obj]
+    /\ \* Free obj: nullify all its outgoing edges (prevents use-after-free)
+       \* In the actual implementation, this happens during trace() when freeing
+       edges' = [edges EXCEPT ![obj] = [x \in Objects |->
+           IF x = obj THEN FALSE ELSE edges[obj][x]]]
+    /\ color' = [color EXCEPT ![obj] = colBlack]  \* Mark as freed
+    /\ UNCHANGED <<roots, rc, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites>>
+
+\* ============================================================================
+\* Collection Cycle: collectCyclesBacon
+\* ============================================================================
+
+StartCollection ==
+    /\ globalLock # NULL
+    /\ ~collecting
+    /\ Len(mergedRoots) >= RootsThreshold
+    /\ collecting' = TRUE
+    /\ gcEnv' = [touched |-> 0, edges |-> 0, rcSum |-> 0, toFree |-> {}]
+    /\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, pendingWrites>>
+
+EndCollection ==
+    /\ globalLock # NULL
+    /\ collecting = TRUE
+    /\ \* Clear root flags
+       inRoots' = [x \in Objects |->
+           IF x \in {r.obj : r \in mergedRoots} THEN FALSE ELSE inRoots[x]]
+    /\ mergedRoots' = <<>>
+    /\ collecting' = FALSE
+    /\ UNCHANGED <<edges, roots, rc, color, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, gcEnv, pendingWrites>>
+
+\* ============================================================================
+\* Mutator Actions
+\* ============================================================================
+
+\* Mutator can write at any time (graph updates are lock-free)
+\* The ATOMIC_RELEASE barrier ensures proper ordering
+\* ASSUMPTION: Users synchronize pointer assignments with locks, so oldVal always
+\* matches the current graph state (as read before the atomic store).
+\* This prevents races at the user level - the GC itself is lock-free.
+MutatorWrite(thread, destObj, destField, oldVal, newVal, desc) ==
+    \* ASSUMPTION: Users synchronize pointer assignments with locks, so oldVal always matches
+    \* the value read before the atomic store. This prevents races at the user level.
+    \* The precondition is enforced in the Next relation.
+    \* Phase 1: Atomic store (topology update) - ALWAYS happens first
+    /\ MutatorWriteAtomicStore(thread, destObj, destField, oldVal, newVal, desc)
+    \* Phase 2: RC buffering - happens if no overflow, otherwise overflow is handled separately
+    \* Note: In reality, if overflow happens, the thread blocks waiting for lock.
+    \* We model this as: atomic store happens, buffering is deferred (handled by merge actions).
+    /\ LET stripe == GetStripe(thread)
+          incOverflow == (newVal # NULL) /\ (toIncLen[stripe] >= QueueSize)
+          decOverflow == (oldVal # NULL) /\ (toDecLen[stripe] >= QueueSize)
+       IN
+       IF incOverflow \/ decOverflow
+       THEN \* Overflow: atomic store happened, but buffering is deferred
+            \* Buffers stay full, merge will happen when lock is available (via MutatorWriteMergeInc/Dec)
+            /\ UNCHANGED <<roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites>>
+       ELSE \* No overflow: buffer normally
+            /\ WriteBarrier(thread, destObj, destField, oldVal, newVal, desc)
+            /\ UNCHANGED <<roots, collecting, pendingWrites>>
+
+\* Stack root assignment: immediate RC increment (not buffered)
+\* When assigning val to a root variable named obj, we set roots[thread][val] = TRUE
+\* to indicate that thread has a stack reference to val
+\* Semantics: obj is root variable name, val is the object being assigned
+\* When val=NULL, obj was the old root value, so we decrement rc[obj]
+MutatorRootAssign(thread, obj, val) ==
+    /\ IF val # NULL
+       THEN /\ roots' = [roots EXCEPT ![thread][val] = TRUE]
+            /\ rc' = [rc EXCEPT ![val] = IF roots[thread][val] THEN @ ELSE @ + 1]  \* Increment only if not already a root
+       ELSE /\ roots' = [roots EXCEPT ![thread][obj] = FALSE]  \* Clear root when assigning NULL
+            /\ rc' = [rc EXCEPT ![obj] = IF roots[thread][obj] THEN @ - 1 ELSE @]  \* Decrement old root value
+    /\ edges' = edges
+    /\ color' = color
+    /\ inRoots' = inRoots
+    /\ toIncLen' = toIncLen
+    /\ toInc' = toInc
+    /\ toDecLen' = toDecLen
+    /\ toDec' = toDec
+    /\ lockInc' = lockInc
+    /\ lockDec' = lockDec
+    /\ globalLock' = globalLock
+    /\ mergedRoots' = mergedRoots
+    /\ collecting' = collecting
+    /\ gcEnv' = gcEnv
+    /\ pendingWrites' = pendingWrites
+
+\* ============================================================================
+\* Collector Actions
+\* ============================================================================
+
+\* Collector acquires global lock for entire collection cycle
+CollectorAcquireLock(thread) ==
+    /\ globalLock = NULL
+    /\ globalLock' = thread
+    /\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, mergedRoots, collecting, gcEnv, pendingWrites>>
+
+CollectorMerge ==
+    /\ globalLock # NULL
+    /\ MergePendingRoots
+
+CollectorStart ==
+    /\ globalLock # NULL
+    /\ StartCollection
+
+\* Mark all roots gray (trial deletion phase)
+CollectorMarkGray ==
+    /\ globalLock # NULL
+    /\ collecting = TRUE
+    /\ \E rootIdx \in DOMAIN mergedRoots:
+        LET root == mergedRoots[rootIdx]
+        IN MarkGray(root.obj, root.desc)
+
+\* Scan all roots (rescue phase)
+CollectorScan ==
+    /\ globalLock # NULL
+    /\ collecting = TRUE
+    /\ \E rootIdx \in DOMAIN mergedRoots:
+        LET root == mergedRoots[rootIdx]
+        IN Scan(root.obj, root.desc)
+
+\* Collect white/gray objects (free phase)
+CollectorCollect ==
+    /\ globalLock # NULL
+    /\ collecting = TRUE
+    /\ \E rootIdx \in DOMAIN mergedRoots, targetColor \in {colGray, colWhite}:
+        LET root == mergedRoots[rootIdx]
+        IN CollectColor(root.obj, root.desc, targetColor)
+
+CollectorEnd ==
+    /\ globalLock # NULL
+    /\ EndCollection
+
+CollectorReleaseLock(thread) ==
+    /\ globalLock = thread
+    /\ globalLock' = NULL
+    /\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, mergedRoots, collecting, gcEnv, pendingWrites>>
+
+\* ============================================================================
+\* Next State Relation
+\* ============================================================================
+
+Next ==
+    \/ \E thread \in Threads:
+         \E destObj \in Objects, oldVal, newVal \in Objects \cup {NULL}, desc \in ObjTypes:
+             \* Precondition: oldVal must match current graph state (user-level synchronization)
+             \* ASSUMPTION: Users synchronize pointer assignments with locks, so oldVal always matches
+             \* the value read before the atomic store. This prevents races at the user level.
+             /\ LET oldValMatches == CASE oldVal = NULL -> TRUE
+                                        [] oldVal \in Objects -> edges[destObj][oldVal]
+                                        [] OTHER -> FALSE
+                IN oldValMatches
+             /\ MutatorWrite(thread, destObj, "field", oldVal, newVal, desc)
+    \/ \E thread \in Threads:
+         \* Handle increment overflow: merge increment buffers when lock becomes available
+         MutatorWriteMergeInc(thread)
+    \/ \E thread \in Threads:
+         \* Handle decrement overflow: merge all buffers when lock becomes available
+         MutatorWriteMergeDec(thread)
+    \/ \E thread \in Threads:
+         \E obj, val \in Objects \cup {NULL}:
+             MutatorRootAssign(thread, obj, val)
+    \/ \E thread \in Threads:
+         CollectorAcquireLock(thread)
+    \/ CollectorMerge
+    \/ CollectorStart
+    \/ CollectorMarkGray
+    \/ CollectorScan
+    \/ CollectorCollect
+    \/ CollectorEnd
+    \/ \E thread \in Threads:
+         CollectorReleaseLock(thread)
+
+\* ============================================================================
+\* Initial State
+\* ============================================================================
+
+Init ==
+    /\ edges = [x \in Objects |->
+                [y \in Objects |->
+                    IF x = y THEN FALSE ELSE FALSE]]  \* Empty graph initially
+    /\ roots = [t \in Threads |->
+                [x \in Objects |->
+                    FALSE]]  \* No stack roots initially
+    /\ rc = [x \in Objects |->
+             0]  \* Zero reference counts
+    /\ color = [x \in Objects |->
+                colBlack]  \* All objects black initially
+    /\ inRoots = [x \in Objects |->
+                  FALSE]  \* No objects in roots array
+    /\ toIncLen = [s \in 0..(NumStripes-1) |->
+                   0]
+    /\ toInc = [s \in 0..(NumStripes-1) |->
+                <<>>]
+    /\ toDecLen = [s \in 0..(NumStripes-1) |->
+                   0]
+    /\ toDec = [s \in 0..(NumStripes-1) |->
+                <<>>]
+    /\ lockInc = [s \in 0..(NumStripes-1) |->
+                  NULL]
+    /\ lockDec = [s \in 0..(NumStripes-1) |->
+                  NULL]
+    /\ globalLock = NULL
+    /\ mergedRoots = <<>>
+    /\ collecting = FALSE
+    /\ gcEnv = [touched |-> 0, edges |-> 0, rcSum |-> 0, toFree |-> {}]
+    /\ pendingWrites = {}
+    /\ TypeOK
+
+\* ============================================================================
+\* Safety Properties
+\* ============================================================================
+
+\* Safety: Objects are only freed if they are unreachable from any thread's stack
+\*
+\* An object is reachable if:
+\*   - It is a direct stack root (roots[t][obj] = TRUE), OR
+\*   - There exists a path from a stack root to obj via heap edges
+\*
+\* Safety guarantee: If an object is reachable, then:
+\*   - It is not white (not marked for collection), OR
+\*   - It is in roots array (protected from collection), OR
+\*   - It is reachable from an object that will be rescued by scanBlack
+\*
+\* More precisely: Only closed cycles (zero external refs, unreachable) are freed.
+
+\* Helper: Compute next set of reachable objects (one step of transitive closure)
+ReachableStep(current) ==
+    current \cup UNION {{y \in Objects : edges[x][y]} : x \in current}
+
+\* Compute the set of all reachable objects using bounded iteration
+\* Since Objects is finite, we iterate at most Cardinality(Objects) times
+\* This computes the transitive closure of edges starting from stack roots
+\* We unroll the iteration explicitly to avoid recursion issues with TLC
+ReachableSet ==
+    LET StackRoots == {x \in Objects : \E t \in Threads : roots[t][x]}
+        Step1 == ReachableStep(StackRoots)
+        Step2 == ReachableStep(Step1)
+        Step3 == ReachableStep(Step2)
+        Step4 == ReachableStep(Step3)
+        \* Add more steps if needed for larger object sets
+        \* For small models (2 objects), 4 steps is sufficient
+    IN Step4
+
+\* Check if an object is reachable
+Reachable(obj) == obj \in ReachableSet
+
+\* Helper: Check if there's a path from 'from' to 'to'
+\* For small object sets, we check all possible paths by checking
+\* all combinations of intermediate objects
+\* Path of length 0: from = to
+\* Path of length 1: edges[from][to]
+\* Path of length 2: \E i1: edges[from][i1] /\ edges[i1][to]
+\* Path of length 3: \E i1, i2: edges[from][i1] /\ edges[i1][i2] /\ edges[i2][to]
+\* etc. up to Cardinality(Objects)
+HasPath(from, to) ==
+    \/ from = to
+    \/ edges[from][to]
+    \/ \E i1 \in Objects:
+         edges[from][i1] /\ (edges[i1][to] \/ \E i2 \in Objects:
+             edges[i1][i2] /\ (edges[i2][to] \/ \E i3 \in Objects:
+                 edges[i2][i3] /\ edges[i3][to]))
+
+\* Helper: Compute set of objects reachable from a given starting object
+\* Uses the same iterative approach as ReachableSet
+ReachableFrom(start) ==
+    LET Step1 == ReachableStep({start})
+        Step2 == ReachableStep(Step1)
+        Step3 == ReachableStep(Step2)
+        Step4 == ReachableStep(Step3)
+    IN Step4
+
+\* Safety: Reachable objects are never freed (remain white without being collected)
+\* A reachable object is safe if:
+\*   - It's not white (not marked for collection), OR
+\*   - It's in roots array (protected from collection), OR
+\*   - There exists a black object in ReachableSet such that obj is reachable from it
+\*     (the black object will be rescued by scanBlack, which rescues all white objects
+\*      reachable from black objects)
+Safety ==
+    \A obj \in Objects:
+        IF obj \in ReachableSet
+        THEN \/ color[obj] # colWhite  \* Not marked for collection
+             \/ inRoots[obj]  \* Protected in roots array
+             \/ \E blackObj \in ReachableSet:
+                  /\ color[blackObj] = colBlack  \* Black object will be rescued by scanBlack
+                  /\ obj \in ReachableFrom(blackObj)  \* obj is reachable from blackObj
+        ELSE TRUE  \* Unreachable objects may be freed (this is safe)
+
+\* Invariant: Reference counts match logical counts after merge
+\* (This is maintained by MergePendingRoots)
+\* Note: Between merge and collection, RC = logicalRC.
+\* During collection (after markGray), RC may be modified by trial deletion.
+\* RC may be inconsistent when:
+\*   - globalLock = NULL (buffered changes pending)
+\*   - globalLock # NULL but merge hasn't happened yet (buffers still have pending changes)
+\* RC must equal LogicalRC when:
+\*   - After merge (buffers are empty) and before collection starts
+RCInvariant ==
+    IF globalLock = NULL
+    THEN TRUE  \* Not in collection, RC may be inconsistent (buffered changes pending)
+    ELSE IF collecting = FALSE /\ \A s \in 0..(NumStripes-1): toIncLen[s] = 0 /\ toDecLen[s] = 0
+         THEN \A obj \in Objects: rc[obj] = LogicalRC(obj)  \* After merge, buffers empty, RC = logical RC
+         ELSE TRUE  \* During collection or before merge, RC may differ from logicalRC
+
+\* Invariant: Only closed cycles are collected
+\* (Objects with external refs are rescued by scanBlack)
+CycleInvariant ==
+    \A obj \in Objects:
+        IF color[obj] = colWhite /\ ~inRoots[obj]
+        THEN ExternalRC(obj) = 0
+        ELSE TRUE
+
+\* ============================================================================
+\* Specification
+\* ============================================================================
+
+Spec == Init /\ [][Next]_<<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites>>
+
+THEOREM Spec => []Safety
+THEOREM Spec => []RCInvariant
+THEOREM Spec => []CycleInvariant
+
+====
--- a/tests/align/talign.nim
+++ b/tests/align/talign.nim
@@ -1,5 +1,6 @@
 discard """
 ccodeCheck: "\\i @'NIM_ALIGN(128) NI mylocal1' .*"
+matrix: "--mm:refc -d:useGcAssert -d:useSysAssert; --mm:orc"
 targets: "c cpp"
 output: "align ok"
 """
@@ -67,3 +68,104 @@ block: # bug #22419

  f()()

+
+type Xxx = object
+  v {.align: 128.}: byte
+
+type Yyy = object
+  v: byte
+  v2: Xxx
+
+for i in 0..<3:
+  let x = new Yyy
+  # echo "addr v2.v:", cast[uint](addr x.v2.v)
+  doAssert cast[uint](addr x.v2.v) mod 128 == 0
+
+let m = new Yyy
+m.v2.v = 42
+doAssert m.v2.v == 42
+m.v = 7
+doAssert m.v == 7
+
+
+type
+  MyType16 = object
+    a {.align(16).}: int
+
+
+var x: array[10, ref MyType16]
+for q in 0..500:
+  for i in 0..<x.len:
+    new x[i]
+    x[i].a = q
+    doAssert(cast[int](x[i]) mod alignof(MyType16) == 0)
+
+type
+  MyType32  = object
+    a{.align(32).}: int
+
+var y: array[10, ref MyType32]
+for q in 0..500:
+  for i in 0..<y.len:
+    new y[i]
+    y[i].a = q
+    doAssert(cast[int](y[i]) mod alignof(MyType32) == 0)
+
+# Additional tests: allocate custom aligned objects using `new`
+type
+  MyType64 = object
+    a{.align(64).}: int
+
+var z: array[10, ref MyType64]
+for q in 0..500:
+  for i in 0..<z.len:
+    new z[i]
+    z[i].a = q
+    doAssert(cast[int](z[i]) mod alignof(MyType64) == 0)
+
+type
+  MyType128 = object
+    a{.align(128).}: int
+
+var w: array[10, ref MyType128]
+for q in 0..500:
+  for i in 0..<w.len:
+    new w[i]
+    w[i].a = q
+    doAssert(cast[int](w[i]) mod alignof(MyType128) == 0)
+
+# Nested aligned-object tests
+type
+  Inner128 = object
+    v {.align(128).}: byte
+
+  OuterWithInner = object
+    prefix: int
+    inner: Inner128
+
+var outerArr: array[8, ref OuterWithInner]
+for q in 0..200:
+  for i in 0..<outerArr.len:
+    new outerArr[i]
+    # write to inner to ensure it's allocated
+    outerArr[i].inner.v = cast[byte](q and 0xFF)
+    doAssert(cast[uint](addr outerArr[i].inner) mod uint(alignof(Inner128)) == 0)
+
+# Nested two-level alignment
+type
+  DeepInner = object
+    b {.align(128).}: int
+
+  Mid = object
+    di: DeepInner
+
+  Top = object
+    m: Mid
+
+var topArr: array[4, ref Top]
+for q in 0..100:
+  for i in 0..<topArr.len:
+    new topArr[i]
+    topArr[i].m.di.b = q
+    doAssert(cast[uint](addr topArr[i].m.di) mod uint(alignof(DeepInner)) == 0)
+
--- a/tests/ccgbugs2/tcodegen.nim
+++ b/tests/ccgbugs2/tcodegen.nim
@@ -56,3 +56,22 @@ proc main = # bug #24677
  for NDEBUG in 0..2:
    doAssert NDEBUG == NDEBUG
 main()
+
+block: # importc type inheritance
+  type
+    A {.inheritable, pure, bycopy, importc: "int".} = object
+    B {.importc: "int", bycopy.} = object of A
+
+  {.emit: """
+  int foo(int a) {
+    return 123;
+  }
+  """.}
+
+  proc foo(a: A): B {.importc, nodecl.}
+
+  var a: A
+  var b = foo(a)
+  doAssert(cast[cint](b) == 123)
+  var c = foo(b)
+  doAssert(cast[cint](c) == 123)
--- a/tests/destructor/tcustomseqs.nim
+++ b/tests/destructor/tcustomseqs.nim
@@ -40,7 +40,7 @@ proc `=destroy`*[T](x: var myseq[T]) =
    x.len = 0
    x.cap = 0

-proc `=`*[T](a: var myseq[T]; b: myseq[T]) =
+proc `=copy`*[T](a: var myseq[T]; b: myseq[T]) =
  if a.data == b.data: return
  if a.data != nil:
    `=destroy`(a)
@@ -66,6 +66,11 @@ proc `=sink`*[T](a: var myseq[T]; b: myseq[T]) =
  a.cap = b.cap
  a.data = b.data

+proc `=wasMoved`*[T](a: var myseq[T]) =
+  a.data = nil
+  a.len = 0
+  a.cap = 0
+
 proc resize[T](s: var myseq[T]) =
  if s.cap == 0: s.cap = 8
  else: s.cap = (s.cap * 3) shr 1
@@ -118,7 +123,7 @@ template `[]=`*[T](x: myseq[T]; i: Natural; y: T) =
 proc createSeq*[T](elems: varargs[T]): myseq[T] =
  result.cap = elems.len
  result.len = elems.len
-  result.data = cast[type(result.data)](alloc(result.cap * sizeof(T)))
+  result.data = cast[type(result.data)](alloc0(result.cap * sizeof(T)))
  inc allocCount
  when supportsCopyMem(T):
    copyMem(result.data, addr(elems[0]), result.cap * sizeof(T))
--- a/tests/destructor/tdup_from_copy.nim
+++ b/tests/destructor/tdup_from_copy.nim
@@ -0,0 +1,44 @@
+discard """
+  output: '''
+copy!
+copy!
+3
+2
+'''
+"""
+
+type Foo = distinct int
+
+var counter = 0
+
+proc `=destroy`(pkt: var Foo) =
+  if cast[int](pkt) != 0:
+    echo cast[int](pkt)
+
+proc `=copy`(a: var Foo, b: Foo) =
+  if cast[int](a) == cast[int](b):
+    return
+
+  `=destroy`(a)
+  if cast[int](b) == 0:
+    zeroMem(addr a, sizeof(Foo))
+  else:
+    counter += 1
+    copyMem(addr a, addr counter, sizeof(Foo))
+    echo "copy!"
+
+proc makeFoo(): Foo =
+  counter += 1
+  cast[Foo](counter)
+
+
+type Bar = object
+  val: Foo
+
+
+proc consume(x: sink Bar) =
+  discard
+
+let x = Bar(val: makeFoo())
+consume(x)
+discard x
--- a/tests/gc/cyclecollector.nim
+++ b/tests/gc/cyclecollector.nim
@@ -12,7 +12,7 @@ type
 proc createCycle(leaf: string): Node =
  new result
  result.a = result
-  when defined(gcArc) or defined(gcOrc):
+  when defined(gcArc) or defined(gcOrc) or defined(gcYrc):
    result.leaf = leaf
  else:
    shallowCopy result.leaf, leaf
--- a/tests/gc/thavlak.nim
+++ b/tests/gc/thavlak.nim
@@ -437,6 +437,6 @@ proc main =

 let mem = getOccupiedMem()
 main()
-when defined(gcOrc):
+when defined(gcOrc) or defined(gcYrc):
  GC_fullCollect()
  doAssert getOccupiedMem() == mem
--- a/tests/generics/tgenerics_issues.nim
+++ b/tests/generics/tgenerics_issues.nim
@@ -892,3 +892,13 @@ block: # https://github.com/nim-lang/Nim/issues/20416
  proc p2[T](sg:Container[T]) = discard
  var v : Container[int]
  p2(v)
+
+block: # issue #25494
+  proc foo[T: enum](s = {T.low..T.high}) =
+    discard
+
+  type
+    MyEnum = enum
+      a, b, c
+
+  foo[MyEnum]()
--- a/tests/misc/taddr.nim
+++ b/tests/misc/taddr.nim
@@ -32,7 +32,7 @@ doAssert objDeref.x == 42

 # String tests
 obj.s = "lorem ipsum dolor sit amet"
-when defined(gcArc) or defined(gcOrc):
+when defined(gcArc) or defined(gcOrc) or defined(gcYrc):
  prepareMutation(obj.s)


@@ -237,7 +237,7 @@ block: # bug #15939
    doAssert bar == "foo"

 template prepareMutationForOrc(x: string) =
-  when defined(gcArc) or defined(gcOrc):
+  when defined(gcArc) or defined(gcOrc) or defined(gcYrc):
    when nimvm:
      discard
    else:
--- a/tests/objects/tobject_default_value.nim
+++ b/tests/objects/tobject_default_value.nim
@@ -239,7 +239,7 @@ template main {.dirty.} =
    # todo
    discard "fixme"
  else:
-    when defined(gcArc) or defined(gcOrc):
+    when defined(gcArc) or defined(gcOrc) or defined(gcYrc):
      block: #seq
        var x = newSeq[Object](10)
        let y = x[0]
@@ -375,7 +375,7 @@ template main {.dirty.} =
    type
      Color = enum
        Red, Blue, Yellow
-  
+
    type
      ObjectVarint3 = object
        case kind: Color = Blue
@@ -663,7 +663,7 @@ template main {.dirty.} =

      when not(T is void):
        v.vResultPrivate
-        
+
    type R = Result[int, string]

    proc testAssignResult() =
--- a/tests/stdlib/mgenast.nim
+++ b/tests/stdlib/mgenast.nim
@@ -31,7 +31,7 @@ macro bindme6UseExpose*(): untyped =
  genAst:
    var tst = "sometext"
    var ss = newStringStream("anothertext")
-    when defined(gcArc) or defined(gcOrc):
+    when defined(gcArc) or defined(gcOrc) or defined(gcYrc):
      prepareMutation(tst)
    writeData(ss, tst[0].addr, 2)
    discard readData(ss, tst[0].addr, 2)
@@ -42,7 +42,7 @@ macro bindme6UseExposeFalse*(): untyped =
  genAstOpt({kDirtyTemplate}, newStringStream, writeData, readData):
    var tst = "sometext"
    var ss = newStringStream("anothertext")
-    when defined(gcArc) or defined(gcOrc):
+    when defined(gcArc) or defined(gcOrc) or defined(gcYrc):
      prepareMutation(tst)
    writeData(ss, tst[0].addr, 2)
    discard readData(ss, tst[0].addr, 2)
--- a/tests/typerel/t25340.nim
+++ b/tests/typerel/t25340.nim
@@ -0,0 +1,16 @@
+
+type
+  Foo[T] = object of T
+
+template inheritanceCheck(a, b: untyped) =
+  doAssert a is b
+  doAssert b isnot a
+
+inheritanceCheck Foo[RootObj], RootObj
+
+inheritanceCheck Foo[Foo[RootObj]], RootObj
+inheritanceCheck Foo[Foo[RootObj]], Foo[RootObj]
+
+inheritanceCheck Foo[Foo[Foo[RootObj]]], RootObj
+inheritanceCheck Foo[Foo[Foo[RootObj]]], Foo[RootObj]
+inheritanceCheck Foo[Foo[Foo[RootObj]]], Foo[Foo[RootObj]]
--- a/tests/yrc/tyrc_cas_race.nim
+++ b/tests/yrc/tyrc_cas_race.nim
@@ -0,0 +1,98 @@
+discard """
+  cmd: "nim c --mm:yrc -d:useMalloc --threads:on $file"
+  output: "ok"
+  valgrind: "leaks"
+  disabled: "windows"
+  disabled: "freebsd"
+  disabled: "openbsd"
+"""
+
+# Test concurrent traversal and mutation of a shared cyclic list under YRC.
+# Multiple threads race to replace nodes using a lock for synchronization.
+# This exercises YRC's write barrier and cycle collection under contention.
+
+import std/locks
+
+type
+  Node = ref object
+    value: int
+    next: Node
+
+proc newCycle(start, count: int): Node =
+  result = Node(value: start)
+  var cur = result
+  for i in 1..<count:
+    cur.next = Node(value: start + i)
+    cur = cur.next
+  cur.next = result  # close the cycle
+
+proc sumCycle(head: Node; count: int): int =
+  var cur = head
+  for i in 0..<count:
+    result += cur.value
+    cur = cur.next
+
+const
+  NumThreads = 4
+  CycleLen = 6
+  Iterations = 50
+
+var
+  shared: Node
+  sharedLock: Lock
+  threads: array[NumThreads, Thread[int]]
+  wins: array[NumThreads, int]
+
+proc worker(id: int) {.thread.} =
+  {.cast(gcsafe).}:
+    for iter in 0..<Iterations:
+      # Under the lock, walk the shared list and replace a node's next pointer
+      withLock sharedLock:
+        var cur = shared
+        if cur == nil: continue
+        for step in 0..<CycleLen:
+          let nxt = cur.next
+          if nxt == nil: break
+          # Replace cur.next with a fresh node that points to nxt.next
+          let replacement = Node(value: id * 1000 + iter, next: nxt.next)
+          cur.next = replacement
+          wins[id] += 1
+          cur = cur.next
+          if cur == nil: break
+
+      # Outside the lock, create a local cycle to exercise the collector
+      let local = newCycle(id * 100 + iter, 3)
+      discard sumCycle(local, 3)
+
+# Create initial shared cyclic list: 0 -> 1 -> 2 -> 3 -> 4 -> 5 -> 0
+initLock(sharedLock)
+shared = newCycle(0, CycleLen)
+
+for i in 0..<NumThreads:
+  createThread(threads[i], worker, i)
+
+for i in 0..<NumThreads:
+  joinThread(threads[i])
+
+# Verify: the list is still traversable (no crashes, no dangling pointers).
+var totalWins = 0
+for i in 0..<NumThreads:
+  totalWins += wins[i]
+
+# Walk the list to verify it's still a valid cycle (or chain)
+var cur = shared
+var seen = 0
+var maxSteps = CycleLen * 3  # generous bound
+while cur != nil and seen < maxSteps:
+  seen += 1
+  cur = cur.next
+  if cur == shared: break  # completed the cycle
+
+shared = nil
+GC_fullCollect()
+deinitLock(sharedLock)
+
+if totalWins > 0 and seen > 0:
+  echo "ok"
+else:
+  echo "FAIL: wins=", totalWins, " seen=", seen
--- a/tests/yrc/tyrc_shared_cycle.nim
+++ b/tests/yrc/tyrc_shared_cycle.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"
+"""
+
+# Test sharing a cyclic list between threads under YRC.
+
+type
+  Node = ref object
+    value: int
+    next: Node
+
+proc newCycle(start, count: int): Node =
+  ## Create a cyclic linked list: start -> start+1 -> ... -> start+count-1 -> start
+  result = Node(value: start)
+  var cur = result
+  for i in 1..<count:
+    cur.next = Node(value: start + i)
+    cur = cur.next
+  cur.next = result  # close the cycle
+
+proc sumCycle(head: Node; count: int): int =
+  var cur = head
+  for i in 0..<count:
+    result += cur.value
+    cur = cur.next
+
+const
+  NumThreads = 4
+  NodesPerCycle = 5
+
+var
+  shared: Node
+  threads: array[NumThreads, Thread[int]]
+  results: array[NumThreads, int]
+
+proc worker(id: int) {.thread.} =
+  # Each thread reads the shared cycle and computes a sum.
+  # Also creates its own local cycle to exercise the collector.
+  {.cast(gcsafe).}:
+    let local = newCycle(id * 100, NodesPerCycle)
+    let localSum = sumCycle(local, NodesPerCycle)
+
+    let sharedSum = sumCycle(shared, NodesPerCycle)
+    results[id] = sharedSum + localSum
+
+# Create a shared cyclic list: 0 -> 1 -> 2 -> 3 -> 4 -> 0
+shared = newCycle(0, NodesPerCycle)
+let expectedSharedSum = 0 + 1 + 2 + 3 + 4  # = 10
+
+for i in 0..<NumThreads:
+  createThread(threads[i], worker, i)
+
+for i in 0..<NumThreads:
+  joinThread(threads[i])
+
+var allOk = true
+for i in 0..<NumThreads:
+  let expectedLocal = i * 100 * NodesPerCycle + (NodesPerCycle * (NodesPerCycle - 1) div 2)
+    # sum of id*100, id*100+1, ..., id*100+4
+  let expected = expectedSharedSum + expectedLocal
+  if results[i] != expected:
+    echo "FAIL thread ", i, ": got ", results[i], " expected ", expected
+    allOk = false
+
+shared = nil  # drop the shared cycle, collector should reclaim it
+GC_fullCollect()
+
+if allOk:
+  echo "ok"
Author	SHA1	Message	Date
araq	4b9f345551	Fix closure environment node sharing in lambda lifting When makeClosure creates multiple closure instances, it was reusing the same env node, causing DFA tracking issues. Each closure construction now gets a fresh nkSym node copy to avoid node identity problems. This fixes hash stability and prevents premature environment moves when closures are shared (e.g., let closure2 = closure1).	2026-02-14 18:23:00 +01:00
Yuriy Glukhov	937e647f4f	Importc codegen fix (#25511 ) This fixes two issues with impotc'ed types. 1. Passing an importc'ed inherited object to where superclass is expected emitted `v.Sup` previously. Now it emits `v`, similar to cpp codegen. 2. Casting between different nim types that resolve to the same C type previously was done like `(T)&v`, now it is just `v`.	2026-02-13 13:29:01 +01:00
Andreas Rumpf	b41049988f	attempt to fix final issue with Nim's multi-threaded allocator (#25513 )	2026-02-13 11:53:17 +01:00
Andreas Rumpf	04933b773a	YRC: bugfixes (#25512 )	2026-02-12 13:29:22 +01:00
Andreas Rumpf	5fa11c5686	YRC: bugfixes (#25504 )	2026-02-11 17:45:40 +01:00
ringabout	94008531c1	fixes #25457 ; make rawAlloc support alignment (#25476 ) fixes https://github.com/nim-lang/Nim/issues/25457 Small chunks allocate memory in fixed-size cells. Each cell is positioned at exact multiples of the cell size from the chunk's data start, which makes it much harder to support alignment ```nim sysAssert c.size == size, "rawAlloc 6" if c.freeList == nil: sysAssert(c.acc.int + smallChunkOverhead() + size <= SmallChunkSize, "rawAlloc 7") result = cast[pointer](cast[int](addr(c.data)) +% c.acc.int) inc(c.acc, size) ``` See also https://github.com/nim-lang/Nim/pull/12926 While using big trunk, each allocation gets its own chunk	2026-02-11 11:33:31 +01:00
ringabout	c346a2b228	fixes #25464 ; infer =dup for distinct types (#25501 ) fixes #25464 --------- Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>	2026-02-11 10:46:34 +01:00
Andreas Rumpf	f62669a5d5	Yrc typos and omissions (#25500 )	2026-02-10 13:21:35 +01:00
Andreas Rumpf	a690a9ac90	YRC: threadsafe cycle collection for Nim (#25495 ) First performance numbers: time tests/arc/torcbench -- YRC true peak memory: true real 0m0,163s user 0m0,161s sys 0m0,002s time tests/arc/torcbench -- ORC true peak memory: true real 0m0,107s user 0m0,104s sys 0m0,003s So it's 1.6x slower. But it's threadsafe and provably correct. (Lean and model checking via TLA+ used.) Of course there is always the chance that the implementation is wrong and doesn't match the model.	2026-02-10 00:04:11 +01:00
lit	9225d9e9e6	fixes #25490 ; Remove unused gEnv & env from `main` func (#25497 ) closes #25490	2026-02-09 17:34:44 +01:00
ringabout	ae5f864bff	fixes #25494 ; [regression] Crash on enum ranges as default parameters in generic procs (#25496 ) fixes #25494;	2026-02-09 11:50:45 +01:00
ringabout	513c9aa69a	fixes #25488 ; Strings can be compared against nil (#25489 ) fixes #25488 ref https://github.com/nim-lang/Nim/pull/20222	2026-02-07 20:46:50 +01:00
ringabout	12a2333817	fixes #25464 ; gives a deprecated warning when `=dup` is not provided while there being a custom `=copy` (#25485 ) Gives a deprecated warning to keep backwards compatibility fixes #25464	2026-02-06 02:19:46 +01:00
Yuriy Glukhov	296b2789b5	Fixes #25340 (#25389 )	2026-02-06 00:54:04 +01:00