test(invariants): INV-30 open-world DETERMINE never asserts False; document typed learning boundary (#770)

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.
This commit is contained in:
Shay 2026-06-15 10:22:47 -07:00 committed by GitHub
parent b3a1366980
commit e8ad11f9e6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 234 additions and 0 deletions

View file

@ -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.

View file

@ -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

View file

@ -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."
)