@@ -5,37 +5,41 @@
 This module is pure **data + algorithm**: it computes a Method Ownership Summary
 (MOS) for each first-party method from per-method *local evidence* (a "skeleton"
 of what a body directly does with each disposable parameter and what it returns),
-resolving the parts that depend on other methods' summaries via a **depth-capped
-bottom-up resolution** over the call graph.
-
-D5.0 deliberately does **nothing** to findings — no extractor wiring, no
-behaviour change. It defines the summary vocabulary and the solver so the lattice
-can be unit-tested in pure Python (the synthetic-flow discipline, lifted to the
-effect level). Lowering a summary into the core's `consume`/`borrow`/`acquire`
-vocabulary is D5.1+; the wrapper/alias (`aliasOf`) obligation-identity model is
-D5.4 (see the note's §11).
-
-The skeleton is the extractor-facing input; here it is hand-authored in tests.
+resolving the parts that depend on other methods' summaries by a **summary
+fixpoint over the strongly-connected-component condensation** of the call graph.
+
+The summary is *context-insensitive*: each method has exactly one MOS, independent
+of who calls it or how deep the call sits. That is what makes the computation both
+linear (each method resolved once and reused — no per-call re-descent) and exact
+on recursion: cycles are solved to their least fixpoint on the four-point lattice
+rather than truncated. There is **no depth cap** — the SCC condensation bounds the
+work without one (an earlier slice capped the recursive descent at depth 3 purely
+to dodge the exponential a memo-less re-descent would otherwise hit on diamond call
+graphs; the condensation removes both the blowup and the cap-induced false
+`unknown`s on deep chains).
+
+Lowering a summary into the core's `consume`/`borrow`/`acquire` vocabulary lives in
+the bridge (`ownir.py`, D5.1+: `must`→consume, `no`→borrow, `may`/`unknown`→plain);
+the wrapper/alias (`aliasOf`) obligation-identity model is D5.4. The skeleton is the
+extractor-facing input; here it is hand-authored in tests.
 
 Precision note: a parameter is reported `must`-transfer only when ownership leaves
-the caller on **every** normal-return path the skeleton lists. A recursive forward
-edge contributes *no* transfer evidence (the cycle is broken at `no`), and a chain
-deeper than the cap, or a forward to an unsummarized (extern) callee, degrades to
-`unknown` — never to a guessed `must`. That keeps the project's precision-first
-stance: we only ever *claim* transfer when we can prove it.
+the caller on **every** normal-return path. The fixpoint seeds each recursive edge
+at the lattice bottom (⊥, "no evidence yet") rather than at a spurious `no`, so a
+method that disposes on its base case and recurses otherwise resolves to `must`
+(every *terminating* path disposes), and mutual recursion that never disposes
+settles at `no`. A forward to an unsummarized (extern) callee is the only residual
+`unknown`, and `solve_with_log` surfaces every such boundary — never a guessed
+`must`. That keeps the project's precision-first stance: we only ever *claim*
+transfer when we can prove it.
 """
 
 from __future__ import annotations
 
-from collections.abc import Iterable
+from collections.abc import Iterable, Iterator
 from dataclasses import dataclass, field
 from enum import StrEnum
 
-# Default interprocedural forward-chain depth, matching CA2000's
-# `max_interprocedural_method_call_chain` default. Beyond it, a forward degrades
-# to `unknown` (and is logged) rather than spending unbounded work.
-DEFAULT_CAP = 3
-
 
 class Transfer(StrEnum):
     """Did ownership of a disposable parameter leave the caller?
@@ -147,90 +151,102 @@ def to_dict(self) -> dict[str, object]:
         }
 
 
