core-labs/core
1
0
Fork 0
Code Issues Pull requests 1 Projects Releases Packages Wiki Activity Actions

docs(adr): ratify ADR-0222 FrameVerdict closed-world design

Browse source 
Ratifies ADR-0222 as the design-only B4 artifact for FrameVerdict: a frame-general closed-world verdict type distinct from open-world Determined.

No runtime type, entry point, lane, or answer=False path is added in this PR. Implementation remains gated behind PR-1 with INV-31, the landed OWA refusal floor, and the staged plan in the ADR.

Final ratification patches included:
- positive_refutation_kind discriminator for entailed_false admissibility;
- PR-1-scoped Determined count wording;
- grounded-negative governance resolution as COMMIT-with-negative-surface at EpistemicState.INFERRED + DisclosureClaim.NONE.
This commit is contained in:
Shay 2026-06-15 13:09:35 -07:00 committed by GitHub
parent a6403edcd9
commit ea7b2d5cbd
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 690 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

690
docs/decisions/ADR-0222-frame-verdict-closed-world.md Normal file
View file

@ -0,0 +1,690 @@
# ADR-0222: FrameVerdict — Frame-General Closed-World Verdict
**Status:** Proposed (design-only). Implementation is gated behind two preconditions:
(a) the ProofWriter-OWA refusal floor has landed — **met** (`evals/proofwriter_owa/`,
PR #779) — and (b) ratification of *this* ADR. The design PR ships **only this
document**; no runtime type, no entry point, no lane, no `answer=False` path, and
no change to `generate/determine/determine.py` lands until the implementation
plan in §10 is authorized.
**Date:** 2026-06-15
**Domains:** `generate/frame_verdict/` (proposed, new), `generate/proof_chain/`,
`sensorium/environment/`, `core/response_governance/`, `core/epistemic_disclosure/`,
`evals/proofwriter_cwa/` (proposed, future)
**Depends on:** ADR-0211 (Conformal Falsification Bench — perceptual closed-frame
verdict), ADR-0206 (response governance / `ReachLevel` / `shape_surface`), ADR-0201/0202
(ROBDD canonicalizer), ADR-0203–0205 (`proof_chain` entailment), ADR-0175 (calibrated
learning / serving gate), ADR-0218 (proof-carrying promotion). Builds on INV-25/INV-27
(independent gold + transitive-import disjointness), INV-29 (status-transition allowlist),
INV-30 (open-world `determine` never asserts False), and the merged Step-3 brief pack
(#777, brief B4).
**Authors:** drafted by agent for architect review (Joshua Shay ratifies). This draft
incorporates an adversarial review pass (6 independent skeptics against real source);
the soundness corrections it produced are folded in and flagged inline as **[adv]**.
The architect approved the direction and resolved §14's two open questions; those
resolutions and the requested precision patches (explicit `positive_refutation_kind`
discriminator; PR-1-scoped `Determined`-count wording) are applied and flagged **[ratify]**.
---
## 1. Context
CORE's open-world determination gear is sound by a hard firewall: `determine()`
(`generate/determine/determine.py`) constructs only `Determined(answer=True)` or
returns `Undetermined(reason=…)`. **Absence of a fact never refutes it.** INV-30
(`tests/test_architectural_invariants.py`) mechanically enforces this: an AST scan
over the whole source tree fails the build if *any* `Determined(…)` construction
sets `answer` to anything but the literal `True` — there are exactly three sites,
all in `determine.py`, all `answer=True`, and `test_determine_construction_sites_are_visible`
pins the count. (The adversarial review ran the real `_determined_constructions`
predicate against the proposed type and confirmed it returns `[]` — see §11.)
This is correct for the open world. But three real capabilities need a sound
**closed-world "No"** — an *entailed negation*:
- **ProofWriter-CWA / FOLIO** two-sided labels (`{True, Unknown, False}`) where the
fact set is declared complete and `False` is a real answer, not a refusal.
- **Perceptual falsification** (ADR-0211): an `ExpectedObservationFrame` is a closed,
completely-enumerated expectation; an expected slot observed with a *contradicting
identity* refutes the conformance of the observation to the expectation.
- Future **audio / vision** frames, which converge on the same envelope.
INV-30's own error message names this gap verbatim: *"a closed-world assert-False
capability must use a distinct result type **and** entry point, never this one."*
The hazard this ADR guards is a `wrong=0`-class soundness breach: a closed-world
`False` leaking into the open-world runtime would assert `not Q` from what is really
just *absence of Q* — exactly the contamination INV-30 exists to prevent. The OWA
floor (#779) is the dual gate from the other side: it fails if the open-world engine
ever asserts `True` on a gold `Unknown`/`False`. FrameVerdict must be built **on top
of** both floors, never around them.
### 1.1 What already exists (the anti-reinvent inventory)
A frame-general closed-world verdict is **not a new solver**. Every soundness-bearing
decision it needs already exists and is sound-by-construction:
| Need | Existing producer | Verdict it emits |
|---|---|---|
| Propositional entailed-`False` | `generate/proof_chain/entail.py::evaluate_entailment_with_trace` | `Entailment.REFUTED` when `(⋀premises) → ¬query` is an ROBDD tautology, with an `EntailmentTrace` proof |
| Inconsistent premises (≠ False) | same, via `generate/logic_canonical.py::CanonicalProposition.is_contradiction` | `Entailment.REFUSED(INCONSISTENT_PREMISES)` — declines (*ex falso quodlibet*), never asserts |
| Out-of-regime (ungrounded ∀/predicate) | same | `Entailment.REFUSED(OUT_OF_REGIME_OR_MALFORMED)` |
| Perceptual frame conformance | `sensorium/environment/falsification.py::compare_expected_to_observation` | `verdict = "SUPPORTED" \| "FALSIFIED"` — a *set-comparison* of one actual frame to one expected frame, with a structural `FalsificationResidual{matched, missing, unexpected, changed}`. **[adv]** This refutes a hypothesis-scoped expectation by set-inequality; it is **not** itself a proof of `¬query` — only the `changed` sub-case is a positively-observed contradiction (see §5.2). |
| Independent text gold (3-way) | `evals/proofwriter_owa/oracle.py::label` (aliased `owa_label` in `score.py`) | `"True" \| "Unknown" \| "False"` — disjoint from the engine (INV-25/27) |
The genuinely missing pieces are narrow and three: **(1)** a single frame-general
*envelope* type with a lane-scoped entry point distinct from `determine()`; **(2)** the
explicit **closed-frame context** that licenses asserting the negation (no runtime
module builds one today for text); and **(3)** a **firewall** (proposed **INV-31**)
that fails loudly if a closed-world verdict reaches the open-world runtime. The `False`
*decision itself* is delegated to the producers above — it is never re-implemented here.
---
## 2. Decision
Introduce **`FrameVerdict`**: a single, frame-general, closed-world verdict type that
1. is a **distinct dataclass** (never `Determined`, no `answer: bool` field), so the
INV-30 call-name scan cannot fire on it and it cannot masquerade as an open-world
answer;
2. is produced **only** at a lane-scoped entry point that takes an explicit
**`ClosedFrame`**, never a `SessionContext` — structurally unable to read open-world
session memory;
3. asserts `entailed_false` **only from a positive proof of the negation** (an ROBDD
refutation, or a perceptual `changed`-slot contradiction), **never from absence** —
neither textual non-provability nor a missing/extra observation;
4. delegates every soundness decision to existing producers (§1.1) — it is a
convergent envelope, not a solver;
5. carries honest standing via the existing `_basis(grounds)` rule, never minting
COHERENT/verified, never writing `epistemic_status` (INV-29);
6. reaches a user surface **only** through the existing response-governance gate
(`govern_response` → `shape_surface`, `choose_served_disposition`), default-dark —
no parallel servability object;
7. is firewalled from the open-world runtime by **INV-31**, a *two-part* firewall
(transitive import containment **and** a typed data-flow guard) specified in §8 with
per-scan non-vacuity anchors.
The spine stays modality-neutral (cf. `project-spine-modality-neutral-convergence`):
text-CWA and perceptual falsification converge **at the front** via a `frame_kind`
discriminator — the same idiom as `RealizedRecord.structure_kind` — not via a spine
rewrite. The shared object is the **output envelope + governance path + replay digest**;
the **input signature differs by frame** (§6).
---
## 3. Type shape
> **Proposed — does not yet exist.** This lands in implementation **PR-1** *together
> with* INV-31, never after it. It is shown here as an illustrative fenced block, not
> an importable module, to keep this PR design-only.
```python
from dataclasses import dataclass
from enum import Enum, unique
@unique
class FrameKind(str, Enum):
TEXT = "text" # a declared-complete CWA fact set (ProofWriter-CWA, FOLIO)
PERCEPTION = "perception" # an ADR-0211 ExpectedObservationFrame vs an ObservationFrame
# AUDIO = "audio"; VISION = "vision" # reserved — they converge identically
@unique
class WorldAssumption(str, Enum):
OPEN = "open" # absence ⇒ undetermined; entailed_false is ILLEGAL here
CLOSED = "closed" # frame declared complete
BOUNDED_CLOSED = "bounded_closed" # complete only within a declared scope
@unique
class FrameVerdictKind(str, Enum):
ENTAILED_TRUE = "entailed_true" # the frame proves query
ENTAILED_FALSE = "entailed_false" # the frame proves ¬query (positive refutation)
UNDETERMINED = "undetermined" # neither query nor ¬query proven — within-frame refusal
CONTRADICTION = "contradiction" # the frame's own premises are inconsistent — NOT a False
SCOPE_BOUNDARY = "scope_boundary" # out of decidable regime / frame not licensed complete
@dataclass(frozen=True, slots=True)
class ClosedWorldProof:
"""Modality-blind, content-addressed proof envelope. Text and perception carry
the SAME shape; only `producer`, `outcome`, and the keys differ."""
producer: str # "proof_chain.entail" | "sensorium.falsification"
outcome: str # the producer's own literal: REFUTED/ENTAILED/UNKNOWN | FALSIFIED/SUPPORTED
proof_keys: tuple[str, ...] # entail: (conjunction_key, query_key, refutation_check_key)
# perception: (FalsificationRun.trace_hash,) -- the FULL run witness
proof_sha256: str # sha256_json over the canonical proof payload
positive_refutation_kind: str | None = None
# [adv/ratify] entailed_false ONLY: "robdd_refutation" (text) | "perception_changed_slot"
# (perception). None for EVERY non-entailed_false verdict. This is the explicit
# discriminator the ratifier required: a GENERIC FALSIFIED (missing / unexpected /
# whole-frame-missing — i.e. absence or over-observation) leaves this None and therefore
# CANNOT satisfy entailed_false's admissibility invariant (FrameVerdict.__post_init__).
# The perception adapter sets it to "perception_changed_slot" only when changed != ().
@dataclass(frozen=True, slots=True)
class FrameVerdict:
"""A closed-world verdict. DISTINCT from generate/determine/Determined:
no `answer: bool`, a 5-way `verdict` enum instead, a distinct name, and a
distinct entry point. INV-30's call-name scan cannot match it; it can never
be confused with an open-world answer."""
frame_id: str # content-addressed id of the explicit closed frame
frame_kind: FrameKind
world_assumption: WorldAssumption
query: str # the proposition under test (canonical key). NOTE [adv]: for
# perception this is the FRAME-CONFORMANCE proposition keyed by
# expected_id ("the observation conforms to this expected frame"),
# NOT an arbitrary asked proposition — see §5.2.
verdict: FrameVerdictKind # the two-sided result — NOT a bool, NOT named `answer`
basis: str # _basis(grounds): "as_told" | "verified" (never hardcoded)
proof: ClosedWorldProof # the replayable refutation/entailment/falsification evidence
evidence: tuple[str, ...] # content-addressed refs (grounds replay_hashes / _reject_unsafe_unit-
# screened merge_keys) — never raw payloads or efferent traces
trace_hash: str # sha256_json deterministic replay digest of the whole verdict
def __post_init__(self) -> None:
# [adv/ratify] Admissibility invariant — makes §12 obligation 2 non-vacuous: entailed_false
# may exist ONLY with a positive-refutation proof, and the proof must name WHICH positive
# refutation it is. A generic FALSIFIED (which ADR-0211 also emits for missing / unexpected /
# whole-frame-missing — i.e. absence) cannot satisfy this; only an ROBDD refutation or a
# perceptual changed-slot contradiction can. A mismatched (verdict, proof) pair fails loudly
# at construction, so a mutation test can trip it.
if self.verdict is FrameVerdictKind.ENTAILED_FALSE:
p = self.proof
ok = (
(p.producer == "proof_chain.entail"
and p.outcome == "REFUTED"
and p.positive_refutation_kind == "robdd_refutation")
or (p.producer == "sensorium.falsification"
and p.outcome == "FALSIFIED"
and p.positive_refutation_kind == "perception_changed_slot")
)
if not ok or not p.proof_sha256:
raise ValueError(
"entailed_false requires a positive-refutation proof: an ROBDD refutation "
"(robdd_refutation) or a perceptual changed-slot contradiction "
"(perception_changed_slot) — never a generic FALSIFIED"
)
```
Notes binding the shape to existing contracts:
- **No `answer` field, distinct name.** INV-30's predicate keys *only* on the literal
call name `Determined` and the `answer` argument. `FrameVerdict` matches neither;
a two-sided enum cannot be smuggled as `answer=True`.
- **`basis ∈ {as_told, verified}`**, computed by the **existing** `_basis(grounds)` rule
over the grounds' `epistemic_status`. Today every realized record is SPECULATIVE →
`as_told`. A proofless verdict can never claim `verified`. The proof-backing lives in
`proof`, *orthogonally* — so a sound refutation over `as_told` grounds is honestly
"I was *told* these facts; from them, ¬query is *proven*." **[adv]** `_basis` currently
lives inside `determine.py`; PR-1 lifts it to a shared `generate/epistemic_basis.py`
so neither package depends on the other's internals (§8).
- **No `epistemic_status` field.** Standing is read-only via `basis` + the grounds' own
stored status; `FrameVerdict` never *writes* an `epistemic_status` key, keeping INV-29's
`{vault/store.py}` allowlist untouched.
- **`proof` and `trace_hash` are content-addressed and replay-stable** (`sha256_json`,
order-invariant). **[adv]** For perception, `proof_keys` carries the **full
`FalsificationRun.trace_hash`** (which binds `expected_sha256 + actual_trace_hash +
verdict`), **not** `residual_sha256` alone — the residual hash does not bind the
expected/actual frame identities and two different `(expected, actual)` pairs can share
a residual delta. No clock, no RNG, no LLM, no probabilistic confidence, no tolerance.
- **`evidence` carries only content-addressed references** (grounds' `replay_hash`,
perception units' `merge_key` — all already `_reject_unsafe_unit`-screened), never raw
modality payloads or efferent traces, matching ADR-0211's discipline.
### 3.1 The closed-frame context
```python
@dataclass(frozen=True, slots=True)
class ClosedFrame:
"""The EXPLICIT closed-world context that licenses asserting a negation. The
entry point takes THIS, never a SessionContext — so it structurally cannot read
open-world session memory where absence ≠ false."""
frame_id: str
frame_kind: FrameKind
world_assumption: WorldAssumption # must be CLOSED or BOUNDED_CLOSED — OPEN ⇒ refuse
propositions: tuple[str, ...] # text: the COMPLETE enumerated fact set incl. declared
# negations/disjointness (content-addressed)
expected_frame_ref: str | None # perception: id of the ExpectedObservationFrame (ADR-0211)
frame_sha256: str
```
A `ClosedFrame` is **constructed explicitly by the lane / scenario**, never defaulted
from `SessionContext` or `VaultStore`. There is no "the session is closed" mode. If a
caller supplies `world_assumption == OPEN`, or omits the closure declaration, the entry
point returns `SCOPE_BOUNDARY` (refusal), never `entailed_false`. This is the dual of
INV-30: the open-world path lacks the completeness license and so may only assert True
or refuse; the closed-world path may assert False **only because it was handed an
explicit, declared-complete frame and a positive proof of the negation.**
---
## 4. Entry points
```text
OPEN WORLD (unchanged): determine(question, ctx: SessionContext) -> Determined | Undetermined
# asserts answer=True or refuses. NEVER FrameVerdict. NEVER answer=False.
CLOSED WORLD (new): evaluate_frame_verdict(frame: ClosedFrame, query: str) -> FrameVerdict
# lives in NEW top-level-isolated package generate/frame_verdict/.
# Takes a ClosedFrame, never a SessionContext. Returns FrameVerdict,
# never Determined. For perception, `query` is synthesized as the
# frame-conformance proposition keyed by expected_id (§5.2).
```
Hard rules (enforced by INV-31, §8):
- For **FrameVerdict PR-1**, `determine()` and `generate/determine/determine.py` are
**untouched**: the return union stays `Determined | Undetermined` and its current
`Determined(answer=True)` construction count is unchanged. **[ratify]** This is a PR-1
*scope* rule, **not** a permanent ban on the number: future open-world True-only
capabilities may add legitimate `Determined(answer=True)` sites **only if** INV-30 is
updated with a *visible* count change (`test_determine_construction_sites_are_visible`)
and **every** new site is a literal `answer=True`. What is permanent is the *firewall*,
not the count: no `answer=False` branch is ever added anywhere, and FrameVerdict adds no
`Determined` site of its own.
- `evaluate_frame_verdict` is the **only** constructor of `FrameVerdict`, and lives in a
package the open-world runtime spine does **not** transitively import.
- The two paths share the **front-end reader** (`comprehend` → `realize`, the same
`RealizedRecord` grounds shape) but diverge at context establishment and entry point.
Reusing the reader is sanctioned; reusing the *entry point* is forbidden. **[adv]**
Because the reader is shared, INV-31 must firewall the *data flow*, not only the module
imports: a `ClosedFrame`-derived grounds must be unable to enter `determine()`, and the
disclosure gate must refuse to render a `FrameVerdict` through an open-world disposition
(§8 Part B).
---
## 5. Semantics — the verdict table
The single load-bearing rule: **a closed frame licenses `False`, and `entailed_false`
is produced only from a *positive proof of the negation*.** "The world is closed" is
realized by the frame *declaring* its closure facts (disjointness, expected-set
completeness), which the existing sound producers then consume — **not** by an unsound
"not-provable ⇒ false" (text) or "not-observed ⇒ false" (perception) leap.
### 5.1 Text frame (`frame_kind = text`)
`evaluate_frame_verdict` lowers the `ClosedFrame.propositions` + `query` to the
propositional regime and calls the *existing* `evaluate_entailment_with_trace(premises,
query)`:
| `entail.py` outcome | `FrameVerdict.verdict` | Rationale |
|---|---|---|
| `ENTAILED` (`(⋀prem) → query` taut.) | `entailed_true` | the frame proves query |
| `REFUTED` (`(⋀prem) → ¬query` taut.) | `entailed_false` | the frame **proves** ¬query — sound closed-world No |
| `UNKNOWN` | `undetermined` | neither proven — within-frame refusal (NOT False) |
| `REFUSED(INCONSISTENT_PREMISES)` | `contradiction` | the frame's own premises clash — decline, *ex falso* |
| `REFUSED(OUT_OF_REGIME_OR_MALFORMED)` | `scope_boundary` | ungrounded ∀/predicate — not decidable here |
The `EntailmentTrace` (with `refutation_check_key` — the ROBDD key of `(⋀prem)→¬query`)
becomes the `ClosedWorldProof`; `producer="proof_chain.entail"`, `outcome="REFUTED"`,
`positive_refutation_kind="robdd_refutation"`.
*(Adversarial review confirmed `REFUTED` is a genuine `(⋀prem)→¬query` tautology — a
real positive proof — and that `UNKNOWN`/`INCONSISTENT_PREMISES` stay strictly out of
`entailed_false`.)*
### 5.2 Perception frame (`frame_kind = perception`) **[adv — fully revised]**
ADR-0211 has **no `query` and no `¬query` proof**: a `FalsificationRun` is a *set
comparison* of one actual frame to one hypothesis-scoped `ExpectedObservationFrame`. So
the perception convergence must (a) name the proposition it decides, and (b) refuse to
launder absence/over-observation into `entailed_false`.
**The perception query is frame-conformance**, keyed by the expected frame:
`query = "observation conforms to expected frame " + expected_id`. Under *that specific*
proposition, the residual decomposes (it is **not** a bare `SUPPORTED/FALSIFIED` map):
| Residual condition (from `FalsificationResidual`) | `FrameVerdict.verdict` | Why |
|---|---|---|
| `SUPPORTED` (`matched == expected`, none missing/changed/unexpected) | `entailed_true` | the conformance proposition is positively observed |
| `changed ≠ ()` (a declared-expected slot observed with a **contradicting** `merge_key`) | `entailed_false` | a **positively observed** contradiction of a declared expectation — sound No |
| `missing ≠ ()` only (an expected slot received **no** observation) | `undetermined` | absence, not contradiction — the perception analogue of NAF (deferred, see §5.3) |
| `unexpected ≠ ()` only (an extra slot appeared) | `undetermined` | over-observation ("saw more than expected") — not a refutation of any expected slot |
| whole actual frame absent (`_missing_actual_run`, `actual_frame_id="__missing_observation_frame__"`) | `scope_boundary` | observed nothing — a coverage gap, never a proof of ¬query |
| `_canonical_refs` conflicting-slot raise (`ExpectedObservationFrame` ill-formed) | `scope_boundary` | the frame is not a licensed complete expectation |
`ClosedWorldProof` for an `entailed_false`: `producer="sensorium.falsification"`,
`outcome="FALSIFIED"`, `proof_keys=(FalsificationRun.trace_hash,)`,
`positive_refutation_kind="perception_changed_slot"` — which the adapter sets **only**
when `changed ≠ ()` (the `__post_init__` invariant of §3 is the backstop: a generic
`FALSIFIED` leaves `positive_refutation_kind=None` and cannot become `entailed_false`). Perception is **binary-native** (ADR-0211 v1 emits only
`SUPPORTED`/`FALSIFIED`), so in v1 it inhabits the subset
`{entailed_true, entailed_false, undetermined, scope_boundary}` of the verdict alphabet;
a query the expected frame under-determines is routed to `scope_boundary`, never forced.
### 5.3 The rules that keep `entailed_false` sound (both frames)
1. **Positive proof only.** `entailed_false` requires either an ROBDD `REFUTED` proof
(text) or a `changed`-slot contradiction (perception). There is **no** `entailed_false`
from textual non-provability, from a missing observation, or from an extra observation.
2. **`contradiction` is not `False`.** Inconsistent frame premises yield `contradiction`
(decline), never `entailed_false`. The design must not collapse `REFUTED` and
`INCONSISTENT_PREMISES` — different facts about the world (and, per §7, they must stay
distinguishable *at the disclosure layer*, not only upstream).
3. **`undetermined` stays `undetermined` outside a complete frame.** Under
`bounded_closed`, anything outside the declared bound is `undetermined`/`scope_boundary`,
never `False`. This is exactly the OWA discipline (`label` returns `Unknown` from
absence, `False` only from declared disjointness).
> **Deferred (separately ratifiable):** *negation-as-failure* in both frames — text
> "declared-complete ⇒ unprovable is false" **and** perception "observation-complete ⇒
> a missing expected slot is false." This is the single riskiest soundness hinge —
> "the frame/observation is truly complete" is a strong, easy-to-get-wrong claim — so v1
> omits it on **both** sides. When pursued, each must carry an explicit, machine-checkable
> completeness witness and its own `wrong=0` proof; the text side must still route through
> `entail` (the completeness facts become premises), and the perception side must carry an
> observation-completeness license, never a bare absence leap.
---
## 6. Modality convergence
```mermaid
flowchart TD
subgraph FRONT[shared front-end reader]
R[comprehend → realize\nRealizedRecord grounds]
end
R --> K{frame_kind\n+ explicit ClosedFrame}
K -->|text: propositions + query| T[evaluate_entailment_with_trace\nENTAILED / REFUTED / UNKNOWN / REFUSED]
K -->|perception: expected vs actual| P[compare_expected_to_observation\nresidual decompose §5.2]
K -.->|audio / vision\n(reserved)| F[same envelope,\ndifferent frame evidence]
T --> V[FrameVerdict\nverdict + ClosedWorldProof + trace_hash]
P --> V
V --> G[core/epistemic_disclosure\nchoose_served_disposition → govern_response → shape_surface]
G --> U[user surface\ndefault-dark]
```
The discriminator `frame_kind` partitions substrates **at the front**, exactly as
`RealizedRecord.structure_kind` already partitions meaning-graph vs binding-graph
substrates. **[adv]** What is *shared* across frames is the **output envelope, the
governance/disclosure path, and the replay digest**. The **input signature differs by
frame**: text takes `(propositions, query)`; perception takes `(expected_frame,
actual_frame)` and *synthesizes* the frame-conformance query (§5.2). A new modality adds
a `FrameKind` member and a producer adapter — never a new verdict alphabet, never a spine
rewrite. The render integration lives entirely in `core/epistemic_disclosure` (§8), so
`chat/runtime.py` never imports the closed-world package.
---
## 7. Standing & servability (no parallel object, default-dark) **[adv — revised]**
`FrameVerdict` produces a typed verdict and **commits/serves nothing itself** — the
discipline of `ConverseEstimate`, which returns a candidate and lets the gate + disclosure
layer decide. A wrong served closed-world verdict must always be a *disclosed* wrong.
Two distinct axes carry standing and must not be conflated:
- **`basis`** (`teaching.epistemic.EpistemicStatus` → `as_told`/`verified`), computed by
`_basis(grounds)`. This is the *grounds' standing*.
- **`EpistemicState`** (`core.epistemic_state`, the 15-member governance taxonomy). For
the *limitation* verdicts, a `FrameVerdict` is lowered to a `LimitationAssessment` whose
state is derived by the **existing** `limitation.py::_KIND_TO_STATE`. For the *committed*
verdicts (`entailed_true`/`entailed_false`), **[ratify]** the default produced state is
`EpistemicState.INFERRED` with `DisclosureClaim.NONE` — a frame-derived conclusion, not
`EVIDENCED` (`RECONCILE` drift) and not `VERIFIED` (which has its own protected producer).
`_basis` does **not** produce an `EpistemicState`; the two enums are orthogonal.
Mapping onto the **existing** closed sets (no fourth taxonomy):
| `FrameVerdict.verdict` | Is it a limitation? | `LimitationKind` / `ResolutionAction` | `ServedDisposition` | Notes |
|---|---|---|---|---|
| `entailed_true` | no — a committed **answer** ("Yes") | — | `COMMIT` | **[ratify]** `EpistemicState.INFERRED` + `DisclosureClaim.NONE` by default; surface carries the `as_told`/`verified` basis honestly. Do **not** stamp `EVIDENCED` (`RECONCILE` drift) or `VERIFIED` (no producer) |
| `entailed_false` | **no — a committed answer ("No")**, not a block | — | `COMMIT` | **[ratify]** `COMMIT`-with-negative-surface: `EpistemicState.INFERRED` + `DisclosureClaim.NONE`; PR-4 adds a grounded-negative renderer (`render_determination` only renders affirmations). It is **not** a `contradiction` and must **not** add or reuse a `LimitationKind` |
| `contradiction` (inconsistent frame) | yes | `contradiction` / `report_contradiction` → `CONTRADICTED` | `REPORT` | the **only** verdict that is a real contradiction; carries `blocking_reason="frame_inconsistent"` |
| `undetermined` | yes | `hard_boundary` / `refuse_known_boundary` → `UNDETERMINED` | `REFUSE` | within-frame refusal |
| `scope_boundary` | yes | `scope_boundary` / `refuse_known_boundary` → `SCOPE_BOUNDARY` | `EXPLAIN` | out-of-regime / unlicensed frame |
This resolves the two governance findings from review: `entailed_false` (a proven "No")
no longer collapses onto the `contradiction` triple (they were colliding on every typed
field of `LimitationAssessment`), and a proven negative is correctly typed as a *committed
answer* rather than a `CONTRADICTED` *block*. The closed `LimitationKind` set has no
"soundly-refuted" member **because `entailed_false` is not a limitation**. **[ratify]
RESOLVED:** the grounded-negative answer is served as `COMMIT`-with-negative-surface — a
PR-4 *renderer*, **no** new `LimitationKind`/`EpistemicState` member. `ServedDisposition.COMMIT`
already means "serve a fully-grounded answer as-is"; `REPORT` stays reserved for the
inconsistent-frame `contradiction`.
Binding rules:
- **Stays STRICT.** A closed-world verdict is *absolute* (proof-backed), not a statistical
estimate — it never rides the `APPROXIMATE` rung. `govern_response` is called with **no**
`license_decision`, returns `STRICT_POLICY`, and `shape_surface` is the byte-identical
identity transform. Serving SHAs and `wrong=0` are unchanged.
- **Cannot self-certify `VERIFIED`.** `DisclosureClaim.VERIFIED` degrades to `COMMIT`
unless `EpistemicState.VERIFIED` (no producer; `RESERVED` in `policy.py`).
- **Default-dark.** **[adv]** `choose_served_disposition` has **no caller on the default
live serving path** — its one caller (`core/epistemic_disclosure/ask_serving.py` via
`chat/ask_runtime.py::maybe_apply_served_ask`) is itself unwired into `chat/runtime.py`.
The `FrameVerdict` disclosure path lands in the same posture: classify + decide a
disposition, but do **not** flip the live `shape_surface` STRICT identity until a
ratified producer + lane exist. Byte-identical serving is preserved.
Standing/persistence (if a lane ever persists a refuted hypothesis): through
`VaultStore.store` only, **SPECULATIVE by default** (INV-21/22/23) — a perceptual
falsification refutes a SPECULATIVE `HypothesisClaim` (ADR-0211), it never mints COHERENT.
The only path to `verified` standing remains the certificate-gated
`apply_certified_promotion` (INV-29). `FrameVerdict` writes no status itself.
---
## 8. INV-31 — the firewall (closed-world `False` cannot reach the open-world runtime) **[adv — fully revised]**
The review showed a single-level, 3-file import scan is **insufficient**: "the open-world
path" is not a scannable unit (`chat/runtime.py` is one file holding the open-world,
realization, and governance-render code together); a single-level scan is defeated by one
transitive hop (the spine already imports into `generate.proof_chain`, the `FrameVerdict`
producer package); and the *actual* leak surface is the **shared reader + shared
disclosure gate**, a data-flow path no import scan touches. INV-31 is therefore a
**two-part** firewall, and it lands in **PR-1 together with the type** — never after.
**Guarantee.** A closed-world verdict (`FrameVerdict`, especially `entailed_false` /
`contradiction`) can never be *produced by*, *imported by*, or *rendered as an open-world
fact by* the open-world runtime spine.
### Part A — transitive import containment
- **A1.** `generate/determine/determine.py` neither imports nor constructs `FrameVerdict`;
`determine()`'s return union stays `Determined | Undetermined`.
- **A2.** `FrameVerdict(…)` is constructed **only** inside an **exact** allowlist (no glob):
`ALLOWED_FRAME_VERDICT_SITES = frozenset({"generate/frame_verdict/evaluate.py", …exact
files…, "evals/proofwriter_cwa/adapter.py", …})`. The matcher must catch **every**
constructor, not just the literal `FrameVerdict(…)` call: classmethod factories,
`dataclasses.replace(v, verdict=…)`, and any helper returning `FrameVerdict` — mirroring
INV-21's receiver-binding matcher, which exists precisely to defeat wrapper evasion. A
drift-guard (à la `test_allowlist_is_actually_used`) flags a listed-but-unused site. The
construction scan's file-walk **must include `evals/`** (unlike INV-30's
`_enumerate_project_py_files`, which excludes it) or the eval-adapter entries are
unenforced.
- **A3 (transitive).** `generate/frame_verdict` is unreachable from the **transitive
first-party import closure** of every open-world spine entry module — computed with the
existing `_transitive_first_party_imports` walker (INV-27's), **not** a single-level
scan. The spine set is the *whole files* `chat/runtime.py`, `session/context.py`,
`vault/store.py` (each barred entirely — there is no "open-world path" sub-unit). The
package is placed so no spine closure touches it, and it is **forbidden to be re-exported
through `generate/proof_chain`** (which the spine already imports). `frame_verdict` may
import *from* `generate.proof_chain.entail` and the lifted `generate/epistemic_basis.py`;
those one-way edges are sanctioned and the scan is **directional** (spine ↛ frame_verdict,
not the reverse).
### Part B — typed data-flow firewall (the shared-reader / shared-gate leak)
Imports alone don't reach the leak surface the shared front-end creates, so:
- **B1.** `determine()`'s grounds input is type-tagged such that a `ClosedFrame`-derived
grounds **cannot** be fed to the open-world `determine()` (a typed guard + a test that a
closed-frame provenance into `determine()` raises).
- **B2.** `choose_served_disposition` / `govern_response` / `shape_surface` **refuse to
render a `FrameVerdict` via an open-world disposition** unless an explicit closed-world
disposition tag is present. The render integration lives **inside
`core/epistemic_disclosure`**, never in `chat/runtime.py`; the spine ↛ frame_verdict
containment (A3) plus this typed render gate means a closed-world `entailed_false` cannot
reach the user surface as an open-world assertion.
### Non-vacuity — a meaningful-failure anchor for *each* scan
Mirroring INV-30's trio (30b non-vacuity, 30b′ no-false-positive, 30c sites-visible) and
INV-29's parallel trio, every scan gets an anchor so a blind/mis-rooted scan fails loudly:
| Test | Fails when |
|---|---|
| `test_inv31_determine_is_visible_and_clean` (anchors A1) | the scan does **not** see `determine.py`'s real `Determined` sites (the count INV-30c pins, whatever it is at the time), or sees a `FrameVerdict` ref there |
| `test_inv31_construction_allowlist` (anchors A2) | any `FrameVerdict`/factory/`replace` construction occurs outside the exact allowlist |
| `test_inv31_construction_detector_is_non_vacuous` | a fixture constructing `FrameVerdict` (and each alternate-constructor shape) in a forbidden location is **not** flagged |
| `test_inv31_spine_imports_resolve_and_exclude` (anchors A3) | a spine module's transitive import set is empty (mis-rooted/typo'd scan), **or** it does include `generate.frame_verdict` |
| `test_inv31_determine_rejects_closed_frame_grounds` (anchors B1) | a `ClosedFrame`-derived grounds fed to `determine()` does **not** raise |
| `test_inv31_open_disposition_rejects_frameverdict` (anchors B2) | the open-world disposition renders a `FrameVerdict` without the closed-world tag |
The non-vacuity claim is scoped per scan — "INV-31 is non-vacuous" holds only because
*each* of A1/A2/A3/B1/B2 has its own meaningful-failure anchor, not because one fixture
test covers the construction scan alone.
---
## 9. Measurement
- **`wrong_total == 0`, closed-world edition.** For a future ProofWriter-CWA lane,
`wrong` is *"the closed-world gear asserted `entailed_false` where the independent CWA
oracle does not entail ¬query (or `entailed_true` where it does not entail query)."*
The analogue of the OWA breach; `wrong` must stay 0, non-vacuous because the oracle is
independent (INV-25/27).
- **Independent gold, disjoint solver.** A CWA oracle is the closed-world analogue of
`evals/proofwriter_owa/oracle.py::label`: same disjoint-oracle discipline (imports no
`determine`/`comprehend`/`frame_verdict`), but it may soundly return `False` more often
under the declared CWA. The oracle stays the scorer; it is never promoted into serving.
- **Capability-index registration.** Unlike the OWA *refusal floor* (deliberately **not** a
capability domain — low coverage drags `coverage_geomean`), a two-sided CWA lane *commits*
`entailed_true`/`entailed_false` and **is** a real capability domain. It registers through
the existing hook: a `proofwriter_cwa_result() -> DomainResult` adapter appended to
`evals/capability_index/adapters.py::ADAPTERS`; a lane that fails to run is recorded in
`Collection.not_covered`, never faked.
- **Replay digest stable.** Every `FrameVerdict.trace_hash` is deterministic (`sha256_json`,
order-invariant). The lane's report digest must be byte-stable — no clock, no LLM, no
sampling.
- **The OWA floor (#779) stays green.** A CWA lane is a *separate* measure-only lane. B4
adds no `False` path to `determine()`, so the OWA `wrong=0` / `coverage_gaps` gate is
unaffected.
---
## 10. Implementation plan (gated; this PR is design-only)
| PR | Scope | Gate |
|---|---|---|
| **PR-0 (this)** | This ADR only. No code. | ratification of this document |
| **PR-1** | Lift `_basis` → `generate/epistemic_basis.py`; add `generate/frame_verdict/` (the `FrameVerdict`/`ClosedFrame`/`ClosedWorldProof` types incl. the `__post_init__` admissibility invariant + `evaluate_frame_verdict` for the **text** frame, delegating to `entail`) + serialization + **INV-31 Part A & B** with all six non-vacuity anchors. No serving wire. | PR-0 ratified |
| **PR-2** | `evals/proofwriter_cwa/` — independent CWA oracle + hand-authored CWA fixtures + scorer (`correct_false` / `wrong_false` columns) + `capability_index` adapter. Measure-only. | PR-1 merged |
| **PR-3** | `sensorium/environment/` → `FrameVerdict` adapter (the **conservative** §5.2 residual decomposition: only `changed`→`entailed_false`; missing/unexpected/whole-missing→undetermined/scope_boundary; frame-conformance query; full-run `trace_hash` proof). Perception-NAF stays deferred. | PR-1 merged |
| **PR-4** | `core/epistemic_disclosure` integration — map `FrameVerdict` → `ServedDisposition` per §7 (committed verdicts → `COMMIT` at `EpistemicState.INFERRED` + `DisclosureClaim.NONE`), incl. a grounded-**negative** renderer for `entailed_false`, **default-dark** (no live `shape_surface` flip). | PR-2/3 merged + a ratified producer |
Sequencing rule: **INV-31 ships with the type (PR-1), never after.** The firewall must
exist the moment a `FrameVerdict` can be constructed.
---
## 11. Non-negotiables honored
| Non-negotiable | How this design satisfies it |
|---|---|
| Do not modify `determine()` to emit `answer=False` | `determine.py` untouched; INV-31 A1 fails if it imports/constructs `FrameVerdict`; the new path is a distinct package/function |
| Do not relax INV-30 | INV-30 unchanged and green; `FrameVerdict` has no `answer` field and a distinct name (review ran the real predicate → `[]`), so the scan cannot match it |
| Do not treat absence as false | text `entailed_false` only from an ROBDD refutation; **perception `entailed_false` only from a `changed`-slot contradiction** — missing/unexpected/whole-missing → undetermined/scope_boundary; NAF deferred both frames |
| No closed-world verdict masquerades as open-world `Determined` | distinct type, distinct entry point, 5-way `verdict` enum (not a bool), **and the typed data-flow firewall** (INV-31 Part B) blocks the shared-reader / shared-gate leak |
| Closed-world `False` requires an explicit closed/bounded frame + proof basis | entry point takes a `ClosedFrame` (never `SessionContext`); `OPEN`/forged/implicit frames → `SCOPE_BOUNDARY`; every `entailed_false` carries a positive-refutation `ClosedWorldProof` (enforced by `__post_init__`) |
| `FrameVerdict` is a separate type/surface from `Determined` | yes — separate package, type, entry point, and (PR-4) grounded-negative renderer |
| `response_governance` stays the final servability gate | verdict commits nothing; surfaces only via `choose_served_disposition` → `govern_response` → `shape_surface`, STRICT, default-dark |
---
## 12. Proof obligations (per *Schema-Defined Proof Obligations*)
Each claim is real only if an executing test can meaningfully fail under the violation it
names. Obligations PR-1+ must discharge:
1. **INV-31 per-scan non-vacuity** — the six anchors in §8 (each of A1/A2/A3/B1/B2 has a
meaningful-failure test; the construction detector is exercised against every alternate
constructor shape).
2. **`entailed_false` is proof-backed (now non-vacuous)** — the §3 `__post_init__` raises
on `verdict==ENTAILED_FALSE` unless the proof is a *named* positive refutation
(`robdd_refutation` from `proof_chain.entail`/`REFUTED`, or `perception_changed_slot`
from `sensorium.falsification`/`FALSIFIED`); a test constructs each mismatch — including
a **generic `FALSIFIED` with `positive_refutation_kind=None`** — and asserts the raise.
3. **`contradiction ≠ entailed_false`** — inconsistent premises → `contradiction`, never
`entailed_false`; and (§7) the two carry distinct `LimitationKind` so they stay
distinguishable at the disclosure layer, not only upstream.
4. **Absence never yields `entailed_false`** — text: an `UNKNOWN` query → `undetermined`;
perception: a **missing-only** residual and a whole-frame-missing run → `undetermined` /
`scope_boundary`, asserted explicitly (the blocker the review caught).
5. **Replay determinism** — identical `trace_hash` across two runs and under input
reordering; perception proof binds the full `FalsificationRun.trace_hash`.
6. **CWA `wrong=0` is non-vacuous** — the lane's scorer, against the independent oracle,
fails if any `entailed_false` is asserted where the oracle does not entail ¬query.
---
## 13. Consequences
**Positive.** A single sound, replayable, frame-general closed-world verdict; text-CWA
and perception converge on one envelope before either is built, so neither invents an
incompatible "False" shape; the open-world runtime is firewalled by both import
containment *and* a typed data-flow guard; no new solver, no relaxed invariant, no serving
regression.
**Costs / risks.**
- **NAF deferral (both frames)** means v1 text-CWA asserts `False` only where the frame
*declares* the refuting facts, and v1 perception asserts `False` only on a `changed`-slot
contradiction. ProofWriter-CWA fixtures must include their closure facts — which matches
how ProofWriter-CWA is presented. Acceptable; NAF is the riskier hinge and is correctly
deferred.
- **Perception is binary-native and conservative.** It inhabits a subset of the verdict
alphabet in v1; under-determined queries → `scope_boundary`. This is the honest cost of
not laundering set-inequality into entailment.
- **Grounded-negative renderer is new (PR-4).** `entailed_false` is a committed "No" with
no existing renderer; **[ratify] resolved** as `COMMIT`-with-negative-surface (no new
closed-set member), served at `EpistemicState.INFERRED` + `DisclosureClaim.NONE`.
- **`_basis` lift** (PR-1) is a small, mechanical refactor that removes the open/closed
package coupling the review flagged; INV-31's directional scan depends on it.
- **INV-31 import scans** must use the project-wide source walk with the maintained
`.claude`/worktree exclusions (CLAUDE.md *Architectural Scan Exclusions*), and the
construction scan must *include* `evals/`.
**Alternatives considered & rejected.**
- *Widen `determine()`/`Determined` with `answer=False`* — rejected: mechanically breaks
INV-30 and contaminates the open-world session-memory path.
- *Map bare `FalsificationRun.verdict` (SUPPORTED/FALSIFIED) onto `entailed_true`/`entailed_false`*
— rejected (review blocker): `FALSIFIED` fires on absence (`missing`, whole-frame-missing)
and over-observation (`unexpected`); `SUPPORTED` is mere set-match, not a proof of any
query. Only `changed` is a positively-observed contradiction.
- *Route `entailed_false` through `LimitationKind=contradiction`* — rejected (review):
collapses a proven "No" with an inconsistent frame and mis-types a grounded answer as a
block.
- *A single-level 3-file import scan as the firewall* — rejected (review): defeated by one
transitive hop and blind to the shared-reader/disclosure leak.
- *Negation-as-failure in v1 (either frame)* — deferred (§5.3), not adopted, for soundness.
---
## 14. Ratification checklist (to be completed by architect)
- [ ] The `FrameVerdict` axes (§3) are the right closed set — `frame_kind`,
`world_assumption`, the 5-way `verdict` (`undetermined`, aligning with the merged
brief and `EpistemicState.UNDETERMINED`), `basis/proof/evidence`, `trace_hash`.
- [ ] No `answer` field / distinct name is accepted as the INV-30-safe shape, and the
`__post_init__` admissibility invariant is accepted.
- [ ] The §5.1 text table and the **revised §5.2 perception decomposition** (only
`changed`→`entailed_false`; missing/unexpected/whole-missing → undetermined/scope_boundary;
frame-conformance query) are correct.
- [ ] NAF deferral on **both** frames (§5.3) is accepted for v1.
- [ ] **INV-31's two-part shape** (§8 — transitive import containment + typed data-flow
firewall) with all six non-vacuity anchors is accepted, shipping in PR-1.
- [ ] The `_basis` lift to `generate/epistemic_basis.py` (PR-1) is authorized.
- [x] **RESOLVED (ratify):** the §7 governance mapping — `entailed_false` as a committed
"No" (not a `contradiction` block), STRICT, default-dark, no `VERIFIED` self-cert.
Grounded-negative answer = `COMMIT`-with-negative-surface (a PR-4 renderer), **no**
new `LimitationKind`/`EpistemicState` member.
- [x] **RESOLVED (ratify):** `entailed_true`/`entailed_false` produced `EpistemicState` =
`INFERRED` with `DisclosureClaim.NONE` by default; never `EVIDENCED`, never `VERIFIED`
unless a later canonical verified producer earns it.
- [x] **APPLIED (ratify):** the explicit `positive_refutation_kind` discriminator (§3) so a
generic `FALSIFIED` cannot satisfy `entailed_false`; and the PR-1-scoped wording for
the `Determined`-count rule (§4, no permanent ban on future visible-count additions).
- [ ] The PR sequence (§10) and the "INV-31 ships with the type" rule are authorized.
- [ ] The new invariant number **INV-31** is free / correctly assigned (review confirmed
no existing `INV-31` reference).