§18. Instructions to the coding agent (AGENTS.md)

planarian @ a924e09 · Spec v4.6 · snapshot main · all versions

0. First deliverable, before any other code: the Phase A fault catalog (crates/gym/catalog/phase-a/: 00-format.toml and one <family>.toml per §15 family, read in filename order as one document), one entry per §15 family at minimum, each with inject, required_post, intent, family; stop for owner review.
1. Second deliverable: the GA demonstration script (gym/demo.sh): fault → repair; bad config → revert; kill planariad during Activating; watchdog reverts; restart daemon; reconciliation record printed. Build toward making it pass; everything else is in service of it.
2. Implement Phase A only; traits for B–E with one implementation.
3. Build order (historical; every crate exists at v4.6): schema → txn (with the journal and the fake backends) → policy → state + backends/linux (systemd, logind, sysfs) → exec + backends/linux (nixos-rebuild) → watchdog → changes → incident → diagnose → gym → intent → cli → daemon → console. The console Graph view may be built as soon as state works.
4. Preserve however the schema evolves: I5, I6, I10–I25; digest() excludes resources and timestamps; Proposal is the only write path; policy facts derived by the executor; gym scores on required_post and intent cases, never on absence of errors; diagnoser before any model; probes with side effects other than None or a bounded Measurement never on a cadence.
5. Do not resolve §19 items; TODO(owner) with the stated default.
6. No language model, LLM API, or prompt anywhere in Phase A.
7. Where NixOS and this spec disagree on mechanism, follow NixOS and record in docs/deviations.md.
8. Every executor outcome must be reproducible from the log: proposal, pre/post state, DerivedFacts, PolicyVersion, probe evidence, decision, outcome.
9. schema, policy, txn in the Verus subset; land policy proofs before starting exec.
10. The Asterinas and Firecracker gym targets may stay red in A. Classify failures; fix only Core.
11. Every new assume/external_body adds a line to docs/assumptions.md in the same PR.
12. The fake backend used by the transaction kernel MUST satisfy every entry in docs/assumptions.md, not only the trait signatures: it is a second real implementation, not a mock. The gym runs the kernel against it under injected Partial, Unknown, and fenced outcomes.
13. The journal is hash-chained from the first commit that writes it (I18).
14. Never implement Planarian’s response to its own failure inside planariad; it lives in nix/posture.nix as systemd and initrd units (§12d).
15. Report the invisibility budget (§21) and the verification ratio (§17a) from the first gym run; treat any degradation as a failing test.
16. docs/future-work.md is non-normative. Cite it; do not implement from it. If anything there seems to block Phase A, stop and ask.
17. Phase A was held open for v4.4: the schema-affecting changes (Override, the Actor shape, the security floor, the hash-chained journal) land before the Phase A proofs are written, not as migrations after them.
18. Keep docs/bypasses.md current (§17b): a PR that adds a path to the machine adds a row or says it opens none.
19. v4.6 handoff, in this order. (a) Reconcile: the close-out review in the project (“Phase A close-out review, head 805cd1c”) lists every finding with its status at that head; before touching anything, confirm each item you take on is still open at your head and record which commit closed the ones that aren’t. (b) B-20 first (I24; §11, §16): register the row, fix, add agent-name-collision to both harnesses. (c) The documentation sweep: every doc agrees with head and with this spec before any further status is cited (ga-status.md’s summary; guarantees.md’s accounting; bypasses.md’s three tables; AGENTS.md mirroring §18 rules 0–23; catalog-review.md’s counts and a v4.6 section; the catalog’s header (phase-a/00-format.toml); the deviations rows §28 names). (d) The §28 required changes, one PR each, each with its §15 acceptance case landing in the same PR. (e) §15’s harness contract and §17a’s accounting checks. (f) Then, and only then, run the whole VM catalog on one commit and update ga-status.md from that run; a gate claim cites one commit and one run, never a union of runs.
20. Equivalent effects, equivalent treatment. When two spellings of a request, two paths to a commit, or two sources of a proposal produce the same effect on the machine, they get the same derived facts, the same floors, and the same bookkeeping (§11, I25). A PR that adds a spelling, a path or a source states which existing one it is equivalent to and shows the gym case that holds them equal.
21. Nothing is derived from a failed tool. A backend or helper that exits nonzero, times out, or returns truncated output never contributes a smaller plan, a None disruption, or a passing verdict; the step fails or the change parks (§9 step 3, §15 harness contract).
22. The guarantees site (§17c) builds on every push. A change that renames an obligation, adds an invariant or assumption, or adds a bypass row makes the site resolve in the same PR.
23. Property tests for logic, regression tests for bugs (owner decision, Nov 3). A PR that changes a pure fold, parser, classifier, ordering or state machine carries a property test (proptest, or a Kani harness where one fits) stating the invariant it changes, not only an example input, and shows that the test fails without the change. A PR that fixes a bug adds a test that fails on the unfixed code and a row to docs/regression-ledger.md (bug, fix, test, kind, evidence it fails on revert); a bug that only a kernel or a VM can show cites its VM test there. Nix wiring, documentation and fixtures need none and say so.