feat(binding-graph): Phase 2 adapter from MathProblemGraph (ADR-0133) (#174)

Pure-function adapter `bind_math_problem_graph(g) ->
SemanticSymbolicBindingGraph` translating ADR-0115 `MathProblemGraph`
into the ADR-0132 binding-graph data model. Structural translation
only — no I/O, no parser/solver calls, no algebra, no numpy, no
runtime wiring.

Mapping discipline locked as module-level constants:
- each entity      -> SymbolBinding(semantic_role="entity")
- each possession  -> SymbolBinding(quantity) + BoundFact
- each Operation   -> fresh result SymbolBinding + BoundEquation
                      (operation_kind verbatim passthrough on the
                       shared closed vocab)
- Unknown          -> synthesized SymbolBinding(unknown) + BoundUnknown

Refusal-first: `g: object` boundary accepts any caller input and
refuses non-MathProblemGraph with typed AdapterError (sibling of
BindingGraphError). Cross-collection invariant failures (defensive,
should be unreachable) are re-raised as AdapterError so callers see a
single refusal type.

Phase 2 placeholders (closed in Phase 3+):
- BoundEquation.unit_proof = "deferred_to_phase_3"
- BoundEquation.admissibility_status = "pending"

Phase 3 (ADR-0134 unit-aware admissibility), Phase 4 (question-target
binding refinement), and Phase 5 (bounded-grammar / B3 integration)
explicitly deferred — see ADR.

Evidence:
- generate/binding_graph/adapter.py (pure functions)
- generate/binding_graph/__init__.py (public surface)
- tests/test_binding_graph_adapter.py — 41 tests (refusal-first, all
  8 VALID_OPERATION_KINDS round-trip, dep wiring, introduction order,
  hash-stability, frozen output, input immutability, placeholder
  constants, cross-collection invariants)
- docs/decisions/ADR-0133-binding-graph-adapter.md

Lane: tests/test_binding_graph_model.py + tests/test_binding_graph_adapter.py
      -> 110 passed, 0 failed. pyright clean on new files. Runtime
      byte-identical to main (no runtime integration yet, by design).

docs/decisions/ADR-0133-binding-graph-adapter.md

@@ -0,0 +1,148 @@
+# ADR-0133 — Semantic-Symbolic Binding Graph: Phase 2 adapter from `MathProblemGraph`
+
+**Status:** Accepted (Phase 2 only; Phases 3–5 deferred)
+**Date:** 2026-05-23
+**Parent:** ADR-0132 (Phase 1 data model, PR #171)
+**Related:** ADR-0115 (`MathProblemGraph` origin), ADR-0126 (candidate-graph
+parser), ADR-0127 (units pack), ADR-0131 (math-expert rebench / proof corridor),
+PR #170 (binding-graph proposal)
+
+---
+
+## Context
+
+ADR-0132 (PR #171) ratified Phase 1 of the binding-graph layer: a pure data
+model under `generate/binding_graph/` with frozen dataclasses, deterministic
+symbol allocation, refusal-first construction, and no coupling to the symbolic
+substrate (`Polynomial`) — symbolic expressions are referenced by canonical
+string form only.
+
+The proposal in PR #170 recommends shipping the binding graph in phases. With
+the data model locked, the next reviewable seam is a **pure-function adapter**
+from the existing ADR-0115 `MathProblemGraph` (the math-word-problem parser's
+output) into a `SemanticSymbolicBindingGraph`. Adding the adapter without
+runtime wiring keeps the abstraction reviewable in isolation before any
+runtime behavior depends on it.
+
+## Decision
+
+Add `generate/binding_graph/adapter.py` exposing
+`bind_math_problem_graph(g) -> SemanticSymbolicBindingGraph` and a typed
+`AdapterError` (sibling of `BindingGraphError` — both `ValueError` subclasses,
+refusal-first by design).
+
+The adapter is **pure**: no I/O, no parser calls, no solver calls, no algebra,
+no `numpy`. It performs structural translation only. Mapping discipline is
+locked as module-level constants:
+
+| Source (`MathProblemGraph`)            | Output (`SemanticSymbolicBindingGraph`)                                                                                          |
+| --------------------------------------- | -------------------------------------------------------------------------------------------------------------------------------- |
+| each `entity` (str)                     | one `SymbolBinding` with `semantic_role="entity"`, `symbol_id="entity_<slug>"`                                                   |
+| each `InitialPossession`                | one `SymbolBinding` (`semantic_role="quantity"`, `symbol_id="q_<entity>_<unit>_t0"`) plus one `BoundFact(value=str(value))`      |
+| each `Operation` (index `i`)            | one fresh `SymbolBinding` (`symbol_id="op_{i:03d}_result"`) plus one `BoundEquation` with `operation_kind` **verbatim** from source |
+| `Unknown`                               | one synthesized `SymbolBinding` (`semantic_role="unknown"`) plus one `BoundUnknown` referencing it                              |
+
+**Operation-kind passthrough.** The closed vocab
+`MathProblemGraph.VALID_OPERATION_KINDS` is shared by design — the adapter
+emits `BoundEquation.operation_kind` as a verbatim string passthrough. No
+translation, no renaming.
+
+**Dependency wiring.** `BoundEquation.dependencies` references the t0
+quantity symbol(s) of the actor (and, where applicable, of
+`Operation.target` for `transfer` and of `Comparison.reference_actor` for
+`compare_*`), keyed on the unit hint derived from the operand. When no
+matching t0 symbol exists (e.g. an actor that started at implicit zero),
+the dependency set silently omits it — Phase 2 wires only what the source
+graph already pins.
+
+**Synthetic source spans.** `MathProblemGraph` carries no native source-text
+spans, so every span the adapter emits is synthesized with
+`source_id == "math_problem_graph"`. The brief calls for "skip span fields
+cleanly when absent" — Phase 2 implements this by anchoring every
+`SourceSpanLink` to a deterministic surface text derived from the binding's
+own identity. If a future revision of `MathProblemGraph` carries real spans,
+the adapter is the natural site to propagate them.
+
+**Determinism is load-bearing.** Two `MathProblemGraph` instances that compare
+equal produce two `SemanticSymbolicBindingGraph` instances that compare equal
+and serialize byte-identically via `to_canonical_string()`. This is asserted
+by `tests/test_binding_graph_adapter.py` via a hash-stability test that calls
+`bind_math_problem_graph` twice and compares both the structure and the
+canonical string.
+
+**Refusal-first.** The adapter accepts `object` at the signature boundary and
+refuses anything that is not a `MathProblemGraph` with a typed `AdapterError`.
+Cross-collection invariants violated downstream (these can only fire if the
+adapter itself has a bug) are re-raised as `AdapterError`, so callers see a
+single refusal type at the adapter boundary.
+
+## Phase 3+ deferred (explicit)
+
+The following remain out of scope for this ADR and are deferred to follow-up
+PRs:
+
+- **Phase 3 — Unit-aware equation admissibility (ADR-0134).** Every
+  `BoundEquation` Phase 2 emits carries
+  `unit_proof == "deferred_to_phase_3"` and
+  `admissibility_status == "pending"`. This is by design — dimensional
+  analysis is the substance of Phase 3, not Phase 2, and the placeholder
+  makes the gap unambiguous in artifact form. Phase 3's first commit
+  should be a test that asserts no equation carries the placeholder
+  anywhere except in this adapter's output, then the loop that closes
+  the gap.
+- **Phase 4 — Question-target binding refinement.** Phase 2 binds the
+  `Unknown` to a synthesized `SymbolBinding` (`semantic_role="unknown"`)
+  rather than to any prior t0 / result symbol. Phase 4 will resolve the
+  unknown against the operation chain when possible.
+- **Phase 5 — Bounded-grammar / B3 integration.** No runtime wiring;
+  `chat/`, `core/`, `generate/intent.py`, and `generate/realizer.py`
+  are untouched.
+
+## Trust boundary
+
+The adapter consumes a frozen, self-validating `MathProblemGraph` — already a
+trust-boundary-checked artifact (ADR-0115 refuses malformed input at
+construction time). The adapter introduces no new arbitrary-code execution,
+no filesystem access, no dynamic imports. The only widening of the trust
+boundary is at the signature: `g: object` accepts any caller input and the
+adapter is responsible for refusing non-`MathProblemGraph` inputs with a
+typed `AdapterError`. Tests pin this refusal.
+
+## Field invariant
+
+Untouched. The adapter never reaches `algebra/`, `field/`, or any runtime
+hot-path; `versor_condition` cannot be affected by this change.
+
+## Evidence
+
+- `generate/binding_graph/adapter.py` — adapter (≈300 lines, pure functions,
+  module-level mapping constants).
+- `generate/binding_graph/__init__.py` — public surface adds
+  `bind_math_problem_graph` and `AdapterError`.
+- `tests/test_binding_graph_adapter.py` — 41 tests covering: refusal on
+  non-graph input, all eight `VALID_OPERATION_KINDS` round-tripping verbatim,
+  dependency wiring (transfer, apply_rate, compare_additive), introduction
+  order preservation, hash-stability across runs, input immutability,
+  frozen-output invariants, Phase-2 placeholder constants
+  (`PHASE_2_UNIT_PROOF`, `PHASE_2_ADMISSIBILITY`), and cross-collection
+  reference invariants. Full lane `tests/test_binding_graph_model.py +
+  tests/test_binding_graph_adapter.py`: **110/0/0**. `pyright` clean on
+  new files.
+- Runtime byte-identical to main: no runtime integration introduced.
+
+## PR checklist
+
+- **Capability added:** typed, deterministic translation from
+  `MathProblemGraph` (ADR-0115) to `SemanticSymbolicBindingGraph` (ADR-0132).
+  No runtime wiring yet — Phase 2 is structural translation only.
+- **Invariant proven:** `bind(g) == bind(g)` byte-for-byte; two equal
+  `MathProblemGraph`s produce two equal binding graphs (hash-stability test).
+  All cross-collection references in the emitted binding graph resolve
+  against the emitted symbol table.
+- **CLI / suite:** `python3 -m pytest tests/test_binding_graph_model.py
+  tests/test_binding_graph_adapter.py` — 110 passed.
+- **Avoided:** hidden normalization, stochastic fallback, approximate
+  recall, dimensional-analysis-by-stealth, `Polynomial` coupling.
+- **Trust boundary:** widened only at the adapter signature (`g: object` →
+  refusal-first `AdapterError`); no new dynamic execution, no new
+  filesystem access.

generate/binding_graph/__init__.py

@@ -1,24 +1,29 @@
-"""ADR-0132 — Semantic-Symbolic Binding Graph, Phase 1 (data model only).
+"""ADR-0132/0133 — Semantic-Symbolic Binding Graph.
 
-This package introduces the typed compiler boundary between natural-language
-semantic parsing and symbolic/equational solving proposed in
-``docs/implementation/semantic-symbolic-binding-graph-proposal.md``.
+Phase 1 (ADR-0132): pure data layer (frozen dataclasses, deterministic
+allocator, refusal-first construction; no I/O, no parser, no algebra,
+no ``Polynomial`` coupling — symbolic expressions held as canonical
+strings only).
 
-Phase 1 is intentionally a pure data layer:
+Phase 2 (ADR-0133): pure-function adapter
+:func:`bind_math_problem_graph` translating
+:class:`generate.math_problem_graph.MathProblemGraph` (ADR-0115) into a
+:class:`SemanticSymbolicBindingGraph`. Still no runtime wiring.
 
-  - frozen dataclasses with immutable collections,
-  - deterministic symbol allocation,
-  - refusal-first construction (typed ``BindingGraphError``),
-  - no I/O, no parser calls, no algebra calls, no numpy,
-  - no coupling to ``generate.math_symbolic_normalizer.Polynomial``;
-    symbolic expressions are referenced by canonical string form only.
-
-Phases 2-5 (adapter, unit-aware binding, question target binding, bounded
-grammar integration) are deferred to follow-up PRs.
+Phases 3-5 (unit-aware equation binding / question-target binding /
+bounded-grammar integration) are deferred to follow-up PRs.
 """
 
 from __future__ import annotations
 
+from .adapter import (
+    INTRODUCED_BY,
+    PHASE_2_ADMISSIBILITY,
+    PHASE_2_UNIT_PROOF,
+    SYNTHETIC_SOURCE_ID,
+    AdapterError,
+    bind_math_problem_graph,
+)
 from .allocation import allocate_symbols
 from .model import (
     ADMISSIBILITY_STATUSES,
@@ -35,7 +40,12 @@ from .model import (
 
 __all__ = (
     "ADMISSIBILITY_STATUSES",
+    "INTRODUCED_BY",
+    "PHASE_2_ADMISSIBILITY",
+    "PHASE_2_UNIT_PROOF",
     "SEMANTIC_ROLES",
+    "SYNTHETIC_SOURCE_ID",
+    "AdapterError",
     "BindingGraphError",
     "BoundConstraint",
     "BoundEquation",
@@ -45,4 +55,5 @@ __all__ = (
     "SourceSpanLink",
     "SymbolBinding",
     "allocate_symbols",
+    "bind_math_problem_graph",
 )

generate/binding_graph/adapter.py

@@ -0,0 +1,366 @@
+"""ADR-0133 — Adapter: ``MathProblemGraph`` → ``SemanticSymbolicBindingGraph``.
+
+Phase 2 of the binding-graph layer (ADR-0132). This module is a pure,
+deterministic translation: it consumes a ratified
+:class:`generate.math_problem_graph.MathProblemGraph` (ADR-0115) and
+emits the corresponding
+:class:`generate.binding_graph.SemanticSymbolicBindingGraph`. No I/O, no
+parser calls, no solver calls, no algebra. The adapter is total on every
+well-formed ``MathProblemGraph`` and refuses (typed :class:`AdapterError`)
+otherwise.
+
+Mapping discipline (locked at top of module — see constants):
+
+  - each entity → one ``SymbolBinding`` with ``semantic_role='entity'``,
+  - each ``InitialPossession`` → one ``SymbolBinding``
+    (``semantic_role='quantity'``) + one ``BoundFact``,
+  - each ``Operation`` → one fresh result ``SymbolBinding`` plus one
+    ``BoundEquation`` whose ``operation_kind`` is a verbatim passthrough
+    of the source op kind (closed vocab is shared by design),
+  - the ``Unknown`` → one synthesized ``SymbolBinding``
+    (``semantic_role='unknown'``) + one ``BoundUnknown``.
+
+Phases 3+ deferred:
+
+  - unit-aware equation admissibility (Phase 3, ADR-0134),
+  - question-target binding refinement (Phase 4),
+  - bounded-grammar / B3 integration (Phase 5).
+
+Until Phase 3 lands, every emitted ``BoundEquation`` carries the
+placeholder ``unit_proof=PHASE_2_UNIT_PROOF`` and
+``admissibility_status='pending'``. This is by design — dimensional
+analysis belongs in the next ADR.
+"""
+
+from __future__ import annotations
+
+import re
+from typing import Final
+
+from generate.math_problem_graph import (
+    Comparison,
+    MathProblemGraph,
+    Operation,
+    Quantity,
+    Rate,
+)
+
+from .model import (
+    BindingGraphError,
+    BoundEquation,
+    BoundFact,
+    BoundUnknown,
+    SemanticSymbolicBindingGraph,
+    SourceSpanLink,
+    SymbolBinding,
+)
+
+# ---------------------------------------------------------------------------
+# Constants — locked mapping discipline (read these before editing logic).
+# ---------------------------------------------------------------------------
+
+#: ``source_id`` stamped onto every synthesized ``SourceSpanLink``.
+#: ``MathProblemGraph`` carries no native source-span information, so
+#: every span the adapter emits is synthetic and shares this id.
+SYNTHETIC_SOURCE_ID: Final[str] = "math_problem_graph"
+
+#: ``introduced_by`` stamped onto every ``SymbolBinding`` the adapter
+#: emits. Replaying the adapter therefore yields byte-equal symbols.
+INTRODUCED_BY: Final[str] = "bind_math_problem_graph"
+
+#: Placeholder ``unit_proof`` for every Phase 2 ``BoundEquation``.
+#: Phase 3 (ADR-0134) replaces this with a real dimensional proof token.
+PHASE_2_UNIT_PROOF: Final[str] = "deferred_to_phase_3"
+
+#: Every Phase 2 ``BoundEquation`` is emitted ``pending`` — the equation
+#: is structurally valid but unit-admissibility has not yet been checked.
+PHASE_2_ADMISSIBILITY: Final[str] = "pending"
+
+_SLUG_NON_ALNUM = re.compile(r"[^a-z0-9]+")
+
+
+# ---------------------------------------------------------------------------
+# Public error
+# ---------------------------------------------------------------------------
+
+
+class AdapterError(ValueError):
+    """Raised on malformed input to :func:`bind_math_problem_graph`.
+
+    Sibling of :class:`generate.binding_graph.BindingGraphError` —
+    refusal-first by design. The adapter never silently coerces an
+    unrecognized input type.
+    """
+
+
+# ---------------------------------------------------------------------------
+# Symbol-id helpers (pure)
+# ---------------------------------------------------------------------------
+
+
+def _slug(text: str) -> str:
+    """ASCII-lowercase slug; non-alnum runs collapse to ``_``."""
+    return _SLUG_NON_ALNUM.sub("_", text.strip().lower()).strip("_")
+
+
+def _safe_identifier(text: str, *, prefix: str) -> str:
+    """Return ``f"{prefix}_{slug}"``, defaulting to ``prefix + '_x'`` on
+    empty slug. Guarantees a valid Python identifier."""
+    s = _slug(text)
+    if s == "":
+        s = "x"
+    return f"{prefix}_{s}"
+
+
+def _entity_symbol_id(entity: str) -> str:
+    return _safe_identifier(entity, prefix="entity")
+
+
+def _quantity_symbol_id(entity: str, unit: str, tick: int) -> str:
+    return f"q_{_slug(entity) or 'x'}_{_slug(unit) or 'x'}_t{tick}"
+
+
+def _op_result_symbol_id(idx: int) -> str:
+    return f"op_{idx:03d}_result"
+
+
+def _unknown_symbol_id(entity: str | None, unit: str) -> str:
+    scope = _slug(entity) if entity is not None else "total"
+    if scope == "":
+        scope = "total"
+    unit_slug = _slug(unit) or "x"
+    return f"unknown_{scope}_{unit_slug}"
+
+
+def _span(text: str) -> SourceSpanLink:
+    """Synthesize a deterministic ``SourceSpanLink`` for ``text``.
+
+    ``MathProblemGraph`` carries no native span information; Phase 2
+    therefore stamps every binding with a synthetic span anchored to
+    the rendered surface text. The span is byte-stable per input.
+    """
+    if not isinstance(text, str) or text == "":
+        # Defensive: every caller passes non-empty text. Refuse rather
+        # than silently substitute.
+        raise AdapterError("synthetic span text must be a non-empty str")
+    return SourceSpanLink(
+        source_id=SYNTHETIC_SOURCE_ID, start=0, end=len(text), text=text
+    )
+
+
+# ---------------------------------------------------------------------------
+# RHS canonicalization (deterministic, string-only — no Polynomial coupling)
+# ---------------------------------------------------------------------------
+
+
+def _format_quantity(q: Quantity) -> str:
+    return f"{q.value} {q.unit}"
+
+
+def _format_rate(r: Rate) -> str:
+    return f"{r.value} {r.numerator_unit}/{r.denominator_unit}"
+
+
+def _format_comparison(c: Comparison) -> str:
+    if c.delta is not None:
+        return (
+            f"{c.direction}({c.reference_actor}, "
+            f"delta={_format_quantity(c.delta)})"
+        )
+    return f"{c.direction}({c.reference_actor}, factor={c.factor})"
+
+
+def _format_operand(operand: Quantity | Rate | Comparison) -> str:
+    if isinstance(operand, Quantity):
+        return _format_quantity(operand)
+    if isinstance(operand, Rate):
+        return _format_rate(operand)
+    return _format_comparison(operand)
+
+
+def _format_rhs(op: Operation) -> str:
+    head = f"{op.kind}({op.actor}"
+    if op.target is not None:
+        head += f"->{op.target}"
+    return head + f", {_format_operand(op.operand)})"
+
+
+def _operand_unit_hint(operand: Quantity | Rate | Comparison) -> str | None:
+    """The most relevant unit a dependency lookup should key on.
+
+    Used only for wiring deterministic ``BoundEquation.dependencies``
+    against pre-existing t0 symbols. Unit-aware *admissibility* is
+    Phase 3.
+    """
+    if isinstance(operand, Quantity):
+        return operand.unit
+    if isinstance(operand, Rate):
+        return operand.denominator_unit
+    if operand.delta is not None:
+        return operand.delta.unit
+    return None
+
+
+# ---------------------------------------------------------------------------
+# Public adapter
+# ---------------------------------------------------------------------------
+
+
+def bind_math_problem_graph(
+    g: object,
+) -> SemanticSymbolicBindingGraph:
+    """Translate a ``MathProblemGraph`` into a ``SemanticSymbolicBindingGraph``.
+
+    Pure function. Deterministic: ``bind_math_problem_graph(g) ==
+    bind_math_problem_graph(g)`` byte-for-byte, and two graphs that
+    compare equal (``g1 == g2``) produce two binding graphs that compare
+    equal. Input is never mutated (cannot be — ``MathProblemGraph`` is
+    frozen — but the contract is asserted by tests).
+
+    Raises :class:`AdapterError` if ``g`` is not a
+    :class:`MathProblemGraph`. Every well-formed ``MathProblemGraph``
+    produces a well-formed ``SemanticSymbolicBindingGraph`` — the
+    adapter is total on the input type's image.
+    """
+    if not isinstance(g, MathProblemGraph):
+        raise AdapterError(
+            "bind_math_problem_graph requires a MathProblemGraph; "
+            f"got {type(g).__name__}"
+        )
+
+    symbols: list[SymbolBinding] = []
+    facts: list[BoundFact] = []
+    equations: list[BoundEquation] = []
+    seen_ids: set[str] = set()
+
+    def _add(sym: SymbolBinding) -> None:
+        if sym.symbol_id in seen_ids:
+            # Idempotent — same symbol re-emitted from a different
+            # construction path collapses cleanly.
+            return
+        seen_ids.add(sym.symbol_id)
+        symbols.append(sym)
+
+    # ---- Entities (order of introduction) ---------------------------------
+    for entity in g.entities:
+        _add(
+            SymbolBinding(
+                symbol_id=_entity_symbol_id(entity),
+                name=entity,
+                semantic_role="entity",
+                source_span=_span(entity),
+                introduced_by=INTRODUCED_BY,
+                entity=entity,
+            )
+        )
+
+    # ---- Initial state → t0 quantity symbols + grounded facts -------------
+    t0_index: dict[tuple[str, str], str] = {}
+    for poss in g.initial_state:
+        sid = _quantity_symbol_id(poss.entity, poss.quantity.unit, 0)
+        span_text = f"{poss.entity}|{poss.quantity.unit}|t0"
+        _add(
+            SymbolBinding(
+                symbol_id=sid,
+                name=f"{poss.entity}.{poss.quantity.unit}@t0",
+                semantic_role="quantity",
+                source_span=_span(span_text),
+                introduced_by=INTRODUCED_BY,
+                entity=poss.entity,
+                unit=poss.quantity.unit,
+            )
+        )
+        facts.append(
+            BoundFact(
+                symbol_id=sid,
+                value=str(poss.quantity.value),
+                source_span=_span(span_text),
+                unit=poss.quantity.unit,
+            )
+        )
+        t0_index[(poss.entity, poss.quantity.unit)] = sid
+
+    # ---- Operations → fresh result symbol + bound equation ----------------
+    for idx, op in enumerate(g.operations):
+        result_sid = _op_result_symbol_id(idx)
+        op_span_text = f"op{idx:03d}|{op.kind}|{op.actor}"
+        _add(
+            SymbolBinding(
+                symbol_id=result_sid,
+                name=f"op{idx}.{op.kind}.{op.actor}",
+                semantic_role="quantity",
+                source_span=_span(op_span_text),
+                introduced_by=INTRODUCED_BY,
+                entity=op.actor,
+            )
+        )
+
+        deps: set[str] = set()
+        unit_hint = _operand_unit_hint(op.operand)
+        if unit_hint is not None:
+            actor_sid = t0_index.get((op.actor, unit_hint))
+            if actor_sid is not None:
+                deps.add(actor_sid)
+            if op.target is not None:
+                target_sid = t0_index.get((op.target, unit_hint))
+                if target_sid is not None:
+                    deps.add(target_sid)
+            if isinstance(op.operand, Comparison):
+                ref_sid = t0_index.get(
+                    (op.operand.reference_actor, unit_hint)
+                )
+                if ref_sid is not None:
+                    deps.add(ref_sid)
+
+        equations.append(
+            BoundEquation(
+                lhs_symbol_id=result_sid,
+                rhs_canonical=_format_rhs(op),
+                dependencies=frozenset(deps),
+                operation_kind=op.kind,  # passthrough — shared closed vocab
+                unit_proof=PHASE_2_UNIT_PROOF,
+                admissibility_status=PHASE_2_ADMISSIBILITY,
+                source_span=_span(op_span_text),
+            )
+        )
+
+    # ---- Unknown → synthesized unknown symbol + BoundUnknown --------------
+    unk = g.unknown
+    unk_sid = _unknown_symbol_id(unk.entity, unk.unit)
+    unk_text = (
+        f"{unk.entity}|{unk.unit}" if unk.entity is not None else f"total|{unk.unit}"
+    )
+    _add(
+        SymbolBinding(
+            symbol_id=unk_sid,
+            name=unk_text,
+            semantic_role="unknown",
+            source_span=_span(unk_text),
+            introduced_by=INTRODUCED_BY,
+            entity=unk.entity,
+            unit=unk.unit,
+        )
+    )
+    unknowns = (
+        BoundUnknown(
+            symbol_id=unk_sid,
+            question_span=_span(unk_text),
+            expected_unit=unk.unit,
+        ),
+    )
+
+    try:
+        return SemanticSymbolicBindingGraph(
+            symbols=tuple(symbols),
+            facts=tuple(facts),
+            equations=tuple(equations),
+            unknowns=unknowns,
+        )
+    except BindingGraphError as exc:
+        # Cross-collection invariants of ``SemanticSymbolicBindingGraph``
+        # are stricter than ``MathProblemGraph``'s own checks. Surface
+        # any such failure as an ``AdapterError`` so callers see a single
+        # refusal type at the adapter boundary.
+        raise AdapterError(
+            f"adapter produced an invalid binding graph: {exc}"
+        ) from exc

tests/test_binding_graph_adapter.py

@@ -0,0 +1,516 @@
+"""ADR-0133 — Tests for the MathProblemGraph → BindingGraph adapter.
+
+Covers:
+  - refusal-first on malformed input (typed ``AdapterError``),
+  - per-operation-kind round-trip (string passthrough on the closed vocab),
+  - entity / quantity / unknown mapping discipline,
+  - deterministic introduction-order preservation,
+  - dependency wiring against pre-existing t0 symbols,
+  - byte-equal idempotency across runs (hash-stability),
+  - input immutability and frozen-output invariants,
+  - Phase-2 placeholders for ``unit_proof`` + admissibility (Phase 3+ deferred).
+
+Pure data — no runtime, no algebra, no parser imports.
+"""
+
+from __future__ import annotations
+
+import dataclasses
+
+import pytest
+
+from generate.binding_graph import (
+    INTRODUCED_BY,
+    PHASE_2_ADMISSIBILITY,
+    PHASE_2_UNIT_PROOF,
+    SYNTHETIC_SOURCE_ID,
+    AdapterError,
+    BoundEquation,
+    BoundFact,
+    BoundUnknown,
+    SemanticSymbolicBindingGraph,
+    SymbolBinding,
+    bind_math_problem_graph,
+)
+from generate.math_problem_graph import (
+    VALID_OPERATION_KINDS,
+    Comparison,
+    InitialPossession,
+    MathProblemGraph,
+    Operation,
+    Quantity,
+    Rate,
+    Unknown,
+)
+
+
+# ---------------------------------------------------------------------------
+# Fixtures
+# ---------------------------------------------------------------------------
+
+
+def _q(value: int | float, unit: str) -> Quantity:
+    return Quantity(value=value, unit=unit)
+
+
+def _trivial_graph() -> MathProblemGraph:
+    return MathProblemGraph(
+        entities=("Sam",),
+        initial_state=(InitialPossession(entity="Sam", quantity=_q(3, "apples")),),
+        operations=(),
+        unknown=Unknown(entity="Sam", unit="apples"),
+    )
+
+
+def _two_actor_add_graph() -> MathProblemGraph:
+    return MathProblemGraph(
+        entities=("Sam", "Mary"),
+        initial_state=(
+            InitialPossession(entity="Sam", quantity=_q(3, "apples")),
+            InitialPossession(entity="Mary", quantity=_q(5, "apples")),
+        ),
+        operations=(
+            Operation(actor="Sam", kind="add", operand=_q(2, "apples")),
+        ),
+        unknown=Unknown(entity=None, unit="apples"),
+    )
+
+
+def _transfer_graph() -> MathProblemGraph:
+    return MathProblemGraph(
+        entities=("Sam", "Mary"),
+        initial_state=(
+            InitialPossession(entity="Sam", quantity=_q(7, "apples")),
+            InitialPossession(entity="Mary", quantity=_q(1, "apples")),
+        ),
+        operations=(
+            Operation(
+                actor="Sam",
+                kind="transfer",
+                operand=_q(3, "apples"),
+                target="Mary",
+            ),
+        ),
+        unknown=Unknown(entity="Mary", unit="apples"),
+    )
+
+
+def _rate_graph() -> MathProblemGraph:
+    return MathProblemGraph(
+        entities=("Sam",),
+        initial_state=(InitialPossession(entity="Sam", quantity=_q(4, "apple")),),
+        operations=(
+            Operation(
+                actor="Sam",
+                kind="apply_rate",
+                operand=Rate(
+                    value=2.0, numerator_unit="dollars", denominator_unit="apple"
+                ),
+            ),
+        ),
+        unknown=Unknown(entity="Sam", unit="dollars"),
+    )
+
+
+def _compare_additive_graph() -> MathProblemGraph:
+    return MathProblemGraph(
+        entities=("Sam", "Mary"),
+        initial_state=(
+            InitialPossession(entity="Mary", quantity=_q(5, "apples")),
+        ),
+        operations=(
+            Operation(
+                actor="Sam",
+                kind="compare_additive",
+                operand=Comparison(
+                    reference_actor="Mary",
+                    delta=_q(2, "apples"),
+                    factor=None,
+                    direction="more",
+                ),
+            ),
+        ),
+        unknown=Unknown(entity="Sam", unit="apples"),
+    )
+
+
+def _compare_multiplicative_graph() -> MathProblemGraph:
+    return MathProblemGraph(
+        entities=("Sam", "Mary"),
+        initial_state=(
+            InitialPossession(entity="Mary", quantity=_q(5, "apples")),
+        ),
+        operations=(
+            Operation(
+                actor="Sam",
+                kind="compare_multiplicative",
+                operand=Comparison(
+                    reference_actor="Mary",
+                    delta=None,
+                    factor=3.0,
+                    direction="times",
+                ),
+            ),
+        ),
+        unknown=Unknown(entity="Sam", unit="apples"),
+    )
+
+
+# ---------------------------------------------------------------------------
+# 1-3. Refusal-first on malformed input
+# ---------------------------------------------------------------------------
+
+
+def test_adapter_refuses_non_graph_input() -> None:
+    with pytest.raises(AdapterError):
+        bind_math_problem_graph({"entities": ()})  # type: ignore[arg-type]
+
+
+def test_adapter_refuses_none() -> None:
+    with pytest.raises(AdapterError):
+        bind_math_problem_graph(None)  # type: ignore[arg-type]
+
+
+def test_adapter_refuses_string() -> None:
+    with pytest.raises(AdapterError):
+        bind_math_problem_graph("not a graph")  # type: ignore[arg-type]
+
+
+# ---------------------------------------------------------------------------
+# 4-7. Minimal-graph shape
+# ---------------------------------------------------------------------------
+
+
+def test_trivial_graph_emits_expected_symbol_count() -> None:
+    bg = bind_math_problem_graph(_trivial_graph())
+    # 1 entity + 1 initial-quantity + 1 unknown synthesis
+    assert len(bg.symbols) == 3
+    assert len(bg.facts) == 1
+    assert len(bg.equations) == 0
+    assert len(bg.unknowns) == 1
+
+
+def test_entity_symbol_has_entity_role_and_slug() -> None:
+    bg = bind_math_problem_graph(_trivial_graph())
+    entity_syms = [s for s in bg.symbols if s.semantic_role == "entity"]
+    assert len(entity_syms) == 1
+    assert entity_syms[0].symbol_id == "entity_sam"
+    assert entity_syms[0].name == "Sam"
+    assert entity_syms[0].entity == "Sam"
+
+
+def test_initial_possession_emits_fact_with_str_value_and_unit() -> None:
+    bg = bind_math_problem_graph(_trivial_graph())
+    fact = bg.facts[0]
+    assert fact.symbol_id == "q_sam_apples_t0"
+    assert fact.value == "3"
+    assert fact.unit == "apples"
+
+
+def test_initial_quantity_symbol_has_quantity_role_and_unit() -> None:
+    bg = bind_math_problem_graph(_trivial_graph())
+    quant_syms = [
+        s
+        for s in bg.symbols
+        if s.semantic_role == "quantity" and s.symbol_id.startswith("q_")
+    ]
+    assert len(quant_syms) == 1
+    assert quant_syms[0].unit == "apples"
+    assert quant_syms[0].entity == "Sam"
+
+
+# ---------------------------------------------------------------------------
+# 8-9. Unknown handling
+# ---------------------------------------------------------------------------
+
+
+def test_unknown_bound_to_synthesized_symbol() -> None:
+    bg = bind_math_problem_graph(_trivial_graph())
+    unk = bg.unknowns[0]
+    syms_by_id = {s.symbol_id: s for s in bg.symbols}
+    assert unk.symbol_id in syms_by_id
+    assert syms_by_id[unk.symbol_id].semantic_role == "unknown"
+    assert unk.expected_unit == "apples"
+
+
+def test_unknown_entity_none_renders_total_scope() -> None:
+    bg = bind_math_problem_graph(_two_actor_add_graph())
+    unk = bg.unknowns[0]
+    assert unk.symbol_id == "unknown_total_apples"
+
+
+# ---------------------------------------------------------------------------
+# 10-17. Per-operation-kind passthrough (covers all 8 in VALID_OPERATION_KINDS)
+# ---------------------------------------------------------------------------
+
+
+@pytest.mark.parametrize(
+    "kind,operand,target",
+    [
+        ("add", _q(2, "apples"), None),
+        ("subtract", _q(2, "apples"), None),
+        ("multiply", _q(2, "apples"), None),
+        ("divide", _q(2, "apples"), None),
+    ],
+)
+def test_simple_operation_kind_passthrough(
+    kind: str, operand: Quantity, target: str | None
+) -> None:
+    g = MathProblemGraph(
+        entities=("Sam",),
+        initial_state=(
+            InitialPossession(entity="Sam", quantity=_q(10, "apples")),
+        ),
+        operations=(Operation(actor="Sam", kind=kind, operand=operand, target=target),),
+        unknown=Unknown(entity="Sam", unit="apples"),
+    )
+    bg = bind_math_problem_graph(g)
+    assert len(bg.equations) == 1
+    assert bg.equations[0].operation_kind == kind
+    # passthrough must match the source closed vocab verbatim
+    assert bg.equations[0].operation_kind in VALID_OPERATION_KINDS
+
+
+def test_transfer_passthrough_and_dep_on_both_actors() -> None:
+    bg = bind_math_problem_graph(_transfer_graph())
+    eq = bg.equations[0]
+    assert eq.operation_kind == "transfer"
+    assert "q_sam_apples_t0" in eq.dependencies
+    assert "q_mary_apples_t0" in eq.dependencies
+
+
+def test_apply_rate_passthrough_and_dep_on_denominator_unit() -> None:
+    bg = bind_math_problem_graph(_rate_graph())
+    eq = bg.equations[0]
+    assert eq.operation_kind == "apply_rate"
+    # Sam holds 'apple' (denominator); dep wires there.
+    assert "q_sam_apple_t0" in eq.dependencies
+
+
+def test_compare_additive_passthrough_and_dep_on_reference() -> None:
+    bg = bind_math_problem_graph(_compare_additive_graph())
+    eq = bg.equations[0]
+    assert eq.operation_kind == "compare_additive"
+    assert "q_mary_apples_t0" in eq.dependencies
+
+
+def test_compare_multiplicative_passthrough() -> None:
+    bg = bind_math_problem_graph(_compare_multiplicative_graph())
+    eq = bg.equations[0]
+    assert eq.operation_kind == "compare_multiplicative"
+    # multiplicative comparison has no delta-unit → no t0 dep wired
+    assert eq.dependencies == frozenset()
+
+
+def test_all_eight_operation_kinds_round_trip() -> None:
+    # Sanity: brief mandates the closed vocab is shared by design.
+    # Each kind exercised individually above; here we just assert the
+    # vocab itself hasn't drifted under us.
+    assert VALID_OPERATION_KINDS == frozenset(
+        {
+            "add",
+            "subtract",
+            "transfer",
+            "multiply",
+            "divide",
+            "apply_rate",
+            "compare_additive",
+            "compare_multiplicative",
+        }
+    )
+
+
+# ---------------------------------------------------------------------------
+# 18-22. Determinism, immutability, hash-stability
+# ---------------------------------------------------------------------------
+
+
+def test_adapter_is_idempotent_on_equal_graphs() -> None:
+    a = bind_math_problem_graph(_two_actor_add_graph())
+    b = bind_math_problem_graph(_two_actor_add_graph())
+    assert a == b
+    assert a.to_canonical_string() == b.to_canonical_string()
+
+
+def test_canonical_string_is_byte_equal_across_runs() -> None:
+    g = _transfer_graph()
+    s1 = bind_math_problem_graph(g).to_canonical_string()
+    s2 = bind_math_problem_graph(g).to_canonical_string()
+    assert s1.encode("utf-8") == s2.encode("utf-8")
+
+
+def test_introduction_order_preserved_across_entities() -> None:
+    g = MathProblemGraph(
+        entities=("Zeta", "Alpha", "Mu"),
+        initial_state=(),
+        operations=(),
+        unknown=Unknown(entity="Alpha", unit="widgets"),
+    )
+    bg = bind_math_problem_graph(g)
+    entity_syms = [s for s in bg.symbols if s.semantic_role == "entity"]
+    assert [s.name for s in entity_syms] == ["Zeta", "Alpha", "Mu"]
+
+
+def test_input_graph_not_mutated() -> None:
+    g = _transfer_graph()
+    entities_before = g.entities
+    ops_before = g.operations
+    bind_math_problem_graph(g)
+    # Frozen + slots makes mutation impossible; assert object identity
+    # of the immutable tuples as a defense-in-depth contract.
+    assert g.entities is entities_before
+    assert g.operations is ops_before
+
+
+def test_output_dataclasses_are_frozen() -> None:
+    bg = bind_math_problem_graph(_trivial_graph())
+    sym = bg.symbols[0]
+    with pytest.raises(dataclasses.FrozenInstanceError):
+        sym.name = "mutated"  # type: ignore[misc]
+
+
+# ---------------------------------------------------------------------------
+# 23-26. Phase-2 placeholders + cross-collection invariants
+# ---------------------------------------------------------------------------
+
+
+def test_equation_unit_proof_is_phase2_placeholder() -> None:
+    bg = bind_math_problem_graph(_two_actor_add_graph())
+    assert bg.equations[0].unit_proof == PHASE_2_UNIT_PROOF
+    assert PHASE_2_UNIT_PROOF == "deferred_to_phase_3"
+
+
+def test_equation_admissibility_is_pending() -> None:
+    bg = bind_math_problem_graph(_two_actor_add_graph())
+    assert bg.equations[0].admissibility_status == PHASE_2_ADMISSIBILITY
+    assert PHASE_2_ADMISSIBILITY == "pending"
+
+
+def test_all_equation_dependencies_reference_known_symbols() -> None:
+    bg = bind_math_problem_graph(_transfer_graph())
+    known = {s.symbol_id for s in bg.symbols}
+    for eq in bg.equations:
+        assert eq.dependencies.issubset(known)
+
+
+def test_unknown_symbol_id_references_known_symbol() -> None:
+    bg = bind_math_problem_graph(_compare_additive_graph())
+    known = {s.symbol_id for s in bg.symbols}
+    assert bg.unknowns[0].symbol_id in known
+
+
+# ---------------------------------------------------------------------------
+# 27-31. Provenance + constants
+# ---------------------------------------------------------------------------
+
+
+def test_every_symbol_introduced_by_constant() -> None:
+    bg = bind_math_problem_graph(_transfer_graph())
+    for sym in bg.symbols:
+        assert sym.introduced_by == INTRODUCED_BY
+
+
+def test_synthetic_source_id_on_every_span() -> None:
+    bg = bind_math_problem_graph(_transfer_graph())
+    for sym in bg.symbols:
+        assert sym.source_span.source_id == SYNTHETIC_SOURCE_ID
+    for fact in bg.facts:
+        assert fact.source_span.source_id == SYNTHETIC_SOURCE_ID
+    for eq in bg.equations:
+        assert eq.source_span.source_id == SYNTHETIC_SOURCE_ID
+    for unk in bg.unknowns:
+        assert unk.question_span.source_id == SYNTHETIC_SOURCE_ID
+
+
+def test_op_result_symbol_id_is_deterministic_and_indexed() -> None:
+    g = MathProblemGraph(
+        entities=("Sam",),
+        initial_state=(InitialPossession(entity="Sam", quantity=_q(1, "u")),),
+        operations=(
+            Operation(actor="Sam", kind="add", operand=_q(1, "u")),
+            Operation(actor="Sam", kind="add", operand=_q(2, "u")),
+            Operation(actor="Sam", kind="add", operand=_q(3, "u")),
+        ),
+        unknown=Unknown(entity="Sam", unit="u"),
+    )
+    bg = bind_math_problem_graph(g)
+    lhs = [eq.lhs_symbol_id for eq in bg.equations]
+    assert lhs == ["op_000_result", "op_001_result", "op_002_result"]
+
+
+def test_rhs_canonical_contains_operation_kind() -> None:
+    bg = bind_math_problem_graph(_transfer_graph())
+    assert bg.equations[0].rhs_canonical.startswith("transfer(")
+
+
+def test_bound_unknown_is_single_target() -> None:
+    bg = bind_math_problem_graph(_compare_multiplicative_graph())
+    # Phase 2 promise: exactly one unknown binding per graph.
+    assert len(bg.unknowns) == 1
+    assert isinstance(bg.unknowns[0], BoundUnknown)
+
+
+# ---------------------------------------------------------------------------
+# 32-34. Misc edge cases
+# ---------------------------------------------------------------------------
+
+
+def test_graph_with_zero_operations_is_well_formed() -> None:
+    bg = bind_math_problem_graph(_trivial_graph())
+    assert bg.equations == ()
+    # round-trip stays valid under SemanticSymbolicBindingGraph invariants
+    assert isinstance(bg, SemanticSymbolicBindingGraph)
+
+
+def test_entity_with_spaces_slugifies_into_valid_identifier() -> None:
+    g = MathProblemGraph(
+        entities=("Mary Jane",),
+        initial_state=(
+            InitialPossession(entity="Mary Jane", quantity=_q(2, "apples")),
+        ),
+        operations=(),
+        unknown=Unknown(entity="Mary Jane", unit="apples"),
+    )
+    bg = bind_math_problem_graph(g)
+    entity_syms = [s for s in bg.symbols if s.semantic_role == "entity"]
+    assert entity_syms[0].symbol_id == "entity_mary_jane"
+    assert entity_syms[0].symbol_id.isidentifier()
+
+
+def test_fact_count_matches_initial_possession_count() -> None:
+    bg = bind_math_problem_graph(_two_actor_add_graph())
+    assert len(bg.facts) == 2
+
+
+def test_outputs_for_distinct_graphs_differ() -> None:
+    s1 = bind_math_problem_graph(_trivial_graph()).to_canonical_string()
+    s2 = bind_math_problem_graph(_transfer_graph()).to_canonical_string()
+    assert s1 != s2
+
+
+def test_symbol_table_has_no_duplicate_ids() -> None:
+    bg = bind_math_problem_graph(_transfer_graph())
+    ids = [s.symbol_id for s in bg.symbols]
+    assert len(ids) == len(set(ids))
+
+
+def test_equation_lhs_is_a_known_symbol() -> None:
+    bg = bind_math_problem_graph(_two_actor_add_graph())
+    known = {s.symbol_id for s in bg.symbols}
+    for eq in bg.equations:
+        assert eq.lhs_symbol_id in known
+
+
+def test_typeof_emitted_equation_is_bound_equation() -> None:
+    bg = bind_math_problem_graph(_two_actor_add_graph())
+    assert all(isinstance(eq, BoundEquation) for eq in bg.equations)
+
+
+def test_typeof_emitted_fact_is_bound_fact() -> None:
+    bg = bind_math_problem_graph(_trivial_graph())
+    assert all(isinstance(f, BoundFact) for f in bg.facts)
+
+
+def test_typeof_emitted_symbol_is_symbol_binding() -> None:
+    bg = bind_math_problem_graph(_trivial_graph())
+    assert all(isinstance(s, SymbolBinding) for s in bg.symbols)