diff --git a/docs/analysis/adr-0184-s3-s5-candidate-source-boundary-2026-06-10.md b/docs/analysis/adr-0184-s3-s5-candidate-source-boundary-2026-06-10.md new file mode 100644 index 00000000..7b00f64e --- /dev/null +++ b/docs/analysis/adr-0184-s3-s5-candidate-source-boundary-2026-06-10.md @@ -0,0 +1,216 @@ +# ADR-0184 S3–S5 — the semantic-ledger candidate-source boundary + +**Date:** 2026-06-10 +**Scope:** design for the boundary stack between the S2 semantic-state ledger and the +existing derivation candidate/verification system, plus the first load-bearing slice +(implemented in the accompanying PR). +**Authority unchanged:** `generate/derivation/verify.py` and `generate/derivation/pool.py` +remain the sole commit authority. Nothing in this stack may commit an answer. + +## 0. Numbering reconciliation + +The mission brief numbers the boundary stack S3–S5. ADR-0184 §7 already assigns +S3 = semantic target wrapper, S4 = semantic candidate source to pool, S5 = transfer +events. To avoid corrupting the repo's durable numbering, **code and tests use the +ADR's numbering**; this note carries the mapping: + +| Brief | Content | ADR-0184 §7 | +|---|---|---| +| S3 | candidate-source adapter boundary (this PR) | **S4** (pool source swap) | +| S4 | replay/provenance equivalence boundary | new — proposed as **S4b** amendment | +| S5 | first narrow semantic-primary path | **S3** (semantic target) then **S5** (transfer) | + +The ADR's S3 (semantic target wrapper) is *not* skipped — it is re-sequenced as a +prerequisite of the first semantic-primary path, because question/target binding is +what makes a semantic-only world safe to expose. The pool source swap (ADR S4) has no +dependency on the target wrapper: it is a byte-equivalent re-plumbing, and ADR-0184 +§11.3 requires it for the ADR to move to Accepted. + +## 1. The current legacy candidate path + +The derivation lane (sealed; no serving import) resolves a problem like this: + +```text +composers (each emits ungated GroundedDerivation candidates) + accumulate.accumulation_candidates — 3 readings: strict, distractor-skip, anchor-skip + search.multiplicative_candidates — in-clause products + multistep.candidate_chains — target-guided bounded search + goal_residual.build_goal_residual — ADR-0207 R4 + | + v +pool.pooled_candidates — dedup by (answer, start token, step tokens), fixed order + | + v +pool.resolve_pooled — classify_derivation (complete/exempt/None) per candidate; + refuse on prior-state question, on zero verifying readings, + on disagreement, on exempt-only; commit sole complete answer +``` + +`compose_accumulation` separately gates the strict reading through +`select_self_verified` for the practice lane. The committed serving metric is owned by +the candidate-graph reader, a disjoint organ; nothing here touches serving. + +**The parser-patch accumulation problem.** Historically each new problem shape landed +as a local composer/matcher patch (the pattern ADR-0175 warns against). ADR-0184's bet +is that capability should instead land as new *transition kinds* over the semantic +ledger plus replay rules — one reading layer, not N parser patches. For that to ever +be true, ledger output needs a single, governed entry point into the candidate pool. +That entry point is what this stack defines. + +## 2. What S2 added (PR #684) + +- `state/model.py` — frozen `SemanticQuantity` / `StateKey` / `StateTransition` / + `SemanticLedger`, closed op set `{set, gain, loss}`, structural validation + (`SemanticStateError`), unit typed `str` (`""` = unitless) to match the extractor + and prevent a `None`-vs-`""` key-identity split. +- `state/ledger.py` — `build_accumulation_ledger`: the proven single-referent + gain/loss reading expressed as SET + GAIN/LOSS transitions over one entity/unit key. +- `state/replay.py` — `replay_accumulation_ledger`: the ONLY bridge from ledger to + `GroundedDerivation` (set→start, gain→add, loss→subtract, change operands inherit + the anchor unit). Refuses non-SET start, cross-key mutation, non-gain/loss ops. +- `accumulate.py` rerouted both reading builders through build+replay. +- Proven behavior-equivalent: byte-for-byte differential over 937 GSM8K problems, + 0 differences. + +After S2, the ledger exists and is exercised, but the *candidate enumeration* (which +worlds exist for a problem) still lives privately in `accumulate.py`, and `pool.py` +still imports `accumulation_candidates` — a composer-named surface, not a +semantic-state surface. There is no single place where ledger worlds become pool +candidates. + +## 3. What the semantic ledger can already express / cannot yet express safely + +**Can express (S2):** linear single-key histories — one entity/unit `StateKey`, a SET +anchor, ordered GAIN/LOSS deltas with licensed cues; build-time distractor-skip +(in-clause foreign-unit drop) and anchor-skip (leading non-anchorable block) readings. + +**Cannot yet express safely:** + +- multi-key worlds (transfer: `Sam gives Tom 3` needs two keys + a conservation law); +- question/target binding (no TARGET transition; the pool's prior-state guard is the + only temporal scope check, and it lives outside the ledger); +- comparison/difference relations; rate/container products (op set excludes + multiply/divide by design); +- temporal scoping (prior-state replay); +- competing worlds as first-class objects (the pool sees only flattened candidates); +- candidate provenance (a `GroundedDerivation` in the pool does not carry which + ledger produced it). + +Every one of these stays out of the candidate path until its own phase lands with +refusal-first tests. + +## 4. The correct adapter boundary (brief-S3 / ADR-S4 — this PR) + +One new module, `generate/derivation/state/source.py`, owns world enumeration and the +ledger→candidate conversion: + +```text +accumulation_world(text, drop_isolated_foreign) -> SemanticLedger | None +anchor_skip_world(text) -> SemanticLedger | None +accumulation_ledger_worlds(text) -> tuple[SemanticLedger, ...] +semantic_state_candidates(text) -> tuple[GroundedDerivation, ...] +``` + +`pool.py` swaps its accumulation source from `accumulate.accumulation_candidates` to +`state.source.semantic_state_candidates` (the ADR §7-S4 swap, verbatim). +`accumulate.py` keeps its public surfaces (`compose_accumulation`, +`accumulation_candidates`) as thin compatibility wrappers per ADR §10, so every +existing consumer (practice runners, tests) is untouched. + +Boundary properties (each pinned by a test): + +1. **Output type is inert.** The boundary emits only `GroundedDerivation` — a value + model with no commit semantics. Acceptance/refusal happens only in verify/pool. +2. **No authority import.** Nothing under `generate/derivation/state/` imports + `verify`, `pool`, or names `Resolution` / `select_self_verified` / + `classify_derivation` / `self_verifies` / `resolve_pooled`. A structural AST scan + (with a predicate self-test so it cannot be vacuous) enforces this. +3. **Fail-closed.** A world that cannot be built (`None`) or a ledger replay that + refuses contributes *nothing* — never a placeholder or synthesized candidate. +4. **Deterministic order** — strict, distractor-skip, anchor-skip — byte-identical to + the legacy enumeration including duplicates (pool dedup is unchanged). + +Why the pool swap is in the same PR as the adapter: an adapter with no consumer is a +dead organ (the router-organ-hygiene precedent, PR #646) and a "schema-defined proof +obligation" with no executing test. The swap is what makes the boundary load-bearing, +and ADR-0184 §11.3 makes it an explicit acceptance criterion. + +## 5. What verifier/pool need to see (and must keep seeing) + +Unchanged tuples of `GroundedDerivation` whose operand `source_token`s, cues, and +units come from the problem text. Three properties of the current pool behavior are +load-bearing and must not drift: + +- the **exempt rival readings** (distractor-skip, anchor-skip) must still be emitted — + ADR-0182's disagreement refusals depend on them; dropping one can unmask a unique + *wrong* commit; +- **candidate multiplicity and order** presented to pool dedup must be identical + (order determines which derivation object a commit reports); +- **unit inheritance** (change operands take the anchor unit) must be preserved, since + classification (complete/exempt) keys off used/unused units. + +## 6. Failure modes that would create wrong=0 violations + +| # | Failure mode | Defense | +|---|---|---| +| 1 | Lost exempt rival reading → disagreement disappears → unique wrong commit | byte-equivalence differential (937 problems); anchor-skip/distractor-skip presence tests | +| 2 | Reorder/dedup drift → different committed derivation object | identical enumeration order pinned by test; pool dedup untouched | +| 3 | Fabricated semantics — a candidate with no deriving ledger, or replay unfaithful to transitions | S2 replay is the only bridge; brief-S4 adds the faithfulness checker before any semantic-only world | +| 4 | Exception swallowing — structural invalidity (`SemanticStateError`) silently became "no candidate" | the boundary catches nothing; structural errors propagate loudly | +| 5 | Direct commit path from `state/` | structural no-authority-import scan (non-vacuous) | +| 6 | Unit-inheritance drift → classification flips | replay untouched; inheritance test exists in S2 suite | +| 7 | Future semantic world emits verifying-but-wrong candidates (soundness ≠ correctness) | out of scope for S3/S4 by construction (no new worlds); brief-S5 requires refusal-first acceptance + sealed gold tether before any new world enters the boundary | + +## 7. Tests proving semantic candidates cannot bypass verifier/pool + +- structural: no module under `state/` imports verify/pool or names any commit + surface (AST scan + predicate self-test on a known-violating snippet); +- behavioral: a boundary candidate that fails verification (ungrounded against the + actual problem text) never commits; rejection (no world) yields `()` and the pool + refuses or falls through to other composers exactly as before; +- the pool's own wrong=0 obligations (disagreement refusal, exempt-only never + commits, prior-state guard) re-run green against the swapped source; +- delegation equality: `accumulation_candidates(text) == semantic_state_candidates(text)` + across the canonical case battery; +- 937-problem byte-for-byte differential vs `main` (local harness, reported in PR). + +## 8. The S3–S5 sequence (brief numbering) + +**S3 (this PR, = ADR S4).** Adapter boundary + pool source swap, byte-equivalent. +No new capability; no serving, CLAIMS, metric, or lane-pin movement. + +**S4 (next, = proposed ADR S4b amendment).** Replay/provenance equivalence boundary — +the precondition for any semantic-only world: + +- an internal provenance record binding each emitted candidate to the ledger that + produced it (`(ledger, derivation)`), so a candidate cannot exist at the boundary + without a deriving ledger; +- a structural `replay_is_faithful(ledger, derivation)` checker — steps correspond 1:1 + to transitions (set→start, gain→add, loss→subtract), values/source tokens/cues + equal, unit-inheritance rule respected — wired into tests so an unfaithful replay + fails loudly; +- a committed equivalence harness (legacy-twin vs boundary) so the legacy enumeration + in `accumulate.py` can later be deleted without losing the equivalence proof. + +**S5 (after S4, = ADR S3 then ADR S5).** First narrow semantic-primary path — the +first reading that exists *only* as a ledger: + +1. land ADR S3 (semantic target wrapper: entity/unit/time-scope/relation binding, + conservative, preserving the prior-state refusals) — question binding is what makes + a multi-key world answerable; +2. then ADR S5 transfer events as the first semantic-primary world: two-key ledgers, + replay restricted to the question-bound key, refusing ambiguous source/target, no + initial state, or unbound questions; +3. entry only through `semantic_state_candidates`; commit only through the unchanged + verify/pool; refusal-first acceptance tests plus sealed-lane gold tether before any + committed metric may move (and then only via ratified PR). + +If at any point a semantic world needs the verifier to change to be admissible, that +is a stop signal, not an integration task. + +## 9. What is deliberately NOT in this PR + +No serving/runtime edits; no CLAIMS/metric/lane-pin movement; no new readings or +capability; no parser changes; no deletion of legacy surfaces (compat wrappers stay +per ADR §10 until brief-S4's committed equivalence harness exists); no provenance +record yet (S4); no transfer/target/temporal work (S5+). diff --git a/generate/derivation/__init__.py b/generate/derivation/__init__.py index b8f10522..f9f65aa3 100644 --- a/generate/derivation/__init__.py +++ b/generate/derivation/__init__.py @@ -29,6 +29,7 @@ from generate.derivation.search import ( multiplicative_candidates, search_multiplicative, ) +from generate.derivation.state.source import semantic_state_candidates from generate.derivation.target import Target, asks_prior_state, extract_target from generate.derivation.verify import ( Resolution, @@ -70,4 +71,5 @@ __all__ = [ "segment_clauses", "select_self_verified", "self_verifies", + "semantic_state_candidates", ] diff --git a/generate/derivation/accumulate.py b/generate/derivation/accumulate.py index 470e5f53..7fdd616d 100644 --- a/generate/derivation/accumulate.py +++ b/generate/derivation/accumulate.py @@ -8,116 +8,34 @@ across clauses **only** when (a) the later clause stays on the **same referent** and (b) it carries a **licensed change cue** whose polarity is unambiguous. Otherwise we refuse — the guard is generalised, never weakened. -Reading: - -1. **Anchor** — clause 1 must establish exactly one quantity ``(actor, N, unit)``. -2. **Change steps** — each later quantity-bearing clause applies ``+ M`` (gain) or - ``- M`` (loss) to the running total, where ``M`` is the clause's single grounded - quantity, taken **in the anchor's unit** (``9 more`` = 9 more *apples*; the unit - is inherited from the running total, which is what accumulation means). -3. **Gate** — the constructed chain runs through the unchanged self-verification - gate (grounding ∧ unit ∧ completeness ∧ uniqueness). The gate keeps - wrong=0; this only proposes a structurally-licensed candidate. - 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. +``generate.derivation.state``; S2 routed both accumulation readings through the +semantic ledger (SET/GAIN/LOSS over one entity/unit key) with replay back to +``GroundedDerivation``; §7 S4 moved world enumeration into the candidate-source +boundary, :mod:`generate.derivation.state.source`. This module remains the public +accumulation composer surface — :func:`compose_accumulation` (the gated strict +reading) and :func:`accumulation_candidates` (a thin compatibility wrapper over +:func:`generate.derivation.state.source.semantic_state_candidates`, per ADR-0184 +§10). Behavior is intentionally unchanged, and every candidate still faces the +unchanged verifier/pool. Sealed (no ``chat/`` import); deterministic; refuse-preferring. """ from __future__ import annotations -import re -from typing import Final - -from generate.derivation.clauses import segment_clauses -from generate.derivation.extract import extract_quantities 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.state.source import accumulation_world, semantic_state_candidates 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: - """Construct the single-referent accumulation chain (ungated). - - ``drop_isolated_foreign`` (ADR-0182): when a change clause carries more than - one quantity, drop those with a **non-empty unit foreign to the anchor's unit** - (a candidate distractor — ``studies for 3 hours`` among ``pencils``) and proceed - if exactly one same-unit/unitless change remains. With the flag off this is the - strict GB-3b.1 reading (a multi-quantity change clause refuses), so - :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. - """ - ledger = build_accumulation_ledger( - _quantity_clauses(problem_text), drop_isolated_foreign=drop_isolated_foreign - ) - if ledger is None: - return None - return replay_accumulation_ledger(ledger) - - -# ADR-0182 anchor-skip: sub-clause split on conjunctions. A single sentence can pack -# a state and its change ("Tom has 8 tickets and buys 4 more tickets") — the -# sentence-level segmenter (used everywhere; not changed) keeps them together. This -# finer split is *local* to the ungated candidate generator, so it cannot move -# GB-1/GB-2/serving/practice (which never call it). Lexeme-level (ADR-0165): it names -# coordinating conjunctions, it does not parse grammar. -_CONJUNCTION_SPLIT: Final[re.Pattern[str]] = re.compile(r",?\s+(?:and then|and|then)\s+") - - -def _sub_clauses(problem_text: str) -> list[str]: - """Sentence clauses, each further split on coordinating conjunctions.""" - parts: list[str] = [] - for clause in segment_clauses(problem_text): - parts.extend(p.strip() for p in _CONJUNCTION_SPLIT.split(clause) if p.strip()) - return parts - - -def _build_accumulation_anchor_skip(problem_text: str) -> GroundedDerivation | None: - """ADR-0182 — accumulation over sub-clauses, skipping a leading all-foreign block. - - Reads ``A train travels 60 mph for 2 hours. Tom has 8 tickets and buys 4 more - tickets.`` by skipping the (anchor-position) train block — its quantities cannot - seed an anchor (≠1 quantity) — and anchoring on the first single-quantity - sub-clause (``Tom has 8 tickets``), then chaining its conjunction-mate change - (``buys 4 more`` → +4). The skipped block's quantities go unused; the pool's - isolated-foreign exemption then classifies the reading ``exempt`` (commit- - ineligible), so it can only force a disagreement refusal, never commit. Ungated. - """ - sub_clauses = [(s, extract_quantities(s)) for s in _sub_clauses(problem_text)] - quantity_subs = [(s, qs) for s, qs in sub_clauses if qs] - if len(quantity_subs) < 2: - return None - - # Anchor = first single-quantity sub-clause; leading non-anchorable (≠1 - # 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 - selected = [sub for sub, _ in quantity_subs[anchor_idx:]] - ledger = build_accumulation_ledger(selected, drop_isolated_foreign=False) + """Construct the single-referent accumulation chain (ungated) — build the + semantic world at the S4 boundary, replay through the S2 bridge.""" + ledger = accumulation_world(problem_text, drop_isolated_foreign=drop_isolated_foreign) if ledger is None: return None return replay_accumulation_ledger(ledger) @@ -138,19 +56,9 @@ def compose_accumulation(problem_text: str) -> Resolution | None: def accumulation_candidates(problem_text: str) -> tuple[GroundedDerivation, ...]: """ADR-0182 — the ungated accumulation readings for cross-composer pooling. - Three readings: the strict GB-3b.1 reading, the distractor-skip reading (drops an - isolated-foreign quantity in a multi-quantity change clause — 0014), and the - anchor-skip reading (skips a leading all-foreign block + reads a conjunction-mate - intra-sentence change — 0016). Ungated: the pool classifies each (``complete`` - commits, ``exempt`` refuses-only) and the disagreement rule does the wrong=0 work. - Deterministic; de-dup is the pool's job. + Compatibility wrapper (ADR-0184 §10): the enumeration lives at the semantic + candidate-source boundary and is byte-identical to the pre-S4 behavior — three + readings (strict, distractor-skip, anchor-skip), ungated, deterministic order, + de-dup left to the pool. """ - candidates: list[GroundedDerivation] = [] - for drop in (False, True): - derivation = _build_accumulation(problem_text, drop_isolated_foreign=drop) - if derivation is not None: - candidates.append(derivation) - anchor_skip = _build_accumulation_anchor_skip(problem_text) - if anchor_skip is not None: - candidates.append(anchor_skip) - return tuple(candidates) + return semantic_state_candidates(problem_text) diff --git a/generate/derivation/pool.py b/generate/derivation/pool.py index 4424f09d..26250a2c 100644 --- a/generate/derivation/pool.py +++ b/generate/derivation/pool.py @@ -29,23 +29,24 @@ never invoked here). from __future__ import annotations -from generate.derivation.accumulate import accumulation_candidates from generate.derivation.goal_residual import build_goal_residual from generate.derivation.model import GroundedDerivation from generate.derivation.multistep import candidate_chains from generate.derivation.search import multiplicative_candidates +from generate.derivation.state.source import semantic_state_candidates from generate.derivation.target import asks_prior_state from generate.derivation.verify import Resolution, classify_derivation def pooled_candidates(problem_text: str) -> list[GroundedDerivation]: """Every composer's ungated candidate readings, de-duplicated. Deterministic - order (accumulation, then multiplicative, then chain).""" + order (semantic-state accumulation worlds via the ADR-0184 §7-S4 candidate-source + boundary, then multiplicative, then chain).""" seen: set[tuple[object, ...]] = set() pooled: list[GroundedDerivation] = [] _goal_residual = build_goal_residual(problem_text) for derivation in ( - *accumulation_candidates(problem_text), + *semantic_state_candidates(problem_text), *multiplicative_candidates(problem_text), *candidate_chains(problem_text), *((_goal_residual,) if _goal_residual is not None else ()), diff --git a/generate/derivation/r1_reconstruction.py b/generate/derivation/r1_reconstruction.py index e6aa042c..49d500b0 100644 --- a/generate/derivation/r1_reconstruction.py +++ b/generate/derivation/r1_reconstruction.py @@ -126,7 +126,7 @@ _GREATER_THAN_RE: Final[re.Pattern[str]] = re.compile( re.IGNORECASE, ) _DOUBLE_WHAT_RE: Final[re.Pattern[str]] = re.compile( - rf"(?P.+?)\b(?Ptwice|double)\s+what\s+(?P[^,.?]+)", + r"(?P.+?)\b(?Ptwice|double)\s+what\s+(?P[^,.?]+)", re.IGNORECASE, ) _THAT_MANY_RE: Final[re.Pattern[str]] = re.compile( diff --git a/generate/derivation/state/__init__.py b/generate/derivation/state/__init__.py index 3959d901..0dc2d3b0 100644 --- a/generate/derivation/state/__init__.py +++ b/generate/derivation/state/__init__.py @@ -4,10 +4,13 @@ This package is the sealed derivation-lane home for reusable semantic reading 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, +replay bridge back to ``GroundedDerivation``. §7 S4 adds the candidate-source +boundary (:mod:`generate.derivation.state.source`): the single surface through which +semantic worlds become pool candidates. 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. +replay through the existing verifier/pool — nothing in this package imports the +verifier or the pool, and nothing here can commit an answer. """ from __future__ import annotations @@ -33,6 +36,10 @@ from generate.derivation.state.model import ( StateTransition, ) from generate.derivation.state.replay import replay_accumulation_ledger +from generate.derivation.state.source import ( + accumulation_ledger_worlds, + semantic_state_candidates, +) __all__ = [ "GAIN_VERBS", @@ -44,10 +51,12 @@ __all__ = [ "SemanticStateError", "StateKey", "StateTransition", + "accumulation_ledger_worlds", "build_accumulation_ledger", "classify_change_polarity", "continues_anchor_referent", "leading_subject_token", "replay_accumulation_ledger", "select_change_cue", + "semantic_state_candidates", ] diff --git a/generate/derivation/state/source.py b/generate/derivation/state/source.py new file mode 100644 index 00000000..168fcb51 --- /dev/null +++ b/generate/derivation/state/source.py @@ -0,0 +1,139 @@ +"""ADR-0184 §7 S4 — the semantic candidate-source boundary. + +The single module through which semantic-ledger worlds become derivation candidates. +World enumeration (which readings exist for a problem) lives here; conversion to the +arithmetic proof object goes only through :func:`replay_accumulation_ledger` (S2's +sole bridge). The output is a tuple of inert ``GroundedDerivation`` values — this +boundary holds no commit authority: acceptance, classification, and refusal happen +only in the unchanged ``generate.derivation.verify`` / ``generate.derivation.pool``. + +Boundary laws (each pinned by tests in +``tests/test_adr_0184_s4_semantic_candidate_source.py``): + +* nothing under ``generate/derivation/state/`` imports verify/pool or names a commit + surface (structural scan); +* a world that cannot be built, or a replay that refuses, contributes nothing — + fail-closed, never a synthesized candidate; +* enumeration order is deterministic (strict, distractor-skip, anchor-skip) and + byte-identical to the pre-S4 ``accumulation_candidates`` enumeration, duplicates + included (de-dup remains the pool's job). + +Sealed (no ``chat/`` import); deterministic; refuse-preferring. +""" + +from __future__ import annotations + +import re +from typing import Final + +from generate.derivation.clauses import segment_clauses +from generate.derivation.extract import extract_quantities +from generate.derivation.model import GroundedDerivation +from generate.derivation.state.ledger import build_accumulation_ledger +from generate.derivation.state.model import SemanticLedger +from generate.derivation.state.replay import replay_accumulation_ledger + + +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 accumulation_world( + problem_text: str, *, drop_isolated_foreign: bool +) -> SemanticLedger | None: + """The single-referent accumulation reading of ``problem_text`` as a ledger. + + ``drop_isolated_foreign`` (ADR-0182): when a change clause carries more than + one quantity, drop those with a **non-empty unit foreign to the anchor's unit** + (a candidate distractor — ``studies for 3 hours`` among ``pencils``) and proceed + if exactly one same-unit/unitless change remains. With the flag off this is the + strict GB-3b.1 reading (a multi-quantity change clause refuses). The + distractor-skip reading is **never committed alone** — it only ever enters the + pool to force a disagreement refusal (see :mod:`generate.derivation.pool`). + """ + return build_accumulation_ledger( + _quantity_clauses(problem_text), drop_isolated_foreign=drop_isolated_foreign + ) + + +# ADR-0182 anchor-skip: sub-clause split on conjunctions. A single sentence can pack +# a state and its change ("Tom has 8 tickets and buys 4 more tickets") — the +# sentence-level segmenter (used everywhere; not changed) keeps them together. This +# finer split is *local* to the ungated candidate generator, so it cannot move +# GB-1/GB-2/serving/practice (which never call it). Lexeme-level (ADR-0165): it names +# coordinating conjunctions, it does not parse grammar. +_CONJUNCTION_SPLIT: Final[re.Pattern[str]] = re.compile(r",?\s+(?:and then|and|then)\s+") + + +def _sub_clauses(problem_text: str) -> list[str]: + """Sentence clauses, each further split on coordinating conjunctions.""" + parts: list[str] = [] + for clause in segment_clauses(problem_text): + parts.extend(p.strip() for p in _CONJUNCTION_SPLIT.split(clause) if p.strip()) + return parts + + +def anchor_skip_world(problem_text: str) -> SemanticLedger | None: + """ADR-0182 — the accumulation-over-sub-clauses reading, skipping a leading + all-foreign block, as a ledger. + + Reads ``A train travels 60 mph for 2 hours. Tom has 8 tickets and buys 4 more + tickets.`` by skipping the (anchor-position) train block — its quantities cannot + seed an anchor (≠1 quantity) — and anchoring on the first single-quantity + sub-clause (``Tom has 8 tickets``), then chaining its conjunction-mate change + (``buys 4 more`` → +4). The skipped block's quantities go unused; the pool's + isolated-foreign exemption then classifies the reading ``exempt`` (commit- + ineligible), so it can only force a disagreement refusal, never commit. + + ``drop_isolated_foreign`` stays off here — the anchor-skip reading drops a whole + leading block, not an in-clause foreign quantity. + """ + sub_clauses = [(s, extract_quantities(s)) for s in _sub_clauses(problem_text)] + quantity_subs = [(s, qs) for s, qs in sub_clauses if qs] + if len(quantity_subs) < 2: + return None + + # Anchor = first single-quantity sub-clause; leading non-anchorable (≠1 + # 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: same referent guard, same one-change-per-clause rule, same + # polarity gate. + anchor_idx = next((i for i, (_, qs) in enumerate(quantity_subs) if len(qs) == 1), None) + if anchor_idx is None: + return None + selected = [sub for sub, _ in quantity_subs[anchor_idx:]] + return build_accumulation_ledger(selected, drop_isolated_foreign=False) + + +def accumulation_ledger_worlds(problem_text: str) -> tuple[SemanticLedger, ...]: + """Every accumulation-backed semantic world for ``problem_text``, in the fixed + enumeration order: strict, distractor-skip, anchor-skip. A world that cannot be + built is simply absent — fail-closed.""" + worlds: list[SemanticLedger] = [] + for drop in (False, True): + world = accumulation_world(problem_text, drop_isolated_foreign=drop) + if world is not None: + worlds.append(world) + anchor_skip = anchor_skip_world(problem_text) + if anchor_skip is not None: + worlds.append(anchor_skip) + return tuple(worlds) + + +def semantic_state_candidates(problem_text: str) -> tuple[GroundedDerivation, ...]: + """ADR-0184 §7 S4 — the semantic candidate source for cross-composer pooling. + + Replays every semantic world through the S2 bridge and returns the resulting + ungated candidates. Byte-identical to the pre-S4 ``accumulation_candidates`` + enumeration: the pool classifies each (``complete`` commits, ``exempt`` + refuses-only) and the disagreement rule does the wrong=0 work. A refused replay + contributes nothing (fail-closed). Deterministic; de-dup is the pool's job. + """ + candidates: list[GroundedDerivation] = [] + for world in accumulation_ledger_worlds(problem_text): + derivation = replay_accumulation_ledger(world) + if derivation is not None: + candidates.append(derivation) + return tuple(candidates) diff --git a/tests/test_adr_0184_s4_semantic_candidate_source.py b/tests/test_adr_0184_s4_semantic_candidate_source.py new file mode 100644 index 00000000..12037d87 --- /dev/null +++ b/tests/test_adr_0184_s4_semantic_candidate_source.py @@ -0,0 +1,190 @@ +"""ADR-0184 §7 S4 — the semantic candidate-source boundary tests. + +The boundary (:mod:`generate.derivation.state.source`) is the single surface through +which semantic-ledger worlds become derivation candidates, and ``pool.py`` now sources +the accumulation readings through it. These tests pin the boundary laws +(CLAUDE.md "Schema-Defined Proof Obligations" — each must fail loudly if exactly its +guard is removed): + +* **byte-equivalence** — the boundary enumeration is identical to the legacy + ``accumulation_candidates`` enumeration (order, duplicates, refusals included); +* **authority unchanged** — a boundary candidate commits only through verify/pool: + acceptance requires classification, rejection fails closed (no world -> no + candidate -> refusal or fall-through, never a synthesized answer); +* **no direct commit path** — nothing under ``generate/derivation/state/`` imports + the verifier or the pool (structural scan, with a predicate self-test so the scan + cannot be vacuous); +* **legacy surfaces preserved** — ``compose_accumulation`` / ``accumulation_candidates`` + behave exactly as before the swap. +""" + +from __future__ import annotations + +import ast +from pathlib import Path + +from generate.derivation import pool +from generate.derivation.accumulate import accumulation_candidates, compose_accumulation +from generate.derivation.model import GroundedDerivation +from generate.derivation.pool import resolve_pooled +from generate.derivation.state.source import ( + accumulation_ledger_worlds, + semantic_state_candidates, +) +from generate.derivation.verify import Resolution, classify_derivation + +_CLEAN_GAIN = "Sam has 14 apples. He buys 9 more apples. How many apples does Sam have?" +_CLEAN_LOSS = "Anna has 25 stickers. She gives 10 away. How many stickers does Anna have?" +_NEW_ACTOR = "Sam has 14 apples. Tom buys 9 more apples. How many apples does Sam have?" +_DISTRACTOR_0014 = ( + "Kate has 20 pencils. She studies for 3 hours and then buys 5 more pencils. " + "How many pencils does Kate have?" +) +_ANCHOR_SKIP_0016 = ( + "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?" +) +_NO_QUANTITIES = "Sam walked to the library and read a book." + +_BATTERY = ( + _CLEAN_GAIN, + _CLEAN_LOSS, + _NEW_ACTOR, + _DISTRACTOR_0014, + _ANCHOR_SKIP_0016, + _NO_QUANTITIES, +) + + +class TestBoundaryEquivalence: + """The boundary is a re-plumbing, not a new reading.""" + + def test_legacy_wrapper_delegates_byte_identically(self) -> None: + for text in _BATTERY: + assert accumulation_candidates(text) == semantic_state_candidates(text) + + def test_enumeration_order_is_strict_then_skip_readings(self) -> None: + # The distractor problem yields the strict refusal (absent) then the + # distractor-skip reading; the anchor-skip problem yields the anchor-skip + # reading. Order changes would change which derivation object a commit + # reports — pinned here. + skip = semantic_state_candidates(_DISTRACTOR_0014) + assert [d.answer for d in skip] == [25.0] + anchor = semantic_state_candidates(_ANCHOR_SKIP_0016) + assert anchor and anchor[-1].answer == 12.0 + + def test_clean_problem_emits_duplicate_readings(self) -> None: + # On a clean problem the strict, distractor-skip, AND anchor-skip worlds all + # coincide; the legacy enumeration emitted all three (pool dedups). + # Collapsing them here would silently change pool input multiplicity. + candidates = semantic_state_candidates(_CLEAN_GAIN) + assert len(candidates) == 3 + assert len(set(candidates)) == 1 + + def test_every_world_starts_with_set(self) -> None: + # The builder can only emit replayable accumulation shapes — a non-SET-start + # world would be silently dropped by replay; prove the enumeration never + # produces one (fail-closed is for hand-built ledgers, not a leak here). + for text in _BATTERY: + for world in accumulation_ledger_worlds(text): + assert world.transitions[0].op == "set" + + def test_compose_accumulation_unchanged(self) -> None: + result = compose_accumulation(_CLEAN_GAIN) + assert result is not None and result.answer == 23.0 + assert compose_accumulation(_NEW_ACTOR) is None + + +class TestAuthorityUnchanged: + """Semantic candidates pass through verify/pool or do not pass at all.""" + + def test_boundary_emits_only_inert_value_objects(self) -> None: + for text in _BATTERY: + for candidate in semantic_state_candidates(text): + assert isinstance(candidate, GroundedDerivation) + assert not isinstance(candidate, Resolution) + + def test_pool_sources_the_boundary_function(self) -> None: + assert pool.semantic_state_candidates is semantic_state_candidates + + def test_acceptance_still_requires_pool_commit_rules(self) -> None: + resolution = resolve_pooled(_CLEAN_GAIN) + assert resolution is not None and resolution.answer == 23.0 + # the committed derivation is one the boundary emitted and verify classified + assert classify_derivation(resolution.derivation, _CLEAN_GAIN) == "complete" + + def test_unverifiable_semantic_candidate_never_commits(self) -> None: + # A boundary candidate evaluated against text it is not grounded in fails + # the verifier — the boundary cannot vouch for its own output. + candidate = semantic_state_candidates(_CLEAN_GAIN)[0] + foreign_text = "Lily has 3 books. She buys 2 more books." + assert classify_derivation(candidate, foreign_text) is None + + def test_rejection_fails_closed(self) -> None: + # No expressible world -> empty tuple -> downstream refusal/fall-through; + # never a placeholder candidate. + assert semantic_state_candidates(_NEW_ACTOR) == () + assert semantic_state_candidates(_NO_QUANTITIES) == () + + def test_distractor_disagreement_still_refuses(self) -> None: + assert resolve_pooled(_DISTRACTOR_0014) is None + + def test_anchor_skip_reading_is_still_exempt_only(self) -> None: + # ADR-0182's refusals depend on the exempt rival reading surviving the swap. + anchor = semantic_state_candidates(_ANCHOR_SKIP_0016)[-1] + assert classify_derivation(anchor, _ANCHOR_SKIP_0016) == "exempt" + + +_STATE_DIR = Path(__file__).resolve().parent.parent / "generate" / "derivation" / "state" +_FORBIDDEN_MODULES = ("generate.derivation.verify", "generate.derivation.pool") +_FORBIDDEN_NAMES = frozenset( + { + "Resolution", + "classify_derivation", + "resolve_pooled", + "select_self_verified", + "self_verifies", + } +) + + +def _authority_imports(source: str) -> list[str]: + """Names a module imports from the verifier/pool authority surfaces.""" + violations: list[str] = [] + tree = ast.parse(source) + for node in ast.walk(tree): + if isinstance(node, ast.Import): + violations.extend( + alias.name for alias in node.names if alias.name in _FORBIDDEN_MODULES + ) + elif isinstance(node, ast.ImportFrom): + module = node.module or "" + if module in _FORBIDDEN_MODULES: + violations.append(module) + else: + violations.extend( + alias.name for alias in node.names if alias.name in _FORBIDDEN_NAMES + ) + return violations + + +class TestNoDirectCommitPath: + """Structural: the semantic-state package cannot reach commit authority.""" + + def test_state_package_never_imports_verifier_or_pool(self) -> None: + scanned = 0 + for path in sorted(_STATE_DIR.glob("*.py")): + violations = _authority_imports(path.read_text()) + assert not violations, f"{path.name} imports commit authority: {violations}" + scanned += 1 + assert scanned >= 6, "state/ package moved? scan would be vacuous" + + def test_scan_predicate_flags_module_import(self) -> None: + # Predicate self-test (non-vacuity): both import forms must be caught. + assert _authority_imports("from generate.derivation.verify import Resolution") + assert _authority_imports("import generate.derivation.pool") + + def test_scan_predicate_flags_indirect_name_import(self) -> None: + # Re-exported authority names are caught even via a laundering module. + assert _authority_imports("from generate.derivation import resolve_pooled") + assert _authority_imports("from generate.derivation import Resolution")