From 8cf4716c99a5fe63ce9c89f10f854fd60f94199a Mon Sep 17 00:00:00 2001 From: Dave Date: Mon, 15 Jun 2026 22:57:47 -0400 Subject: [PATCH] docs(#1279): ratify ADR-550 addendum + FEATURES/reference/verify-phase + changeset - ADR-550 dated 2026-06-15 addendum: machine-proven fail-first REALIZED (D5d CLOSED); ratify violationFixture, GSD_PROHIB_SUBJECT, failFirst demotion - FEATURES REQ-PROHIB-07 reads shipped (machine-proven, not caller-attested) - prohibition-probe reference + verify-phase descriptor shape updated with violationFixture + convention - tag GSD_PROHIB_SUBJECT + violationFixture PROPOSED/renamable (zero live consumers) as a PR-review flag - add .changeset/1279-machine-proven-fail-first.md (type: Changed) --- .changeset/1279-machine-proven-fail-first.md | 10 +++++ docs/FEATURES.md | 2 +- docs/adr/550-spec-phase-probe-contract.md | 16 ++++++++ gsd-core/references/prohibition-probe.md | 39 ++++++++++++++++---- gsd-core/workflows/verify-phase.md | 2 +- 5 files changed, 59 insertions(+), 10 deletions(-) create mode 100644 .changeset/1279-machine-proven-fail-first.md diff --git a/.changeset/1279-machine-proven-fail-first.md b/.changeset/1279-machine-proven-fail-first.md new file mode 100644 index 000000000..79b9d331c --- /dev/null +++ b/.changeset/1279-machine-proven-fail-first.md @@ -0,0 +1,10 @@ +--- +type: Changed +pr: TODO +--- + +**Test-tier prohibition fail-first is now MACHINE-PROVEN, not caller-attested** — the deferred literal `regression-must-fail-first` property of ADR-550 Decision 4 (the gap #1259 / PR #1273 left as a tracked follow-up) has landed. The `check prohibition-enforcement` producer (`src/prohibition-enforcement.cts`, compiled by `build:lib` to the gitignored `gsd-core/bin/lib/prohibition-enforcement.cjs`) no longer trusts the caller's `failFirst` attestation: before a clean, non-vacuous pass can dispose a `test`-tier prohibition green, the new `defaultProveFailFirst` prover independently RUNS the wired check against a KNOWN VIOLATION and confirms it goes RED. Attestation is gone from the green AND (`passed = proof.provenFailFirst === true && run.passed === true`); any other outcome — passes-on-violation, can't-prove, throws, times out, or no violation source — **hard-gates in BOTH interactive and autonomous modes** (ADR-550 D4 / D3). The evidence record gains a `failFirstProof` field recording HOW fail-first was proven (FF-07). A caller can no longer green a toothless check. + +The violation is sourced from a new descriptor field, **`CheckDescriptor.violationFixture`** — an author-supplied path to a known-bad subject. For a `lint-rule` the prover lints that fixture and requires the rule id to appear in the JSON report (the rule must have teeth); for a `node-test` the prover spawns the negative test with the subject injected through the **`GSD_PROHIB_SUBJECT`** env convention and requires the run to report `# fail >= 1` (the pure, mutation-pinned `isNodeTestRed` helper). The `lint-rule` path is fully shippable now and is dogfooded against the in-tree `local/no-source-grep` rule; the `node-test` path ships its mechanism (a fixture-bearing descriptor IS machine-proven) and is exercised by SYNTHETIC temp fixtures — there is no live in-tree `node --test` prohibition to dogfood. `CheckDescriptor.failFirst` is **DEMOTED, not removed** (FF-08): it is kept as a non-authoritative hint so the #1259 route-JSON shape and the `CheckDescriptor` type stay backward-compatible mid-migration, but no path greens on it alone. The green/fail-closed policy in `src/probe-core.cts` (`dispositionForProhibition`, reads only `evidence.length > 0`) is untouched; the evidence array shape is additive. This closes ADR-550's D5d follow-up — see the dated 2026-06-15 ADR-550 addendum. (#1279) + +**PR-review flag — `GSD_PROHIB_SUBJECT` + `violationFixture` are PROPOSED, renamable conventions.** Both are net-new surface with ZERO live in-tree consumers (no in-tree node-test prohibition yet; node-test proof runs only on synthetic test fixtures, the real dogfood stays the lint-rule). They are forward-looking scaffolding, so a later rename — or replacing the env var with an argv — is a mechanical, zero-migration find/replace. Surfacing them here so the maintainer can **ratify, rename, or replace them at PR review** with no migration cost, exactly as #1278's ADR addendum was reviewed at PR time. The `failFirst` demotion is likewise open to weighing outright removal; the keep-as-hint rationale is recorded in the ADR addendum. diff --git a/docs/FEATURES.md b/docs/FEATURES.md index 3d2ad7a5a..03ce0b358 100644 --- a/docs/FEATURES.md +++ b/docs/FEATURES.md @@ -3180,6 +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 caller-attested, genuinely-passing (non-vacuous) wired mechanical check (a `node --test` negative test OR a lint/AST rule) MUST dispose green and be satisfiable; a missing, non-attested, or non-passing check MUST hard-gate (flagged, non-green) in both interactive and autonomous modes (#1259, ADR-550 D5d — the enforcement half; machine-proven fail-first is tracked in #1279, deterministic descriptor auto-locate in #1278). +- REQ-PROHIB-07: A `test`-tier prohibition with a **machine-proven-fail-first**, genuinely-passing (non-vacuous) wired mechanical check (a `node --test` negative test OR a lint/AST rule) MUST dispose green and be satisfiable; a missing, un-provable, or non-passing check MUST hard-gate (flagged, non-green) in both interactive and autonomous modes. Fail-first is **machine-proven, not caller-attested** (#1279, ADR-550 D5d): before a clean pass greens, the producer independently runs the wired check against a known violation (the descriptor's `violationFixture`) and confirms it goes RED — a lint rule via the violating fixture, a node test via the violating subject injected through the `GSD_PROHIB_SUBJECT` convention; absent a violation source it fails closed, never falling back to attestation. (Enforcement half shipped #1259; deterministic descriptor auto-locate in #1278.) **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 b76ebf637..802439781 100644 --- a/docs/adr/550-spec-phase-probe-contract.md +++ b/docs/adr/550-spec-phase-probe-contract.md @@ -96,3 +96,19 @@ Decision 4 describes the `test`-tier as a "**Hard gate in both interactive and a 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 genuine-execution half — a test-tier prohibition with a passing, non-vacuous wired check can reach `green`/`passed`, and a missing/failing one hard-gates. The previously-unreachable green branch in `dispositionForProhibition()` is reachable from the live pipeline, and the fail-closed default backs every miss/fail. The one remaining gap to D4's literal intent — *machine-proven* fail-first — is documented above as a tracked follow-up. 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. + +## Addendum (2026-06-15, #1279) — machine-proven fail-first REALIZED (D5d follow-up CLOSED) + +The 2026-06-12 addendum above closed with one honest gap to D4's literal intent: `failFirst` was **caller-ATTESTED**, not machine-proven (the note at *"Honest scope"* and the *Net effect on D4* paragraph deferred the literal `regression-must-fail-first` property to #1279). **#1279 closes that follow-up.** The literal `regression-must-fail-first` property is now **machine-proven at verify time**: before a clean pass can dispose a `test`-tier prohibition green, the producer independently RUNS the wired check against a KNOWN VIOLATION and confirms it goes RED. Any other outcome (passes-on-violation, can't-prove, throws, times out, no violation source) **hard-gates in both modes** — attestation is gone from the green AND (`passed = proof.provenFailFirst === true && run.passed === true`). The previously-deferred half of D4's intent is therefore REALIZED; the D5d follow-up is **CLOSED**. The mechanism landed in `src/prohibition-enforcement.cts` (the `defaultProveFailFirst` real prover + the pure `isNodeTestRed` helper) and is compiled by `build:lib` to the gitignored `gsd-core/bin/lib/prohibition-enforcement.cjs`. + +This addendum ratifies three contract points: + +- **(a) `CheckDescriptor.violationFixture?` — the violation-sourcing shape.** An author-supplied path to a KNOWN-BAD subject the prover runs the check against. For `lint-rule`: a file whose content violates `rule` (the prover lints it and requires the rule id to appear in the JSON report — the rule must have teeth). For `node-test`: a subject the negative test exercises, expected to drive it RED. A generic producer cannot synthesize a violation for an arbitrary check, so the fixture is required to prove fail-first; **absent → the prover fails closed (never attestation).** This is the uniform field for BOTH kinds (the inline producer-written snippet was rejected as it bakes rule-specific source into a generic producer). + +- **(b) `GSD_PROHIB_SUBJECT` — the node-test subject-injection convention.** For the `node-test` kind the producer spawns the negative test with `GSD_PROHIB_SUBJECT=` in the child env; the test reads that env var to locate the subject-under-test and is expected to go RED against the violating subject. The synthetic temp fixtures in `tests/prohibition-enforcement.test.cjs` demonstrate a test that honors the convention (defaulting to a clean in-dir subject when the env var is absent, so the plain run passes non-vacuously while the prover's run goes red). + +- **(c) The `failFirst` DEMOTION (FF-08).** `CheckDescriptor.failFirst` is **kept** (so the #1259 route-JSON shape and the `CheckDescriptor` type stay backward-compatible for any caller mid-migration) but **DEMOTED to a non-authoritative hint** — the machine prover supersedes it and **no path greens on attestation alone**. Removal was rejected as it breaks the route-JSON shape mid-migration; demote-and-ignore is safer and still satisfies "no path greens on attestation." + +> **PR-review flag — PROPOSED, renamable conventions (zero live consumers).** Both **`GSD_PROHIB_SUBJECT`** and **`CheckDescriptor.violationFixture`** are net-new surface introduced by this PR with **ZERO live in-tree consumers** — there is no in-tree `node --test` prohibition yet (the #1259 dogfood anchor and the #1279 lint-rule dogfood are both the LINT-rule `local/no-source-grep`; node-test fail-first is exercised only by SYNTHETIC temp fixtures in tests). They are therefore forward-looking scaffolding, and a later rename (or replacing the env var with an argv) is a **mechanical, zero-migration find/replace**. They are surfaced here explicitly so the maintainer can **rename or replace them at PR review** — the natural ratification point, exactly as #1278's ADR addendum was reviewed at PR time — without any migration cost. The `failFirst` DEMOTION is likewise open to the reviewer weighing outright removal; the rationale for keeping it as a hint is recorded above. + +Net effect on D4: the *guarantee* ("a `test`-tier prohibition is never a silent pass") was preserved at every step — fail-closed-now (#644), genuine-execution (#1259), and now **machine-proven fail-first (#1279)**. A `test`-tier prohibition reaches `green`/`passed` ONLY when the wired check both genuinely, non-vacuously passes AND is independently proven to fail on a violation; every miss/fail/un-provable hard-gates. The decision also lives in `src/prohibition-enforcement.cts` comments, `gsd-core/references/prohibition-probe.md`, `gsd-core/workflows/verify-phase.md`, and the #1279 changeset. diff --git a/gsd-core/references/prohibition-probe.md b/gsd-core/references/prohibition-probe.md index 2cebfa403..605027b8d 100644 --- a/gsd-core/references/prohibition-probe.md +++ b/gsd-core/references/prohibition-probe.md @@ -112,15 +112,38 @@ lifecycle is identical to the edge-probe, the verification tiers differ): 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 + `check prohibition-enforcement` sub-command (#1259 + #1279, ADR-550 D5d): it locates the wired mechanical check (a `node --test` negative test OR a lint/AST rule run as - `eslint --format json` and filtered by `ruleId`), requires the caller-attested `failFirst` - marker, runs it for a genuine **non-vacuous** pass, and emits the - `dispositionForProhibition()` verdict. A passing wired check disposes **green** (satisfiable - → can reach `passed`); a missing, non-attested, or genuinely-non-passing check **hard-gates** - (flagged, never green → `gaps_found`) in BOTH interactive and autonomous modes — never a - silent pass. (`failFirst` is caller-attested, not yet machine-proven against a violation - fixture — a tracked follow-up; see ADR-550 D5d.) + `eslint --format json` and filtered by `ruleId`), **machine-proves it is fail-first** against a + known violation, runs it for a genuine **non-vacuous** pass, and emits the + `dispositionForProhibition()` verdict. A passing, fail-first-proven wired check disposes **green** + (satisfiable → can reach `passed`); a missing, un-provable, or genuinely-non-passing check + **hard-gates** (flagged, never green → `gaps_found`) in BOTH interactive and autonomous modes — + never a silent pass. + + **Machine-proven fail-first (#1279).** `failFirst` is now **machine-proven, not caller-attested**: + before a clean pass greens, the producer independently runs the wired check against a KNOWN + VIOLATION and confirms it goes RED (any other outcome — passes-on-violation, can't-prove, throws, + times out, no violation source — hard-gates). The violation is sourced from a descriptor field: + - **`violationFixture`** — an author-supplied path to a KNOWN-BAD subject. For `lint-rule`: a file + whose content violates `rule`; the prover lints it and requires the rule id to appear in the + JSON report (the rule must have teeth). For `node-test`: a subject the negative test exercises, + expected to drive it RED. + - **`GSD_PROHIB_SUBJECT`** — the node-test subject-injection convention: the producer spawns the + negative test with `GSD_PROHIB_SUBJECT=` in the child env; the test reads that + env var to locate its subject-under-test and is expected to go red against the violating subject. + - **lint-fixture authoring gotcha** — the violating fixture must actually trigger the rule. For the + `local/no-source-grep` dogfood anchor specifically, use the `path.join('lib','foo.cjs')` form + (a standalone quoted dir token); a single string literal like `'src/x.cjs'` does NOT trigger the + rule, so a mis-authored fixture makes the prover report "not proven" and hard-gate a legitimately + wired check. (`no-source-grep` has no filename guard — any `.cjs` with the pattern fires.) + + > **PROPOSED, renamable conventions (zero live consumers).** Both `GSD_PROHIB_SUBJECT` and + > `violationFixture` are net-new surface with **no live in-tree consumer yet** — there is no + > in-tree `node --test` prohibition; node-test fail-first proof is exercised only by SYNTHETIC + > temp fixtures in the tests, and the real dogfood remains the LINT-rule `local/no-source-grep`. + > They are therefore **open to maintainer adjustment (rename, or replacing the env var with an + > argv) at PR review with zero migration cost.** See the ADR-550 2026-06-15 addendum (#1279). - A **judgment**-tier prohibition routes to a never-silent / never-hard-halt soft gate (autonomous emits an `unverified-prohibition — human review recommended` flag). diff --git a/gsd-core/workflows/verify-phase.md b/gsd-core/workflows/verify-phase.md index fa556c2a8..c77fcb1ce 100644 --- a/gsd-core/workflows/verify-phase.md +++ b/gsd-core/workflows/verify-phase.md @@ -76,7 +76,7 @@ Aggregate all must_haves across plans for phase-level verification. gsd_run check prohibition-enforcement ``` - where `` carries `{ prohibition, check, mode }` — `check` being the wired mechanical-check descriptor `{ kind: 'node-test' | 'lint-rule', target, rule?, failFirst: true }`. For `node-test`, `target` is the negative-test file path; for `lint-rule`, `target` is the PATH to lint and `rule` is the eslint rule id (e.g. `local/no-source-grep`) — both required (a lint-rule without `rule` is not a valid wired check). The producer LOCATES the wired check, requires the caller-attested `failFirst` marker, RUNS it for a genuine non-vacuous pass, builds `enforcementEvidence`, and emits the `dispositionForProhibition()` verdict (#1259, ADR-550 D5d). (`failFirst` is caller-attested, not yet machine-proven against a violation fixture — a tracked follow-up.) Route the result by its typed fields: + where `` carries `{ prohibition, check, mode }` — `check` being the wired mechanical-check descriptor `{ kind: 'node-test' | 'lint-rule', target, rule?, violationFixture, failFirst? }`. For `node-test`, `target` is the negative-test file path; for `lint-rule`, `target` is the PATH to lint and `rule` is the eslint rule id (e.g. `local/no-source-grep`) — both required (a lint-rule without `rule` is not a valid wired check). `violationFixture` is the author-supplied path to a KNOWN-BAD subject the producer runs the check against to **machine-prove fail-first** (for `node-test`, injected via the `GSD_PROHIB_SUBJECT` env convention); `failFirst` is a DEMOTED, non-authoritative hint kept only for backward route-JSON shape (no path greens on it alone — FF-08). The producer LOCATES the wired check, **machine-proves it is fail-first** by running it against the violation and confirming it goes RED, RUNS it for a genuine non-vacuous pass, builds `enforcementEvidence`, and emits the `dispositionForProhibition()` verdict (#1259 + #1279, ADR-550 D5d). Fail-first is **machine-proven, not caller-attested** — absent a provable violation the producer fails closed, never falling back to attestation. Route the result by its typed fields: - **`status: 'green'`, `flagged: false`** (a genuinely-passing wired negative test / lint rule, `located: true`, non-empty `evidence`) → the item is satisfiable → it can reach **passed**. - **missing, non-attested, or genuinely-non-passing 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`).