golem15/msd-core
3
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

enhance(verify-phase): node-test causation control — prove the RED is content-caused (#1346)

Browse Source 
The #1279 node-test machine-proof confirmed a known-bad subject drives the
negative test RED, but could not distinguish a genuine content-violation from a
deceptive test that reds merely because GSD_PROHIB_SUBJECT is set. Add an
optional fifth flat scalar `check_clean_fixture` (-> CheckDescriptor.cleanFixture)
threading a KNOWN-CLEAN control subject through projectProhibitions +
descriptorFromProjection. When present, the prover also runs the check against
the clean subject and requires GREEN, so fail-first is proven only when the check
is RED on the violation AND GREEN on the clean subject (content-dependent).

Opt-in and additive: absent a clean fixture the prover behaves exactly as
post-#1314 (no control, documented residual), preserving the zero-authoring
compose path; the lint-rule kind needs no analog (its subject IS the linted
file, no env indirection). Coverage: RED-first deceptive case, positive,
missing-clean fail-closed, round-trip read-back/emit, fast-check property
extended to the 5th scalar, and an end-to-end COMPOSE capstone (honest vs
deceptive). Docs: ADR-550 dated addendum, prohibition-probe reference,
spec-phase + verify-phase workflows.

Closes #1346

Claude-Session: https://claude.ai/code/session_01GsPRb8zvpcT7Eat6vZw8PX
This commit is contained in:
Dave
2026-06-21 10:44:48 -04:00
parent eb81faaeab
commit c09c13f295
11 changed files with 323 additions and 50 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
src/probe-core.cts
View File

@@ -303,6 +303,11 @@ export interface Prohibition {
// 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;
// Optional 5th flat scalar (#1346): the path to a KNOWN-CLEAN control subject the prover ALSO runs
// the check against, requiring it to stay GREEN — proving the violation RED is caused by the
// subject's CONTENT, not merely by GSD_PROHIB_SUBJECT being set. Projected only alongside a
// well-formed descriptor; absent -> no control (documented residual). Mirrors `CheckDescriptor.cleanFixture`.
check_clean_fixture?: string;
}
/**
@@ -387,6 +392,13 @@ export function projectProhibitions(
if (typeof p.check_violation_fixture === 'string' && p.check_violation_fixture.trim() !== '') {
entry.check_violation_fixture = String(p.check_violation_fixture);
}
// `check_clean_fixture` (#1346) rides BOTH kinds — the KNOWN-CLEAN control subject the prover
// requires to stay GREEN (content-dependence proof). Emit ONLY a non-empty fixture (blank ->
// absent so no control runs; the documented residual remains). Like the violation fixture it is
// meaningless without the descriptor, so it lives inside this well-formed-descriptor branch.
if (typeof p.check_clean_fixture === 'string' && p.check_clean_fixture.trim() !== '') {
entry.check_clean_fixture = String(p.check_clean_fixture);
}
}
out.push(entry);
}

89
src/prohibition-enforcement.cts
View File

@@ -76,6 +76,15 @@ export interface CheckDescriptor {
* prove fail-first; ABSENT for node-test → the default prover fails closed (never attestation).
*/
violationFixture?: string;
/**
* OPTIONAL author-supplied path to a KNOWN-CLEAN control subject (#1346). When present, the prover
* runs the check against it as a CAUSATION CONTROL and requires it to stay GREEN — proof that the
* RED on `violationFixture` was caused by the subject's CONTENT, not merely by `GSD_PROHIB_SUBJECT`
* being set. A deceptive content-independent check reds on the clean subject too → control fails →
* not proven. ABSENT → no control runs (the documented residual remains; backward-compatible with
* the #1314 zero-authoring compose path). A supplied-but-missing path fails closed.
*/
cleanFixture?: string;
}
/**
@@ -90,8 +99,9 @@ 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, and `violationFixture: check_violation_fixture`
* ONLY when that scalar is a non-empty string (#1346 — composes #1278 locate with #1279 proof).
* ONLY when `check_rule` is a non-empty string, `violationFixture: check_violation_fixture`
* ONLY when that scalar is a non-empty string (composes #1278 locate with #1279 proof), and
* `cleanFixture: check_clean_fixture` ONLY when that scalar is non-empty (#1346 causation control).
* - `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
@@ -128,6 +138,12 @@ export function descriptorFromProjection(
// 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;
// `cleanFixture` (#1346) rides BOTH kinds — reconstruct it from `check_clean_fixture` so the
// causation control runs end-to-end: when present the prover also requires the check to stay GREEN
// against this known-clean subject (proving the violation RED is content-dependent). Absent/blank ->
// no control (the documented residual remains; backward-compatible with the #1314 compose path).
const clean = scalar(projected.check_clean_fixture);
if (clean.trim().length > 0) descriptor.cleanFixture = clean;
return descriptor;
}
@@ -438,6 +454,31 @@ function posTimeout(timeoutMs: number | undefined, def: number): number {
return typeof timeoutMs === 'number' && timeoutMs > 0 ? timeoutMs : def;
}
/**
* Spawn the negative `node --test` against a single subject (set via the `GSD_PROHIB_SUBJECT`
* convention, #1279) and return its TAP output. Reuses the bounded-subprocess machinery
* (`process.execPath`, arg arrays → no shell, `childEnv`, bounded `timeout`/`maxBuffer`) and NEVER
* throws — a RED run exits non-zero, so the partial TAP (with the `# fail` summary) is recovered from
* the thrown error's `stdout`. The prover calls this once per subject: the KNOWN-BAD violation fixture
* (expect RED) and, for the #1346 causation control, the KNOWN-CLEAN control subject (expect GREEN).
*/
function runNodeTestWithSubject(check: CheckDescriptor, cwd: string, subject: string, timeoutMs?: number): string {
try {
return execFileSync(process.execPath, buildNodeTestArgs(check), {
cwd,
encoding: 'utf-8',
stdio: ['ignore', 'pipe', 'pipe'],
windowsHide: true,
env: { ...childEnv(), GSD_PROHIB_SUBJECT: subject },
timeout: posTimeout(timeoutMs, NODE_TEST_TIMEOUT_MS),
maxBuffer: CHECK_MAX_BUFFER,
});
} catch (e) {
const stdout = e && typeof e === 'object' && 'stdout' in e ? (e as { stdout?: unknown }).stdout : '';
return typeof stdout === 'string' ? stdout : '';
}
}
function defaultRunCheck(check: CheckDescriptor, cwd: string, timeoutMs?: number): CheckRunResult {
try {
if (check.kind === 'node-test') {
@@ -554,34 +595,32 @@ function defaultProveFailFirst(check: CheckDescriptor, cwd: string, timeoutMs?:
// 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.
// CAUSATION (#1346): existence + a non-vacuous red is necessary but not sufficient — a deceptive
// negative test that reds merely BECAUSE `GSD_PROHIB_SUBJECT` is set (rather than because the
// subject's CONTENT violates the must-NOT) would otherwise be accepted. The OPTIONAL `cleanFixture`
// control below proves content-dependence when supplied (red on bad AND green on clean). When NO
// clean fixture is authored the control cannot run, so the residual remains a documented constraint
// for that case (an author opts into the stronger proof by supplying a known-clean control subject).
// 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 : '';
// Run the negative test against the KNOWN-BAD subject and require a NON-VACUOUS red.
const redOut = runNodeTestWithSubject(check, cwd, fixture, timeoutMs);
if (!isNonVacuousNodeTestRed(redOut, check.target)) return { provenFailFirst: false, method: 'violation-fixture' };
// #1346 CAUSATION CONTROL (optional): if a clean control subject is supplied, run the SAME test
// against it and require it to stay GREEN. This proves the red above was caused by the subject's
// CONTENT — a deceptive test that reds merely because GSD_PROHIB_SUBJECT is SET reds here too →
// not content-dependent → not proven. Absent → no control (documented residual; backward-compat).
const clean = check.cleanFixture;
if (clean) {
// A supplied-but-missing/typo'd control path can't run the control → fail-closed, symmetric
// with the violation-fixture existence guard (resolve against the SAME `cwd` as the child).
if (!fs.existsSync(path.resolve(cwd, clean))) return { provenFailFirst: false, method: 'violation-fixture' };
const cleanOut = runNodeTestWithSubject(check, cwd, clean, timeoutMs);
if (!isNonVacuousNodeTestPass(cleanOut, check.target)) return { provenFailFirst: false, method: 'violation-fixture' };
}
return { provenFailFirst: isNonVacuousNodeTestRed(out, check.target), method: 'violation-fixture' };
return { provenFailFirst: true, method: 'violation-fixture' };
}
// Unknown kind — defensive; the LOCATE guard already rejects it.
return { provenFailFirst: false };