diff --git a/.changeset/1279-machine-proven-fail-first.md b/.changeset/1279-machine-proven-fail-first.md new file mode 100644 index 000000000..3459c44f7 --- /dev/null +++ b/.changeset/1279-machine-proven-fail-first.md @@ -0,0 +1,10 @@ +--- +type: Changed +pr: 1314 +--- + +**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 a NON-VACUOUS red — `# fail >= 1` AND a failing test named distinctly from the file (`isNonVacuousNodeTestRed`), so a violation fixture that merely CRASHES the test at load is not mistaken for the negative assertion firing red (symmetric with the clean-pass non-vacuity guard). The node-test prover also requires the `violationFixture` to EXIST (resolved against `cwd`) before spawning — a missing/typo'd path fail-CLOSES rather than letting an honest test's ENOENT crash forge a green (symmetric with the lint path's file-result guard). The deterministic spec→verify path composes end-to-end: a fourth flat scalar **`check_violation_fixture`** is projected by `projectProhibitions` and read back by `descriptorFromProjection` (rides both kinds), so a prohibition authored with all four `check_*` scalars machine-proves fail-first and greens through the projection alone — zero hand-authoring at verify time (#1278 + #1279 + #1346; round-trip pinned by a fast-check property + CHK-03(D) + an end-to-end COMPOSE capstone). One documented residual remains under **#1346**: the node-test proof confirms the fixture exists and the check reds, but cannot generically prove the red was *caused by* the subject's content rather than by the env merely being set. 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 cdf2bf822..808a67b68 100644 --- a/docs/FEATURES.md +++ b/docs/FEATURES.md @@ -3182,6 +3182,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 1433af18c..805dd8251 100644 --- a/docs/adr/550-spec-phase-probe-contract.md +++ b/docs/adr/550-spec-phase-probe-contract.md @@ -97,6 +97,26 @@ Net effect on D4: the *guarantee* ("a `test`-tier prohibition is never a silent 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 node-test red proof requires a NON-VACUOUS red via `isNonVacuousNodeTestRed` — a failing test named distinctly from the file, so a load crash on the bad subject is not mistaken for the negative assertion firing red) 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. + +**Review corrections (#1314 maintainer review) — two soundness items:** +- **node-test fixture-existence guard (was fail-OPEN) — FIXED.** The node-test prover originally guarded only `if (!fixture)`. A missing/typo'd/stale `violationFixture` path made `GSD_PROHIB_SUBJECT` point at a non-existent file; an honest negative test then threw ENOENT *inside its callback* — a failing test named distinctly from the file — which `isNonVacuousNodeTestRed` accepted as proof, **forging a green from a setup crash** (asymmetric with the lint-rule path, which fail-CLOSES on `< 1` file result). Fixed by requiring `fs.existsSync(path.resolve(cwd, fixture))` before spawning (symmetric fail-closed; resolved against the producer's `cwd` to match the child's resolution). **Documented residual (#1346):** existence is necessary but not sufficient — a deceptive test that reds merely *because* `GSD_PROHIB_SUBJECT` is set (not because the subject's CONTENT violates) is still accepted; proving causation generically for an arbitrary author-supplied test is not possible, so it is recorded as a constraint, not implied-solved. +- **`violationFixture` projection source (#1278 ↔ #1279 now COMPOSE) — DELIVERED.** Initially `descriptorFromProjection` reconstructed only `{ kind, target, rule? }` and the projection carried no fixture, so a prohibition wired purely through the deterministic path always hard-gated. This PR threads a **fourth flat scalar `check_violation_fixture`** through `projectProhibitions` + `descriptorFromProjection` (rides both kinds; mirrors `CheckDescriptor.violationFixture`). A prohibition authored with all four scalars now **machine-proves fail-first and greens end-to-end through the projection alone** (zero hand-authoring) — the round-trip is pinned by a fast-check property + CHK-03(D) + an end-to-end COMPOSE capstone. Fail-closed is preserved: a descriptor with no `check_violation_fixture` (or a blank one) projects absent and hard-gates. The remaining work under #1346 is now just the node-test causation residual above. + ## Addendum (2026-06-15): optional `check` descriptor on the prohibition item — D3 shape extension (#1278) This ratifies the **deterministic SOURCE** for the test-tier `CheckDescriptor` that #1259 (PR #1273) left caller/verifier-supplied. #1259 shipped the PRODUCER (`check prohibition-enforcement`) that *runs* a wired check given a `{kind, target, rule?}` descriptor, but the descriptor itself was invented by the verify-phase LLM each run (the "locate" half). #1278 makes that locate half **deterministic**: an optional `check` descriptor is authored at spec-phase on the resolved `test`-tier prohibition, projected by `projectProhibitions`, and read back by verify-phase — so a wired, passing test closes the gap with **zero manual authoring**. This extends the **Decision 3 prohibition-item shape** (it adds optional keys to that item), so it is ratified here rather than rewriting D3 in place. diff --git a/eslint.config.mjs b/eslint.config.mjs index f9baa6efb..9f3df9be1 100644 --- a/eslint.config.mjs +++ b/eslint.config.mjs @@ -265,4 +265,19 @@ export default tseslint.config( 'no-irregular-whitespace': 'warn', }, }, + + // ── #1279 lint-rule fail-first fixture ────────────────────────────────────── + // `tests/_ff_lint_violation.cjs` is a PLAIN `.cjs` (NOT `*.test.cjs`) on purpose: it is a KNOWN + // `local/no-source-grep` violation that `defaultProveFailFirst` lints to machine-prove the rule + // has teeth, and it must stay OFF the `node --test` runner glob (executing it ENOENTs on the + // intentional `lib/foo.cjs` path). It still needs the `local` plugin registered so its inline + // `/* eslint-disable local/no-source-grep */` resolves (otherwise `eslint .` errors "rule not + // found") and the violation lands in `suppressedMessages` (which the prover reads), keeping the + // project's own `eslint .` green. (#1279) + { + files: ['tests/_ff_lint_violation.cjs'], + plugins: { local: localPlugin }, + languageOptions: { sourceType: 'commonjs', globals: { ...globals.node } }, + rules: { 'local/no-source-grep': 'error' }, + }, ); diff --git a/gsd-core/references/prohibition-probe.md b/gsd-core/references/prohibition-probe.md index e30ac4dc8..fa32c7f3b 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). @@ -128,33 +151,39 @@ Splitting these axes keeps the lifecycle enum free of a verification fact and le prohibition adapter declare `test | judgment` without forking the shared lifecycle enum that the edge-probe's `explicit | backstop` also uses. -## Optional wired-check descriptor (deterministic locate, #1278) +## Optional wired-check descriptor (deterministic locate + machine-proof, #1278 + #1346) A `resolved`/`test`-tier prohibition MAY carry an **optional `check` descriptor** that names the wired mechanical check, so verify-phase locates it deterministically instead of inventing `{kind, target, rule}` each run. The descriptor is captured at spec-phase (soft / optional — the author wires it when the negative test or lint rule already exists) and is represented as -**three flat scalar keys** on the `must_haves.prohibitions` item — never a nested `check: {}` +**four flat scalar keys** on the `must_haves.prohibitions` item — never a nested `check: {}` object: - `check_kind` — `node-test` | `lint-rule` (which producer mechanism runs the check). - `check_target` — the test file (`node-test`) or the file the rule runs against (`lint-rule`). - `check_rule` — the `ruleId` to filter on, **lint-rule only** (absent for `node-test`). +- `check_violation_fixture` — path to a KNOWN-BAD subject the #1279 prover runs the check against to + machine-prove fail-first (rides BOTH kinds; for `node-test` it is injected via `GSD_PROHIB_SUBJECT`). The flat-scalar shape is load-bearing: the shared `parseMustHavesBlock` is a flat parser and a nested object would flatten/mangle the round-trip (ADR-550 2026-06-15 addendum; #644 "no parser rewrite" precedent). `projectProhibitions` emits these keys **only for a well-formed descriptor** -(valid `check_kind` + non-empty `check_target`; `check_rule` only on the lint-rule path), and -verify-phase reads them back via `descriptorFromProjection` into the `CheckDescriptor` handed to -`check prohibition-enforcement`. A wired, passing test then closes the gap with **zero manual -descriptor authoring**. +(valid `check_kind` + non-empty `check_target`; `check_rule` only on the lint-rule path; +`check_violation_fixture` only when non-empty), and verify-phase reads them back via +`descriptorFromProjection` into the `CheckDescriptor` handed to `check prohibition-enforcement`. This +closes **both** the locate (#1278) and the machine-proof-fixture (#1346) halves with **zero manual +descriptor authoring**: a prohibition authored with all four scalars greens end-to-end through the +projection alone. **Fail-closed + backward-compat.** A partial descriptor (`lint-rule` missing `check_rule`), an -unknown `check_kind`, or an **absent** descriptor on a test-tier prohibition falls through to the -producer's existing fail-closed locate — never a silent green. A prohibition with no descriptor -parses and disposes byte-identically to today. `failFirst` is **not** sourced from the -descriptor — it stays a verify-time caller attestation (machine-proven fail-first is tracked in -#1279; the `dispositionForProhibition` policy is unchanged). +unknown `check_kind`, an **absent** descriptor, OR a descriptor with **no `check_violation_fixture`** +falls through to the producer's fail-closed paths (`located: false`, or located-but-unprovable) — +never a silent green. A prohibition with no descriptor parses and disposes byte-identically to today. +`failFirst` is **not** sourced from the descriptor and is **demoted** (machine-proven fail-first +DELIVERED in #1279 — no path greens on attestation alone, FF-08); the `dispositionForProhibition` +policy is unchanged. Residual (tracked **#1346**): the node-test proof confirms the fixture exists and +the check goes RED, but cannot generically prove the red was *caused by* the subject's content. ## Output schema diff --git a/gsd-core/workflows/spec-phase.md b/gsd-core/workflows/spec-phase.md index 7a6d49bde..22ec44c2b 100644 --- a/gsd-core/workflows/spec-phase.md +++ b/gsd-core/workflows/spec-phase.md @@ -365,11 +365,16 @@ For each Requirement gathered so far, run the two-stage recall→precision pass: - `check_target` — the negative-test file path (for `node-test`), or the path to lint (for `lint-rule`). - `check_rule` — the eslint rule id (e.g. `local/no-source-grep`); `lint-rule` only. + - `check_violation_fixture` (#1346) — path to a KNOWN-BAD subject the wired check is run + against to **machine-prove fail-first**; rides BOTH kinds. Capture it to let the item green + end-to-end with zero hand-authoring at verify time; for `node-test` the negative test should + read its subject from the `GSD_PROHIB_SUBJECT` env var so the prover can inject this fixture. This is a **SOFT capture (CHK-04): a `test`-tier prohibition WITHOUT a descriptor is still allowed** — if the author cannot yet name the wired check, leave the descriptor empty and proceed. It is NOT a hard authoring block; the item simply stays fail-closed/flagged - downstream (an absent/partial descriptor → `descriptorFromProjection` null/under-specified - → producer fail-closed locate, never green). Do NOT capture `failFirst` here — it is a + downstream (an absent/partial descriptor — or one with no `check_violation_fixture` — + → `descriptorFromProjection` null/under-specified/fixture-less → producer fail-closed + locate-or-unprovable, never green). Do NOT capture `failFirst` here — it is a verify-time caller attestation, not a spec-authored field (#1279). - **Dismiss (reason)** → mark `dismissed` with a REQUIRED non-empty reason (PROB-05). The reason string is the audit trail; silence is not a valid dismissal. @@ -390,8 +395,8 @@ For each Requirement gathered so far, run the two-stage recall→precision pass: written (test or judgment tier); otherwise leave `unresolved`. **`--auto` NEVER auto-dismisses a prohibition** — a wrong dismissal is the exact silent failure this probe eliminates (PROB-06, the load-bearing safety property). On a `test`-tier auto-resolution, capture the `check_kind` / -`check_target` / `check_rule` descriptor **only when a wired check is unambiguous**; otherwise -leave it empty — `--auto` NEVER fabricates a check path (a wrong locate is re-validated and +`check_target` / `check_rule` / `check_violation_fixture` descriptor **only when a wired check is unambiguous**; otherwise +leave it empty — `--auto` NEVER fabricates a check path or fixture (a wrong locate is re-validated and fails closed at the producer, but a fabricated path is still noise to avoid). Log: `[auto] prohibitions: R resolved, U unresolved`. @@ -402,8 +407,8 @@ runs identically for non-Claude / text-mode hosts. Populate the `## Prohibitions` section of SPEC.md from the resolved prohibitions (each `resolved`/`test` row is a checkable negative acceptance criterion; `resolved`/`judgment` rows route to judgment review; `⚠ UNRESOLVED` rows are flagged as assumptions). A -`resolved`/`test` row ALSO carries its captured `check_kind` / `check_target` / `check_rule` -descriptor when present (so the projection feeds `verify-phase`'s deterministic locate, #1278); +`resolved`/`test` row ALSO carries its captured `check_kind` / `check_target` / `check_rule` / +`check_violation_fixture` descriptor when present (so the projection feeds `verify-phase`'s deterministic locate + machine-proof, #1278 + #1346); a `test` row with no captured descriptor is still valid — it stays fail-closed/flagged downstream rather than blocking authoring. diff --git a/gsd-core/workflows/verify-phase.md b/gsd-core/workflows/verify-phase.md index 0fbdc4ff2..c8335ddc9 100644 --- a/gsd-core/workflows/verify-phase.md +++ b/gsd-core/workflows/verify-phase.md @@ -70,17 +70,17 @@ 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 → 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 builds `request.check` **DETERMINISTICALLY from the projected descriptor** — it does NOT invent `{ kind, target, rule }`. Read the flat scalar keys `check_kind` / `check_target` / `check_rule` off the `must_haves.prohibitions` item and reconstruct the `CheckDescriptor` via the `descriptorFromProjection` adapter in `prohibition-enforcement` (`descriptorFromProjection(projectedItem)` → `{ kind: check_kind, target: check_target, rule?: check_rule }`). Then attest `failFirst: true` in the request — `failFirst` is the ONE field NOT sourced from the projection; it stays a verify-time caller attestation (#1279 machine-proves it against a violation fixture). Invoke the producer (CLI surface unchanged): +- **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 builds `request.check` **DETERMINISTICALLY from the projected descriptor** — it does NOT invent `{ kind, target, rule }`. Read the flat scalar keys `check_kind` / `check_target` / `check_rule` / `check_violation_fixture` off the `must_haves.prohibitions` item and reconstruct the `CheckDescriptor` via the `descriptorFromProjection` adapter in `prohibition-enforcement` (`descriptorFromProjection(projectedItem)` → `{ kind: check_kind, target: check_target, rule?: check_rule, violationFixture?: check_violation_fixture }`). The `violationFixture` (a path to a KNOWN-BAD subject) is the field that gates **green** and it is **now projected** (`check_violation_fixture`, #1346) — so a prohibition authored with all four scalars greens through the projection alone, **zero hand-authoring at verify time**. Do NOT rely on `failFirst`: it is DEMOTED (#1279) and greens nothing on its own; an item with no projected fixture hard-gates fail-closed. Invoke the producer (CLI surface unchanged): ```bash 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 }`, with `kind`/`target`/`rule` now sourced from the projected `check_*` scalars (not author/verifier invention) and `failFirst` caller-attested. For `node-test`, `target` (from `check_target`) is the negative-test file path; for `lint-rule`, `target` is the PATH to lint and `rule` (from `check_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). 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? }`, with `kind`/`target`/`rule`/`violationFixture` now sourced from the projected `check_*` scalars (not author/verifier invention — #1278 + #1346). For `node-test`, `target` (from `check_target`) is the negative-test file path; for `lint-rule`, `target` is the PATH to lint and `rule` (from `check_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` (from `check_violation_fixture`) is the 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 — #1279); `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 from the projection, **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 + #1278 + #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`). - > **Descriptor source — deterministic locate (#1278, DELIVERED).** The `check` descriptor's `{ kind, target, rule }` is now sourced **deterministically from the projected `check_kind` / `check_target` / `check_rule` scalars** on the `must_haves.prohibitions` item (authored at `/gsd:spec-phase`, projected by `projectProhibitions`, read back via the `descriptorFromProjection` adapter). So a wired passing test closes the gap with **zero manual descriptor authoring** — the verifier no longer invents the locate (removing the spoofable invent-at-verify-time surface; ADR-857 §147 exogenous grading). **Fail-closed is preserved:** an item with NO projected descriptor — or a PARTIAL one (e.g. a `lint-rule` missing `check_rule`) — makes `descriptorFromProjection` return `null` / an under-specified descriptor, which falls through to the producer's existing fail-closed LOCATE (`located: false`) → flagged-unverified, NEVER green, in BOTH modes. The only field still attested at verify time (not projected) is `failFirst`; machine-proving it against a violation fixture is the remaining **tracked follow-up: #1279**. + > **Descriptor source — deterministic locate + machine-proof compose (#1278 + #1346, DELIVERED).** The `check` descriptor's `{ kind, target, rule, violationFixture }` is now sourced **deterministically from the projected `check_kind` / `check_target` / `check_rule` / `check_violation_fixture` scalars** on the `must_haves.prohibitions` item (authored at `/gsd:spec-phase`, projected by `projectProhibitions`, read back via the `descriptorFromProjection` adapter). So both halves close with **zero manual descriptor authoring** — the verifier neither invents the locate (#1278) nor hand-supplies the violation fixture (#1346): a prohibition authored with all four scalars machine-proves fail-first and greens end-to-end through the projection alone (removing the spoofable invent-at-verify-time surface; ADR-857 §147 exogenous grading). **Fail-closed is preserved:** an item with NO projected descriptor, a PARTIAL one (e.g. a `lint-rule` missing `check_rule`), OR a descriptor with **no `check_violation_fixture`** makes `descriptorFromProjection` return `null` / an under-specified or fixture-less descriptor, which falls through to the producer's fail-closed paths (`located: false`, or located-but-unprovable) → flagged-unverified, NEVER green, in BOTH modes. `failFirst` is demoted and greens nothing on its own (#1279, FF-08). Residual (tracked **#1346**): the node-test proof confirms the fixture exists and the check goes RED, but cannot generically prove the red was *caused by* the subject's content vs the env merely being set. **Option B: Use Success Criteria from ROADMAP.md** diff --git a/src/probe-core.cts b/src/probe-core.cts index 7a924fe94..bbac605c9 100644 --- a/src/probe-core.cts +++ b/src/probe-core.cts @@ -299,6 +299,10 @@ export interface Prohibition { check_kind?: 'node-test' | 'lint-rule'; check_target?: string; check_rule?: string; + // Optional 4th flat scalar (#1346): the path to a KNOWN-BAD subject the #1279 prover runs the check + // against to MACHINE-PROVE fail-first. Projected only alongside a well-formed descriptor; absent -> + // the producer hard-gates (green requires a fixture). Mirrors `CheckDescriptor.violationFixture`. + check_violation_fixture?: string; } /** @@ -376,6 +380,13 @@ export function projectProhibitions( if (kind === 'lint-rule' && typeof p.check_rule === 'string' && p.check_rule.trim() !== '') { entry.check_rule = String(p.check_rule); } + // `check_violation_fixture` (#1346) rides BOTH kinds — it's what the #1279 prover machine-proves + // fail-first against. Emit ONLY a non-empty fixture (a blank one projects absent so green still + // hard-gates downstream — never a partial green); meaningless without the descriptor, so it lives + // inside this well-formed-descriptor branch. + if (typeof p.check_violation_fixture === 'string' && p.check_violation_fixture.trim() !== '') { + entry.check_violation_fixture = String(p.check_violation_fixture); + } } out.push(entry); } diff --git a/src/prohibition-enforcement.cts b/src/prohibition-enforcement.cts index d0bf84a2b..6a5e5e2fa 100644 --- a/src/prohibition-enforcement.cts +++ b/src/prohibition-enforcement.cts @@ -18,12 +18,14 @@ * (flagged, non-green) in BOTH interactive and autonomous modes (ADR-550 D4 / D3) — never a silent * green. * - * FAIL-FIRST IS CALLER-ATTESTED (honest scope, #1259): the producer requires the caller to ATTEST - * `failFirst: true` AND requires the runner to observe a real non-vacuous pass — but it does NOT - * independently prove the check fails-on-violation. Genuine fail-first confirmation needs running - * the check against a known violation fixture and is a tracked follow-up (recorded in ADR-550's D5d - * note). What ships here closes the permanent-`gaps_found` dead-end with a genuinely-executed gate; - * it does not yet replace caller attestation with machine proof of the red-first property. + * FAIL-FIRST IS MACHINE-PROVEN (#1279): the producer no longer greens on caller attestation. The + * green verdict requires the injectable prover (`proveFailFirst`, default `defaultProveFailFirst`) to + * INDEPENDENTLY run the check against a known violation fixture and observe it go red, AND the runner + * to observe a real non-vacuous pass: `passed = proof.provenFailFirst === true && run.passed === true`. + * Caller attestation (`CheckDescriptor.failFirst`) is demoted to a non-authoritative hint kept only + * for backward route-JSON shape — no path greens on it alone (FF-08). The proof method is recorded in + * the evidence (`failFirstProof`, FF-07). This replaces the #1259 caller-attested red-first property + * with machine proof, closing the gap the ADR-550 D5d note tracked as a follow-up. * * Authored as strict TypeScript (`src/prohibition-enforcement.cts`) and compiled by * `tsc -p tsconfig.build.json` (`npm run build:lib`) to the gitignored runtime artifact @@ -56,14 +58,24 @@ export type CheckKind = 'node-test' | 'lint-rule'; * runner family; `target` is the negative-test file path (node-test) or the PATH to lint * (lint-rule); `rule` is the eslint rule id (lint-rule only — e.g. `local/no-source-grep`) and is * REQUIRED for the lint-rule kind (a lint-rule descriptor without it is not a valid wired check); - * `failFirst` is the caller's ATTESTATION that the check is a genuine `regression-must-fail-first` - * proof (caller-declared — see the module docstring; not independently confirmed at verify time). + * `failFirst` is a DEMOTED, non-authoritative hint kept only for backward route-JSON shape — the + * machine prover (`proveFailFirst`) supersedes it, and NO path greens on attestation alone (FF-08, + * #1279). The descriptor's `violationFixture` is what the prover actually uses to prove fail-first. */ export interface CheckDescriptor { kind: CheckKind; target: string; rule?: string; failFirst?: boolean; + /** + * Author-supplied path to a KNOWN-BAD subject the prover runs the check against to machine-prove + * the check is fail-first (#1279). For `lint-rule`: a file whose content violates `rule` (the + * prover lints it and requires the rule id to appear). For `node-test`: a subject the negative + * test exercises via the `GSD_PROHIB_SUBJECT` env convention, expected to drive the test RED. + * A generic producer cannot synthesize a violation for an arbitrary check, so this is required to + * prove fail-first; ABSENT for node-test → the default prover fails closed (never attestation). + */ + violationFixture?: string; } /** @@ -78,7 +90,8 @@ export interface CheckDescriptor { * - `null`/`undefined`/non-object input -> `null`. * - `check_kind` ABSENT -> `null` (no descriptor -> producer locates nothing -> fail-closed). * - `check_kind` present -> `{ kind: check_kind, target: check_target }`, adding `rule: check_rule` - * ONLY when `check_rule` is a non-empty string. + * ONLY when `check_rule` is a non-empty string, and `violationFixture: check_violation_fixture` + * ONLY when that scalar is a non-empty string (#1346 — composes #1278 locate with #1279 proof). * - `failFirst` is NEVER sourced from the projection — it stays a verify-time caller attestation * (#1279 machine-proves it; out of scope here). The returned descriptor carries no `failFirst`. * - The adapter does NOT strictly validate kind/target/rule: it faithfully reconstructs whatever @@ -109,15 +122,21 @@ export function descriptorFromProjection( const rule = scalar(projected.check_rule); if (rule.trim().length > 0) descriptor.rule = rule; } + // `violationFixture` (#1346) rides BOTH kinds — reconstruct it from `check_violation_fixture` so the + // deterministic #1278 locate path and the #1279 machine-proof COMPOSE: a projected fixture lets the + // default prover green end-to-end with zero hand-authoring. Absent/blank -> no fixture -> the prover + // hard-gates (fail-closed; green requires a fixture), never fabricated. + const fixture = scalar(projected.check_violation_fixture); + if (fixture.trim().length > 0) descriptor.violationFixture = fixture; return descriptor; } /** * The result a check-runner returns: whether the check genuinely, non-vacuously PASSED. The runner - * reports only what it can OBSERVE (a real pass) — it does NOT determine fail-first. Whether the - * check is a `regression-must-fail-first` proof is a CALLER-ATTESTED property of the descriptor - * (`CheckDescriptor.failFirst`); the producer cannot independently confirm it at verify time without - * a violation fixture (a tracked follow-up — see the module docstring). + * reports only what it can OBSERVE (a real clean pass) — it does NOT determine fail-first. Whether the + * check is a `regression-must-fail-first` proof is now MACHINE-PROVEN by the separate `proveFailFirst` + * seam (#1279), which runs the check against the descriptor's `violationFixture` and observes it go + * red — not the caller's word (`CheckDescriptor.failFirst` is a demoted, non-authoritative hint). */ export interface CheckRunResult { passed: boolean; @@ -128,14 +147,38 @@ export interface EnforcementEvidence { kind: CheckKind; target: string; rule?: string; + /** Machine-proven fail-first (#1279): true ONLY when the prover observed the check go red on a + * violation. No longer the caller's attestation — a green item always carries a proven `true`. */ failFirst: boolean; passed: boolean; + /** HOW fail-first was machine-proven (FF-07) — recorded from the proof result for provenance. + * Additive; keeps the array shape `dispositionForProhibition` reads stable. */ + failFirstProof?: FailFirstProof['method']; +} + +/** + * The result of machine-proving a check is fail-first (#1279). `provenFailFirst` is true ONLY when + * the prover independently ran the check against a KNOWN VIOLATION and observed it go red (lint rule + * flags the violation / negative test fails). `method` records HOW it was proven, for evidence + * provenance. Any un-provable outcome (no fixture, toothless rule, throw, timeout) → `provenFailFirst: + * false` (fail-closed) so attestation can never silently green a toothless check. + */ +export interface FailFirstProof { + provenFailFirst: boolean; + method?: 'violation-fixture'; } /** Injectable options for `runProhibitionEnforcement` (defaults wire to the real runner). */ export interface EnforcementOptions { /** Runs the located check; injected in tests so no real subprocess is spawned. */ runCheck?: (check: CheckDescriptor) => CheckRunResult; + /** + * Machine-proves the located check is fail-first by running it against the descriptor's + * `violationFixture` and confirming it goes red (#1279). Injected in tests so no real subprocess is + * spawned; defaults to the real `defaultProveFailFirst`. Mirrors the `runCheck` seam. Plan 03 wires + * the result into the green decision; this plan only constructs the prover. + */ + proveFailFirst?: (check: CheckDescriptor) => FailFirstProof; /** Verify mode — recorded for transparency; the hard-gate applies in BOTH modes (ADR-550 D4). */ mode?: string; /** Project root for the default real runner (defaults to process.cwd()). */ @@ -208,6 +251,17 @@ export function parseNodeTestSummary(out: string): { tests: number; pass: number }; } +/** + * Pure: did a `node --test` run go RED on the violation fixture? True iff the TAP summary reports at + * least one failure (`# fail >= 1`). The default node-test prover requires this — a negative test + * that does NOT go red against a known-bad subject is toothless and must not prove fail-first. + * Mutation-pinned (`>= 1` boundary): a mutant flipping `>=`→`>` (or the threshold) is caught by the + * `# fail 1` unit case. An unparseable summary yields `fail: 0` → false (fail-closed for the prover). + */ +export function isNodeTestRed(out: string): boolean { + return parseNodeTestSummary(out).fail >= 1; +} + /** The names of REAL (run) tests from TAP `ok N - ` / `not ok N - ` lines. A line with a * `# SKIP` / `# TODO` directive is EXCLUDED — a skipped/todo negative test never executed, so it must * not count toward non-vacuity (#1259 m1). */ @@ -247,6 +301,40 @@ export function isNonVacuousNodeTestPass(out: string, target: string): boolean { return tapTestNames(out).some((n) => baseOf(n) !== tgtBase); } +/** The names of FAILING (run) tests from TAP `not ok N - ` lines, excluding `# SKIP`/`# TODO` + * directives (a skipped/todo line never ran). The fail-first analog of `tapTestNames`. */ +export function tapFailedTestNames(out: string): string[] { + if (typeof out !== 'string') return []; + const names: string[] = []; + const re = /^not ok \d+ - (.+)$/gm; + let m: RegExpExecArray | null; + while ((m = re.exec(out)) !== null) { + const rest = m[1]; + if (/\s#\s*(?:SKIP|TODO)\b/i.test(rest)) continue; // skipped/todo did not run + names.push(rest.replace(/\s+#\s.*$/, '').trim()); + } + return names; +} + +/** + * A NON-VACUOUS node-test RED — the fail-first proof analog of `isNonVacuousNodeTestPass`. True iff + * the run reports `# fail >= 1` AND at least one FAILING test is named DISTINCTLY from the target file. + * + * Why the distinct-name guard: a violation fixture that makes the negative test CRASH at load + * (ENOENT / throw-on-require / syntax error) emits a FILE-NAMED `not ok 1 - ` with `# fail 1`. + * That is a crash, NOT the negative assertion firing red — so it must not "prove" the test is a + * regression guard (the RED-side mirror of the BL-01 vacuity hole on the pass side). Requiring a + * failing test named distinctly from the file closes that hole, symmetric with the clean-pass guard. + * + * KNOWN CONSTRAINT (fail-closed, not a hole): a negative test whose `test('...')` name is EXACTLY its + * own file basename is conservatively rejected — same benign authoring constraint, same safe direction. + */ +export function isNonVacuousNodeTestRed(out: string, target: string): boolean { + if (!isNodeTestRed(out)) return false; // no `# fail >= 1` summary -> not red (fail-closed) + const tgtBase = baseOf(target); + return tapFailedTestNames(out).some((n) => baseOf(n) !== tgtBase); +} + /** Number of file results in an eslint `--format json` report (0 if unparseable / not an array). */ export function eslintFileResultCount(jsonText: string): number { try { @@ -309,7 +397,8 @@ export function eslintJsonHasRule(jsonText: string, rule: string): boolean { /** * The default REAL check runner (used when no `runCheck` is injected). Reports only an OBSERVED, * genuinely-non-vacuous pass; guarded so a missing tool / non-zero exit yields a non-passing result, - * NEVER an uncaught throw (the no-throw contract). It does NOT determine fail-first (caller-attested). + * NEVER an uncaught throw (the no-throw contract). It does NOT determine fail-first — that is the + * separate `proveFailFirst` seam's job (machine-proven against the violation fixture, #1279). * - node-test: runs `node --test` (TAP) and requires a NON-VACUOUS pass (>=1 test, >=1 pass, 0 fail * AND a reported test named distinctly from the file). A bare exit 0 for an empty/zero-test file * — which `node --test` counts as one passing "test" named after the file — is NOT a pass (the @@ -406,18 +495,118 @@ function defaultRunCheck(check: CheckDescriptor, cwd: string, timeoutMs?: number } /** - * LOCATE -> CONFIRM fail-first -> RUN -> build enforcementEvidence -> dispositionForProhibition. + * The default REAL fail-first prover (#1279; used when no `proveFailFirst` is injected). It runs the + * wired check against the descriptor's `violationFixture` (a KNOWN-BAD subject) and requires it to go + * RED — the machine proof that replaces caller attestation. Like `defaultRunCheck`, it is the + * impure/injectable seam (spawns eslint / `node --test`), reuses the identical bounded-subprocess + * machinery (`childEnv`/`posTimeout`/`CHECK_MAX_BUFFER`, `execFileSync(process.execPath, …)`, arg + * arrays → no shell), and NEVER throws — every un-provable path returns `{ provenFailFirst: false }`. + * + * - lint-rule: lint the `violationFixture` via the project flat config (so `local/*` plugins load) + * and require the target to actually lint (>=1 file result) AND no fatal/parse error AND the rule + * id to appear in the report (messages OR suppressedMessages — an inline-disabled violation still + * proves the rule has teeth, #1259 B1). Absent fixture / unresolvable eslint → not proven. + * - node-test: spawn the negative test (TAP) with `GSD_PROHIB_SUBJECT` set to the `violationFixture` + * — the CONVENTION (#1279) by which a negative test reads its subject-under-test — and require a + * NON-VACUOUS red (`isNonVacuousNodeTestRed`: `# fail >= 1` AND a failing test named distinctly + * from the file, so a load-CRASH on the bad subject is not mistaken for the assertion firing red). + * A toothless test that passes anyway → not proven. Absent fixture → not proven (fail-closed; + * NEVER falls back to attestation). + */ +function defaultProveFailFirst(check: CheckDescriptor, cwd: string, timeoutMs?: number): FailFirstProof { + try { + if (check.kind === 'lint-rule') { + const fixture = check.violationFixture; + if (!fixture) return { provenFailFirst: false }; // can't prove without a known violation -> hard-gate + const eslintCli = resolveEslintCli(cwd); + if (!eslintCli) return { provenFailFirst: false }; // eslint not installed -> fail closed, never throw + let json = ''; + try { + json = execFileSync(process.execPath, [eslintCli, ...buildLintArgs({ ...check, target: fixture })], { + cwd, + encoding: 'utf-8', + stdio: ['ignore', 'pipe', 'pipe'], + windowsHide: true, + env: childEnv(), + timeout: posTimeout(timeoutMs, ESLINT_TIMEOUT_MS), + maxBuffer: CHECK_MAX_BUFFER, + }); + } catch (e) { + // eslint exits non-zero on any error; the JSON report is still on stdout. A timeout/kill + // leaves no parseable JSON -> eslintHasFatalError(unparseable) -> not proven (fail-closed). + const stdout = e && typeof e === 'object' && 'stdout' in e ? (e as { stdout?: unknown }).stdout : ''; + json = typeof stdout === 'string' ? stdout : ''; + } + // Proven iff: the fixture actually linted (>=1 file result), the rule RAN (no fatal/parse + // error), and the rule id appears (the violation was flagged -> the rule has teeth). + const proven = eslintFileResultCount(json) >= 1 + && !eslintHasFatalError(json) + && eslintJsonHasRule(json, check.rule as string); + return { provenFailFirst: proven, method: 'violation-fixture' }; + } + if (check.kind === 'node-test') { + const fixture = check.violationFixture; + // Fail-CLOSED on a missing/typo'd/stale fixture path, SYMMETRIC with the lint-rule path's + // `eslintFileResultCount >= 1` guard. Without the existence check, a non-existent fixture makes + // `GSD_PROHIB_SUBJECT` point at a missing file; an honest negative test reading that subject + // throws ENOENT *inside its callback* — a failing test named DISTINCTLY from the file, which + // `isNonVacuousNodeTestRed` would accept as proof. That is fail-OPEN: a typo forges a green from + // a setup crash, not from the prohibition firing. Requiring the fixture to exist before spawning + // closes the realistic typo/stale-path case (#1279 review, Major 1). + // + // KNOWN RESIDUAL (documented, fail-open direction, tracked follow-up #1346): existence is + // necessary but not sufficient — a deliberately deceptive negative test that reds merely BECAUSE + // `GSD_PROHIB_SUBJECT` is set (rather than because the subject's CONTENT violates the must-NOT) + // is still accepted. Proving "the red was CAUSED BY the violation" cannot be done generically for + // an arbitrary author-supplied test, so it is recorded as a constraint, not silently implied-solved. + // Resolve the fixture against `cwd` (NOT the verify process's cwd): the spawned test reads + // `GSD_PROHIB_SUBJECT` and resolves a relative subject against `cwd`, so the existence check must + // use the SAME base or it could pass here yet ENOENT in the child (re-opening the fail-open hole). + if (!fixture || !fs.existsSync(path.resolve(cwd, fixture))) return { provenFailFirst: false }; + let out = ''; + try { + out = execFileSync(process.execPath, buildNodeTestArgs(check), { + cwd, + encoding: 'utf-8', + stdio: ['ignore', 'pipe', 'pipe'], + windowsHide: true, + // CONVENTION (#1279): the negative test reads its subject-under-test from this env var. + env: { ...childEnv(), GSD_PROHIB_SUBJECT: fixture }, + timeout: posTimeout(timeoutMs, NODE_TEST_TIMEOUT_MS), + maxBuffer: CHECK_MAX_BUFFER, + }); + } catch (e) { + // A negative test that goes RED exits non-zero; the partial TAP (with the `# fail` summary) + // is on stdout. Parse what we have: a real failure here is the PROOF the test is fail-first. + const stdout = e && typeof e === 'object' && 'stdout' in e ? (e as { stdout?: unknown }).stdout : ''; + out = typeof stdout === 'string' ? stdout : ''; + } + return { provenFailFirst: isNonVacuousNodeTestRed(out, check.target), method: 'violation-fixture' }; + } + // Unknown kind — defensive; the LOCATE guard already rejects it. + return { provenFailFirst: false }; + } catch { + return { provenFailFirst: false }; + } +} + +export { defaultProveFailFirst }; + +/** + * LOCATE -> PROVE fail-first -> RUN -> build enforcementEvidence -> dispositionForProhibition. * * (1) LOCATE: if no well-formed check descriptor is locatable -> fail-closed * (`dispositionForProhibition` with empty evidence) plus `{ located: false, kind: null, evidence: [] }`. - * (2) ATTEST + RUN: require the caller to attest `failFirst: true` and run it via `runCheck`. A check - * the caller does not attest as fail-first, or that does not genuinely (non-vacuously) PASS -> - * fail-closed disposition with `located: true` (a real located miss, non-green, flagged) in BOTH - * modes. Fail-first is caller-attested, not independently proven (see module docstring). - * (3) PASS: build a typed `enforcementEvidence` array and call `dispositionForProhibition` — the - * non-empty array flips a test-tier item to green (the previously-unreachable branch). + * (2) PROVE + RUN: machine-prove fail-first via `proveFailFirst` (default `defaultProveFailFirst`) AND + * run the check via `runCheck`. The green AND is `proof.provenFailFirst === true && run.passed === + * true` — caller attestation is NOT consulted (FF-08). A check that cannot be proven fail-first, or + * that does not genuinely (non-vacuously) PASS -> fail-closed disposition with `located: true` (a + * real located miss, non-green, flagged) in BOTH modes. + * (3) PASS: build a typed `enforcementEvidence` array (recording the proof method) and call + * `dispositionForProhibition` — the non-empty array flips a test-tier item to green. * - * Pure/deterministic: same (prohibition, check, runCheck) -> same result. + * Pure/deterministic DECISION layer: the only impure seams are the injectable `runCheck`/`proveFailFirst`; + * given their results the disposition is same-input-same-output and mutation-survivable. */ export function runProhibitionEnforcement( prohibition: unknown, @@ -440,24 +629,33 @@ export function runProhibitionEnforcement( } const runCheck = options.runCheck ?? ((toRun: CheckDescriptor) => defaultRunCheck(toRun, options.cwd ?? process.cwd(), options.timeoutMs)); + const proveFailFirst = options.proveFailFirst ?? ((toProve: CheckDescriptor) => defaultProveFailFirst(toProve, options.cwd ?? process.cwd(), options.timeoutMs)); - // (2) ATTEST fail-first (CALLER-DECLARED) + RUN. The caller must attest `failFirst: true` AND the - // runner must observe a genuine NON-VACUOUS pass. The producer does NOT independently prove - // fail-first (that needs a violation fixture — tracked follow-up, ADR-550 D5d). A non-attested or - // non-passing check hard-gates (never green) in BOTH modes. - const attestedFailFirst = c.failFirst === true; - // No-throw contract end-to-end: even a (test-injected) runCheck that throws must fail closed, - // never propagate. The default real runner already never throws. + // (2) PROVE fail-first (MACHINE) + RUN. The prover must INDEPENDENTLY run the check against the + // descriptor's violation fixture and observe it go red (`proof.provenFailFirst`), AND the runner + // must observe a genuine NON-VACUOUS pass. Caller attestation (`c.failFirst`) is NOT consulted for + // the green verdict (FF-08) — a check that cannot be machine-proven fail-first hard-gates (never + // green) in BOTH modes, even if attested. + // No-throw contract end-to-end: even a (test-injected) prover/runner that throws must fail closed, + // never propagate. The default real prover/runner already never throw. + let proof: FailFirstProof; + try { + proof = proveFailFirst(c); + } catch { + proof = { provenFailFirst: false }; + } let run: CheckRunResult; try { run = runCheck(c); } catch { run = { passed: false }; } - const passed = attestedFailFirst && run.passed === true; + // The `&&` and `=== true` are mutation-load-bearing — both directions (proven-red AND clean-pass) + // must hold for green; Plan 01/02 guards pin them. + const passed = proof.provenFailFirst === true && run.passed === true; if (!passed) { - // NOT attested fail-first OR did not genuinely pass -> fail-closed, located: true (an actual + // NOT machine-proven fail-first OR did not genuinely pass -> fail-closed, located: true (an actual // located miss/fail). Hard-gate applies in BOTH modes; the disposition stays non-green / flagged. const disposition = dispositionForProhibition(prohibition, { enforcementEvidence: [] }); return { @@ -470,13 +668,15 @@ export function runProhibitionEnforcement( } // (3) PASS -> build typed enforcementEvidence and let the policy flip a test-tier item green. - // `failFirst` here is the caller's attestation (recorded for provenance), not a machine proof. + // `failFirst: true` here means MACHINE-PROVEN (the green AND required `proof.provenFailFirst`), + // and `failFirstProof` records HOW it was proven (FF-07). const evidence: EnforcementEvidence[] = [{ kind: c.kind, target: c.target, ...(typeof c.rule === 'string' ? { rule: c.rule } : {}), failFirst: true, passed: true, + ...(proof.method ? { failFirstProof: proof.method } : {}), }]; const disposition = dispositionForProhibition(prohibition, { enforcementEvidence: evidence }); return { diff --git a/tests/_ff_lint_violation.cjs b/tests/_ff_lint_violation.cjs new file mode 100644 index 000000000..73a3eaf8b --- /dev/null +++ b/tests/_ff_lint_violation.cjs @@ -0,0 +1,27 @@ +/* eslint-disable local/no-source-grep */ +// PERMANENT LOAD-BEARING FIXTURE for #1279 — DO NOT "simplify" or delete. +// +// This file is a KNOWN `local/no-source-grep` violation used by `defaultProveFailFirst`'s lint-rule +// path to machine-prove the rule has teeth (the fail-first proof). The exact form below is the ONLY +// shape that fires `local/no-source-grep` under the project flat config (verified empirically, #1279 +// RESEARCH): a lint-scoped `.cjs` file under `tests/` whose `readFileSync` argument is the +// `path.join('lib','foo.cjs')` form (a STANDALONE quoted source-dir token `'lib'` + a quoted +// `.cjs` extension) followed by a text-search method (`.includes`) on the bound variable. +// +// - `'src/x.cjs'` as a single string literal does NOT fire (no standalone quoted dir token). +// - a repo-root / tmp path does NOT fire (no source-dir token). +// +// NAME: this is a PLAIN `.cjs` fixture, NOT `*.test.cjs`. `no-source-grep` has no filename guard, so +// it fires on any lint-scoped `.cjs`; the `.test.cjs` suffix would make the `node --test` runner +// EXECUTE it (ENOENT on `lib/foo.cjs` at module load → a real full-suite failure, #1279 wave 5). It +// is a lint fixture, never a test — keep it off the `.test.cjs` glob. +// +// The leading `/* eslint-disable local/no-source-grep */` keeps the project's own `eslint .` green +// (the violation lands in eslint's `suppressedMessages`, which the prover's `eslintJsonHasRule` +// reads — an inline-disabled violation still proves the rule has teeth, #1259 B1). If the prover +// ever reports `provenFailFirst:false` for the lint-rule kind, suspect THIS file's form first. +'use strict'; +const fs = require('node:fs'); +const path = require('node:path'); +const s = fs.readFileSync(path.join('lib', 'foo.cjs'), 'utf-8'); +module.exports = s.includes('x'); diff --git a/tests/probe-core.property.test.cjs b/tests/probe-core.property.test.cjs index 003ea4858..1a41d855c 100644 --- a/tests/probe-core.property.test.cjs +++ b/tests/probe-core.property.test.cjs @@ -193,6 +193,7 @@ function renderProhibitionsDoc(entries) { if (e.check_kind !== undefined) lines.push(` check_kind: ${e.check_kind}`); if (e.check_target !== undefined) lines.push(` check_target: ${e.check_target}`); if (e.check_rule !== undefined) lines.push(` check_rule: ${e.check_rule}`); + if (e.check_violation_fixture !== undefined) lines.push(` check_violation_fixture: ${e.check_violation_fixture}`); } lines.push('---', '', 'Body.', ''); return lines.join('\n'); @@ -216,19 +217,20 @@ const pathScalarArb = fc.array(fc.constantFrom(...PATH_CHARS), { minLength: 1, m const numericScalarArb = fc.nat({ max: 9999999 }).map(String); const targetArb = fc.oneof(pathScalarArb, numericScalarArb); -// A fully well-formed descriptor item (resolved test-tier); node-test carries no rule. +// A fully well-formed descriptor item (resolved test-tier); node-test carries no rule. The +// violation fixture (#1346) rides BOTH kinds and exercises the numeric-coercion path too. const wellFormedArb = KIND_ARB.chain((kind) => - fc.record({ target: targetArb, rule: pathScalarArb }).map(({ target, rule }) => { - const item = { ...BASE_TIER, check_kind: kind, check_target: target }; + fc.record({ target: targetArb, rule: pathScalarArb, fixture: targetArb }).map(({ target, rule, fixture }) => { + const item = { ...BASE_TIER, check_kind: kind, check_target: target, check_violation_fixture: fixture }; if (kind === 'lint-rule') item.check_rule = rule; - return { item, kind, target, rule: kind === 'lint-rule' ? rule : undefined }; + return { item, kind, target, rule: kind === 'lint-rule' ? rule : undefined, fixture }; }), ); describe('probe-core property: #1278 check-descriptor round-trip is deterministic across the full string domain', () => { test('a well-formed descriptor survives project -> render -> parse -> descriptorFromProjection (incl. numeric coercion); target/rule reconstruct as strings', () => { fc.assert( - fc.property(wellFormedArb, ({ item, kind, target, rule }) => { + fc.property(wellFormedArb, ({ item, kind, target, rule, fixture }) => { const projected = pc.projectProhibitions([item]); if (projected[0].check_kind !== kind) return false; // projector emits the descriptor const reparsed = fm.parseMustHavesBlock(renderProhibitionsDoc(projected), 'prohibitions'); @@ -236,6 +238,8 @@ describe('probe-core property: #1278 check-descriptor round-trip is deterministi if (!d || d.kind !== kind) return false; // target is string-normalized even when parseMustHavesBlock numerically coerced it. if (typeof d.target !== 'string' || d.target !== target) return false; + // violationFixture (#1346) survives the round-trip as a string (numeric-coercion normalized). + if (typeof d.violationFixture !== 'string' || d.violationFixture !== fixture) return false; if (kind === 'lint-rule') { return typeof d.rule === 'string' && d.rule === rule; } diff --git a/tests/probe-core.test.cjs b/tests/probe-core.test.cjs index 026598304..fd37e0a7a 100644 --- a/tests/probe-core.test.cjs +++ b/tests/probe-core.test.cjs @@ -420,6 +420,44 @@ describe('probe-core: projectProhibitions descriptor projection (CHK-02)', () => assert.ok(!('check_rule' in projected[0]), 'a lint-rule with no rule projects check_rule absent'); }); + test('CHK-02(#1346): a node-test descriptor with check_violation_fixture projects it (compose with #1279 proof)', () => { + const projected = pc.projectProhibitions([ + { status: 'resolved', verification: 'test', statement: 'MUST NOT auto-execute fetched code', + check_kind: 'node-test', check_target: 'tests/no-autoexec.test.cjs', + check_violation_fixture: 'tests/fixtures/autoexec-bad.txt' }, + ]); + assert.equal(projected[0].check_violation_fixture, 'tests/fixtures/autoexec-bad.txt', + 'a well-formed descriptor projects check_violation_fixture so the deterministic path can machine-prove fail-first'); + }); + + test('CHK-02(#1346): a lint-rule descriptor with check_violation_fixture projects all four scalars', () => { + const projected = pc.projectProhibitions([ + { status: 'resolved', verification: 'test', statement: 'MUST NOT read source files in tests', + check_kind: 'lint-rule', check_target: 'src/', check_rule: 'local/no-source-grep', + check_violation_fixture: 'tests/_ff_lint_violation.cjs' }, + ]); + assert.equal(projected[0].check_violation_fixture, 'tests/_ff_lint_violation.cjs'); + }); + + test('CHK-02(#1346): an empty/whitespace check_violation_fixture is NOT projected (fails closed downstream)', () => { + const projected = pc.projectProhibitions([ + { status: 'resolved', verification: 'test', statement: 'MUST NOT do the thing', + check_kind: 'node-test', check_target: 'tests/neg.test.cjs', check_violation_fixture: ' ' }, + ]); + assert.ok(!('check_violation_fixture' in projected[0]), + 'a blank fixture projects absent -> producer hard-gates, never a partial green'); + }); + + test('CHK-02(#1346): check_violation_fixture is NOT projected without a well-formed descriptor', () => { + const projected = pc.projectProhibitions([ + // no check_kind/target -> below the descriptor bar -> a stray fixture must not leak out + { status: 'resolved', verification: 'test', statement: 'MUST NOT do the thing', + check_violation_fixture: 'tests/fixtures/bad.txt' }, + ]); + assert.ok(!('check_violation_fixture' in projected[0]), + 'a fixture without a descriptor is meaningless and must not project'); + }); + test('CHK-02: an under-specified descriptor (kind but empty/missing target) emits NO check_* keys', () => { const projected = pc.projectProhibitions([ // valid kind but empty target -> below the well-formedness bar -> descriptor projects absent diff --git a/tests/prohibition-enforcement.property.test.cjs b/tests/prohibition-enforcement.property.test.cjs index 6d07e5ade..935a302cf 100644 --- a/tests/prohibition-enforcement.property.test.cjs +++ b/tests/prohibition-enforcement.property.test.cjs @@ -57,4 +57,42 @@ describe('prohibition-enforcement properties (#1259)', () => { assert.ok(Number.isInteger(n) && n >= 0); })); }); + + // ─── #1279 isNodeTestRed (FF-03 / FF-06) ─── + test('isNodeTestRed agrees with parseNodeTestSummary().fail >= 1 and never throws', () => { + const enforce = require(ENFORCEMENT_LIB); + fc.assert(fc.property(fc.string(), (s) => { + const red = enforce.isNodeTestRed(s); + assert.equal(red, enforce.parseNodeTestSummary(s).fail >= 1, + 'isNodeTestRed(s) === (parseNodeTestSummary(s).fail >= 1)'); + })); + }); + + // ─── #1279 proven-fail-first is NECESSARY for green (FF-08 necessity invariant) ─── + test('NO clean pass greens when the prover did not prove fail-first — proof is necessary for green (FF-08)', () => { + const enforce = require(ENFORCEMENT_LIB); + const TEST_TIER = Object.freeze({ + requirement_id: 'R1', category: 'safety', status: 'resolved', verification: 'test', + resolution: null, reason: null, statement: 'MUST NOT do the forbidden thing', + }); + fc.assert(fc.property( + fc.constantFrom('node-test', 'lint-rule'), + fc.string({ minLength: 1 }).filter((s) => s.trim().length > 0), + fc.boolean(), + fc.string({ minLength: 1 }).filter((s) => s.trim().length > 0), + (kind, target, attest, rule) => { + // ANY well-formed descriptor + a CLEAN pass + a prover that did NOT prove fail-first must + // NEVER green, regardless of the caller's `failFirst` attestation. Proof is necessary for green. + const descriptor = kind === 'lint-rule' + ? { kind, target, rule, failFirst: attest } + : { kind, target, failFirst: attest }; + const result = enforce.runProhibitionEnforcement(TEST_TIER, descriptor, { + runCheck: () => ({ passed: true }), + proveFailFirst: () => ({ provenFailFirst: false }), + }); + assert.notEqual(result.status, 'green', + 'an un-proven-fail-first check must never green even on a clean pass (FF-08 necessity)'); + }, + )); + }); }); diff --git a/tests/prohibition-enforcement.test.cjs b/tests/prohibition-enforcement.test.cjs index 2914facec..e2f7239d0 100644 --- a/tests/prohibition-enforcement.test.cjs +++ b/tests/prohibition-enforcement.test.cjs @@ -54,12 +54,17 @@ describe('prohibition-enforcement: deterministic test-tier producer (#1259 / ADR assert.equal(result.flagged, true); }); - test('node-test check that passes -> green + non-empty typed evidence', () => { + test('node-test check that passes AND is machine-proven fail-first -> green + non-empty typed evidence', () => { const enforce = require(ENFORCEMENT_LIB); + // Migrated to machine proof (#1279): green now requires an injected proving prover, not + // attestation. `failFirstProof` is asserted on the evidence (FF-07). const result = enforce.runProhibitionEnforcement( TEST_TIER, { kind: 'node-test', target: 'tests/neg.test.cjs', failFirst: true }, - { runCheck: () => ({ passed: true }) }, + { + runCheck: () => ({ passed: true }), + proveFailFirst: () => ({ provenFailFirst: true, method: 'violation-fixture' }), + }, ); assert.equal(result.status, 'green'); assert.equal(result.flagged, false); @@ -72,14 +77,20 @@ describe('prohibition-enforcement: deterministic test-tier producer (#1259 / ADR assert.equal(ev.target, 'tests/neg.test.cjs'); assert.equal(ev.failFirst, true); assert.equal(ev.passed, true); + assert.equal(ev.failFirstProof, 'violation-fixture', + 'evidence records HOW fail-first was machine-proven (FF-07)'); }); - test('lint-rule (no-source-grep) check that passes -> green, evidence carries rule id', () => { + test('lint-rule (no-source-grep) check that passes AND is machine-proven -> green, evidence carries rule id', () => { const enforce = require(ENFORCEMENT_LIB); + // Migrated to machine proof (#1279): inject a proving prover alongside the clean runCheck. const result = enforce.runProhibitionEnforcement( TEST_TIER, { kind: 'lint-rule', rule: 'local/no-source-grep', target: 'tests/', failFirst: true }, - { runCheck: () => ({ passed: true }) }, + { + runCheck: () => ({ passed: true }), + proveFailFirst: () => ({ provenFailFirst: true, method: 'violation-fixture' }), + }, ); assert.equal(result.status, 'green'); assert.equal(result.flagged, false); @@ -171,15 +182,154 @@ describe('prohibition-enforcement: deterministic test-tier producer (#1259 / ADR test('passing run echoes the requested mode without changing the green verdict', () => { const enforce = require(ENFORCEMENT_LIB); + // Migrated to machine proof (#1279): inject a proving prover so green is reached via proof. const result = enforce.runProhibitionEnforcement( TEST_TIER, { kind: 'node-test', target: 'tests/neg.test.cjs', failFirst: true }, - { runCheck: () => ({ passed: true }), mode: 'autonomous' }, + { + runCheck: () => ({ passed: true }), + proveFailFirst: () => ({ provenFailFirst: true, method: 'violation-fixture' }), + mode: 'autonomous', + }, ); assert.equal(result.status, 'green', 'a passing wired check is green in autonomous mode too'); assert.equal(result.mode, 'autonomous'); }); + // ─── #1279 RED-first adversarial guards (FF-01 / FF-04 / FF-05) ─────────────── + // These pin MACHINE-PROVEN fail-first BEFORE the producer change. They inject a NEW + // `proveFailFirst` option that the current producer does not read, so they FAIL against the + // attestation-greens code (src/prohibition-enforcement.cts:411). Their failure IS the FF-01 RED + // signal; Plans 02-03 wire the prover and turn them green. No source is edited in this plan. + + test('attestation alone no longer greens: a clean pass with no proving prover hard-gates (FF-01)', () => { + const enforce = require(ENFORCEMENT_LIB); + // The single most important guard: caller attests failFirst:true AND the run passes cleanly, + // but the prover could NOT prove the check fails-on-violation (provenFailFirst:false). Without a + // machine proof, attestation alone must NEVER green — it must hard-gate, flagged, located. + const result = enforce.runProhibitionEnforcement( + TEST_TIER, + { kind: 'node-test', target: 'tests/neg.test.cjs', failFirst: true }, + { + runCheck: () => ({ passed: true }), + proveFailFirst: () => ({ provenFailFirst: false }), + }, + ); + assert.notEqual(result.status, 'green', + 'attestation + a clean pass but no machine proof of fail-first must NEVER green (FF-01)'); + assert.equal(result.flagged, true, 'an un-proven check is flagged'); + assert.equal(result.located, true, 'the descriptor was located; it just was not proven fail-first'); + }); + + test('a machine-proven fail-first check with a clean pass greens (FF-01 positive)', () => { + const enforce = require(ENFORCEMENT_LIB); + const result = enforce.runProhibitionEnforcement( + TEST_TIER, + { kind: 'node-test', target: 'tests/neg.test.cjs', failFirst: true }, + { + runCheck: () => ({ passed: true }), + proveFailFirst: () => ({ provenFailFirst: true, method: 'violation-fixture' }), + }, + ); + assert.equal(result.status, 'green', + 'a check proven to fail-on-violation AND pass-on-clean must green'); + assert.equal(result.located, true); + assert.equal(result.evidence.length, 1, 'one evidence record built on a proven green'); + }); + + test('passes-on-violation (prover could not prove red) hard-gates, never green (FF-04 both-directions)', () => { + const enforce = require(ENFORCEMENT_LIB); + // The wired check passes on a clean run, but the prover ran it against a known violation and the + // check did NOT go red (provenFailFirst:false). A check that passes-on-violation is not a + // regression guard -> hard-gate. + const result = enforce.runProhibitionEnforcement( + TEST_TIER, + { kind: 'node-test', target: 'tests/neg.test.cjs', failFirst: true }, + { + runCheck: () => ({ passed: true }), + proveFailFirst: () => ({ provenFailFirst: false }), + }, + ); + assert.notEqual(result.status, 'green', + 'a check that does not go red on a known violation is not a regression guard (FF-04)'); + assert.equal(result.flagged, true); + assert.equal(result.located, true); + }); + + test('fails-on-clean (clean run did not pass) hard-gates even when fail-first is proven (FF-04 both-directions)', () => { + const enforce = require(ENFORCEMENT_LIB); + // The prover proved the check goes red on a violation, but the clean run FAILED — both directions + // must hold (fail-on-violation AND non-vacuous pass-on-clean) for green. A failing clean run + // hard-gates regardless of the proof. + const result = enforce.runProhibitionEnforcement( + TEST_TIER, + { kind: 'node-test', target: 'tests/neg.test.cjs', failFirst: true }, + { + runCheck: () => ({ passed: false }), + proveFailFirst: () => ({ provenFailFirst: true, method: 'violation-fixture' }), + }, + ); + assert.notEqual(result.status, 'green', + 'a proven-fail-first check whose clean run failed must still hard-gate (FF-04)'); + assert.equal(result.flagged, true); + assert.equal(result.located, true); + }); + + test('node-test with NO violationFixture fail-closes via the default prover, never falls back to attestation (FF-05)', () => { + const enforce = require(ENFORCEMENT_LIB); + // Decision-layer/default-prover guard: a node-test descriptor with no violationFixture cannot be + // machine-proven (a generic producer cannot synthesize a violation), so the DEFAULT real prover + // returns provenFailFirst:false -> hard-gate. We inject NO proveFailFirst so the default path is + // exercised. It must NEVER silently weaken to attestation. (Default prover lands in Plans 02-03, + // so this is RED now and greens with the producer change.) + const result = enforce.runProhibitionEnforcement( + TEST_TIER, + { kind: 'node-test', target: 'tests/neg.test.cjs', failFirst: true }, + { runCheck: () => ({ passed: true }) }, + ); + assert.notEqual(result.status, 'green', + 'a node-test with no violationFixture cannot be proven fail-first -> fail-closed (FF-05)'); + assert.equal(result.flagged, true, 'an un-provable check is flagged'); + assert.equal(result.located, true, 'the descriptor was located; it just could not be proven'); + }); + + test('a proveFailFirst that THROWS fails closed, never propagates and never greens (FF-05 no-throw)', () => { + const enforce = require(ENFORCEMENT_LIB); + // No-throw contract on the prove seam, mirroring the runCheck-throws guard: a prover that blows up + // must fail closed (treated as provenFailFirst:false), never propagate and never green. + const result = enforce.runProhibitionEnforcement( + TEST_TIER, + { kind: 'node-test', target: 'tests/neg.test.cjs', failFirst: true }, + { + runCheck: () => ({ passed: true }), + proveFailFirst: () => { throw new Error('prover blew up'); }, + }, + ); + assert.notEqual(result.status, 'green', 'a throwing prover must never green (FF-05)'); + assert.equal(result.flagged, true); + assert.equal(result.located, true); + }); + + test('an un-provable fail-first check fails closed in BOTH interactive and autonomous modes (FF-04 / ADR-550 D4)', () => { + const enforce = require(ENFORCEMENT_LIB); + // A clean pass + a prover that could not prove fail-first must hard-gate in BOTH modes, with the + // mode echoed for transparency. Mirrors the existing both-modes failing-check guard (:158). + for (const mode of ['interactive', 'autonomous']) { + const result = enforce.runProhibitionEnforcement( + TEST_TIER, + { kind: 'node-test', target: 'tests/neg.test.cjs', failFirst: true }, + { + runCheck: () => ({ passed: true }), + proveFailFirst: () => ({ provenFailFirst: false }), + mode, + }, + ); + assert.notEqual(result.status, 'green', `un-provable check must not green in ${mode}`); + assert.equal(result.flagged, true, `un-provable check is flagged in ${mode}`); + assert.equal(result.mode, mode, 'mode echoed for transparency'); + } + }); + test('routeProhibitionEnforcement parses a JSON request file and emits a structured result', (t) => { const fs = require('node:fs'); const { execFileSync } = require('node:child_process'); @@ -224,6 +374,46 @@ describe('prohibition-enforcement real-runner helpers (#1259)', () => { assert.deepEqual(enforce.parseNodeTestSummary('no summary here'), { tests: 0, pass: 0, fail: 0, cancelled: 0 }); }); + // ─── #1279 isNodeTestRed pure helper (FF-03 / FF-06) — mutation-pinned `>= 1` boundary ─── + test('isNodeTestRed is true iff the TAP summary reports # fail >= 1 (mutation-pinned boundary)', () => { + const enforce = require(ENFORCEMENT_LIB); + // The `# fail 1` case is load-bearing: it pins `>= 1`, not `> 1`. A mutant flipping `>=`→`>` + // (or bumping the threshold) flips this assertion and is caught. + assert.equal(enforce.isNodeTestRed('# fail 1\n'), true, '# fail 1 is RED (boundary: >= 1, not > 1)'); + assert.equal(enforce.isNodeTestRed('# fail 0\n'), false, '# fail 0 is not RED'); + assert.equal(enforce.isNodeTestRed('# fail 2\n'), true, '# fail 2 is RED'); + assert.equal(enforce.isNodeTestRed('no summary'), false, 'no parseable summary -> not RED (fail-closed for the prover)'); + }); + + // ─── #1279 isNonVacuousNodeTestRed (FF-03 hardening) — a NON-VACUOUS red proof ─── + // The fail-first PROOF must mirror the clean-pass non-vacuity discipline: a violation fixture that + // makes the negative test CRASH at load (ENOENT/throw/syntax) emits a FILE-NAMED `# fail 1` — the + // test never ran its assertion, so that is NOT proof the test is a regression guard. Require at + // least one FAILING test named DISTINCTLY from the target file (symmetric with isNonVacuousNodeTestPass). + test('isNonVacuousNodeTestRed: a file-named-only failure (a crash, not an assertion) does NOT prove fail-first', () => { + const enforce = require(ENFORCEMENT_LIB); + // node --test of a file that throws at load: `not ok 1 - `, `# fail 1` — a crash, not a + // negative assertion firing red. Must NOT count as a non-vacuous red. + const crash = 'not ok 1 - neg.test.cjs\n# tests 1\n# pass 0\n# fail 1\n'; + assert.equal(enforce.isNonVacuousNodeTestRed(crash, 'neg.test.cjs'), false, + 'a file-named-only failure is a load crash, not a proven regression guard — fail-closed'); + // BASENAME-NORMALIZED: node may report the file failure by an absolute/normalized path. + const crashAbs = 'not ok 1 - /tmp/x/neg.test.cjs\n# tests 1\n# pass 0\n# fail 1\n'; + assert.equal(enforce.isNonVacuousNodeTestRed(crashAbs, 'neg.test.cjs'), false, + 'an absolute-path file-named failure is still a crash (basename compare)'); + // A genuine negative assertion firing red carries a descriptive name distinct from the file. + const realRed = 'not ok 1 - rejects the forbidden pattern\n# tests 1\n# pass 0\n# fail 1\n'; + assert.equal(enforce.isNonVacuousNodeTestRed(realRed, 'neg.test.cjs'), true, + 'a distinctly-named failing test is a genuine non-vacuous red — proves fail-first'); + // No failure at all -> not red. + assert.equal(enforce.isNonVacuousNodeTestRed('ok 1 - guards\n# tests 1\n# pass 1\n# fail 0\n', 'neg.test.cjs'), false, + '# fail 0 is not red regardless of names'); + // SKIP/TODO failing lines never ran -> excluded (mirror tapTestNames m1). + const skippedRed = 'not ok 1 - rejects the forbidden pattern # SKIP\n# tests 1\n# pass 0\n# fail 1\n'; + assert.equal(enforce.isNonVacuousNodeTestRed(skippedRed, 'neg.test.cjs'), false, + 'a SKIP/TODO failing line did not actually run -> not a proof'); + }); + test('tapTestNames EXCLUDES skipped/todo tests (they never ran, m1)', () => { const enforce = require(ENFORCEMENT_LIB); assert.deepEqual(enforce.tapTestNames('ok 1 - guards the must-NOT\nok 2 - other # SKIP\nok 3 - later # TODO\n'), @@ -307,21 +497,36 @@ describe('prohibition-enforcement real-runner helpers (#1259)', () => { describe('prohibition-enforcement REAL runner end-to-end (#1259)', () => { const fs = require('node:fs'); - test('a genuine non-vacuous passing node-test greens via the real runner', (t) => { + test('a genuine non-vacuous passing node-test proven fail-first greens via the real runner + real prover', (t) => { const enforce = require(ENFORCEMENT_LIB); const dir = createTempDir('prohib-real-pass-'); t.after(() => cleanup(dir)); + // Migrated to the SHIPPING prover (#1279): a REAL negative test that honors the + // GSD_PROHIB_SUBJECT convention — it asserts its subject is clean. The clean runCheck run reads + // the CLEAN subject (passes, non-vacuous); the prover runs it against a KNOWN-BAD subject so it + // goes RED (fail-first proven). Both directions exercised against real `node --test`. const tf = path.join(dir, 'neg.test.cjs'); fs.writeFileSync(tf, - "const { test } = require('node:test');\nconst assert = require('node:assert');\ntest('guards the must-NOT', () => { assert.ok(true); });\n"); + "const { test } = require('node:test');\n" + + "const assert = require('node:assert');\n" + + "const fs = require('node:fs');\n" + + "test('guards the must-NOT: subject is clean', () => {\n" + + " const subject = fs.readFileSync(process.env.GSD_PROHIB_SUBJECT, 'utf-8');\n" + + " assert.ok(!subject.includes('FORBIDDEN'), 'subject must not contain FORBIDDEN');\n" + + "});\n"); + const cleanSubject = path.join(dir, 'clean-subject.txt'); + fs.writeFileSync(cleanSubject, 'this subject is clean\n'); + const badFixture = path.join(dir, 'bad-subject.txt'); + fs.writeFileSync(badFixture, 'this subject contains FORBIDDEN content\n'); const result = enforce.runProhibitionEnforcement( TEST_TIER, - { kind: 'node-test', target: tf, failFirst: true }, - { cwd: dir }, + { kind: 'node-test', target: tf, failFirst: true, violationFixture: badFixture }, + { cwd: dir, runCheck: () => ({ passed: true }) }, ); - assert.equal(result.status, 'green', 'a real, passing, non-vacuous negative test must green'); + assert.equal(result.status, 'green', 'a real negative test proven fail-first + clean pass must green'); assert.equal(result.located, true); assert.equal(result.evidence.length, 1); + assert.equal(result.evidence[0].failFirstProof, 'violation-fixture'); }); test('a HANGING node-test fails closed via the bounded timeout (B2: no unbounded subprocess)', (t) => { @@ -357,18 +562,27 @@ describe('prohibition-enforcement REAL runner end-to-end (#1259)', () => { assert.equal(result.evidence.length, 0); }); - test('a clean in-tree target greens the lint-rule kind via the real eslint runner (SF-01: plugin loads)', () => { + test('a clean in-tree target greens the lint-rule kind via the real eslint + real prover (SF-01: plugin loads)', () => { const enforce = require(ENFORCEMENT_LIB); - // Runs real `npx eslint --format json src/clock.cts` under the project flat config (so the - // `local` plugin loads). src/clock.cts is a clean source with no no-source-grep violation. + // Migrated to the SHIPPING prover (#1279): the default real prover lints the committed + // `_ff_lint_violation.cjs` violationFixture (the rule fires -> fail-first proven) while the + // clean runCheck lints src/clock.cts (no violation -> non-vacuous pass). Both via real eslint. const result = enforce.runProhibitionEnforcement( TEST_TIER, - { kind: 'lint-rule', rule: 'local/no-source-grep', target: 'src/clock.cts', failFirst: true }, + { + kind: 'lint-rule', + rule: 'local/no-source-grep', + target: 'src/clock.cts', + failFirst: true, + violationFixture: path.join('tests', '_ff_lint_violation.cjs'), + }, { cwd: process.cwd() }, ); - assert.equal(result.status, 'green', 'a clean target with no no-source-grep violation must green via real eslint'); + assert.equal(result.status, 'green', 'a clean target proven fail-first must green via real eslint'); assert.equal(result.kind, 'lint-rule'); assert.equal(result.evidence[0].rule, 'local/no-source-grep'); + assert.equal(result.evidence[0].failFirstProof, 'violation-fixture', + 'the real prover records the proof method (FF-07)'); }); test('an eslint-IGNORED target does NOT green the lint-rule kind (vacuous-green guard, NEW-BL-01)', () => { @@ -383,6 +597,363 @@ describe('prohibition-enforcement REAL runner end-to-end (#1259)', () => { assert.notEqual(result.status, 'green', 'an ignored path lints nothing — must NEVER green'); assert.equal(result.located, true, 'the descriptor was well-formed; it just did not genuinely pass'); }); + + // ─── #1279 FULL-producer real-runner capstone (NO injected runCheck / proveFailFirst) ─────────── + // These exercise the COMPOSED runProhibitionEnforcement producer with NEITHER seam injected — the + // SHIPPING defaultProveFailFirst + defaultRunCheck both run real subprocesses. This is the exact + // path #1259's BL-01/SF-01 bypassed: an injected double can fake the runner, so the real-subprocess + // behavior (eslint plugin load, GSD_PROHIB_SUBJECT convention, fail-first proof) was unproven at the + // producer level until now. Both kinds, both directions, both modes. Typed-field assertions only. + + test('FULL producer (real prover + real runner): lint-rule greens on a real no-source-grep violation fixture + clean target (FF-02/FF-10)', () => { + const enforce = require(ENFORCEMENT_LIB); + // No injected runCheck/proveFailFirst: the default prover lints the committed + // `_ff_lint_violation.cjs` (the rule fires -> fail-first proven) AND the default runner lints + // the clean `src/clock.cts` (no violation -> non-vacuous pass). BOTH directions via real eslint. + const result = enforce.runProhibitionEnforcement( + TEST_TIER, + { + kind: 'lint-rule', + rule: 'local/no-source-grep', + target: 'src/clock.cts', + violationFixture: path.join('tests', '_ff_lint_violation.cjs'), + }, + { cwd: process.cwd() }, + ); + assert.equal(result.status, 'green', 'real prover (violation fixture red) + real runner (clean pass) must green'); + assert.equal(result.kind, 'lint-rule'); + assert.equal(result.located, true); + assert.equal(result.evidence.length, 1); + assert.equal(result.evidence[0].failFirstProof, 'violation-fixture', + 'the SHIPPING prover records the proof method (FF-07)'); + }); + + test('FULL producer (real): lint-rule hard-gates on a TOOTHLESS violationFixture (rule does not flag it) (FF-02 wrong-direction)', () => { + const enforce = require(ENFORCEMENT_LIB); + // The "violation fixture" is a CLEAN in-tree file (src/clock.cts) the rule does NOT flag, so the + // default prover cannot prove fail-first -> the producer must hard-gate (never green), even though + // the clean target itself would pass the runner. A toothless guard is not a guard. + const result = enforce.runProhibitionEnforcement( + TEST_TIER, + { + kind: 'lint-rule', + rule: 'local/no-source-grep', + target: 'src/clock.cts', + violationFixture: 'src/clock.cts', + }, + { cwd: process.cwd() }, + ); + assert.notEqual(result.status, 'green', 'a fixture the rule does not flag cannot prove fail-first -> not green'); + assert.equal(result.flagged, true, 'the toothless-fixture miss is flagged'); + assert.equal(result.located, true, 'the descriptor was well-formed; it just could not be machine-proven'); + assert.equal(result.evidence.length, 0, 'no enforcement evidence on a hard-gate'); + }); + + test('FULL producer (real): lint-rule TOOTHLESS-fixture hard-gate holds in BOTH interactive and autonomous modes (FF-04)', () => { + const enforce = require(ENFORCEMENT_LIB); + for (const mode of ['interactive', 'autonomous']) { + const result = enforce.runProhibitionEnforcement( + TEST_TIER, + { + kind: 'lint-rule', + rule: 'local/no-source-grep', + target: 'src/clock.cts', + violationFixture: 'src/clock.cts', + }, + { cwd: process.cwd(), mode }, + ); + assert.notEqual(result.status, 'green', `un-provable lint-rule must not green in ${mode}`); + assert.equal(result.flagged, true, `un-provable lint-rule is flagged in ${mode}`); + assert.equal(result.mode, mode, 'mode echoed for transparency'); + } + }); + + test('FULL producer (real prover + real runner): node-test greens via GSD_PROHIB_SUBJECT — red on bad fixture, clean pass on clean subject (FF-03/FF-10)', (t) => { + const enforce = require(ENFORCEMENT_LIB); + const dir = createTempDir('prohib-full-node-green-'); + t.after(() => cleanup(dir)); + // A REAL negative test that honors the GSD_PROHIB_SUBJECT convention: it reads its subject and + // asserts it is CLEAN. The default runner runs it with NO GSD_PROHIB_SUBJECT set -> the fixture + // defaults to a clean in-dir subject -> passes non-vacuously. The default prover runs it with + // GSD_PROHIB_SUBJECT= -> the assertion fails -> RED -> fail-first proven. + const negTest = path.join(dir, 'neg.test.cjs'); + fs.writeFileSync(negTest, + "const { test } = require('node:test');\n" + + "const assert = require('node:assert');\n" + + "const fs = require('node:fs');\n" + + "const path = require('node:path');\n" + + "test('guards the must-NOT: subject is clean', () => {\n" + + " const subjectPath = process.env.GSD_PROHIB_SUBJECT || path.join(__dirname, 'clean-subject.txt');\n" + + " const subject = fs.readFileSync(subjectPath, 'utf-8');\n" + + " assert.ok(!subject.includes('FORBIDDEN'), 'subject must not contain FORBIDDEN');\n" + + "});\n"); + fs.writeFileSync(path.join(dir, 'clean-subject.txt'), 'this subject is clean\n'); + const badFixture = path.join(dir, 'bad-subject.txt'); + fs.writeFileSync(badFixture, 'this subject contains FORBIDDEN content\n'); + const result = enforce.runProhibitionEnforcement( + TEST_TIER, + { kind: 'node-test', target: negTest, violationFixture: badFixture }, + { cwd: dir }, + ); + assert.equal(result.status, 'green', 'real node-test proven RED on the bad subject + clean pass must green'); + assert.equal(result.kind, 'node-test'); + assert.equal(result.located, true); + assert.equal(result.evidence.length, 1); + assert.equal(result.evidence[0].failFirstProof, 'violation-fixture'); + }); + + test('FULL producer (real): node-test WITHOUT a violationFixture hard-gates — default prover cannot prove fail-first (FF-05)', (t) => { + const enforce = require(ENFORCEMENT_LIB); + const dir = createTempDir('prohib-full-node-nofix-'); + t.after(() => cleanup(dir)); + // The SAME genuinely-passing negative test, but NO violationFixture. The default runner observes a + // real non-vacuous pass, yet the default prover returns provenFailFirst:false (no fixture to prove + // against) -> the producer must hard-gate. Pass alone never greens (machine proof required). + const negTest = path.join(dir, 'neg.test.cjs'); + fs.writeFileSync(negTest, + "const { test } = require('node:test');\n" + + "const assert = require('node:assert');\n" + + "const fs = require('node:fs');\n" + + "const path = require('node:path');\n" + + "test('guards the must-NOT: subject is clean', () => {\n" + + " const subjectPath = process.env.GSD_PROHIB_SUBJECT || path.join(__dirname, 'clean-subject.txt');\n" + + " const subject = fs.readFileSync(subjectPath, 'utf-8');\n" + + " assert.ok(!subject.includes('FORBIDDEN'), 'subject must not contain FORBIDDEN');\n" + + "});\n"); + fs.writeFileSync(path.join(dir, 'clean-subject.txt'), 'this subject is clean\n'); + const result = enforce.runProhibitionEnforcement( + TEST_TIER, + { kind: 'node-test', target: negTest }, // no violationFixture + { cwd: dir }, + ); + assert.notEqual(result.status, 'green', 'a real pass without a machine fail-first proof must hard-gate (FF-05)'); + assert.equal(result.flagged, true, 'the un-provable node-test miss is flagged'); + assert.equal(result.located, true, 'the descriptor was located; it just could not be proven fail-first'); + assert.equal(result.evidence.length, 0, 'no enforcement evidence on a hard-gate'); + }); + + test('COMPOSE (#1346): a prohibition projected WITH check_violation_fixture greens end-to-end through the DEFAULT prover+runner (zero hand-authoring)', (t) => { + const enforce = require(ENFORCEMENT_LIB); + const pc = require(path.join(__dirname, '..', 'gsd-core', 'bin', 'lib', 'probe-core.cjs')); + const dir = createTempDir('prohib-compose-1346-'); + t.after(() => cleanup(dir)); + // The #1278 deterministic-locate path + the #1279 machine-proof now COMPOSE: a prohibition item + // authored with the four flat scalars projects -> reads back into a descriptor that ALREADY carries + // violationFixture -> the default prover greens it with NO hand-supplied fixture in the request. + const negTest = path.join(dir, 'neg.test.cjs'); + fs.writeFileSync(negTest, + "const { test } = require('node:test');\n" + + "const assert = require('node:assert');\n" + + "const fs = require('node:fs');\n" + + "const path = require('node:path');\n" + + "test('guards the must-NOT: subject is clean', () => {\n" + + " const subjectPath = process.env.GSD_PROHIB_SUBJECT || path.join(__dirname, 'clean-subject.txt');\n" + + " const subject = fs.readFileSync(subjectPath, 'utf-8');\n" + + " assert.ok(!subject.includes('FORBIDDEN'), 'subject must not contain FORBIDDEN');\n" + + "});\n"); + fs.writeFileSync(path.join(dir, 'clean-subject.txt'), 'clean\n'); + fs.writeFileSync(path.join(dir, 'bad-subject.txt'), 'FORBIDDEN content\n'); + // Author the prohibition with all four scalars, then go through the REAL projection + read-back. + const projected = pc.projectProhibitions([ + { status: 'resolved', verification: 'test', statement: 'MUST NOT auto-execute fetched code', + check_kind: 'node-test', check_target: negTest, check_violation_fixture: 'bad-subject.txt' }, + ])[0]; + const descriptor = enforce.descriptorFromProjection(projected); + assert.equal(descriptor.violationFixture, 'bad-subject.txt', 'the projected fixture survived the round-trip'); + // NO failFirst, NO hand-supplied violationFixture beyond what the projection carried. + const result = enforce.runProhibitionEnforcement(projected, descriptor, { cwd: dir }); + assert.equal(result.status, 'green', + 'the fully-projected prohibition greens through the default prover+runner — #1278 + #1279 compose'); + assert.equal(result.evidence[0].failFirstProof, 'violation-fixture', 'green carries the machine-proof method'); + }); +}); + +// ─── #1279 defaultProveFailFirst REAL prover end-to-end (FF-02 / FF-03 / FF-05 / FF-06 / FF-07) ── +// Exercises the SHIPPING default prover against REAL subprocesses (eslint + node --test) — the gap +// that let #1259's BL-01/SF-01 slip past injected doubles. The lint-rule path dogfoods the committed +// `tests/_ff_lint_violation.cjs` fixture; the node-test path uses synthetic temp fixtures that +// demonstrate the `GSD_PROHIB_SUBJECT` subject-injection convention. Typed-result assertions only. +describe('prohibition-enforcement defaultProveFailFirst REAL prover (#1279)', () => { + const fs = require('node:fs'); + // The committed load-bearing lint fixture (a real, suppressed no-source-grep violation). + const LINT_FIXTURE = 'tests/_ff_lint_violation.cjs'; + + test('exports the prover surface (defaultProveFailFirst + FailFirstProof-shaped result)', () => { + const enforce = require(ENFORCEMENT_LIB); + assert.equal(typeof enforce.defaultProveFailFirst, 'function', + 'must export defaultProveFailFirst — the default real prover'); + }); + + test('lint-rule: proves red on the committed no-source-grep violation fixture (FF-02 red direction)', () => { + const enforce = require(ENFORCEMENT_LIB); + // Lint the KNOWN-violating fixture through the project flat config; the rule id MUST appear + // (in messages or suppressedMessages) → the rule has teeth → fail-first proven. + const proof = enforce.defaultProveFailFirst( + { kind: 'lint-rule', rule: 'local/no-source-grep', target: LINT_FIXTURE, violationFixture: LINT_FIXTURE }, + process.cwd(), + ); + assert.equal(proof.provenFailFirst, true, + 'a real no-source-grep violation fixture proves the lint rule fails-on-violation'); + assert.equal(proof.method, 'violation-fixture', 'records the proof method'); + }); + + test('lint-rule: a CLEAN violationFixture (rule does not flag) is NOT proven (FF-02 toothless direction)', () => { + const enforce = require(ENFORCEMENT_LIB); + // src/clock.cts is a clean in-tree source with no no-source-grep violation. If a "violation + // fixture" does not actually trigger the rule, the rule is toothless on it → not a guard → not + // proven → must hard-gate. + const proof = enforce.defaultProveFailFirst( + { kind: 'lint-rule', rule: 'local/no-source-grep', target: 'src/clock.cts', violationFixture: 'src/clock.cts' }, + process.cwd(), + ); + assert.equal(proof.provenFailFirst, false, + 'a fixture the rule does not flag cannot prove fail-first'); + }); + + test('lint-rule: no violationFixture -> not proven (FF-05 fail-closed)', () => { + const enforce = require(ENFORCEMENT_LIB); + const proof = enforce.defaultProveFailFirst( + { kind: 'lint-rule', rule: 'local/no-source-grep', target: 'src/clock.cts' }, // no violationFixture + process.cwd(), + ); + assert.equal(proof.provenFailFirst, false, 'no violationFixture -> cannot prove -> hard-gate'); + }); + + test('node-test: a negative test that goes RED against a known-bad GSD_PROHIB_SUBJECT is proven (FF-03 red direction)', (t) => { + const enforce = require(ENFORCEMENT_LIB); + const dir = createTempDir('prohib-ff-node-red-'); + t.after(() => cleanup(dir)); + // A negative test that HONORS the GSD_PROHIB_SUBJECT convention: it reads the subject path and + // asserts the subject is "clean" (does not contain the forbidden token). Against a KNOWN-BAD + // fixture, the assertion fails → the run goes RED → fail-first proven. + const negTest = path.join(dir, 'neg.test.cjs'); + fs.writeFileSync(negTest, + "const { test } = require('node:test');\n" + + "const assert = require('node:assert');\n" + + "const fs = require('node:fs');\n" + + "test('subject must not contain FORBIDDEN', () => {\n" + + " const subject = fs.readFileSync(process.env.GSD_PROHIB_SUBJECT, 'utf-8');\n" + + " assert.ok(!subject.includes('FORBIDDEN'), 'subject is clean');\n" + + "});\n"); + const badFixture = path.join(dir, 'bad-subject.txt'); + fs.writeFileSync(badFixture, 'this subject contains FORBIDDEN content\n'); + const proof = enforce.defaultProveFailFirst( + { kind: 'node-test', target: negTest, violationFixture: badFixture }, + dir, + ); + assert.equal(proof.provenFailFirst, true, + 'the negative test goes RED against the known-bad subject -> fail-first proven'); + assert.equal(proof.method, 'violation-fixture'); + }); + + test('node-test: a toothless negative test that PASSES even against the violation is NOT proven (FF-03 toothless direction)', (t) => { + const enforce = require(ENFORCEMENT_LIB); + const dir = createTempDir('prohib-ff-node-tooth-'); + t.after(() => cleanup(dir)); + // A negative test that ignores the subject and always passes — it never goes red, so it cannot + // prove fail-first even with a violation fixture supplied. + const negTest = path.join(dir, 'neg.test.cjs'); + fs.writeFileSync(negTest, + "const { test } = require('node:test');\n" + + "const assert = require('node:assert');\n" + + "test('always passes (toothless)', () => { assert.ok(true); });\n"); + const badFixture = path.join(dir, 'bad-subject.txt'); + fs.writeFileSync(badFixture, 'FORBIDDEN\n'); + const proof = enforce.defaultProveFailFirst( + { kind: 'node-test', target: negTest, violationFixture: badFixture }, + dir, + ); + assert.equal(proof.provenFailFirst, false, + 'a test that does not go red against the violation is toothless -> not proven'); + }); + + test('node-test: no violationFixture -> not proven (FF-05 fail-closed)', (t) => { + const enforce = require(ENFORCEMENT_LIB); + const dir = createTempDir('prohib-ff-node-nofix-'); + t.after(() => cleanup(dir)); + const negTest = path.join(dir, 'neg.test.cjs'); + fs.writeFileSync(negTest, + "const { test } = require('node:test');\ntest('guards', () => {});\n"); + const proof = enforce.defaultProveFailFirst( + { kind: 'node-test', target: negTest }, // no violationFixture + dir, + ); + assert.equal(proof.provenFailFirst, false, + 'a node-test with no violationFixture cannot be proven -> hard-gate, never attestation'); + }); + + test('node-test: an HONEST test + a non-existent violationFixture path is NOT proven (FF-05 fail-OPEN guard, #1314 Major 1)', (t) => { + const enforce = require(ENFORCEMENT_LIB); + const dir = createTempDir('prohib-ff-node-missingfix-'); + t.after(() => cleanup(dir)); + // REGRESSION (#1314 review, Major 1): a REAL, honest negative test (its target file EXISTS and + // loads cleanly) reads GSD_PROHIB_SUBJECT and fs.readFileSync's it. Point violationFixture at a + // MISSING path (the realistic author typo / stale / moved-fixture case). Before the fix the missing + // subject made the honest test throw ENOENT *inside its callback* — a failing test named distinctly + // from the file — which isNonVacuousNodeTestRed accepted as a genuine RED, FORGING provenFailFirst:true + // from a setup crash (fail-OPEN). The fs.existsSync(fixture) guard now fail-CLOSES this, symmetric + // with the lint-rule path. Note this is the SAME honest-test shape as the FF-03 red-direction test — + // only the fixture path is missing — so it is exactly the green-able producer minus a valid fixture. + const negTest = path.join(dir, 'neg.test.cjs'); + fs.writeFileSync(negTest, + "const { test } = require('node:test');\n" + + "const assert = require('node:assert');\n" + + "const fs = require('node:fs');\n" + + "test('subject must not contain FORBIDDEN', () => {\n" + + " const subject = fs.readFileSync(process.env.GSD_PROHIB_SUBJECT, 'utf-8');\n" + + " assert.ok(!subject.includes('FORBIDDEN'), 'subject is clean');\n" + + "});\n"); + const missingFixture = path.join(dir, 'does-not-exist-subject.txt'); // deliberately NOT written + const proof = enforce.defaultProveFailFirst( + { kind: 'node-test', target: negTest, violationFixture: missingFixture }, + dir, + ); + assert.equal(proof.provenFailFirst, false, + 'a missing/typo\'d violationFixture must NOT forge a green from the honest test\'s ENOENT crash (fail-closed, symmetric with lint-rule)'); + }); + + test('node-test: a RELATIVE violationFixture is resolved against cwd (existence guard matches the child, #1314 Major 1)', (t) => { + const enforce = require(ENFORCEMENT_LIB); + const dir = createTempDir('prohib-ff-node-relfix-'); + t.after(() => cleanup(dir)); + // The fixture is named RELATIVELY; the prover runs with cwd=dir and sets GSD_PROHIB_SUBJECT to the + // raw relative name, which the child resolves against its cwd (=dir). The existence guard must use + // the SAME base (path.resolve(cwd, fixture)) — a bare existsSync against the verify process's cwd + // would not find it and would wrongly hard-gate a valid fixture. Proving TRUE here confirms the + // relative path is honored end-to-end and the guard is cwd-correct. + const negTest = path.join(dir, 'neg.test.cjs'); + fs.writeFileSync(negTest, + "const { test } = require('node:test');\n" + + "const assert = require('node:assert');\n" + + "const fs = require('node:fs');\n" + + "test('subject must not contain FORBIDDEN', () => {\n" + + " const subject = fs.readFileSync(process.env.GSD_PROHIB_SUBJECT, 'utf-8');\n" + + " assert.ok(!subject.includes('FORBIDDEN'), 'subject is clean');\n" + + "});\n"); + fs.writeFileSync(path.join(dir, 'bad-subject.txt'), 'this subject contains FORBIDDEN content\n'); + const proof = enforce.defaultProveFailFirst( + { kind: 'node-test', target: negTest, violationFixture: 'bad-subject.txt' }, // RELATIVE to cwd + dir, + ); + assert.equal(proof.provenFailFirst, true, + 'a relative violationFixture resolved against cwd is found, runs RED, and proves fail-first'); + }); + + test('prover never throws: a non-existent fixture / unresolvable tooling -> provenFailFirst:false (FF-05/FF-06)', () => { + const enforce = require(ENFORCEMENT_LIB); + // Non-existent lint fixture path -> eslint lints nothing / errors -> fail-closed, no throw. + const lintProof = enforce.defaultProveFailFirst( + { kind: 'lint-rule', rule: 'local/no-source-grep', target: 'no/such/file.cjs', violationFixture: 'no/such/file.cjs' }, + process.cwd(), + ); + assert.equal(lintProof.provenFailFirst, false, 'a missing lint fixture proves nothing, never throws'); + // Non-existent node-test target -> the run is not RED in the intended way / errors -> fail-closed. + const nodeProof = enforce.defaultProveFailFirst( + { kind: 'node-test', target: 'no/such/neg.test.cjs', violationFixture: 'no/such/subject.txt' }, + process.cwd(), + ); + assert.equal(typeof nodeProof.provenFailFirst, 'boolean', 'returns a typed proof, never throws'); + }); }); // ─── CHK-06 (#1278): fail-closed on partial / invalid / absent descriptor-from-projection ──────── @@ -421,6 +992,38 @@ describe('prohibition-enforcement: fail-closed descriptor-from-projection (CHK-0 assert.ok(Array.isArray(result.evidence) && result.evidence.length === 0, 'no evidence on an absent descriptor'); }); + test('CHK-08(#1346): descriptorFromProjection maps check_violation_fixture -> violationFixture (node-test)', () => { + const enforce = require(ENFORCEMENT_LIB); + const descriptor = enforce.descriptorFromProjection({ + ...PROJECTED_TIER, check_kind: 'node-test', check_target: 'tests/neg.test.cjs', + check_violation_fixture: 'tests/fixtures/bad-subject.txt', + }); + assert.equal(descriptor.kind, 'node-test'); + assert.equal(descriptor.target, 'tests/neg.test.cjs'); + assert.equal(descriptor.violationFixture, 'tests/fixtures/bad-subject.txt', + 'the projected check_violation_fixture must reconstruct as violationFixture so #1278 locate + #1279 proof compose'); + }); + + test('CHK-08(#1346): descriptorFromProjection maps check_violation_fixture -> violationFixture (lint-rule)', () => { + const enforce = require(ENFORCEMENT_LIB); + const descriptor = enforce.descriptorFromProjection({ + ...PROJECTED_TIER, check_kind: 'lint-rule', check_target: 'src/', check_rule: 'local/no-source-grep', + check_violation_fixture: 'tests/_ff_lint_violation.cjs', + }); + assert.equal(descriptor.kind, 'lint-rule'); + assert.equal(descriptor.rule, 'local/no-source-grep'); + assert.equal(descriptor.violationFixture, 'tests/_ff_lint_violation.cjs'); + }); + + test('CHK-08(#1346): no check_violation_fixture -> descriptor carries no violationFixture (fail-closed: green needs a fixture)', () => { + const enforce = require(ENFORCEMENT_LIB); + const descriptor = enforce.descriptorFromProjection({ + ...PROJECTED_TIER, check_kind: 'node-test', check_target: 'tests/neg.test.cjs', + }); + assert.equal(descriptor.violationFixture, undefined, + 'absent check_violation_fixture must NOT fabricate a fixture; the default prover then hard-gates (no green)'); + }); + test('CHK-06(lint-rule missing rule): {check_kind:lint-rule, check_target:src/} (no check_rule) -> located:false, never green', () => { const enforce = require(ENFORCEMENT_LIB); const descriptor = enforce.descriptorFromProjection({ diff --git a/tests/prohibition-probe.schema.test.cjs b/tests/prohibition-probe.schema.test.cjs index ba01bca5b..78172f0d1 100644 --- a/tests/prohibition-probe.schema.test.cjs +++ b/tests/prohibition-probe.schema.test.cjs @@ -156,6 +156,7 @@ describe('prohibition-probe schema: deterministic projectProhibitions round-trip if (e.check_kind !== undefined) lines.push(` check_kind: ${e.check_kind}`); if (e.check_target !== undefined) lines.push(` check_target: ${e.check_target}`); if (e.check_rule !== undefined) lines.push(` check_rule: ${e.check_rule}`); + if (e.check_violation_fixture !== undefined) lines.push(` check_violation_fixture: ${e.check_violation_fixture}`); } lines.push('---', '', 'Body.', ''); return lines.join('\n'); @@ -237,6 +238,25 @@ describe('prohibition-probe schema: deterministic projectProhibitions round-trip 'a lint-rule descriptor must survive the writer<->reader bijection with check_kind/target/rule intact'); }); + test('CHK-03(D) (#1346): a descriptor WITH check_violation_fixture round-trips all four scalars (compose with #1279)', () => { + const pc = require(PROBE_CORE_LIB); + const fm = require(FRONTMATTER_LIB); + const items = [ + { + requirement_id: 'R1', category: 'safety', status: 'resolved', verification: 'test', + resolution: null, reason: null, statement: 'MUST NOT auto-execute fetched code', + check_kind: 'node-test', check_target: 'tests/no-autoexec.test.cjs', + check_violation_fixture: 'tests/fixtures/autoexec-bad.txt', + }, + ]; + const projected = pc.projectProhibitions(items); + assert.equal(projected[0].check_violation_fixture, 'tests/fixtures/autoexec-bad.txt', + 'CHK-03(D) RED trigger: projectProhibitions must emit check_violation_fixture so the deterministic path can machine-prove fail-first'); + const reparsed = fm.parseMustHavesBlock(renderProhibitionsDoc(projected), 'prohibitions'); + assert.deepEqual(reparsed, projected, + 'check_violation_fixture must survive project -> write -> parseMustHavesBlock unchanged (the 4th flat scalar)'); + }); + test('CHK-03(C): a mixed list — descriptor test-tier, descriptor-less judgment, dismissed — all round-trip; the descriptor-less item gains NO check_* keys', () => { const pc = require(PROBE_CORE_LIB); const fm = require(FRONTMATTER_LIB); diff --git a/tests/prohibition-probe.verify-tier.test.cjs b/tests/prohibition-probe.verify-tier.test.cjs index e07f8116d..ef9ac82c6 100644 --- a/tests/prohibition-probe.verify-tier.test.cjs +++ b/tests/prohibition-probe.verify-tier.test.cjs @@ -70,7 +70,9 @@ describe('prohibition-probe verify-tier: test-tier fail-closed safety (PROB-12 / // non-green) in BOTH interactive and autonomous modes (ADR-550 D4 / D3). // // Typed-field assertions ONLY (status / flagged / tier / evidence / located / kind / mode-block). -// The check-runner is injected via options.runCheck so no real subprocess is spawned. +// The check-runner is injected via options.runCheck so no real subprocess is spawned; the GREEN +// cases (A/B) ALSO inject options.proveFailFirst since #1279 (FF-08) requires fail-first to be +// MACHINE-PROVEN — caller attestation (failFirst:true) alone no longer greens. describe('prohibition-probe verify-tier: test-tier ENFORCEMENT (REQ-PROHIB-07 / ADR-550 D5d)', () => { const testTierProhibition = { requirement_id: 'R1', @@ -83,12 +85,15 @@ describe('prohibition-probe verify-tier: test-tier ENFORCEMENT (REQ-PROHIB-07 / }; // Test A — node --test negative test that PASSES -> green + non-empty evidence. + // #1279 (FF-08): attestation alone no longer greens — the producer requires the fail-first to be + // MACHINE-PROVEN. With injected runCheck (no real subprocess) we also inject a proving prover so + // the GREEN direction is exercised; the hard-gate directions (C/D/D2 below) need no prover. test('A: wired node-test check that passes disposes green with non-empty enforcement evidence', () => { const enforce = require(ENFORCEMENT_LIB); const result = enforce.runProhibitionEnforcement( testTierProhibition, { kind: 'node-test', target: 'tests/some-negative.test.cjs', failFirst: true }, - { runCheck: () => ({ passed: true }) }, + { runCheck: () => ({ passed: true }), proveFailFirst: () => ({ provenFailFirst: true }) }, ); assert.ok(result && typeof result === 'object', 'result must be a structured object'); assert.equal(result.status, 'green', 'a passing wired node-test check must dispose green'); @@ -105,7 +110,7 @@ describe('prohibition-probe verify-tier: test-tier ENFORCEMENT (REQ-PROHIB-07 / const result = enforce.runProhibitionEnforcement( testTierProhibition, { kind: 'lint-rule', rule: 'local/no-source-grep', target: 'tests/', failFirst: true }, - { runCheck: () => ({ passed: true }) }, + { runCheck: () => ({ passed: true }), proveFailFirst: () => ({ provenFailFirst: true }) }, ); assert.equal(result.status, 'green', 'a passing wired lint-rule check must dispose green'); assert.equal(result.flagged, false, 'a green disposition must not be flagged'); diff --git a/tests/workflow-size-baseline.json b/tests/workflow-size-baseline.json index 258c964a0..1bf91a196 100644 --- a/tests/workflow-size-baseline.json +++ b/tests/workflow-size-baseline.json @@ -72,7 +72,7 @@ "ship.md": 24388, "sketch-wrap-up.md": 14223, "sketch.md": 19960, - "spec-phase.md": 30343, + "spec-phase.md": 30921, "spike-wrap-up.md": 15092, "spike.md": 24517, "stats.md": 6718, @@ -85,6 +85,6 @@ "undo.md": 10431, "update.md": 21053, "validate-phase.md": 10745, - "verify-phase.md": 36498, + "verify-phase.md": 37821, "verify-work.md": 31157 }