checkpoint(2026-06-13): record dogfood proof-CI in state/roadmap/wiki + harden Lean job (#244)

hyperpolymath · claude · web-flow · commit df71e5f82733 · 2026-06-13T13:05:59.000+01:00
Estate checkpoint refresh (echidna half), tracked in #238. Brings the machine-readable state and docs current with PR #234 (proof corpus repaired + CI-gated, squash-merged to `main` 2026-06-06), and hardens the seam that flaked on #234. ## `docs(checkpoint)` — state/roadmap/wiki - **`STATE.a2ml`**: new `session-2026-06-13-dogfood-proof-ci` entry (changes, latent bugs fixed, CI-environment gotchas, gap closed); `last-updated` bumped. - **`ROADMAP.a2ml`**: proof-corpus CI recorded as a Stage-1 (Autonomous Proof Execution) gate; dates bumped. - **`docs/ROADMAP.md`**: proof-corpus CI noted alongside the R5a/R5b guardrails. - **`docs/wiki/{Getting-Started,Home}.md`**: document `just proofs*` + the dogfood proof-CI for local runs (wiki kept bleeding-edge). ## `ci(proofs)` — Lean dependability The Lean job let `lake build` resolve the pinned toolchain lazily; elan maps the version against the GitHub releases API, which flaked once on #234's pre-merge run (`failed to parse latest release tag`). The post-merge run on `main` passed, but the seam is non-deterministic. Now the exact toolchain from `proofs/lean/lean-toolchain` is pre-installed in the install step with retry/backoff, then `elan default`-ed — so `lake build` uses an already-resolved toolchain. Editing the workflow means the Dogfood CI runs on this PR and validates the change live. ## Flagged for owner (not changed here) - **Prover-count drift across surfaces**: GitHub repo *description* says "48 prover backends", the wiki says "128", `STATE.a2ml`/echidnabot say "113", `ROADMAP.a2ml` says "105". `docs/PROVER_COUNT.md` is canonical and these are owner-managed (R5a) — left untouched; recommend reconciling, starting with the repo description. - **Stale `estate-standardization-20260607` branch**: no PR, sits behind `main` at the same SHA as `chore/training-infrastructure-cleanups` — looks abandoned. - **`test-gpg-sign` + `test/ci-echidna-hypatia-fix`**: queued for deletion in #238 but the git proxy returns 403 on ref deletes and the GitHub MCP has no delete-branch tool — needs a one-line owner action. Draft until reviewed. https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv --- _Generated by [Claude Code](https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
diff --git a/.github/workflows/dogfood-proofs-ci.yml b/.github/workflows/dogfood-proofs-ci.yml
@@ -68,16 +68,37 @@ jobs:
     steps:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
-      - name: Install elan + Lean toolchain
+      - name: Install elan + pinned Lean toolchain
         run: |
           set -euo pipefail
-          # The toolchain version is pinned by proofs/lean/lean-toolchain; lake reads
-          # it and fetches that exact Lean on first invocation.
+          # elan-init installs the elan shim only (--default-toolchain none). We then
+          # pre-install the exact toolchain pinned by proofs/lean/lean-toolchain *here*,
+          # with retry/backoff, rather than letting `lake build` resolve it lazily:
+          # elan maps the pinned version against the GitHub releases API, which can
+          # transiently fail ("failed to parse latest release tag" — observed once on
+          # PR #234's pre-merge run; the post-merge run on main passed). Isolating and
+          # retrying that one network step keeps the Build step deterministic.
           curl -fsSL --retry 3 \
             https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
             -o /tmp/elan-init.sh
           sh /tmp/elan-init.sh -y --default-toolchain none
+          export PATH="$HOME/.elan/bin:$PATH"
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          toolchain="$(tr -d '[:space:]' < proofs/lean/lean-toolchain)"
+          for attempt in 1 2 3 4 5; do
+            if elan toolchain install "$toolchain"; then
+              break
+            fi
+            if [ "$attempt" -eq 5 ]; then
+              echo "elan toolchain install failed after 5 attempts" >&2
+              exit 1
+            fi
+            backoff=$((attempt * 5))
+            echo "elan toolchain install failed (attempt $attempt); retrying in ${backoff}s" >&2
+            sleep "$backoff"
+          done
+          elan default "$toolchain"
+          lean --version
 
       - name: Install just
         run: |
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
@@ -9,7 +9,7 @@ type = "state-file"
 [metadata]
 project = "echidna"
 version = "2.3.0"
-last-updated = "2026-06-02"
+last-updated = "2026-06-13"
 status = "active"
 release-tag = "v2.3.0"
 
@@ -18,6 +18,28 @@ name = "echidna"
 completion-percentage = 100
 phase = "v2.3.0 Released — saturation+typing (#198) + GNN training wiring (#207) + dispatcher all-17-adapters (PR pending SPDX hook) + comprehensive contractile family (#214) + first owner-authorised GNN training run completed (best MRR 0.92)"
 
+[session-2026-06-13-dogfood-proof-ci]
+summary = "Proof corpus repaired and gated in CI (PR #234, squash-merged to main 2026-06-06)"
+pr = "https://github.com/hyperpolymath/echidna/pull/234"
+tracker = "https://github.com/hyperpolymath/echidna/issues/238"
+changes = [
+  "proofs/{coq,lean,agda} + src/idris: every theorem now type-checks against real toolchains (Coq 8.18, Lean v4.13.0, Agda 2.6.3 + stdlib v1.7.3, Idris2 0.8.0)",
+  "New .github/workflows/dogfood-proofs-ci.yml — Coq + Lean + Agda jobs, each invoking a just proofs-* recipe so CI and local runs share one command surface (RSR-H14)",
+  "idris2-abi-ci.yml extended to type-check the src/idris validator (src/idris/** added to its triggers)",
+  "New Justfile recipes: proofs, proofs-coq, proofs-lean, proofs-agda, proofs-idris",
+]
+latent-bugs-fixed = [
+  "proofs/lean/lakefile.lean rooted only ECHIDNA, so lake build was silently broken (unknown module prefix); now every module is a root",
+  "src/idris/Validator.idr had no main though its ipkg declares an executable; added main = testValidation",
+]
+ci-environment-notes = [
+  "taiki-e/install-action reproducibly startup_failure'd in the new workflow even though mvp-smoke.yml uses the same pin on main; worked around with plain run: installs (apt + curl tarballs). Allowed-actions policy worth a look.",
+  "apt --fix-missing silently dropped agda-stdlib (exit 0, library unregistered); Agda now fetches stdlib v1.7.3 from GitHub deterministically.",
+  "Lean toolchain resolution via elan flaked once on the pre-merge ref ('failed to parse latest release tag', a GitHub releases-API hiccup); the post-merge run on main passed. Hardened by pre-installing the pinned toolchain with retry/backoff.",
+]
+gap-closed = "Before #234 the corpus had zero CI: agda-meta-checker.yml gated meta-checker/**, idris2-abi-ci.yml gated src/abi/**, and there was no Coq or Lean workflow at all, so a green PR proved nothing about proofs/."
+verification = "All proof jobs green end-to-end on PR #234 and on the post-merge push to main (Dogfood Proof Corpus run #11)."
+
 [session-2026-06-02]
 description = "Major wave: 20+ PRs across echidna+echidnabot+gitbot-fleet+hyperpolymath"
 notable-pr-merges = [
diff --git a/.machine_readable/ROADMAP.a2ml b/.machine_readable/ROADMAP.a2ml
@@ -7,10 +7,10 @@
 
 [metadata]
 version = "1.0.0"
-last-updated = "2026-04-25"
+last-updated = "2026-06-13"
 status = "Stage 1 active"
 maintainer = "Jonathan D.A. Jewell (hyperpolymath)"
-next-review = "2026-05-25"
+next-review = "2026-07-13"
 
 [vision]
 summary = """
@@ -61,7 +61,8 @@ prerequisites = [
   "✓ API surfaces: REST, GraphQL, gRPC (done 2026-04-10)",
   "✓ Bebop3 serialization (gRPC proto + axum, done 2026-04-15)",
   "✓ A2ML conformance (AGENTIC, NEUROSYM, done 2026-04-25)",
-  "⚠ Container isolation hardening (IN-PROGRESS; blocks production release)"
+  "⚠ Container isolation hardening (IN-PROGRESS; blocks production release)",
+  "✓ Dogfood proof corpus CI-gated — proofs/{coq,lean,agda} + src/idris type-check on every PR via dogfood-proofs-ci.yml + idris2-abi-ci.yml (done 2026-06-06, PR #234)"
 ]
 
 blockers = [
diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md
@@ -13,7 +13,11 @@ guardrail landed in two halves — R5a (prover-count drift, echidna‑local
 at `.github/canonical-references/` after PR #174 migration) and R5b
 (estate‑wide `Version: x.y.z` drift, in the standards reusable, consumed
 via PR #172). MVP smoke (#167) and the pareto/bare-build governance
-harness are green on `main`. None of these change the stage map below;
+harness are green on `main`. The dogfood proof corpus (`proofs/{coq,lean,agda}` + `src/idris`) is now
+CI-gated by `dogfood-proofs-ci.yml` (Coq/Lean/Agda) and `idris2-abi-ci.yml`
+(the `src/idris` validator), each driven by a `just proofs-*` recipe — closing
+a gap where the corpus had no CI and a green PR proved nothing about the
+proofs (PR #234). None of these change the stage map below;
 they are infrastructure around the work, not on the critical path.
 
 This document is the single source of truth for where ECHIDNA is going.
diff --git a/docs/wiki/Getting-Started.md b/docs/wiki/Getting-Started.md
@@ -41,6 +41,24 @@ just repl
 just verify examples/simple.v
 ```
 
+## Verify the dogfood proof corpus
+
+ECHIDNA dogfoods formal verification: its own trust-kernel proofs live under
+`proofs/` (Coq, Lean 4, Agda) and `src/idris`, and every one type-checks in CI
+(`dogfood-proofs-ci.yml` for Coq/Lean/Agda, `idris2-abi-ci.yml` for the Idris2
+ABI + validator). Run the same checks locally with the `just` recipes CI calls:
+
+```bash
+just proofs          # roll-up: Coq + Lean + Agda + Idris2
+just proofs-coq      # coqc over proofs/coq
+just proofs-lean     # lake build in proofs/lean (Lean toolchain pinned by lean-toolchain)
+just proofs-agda     # agda over proofs/agda (needs agda-stdlib registered)
+just proofs-idris    # idris2 --typecheck the src/idris validator
+```
+
+Toolchain versions match CI: Coq 8.18, Lean v4.13.0, Agda 2.6.3 with stdlib
+v1.7.3, and Idris2 0.8.0.
+
 ## Install prover backends
 
 The 12 core (Tier 1) backends need their binaries on PATH. See
diff --git a/docs/wiki/Home.md b/docs/wiki/Home.md
@@ -52,3 +52,5 @@ The 2026-06-01 **prover/corpus/vocab/synonyms/arbitration saturation campaign**
 - [`docs/architecture/VERISIM-ER-SCHEMA.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/architecture/VERISIM-ER-SCHEMA.md) — VeriSim ↔ ECHIDNA E-R schema (12 entities + 7 relationships, each with Rust struct + VeriSimDB table + Cap'n Proto schema + PK/FK).
 - [`docs/decisions/2026-06-01-saturation-campaign.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/decisions/2026-06-01-saturation-campaign.md) — ADR documenting the ordered marginal-benefit hierarchy and the decision to execute levers (1)–(6) and defer (7) GNN-training.
 - [`docs/handover/PROVER-CORPUS-SATURATION-LANE.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/handover/PROVER-CORPUS-SATURATION-LANE.md) — saturation lane handover with sibling-branch collision avoidance.
+
+The **dogfood proof corpus is now CI-gated**: every theorem under `proofs/{coq,lean,agda}` and the `src/idris` validator type-checks on each PR (`dogfood-proofs-ci.yml` + `idris2-abi-ci.yml`), each driven by a `just proofs-*` recipe — closing a gap where the corpus had no CI. Run it locally via `just proofs`; see [Getting Started](Getting-Started).
