Files
msd-core/gsd-core/references/prohibition-probe.md
Rezolv e50ead7ad2 enhance(verify-phase): deterministic auto-locate of the prohibition check descriptor (#1278) (#1301)
* test(1278): RED-first descriptor parity + fail-closed guards + CHK-07 byte-stability (wave 1)

- CHK-03 (RED): extend PROB-14 parity in prohibition-probe.schema.test.cjs to carry the flat
  check_kind/check_target/check_rule scalars through project->write->parseMustHavesBlock; the
  non-droppable check_kind-presence assertion is the load-bearing RED trigger (fails because
  projectProhibitions strips check_* on the current build).
- CHK-07 (GREEN forward-guard): probe-core.test.cjs pins descriptor-less byte-stability +
  dispositionForProhibition fail-closed policy, with a t.todo marker forward-locking plan 01-02.
- CHK-06 (RED): prohibition-enforcement.test.cjs asserts descriptorFromProjection export +
  fail-closed on absent/partial/unknown descriptors via the projection adapter (RED until 01-03).
- No src/*.cts or .cjs edits; no new test files; lint-test-file-count clean.

* feat(1278): add optional flat-scalar check descriptor fields to Prohibition interface (wave 2)

- check_kind?/check_target?/check_rule? mirror CheckDescriptor.kind/target/rule (minus caller-attested failFirst, #1279)
- optional so existing Prohibition consumers compile unchanged

* feat(1278): project check descriptor as flat scalars in projectProhibitions (wave 2)

- emit check_kind/check_target (+ check_rule only for lint-rule with a rule) when descriptor well-formed
- under-specified/descriptor-less items project byte-identically (CHK-07); flat scalars ride existing parseMustHavesBlock continuation-KV path (no parser rewrite)
- add CHK-02 probe-core unit cases pinning the projection
- turns CHK-03 parity test GREEN; dispositionForProhibition untouched

* feat(1278): descriptorFromProjection read-back adapter feeds fail-closed locate (wave 3)

- Add descriptorFromProjection(projected) -> CheckDescriptor | null to
  src/prohibition-enforcement.cts: renames the projected flat scalars
  check_kind/check_target/check_rule -> {kind,target,rule?}, or null when
  the descriptor is absent/non-object (no check_kind key).
- failFirst is NEVER sourced from the projection (stays caller-attested; #1279).
- rule is set only when check_rule is a non-empty string; the adapter does NOT
  re-validate kind/target/rule — an under-specified descriptor reconstructs to
  one the EXISTING runProhibitionEnforcement LOCATE guard rejects (located:false,
  never green). The merged #1259 guard stays the single source of fail-closed truth.
- Turns the RED CHK-06 fail-closed tests (plan 01-01) GREEN end-to-end; CHK-03 /
  CHK-07 stay green. CheckDescriptor type, locate guard, dispositionForProhibition,
  and parseMustHavesBlock are unchanged (additive +36/-0).

* feat(1278): verify-phase locates prohibition check from projected descriptor (wave 3)

- request.check kind/target/rule sourced from projected check_kind/check_target/check_rule via descriptorFromProjection, not verifier invention (CHK-05)
- replaces the #1278 author-supplied / tracked-follow-up note with the delivered deterministic-locate behavior
- preserves fail-closed routing: absent/partial descriptor -> never green, hard-gate in both modes
- failFirst stays a verify-time caller attestation; #1279 bounds the remaining fail-first proof

* feat(1278): spec-phase captures wired-check descriptor on test-tier resolution (wave 3)

- Step 5.6 'Keep it' / verification: test path captures check_kind/check_target/check_rule, projected onto must_haves.prohibitions for verify-phase deterministic locate (CHK-04)
- SOFT capture: a test-tier prohibition without a descriptor is still allowed (no hard authoring block); stays fail-closed/flagged downstream
- --auto captures only an unambiguous descriptor, never fabricates a check path
- failFirst NOT captured at spec-phase (verify-time attestation; #1279)
- PROB-06 soft-gate + text-mode (PROB-09) behavior unchanged

* chore(1278): re-baseline workflow size for grown verify-phase + spec-phase prose (wave 3)

- spec-phase.md 28438 -> 30343 (+1905), verify-phase.md 35362 -> 36498 (+1136)
- regenerated via npm run size:baseline (no hand-picked numbers); growth is the #1278 deterministic-locate + descriptor-capture prose
- workflow-size-budget guard green (122/122)

* docs(1278): ratify optional check descriptor in dated ADR-550 addendum + type:Changed changeset

- Append dated 2026-06-15 ADR-550 addendum ratifying the D3 prohibition-item
  shape extension (optional flat-scalar check_kind/check_target/check_rule)
- Document flat-scalar rationale, deterministic projection/read-back,
  fail-closed on partial/invalid/absent, #1279/policy out-of-scope
- Add .changeset/1278-prohibition-check-descriptor.md (type: Changed)

* docs(1278): document optional check descriptor in prohibition-probe reference + FEATURES

- Add 'Optional wired-check descriptor (deterministic locate, #1278)' section
  to the prohibition-probe reference (flat-scalar keys, projection/read-back,
  fail-closed + backward-compat, failFirst stays attested)
- Add deterministic prohibition-check descriptor source entry to FEATURES.md
- No CONTEXT.md glossary change: descriptor reuses existing wired-check /
  verification:test vocabulary, no new glossary term introduced

* fix(1278): pass packaging gates — changeset pr field + retired slash-form fix

- Add required pr: 1278 to changeset (lint:changeset MISSING_PR hard requirement;
  plan's 'omit if unknown' was inaccurate — issue number per #1259 convention,
  updated to real PR number when opened) [Rule 3 - blocking]
- Fix retired /gsd-spec-phase -> /gsd:spec-phase at verify-phase.md:83 (wave-3
  prose; caught by slash-namespace invariant #3443/bug-2543, blocked CHK-09
  full-suite-green) [Rule 1 - bug]
- size:baseline + INVENTORY manifest verified in-sync post-build (no diff)

* docs(1278): add check descriptor + descriptorFromProjection to CONTEXT.md prohibition glossary

* fix(1278): harden descriptorFromProjection round-trip (numeric-coercion + stray-rule) per review

- MD-01/LW-01: narrow projected scalars to primitives + String()-coerce, so a
  numeric-looking check_target (parseMustHavesBlock coerces ^\d+$ to number)
  reconstructs as a string and locates instead of silently un-locating; no
  as-string type-lie, satisfies no-base-to-string.
- LW-02: attach rule only for the lint-rule kind (drop a stray node-test rule).
- LW-03: document the optional check_* keys in the reference Output schema.
RED->GREEN tests added in prohibition-enforcement.test.cjs.

* chore(1278): set changeset pr to 1301

* test(1278): add fast-check property for the check-descriptor round-trip + fail-closed (trek-e review)

RULESET.TESTS.property-based-testing: the projectProhibitions -> render ->
parseMustHavesBlock -> descriptorFromProjection chain is a bijective/transformation
contract. Adds 2 fc properties to tests/probe-core.property.test.cjs (no new file;
ratchet stays at 2 for probe-core):
- well-formed descriptors survive the round-trip across the full string domain
  incl. the numeric-coercion case (target/rule reconstruct as strings);
- under-specified/invalid descriptors (absent / target-less / rule-less /
  unknown-kind) are always fail-closed (never green, flagged, unlocated).
Stability is asserted at the descriptorFromProjection layer (the raw parse step is
intentionally lossy for numeric scalars; the shared parser is unchanged).

---------

Co-authored-by: Tom Boucher <trekkie@nomorestars.com>
2026-06-16 00:01:03 -04:00

298 lines
17 KiB
Markdown
Raw Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
# Prohibition-Probe — Spec-Completeness Must-NOT Reference
Shared reference for the spec/requirements phase. Companion to
`@~/.claude/gsd-core/references/edge-probe.md`: `edge-probe` reaches the
**data/behavior-shape axis** (boundaries, adjacency, encoding, ordering) — the things a
feature must *do*. This reference reaches the orthogonal **must-NOT axis** (product, values,
safety, ethics) — the things a feature must *never silently become*. The edge-probe caught
0/8 of these in controlled testing because it is the wrong instrument: a shape taxonomy
cannot surface "the reminder must not shame the user." Walk each requirement through the
two-stage recall→precision protocol below and resolve each surfaced prohibition to exactly
one state.
This doc is written in generic `requirements → checks → verifier` terms with no
tool-specific vocabulary, so it is portable: copy it into any spec/requirements process.
A short mapping table at the end binds it to common host structures.
## Why front-of-pipeline
A goal-backward verifier only checks assertions that exist; an assertion only exists for a
requirement that was written down. The class of constraint this probe targets — the
*"must-NOT"* the author assumed but never wrote — is invisible to the verifier in exactly
the same way an omitted edge is, but with a sharper failure mode: a `✅ done` that means
"the code matches the words in the spec" can still ship a feature that does what the author
explicitly would *not* want. The manipulative-streak reminder, the loan model that proxies
on zip code, the audit log that stores raw SSN — each one passes a literal spec while
violating the intent. The fix is not a better verifier; it is **spec completeness**: surface
the omitted prohibition into an explicit, checkable acceptance criterion *before* any code
exists, after which the verifier reliably enforces it.
The technique is adversarial elicitation, not deterministic computation. Unlike the edge
taxonomy (a closed eight categories a classifier can apply), the recall stage is inherently
model-driven: it asks an open question and reads prose. There is **no compiled
`prohibition-probe.cjs` engine** — the recall stage is an LLM prose pass, and only the
schema/projection layer is real code (ADR-550 Decision 7b). Building a deterministic
recall adapter would be the scope-creep the maintainer flags.
## Inputs
A list of requirements, each a `{ id, text }` record where `text` is a testable statement.
There is no shape override and no taxonomy classifier — the recall stage reads the prose
directly and the precision stage filters its raw output. The probe runs **after** the
edge-probe in the spec phase, over the same requirement list.
## Two-stage protocol (recall → precision)
The probe is a two-pass pipeline per requirement. Stage 1 maximizes recall (cast wide);
Stage 2 restores precision (drop the noise). Running them in this order — wide then narrow —
is what keeps the surfaced list both complete and short.
**Stage 1 — Recall (adversarial probe).** Ask the single adversarial question of each
requirement:
> *What could this feature silently become that the author would NOT want, but the spec
> does not forbid?*
This question is model-robust (17/17 holistic surfacing including smaller models in the N18
experiment). It deliberately over-produces: ~10 raw candidates per requirement, including
routine engineering items. That over-production is intentional — recall first.
**Stage 2 — Precision (one-pass classifier).** Filter the raw Stage-1 list in a single pass.
The rule is a drop/keep split:
- **DROP routine-engineering items** — anything that is a normal correctness or hygiene
concern rather than an intent constraint: "must not mutate its input", "must not throw on
empty list", "must return a primitive not an object", "must not leak a file handle". These
belong to the edge-probe or to ordinary code review, not here.
- **KEEP values / safety / ethics items** — anything that, if violated, makes the feature do
something the author would object to on product, fairness, privacy, transparency, or
safety grounds: "must not use shaming framing", "must not proxy on protected attributes",
"must not store raw PII in plaintext".
This collapses the raw ~10 to ~2–3 genuine prohibitions (GT 5/5, 0 false positives on the
N18 eight-spec battery). A requirement that yields zero kept prohibitions emits an empty
list — that is the correct precision outcome for a pure utility, not a failure.
## Canon-referral (do not mint canon items)
Some kept candidates are not bespoke at all — they are **canon** security/compliance
constraints that a dedicated tool already owns. Do NOT mint a prohibition for them. Instead
emit a one-line breadcrumb and stop:
- OWASP / prototype-pollution / path-traversal / injection → breadcrumb to `/gsd:secure-phase`
and `eslint` (security plugins), not a minted prohibition.
- GDPR / data-retention / consent → breadcrumb to `/gsd:secure-phase`.
- Generic fairness/bias canon → breadcrumb to `/gsd:secure-phase`.
The breadcrumb reads like: *"prototype-pollution is canon — covered by /gsd:secure-phase +
eslint; not minted here."* This keeps the surfaced list to the ~2–3 **bespoke** items that
no other tool would catch — the manipulative-framing prohibition, the product-specific
fairness constraint — which is the whole value of the probe. Minting canon items both
duplicates other tooling and drowns the bespoke signal (ADR-550 Decision 6).
## Resolution states
Each surfaced prohibition carries two orthogonal axes — a resolution **lifecycle** and, when
resolved, a **verification** tier (ADR-550 Decision 7, the shared probe-core model; the
lifecycle is identical to the edge-probe, the verification tiers differ):
- **status** — `resolved | dismissed | unresolved` (IDENTICAL to the edge-probe):
- **resolved** — the prohibition is addressed; *how* it is addressed is the verification tier.
- **dismissed** — not a genuine prohibition for this feature, accompanied by a required,
non-empty reason string. "N/A — this utility has no user-facing surface, no values
constraint applies" is valid; silence is not. The reason string is the audit trail.
- **unresolved** — carried forward and flagged; the author chose not to resolve it yet.
- **verification** (only when `status` is `resolved`; `null` otherwise) — `test | judgment`
(this REPLACES the edge-probe's `explicit | backstop`):
- **test** — the prohibition can be mechanically checked (a negative test, a lint rule, an
assertion that the audit log contains no raw SSN). A checkable assertion exists.
- **judgment** — the prohibition is real but cannot be reduced to a mechanical test (a
human/LLM judgment that the framing is not manipulative). It records intent and routes
to a judgment-based review rather than a green/red test.
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
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.)
- A **judgment**-tier prohibition routes to a never-silent / never-hard-halt soft gate
(autonomous emits an `unverified-prohibition — human review recommended` flag).
Splitting these axes keeps the lifecycle enum free of a verification fact and lets the
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)
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: {}`
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`).
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**.
**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).
## Output schema
The probe emits, per kept prohibition, an item of the form:
```
{ requirement_id, category, status, verification, resolution, reason, statement,
check_kind?, check_target?, check_rule? }
```
where `statement` is the must-NOT sentence and `category` is the values/safety/ethics class
(`values`, `fairness`, `privacy`, `transparency`, `safety`, …). The optional **flat-scalar
`check_*` descriptor** (#1278) is present only on a resolved `test`-tier prohibition carrying a
wired check: `check_kind` (`node-test` | `lint-rule`), `check_target`, and `check_rule` (lint-rule
only). `projectProhibitions` emits these into `must_haves.prohibitions` and `descriptorFromProjection`
reads them back into a `{ kind, target, rule? }` `CheckDescriptor`; they are flat scalars (never a
nested `check:{}` object) so they round-trip through the unchanged `parseMustHavesBlock`. Plus a
coverage summary:
```
coverage: { applicable, resolved, unresolved, byVerification: { test, judgment } }
```
`applicable` is the number of kept prohibitions, `resolved` = closed (`resolved` +
`dismissed`) status items, `unresolved` is the remainder, and `byVerification` breaks the
`resolved`-status items down by tier (`{ test, judgment }`). This JSON is the stable contract
both the reference implementation and any third-party port emit.
## Generic mapping (requirements → checks → verifier)
| Host structure | "requirement" | a `resolved`/`test` prohibition becomes | a `resolved`/`judgment` prohibition becomes |
|----------------|---------------|------------------------------------------|----------------------------------------------|
| GSD SPEC | a SPEC Requirement | a SPEC acceptance criterion (marked prohibition) that `plan-phase` lifts into `must_haves.prohibitions` | a `must_haves.prohibitions` item routed to judgment review |
| Gherkin feature | a Scenario | a negative `Then` assertion / tagged negative scenario | a tagged scenario routed to manual review |
| OpenAPI operation | an operation | a contract test asserting the forbidden behavior never occurs | a documented constraint flagged for review |
| Docstring contract | a documented behavior | a negative assertion in the contract test | a documented must-NOT for reviewers |
The portable invariant: a `resolved`/`test` prohibition produces **a checkable negative the
verifier iterates over** (GSD: a `must_haves.prohibitions` item with a test); a
`resolved`/`judgment` prohibition produces a recorded intent routed to judgment review. An
`unresolved` prohibition is an explicit assumption the downstream planner must surface, not
silently drop.
## Worked example (streak-reminder)
A single requirement to send a daily habit reminder. The edge-probe sees a `stateful`
requirement and asks about idempotency; the prohibition-probe asks the adversarial question
and surfaces what the reminder must never *become*. Stage 1 over-produces ("must not spam",
"must not throw on a deleted habit", "must not use shaming framing"); Stage 2 drops the
routine-engineering items and keeps the one genuine values prohibition:
```json prohibition-probe:01-streak-reminder/expected.json
{
"items": [
{
"requirement_id": "R1",
"category": "values",
"status": "resolved",
"verification": "judgment",
"resolution": null,
"reason": null,
"statement": "MUST NOT use shaming, guilt, or loss-aversion streak framing (e.g. \"Don't lose your streak!\") — the reminder must encourage without penalty framing"
}
],
"coverage": { "applicable": 1, "resolved": 1, "unresolved": 0, "byVerification": { "test": 0, "judgment": 1 } }
}
```
The kept prohibition is `judgment`-tier: "manipulative framing" cannot be reduced to a
mechanical test, so it records intent and routes to judgment review — but it is now an
explicit acceptance criterion the spec must clear, not an unwritten assumption.
## Worked example (clean-utility)
A pure utility requirement — "deduplicate a list of integers" — has no user-facing surface,
no values/safety/ethics dimension. Stage 1 still over-produces ("must not mutate the input",
"must not change order"), but every candidate is routine engineering that Stage 2 drops (and
the edge-probe already owns). The correct precision outcome is an empty prohibition list — a
zero, not a false positive:
```json prohibition-probe:02-clean-utility/expected.json
{
"items": [],
"coverage": { "applicable": 0, "resolved": 0, "unresolved": 0, "byVerification": { "test": 0, "judgment": 0 } }
}
```
This is the precision discipline that keeps the probe from crying wolf: a utility with no
intent surface produces zero prohibitions, so a non-empty list always carries signal.
## Worked example (multi-prohibition)
A loan-decision requirement is the high-stakes case: it surfaces several distinct
prohibitions across categories. Stage 1 produces a long list including canon items
(prototype-pollution, generic GDPR retention) that canon-referral breadcrumbs out; Stage 2
keeps the three bespoke values/safety items — a `fairness` constraint, a `privacy` constraint
(`test`-tier, mechanically checkable against the audit log), and a `transparency` constraint:
```json prohibition-probe:03-multi-prohibition/expected.json
{
"items": [
{
"requirement_id": "R1",
"category": "fairness",
"status": "resolved",
"verification": "judgment",
"resolution": null,
"reason": null,
"statement": "MUST NOT use protected attributes (race, gender, age, national origin) or their proxies (zip code, name) in the loan decision or rate"
},
{
"requirement_id": "R1",
"category": "privacy",
"status": "resolved",
"verification": "test",
"resolution": null,
"reason": null,
"statement": "MUST NOT store raw PII / financial secrets (SSN, full account or card numbers) in plaintext in the audit log"
},
{
"requirement_id": "R1",
"category": "transparency",
"status": "resolved",
"verification": "judgment",
"resolution": null,
"reason": null,
"statement": "MUST NOT mislead or omit the true rate/APR/terms in the explanation; an adverse decision must state the real principal reason (adverse-action)"
}
],
"coverage": { "applicable": 3, "resolved": 3, "unresolved": 0, "byVerification": { "test": 1, "judgment": 2 } }
}
```
The `privacy` row is `test`-tier — "no raw SSN in the audit log" is a mechanical assertion —
while `fairness` and `transparency` are `judgment`-tier. The byVerification rollup
`{ test: 1, judgment: 2 }` is the count-preserved breakdown of the three `resolved`-status
items. Each worked-example block above is kept byte-for-byte (parsed-JSON) identical to its
fixture under `gsd-core/references/prohibition-probe-fixtures/` by
`tests/prohibition-probe.docs-fixtures.test.cjs`, so the doc and the reference data cannot
silently drift.