"""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, to_syllogism
from generate.meaning_graph.reader import Comprehension, comprehend
from generate.proof_chain.categorical import CategoricalError, decide_syllogism
from generate.proof_chain.english import EnglishArgument, read_english_argument
from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace
from generate.proof_chain.member import MemberArgument, read_member_argument
from generate.proof_chain.shape import (
    ATOMIC,
    CATEGORICAL,
    CONDITIONAL_CHAIN,
    CONDITIONAL_SINGLE,
    DISJUNCTIVE,
    EN_ATOMIC,
    EN_CONDITIONAL_CHAIN,
    EN_CONDITIONAL_SINGLE,
    EN_DISJUNCTIVE,
    EN_MEMBER_ATOMIC,
    EN_MEMBER_CHAIN,
    EN_MEMBER_NEGATIVE,
    EN_MEMBER_SINGLE,
    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.
    ),
    # Categorical (syllogism). Terms are synthetic PLURAL class nouns (``x3s`` →
    # the reader singularizes to ``x3``); ``a, b, c`` are the three distinct
    # middle/subject/predicate classes. Gold is the unconditional validity (modern
    # reading) of the standard form — cross-checked against the INDEPENDENT
    # syllogism oracle in ``assert_corpus_sound``.
    CATEGORICAL: (
        # Barbara (AAA) — valid.
        ("valid", lambda a, b, c: f"All {a}s are {b}s. All {c}s are {a}s. Therefore all {c}s are {b}s."),
        # Celarent (EAE) — valid.
        ("valid", lambda a, b, c: f"No {a}s are {b}s. All {c}s are {a}s. Therefore no {c}s are {b}s."),
        # Darii (AII) — valid.
        ("valid", lambda a, b, c: f"All {a}s are {b}s. Some {c}s are {a}s. Therefore some {c}s are {b}s."),
        # Ferio (EIO) — valid.
        ("valid", lambda a, b, c: f"No {a}s are {b}s. Some {c}s are {a}s. Therefore some {c}s are not {b}s."),
        # Undistributed middle (AAA-2) — INVALID.
        ("invalid", lambda a, b, c: f"All {b}s are {a}s. All {c}s are {a}s. Therefore all {c}s are {b}s."),
        # Existential-import overreach — INVALID in the modern reading.
        ("invalid", lambda a, b, c: f"All {a}s are {b}s. All {a}s are {c}s. Therefore some {c}s are {b}s."),
    ),
}


# --- Band v2-EN (ADR-0257): English-clause synthetic corpus -------------------
#
# Deterministic copular-clause lexicon: 20 subjects × 12 states = 240 distinct
# clauses ("the alarm is armed", …). Negation is the copular form the English
# reader normalizes ("the alarm is not armed" → ``~atom``), so the corpus
# exercises the negation machinery (modus tollens, disjunctive syllogism), not
# just affirmative flows. Content is synthetic ON PURPOSE — the reader is
# content-blind (opaque atoms), so the license certifies STRUCTURAL fidelity per
# shape; hand-authored real-English cases live in the eval lane
# (``evals/deduction_serve/v2_en``) to keep the synthetic corpus honest.

_EN_SUBJECTS: tuple[str, ...] = (
    "the alarm", "the door", "the light", "the valve", "the engine",
    "the fan", "the screen", "the sensor", "the pump", "the relay",
    "the switch", "the heater", "the camera", "the router", "the beacon",
    "the latch", "the motor", "the buzzer", "the gate", "the lamp",
)
_EN_STATES: tuple[str, ...] = (
    "on", "off", "open", "closed", "armed", "active",
    "locked", "ready", "hot", "cold", "live", "set",
)
_EN_CLAUSE_COUNT = len(_EN_SUBJECTS) * len(_EN_STATES)


def _en_clause(slot: int) -> str:
    subject = _EN_SUBJECTS[slot % len(_EN_SUBJECTS)]
    state = _EN_STATES[(slot // len(_EN_SUBJECTS)) % len(_EN_STATES)]
    return f"{subject} is {state}"


def _en_clauses(index: int, count: int) -> tuple[str, ...]:
    """``count`` distinct clauses for case ``index`` — deterministic, no RNG."""
    base = (index * 7) % (_EN_CLAUSE_COUNT - count)
    return tuple(_en_clause(base + j) for j in range(count))


def _en_neg(clause: str) -> str:
    """The copular negation of a lexicon clause ("… is X" → "… is not X")."""
    return clause.replace(" is ", " is not ", 1)


#: English-band templates: (gold, text_builder, intended_premises, intended_query).
#: The INTENDED formulas are the template's logical form over fixed placeholder
#: atoms — the reader-independent gold ``assert_corpus_sound`` cross-checks
#: against the truth-table oracle (INV-25: no reader, no ROBDD involvement).
_EN_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = {
    EN_CONDITIONAL_SINGLE: (
        # Modus ponens.
        ("entailed", lambda a, b, c: f"If {a} then {b}. {a.capitalize()}. Therefore {b}.",
         ("pa implies pb", "pa"), "pb"),
        # Modus tollens (copular negation).
        ("entailed", lambda a, b, c: f"If {a} then {b}. {_en_neg(b).capitalize()}. Therefore {_en_neg(a)}.",
         ("pa implies pb", "not pb"), "not pa"),
        # Direct contradiction of the consequent.
        ("refuted", lambda a, b, c: f"If {a} then {b}. {a.capitalize()}. Therefore {_en_neg(b)}.",
         ("pa implies pb", "pa"), "not pb"),
        # Affirming the consequent — classic non-sequitur.
        ("unknown", lambda a, b, c: f"If {a} then {b}. {b.capitalize()}. Therefore {a}.",
         ("pa implies pb", "pb"), "pa"),
        # Denying the antecedent — classic non-sequitur.
        ("unknown", lambda a, b, c: f"If {a} then {b}. {_en_neg(a).capitalize()}. Therefore {_en_neg(b)}.",
         ("pa implies pb", "not pa"), "not pb"),
        # No anchor at all.
        ("unknown", lambda a, b, c: f"If {a} then {b}. Therefore {a}.",
         ("pa implies pb",), "pa"),
    ),
    EN_CONDITIONAL_CHAIN: (
        # Two-hop modus ponens.
        ("entailed", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. {a.capitalize()}. Therefore {c}.",
         ("pa implies pb", "pb implies pc", "pa"), "pc"),
        # Two-hop modus tollens (contraposition through the chain).
        ("entailed", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. {_en_neg(c).capitalize()}. Therefore {_en_neg(a)}.",
         ("pa implies pb", "pb implies pc", "not pc"), "not pa"),
        # Hypothetical syllogism — a conditional CONCLUSION.
        ("entailed", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. Therefore if {a} then {c}.",
         ("pa implies pb", "pb implies pc"), "pa implies pc"),
        # Chain contradiction.
        ("refuted", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. {a.capitalize()}. Therefore {_en_neg(c)}.",
         ("pa implies pb", "pb implies pc", "pa"), "not pc"),
        # Chain with no anchor.
        ("unknown", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. Therefore {c}.",
         ("pa implies pb", "pb implies pc"), "pc"),
    ),
    EN_DISJUNCTIVE: (
        # Disjunctive syllogism.
        ("entailed", lambda a, b, c: f"{a.capitalize()} or {b}. {_en_neg(a).capitalize()}. Therefore {b}.",
         ("pa or pb", "not pa"), "pb"),
        # Disjunctive syllogism, "either" spelling, other disjunct.
        ("entailed", lambda a, b, c: f"Either {a} or {b}. {_en_neg(b).capitalize()}. Therefore {a}.",
         ("pa or pb", "not pb"), "pa"),
        # Constructive dilemma.
        ("entailed", lambda a, b, c: f"If {a} then {c}. If {b} then {c}. {a.capitalize()} or {b}. Therefore {c}.",
         ("pa implies pc", "pb implies pc", "pa or pb"), "pc"),
        # Eliminating one disjunct entails the other — its negation is refuted.
        ("refuted", lambda a, b, c: f"{a.capitalize()} or {b}. {_en_neg(a).capitalize()}. Therefore {_en_neg(b)}.",
         ("pa or pb", "not pa"), "not pb"),
        # A bare disjunction settles neither disjunct.
        ("unknown", lambda a, b, c: f"{a.capitalize()} or {b}. Therefore {a}.",
         ("pa or pb",), "pa"),
    ),
    EN_ATOMIC: (
        # Restatement.
        ("entailed", lambda a, b, c: f"{a.capitalize()}. Therefore {a}.",
         ("pa",), "pa"),
        # Conjunction elimination (top-level "and" premise splits).
        ("entailed", lambda a, b, c: f"{a.capitalize()} and {b}. Therefore {a}.",
         ("pa", "pb"), "pa"),
        # Disjunction introduction.
        ("entailed", lambda a, b, c: f"{a.capitalize()}. Therefore {a} or {b}.",
         ("pa",), "pa or pb"),
        # Conjunction introduction (an "and" CONCLUSION).
        ("entailed", lambda a, b, c: f"{a.capitalize()}. {b.capitalize()}. Therefore {a} and {b}.",
         ("pa", "pb"), "pa and pb"),
        # Direct self-contradiction.
        ("refuted", lambda a, b, c: f"{a.capitalize()}. Therefore {_en_neg(a)}.",
         ("pa",), "not pa"),
        # Unrelated conclusion.
        ("unknown", lambda a, b, c: f"{a.capitalize()}. Therefore {b}.",
         ("pa",), "pb"),
    ),
}

# --- Band v3-MEM (ADR-0258): member-argument synthetic corpus -----------------
#
# Names × class-noun (singular, plural) pairs × state adjectives. The class
# lexicon deliberately exercises EVERY row-type of the reader's closed number
# table — irregular (man/men, person/people, child/children, wolf/wolves,
# mouse/mice, goose/geese), invariant (sheep, fish), and each regular suffix
# rule (+s, +es, y↔ies) — so the earned license certifies the linking relation
# itself, not just the sentence grammar. Content is synthetic ON PURPOSE
# (same posture as the v2-EN corpus above); hand-authored real-English cases
# live in ``evals/deduction_serve/v2_member``.

_MEM_NAMES: tuple[str, ...] = (
    "Rex", "Ada", "Kai", "Milo", "Nova", "Otis", "Pia", "Quinn", "Rio", "Sol",
    "Tara", "Ugo", "Vera", "Wren", "Yara", "Zed", "Bo", "Cyra", "Dax", "Elio",
)
_MEM_CLASSES: tuple[tuple[str, str], ...] = (
    ("man", "men"), ("person", "people"), ("child", "children"),
    ("wolf", "wolves"), ("mouse", "mice"), ("goose", "geese"),
    ("sheep", "sheep"), ("fish", "fish"),
    ("cat", "cats"), ("dog", "dogs"), ("fox", "foxes"), ("pony", "ponies"),
)
_MEM_STATES: tuple[str, ...] = (
    "mortal", "loyal", "wild", "tame", "swift", "calm",
    "bold", "shy", "warm", "quiet", "brave", "free",
)


def _mem_case(index: int) -> tuple[str, str, tuple[str, str], tuple[str, str], tuple[str, str], str]:
    """Deterministic (name1, name2, class1, class2, class3, state) for case
    ``index`` — names and the three classes are always pairwise distinct."""
    n1 = _MEM_NAMES[(index * 3) % len(_MEM_NAMES)]
    n2 = _MEM_NAMES[(index * 3 + 1) % len(_MEM_NAMES)]
    base = (index * 5) % (len(_MEM_CLASSES) - 2)
    c1, c2, c3 = _MEM_CLASSES[base], _MEM_CLASSES[base + 1], _MEM_CLASSES[base + 2]
    state = _MEM_STATES[(index * 7) % len(_MEM_STATES)]
    return n1, n2, c1, c2, c3, state


#: Member-band templates: (gold, text_builder, intended_premises, intended_query).
#: Builders take ``(n1, n2, c1, c2, c3, st)`` from ``_mem_case``; the INTENDED
#: formulas are the template's per-individual lowering over fixed placeholder
#: atoms (``ma`` = first (individual, class) pair, …), cross-checked against
#: the truth-table oracle with no reader in the loop (INV-25).
_MEM_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = {
    EN_MEMBER_SINGLE: (
        # Instantiated modus ponens onto a state predicate.
        ("entailed",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Therefore {n1} is {st}.",
         ("ma", "ma implies mb"), "mb"),
        # Instantiated modus ponens onto a membership conclusion ("every" spelling).
        ("entailed",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. Every {c1[0]} is a {c2[0]}. Therefore {n1} is a {c2[0]}.",
         ("ma", "ma implies mb"), "mb"),
        # Universal stated FIRST ("each" spelling) — order independence.
        ("entailed",
         lambda n1, n2, c1, c2, c3, st: f"Each {c1[0]} is {st}. {n1} is a {c1[0]}. Therefore {n1} is {st}.",
         ("ma implies mb", "ma"), "mb"),
        # Contradicting the instantiated consequent.
        ("refuted",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Therefore {n1} is not {st}.",
         ("ma", "ma implies mb"), "not mb"),
        # Converse instantiation — affirming the consequent.
        ("unknown",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is {st}. All {c1[1]} are {st}. Therefore {n1} is a {c1[0]}.",
         ("mb", "ma implies mb"), "ma"),
        # The universal binds a DIFFERENT named individual than the conclusion's.
        ("unknown",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Therefore {n2} is {st}.",
         ("ma", "ma implies mb", "mc implies md"), "md"),
    ),
    EN_MEMBER_CHAIN: (
        # Two-hop instantiated chain onto a state.
        ("entailed",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Therefore {n1} is {st}.",
         ("ma", "ma implies mb", "mb implies mc"), "mc"),
        # Two-hop chain onto a MEMBERSHIP conclusion — the conclusion's singular
        # article form links to the chain's plural class.
        ("entailed",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {c3[1]}. Therefore {n1} is a {c3[0]}.",
         ("ma", "ma implies mb", "mb implies mc"), "mc"),
        # Chain contradiction.
        ("refuted",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Therefore {n1} is not {st}.",
         ("ma", "ma implies mb", "mb implies mc"), "not mc"),
        # Broken chain — the individual's class never enters it.
        ("unknown",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c2[1]} are {c3[1]}. All {c3[1]} are {st}. Therefore {n1} is {st}.",
         ("ma", "mb implies mc", "mc implies md"), "md"),
        # Reverse traversal — chains do not run backwards.
        ("unknown",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is {st}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Therefore {n1} is a {c1[0]}.",
         ("mc", "ma implies mb", "mb implies mc"), "ma"),
    ),
    EN_MEMBER_NEGATIVE: (
        # Instantiated E-form onto a state.
        ("entailed",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. No {c1[1]} are {st}. Therefore {n1} is not {st}.",
         ("ma", "ma implies not mb"), "not mb"),
        # Instantiated E-form onto a membership conclusion.
        ("entailed",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. No {c1[1]} are {c2[1]}. Therefore {n1} is not a {c2[0]}.",
         ("ma", "ma implies not mb"), "not mb"),
        # A-chain into an E-form.
        ("entailed",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. No {c2[1]} are {st}. Therefore {n1} is not {st}.",
         ("ma", "ma implies mb", "mb implies not mc"), "not mc"),
        # Contradicting the E-form's instantiation.
        ("refuted",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. No {c1[1]} are {st}. Therefore {n1} is {st}.",
         ("ma", "ma implies not mb"), "mb"),
        # Denied antecedent under an E-form — nothing follows.
        ("unknown",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is not a {c1[0]}. No {c1[1]} are {st}. Therefore {n1} is not {st}.",
         ("not ma", "ma implies not mb"), "not mb"),
    ),
    EN_MEMBER_ATOMIC: (
        # Membership restatement (the promoted ds-en-0022 shape).
        ("entailed",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. Therefore {n1} is a {c1[0]}.",
         ("ma",), "ma"),
        # State restatement.
        ("entailed",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is {st}. Therefore {n1} is {st}.",
         ("ma",), "ma"),
        # Selection from two facts about one individual.
        ("entailed",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. {n1} is {st}. Therefore {n1} is {st}.",
         ("ma", "mb"), "mb"),
        # Self-contradiction (membership).
        ("refuted",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. Therefore {n1} is not a {c1[0]}.",
         ("ma",), "not ma"),
        # Negated fact contradicted.
        ("refuted",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is not {st}. Therefore {n1} is {st}.",
         ("not ma",), "ma"),
        # Unrelated conclusion.
        ("unknown",
         lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. Therefore {n1} is {st}.",
         ("ma",), "mb"),
    ),
}

#: Ledger band order: the five v1 bands, the four v2-EN bands, then the four
#: v3-MEM bands.
_ALL_BANDS: tuple[str, ...] = (
    CONDITIONAL_SINGLE, CONDITIONAL_CHAIN, DISJUNCTIVE, ATOMIC, CATEGORICAL,
    EN_CONDITIONAL_SINGLE, EN_CONDITIONAL_CHAIN, EN_DISJUNCTIVE, EN_ATOMIC,
    EN_MEMBER_SINGLE, EN_MEMBER_CHAIN, EN_MEMBER_NEGATIVE, EN_MEMBER_ATOMIC,
)


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
    deterministic atom/clause selection. Each ``payload`` carries the raw
    ``text`` and the by-construction ``gold`` the tether scores against;
    English-band payloads additionally carry the template's ``intended``
    logical form for the reader-independent oracle cross-check.
    """
    problems: list[Problem] = []
    if band in _MEM_TEMPLATES:
        templates = _MEM_TEMPLATES[band]
        for i in range(n):
            gold, builder, intended_premises, intended_query = templates[i % len(templates)]
            problems.append(
                Problem(
                    problem_id=f"{band}-{i:04d}",
                    class_name=band,
                    payload={
                        "text": builder(*_mem_case(i)),
                        "gold": gold,
                        "intended": {
                            "premises": list(intended_premises),
                            "query": intended_query,
                        },
                    },
                )
            )
        return problems
    if band in _EN_TEMPLATES:
        templates = _EN_TEMPLATES[band]
        for i in range(n):
            gold, builder, intended_premises, intended_query = templates[i % len(templates)]
            a, b, c = _en_clauses(i, 3)
            problems.append(
                Problem(
                    problem_id=f"{band}-{i:04d}",
                    class_name=band,
                    payload={
                        "text": builder(a, b, c),
                        "gold": gold,
                        "intended": {
                            "premises": list(intended_premises),
                            "query": intended_query,
                        },
                    },
                )
            )
        return problems
    templates = _TEMPLATES[band]
    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 _ALL_BANDS:
        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",
}

