Commit graph

2 commits

Author SHA1 Message Date
Shay
6cbaa74076
feat(binding-graph): Phase 3 unit-aware admissibility (ADR-0134) (#176)
Wires deterministic, refusal-first dimensional analysis into the
binding-graph adapter. Every BoundEquation emitted by
bind_math_problem_graph now carries either admissibility_status='admitted'
+ populated unit_proof or admissibility_status='refused' + typed
refusal_reason. No silent coercion; no invented units; no solver.

Adds:
- generate/binding_graph/units.py — pure unit algebra over a 6-dim
  integer exponent vector (length, time, mass, money, count,
  temperature). Closed vocabulary loaded once from en_units_v1
  (ADR-0127) and memoized; composite "<num>_per_<denom>" resolved
  recursively; conservative depluralization; refusal-first.
- generate/binding_graph/admissibility.py — check_admissibility with
  per-operation-kind dispatch over the closed 8-string vocab, typed
  AdmissibilityError (closed reason set), frozen UnitProof.
- ADR-0134 documenting the contract, invariants, and Phase 4-5
  deferrals.

Adapter changes are surgical: synthesizes operand-literal symbols where
the verifier needs them (op<NNN>__multiplicand / __divisor / __rate),
then stamps each equation via check_admissibility. Input/output types
unchanged; bind_math_problem_graph still byte-equal across runs.

Tests: 226 total in the binding-graph lane (110 Phase 1+2 still pass; 47
units + 40 admissibility + 29 adapter-units new). Pyright clean on all
new files. No runtime wiring outside generate/binding_graph/.

Phase 4 (question-target binding) and Phase 5 (B3 / bounded grammar)
remain deferred per the brief.
2026-05-23 11:07:05 -07:00
Shay
5b668cc866
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).
2026-05-23 10:45:15 -07:00