From 32600629be4989f8fd902b2d28fd4484827985fd Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 06:38:41 +0000 Subject: [PATCH 1/3] perf(d5): solve MOS by SCC-condensed summary fixpoint, drop the depth cap MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The MOS solver resolved each method's summary by a memo-less recursive descent over the call graph, capped at depth 3. The cap existed only to dodge the exponential that re-descent hits on diamond-shaped call graphs (A forwards a param down two paths that reconverge on a shared callee), and it bought that safety with two costs: false `unknown`s on forward chains deeper than the cap, and a less-precise `may` on recursion (the descent broke each cycle at a spurious `no`, which a later join turned a provable `must` into `may`). Replace it with the textbook interprocedural summary fixpoint: * condense the call graph into strongly-connected components (iterative Tarjan, emitted bottom-up = reverse-topological); * process components bottom-up — a callee's summary is final before any caller reads it, so each method is resolved once and reused (the context-insensitive summary IS the memoization); * within a recursive component, seed each edge at the lattice bottom (⊥, "no evidence yet") and iterate the four-point transfer lattice to its least fixpoint, mapping any residual ⊥ to `no` at finalization; * resolve forward-returns by a memoized, cycle-safe chase. This removes the exponential without the cap, and is strictly more precise on recursion: a method that disposes on its base case and recurses otherwise now resolves to `must` (every terminating path disposes), and mutual recursion grounded by a dispose deep in the cycle carries that `must` across the whole SCC. Mutual recursion that never disposes still settles at `no` and still terminates. The only residual `unknown` is an extern (unsummarized) forward boundary; `solve_with_log` now surfaces exactly those (sorted, deterministic) in place of the old cap log — no silent truncation. Public API unchanged in shape: solve() / solve_with_log() keep their return types; the now-meaningless `cap` keyword is dropped (the sole caller, the ownir bridge, never passed it). Tests that asserted the old depth-broken behaviour (chain past cap -> unknown; self-recursion -> may) are updated to the precise fixpoint results, plus new diamond, deep-chain, extern-log, and grounded-mutual-recursion cases. Full suite green (ownership 40/40, ownir bridge 194/194, mypy --strict, ruff). No existing bridge/corpus diagnostic shifts. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019846YSZ35c7CdkWQ1qX5gm --- ownlang/ownership.py | 340 ++++++++++++++++++++++++++-------------- tests/test_ownership.py | 45 ++++-- 2 files changed, 258 insertions(+), 127 deletions(-) diff --git a/ownlang/ownership.py b/ownlang/ownership.py index b03af6bf..f6b49857 100644 --- a/ownlang/ownership.py +++ b/ownlang/ownership.py @@ -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: 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] diff --git a/tests/test_ownership.py b/tests/test_ownership.py index 65c39c8c..76f20c3a 100644 --- a/tests/test_ownership.py +++ b/tests/test_ownership.py @@ -3,8 +3,9 @@ Pure-Python, no extractor, no dotnet: hand-author method skeletons and assert the solved Method Ownership Summaries. Exercises the transfer lattice (must/may/no/ -unknown), the depth-capped bottom-up resolution, recursion/SCC convergence, the -extern boundary, return-kind resolution (fresh/aliasOf/aliased), and the +unknown), the summary fixpoint over the call graph's SCC condensation (deep chains +resolve without a depth cap; recursion is solved, not truncated), the extern +boundary and its log, return-kind resolution (fresh/aliasOf/aliased), and the `summaries[]` serialization. Run: python tests/test_ownership.py @@ -120,30 +121,50 @@ def expect(cond, msg): s = solve([_m("Caller", _p(0, PathAction("forward", "Extern", 0)))]) # Extern unsummarized expect(_t(s, "Caller", 0) == Transfer.UNKNOWN, "forward to extern -> unknown") - # --- depth cap ---------------------------------------------------------- - chain = [ + # --- deep chains: no depth cap (the SCC condensation bounds the work) ----- + # A 4-hop forward chain a former depth-3 cap would have degraded to `unknown` + # now resolves end-to-end: the consumer at the bottom propagates up exactly. + deep = [ _m("A", _p(0, PathAction("forward", "B", 0))), _m("B", _p(0, PathAction("forward", "C", 0))), - _m("C", _p(0, PathAction("dispose"))), + _m("C", _p(0, PathAction("forward", "D", 0))), + _m("D", _p(0, PathAction("dispose"))), ] - s2, log = solve_with_log(chain, cap=2) - expect(s2["A"].params[0].transfer == Transfer.UNKNOWN, "chain past cap=2 -> unknown") - expect(any("C#0" in e for e in log), "depth cap is logged, not silent") + s2, log = solve_with_log(deep) + expect(s2["A"].params[0].transfer == Transfer.MUST, "deep chain resolves (no cap)") + expect(log == [], "a fully-summarized graph leaves nothing unresolved") + + # The log is not silent about the one residual unknown: an extern (unsummarized) + # forward boundary is named, so a run can see exactly what it could not resolve. + _, log2 = solve_with_log([_m("Caller", _p(0, PathAction("forward", "Extern", 0)))]) + expect(any("Extern#0" in e for e in log2), "extern forward is logged, not silent") # --- recursion / SCC convergence ---------------------------------------- - # Mutual recursion that never disposes -> no (and, crucially, terminates). + # Mutual recursion that never disposes -> no (the cycle seeds at bottom and the + # fixpoint settles at `no`; crucially, it terminates). s = solve([ _m("F", _p(0, PathAction("forward", "G", 0))), _m("G", _p(0, PathAction("forward", "F", 0))), ]) expect(_t(s, "F", 0) == Transfer.NO, "mutual recursion w/o dispose -> no (terminates)") - # Self-recursion with a base-case dispose: provable on some but not all paths - # through the recursion -> may (precision-safe; never a hard must). + # Self-recursion with a base-case dispose: every *terminating* path disposes (the + # recursive edge defers, it does not keep), so the fixpoint resolves it to `must`. + # The old depth-broken resolver injected a spurious `no` at the cycle and got the + # weaker `may`; the least-fixpoint over the lattice is exact here. s = solve([ _m("Rec", _p(0, PathAction("dispose"), PathAction("forward", "Rec", 0))), ]) - expect(_t(s, "Rec", 0) == Transfer.MAY, "self-recursion + base dispose -> may") + expect(_t(s, "Rec", 0) == Transfer.MUST, "self-recursion + base dispose -> must") + + # Mutual recursion where the only ground is a dispose deep in the cycle: the + # fixpoint carries it across the SCC, where breaking the cycle at `no` would not. + s = solve([ + _m("P", _p(0, PathAction("forward", "Q", 0))), + _m("Q", _p(0, PathAction("dispose"), PathAction("forward", "P", 0))), + ]) + expect(_t(s, "P", 0) == Transfer.MUST, "mutual recursion grounded by dispose -> must") + expect(_t(s, "Q", 0) == Transfer.MUST, "the grounding method is must too") # --- return-kind resolution --------------------------------------------- s = solve([_m("Factory", ret=ReturnSkeleton("fresh"))]) From e2bb4caee45732f2e80810a75f31062edd3a2be8 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 06:47:06 +0000 Subject: [PATCH 2/3] fix(d5): resolve forward-returns iteratively, not recursively MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The SCC pass and the param fixpoint are iterative, but resolve_return was left recursive — one Python frame per forward-return hop. With the depth cap gone, a long but acyclic chain of `ReturnSkeleton("forward")` wrappers recurses to Python's default limit and raises RecursionError. The bridge catches a solve() exception by dropping to an EMPTY MOS, so one deep wrapper chain would disable interprocedural ownership summaries for the entire input rather than just that one return chain. (Codex P2.) A return has at most one forward target, so resolution is a linked-list walk: chase the forward edges to a terminal / extern / cycle, then propagate the value back up applying the aliasOf-through-forward degrade at each hop. Behaviour is identical to the recursive version (same memo, same cycle -> unknown, same aliasOf rule); it just no longer grows the call stack. Adds deep-chain (N=3000, past the recursion limit) regression tests for both the forward-return and forward-param chains. ownership 42/42, ownir bridge 194/194, mypy --strict, ruff — all green. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019846YSZ35c7CdkWQ1qX5gm --- ownlang/ownership.py | 78 ++++++++++++++++++++++++++--------------- tests/test_ownership.py | 15 ++++++++ 2 files changed, 64 insertions(+), 29 deletions(-) diff --git a/ownlang/ownership.py b/ownlang/ownership.py index f6b49857..39f870e0 100644 --- a/ownlang/ownership.py +++ b/ownlang/ownership.py @@ -318,39 +318,59 @@ def transfer_of(key: str, index: int, 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 -------- + # --- returns: an iterative, memoized, cycle-safe chase along forward edges ---- + # A return has at most ONE forward target, so resolution is a linked-list walk, + # not a tree. Done iteratively (not recursively) so a deep but acyclic wrapper + # chain cannot blow Python's recursion limit — which, since the bridge catches a + # solve() exception by dropping to an EMPTY MOS, would otherwise disable every + # method's summary over one long chain rather than just that chain (Codex P2). 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 + def _terminal(r: ReturnSkeleton) -> str: 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": + return "fresh" + if r.kind == "aliasOf": + return f"aliasOf:{r.arg}" + if r.kind == "aliased": + return "aliased" + if r.kind == "none": + return "none" # explicit no-owned-return + return "unknown" # an unrecognised kind fails closed, never silently "none" + + def resolve_return(start: str) -> str: + if start in ret_val: + return ret_val[start] # context-insensitive: one forward target per return + path: list[str] = [] # forward nodes above the stop node (shallow -> deep) + on_path: set[str] = set() + key = start + while True: + if key in ret_val: + val = ret_val[key] + break + r = sk[key].ret + if r.kind != "forward": + val = ret_val[key] = _terminal(r) + break 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: 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 + val = ret_val[key] = "unknown" + break + if r.callee == key or r.callee in on_path: + # forward-return cycle: this node (and all that feed it) have no ground + val = ret_val[key] = "unknown" + break + path.append(key) + on_path.add(key) + key = r.callee + # Propagate the stop node's value up the forward chain. At each hop an + # aliasOf: aliases one of the *callee's* params; remapping it to OUR args + # needs the call's argument mapping the skeleton does not carry yet (the + # obligation-identity model, D5.4) — so degrade to unknown rather than + # propagate a wrong index. fresh / aliased / none / unknown propagate as-is. + for k in reversed(path): + val = "unknown" if val.startswith("aliasOf:") else val + ret_val[k] = val + return ret_val[start] out: dict[str, MethodSummary] = {} for key, skel in sk.items(): @@ -362,7 +382,7 @@ def resolve_return(key: str, visiting: frozenset[str]) -> str: ) for p in skel.params ) - returns = resolve_return(key, frozenset()) + returns = resolve_return(key) out[key] = MethodSummary(key, params, returns, skel.file, skel.line) return out, sorted(unresolved) diff --git a/tests/test_ownership.py b/tests/test_ownership.py index 76f20c3a..129a2aa8 100644 --- a/tests/test_ownership.py +++ b/tests/test_ownership.py @@ -139,6 +139,21 @@ def expect(cond, msg): _, log2 = solve_with_log([_m("Caller", _p(0, PathAction("forward", "Extern", 0)))]) expect(any("Extern#0" in e for e in log2), "extern forward is logged, not silent") + # A deep but acyclic chain must not blow Python's recursion limit (the solver is + # iterative end to end; a RecursionError here would, via the bridge's catch-all, + # drop the WHOLE input's MOS to empty over one long chain). 3000 > default limit. + N = 3000 + param_chain = [ + _m(f"L{i}", _p(0, PathAction("forward", f"L{i + 1}", 0))) for i in range(N) + ] + [_m(f"L{N}", _p(0, PathAction("dispose")))] + expect(_t(solve(param_chain), "L0", 0) == Transfer.MUST, + "deep param forward chain resolves without RecursionError") + ret_chain = [ + _m(f"R{i}", ret=ReturnSkeleton("forward", callee=f"R{i + 1}")) for i in range(N) + ] + [_m(f"R{N}", ret=ReturnSkeleton("fresh"))] + expect(solve(ret_chain)["R0"].returns == "fresh", + "deep forward-return chain resolves without RecursionError") + # --- recursion / SCC convergence ---------------------------------------- # Mutual recursion that never disposes -> no (the cycle seeds at bottom and the # fixpoint settles at `no`; crucially, it terminates). From 0e7125baf9a4dc53c4b07e9648bf63a279a5f403 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 06:49:27 +0000 Subject: [PATCH 3/3] docs(d5): correct the unresolved-log contract; test return extern boundary MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CodeRabbit review: the solve_with_log / module docstrings claimed the extern boundary is the ONLY source of `unknown`. It isn't — resolve_return also yields `unknown` (without logging) for a return-forward cycle, an un-remappable aliasOf, and an unrecognised return kind, and lookup does for a missing param index. Those are intrinsic, precision-safe, deterministic-from-input degradations, not "gave up on something external", so they are intentionally not logged. Soften the wording: the log covers extern (outside-the-analyzed-set) boundaries, not every `unknown`. Also add a forward-return extern-boundary log assertion — the return chase is a separate code path from the param-forward case the existing test covered, so a regression in return-boundary logging would otherwise slip through. Docs/test only — no behaviour change. ownership 44/44, ownir 194/194, mypy --strict, ruff all green. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019846YSZ35c7CdkWQ1qX5gm --- ownlang/ownership.py | 19 ++++++++++++------- tests/test_ownership.py | 6 ++++++ 2 files changed, 18 insertions(+), 7 deletions(-) diff --git a/ownlang/ownership.py b/ownlang/ownership.py index 39f870e0..1908ae04 100644 --- a/ownlang/ownership.py +++ b/ownlang/ownership.py @@ -28,10 +28,12 @@ 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. +settles at `no`. A residual `unknown` is never a guessed `must`: it comes either +from an extern (unsummarized) callee — which `solve_with_log` surfaces in its log — +or from a deliberate precision-safe degradation intrinsic to the input (a +return-forward cycle, an `aliasOf` that cannot be re-mapped without the call's arg +mapping, an unrecognised or sparse shape), which is not logged. That keeps the +project's precision-first stance: we only ever *claim* transfer when we can prove it. """ from __future__ import annotations @@ -243,9 +245,12 @@ def solve_with_log(skeletons: Iterable[MethodSkeleton]) -> tuple[ """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 + Returns (summaries-by-key, unresolved-log). The log names every forward — param + or return — that crosses an extern (unsummarized) boundary: the `unknown`s that + come from *outside* the analyzed set. It is NOT a log of all `unknown`s — the + intrinsic, precision-safe degradations (a return-forward cycle, an un-remappable + `aliasOf`, a missing param index or unrecognised shape) are deterministic from + the input and not logged. There is no depth cap, so no work is truncated: the condensation makes the work linear, and recursion is solved, not cut off.""" sk: dict[str, MethodSkeleton] = {} for s in skeletons: diff --git a/tests/test_ownership.py b/tests/test_ownership.py index 129a2aa8..42006ea8 100644 --- a/tests/test_ownership.py +++ b/tests/test_ownership.py @@ -139,6 +139,12 @@ def expect(cond, msg): _, log2 = solve_with_log([_m("Caller", _p(0, PathAction("forward", "Extern", 0)))]) expect(any("Extern#0" in e for e in log2), "extern forward is logged, not silent") + # The return chase logs its extern boundary too (a separate code path from the + # param forward above) — a forward-return to an unsummarized callee. + s3, log3 = solve_with_log([_m("Caller", ret=ReturnSkeleton("forward", callee="Extern"))]) + expect(s3["Caller"].returns == "unknown", "forward-return to extern -> unknown") + expect(any("return Extern" in e for e in log3), "extern forward-return is logged") + # A deep but acyclic chain must not blow Python's recursion limit (the solver is # iterative end to end; a RecursionError here would, via the bridge's catch-all, # drop the WHOLE input's MOS to empty over one long chain). 3000 > default limit.