From 3e2a52870de4be1d05181cf39e3ddf37cf272d3a Mon Sep 17 00:00:00 2001 From: Shay Date: Thu, 4 Jun 2026 16:32:03 -0700 Subject: [PATCH] =?UTF-8?q?feat:=20Phase=202=20=E2=80=94=20finite-entity?= =?UTF-8?q?=20grounding=20compiler=20+=20Phase=201.5=20finding?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The first comprehension->structure compiler: evals/deductive_logic/grounding.py lowers a typed finite-entity problem (finite entities + unary predicates + single-variable universal rules) into the propositional regime the ADR-0206 entailment operator decides, refusal-first with a closed typed reason vocabulary (unsafe_symbol / unknown_entity / unsupported_predicate_arity / unsupported_ quantifier / malformed_case / empty_case) and collision-safe atom slugging. finite_entity/v1/cases.jsonl: 8 cases with INDEPENDENT (oracle-derived) gold (4 entailed, 2 unknown, 1 refuted, 1 refused) — chained rules, conjunctive bodies, negative heads, inconsistent premises. 20 tests gate engine==oracle==gold. This is the second diversity-panel domain (distinct comprehension, same checkable substrate) — the universal-structure thesis validated on a different problem shape, with the anti-overfit >=2-domain discipline now live. Phase 1.5 finding recorded: a clean geometric/algebraic propositional decoder agrees 716/716 with the oracle but is O(2^n) (enumeration-class), so logic is the wrong first domain for field-as-reasoner; the wedge redirects to quantitative- relational structure where the field is the natural non-redundant decoder. --- ...-field-symbol-coherence-gate-2026-06-04.md | 68 ++++-- .../finite_entity/v1/cases.jsonl | 8 + evals/deductive_logic/grounding.py | 201 ++++++++++++++++++ ...deductive_logic_finite_entity_grounding.py | 169 +++++++++++++++ 4 files changed, 425 insertions(+), 21 deletions(-) create mode 100644 evals/deductive_logic/finite_entity/v1/cases.jsonl create mode 100644 evals/deductive_logic/grounding.py create mode 100644 tests/test_deductive_logic_finite_entity_grounding.py diff --git a/docs/analysis/universal-structure-and-field-symbol-coherence-gate-2026-06-04.md b/docs/analysis/universal-structure-and-field-symbol-coherence-gate-2026-06-04.md index a682c38e..d756e7f2 100644 --- a/docs/analysis/universal-structure-and-field-symbol-coherence-gate-2026-06-04.md +++ b/docs/analysis/universal-structure-and-field-symbol-coherence-gate-2026-06-04.md @@ -112,13 +112,28 @@ result is an acceptable, honest outcome: where the field cannot earn agreement, **stays a servant** and the symbolic path carries that domain, refusing where it cannot verify. **No unfalsifiable "the field knows" claim ever enters the codebase.** -**The wedge (Phase 1.5):** *Can the field decide propositional entailment -geometrically and agree with the ROBDD oracle on held-out, `wrong = 0`?* Logic is -the ideal first test — the ROBDD + independent oracle already give a rock-solid gold -(500/500). Embed atoms/clauses as geometric objects; decide entailment by -incidence/coherence; require `field_verdict == ROBDD_verdict == oracle` on a -held-out set. Agree → the field has earned a reasoning role and we have our first -genuine second derivation. Cannot → we learned it cheaply and honestly. +**The wedge (Phase 1.5) — FINDING (2026-06-04): logic is the wrong first domain.** +The original wedge asked whether the field could decide *propositional entailment* +geometrically and agree with the ROBDD oracle. A bounded experiment settled it: the +cleanest geometric/algebraic encoding (the commuting-idempotent *function-algebra*, +each formula → its function on the `2^n` minterms) **agrees 716/716 with the oracle +but is `O(2^n)`** — it is truth-table enumeration in algebraic clothing, *not* a +genuine sub-enumeration reduction the way the ROBDD is. So a geometric decoder for +logic would either re-encode enumeration (adding no independence the oracle does not +already provide) or be decoration. **Propositional logic is combinatorial +(all-assignments), not geometric/metric** — the field engine's native strength +(distance, incidence, proportion, betweenness) has no purchase there. + +**Corrected wedge — quantitative-relational structure.** The field must first earn +its reasoning role where the structure is genuinely *metric*: quantitative-relational +problems (`A is twice B`, `A is 3 more than B`, part-whole, ratios) — exactly where +GSM8K *comprehension* lives. There, the field derivation (solve the linear/metric +relation system by propagation) and the symbolic derivation (step-by-step arithmetic) +are two genuinely distinct decodings, and their agreement on the dataset answer is a +real second derivation. Logic keeps its independent gold (ROBDD ⟂ truth-table oracle) +as a *symbolic* second derivation; the *field* earns its role in the metric domains. +This is the plan working as designed: the field earned nothing it did not deserve, +and we learned the right domain cheaply. ## 4. Phased plan @@ -126,20 +141,31 @@ genuine second derivation. Cannot → we learned it cheaply and honestly. (`tests/test_architectural_invariants.py`): no capability claim without an independent gold sharing no code with the SUT; deductive lane SHA-pinned (`deductive_logic_v1`). The foundation every later phase rides on. -- **Phase 1 — canonize the universal structure.** Promote - `SemanticSymbolicBindingGraph` to *the* documented problem-structure interlingua; - resolve its closed-vocab placeholder (`semantic_role="unknown"`) only when a - load-bearing consumer defines it. Add a **hemisphere-role invariant**: servant - modules (parsers, metrics, vault) may not bypass the structure's consistency - checks. (The taxonomy is a proposal to validate before the enforcing INV lands.) -- **Phase 1.5 — the keystone wedge.** Field-decides-entailment vs. ROBDD oracle on - the deductive lane. Prove (or honestly refute) field-as-reasoner on the safest - gold. Gate to everything geometric. -- **Phase 2 — comprehension compiler → binding graph** (finite-entity grounding - first), with **field ⟂ symbol agreement** as the admission gate from the moment - Phase 1.5 succeeds. **The diversity panel starts here** (see cross-cutting): the - compiler is validated against ≥2 structurally-distinct golded domains from its - first commit, so it cannot overfit to math-shaped problems. +- **Phase 1 — canonize the universal structure. ✅ SHIPPED.** + `SemanticSymbolicBindingGraph` is the documented problem-structure interlingua; + **INV-26** enforces its neutrality (the interlingua imports no field/eval/runtime, + and its core imports no domain reader — only allowlisted bridges may). Deferred: + resolving the closed-vocab placeholder (`semantic_role="unknown"`) until a + load-bearing consumer defines it; the stronger "servant may not bypass consistency + checks" rule (the checkable neutrality half shipped; the rest stays doctrine until + a checkable form exists). +- **Phase 1.5 — the keystone wedge. ✅ RUN (logic ruled out; wedge redirected).** + The propositional-logic wedge was settled by experiment (§3): a clean geometric + encoding is enumeration-class, so logic cannot prove field-as-reasoner. The wedge + is redirected to **quantitative-relational** structure, where the field + (metric/proportion propagation) and the symbol (step arithmetic) are genuinely + distinct decodings. The dedicated quantitative wedge is the next field-reasoner + experiment. +- **Phase 2 — comprehension compiler → binding graph.** **✅ FIRST SLICE SHIPPED:** + the finite-entity grounding compiler (`evals/deductive_logic/grounding.py`) lowers + a typed finite-entity problem (entities + unary predicates + single-var universal + rules) into the propositional regime, refusal-first, gated by `engine == oracle == + gold` — the first reader proving a *different problem shape* compiles into the same + checkable substrate. **The diversity panel starts here** (see cross-cutting): + finite-entity is the second golded domain, so the compiler is validated against ≥2 + structurally-distinct domains from its first commit and cannot overfit to one + shape. Remaining Phase 2: target the binding-graph interlingua directly and add + **field ⟂ symbol agreement** as the admission gate once the quantitative wedge lands. - **Phase 3 — activate `t2_precision`.** The field⟂symbol agreement *is* the t2 signal; wire the propose-loop consuming `checker="t2_precision"`. No invented second derivation needed — it is real now. diff --git a/evals/deductive_logic/finite_entity/v1/cases.jsonl b/evals/deductive_logic/finite_entity/v1/cases.jsonl new file mode 100644 index 00000000..98038e76 --- /dev/null +++ b/evals/deductive_logic/finite_entity/v1/cases.jsonl @@ -0,0 +1,8 @@ +{"entities": ["cat", "dog"], "facts": [{"entity": "cat", "polarity": true, "predicate": "furry"}], "gold": "entailed", "id": "fe-v1-0001", "query": {"entity": "cat", "polarity": true, "predicate": "mammal"}, "rules": [{"if": [{"polarity": true, "predicate": "furry", "var": "x"}], "then": {"polarity": true, "predicate": "mammal", "var": "x"}}]} +{"entities": ["cat", "dog"], "facts": [{"entity": "cat", "polarity": true, "predicate": "furry"}], "gold": "unknown", "id": "fe-v1-0002", "query": {"entity": "dog", "polarity": true, "predicate": "mammal"}, "rules": [{"if": [{"polarity": true, "predicate": "furry", "var": "x"}], "then": {"polarity": true, "predicate": "mammal", "var": "x"}}]} +{"entities": ["alice"], "facts": [{"entity": "alice", "polarity": true, "predicate": "human"}], "gold": "entailed", "id": "fe-v1-0003", "query": {"entity": "alice", "polarity": true, "predicate": "mortal"}, "rules": [{"if": [{"polarity": true, "predicate": "human", "var": "x"}], "then": {"polarity": true, "predicate": "mortal", "var": "x"}}]} +{"entities": ["bird1"], "facts": [{"entity": "bird1", "polarity": true, "predicate": "penguin"}], "gold": "refuted", "id": "fe-v1-0004", "query": {"entity": "bird1", "polarity": true, "predicate": "flies"}, "rules": [{"if": [{"polarity": true, "predicate": "penguin", "var": "x"}], "then": {"polarity": false, "predicate": "flies", "var": "x"}}]} +{"entities": ["x1"], "facts": [{"entity": "x1", "polarity": true, "predicate": "a"}], "gold": "entailed", "id": "fe-v1-0005", "query": {"entity": "x1", "polarity": true, "predicate": "c"}, "rules": [{"if": [{"polarity": true, "predicate": "a", "var": "v"}], "then": {"polarity": true, "predicate": "b", "var": "v"}}, {"if": [{"polarity": true, "predicate": "b", "var": "v"}], "then": {"polarity": true, "predicate": "c", "var": "v"}}]} +{"entities": ["t"], "facts": [{"entity": "t", "polarity": true, "predicate": "red"}, {"entity": "t", "polarity": true, "predicate": "round"}], "gold": "entailed", "id": "fe-v1-0006", "query": {"entity": "t", "polarity": true, "predicate": "apple"}, "rules": [{"if": [{"polarity": true, "predicate": "red", "var": "x"}, {"polarity": true, "predicate": "round", "var": "x"}], "then": {"polarity": true, "predicate": "apple", "var": "x"}}]} +{"entities": ["t"], "facts": [{"entity": "t", "polarity": true, "predicate": "red"}], "gold": "unknown", "id": "fe-v1-0007", "query": {"entity": "t", "polarity": true, "predicate": "apple"}, "rules": [{"if": [{"polarity": true, "predicate": "red", "var": "x"}, {"polarity": true, "predicate": "round", "var": "x"}], "then": {"polarity": true, "predicate": "apple", "var": "x"}}]} +{"entities": ["s"], "facts": [{"entity": "s", "polarity": true, "predicate": "sick"}, {"entity": "s", "polarity": false, "predicate": "sick"}], "gold": "refused", "id": "fe-v1-0008", "query": {"entity": "s", "polarity": true, "predicate": "sick"}, "rules": []} diff --git a/evals/deductive_logic/grounding.py b/evals/deductive_logic/grounding.py new file mode 100644 index 00000000..eb125434 --- /dev/null +++ b/evals/deductive_logic/grounding.py @@ -0,0 +1,201 @@ +"""Finite-entity grounding — compile a typed finite-entity problem to +propositional atoms (Phase 2 of the universal-structure plan; the deductive-logic +runway doc's PR-1). + +This is the first **comprehension compiler**: it lowers a structured, finite-entity +problem (finite named entities, unary predicates, single-variable universal rules) +into the propositional regime the ADR-0206 entailment operator already decides — +exactly where `wrong == 0` is structural. A grounded finite-entity problem (each +``predicate(entity)`` pair → one atom) IS propositional and in scope; anything +outside the narrow v1 grammar refuses with a typed reason rather than guessing. + +Lowering law (deterministic): + + predicate(entity) -> ``predicate_slug__entity_slug`` (atom) + negative literal -> ``~atom`` + rule body (∧ of literals) -> conjunction of lowered body literals + universal rule ∀x. B(x)->H(x)-> for each entity e: ``lower(B[e]) -> lower(H[e])`` + query -> the lowered query literal + +The lowered ``(premises, query)`` is decided by **two independent procedures** +(the ROBDD engine and the truth-table oracle); a case counts only when both agree +with the gold (INV-25). v1 keeps the grammar intentionally narrow — that narrowness +is the firewall, not a weakness. + +Sealed: no ``chat`` import, no serving path. Deterministic. +""" + +from __future__ import annotations + +import re +from dataclasses import dataclass +from typing import Any, Final + +# Closed refusal vocabulary for the grounding layer — distinct from the entailment +# operator's reasons so a malformed case never leaks into an ambiguous failure. +UNSUPPORTED_PREDICATE_ARITY: Final[str] = "unsupported_predicate_arity" +UNSUPPORTED_QUANTIFIER: Final[str] = "unsupported_quantifier" +UNSAFE_SYMBOL: Final[str] = "unsafe_symbol" +UNKNOWN_ENTITY: Final[str] = "unknown_entity" +UNKNOWN_VARIABLE: Final[str] = "unknown_variable" +MALFORMED_CASE: Final[str] = "malformed_case" +EMPTY_CASE: Final[str] = "empty_case" + +GROUNDING_REASONS: Final[frozenset[str]] = frozenset({ + UNSUPPORTED_PREDICATE_ARITY, + UNSUPPORTED_QUANTIFIER, + UNSAFE_SYMBOL, + UNKNOWN_ENTITY, + UNKNOWN_VARIABLE, + MALFORMED_CASE, + EMPTY_CASE, +}) + +_ATOM_SEPARATOR: Final[str] = "__" +# A slug component: lowercase ASCII letters/digits/single underscores, no leading +# digit, no empty, no double-underscore (would collide with the separator). +_SLUG_RE: Final[re.Pattern[str]] = re.compile(r"[a-z][a-z0-9]*(?:_[a-z0-9]+)*") + + +class GroundingError(ValueError): + """A finite-entity case outside the v1 grammar. Carries a typed reason.""" + + def __init__(self, reason: str, detail: str = "") -> None: + if reason not in GROUNDING_REASONS: + raise ValueError(f"unknown grounding reason: {reason!r}") + self.reason = reason + super().__init__(f"{reason}: {detail}" if detail else reason) + + +@dataclass(frozen=True, slots=True) +class GroundedProblem: + """The lowered finite-entity problem: propositional premises + query.""" + + premises: tuple[str, ...] + query: str + + +def slug(token: Any) -> str: + """Deterministic, collision-safe slug. Rejects (never silently repairs) + anything outside ``[a-z][a-z0-9]*(_[a-z0-9]+)*`` — including the separator, + leading digits, empties, and double underscores.""" + if not isinstance(token, str): + raise GroundingError(UNSAFE_SYMBOL, f"non-string symbol {token!r}") + s = token.strip().lower() + if not s: + raise GroundingError(UNSAFE_SYMBOL, "empty symbol") + if _ATOM_SEPARATOR in s: + raise GroundingError(UNSAFE_SYMBOL, f"symbol {token!r} contains separator '{_ATOM_SEPARATOR}'") + if not _SLUG_RE.fullmatch(s): + raise GroundingError(UNSAFE_SYMBOL, f"symbol {token!r} is not a safe slug") + return s + + +def atom(predicate: Any, entity: Any) -> str: + """``predicate(entity)`` → the canonical propositional atom.""" + return f"{slug(predicate)}{_ATOM_SEPARATOR}{slug(entity)}" + + +def _literal(predicate: Any, entity: Any, polarity: Any) -> str: + if not isinstance(polarity, bool): + raise GroundingError(MALFORMED_CASE, f"polarity must be a bool, got {polarity!r}") + a = atom(predicate, entity) + return a if polarity else f"~{a}" + + +def _require(condition: bool, reason: str, detail: str = "") -> None: + if not condition: + raise GroundingError(reason, detail) + + +def _check_unary(obj: dict[str, Any], *, allow_var: bool) -> None: + """Reject any non-unary / relational / functional shape (v1 is unary only).""" + keys = set(obj) + # A binary relation / function would carry extra argument keys. + extra = keys - {"predicate", "entity", "var", "polarity"} + _require(not extra, UNSUPPORTED_PREDICATE_ARITY, f"unexpected keys {sorted(extra)}") + has_entity = "entity" in obj + has_var = "var" in obj + if allow_var: + _require(has_entity ^ has_var, MALFORMED_CASE, "literal needs exactly one of entity/var") + else: + _require(has_entity and not has_var, UNKNOWN_VARIABLE, "free variable outside a rule") + + +def lower_case(case: dict[str, Any]) -> GroundedProblem: + """Lower a finite-entity case to ``(premises, query)``. Refuse-first. + + Schema (v1): + {"entities": [str, ...], + "facts": [{"predicate": str, "entity": str, "polarity": bool}, ...], + "rules": [{"if": [, ...], + "then": }, ...], + "query": {"predicate": str, "entity": str, "polarity": bool}} + """ + if not isinstance(case, dict) or not case: + raise GroundingError(EMPTY_CASE, "case is empty or not a mapping") + + entities = case.get("entities") + if not (isinstance(entities, list) and entities): + raise GroundingError(EMPTY_CASE, "no entities") + entity_set = {slug(e) for e in entities} # also validates each entity slug + _require(len(entity_set) == len(entities), MALFORMED_CASE, "duplicate entities after slugging") + + if "query" not in case: + raise GroundingError(MALFORMED_CASE, "no query") + + premises: list[str] = [] + + facts = case.get("facts", []) or [] + rules = case.get("rules", []) or [] + _require(isinstance(facts, list), MALFORMED_CASE, "facts must be a list") + _require(isinstance(rules, list), MALFORMED_CASE, "rules must be a list") + + # Facts — ground unary literals over named entities. + for fact in facts: + _require(isinstance(fact, dict), MALFORMED_CASE, f"fact is not a mapping: {fact!r}") + _check_unary(fact, allow_var=False) + _require(slug(fact["entity"]) in entity_set, UNKNOWN_ENTITY, str(fact.get("entity"))) + premises.append(_literal(fact["predicate"], fact["entity"], fact.get("polarity", True))) + + # Rules — single-variable universal rules, grounded by explicit entity expansion. + for rule in rules: + _require(isinstance(rule, dict), MALFORMED_CASE, f"rule is not a mapping: {rule!r}") + _require("quantifier" not in rule and "exists" not in rule, + UNSUPPORTED_QUANTIFIER, "only implicit single-var universal rules in v1") + body = rule.get("if") + head = rule.get("then") + if not (isinstance(body, list) and body): + raise GroundingError(MALFORMED_CASE, "rule body must be a non-empty list") + if not isinstance(head, dict): + raise GroundingError(MALFORMED_CASE, "rule head must be a literal") + var = _rule_variable(body, head) + for ent in entities: + body_atoms = [_literal(lit["predicate"], ent, lit.get("polarity", True)) for lit in body] + head_atom = _literal(head["predicate"], ent, head.get("polarity", True)) + body_conj = " & ".join(f"({b})" for b in body_atoms) + premises.append(f"({body_conj}) -> ({head_atom})") + _ = var # validated; grounding is by explicit entity expansion, not by name + + query = case["query"] + _require(isinstance(query, dict), MALFORMED_CASE, "query must be a literal") + _check_unary(query, allow_var=False) + _require(slug(query["entity"]) in entity_set, UNKNOWN_ENTITY, str(query.get("entity"))) + query_lit = _literal(query["predicate"], query["entity"], query.get("polarity", True)) + + return GroundedProblem(premises=tuple(premises), query=query_lit) + + +def _rule_variable(body: list[dict[str, Any]], head: dict[str, Any]) -> str: + """Confirm the rule is single-variable: every literal uses one shared var, + no named entities (those would make it not universal). Returns the var name.""" + seen: set[str] = set() + for lit in (*body, head): + _require(isinstance(lit, dict), MALFORMED_CASE, f"rule literal not a mapping: {lit!r}") + _check_unary(lit, allow_var=True) + _require("var" in lit, MALFORMED_CASE, "rule literals must use a variable, not a named entity") + v = lit["var"] + _require(isinstance(v, str) and bool(v.strip()), MALFORMED_CASE, "empty variable") + seen.add(v) + _require(len(seen) == 1, UNSUPPORTED_QUANTIFIER, f"v1 allows one variable per rule, saw {sorted(seen)}") + return seen.pop() diff --git a/tests/test_deductive_logic_finite_entity_grounding.py b/tests/test_deductive_logic_finite_entity_grounding.py new file mode 100644 index 00000000..6b7efb87 --- /dev/null +++ b/tests/test_deductive_logic_finite_entity_grounding.py @@ -0,0 +1,169 @@ +"""Phase 2 — finite-entity grounding compiler (deductive-logic runway PR-1/PR-2). + +Proves the first comprehension compiler lowers a typed finite-entity problem into +the propositional regime deterministically and refusal-first, and that the lowered +form is decided identically by the ROBDD engine AND the independent truth-table +oracle (INV-25: the committed gold is reproduced by a procedure sharing no code +with the engine). +""" + +from __future__ import annotations + +import json +from pathlib import Path + +import pytest + +from evals.deductive_logic.grounding import ( + MALFORMED_CASE, + UNKNOWN_ENTITY, + UNSAFE_SYMBOL, + UNSUPPORTED_PREDICATE_ARITY, + UNSUPPORTED_QUANTIFIER, + GroundingError, + atom, + lower_case, + slug, +) +from evals.deductive_logic.oracle import oracle_entailment +from generate.proof_chain.entail import evaluate_entailment + +_FIXTURE = Path(__file__).resolve().parents[1] / "evals" / "deductive_logic" / "finite_entity" / "v1" / "cases.jsonl" + + +def _load_fixture() -> list[dict]: + return [json.loads(line) for line in _FIXTURE.read_text(encoding="utf-8").splitlines() if line.strip()] + + +# --- lowering correctness ----------------------------------------------------- + + +def test_atom_lowering_is_deterministic_and_canonical() -> None: + assert atom("Furry", "Cat") == "furry__cat" + assert atom("furry", "cat") == atom("Furry", " CAT ") # case/space-insensitive + assert atom("needs_food", "cat") == "needs_food__cat" + + +def test_unsafe_symbols_and_separator_ambiguity_reject() -> None: + for bad in ("fur__ry", "9lives", "", "has-claws", "a b", "tïger"): + with pytest.raises(GroundingError) as exc: + slug(bad) + assert exc.value.reason == UNSAFE_SYMBOL + + +def test_fact_lowering_including_negative_facts() -> None: + case = { + "entities": ["cat"], + "facts": [ + {"predicate": "furry", "entity": "cat", "polarity": True}, + {"predicate": "aquatic", "entity": "cat", "polarity": False}, + ], + "query": {"predicate": "furry", "entity": "cat", "polarity": True}, + } + gp = lower_case(case) + assert "furry__cat" in gp.premises + assert "~aquatic__cat" in gp.premises + + +def test_unary_universal_rule_expands_over_all_entities() -> None: + case = { + "entities": ["cat", "dog", "fish"], + "facts": [], + "rules": [{"if": [{"predicate": "furry", "var": "x", "polarity": True}], + "then": {"predicate": "mammal", "var": "x", "polarity": True}}], + "query": {"predicate": "mammal", "entity": "cat", "polarity": True}, + } + gp = lower_case(case) + grounded = [p for p in gp.premises if "->" in p] + assert len(grounded) == 3 # one per entity + assert any("furry__cat" in p and "mammal__cat" in p for p in grounded) + assert any("furry__dog" in p and "mammal__dog" in p for p in grounded) + assert any("furry__fish" in p and "mammal__fish" in p for p in grounded) + + +def test_conjunctive_rule_body_lowers_to_conjunction() -> None: + case = { + "entities": ["t"], + "facts": [], + "rules": [{"if": [{"predicate": "red", "var": "x", "polarity": True}, + {"predicate": "round", "var": "x", "polarity": True}], + "then": {"predicate": "apple", "var": "x", "polarity": True}}], + "query": {"predicate": "apple", "entity": "t", "polarity": True}, + } + gp = lower_case(case) + rule = next(p for p in gp.premises if "->" in p) + assert "red__t" in rule and "round__t" in rule and "&" in rule and "apple__t" in rule + + +# --- refusal boundary (typed reasons) ---------------------------------------- + + +def test_unknown_entity_query_refuses() -> None: + case = {"entities": ["cat"], "facts": [], + "query": {"predicate": "furry", "entity": "mouse", "polarity": True}} + with pytest.raises(GroundingError) as exc: + lower_case(case) + assert exc.value.reason == UNKNOWN_ENTITY + + +def test_unknown_entity_in_fact_refuses() -> None: + case = {"entities": ["cat"], + "facts": [{"predicate": "furry", "entity": "mouse", "polarity": True}], + "query": {"predicate": "furry", "entity": "cat", "polarity": True}} + with pytest.raises(GroundingError) as exc: + lower_case(case) + assert exc.value.reason == UNKNOWN_ENTITY + + +def test_binary_relation_refuses_as_unsupported_arity() -> None: + # a relation carries a second argument key -> not unary -> refuse + case = {"entities": ["a", "b"], + "facts": [{"predicate": "loves", "entity": "a", "object": "b", "polarity": True}], + "query": {"predicate": "loves", "entity": "a", "polarity": True}} + with pytest.raises(GroundingError) as exc: + lower_case(case) + assert exc.value.reason == UNSUPPORTED_PREDICATE_ARITY + + +def test_multi_variable_rule_refuses() -> None: + case = {"entities": ["a"], + "rules": [{"if": [{"predicate": "p", "var": "x", "polarity": True}], + "then": {"predicate": "q", "var": "y", "polarity": True}}], + "query": {"predicate": "p", "entity": "a", "polarity": True}} + with pytest.raises(GroundingError) as exc: + lower_case(case) + assert exc.value.reason == UNSUPPORTED_QUANTIFIER + + +def test_empty_case_refuses() -> None: + with pytest.raises(GroundingError) as exc: + lower_case({}) + assert exc.value.reason in {"empty_case", MALFORMED_CASE} + + +# --- determinism + the lane gate (engine == oracle == committed gold) -------- + + +def test_lowering_is_deterministic_across_replay() -> None: + case = _load_fixture()[0] + a = lower_case(case) + b = lower_case(case) + assert a == b + + +@pytest.mark.parametrize("case", _load_fixture(), ids=lambda c: c["id"]) +def test_committed_gold_is_engine_and_independent_oracle_agreement(case: dict) -> None: + """The lane gate: every committed finite-entity case is decided identically by + the ROBDD engine AND the independent oracle, both equal to the committed gold.""" + gp = lower_case(case) + engine = evaluate_entailment(gp.premises, gp.query).outcome.value + oracle = oracle_entailment(gp.premises, gp.query) + assert oracle == case["gold"], f"{case['id']}: independent oracle != committed gold" + assert engine == case["gold"], f"{case['id']}: engine confabulated vs gold (wrong=0 breach)" + + +def test_fixture_has_nontrivial_signal() -> None: + """Guard against a vacuous fixture: it must carry entailed/refuted cases, not + only unknown/refused, or the lane proves nothing.""" + golds = {c["gold"] for c in _load_fixture()} + assert "entailed" in golds and "refuted" in golds