Merge origin/main into feat/solo-core-metatheory-proofs

Reconcile the metatheory-proofs branch (61 commits off an old base) with
the standalone-CI + codegen work that has since landed on main. Conflict
resolutions:

- CI workflows (governance.yml, scorecard.yml, scorecard-enforcer.yml,
  hypatia-scan.yml): take main's versions. main migrated these off the
  estate "standards" reusables to self-contained standalone gates (#603/
  #604) precisely to stop the run-creation startup_failures; the branch's
  re-adoption of the reusables predates that work. main's hypatia-scan.yml
  also restores the permissions Hypatia needs (security-events: write,
  pull-requests: write, secrets: inherit) and the MPL-2.0 SPDX id that the
  Palimpsest license doc itself mandates for tooling.
- docs/PROOF-NEEDS: drop the branch's stale 103-line .md; keep main's
  canonical 359-line .adoc authored in #609 (also satisfies DOC-FORMAT).
- docs/history/MODULE-SYSTEM-PROGRESS: keep the branch's .md -> .adoc
  migration; port main's additive #138 codegen-follow-up note + status-
  table row into the .adoc so main's work is not lost.

spark-theatre-gate.yml and mirror.yml were identical to main. Tree builds
clean (dune build).

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

Author: claude

.claude/CLAUDE.md

@@ -230,24 +230,35 @@ not the log content. The fast paths for an agent are:
   `gh run view --log-failed <run-id>`; do not loop trying to scrape
   the UI.
 
-### Known-failing baseline checks
-
-These checks currently fail on *every* PR for repo-wide reasons, not
-because of any individual PR's changes. Do not waste turns
-investigating them on a per-PR basis:
-
-* `vscode-smoke` — npm 404 on `@hyperpolymath/affine-vscode` (the
-  in-editor harness depends on a not-yet-published npm package).
-* `migration-assistant` — was fixed by #342, but any branch created
-  from a base older than #342 will still see it red until rebased.
-* `governance / Language / package anti-pattern policy` — flags the
-  approved TypeScript exemptions (`affinescript-deno-test/*.ts`,
-  `editors/vscode/test/*.js`, etc., all documented in this file's
-  exemptions tables); the check has no allowlist for them.
-* The Hypatia security-scan bot comment — 143 findings; the bulk are
-  the same TypeScript exemption hits + pre-existing root files. A
-  real new finding will show as a *delta* in the count; otherwise
-  ignore.
+### Known-failing baseline checks — updated 2026-06-20
+
+Historically these failed on *every* PR for repo-wide reasons. Most are now
+resolved; kept here with current status so agents don't re-investigate:
+
+* `vscode-smoke` — **now passes**. Self-contained since the codegen-embed fix
+  (skips cleanly when the optional `@hyperpolymath/affine-vscode` npm package
+  is absent). The old "npm 404 fails every PR" no longer holds.
+* `migration-assistant` — **passes on current `main`**; only red on branches
+  based before #342. Rebase to clear.
+* `governance` — replaced (#603/#604) by a self-contained local gate
+  (`tools/ci/governance-standalone.sh`); the old estate
+  `Language / package anti-pattern policy` sub-check (from the
+  `hyperpolymath/standards` reusable) no longer runs.
+* The Hypatia security-scan bot *comment* — ~43–71 findings depending on scan
+  scope; the bulk are the documented TypeScript/JS exemptions + pre-existing
+  root files. A real new finding shows as a *delta in your changed files*;
+  otherwise ignore. (The Hypatia *check run* gates separately and is green.)
+
+**CI is now standalone and green on `main` (since #604 / `c7922cf`).** Two
+`startup_failure` classes bit `ci` / `governance` / `secret-scanner` for days
+(and `main` itself) — worth knowing so they aren't reintroduced:
+
+1. The repo's Actions "allowed actions" policy **rejects tag-pinned action
+   refs at run-creation** (a `startup_failure` with zero jobs). **Pin every
+   `uses:` to a full commit SHA** — `actions/foo@v4` will fail to start.
+2. A reusable-workflow *caller* that declares `concurrency:` on the same key
+   the reusable also declares is rejected at run-creation (BP008 — see
+   `.github/workflows/spark-theatre-gate.yml`).
 
 If a check from this list *changes status* on a PR (e.g.
 `vscode-smoke` suddenly passes, or Hypatia surfaces a new class of

.github/workflows/affine-vscode-publish.yml

@@ -32,7 +32,7 @@ jobs:
     timeout-minutes: 10
     steps:
       - name: Checkout code
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       - name: Verify tag matches package version
         working-directory: packages/affine-vscode
         run: |

.github/workflows/casket-pages.yml

@@ -49,9 +49,9 @@ jobs:
     timeout-minutes: 10
     steps:
       - name: Checkout
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v4
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       - name: Checkout casket-ssg
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v4
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
         with:
           repository: hyperpolymath/casket-ssg
           path: .casket-ssg

.github/workflows/ci.yml

@@ -1,4 +1,16 @@
 # SPDX-License-Identifier: MPL-2.0
+#
+# Standalone CI: no dependency on third-party actions or external-repo
+# reusable workflows. The OCaml toolchain is self-hosted via apt + opam
+# (replacing ocaml/setup-ocaml), and only first-party `actions/*` are used
+# (checkout / setup-node / upload-artifact), SHA-pinned. dune-project requires
+# OCaml >= 4.14, satisfied by the runner's apt OCaml (ocaml-system), with a
+# base-compiler fallback.
+#
+# NOTE on pins: first-party `actions/*` are SHA-pinned (repo SHA-pinning
+# policy + Hypatia workflow_audit + the "allowed actions" policy that rejects
+# tag refs at run-creation). `actions/checkout` is v7.0.0 (`9c091bb…`, bumped
+# by Dependabot in #605); `setup-node` / `upload-artifact` remain v4.
 name: CI
 on:
   push:
@@ -9,27 +21,36 @@ permissions:
   contents: read
 # Actions concurrency pool. Applied only to read-only check workflows
 # (no publish/mutation), so cancelling a superseded run is always safe.
+# Safe here: this is a normal workflow (not a reusable-workflow caller),
+# so there is no caller/reusable concurrency stacking (the BP008 startup
+# failure class).
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 jobs:
   build:
     runs-on: ubuntu-latest
-    timeout-minutes: 10
+    timeout-minutes: 25
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
-      - name: Set up OCaml
-        uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3
-        with:
-          ocaml-compiler: "5.1"
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+      - name: Set up OCaml toolchain (self-hosted; replaces ocaml/setup-ocaml)
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends opam ocaml
+          opam init --bare --disable-sandboxing --yes
+          # Prefer the runner's system OCaml (>= 4.14 satisfies dune-project)
+          # for an instant switch; fall back to a pinned base compiler.
+          opam switch create . ocaml-system --no-install --yes \
+            || opam switch create . ocaml-base-compiler.4.14.2 --no-install --yes
+          opam exec -- ocaml -version
       - name: Set up Node.js
         uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v4
         with:
           node-version: "20"
       - name: Install dependencies
-        run: opam install . --deps-only --with-test --with-doc
+        run: opam install . --deps-only --with-test --with-doc --yes
       - name: Install tree-sitter CLI (for res-to-affine walker tests)
         # Same rationale as the migration-assistant job (see below):
         # npm distribution is the fast CI install (~5 s). The walker
@@ -72,21 +93,25 @@ jobs:
         run: opam exec -- dune build @fmt
   lint:
     runs-on: ubuntu-latest
-    timeout-minutes: 10
+    timeout-minutes: 25
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
-      - name: Set up OCaml
-        uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3
-        with:
-          ocaml-compiler: "5.1"
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+      - name: Set up OCaml toolchain (self-hosted; replaces ocaml/setup-ocaml)
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends opam ocaml
+          opam init --bare --disable-sandboxing --yes
+          opam switch create . ocaml-system --no-install --yes \
+            || opam switch create . ocaml-base-compiler.4.14.2 --no-install --yes
+          opam exec -- ocaml -version
       - name: Install dependencies
         # Match the build job: `dune build` compiles everything including
         # test/ (which depends on alcotest, with-test) and the @doc target
         # below (which depends on odoc, with-doc). Without these flags, lint
         # fails on missing alcotest before it ever reaches the doc step.
-        run: opam install . --deps-only --with-test --with-doc
+        run: opam install . --deps-only --with-test --with-doc --yes
       - name: Build
         run: opam exec -- dune build
       - name: Lint with odoc
@@ -97,17 +122,21 @@ jobs:
     # §"Bench standards". Does NOT block merge. Promotion to a
     # ratcheted gate requires a calibrated baseline first.
     runs-on: ubuntu-latest
-    timeout-minutes: 10
+    timeout-minutes: 25
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
-      - name: Set up OCaml
-        uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3
-        with:
-          ocaml-compiler: "5.1"
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+      - name: Set up OCaml toolchain (self-hosted; replaces ocaml/setup-ocaml)
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends opam ocaml
+          opam init --bare --disable-sandboxing --yes
+          opam switch create . ocaml-system --no-install --yes \
+            || opam switch create . ocaml-base-compiler.4.14.2 --no-install --yes
+          opam exec -- ocaml -version
       - name: Install dependencies
-        run: opam install . --deps-only --with-test --with-doc
+        run: opam install . --deps-only --with-test --with-doc --yes
       - name: Build bench targets
         run: opam exec -- dune build @bench --force
         continue-on-error: true
@@ -133,7 +162,7 @@ jobs:
           } >> "$GITHUB_STEP_SUMMARY"
       - name: Upload bench log
         if: always()
-        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v4
         with:
           name: bench-output
           path: bench-output.log
@@ -143,17 +172,21 @@ jobs:
     # docs/standards/TESTING.adoc §"Coverage (visibility-only)".
     # No merge-blocking floor today.
     runs-on: ubuntu-latest
-    timeout-minutes: 10
+    timeout-minutes: 25
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
-      - name: Set up OCaml
-        uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3
-        with:
-          ocaml-compiler: "5.1"
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+      - name: Set up OCaml toolchain (self-hosted; replaces ocaml/setup-ocaml)
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends opam ocaml
+          opam init --bare --disable-sandboxing --yes
+          opam switch create . ocaml-system --no-install --yes \
+            || opam switch create . ocaml-base-compiler.4.14.2 --no-install --yes
+          opam exec -- ocaml -version
       - name: Install dependencies
-        run: opam install . --deps-only --with-test --with-doc
+        run: opam install . --deps-only --with-test --with-doc --yes
       - name: Run tests with bisect_ppx instrumentation
         run: |
           opam exec -- dune runtest --force --instrument-with bisect_ppx
@@ -178,7 +211,7 @@ jobs:
           } >> "$GITHUB_STEP_SUMMARY"
       - name: Upload coverage HTML
         if: always()
-        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v4
         with:
           name: coverage-html
           path: _coverage
@@ -203,7 +236,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       - name: Set up Node.js
         uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v4
         with:
@@ -248,7 +281,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       - name: Set up Node.js
         uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v4
         with:

.github/workflows/codeql.yml

@@ -32,7 +32,7 @@ jobs:
             build-mode: none
     steps:
       - name: Checkout
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       - name: Initialize CodeQL
         uses: github/codeql-action/init@8aad20d150bbac5944a9f9d289da16a4b0d87c1e # v3.28.1
         with:

.github/workflows/governance.yml

@@ -1,16 +1,38 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
+#
+# Standalone governance gate. Previously a thin caller of
+# `hyperpolymath/standards/.github/workflows/governance-reusable.yml@main`;
+# that cross-repo dependency (a) coupled this repo's CI to another repo's
+# moving `@main` and (b) startup-failed because a `concurrency:` block in a
+# reusable-workflow caller, when the reusable also declares concurrency on the
+# same key, is rejected at run-creation (the BP008 class — see
+# spark-theatre-gate.yml's note). This self-contained version runs the repo's
+# own conservative, delta-aware checks (tools/ci/governance-standalone.sh) and
+# is a normal workflow, so the concurrency block is safe to keep.
 name: Governance
-
 on:
   push:
     branches: [main, master]
   pull_request:
-    branches: [main, master]
   workflow_dispatch:
-
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 permissions:
   contents: read
-
 jobs:
   governance:
-    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@5a93d9d57cc04de4002d6d0ecd336fc7a8698910
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        with:
+          fetch-depth: 0
+      - name: Fetch base ref (DOC-FORMAT delta)
+        if: github.event_name == 'pull_request'
+        run: git fetch --no-tags origin "+refs/heads/${GITHUB_BASE_REF}:refs/remotes/origin/${GITHUB_BASE_REF}"
+      - name: Run governance gate
+        env:
+          GITHUB_BASE_REF: ${{ github.base_ref }}
+        run: ./tools/ci/governance-standalone.sh

.github/workflows/hypatia-scan.yml

@@ -1,6 +1,8 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
-name: Hypatia Security Scan
+# SPDX-License-Identifier: MPL-2.0
+# Thin wrapper around hyperpolymath/standards hypatia-scan-reusable.yml.
+# See standards#191 for the reusable's purpose and design.
 
+name: Hypatia Security Scan
 on:
   push:
     branches: [main, master, develop]
@@ -9,11 +11,15 @@ on:
   schedule:
     - cron: '0 0 * * 0'
   workflow_dispatch:
-
+# Estate guardrail: cancel superseded runs so re-pushes don't pile up.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 permissions:
   contents: read
-  security-events: read
-
+  security-events: write
+  pull-requests: write
 jobs:
-  scan:
-    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@5a93d9d57cc04de4002d6d0ecd336fc7a8698910
+  hypatia:
+    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@5eb28d7d8790d5389b7b6a5233fe6265a775e3d0
+    secrets: inherit

.github/workflows/panic-attack.yml

@@ -31,7 +31,7 @@ jobs:
     timeout-minutes: 10
     steps:
       - name: Checkout
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
         with:
           persist-credentials: false
       - name: Install Rust toolchain (stable)

.github/workflows/publish-jsr.yml

@@ -39,7 +39,7 @@ jobs:
     runs-on: ubuntu-latest
     timeout-minutes: 10
     steps:
-      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10
+      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       - uses: denoland/setup-deno@v2
         with:
           deno-version: v2.x

.github/workflows/release.yml

@@ -33,7 +33,7 @@ jobs:
     timeout-minutes: 10
     steps:
       - name: Checkout code
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       - name: Create the release (idempotent)
         env:
           GH_TOKEN: ${{ github.token }}
@@ -60,7 +60,7 @@ jobs:
     timeout-minutes: 10
     steps:
       - name: Checkout code
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
       - name: Set up OCaml
         uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3
         with: