fix(quality): prove criterion binding semantics
ci/woodpecker/pr/ci Pipeline was successful

This commit is contained in:
2026-08-01 00:17:50 -05:00
parent 9b4d4beb0e
commit 38f1b249cc
9 changed files with 414 additions and 79 deletions
+3 -3
View File
@@ -14,8 +14,8 @@ Investigate any of these immediately:
## Updating a gate
1. Add or change the criterion and exact case.
2. Observe the case fail for its own stated reason.
1. Add or change the criterion, its exact criterion-side `caseRefs`, and matching case-side `criterionIds`.
2. Observe the must-fail case fail for its own stated reason; moving the binding to any undeclared case must fail verification.
3. Declare an exact inerting mutation and observe the verifier detect it.
4. If required and actual behavior differ, add a tracked remediation owner and justification.
5. If meaning changed, append provenance; never replace the original silently.
@@ -32,4 +32,4 @@ Provider evidence input is an optional JSON array of normalized pipeline records
PR CI executes current-tree verification only, unprivileged and fail-closed. It does not execute isolated own-tree replay: RM-60 must provide a protected launcher or runner-level rootless sandbox before any PR-controlled executable/configuration is evaluated. Repo-only code cannot safely grant itself the capability intended to contain itself.
The deferred replay implementation remains hard-fail when its sandbox cannot be established; it is not silently skipped as a successful replay. When RM-60 activates it under protected authority, it uses frozen own-tree dependencies, namespace/environment isolation, and archived-file identity checks. A post-merge failure triggers quarantine and revert. This is detection, not pre-merge prevention.
The deferred replay implementation remains hard-fail when its sandbox cannot be established; it is not silently skipped as a successful replay. Tests recognize unavailability only from parent-generated Bubblewrap-launch provenance combined with proof that the sandbox entry command did not run. A denial-looking string from child-controlled output is not evidence. When RM-60 activates replay under protected authority, it uses frozen own-tree dependencies, namespace/environment isolation, and archived-file identity checks. A post-merge failure triggers quarantine and revert. This is detection, not pre-merge prevention.
@@ -20,7 +20,9 @@ The queue guard currently has RM-03-owned deltas. In particular, its stdin/hered
## Criteria, prose, and compatibility
Each criterion must bind to a must-fail case. Designated governing prose uses `GATE-CLAIM:<id>` markers; an unbound marker or registered-but-missing marker fails. Orchestrator-owned claims from `TASKS.md` are bound through `docs/remediation/GATE-CLAIMS.md`, which records source headings and anchored text without changing task tracking. Marker completeness still requires RM-54 review because arbitrary English claims cannot be inferred safely.
Each criterion declares exact `caseRefs`; the verifier compares those semantic declarations bidirectionally with case-side `criterionIds` and requires at least one must-fail case. Moving a criterion ID to an unrelated case therefore fails as both a missing declared exercising case and an undeclared binding. Registered meta-negative controls misbind a criterion, remove meaning provenance, and misbind a prose claim, and each must make structure verification red for its stated reason.
Designated governing prose uses `GATE-CLAIM:<id>` markers. Each claim also names the exact must-fail `caseRef` that exercises its criterion; unknown, positive-only, unrelated, unbound, or registered-but-missing claims fail. Orchestrator-owned claims from `TASKS.md` are bound through `docs/remediation/GATE-CLAIMS.md`, which records source headings and anchored text without changing task tracking. Marker completeness still requires RM-54 review because arbitrary English claims cannot be inferred safely.
Compatibility checks detect direct contradictions in declared finite constructions. The verifier combines referenced case fixtures and environments in one isolated tree, rejects conflicting fixture/environment values, executes the construction's exact invocation, and checks its exact outcome. They do not prove semantic consistency of arbitrary natural language.
@@ -36,7 +38,7 @@ A gate with an external installed counterpart declares it explicitly. When the i
**DOES NOT:** Repository-controlled PR CI does not execute a commit's own verifier in an isolated replay. Doing so safely would require granting namespace capability before PR-controlled configuration or code runs; that same PR could consume the capability directly. This is an absent trust boundary, not unfinished hardening. RM-60 owns a runner-level rootless sandbox or protected immutable launcher; RM-59 owns the parallel artifact-integrity anchor.
The replay implementation and abuse-case tests remain fail-closed: when invoked by a future protected authority, inability to establish Bubblewrap is terminal nonzero; controls are never omitted or treated as replay success. On an unprivileged CI runner, sandbox integration tests pass only by asserting that this refusal is nonzero, while capable local/protected environments exercise the full abuse cases. Historical installs use frozen lockfiles, isolated network/PID/IPC/UTS and environment/home boundaries, and authoritative-file snapshots that detect lifecycle rewrites.
The replay implementation and abuse-case tests remain fail-closed: when invoked by a future protected authority, inability to establish Bubblewrap is terminal nonzero; controls are never omitted or treated as replay success. On an unprivileged CI runner, sandbox integration tests pass only when the result carries parent-generated Bubblewrap-launch provenance and proves the sandbox entry command never ran. Child-controlled text that merely reproduces a Bubblewrap denial is not accepted. Capable local/protected environments exercise the full abuse cases. Historical installs use frozen lockfiles, isolated network/PID/IPC/UTS and environment/home boundaries, and authoritative-file snapshots that detect lifecycle rewrites.
Retained provider evidence can assert terminal-success **current-tree** records for prior commits when supplied through `GATE_PROVIDER_EVIDENCE_FILE`. Each normalized record contains `commit`, unique integer pipeline `number`, pipeline `status`, and exactly one `gate-verify` step; the highest-numbered rerun is authoritative. Ambiguous duplicates fail. Absent, expired, or currently-running evidence is reported explicitly and never inferred as success.
+4 -3
View File
@@ -30,7 +30,7 @@ Existing deterministic gates can return success without enforcing their stated p
1. `RM02-REQ-01`: The JSON registry SHALL give every gate and criterion a stable ID and SHALL declare exact invocation, input classes, cases, exact observed and required exit codes, reason diagnostics, and criterion bindings.
2. `RM02-REQ-02`: Every gate SHALL have at least one observed-red must-fail case. The verifier SHALL reject missing, stale, ambiguous, or ineffective declared inert mutations and SHALL name an externally inerted gate.
3. `RM02-REQ-03`: Every acceptance criterion SHALL bind to a case that can fail for that criterion's stated reason. Security/integrity prose claims in the designated governing documents SHALL carry bound `GATE-CLAIM:<id>` markers.
3. `RM02-REQ-03`: Every acceptance criterion SHALL declare exact criterion-side `caseRefs` that match case-side `criterionIds` bidirectionally and include a case that can fail for that criterion's stated reason. Moving a binding to an unrelated case SHALL fail verification. Security/integrity prose claims in the designated governing documents SHALL carry bound `GATE-CLAIM:<id>` markers and declare the exact must-fail case exercising the claim criterion.
4. `RM02-REQ-04`: Declared finite compatibility scenarios SHALL execute together and direct modeled contradictions SHALL fail. This does not claim semantic consistency of arbitrary English.
5. `RM02-REQ-05`: Restated criteria SHALL retain original text, current text, reason, finding/task, and dated meaning-change history.
6. `RM02-REQ-06`: An observed behavior differing from required behavior SHALL be reported as `DEFECT` with a tracked owner; an ownerless delta SHALL fail verification. Such a gate SHALL never be described as passing, green, or OK.
@@ -51,13 +51,14 @@ Existing deterministic gates can return success without enforcing their stated p
2. `RM02-AC-02`: Externally mutate any registered gate at its declared inerting point so its failure path succeeds; verification returns nonzero and names that gate. The verifier's internal meta-control is observed red before its healthy result is trusted.
3. `RM02-AC-03`: An executable added under a declared gate root without an entry returns nonzero and includes `unregistered gate`.
4. `RM02-AC-04`: A gate with zero must-fail cases returns nonzero and includes `no negative control`.
5. `RM02-AC-05`: Unbound criteria, unbound governing prose markers, ownerless behavior deltas, stale mutations, source/deployed drift, and modeled compatibility conflicts each return nonzero with the responsible stable ID.
5. `RM02-AC-05`: Unbound or semantically misbound criteria, prose claims bound to unrelated cases, unbound governing prose markers, ownerless behavior deltas, stale mutations, source/deployed drift, and modeled compatibility conflicts each return nonzero with the responsible stable ID. Registered meta-negative controls move a criterion binding, remove meaning provenance, and redirect a prose claim to an unrelated case; each is observed red for its stated reason.
6. `RM02-AC-06`: CI configuration invokes the verifier unconditionally on every pull request.
7. `RM02-AC-07`: PR output states adjacent `DOES`/`DOES NOT` boundaries: current-tree gates and inerting mutations execute unprivileged and fail-closed; isolated own-tree replay does not execute in repository-controlled PR CI. RM-60/RM-59 are named, retained provider evidence is never inferred, and future protected post-merge detection specifies quarantine/revert rather than claiming pre-merge prevention.
### Risks, dependencies, and verification boundary
- The repository verifier proves declared controls, modeled scenarios, source/deployed equality at execution time, and unprivileged current-tree behavior. It does **not** execute isolated per-commit replay or defend against an actor able to rewrite the gate, registry, verifier, and sandbox entry consistently.
- The repository verifier proves declared controls, modeled scenarios, bidirectional declared criterion/case relationships, source/deployed equality at execution time, and unprivileged current-tree behavior. It does **not** infer arbitrary-English semantics, execute isolated per-commit replay, or defend against an actor able to rewrite the gate, registry, verifier, and sandbox entry consistently.
- Sandbox refusal tests require parent-generated Bubblewrap-launch provenance and proof that the sandbox entry command never ran; child-controlled denial-looking text alone cannot establish unavailability.
- Repo-only code cannot both grant namespace capability to PR configuration and prevent that same PR from using the capability directly. RM-60 owns a runner/provider-controlled pre-execution boundary; RM-59 owns the parallel artifact-integrity anchor.
- Protected post-merge replay, once RM-60 exists, is detection only. Failure requires immediate quarantine of the affected result and revert of the offending merge; it is not equivalent to a pre-merge gate.
- External branch protection and provider CI history supply merge-time current-tree evidence where retained. RM-25 tracks provider-side enforcement.
+3 -2
View File
@@ -39,7 +39,7 @@ Deliver the seven-gate registry and RED-first anti-inert verifier on `feat/rm-02
- CI wiring RED: package script and unconditional Woodpecker step tests both failed before wiring.
- History RED: history test failed with missing module before own-tree manifest selection/provider classification was implemented.
- `pnpm gate:verify`: exit 0; seven gates each reported `META-NEGATIVE-CONTROL ... observed red`; queue source/deployed drift control observed red; six queue behavior deltas printed as `DEFECT (owner: RM-03)`.
- Focused Node tests: 35/35 pass after review hardening (24 verifier/wiring plus 11 history/provider tests).
- Focused Node tests: 37/37 pass after review hardening (26 verifier/wiring plus 11 history/provider tests).
- `pnpm typecheck`: pass (45/45 Turbo tasks).
- `pnpm lint`: pass (25/25 Turbo tasks).
- `pnpm format:check`: pass.
@@ -61,7 +61,8 @@ The queue guard's `get_state_from_status_json` runs `python3 - <<'PY'` while pro
- Initial PR pipeline #2177 exposed Woodpecker's shallow boundary: the activation parent object was present but marked shallow, so `merge-base --is-ancestor` correctly refused to infer ancestry. The unconditional gate step now unshallows before ancestry/provenance checks; its wiring test was observed RED before the CI fix.
- Pipeline #2178 then proved the unprivileged Docker runner cannot establish Bubblewrap namespaces. A privileged experiment remained uncommitted and was rejected after Codex correctly rated it CRITICAL: PR-controlled code executes before an in-repository sandbox and could directly use the granted capability.
- `mos-remediation` and `rev-974` independently ruled Option C. RM02-REQ-10 now retains its original text, restatement, and reason: PR CI verifies only the current tree, unprivileged and fail-closed; isolated own-tree replay is deferred to RM-60/#1031's external pre-execution authority, cross-referenced with RM-59. Future protected post-merge replay is detection with quarantine/revert, never pre-merge prevention.
- RED-first boundary test proved the old path executed an inert intermediate verifier. The revised path states adjacent `DOES`/`DOES NOT` claims, validates historical manifest provenance without executing it, and infers no replay success. Direct sandbox tests remain hard-fail; unprivileged CI asserts terminal refusal instead of treating replay as success. Pipelines #2179/#2180/#2181 exposed two runner refusal forms: namespace denial as `spawnSync bwrap` with `error.code=EPERM`, and a test image without Bubblewrap as `error.code=ENOENT`. The replay diagnostic now preserves spawn errors; the refusal detector recognizes only exact `spawnSync bwrap` provenance for `EPERM`/`EACCES`/`ENOENT`, plus Bubblewrap's known namespace-refusal text. Focused negative assertions reject both unrelated `spawnSync git EPERM` and verifier output that merely says `bwrap ENOENT`.
- RED-first boundary test proved the old path executed an inert intermediate verifier. The revised path states adjacent `DOES`/`DOES NOT` claims, validates historical manifest provenance without executing it, and infers no replay success. Direct sandbox tests remain hard-fail; unprivileged CI asserts terminal refusal instead of treating replay as success. Pipelines #2179/#2180/#2181 exposed two runner refusal forms: namespace denial as `spawnSync bwrap` with `error.code=EPERM`, and a test image without Bubblewrap as `error.code=ENOENT`. The replay diagnostic now preserves spawn errors. Parent-generated launcher/entry metadata distinguishes refusal before sandbox entry from child-controlled output; the detector recognizes exact `spawnSync bwrap` provenance for `EPERM`/`EACCES`/`ENOENT` and known namespace-refusal text only when the entry command provably did not run. Focused negative assertions reject unrelated `spawnSync git EPERM`, verifier output that merely says `bwrap ENOENT`, and exact namespace-denial impersonation without provenance or after sandbox entry.
- Exact-head independent review at `9b4d4beb` found two valid blockers. RED-first controls reproduced both: denial-looking child stderr was accepted as sandbox unavailability, and moving meaning/prose criterion IDs to an unrelated type-error case left `gate:verify` green. Bubblewrap execution now emits a parent-generated random entry marker and returns parent-owned launcher/entry metadata; unavailability requires Bubblewrap launcher provenance plus proof entry never ran, so exact denial impersonation from plain or entered-child results is rejected. Criterion objects now declare exact `caseRefs`, checked bidirectionally against case-side `criterionIds`; prose claims declare an exact must-fail `caseRef`. Registered must-fail cases move a criterion binding, remove meaning provenance, and redirect a prose claim, each producing its stable reason. The review freeze was deliberately lifted before remediation.
- Option C security review reported no findings. Code review rejected an initial unrelated typecheck binding for the new security criterion. It was replaced with a dedicated registered `privileged-pr-gate` case: the fixture injects a privilege key into the gate step, the wiring control rejects it for that exact reason, and `gate:verify` observes the boundary negative control. Follow-up hardening uses a closed exact gate-step construction, rejects privilege across the entire pipeline, rejects non-canonical/merged YAML keys, and pins the unrestricted PR/main trigger block; quoted/escaped/alias/merge/duplicate/filter bypass tests pass. Final Codex code review approved with no findings.
## Documentation checklist