feat(eval): ProofWriter-OWA refusal-floor lane (B1) — independent oracle, measure-only (#779)

* feat(eval): ProofWriter-OWA refusal-floor lane (B1) — independent oracle, measure-only

Mastery-v2 Step-3 Brief 1. Proves the open-world soundness floor: determine() never
asserts a query True when the open-world truth is Unknown or False. Hardens
"unknown != false" before the transitive-chain (B2) and closed-world (B4) work can
stress it.

- evals/proofwriter_owa/oracle.py: a SEPARATE minimal OWA label oracle (its own parser
  + reasoner + inverse/symmetric tables), importing NONE of determine, comprehend/
  MeaningGraph realization, or production predicate-entailment helpers (INV-25/27 — the
  gold producer is disjoint from the solver). Grammar: member/subset/is-a closure,
  explicit negation (No X is a Y -> disjointness, the source of gold-False), and #775
  inverse/symmetric ONE-HOP relational rules. No transitive relational chains.
- evals/proofwriter_owa/fixtures.jsonl: 19 hand-authored ProofWriter-OWA-style items
  (9 True / 7 Unknown / 3 False), SHA-pinned. Gold computed by the oracle; the fixture's
  hand-authored `expected` pins the oracle (so the oracle is itself verified).
- evals/proofwriter_owa/score.py: runs the production path (comprehend/comprehend_relational
  -> realize -> determine) vs the oracle gold; wrong = determine asserted True on a non-True
  gold.
- tests/test_proofwriter_owa_lane.py: SHA pin; oracle==expected; wrong==0; every
  serving_support gold-True determines True (no coverage gaps); no answer=False (INV-30).

Result: 19 items -> 9 correct (all serving_support True), 10 refused (Unknown/False),
0 wrong. Measure-only: no engine code touched; deliberately NOT a capability-index domain
(a refusal floor has low coverage and would drag coverage_geomean). INV-30 green; smoke 99/99.

Note: no live ProofWriter dataset access in this environment, so items are hand-authored
in OWA style (provenance.md cites ProofWriter V2020.12.3 / arXiv:2012.13048 for semantics,
attribution only) — but the GOLD is oracle-computed and verified, not hand-asserted.

* harden(eval): OWA lane CLI fails on coverage_gaps too (review #779)

score.py::main() exited nonzero only on wrong>0; it now ALSO exits nonzero when
coverage_gaps is non-empty (serving-supported gold-True items that refused), matching
the acceptance rule the tests already enforce and the module docstring. Both failure
modes print to stderr; exit is 1 if either fires. Verified non-vacuously (injected gap
-> exit 1). Lane test 5/5 green.

evals/proofwriter_owa/fixtures.jsonl

@@ -0,0 +1,19 @@
+{"id": "owa-001", "facts": ["Rex is a dog.", "All dogs are mammals."], "query": "Is Rex a mammal?", "expected": "True", "serving_support": true, "note": "member then subset (member o subset)"}
+{"id": "owa-002", "facts": ["Rex is a dog.", "All dogs are mammals.", "All mammals are animals."], "query": "Is Rex an animal?", "expected": "True", "serving_support": true, "note": "member o subset o subset"}
+{"id": "owa-003", "facts": ["All dogs are mammals."], "query": "Are all dogs mammals?", "expected": "True", "serving_support": true, "note": "direct subset"}
+{"id": "owa-004", "facts": ["All dogs are mammals.", "All mammals are animals."], "query": "Are all dogs animals?", "expected": "True", "serving_support": true, "note": "subset o subset"}
+{"id": "owa-005", "facts": ["Truth is a concept."], "query": "Is truth a concept?", "expected": "True", "serving_support": true, "note": "direct member"}
+{"id": "owa-006", "facts": ["Alice is the parent of Bob."], "query": "Is Alice the parent of Bob?", "expected": "True", "serving_support": true, "note": "relational direct"}
+{"id": "owa-007", "facts": ["Bob is the child of Alice."], "query": "Is Alice the parent of Bob?", "expected": "True", "serving_support": true, "note": "relational inverse one-hop (#775)"}
+{"id": "owa-008", "facts": ["Alice is the sibling of Bob."], "query": "Is Bob the sibling of Alice?", "expected": "True", "serving_support": true, "note": "relational symmetric one-hop (#775)"}
+{"id": "owa-009", "facts": ["Bob is less than Alice."], "query": "Is Alice greater than Bob?", "expected": "True", "serving_support": true, "note": "relational inverse order one-hop (#775)"}
+{"id": "owa-010", "facts": ["All dogs are mammals."], "query": "Are all mammals dogs?", "expected": "Unknown", "serving_support": false, "note": "reverse subset is not entailed"}
+{"id": "owa-011", "facts": ["Rex is a dog.", "All cats are mammals."], "query": "Is Rex a mammal?", "expected": "Unknown", "serving_support": false, "note": "no chain: dog has no superclass given"}
+{"id": "owa-012", "facts": ["Alice is the sibling of Bob."], "query": "Is Alice the parent of Bob?", "expected": "Unknown", "serving_support": false, "note": "cross-predicate: sibling does not imply parent"}
+{"id": "owa-013", "facts": ["Alice is less than Bob."], "query": "Is Bob less than Alice?", "expected": "Unknown", "serving_support": false, "note": "asymmetric: a<b does not give b<a"}
+{"id": "owa-014", "facts": [], "query": "Is Alice the sibling of Bob?", "expected": "Unknown", "serving_support": false, "note": "ungrounded: no told fact"}
+{"id": "owa-015", "facts": ["Rex is a dog."], "query": "Is Spot a dog?", "expected": "Unknown", "serving_support": false, "note": "unrelated subject: Spot ungrounded"}
+{"id": "owa-016", "facts": ["Socrates is a man.", "Man is a species."], "query": "Is Socrates a species?", "expected": "Unknown", "serving_support": false, "note": "member o member fallacy: instance-of is not transitive"}
+{"id": "owa-017", "facts": ["Felix is a cat.", "All cats are mammals.", "No mammal is a reptile."], "query": "Is Felix a reptile?", "expected": "False", "serving_support": false, "note": "negation entailed via subset + disjointness"}
+{"id": "owa-018", "facts": ["Tweety is a bird.", "No bird is a mammal."], "query": "Is Tweety a mammal?", "expected": "False", "serving_support": false, "note": "negation entailed: direct disjoint membership"}
+{"id": "owa-019", "facts": ["All sparrows are birds.", "No bird is a mammal."], "query": "Are all sparrows mammals?", "expected": "False", "serving_support": false, "note": "negation entailed: subset into a disjoint class"}

evals/proofwriter_owa/oracle.py

@@ -0,0 +1,159 @@
+"""Independent OWA label oracle for the ProofWriter-OWA refusal-floor lane (B1).
+
+This computes the open-world-assumption gold label (`True` / `Unknown` / `False`) for
+each fixture item, DISJOINTLY from the engine: it does NOT import `determine`,
+`comprehend`/MeaningGraph realization, or any production predicate-entailment helper
+(INV-25 / INV-27). It has its own tiny parser for the closed B1 fixture grammar and its
+own minimal relational algebra. The fixture's hand-authored `expected` field is pinned
+equal to this oracle's output by the lane test, so the oracle is itself verified.
+
+Grammar (closed — anything else raises):
+    facts:  "<X> is a[n] <Y>."                 -> member(x, y)
+            "All <Xs> are <Ys>."               -> subset(x, y)        (regular plurals)
+            "No <X> is a[n] <Y>."              -> disjoint(x, y)
+            "<A> is [the] <connective> <B>."   -> rel(lemma, a, b)
+    query:  "Is <X> a[n] <Y>?"                  -> member?(x, y)
+            "Are all <Xs> <Ys>?"               -> subset?(x, y)
+            "Is <A> [the] <connective> <B>?"   -> rel?(lemma, a, b)
+
+OWA semantics:
+    member?(x, y): True if y is in the is-a closure of x's classes; False if some class
+        in that closure is declared disjoint from y; else Unknown.
+    subset?(x, y): True if y is in x's superclass closure; False if some class in that
+        closure is disjoint from y; else Unknown.
+    rel?(lemma, a, b): True on a direct edge, a declared INVERSE edge (b,a), or a declared
+        SYMMETRIC edge (b,a) — ONE hop only. Else Unknown. (No transitive relational
+        chains in B1; no relational negation in this grammar.)
+"""
+
+from __future__ import annotations
+
+import re
+
+# The oracle's OWN relational ontology — declared here, NOT imported from
+# generate.meaning_graph.relational, so the gold producer stays disjoint from the
+# solver. (It mirrors the pack's algebra for the predicates this fixture uses.)
+_INVERSE: dict[str, str] = {
+    "less_than": "greater_than", "greater_than": "less_than",
+    "parent_of": "child_of", "child_of": "parent_of",
+    "left_of": "right_of", "right_of": "left_of",
+    "before_event": "after_event", "after_event": "before_event",
+}
+_SYMMETRIC: frozenset[str] = frozenset({
+    "sibling_of", "spouse_of", "equal_to", "distinct_from", "adjacent_to",
+})
+_CONNECTIVE: dict[str, str] = {
+    "parent of": "parent_of", "child of": "child_of", "sibling of": "sibling_of",
+    "spouse of": "spouse_of", "less than": "less_than", "greater than": "greater_than",
+    "equal to": "equal_to", "distinct from": "distinct_from",
+    "left of": "left_of", "right of": "right_of", "inside of": "inside_of",
+    "adjacent to": "adjacent_to",
+}
+# longest connective first so "parent of" wins before any single-token prefix
+_CONN_ALT = "|".join(re.escape(k) for k in sorted(_CONNECTIVE, key=len, reverse=True))
+
+_MEMBER = re.compile(r"^(\w+) is an? (\w+)\.$")
+_SUBSET = re.compile(r"^All (\w+) are (\w+)\.$")
+_DISJOINT = re.compile(r"^No (\w+) is an? (\w+)\.$")
+_REL = re.compile(rf"^(\w+) is (?:the )?({_CONN_ALT}) (\w+)\.$")
+
+_Q_MEMBER = re.compile(r"^Is (\w+) an? (\w+)\?$")
+_Q_SUBSET = re.compile(r"^Are all (\w+) (\w+)\?$")
+_Q_REL = re.compile(rf"^Is (\w+) (?:the )?({_CONN_ALT}) (\w+)\?$")
+
+
+class OracleParseError(ValueError):
+    """A fixture string is outside the closed B1 grammar — fail loudly, never guess."""
+
+
+def _sing(word: str) -> str:
+    """Singularize a regular plural class noun ('dogs' -> 'dog'). Used ONLY in the
+    explicitly-plural slots of the subset patterns, so 'species'/'Socrates' (which only
+    appear in singular `is a` slots) are never mangled."""
+    w = word.lower()
+    return w[:-1] if w.endswith("s") and not w.endswith("ss") else w
+
+
+def parse_fact(text: str) -> tuple:
+    t = text.strip()
+    if (m := _DISJOINT.match(t)):
+        return ("disjoint", m.group(1).lower(), m.group(2).lower())
+    if (m := _SUBSET.match(t)):
+        return ("subset", _sing(m.group(1)), _sing(m.group(2)))
+    if (m := _REL.match(t)):
+        return ("rel", _CONNECTIVE[m.group(2)], m.group(1).lower(), m.group(3).lower())
+    if (m := _MEMBER.match(t)):
+        return ("member", m.group(1).lower(), m.group(2).lower())
+    raise OracleParseError(f"unparseable fact: {text!r}")
+
+
+def parse_query(text: str) -> tuple:
+    t = text.strip()
+    if (m := _Q_REL.match(t)):
+        return ("rel?", _CONNECTIVE[m.group(2)], m.group(1).lower(), m.group(3).lower())
+    if (m := _Q_SUBSET.match(t)):
+        return ("subset?", _sing(m.group(1)), _sing(m.group(2)))
+    if (m := _Q_MEMBER.match(t)):
+        return ("member?", m.group(1).lower(), m.group(2).lower())
+    raise OracleParseError(f"unparseable query: {text!r}")
+
+
+def _closure(start: str, supers: dict[str, set[str]]) -> set[str]:
+    """`start` plus every superclass reachable over subset edges (BFS, deterministic)."""
+    seen = {start}
+    stack = [start]
+    while stack:
+        node = stack.pop()
+        for sup in sorted(supers.get(node, ())):
+            if sup not in seen:
+                seen.add(sup)
+                stack.append(sup)
+    return seen
+
+
+def label(facts: list[str], query: str) -> str:
+    """The OWA gold label for `query` given `facts`: 'True' | 'Unknown' | 'False'."""
+    members: dict[str, set[str]] = {}
+    supers: dict[str, set[str]] = {}
+    disjoint: set[frozenset[str]] = set()
+    rels: set[tuple[str, str, str]] = set()
+    for text in facts:
+        f = parse_fact(text)
+        if f[0] == "member":
+            members.setdefault(f[1], set()).add(f[2])
+        elif f[0] == "subset":
+            supers.setdefault(f[1], set()).add(f[2])
+        elif f[0] == "disjoint":
+            disjoint.add(frozenset((f[1], f[2])))
+        else:  # rel
+            rels.add((f[1], f[2], f[3]))
+
+    q = parse_query(query)
+    if q[0] == "member?":
+        _, subj, cls = q
+        reach: set[str] = set()
+        for c0 in members.get(subj, ()):
+            reach |= _closure(c0, supers)
+        if cls in reach:
+            return "True"
+        if any(frozenset((d, cls)) in disjoint for d in reach):
+            return "False"
+        return "Unknown"
+    if q[0] == "subset?":
+        _, x, y = q
+        clo = _closure(x, supers)
+        if y in clo:
+            return "True"
+        if any(frozenset((d, y)) in disjoint for d in clo):
+            return "False"
+        return "Unknown"
+    # rel?
+    _, lemma, a, b = q
+    if (lemma, a, b) in rels:
+        return "True"
+    inv = _INVERSE.get(lemma)
+    if inv is not None and (inv, b, a) in rels:
+        return "True"
+    if lemma in _SYMMETRIC and (lemma, b, a) in rels:
+        return "True"
+    return "Unknown"

evals/proofwriter_owa/provenance.md

@@ -0,0 +1,46 @@
+# evals/proofwriter_owa — provenance (B1: OWA refusal floor)
+
+The ProofWriter-OWA refusal-floor lane (mastery-v2 Step 3, Brief 1). It proves the
+open-world soundness floor: the engine's `determine()` never asserts a query `True` when
+the open-world truth is `Unknown` or `False`. It hardens "unknown ≠ false" before the
+transitive-chain (B2) and closed-world (B4) work can stress it.
+
+## Independent gold (oracle), not a dataset slice
+
+This environment has no live ProofWriter dataset access, so the items are **hand-authored
+in ProofWriter-OWA style** — small is-a / relational theories + one yes/no query — rather
+than verbatim dataset rows. Critically, the gold label is **not** hand-asserted: it is
+computed by a **separate minimal oracle** (`oracle.py`) with its own parser and its own
+OWA reasoner, importing **none** of `determine`, `comprehend` / MeaningGraph realization,
+or the production predicate-entailment helpers (INV-25 / INV-27 — the gold producer is
+disjoint from the solver). The fixture's hand-authored `expected` field pins the oracle's
+output, so the oracle is itself verified (`test_oracle_matches_authored_expected`).
+
+Source / semantics reference: AllenAI **ProofWriter** (V2020.12.3, arXiv:2012.13048) — the
+open-world `{True, Unknown, False}` label semantics. Attribution only; no dataset
+redistribution.
+
+## What the lane checks
+
+- **`wrong == 0`** — `determine()` asserts `True` only on a gold-`True` item. A `True`
+  assertion on a gold `Unknown` OR `False` is a soundness breach. (`determine()` is sound,
+  so this is a hard floor; the lane makes any regression *findable* against the
+  independent oracle.)
+- gold-`True` items marked `serving_support` (member/subset subsumption, plus #775
+  inverse/symmetric one-hop) **must** determine `True` — no silent coverage loss.
+- no `answer=False` is ever constructed (INV-30 holds, behaviorally re-checked here).
+
+## Scope (oracle grammar)
+
+member / subset / is-a closure; explicit negation (`No X is a Y` → disjointness, the
+source of every gold-`False`); and #775 inverse/symmetric **one-hop** relational rules.
+**No transitive relational chains** — that is Brief 2; an "oracle-only gold side" hook is
+left for when it lands.
+
+This lane is **measure-only**: it touches no engine code and is deliberately **not a
+capability-index domain** (a refusal floor has low coverage and would drag the index's
+`coverage_geomean`). It runs as its own standalone wrong=0 gate.
+
+## Current result
+
+`19 items → 9 correct (all serving_support True), 10 refused (Unknown/False), 0 wrong`.

evals/proofwriter_owa/score.py

@@ -0,0 +1,117 @@
+"""Score the ProofWriter-OWA refusal floor: `determine()` vs the independent oracle.
+
+For each fixture item: compute the OWA gold with the disjoint `oracle.label(...)`, then run
+the production path (`comprehend`/`comprehend_relational` -> `realize` -> `determine`) and
+compare. The invariant is **wrong=0**: `determine()` may assert True only on a gold-`True`
+item; asserting True on a gold `Unknown` or `False` is a soundness breach (it would mean
+the engine claimed entailment where the open world does not entail it).
+
+Measure-only — imports no `generate.derivation` / `core.reliability_gate`; NOT a
+capability-index domain. A refusal on a gold-`True` item is a coverage miss (recorded),
+never a wrong — UNLESS the item is marked `serving_support` (within the engine's claimed
+support), in which case it must determine True.
+"""
+
+from __future__ import annotations
+
+import json
+import sys
+from pathlib import Path
+from typing import Any
+
+from chat.runtime import ChatRuntime
+from evals.proofwriter_owa.oracle import label as owa_label
+from generate.determine import Determined, determine
+from generate.meaning_graph.reader import Refusal, comprehend
+from generate.meaning_graph.relational import (
+    comprehend_relational,
+    load_relational_pack_lemmas,
+)
+from generate.realize import realize_comprehension
+from session.context import SessionContext
+
+_FIXTURES = Path(__file__).resolve().parent / "fixtures.jsonl"
+_HIGH = 10**9
+
+
+def _load(path: Path = _FIXTURES) -> list[dict[str, Any]]:
+    return [
+        json.loads(line)
+        for line in path.read_text(encoding="utf-8").splitlines()
+        if line.strip()
+    ]
+
+
+def _comprehend_any(text: str, pack):
+    """Relational reader first (specific), else the general comprehension reader."""
+    c = comprehend_relational(text, pack)
+    if isinstance(c, Refusal):
+        return comprehend(text)
+    return c
+
+
+def run(path: Path = _FIXTURES) -> dict[str, Any]:
+    items = _load(path)
+    pack = load_relational_pack_lemmas()
+    rt = ChatRuntime(no_load_state=True)
+    vocab, persona = rt._context.vocab, rt._context.persona
+
+    correct = refused = wrong = 0
+    wrongs: list[dict[str, Any]] = []
+    coverage_gaps: list[dict[str, Any]] = []  # serving_support gold-True that refused
+
+    for it in items:
+        gold = owa_label(it["facts"], it["query"])
+        ctx = SessionContext(
+            vocab=vocab, persona=persona, vault_reproject_interval=_HIGH
+        )
+        for fact in it["facts"]:
+            realize_comprehension(_comprehend_any(fact, pack), ctx)
+        res = determine(_comprehend_any(it["query"], pack), ctx)
+        asserted_true = isinstance(res, Determined) and res.answer is True
+
+        if asserted_true and gold == "True":
+            correct += 1
+        elif asserted_true:  # gold Unknown/False but engine asserted True -> BREACH
+            wrong += 1
+            wrongs.append({"id": it["id"], "gold": gold, "query": it["query"]})
+        else:
+            refused += 1
+            if it.get("serving_support") and gold == "True":
+                coverage_gaps.append({"id": it["id"], "query": it["query"]})
+
+    return {
+        "domain": "proofwriter_owa",
+        "total": len(items),
+        "correct": correct,
+        "refused": refused,
+        "wrong": wrong,
+        "wrongs": wrongs,
+        "coverage_gaps": coverage_gaps,
+        "counts": {"correct": correct, "wrong": wrong, "refused": refused},
+    }
+
+
+def main() -> int:
+    r = run()
+    print(json.dumps({k: v for k, v in r.items() if k != "wrongs"}, indent=2, sort_keys=True))
+    failed = False
+    if r["wrong"]:
+        print(
+            "WRONG > 0 — determine asserted True on a non-True OWA gold (soundness breach):",
+            file=sys.stderr,
+        )
+        print(json.dumps(r["wrongs"], indent=2), file=sys.stderr)
+        failed = True
+    if r["coverage_gaps"]:
+        print(
+            "COVERAGE GAPS — serving-supported gold-True items refused (acceptance breach):",
+            file=sys.stderr,
+        )
+        print(json.dumps(r["coverage_gaps"], indent=2), file=sys.stderr)
+        failed = True
+    return 1 if failed else 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

tests/test_proofwriter_owa_lane.py

@@ -0,0 +1,76 @@
+"""Lane test — ProofWriter-OWA refusal floor (B1, measure-only).
+
+The independent oracle computes the OWA gold; the production `determine()` path must never
+assert True on a non-`True` gold (wrong=0 — the soundness floor). The oracle is itself
+pinned to the fixture's hand-authored `expected`. This is NOT a capability-index domain.
+"""
+
+from __future__ import annotations
+
+import hashlib
+from pathlib import Path
+
+import pytest
+
+from chat.runtime import ChatRuntime
+from evals.proofwriter_owa.oracle import label as owa_label
+from evals.proofwriter_owa.score import _comprehend_any, _load, run
+from generate.determine import Determined, determine
+from generate.meaning_graph.relational import load_relational_pack_lemmas
+from generate.realize import realize_comprehension
+from session.context import SessionContext
+
+_FIXTURES = (
+    Path(__file__).resolve().parent.parent
+    / "evals"
+    / "proofwriter_owa"
+    / "fixtures.jsonl"
+)
+_FIXTURES_SHA = "7b340849a945d27306793a109fd65532803be40281b6da15809f9d33ea7f6580"
+_HIGH = 10**9
+
+
+def test_fixtures_sha_pinned() -> None:
+    got = hashlib.sha256(_FIXTURES.read_bytes()).hexdigest()
+    assert got == _FIXTURES_SHA, f"fixtures.jsonl drifted: {got}"
+
+
+def test_oracle_matches_authored_expected() -> None:
+    """Pin the independent oracle to the hand-authored intent — the oracle is verified,
+    so its gold can be trusted as the disjoint reference for `determine()`."""
+    for it in _load():
+        assert owa_label(it["facts"], it["query"]) == it["expected"], it["id"]
+
+
+@pytest.fixture(scope="module")
+def report():
+    return run()
+
+
+def test_refusal_floor_wrong_zero(report) -> None:
+    """THE floor: `determine()` never asserts True on a gold `Unknown`/`False`."""
+    assert report["wrong"] == 0, report["wrongs"]
+
+
+def test_serving_support_truths_are_determined(report) -> None:
+    """Every gold-`True` item inside the engine's claimed support determines True —
+    no silent coverage loss — and the lane actually exercises a positive path."""
+    assert report["coverage_gaps"] == [], report["coverage_gaps"]
+    assert report["correct"] > 0
+
+
+def test_no_answer_false_constructed() -> None:
+    """Behavioral echo of INV-30: across every item, `determine()` never yields
+    `answer=False` (the open-world gear is True-or-refuse)."""
+    pack = load_relational_pack_lemmas()
+    rt = ChatRuntime(no_load_state=True)
+    vocab, persona = rt._context.vocab, rt._context.persona
+    for it in _load():
+        ctx = SessionContext(
+            vocab=vocab, persona=persona, vault_reproject_interval=_HIGH
+        )
+        for fact in it["facts"]:
+            realize_comprehension(_comprehend_any(fact, pack), ctx)
+        res = determine(_comprehend_any(it["query"], pack), ctx)
+        if isinstance(res, Determined):
+            assert res.answer is True, it["id"]