diff --git a/.agents/skills/doctrine/msdmd-checks.md b/.agents/skills/doctrine/msdmd-checks.md new file mode 100644 index 0000000..9faffb1 --- /dev/null +++ b/.agents/skills/doctrine/msdmd-checks.md @@ -0,0 +1,150 @@ +# msdmd doctrine: CONTRACTS / CHECKS / audit + +Status: ratified for skill-lib. Reference implementation: +`skill_lib/safety/repo_loto.py` + `tests/test_repo_loto.py`. + +## The triad + +``` +CONTRACTS are obligations. +CHECKS are accountable witnesses. +audit reconciles the witness list against the obligation list. +``` + +Source modules own promises. Test modules own evidence. Neither owns +the other's declarations. + +## Ownership + +**CONTRACTS live in the source module.** A contract is a normative +claim: what must remain true of this module's behavior. It belongs to +the module doing the promising, never to the file checking it. + +**CHECKS live in the test module.** A check is an evidentiary +procedure: an executable claim to prove a named contract. Test +topology is the test module's business; source modules do not carry +`call:` fields. There is no legacy bridge in skill-lib — new code +adopts this split directly. + +## Grammar + +Blocks are comment-fenced, one entry per `id:`, fields indented +beneath it: + +```python +# === CONTRACTS === +# id: loto_scope_enforced +# given: files touched outside the declared --files globs +# then: close refuses with the violating paths named +# class: safety +# === END CONTRACTS === +``` + +```python +# === CHECKS === +# id: check_scope_enforced +# proves: loto_scope_enforced +# call: self::test_scope_enforced +# requires: git, python3, posix_shell +# timeout: 20 +# mutates: filesystem +# cleanup: tempdir_teardown +# === END CHECKS === +``` + +CONTRACTS fields: `id`, `given`, `then`, `class` +(doctrine | evidence | safety | security). + +CHECKS fields — every one has a consumer, whether the runner or the +operator: `id`, `proves`, `call`, `requires` (runner refuses to execute +on hosts missing them), `timeout` (runner sets the active subprocess +bound per check) — these four are **runner-consumed** — plus `mutates` +and `cleanup`, which are **operator-consumed**: the danger documentation +a human reads to decide when a check may run. Operator-consumed is +consumed; it is not decoration. + +## The field-entry rule + +A field enters the schema in the same change that gives it a consumer — +a runner mode that reads it, or a documented operator decision it feeds +— not before. Metadata read by *neither* runner nor operator is F6 — +decorative preservation — and is treated as a defect, not diligence. +(`mutates`/`cleanup` clear this bar as operator-consumed. `determinism` +and `level` do not yet: nothing reads them, so they stay out until a +runner mode does. Note that `determinism` is self-reported until a +runner measures it by repeated execution.) + +## call: resolution + +The only sanctioned form is `self::fn` — a function defined in the +file that declares the check. Dotted import paths are refused by the +audit: Python imports execute module top level, and **an audit that +executes is not an audit**. A no-exec audit therefore resolves `self::fn` +against the file's **parsed** `def`/`async def` names (read the source, +walk the AST) — never by importing the module or inspecting loaded +callables. (The reference `tests/test_repo_loto.py` reads `globals()` +only because its audit runs *as* that module, so the definitions are +already in scope; a central audit walking many files must parse.) The +`self::` form is also rename-immune; copies and uploads reconcile +identically. + +## audit + +The cheapest runner mode and the first one built: no execution, pure +reconciliation of the declared graph. It must report, at minimum: + +``` +GAP has no CHECKS entry claiming to prove it +GAP claims unknown contract: +GAP call does not resolve: +GAP executable check has no resolving CHECKS declaration +``` + +Exit nonzero on any gap. A reconciler that has only ever said +"closed" is itself unverified: every audit implementation must be +negative-tested by planting an orphan contract, a phantom `proves` +target, and an unresolvable call, and observing the GAP. + +## Semantics of "proves" + +`proves:` means *claims to prove*. The audit verifies linkage and +resolution, not that the check exercises the contract. The rung above +— break the module, confirm the witness notices (mutation-level +verification) — is named here so its absence stays visible. A module +is `[test-backed]` when its suite passes and its graph closes; it is +not thereby mutation-verified. + +## Evidence discipline + +- **Latest run wins, per identical command.** A rerun supersedes its + predecessor as standing evidence; history persists in working + memory until distillation. Superseding is by exact command string — + a passing narrow rerun does not launder a failing broad one. +- **Skipped or flaky checks are non-proof** unless explicitly waived, + and waivers ride the record; they do not erase it. +- **Execution semantics are evidence.** Records carry `shell:`, + exit codes, and timestamps, not just command strings. +- **Harness errors are results.** The runner reports TimeoutExpired, + CalledProcessError, and resolver failures as `ERROR` per check and + continues; an aborted run is not evidence about the unrun checks. +- **Subprocesses are bounded and owned.** Every spawned process runs + in its own session with a metadata-driven timeout; on expiry the + whole process group is killed. A hung witness is dismissed, on the + record, not waited on. + +## Status vocabulary + +``` +[implemented-prototype] runs; verified by session contact only +[test-backed] suite passes and audit closes the graph +[mutation-verified] checks demonstrated to notice planted breakage +``` + +Each term is earned, never assumed, and never claimed one rung above +its evidence. + +hmmm: the block-type for harness/infrastructure tests that prove no +contract remains unnamed; mutation-level verification is defined but +unbuilt; the audit grammar is currently specified by its reference +parser rather than by this document, and if a second parser disagrees, +one of them yields here, in writing.