Merge pull request #1314 from davesienkowski/feat/1279-fail-first-prover
This commit is contained in:
Rezolv
10
.changeset/1279-machine-proven-fail-first.md
Normal file
10
.changeset/1279-machine-proven-fail-first.md
Normal file
@@ -0,0 +1,10 @@
|
||||
---
|
||||
type: Changed
|
||||
pr: 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.
|
||||
@@ -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)
|
||||
|
||||
@@ -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=<violationFixture>` in the child env; the test reads that env var to locate the subject-under-test and is expected to go RED against the violating subject. The synthetic temp fixtures in `tests/prohibition-enforcement.test.cjs` demonstrate a test that honors the convention (defaulting to a clean in-dir subject when the env var is absent, so the plain run passes non-vacuously while the prover's run goes red).
|
||||
|
||||
- **(c) The `failFirst` DEMOTION (FF-08).** `CheckDescriptor.failFirst` is **kept** (so the #1259 route-JSON shape and the `CheckDescriptor` type stay backward-compatible for any caller mid-migration) but **DEMOTED to a non-authoritative hint** — the machine prover supersedes it and **no path greens on attestation alone**. Removal was rejected as it breaks the route-JSON shape mid-migration; demote-and-ignore is safer and still satisfies "no path greens on attestation."
|
||||
|
||||
> **PR-review flag — PROPOSED, renamable conventions (zero live consumers).** Both **`GSD_PROHIB_SUBJECT`** and **`CheckDescriptor.violationFixture`** are net-new surface introduced by this PR with **ZERO live in-tree consumers** — there is no in-tree `node --test` prohibition yet (the #1259 dogfood anchor and the #1279 lint-rule dogfood are both the LINT-rule `local/no-source-grep`; node-test fail-first is exercised only by SYNTHETIC temp fixtures in tests). They are therefore forward-looking scaffolding, and a later rename (or replacing the env var with an argv) is a **mechanical, zero-migration find/replace**. They are surfaced here explicitly so the maintainer can **rename or replace them at PR review** — the natural ratification point, exactly as #1278's ADR addendum was reviewed at PR time — without any migration cost. The `failFirst` DEMOTION is likewise open to the reviewer weighing outright removal; the rationale for keeping it as a hint is recorded above.
|
||||
|
||||
Net effect on D4: the *guarantee* ("a `test`-tier prohibition is never a silent pass") was preserved at every step — fail-closed-now (#644), genuine-execution (#1259), and now **machine-proven fail-first (#1279)**. A `test`-tier prohibition reaches `green`/`passed` ONLY when the wired check both genuinely, non-vacuously passes AND is independently proven to fail on a violation; every miss/fail/un-provable hard-gates. The decision also lives in `src/prohibition-enforcement.cts` comments, `gsd-core/references/prohibition-probe.md`, `gsd-core/workflows/verify-phase.md`, and the #1279 changeset.
|
||||
|
||||
**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.
|
||||
|
||||
@@ -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' },
|
||||
},
|
||||
);
|
||||
|
||||
@@ -112,15 +112,38 @@ lifecycle is identical to the edge-probe, the verification tiers differ):
|
||||
|
||||
At verify time these tiers are routed differently (ADR-550 D4):
|
||||
- A **test**-tier prohibition is enforced + hard-gates via the deterministic
|
||||
`check prohibition-enforcement` sub-command (#1259, ADR-550 D5d): it locates the wired
|
||||
`check prohibition-enforcement` sub-command (#1259 + #1279, ADR-550 D5d): it locates the wired
|
||||
mechanical check (a `node --test` negative test OR a lint/AST rule run as
|
||||
`eslint --format json` and filtered by `ruleId`), requires the caller-attested `failFirst`
|
||||
marker, runs it for a genuine **non-vacuous** pass, and emits the
|
||||
`dispositionForProhibition()` verdict. A passing wired check disposes **green** (satisfiable
|
||||
→ can reach `passed`); a missing, non-attested, or genuinely-non-passing check **hard-gates**
|
||||
(flagged, never green → `gaps_found`) in BOTH interactive and autonomous modes — never a
|
||||
silent pass. (`failFirst` is caller-attested, not yet machine-proven against a violation
|
||||
fixture — a tracked follow-up; see ADR-550 D5d.)
|
||||
`eslint --format json` and filtered by `ruleId`), **machine-proves it is fail-first** against a
|
||||
known violation, runs it for a genuine **non-vacuous** pass, and emits the
|
||||
`dispositionForProhibition()` verdict. A passing, fail-first-proven wired check disposes **green**
|
||||
(satisfiable → can reach `passed`); a missing, un-provable, or genuinely-non-passing check
|
||||
**hard-gates** (flagged, never green → `gaps_found`) in BOTH interactive and autonomous modes —
|
||||
never a silent pass.
|
||||
|
||||
**Machine-proven fail-first (#1279).** `failFirst` is now **machine-proven, not caller-attested**:
|
||||
before a clean pass greens, the producer independently runs the wired check against a KNOWN
|
||||
VIOLATION and confirms it goes RED (any other outcome — passes-on-violation, can't-prove, throws,
|
||||
times out, no violation source — hard-gates). The violation is sourced from a descriptor field:
|
||||
- **`violationFixture`** — an author-supplied path to a KNOWN-BAD subject. For `lint-rule`: a file
|
||||
whose content violates `rule`; the prover lints it and requires the rule id to appear in the
|
||||
JSON report (the rule must have teeth). For `node-test`: a subject the negative test exercises,
|
||||
expected to drive it RED.
|
||||
- **`GSD_PROHIB_SUBJECT`** — the node-test subject-injection convention: the producer spawns the
|
||||
negative test with `GSD_PROHIB_SUBJECT=<violationFixture>` in the child env; the test reads that
|
||||
env var to locate its subject-under-test and is expected to go red against the violating subject.
|
||||
- **lint-fixture authoring gotcha** — the violating fixture must actually trigger the rule. For the
|
||||
`local/no-source-grep` dogfood anchor specifically, use the `path.join('lib','foo.cjs')` form
|
||||
(a standalone quoted dir token); a single string literal like `'src/x.cjs'` does NOT trigger the
|
||||
rule, so a mis-authored fixture makes the prover report "not proven" and hard-gate a legitimately
|
||||
wired check. (`no-source-grep` has no filename guard — any `.cjs` with the pattern fires.)
|
||||
|
||||
> **PROPOSED, renamable conventions (zero live consumers).** Both `GSD_PROHIB_SUBJECT` and
|
||||
> `violationFixture` are net-new surface with **no live in-tree consumer yet** — there is no
|
||||
> in-tree `node --test` prohibition; node-test fail-first proof is exercised only by SYNTHETIC
|
||||
> temp fixtures in the tests, and the real dogfood remains the LINT-rule `local/no-source-grep`.
|
||||
> They are therefore **open to maintainer adjustment (rename, or replacing the env var with an
|
||||
> argv) at PR review with zero migration cost.** See the ADR-550 2026-06-15 addendum (#1279).
|
||||
- A **judgment**-tier prohibition routes to a never-silent / never-hard-halt soft gate
|
||||
(autonomous emits an `unverified-prohibition — human review recommended` flag).
|
||||
|
||||
@@ -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
|
||||
|
||||
|
||||
@@ -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.
|
||||
|
||||
|
||||
@@ -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 <request.json>
|
||||
```
|
||||
|
||||
where `<request.json>` carries `{ prohibition, check, mode }` — `check` being the wired mechanical-check descriptor `{ kind: 'node-test' | 'lint-rule', target, rule?, failFirst: true }`, 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 `<request.json>` 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**
|
||||
|
||||
|
||||
@@ -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);
|
||||
}
|
||||
|
||||
@@ -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 - <name>` / `not ok N - <name>` 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 - <name>` 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 - <file>` 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 {
|
||||
|
||||
27
tests/_ff_lint_violation.cjs
Normal file
27
tests/_ff_lint_violation.cjs
Normal file
@@ -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');
|
||||
@@ -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;
|
||||
}
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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)');
|
||||
},
|
||||
));
|
||||
});
|
||||
});
|
||||
|
||||
@@ -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 - <file>`, `# 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=<bad fixture> -> 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({
|
||||
|
||||
@@ -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);
|
||||
|
||||
@@ -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');
|
||||
|
||||
@@ -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
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user