docs(1259-01): wire verify-phase consumer + ADR-550/FEATURES/reference + changeset

- verify-phase.md: replace test-tier 'fail-closed/deferred' bullet with the check prohibition-enforcement
  enforcement step (locate -> fail-first -> run -> evidence -> green-or-hard-gate); update determine_status tree
- ADR-550 addendum: mark D5d enforcement half LANDED (#1259); cite ADR-857 open-question §147 + D6 (core verify rail)
- FEATURES §146: enforcement wording + add REQ-PROHIB-07; keep REQ-PROHIB-06 intact
- references/prohibition-probe.md: test-tier enforced + hard-gates via check prohibition-enforcement
- changeset (type: Changed) with the D5 '2 no-source-grep invalid cases, not 96' correction
This commit is contained in:
Dave
2026-06-15 12:47:00 -04:00
parent 8f428bdd41
commit ce01e1376b
5 changed files with 36 additions and 6 deletions

View File

@@ -0,0 +1,8 @@
---
type: Changed
pr: 1259
---
**Test-tier prohibitions are now a real, provable gate instead of a permanent, unsatisfiable `gaps_found`** — the deferred ENFORCEMENT half of ADR-550 Decision 5d (the "heavy half" that #644 / PR #1149 deferred) has landed. A new deterministic `check prohibition-enforcement` sub-command (authored as `src/prohibition-enforcement.cts`, compiled by `build:lib` to the gitignored `gsd-core/bin/lib/prohibition-enforcement.cjs`) is the missing PRODUCER: it locates the wired mechanical check, confirms it is fail-first (`regression-must-fail-first`), runs it, builds `enforcementEvidence`, and emits the `dispositionForProhibition()` verdict. The previously-unreachable green branch in `dispositionForProhibition()` is now reachable from the live pipeline — a test-tier prohibition with a PASSING wired check disposes `green` and can reach `passed`, while a missing, failing, or non-fail-first check hard-gates (flagged, never green → `gaps_found`) in BOTH interactive and autonomous modes (ADR-550 D4 / D3). `verify-phase.md` wires the consumer; the green/fail-closed policy in `src/probe-core.cts` is untouched. Both wired-check kinds are accepted (ADR-550 D2): a `node --test` negative test AND a lint/AST rule, anchored on the in-tree `no-source-grep` rule (dogfooding, ADR-550 D4). This enforcement seam is the concrete instance of ADR-857 open-question §147 and lands on the core verify rail, never in `capabilities/` (D6). (#1259)
**Correction to the issue body (#1259):** the issue's "96 invalid/error negative-proof cases" figure is wrong. The definitive count is **26 invalid cases / 23 error-expectation objects** across all rule-test files; the `no-source-grep` anchor itself has exactly **2 invalid cases** (`tests/eslint-rules.test.cjs`, the `.includes()` and `.match()` invalid blocks). Those 2 cases ARE genuine `regression-must-fail-first` proofs, so the anchor argument is unaffected — but the count is "the 2 `no-source-grep` invalid cases," not 96.

View File

@@ -3169,7 +3169,7 @@ Each surfaced prohibition is resolved to exactly one of three states:
| `dismissed` | Not a genuine prohibition (requires a non-empty reason) | Recorded with its reason; empty dismissals are rejected |
| `unresolved` | Deferred | Soft-gates the spec; surfaced as a planner assumption |
Each resolved prohibition carries a `verification` tier — `test` (a negative test can enforce it) or `judgment` (only human/LLM judgment can). At verify time, judgment-tier prohibitions route to a never-silent / never-hard-halt soft gate (autonomous emits an `unverified-prohibition — human review recommended` flag); test-tier prohibitions fail closed when unwired (never silently green). Under `--auto`, the probe **never auto-dismisses**. Canon-bound concerns (OWASP / GDPR / fairness) are referred to `/gsd:secure-phase` rather than minting SPEC prohibitions (ADR-550 D6).
Each resolved prohibition carries a `verification` tier — `test` (a negative test can enforce it) or `judgment` (only human/LLM judgment can). At verify time, judgment-tier prohibitions route to a never-silent / never-hard-halt soft gate (autonomous emits an `unverified-prohibition — human review recommended` flag); test-tier prohibitions are enforced via the deterministic `check prohibition-enforcement` gate — green when the wired negative test / lint rule passes, hard-gate (flagged, non-green) when missing or failing, in both interactive and autonomous modes (#1259, ADR-550 D5d). Under `--auto`, the probe **never auto-dismisses**. Canon-bound concerns (OWASP / GDPR / fairness) are referred to `/gsd:secure-phase` rather than minting SPEC prohibitions (ADR-550 D6).
The load-bearing wire is the `plan-phase` lift into `must_haves.prohibitions`, so the section is not merely documentation.
@@ -3180,5 +3180,6 @@ The load-bearing wire is the `plan-phase` lift into `must_haves.prohibitions`, s
- REQ-PROHIB-04: `--auto` MUST never auto-dismiss.
- REQ-PROHIB-05: `plan-phase` MUST lift resolved prohibitions into `must_haves.prohibitions` (never `truths`).
- REQ-PROHIB-06: A well-formed but unwired `test`-tier prohibition MUST fail closed at verify time — never a silent pass.
- REQ-PROHIB-07: A `test`-tier prohibition with a PASSING wired mechanical check (a `node --test` negative test OR a lint/AST rule) MUST dispose green and be satisfiable; a missing or failing check MUST hard-gate (flagged, non-green) in both interactive and autonomous modes (#1259, ADR-550 D5d — the enforcement half).
**Reference:** [Prohibition Probe](../gsd-core/references/prohibition-probe.md)

View File

@@ -85,11 +85,13 @@ The capability system (ADR-857) classifies **predicate-generation as core verifi
- **The probe *adapters* are the core-default *generator*** — `edge-probe`'s `classifyShape`/`proposeEdges` and the prohibition probe's adversarial LLM-propose, the surfaces that *propose* predicates — default-on and non-removable, but **independently versionable**. The classifier's measured recall gap (the prose→shape under-fire on terse prose) is the reason they stay their own modules under this ADR rather than being folded into the slow core rail. **`probe-core` is not the generator:** per Decision 7b it ingests already-proposed items, and its deterministic validators are the **contract**'s CI-testable surface (Decision 5) — so `probe-core` sits on the contract side, the adapters on the generator side. ADR-857 phase 6 wires these modules onto the core predicate rail; it does **not** relabel them as a `capabilities/edge-probe/` plug-in.
- Decision 5's rule — *the CI-testable surface is the contract, not the classifier* — extends to ADR-857's core rail: the deterministic conformance test is the contract shape the verifier consumes, never the LLM's judgment.
## Addendum (2026-06-12): test-tier disposition — fail-closed now, heavy enforcement deferred
## Addendum (2026-06-12; updated 2026-06-15): test-tier disposition — fail-closed safety half (#644) + enforcement half LANDED (#1259)
Decision 4 describes the `test`-tier as a "**Hard gate in both interactive and autonomous modes.**" The #644 implementation revises that to a **fail-closed-now / deferred-enforcement** resolution (the "B-with-guard" maintainer decision of 2026-06-12), so the architecture-of-record matches the shipped code:
- A well-formed but **unwired** `test`-tier prohibition resolves via `dispositionForProhibition()` to `{ status: 'unverified', flagged: true }` — **provably never green** without explicit evidence (REQ-PROHIB-06). This is the load-bearing safety half and it holds today.
- The **heavy negative-test enforcement mechanism** — a contrived `test`-tier consumer that mechanically runs the negative test — is **deferred to a follow-up**, because the #644 corpus is entirely `judgment`-tier and wiring a synthetic test-tier consumer now would be gold-plating. The fail-closed disposition guards the gap in the meantime: the gate cannot silently pass, it can only report `unverified`/flagged until enforcement lands.
- The **heavy negative-test enforcement mechanism** — locating the wired mechanical check, confirming it is fail-first, running it, and building the `enforcementEvidence` that flips a passing test-tier item green — **landed in #1259** as the deterministic `check prohibition-enforcement` sub-command (authored as `src/prohibition-enforcement.cts`, compiled by `build:lib` to the gitignored `gsd-core/bin/lib/prohibition-enforcement.cjs`). It accepts BOTH wired-check kinds — a `node --test` negative test OR a lint/AST rule — and is anchored on the in-tree `no-source-grep` AST rule (dogfooding the existing must-NOT proof, ADR-550 D4; the #644 corpus had zero authored test-tier prohibitions, so no contrived consumer was minted). A passing wired check disposes green; a missing, failing, or non-fail-first check hard-gates (flagged, non-green) in both interactive and autonomous modes.
Net effect on D4: the *guarantee* ("a `test`-tier prohibition is never a silent pass") is preserved exactly; what is deferred is only the mechanical-pass half of the gate, not the never-green safety property. This addendum supersedes the unqualified "hard gate" wording of Decision 4 for `test`-tier items until the enforcement follow-up lands. The decision also lives in `src/probe-core.cts` comments, `verify-phase.md`, and the #644 changeset.
Net effect on D4: the *guarantee* ("a `test`-tier prohibition is never a silent pass") was preserved through the fail-closed-now half and is now joined by the mechanical-pass half — a test-tier prohibition with a passing wired check can reach `green`/`passed`, and a missing/failing one hard-gates. The unqualified "hard gate" wording of Decision 4 is now fully realized for `test`-tier items: the previously-unreachable green branch in `dispositionForProhibition()` is reachable from the live pipeline, and the fail-closed default backs every miss/fail. The decision also lives in `src/probe-core.cts` comments, `src/prohibition-enforcement.cts`, `verify-phase.md`, and the #644 / #1259 changesets.
This enforcement seam is the concrete instance of **ADR-857 open-question §147** — the deferred "deterministic CI conformance test for the verifier↔predicate contract." Per D6 it lands on the **core verify rail** (non-toggleable substrate), never in `capabilities/`: the verifier consuming a contract-shaped, deterministic predicate is core, not an opt-in capability.

View File

@@ -110,6 +110,17 @@ lifecycle is identical to the edge-probe, the verification tiers differ):
human/LLM judgment that the framing is not manipulative). It records intent and routes
to a judgment-based review rather than a green/red test.
At verify time these tiers are routed differently (ADR-550 D4):
- A **test**-tier prohibition is enforced + hard-gates via the deterministic
`check prohibition-enforcement` sub-command (#1259, ADR-550 D5d): it locates the wired
mechanical check (a `node --test` negative test OR a lint/AST rule), confirms it is
fail-first, runs it, and emits the `dispositionForProhibition()` verdict. A passing wired
check disposes **green** (satisfiable → can reach `passed`); a missing, failing, or
non-fail-first check **hard-gates** (flagged, never green → `gaps_found`) in BOTH
interactive and autonomous modes — never a silent pass.
- A **judgment**-tier prohibition routes to a never-silent / never-hard-halt soft gate
(autonomous emits an `unverified-prohibition — human review recommended` flag).
Splitting these axes keeps the lifecycle enum free of a verification fact and lets the
prohibition adapter declare `test | judgment` without forking the shared lifecycle enum that
the edge-probe's `explicit | backstop` also uses.

View File

@@ -70,7 +70,15 @@ Aggregate all must_haves across plans for phase-level verification.
**Prohibitions (`must_haves.prohibitions`, ADR-550 D3 — the must-NOT sibling block):** When a plan carries `must_haves.prohibitions`, extract each `{ statement, status, verification }` item and route it by `verification` tier in verdict assembly (ADR-550 D4, "B-with-guard", 2026-06-12 maintainer decision). These are NEGATIVE checks (the must-NOT must NOT have happened), distinct from positive `truths`:
- **judgment-tier → mode-dependent soft-gate.** Interactive verify defers each item to the end-of-phase human checkpoint (`human_verify_mode: end-of-phase`). Autonomous verify records a NON-AUTHORITATIVE LLM-judge verdict + a prominent `unverified-prohibition — human review recommended` flag (autonomous completion reads "complete with N flagged prohibitions"). NEVER a silent pass; NEVER a hard halt of an AFK run.
- **test-tier → FAIL CLOSED (accept-and-flag).** Accept the `verification: test` value (the SPEC↔must_haves.prohibitions projection contract holds — no forced schema change later), but a well-formed test-tier item reaching verify with NO wired enforcement disposes as UNVERIFIED, flagged like an unresolved judgment item, NEVER green. The deterministic fail-closed default is `dispositionForProhibition()` in probe-core (`status: 'unverified'`, `flagged: true` on empty `enforcementEvidence`). The real fail-first negative-test enforcement MECHANISM defers to a follow-up PR (#644's corpus is entirely judgment-tier; a contrived test-tier fixture here would be the gold-plating failure mode).
- **test-tier → ENFORCED via `check prohibition-enforcement` (green on pass, hard-gate on miss/fail).** Accept the `verification: test` value (the SPEC↔must_haves.prohibitions projection contract holds — no forced schema change later). For each test-tier item, the verifier invokes the deterministic producer:
```bash
gsd_run check prohibition-enforcement <request.json>
```
where `<request.json>` carries `{ prohibition, check, mode }` — `check` being the wired mechanical-check descriptor `{ kind: 'node-test' | 'lint-rule', target, failFirst: true }`. The producer LOCATES the wired check, CONFIRMS it is fail-first (`regression-must-fail-first`), RUNS it, builds `enforcementEvidence`, and emits the `dispositionForProhibition()` verdict (#1259, ADR-550 D5d). Route the result by its typed fields:
- **`status: 'green'`, `flagged: false`** (a passing wired negative test / lint rule, `located: true`, non-empty `evidence`) → the item is satisfiable → it can reach **passed**.
- **missing, failing, or non-fail-first check** (`located: false` OR `status: 'unverified'`, `flagged: true`) → **hard-gate**: disposes flagged-unverified, NEVER green, routing to `gaps_found` in BOTH interactive and autonomous modes (a failing mechanical check blocks even AFK; ADR-550 D4 / D3). The deterministic fail-closed default backing every miss/fail is `dispositionForProhibition()` in probe-core (`status: 'unverified'`, `flagged: true` on empty `enforcementEvidence`).
**Option B: Use Success Criteria from ROADMAP.md**
@@ -471,7 +479,7 @@ Classify status using this decision tree IN ORDER (most restrictive first):
→ **gaps_found**
2. IF any `must_haves.prohibitions` item disposes as flagged-unverified (ADR-550 D4):
- **test-tier, fail-closed** (no wired enforcement — `dispositionForProhibition()` returns `status: 'unverified'`, `flagged: true`): → **gaps_found** (never green; the unwired test-tier item is an unverified gap).
- **test-tier, fail-closed when the wired check is MISSING OR FAILS** (now run via `check prohibition-enforcement` — `located: false`, or `dispositionForProhibition()` returns `status: 'unverified'`, `flagged: true`): → **gaps_found** in both interactive and autonomous modes (never green; a missing/failing mechanical check is an unverified gap). A test-tier item whose wired check PASSES disposes `status: 'green'`, `flagged: false` and is NOT a gap — it can reach **passed**.
- **judgment-tier, autonomous run** (non-authoritative LLM-judge verdict): emit the `unverified-prohibition — human review recommended` flag and classify → **human_needed** (autonomous completion reads "complete with N flagged prohibitions"; never a silent pass, never a hard halt).
- **judgment-tier, interactive run**: route to the end-of-phase human checkpoint → **human_needed**.