-def _resolve_param(key: str, i: int, depth: int, stack: frozenset[str],
-                   cap: int, sk: dict[str, MethodSkeleton],
-                   capped: list[str]) -> Transfer:
-    skel = sk.get(key)
-    if skel is None:
-        return Transfer.UNKNOWN
-    # `i` is the callee's *logical* parameter index (`ParamSkeleton.index`), which
-    # need not equal the tuple offset — a skeleton may list only the disposable /
-    # interesting params, so a wrapper `Create(cmd, reader)` can carry just index 1.
-    # Resolve by `.index`, never by position.
-    p = next((q for q in skel.params if q.index == i), None)
-    if p is None:
-        return Transfer.UNKNOWN
-    if not p.disposable:
-        return Transfer.NO
-    if not p.paths:
-        return Transfer.NO  # nothing happens to it -> kept (borrowed)
-    verdict: Transfer | None = None
-    for a in p.paths:
-        verdict = _path_verdict(a, depth, stack, cap, sk, capped) if verdict is None \
-            else join(verdict, _path_verdict(a, depth, stack, cap, sk, capped))
-    return verdict if verdict is not None else Transfer.NO
-
-
-def _path_verdict(a: PathAction, depth: int, stack: frozenset[str], cap: int,
-                  sk: dict[str, MethodSkeleton], capped: list[str]) -> Transfer:
-    if a.kind in ("dispose", "adopt", "return"):
-        return Transfer.MUST  # ownership left the caller on this path
-    if a.kind == "borrow":
-        return Transfer.NO
-    if a.kind == "forward":
-        if a.callee not in sk:
-            return Transfer.UNKNOWN  # extern / unsummarized callee
-        if depth + 1 >= cap:
-            capped.append(f"{a.callee}#{a.arg} (depth {depth + 1} >= cap {cap})")
-            return Transfer.UNKNOWN
-        if a.callee in stack:
-            return Transfer.NO  # recursion: this edge carries no transfer evidence
-        return _resolve_param(a.callee, a.arg, depth + 1, stack | {a.callee},
-                              cap, sk, capped)
-    return Transfer.UNKNOWN
-
-
-def _resolve_return(key: str, depth: int, stack: frozenset[str], cap: int,
-                    sk: dict[str, MethodSkeleton], capped: list[str]) -> str:
-    skel = sk.get(key)
-    if skel is None:
-        return "unknown"
-    r = skel.ret
-    if r.kind == "fresh":
-        return "fresh"
-    if r.kind == "aliasOf":
-        return f"aliasOf:{r.arg}"
-    if r.kind == "aliased":
-        return "aliased"
-    if r.kind == "forward":
-        if r.callee not in sk:
-            return "unknown"
-        if depth + 1 >= cap:
-            capped.append(f"return {r.callee} (depth {depth + 1} >= cap {cap})")
-            return "unknown"
-        if r.callee in stack:
-            return "unknown"
-        inner = _resolve_return(r.callee, depth + 1, stack | {r.callee}, cap, sk, capped)
-        if inner.startswith("aliasOf:"):
-            # `inner` aliases one of the *callee's* params; remapping it to one of
-            # OUR args needs the call's argument mapping, which the skeleton does not
-            # carry yet (it arrives with the obligation-identity model in D5.4). Until
-            # then, never propagate a wrong index — degrade to unknown (precision-safe:
-            # nothing is acquired/aliased at lowering).
-            return "unknown"
-        return inner  # fresh / aliased / none / unknown propagate as-is
-    if r.kind == "none":
-        return "none"  # explicit no-owned-return
-    return "unknown"  # an unrecognised kind fails closed, never silently "none"
-
-
-def solve_with_log(skeletons: Iterable[MethodSkeleton], *,
-                   cap: int = DEFAULT_CAP) -> tuple[dict[str, MethodSummary], list[str]]:
-    """Resolve every method's MOS from its skeleton plus its callees' skeletons.
-
-    Returns (summaries-by-key, capped-log). The log names every forward that hit
-    the depth cap, so a run can surface what it gave up on (no silent
-    truncation)."""
+# A parameter is resolved by `.index` (its logical `ParamSkeleton.index`), never by
+# tuple offset: a skeleton may list only the disposable/interesting params, so a
+# wrapper `Create(cmd, reader)` can carry just index 1.
+ParamKey = tuple[str, int]  # (method key, logical parameter index)
+
+# `None` is the lattice bottom ⊥ ("no evidence yet") used only as the fixpoint seed
+# on a recursive edge. It never escapes a solved summary — it is mapped to `no` at
+# finalization (a parameter nothing demonstrably consumes is kept = borrowed).
+def _join_opt(a: Transfer | None, b: Transfer | None) -> Transfer | None:
+    """`join` lifted to the bottom-extended lattice: ⊥ (None) is the identity."""
+    if a is None:
+        return b
+    if b is None:
+        return a
+    return join(a, b)
+
+
+def _sccs(adj: dict[str, set[str]]) -> list[list[str]]:
+    """Tarjan's SCCs, returned bottom-up (every component precedes its callers).
+
+    Iterative (no Python recursion limit on deep call graphs). Tarjan emits each
+    component only after all components it depends on, so the natural output order
+    is exactly the reverse-topological order the summary fixpoint wants: a callee's
+    summary is final before any caller reads it; only same-SCC callees are still
+    mid-iteration. Adjacency is sorted so the result (and the cap-free log) is
+    deterministic regardless of input ordering."""
+    index: dict[str, int] = {}
+    low: dict[str, int] = {}
+    on_stack: set[str] = set()
+    stack: list[str] = []
+    out: list[list[str]] = []
+    counter = 0
+    for root in adj:
+        if root in index:
+            continue
+        index[root] = low[root] = counter
+        counter += 1
+        stack.append(root)
+        on_stack.add(root)
+        work: list[tuple[str, Iterator[str]]] = [(root, iter(sorted(adj[root])))]
+        while work:
+            node, it = work[-1]
+            descended = False
+            for w in it:  # the iterator is stored in `work`, so it resumes here
+                if w not in index:
+                    index[w] = low[w] = counter
+                    counter += 1
+                    stack.append(w)
+                    on_stack.add(w)
+                    work.append((w, iter(sorted(adj[w]))))
+                    descended = True
+                    break
+                if w in on_stack:
+                    low[node] = min(low[node], index[w])
+            if descended:
+                continue
+            if low[node] == index[node]:  # component root
+                comp: list[str] = []
+                while True:
+                    x = stack.pop()
+                    on_stack.discard(x)
+                    comp.append(x)
+                    if x == node:
+                        break
+                out.append(comp)
+            work.pop()
+            if work:  # propagate this node's low-link up to its DFS parent
+                parent = work[-1][0]
+                low[parent] = min(low[parent], low[node])
+    return out
+
+
+def _call_graph(sk: dict[str, MethodSkeleton]) -> dict[str, set[str]]:
+    """Dependency edges M -> callees whose summaries M's summary reads: every
+    first-party callee a param forwards to, plus a forwarded return target."""
+    adj: dict[str, set[str]] = {k: set() for k in sk}
+    for k, skel in sk.items():
+        deps = adj[k]
+        for p in skel.params:
+            for a in p.paths:
+                if a.kind == "forward" and a.callee in sk:
+                    deps.add(a.callee)
+        if skel.ret.kind == "forward" and skel.ret.callee in sk:
+            deps.add(skel.ret.callee)
+    return adj
+
+
+def solve_with_log(skeletons: Iterable[MethodSkeleton]) -> tuple[
+        dict[str, MethodSummary], list[str]]:
+    """Resolve every method's MOS by a summary fixpoint over the call graph's SCC
+    condensation.
+
+    Returns (summaries-by-key, unresolved-log). The log names every forward that
+    crosses an extern (unsummarized) boundary — the only place a transfer or return
+    degrades to `unknown`. There is no depth cap and so no silent truncation: the
+    condensation makes the work linear, and recursion is solved, not cut off."""
     sk: dict[str, MethodSkeleton] = {}
     for s in skeletons:
         if s.key in sk:
