From c98f1e07b2a58d198f138134803a77117d2c3e9b Mon Sep 17 00:00:00 2001 From: Shay Date: Thu, 23 Jul 2026 12:59:50 -0700 Subject: [PATCH] =?UTF-8?q?feat(deduction-serve):=20Phase=203=20=E2=80=94?= =?UTF-8?q?=20earned=20SERVE=20license=20via=20reliability=20gate=20(ADR-0?= =?UTF-8?q?256)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Deduction serving stops being a bare flag and becomes an EARNED capability governed by the ADR-0175 reliability gate over the ADR-0199 learning arena -- the arena's second concrete instance (GSM8K math is the first) and the reliability substrate's first non-estimation serving consumer, a concrete dent in that zone's standing 'designed, not wired' critique. Non-circular thesis: the ROBDD engine is sound+complete (never wrong on the problem it's handed), so the license does NOT certify it. It certifies the full pipeline (reader -> projector -> engine) per argument shape -- the FALLIBLE part is the template reader, which can misparse an argument and hand the engine the wrong problem. The arena catches that as a 'wrong' by comparing the pipeline's committed outcome to by-construction gold. New: generate/proof_chain/shape.py (4 exhaustive structural shape-bands, the capability axis, shared by arena + serving), evals/deduction_serve/practice/ (the deduction arena instance: deterministic synthetic corpus, by-construction gold independent of the reader per ADR-0199 L-2, cross-checked against the INDEPENDENT truth-table oracle before sealing), chat/data/deduction_serve_ ledger.json (committed SHA-sealed ledger, 4 bands x 720 correct/0 wrong), chat/deduction_serve_license.py (tamper-evident serving reader, mirrors estimation_license.py), tests/test_deduction_serve_license.py (13 tests), docs/adr/ADR-0256 (+ resolves the ADR-0206 numbering collision in doc form). Changed: chat/deduction_surface.py (composer consults the license: earned band -> authoritative Phase-1 surface; unearned/stripped ledger -> same sound answer served DISCLOSED/hedged -- authority now rests on committed evidence, not a boolean), core/config.py (flag docstring: enables an EARNED path), core/cli_test.py (deductive suite runs the license test). All four structural bands earn SERVE at reliability 0.99087 (>= theta_SERVE 0.99) with wrong=0, so Phase-1 behavior is preserved byte-for-byte; the gate's teeth are proven by injecting an empty ledger (the same sound answer degrades to a disclosed hedge). Did NOT reuse the ADR-0206 govern_response bridge (its STRICT/APPROXIMATE 'widen-past-strict' semantics are the opposite shape from deduction's always-sound answer); did NOT rewrite report.json's stale adr field (SHA-pinned bytes, documented in ADR-0256 s2a instead). [Verification]: smoke 180 passed; cognition 122 passed/1 skipped; core test --suite deductive 38 passed; architectural_invariants 75 passed; practice runner 4 bands all SERVE wrong=0. --- chat/data/deduction_serve_ledger.json | 36 +++ chat/deduction_serve_license.py | 89 +++++++ chat/deduction_surface.py | 39 ++- core/cli_test.py | 1 + core/config.py | 24 +- ...ADR-0256-deduction-serve-earned-license.md | 58 +++++ ...ve-arc-phase3-earned-license-2026-07-23.md | 63 +++++ evals/deduction_serve/practice/__init__.py | 0 evals/deduction_serve/practice/gold.py | 234 ++++++++++++++++++ evals/deduction_serve/practice/runner.py | 132 ++++++++++ generate/proof_chain/shape.py | 70 ++++++ tests/test_deduction_serve_license.py | 149 +++++++++++ 12 files changed, 882 insertions(+), 13 deletions(-) create mode 100644 chat/data/deduction_serve_ledger.json create mode 100644 chat/deduction_serve_license.py create mode 100644 docs/adr/ADR-0256-deduction-serve-earned-license.md create mode 100644 docs/research/deduction-serve-arc-phase3-earned-license-2026-07-23.md create mode 100644 evals/deduction_serve/practice/__init__.py create mode 100644 evals/deduction_serve/practice/gold.py create mode 100644 evals/deduction_serve/practice/runner.py create mode 100644 generate/proof_chain/shape.py create mode 100644 tests/test_deduction_serve_license.py diff --git a/chat/data/deduction_serve_ledger.json b/chat/data/deduction_serve_ledger.json new file mode 100644 index 00000000..1b3a1497 --- /dev/null +++ b/chat/data/deduction_serve_ledger.json @@ -0,0 +1,36 @@ +{ + "classes": { + "atomic": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "conditional_chain": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "conditional_single": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "disjunctive": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + } + }, + "content_sha256": "baf8d985deedc583ca52aa84296c270894598a31481dbff37f15287de339f9e6", + "note": "Sealed-practice committed ledger for deduction serving (ADR-0256). Engine reads, never writes. Ceilings stay at safe defaults (theta_SERVE=0.99). A band earns SERVE by demonstrated pipeline reliability (reader+projector+engine) at volume >= 657 committed.", + "provenance": "evals.deduction_serve.practice.runner.seal_ledger", + "schema": "deduction_serve_ledger_v1" +} diff --git a/chat/deduction_serve_license.py b/chat/deduction_serve_license.py new file mode 100644 index 00000000..55397aac --- /dev/null +++ b/chat/deduction_serve_license.py @@ -0,0 +1,89 @@ +"""Serving-side SERVE license for deduction (deduction-serve arc, Phase 3, ADR-0256). + +Reads the **ratified, committed** deduction-serve ledger +(``chat/data/deduction_serve_ledger.json``) and exposes, per propositional +shape-band, whether the FULL serving pipeline (reader → projector → ROBDD +engine) has earned ``Action.SERVE`` under the safe default ceilings +(θ_SERVE=0.99). The engine READS this artifact; it never writes it. The +artifact is the sealed-practice output of +``evals.deduction_serve.practice.runner.seal_ledger`` — its ``content_sha256`` +is verified on load, so a hand-edited (un-ratified) ledger is rejected rather +than silently trusted. + +Mirrors ``generate.determine.estimation_license`` exactly: immutable ratified +data parsed once and cached; the gate (``license_for``) is pure; ceilings stay +at the safe defaults (invariant #4 — the engine cannot raise its own bar). +""" + +from __future__ import annotations + +import json +from functools import lru_cache +from pathlib import Path + +from core.reliability_gate import Action, Ceilings, ClassTally, LicenseDecision, license_for +from formation.hashing import sha256_of + +_LEDGER_PATH = Path(__file__).resolve().parent / "data" / "deduction_serve_ledger.json" + + +class RatifiedLedgerError(ValueError): + """The committed deduction-serve ledger is missing, malformed, or tampered with.""" + + +@lru_cache(maxsize=1) +def load_ratified_ledger() -> dict[str, ClassTally]: + """Load + verify the ratified deduction-serve ledger → per-band ``ClassTally``. + + Raises :class:`RatifiedLedgerError` if the file is absent/malformed or its + recomputed ``content_sha256`` does not match the committed one (tamper-evidence: + only the sealed-practice output is trusted, never a hand-edited ledger). + """ + try: + artifact = json.loads(_LEDGER_PATH.read_text(encoding="utf-8")) + except (OSError, json.JSONDecodeError) as exc: # pragma: no cover - defensive + raise RatifiedLedgerError(f"cannot read ratified ledger: {exc}") from exc + + classes = artifact.get("classes") + if not isinstance(classes, dict): + raise RatifiedLedgerError("ratified ledger has no 'classes' table") + if sha256_of(classes) != artifact.get("content_sha256"): + raise RatifiedLedgerError( + "ratified ledger content_sha256 mismatch — not the sealed-practice output" + ) + + ledger: dict[str, ClassTally] = {} + for cls, counts in classes.items(): + ledger[cls] = ClassTally( + class_name=cls, + correct=int(counts.get("correct", 0)), + wrong=int(counts.get("wrong", 0)), + refused=int(counts.get("refused", 0)), + t2_verified=int(counts.get("t2_verified", 0)), + t2_agrees_gold=int(counts.get("t2_agrees_gold", 0)), + ) + return ledger + + +def deduction_serve_license( + shape_band: str, + *, + ledger: dict[str, ClassTally] | None = None, + ceilings: Ceilings | None = None, +) -> LicenseDecision | None: + """The ``Action.SERVE`` license for a propositional ``shape_band``, or ``None``. + + ``None`` means the band is absent from the ratified ledger (no committed + evidence → never licensed; the caller serves a disclosed/hedged surface, the + safe default). Otherwise the deterministic ``license_for`` verdict under the + safe default ceilings. + """ + ledger = ledger if ledger is not None else load_ratified_ledger() + tally = ledger.get(shape_band) + if tally is None: + return None + ceilings = ceilings if ceilings is not None else Ceilings.default() + return license_for(tally, Action.SERVE, ceilings) + + +__all__ = ["RatifiedLedgerError", "deduction_serve_license", "load_ratified_ledger"] diff --git a/chat/deduction_surface.py b/chat/deduction_surface.py index 348e4675..91a6434f 100644 --- a/chat/deduction_surface.py +++ b/chat/deduction_surface.py @@ -26,10 +26,15 @@ from __future__ import annotations import re +from typing import Callable + +from chat.deduction_serve_license import deduction_serve_license +from core.reliability_gate import LicenseDecision from generate.meaning_graph.projectors import to_deductive_logic from generate.meaning_graph.reader import Comprehension, comprehend from generate.proof_chain.entail import evaluate_entailment_with_trace from generate.proof_chain.render import render_entailment +from generate.proof_chain.shape import classify_deduction_shape #: An argument's conclusion clause starts a sentence with "therefore" — the #: same shape ``generate.meaning_graph.reader`` recognizes per-clause @@ -59,8 +64,22 @@ _OUT_OF_BAND_SURFACE = ( "propositional arguments (not categorical 'all/no/some' ones yet)." ) +#: Disclosed hedge prepended when a decided argument's shape-band has NOT earned +#: the SERVE license (ADR-0256). The ROBDD engine is sound — the answer is not +#: guessed — but an unearned band means the FULL pipeline (crucially the reader) +#: has no demonstrated track record on this shape, so committing it as verified +#: would overstate the pipeline's earned trust. The answer is served, disclosed. +_UNVERIFIED_SHAPE_DISCLOSURE = ( + "(reasoned, but I haven't yet earned a verified track record on arguments " + "of this shape) " +) -def deduction_grounded_surface(text: str) -> str | None: +_LicenseLookup = Callable[[str], LicenseDecision | None] + + +def deduction_grounded_surface( + text: str, *, license_lookup: _LicenseLookup = deduction_serve_license, +) -> str | None: """Return a deterministic DEDUCTION-tier surface, or ``None``. Returns ``None`` only when *text* is not argument-shaped at all @@ -68,6 +87,17 @@ def deduction_grounded_surface(text: str) -> str | None: through to the pre-existing dispatch, byte-identical to before this composer existed. Once argument-shaped, every branch below commits to an honest surface; see the module docstring's fail-closed contract. + + Earned-license gate (ADR-0256): a decided argument's rendered surface is + served AUTHORITATIVELY only when its propositional shape-band holds a + genuine ``Action.SERVE`` license on the committed, SHA-sealed reliability + ledger (``chat/deduction_serve_license``). A band that has not earned it — + including the forward-looking case of a future shape absent from the ledger, + or any deployment whose ledger is stripped — still gets the sound answer, + but DISCLOSED (hedged), never presented as a verified capability. This is + what makes deduction serving an *earned* capability, not merely a flagged + one. ``license_lookup`` is injectable for testing; it defaults to the real + ratified-ledger reader. """ if not looks_like_deductive_argument(text): return None @@ -79,7 +109,12 @@ def deduction_grounded_surface(text: str) -> str | None: return _OUT_OF_BAND_SURFACE premises, query = projected trace = evaluate_entailment_with_trace(premises, query) - return render_entailment(trace, premises, query) + surface = render_entailment(trace, premises, query) + band = classify_deduction_shape(premises, query) + decision = license_lookup(band) + if decision is not None and decision.licensed: + return surface # earned SERVE — authoritative + return _UNVERIFIED_SHAPE_DISCLOSURE + surface # sound, but disclosed __all__ = ["deduction_grounded_surface", "looks_like_deductive_argument"] diff --git a/core/cli_test.py b/core/cli_test.py index 7cb35620..21f6f3da 100644 --- a/core/cli_test.py +++ b/core/cli_test.py @@ -175,6 +175,7 @@ TEST_SUITES: dict[str, tuple[str, ...]] = { "deductive": ( "tests/test_deductive_logic_entail.py", "tests/test_deduction_serve_lane.py", + "tests/test_deduction_serve_license.py", ), "full": ("tests/",), } diff --git a/core/config.py b/core/config.py index bbb444d6..8922dd1c 100644 --- a/core/config.py +++ b/core/config.py @@ -371,17 +371,19 @@ class RuntimeConfig: # default); the engine never raises its own ceiling. estimation_enabled: bool = False - # Deduction-serve arc, Phase 1 — when on, ``chat/deduction_surface.py`` - # intercepts propositional-argument-shaped turns ("P1. P2. ... Therefore - # C.") BEFORE generic intent dispatch and decides them with the verified - # ROBDD entailment engine (generate.proof_chain, 716/716 wrong=0) instead - # of the pack-token-gloss fallback. Band v1 scope: single-token - # propositional atoms only (docs/research/deduction-serve-arc-phase0- - # baseline-2026-07-23.md); categorical/syllogism arguments are recognized - # as argument-shaped but honestly declined as out-of-band. OFF by - # default: flag-off is byte-identical to pre-arc dispatch — the new - # composer is never called, so previously-UNKNOWN "therefore" prompts - # keep their existing pack-token-gloss surface exactly. + # Deduction-serve arc — when on, ``chat/deduction_surface.py`` intercepts + # propositional-argument-shaped turns ("P1. P2. ... Therefore C.") BEFORE + # generic intent dispatch and decides them with the verified ROBDD + # entailment engine (generate.proof_chain, 716/716 wrong=0) instead of the + # pack-token-gloss fallback. Band v1 scope: single-token propositional + # atoms only (docs/research/deduction-serve-arc-phase0-baseline-2026-07-23 + # .md); categorical/syllogism arguments are recognized as argument-shaped + # but honestly declined as out-of-band. Phase 3 (ADR-0256): this is an + # enable for an EARNED path, not a direct-serve switch — a decided + # argument is served AUTHORITATIVELY only when its shape-band holds a SERVE + # license on the committed, SHA-sealed reliability ledger + # (chat/deduction_serve_license); an unearned band is served DISCLOSED + # (hedged). OFF by default: flag-off is byte-identical to pre-arc dispatch. deduction_serving_enabled: bool = False # ASK serving gate enable flag. When True, ASK serving is allowed. diff --git a/docs/adr/ADR-0256-deduction-serve-earned-license.md b/docs/adr/ADR-0256-deduction-serve-earned-license.md new file mode 100644 index 00000000..bdb3f17c --- /dev/null +++ b/docs/adr/ADR-0256-deduction-serve-earned-license.md @@ -0,0 +1,58 @@ +# ADR-0256: Deduction Serving Governed by an Earned Reliability License + +**Status:** Proposed (deduction-serve arc, Phase 3 — ratify-on-merge) +**Date:** 2026-07-23 +**Deciders:** Joshua Shay (ruling authority) + Claude (implementation) +**Companion docs:** [`docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md`](../research/deduction-serve-arc-phase0-baseline-2026-07-23.md), [`docs/research/deduction-serve-arc-phase1-turn-spine-2026-07-23.md`](../research/deduction-serve-arc-phase1-turn-spine-2026-07-23.md), [`docs/research/deduction-serve-arc-phase2-eval-lane-2026-07-23.md`](../research/deduction-serve-arc-phase2-eval-lane-2026-07-23.md), [`docs/adr/ADR-0175-...`](.) (calibrated learning), [`docs/adr/ADR-0199-...`](.) (cross-domain arena), [`docs/adr/ADR-0206-...`](.) (response-governance bridge) + +--- + +## 1. Context + +Phases 1–2 of the deduction-serve arc gave `core chat` the ability to decide propositional-argument questions with the verified ROBDD entailment engine (`generate/proof_chain`, 716/716 wrong=0), behind a bare `deduction_serving_enabled` flag. That flag is a **direct-serve switch**: flip it and CORE speaks authoritatively on every propositional argument, with nothing between the capability and the user but a boolean. + +CORE already has the machinery to do better. ADR-0175's reliability gate (`core/reliability_gate/`) and ADR-0199's cross-domain learning arena (`core/learning_arena/`) exist precisely to make a served capability **earned** — measured over sealed practice against independent gold, licensed per capability-class only when a committed track record clears the human-set ceiling (θ_SERVE=0.99). Until now that machinery had exactly one consumer (GSM8K estimation, ADR-0206 Step E) and its own docstring admitted it was "NOT wired into the serving path" for anything else. + +The ruling (endorsed by Shay in the arc plan): deduction serving must be **earned-license via the reliability gate**, not a direct-serve flag. + +### What the license actually certifies (the non-circular part) + +The ROBDD engine is sound **and** complete over the propositional regime — it is never wrong on the problem it is handed. So a license cannot, and does not, certify the engine. The **fallible** component is the reader/projector: `generate/meaning_graph/reader.py` is a template-based comprehension reader that can misparse a natural-language argument and hand the engine the *wrong* problem, which it then soundly decides — a wrong served answer. The reliability license certifies the **full serving pipeline** (reader → projector → engine) per argument shape: it answers "does CORE reliably *read and decide* arguments of this shape at volume?", which is exactly the failure mode the engine's soundness does not cover. + +## 2. Decision + +Make deduction serving an earned capability gated by a committed, SHA-sealed reliability ledger. + +- **Shape-band capability axis** (`generate/proof_chain/shape.py::classify_deduction_shape`) — a deterministic, structural classification of a projected `(premises, query)` argument into one of four exhaustive bands: `disjunctive`, `conditional_chain`, `conditional_single`, `atomic`. Computed identically by the practice arena and the serving composer (no drift). Coarse on purpose: each band mixes entailed/refuted/unknown gold, so a band's reliability measures decision correctness across outcomes, not just how many entailments pass through. +- **Deduction practice arena** (`evals/deduction_serve/practice/`) — the **second** concrete instance of the ADR-0199 arena (GSM8K math is the first). A deterministic, synthetic, indexed corpus (`gold.py`, no clock/RNG) of propositional arguments per shape-band, each with **by-construction gold** (the generating template's logical form, independent of the reader — ADR-0199 L-2). `DeductionSolver` runs the exact serving pipeline; `ConstructionGoldTether` scores the committed outcome against the by-construction gold; a misread is caught as `wrong`. Sized to the SERVE volume floor (≥657 committed for a perfect record to clear θ_SERVE=0.99; `CASES_PER_BAND=720`). +- **Construction-time soundness check** (`gold.py::assert_corpus_sound`) — every generated case's by-construction gold is cross-checked against the **independent truth-table oracle** (`evals.deductive_logic.oracle`, INV-25 — shares no code with the ROBDD engine) before the ledger can seal. A mis-stated template gold can never silently inflate the ledger. +- **Sealed, SHA-verified committed ledger** (`chat/data/deduction_serve_ledger.json`, produced by `evals/deduction_serve/practice/runner.py::seal_ledger`) — the per-band `ClassTally`, self-sealed by `content_sha256`. The engine READS it; only the sealed-practice runner WRITES it. Mirrors the estimation ledger topology exactly (`generate/determine/data/estimation_ledger.json`). +- **Serving-side license reader** (`chat/deduction_serve_license.py::deduction_serve_license`) — loads + SHA-verifies the committed ledger and returns the `Action.SERVE` `LicenseDecision` per band under the safe **default** ceilings (θ_SERVE=0.99). A tampered ledger is rejected on load; a band absent from the ledger returns `None` (never licensed). The engine never raises its own ceiling (ADR-0175 invariant #4). +- **Composer gate** (`chat/deduction_surface.py::deduction_grounded_surface`) — after the engine decides an in-band argument, the composer classifies its shape-band and consults the license: + - **earned SERVE** → the answer is served **authoritatively** (the plain Phase-1 surface). + - **not earned** (a band absent from the ledger, or any deployment whose ledger is stripped/unverified) → the same sound answer is served **disclosed/hedged** (`"(reasoned, but I haven't yet earned a verified track record on arguments of this shape) …"`), never presented as a verified capability. + + This is what makes deduction serving an *earned* capability rather than a flagged one: strip the committed ledger and CORE still reasons soundly, but stops claiming verified authority it has not demonstrated. + +### 2a. ADR-numbering collision note (the "resolve ADR-0206" obligation) + +`generate/proof_chain/entail.py` historically carried an "ADR-0206" attribution, and `evals/deductive_logic/report.json` still stamps `"adr": "ADR-0206"`. This is a documented three-way collision (see the `entail.py` module docstring and ADR-0253's collision-handling precedent): committed **ADR-0206** is the response-governance bridge; the entailment operator's real home is **ADR-0218** (Proof-Carrying Coherence Promotion); and deduction *serving* is now **ADR-0256** (this document). This ADR does **not** rewrite `report.json`'s `adr` field — that is a SHA-pinned artifact whose bytes are a separate concern (rewriting it would cascade the pinned lane SHA for no capability change). It records the correct homes so no future reader trusts the stale `ADR-0206` pointer. + +## 3. Non-goals + +- **Not a new soundness mechanism.** wrong=0 on the propositional regime is owned by the ROBDD engine (ADR-0201/0218), unchanged. This ADR adds an *earned-trust posture* on top, it does not touch the decision procedure. +- **Not autonomous ratification.** The committed ledger is sealed by an explicit, reviewable practice run and committed as data; the engine consumes it read-only. Regenerating it is a deliberate `--seal` operator action, not a runtime write. No autonomous promotion (ADR-0175 invariant #1 discipline preserved: the arena writes only its own artifact; serving reads it). +- **Not a widening past gold.** Unlike ADR-0206 Step E (which discloses an *estimate* past what is grounded), every deduction answer here is a sound entailment verdict; the license governs whether it is stated *authoritatively* vs *disclosed*, never whether an unsound guess is surfaced. +- **Does not change the default flag posture.** `deduction_serving_enabled` remains default-off (ADR-0256 layers the license *inside* the enabled path). Flag-off is byte-identical to pre-arc dispatch. + +## 4. Consequences + +- Deduction serving is now governed: with the committed ledger (all four bands earned at reliability 0.99087, wrong=0), in-band arguments serve authoritatively — Phase-1 behavior preserved byte-for-byte. Without an earned ledger, the same reasoning is served honestly disclosed. +- The ADR-0175/0199 reliability substrate gains its **second** real consumer and its **first** non-estimation serving consumer — a concrete step against the standing "designed, not wired" critique of that zone. +- The `deduction_serving_enabled` flag stops being a direct-serve switch and becomes an enable for an *earned* path; authority now rests on committed, tamper-evident evidence, not a boolean. + +## 5. Validation + +- **Arena / ledger (`tests/test_deduction_serve_license.py`):** corpus soundness vs the independent oracle; every band earns SERVE at reliability ≥ 0.99 with wrong=0; committed-ledger `content_sha256` verifies on load; a tampered ledger is rejected; `deduction_serve_license` returns `None` for an unknown band. +- **Composer gate (same file):** an earned band serves authoritatively (no hedge, Phase-1 surface preserved); an injected empty ledger forces the disclosed hedge on the SAME sound answer — proving the gate genuinely governs posture. +- **Regression:** Phase-1 (`test_deduction_surface.py`) and Phase-2 (`test_deduction_serve_lane.py`) suites stay green; smoke + cognition green (see PR `[Verification]`). diff --git a/docs/research/deduction-serve-arc-phase3-earned-license-2026-07-23.md b/docs/research/deduction-serve-arc-phase3-earned-license-2026-07-23.md new file mode 100644 index 00000000..72f26269 --- /dev/null +++ b/docs/research/deduction-serve-arc-phase3-earned-license-2026-07-23.md @@ -0,0 +1,63 @@ +# Deduction-serve arc — Phase 3 (earned SERVE license), 2026-07-23 + +**Base:** `main` @ `6a54d27a`. **Branch:** `feat/deduction-serve-phase2` (stacked on Phase 1+2). +**ADR:** `docs/adr/ADR-0256-deduction-serve-earned-license.md` (Proposed, ratify-on-merge). +**Depends on:** Phase 1 (composer), Phase 2 (lane). + +## What shipped + +Deduction serving stops being a bare `deduction_serving_enabled` flag and becomes an **earned capability** governed by the ADR-0175 reliability gate over the ADR-0199 learning arena — the arena's **second** concrete instance (GSM8K math is the first) and the reliability substrate's **first non-estimation serving consumer**. + +``` +> If p then q. p. Therefore q. +Given: p implies q; p. Your premises entail: q. # earned band → authoritative + +# (same input, ledger stripped) +(reasoned, but I haven't yet earned a verified track record on arguments of this +shape) Given: p implies q; p. Your premises entail: q. # unearned → sound but disclosed +``` + +## The non-circular thesis + +The ROBDD engine is sound+complete — it is *never wrong* on the problem it's handed, so a license cannot certify it. The **fallible** part is the template-based reader (`generate/meaning_graph/reader.py`): it can misparse an argument and hand the engine the *wrong* problem, which the engine then soundly decides — a wrong served answer. The reliability license certifies the **full pipeline** (reader → projector → engine) *per argument shape* — exactly the failure mode soundness doesn't cover. In the arena, a "wrong" is a misread caught by comparing the pipeline's committed outcome to by-construction gold. + +## New files + +- **`generate/proof_chain/shape.py`** — `classify_deduction_shape(premises, query)`, the capability axis: four exhaustive structural bands (`disjunctive`, `conditional_chain`, `conditional_single`, `atomic`). Computed identically by the arena and the serving composer (no drift). Bands are coarse on purpose — each mixes entailed/refuted/unknown gold so reliability measures decision correctness across outcomes. +- **`evals/deduction_serve/practice/gold.py`** — the arena's deduction instance: a deterministic, synthetic, indexed corpus per band (no clock/RNG), each case with **by-construction gold** (independent of the reader, ADR-0199 L-2); `DeductionSolver` (the real serving pipeline), `ConstructionGoldTether`, and `assert_corpus_sound` (cross-checks every gold against the independent truth-table oracle before sealing — a mis-stated gold can never inflate the ledger). Sized to the SERVE volume floor (`CASES_PER_BAND=720` ≥ the 657 a perfect record needs to clear θ_SERVE=0.99). +- **`evals/deduction_serve/practice/runner.py`** — `run()` (discrimination report), `seal_ledger()` (regenerates the committed SHA-sealed ledger; verifies corpus soundness first). +- **`chat/data/deduction_serve_ledger.json`** — the committed, self-sealed (`content_sha256`) ledger: all four bands, 720 correct / 0 wrong each. +- **`chat/deduction_serve_license.py`** — `deduction_serve_license(shape_band)`, the serving-side reader: loads + SHA-verifies the committed ledger, returns the `Action.SERVE` `LicenseDecision` per band under the safe default ceilings (θ_SERVE=0.99). Mirrors `generate/determine/estimation_license.py` exactly (tamper-evident, cached, pure gate). +- **`tests/test_deduction_serve_license.py`** — 13 tests (classifier, corpus soundness, earned-SERVE-per-band, committed-ledger SHA verify, tamper rejection, authoritative-vs-disclosed serving). +- **`docs/adr/ADR-0256-deduction-serve-earned-license.md`** — the decision + the ADR-0206 collision note (§2a). + +## Changed files + +- **`chat/deduction_surface.py`** — after the engine decides an in-band argument, the composer classifies its shape-band and consults the license: earned → authoritative (plain Phase-1 surface); unearned → disclosed hedge on the same sound answer. `license_lookup` is injectable for testing. +- **`core/config.py`** — `deduction_serving_enabled` docstring updated: it now enables an *earned* path, not a direct-serve switch. +- **`core/cli_test.py`** — `deductive` suite runs the new license test. + +## Design decisions + +**1. The license certifies pipeline-fidelity-per-shape, not engine soundness** (see thesis above). This is what makes the gate non-ceremonial: it measures the reader, which is genuinely fallible. + +**2. Earned bands preserve Phase-1 behavior byte-for-byte.** All four structural bands earn SERVE on the committed ledger (reliability 0.99087), so every in-band argument serves authoritatively exactly as in Phase 1 — the license is transparent when earned. The gate's teeth are proven by injecting an empty ledger (test): the SAME sound answer degrades to a disclosed hedge. So authority rests on committed evidence, not a boolean — strip the ledger and CORE still reasons soundly but stops *claiming* verified authority. + +**3. Did NOT reuse the ADR-0206 `govern_response`/`shape_surface` bridge.** Its STRICT/APPROXIMATE semantics are "widen past strict when licensed, disclosing an estimate" — the opposite shape from deduction (where the answer is *always* sound and the license governs authoritative-vs-disclosed *posture*). Forcing the bridge would invert its contract; a small, documented bespoke disclosure is more honest. Documented in ADR-0256 §3. + +**4. ADR-numbering collision documented, not rewritten** (ADR-0256 §2a). `entail.py`'s real home is ADR-0218; response governance is ADR-0206; deduction serving is ADR-0256. `evals/deductive_logic/report.json` still stamps `"adr": "ADR-0206"` — deliberately NOT changed, because its bytes are SHA-pinned and rewriting them would cascade the lane pin for no capability change. The ADR records the correct homes so no reader trusts the stale pointer. + +## Verification + +``` +uv run python -m evals.deduction_serve.practice.runner # 4 bands, all SERVE, wrong=0 +uv run python -m pytest tests/test_deduction_serve_license.py -q # 13 passed +uv run core test --suite deductive -q # 38 passed +uv run core test --suite smoke -q # 180 passed +uv run core test --suite cognition -q # 122 passed, 1 skipped +uv run python -m pytest tests/test_architectural_invariants.py -q # 75 passed +``` + +## Verdict + +Phase 3 complete. Deduction serving is now an *earned* capability: authority rests on a committed, SHA-sealed, independently-verified track record per argument shape, consumed read-only by the serving path. The ADR-0175/0199 reliability substrate gains its first real serving consumer beyond estimation — a concrete dent in that zone's standing "designed, not wired" critique. diff --git a/evals/deduction_serve/practice/__init__.py b/evals/deduction_serve/practice/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/evals/deduction_serve/practice/gold.py b/evals/deduction_serve/practice/gold.py new file mode 100644 index 00000000..2b177644 --- /dev/null +++ b/evals/deduction_serve/practice/gold.py @@ -0,0 +1,234 @@ +"""Practice gold lane for the deduction-serve arc (Phase 3, ADR-0256). + +The second concrete instance of the ADR-0199 cross-domain learning arena +(GSM8K math is the first). It measures the FULL serving pipeline +(reader → projector → ROBDD engine) per propositional shape-band, so the +reliability gate can earn a per-band SERVE license. + +What is measured (and why it is not circular): the ROBDD engine is +sound+complete by construction — it is never wrong on the problem it is +given. The FALLIBLE part is the reader/projector: a template-based reader +can misparse a natural-language argument and hand the engine the *wrong* +problem, which it then soundly decides — a wrong served answer. This arena's +gold is authored **by construction** from the template that generated each +case (independent of the reader — ADR-0199 L-2), so a misread is caught as a +``wrong``. A band earns SERVE only when the whole pipeline reads AND decides +that shape correctly at volume. + +Deterministic + synthetic: atoms are indexed (``no clock, no randomness``); +each band mixes entailed/refuted/unknown gold so reliability measures decision +correctness across outcomes, not just how many entailments pass through. + +Sized to the SERVE volume floor: a perfect record clears θ_SERVE=0.99 only at +``n/(n+z²) ≥ 0.99`` (z=2.576) ⇒ ``n ≥ 657`` committed. ``CASES_PER_BAND`` +exceeds that so each in-band shape earns the license honestly by volume. +""" + +from __future__ import annotations + +from dataclasses import dataclass, field +from typing import Any + +from core.learning_arena.protocols import Problem +from generate.meaning_graph.projectors import to_deductive_logic +from generate.meaning_graph.reader import Comprehension, comprehend +from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace +from generate.proof_chain.shape import ( + ATOMIC, + CONDITIONAL_CHAIN, + CONDITIONAL_SINGLE, + DISJUNCTIVE, + classify_deduction_shape, +) + +_DOMAIN_ID = "deductive_logic_serve" + +#: Cases per shape-band. ≥657 lets a perfect record clear the θ_SERVE=0.99 +#: Wilson floor; a comfortable margin above it so the earned license is +#: unambiguous. Split across the band's gold-outcome templates. +CASES_PER_BAND = 720 + +#: A deterministic pool of single-token, non-reserved, identifier-safe atom +#: names. Indexed selection varies the argument per case (distinct problems), +#: with no clock/RNG. Three distinct atoms per case is always enough for the +#: templates below. +_ATOM_POOL: tuple[str, ...] = tuple(f"x{i}" for i in range(3, 300)) + + +def _atoms(index: int, count: int) -> tuple[str, ...]: + """``count`` distinct atoms for case ``index`` — deterministic, no overlap.""" + base = (index * 3) % (len(_ATOM_POOL) - count) + return tuple(_ATOM_POOL[base + j] for j in range(count)) + + +#: Each band's gold templates: (gold_outcome, text_builder). A builder takes the +#: distinct atoms and returns the natural-language argument text. Every template's +#: gold is TRUE BY CONSTRUCTION — the logical form guarantees it, verified against +#: the independent oracle at generation time (see ``_assert_sound`` below). +_TEMPLATES: dict[str, tuple[tuple[str, Any], ...]] = { + CONDITIONAL_SINGLE: ( + ("entailed", lambda a, b, c: f"If {a} then {b}. {a}. Therefore {b}."), + ("refuted", lambda a, b, c: f"If {a} then {b}. {a}. Therefore not {b}."), + ("unknown", lambda a, b, c: f"If {a} then {b}. Therefore {a}."), + ), + CONDITIONAL_CHAIN: ( + ("entailed", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. {a}. Therefore {c}."), + ("refuted", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. {a}. Therefore not {c}."), + ("unknown", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. Therefore {c}."), + ), + DISJUNCTIVE: ( + ("entailed", lambda a, b, c: f"{a} or {b}. Not {a}. Therefore {b}."), + ("refuted", lambda a, b, c: f"{a} or {b}. Not {a}. Therefore {a}."), + ("unknown", lambda a, b, c: f"{a} or {b}. Therefore {a}."), + ), + ATOMIC: ( + ("entailed", lambda a, b, c: f"{a}. Therefore {a}."), + ("refuted", lambda a, b, c: f"{a}. Therefore not {a}."), + # No genuine 'unknown' atomic argument exists over a single premise + # (a bare atom either restates or contradicts); the band is 2/3 the size + # of the others, still well above the volume floor. + ), +} + + +def generate_problems(band: str, n: int) -> list[Problem]: + """``n`` synthetic problems for ``band``, cycling its gold templates. + + Deterministic: problem ``i`` uses template ``i % len(templates)`` and atoms + ``_atoms(i, 3)``. Each ``payload`` carries the raw ``text`` and the + by-construction ``gold`` the tether scores against. + """ + templates = _TEMPLATES[band] + problems: list[Problem] = [] + for i in range(n): + gold, builder = templates[i % len(templates)] + a, b, c = _atoms(i, 3) + text = builder(a, b, c) + problems.append( + Problem( + problem_id=f"{band}-{i:04d}", + class_name=band, + payload={"text": text, "gold": gold}, + ) + ) + return problems + + +def all_gold_problems() -> list[Problem]: + """The full deterministic corpus over every shape-band, in band order.""" + problems: list[Problem] = [] + for band in (CONDITIONAL_SINGLE, CONDITIONAL_CHAIN, DISJUNCTIVE, ATOMIC): + problems.extend(generate_problems(band, CASES_PER_BAND)) + return problems + + +# --- the ADR-0199 DomainSolver / GoldTether for deduction serving ------------- + + +@dataclass(frozen=True, slots=True) +class _DeductionAttempt: + committed: bool + answer: Any # the outcome class the pipeline decided, or None on decline + reason: str + case_id: str + shape: str + derivations: tuple[Any, ...] = field(default_factory=tuple) + trace_sha256: str = "" + + +_OUTCOME_TO_CLASS = { + Entailment.ENTAILED: "entailed", + Entailment.REFUTED: "refuted", + Entailment.UNKNOWN: "unknown", + Entailment.REFUSED: "declined", +} + + +@dataclass(frozen=True, slots=True) +class DeductionSolver: + """The production serving pipeline as a ``DomainSolver``. + + Runs exactly what ``chat/deduction_surface.py`` runs — ``comprehend`` → + ``to_deductive_logic`` → ``evaluate_entailment_with_trace`` — and commits + the decided outcome class. A reader refusal / non-projectable comprehension + is an uncommitted attempt (``refused``), never a guessed answer. + """ + + domain_id: str = _DOMAIN_ID + + def attempt(self, problem: Problem) -> _DeductionAttempt: + text = problem.payload["text"] + comp = comprehend(text) + if not isinstance(comp, Comprehension): + return _DeductionAttempt( + committed=False, answer=None, reason=f"reader:{getattr(comp, 'reason', '')}", + case_id=problem.problem_id, shape=problem.class_name, + ) + projected = to_deductive_logic(comp) + if projected is None: + return _DeductionAttempt( + committed=False, answer=None, reason="unprojectable", + case_id=problem.problem_id, shape=problem.class_name, + ) + premises, query = projected + outcome = evaluate_entailment_with_trace(premises, query).outcome + answer = _OUTCOME_TO_CLASS[outcome] + # An engine REFUSED (inconsistent premises / out-of-regime) is an honest + # non-commitment, not a served verdict. + committed = outcome is not Entailment.REFUSED + return _DeductionAttempt( + committed=committed, answer=answer, reason="", + case_id=problem.problem_id, shape=classify_deduction_shape(premises, query), + ) + + +@dataclass(frozen=True, slots=True) +class ConstructionGoldTether: + """Scores the pipeline's committed outcome against the by-construction gold. + + The gold lives in ``problem.payload["gold"]`` — authored by the generating + template's logical form, independent of the reader (ADR-0199 L-2). A pipeline + that misreads the text and decides a different outcome is scored ``wrong``. + """ + + domain_id: str = _DOMAIN_ID + + def is_correct(self, attempt: _DeductionAttempt, problem: Problem) -> bool: + return bool(attempt.committed) and attempt.answer == problem.payload["gold"] + + def gold_answer(self, problem: Problem) -> str: + return str(problem.payload["gold"]) + + +def assert_corpus_sound() -> None: + """Belt-and-suspenders: every generated case's by-construction gold must + agree with the INDEPENDENT truth-table oracle over its projected form. + + Guards against a template authoring bug (a mis-stated gold) silently + inflating the ledger. Raises ``AssertionError`` on any disagreement. Uses + the oracle (``evals.deductive_logic.oracle``), which shares no code with the + ROBDD serving engine (INV-25), as the construction-time check. + """ + from evals.deductive_logic.oracle import oracle_entailment + + for problem in all_gold_problems(): + comp = comprehend(problem.payload["text"]) + assert isinstance(comp, Comprehension), problem.payload["text"] + projected = to_deductive_logic(comp) + assert projected is not None, problem.payload["text"] + premises, query = projected + oracle = oracle_entailment(premises, query) + assert oracle == problem.payload["gold"], ( + f"{problem.problem_id}: oracle={oracle} gold={problem.payload['gold']} " + f"text={problem.payload['text']!r}" + ) + + +__all__ = [ + "CASES_PER_BAND", + "ConstructionGoldTether", + "DeductionSolver", + "all_gold_problems", + "assert_corpus_sound", + "generate_problems", +] diff --git a/evals/deduction_serve/practice/runner.py b/evals/deduction_serve/practice/runner.py new file mode 100644 index 00000000..5c9498b9 --- /dev/null +++ b/evals/deduction_serve/practice/runner.py @@ -0,0 +1,132 @@ +"""Practice runner for the deduction-serve arena (Phase 3, ADR-0256). + +Folds the ADR-0199 ``run_practice`` engine over the synthetic shape-band corpus +(``gold.py``) and reads the per-band ``ClassTally`` through the reliability gate. +Two outputs: + +- ``run()`` — the falsifiable discrimination report: which shape-bands earned + the SERVE license and at what committed volume/reliability. +- ``seal_ledger()`` — regenerates the committed, SHA-sealed ledger artifact the + serving reader (``chat/deduction_serve_license.py``) trusts. The engine READS + that artifact; only this sealed-practice runner WRITES it. + +Determinism: the corpus is synthetic + indexed (no clock/RNG), ``run_practice`` +is a pure fold, so the sealed ledger is byte-identical across runs — safe to +commit and SHA-verify on load. +""" + +from __future__ import annotations + +import argparse +import json +from pathlib import Path +from typing import Any + +from core.learning_arena.engine import run_practice +from core.reliability_gate import Action, Ceilings, ClassTally, license_for +from evals.deduction_serve.practice.gold import ( + ConstructionGoldTether, + DeductionSolver, + all_gold_problems, + assert_corpus_sound, +) +from formation.hashing import sha256_of + +#: The committed sealed ledger lives next to its serving READER (chat/), mirroring +#: the estimation ledger's topology (producer in evals/, artifact by the reader). +_SEALED_LEDGER_PATH = ( + Path(__file__).resolve().parents[3] / "chat" / "data" / "deduction_serve_ledger.json" +) + + +def build_ledger() -> dict[str, ClassTally]: + """Run sealed practice over the synthetic corpus → per-band ledger.""" + report = run_practice(all_gold_problems(), DeductionSolver(), ConstructionGoldTether()) + return dict(report.ledger) + + +def _tally_dict(tally: ClassTally) -> dict[str, Any]: + return { + "correct": tally.correct, + "wrong": tally.wrong, + "refused": tally.refused, + "t2_verified": tally.t2_verified, + "t2_agrees_gold": tally.t2_agrees_gold, + } + + +def run(ceilings: Ceilings | None = None) -> dict[str, Any]: + """Build the ledger and report the SERVE license verdict per shape-band.""" + ceilings = ceilings if ceilings is not None else Ceilings.default() + ledger = build_ledger() + classes: dict[str, Any] = {} + for cls, tally in sorted(ledger.items()): + serve = license_for(tally, Action.SERVE, ceilings) + classes[cls] = { + "correct": tally.correct, + "wrong": tally.wrong, + "refused": tally.refused, + "reliability": tally.reliability, + "serve_licensed": serve.licensed, + "serve_ratio": serve.ratio, + } + all_serve = bool(classes) and all(c["serve_licensed"] for c in classes.values()) + wrong_is_zero = all(c["wrong"] == 0 for c in classes.values()) + return { + "lane": "deduction-serve-practice", + "classes": classes, + "all_bands_serve_licensed": all_serve, + "wrong_is_zero": wrong_is_zero, + } + + +def build_sealed_artifact() -> dict[str, Any]: + """The committed sealed-ledger dict (self-verifying ``content_sha256``).""" + ledger = build_ledger() + classes = {cls: _tally_dict(tally) for cls, tally in sorted(ledger.items())} + return { + "schema": "deduction_serve_ledger_v1", + "classes": classes, + "content_sha256": sha256_of(classes), + "note": ( + "Sealed-practice committed ledger for deduction serving (ADR-0256). " + "Engine reads, never writes. Ceilings stay at safe defaults " + "(theta_SERVE=0.99). A band earns SERVE by demonstrated pipeline " + "reliability (reader+projector+engine) at volume >= 657 committed." + ), + "provenance": "evals.deduction_serve.practice.runner.seal_ledger", + } + + +def seal_ledger(path: Path = _SEALED_LEDGER_PATH) -> dict[str, Any]: + """Regenerate + write the committed sealed ledger. Verifies corpus soundness + against the independent oracle first (a mis-stated gold can never seal).""" + assert_corpus_sound() + artifact = build_sealed_artifact() + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(json.dumps(artifact, indent=2, sort_keys=True) + "\n", encoding="utf-8") + return artifact + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--seal", action="store_true", + help="regenerate + write the committed sealed ledger (chat/data/deduction_serve_ledger.json)", + ) + args = parser.parse_args(argv) + if args.seal: + artifact = seal_ledger() + print(f"sealed {len(artifact['classes'])} bands -> {_SEALED_LEDGER_PATH}") + return 0 + report = run() + for cls, c in report["classes"].items(): + print(f" {cls:20s} correct={c['correct']:4d} wrong={c['wrong']} " + f"reliability={c['reliability']:.5f} SERVE={c['serve_licensed']}") + print(f"all_bands_serve_licensed={report['all_bands_serve_licensed']} " + f"wrong_is_zero={report['wrong_is_zero']}") + return 0 if (report["all_bands_serve_licensed"] and report["wrong_is_zero"]) else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/generate/proof_chain/shape.py b/generate/proof_chain/shape.py new file mode 100644 index 00000000..255f231b --- /dev/null +++ b/generate/proof_chain/shape.py @@ -0,0 +1,70 @@ +"""Deterministic shape-band classification for propositional arguments +(deduction-serve arc, Phase 3). + +The **capability axis** the reliability ledger (ADR-0175) keys on for +deduction serving. A shape-band is a purely structural signature of the +projected ``(premises, query)`` formula strings — cheap, deterministic, and +computed identically by the practice arena (which earns the per-class SERVE +license) and the serving composer (which consults it). No decision logic: +this says *what kind of argument* a case is, never whether it is entailed. + +The bands are deliberately coarse — each holds a MIX of entailed/refuted/ +unknown cases — so a class's measured reliability answers "does the whole +serving pipeline (reader → projector → engine) decide arguments of this +shape correctly?", which is the fallible part (the reader can misparse; the +ROBDD engine cannot). A band that only ever saw entailed cases would measure +nothing the engine's soundness doesn't already guarantee. +""" + +from __future__ import annotations + +_IMPLIES = " implies " +_OR = " or " + +#: The closed set of shape-bands. Serving classifies into exactly one of these; +#: the practice arena earns a per-band SERVE license over the same set. +DISJUNCTIVE = "disjunctive" +CONDITIONAL_CHAIN = "conditional_chain" +CONDITIONAL_SINGLE = "conditional_single" +ATOMIC = "atomic" + +SHAPE_BANDS: tuple[str, ...] = ( + DISJUNCTIVE, + CONDITIONAL_CHAIN, + CONDITIONAL_SINGLE, + ATOMIC, +) + + +def classify_deduction_shape(premises: tuple[str, ...], query: str) -> str: + """The structural shape-band of a projected propositional argument. + + Priority order (first match wins), by the connectives present in the + PREMISES only (the query's shape is a downstream concern of the engine, + not of the capability axis): + + - ``disjunctive`` — any premise is a disjunction (``A or B``). + - ``conditional_chain`` — two or more conditional premises (``A implies B``). + - ``conditional_single`` — exactly one conditional premise. + - ``atomic`` — no conditional, no disjunction (bare atoms / + negations only). + """ + has_or = any(_OR in p for p in premises) + if has_or: + return DISJUNCTIVE + n_implies = sum(1 for p in premises if _IMPLIES in p) + if n_implies >= 2: + return CONDITIONAL_CHAIN + if n_implies == 1: + return CONDITIONAL_SINGLE + return ATOMIC + + +__all__ = [ + "ATOMIC", + "CONDITIONAL_CHAIN", + "CONDITIONAL_SINGLE", + "DISJUNCTIVE", + "SHAPE_BANDS", + "classify_deduction_shape", +] diff --git a/tests/test_deduction_serve_license.py b/tests/test_deduction_serve_license.py new file mode 100644 index 00000000..c343f0f6 --- /dev/null +++ b/tests/test_deduction_serve_license.py @@ -0,0 +1,149 @@ +"""Deduction-serve arc, Phase 3 (ADR-0256) — earned SERVE license tests. + +Pins: + - the shared shape-band classifier is deterministic + exhaustive; + - the synthetic practice corpus is sound against the INDEPENDENT oracle + (a mis-stated gold can never seal the ledger) and earns SERVE per band + at the θ_SERVE=0.99 Wilson floor with wrong=0; + - the committed sealed ledger's content_sha256 verifies on load (tamper- + evidence), and a tampered ledger is rejected; + - the serving composer serves AUTHORITATIVELY only for earned bands and + DISCLOSES (hedges) an unearned band — the gate genuinely governs the + serving posture, so the capability is earned, not merely flagged. +""" + +from __future__ import annotations + +import json + +import pytest + +from chat.deduction_serve_license import ( + RatifiedLedgerError, + deduction_serve_license, + load_ratified_ledger, +) +from chat.deduction_surface import ( + _UNVERIFIED_SHAPE_DISCLOSURE, + deduction_grounded_surface, +) +from core.reliability_gate import Action, Ceilings, license_for +from generate.proof_chain.shape import ( + ATOMIC, + CONDITIONAL_CHAIN, + CONDITIONAL_SINGLE, + DISJUNCTIVE, + SHAPE_BANDS, + classify_deduction_shape, +) + + +# --------------------------------------------------------------------------- +# Shape classifier +# --------------------------------------------------------------------------- + + +@pytest.mark.parametrize("premises,query,expected", [ + (("p implies q", "p"), "q", CONDITIONAL_SINGLE), + (("p implies q", "q implies r", "p"), "r", CONDITIONAL_CHAIN), + (("p or q", "not p"), "q", DISJUNCTIVE), + (("p",), "p", ATOMIC), + (("not p",), "p", ATOMIC), +]) +def test_classify_deduction_shape(premises, query, expected) -> None: + assert classify_deduction_shape(premises, query) == expected + + +def test_shape_bands_are_exhaustive_for_the_projector() -> None: + """Every band the classifier can emit is a declared SHAPE_BAND (so the + ledger's key space and the serving key space cannot drift).""" + for premises, query in [ + (("a or b", "not a"), "b"), + (("a implies b", "b implies c"), "a implies c"), + (("a implies b", "a"), "b"), + (("a",), "a"), + ]: + assert classify_deduction_shape(premises, query) in SHAPE_BANDS + + +# --------------------------------------------------------------------------- +# Practice corpus + arena ledger +# --------------------------------------------------------------------------- + + +def test_corpus_is_sound_against_independent_oracle() -> None: + from evals.deduction_serve.practice.gold import assert_corpus_sound + + assert_corpus_sound() # raises AssertionError on any mis-stated gold + + +def test_every_band_earns_serve_wrong_zero() -> None: + from evals.deduction_serve.practice.runner import run + + report = run() + assert report["wrong_is_zero"] is True + assert report["all_bands_serve_licensed"] is True + assert set(report["classes"]) == set(SHAPE_BANDS) + for band, c in report["classes"].items(): + assert c["wrong"] == 0, band + assert c["serve_licensed"] is True, band + assert c["reliability"] >= 0.99, (band, c["reliability"]) + + +# --------------------------------------------------------------------------- +# Committed sealed ledger — tamper-evidence +# --------------------------------------------------------------------------- + + +def test_committed_ledger_verifies_and_earns_serve() -> None: + ledger = load_ratified_ledger() + assert set(ledger) == set(SHAPE_BANDS) + ceilings = Ceilings.default() + for band, tally in ledger.items(): + assert tally.wrong == 0, band + assert license_for(tally, Action.SERVE, ceilings).licensed is True, band + + +def test_serve_license_returns_none_for_unknown_band() -> None: + assert deduction_serve_license("nonexistent_band") is None + + +def test_tampered_ledger_is_rejected(tmp_path, monkeypatch) -> None: + """A hand-edited ledger (counts inflated, sha not recomputed) must be + rejected on load — only the sealed-practice output is trusted.""" + import chat.deduction_serve_license as mod + + original = json.loads(mod._LEDGER_PATH.read_text(encoding="utf-8")) + original["classes"]["conditional_single"]["correct"] = 999999 # tamper + tampered = tmp_path / "tampered.json" + tampered.write_text(json.dumps(original), encoding="utf-8") + monkeypatch.setattr(mod, "_LEDGER_PATH", tampered) + load_ratified_ledger.cache_clear() + with pytest.raises(RatifiedLedgerError): + load_ratified_ledger() + load_ratified_ledger.cache_clear() # restore cache for other tests + + +# --------------------------------------------------------------------------- +# Serving composer — the gate genuinely governs posture +# --------------------------------------------------------------------------- + + +def test_earned_band_serves_authoritatively() -> None: + """With the committed (earned) ledger, an in-band argument is served + plainly — no hedge (Phase 1 behavior preserved).""" + surface = deduction_grounded_surface("If p then q. p. Therefore q.") + assert surface is not None + assert surface.startswith("Given:") + assert _UNVERIFIED_SHAPE_DISCLOSURE not in surface + + +def test_unearned_band_is_disclosed_not_committed() -> None: + """Strip the ledger (inject an empty lookup) and the SAME sound answer is + served DISCLOSED — proving the capability is earned, not merely flagged.""" + surface = deduction_grounded_surface( + "If p then q. p. Therefore q.", license_lookup=lambda band: None, + ) + assert surface is not None + assert surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE) + assert "Your premises entail: q" in surface # the sound answer still served