docs(d5): correct the unresolved-log contract; test return extern boundary

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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019846YSZ35c7CdkWQ1qX5gm

Author: claude

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:

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.