build/ci/docs: re-green CI (dune < 3.24, rocq < 9.2), repo hygiene, script-derived README status (#84)

- pin dune < 3.24 and rocq-runtime/coq-core/coq-stdlib
  < 9.2 (upstream breaks)
  - weekly CI cron + workflow_dispatch, per-job timeouts, dependabot, MIT LICENSE
  - script-derived README status table + CI doc-count gate; docs drift sweep
  - check.py warns on cert backend.version vs manifest adapter_version

Author: levineuwirth

.github/dependabot.yml

@@ -0,0 +1,17 @@
+# Dependabot: keep the SHA-pinned GitHub Actions in validate.yml current.
+# Every `uses:` there is pinned to a full commit SHA with a `# vX.Y.Z`
+# trailing comment (audit M8); Dependabot understands that convention
+# and bumps both the SHA and the comment. Solver / toolchain pins
+# (cvc5, Vampire, elan, Lean) are NOT actions and stay manual — a bump
+# of any of those regenerates fixtures or trips delta.md §5 and needs
+# the toolchain-refresh playbook, not an automated PR.
+version: 2
+updates:
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "weekly"
+      day: "monday"
+    labels: ["ci"]
+    commit-message:
+      prefix: "ci"

.github/workflows/validate.yml

@@ -4,10 +4,27 @@ on:
   push:
     branches: [main]
   pull_request:
+  # Weekly cron (Monday 06:17 UTC): the toolchain surface — apt z3/cvc4,
+  # opam's newest resolvable rocq/dune/Mathlib caches, GitHub release
+  # assets — moves under a quiet repo. A scheduled run turns "CI will be
+  # red on the next push" (the dune-3.24 break sat unnoticed for 72
+  # days) into a red badge within a week. Odd minute to avoid the
+  # top-of-hour queue.
+  schedule:
+    - cron: "17 6 * * 1"
+  # Manual re-run without a push (no-op PRs are not needed to re-validate).
+  workflow_dispatch:
 
 jobs:
   schemas:
     runs-on: ubuntu-latest
+    # timeout-minutes on every job: ~2x the observed wall-clock of the
+    # last green main run (schemas 10 s, sdk 1m54, cross-platform 2m18,
+    # lean-bridge 15m09, rocq-bridge 6m20) so a hung solver or a
+    # runaway Mathlib build fails the job instead of burning the
+    # 6-hour default. Raise deliberately when a phase adds real work
+    # (R1's live suite, R0.5's Mathlib bump).
+    timeout-minutes: 10
     steps:
       - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0  # v7.0.0
 
@@ -29,6 +46,16 @@ jobs:
       - name: Run cross-doc checker negative tests
         run: python tools/test_check.py
 
+      # Doc-count gate: every number README's Status section shows is
+      # printed by tools/status_table.py from the committed JSON/source
+      # files; the embedded copy must match byte-for-byte. Hand-typed
+      # counts went stale within weeks every time (retros); this turns
+      # that into a red schemas job. `--write` refreshes the block.
+      - name: README status table up to date
+        run: |
+          python tools/status_table.py --check
+          python tools/test_status_table.py
+
       - name: Run trust-gate parser tests (axiom-check C2/C3)
         run: python tools/test_check_axioms.py
 
@@ -85,6 +112,7 @@ jobs:
 
   sdk:
     runs-on: ubuntu-latest
+    timeout-minutes: 20
     steps:
       - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0  # v7.0.0
 
@@ -102,6 +130,22 @@ jobs:
       - name: Install Python validator deps
         run: pip install -r tools/requirements.txt
 
+      - name: Pin dune < 3.24 (rocq-runtime constraint, WATCH)
+        # dune 3.24 (2026-06-21) deleted `(using coq …)` from the dune
+        # language; only `(using rocq 0.11)` parses there. But every
+        # published rocq-runtime (<= 9.2.0) declares
+        # `dune {>= "3.8" & < "3.24"}` (`opam show rocq-runtime.9.2.0`),
+        # so a dune-3.24 workspace cannot host the Rocq bridge at all.
+        # dune-project therefore stays on `(using coq 0.8)` and pins
+        # `(dune (< 3.24))` in every package. setup-ocaml installs the
+        # newest dune; pin it here BEFORE the deps so `dune build` parses
+        # dune-project. (The rocq-bridge job gets the same downgrade for
+        # free from rocq-runtime's constraint and needs no pin step.)
+        # WATCH(rocq-dune-3.24): when a rocq-runtime release lifts the
+        # bound, migrate dune-project to `(lang dune 3.24)` +
+        # `(using rocq 0.11)` and delete this step in all three jobs.
+        run: opam install -y "dune<3.24"
+
       - name: Install SDK deps
         # The opam files (proof_broker.opam, proof_broker_rocq.opam)
         # live at repo root after the Phase 1 workspace merge; pre-
@@ -194,6 +238,7 @@ jobs:
           - os: macos-14
             label: macos-aarch64
     runs-on: ${{ matrix.os }}
+    timeout-minutes: 20
     name: sdk-cross-platform (${{ matrix.label }})
     steps:
       - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0  # v7.0.0
@@ -203,6 +248,22 @@ jobs:
           ocaml-compiler: "5.4"
           dune-cache: true
 
+      - name: Pin dune < 3.24 (rocq-runtime constraint, WATCH)
+        # dune 3.24 (2026-06-21) deleted `(using coq …)` from the dune
+        # language; only `(using rocq 0.11)` parses there. But every
+        # published rocq-runtime (<= 9.2.0) declares
+        # `dune {>= "3.8" & < "3.24"}` (`opam show rocq-runtime.9.2.0`),
+        # so a dune-3.24 workspace cannot host the Rocq bridge at all.
+        # dune-project therefore stays on `(using coq 0.8)` and pins
+        # `(dune (< 3.24))` in every package. setup-ocaml installs the
+        # newest dune; pin it here BEFORE the deps so `dune build` parses
+        # dune-project. (The rocq-bridge job gets the same downgrade for
+        # free from rocq-runtime's constraint and needs no pin step.)
+        # WATCH(rocq-dune-3.24): when a rocq-runtime release lifts the
+        # bound, migrate dune-project to `(lang dune 3.24)` +
+        # `(using rocq 0.11)` and delete this step in all three jobs.
+        run: opam install -y "dune<3.24"
+
       - name: Install SDK deps
         # See retry rationale in the `sdk` job's Install SDK deps step.
         run: |
@@ -282,6 +343,7 @@ jobs:
 
   lean-bridge:
     runs-on: ubuntu-latest
+    timeout-minutes: 40
     needs: sdk
     steps:
       - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0  # v7.0.0
@@ -353,6 +415,22 @@ jobs:
           sudo install -m 755 /tmp/vampire/vampire /usr/local/bin/vampire
           vampire --version | head -1
 
+      - name: Pin dune < 3.24 (rocq-runtime constraint, WATCH)
+        # dune 3.24 (2026-06-21) deleted `(using coq …)` from the dune
+        # language; only `(using rocq 0.11)` parses there. But every
+        # published rocq-runtime (<= 9.2.0) declares
+        # `dune {>= "3.8" & < "3.24"}` (`opam show rocq-runtime.9.2.0`),
+        # so a dune-3.24 workspace cannot host the Rocq bridge at all.
+        # dune-project therefore stays on `(using coq 0.8)` and pins
+        # `(dune (< 3.24))` in every package. setup-ocaml installs the
+        # newest dune; pin it here BEFORE the deps so `dune build` parses
+        # dune-project. (The rocq-bridge job gets the same downgrade for
+        # free from rocq-runtime's constraint and needs no pin step.)
+        # WATCH(rocq-dune-3.24): when a rocq-runtime release lifts the
+        # bound, migrate dune-project to `(lang dune 3.24)` +
+        # `(using rocq 0.11)` and delete this step in all three jobs.
+        run: opam install -y "dune<3.24"
+
       - name: Install SDK deps
         # See retry rationale in the `sdk` job's Install SDK deps step.
         run: |
@@ -406,6 +484,7 @@ jobs:
 
   rocq-bridge:
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     needs: sdk
     steps:
       - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0  # v7.0.0
@@ -476,6 +555,10 @@ jobs:
           opam update
 
       - name: Install SDK + rocq-bridge deps
+        # No explicit `dune<3.24` pin here: rocq-runtime's own
+        # `dune {>= "3.8" & < "3.24"}` constraint makes the solver
+        # downgrade dune (WATCH(rocq-dune-3.24), see the pin step in
+        # the sdk / sdk-cross-platform / lean-bridge jobs).
         # proof_broker_rocq pulls in rocq-runtime (>= 9.0); proof_broker
         # pulls the OCaml SDK deps; proof_broker_rocq_hammer
         # (Phase-3 #1 Rocq parity, opt-in HOL closer via hauto)
@@ -539,6 +622,7 @@ jobs:
     if: ${{ always() }}
     needs: [schemas, sdk, sdk-cross-platform, lean-bridge, rocq-bridge]
     runs-on: ubuntu-latest
+    timeout-minutes: 5
     steps:
       - name: Require every required job to have succeeded
         run: |

.gitignore

@@ -26,3 +26,8 @@ lake-manifest.json
 # Locally cached cvc5 release archive. Adapters spawn the system-installed
 # solver, not anything from this zip; it just lives in-repo for offline reinstall.
 cvc5-*.zip
+
+# Captured build logs the CI jobs (and the local harness) write at the repo root
+# for tools/check_axioms.py; never committed.
+lake_build.log
+rocq_build.log

AUDIT.md

@@ -13,6 +13,15 @@ The highest-severity findings were re-verified by hand against source
 
 ## 1. Status summary
 
+> **Status note (2026-08-30).** The table and the "Issue tracker &
+> pass status" block below are the 2026-05-17 snapshot. Since then,
+> audit passes 2–10 landed as PRs #21–#29, and the Rocq bridge
+> (marked "NOT BUILT" below and in §2) has been built locally on the
+> rocq 9.1.1 stack (2026-08-30; `rocq-runtime` is pinned `< 9.2` in
+> `dune-project` because 9.2.0 changed the `Assumptions.assumptions`
+> API used by `rocq-bridge/src/llm_replay.ml`) and is built in CI by
+> the dedicated `rocq-bridge` job in `validate.yml`.
+
 The project is in genuinely good shape. 4 of 5 CI surfaces pass
 end-to-end from a clean environment; the shipped trust footprint is
 exactly the documented 5 core axioms with **no `sorryAx`/`sorry`/admit**.

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2026 Levi Neuwirth
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.