6cbaa74076
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.
485 lines
15 KiB
Python
485 lines
15 KiB
Python
"""ADR-0134 — Equation admissibility check (per-kind dispatch).
|
||
|
||
Covers the closed eight-string ``operation_kind`` vocab with positive and
|
||
negative cases, plus the typed-refusal contract.
|
||
"""
|
||
|
||
from __future__ import annotations
|
||
|
||
import pytest
|
||
|
||
from generate.binding_graph import (
|
||
ADMISSIBILITY_REASONS,
|
||
AdmissibilityError,
|
||
BoundEquation,
|
||
SourceSpanLink,
|
||
SymbolBinding,
|
||
UnitProof,
|
||
check_admissibility,
|
||
parse_unit,
|
||
)
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# Builders
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
def _span(text: str = "x") -> SourceSpanLink:
|
||
return SourceSpanLink(source_id="t", start=0, end=len(text), text=text)
|
||
|
||
|
||
def _sym(
|
||
sid: str,
|
||
*,
|
||
unit: str | None = None,
|
||
role: str = "quantity",
|
||
) -> SymbolBinding:
|
||
return SymbolBinding(
|
||
symbol_id=sid,
|
||
name=sid,
|
||
semantic_role=role,
|
||
source_span=_span(sid),
|
||
introduced_by="test",
|
||
unit=unit,
|
||
)
|
||
|
||
|
||
def _eq(
|
||
*,
|
||
kind: str,
|
||
deps: frozenset[str],
|
||
lhs: str = "res",
|
||
) -> BoundEquation:
|
||
return BoundEquation(
|
||
lhs_symbol_id=lhs,
|
||
rhs_canonical=f"{kind}(test)",
|
||
dependencies=deps,
|
||
operation_kind=kind,
|
||
unit_proof="placeholder",
|
||
admissibility_status="pending",
|
||
source_span=_span(kind),
|
||
)
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# Closed refusal-reason vocab
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
def test_admissibility_reasons_is_closed_set() -> None:
|
||
assert isinstance(ADMISSIBILITY_REASONS, frozenset)
|
||
assert "unit_mismatch" in ADMISSIBILITY_REASONS
|
||
assert "unknown_unit" in ADMISSIBILITY_REASONS
|
||
assert "unit_unbound" in ADMISSIBILITY_REASONS
|
||
assert "unknown_symbol" in ADMISSIBILITY_REASONS
|
||
|
||
|
||
def test_admissibility_error_rejects_unknown_reason() -> None:
|
||
with pytest.raises(ValueError):
|
||
AdmissibilityError("bogus", "x")
|
||
|
||
|
||
def test_admissibility_error_carries_typed_reason_and_detail() -> None:
|
||
exc = AdmissibilityError("unit_mismatch", "sym_a != sym_b")
|
||
assert exc.reason == "unit_mismatch"
|
||
assert exc.detail == "sym_a != sym_b"
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# add / subtract / compare_additive / transfer (additive class)
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
@pytest.mark.parametrize("kind", ["add", "subtract", "compare_additive", "transfer"])
|
||
def test_additive_kinds_admit_matching_units(kind: str) -> None:
|
||
symbols = {
|
||
"a": _sym("a", unit="dollar"),
|
||
"b": _sym("b", unit="dollar"),
|
||
}
|
||
proof = check_admissibility(
|
||
_eq(kind=kind, deps=frozenset({"a", "b"})), symbols=symbols
|
||
)
|
||
assert isinstance(proof, UnitProof)
|
||
assert proof.lhs_unit == parse_unit("dollar")
|
||
assert proof.operation_kind == kind
|
||
|
||
|
||
@pytest.mark.parametrize("kind", ["add", "subtract", "compare_additive", "transfer"])
|
||
def test_additive_kinds_refuse_mismatched_units(kind: str) -> None:
|
||
symbols = {
|
||
"a": _sym("a", unit="dollar"),
|
||
"b": _sym("b", unit="foot"),
|
||
}
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(
|
||
_eq(kind=kind, deps=frozenset({"a", "b"})), symbols=symbols
|
||
)
|
||
assert ei.value.reason == "unit_mismatch"
|
||
|
||
|
||
def test_add_admits_single_dep() -> None:
|
||
# When the operand unit already matches the actor, a single-dep equation
|
||
# is fine — verifier just records the unit.
|
||
symbols = {"a": _sym("a", unit="dollar")}
|
||
proof = check_admissibility(
|
||
_eq(kind="add", deps=frozenset({"a"})), symbols=symbols
|
||
)
|
||
assert proof.lhs_unit == parse_unit("dollar")
|
||
|
||
|
||
def test_add_refuses_with_no_deps() -> None:
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(_eq(kind="add", deps=frozenset()), symbols={})
|
||
assert ei.value.reason == "operand_arity"
|
||
|
||
|
||
def test_additive_refuses_three_way_unit_disagreement() -> None:
|
||
symbols = {
|
||
"a": _sym("a", unit="dollar"),
|
||
"b": _sym("b", unit="dollar"),
|
||
"c": _sym("c", unit="foot"),
|
||
}
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(
|
||
_eq(kind="add", deps=frozenset({"a", "b", "c"})), symbols=symbols
|
||
)
|
||
assert ei.value.reason == "unit_mismatch"
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# multiply
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
def test_multiply_lhs_is_product_of_dep_units() -> None:
|
||
symbols = {
|
||
"a": _sym("a", unit="foot"),
|
||
"b": _sym("b", unit="foot"),
|
||
}
|
||
proof = check_admissibility(
|
||
_eq(kind="multiply", deps=frozenset({"a", "b"})), symbols=symbols
|
||
)
|
||
assert proof.lhs_unit.exponents == (2, 0, 0, 0, 0, 0)
|
||
|
||
|
||
def test_multiply_mixed_units_yields_composite() -> None:
|
||
symbols = {
|
||
"a": _sym("a", unit="foot"),
|
||
"b": _sym("b", unit="hour"),
|
||
}
|
||
proof = check_admissibility(
|
||
_eq(kind="multiply", deps=frozenset({"a", "b"})), symbols=symbols
|
||
)
|
||
# length * time
|
||
assert proof.lhs_unit.exponents == (1, 1, 0, 0, 0, 0)
|
||
|
||
|
||
def test_multiply_refuses_no_operands() -> None:
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(
|
||
_eq(kind="multiply", deps=frozenset()), symbols={}
|
||
)
|
||
assert ei.value.reason == "operand_arity"
|
||
|
||
|
||
def test_multiply_no_equality_requirement_between_operands() -> None:
|
||
# Brief: "multiply / divide: lhs unit = product / quotient of operand
|
||
# units; no equality requirement among operands."
|
||
symbols = {
|
||
"a": _sym("a", unit="foot"),
|
||
"b": _sym("b", unit="pound"),
|
||
}
|
||
proof = check_admissibility(
|
||
_eq(kind="multiply", deps=frozenset({"a", "b"})), symbols=symbols
|
||
)
|
||
# length * mass — no refusal, even though units differ.
|
||
assert proof.lhs_unit.exponents == (1, 0, 1, 0, 0, 0)
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# divide
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
def test_divide_lhs_is_quotient() -> None:
|
||
symbols = {
|
||
"q_actor_foot_t0": _sym("q_actor_foot_t0", unit="foot"),
|
||
"op_000__divisor": _sym("op_000__divisor", unit="hour"),
|
||
}
|
||
proof = check_admissibility(
|
||
_eq(
|
||
kind="divide",
|
||
deps=frozenset({"q_actor_foot_t0", "op_000__divisor"}),
|
||
),
|
||
symbols=symbols,
|
||
)
|
||
# foot / hour = speed
|
||
assert proof.lhs_unit.exponents == (1, -1, 0, 0, 0, 0)
|
||
|
||
|
||
def test_divide_refuses_when_no_divisor_named() -> None:
|
||
symbols = {
|
||
"a": _sym("a", unit="foot"),
|
||
"b": _sym("b", unit="hour"),
|
||
}
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(
|
||
_eq(kind="divide", deps=frozenset({"a", "b"})), symbols=symbols
|
||
)
|
||
assert ei.value.reason == "operand_arity"
|
||
|
||
|
||
def test_divide_refuses_three_deps() -> None:
|
||
symbols = {
|
||
"a": _sym("a", unit="foot"),
|
||
"b": _sym("b", unit="hour"),
|
||
"op_000__divisor": _sym("op_000__divisor", unit="hour"),
|
||
}
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(
|
||
_eq(
|
||
kind="divide",
|
||
deps=frozenset({"a", "b", "op_000__divisor"}),
|
||
),
|
||
symbols=symbols,
|
||
)
|
||
assert ei.value.reason == "operand_arity"
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# apply_rate
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
def test_apply_rate_admits_clean_form() -> None:
|
||
symbols = {
|
||
"q_actor_hour_t0": _sym("q_actor_hour_t0", unit="hour"),
|
||
"op_000__rate": _sym(
|
||
"op_000__rate", unit="dollar_per_hour", role="rate"
|
||
),
|
||
}
|
||
proof = check_admissibility(
|
||
_eq(
|
||
kind="apply_rate",
|
||
deps=frozenset({"q_actor_hour_t0", "op_000__rate"}),
|
||
),
|
||
symbols=symbols,
|
||
)
|
||
# money/time × time = money
|
||
assert proof.lhs_unit == parse_unit("dollar")
|
||
|
||
|
||
def test_apply_rate_refuses_when_duration_does_not_match_denominator() -> None:
|
||
symbols = {
|
||
"q_actor_foot_t0": _sym("q_actor_foot_t0", unit="foot"),
|
||
"op_000__rate": _sym(
|
||
"op_000__rate", unit="dollar_per_hour", role="rate"
|
||
),
|
||
}
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(
|
||
_eq(
|
||
kind="apply_rate",
|
||
deps=frozenset({"q_actor_foot_t0", "op_000__rate"}),
|
||
),
|
||
symbols=symbols,
|
||
)
|
||
assert ei.value.reason == "rate_form_invalid"
|
||
|
||
|
||
def test_apply_rate_refuses_missing_rate_role() -> None:
|
||
symbols = {
|
||
"a": _sym("a", unit="hour"),
|
||
"b": _sym("b", unit="dollar_per_hour"), # role='quantity', not 'rate'
|
||
}
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(
|
||
_eq(kind="apply_rate", deps=frozenset({"a", "b"})), symbols=symbols
|
||
)
|
||
assert ei.value.reason == "rate_form_invalid"
|
||
|
||
|
||
def test_apply_rate_refuses_wrong_arity() -> None:
|
||
symbols = {
|
||
"op_000__rate": _sym(
|
||
"op_000__rate", unit="dollar_per_hour", role="rate"
|
||
),
|
||
}
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(
|
||
_eq(kind="apply_rate", deps=frozenset({"op_000__rate"})),
|
||
symbols=symbols,
|
||
)
|
||
assert ei.value.reason == "operand_arity"
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# compare_multiplicative
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
def test_compare_multiplicative_lhs_is_dimensionless() -> None:
|
||
symbols = {
|
||
"a": _sym("a", unit="dollar"),
|
||
"b": _sym("b", unit="dollar"),
|
||
}
|
||
proof = check_admissibility(
|
||
_eq(kind="compare_multiplicative", deps=frozenset({"a", "b"})),
|
||
symbols=symbols,
|
||
)
|
||
assert proof.lhs_unit.exponents == (0, 0, 0, 0, 0, 0)
|
||
|
||
|
||
def test_compare_multiplicative_no_deps_is_dimensionless() -> None:
|
||
proof = check_admissibility(
|
||
_eq(kind="compare_multiplicative", deps=frozenset()),
|
||
symbols={},
|
||
)
|
||
assert proof.lhs_unit.exponents == (0, 0, 0, 0, 0, 0)
|
||
|
||
|
||
def test_compare_multiplicative_refuses_unit_mismatch() -> None:
|
||
symbols = {
|
||
"a": _sym("a", unit="dollar"),
|
||
"b": _sym("b", unit="foot"),
|
||
}
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(
|
||
_eq(kind="compare_multiplicative", deps=frozenset({"a", "b"})),
|
||
symbols=symbols,
|
||
)
|
||
assert ei.value.reason == "unit_mismatch"
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# Closed refusal-reason coverage
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
def test_refuses_unknown_symbol() -> None:
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(
|
||
_eq(kind="add", deps=frozenset({"missing"})), symbols={}
|
||
)
|
||
assert ei.value.reason == "unknown_symbol"
|
||
assert ei.value.detail == "missing"
|
||
|
||
|
||
def test_refuses_unit_unbound_when_dep_symbol_has_no_unit() -> None:
|
||
symbols = {"a": _sym("a", unit=None)}
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(
|
||
_eq(kind="add", deps=frozenset({"a"})), symbols=symbols
|
||
)
|
||
assert ei.value.reason == "unit_unbound"
|
||
|
||
|
||
def test_refuses_unknown_unit_when_dep_unit_outside_vocab() -> None:
|
||
symbols = {"a": _sym("a", unit="apples")}
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(
|
||
_eq(kind="add", deps=frozenset({"a"})), symbols=symbols
|
||
)
|
||
assert ei.value.reason == "unknown_unit"
|
||
|
||
|
||
def test_refuses_unknown_operation_kind() -> None:
|
||
eq = _eq(kind="bogus_kind", deps=frozenset())
|
||
with pytest.raises(AdmissibilityError) as ei:
|
||
check_admissibility(eq, symbols={})
|
||
assert ei.value.reason == "unknown_operation"
|
||
|
||
|
||
def test_check_admissibility_rejects_non_equation() -> None:
|
||
with pytest.raises(TypeError):
|
||
check_admissibility("not an equation", symbols={}) # type: ignore[arg-type]
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# UnitProof contract
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
def test_unit_proof_to_canonical_string_has_kind_and_arrow() -> None:
|
||
symbols = {"a": _sym("a", unit="dollar"), "b": _sym("b", unit="dollar")}
|
||
proof = check_admissibility(
|
||
_eq(kind="add", deps=frozenset({"a", "b"})), symbols=symbols
|
||
)
|
||
s = proof.to_canonical_string()
|
||
assert s.startswith("add:")
|
||
assert "->" in s
|
||
assert "money" in s
|
||
|
||
|
||
def test_unit_proof_is_frozen() -> None:
|
||
symbols = {"a": _sym("a", unit="dollar")}
|
||
proof = check_admissibility(
|
||
_eq(kind="add", deps=frozenset({"a"})), symbols=symbols
|
||
)
|
||
import dataclasses
|
||
|
||
with pytest.raises(dataclasses.FrozenInstanceError):
|
||
proof.lhs_unit = parse_unit("foot") # type: ignore[misc]
|
||
|
||
|
||
def test_unit_proof_operand_units_preserved() -> None:
|
||
symbols = {"a": _sym("a", unit="dollar"), "b": _sym("b", unit="dollar")}
|
||
proof = check_admissibility(
|
||
_eq(kind="add", deps=frozenset({"a", "b"})), symbols=symbols
|
||
)
|
||
assert len(proof.operand_units) == 2
|
||
assert all(u == parse_unit("dollar") for u in proof.operand_units)
|
||
|
||
|
||
def test_unit_proof_byte_equal_for_equivalent_inputs() -> None:
|
||
symbols = {"a": _sym("a", unit="dollar"), "b": _sym("b", unit="dollar")}
|
||
p1 = check_admissibility(
|
||
_eq(kind="add", deps=frozenset({"a", "b"})), symbols=symbols
|
||
)
|
||
p2 = check_admissibility(
|
||
_eq(kind="add", deps=frozenset({"a", "b"})), symbols=symbols
|
||
)
|
||
assert p1 == p2
|
||
assert p1.to_canonical_string() == p2.to_canonical_string()
|
||
|
||
|
||
def test_unit_proof_rejects_bad_construction() -> None:
|
||
with pytest.raises(ValueError):
|
||
UnitProof(operation_kind="", lhs_unit=parse_unit("foot"), operand_units=())
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# Determinism
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
def test_check_admissibility_deterministic_sorted_dep_iteration() -> None:
|
||
# Same dep set in different insertion order → same proof.
|
||
symbols = {"a": _sym("a", unit="dollar"), "b": _sym("b", unit="dollar")}
|
||
p1 = check_admissibility(
|
||
_eq(kind="add", deps=frozenset(["a", "b"])), symbols=symbols
|
||
)
|
||
p2 = check_admissibility(
|
||
_eq(kind="add", deps=frozenset(["b", "a"])), symbols=symbols
|
||
)
|
||
assert p1 == p2
|
||
|
||
|
||
def test_pack_composite_resolves_to_quotient_in_admissibility() -> None:
|
||
# composite unit resolves through parse_unit; admissibility uses it.
|
||
symbols = {
|
||
"q_actor_hour_t0": _sym("q_actor_hour_t0", unit="hour"),
|
||
"op_000__rate": _sym(
|
||
"op_000__rate", unit="cent_per_hour", role="rate"
|
||
),
|
||
}
|
||
proof = check_admissibility(
|
||
_eq(
|
||
kind="apply_rate",
|
||
deps=frozenset({"q_actor_hour_t0", "op_000__rate"}),
|
||
),
|
||
symbols=symbols,
|
||
)
|
||
# cent ∈ units.money → lhs = money
|
||
assert proof.lhs_unit == parse_unit("cent")
|