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)
This commit is contained in:
Dave
10
.changeset/1279-machine-proven-fail-first.md
Normal file
10
.changeset/1279-machine-proven-fail-first.md
Normal file
@@ -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.
|
||||
@@ -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)
|
||||
|
||||
@@ -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=<violationFixture>` 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.
|
||||
|
||||
@@ -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=<violationFixture>` 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).
|
||||
|
||||
|
||||
@@ -76,7 +76,7 @@ Aggregate all must_haves across plans for phase-level verification.
|
||||
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, 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 `<request.json>` 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`).
|
||||
|
||||
|
||||
Reference in New Issue
Block a user