Merge pull request 'release: v4.0.0-alpha.3; the proofs run capped to fit the server' (#132 ) from StarForth-v4.0.0 into master

release v4.0.0-alpha.3: accepted in full, logs
On 50d2bc98 (LithosAnanke v4.0.0-alpha.3), in this session, one QEMU at a time in the foreground: amd64 logs/20261107-195526, aarch64 -195725, riscv64 -200055 (POST 538/538, dict_hash=0xfec8c47cfc6f437f on all three), the stick loaded high, test-32 (39 programs, 0 failures); the proofs through the capped stage, logs/20261107-195341 (47 s, ~1.8 GiB). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
2026-11-07 20:52:52 +00:00 · 2026-11-07 20:09:33 +00:00 · 2026-11-07 19:54:47 +00:00 · 2026-11-07 19:32:30 +00:00 · 2026-11-07 19:15:04 +00:00 · 2026-11-07 18:59:34 +00:00
90 changed files with 2545 additions and 44 deletions
@@ -18,7 +18,8 @@ on:
  workflow_dispatch:

 concurrency:
-  group: qemu                     # one QEMU at a time on the runner: shared with nightly.yml and release.yml
+  group: qemu                     # every workflow shares this one group: one run at a time,
+                                  # a runner-image rebuild included (Captain Bob, 2026-11-07)
  cancel-in-progress: false

 jobs:
@@ -26,7 +27,7 @@ jobs:
    name: Acceptance
    runs-on: ubuntu-latest
    container:
-      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1   # ci/runner-image (#120)
+      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2   # ci/runner-image (#120)
      credentials:                # the registry refuses anonymous pulls
        username: rajames
        password: ${{ secrets.PACKAGES_TOKEN }}
@@ -37,6 +38,18 @@ 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

+      - name: The capsule-signing key
+        env:
+          KEY: ${{ secrets.CAPSULE_SIGN_KEY }}
+        run: |                    # ci/pki/make-ca.sh; kernel/Makefile signs with SIGN_KEY
+          if [ -n "$KEY" ]; then
+            f="${RUNNER_TEMP:-/tmp}/capsule-signing.key"
+            (umask 077; printf '%s\n' "$KEY" > "$f")
+            echo "SIGN_KEY=$f" >> "$GITHUB_ENV"; echo "The capsules will be signed."
+          else
+            echo "::warning::No CAPSULE_SIGN_KEY secret: the capsules are built unsigned."
+          fi
+
      - name: Acceptance amd64
        run: scripts/nightly.sh accept amd64
      - name: Acceptance aarch64
@@ -9,14 +9,20 @@ name: Build
 on:
  push:
    branches: [StarForth-v4.0.0]   # not master: what reaches it has just passed acceptance (#119)
+    paths-ignore: ['site/**']        # the websites (site/) build nothing here; each run is ~17 min on
+                                     # the server the wikis share (Captain Bob, 2026-11-07)
  workflow_dispatch:

+concurrency:
+  group: qemu                     # every workflow shares this one group (Captain Bob, 2026-11-07: a
+  cancel-in-progress: false       # runner-image rebuild blocks other jobs, always): one run at a time
+
 jobs:
  image:
    name: Image ${{ matrix.board }}
    runs-on: ubuntu-latest
    container:
-      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1   # ci/runner-image (#120)
+      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2   # ci/runner-image (#120)
      credentials:                # the registry refuses anonymous pulls
        username: rajames
        password: ${{ secrets.PACKAGES_TOKEN }}
@@ -34,6 +40,18 @@ 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

+      - name: The capsule-signing key
+        env:
+          KEY: ${{ secrets.CAPSULE_SIGN_KEY }}
+        run: |                    # ci/pki/make-ca.sh; kernel/Makefile signs with SIGN_KEY
+          if [ -n "$KEY" ]; then
+            f="${RUNNER_TEMP:-/tmp}/capsule-signing.key"
+            (umask 077; printf '%s\n' "$KEY" > "$f")
+            echo "SIGN_KEY=$f" >> "$GITHUB_ENV"; echo "The capsules will be signed."
+          else
+            echo "::warning::No CAPSULE_SIGN_KEY secret: the capsules are built unsigned."
+          fi
+
      - name: Boot image
        run: make boot_image TARGET=${{ matrix.board }}

@@ -52,7 +70,7 @@ jobs:
    name: v4 tests (32- and 64-bit cells)
    runs-on: ubuntu-latest
    container:
-      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1   # ci/runner-image (#120)
+      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2   # ci/runner-image (#120)
      credentials:                # the registry refuses anonymous pulls
        username: rajames
        password: ${{ secrets.PACKAGES_TOKEN }}
@@ -62,5 +80,17 @@ jobs:
        with:
          lfs: false

+      - name: The capsule-signing key
+        env:
+          KEY: ${{ secrets.CAPSULE_SIGN_KEY }}
+        run: |                    # ci/pki/make-ca.sh; kernel/Makefile signs with SIGN_KEY
+          if [ -n "$KEY" ]; then
+            f="${RUNNER_TEMP:-/tmp}/capsule-signing.key"
+            (umask 077; printf '%s\n' "$KEY" > "$f")
+            echo "SIGN_KEY=$f" >> "$GITHUB_ENV"; echo "The capsules will be signed."
+          else
+            echo "::warning::No CAPSULE_SIGN_KEY secret: the capsules are built unsigned."
+          fi
+
      - name: make -C v4 test
        run: make -C v4 test
@@ -14,12 +14,16 @@ on:
    - cron: '0 4 * * *'        # 04:00 UTC, after the images (nightly.yml, 03:00)
  workflow_dispatch:

+concurrency:
+  group: qemu                     # every workflow shares this one group (Captain Bob, 2026-11-07: a
+  cancel-in-progress: false       # runner-image rebuild blocks other jobs, always): one run at a time
+
 jobs:
  docs:
    name: Book, volumes, API reference
    runs-on: ubuntu-latest
    container:
-      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1   # ci/runner-image (#120)
+      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2   # ci/runner-image (#120)
      credentials:                # the registry refuses anonymous pulls
        username: rajames
        password: ${{ secrets.PACKAGES_TOKEN }}
@@ -1,12 +1,15 @@
-# Nightly snapshot of the kernel images: the acceptance protocol, the proofs, the board images,
-# then Nexus. Each stage is a step of scripts/nightly.sh (its header says what each does); any
-# failure stops the run, and nothing is published unless every stage before it passed.
+# Nightly snapshot of the kernel images: the acceptance protocol, the board images, Nexus, then
+# the proofs. Each stage is a step of scripts/nightly.sh (its header says what each does); any
+# failure stops the run, and nothing is published unless every stage before it passed. The proofs
+# come last and run whatever happened before them: they check the theories, not the images, so a
+# failed proof does not hold back images that passed acceptance -- it turns the run red.
 #
 #   org.starship:kernelImage:<LITHOS_VERSION>-SNAPSHOT, starshipos-snapshots
 #     classifier pc      StarshipOS.iso   amd64, UEFI -- the ISO the amd64 acceptance boot booted
 #     classifier raspi5  raspi5.img.xz    Raspberry Pi 5, for Raspberry Pi Imager
 #     classifier milkv   MilkV.img.xz     Milk-V Mars
-#     classifier logs    logs.tar.gz      this run's serial logs, proof log and DoE CSVs
+#     classifier logs    logs.tar.gz      this run's serial logs and DoE CSVs (the proof log is in
+#                                         the run's logs artifact)
 #
 # Gitea runs a schedule from the default branch, master, so this builds master.
 name: Nightly snapshot
@@ -17,15 +20,16 @@ on:
  workflow_dispatch:

 concurrency:
-  group: qemu                     # one QEMU at a time on the runner: shared with acceptance.yml
+  group: qemu                     # every workflow shares this one group: one run at a time,
+                                  # a runner-image rebuild included (Captain Bob, 2026-11-07)
  cancel-in-progress: false

 jobs:
  nightly:
-    name: Acceptance, proofs, images
+    name: Acceptance, images, proofs
    runs-on: ubuntu-latest
    container:
-      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1   # ci/runner-image (#120)
+      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2   # ci/runner-image (#120)
      credentials:                # the registry refuses anonymous pulls
        username: rajames
        password: ${{ secrets.PACKAGES_TOKEN }}
@@ -36,6 +40,18 @@ 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

+      - name: The capsule-signing key
+        env:
+          KEY: ${{ secrets.CAPSULE_SIGN_KEY }}
+        run: |                    # ci/pki/make-ca.sh; kernel/Makefile signs with SIGN_KEY
+          if [ -n "$KEY" ]; then
+            f="${RUNNER_TEMP:-/tmp}/capsule-signing.key"
+            (umask 077; printf '%s\n' "$KEY" > "$f")
+            echo "SIGN_KEY=$f" >> "$GITHUB_ENV"; echo "The capsules will be signed."
+          else
+            echo "::warning::No CAPSULE_SIGN_KEY secret: the capsules are built unsigned."
+          fi
+
      - name: Acceptance amd64
        run: scripts/nightly.sh accept amd64
      - name: Acceptance aarch64
@@ -46,8 +62,6 @@ jobs:
        run: scripts/nightly.sh accept stick-high
      - name: Acceptance 32-bit build
        run: scripts/nightly.sh test-32
-      - name: Isabelle/HOL proofs
-        run: scripts/nightly.sh proofs

      - name: Images
        run: scripts/nightly.sh images
@@ -64,6 +78,10 @@ jobs:
          name: kernel-images-${{ github.run_number }}
          path: build/nightly/

+      - name: Isabelle/HOL proofs
+        if: always()
+        run: scripts/nightly.sh proofs
+
      - name: Keep the logs and DoE CSVs
        if: always()
        uses: actions/upload-artifact@v3
@@ -14,7 +14,8 @@ on:
    tags: ['v*']

 concurrency:
-  group: qemu                     # one QEMU at a time on the runner: shared with acceptance.yml
+  group: qemu                     # every workflow shares this one group: one run at a time,
+                                  # a runner-image rebuild included (Captain Bob, 2026-11-07)
  cancel-in-progress: false

 jobs:
@@ -22,7 +23,7 @@ jobs:
    name: Release ${{ github.ref_name }}
    runs-on: ubuntu-latest
    container:
-      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:72b6cf370db1   # ci/runner-image (#120)
+      image: gitea.starshipos-f18.org/rajames/lithosananke-runner:4f675c8b75b2   # ci/runner-image (#120)
      credentials:                # the registry refuses anonymous pulls
        username: rajames
        password: ${{ secrets.PACKAGES_TOKEN }}
@@ -33,6 +34,18 @@ jobs:
          fetch-depth: 0
          lfs: false

+      - name: The capsule-signing key
+        env:
+          KEY: ${{ secrets.CAPSULE_SIGN_KEY }}
+        run: |                    # ci/pki/make-ca.sh; kernel/Makefile signs with SIGN_KEY
+          if [ -n "$KEY" ]; then
+            f="${RUNNER_TEMP:-/tmp}/capsule-signing.key"
+            (umask 077; printf '%s\n' "$KEY" > "$f")
+            echo "SIGN_KEY=$f" >> "$GITHUB_ENV"; echo "The capsules will be signed."
+          else
+            echo "::warning::No CAPSULE_SIGN_KEY secret: the capsules are built unsigned."
+          fi
+
      - name: The tag names the tree's version
        run: |
          tree="v$(sed -n 's/^LITHOS_VERSION *?= *//p' kernel/Makefile)"
@@ -41,7 +54,10 @@ jobs:
          echo "NIGHTLY_VERSION=${tree#v}" >> "$GITHUB_ENV"

      - name: Install the dependencies
-        run: make ARCH=amd64,aarch64,riscv64 init   # the image has all but the documents' packages
+        # INIT_PROOFS=0: the image's Isabelle has HOL-Library prebuilt; a full init would fetch a fresh
+        # Isabelle into the workspace and point isabelle at it, and the proofs would build HOL-Library
+        # from scratch -- killed (release run 196, v4.0.0-alpha.1)
+        run: make ARCH=amd64,aarch64,riscv64 init INIT_PROOFS=0   # the image has all but the documents' packages

      - name: Acceptance amd64
        run: scripts/nightly.sh accept amd64
@@ -17,6 +17,10 @@ on:
    paths: ['ci/runner-image/**', 'Makefile']
  workflow_dispatch:

+concurrency:
+  group: qemu                     # every workflow shares this one group (Captain Bob, 2026-11-07: a
+  cancel-in-progress: false       # runner-image rebuild blocks other jobs, always): one run at a time
+
 jobs:
  image:
    name: Build and publish the runner image
@@ -44,7 +48,9 @@ jobs:
          tag=$(git rev-parse --short=12 HEAD)
          ctx=$(mktemp -d)                                  # not the repository: 7 GB of context
          cp -r Makefile boards ci/runner-image/Dockerfile "$ctx/"
-          docker build -t "$img:$tag" "$ctx"
+          tok=$(mktemp); printf '%s' "$TOKEN" > "$tok"          # the HOL-Library heap's download (Dockerfile)
+          docker build --secret id=pkgtoken,src="$tok" -t "$img:$tag" "$ctx"
+          rm -f "$tok"
          echo "$TOKEN" | docker login gitea.starshipos-f18.org -u rajames --password-stdin
          docker push "$img:$tag"
          echo "Published $img:$tag"
@@ -1,5 +1,34 @@
 # Changelog

+## 2026-11-07 — LithosAnanke v4.0.0-alpha.3: the first published alpha
+
+`v4.0.0-alpha.2` (`2d43db25`) used the image's HOL-Library as intended, but its release run (200) ran
+the proofs with Isabelle's defaults -- Java's heap up to 4 GiB, a thread per CPU -- and they were
+killed in the StarForth session. Nothing was published; the tag stays where it is. The proofs now run
+capped (`scripts/nightly.sh proofs`: one thread, Java 512 MiB, Poly/ML 900 MiB; 47 s, ~1.8 GiB), and
+`v4.0.0-alpha.3` is the first alpha published. `docs/fabric/FABRIC-3.md` XLVII.6.
+
+## 2026-11-07 — LithosAnanke v4.0.0-alpha.2: not published
+
+`v4.0.0-alpha.1` (`233025da`) was accepted and tagged, but its release run (196) built HOL-Library
+from scratch in the proofs step and was killed: `release.yml`'s full `make init` replaced the
+image's Isabelle, the one with HOL-Library prebuilt. Nothing was published; the tag stays where it is
+(Captain Bob, 2026-11-07). `release.yml` now runs `init INIT_PROOFS=0`, and `v4.0.0-alpha.2` is the
+first alpha published -- the same system as below. `docs/fabric/FABRIC-3.md` XLVII.5.
+
+## 2026-11-07 — LithosAnanke v4.0.0-alpha.1: the first alpha release
+
+The first alpha of the kernel, `v4.0.0-alpha.1`: v4, StarForth's F18 engine, is the system every
+board boots by default, with v3 a boot argument away. The kernel's version goes from 2.1.0 to the
+4.x working line (Captain Bob, 2026-11-07); the engine stays 3.2.0. Accepted in full before the tag:
+amd64, aarch64 and riscv64 to `[zuse@Hera] ok>` with POST 538/538 and one `dict_hash`
+(`0xfec8c47cfc6f437f`), the PC stick loaded high, `test-32` (39 programs, 0 failures), and the
+Isabelle/HOL proofs. An alpha: the v4.0.0 milestone's own definition -- parity with v3's vocabulary,
+K=1.0 measured on v4, the hosted mesh, Verilator -- is still open, and the capsules are unsigned until
+the StarshipOS CA is made (FABRIC-3.md XLVI). Also today: CI in a prebuilt runner image, the
+nightly's proofs no longer able to hold back its images, and the .com and .org websites. Full record:
+`docs/fabric/FABRIC-3.md` XLVII.
+
 ## 2026-11-07 — CI jobs start ready: the runner image

 The CI jobs now run in `lithosananke-runner` (`ci/runner-image`, #120), an image with everything
@@ -0,0 +1,81 @@
+#!/bin/bash
+# make-ca.sh -- the StarshipOS capsule-signing PKI, made once, on the CI box (Captain Bob,
+# 2026-11-07: "New root CA on the CI box. Valid StarshipOS rather than snake oil intermediate").
+#
+#   StarshipOS Root CA              Ed25519, 20 years, self-signed. Its key never leaves this box:
+#                                   not in the repository, not in Gitea, not in any image.
+#   StarshipOS Capsule Signing      Ed25519, 10 years, signed by the root; CA:TRUE, pathlen:0.
+#                                   Its certificate is built into every image (capsules/pki/
+#                                   starshipos-intermediate.der) and checks each capsule at boot;
+#                                   its key signs the capsules (mkcapsule --sign-key), in CI from
+#                                   the repository secret CAPSULE_SIGN_KEY.
+#
+# Replaces the offline LithosAnanke Root CA and its snakeoil intermediate (FABRIC-2.md,
+# Milestone 6) for every build. Run as root:
+#
+#   sudo ci/pki/make-ca.sh [dir]                       # dir defaults to /var/lib/starshipos-ca
+#
+# It refuses to overwrite an existing CA. When it is done it prints the two certificates (public:
+# paste them where they are wanted) and says how to put the signing key into Gitea. With
+# GITEA_TOKEN set (a token that may administer the repository), it stores the secret itself.
+set -euo pipefail
+umask 077
+dir=${1:-/var/lib/starshipos-ca}
+repo=${GITEA_REPO:-rajames/LithosAnanke}
+api=${GITEA_API:-https://gitea.starshipos-f18.org/api/v1}
+
+command -v openssl >/dev/null || { echo "make-ca: needs openssl" >&2; exit 1; }
+[ -e "$dir/root/root.key" ] && { echo "make-ca: $dir already holds a CA; not overwriting it" >&2; exit 1; }
+mkdir -p "$dir/root" "$dir/signing"
+cd "$dir"
+
+cat > ca.cnf <<'CNF'
+[ req ]
+distinguished_name = dn
+prompt             = no
+[ dn ]
+[ root_ext ]
+basicConstraints     = critical, CA:TRUE
+keyUsage             = critical, keyCertSign, cRLSign
+subjectKeyIdentifier = hash
+[ signing_ext ]
+basicConstraints       = critical, CA:TRUE, pathlen:0
+keyUsage               = critical, keyCertSign, cRLSign, digitalSignature
+subjectKeyIdentifier   = hash
+authorityKeyIdentifier = keyid:always
+CNF
+
+# the root
+openssl genpkey -algorithm ed25519 -out root/root.key
+openssl req -new -x509 -key root/root.key -days 7305 -config ca.cnf -extensions root_ext \
+    -subj "/O=StarshipOS/CN=StarshipOS Root CA" -out root/root.pem
+
+# the capsule-signing intermediate, signed by the root
+openssl genpkey -algorithm ed25519 -out signing/signing.key
+openssl req -new -key signing/signing.key -config ca.cnf \
+    -subj "/O=StarshipOS/CN=StarshipOS Capsule Signing" -out signing/signing.csr
+openssl x509 -req -in signing/signing.csr -CA root/root.pem -CAkey root/root.key \
+    -CAcreateserial -days 3652 -extfile ca.cnf -extensions signing_ext -out signing/signing.pem
+openssl x509 -in signing/signing.pem -outform DER -out signing/starshipos-intermediate.der
+openssl verify -CAfile root/root.pem signing/signing.pem
+
+chmod 700 root signing; chmod 600 root/* signing/*
+
+if [ -n "${GITEA_TOKEN:-}" ]; then
+    python3 -c 'import json,sys; print(json.dumps({"data": open(sys.argv[1]).read()}))' signing/signing.key |
+    curl -fsS -o /dev/null -X PUT -H "Authorization: token $GITEA_TOKEN" -H 'Content-Type: application/json' \
+        "$api/repos/$repo/actions/secrets/CAPSULE_SIGN_KEY" -d @- &&
+    echo "make-ca: stored the signing key as $repo's secret CAPSULE_SIGN_KEY"
+else
+    echo "make-ca: put $dir/signing/signing.key, whole, into $repo's Actions secret CAPSULE_SIGN_KEY"
+    echo "         (Settings -> Actions -> Secrets), or run again with GITEA_TOKEN set -- after"
+    echo "         removing $dir, since it refuses to overwrite a CA."
+fi
+echo
+echo "=== The root certificate (public) -- $dir/root/root.pem"
+cat root/root.pem
+echo "=== The capsule-signing certificate (public) -- $dir/signing/signing.pem"
+cat signing/signing.pem
+echo "=== Fingerprints"
+openssl x509 -in root/root.pem -noout -fingerprint -sha256 -subject -enddate
+openssl x509 -in signing/signing.pem -noout -fingerprint -sha256 -subject -issuer -enddate
@@ -1,7 +1,8 @@
 # The CI runner image (#120): gitea/runner-images' Ubuntu 24.04 with Node -- which
 # actions/checkout and upload-artifact run on -- plus everything the jobs install at their start:
 # what `make ARCH=amd64,aarch64,riscv64 init INIT_DOCS=0` installs (taken from the Makefile
-# itself, not copied, so the two cannot drift), and Maven and a JRE for the publish steps.
+# itself, not copied, so the two cannot drift), Maven and a JRE for the publish steps, and
+# Isabelle's HOL-Library already built, for the proofs.
 #
 # Built by .gitea/workflows/runner-image.yml, from a context of the Makefile, boards/ and this file.
 FROM gitea/runner-images:ubuntu-24.04-v26.11.03
@@ -11,4 +12,19 @@ WORKDIR /opt/starship-init
 RUN make --no-print-directory ARCH=amd64,aarch64,riscv64 init INIT_DOCS=0 \
 && DEBIAN_FRONTEND=noninteractive apt-get install -y -qq maven default-jre-headless \
 && rm -rf /var/lib/apt/lists/* /opt/starship-init/build/cache/downloads
+# HOL-Library, prebuilt, into Isabelle's own heaps, so the proofs build only the StarForth session
+# (~2.2 GiB, under a minute). Built from scratch it takes ~5.3 GiB (nightly 174 was killed doing it),
+# and capped it still needs ~2.6-3.3 GiB: more than the server has. So it is built once, elsewhere,
+# by the same Isabelle2025-2, and fetched from this repository's package registry, its checksum
+# pinned here (FABRIC-3.md XLVII). Isabelle ships its own HOL heap the same way. The token is a
+# build secret (runner-image.yml): it is in neither the image nor its history.
+ARG HOL_LIBRARY_URL=https://gitea.starshipos-f18.org/api/packages/rajames/generic/isabelle-hol-library/Isabelle2025-2/hol-library-Isabelle2025-2.tar.xz
+ARG HOL_LIBRARY_SHA256=bb24784664def9379e5db27f88802e3679b8e1c628177f6fbe7084e999cb339e
+RUN --mount=type=secret,id=pkgtoken \
+    curl -fsSL -H "Authorization: token $(cat /run/secrets/pkgtoken)" -o /tmp/hol-library.tar.xz "$HOL_LIBRARY_URL" \
+ && echo "$HOL_LIBRARY_SHA256  /tmp/hol-library.tar.xz" | sha256sum -c - \
+ && heaps=$(isabelle getenv -b ISABELLE_HEAPS_SYSTEM) && mkdir -p "$heaps" \
+ && xz -dc /tmp/hol-library.tar.xz | tar -C "$heaps" -xf - \
+ && rm /tmp/hol-library.tar.xz \
+ && test -s "$heaps/polyml-5.9.2_x86_64_32-linux/HOL-Library"
 WORKDIR /
@@ -6061,3 +6061,133 @@ four conflicts resolved to the branch's files (`92ca805e`).
 - The first scheduled nightly's publish to Nexus (#17).
 - The Pi 5 and Mars images booted on their boards (#27, #28); a Pi 4 port (#26).
 - Revoke the access token `claude-session-20261106` (Settings, Applications).
+
+## XLVI. The StarshipOS CA: capsules signed in CI, by a root on the CI box (2026-11-07)
+
+### 1. Found
+
+Every image built anywhere but Captain Bob's machine carried unsigned capsules: CI, the
+acceptance runs, the nightly bound for Nexus, a release, the demo. The capsule-signing key -- the
+snakeoil intermediate of the offline LithosAnanke Root CA (FABRIC-2.md, Milestone 6) -- lived only
+there, `kernel/Makefile`'s `SIGN_KEY` named its path, and a missing signature is a warning by
+design (2026-08-26), so they booted: `V4: capsule v4:sys:core.f18 signature: missing (unsigned)`
+in every accepted log (`logs/20261106-004933`). And `mkcapsule` signed with whatever key it was
+given: a key that is not the embedded certificate's makes every signature INVALID, which refuses
+Mama.
+
+### 2. Ruled
+
+Captain Bob, 2026-11-07: "New root CA on the CI box. Valid StarshipOS rather than snake oil
+intermediate."
+
+### 3. Built
+
+- `ci/pki/make-ca.sh`, run once on the CI box: **StarshipOS Root CA** (Ed25519, 20 years,
+  self-signed; its key stays on that box, in `/var/lib/starshipos-ca`) and **StarshipOS Capsule
+  Signing** (Ed25519, 10 years, issued by the root, `CA:TRUE, pathlen:0`). It refuses to
+  overwrite a CA, prints both certificates, and stores the signing key as the repository secret
+  `CAPSULE_SIGN_KEY` (or says how).
+- The image carries `capsules/pki/starshipos-intermediate.der` in place of the snakeoil
+  intermediate; the kernel finds it by one name, `CAPSULE_SIGNING_CERT_NAME` (`capsule_sig.h`).
+- `mkcapsule` checks the signing key against that certificate before it writes anything, and
+  refuses a key that is not its, or a key with no certificate to check.
+- `SIGN_KEY` has no default (`kernel/Makefile`, `v4/Makefile`): CI sets it from the secret (a step
+  in `acceptance.yml`, `build.yml`, `nightly.yml`, `release.yml`); unset, the capsules are built
+  unsigned, as before.
+
+What it is not: the kernel still does not check the intermediate against a root at boot
+(`x509_ed25519.h`; `ACL.4th`'s `ACL-CA-KEY` is still 0). A signature proves a capsule matches the
+certificate in the same image. That is unchanged by this, and a ruling of its own.
+
+### 4. Verified
+
+With a CA made by `make-ca.sh` in a scratch directory (not the real one): `openssl verify` of the
+chain OK; `make-ca.sh` refuses a second run; `mkcapsule` with the signing key -- "signing key
+matches"; with the root's key -- refused; with a key and no certificate -- refused; with no key --
+unsigned, as before. The acceptance with the real certificate is the PR's.
+
+## XLVII. LithosAnanke v4.0.0-alpha.1: the first alpha release (2026-11-07)
+
+### 1. Ruled
+
+Captain Bob, 2026-11-07: "next on the list is do a tag/release of v4.0.0" -- then, on what the number
+names: "StarForth version stays the same ... Kernel is 4.0.0. This is our first alpha release." The
+tag names the kernel (`release.yml`: `v<LITHOS_VERSION>`), so:
+
+- `LITHOS_VERSION` 2.1.0 -> **4.0.0-alpha.1**; the tag is `v4.0.0-alpha.1`; Nexus takes
+  `org.starship:kernelImage:4.0.0-alpha.1` and `org.starship:documentation:4.0.0-alpha.1`.
+- The engine's `VERSION` stays **3.2.0**.
+- The versioning policy (`kernel/Makefile`, FABRIC-3.5.md XXX): 4.x is a working line (even major).
+  v3.0.0, the first LTS, is no longer the next number; an LTS line takes the next odd major when
+  XXX.5's criteria are met. Alphas are numbered: a release repository takes each version once.
+- The v4.0.0 milestone is unchanged: its definition (v4 equivalent to v3, K=1.0 on all three host
+  ISAs, a hosted mesh, Verilator co-simulation) is what 4.0.0 itself will be; nine of its issues
+  are open. This is an alpha of it.
+- The release is built and proved here first (this session, 15 GiB), its logs committed; the
+  server's release run follows once it can pass -- the proofs need HOL-Library in the runner image.
+  The capsules are unsigned for this release.
+
+### 2. Verified (this session, `b7534107`, before the tag)
+
+- amd64 (`logs/20261107-150809`), aarch64 (`-151023`), riscv64 (`-151359`): `LithosAnanke
+  v4.0.0-alpha.1 <arch>`, `[zuse@Hera] ok>`, `PARITY:V4_POST tests=538 pass=538 fail=0`,
+  `POST: PASSED`, Zuse identity confirmed, `PARITY:V4_SYSTEM word_count=317
+  dict_hash=0xfec8c47cfc6f437f` on all three.
+- The PC stick loaded high (`logs/20261107-151539`): the same, from the stick, no fault.
+- `make -C v4 test-32`: 39 programs, 0 failures.
+- The Isabelle/HOL proofs (`logs/20261107-152312/isabelle`).
+- Each v4 capsule logs `signature: no root key (cert not found/parseable)`: the kernel looks for the
+  StarshipOS Capsule Signing certificate (XLVI), which is not in the tree until `ci/pki/make-ca.sh`
+  has run. A warning, as "missing (unsigned)" was before; nothing is refused.
+
+### 3. The StarshipOS CA, and acceptance again (`4ca935d8`)
+
+`ci/pki/make-ca.sh` ran on the CI box (2026-11-07 16:50 UTC): the StarshipOS Root CA there, the
+signing key in the secret `CAPSULE_SIGN_KEY`, and the certificate -- O=StarshipOS, CN=StarshipOS
+Capsule Signing, issued by the root, 2026-11-07 to 2036-11-06, `CA:TRUE, pathlen:0`, SHA-256 of the
+DER `13a28dda...029b9a6c` -- in the tree as `capsules/pki/starshipos-intermediate.der`, the snakeoil
+intermediate out of it. The tree changed, so the protocol ran again here: amd64
+(`logs/20261107-165611`), aarch64 (`-165817`), riscv64 (`-170149`) -- POST 538/538,
+`dict_hash=0xfec8c47cfc6f437f` on all three; the stick loaded high (`-170326`); `test-32`, 39
+programs, 0 failures; the proofs (`-171020`). Each capsule now logs `signature: missing (unsigned)`:
+the kernel found and read the StarshipOS certificate (it said "no root key" without it), and this
+session has no key to sign with. CI signs with the secret: the PR's acceptance and the release are
+where every capsule first verifies.
+
+### 4. HOL-Library, prebuilt
+
+The runner image was to build HOL-Library itself (XLVI's companion change, `4ae1f759`); the server
+cannot: from scratch it peaks at ~5.3 GiB, and with Poly/ML capped at 1.6 GiB the build still needs
+Isabelle's Java side at ~1 GiB (at 384 MiB it ran out and hung) -- 2.6-3.3 GiB against the server's
+3.8 GiB in all, ~2.3 GiB free with both wikis stopped. So the heap built here by the same
+Isabelle2025-2 (HOL-Library and its build database) is a package in this repository's registry,
+`generic/isabelle-hol-library/Isabelle2025-2/hol-library-Isabelle2025-2.tar.xz` (45 MB, SHA-256
+`bb247846...e999cb339e`), and the image fetches it into Isabelle's system heaps, checksum pinned,
+its token a Docker build secret. Shown portable first: a fresh Isabelle home holding only that heap
+checks the StarForth session without rebuilding HOL-Library (24 s).
+
+### 5. v4.0.0-alpha.1 not published; v4.0.0-alpha.2
+
+PR #127 merged (`4f675c8b`, acceptance run 192 with the capsules signed); `runner-image.yml` built
+`lithosananke-runner:4f675c8b75b2` with HOL-Library fetched (checksum OK, 4.8 s); PR #128 moved the
+workflows onto it (`233025da`, acceptance run 195 in the new image). `v4.0.0-alpha.1` was tagged on
+`233025da`. Its release run (196) passed acceptance in full, then the proofs step built HOL-Library
+from scratch and was killed (exit 137): `release.yml` ran a full `make init` for the documents'
+packages, which also fetched Isabelle into the workspace and pointed `/usr/local/bin/isabelle` at it
+-- an Isabelle without the image's HOL-Library. Nothing was published. Ruled (Captain Bob,
+2026-11-07): the tag stays where it is; `release.yml` runs `init INIT_PROOFS=0` (as
+`nightly-docs.yml` does), `LITHOS_VERSION` becomes `4.0.0-alpha.2`, and `v4.0.0-alpha.2` is the
+first published alpha.
+
+### 6. v4.0.0-alpha.2 not published either; v4.0.0-alpha.3
+
+PR #130 merged (`2d43db25`, acceptance run 199; run 197 before it failed one riscv64 check, #131);
+`v4.0.0-alpha.2` tagged there. Its release run (200) passed acceptance and used the image's
+Isabelle and HOL-Library, as XLVII.5 meant -- then the StarForth session was killed (exit 137) in
+the proofs: Isabelle ran with its defaults, Java's heap up to 4 GiB and a thread per CPU, more than
+the server (3.8 GiB, ~2.3 GiB free with the wikis stopped; perhaps a per-job cap besides). Capped
+-- one thread, Java 512 MiB, Poly/ML 900 MiB, in a settings file of a home made for the run, its
+heaps linked to the user's -- the session passes in 47 s at ~1.8 GiB, through
+`scripts/nightly.sh proofs` itself (`logs/20261107-195341`). Nothing was published. Ruled (Captain
+Bob, 2026-11-07): the tag stays; `LITHOS_VERSION` `4.0.0-alpha.3`, the first published alpha; the
+review list begun meanwhile goes to the milestone v4.0.0-alpha.4.
--- a/Show More
+++ b/Show More