core-labs/core
1
0
Fork 0
Code Issues Pull requests 1 Projects Releases Packages Wiki Activity Actions

feat: proof-graph builder — proof_chain's first binding-graph consumer (ADR-0204)

Browse source 
Phase 2.2, structure only (no inference rule — modus_ponens is 2.3). Translates a
Proof into a SemanticSymbolicBindingGraph; the ADR-0203 acyclicity guard + ADR-0132
referential integrity fire at construction.

- generate/proof_chain/model.py: the one canonical proof input shape (ProofNode/Proof
  + proof_from_premises desugaring of the corpus premises/conclusion shape).
- generate/proof_chain/builder.py: build_proof_graph — node→symbol+equation;
  canonical_key→rhs_canonical, depends_on→dependencies, rule→operation_kind;
  premises = empty-deps/op="premise"; unit_proof=PROOF_NO_UNIT, admissibility="pending";
  conclusion tracked as conclusion_symbol_id.
- tests: 9 — valid DAG (PC-MP-001 desugared) + multistep construct; PC-CYCLE-001
  refuses THROUGH the real builder (circular_dependency); canonical_key round-trips
  byte-identical + equivalent formulas share rhs_canonical; admissibility-dispatch
  confirmation; self/dangling refusals; out-of-regime node refuses. Mutation-verified
  (drop dep-wiring -> cycle admitted -> test fails).

Admissibility dispatch confirmed graceful on proof operation_kinds: unknown kinds
-> AdmissibilityError(unknown_operation), unitless deps -> unit_unbound; NEVER
misroutes into _check_additive. Named 2.3 constraint: check_admissibility runs
_resolve_dep_units before dispatch, so modus_ponens must bypass unit-resolution.

Open items named for 2.3 (ADR-0204): conclusion typing (BoundUnknown revisit),
semantic_role="unknown" (closed vocab has no "proposition"), unit_proof sentinel.

Additive (first consumer; math lane untouched). Full binding-graph surface green;
smoke 67. Honesty boundary: through 2.3, sound over declared atoms, not grounded in input.
This commit is contained in:
Shay 2026-06-02 19:53:41 -07:00
parent 6ee6bb7915
commit 4cae904563
5 changed files with 520 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

117
docs/decisions/ADR-0204-proof-graph-builder.md Normal file
View file

@ -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.

33
generate/proof_chain/__init__.py Normal file
View file

@ -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",
)

108
generate/proof_chain/builder.py Normal file
View file

@ -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)

102
generate/proof_chain/model.py Normal file
View file

@ -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")

160
tests/test_proof_chain_builder.py Normal file
View file

@ -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)