From b2a7a3980d21a70a7a85051a60cd22f185089386 Mon Sep 17 00:00:00 2001 From: Rezolv Date: Thu, 25 Jun 2026 20:13:00 -0400 Subject: [PATCH] docs(#1606): ADR for the prohibition-enforcement verify-time seam (#1712) Promotes the verify-time enforcement decision that accreted as four chronological addenda on ADR-550 (#1259/#1279/#1346/#1278) into a single first-class architecture-of-record. ADR-550 keeps the spec-phase contract; this ADR owns the test-tier enforcement producer (locate -> machine-prove-fail-first -> run -> dispose) in src/prohibition-enforcement.cts. Verified against live src/*.cts: the green AND-gate lives in runProhibitionEnforcement, the empty-file vacuity guard is isNonVacuousNodeTestPass (red-side is isNonVacuousNodeTestRed), and the ADR-857 pointer cites the real 'Verification substrate vs. plug-in tier' section / decision #6. Closes #1606. --- ...606-prohibition-enforcement-verify-seam.md | 189 ++++++++++++++++++ 1 file changed, 189 insertions(+) create mode 100644 docs/adr/1606-prohibition-enforcement-verify-seam.md diff --git a/docs/adr/1606-prohibition-enforcement-verify-seam.md b/docs/adr/1606-prohibition-enforcement-verify-seam.md new file mode 100644 index 000000000..028735507 --- /dev/null +++ b/docs/adr/1606-prohibition-enforcement-verify-seam.md @@ -0,0 +1,189 @@ +# ADR 1606: prohibition-enforcement verify-time seam [Proposed] + +- **Status:** Proposed (consolidation ADR — see "Relationship to ADR-550") +- **Date:** 2026-06-22 + +> **Provenance.** Drafted 2026-06-22 to promote a decision that accreted as **four** +> chronological addendum blocks on ADR-550 (the 2026-06-12 test-tier disposition note that +> folded in #1259, then #1279, #1346, and #1278) into a single, first-class architecture-of- +> record for the verify-time enforcement subsystem. Authored by the #644/#1259 implementer. +> The *area* (why prohibitions are first-class at all) traces to the author's +> prohibition-elicitation (N18) and verifier-abstention (N17) findings — *the author's own +> research*, cited as motivation, not claimed as a novel GSD contribution; the *enforcement +> mechanism* in this ADR is motivated specifically by closing the caller-attestation fake- +> green hole. Verified against `next` + `src/prohibition-enforcement.cts` (≈43KB) and +> `gsd-core/references/prohibition-probe.md`. + +## Relationship to ADR-550 (read this first) + +ADR-550 is the **spec-phase probe contract**: what a prohibition *is*, how it is +represented (`SPEC.md` acceptance criterion ↔ `must_haves.prohibitions:`), and how it is +*tiered* (`test` vs `judgment`, Decisions 3–7). That ownership is unchanged. + +This ADR carves out and consolidates the **verify-time enforcement mechanism** for the +`test` tier — the `check prohibition-enforcement` producer in +`src/prohibition-enforcement.cts` — which ADR-550 only documents as a chain of dated +addenda. The boundary: + +| Concern | Owner | +|---------|-------| +| Prohibition representation, tiering, spec→plan projection | **ADR-550** (D3, D7) | +| Judgment-tier soft-gate / "never a silent pass" policy | **ADR-550** (D4) | +| Test-tier *enforcement producer* (locate → prove-fail-first → run → dispose) | **this ADR** | +| Capability/core-rail placement of the verifier↔predicate contract | **ADR-857** *"Verification substrate vs. plug-in tier (the predicate boundary)"* (decision #6), referenced by both | + +**Dedup proposal (decide at PR review):** on accepting this ADR, replace ADR-550's +2026-06-12 / #1259 / #1279 / #1346 / #1278 enforcement addenda with a one-line pointer to +this ADR, leaving 550 to own the contract and this ADR to own the mechanism. Until that is +agreed, 550's addenda remain authoritative and this ADR is non-binding. + +## Context + +ADR-550 D4 originally specified the `test` tier as a "hard gate in both interactive and +autonomous modes" but left the *mechanism* unspecified. As the prohibition probe shipped +(#644) and grew an enforcement producer (#1259→#1346), a set of load-bearing decisions had +to be made that are not derivable from the contract alone: + +- A generic producer cannot *trust* that a wired check actually fails on a violation. Caller + attestation (`failFirst: true`) is unfalsifiable at verify time and was a fake-green hole. +- A generic producer cannot *synthesize* a violation for an arbitrary check, so proving + fail-first requires an author-supplied known-bad subject. +- "The test went red" is not proof the *content* caused the red — an env-var-triggered or + load-crash red forges a green. +- The check descriptor must round-trip through the **flat** `parseMustHavesBlock` shared by + `truths`/`artifacts`/`key_links` without a parser rewrite that would regress those readers. +- A missing, partial, or un-provable check must **fail closed**, never silently pass — the + whole point of the tier. + +## Decision + +1. **No path greens on attestation alone.** A `test`-tier prohibition reaches + `passed`/`green` **only** when its wired check (a) genuinely, **non-vacuously** runs and + passes AND (b) is independently **machine-proven fail-first** against a known violation. + The enforcement producer (`runProhibitionEnforcement` in + `src/prohibition-enforcement.cts`) computes this as + `passed = proof.provenFailFirst === true && run.passed === true` and only then emits + non-empty `enforcementEvidence`. The disposition step + (`dispositionForProhibition` in `src/probe-core.cts`) then greens a `test`-tier item + **only** on that non-empty evidence; every other outcome — missing check, partial/invalid + descriptor, can't-prove, throws, times out, no violation source, passes-on-violation, + `located:false` — yields `{status:'unverified', flagged:true}` (`gaps_found`, never green) + in both interactive and autonomous modes. (The green rule and the fail-closed default are + intentionally split across the producer and the disposition so the disposition can fail + closed even when the producer never ran.) This is the standing form of ADR-550 D4's + guarantee. + +2. **Two wired-check kinds, one producer.** The producer accepts exactly two mechanisms: + - **`node-test`** — a `node --test` negative test that reports a real, **non-vacuous** + failing test. Two distinct vacuity guards apply: `isNonVacuousNodeTestRed` rejects a + load-crash red by requiring a failing test **named distinctly from the target file**; + `isNonVacuousNodeTestPass` rejects the empty-file "0 tests = pass" forgery on the + pass side. (Both live in `src/prohibition-enforcement.cts`.) + - **`lint-rule`** — a lint/AST rule run through the project flat config as + `eslint --format json` and filtered by `ruleId` (so `local/*` plugin rules load; a bare + `--rule` cannot). Invoked via `process.execPath` against the resolved eslint CLI, not a + bare `eslint` binary. Dogfooded on the in-tree `local/no-source-grep` rule. + +3. **Machine-proven fail-first via an author-supplied violation fixture.** Before a clean + pass can green, the producer runs the wired check against a **known-bad subject** and + requires RED. The subject is sourced from `violationFixture`: + - `lint-rule`: a file whose content violates `rule`; the rule id must appear in the JSON + report (the rule must have teeth). + - `node-test`: injected into the child as `GSD_PROHIB_SUBJECT=`; the + negative test reads that env var to locate its subject and must go RED against it. + - **Absent fixture → fail closed** (never attestation). Existence is checked + (`fs.existsSync(path.resolve(cwd, fixture))`) before spawning, symmetric with the + lint-rule path which fail-closes on a `< 1`-file result. + +4. **Causation control (opt-in).** A node-test red proves nothing about *why* it is red. An + optional `cleanFixture` runs the same negative test a second time with + `GSD_PROHIB_SUBJECT=` and requires **non-vacuous GREEN** + (`isNonVacuousNodeTestPass`) — so fail-first is proven only when the check is **RED on the + violation AND GREEN on the clean subject** (content-dependent red). Opt-in, not mandatory: + absent `cleanFixture`, behaviour matches the pre-#1346 zero-authoring compose path and the + "reds because the env var is set" case stays a documented residual for that one author's + check. The lint-rule kind needs no analog (its subject *is* the linted file; no env-var + indirection). + +5. **Deterministic locate via five flat scalars — never a nested object.** The wired-check + descriptor is authored at spec-phase and projected onto the `must_haves.prohibitions` + item as **five flat scalar keys**: `check_kind`, `check_target`, `check_rule` (lint-rule + only), `check_violation_fixture`, `check_clean_fixture` (optional). A nested `check: {}` + object is **rejected**: `parseMustHavesBlock` is a flat parser and its + `reconstructFrontmatter` serializer is lossy for nested object-lists, so a nested shape + would mangle the round-trip and risk the shared `truths`/`artifacts`/`key_links` readers. + `projectProhibitions` (in `src/probe-core.cts`) emits the scalars only for a well-formed + descriptor; `descriptorFromProjection` (in `src/prohibition-enforcement.cts`) reads them + back into the `{ kind, target, rule? }` `CheckDescriptor`. A prohibition authored with all + five scalars machine-proves fail-first and greens **end-to-end through the projection with + zero hand-authoring**. + +6. **`failFirst` is demoted, not removed (FF-08).** The `CheckDescriptor.failFirst` field is + kept for route-JSON backward-compat but **demoted to a non-authoritative hint** — the + machine prover supersedes it. Removal was rejected (breaks the route-JSON shape mid- + migration); demote-and-ignore satisfies "no path greens on attestation." + +7. **The contract is the CI surface, not the LLM.** Per ADR-550 D5, CI deterministically + tests parse/validate, the projection round-trip (fast-check property + CHK-03), the + fail-closed guards (CHK-06), and backward-compat (CHK-07) — never the model's judgment. + This ADR adds no CI claim over LLM behaviour. + +## Consequences + +- **Positive:** the verify-time enforcement subsystem has a single architecture-of-record + instead of five addenda on a spec-phase ADR; the "never a silent pass" guarantee is stated + once, completely, with its fail-closed defaults; the descriptor's flat-scalar shape and its + rationale are findable without reading the frontmatter parser. +- **Costs:** one more ADR to keep in sync with `src/prohibition-enforcement.cts`; the dedup + against ADR-550's addenda must actually be executed at PR time or the repo carries two + homes for the same decision (the explicit risk this ADR is meant to *remove*). +- **Open conventions (renamable at review, zero live consumers):** `GSD_PROHIB_SUBJECT` and + the `check_violation_fixture`/`check_clean_fixture` scalars have **no in-tree `node-test` + consumer** yet (the only live dogfood is the lint-rule `local/no-source-grep`; node-test + fail-first is exercised only by synthetic temp fixtures). A rename or an argv-for-env-var + swap is a mechanical zero-migration find/replace — surfaced here for the maintainer to + settle at review, exactly as #1278/#1279 were. (Hyrum's Law: this ADR deliberately marks + them as not-yet-depended-on so they remain changeable; the *scalar key names emitted by + `projectProhibitions` in shipped code* are, by contrast, already a contract.) +- **Boundary held:** canon security/compliance is referred to `/gsd:secure-phase` + eslint, + not minted here (ADR-550 D6); this ADR governs only bespoke product/values test-tier + enforcement. + +## Alternatives considered (rejected & deferred) + +Enforcement-side alternatives, each with the standing reason and a re-open condition. *(The +recall/representation/packaging-side alternatives — the withdrawn LLM classifier #652, a +deterministic recall engine, a `polarity` field on `truths`, and the deferred dispatcher CLI — +belong to the spec-phase contract and are recorded in ADR-550's "Alternatives considered.")* + +- **A nested `check: {}` descriptor object — REJECTED.** `parseMustHavesBlock` is a flat + parser and `reconstructFrontmatter` is lossy for nested object-lists, so a nested shape + would mangle the round-trip and could regress the shared `truths`/`artifacts`/`key_links` + readers. Hence the five **flat scalar** keys (Decision 5). *Re-open only if* + `parseMustHavesBlock` is replaced with a structured parser (its own ADR, with the full + shared-reader regression surface). +- **An inline producer-written violation snippet — REJECTED.** To machine-prove fail-first the + violation is an author-supplied **fixture path** (`check_violation_fixture`), not source the + producer writes inline, which would bake rule-specific source into a generic producer + (Decision 3). +- **`failFirst` caller attestation as authoritative — REJECTED → DEMOTED (FF-08).** Trusting + the caller's `failFirst: true` was an unfalsifiable fake-green hole; the machine prover + supersedes it and the field is demoted to a non-authoritative hint kept only for route-JSON + backward-compat (Decision 6). Outright removal was also rejected (breaks the route-JSON + shape mid-migration). +- **Mandatory causation control — REJECTED in favour of opt-in.** Requiring every node-test + prohibition to ship a `cleanFixture` would regress the zero-authoring compose path and + hard-gate every existing descriptor without one; the control is opt-in (Decision 4), leaving + one documented residual rather than breaking working checks. + +## Cross-references + +- **ADR-550** — spec-phase probe contract; this ADR consolidates its enforcement addenda, and + ADR-550 holds the recall/representation/packaging-side rejected alternatives. +- **ADR-857** — section *"Verification substrate vs. plug-in tier (the predicate boundary)"* + (decision #6): the verifier↔predicate contract lands on the **core verify rail** + (non-toggleable), never in `capabilities/`; this seam is its concrete enforcement instance. +- **`gsd-core/references/prohibition-probe.md`** — the portable runtime reference. +- **`docs/how-to/resolve-prohibition-findings.md`** — user-facing resolution guide. +- Code: `src/prohibition-enforcement.cts`, `src/probe-core.cts` (`projectProhibitions`), + `gsd-core/workflows/verify-phase.md`. Issues: #644, #1259, #1278, #1279, #1346.