From e8ad11f9e6855cefd996890e3f9b1538c6f49f34 Mon Sep 17 00:00:00 2001 From: Shay Date: Mon, 15 Jun 2026 10:22:47 -0700 Subject: [PATCH] test(invariants): INV-30 open-world DETERMINE never asserts False; document typed learning boundary (#770) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the one missing mechanical firewall in the learning-boundary set: the open-world determination gear (generate/determine/determine.py) may construct only Determined(answer=True) or refuse (Undetermined) — it can never assert answer=False. Absence never refutes (open-world); a False from absence would be an unsound, wrong=0-class assertion. The planned DEEPEN/Step-2b closed-world entailed-negation capability (ProofWriter-CWA / FOLIO two-sided labels) must use a distinct closed-world result type and entry point, so this invariant keeps it lane-scoped by construction rather than by reviewer vigilance. INV-30 follows the existing suite's Schema-Defined-Proof-Obligation discipline: - test_no_determined_asserts_false — the firewall (project-wide AST scan) - test_detector_is_non_vacuous — proves it FAILS on injected answer=False - test_detector_ignores_true_and_reads — proves no false positives - test_determine_construction_sites_are_visible — proves the scan is not blind Doctrine: CLAUDE.md Teaching Safety + docs/runtime_contracts.md now state the corrected typed-learning boundary (durable=reviewed/proof-carrying; provisional=autonomous iff typed/isolated/replayable/non-masquerading) and cite the enforcing invariants INV-21/22/23/24/29/30, including the honest wrinkle that ADR-0148 promote_eligible_entries is a second, opt-in, default-off COHERENT path. No source code changed; firewall is additive. Full architectural invariant suite: 65/65 green. --- CLAUDE.md | 47 +++++++ docs/runtime_contracts.md | 23 ++++ tests/test_architectural_invariants.py | 164 +++++++++++++++++++++++++ 3 files changed, 234 insertions(+) diff --git a/CLAUDE.md b/CLAUDE.md index bd2ddbb3..97529fe3 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -231,6 +231,53 @@ Learning must be reviewed and auditable. Do not create a parallel correction/learning path. +### The learning boundary is typed, not "everything is proposal-only" + +A common misreading treats *all* learning as proposal-only. That is a false +bottleneck. The real boundary is between **durable** standing and +**provisional** standing, and it is already mechanically enforced — the rule +below names what each invariant guarantees, it does not loosen any of them. + +- **Durable mutation stays reviewed or proof-carrying.** Corpus / pack / + policy / identity changes, and any promotion to COHERENT/verified standing, + go through the reviewed teaching loop (`teaching/*`, proposal-only) or the + proof-carrying promotion gate (ADR-0218 `apply_certified_promotion`, which + re-verifies the entailment from a curator-certified coherent base before the + flip). +- **Provisional state may update autonomously — iff typed, isolated, + replayable, and unable to masquerade as ratified truth.** This covers + session memory, sealed practice ledgers, SPECULATIVE idle consolidation of + soundly-derived facts, reliability-ledger counts, proposal emission, and + disclosed licensed estimates. Each is written SPECULATIVE (never COHERENT), + through the same `VaultStore.store` path (no parallel memory), deterministically + (no clock, no LLM, no sampling), and carries its standing honestly + (`basis="as_told"`, `[approximate]`, "proposal", …). + +This boundary is a set of failing-when-violated invariants, not a convention: + +- **INV-21** — only allowlisted modules may call `VaultStore.store(...)`. +- **INV-22 / INV-23** — an unmarked pack row and an unmarked `store()` default + to SPECULATIVE; COHERENT requires an explicit stamp. +- **INV-24** — every `vault.recall` callsite is categorized; user-facing + evidence must pass `min_status=COHERENT`. +- **INV-29** — only `vault/store.py` may transition an `epistemic_status`; the + only *default-reachable* COHERENT producer is the certificate-gated + `apply_certified_promotion`. (Honest wrinkle: ADR-0148 + `promote_eligible_entries` is a second, non-certificate COHERENT path, but it + is opt-in — it fires only when a caller passes a promotion policy — and is + off by default.) +- **INV-30** — the open-world `determine()` gear constructs only + `Determined(answer=True)` or refuses; it can never assert `answer=False`. + Closed-world entailed-negation (assert-False) must use a distinct + closed-world type and entry point, never the open-world path. + +When you add an autonomous learning surface, it must land inside this boundary +(SPECULATIVE, same store path, replayable) and the relevant invariant above must +*fail loudly* if it does not. An autonomous path that can reach COHERENT, emit +verified without a replayed certificate, persist non-replayably, or assert a +closed-world False into the open-world runtime is a boundary breach, not a +feature. + ## Semantic Pack Discipline Prefer compact, curated packs. Do not bulk-ingest corpora into runtime. diff --git a/docs/runtime_contracts.md b/docs/runtime_contracts.md index 3e8b311d..aea4bf8f 100644 --- a/docs/runtime_contracts.md +++ b/docs/runtime_contracts.md @@ -374,6 +374,29 @@ not directly rewrite language packs, frames, identity axes, or operator code. Identity manifold mutation by user prompt or correction is forbidden. +### Provisional vs durable standing (the typed learning boundary) + +The boundary is between **durable** and **provisional** standing, not between +"reviewed" and "everything else". Provisional state — session memory, idle +SPECULATIVE consolidation, sealed practice ledgers, reliability counts, emitted +proposals, disclosed licensed estimates — may update autonomously *iff* it is +typed (carries its standing), isolated (same `VaultStore.store` path, no +parallel memory), replayable (no clock, no LLM, no sampling), and cannot +masquerade as ratified truth (written SPECULATIVE; rendered `as_told` / +`[approximate]` / "proposal"). Durable standing — corpus/pack/policy/identity +mutation, and any promotion to COHERENT/verified — stays reviewed +(`teaching/*`, proposal-only) or proof-carrying (ADR-0218 +`apply_certified_promotion`, re-verified from a curator-certified coherent +base). + +This is enforced by failing-when-violated invariants, not convention: INV-21 +(vault-writer allowlist), INV-22/INV-23 (default SPECULATIVE), INV-24 (recall +categorization; user-facing evidence is COHERENT-only), INV-29 (only +`vault/store.py` transitions `epistemic_status`; the certificate gate is the +only default-reachable COHERENT producer), and INV-30 (the open-world +`determine()` gear asserts only `answer=True` or refuses — never `False`; +closed-world entailed-negation must be a distinct, lane-scoped type). + ## Environmental falsification contract (ADR-0211) `sensorium.environment.falsification` compares expected afferent evidence with diff --git a/tests/test_architectural_invariants.py b/tests/test_architectural_invariants.py index 208feb6b..e43a05ec 100644 --- a/tests/test_architectural_invariants.py +++ b/tests/test_architectural_invariants.py @@ -1993,3 +1993,167 @@ class TestINV29EpistemicStatusTransitionSites: "the ADR-0218 apply_certified_promotion site in " "vault/store.py to be visible to the INV-29 scan." ) + + +# =========================================================================== +# INV-30 Open-world DETERMINE never asserts False +# =========================================================================== +# +# Claim (generate/determine/determine.py §"wrong=0 / soundness (open-world)"; +# ADR-0206; mastery-v2 reviewer Amendment 3): +# The open-world determination gear answers a question ONLY from what the held +# self has realized, under the OPEN-WORLD assumption — absence never refutes. +# It asserts only `answer=True` (a direct or sound-transitive POSITIVE +# entailment) or refuses (`Undetermined`). It must NEVER construct a +# `Determined` with `answer=False`: a False from absence would be an +# unsound, wrong=0-class assertion (closed-world falsehood imported into an +# open-world path, where "not stored" ≠ "false"). +# +# This matters because the next planned capability (DEEPEN / Step 2b) adds +# CLOSED-WORLD entailed-negation — `answer=False` for ProofWriter-CWA and +# FOLIO two-sided labels. That capability is sound ONLY inside an explicit +# closed-world / proof-backed context. It must therefore use a DISTINCT +# closed-world result type and a DISTINCT entry point — never the open-world +# `Determined` constructed here — so closed-world falsehood cannot leak into +# the runtime session-memory determination path. This invariant is that +# firewall: it is mechanically impossible to emit `Determined(answer=False)` +# from anywhere, so a closed-world assert-False has to be lane-scoped by +# construction rather than by reviewer vigilance. +# +# `Determined` is a single named type (generate/determine/determine.py); the +# disclosed-estimate path uses the separately-named `ConverseEstimate`, so a +# project-wide scan for `Determined(answer=...)` is exact and unambiguous. + + +def _determined_constructions(tree: ast.AST) -> list[tuple[int, bool]]: + """Every ``Determined(...)`` construction in ``tree``, paired with whether + its ``answer`` is the constant ``True``. + + ``answer`` is read from the ``answer=`` keyword or, failing that, the first + positional argument (the dataclass field order is + ``answer, basis, predicate, subject, object, grounds``). A non-``True`` + constant, a computed expression, or a missing answer all count as + "not provably True" — i.e. a potential closed-world False. + + Uses AST so comments/docstrings/strings cannot trigger false positives. + """ + out: list[tuple[int, bool]] = [] + for node in ast.walk(tree): + if not isinstance(node, ast.Call): + continue + func = node.func + name = ( + func.id if isinstance(func, ast.Name) + else func.attr if isinstance(func, ast.Attribute) + else "" + ) + if name != "Determined": + continue + answer: ast.expr | None = None + for kw in node.keywords: + if kw.arg == "answer": + answer = kw.value + break + if answer is None and node.args: + answer = node.args[0] + is_true = isinstance(answer, ast.Constant) and answer.value is True + out.append((node.lineno, is_true)) + return out + + +def _determined_false_construction_sites(path: Path) -> list[int]: + try: + tree = ast.parse(path.read_text()) + except (OSError, SyntaxError): + return [] + return [ln for ln, ok in _determined_constructions(tree) if not ok] + + +class TestINV30OpenWorldDetermineNeverAssertsFalse: + """ + Claim: no production module may construct a `Determined` whose `answer` is + not the constant `True`. The open-world gear asserts only positive direct + or sound-transitive entailment, or refuses. A closed-world assert-False + capability must use a distinct result type and entry point, never this one. + """ + + def test_no_determined_asserts_false(self): + offenders: list[str] = [] + for path in _enumerate_project_py_files(): + for ln in _determined_false_construction_sites(path): + rel = str(path.relative_to(PROJECT_ROOT_FOR_INV21)) + offenders.append(f"{rel}:{ln}") + assert not offenders, ( + "Open-world DETERMINE constructed `Determined(answer=...)` with a " + "non-`True` answer at:\n " + "\n ".join(offenders) + + "\n\nThe open-world gear may assert only `answer=True` or refuse " + "(`Undetermined`); absence never refutes (open-world). If you are " + "adding a CLOSED-WORLD entailed-negation capability (ProofWriter-" + "CWA / FOLIO two-sided labels), route assert-False through a " + "DISTINCT closed-world result type and entry point — not the " + "open-world `Determined` — so closed-world falsehood cannot reach " + "the runtime session-memory determination path (determine.py " + "§soundness; mastery-v2 reviewer Amendment 3)." + ) + + def test_detector_is_non_vacuous(self): + """30b — prove 30a can fail: the predicate flags every `answer`-not-True + construction shape (False constant, computed expr, positional False, + unary negation), whether keyword or positional.""" + flagged = ( + "Determined(answer=False, basis='b', predicate='p', subject='s', object='o', grounds=())", + "Determined(answer=flag, basis='b', predicate='p', subject='s', object='o', grounds=())", + "Determined(False, 'b', 'p', 's', 'o', ())", + "Determined(answer=not hit, basis='b', predicate='p', subject='s', object='o', grounds=())", + ) + missed = [ + s for s in flagged + if not [ln for ln, ok in _determined_constructions(ast.parse(s)) if not ok] + ] + assert not missed, ( + "INV-30 predicate failed to flag a non-True `Determined` answer " + "shape:\n " + "\n ".join(missed) + + "\n— the assert-False firewall has gone partially blind." + ) + + def test_detector_ignores_true_and_reads(self): + """30b' — no false positives: `answer=True` (keyword or positional) and + reads of `.answer` stay clean, so the firewall does not train people to + route around it.""" + clean = ( + "Determined(answer=True, basis='b', predicate='p', subject='s', object='o', grounds=())", + "Determined(True, 'b', 'p', 's', 'o', ())", + "x = d.answer", + "if result.answer:\n pass", + ) + noisy = [ + s for s in clean + if [ln for ln, ok in _determined_constructions(ast.parse(s)) if not ok] + ] + assert not noisy, ( + "INV-30 predicate flagged an `answer=True` construction or a read " + "of `.answer`:\n " + "\n ".join(noisy) + + "\n— false positives would train people to allowlist reflexively." + ) + + def test_determine_construction_sites_are_visible(self): + """30c — the scan actually sees the open-world gear's two `Determined` + sites (direct entailment + transitive subsumption), and both assert + True. If the count drops the scan went blind, not clean; if `ok` drops + the firewall was breached at its own source.""" + determine_path = ( + PROJECT_ROOT_FOR_INV21 / "generate" / "determine" / "determine.py" + ) + constructions = _determined_constructions( + ast.parse(determine_path.read_text()) + ) + assert len(constructions) == 2, ( + "Expected exactly the two open-world `Determined(answer=True)` " + f"construction sites in determine.py; saw {len(constructions)}. " + "If the gear legitimately changed shape, update this count — but " + "confirm every site still asserts only `answer=True`." + ) + assert all(ok for _, ok in constructions), ( + "A `Determined` site in determine.py no longer asserts the constant " + "`True` — the open-world soundness firewall was breached at source." + )