notes: the developer protocol, and its strictness ruled

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017RzZgrf7V7Zk2iczBXDRbm

.claude/memory/rules.md

@@ -106,3 +106,14 @@ v3 is not part of acceptance. There is no `make test`. Hosted `make` is compile
 - Toolchain for acceptance: `make ARCH=amd64,aarch64,riscv64 init INIT_DOCS=0 INIT_PROOFS=0` (the repo's own).
 - Clean tree: since 90c5c140 a build changes no tracked file (version.h untracked; BLOCK_MAP.md has no
   timestamp). A *signed* build still rewrites BLOCK_MAP.md's Signed column -- open, Bob's call.
+
+## The developer protocol (#135, built 2026-11-12)
+- `scripts/nightly.sh protocol <stage>` one stage per foreground command (accept-amd64 begins it), then
+  `protocol-report` -> logs/<TS>/PROTOCOL.md; commit logs/ + experiments/bare_metal/runs/; the PR's gate runs
+  `scripts/check_protocol.sh` on the head first.
+- **Strict, ruled** (Bob 2026-11-12: "Keep it strict"): ANY change outside logs/ and the DoE CSVs after the run --
+  documents and notes included -- makes the evidence stale and needs a full protocol rerun. So batch docs/notes
+  commits and push them with the next protocol, not one by one. Hold commits that would stale an open PR.
+- The docs stage takes ~30 min here (the API reference); it outlasts the foreground limit and the tool
+  moves it to the background (not an acceptance boot; no QEMU). Proofs need the HOL-Library heap
+  (ci/runner-image's URL, checksum in its Dockerfile).