A rule carries its check, and a key that signs only check results records whether it held

[felipesauer]

What

A decision in force can now carry the program that checks it, and a machine with a key of its own can record, at a commit, whether the rule held.

• mnema check declare <rule> <program> [args...] records the program that checks a rule. It is started without a shell, so nothing in the program or its arguments is split, globbed or expanded; a credential in either refuses the declaration.
• mnema check run runs the check of every rule in force from the project root, with a timeout (300 s by default), and records one check.passed or check.failed per rule, naming the rule and the commit. What a program printed is kept as its last 4000 characters, with control bytes made visible and credentials redacted. It exits non-zero when any check failed, and refuses a tree that has changes outside the record or is not at a commit.
• The results are signed by a key of the runner's own. A member of an identity enrolls it (mnema key request --checker, mnema key enroll --checker); a key that is already a member is refused. A checker key signs check results and nothing else: verify refuses a check result from any other key, and refuses any other kind signed by a checker key, in both readers (TypeScript and the Python second reader, with the same vectors and an agreement test).
• mnema accountability lists the checker as a machine.
• Four new event kinds: check.declared, checker.enrolled, check.passed, check.failed. Existing kinds and the canonical form are untouched.
• The README has a page for it, and says what it does not promise.

Wiring to the Action (not done here): packages/action reads the record and runs verify; it does not run check run. Connecting them is a later step: a job that has the runner's key as a secret, runs mnema check run --key, and commits or uploads the results. Until then the step is one of the team's own workflow.

Proof

• Both refusals are tested in the two readers. Removing the "checker key signs another kind" refusal, and then the "check result needs a checker" refusal, from the TypeScript reader each fails its own agreement test.
• Base against head, in a sandbox HOME with a clean environment: the head wrote a record with a declared check, an enrolled checker and a check.passed; the binary of main-v1 reads it as UNREADABLE ... unknown event kind "check.declared" and verify reports the tail as unreadable. A check.passed forged under a person's key makes the head's verify fail with check.passed is signed by <key>, which is not enrolled as a checker at this point. accountability printed the runner as machine (signs check results only).
• Guards that count kinds, operations, verbs and sites were extended by their own mechanisms, and every kind has a driver in the field, advance and stale-anchor sweeps.

Known limits

• A binary from before this change stops reading the whole record once a check kind is in the committed tree, as it does for any kind it does not know (FORMAT.md section 4.1).
• A result says that a key the team enrolled reported the rule held at that commit. It does not prove the program ran as declared on that machine, nor that it checks what its rule says.
• A declared program runs on the runner: whoever can commit a declaration can make the runner start that program. There is no sandbox; the timeout and the output bound are the only limits.
• A program started by check run runs as the runner and can read the checker's key and the environment the runner has. The role narrows what such a key can sign, and only that: a key taken this way can say that any rule's check passed at any commit, and no fact withdraws the role yet, so a leaked checker key keeps signing passes the verifier accepts. Keep the key in a secret scoped to the job that runs check run, and treat a leak as a reason to stop trusting every result that key signed. The program does not inherit the MNEMA_* variables, which narrows what it is handed, not what it can read from disk.
• The results are written to the working tree; committing or uploading them is the caller's step.

[felipesauer]

Superseded by 691: the same tree, with two commits re-authored under the project's commit address.