Merge pull request #525 from AssetOverflow/feat/adr-0201-1-out-of-regime

Canonicalizer hardening: principled out_of_decidable_regime detector (ADR-0201.1)

docs/decisions/ADR-0201.1-out-of-regime-detector.md

@@ -0,0 +1,112 @@
+# ADR-0201.1 — Principled Out-of-Regime Detector (`out_of_decidable_regime`)
+
+**Status:** Accepted (additive hardening of ADR-0201; phase-1 canonicalizer)
+**Date:** 2026-06-02
+**Relates to:** **ADR-0201** (propositional canonicalizer — this hardens it; see
+§amend-vs-additive), ADR-0202 §3 (the contract that names this typed refusal),
+ADR-0203 (the prior additive-not-amend precedent).
+
+---
+
+## Context
+
+GPT-5.5's independent proof-chain corpus (the separate-author oracle for
+`logic_canonical.py`) cross-checked **22/22** cases against the *real*
+canonicalizer. Twenty agreed exactly; two — the out-of-regime probes
+`forall x. rains(x) -> wet(x)` and `exists x. wet(x)` — agreed on **outcome**
+(both refused) but disagreed on the **reason**:
+
+- ADR-0202 §3 names a typed refusal: quantified/predicate input "must REFUSE
+  (`out_of_decidable_regime`)."
+- The keystone refused, but with a generic `LogicError: "unexpected character
+  '.' at position 8"` — it had **no regime detector**. It refused these inputs
+  only because the tokenizer incidentally chokes on the `.` (or trips on the
+  predicate `(`).
+
+That is a **by-luck-not-by-design refusal** — the exact failure mode the
+`wrong == 0` discipline rejects. The propositional-only boundary that ADR-0202
+declares load-bearing was being enforced by accident, not on purpose. Blessing
+it (relaxing the contract) would write the accident into the contract. The
+corpus caught precisely the thing an independent oracle exists to catch.
+
+## Decision
+
+Make the boundary principled. Add a typed regime refusal, checked **before** the
+generic grammar error:
+
+- **`LogicRegimeError(LogicError)`** carrying the typed reason
+  `OUT_OF_DECIDABLE_REGIME = "out_of_decidable_regime"`. A `LogicError` subclass,
+  so callers refusing on `LogicError` still refuse — but the regime boundary is
+  now distinguishable from a malformed-propositional-formula grammar error.
+- **`_reject_out_of_regime_text(formula)`** — a raw-text pre-scan (before
+  tokenizing) for quantifier markers: the words `forall`/`exists` (word-boundary,
+  case-insensitive) and the symbols `∀`/`∃`. `forall`/`exists` are thereby
+  reserved — not usable as atom ids.
+- **`_reject_out_of_regime_tokens(tokens)`** — a token-stream scan for
+  **predicate-application shape**: an `ATOM` immediately followed by `(`. In the
+  propositional grammar an atom is never followed by `(`, so `ATOM (` is a
+  predicate (`rains(x)`), not a well-formed formula. Keyword operators (`not`,
+  `and`, …) are not `ATOM` tokens, so `not (P)` is unaffected.
+- `canonicalize` runs `_reject_out_of_regime_text` → `_tokenize` →
+  `_reject_out_of_regime_tokens` → parse. `check_equivalence` surfaces the typed
+  reason via a `LogicRegimeError` branch placed before its generic `LogicError`
+  branch.
+
+This is a **refusal**, not new capability: the engine still does no
+predicate/FOL reasoning. It now refuses it **on purpose**, with an inspectable
+typed reason, instead of by tokenizer accident.
+
+## amend-vs-additive
+
+**This is a new additive sub-ADR (ADR-0201.1), not an amendment of the landed
+ADR-0201** — same discipline as ADR-0203-vs-0132: the regime detector became
+load-bearing only when the corpus surfaced the incidental-refusal gap; recording
+it additively preserves that *why-added-later* history rather than rewriting the
+closed canonicalizer record.
+
+Chosen as a **sub-number (0201.1), not a fresh top-level number**, for two
+reasons: (a) it is specifically a hardening of the ADR-0201 canonicalizer (same
+module, same phase-1 keystone), which the sub-number communicates precisely; and
+(b) a top-level `ADR-0204` would collide with the forward references in the
+already-merged ADR-0203 and the recorded phase-2 plan (`0204` = wiring, `0205` =
+modus_ponens, `0206` = grounding). The sub-number keeps those intact.
+
+## Honesty boundary (load-bearing — carried by every phase-2 ADR, 0203–0205)
+
+Through phase 2.3, `proof_chain` is **sound over its declared atoms**, not
+grounded in recognized input (grounding is phase 2.4). This ADR does **not**
+soften that, and it does not add predicate/FOL reasoning — it makes the
+**propositional-only** boundary principled by refusing out-of-regime input with a
+typed reason. The boundary is enforced by design, never "reasons over input."
+
+## Evidence
+
+- `tests/test_logic_canonical.py` — 43 tests (33 keystone + 10 new): quantifier
+  words/symbols and predicate application refuse with `LogicRegimeError` /
+  `out_of_decidable_regime`; the equivalence path surfaces the typed reason;
+  genuine grammar errors (`P &`, `P @ Q`, `(P`) still raise *plain* `LogicError`
+  (detector does not over-fire); `not (P)` is not mistaken for predicate
+  application.
+- **Mutation-verified by-design:** neutering both detectors makes
+  `forall x. …` fall through to the generic grammar error
+  (`unexpected character '.'`) instead of the typed reason —
+  `test_out_of_regime_refuses_with_typed_reason` would fail. The boundary holds
+  on purpose, not by luck.
+- **Corpus now 22/22:** the two OOR cases (PC-OOR-001/002) now agree on the
+  principled `out_of_decidable_regime` reason.
+- Full canonicalizer suite green; smoke: 67 passed.
+
+## Note carried to the corpus (rule-reasons pending 2.3)
+
+The 3 `modus_ponens` corpus cases were validated only at the **entailment** level
+the canonicalizer provides (`(⋀premises) → conclusion` is/ isn't a tautology).
+Their typed *rule* reasons (`modus_ponens_conclusion_mismatch`,
+`modus_ponens_missing_implication`) are **deferred to ADR-0205** (phase 2.3), when
+the `modus_ponens` rule is built. The corpus should carry an explicit
+"rule-reasons pending 2.3" marker on those cases so the deferral is recorded, not
+assumed validated.
+
+## Scope
+
+Phase-1 canonicalizer hardening only. Does **not** build `modus_ponens`,
+binding-graph wiring, or any predicate/FOL support.

generate/logic_canonical.py

@@ -30,6 +30,7 @@ hand-rolled symbolic normalizer.
 
 from __future__ import annotations
 
+import re
 from dataclasses import dataclass
 from typing import Final
 
@@ -50,6 +51,21 @@ class LogicBudgetError(LogicError):
     math gate refusing rather than churning."""
 
 
+class LogicRegimeError(LogicError):
+    """Raised when the input is outside the decidable **propositional** regime —
+    quantified or predicate logic (ADR-0201.1; the typed refusal ADR-0202 §3
+    names). A subclass of :class:`LogicError` so callers that refuse on
+    ``LogicError`` refuse here too, but it carries the typed
+    :data:`OUT_OF_DECIDABLE_REGIME` reason so the regime boundary is
+    distinguishable from a generic malformed-formula grammar error.
+
+    Crucially, the boundary is enforced **by design** (see
+    :func:`_reject_out_of_regime_text` / :func:`_reject_out_of_regime_tokens`),
+    not by the tokenizer incidentally choking on an out-of-grammar character —
+    the latter is the by-luck-not-by-design refusal the ``wrong == 0``
+    discipline rejects."""
+
+
 # ---------------------------------------------------------------------------
 # Public defaults
 # ---------------------------------------------------------------------------
@@ -460,11 +476,69 @@ class CanonicalProposition:
     is_contradiction: bool
 
 
+# ---------------------------------------------------------------------------
+# Out-of-regime detection (ADR-0201.1)
+#
+# Propositional logic is the only regime with a canonical form + decidable
+# equivalence. Quantified / predicate input must REFUSE with the typed
+# `out_of_decidable_regime` reason (ADR-0202 §3) — by DESIGN, recognized as
+# out-of-regime, not by accident of the tokenizer choking on an out-of-grammar
+# character. These checks run BEFORE the generic grammar error so the regime
+# boundary is principled, typed, and inspectable.
+# ---------------------------------------------------------------------------
+
+OUT_OF_DECIDABLE_REGIME: Final[str] = "out_of_decidable_regime"
+
+# Quantifier markers: ASCII keywords (word-boundary, case-insensitive) and the
+# logic symbols ∀ / ∃. Their presence means first-order/predicate reasoning,
+# which has no ROBDD canonical form and is undecidable in general. `forall` and
+# `exists` are therefore reserved — not usable as atom ids.
+_QUANTIFIER_WORD_RE: Final[re.Pattern[str]] = re.compile(r"\b(forall|exists)\b", re.IGNORECASE)
+_QUANTIFIER_SYMBOLS: Final[frozenset[str]] = frozenset({"∀", "∃"})  # ∀ ∃
+
+
+def _reject_out_of_regime_text(formula: str) -> None:
+    """Refuse raw input that carries a quantifier marker. Runs before tokenizing
+    so quantifier symbols (∀/∃) and the ``forall x. …`` / ``exists x. …`` shape
+    refuse with the typed regime reason rather than a generic 'unexpected
+    character' grammar error from the trailing ``.``/predicate syntax."""
+    for sym in sorted(_QUANTIFIER_SYMBOLS):
+        if sym in formula:
+            raise LogicRegimeError(f"{OUT_OF_DECIDABLE_REGIME}: quantifier symbol {sym!r}")
+    match = _QUANTIFIER_WORD_RE.search(formula)
+    if match is not None:
+        raise LogicRegimeError(f"{OUT_OF_DECIDABLE_REGIME}: quantifier {match.group(0)!r}")
+
+
+def _reject_out_of_regime_tokens(tokens: list[tuple[str, str]]) -> None:
+    """Refuse predicate-application shape — an atom immediately applied to an
+    argument list, e.g. ``rains(x)``. In the propositional grammar an atom is
+    never followed by ``(`` (grouping only follows an operator or opens an
+    expression), so ``ATOM (`` is a predicate, not a well-formed propositional
+    formula. Runs before the parser's generic trailing-token error so the regime
+    boundary is the reason that surfaces. (Keyword operators such as ``not`` are
+    NOT ``ATOM`` tokens, so ``not (P)`` is unaffected.)"""
+    for (kind, lexeme), (next_kind, _next_lexeme) in zip(tokens, tokens[1:]):
+        if kind == "ATOM" and next_kind == "LPAREN":
+            raise LogicRegimeError(
+                f"{OUT_OF_DECIDABLE_REGIME}: predicate application {lexeme!r}(…)"
+            )
+
+
 def canonicalize(formula: str, *, max_nodes: int = DEFAULT_MAX_NODES) -> CanonicalProposition:
     """Canonicalize ``formula`` to its ROBDD identity under the sorted-atom
-    ordering. Raises :class:`LogicError` on out-of-grammar input and
-    :class:`LogicBudgetError` if the diagram exceeds ``max_nodes``."""
-    ast = _Parser(_tokenize(formula)).parse()
+    ordering. Refusal-first:
+
+    * :class:`LogicRegimeError` (``out_of_decidable_regime``) if the input is
+      quantified / predicate logic — checked *before* grammar, so the regime
+      boundary is principled, not an incidental tokenizer failure;
+    * :class:`LogicError` on out-of-grammar (malformed propositional) input;
+    * :class:`LogicBudgetError` if the diagram exceeds ``max_nodes``.
+    """
+    _reject_out_of_regime_text(formula)
+    tokens = _tokenize(formula)
+    _reject_out_of_regime_tokens(tokens)
+    ast = _Parser(tokens).parse()
     declared = tuple(sorted(_collect_atoms(ast)))  # fixed variable ordering
     index_of = {name: i for i, name in enumerate(declared)}
     bdd = _Bdd(var_count=len(declared), max_nodes=max_nodes)

generate/logic_equivalence.py

@@ -19,8 +19,10 @@ from typing import Final
 
 from generate.logic_canonical import (
     DEFAULT_MAX_NODES,
+    OUT_OF_DECIDABLE_REGIME,
     LogicBudgetError,
     LogicError,
+    LogicRegimeError,
     canonicalize,
 )
 
@@ -65,6 +67,15 @@ def check_equivalence(
             canonical_b=None,
             reason=f"canonicalization_budget_exceeded: {exc}",
         )
+    except LogicRegimeError as exc:
+        # Out of the decidable propositional regime (quantified/predicate).
+        # Caught before the generic LogicError branch since it is a subclass.
+        return EquivalenceVerdict(
+            verdict=Verdict.REFUSED,
+            canonical_a=None,
+            canonical_b=None,
+            reason=f"{OUT_OF_DECIDABLE_REGIME}: {exc}",
+        )
     except LogicError as exc:
         return EquivalenceVerdict(
             verdict=Verdict.REFUSED,

tests/test_logic_canonical.py

@@ -13,8 +13,10 @@ import pytest
 
 from generate.logic_canonical import (
     DEFAULT_MAX_NODES,
+    OUT_OF_DECIDABLE_REGIME,
     LogicBudgetError,
     LogicError,
+    LogicRegimeError,
     canonicalize,
 )
 from generate.logic_equivalence import Verdict, check_equivalence
@@ -165,3 +167,53 @@ def test_bounded_formula_stays_within_default_budget() -> None:
     # A realistic proof-step proposition canonicalizes well within budget.
     c = canonicalize("(P -> Q) & (Q -> R) & P", max_nodes=DEFAULT_MAX_NODES)
     assert c.canonical_key  # non-empty, did not refuse
+
+
+# ---------------------------------------------------------------------------
+# Out-of-regime: quantified / predicate input REFUSES with the typed reason
+# (ADR-0201.1). The boundary is enforced by DESIGN, before the generic grammar
+# error — not by the tokenizer incidentally choking on '.' or a predicate '('.
+# ---------------------------------------------------------------------------
+
+OUT_OF_REGIME_INPUTS = [
+    "forall x. rains(x) -> wet(x)",   # universal (the PC-OOR-001 corpus case)
+    "exists x. wet(x)",               # existential (PC-OOR-002)
+    "∀ x rains",                      # quantifier symbol
+    "∃ y wet",                        # quantifier symbol
+    "rains(x)",                       # predicate application, no quantifier word
+    "P & wet(y)",                     # predicate application mid-formula
+    "FORALL z holds",                 # case-insensitive keyword
+]
+
+
+@pytest.mark.parametrize("text", OUT_OF_REGIME_INPUTS)
+def test_out_of_regime_refuses_with_typed_reason(text: str) -> None:
+    with pytest.raises(LogicRegimeError) as exc:
+        canonicalize(text)
+    assert OUT_OF_DECIDABLE_REGIME in str(exc.value)
+    # And the equivalence path surfaces the typed reason, not a generic one.
+    v = check_equivalence(text, "P")
+    assert v.verdict is Verdict.REFUSED
+    assert OUT_OF_DECIDABLE_REGIME in v.reason
+
+
+def test_regime_error_is_a_logic_error_subclass() -> None:
+    # Callers refusing on LogicError still refuse on out-of-regime.
+    assert issubclass(LogicRegimeError, LogicError)
+
+
+def test_genuine_grammar_errors_are_not_misreported_as_out_of_regime() -> None:
+    # The detector is principled: malformed *propositional* input is a plain
+    # LogicError (grammar), NOT a regime refusal. Guards against over-firing.
+    for bad in ["P &", "P @ Q", "P -> -> Q", "(P", "P)"]:
+        with pytest.raises(LogicError) as exc:
+            canonicalize(bad)
+        assert not isinstance(exc.value, LogicRegimeError), bad
+        assert OUT_OF_DECIDABLE_REGIME not in str(exc.value), bad
+
+
+def test_keyword_operators_before_paren_are_not_predicate_application() -> None:
+    # `not (P)` is valid: NOT is a keyword operator, not an ATOM, so the
+    # ATOM-then-LPAREN predicate rule must not fire.
+    assert canonicalize("not (P)").canonical_key == canonicalize("~P").canonical_key
+    assert canonicalize("not(P)").canonical_key == canonicalize("~P").canonical_key