From ce01e1376b431594af165f09fd5c9eeeb44fa5c7 Mon Sep 17 00:00:00 2001 From: Dave Date: Mon, 15 Jun 2026 12:47:00 -0400 Subject: [PATCH] docs(1259-01): wire verify-phase consumer + ADR-550/FEATURES/reference + changeset MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 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 --- .changeset/1259-test-tier-enforcement.md | 8 ++++++++ docs/FEATURES.md | 3 ++- docs/adr/550-spec-phase-probe-contract.md | 8 +++++--- gsd-core/references/prohibition-probe.md | 11 +++++++++++ gsd-core/workflows/verify-phase.md | 12 ++++++++++-- 5 files changed, 36 insertions(+), 6 deletions(-) create mode 100644 .changeset/1259-test-tier-enforcement.md diff --git a/.changeset/1259-test-tier-enforcement.md b/.changeset/1259-test-tier-enforcement.md new file mode 100644 index 000000000..a0b02d905 --- /dev/null +++ b/.changeset/1259-test-tier-enforcement.md @@ -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. diff --git a/docs/FEATURES.md b/docs/FEATURES.md index 8f6e038c0..396079842 100644 --- a/docs/FEATURES.md +++ b/docs/FEATURES.md @@ -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) diff --git a/docs/adr/550-spec-phase-probe-contract.md b/docs/adr/550-spec-phase-probe-contract.md index 0567658ef..015b5ef0d 100644 --- a/docs/adr/550-spec-phase-probe-contract.md +++ b/docs/adr/550-spec-phase-probe-contract.md @@ -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. diff --git a/gsd-core/references/prohibition-probe.md b/gsd-core/references/prohibition-probe.md index 1915d2d23..ccb34de67 100644 --- a/gsd-core/references/prohibition-probe.md +++ b/gsd-core/references/prohibition-probe.md @@ -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. diff --git a/gsd-core/workflows/verify-phase.md b/gsd-core/workflows/verify-phase.md index d725c67cd..a4fa95d67 100644 --- a/gsd-core/workflows/verify-phase.md +++ b/gsd-core/workflows/verify-phase.md @@ -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 + ``` + + where `` 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**.