feat(derivation): route accumulation through ADR-0184 S2 semantic ledger
ADR-0184 S1 (state/bind.py, state/change.py) landed the reusable referent and
change-cue helpers. S2 adds the first explicit state-transition substrate and
routes both accumulation readings through it:
- state/model.py frozen SET/GAIN/LOSS transition model over one entity/unit
StateKey, with structural validation (closed op set; unit is a
str with "" = unitless, mirroring the extractor's Quantity.unit
contract; entity optional, mirroring leading_subject_token).
- state/ledger.py build_accumulation_ledger() — the proven single-referent
gain/loss reading, expressed as a SemanticLedger.
- state/replay.py replay_accumulation_ledger() — the only bridge to
GroundedDerivation; refuses any non-accumulation ledger shape
(non-SET start, cross-key mutation).
accumulate.py's _build_accumulation / _build_accumulation_anchor_skip now build a
ledger and replay it instead of constructing the arithmetic chain inline; the
public compose_accumulation()/accumulation_candidates() surfaces are unchanged.
Behavior-equivalent: a byte-for-byte differential over 937 real GSM8K problems
(accumulation_candidates, compose_accumulation, pooled_candidates, resolve_pooled)
shows 0 differences vs main. Semantic worlds never commit directly — replay emits
GroundedDerivation and verify.py / pool.py remain the sole authority. Sealed: no
serving/runtime/chat import; no CLAIMS or eval-lane-SHA movement.
Refs ADR-0184 section 7 (S2).
This commit is contained in:
parent
7d6b7918aa
commit
9dcb00248c
6 changed files with 575 additions and 70 deletions
|
|
@ -19,9 +19,13 @@ Reading:
|
|||
gate (grounding ∧ unit ∧ completeness ∧ uniqueness). The gate keeps
|
||||
wrong=0; this only proposes a structurally-licensed candidate.
|
||||
|
||||
ADR-0184 S1 extracts the reusable referent and change-cue helpers into
|
||||
``generate.derivation.state``. This module remains the public accumulation
|
||||
composer surface; behavior is intentionally unchanged.
|
||||
ADR-0184 S1 extracted the reusable referent and change-cue helpers into
|
||||
``generate.derivation.state``. S2 routes both accumulation readings through a
|
||||
minimal semantic ledger (SET/GAIN/LOSS over one entity/unit key) and replays it to
|
||||
``GroundedDerivation`` — the transition construction now lives in ``state.ledger``
|
||||
and ``state.replay``, not as inline arithmetic here. This module remains the public
|
||||
accumulation composer surface; behavior is intentionally unchanged, and the replayed
|
||||
``GroundedDerivation`` still faces the unchanged verifier/pool.
|
||||
|
||||
Sealed (no ``chat/`` import); deterministic; refuse-preferring.
|
||||
"""
|
||||
|
|
@ -33,18 +37,18 @@ from typing import Final
|
|||
|
||||
from generate.derivation.clauses import segment_clauses
|
||||
from generate.derivation.extract import extract_quantities
|
||||
from generate.derivation.model import GroundedDerivation, Quantity, Step
|
||||
from generate.derivation.state.bind import (
|
||||
continues_anchor_referent,
|
||||
leading_subject_token,
|
||||
)
|
||||
from generate.derivation.state.change import (
|
||||
classify_change_polarity,
|
||||
select_change_cue,
|
||||
)
|
||||
from generate.derivation.model import GroundedDerivation
|
||||
from generate.derivation.state.ledger import build_accumulation_ledger
|
||||
from generate.derivation.state.replay import replay_accumulation_ledger
|
||||
from generate.derivation.verify import Resolution, select_self_verified
|
||||
|
||||
|
||||
def _quantity_clauses(problem_text: str) -> list[str]:
|
||||
"""Sentence-level clauses that carry extracted quantities (the ledger anchor +
|
||||
change-clause sequence)."""
|
||||
return [c for c in segment_clauses(problem_text) if extract_quantities(c)]
|
||||
|
||||
|
||||
def _build_accumulation(
|
||||
problem_text: str, *, drop_isolated_foreign: bool
|
||||
) -> GroundedDerivation | None:
|
||||
|
|
@ -58,42 +62,16 @@ def _build_accumulation(
|
|||
:func:`compose_accumulation` is byte-identical to its pre-ADR-0182 behavior.
|
||||
The distractor-skip reading is **never committed alone** — it only ever enters
|
||||
the pool to force a disagreement refusal (see :mod:`generate.derivation.pool`).
|
||||
|
||||
ADR-0184 S2: the SET/GAIN/LOSS reading is built as a semantic ledger and replayed
|
||||
to ``GroundedDerivation``; the construction is unchanged in behavior.
|
||||
"""
|
||||
clauses = segment_clauses(problem_text)
|
||||
quantity_clauses = [c for c in clauses if extract_quantities(c)]
|
||||
if len(quantity_clauses) < 2:
|
||||
ledger = build_accumulation_ledger(
|
||||
_quantity_clauses(problem_text), drop_isolated_foreign=drop_isolated_foreign
|
||||
)
|
||||
if ledger is None:
|
||||
return None
|
||||
|
||||
anchor_clause, *change_clauses = quantity_clauses
|
||||
anchor_quantities = extract_quantities(anchor_clause)
|
||||
if len(anchor_quantities) != 1:
|
||||
return None # the anchor must establish exactly one quantity (GB-3b.1 scope)
|
||||
start = anchor_quantities[0]
|
||||
anchor_subject = leading_subject_token(anchor_clause)
|
||||
|
||||
steps: list[Step] = []
|
||||
for clause in change_clauses:
|
||||
if not continues_anchor_referent(clause, anchor_subject):
|
||||
return None # new named actor -> referent hazard -> refuse
|
||||
change_quantities = list(extract_quantities(clause))
|
||||
if drop_isolated_foreign and len(change_quantities) > 1:
|
||||
change_quantities = [
|
||||
q for q in change_quantities if not (q.unit and q.unit != start.unit)
|
||||
]
|
||||
if len(change_quantities) != 1:
|
||||
return None # one change per clause (multi-change is GB-3b.2)
|
||||
polarity = classify_change_polarity(clause)
|
||||
if polarity is None:
|
||||
return None # no unambiguous licensed change cue -> refuse
|
||||
change = change_quantities[0]
|
||||
# The change is in the running total's dimension ("9 more" = 9 more apples).
|
||||
operand = Quantity(value=change.value, unit=start.unit, source_token=change.source_token)
|
||||
op = "add" if polarity > 0 else "subtract"
|
||||
steps.append(Step(op=op, operand=operand, cue=select_change_cue(clause, polarity)))
|
||||
|
||||
if not steps:
|
||||
return None
|
||||
return GroundedDerivation(start=start, steps=tuple(steps))
|
||||
return replay_accumulation_ledger(ledger)
|
||||
|
||||
|
||||
# ADR-0182 anchor-skip: sub-clause split on conjunctions. A single sentence can pack
|
||||
|
|
@ -130,31 +108,19 @@ def _build_accumulation_anchor_skip(problem_text: str) -> GroundedDerivation | N
|
|||
return None
|
||||
|
||||
# Anchor = first single-quantity sub-clause; leading non-anchorable (≠1
|
||||
# quantity) sub-clauses are skipped (candidate distractor blocks).
|
||||
# quantity) sub-clauses are skipped (candidate distractor blocks). The anchor and
|
||||
# its trailing change sub-clauses are then read by the same semantic ledger as the
|
||||
# sentence-level path (ADR-0184 S2): same referent guard, same one-change-per-clause
|
||||
# rule, same polarity gate. drop_isolated_foreign stays off here — the anchor-skip
|
||||
# reading drops a whole leading block, not an in-clause foreign quantity.
|
||||
anchor_idx = next((i for i, (_, qs) in enumerate(quantity_subs) if len(qs) == 1), None)
|
||||
if anchor_idx is None:
|
||||
return None
|
||||
anchor_sub, anchor_qs = quantity_subs[anchor_idx]
|
||||
start = anchor_qs[0]
|
||||
anchor_subject = leading_subject_token(anchor_sub)
|
||||
|
||||
steps: list[Step] = []
|
||||
for sub, qs in quantity_subs[anchor_idx + 1:]:
|
||||
if not continues_anchor_referent(sub, anchor_subject):
|
||||
return None # new named actor -> referent hazard -> refuse
|
||||
if len(qs) != 1:
|
||||
return None # one change per sub-clause (multi-change is GB-3b.2)
|
||||
polarity = classify_change_polarity(sub)
|
||||
if polarity is None:
|
||||
return None # no unambiguous licensed change cue -> refuse
|
||||
change = qs[0]
|
||||
operand = Quantity(value=change.value, unit=start.unit, source_token=change.source_token)
|
||||
op = "add" if polarity > 0 else "subtract"
|
||||
steps.append(Step(op=op, operand=operand, cue=select_change_cue(sub, polarity)))
|
||||
|
||||
if not steps:
|
||||
selected = [sub for sub, _ in quantity_subs[anchor_idx:]]
|
||||
ledger = build_accumulation_ledger(selected, drop_isolated_foreign=False)
|
||||
if ledger is None:
|
||||
return None
|
||||
return GroundedDerivation(start=start, steps=tuple(steps))
|
||||
return replay_accumulation_ledger(ledger)
|
||||
|
||||
|
||||
def compose_accumulation(problem_text: str) -> Resolution | None:
|
||||
|
|
|
|||
|
|
@ -1,9 +1,13 @@
|
|||
"""ADR-0184 — scoped semantic-state helper substrate.
|
||||
|
||||
This package is the sealed derivation-lane home for reusable semantic reading
|
||||
helpers. S1 intentionally exposes only behavior-equivalent helpers extracted
|
||||
from :mod:`generate.derivation.accumulate`; no serving path imports this package,
|
||||
and no new candidate behavior is introduced here.
|
||||
helpers. S1 exposes behavior-equivalent referent/change-cue helpers extracted from
|
||||
:mod:`generate.derivation.accumulate`. S2 adds a minimal semantic-state model
|
||||
(SET/GAIN/LOSS over one entity/unit key), an accumulation ledger builder, and a
|
||||
replay bridge back to ``GroundedDerivation``. No serving path imports this package,
|
||||
and no new candidate behavior is introduced here: the ledger only re-expresses the
|
||||
proven accumulation reading, and arithmetic commitment still happens only after
|
||||
replay through the existing verifier/pool.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
|
@ -19,13 +23,31 @@ from generate.derivation.state.change import (
|
|||
classify_change_polarity,
|
||||
select_change_cue,
|
||||
)
|
||||
from generate.derivation.state.ledger import build_accumulation_ledger
|
||||
from generate.derivation.state.model import (
|
||||
VALID_TRANSITION_OPS,
|
||||
SemanticLedger,
|
||||
SemanticQuantity,
|
||||
SemanticStateError,
|
||||
StateKey,
|
||||
StateTransition,
|
||||
)
|
||||
from generate.derivation.state.replay import replay_accumulation_ledger
|
||||
|
||||
__all__ = [
|
||||
"GAIN_VERBS",
|
||||
"LOSS_VERBS",
|
||||
"PRONOUNS",
|
||||
"VALID_TRANSITION_OPS",
|
||||
"SemanticLedger",
|
||||
"SemanticQuantity",
|
||||
"SemanticStateError",
|
||||
"StateKey",
|
||||
"StateTransition",
|
||||
"build_accumulation_ledger",
|
||||
"classify_change_polarity",
|
||||
"continues_anchor_referent",
|
||||
"leading_subject_token",
|
||||
"replay_accumulation_ledger",
|
||||
"select_change_cue",
|
||||
]
|
||||
|
|
|
|||
83
generate/derivation/state/ledger.py
Normal file
83
generate/derivation/state/ledger.py
Normal file
|
|
@ -0,0 +1,83 @@
|
|||
"""ADR-0184 S2 — semantic-ledger construction for accumulation.
|
||||
|
||||
This module owns only the semantic transition construction. It deliberately does
|
||||
not verify or commit answers; callers replay the ledger into ``GroundedDerivation``
|
||||
and then use the existing verifier/pool.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from generate.derivation.extract import extract_quantities
|
||||
from generate.derivation.state.bind import continues_anchor_referent, leading_subject_token
|
||||
from generate.derivation.state.change import classify_change_polarity, select_change_cue
|
||||
from generate.derivation.state.model import (
|
||||
SemanticLedger,
|
||||
SemanticQuantity,
|
||||
StateKey,
|
||||
StateTransition,
|
||||
)
|
||||
|
||||
|
||||
def build_accumulation_ledger(
|
||||
quantity_clauses: list[str], *, drop_isolated_foreign: bool
|
||||
) -> SemanticLedger | None:
|
||||
"""Build the single-referent gain/loss accumulation ledger.
|
||||
|
||||
``quantity_clauses`` must be the already-filtered sequence of clauses/sub-clauses
|
||||
that contain quantities. The behavior mirrors the pre-S2 accumulation composer:
|
||||
|
||||
* first clause must have exactly one quantity and becomes ``set``;
|
||||
* later clauses must continue the anchor referent;
|
||||
* each later clause must reduce to exactly one change quantity;
|
||||
* polarity must be an unambiguous licensed gain/loss cue;
|
||||
* change quantities inherit the anchor unit during replay.
|
||||
"""
|
||||
|
||||
if len(quantity_clauses) < 2:
|
||||
return None
|
||||
|
||||
anchor_clause, *change_clauses = quantity_clauses
|
||||
anchor_quantities = extract_quantities(anchor_clause)
|
||||
if len(anchor_quantities) != 1:
|
||||
return None
|
||||
|
||||
anchor_quantity = anchor_quantities[0]
|
||||
anchor_subject = leading_subject_token(anchor_clause)
|
||||
key = StateKey(entity=anchor_subject, unit=anchor_quantity.unit)
|
||||
transitions: list[StateTransition] = [
|
||||
StateTransition(
|
||||
key=key,
|
||||
op="set",
|
||||
quantity=SemanticQuantity.from_quantity(anchor_quantity, clause_index=0),
|
||||
cue="set",
|
||||
clause_index=0,
|
||||
)
|
||||
]
|
||||
|
||||
for idx, clause in enumerate(change_clauses, start=1):
|
||||
if not continues_anchor_referent(clause, anchor_subject):
|
||||
return None
|
||||
change_quantities = list(extract_quantities(clause))
|
||||
if drop_isolated_foreign and len(change_quantities) > 1:
|
||||
change_quantities = [
|
||||
q for q in change_quantities if not (q.unit and q.unit != anchor_quantity.unit)
|
||||
]
|
||||
if len(change_quantities) != 1:
|
||||
return None
|
||||
polarity = classify_change_polarity(clause)
|
||||
if polarity is None:
|
||||
return None
|
||||
change = change_quantities[0]
|
||||
transitions.append(
|
||||
StateTransition(
|
||||
key=key,
|
||||
op="gain" if polarity > 0 else "loss",
|
||||
quantity=SemanticQuantity.from_quantity(change, clause_index=idx),
|
||||
cue=select_change_cue(clause, polarity),
|
||||
clause_index=idx,
|
||||
)
|
||||
)
|
||||
|
||||
if len(transitions) <= 1:
|
||||
return None
|
||||
return SemanticLedger(transitions=tuple(transitions))
|
||||
152
generate/derivation/state/model.py
Normal file
152
generate/derivation/state/model.py
Normal file
|
|
@ -0,0 +1,152 @@
|
|||
"""ADR-0184 S2 — minimal semantic-state model.
|
||||
|
||||
The S2 model represents the first scoped state-transition substrate used by the
|
||||
accumulation composer. It is intentionally narrow: SET_STATE plus GAIN/LOSS over
|
||||
one entity/unit key. Arithmetic commitment still happens only after replay into
|
||||
``GroundedDerivation`` and the existing verifier/pool.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from dataclasses import dataclass
|
||||
from typing import Final
|
||||
|
||||
from generate.derivation.model import Quantity
|
||||
|
||||
VALID_TRANSITION_OPS: Final[frozenset[str]] = frozenset({"set", "gain", "loss"})
|
||||
|
||||
|
||||
class SemanticStateError(ValueError):
|
||||
"""Raised when a semantic-state object is structurally invalid."""
|
||||
|
||||
|
||||
def _require_optional_str(value: object, field_name: str) -> None:
|
||||
if value is not None and (not isinstance(value, str) or value == ""):
|
||||
raise SemanticStateError(f"{field_name} must be None or a non-empty str; got {value!r}")
|
||||
|
||||
|
||||
def _require_unit_str(value: object, field_name: str) -> None:
|
||||
# Units mirror the extractor's ``Quantity.unit`` contract exactly: a ``str``,
|
||||
# with ``""`` denoting unitless (the extractor never yields ``None``). Keeping
|
||||
# the substrate's unit type identical to the arithmetic layer avoids a latent
|
||||
# ``None``-vs-``""`` key-identity split in :func:`StateKey` equality.
|
||||
if not isinstance(value, str):
|
||||
raise SemanticStateError(f"{field_name} must be a str ('' = unitless); got {value!r}")
|
||||
|
||||
|
||||
def _require_non_empty_str(value: object, field_name: str) -> None:
|
||||
if not isinstance(value, str) or value == "":
|
||||
raise SemanticStateError(f"{field_name} must be a non-empty str; got {value!r}")
|
||||
|
||||
|
||||
def _require_non_negative_int(value: object, field_name: str) -> None:
|
||||
if not isinstance(value, int) or isinstance(value, bool) or value < 0:
|
||||
raise SemanticStateError(f"{field_name} must be an int >= 0; got {value!r}")
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class SemanticQuantity:
|
||||
"""A quantity mention attached to a semantic transition.
|
||||
|
||||
``unit`` is a ``str`` (``""`` = unitless), identical to the extractor's
|
||||
``Quantity.unit`` contract. Replay can override the operand unit with the ledger
|
||||
key's running unit, matching the existing accumulation behavior ("9 more"
|
||||
inherits the anchor unit).
|
||||
"""
|
||||
|
||||
value: float
|
||||
unit: str
|
||||
source_token: str
|
||||
clause_index: int
|
||||
|
||||
def __post_init__(self) -> None:
|
||||
if not isinstance(self.value, int | float) or isinstance(self.value, bool):
|
||||
raise SemanticStateError(
|
||||
f"SemanticQuantity.value must be numeric; got {type(self.value).__name__}"
|
||||
)
|
||||
_require_unit_str(self.unit, "SemanticQuantity.unit")
|
||||
_require_non_empty_str(self.source_token, "SemanticQuantity.source_token")
|
||||
_require_non_negative_int(self.clause_index, "SemanticQuantity.clause_index")
|
||||
|
||||
@classmethod
|
||||
def from_quantity(cls, quantity: Quantity, *, clause_index: int) -> "SemanticQuantity":
|
||||
"""Lift a derivation ``Quantity`` into a semantic quantity mention."""
|
||||
|
||||
return cls(
|
||||
value=float(quantity.value),
|
||||
unit=quantity.unit,
|
||||
source_token=quantity.source_token,
|
||||
clause_index=clause_index,
|
||||
)
|
||||
|
||||
def to_quantity(self, *, unit_override: str | None = None) -> Quantity:
|
||||
"""Project back to the arithmetic proof object's ``Quantity`` type."""
|
||||
|
||||
return Quantity(
|
||||
value=self.value,
|
||||
unit=self.unit if unit_override is None else unit_override,
|
||||
source_token=self.source_token,
|
||||
)
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class StateKey:
|
||||
"""Entity-owned quantity dimension.
|
||||
|
||||
``entity`` remains optional in S2 (``None`` when the loose leading subject is
|
||||
absent, mirroring :func:`generate.derivation.state.bind.leading_subject_token`);
|
||||
later ADR-0184 phases can tighten this once explicit entity binding exists.
|
||||
``unit`` is a ``str`` (``""`` = unitless), identical to the extractor contract.
|
||||
"""
|
||||
|
||||
entity: str | None
|
||||
unit: str
|
||||
|
||||
def __post_init__(self) -> None:
|
||||
_require_optional_str(self.entity, "StateKey.entity")
|
||||
_require_unit_str(self.unit, "StateKey.unit")
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class StateTransition:
|
||||
"""One semantic mutation over a ``StateKey``."""
|
||||
|
||||
key: StateKey
|
||||
op: str
|
||||
quantity: SemanticQuantity
|
||||
cue: str
|
||||
clause_index: int
|
||||
|
||||
def __post_init__(self) -> None:
|
||||
if not isinstance(self.key, StateKey):
|
||||
raise SemanticStateError(
|
||||
f"StateTransition.key must be StateKey; got {type(self.key).__name__}"
|
||||
)
|
||||
if self.op not in VALID_TRANSITION_OPS:
|
||||
raise SemanticStateError(
|
||||
f"StateTransition.op must be one of {sorted(VALID_TRANSITION_OPS)}; got {self.op!r}"
|
||||
)
|
||||
if not isinstance(self.quantity, SemanticQuantity):
|
||||
raise SemanticStateError(
|
||||
"StateTransition.quantity must be SemanticQuantity; "
|
||||
f"got {type(self.quantity).__name__}"
|
||||
)
|
||||
_require_non_empty_str(self.cue, "StateTransition.cue")
|
||||
_require_non_negative_int(self.clause_index, "StateTransition.clause_index")
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class SemanticLedger:
|
||||
"""Ordered semantic transitions for one candidate world."""
|
||||
|
||||
transitions: tuple[StateTransition, ...]
|
||||
|
||||
def __post_init__(self) -> None:
|
||||
if not isinstance(self.transitions, tuple):
|
||||
raise SemanticStateError("SemanticLedger.transitions must be a tuple")
|
||||
for idx, transition in enumerate(self.transitions):
|
||||
if not isinstance(transition, StateTransition):
|
||||
raise SemanticStateError(
|
||||
"SemanticLedger.transitions entries must be StateTransition; "
|
||||
f"got {type(transition).__name__} at index {idx}"
|
||||
)
|
||||
49
generate/derivation/state/replay.py
Normal file
49
generate/derivation/state/replay.py
Normal file
|
|
@ -0,0 +1,49 @@
|
|||
"""ADR-0184 S2 — replay semantic ledgers into arithmetic proof objects.
|
||||
|
||||
Replay is the only bridge from scoped semantic state to arithmetic candidates.
|
||||
It emits ``GroundedDerivation`` so the existing verifier/classifier/pool remain the
|
||||
authoritative commit path.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from generate.derivation.model import GroundedDerivation, Step
|
||||
from generate.derivation.state.model import SemanticLedger, StateTransition
|
||||
|
||||
|
||||
def replay_accumulation_ledger(ledger: SemanticLedger) -> GroundedDerivation | None:
|
||||
"""Replay a SET_STATE + GAIN/LOSS ledger to ``GroundedDerivation``.
|
||||
|
||||
Returns ``None`` when the ledger is not the narrow accumulation shape S2 owns.
|
||||
This keeps future transition kinds from accidentally being interpreted as a
|
||||
linear arithmetic chain before they receive their own proof model.
|
||||
"""
|
||||
|
||||
transitions = ledger.transitions
|
||||
if len(transitions) < 2:
|
||||
return None
|
||||
start_transition = transitions[0]
|
||||
if start_transition.op != "set":
|
||||
return None
|
||||
key = start_transition.key
|
||||
start = start_transition.quantity.to_quantity()
|
||||
steps: list[Step] = []
|
||||
|
||||
for transition in transitions[1:]:
|
||||
if not _same_key(transition, start_transition):
|
||||
return None
|
||||
if transition.op not in {"gain", "loss"}:
|
||||
return None
|
||||
op = "add" if transition.op == "gain" else "subtract"
|
||||
operand = transition.quantity.to_quantity(unit_override=key.unit)
|
||||
steps.append(Step(op=op, operand=operand, cue=transition.cue))
|
||||
|
||||
if not steps:
|
||||
return None
|
||||
return GroundedDerivation(start=start, steps=tuple(steps))
|
||||
|
||||
|
||||
def _same_key(a: StateTransition, b: StateTransition) -> bool:
|
||||
"""True iff two transitions mutate the same scoped state key."""
|
||||
|
||||
return a.key == b.key
|
||||
233
tests/test_adr_0184_s2_semantic_ledger.py
Normal file
233
tests/test_adr_0184_s2_semantic_ledger.py
Normal file
|
|
@ -0,0 +1,233 @@
|
|||
"""ADR-0184 S2 — semantic ledger model, builder, and replay tests.
|
||||
|
||||
The semantic ledger is the first explicit state-transition substrate. These tests
|
||||
pin the narrow S2 shape: SET_STATE plus same-key GAIN/LOSS transitions replay to the
|
||||
same ``GroundedDerivation`` shape the existing verifier/pool already accepts, and the
|
||||
model rejects structurally illegal states.
|
||||
|
||||
The wrong=0 obligations these tests must *non-vacuously* catch (CLAUDE.md
|
||||
"Schema-Defined Proof Obligations"): a non-SET start, a cross-key mutation, a new
|
||||
named actor, an absent/ambiguous change cue, and an out-of-vocabulary transition op.
|
||||
Each has a test that fails if exactly that guard is removed.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import pytest
|
||||
|
||||
from generate.derivation.accumulate import accumulation_candidates, compose_accumulation
|
||||
from generate.derivation.state.ledger import build_accumulation_ledger
|
||||
from generate.derivation.state.model import (
|
||||
VALID_TRANSITION_OPS,
|
||||
SemanticLedger,
|
||||
SemanticQuantity,
|
||||
SemanticStateError,
|
||||
StateKey,
|
||||
StateTransition,
|
||||
)
|
||||
from generate.derivation.state.replay import replay_accumulation_ledger
|
||||
|
||||
|
||||
class TestSemanticLedgerModel:
|
||||
def test_valid_transition_ops_are_the_closed_set(self) -> None:
|
||||
assert VALID_TRANSITION_OPS == frozenset({"set", "gain", "loss"})
|
||||
|
||||
def test_rejects_unknown_transition_op(self) -> None:
|
||||
with pytest.raises(SemanticStateError):
|
||||
StateTransition(
|
||||
key=StateKey(entity="Sam", unit="apples"),
|
||||
op="multiply",
|
||||
quantity=SemanticQuantity(3.0, "apples", "3", 0),
|
||||
cue="times",
|
||||
clause_index=0,
|
||||
)
|
||||
|
||||
def test_rejects_non_tuple_ledger(self) -> None:
|
||||
with pytest.raises(SemanticStateError):
|
||||
SemanticLedger(transitions=[]) # type: ignore[arg-type]
|
||||
|
||||
def test_rejects_non_transition_entry(self) -> None:
|
||||
with pytest.raises(SemanticStateError):
|
||||
SemanticLedger(transitions=("not a transition",)) # type: ignore[arg-type]
|
||||
|
||||
def test_unit_must_be_str_not_none(self) -> None:
|
||||
# ADR-0184 S2 tightening: units mirror the extractor's ``Quantity.unit``
|
||||
# contract exactly (a ``str``, ``""`` = unitless). ``None`` is rejected so a
|
||||
# ``None``-unit can never split key identity from a ``""``-unit transition.
|
||||
with pytest.raises(SemanticStateError):
|
||||
SemanticQuantity(3.0, None, "3", 0) # type: ignore[arg-type]
|
||||
with pytest.raises(SemanticStateError):
|
||||
StateKey(entity="Sam", unit=None) # type: ignore[arg-type]
|
||||
|
||||
def test_unitless_empty_string_is_accepted(self) -> None:
|
||||
quantity = SemanticQuantity(9.0, "", "9", 1)
|
||||
assert quantity.unit == ""
|
||||
assert StateKey(entity=None, unit="").unit == ""
|
||||
|
||||
def test_entity_may_be_none(self) -> None:
|
||||
assert StateKey(entity=None, unit="apples").entity is None
|
||||
|
||||
|
||||
class TestAccumulationLedgerBuilder:
|
||||
def test_builds_set_and_gain_transitions(self) -> None:
|
||||
ledger = build_accumulation_ledger(
|
||||
["Sam has 14 apples.", "He buys 9 more apples."],
|
||||
drop_isolated_foreign=False,
|
||||
)
|
||||
assert ledger is not None
|
||||
assert [t.op for t in ledger.transitions] == ["set", "gain"]
|
||||
assert ledger.transitions[0].key == StateKey(entity="Sam", unit="apples")
|
||||
assert ledger.transitions[1].cue == "more"
|
||||
|
||||
def test_loss_transition(self) -> None:
|
||||
ledger = build_accumulation_ledger(
|
||||
["Anna has 25 stickers.", "She gives 10 to her friend."],
|
||||
drop_isolated_foreign=False,
|
||||
)
|
||||
assert ledger is not None
|
||||
assert [t.op for t in ledger.transitions] == ["set", "loss"]
|
||||
assert ledger.transitions[1].cue == "gives"
|
||||
|
||||
def test_new_named_actor_refuses(self) -> None:
|
||||
assert (
|
||||
build_accumulation_ledger(
|
||||
["Sam has 14 apples.", "Tom buys 9 more apples."],
|
||||
drop_isolated_foreign=False,
|
||||
)
|
||||
is None
|
||||
)
|
||||
|
||||
def test_no_change_cue_refuses(self) -> None:
|
||||
assert (
|
||||
build_accumulation_ledger(
|
||||
["Lisa has 30 coins.", "She owns 15 coins."],
|
||||
drop_isolated_foreign=False,
|
||||
)
|
||||
is None
|
||||
)
|
||||
|
||||
def test_multi_quantity_anchor_refuses(self) -> None:
|
||||
assert (
|
||||
build_accumulation_ledger(
|
||||
["Sam has 14 apples and 3 pears.", "He buys 9 more apples."],
|
||||
drop_isolated_foreign=False,
|
||||
)
|
||||
is None
|
||||
)
|
||||
|
||||
def test_drop_isolated_foreign_preserves_candidate_only_when_enabled(self) -> None:
|
||||
clauses = [
|
||||
"Kate has 20 pencils.",
|
||||
"She studies for 3 hours and then buys 5 more pencils.",
|
||||
]
|
||||
assert build_accumulation_ledger(clauses, drop_isolated_foreign=False) is None
|
||||
ledger = build_accumulation_ledger(clauses, drop_isolated_foreign=True)
|
||||
assert ledger is not None
|
||||
assert [t.quantity.source_token for t in ledger.transitions] == ["20", "5"]
|
||||
|
||||
|
||||
class TestLedgerReplay:
|
||||
def test_replays_gain_to_grounded_derivation(self) -> None:
|
||||
ledger = build_accumulation_ledger(
|
||||
["Sam has 14 apples.", "He buys 9 more apples."],
|
||||
drop_isolated_foreign=False,
|
||||
)
|
||||
assert ledger is not None
|
||||
derivation = replay_accumulation_ledger(ledger)
|
||||
assert derivation is not None
|
||||
assert derivation.start.value == 14.0
|
||||
assert derivation.steps[0].op == "add"
|
||||
assert derivation.steps[0].operand.value == 9.0
|
||||
assert derivation.answer == 23.0
|
||||
|
||||
def test_replays_loss_to_grounded_derivation(self) -> None:
|
||||
ledger = build_accumulation_ledger(
|
||||
["Sam has 30 apples.", "He eats 8 apples."],
|
||||
drop_isolated_foreign=False,
|
||||
)
|
||||
assert ledger is not None
|
||||
derivation = replay_accumulation_ledger(ledger)
|
||||
assert derivation is not None
|
||||
assert derivation.steps[0].op == "subtract"
|
||||
assert derivation.answer == 22.0
|
||||
|
||||
def test_change_operand_inherits_anchor_unit(self) -> None:
|
||||
# "9 more" extracts unitless ("") but accumulates in the anchor's dimension.
|
||||
ledger = build_accumulation_ledger(
|
||||
["Sam has 14 apples.", "He buys 9 more."],
|
||||
drop_isolated_foreign=False,
|
||||
)
|
||||
assert ledger is not None
|
||||
derivation = replay_accumulation_ledger(ledger)
|
||||
assert derivation is not None
|
||||
assert derivation.start.unit == "apples"
|
||||
assert derivation.steps[0].operand.unit == "apples"
|
||||
|
||||
def test_replay_refuses_non_set_start(self) -> None:
|
||||
ledger = SemanticLedger(
|
||||
transitions=(
|
||||
StateTransition(
|
||||
key=StateKey(entity="Sam", unit="apples"),
|
||||
op="gain",
|
||||
quantity=SemanticQuantity(9.0, "apples", "9", 0),
|
||||
cue="more",
|
||||
clause_index=0,
|
||||
),
|
||||
)
|
||||
)
|
||||
assert replay_accumulation_ledger(ledger) is None
|
||||
|
||||
def test_replay_refuses_cross_key_mutation(self) -> None:
|
||||
ledger = SemanticLedger(
|
||||
transitions=(
|
||||
StateTransition(
|
||||
key=StateKey(entity="Sam", unit="apples"),
|
||||
op="set",
|
||||
quantity=SemanticQuantity(14.0, "apples", "14", 0),
|
||||
cue="set",
|
||||
clause_index=0,
|
||||
),
|
||||
StateTransition(
|
||||
key=StateKey(entity="Tom", unit="apples"),
|
||||
op="gain",
|
||||
quantity=SemanticQuantity(9.0, "apples", "9", 1),
|
||||
cue="more",
|
||||
clause_index=1,
|
||||
),
|
||||
)
|
||||
)
|
||||
assert replay_accumulation_ledger(ledger) is None
|
||||
|
||||
|
||||
class TestAccumulationComposerEquivalence:
|
||||
"""The composer surfaces still produce the proven accumulation answers; the
|
||||
ledger is purely an internal re-expression."""
|
||||
|
||||
def test_compose_accumulation_still_commits_clean_gain(self) -> None:
|
||||
result = compose_accumulation(
|
||||
"Sam has 14 apples. He buys 9 more. How many apples does Sam have now?"
|
||||
)
|
||||
assert result is not None
|
||||
assert result.answer == 23.0
|
||||
|
||||
def test_compose_accumulation_still_commits_clean_loss(self) -> None:
|
||||
result = compose_accumulation(
|
||||
"Anna has 25 stickers. She gives 10 away. How many stickers does Anna have?"
|
||||
)
|
||||
assert result is not None
|
||||
assert result.answer == 15.0
|
||||
|
||||
def test_new_actor_problem_still_refuses(self) -> None:
|
||||
assert (
|
||||
compose_accumulation(
|
||||
"Sam has 14 apples. Tom buys 9 more. How many apples does Sam have?"
|
||||
)
|
||||
is None
|
||||
)
|
||||
|
||||
def test_anchor_skip_still_emits_exempt_candidate_shape(self) -> None:
|
||||
text = (
|
||||
"A train travels at 60 miles per hour for 2 hours. Tom has 8 tickets and "
|
||||
"he buys 4 more tickets. How many tickets does Tom have?"
|
||||
)
|
||||
assert any(d.answer == 12.0 for d in accumulation_candidates(text))
|
||||
Loading…
Reference in a new issue