diff --git a/docs/decisions/ADR-0204-proof-graph-builder.md b/docs/decisions/ADR-0204-proof-graph-builder.md new file mode 100644 index 00000000..4fb78b4e --- /dev/null +++ b/docs/decisions/ADR-0204-proof-graph-builder.md @@ -0,0 +1,117 @@ +# ADR-0204 — Proof-Graph Builder (proof_chain's first binding-graph consumer) + +**Status:** Accepted (proof_chain phase 2.2 — structure only; ADR-0201 §Deferred) +**Date:** 2026-06-02 +**Relates to:** ADR-0132 (binding-graph data model — the substrate this consumes), +ADR-0201 / ADR-0201.1 (canonicalizer + out-of-regime detector), ADR-0202 +(proposition representation contract), ADR-0203 (acyclicity guard this exercises). +**Deferred to:** ADR-0205 (modus_ponens + disagreement rule), ADR-0206 (atom→carrier +grounding). + +--- + +## Context + +The ADR-0132 binding graph is the proof-DAG substrate; until now it had **zero +consumers**. Phase 2.2 makes `proof_chain` its first: a builder that translates a +propositional proof into a `SemanticSymbolicBindingGraph`. **Structure only** — no +inference rule (modus_ponens is 2.3). The builder constructs the DAG and lets the +substrate's guards fire; it asserts nothing about whether a step is *valid*. + +## Decision + +### One canonical proof input shape + +`generate/proof_chain/model.py` defines the single committed proof representation — +the corpus surface shapes desugar onto it, so proof input never becomes a second +dialect (the ADR-0202 discipline, for proofs): + +- `ProofNode(node_id, formula, depends_on, rule)` — `node_id` is a Python + identifier (→ `symbol_id`); `formula` is an ADR-0202 propositional string; + `depends_on` names derived-from nodes; `rule` is the inference label. +- `Proof(nodes, conclusion_id)`. +- `proof_from_premises(premises, conclusion, rule)` desugars the + `premises`/`conclusion`/`rule` corpus shape (each premise → a `rule="premise"` + node; the conclusion → one node depending on all premises). + +### The mapping (every node → one symbol + one equation) + +| ProofNode | Binding-graph target | +|---|---| +| `node_id` | `SymbolBinding.symbol_id` / `BoundEquation.lhs_symbol_id` | +| `canonicalize(formula).canonical_key` | `BoundEquation.rhs_canonical` | +| `depends_on` | `BoundEquation.dependencies` | +| `rule` | `BoundEquation.operation_kind` (`"premise"` for assumptions) | + +Premises are equations with empty `dependencies` and `operation_kind="premise"` — +uniform, and every node thereby carries its proposition's canonical key in +`rhs_canonical` (which 2.3's rule check needs). Construction runs the ADR-0203 +acyclicity guard + ADR-0132 referential integrity in `__post_init__`: a cyclic or +dangling proof **refuses there**, through the real builder path. + +### Admissibility-dispatch confirmation (the operation_kind question) + +The builder writes logic labels (`"premise"`, later `"modus_ponens"`) into +`operation_kind`, a field the math admissibility checker reads (closed arithmetic +vocab). **Confirmed by code + test that the dispatch handles unknown-to-math kinds +gracefully and never misroutes:** `check_admissibility` ends in +`raise AdmissibilityError("unknown_operation", kind)` — there is no default into +`_check_additive`. Empirically, on built proof equations: a `premise` (no deps) +reaches the dispatch → `unknown_operation`; a `modus_ponens` (unitless deps) +refuses at unit-resolution → `unit_unbound`. Neither returns a math `UnitProof`; +neither misroutes. Baked into `test_proof_operation_kinds_refuse_in_admissibility_never_misroute`. + +**Named constraint carried to 2.3:** `check_admissibility` runs `_resolve_dep_units` +*before* the kind dispatch, so a proof equation with dependencies refuses with +`unit_unbound` first. The 2.3 `modus_ponens` check must therefore be wired to +**bypass unit resolution** (dispatch-on-kind before `_resolve_dep_units`, or a +separate proof-admissibility entry) — proofs have no units to resolve. + +## Open items (named for 2.3, not "we'll see") + +1. **Conclusion typing.** 2.2 tracks `ProofGraph.conclusion_symbol_id` (not a + `BoundUnknown` — ADR-0135's `question_form` vocab does not fit "is this + proven"). The 2.3 disagreement rule operates on the conclusion's canonical key + and may need richer conclusion typing; **revisit conclusion typing in ADR-0205.** +2. **`semantic_role` for propositions.** Proposition symbols use + `semantic_role="unknown"` because the **closed** ADR-0132 role vocab + (`entity`/`quantity`/`rate`/…) has no `"proposition"` member. This is the + role-field analog of the `operation_kind` situation. Extending `SEMANTIC_ROLES` + would be an ADR-0132 closed-vocab change (its exact set is test-pinned); left as + `"unknown"` for the additive 2.2 builder. **Decide whether to add a + `"proposition"` role when proofs become load-bearing.** +3. **`unit_proof`.** Set to the `PROOF_NO_UNIT` sentinel — units are non-applicable + to propositional proof steps. Composes with constraint (2) above for 2.3's + admissibility wiring. + +## Honesty boundary (load-bearing — every phase-2 ADR, 0203–0205) + +Through phase 2.3, proof_chain is **sound over its declared atoms**, not grounded in +recognized input (grounding is 2.4 / ADR-0206). The builder is structure-only: it +builds and refuses cycles/malformed/out-of-regime formulas; it makes **no** +soundness or grounding claim. Out-of-regime node formulas inherit the +canonicalizer's typed `LogicRegimeError` refusal (no silent predicate-logic +admission). + +## Evidence + +- `tests/test_proof_chain_builder.py` — 9 tests: valid DAG (incl. PC-MP-001 + desugared) + multistep DAG construct; **PC-CYCLE-001 refuses through the real + builder** (`circular_dependency`); canonical_key round-trips byte-identical + + equivalent node formulas share `rhs_canonical`; admissibility-dispatch + confirmation; self/dangling-dependency refusals; out-of-regime node formula + refuses. +- **Mutation-verified:** neutering the `depends_on → dependencies` wiring makes + PC-CYCLE-001 construct without refusal → the cycle test fails. The dep-wiring is + load-bearing, not the guard alone. +- **First-consumer non-perturbation:** full binding-graph + admissibility surface + green (the 392 intact); builder is purely additive (touches no math path). +- **Real corpus fixture:** PC-CYCLE-001 refuses through the builder; PC-MP-001/002/003 + structures construct (rule-check deferred to 2.3). Smoke: 67 passed. + +## Deferred + +- **2.3** — `modus_ponens` (`_check_modus_ponens` via ROBDD equivalence, wired to + bypass unit-resolution per §named constraint) + the disagreement/uniqueness rule + (the wrong=0 mechanism) — ADR-0205. +- **2.4** — atom→ADR-0144 `EpistemicNode` grounding — ADR-0206. diff --git a/generate/proof_chain/__init__.py b/generate/proof_chain/__init__.py new file mode 100644 index 00000000..9c75b18e --- /dev/null +++ b/generate/proof_chain/__init__.py @@ -0,0 +1,33 @@ +"""ADR-0204 — proof_chain: propositional proof graphs over the binding-graph DAG. + +Phase 2.2 (this module set): the proof-graph *builder* — proof → binding graph, +structure only. The canonicalizer (`generate.logic_canonical`) and equivalence +check (`generate.logic_equivalence`) it rides on are top-level modules; the +inference rule (`modus_ponens` + the disagreement rule) is phase 2.3 / ADR-0205. + +Honesty boundary (load-bearing through 2.3): sound over declared atoms, not +grounded in recognized input. +""" + +from __future__ import annotations + +from .builder import ( + PROOF_INTRODUCED_BY, + PROOF_NO_UNIT, + PROOF_SOURCE_ID, + ProofGraph, + build_proof_graph, +) +from .model import Proof, ProofError, ProofNode, proof_from_premises + +__all__ = ( + "PROOF_INTRODUCED_BY", + "PROOF_NO_UNIT", + "PROOF_SOURCE_ID", + "Proof", + "ProofError", + "ProofGraph", + "ProofNode", + "build_proof_graph", + "proof_from_premises", +) diff --git a/generate/proof_chain/builder.py b/generate/proof_chain/builder.py new file mode 100644 index 00000000..f8fe34c3 --- /dev/null +++ b/generate/proof_chain/builder.py @@ -0,0 +1,108 @@ +"""ADR-0204 — Proof-graph builder (proof_chain is the binding graph's first consumer). + +Translates a :class:`generate.proof_chain.model.Proof` into a +:class:`SemanticSymbolicBindingGraph`. **Structure only** — no inference rule +(``modus_ponens`` is phase 2.3 / ADR-0205). The builder constructs the DAG and +lets the ADR-0203 acyclicity guard + ADR-0132 referential-integrity checks fire at +construction; it asserts nothing about whether a step is *valid*. + +Mapping (one canonical shape; every node → one symbol + one equation): + +================== =================================== +ProofNode field Binding-graph target +================== =================================== +``node_id`` ``SymbolBinding.symbol_id`` / ``BoundEquation.lhs_symbol_id`` +``formula``→key ``BoundEquation.rhs_canonical`` (the ROBDD canonical key) +``depends_on`` ``BoundEquation.dependencies`` +``rule`` ``BoundEquation.operation_kind`` (``"premise"`` for assumptions) +================== =================================== + +Non-applicable math fields are typed placeholders (proofs have no units): +``unit_proof = PROOF_NO_UNIT``, ``admissibility_status = "pending"`` (nothing is +admitted in 2.2 — the rule check is 2.3). ``semantic_role`` uses ``"unknown"`` +because the closed ADR-0132 role vocab has no ``"proposition"`` member; see +ADR-0204 §Open items. + +May raise: the canonicalizer's ``LogicError`` family (malformed / out-of-regime / +budget on a node formula) and ``BindingGraphError`` (circular dependency, +referential integrity) — all refusal-first, none silently swallowed. +""" + +from __future__ import annotations + +from dataclasses import dataclass +from typing import Final + +from generate.binding_graph import ( + BoundEquation, + SemanticSymbolicBindingGraph, + SourceSpanLink, + SymbolBinding, +) +from generate.logic_canonical import canonicalize +from generate.proof_chain.model import Proof + +#: Synthetic provenance for proofs that have no NL source span (e.g. fixtures). +PROOF_SOURCE_ID: Final[str] = "proof_chain" +PROOF_INTRODUCED_BY: Final[str] = "build_proof_graph" +#: ``unit_proof`` sentinel — units are non-applicable to propositional proof steps. +PROOF_NO_UNIT: Final[str] = "proof_step_no_unit" +#: Proposition symbols have no math role; the closed ADR-0132 vocab has no +#: "proposition" member (ADR-0204 §Open items tracks revisiting this). +_PROPOSITION_ROLE: Final[str] = "unknown" + + +@dataclass(frozen=True, slots=True) +class ProofGraph: + """A built proof graph plus its designated conclusion symbol. + + ``conclusion_symbol_id`` is tracked here rather than as a ``BoundUnknown`` + in 2.2 (ADR-0135's ``question_form`` vocab does not fit "is this proven"); + conclusion typing is revisited in 2.3 when the disagreement rule operates on + the conclusion's canonical key (ADR-0204 §Open items / ADR-0205).""" + + graph: SemanticSymbolicBindingGraph + conclusion_symbol_id: str + + +def _span(formula: str) -> SourceSpanLink: + return SourceSpanLink( + source_id=PROOF_SOURCE_ID, start=0, end=len(formula), text=formula + ) + + +def build_proof_graph(proof: Proof) -> ProofGraph: + """Build the binding graph for ``proof``. Structure only; refusal-first.""" + symbols: list[SymbolBinding] = [] + equations: list[BoundEquation] = [] + for node in proof.nodes: + # Canonicalize the node's proposition; propagate any LogicError/regime/ + # budget refusal — a proof over a non-propositional formula refuses. + canonical_key = canonicalize(node.formula).canonical_key + span = _span(node.formula) + symbols.append( + SymbolBinding( + symbol_id=node.node_id, + name=node.node_id, + semantic_role=_PROPOSITION_ROLE, + source_span=span, + introduced_by=PROOF_INTRODUCED_BY, + ) + ) + equations.append( + BoundEquation( + lhs_symbol_id=node.node_id, + rhs_canonical=canonical_key, + dependencies=frozenset(node.depends_on), + operation_kind=node.rule, + unit_proof=PROOF_NO_UNIT, + admissibility_status="pending", + source_span=span, + ) + ) + # Construction runs the ADR-0203 acyclicity guard + ADR-0132 referential + # integrity in __post_init__ — a cyclic or dangling proof refuses HERE. + graph = SemanticSymbolicBindingGraph( + symbols=tuple(symbols), equations=tuple(equations) + ) + return ProofGraph(graph=graph, conclusion_symbol_id=proof.conclusion_id) diff --git a/generate/proof_chain/model.py b/generate/proof_chain/model.py new file mode 100644 index 00000000..159fbabe --- /dev/null +++ b/generate/proof_chain/model.py @@ -0,0 +1,102 @@ +"""ADR-0204 — Proof input model (the one canonical proof shape). + +A ``Proof`` is the single committed input representation for proof_chain — the +corpus surface shapes (``proof_nodes``/``depends_on``/``conclusion_node`` and +``premises``/``conclusion``/``rule``) desugar onto it, so proof input never +becomes a second dialect (same discipline ADR-0202 applies to formulas). + +Pure data — no canonicalizer, no binding graph. :func:`generate.proof_chain.builder` +translates a ``Proof`` into a ``SemanticSymbolicBindingGraph``. + +Honesty boundary (load-bearing through phase 2.3): proof_chain is **sound over its +declared atoms**, not grounded in recognized input. This module declares structure +only. +""" + +from __future__ import annotations + +from dataclasses import dataclass + + +class ProofError(ValueError): + """Raised on malformed proof input. Refusal-first; never coerces.""" + + +@dataclass(frozen=True, slots=True) +class ProofNode: + """One node of a proof DAG. + + ``node_id`` becomes the binding-graph ``symbol_id`` / ``lhs_symbol_id`` and so + must be a Python identifier. ``formula`` is an ADR-0202 propositional string. + ``depends_on`` names the nodes this one is derived from (→ the equation's + ``dependencies``). ``rule`` is the inference label (→ ``operation_kind``); + ``"premise"`` for an assumption (no ``depends_on``).""" + + node_id: str + formula: str + depends_on: tuple[str, ...] + rule: str + + def __post_init__(self) -> None: + object.__setattr__(self, "depends_on", tuple(self.depends_on)) + if not self.node_id or not self.node_id.isidentifier(): + raise ProofError(f"ProofNode.node_id must be a Python identifier; got {self.node_id!r}") + if not self.formula.strip(): + raise ProofError("ProofNode.formula must be non-empty") + if not self.rule: + raise ProofError("ProofNode.rule must be non-empty") + if self.node_id in self.depends_on: + # A self-dependency is a length-1 cycle; the binding-graph acyclicity + # guard (ADR-0203) would also catch it, but refuse early and clearly. + raise ProofError(f"ProofNode {self.node_id!r} depends on itself") + + +@dataclass(frozen=True, slots=True) +class Proof: + """A proof DAG: nodes plus the designated conclusion node. + + Construction validates only proof-shape integrity (unique ids, conclusion + exists, dependencies name declared nodes). Acyclicity and referential + integrity at the symbol level are enforced by the binding graph at build + time (ADR-0203 / ADR-0132) — deliberately, so the guard fires through the + real builder path rather than a duplicate pre-check.""" + + nodes: tuple[ProofNode, ...] + conclusion_id: str + + def __post_init__(self) -> None: + object.__setattr__(self, "nodes", tuple(self.nodes)) + if not self.nodes: + raise ProofError("Proof must have at least one node") + ids = [n.node_id for n in self.nodes] + if len(ids) != len(set(ids)): + raise ProofError(f"duplicate ProofNode.node_id: {ids}") + known = set(ids) + for node in self.nodes: + for dep in node.depends_on: + if dep not in known: + raise ProofError( + f"ProofNode {node.node_id!r} depends on undeclared node {dep!r}" + ) + if self.conclusion_id not in known: + raise ProofError(f"conclusion_id {self.conclusion_id!r} is not a declared node") + + +def proof_from_premises( + premises: tuple[str, ...], conclusion: str, *, rule: str +) -> Proof: + """Desugar the ``premises``/``conclusion``/``rule`` corpus shape onto ``Proof``. + + Each premise becomes a ``rule="premise"`` node with no dependencies; the + conclusion becomes one node with ``rule=rule`` depending on every premise.""" + nodes: list[ProofNode] = [] + premise_ids: list[str] = [] + for i, formula in enumerate(premises): + nid = f"premise_{i}" + premise_ids.append(nid) + nodes.append(ProofNode(node_id=nid, formula=formula, depends_on=(), rule="premise")) + nodes.append( + ProofNode(node_id="conclusion", formula=conclusion, + depends_on=tuple(premise_ids), rule=rule) + ) + return Proof(nodes=tuple(nodes), conclusion_id="conclusion") diff --git a/tests/test_proof_chain_builder.py b/tests/test_proof_chain_builder.py new file mode 100644 index 00000000..4faa496a --- /dev/null +++ b/tests/test_proof_chain_builder.py @@ -0,0 +1,160 @@ +"""ADR-0204 — proof-graph builder (phase 2.2, structure only). + +Proves the builder in isolation before any inference rule sits on it: +1. valid proof DAGs construct cleanly; +2. the corpus cycle case (PC-CYCLE-001) refuses through the REAL builder path — + the ADR-0203 guard firing on a real proof construction for the first time; +3. canonical_key round-trips byte-identically through rhs_canonical; +plus the admissibility-dispatch confirmation (proof operation_kinds refuse +gracefully, never misroute into the math checkers) and referential/out-of-regime +refusals inherited from the real substrate. +""" + +from __future__ import annotations + +import pytest + +from generate.binding_graph import ( + AdmissibilityError, + BindingGraphError, + check_admissibility, +) +from generate.logic_canonical import LogicRegimeError, canonicalize +from generate.proof_chain import ( + PROOF_NO_UNIT, + Proof, + ProofError, + ProofNode, + build_proof_graph, + proof_from_premises, +) + + +# --------------------------------------------------------------------------- +# 1. Valid proof DAGs construct cleanly +# --------------------------------------------------------------------------- + + +def test_valid_modus_ponens_shape_constructs() -> None: + # PC-MP-001 desugared. The STRUCTURE builds; the modus_ponens CHECK is 2.3. + proof = proof_from_premises( + ("P_rains -> Q_ground_wet", "P_rains"), "Q_ground_wet", rule="modus_ponens" + ) + pg = build_proof_graph(proof) + assert pg.conclusion_symbol_id == "conclusion" + assert len(pg.graph.equations) == 3 + concl = next(e for e in pg.graph.equations if e.lhs_symbol_id == "conclusion") + assert concl.operation_kind == "modus_ponens" + assert concl.dependencies == frozenset({"premise_0", "premise_1"}) + # Premises are equations with empty deps and operation_kind="premise". + prem = next(e for e in pg.graph.equations if e.lhs_symbol_id == "premise_0") + assert prem.operation_kind == "premise" + assert prem.dependencies == frozenset() + assert prem.unit_proof == PROOF_NO_UNIT + + +def test_multistep_dag_constructs() -> None: + # n1 (premise), n2 (premise), n3 := f(n1,n2), n4 := f(n3) — strict DAG. + proof = Proof( + nodes=( + ProofNode("n1", "P", (), "premise"), + ProofNode("n2", "P -> Q", (), "premise"), + ProofNode("n3", "Q", ("n1", "n2"), "modus_ponens"), + ProofNode("n4", "Q | R", ("n3",), "or_intro"), + ), + conclusion_id="n4", + ) + pg = build_proof_graph(proof) + assert len(pg.graph.equations) == 4 + + +# --------------------------------------------------------------------------- +# 2. PC-CYCLE-001 refuses through the REAL builder path +# --------------------------------------------------------------------------- + + +def test_corpus_cycle_refuses_through_builder() -> None: + # PC-CYCLE-001: n1 depends_on n2, n2 depends_on n1. The 2.1 acyclicity guard + # must fire through real proof construction — not just standalone find_cycle. + proof = Proof( + nodes=( + ProofNode("n1", "P_rains", ("n2",), "modus_ponens"), + ProofNode("n2", "Q_ground_wet", ("n1",), "modus_ponens"), + ), + conclusion_id="n1", + ) + with pytest.raises(BindingGraphError) as exc: + build_proof_graph(proof) + assert "circular_dependency" in str(exc.value) + + +def test_self_dependency_refused_at_proof_model() -> None: + # A length-1 cycle is refused early and clearly by the Proof model. + with pytest.raises(ProofError): + ProofNode("n1", "P", ("n1",), "modus_ponens") + + +def test_dangling_dependency_refuses() -> None: + with pytest.raises(ProofError): + Proof(nodes=(ProofNode("n1", "P", ("ghost",), "modus_ponens"),), conclusion_id="n1") + + +# --------------------------------------------------------------------------- +# 3. canonical_key round-trips byte-identically through rhs_canonical +# --------------------------------------------------------------------------- + + +def test_canonical_key_round_trips_byte_identical() -> None: + formula = "(P -> Q) & (R | ~S)" + proof = Proof(nodes=(ProofNode("n1", formula, (), "premise"),), conclusion_id="n1") + eq = build_proof_graph(proof).graph.equations[0] + assert eq.rhs_canonical == canonicalize(formula).canonical_key # byte-identical + + +def test_equivalent_node_formulas_share_rhs_canonical() -> None: + # Two nodes whose formulas are logically equivalent store identical + # rhs_canonical — the graph can decide equivalence by string comparison + # (the propositional twin of how the math graph uses rhs_canonical). + proof = Proof( + nodes=( + ProofNode("a", "P & Q", (), "premise"), + ProofNode("b", "Q & P", (), "premise"), + ), + conclusion_id="a", + ) + eqs = {e.lhs_symbol_id: e.rhs_canonical for e in build_proof_graph(proof).graph.equations} + assert eqs["a"] == eqs["b"] + + +# --------------------------------------------------------------------------- +# Admissibility-dispatch confirmation: proof operation_kinds refuse gracefully, +# never misroute into the math checkers (2.3's modus_ponens check hangs off this). +# --------------------------------------------------------------------------- + + +def test_proof_operation_kinds_refuse_in_admissibility_never_misroute() -> None: + proof = proof_from_premises(("P -> Q", "P"), "Q", rule="modus_ponens") + graph = build_proof_graph(proof).graph + symbols = {s.symbol_id: s for s in graph.symbols} + for eq in graph.equations: + with pytest.raises(AdmissibilityError) as exc: + check_admissibility(eq, symbols=symbols) + # premise (no deps) reaches the kind dispatch -> unknown_operation; + # modus_ponens (unitless deps) refuses at unit-resolution -> unit_unbound. + # Either way it REFUSES and never returns a math UnitProof / misroutes. + assert exc.value.reason in {"unknown_operation", "unit_unbound"} + + +# --------------------------------------------------------------------------- +# Out-of-regime formula in a node: the builder inherits the canonicalizer's +# typed refusal (honesty boundary — no silent admission of predicate logic). +# --------------------------------------------------------------------------- + + +def test_out_of_regime_node_formula_refuses() -> None: + proof = Proof( + nodes=(ProofNode("n1", "forall x. rains(x)", (), "premise"),), + conclusion_id="n1", + ) + with pytest.raises(LogicRegimeError): + build_proof_graph(proof)