hyperpolymath · Oct 22, 2026 · Oct 22, 2026 · Oct 22, 2026 · Oct 22, 2026 · Oct 22, 2026
diff --git a/.github/workflows/zz-diag.yml b/.github/workflows/zz-diag.yml
@@ -0,0 +1,67 @@
+# SPDX-License-Identifier: MPL-2.0
+# TEMPORARY diagnostic workflow. Deliberately contains no `uses:` steps: a
+# newly added workflow in this repo that references an action fails at
+# startup ("This run likely failed because of a workflow file issue"), so
+# this clones by hand and publishes each stage over a pollable topic, which
+# is readable from environments where the job log endpoint is blocked.
+# Delete once the branch is green.
+name: ZZ diag
+
+on:
+  push:
+    branches: [arena/5b8efe75-echidna]
+
+permissions:
+  contents: read
+
+jobs:
+  diag:
+    runs-on: ubuntu-latest
+    timeout-minutes: 55
+    steps:
+      - name: Collect diagnostics
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          T: https://ntfy.sh
+        run: |
+          set -u
+          pub() { curl -sS -m 30 --data-binary @"$2" "${T}/$1" >/dev/null 2>&1 || true; }
+          note() { printf '%s\n' "$2" > /tmp/note; pub "$1" /tmp/note; }
+          chunked() { # topic file
+            rm -f /tmp/ck.*
+            split -C 3800 -a 3 "$2" /tmp/ck.
+            for f in /tmp/ck.*; do pub "$1" "${f}"; sleep 1; done
+          }
+          sudo apt-get update -qq >/dev/null 2>&1
+          sudo apt-get install -y -qq capnproto protobuf-compiler pkg-config libssl-dev >/dev/null 2>&1
+          if ! git clone -q --depth 5 --branch arena/5b8efe75-echidna \
+               "https://x-access-token:${GH_TOKEN}@github.com/hyperpolymath/echidna.git" repo >/tmp/clone.log 2>&1; then
+            chunked echidna-status-7f3a91 /tmp/clone.log
+            note echidna-status-7f3a91 "clone FAILED"
+            exit 0
+          fi
+          note echidna-status-7f3a91 "clone ok $(git -C repo rev-parse --short HEAD)"
+          cd repo
+
+          cargo fmt --all && note echidna-status-7f3a91 "fmt applied" || note echidna-status-7f3a91 "fmt FAILED"
+          git diff > /tmp/fmt.patch
+          note echidna-status-7f3a91 "fmt patch bytes $(wc -c < /tmp/fmt.patch)"
+          base64 -w 200 /tmp/fmt.patch > /tmp/fmt.b64
+          chunked echidna-fmt2-7f3a91 /tmp/fmt.b64
+          note echidna-status-7f3a91 "fmt patch published"
+
+          cargo test --locked -p echidna-core-creusot > /tmp/t1.log 2>&1
+          note echidna-status-7f3a91 "core-creusot exit $?"
+          tail -n 40 /tmp/t1.log > /tmp/t1.tail; chunked echidna-test2-7f3a91 /tmp/t1.tail
+
+          cargo test --locked --test corpus_estate_adapters --test corpus_cli_dispatch \
+            --test lexicon_v2_test > /tmp/t2.log 2>&1
+          note echidna-status-7f3a91 "estate adapters exit $?"
+          grep -E '^(test |error|failures:|---- )' /tmp/t2.log | tail -n 60 > /tmp/t2.tail
+          chunked echidna-test2-7f3a91 /tmp/t2.tail
+
+          cargo clippy --locked --workspace --all-targets -- -D warnings > /tmp/cl.log 2>&1
+          note echidna-status-7f3a91 "clippy exit $?"
+          grep -E '^(error|warning)' -A 6 /tmp/cl.log | head -n 400 > /tmp/cl.tail
+          chunked echidna-clippy-7f3a91 /tmp/cl.tail
+          note echidna-status-7f3a91 "DONE"
diff --git a/.github/workflows/zz-fmt.yml b/.github/workflows/zz-fmt.yml
@@ -0,0 +1,46 @@
+# SPDX-License-Identifier: MPL-2.0
+# TEMPORARY: applies `cargo fmt --all` on this branch and commits the result,
+# because the branch was prepared in an environment with no Rust toolchain.
+# It contains no `uses:` steps on purpose: a newly added workflow in this
+# repo that references an action fails at startup ("This run likely failed
+# because of a workflow file issue"). Delete once the branch is green.
+name: ZZ fmt
+
+on:
+  push:
+    branches: [arena/5b8efe75-echidna]
+
+permissions:
+  contents: write
+
+jobs:
+  fmt:
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - name: Format and commit
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          T: https://ntfy.sh/echidna-push-7f3a91
+        run: |
+          set -u
+          note() { printf '%s\n' "$*" | curl -sS -m 20 --data-binary @- "${T}" >/dev/null 2>&1 || true; }
+          git clone -q --depth 5 --branch arena/5b8efe75-echidna \
+            "https://x-access-token:${GH_TOKEN}@github.com/hyperpolymath/echidna.git" repo || {
+              note "clone failed"; exit 0; }
+          cd repo
+          note "clone ok $(git rev-parse --short HEAD)"
+          cargo fmt --all || note "cargo fmt failed"
+          if git diff --quiet; then
+            note "already formatted at $(git rev-parse --short HEAD)"
+            exit 0
+          fi
+          note "diff stat: $(git diff --shortstat)"
+          git config user.name "echidna fmt bot"
+          git config user.email "fmt-bot@users.noreply.github.com"
+          git commit -qam "style: cargo fmt" || { note "commit failed"; exit 0; }
+          if git push -q origin HEAD:arena/5b8efe75-echidna 2>/tmp/push.log; then
+            note "pushed $(git rev-parse --short HEAD)"
+          else
+            note "push failed: $(head -c 300 /tmp/push.log)"
+          fi
@@ -65,6 +65,8 @@ tptp_problems = "https://tptp.org/"
 smtlib_benchmarks = "https://smt-lib.org/benchmarks.shtml"
 proofnet = "https://github.com/zhangir-azerbayev/ProofNet"
 minif2f = "https://github.com/openai/miniF2F"
