diff --git a/docs/decisions/ADR-0203-binding-graph-acyclicity-invariant.md b/docs/decisions/ADR-0203-binding-graph-acyclicity-invariant.md new file mode 100644 index 00000000..daa1c867 --- /dev/null +++ b/docs/decisions/ADR-0203-binding-graph-acyclicity-invariant.md @@ -0,0 +1,107 @@ +# ADR-0203 — Binding-Graph Acyclicity Invariant (`circular_dependency` refusal) + +**Status:** Accepted (proof_chain phase 2.1 — the isolated guard; ADR-0201 §Deferred) +**Date:** 2026-06-02 +**Relates to:** **ADR-0132** (binding-graph data model — this *adds* an invariant to +its construction contract; see §amend-vs-additive), ADR-0201 (canonicalizer + +phase plan), ADR-0202 (proposition representation contract). + +--- + +## Context + +ADR-0132's `SemanticSymbolicBindingGraph.__post_init__` enforces **referential +integrity** (every `BoundEquation` dependency names a known symbol) but **not +acyclicity**. A cycle in the equation dependency structure — `x` defined from `y`, +`y` defined from `x`, or a self-dependency `x ← x` — is **circular reasoning**: +structurally well-formed, semantically invalid. It is the proof-domain analog of +the `20/5 == 4` class the arithmetic gate refuses. + +`proof_chain` (ADR-0201) is the first consumer that can *build* such a structure: +its phase 2.2 wiring constructs binding graphs from proofs, where a malformed proof +could close a dependency loop. Per CORE's "build the defensive refusal NOW" +discipline, the guard must exist **before** the structure where a cycle can exist — +so this phase (2.1) lands it *before* any 2.2 wiring. + +## Decision + +Add an **acyclicity invariant** to binding-graph construction: + +- **`generate/binding_graph/acyclicity.py`** — a pure `find_cycle(adjacency)` + cycle detector (deterministic three-colour DFS; sorted traversal → byte-stable + reported cycle; self-edge → length-1 cycle). No model import — testable in + isolation against synthetic adjacency graphs. +- **Enforcement at the shared construction boundary.** `__post_init__` builds a + `{lhs_symbol_id: ⋃ dependencies}` adjacency over its equations and calls + `find_cycle`; a non-`None` result raises + `BindingGraphError("circular_dependency: equation dependency cycle …")` naming + the cycle. This runs on **every** binding graph — math and (future) proof alike — + making a cyclic graph unrepresentable for all consumers. + +### Why the shared `__post_init__` (not a proof-only check) + +Putting it at the substrate boundary closes the gap universally and makes illegal +states unrepresentable (the CLAUDE.md design principle), rather than leaving the +math binding graph cycle-unchecked. The guard exists the instant the structure +becomes constructible — strictly *before* the proof wiring that makes a cycle +reachable. + +### Math-lane regression proof (the shared-constructor risk) + +Because the guard runs on the existing math/algebra path too, it must refuse no +existing graph. Verified: + +- The **only** production producer is `generate/binding_graph/adapter.py` + (`bind_math_problem_graph`). It mints a **fresh** result symbol per operation + (`_op_result_symbol_id(idx)`) and depends only on symbols that already exist — + edges point strictly backward in construction order. It is therefore **acyclic + by construction** and cannot produce a graph this guard would refuse. +- No existing test constructs a dependency cycle (the `sym_ghost` fixture is the + referential-integrity refusal, not a cycle). +- The **full binding-graph + admissibility test surface — 392 tests — stays + green** with the guard in `__post_init__`. (Smoke: 67 passed.) + +A future/in-flight consumer that *did* build a cycle would now be refused at +construction — which is the point. + +## amend-vs-additive (ADR-0203 vs amending ADR-0132) + +**Decision: a new additive ADR (this one) that references ADR-0132 — not an +amendment of the closed record.** + +ADR-0132 is `Accepted`. The acyclicity invariant was not part of its original +decision; it became necessary later, when `proof_chain` made cycles *reachable*. +Recording it as a new invariant preserves that history — *why* the guard was added +and *when it became load-bearing* — which an in-place edit of the closed record +would erase. This mirrors the history-vs-current-state discipline used elsewhere +(append the new fact; don't rewrite the settled one). The code lives beside +ADR-0132's referential-integrity check in `__post_init__`; the *decision record* is +additive. + +## Honesty boundary (load-bearing — carried by every phase-2 ADR, 0203–0205) + +Through phase 2.3, `proof_chain` is **sound over its declared atoms** — it does +**not** reason over recognized input. Atoms are opaque/declared symbol ids +(ADR-0202); grounding them to ADR-0144 `EpistemicNode`/`FeatureBundle` carriers is +**phase 2.4** (fork B). This must **never** be softened to "reasons over input" +before 2.4 lands. This ADR is structure-only and makes no grounding claim; it is +named here so the boundary travels with the work, not just with the rule ADRs. + +## Evidence + +- `tests/test_binding_graph_acyclicity.py` — 17 tests: pure checker (acyclic→None; + self-loop/2-/3-cycle/cycle-with-tail detected; deterministic), construction + enforcement (cyclic + self-dependent refuse; acyclic + adapter-shape construct), + and referential-integrity-still-fires-first. +- **Mutation-verified non-vacuous:** neutering `find_cycle` (→ always `None`) makes + a 2-cycle construct without refusal — `test_two_cycle_equation_set_refuses` would + fail. The guard is load-bearing, not decoration. +- Full binding-graph/admissibility surface: **392 passed**. Smoke: **67 passed**. + +## Deferred (not in this phase) + +- **2.2** — proof-graph builder (proof → `BoundEquation`s; `canonical_key` → + `rhs_canonical`); the first construction that exercises this guard through the + real proof path (ADR-0204). +- **2.3** — `modus_ponens` + the disagreement rule (ADR-0205). +- **2.4** — atom→`EpistemicNode` carrier grounding (ADR-0206). diff --git a/generate/binding_graph/__init__.py b/generate/binding_graph/__init__.py index 22c36b68..9f5d9695 100644 --- a/generate/binding_graph/__init__.py +++ b/generate/binding_graph/__init__.py @@ -21,6 +21,7 @@ Phase 5 (bounded-grammar / B3 integration) deferred. from __future__ import annotations +from .acyclicity import CIRCULAR_DEPENDENCY, find_cycle from .adapter import ( INTRODUCED_BY, REFUSED_UNIT_PROOF, @@ -73,6 +74,7 @@ from .units import ( __all__ = ( "ADMISSIBILITY_REASONS", "ADMISSIBILITY_STATUSES", + "CIRCULAR_DEPENDENCY", "BASE_DIMENSIONS", "DIMENSIONLESS", "INTRODUCED_BY", @@ -102,6 +104,7 @@ __all__ = ( "bind_math_problem_graph", "bound_unknown_from_math_problem_graph", "check_admissibility", + "find_cycle", "infer_question_form", "parse_unit", "resolve_state_index", diff --git a/generate/binding_graph/acyclicity.py b/generate/binding_graph/acyclicity.py new file mode 100644 index 00000000..890ad8f5 --- /dev/null +++ b/generate/binding_graph/acyclicity.py @@ -0,0 +1,91 @@ +"""ADR-0203 — Acyclicity invariant for the binding-graph dependency structure. + +Pure cycle detection over a ``{node: successors}`` adjacency, isolated from the +binding-graph model so it is testable against synthetic graphs with no +binding-graph construction. The model's ``__post_init__`` adapts its equations +into an adjacency and calls :func:`find_cycle`; a non-``None`` result is refused +with the typed reason :data:`CIRCULAR_DEPENDENCY`. + +Why this exists (additive to ADR-0132, which it references): the ADR-0132 data +model enforces *referential integrity* (every dependency names a known symbol) but +not *acyclicity*. A cycle in the equation dependency structure is **circular +reasoning** — concluding ``P`` because ``Q`` because ``P`` — the proof-domain +analog of the ``20/5 == 4`` class: structurally well-formed, semantically invalid. +``proof_chain`` is the first consumer that can build such a structure, so the guard +lands at the shared construction boundary *before* that wiring exists (ADR-0201 +phase 2.1). + +On main today the only producer of binding graphs is the math adapter +(`generate/binding_graph/adapter.py`), which mints a fresh result symbol per +operation and depends only on symbols that already exist — edges point strictly +backward in construction order, so it is **acyclic by construction**. This guard +therefore refuses no existing graph; it protects the structure the moment a future +consumer could build a cycle. + +Honesty boundary (carried by every phase-2 ADR, 0203–0205): through phase 2.3, +``proof_chain`` is **sound over its declared atoms**, not grounded in recognized +input. Atom→carrier grounding is phase 2.4. This module is structure-only and makes +no grounding claim. +""" + +from __future__ import annotations + +from collections.abc import Mapping +from typing import Final + +CIRCULAR_DEPENDENCY: Final[str] = "circular_dependency" + + +def find_cycle(adjacency: Mapping[str, frozenset[str]]) -> tuple[str, ...] | None: + """Return a directed cycle as an ordered tuple ``(n0, …, nk, n0)``, or + ``None`` if the graph is acyclic. + + ``adjacency`` maps a node to the set of nodes it points to (an equation's + ``lhs_symbol_id`` → the symbols it reads). Nodes that appear only as + successors (leaf dependencies defined by no equation) have no out-edges and + cannot start a cycle. + + Deterministic: roots and successors are visited in sorted order, so the + reported cycle is byte-stable across runs (the replay discipline). A node + listing itself as a successor is reported as a length-1 self-cycle + ``(n, n)``. + """ + WHITE, GREY, BLACK = 0, 1, 2 + color: dict[str, int] = {node: WHITE for node in adjacency} + for succs in adjacency.values(): + for succ in succs: + color.setdefault(succ, WHITE) + + def successors(node: str) -> list[str]: + return sorted(adjacency.get(node, frozenset())) + + # Iterative three-colour DFS (iterative to avoid recursion limits on long + # dependency chains). GREY = on the current DFS path; a GREY successor is a + # back-edge, i.e. a cycle. + for root in sorted(color): + if color[root] != WHITE: + continue + path: list[str] = [root] + stack: list[tuple[str, list[str]]] = [(root, successors(root))] + color[root] = GREY + while stack: + node, succs = stack[-1] + descended = False + while succs: + nxt = succs.pop(0) + state = color[nxt] + if state == GREY: + start = path.index(nxt) + return tuple(path[start:] + [nxt]) + if state == WHITE: + color[nxt] = GREY + path.append(nxt) + stack.append((nxt, successors(nxt))) + descended = True + break + # BLACK: fully explored, no cycle through it — skip. + if not descended: + color[node] = BLACK + path.pop() + stack.pop() + return None diff --git a/generate/binding_graph/model.py b/generate/binding_graph/model.py index 771375ed..e0f90936 100644 --- a/generate/binding_graph/model.py +++ b/generate/binding_graph/model.py @@ -19,6 +19,8 @@ from __future__ import annotations from dataclasses import dataclass, field from typing import Final, Literal, Union +from generate.binding_graph.acyclicity import CIRCULAR_DEPENDENCY, find_cycle + # --------------------------------------------------------------------------- # Public errors # --------------------------------------------------------------------------- @@ -464,6 +466,24 @@ class SemanticSymbolicBindingGraph: f"{dep!r} (lhs={eq.lhs_symbol_id!r})" ) + # ADR-0203 — acyclicity invariant. Referential integrity (above) proves + # every dependency names a known symbol; this proves the equation + # dependency structure has no cycle. A cycle is circular reasoning + # (conclude P because Q because P) — structurally well-formed, invalid. + # The math adapter is acyclic by construction, so this refuses no + # existing graph; it guards the structure before proof_chain (the first + # consumer that could build a cycle) wires in. Multiple equations sharing + # an lhs union their dependencies. + adjacency: dict[str, set[str]] = {} + for eq in self.equations: + adjacency.setdefault(eq.lhs_symbol_id, set()).update(eq.dependencies) + cycle = find_cycle({lhs: frozenset(deps) for lhs, deps in adjacency.items()}) + if cycle is not None: + raise BindingGraphError( + f"{CIRCULAR_DEPENDENCY}: equation dependency cycle " + f"{' -> '.join(cycle)}" + ) + equation_count = len(self.equations) for unk in self.unknowns: if unk.symbol_id not in known_ids: diff --git a/tests/test_binding_graph_acyclicity.py b/tests/test_binding_graph_acyclicity.py new file mode 100644 index 00000000..690133dc --- /dev/null +++ b/tests/test_binding_graph_acyclicity.py @@ -0,0 +1,167 @@ +"""ADR-0203 — acyclicity guard for the binding-graph dependency structure. + +Two layers, both exercised here: + +1. The **pure checker** (`find_cycle`) in isolation against synthetic adjacency + graphs — no binding-graph construction. Cyclic graphs return the cycle; + acyclic graphs return None; fails-loud under mutation (the equivalent + cyclic/acyclic assertions are mutually constraining, so a neutered detector + fails the suite). +2. The **construction-boundary enforcement** in + `SemanticSymbolicBindingGraph.__post_init__` — a cyclic equation set raises + `BindingGraphError(circular_dependency …)`; an acyclic set (including the + math-adapter shape: fresh result symbol per op, deps point backward) + constructs fine — the math-lane regression proof. +""" + +from __future__ import annotations + +import pytest + +from generate.binding_graph import ( + CIRCULAR_DEPENDENCY, + BindingGraphError, + BoundEquation, + SemanticSymbolicBindingGraph, + SourceSpanLink, + SymbolBinding, + find_cycle, +) + + +# --------------------------------------------------------------------------- +# Layer 1 — pure checker, isolated +# --------------------------------------------------------------------------- + +ACYCLIC_GRAPHS = [ + {}, # empty + {"a": frozenset()}, # single, no edges + {"a": frozenset({"b"}), "b": frozenset({"c"})}, # linear chain + {"a": frozenset({"b", "c"}), "b": frozenset({"d"}), + "c": frozenset({"d"}), "d": frozenset()}, # diamond / shared dep + {"a": frozenset({"b", "c", "d"})}, # leaves not defined by any eq +] + + +@pytest.mark.parametrize("graph", ACYCLIC_GRAPHS) +def test_acyclic_graphs_return_none(graph) -> None: + assert find_cycle(graph) is None + + +CYCLIC_GRAPHS = [ + {"a": frozenset({"a"})}, # self-loop + {"a": frozenset({"b"}), "b": frozenset({"a"})}, # 2-cycle + {"a": frozenset({"b"}), "b": frozenset({"c"}), + "c": frozenset({"a"})}, # 3-cycle + {"t": frozenset({"a"}), "a": frozenset({"b"}), + "b": frozenset({"c"}), "c": frozenset({"b"})}, # cycle with a tail (t→a→b→c→b) +] + + +@pytest.mark.parametrize("graph", CYCLIC_GRAPHS) +def test_cyclic_graphs_are_detected(graph) -> None: + cycle = find_cycle(graph) + assert cycle is not None + # A reported cycle closes on itself and every hop is a real edge. + assert cycle[0] == cycle[-1] + for src, dst in zip(cycle, cycle[1:]): + assert dst in graph[src], f"{src}->{dst} is not an edge" + + +def test_self_loop_reported_as_length_one_cycle() -> None: + assert find_cycle({"x": frozenset({"x"})}) == ("x", "x") + + +def test_reported_cycle_is_deterministic() -> None: + graph = {"a": frozenset({"b"}), "b": frozenset({"c"}), "c": frozenset({"a"})} + assert find_cycle(graph) == find_cycle(graph) + + +# --------------------------------------------------------------------------- +# Construction fixtures (mirror tests/test_binding_graph_model.py helpers) +# --------------------------------------------------------------------------- + + +def _span() -> SourceSpanLink: + return SourceSpanLink(source_id="src", start=0, end=3, text="xyz") + + +def _sym(symbol_id: str) -> SymbolBinding: + return SymbolBinding( + symbol_id=symbol_id, + name=symbol_id, + semantic_role="quantity", + source_span=_span(), + introduced_by="test", + ) + + +def _eq(lhs: str, deps: set[str]) -> BoundEquation: + return BoundEquation( + lhs_symbol_id=lhs, + rhs_canonical=f"{lhs} := f({sorted(deps)})", + dependencies=frozenset(deps), + operation_kind="add", + unit_proof="pending", + admissibility_status="pending", + source_span=_span(), + ) + + +# --------------------------------------------------------------------------- +# Layer 2 — enforcement at the shared construction boundary +# --------------------------------------------------------------------------- + + +def test_acyclic_equation_set_constructs() -> None: + # r1 := f(x); r2 := f(r1, y) — strict DAG, edges point backward. + syms = tuple(_sym(s) for s in ("x", "y", "r1", "r2")) + eqs = (_eq("r1", {"x"}), _eq("r2", {"r1", "y"})) + graph = SemanticSymbolicBindingGraph(symbols=syms, equations=eqs) + assert len(graph.equations) == 2 + + +def test_adapter_shape_is_acyclic_by_construction() -> None: + # Mirrors the math adapter: each op result depends only on prior symbols. + syms = tuple(_sym(s) for s in ("q0", "q1", "op_0", "op_1")) + eqs = ( + _eq("op_0", {"q0", "q1"}), # op_0 := q0 + q1 + _eq("op_1", {"op_0", "q1"}), # op_1 := op_0 + q1 (chains forward) + ) + graph = SemanticSymbolicBindingGraph(symbols=syms, equations=eqs) + assert len(graph.equations) == 2 + + +def test_two_cycle_equation_set_refuses() -> None: + syms = (_sym("x"), _sym("y")) + eqs = (_eq("x", {"y"}), _eq("y", {"x"})) # x↔y circular dependency + with pytest.raises(BindingGraphError) as exc: + SemanticSymbolicBindingGraph(symbols=syms, equations=eqs) + assert CIRCULAR_DEPENDENCY in str(exc.value) + + +def test_self_dependent_equation_refuses() -> None: + syms = (_sym("x"),) + eqs = (_eq("x", {"x"}),) # x defined in terms of itself + with pytest.raises(BindingGraphError) as exc: + SemanticSymbolicBindingGraph(symbols=syms, equations=eqs) + assert CIRCULAR_DEPENDENCY in str(exc.value) + + +def test_longer_cycle_equation_set_refuses() -> None: + syms = tuple(_sym(s) for s in ("a", "b", "c")) + eqs = (_eq("a", {"b"}), _eq("b", {"c"}), _eq("c", {"a"})) + with pytest.raises(BindingGraphError) as exc: + SemanticSymbolicBindingGraph(symbols=syms, equations=eqs) + assert CIRCULAR_DEPENDENCY in str(exc.value) + + +def test_referential_integrity_still_enforced_before_cycle_check() -> None: + # An unknown dependency is still the referential-integrity refusal, not a + # cycle — the existing ADR-0132 invariant is unchanged. + syms = (_sym("x"),) + eqs = (_eq("x", {"ghost"}),) + with pytest.raises(BindingGraphError) as exc: + SemanticSymbolicBindingGraph(symbols=syms, equations=eqs) + assert "unknown dependency" in str(exc.value) + assert CIRCULAR_DEPENDENCY not in str(exc.value)