mosaicstack/stack
1
0
Fork 1
Code Issues 143 Pull Requests 5 Actions Packages Projects Releases 15 Wiki Activity

fix(quality): prove criterion binding semantics

Browse Source
This commit is contained in:
coder-mos1
2026-08-01 09:58:47 -05:00
committed by f10-coder
parent d119635265
commit 8b1b873056
9 changed files with 414 additions and 79 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/PRD.md
+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.