@@ -239,24 +255,118 @@ def solve_with_log(skeletons: Iterable[MethodSkeleton], *,
             # depend on input order — fail fast instead.
             raise ValueError(f"duplicate MethodSkeleton key: {s.key}")
         sk[s.key] = s
-    capped: list[str] = []
+
+    unresolved: set[str] = set()
+    param_val: dict[ParamKey, Transfer] = {}  # finalized disposable-param transfers
+
+    def lookup(callee: str, arg: int, cur: dict[ParamKey, Transfer | None]) -> Transfer | None:
+        """The current transfer of callee param `arg` (resolve by `.index`): a final
+        value for a callee in a lower SCC, the live iterate for one in the current
+        SCC (possibly ⊥), `no` for a non-disposable, `unknown` past an extern edge."""
+        skel = sk.get(callee)
+        if skel is None:
+            unresolved.add(f"{callee}#{arg} (extern, no summary)")
+            return Transfer.UNKNOWN
+        p = next((q for q in skel.params if q.index == arg), None)
+        if p is None:
+            return Transfer.UNKNOWN  # callee has no such logical param
+        if not p.disposable:
+            return Transfer.NO
+        keyp = (callee, arg)
+        if keyp in param_val:
+            return param_val[keyp]
+        if keyp in cur:
+            return cur[keyp]  # same-SCC member, mid-fixpoint (may be ⊥)
+        return Transfer.UNKNOWN  # unreachable under a correct topo order; fail closed
+
+    def contrib(a: PathAction, cur: dict[ParamKey, Transfer | None]) -> Transfer | None:
+        if a.kind in ("dispose", "adopt", "return"):
+            return Transfer.MUST  # ownership left the caller on this path
+        if a.kind == "borrow":
+            return Transfer.NO
+        if a.kind == "forward":
+            return lookup(a.callee, a.arg, cur)
+        return Transfer.UNKNOWN
+
+    def transfer_of(key: str, index: int,
+                    cur: dict[ParamKey, Transfer | None]) -> Transfer | None:
+        p = next(q for q in sk[key].params if q.index == index)
+        if not p.paths:
+            return Transfer.NO  # nothing happens to it -> kept (borrowed)
+        acc: Transfer | None = None
+        for a in p.paths:
+            acc = _join_opt(acc, contrib(a, cur))
+        return acc
+
+    # --- param transfers: bottom-up, per-SCC least fixpoint on the lattice -------
+    for comp in _sccs(_call_graph(sk)):
+        members: list[ParamKey] = [
+            (k, p.index) for k in comp for p in sk[k].params if p.disposable
+        ]
+        if not members:
+            continue
+        cur: dict[ParamKey, Transfer | None] = dict.fromkeys(members)  # seed ⊥ (None)
+        changed = True
+        while changed:  # monotone ascent on a height-3 lattice: converges fast
+            changed = False
+            for m in members:
+                new = transfer_of(m[0], m[1], cur)
+                if new != cur[m]:
+                    cur[m] = new
+                    changed = True
+        for m in members:  # ⊥ (no evidence) finalizes as `no` (kept/borrowed)
+            v = cur[m]
+            param_val[m] = v if v is not None else Transfer.NO
+
+    # --- returns: a memoized, cycle-safe chase along forward-return edges --------
+    ret_val: dict[str, str] = {}
+
+    def resolve_return(key: str, visiting: frozenset[str]) -> str:
+        if key in ret_val:
+            return ret_val[key]  # context-insensitive: a return has one forward target
+        r = sk[key].ret
+        if r.kind == "fresh":
+            v = "fresh"
+        elif r.kind == "aliasOf":
+            v = f"aliasOf:{r.arg}"
+        elif r.kind == "aliased":
+            v = "aliased"
+        elif r.kind == "none":
+            v = "none"  # explicit no-owned-return
+        elif r.kind == "forward":
+            if r.callee not in sk:
+                unresolved.add(f"return {r.callee} (extern, no summary)")
+                v = "unknown"
+            elif r.callee in visiting:
+                v = "unknown"  # return-forward cycle: no ground to stand on
+            else:
+                inner = resolve_return(r.callee, visiting | {key})
+                # `inner` aliasOf:<i> aliases one of the *callee's* params; remapping it
+                # to OUR args needs the call's argument mapping, which the skeleton does
+                # not carry yet (the obligation-identity model, D5.4). Never propagate a
+                # wrong index — degrade to unknown (precision-safe: nothing aliased at
+                # lowering). fresh / aliased / none / unknown propagate as-is.
+                v = "unknown" if inner.startswith("aliasOf:") else inner
+        else:
+            v = "unknown"  # an unrecognised kind fails closed, never silently "none"
+        ret_val[key] = v
+        return v
+
     out: dict[str, MethodSummary] = {}
     for key, skel in sk.items():
         params = tuple(
             ParamSummary(
                 p.index, p.name, p.disposable,
-                _resolve_param(key, p.index, 0, frozenset({key}), cap, sk, capped)
-                if p.disposable else Transfer.NO,
+                param_val.get((key, p.index), Transfer.NO) if p.disposable else Transfer.NO,
                 p.escapes,
             )
             for p in skel.params
         )
-        returns = _resolve_return(key, 0, frozenset({key}), cap, sk, capped)
+        returns = resolve_return(key, frozenset())
         out[key] = MethodSummary(key, params, returns, skel.file, skel.line)
-    return out, capped
+    return out, sorted(unresolved)
 
 
-def solve(skeletons: Iterable[MethodSkeleton], *,
-          cap: int = DEFAULT_CAP) -> dict[str, MethodSummary]:
-    """Convenience wrapper around :func:`solve_with_log` dropping the cap log."""
-    return solve_with_log(skeletons, cap=cap)[0]
+def solve(skeletons: Iterable[MethodSkeleton]) -> dict[str, MethodSummary]:
+    """Convenience wrapper around :func:`solve_with_log` dropping the unresolved log."""
+    return solve_with_log(skeletons)[0]