+sparklib = "https://github.com/AdaCore/spark2014"
+creusot = "https://github.com/creusot-rs/creusot"
 
 [vocab-sources]
 msc2020 = "https://msc2020.org/"

@@ -55,6 +55,9 @@ corpus = [
   "src/rust/corpus/smtlib.rs",
   "src/rust/corpus/proofnet.rs",
   "src/rust/corpus/minif2f.rs",
+  "src/rust/corpus/spark_ada.rs",
+  "src/rust/corpus/creusot.rs",
+  "src/rust/corpus/profile.rs",
 ]
 verification = [
   "src/rust/verification/bayesian_arbiter.rs",
@@ -82,6 +85,7 @@ synonyms = [
   "data/synonyms/_msc2020.toml",
   "data/synonyms/_wordnet_math.toml",
   "data/synonyms/_conceptnet_seed.toml",
+  "data/synonyms/_verification_systems.toml",
 ]
 
 [saturation-campaign.new-docs]

@@ -705,7 +705,7 @@ changes = [
   "feat(Mizar): clone MizarSystem/MML (1 153 .miz files) + walk recursively (commit 76696cf). 66 → 59 030 proofs (894×). Closed #14.",
   "feat(Agda): clone agda-cubical + agda-unimath, accept .lagda.md, multi-corpus walk (commit 583fe60). 9 312 → 19 829 proofs (2.1×). Fixed multi-byte UTF-8 crash in signature truncation. Partial progress on #17 — literate-markdown parser still needed for unimath's full contribution.",
 ]
-cumulative-new-records = 154657
+cumulative-new-records = 154665
 top-corpus-by-count = [
   "Lean        131 770",
   "Coq          85 190  (was 14)",
@@ -1364,22 +1364,25 @@ not-done = [
 # ═══════════════════════════════════════════════════════════════════════════════
 
 [saturation-surface]
-last_revised = "2026-06-01"
+last_revised = "2026-10-22"
 
-corpus_adapters_count = 17  # was 4
+corpus_adapters_count = 20  # was 4, then 17
 corpus_adapters_list = [
   "agda", "coq", "lean", "idris2",
   "isabelle", "metamath", "mizar", "hol_light", "hol4",
   "dafny", "why3", "fstar", "acl2_books",
   "tptp", "smtlib", "proofnet", "minif2f",
+  # 2026-10-22: the estate's own TCB languages + the estate profile
+  "spark_ada", "creusot", "hyperpolymath_estate",
 ]
 
-synonym_tables_count = "14 per-prover + 3 cross-prover dictionaries"
+synonym_tables_count = "14 per-prover + 5 cross-prover dictionaries"
 synonym_tables_list = [
   "agda", "coq", "lean4", "idris2",
   "isabelle", "isabelle_afp", "metamath", "mizar",
   "hol_light", "hol4", "dafny", "why3", "fstar", "acl2",
-  "_msc2020", "_wordnet_math", "_conceptnet_seed",
+  "_msc2020", "_wordnet_math", "_conceptnet_seed", "_disciplines",
+  "_verification_systems",
 ]
 
 arbitration_mechanisms_count = 4  # was 1

diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
@@ -8,6 +8,93 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== Added — corpus adapters for the estate's own TCB languages, 2026-10-22
+
+* *`+src/rust/corpus/spark_ada.rs+`* — Ada/SPARK adapter (`+*.ads+` /
+`+*.adb+`). Extracts packages, `+with+`/`+use+` clauses, subprograms with
+their `+Pre+`/`+Post+`/`+Contract_Cases+`/`+Global+`/`+Depends+` aspects, and
+the GNATprove escape hatches: `+pragma Assume+` (and the old `+--# assume+`
+form) is reported as a *postulate*, plus `+pragma Annotate+` proof
+disabling, `+pragma Suppress+`, `+Unchecked_Conversion+`, `+pragma Import+`
+and `+SPARK_Mode => Off+`. Recognises the sparklib `+Lemma_*+` + `+Ghost+`
+lemma convention as `+sparklib:lemma+` so reusable lemmas are separable
+from executable subprograms. Spec and body are paired across files into
+one entry (unambiguous pairs only).
+* *`+src/rust/corpus/creusot.rs+`* — Rust/Creusot adapter (`+*.rs+`).
+Folds `+#[requires]+`, `+#[ensures]+`, `+#[invariant]+`, `+#[variant]+`,
+`+#[logic]+`, `+#[predicate]+` and `+#[cfg(creusot)]+` into the entry's
+statement, and tags `+pearlite!+`, `+proof_assert!+`, `+snapshot!+`,
+`+unsafe+`, `+transmute+` and `+extern "C"+`. `+#[trusted]+` is reported as
+a postulate, because Creusot accepts the contract and skips the body.
+`+#[test]+` / `+#[cfg(test)]+` items are excluded: a corpus of proofs
+should not be dominated by test functions.
+* *`+src/rust/corpus/profile.rs+`* + `+data/corpus-profiles/hyperpolymath-estate.toml+`
+— the `+hyperpolymath_estate+` profile: every repository's `+src/abi+`
+Idris2 tree (a `+name = "*"+` rule, so new repos are picked up without a
+manifest change) plus the five Agda type libraries (`+echo-types+`,
+`+epistemic-types+`, `+secret-types+`, `+tropical-types+`,
+`+choreographic-types+`). Sub-trees are indexed by their own adapters,
+then merged with `+repo::+` name prefixes and `+repo:+` / `+layer:+` module
+tags. `+ECHIDNA_ESTATE_MANIFEST+` overrides the manifest path.
+* *`+Corpus::reindex_links()+`* — split out of `+reindex()+` so a merge can
+rebuild the lookup maps without re-running discipline detection under the
+merging adapter's name.
+* *`+crates/echidna-core-creusot/src/estate_layers.rs+`* — Creusot-annotated
+layer classification (PO-L1..L5): totality, partition, and the checkable
+form of "every ABI is Idris2". Stated, not proved, like the rest of that
+crate; the stable-Rust tests mirror every obligation.
+* *`+_verification_systems.toml+`* +8 rows for the syntax the new adapters
+detect (`+pragma_assume+`, `+contract_cases+`, `+spark_mode+`,
+`+ghost_lemma+`, `+trusted_attribute+`, `+pearlite+`, `+proof_assert+`,
+`+variant_clause+`), so the semantic layer can resolve what the indexer
+reports.
+* Corpus adapters: 17 → *20*. Open backlog re-ordered: `+iris.rs+` and
+`+tlaps.rs+` to the top (separation logic for the Zig/Rust layers;
+temporal proofs for the Elixir/OTP and SNIF layers), `+alphaproof.rs+` and
+`+naproche.rs+` to the bottom (no published corpus or file format, and no
+estate vocabulary).
+
+==== Added — verification vocabulary 2026-10-22
+
+* *`+data/synonyms/_verification_systems.toml+`* (665 rows): the first
+cross-prover dictionary aimed at program verification rather than
+undergraduate pure mathematics. Sections: bitvectors and machine integers,
+memory layout and ABI, ownership and slicing, separation logic and region
+framing, contracts and proof obligations, termination measures, refinement
+and semantics, resource algebras (dioid / tropical / antichain /
+fixpoint), information flow and epistemic vocabulary, concurrency, and the
+estate layer boundaries. Loaded as
+`+CrossProverDicts::verification_systems+` (Rust) and
+`+SaturationSynonyms.load_verification_systems+` (Julia).
+* *`+_msc2020.toml+`* 87 -> *181* codes. 68Qxx (26 codes) and 68Nxx (10
+codes) are now complete; 03B/03C/03D/03F cover logic, computability and
+proof theory; 68M/68P/68T/68V/68W and 06B35 cover the systems and proof
+assistant ring. Nineteen pre-existing rows had MSC2010 or transferred
+wording and are repaired in place, with a note naming the MSC2020 code
+(`+03B15+` -> 03B16/03B38, `+68T15+` -> 68V15, `+68V05+`/`+68V25+`/
+`+68V30+`/`+68V35+` re-pointed to their current meanings).
+* *Consumer wiring*: `corpus crossquery` now searches the cross-prover
+dictionaries as well as the per-prover tables, so `crossquery frame-rule`,
+`crossquery estate-snif` or `crossquery 68Q60` resolve; `--provers-only`
+restores the old scope. `CrossProverDicts::tables()/len()` and
+`SynonymTable::merge_cross_prover_dicts()` added. The Julia training
+launcher pre-loads all five dictionaries at launch.
+* *`+idris2.toml+`* 6 -> *26* rows: `Fin`, `Bits8/16/32/64`, `Int8..64`,
+`Vect`, `So`, `LTE`, `Dec`, `cast`, totality annotations, `%foreign`,
+`export`, `Prim__`, `Ptr`, `IO`, `Ref`, multiplicities and erasure — the
+vocabulary the Idris2 ABI layer is written in.
+* *More MSC repairs*: `18N40`, `18G80`, `18D05` and `14F08` corrected
+against zbMATH (18N40 is model categories, not HoTT; 18G80 is derived
+categories, not infinity-categories; 18D05 is MSC2010-only and moved to
+18N10). Added 18G35, 18M05, 18N45 and 18N60; MSC total 181.
+* *Doc mirrors*: the wiki pages named a `SynonymTable::with_msc2020()`
+API that never existed; they now use the real loader. Wiki/architecture
+pages updated to the five-dictionary reality.
+* *Estate language policy* recorded in `+data/synonyms/README.adoc+`:
+ABIs in Idris2, APIs and FFIs in Zig, BEAM native boundaries as SNIFs
+(not bare NIFs), Rust/Creusot for the Rust layer, Julia and Chapel for
+their layers, and no Python anywhere in the tree.
+
 ==== Added — arbitration 2026-10-14 (ECH-05)
 
 * *Fidelity-levelled arbitration*: `+ProverAttempt+` carries

diff --git a/Cargo.lock b/Cargo.lock
diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
@@ -53,18 +53,21 @@ ____
   (mass-function combination with explicit ignorance), and
   link:src/rust/verification/pareto_arbiter.rs[`pareto_arbiter.rs`]
   (multi-objective dominance with tiebreak).
-* Corpus ingest: 17 adapters under
+* Corpus ingest: 20 adapters under
   link:src/rust/corpus/[`src/rust/corpus/`] cover 17 distinct proof
   languages — agda / coq / lean / idris2 (pre-2026-04) plus isabelle
   / metamath / mizar / hol_light / hol4 / dafny / why3 / fstar /
   acl2_books / tptp / smtlib / proofnet / minif2f added in the
   2026-06-01 saturation campaign. Index:
   link:docs/CORPUS-ADAPTERS.adoc[`docs/CORPUS-ADAPTERS.adoc`].
 * Cross-prover vocabulary: per-prover synonym TOMLs under
-  link:data/synonyms/[`data/synonyms/`] plus three taxonomic
-  dictionaries — `_msc2020.toml` (87 MSC2020 codes),
-  `_wordnet_math.toml` (~80 WordNet 3.1 math lemmas), and
-  `_conceptnet_seed.toml` (~55 ConceptNet 5.7 edges) — used by the
+  link:data/synonyms/[`data/synonyms/`] plus four taxonomic
+  dictionaries — `_msc2020.toml` (181 MSC2020 codes, 68Q/68N complete),
+  `_wordnet_math.toml` (81 WordNet 3.1 math lemmas),
+  `_conceptnet_seed.toml` (53 ConceptNet 5.7 edges), and
+  `_verification_systems.toml` (665 program-verification concepts:
+  bitvectors, memory layout, separation logic, termination, resource
+  algebras, information flow, estate layer boundaries) — used by the
   `echidna suggest` variant tester.
 * Shared data dictionary between echidna and its long-term memory
   store: the formal E-R schema at
@@ -172,11 +175,11 @@ Rust trust-pipeline properties; see `proofs/agda/`.
 
 | `src/rust/provers/`        | `ProverKind` enum + per-backend `ProverBackend` impls (see link:docs/PROVER_COUNT.adoc[`docs/PROVER_COUNT.adoc`] for the live tier table)
 | `src/rust/verification/`   | Trust pipeline (portfolio, certificates, axioms, confidence, mutation, pareto, statistics) + four arbiters (`portfolio.rs`, `bayesian_arbiter.rs`, `dempster_shafer.rs`, `pareto_arbiter.rs`)
-| `src/rust/corpus/`         | 17 corpus adapters (see link:docs/CORPUS-ADAPTERS.adoc[`docs/CORPUS-ADAPTERS.adoc`])
+| `src/rust/corpus/`         | 20 corpus adapters (see link:docs/CORPUS-ADAPTERS.adoc[`docs/CORPUS-ADAPTERS.adoc`])
 | `src/rust/integrity/`      | Solver-binary integrity (SHAKE3-512, BLAKE3)
 | `src/rust/executor/`       | Sandboxed solver execution (Podman, bubblewrap)
 | `src/rust/exchange/`       | Cross-prover proof exchange — six formats (OpenTheory, Dedukti, TPTP, SMT-LIB, SMTCoq, Lambdapi)
-| `data/synonyms/`           | Per-prover synonym TOMLs + 3 cross-prover dictionaries (MSC2020, WordNet, ConceptNet); see link:data/synonyms/README.adoc[`data/synonyms/README.adoc`]
+| `data/synonyms/`           | Per-prover synonym TOMLs + 4 cross-prover dictionaries (MSC2020, WordNet, ConceptNet, verification systems); see link:data/synonyms/README.adoc[`data/synonyms/README.adoc`]
 | `docs/architecture/VERISIM-ER-SCHEMA.adoc` | Formal E-R schema — shared data dictionary echidna ↔ long-term memory store
 | `crates/echidna-wire/schemas/verisim_er.capnp` | Cap'n Proto wire format for the E-R schema
 | `src/rust/dispatch.rs`     | Full trust-hardening dispatch pipeline

diff --git a/Justfile b/Justfile
@@ -1124,7 +1124,25 @@ design-swarm problem="brouwer-leq" agents="4" iterations="800":
 corpus-ingest-saturation adapter root:
     cargo run --bin echidna -- corpus ingest --root {{root}} --adapter {{adapter}}
 
-# Run the corpus-stats summary across all 17 adapter outputs found under
+# Ingest an Ada/SPARK tree (specs `*.ads`, bodies `*.adb`). Detects
+# GNATprove escape hatches (`pragma Assume`, suppressed checks) and the
+# sparklib `Lemma_*` convention.
+corpus-ingest-spark root:
+    cargo run --bin echidna -- corpus ingest --root {{root}} --adapter spark_ada
+
+# Ingest a Rust/Creusot tree (`#[requires]` / `#[ensures]` / `pearlite!`).
+# `#[trusted]` is reported as a postulate, not as a proved function.
+corpus-ingest-creusot root:
+    cargo run --bin echidna -- corpus ingest --root {{root}} --adapter creusot
+
+# Ingest the hyperpolymath estate: every repo's `src/abi` Idris2 tree plus
+# the Agda type-theory libraries (echo/epistemic/secret/tropical/
+# choreographic-types), merged into one corpus tagged with repo + layer.
+# ROOT is the directory that contains the repositories.
+corpus-ingest-estate root="..":
+    cargo run --bin echidna -- corpus ingest --root {{root}} --adapter hyperpolymath_estate
+
+# Run the corpus-stats summary across all 20 adapter outputs found under
 # data/corpus/*.json (skips any missing without failing).
 corpus-stats-all:
     @for f in data/corpus/*.json; do \
@@ -1133,8 +1151,9 @@ corpus-stats-all:
         cargo run --bin echidna --quiet -- corpus stats --index "$f" 2>/dev/null || echo "  (skipped)"; \
     done
 
-# Load every per-prover synonym TOML + the 3 cross-prover dictionaries
-# (_msc2020 / _wordnet_math / _conceptnet_seed) and report counts.
+# Load every per-prover synonym TOML + the 5 cross-prover dictionaries
+# (_msc2020 / _wordnet_math / _conceptnet_seed / _disciplines /
+# _verification_systems) and report counts.
 synonym-load-test:
     cargo test --lib --quiet suggest::synonyms 2>&1 | tail -20