#: Categorical outcome mapping: a syllogism is VALID iff the conclusion is
#: entailed; UNKNOWN/REFUTED ⇒ invalid; REFUSED ⇒ declined (inconsistent).
_CATEGORICAL_TO_CLASS = {
    Entailment.ENTAILED: "valid",
    Entailment.REFUTED: "invalid",
    Entailment.UNKNOWN: "invalid",
    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 — the propositional
    path (``to_deductive_logic`` → ``evaluate_entailment_with_trace``) then the
    categorical path (``to_syllogism`` → ``decide_syllogism``) — and commits the
    decided outcome class. A reader refusal / non-projectable comprehension /
    engine REFUSED is an uncommitted attempt, never a guessed answer. Kept in
    lock-step with the composer's dual path; the lane + license tests cover both.
    """

    domain_id: str = _DOMAIN_ID

    def attempt(self, problem: Problem) -> _DeductionAttempt:
        text = problem.payload["text"]
        comp = comprehend(text)
        if not isinstance(comp, Comprehension):
            # Band v2-EN / v3-MEM fallbacks — mirror the composer: the shared
            # reader refused, but the English-clause or member-argument reader
            # may read it.
            english = self._attempt_english(problem)
            if english is not None:
                return english
            member = self._attempt_member(problem)
            if member is not None:
                return member
            return _DeductionAttempt(
                committed=False, answer=None, reason=f"reader:{getattr(comp, 'reason', '')}",
                case_id=problem.problem_id, shape=problem.class_name,
            )
        # Band v1 — propositional.
        projected = to_deductive_logic(comp)
        if projected is not None:
            premises, query = projected
            outcome = evaluate_entailment_with_trace(premises, query).outcome
            return _DeductionAttempt(
                committed=outcome is not Entailment.REFUSED,
                answer=_OUTCOME_TO_CLASS[outcome], reason="",
                case_id=problem.problem_id, shape=classify_deduction_shape(premises, query),
            )
        # Band v1b — categorical / syllogism.
        syllogism = to_syllogism(comp)
        if syllogism is not None:
            structure, s_query = syllogism
            try:
                outcome = decide_syllogism(structure, s_query).outcome
            except CategoricalError:
                return _DeductionAttempt(
                    committed=False, answer=None, reason="categorical_malformed",
                    case_id=problem.problem_id, shape=CATEGORICAL,
                )
            return _DeductionAttempt(
                committed=outcome is not Entailment.REFUSED,
                answer=_CATEGORICAL_TO_CLASS[outcome], reason="",
                case_id=problem.problem_id, shape=CATEGORICAL,
            )
        english = self._attempt_english(problem)
        if english is not None:
            return english
        member = self._attempt_member(problem)
        if member is not None:
            return member
        return _DeductionAttempt(
            committed=False, answer=None, reason="unprojectable",
            case_id=problem.problem_id, shape=problem.class_name,
        )

    def _attempt_english(self, problem: Problem) -> _DeductionAttempt | None:
        """Band v2-EN: the English-clause argument path, or ``None`` when the
        English reader refuses (the caller then records the honest decline)."""
        arg = read_english_argument(problem.payload["text"])
        if not isinstance(arg, EnglishArgument):
            return None
        outcome = evaluate_entailment_with_trace(
            arg.premise_formulas, arg.query_formula
        ).outcome
        return _DeductionAttempt(
            committed=outcome is not Entailment.REFUSED,
            answer=_OUTCOME_TO_CLASS[outcome], reason="",
            case_id=problem.problem_id, shape=arg.band,
        )

    def _attempt_member(self, problem: Problem) -> _DeductionAttempt | None:
        """Band v3-MEM: the member-argument path, or ``None`` when the member
        reader refuses (the caller then records the honest decline)."""
        arg = read_member_argument(problem.payload["text"])
        if not isinstance(arg, MemberArgument):
            return None
        outcome = evaluate_entailment_with_trace(
            arg.premise_formulas, arg.query_formula
        ).outcome
        return _DeductionAttempt(
            committed=outcome is not Entailment.REFUSED,
            answer=_OUTCOME_TO_CLASS[outcome], reason="",
            case_id=problem.problem_id, shape=arg.band,
        )


@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 an INDEPENDENT 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
    oracles that share no code with the ROBDD serving engine (INV-25): the
    truth-table ``evals.deductive_logic.oracle`` for propositional bands, and
    the finite-model ``evals.syllogism.oracle`` for the categorical band.
    """
    from evals.deductive_logic.oracle import oracle_entailment
    from evals.syllogism.oracle import oracle_answer

    for problem in all_gold_problems():
        gold = problem.payload["gold"]
        # Band v2-EN: the payload carries the template's INTENDED logical form —
        # the oracle checks it directly, with no reader in the loop at all
        # (stronger independence than the v1 path below, which needs the reader
        # to project before the oracle can pronounce).
        intended = problem.payload.get("intended")
        if intended is not None:
            oracle = oracle_entailment(tuple(intended["premises"]), intended["query"])
            assert oracle == gold, (
                f"{problem.problem_id}: oracle={oracle} gold={gold} "
                f"intended={intended!r} text={problem.payload['text']!r}"
            )
            continue
        comp = comprehend(problem.payload["text"])
        assert isinstance(comp, Comprehension), problem.payload["text"]
        projected = to_deductive_logic(comp)
        if projected is not None:
            premises, query = projected
            oracle = oracle_entailment(premises, query)
            assert oracle == gold, (
                f"{problem.problem_id}: oracle={oracle} gold={gold} "
                f"text={problem.payload['text']!r}"
            )
            continue
        syllogism = to_syllogism(comp)
        assert syllogism is not None, problem.payload["text"]
        structure, s_query = syllogism
        oracle_valid = oracle_answer(structure, s_query)["valid"]
        oracle_class = "valid" if oracle_valid else "invalid"
        assert oracle_class == gold, (
            f"{problem.problem_id}: syllogism_oracle={oracle_class} gold={gold} "
            f"text={problem.payload['text']!r}"
        )


__all__ = [
    "CASES_PER_BAND",
    "ConstructionGoldTether",
    "DeductionSolver",
    "all_gold_problems",
    "assert_corpus_sound",
    "generate_problems",
]