ci: the developer protocol -- nightly.sh protocol, PROTOCOL.md, and the gate checks it (#135)

scripts/nightly.sh protocol: every stage a PR, the nightly and a release run --
accept amd64, aarch64, riscv64, stick-high, test-32, proofs, images, docs --
in order, never publish; the first failure ends it. protocol <stage>... runs
those only, so each can be its own foreground command (the QEMU rule);
accept-amd64 begins a protocol, recording the commit and whether the tree is
clean. protocol-report writes logs/<TS>/PROTOCOL.md (the commit, the tree,
each stage's result and output, POST and dict_hash per architecture compared,
test-32's totals, the proofs' log, the images' and documents' SHA-256) and
keeps every stage's output in logs/<TS>/protocol/ -- nothing is left only in
build/nightly. PASS only if every stage passed on the commit it began on and
the tree is unchanged but for the evidence.

acceptance.yml: scripts/check_protocol.sh on the PR's head, first, before the
boots. The PR template asks for PROTOCOL.md; .claude/CLAUDE.md names the
protocol as the acceptance a developer runs.

Captain Bob, 2026-11-07 (#135); 2026-11-12: "Keep working on alpha.5".

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

.claude/CLAUDE.md

@@ -300,6 +300,25 @@ make -f kernel/Makefile ARCH=amd64   clean qemu-stick-high
 make -C v4 test-32
 ```
 
+**The developer protocol (#135, 2026-11-12) is the acceptance a developer runs, and its evidence
+goes in the PR** (Captain Bob, 2026-11-07: "We can simply run nightly as developers ... Just no
+Nexus push ... Then the protocol evidence can be submitted in the PR."):
+
+```bash
+scripts/nightly.sh protocol        # every stage above, then the proofs, the images, the documents; never publish
+```
+
+It writes `logs/<TS>/PROTOCOL.md` (the commit, its tree clean or not, each stage's result, POST and
+`dict_hash` per architecture, test-32, the proofs, the images' and documents' SHA-256) and each
+stage's output in `logs/<TS>/protocol/`. Commit `logs/` and `experiments/bare_metal/runs/`; the
+PR's Acceptance check (`scripts/check_protocol.sh`) refuses a head without a passing PROTOCOL.md
+for its tree -- any change outside the evidence after the run is stale, and the protocol is run
+again. **One stage per foreground command is also a protocol**, and is how an agent runs it (the
+QEMU rule: never in the background): `scripts/nightly.sh protocol accept-amd64`, then
+`accept-aarch64`, `accept-riscv64`, `accept-stick-high`, `test-32`, `proofs`, `images`, `docs`,
+each its own command, then `scripts/nightly.sh protocol-report`. The tools: `make
+ARCH=amd64,aarch64,riscv64 init`, plus the HOL-Library heap the CI image has (`ci/runner-image`).
+
 **v4 is the default build (Captain Bob, 2026-10-14: "v4 is the default build ... no, qemu to v4
 too ... we are effectively trying to retire v3").** Every kernel build carries v4 and v3 and
 boots v4; `system=v3` in the boot arguments (`KERNEL_ARGS` for QEMU, `starforth.cfg` /

.gitea/pull_request_template.md

@@ -10,7 +10,10 @@ The **Acceptance** check runs on this pull request by itself -- amd64, aarch64,
 stick loaded high, test-32 -- and `master` takes nothing that has not passed it. Note here
 anything it does not cover:
 
-- [ ] Logs from runs made by hand are committed in `logs/`, if any
+- [ ] `logs/<TS>/PROTOCOL.md` for the head commit: `scripts/nightly.sh protocol`, run by hand,
+      its `logs/` and `experiments/bare_metal/runs/` committed (#135). The check refuses a head
+      without one, or with one for another tree.
+- [ ] Logs from other runs made by hand are committed in `logs/`, if any
 - [ ] Hardware this was tried on, if any:
 
 ## The record

.gitea/workflows/acceptance.yml

@@ -38,6 +38,12 @@ jobs:
           fetch-depth: 0          # the SBOM's version is git describe
           lfs: false              # only the logs and DoE CSVs are in LFS; the build needs neither
 
+      # The developer protocol's evidence first (#135): the PR's head carries a passing
+      # logs/<TS>/PROTOCOL.md for its own tree (scripts/nightly.sh protocol, run by hand), or it is
+      # refused here, before the boots. The head, not the merge commit the checkout made.
+      - name: The developer protocol's evidence
+        run: scripts/check_protocol.sh "${{ github.event.pull_request.head.sha || 'HEAD' }}"
+
       - name: The capsule-signing key
         env:
           KEY: ${{ secrets.CAPSULE_SIGN_KEY }}

scripts/nightly.sh

@@ -46,6 +46,22 @@
 #       dictionary (The Dictionary of v4, #157 -- it fails the stage if a live word has no entry),
 #       vol1, vol2, vol3, api (pdf).
 #
+# The developer protocol (#135; Captain Bob, 2026-11-07: "We can simply run nightly as developers
+# to further make sure nothing sneaks in. Just no Nexus push."):
+#
+#   scripts/nightly.sh protocol
+#       Every stage, in order -- accept amd64, aarch64, riscv64, stick-high, test-32, proofs,
+#       images, docs -- never publish; the first that fails ends it. Then protocol-report.
+#   scripts/nightly.sh protocol <stage>...
+#       Those stages only (accept-amd64 begins a protocol), each recorded; one per call runs each
+#       in a foreground command of its own. Then protocol-report, by hand.
+#   scripts/nightly.sh protocol-report
+#       logs/<TS>/PROTOCOL.md: the commit and whether its tree was clean; each stage's result and
+#       logs; POST and dict_hash per architecture, compared; test-32's totals; the proofs'; the
+#       images' and documents' SHA-256 -- and each stage's own output, in logs/<TS>/protocol/. The
+#       developer commits logs/ and experiments/bare_metal/runs/; the PR's Acceptance check
+#       (scripts/check_protocol.sh) refuses a head without a passing PROTOCOL.md for its tree.
+#
 # VERSION is <LITHOS_VERSION>-SNAPSHOT, or NIGHTLY_VERSION when set (a release sets it from its
 # tag). NEXUS_USER (default ci-publisher) and NEXUS_PASSWORD; publishing needs mvn and a JRE.
 # Needs what make ARCH=amd64,aarch64,riscv64 init installs (INIT_DOCS=0 for the images,
@@ -60,8 +76,15 @@ VERSION=${NIGHTLY_VERSION:-$LITHOS-SNAPSHOT}
 usage() {
     echo "Usage: scripts/nightly.sh accept <amd64|aarch64|riscv64|stick-high> | test-32 | proofs | images" >&2
     echo "                          | publish <URL> | docs | publish-docs <URL> | gitea-release <tag>" >&2
+    echo "                          | protocol [<stage>...] | protocol-report" >&2
+    echo "  protocol stages: $PROTOCOL_STAGES" >&2
     exit 2
 }
+PROTO=build/protocol
+PROTOCOL_STAGES="accept-amd64 accept-aarch64 accept-riscv64 accept-stick-high test-32 proofs images docs"
+# The tree, but for the evidence the run writes (logs/, the DoE CSVs) and what builds leave behind
+# untracked: what scripts/check_protocol.sh compares.
+tree_dirt() { git status --porcelain -- . ':(exclude)logs' ':(exclude)experiments/bare_metal/runs'; }
 need() { for f in "$@"; do [ -f "$f" ] || { echo "nightly: no $f -- run the stages before this one" >&2; exit 1; }; done; }
 
 # deploy <URL> <artifactId> <main file> <main ext> <main classifier> [file ext classifier]...
@@ -239,5 +262,124 @@ publish-docs)
         "$DOCS/vol1.pdf" pdf vol1 "$DOCS/vol2.pdf" pdf vol2 "$DOCS/vol3.pdf" pdf vol3 \
         "$DOCS/api.pdf" pdf api
     ;;
+protocol)
+    # The developer protocol (#135): the stages a PR, the nightly and a release run, never publish.
+    shift
+    all=0; [ $# -gt 0 ] || { set -- $PROTOCOL_STAGES; all=1; }
+    for s in "$@"; do case " $PROTOCOL_STAGES " in *" $s "*) ;; *) usage ;; esac; done
+    self="$(pwd)/scripts/nightly.sh"
+    for s in "$@"; do
+        if [ "$s" = accept-amd64 ]; then                 # a protocol begins: the commit, and its tree
+            rm -rf "$PROTO"; mkdir -p "$PROTO"
+            git rev-parse HEAD > "$PROTO/commit"
+            date -u +%Y%m%d-%H%M%S > "$PROTO/ts"
+            if [ -z "$(git status --porcelain)" ]; then echo clean > "$PROTO/tree"; else echo dirty > "$PROTO/tree"; fi
+            echo "=== nightly: protocol for $(git rev-parse --short HEAD), tree $(cat "$PROTO/tree")"
+        fi
+        need "$PROTO/commit"
+        [ "$(git rev-parse HEAD)" = "$(cat "$PROTO/commit")" ] \
+            || { echo "nightly: HEAD is not the commit this protocol began on -- begin again with accept-amd64" >&2; exit 1; }
+        echo "=== nightly: protocol stage $s"
+        set +e
+        case $s in
+            accept-*) "$self" accept "${s#accept-}" ;;
+            *)        "$self" "$s" ;;
+        esac 2>&1 | tee "$PROTO/$s.txt"
+        rc=${PIPESTATUS[0]}
+        set -e
+        echo "$rc" > "$PROTO/$s.rc"
+        if [ "$rc" != 0 ]; then
+            echo "nightly: protocol stage $s failed (exit $rc)" >&2
+            [ $all = 0 ] || "$self" protocol-report || true
+            exit "$rc"
+        fi
+    done
+    [ $all = 0 ] || "$self" protocol-report
+    ;;
+protocol-report)
+    # logs/<TS>/PROTOCOL.md: what scripts/check_protocol.sh reads (- Commit:, - Tree:, - Result:)
+    # and what a reviewer reads. PASS only when every stage of this protocol passed, on the commit
+    # it began on, and the tree is still that commit's but for the evidence.
+    need "$PROTO/commit" "$PROTO/ts" "$PROTO/tree"
+    commit=$(cat "$PROTO/commit"); ts=$(cat "$PROTO/ts"); tree=$(cat "$PROTO/tree")
+    dir=logs/$ts; mkdir -p "$dir/protocol"
+    result=PASS; why=()
+    [ "$tree" = clean ] || { result=FAIL; why+=("the tree was not clean when the protocol began"); }
+    [ "$(git rev-parse HEAD)" = "$commit" ] || { result=FAIL; why+=("HEAD moved during the protocol"); }
+    [ -z "$(tree_dirt)" ] || { result=FAIL; why+=("the stages left the tree changed: $(tree_dirt | head -3 | tr '\n' ' ')"); }
+    rows=()
+    for s in $PROTOCOL_STAGES; do
+        if [ -f "$PROTO/$s.rc" ]; then
+            rc=$(cat "$PROTO/$s.rc"); cp "$PROTO/$s.txt" "$dir/protocol/$s.log"
+            if [ "$rc" = 0 ]; then st=PASS; else st="FAIL (exit $rc)"; result=FAIL; why+=("$s failed"); fi
+        else
+            st="not run"; result=FAIL; why+=("$s was not run")
+        fi
+        rows+=("| \`$s\` | $st | \`$dir/protocol/$s.log\` |")
+    done
+    boots=()
+    for a in amd64 aarch64 riscv64 stick-high; do
+        log=$(sed -n 's/^LOG: //p' "$OUT/accept-$a.txt" 2>/dev/null | head -1)
+        post=$( [ -n "$log" ] && grep -aoE "PARITY:V4_POST [^[:cntrl:]]*" "$log" | head -1)
+        sys=$(  [ -n "$log" ] && grep -aoE "PARITY:V4_SYSTEM [^[:cntrl:]]*" "$log" | head -1)
+        boots+=("| $a | \`${log:-none}\` | \`${post:-none}\` | \`${sys:-none}\` |")
+    done
+    hashes=$(for a in amd64 aarch64 riscv64; do
+                 log=$(sed -n 's/^LOG: //p' "$OUT/accept-$a.txt" 2>/dev/null | head -1)
+                 [ -n "$log" ] && grep -aoE "PARITY:V4_SYSTEM [^[:cntrl:]]*" "$log" | sed -n 's/.*dict_hash=//p' | head -1
+             done)
+    nh=$(grep -c . <<<"$hashes" || true); nu=$(sort -u <<<"$hashes" | grep -c . || true)
+    if [ "$nh" = 3 ] && [ "$nu" = 1 ]; then same="the same on all three: \`$(head -1 <<<"$hashes")\`"
+    else same="**not** one value on three architectures ($nh found, $nu distinct)"; result=FAIL; why+=("dict_hash"); fi
+    t32=$(grep -E '[0-9]+ checks, [0-9]+ failures' "$OUT/test-32.txt" 2>/dev/null |
+          awk '{c+=$(NF-3); f+=$(NF-1)} END {printf "%d programs, %d checks, %d failures", NR, c, f}')
+    isalog=$(find logs -path '*/isabelle/*.log' -newer "$PROTO/commit" 2>/dev/null | sort | tail -1)
+    {
+        echo "# Protocol for ${commit:0:8}"
+        echo
+        echo "- Commit: $commit"
+        echo "- Tree: $tree"
+        echo "- Result: $result"
+        echo
+        echo "\`scripts/nightly.sh protocol\` (#135), begun $ts UTC; \`$(git log -1 --format=%s "$commit")\`."
+        [ ${#why[@]} = 0 ] || { echo; echo "Not passed: $(IFS=';'; echo "${why[*]}")."; }
+        echo
+        echo "## Stages"
+        echo
+        echo "| Stage | Result | Output |"
+        echo "|---|---|---|"
+        printf '%s\n' "${rows[@]}"
+        echo
+        echo "## The boots"
+        echo
+        echo "| Boot | Serial log | POST | System |"
+        echo "|---|---|---|---|"
+        printf '%s\n' "${boots[@]}"
+        echo
+        echo "dict_hash: $same."
+        echo
+        echo "## test-32"
+        echo
+        echo "${t32:-not run}"
+        echo
+        echo "## The proofs"
+        echo
+        echo "\`${isalog:-none}\`"
+        echo
+        echo "## The images (SHA-256)"
+        echo
+        echo '```'
+        cat "$OUT/SHA256SUMS" 2>/dev/null || echo "not built"
+        echo '```'
+        echo
+        echo "## The documents (SHA-256)"
+        echo
+        echo '```'
+        cat "$DOCS/SHA256SUMS" 2>/dev/null || echo "not built"
+        echo '```'
+    } > "$dir/PROTOCOL.md"
+    echo "=== nightly: $dir/PROTOCOL.md: $result"
+    [ "$result" = PASS ]
+    ;;
 *) usage ;;
 esac