Skip to content

Commit cced305

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
feat(saturation+typing): corpus 4→17, vocab 5→14+4, arbiters 1→4, exchange 2→6, 42-discipline embedding, E-R schema (#198)
## Summary Owner-directed marginal-benefit push across echidna's corpus / vocabulary / arbitration / exchange / wire-schema / type-discipline surfaces, plus the typing-embedding follow-up. Disjoint from sibling branch `wave3/161-162-bench-telemetry-corpus` (handover doc enumerates the hard exclusion list). All commits GPG-signed; 11-commit chain ending @ \`46f02b2\`. ## What landed **Corpus** — adapters 4 → **17** (4.25×). Added: isabelle, metamath, mizar, hol_light, hol4, dafny, why3, fstar, acl2_books, tptp, smtlib, proofnet, minif2f. All follow the agda.rs two-pass extraction pattern with \`AxiomUsage\` hazard surfacing. See [\`docs/CORPUS-ADAPTERS.md\`](docs/CORPUS-ADAPTERS.md). **Vocabulary** — per-prover synonym tables 5 → **14**, plus 4 cross-prover taxonomic dictionaries (underscore-prefix): - \`_msc2020.toml\` (87 codes) - \`_wordnet_math.toml\` (~80 lemmas) - \`_conceptnet_seed.toml\` (~55 edges, offline-resilient) - \`_disciplines.toml\` (42 TypeChecker disciplines) \`SynonymTable::load_all\` now iterates 14 provers; new \`CrossProverDicts\` + \`load_cross_prover_dicts\` + \`SynonymTable::merge_external\`. **Arbitration** — mechanisms 1 → **4**: Portfolio (existing) + \`BayesianArbiter\` (log-odds posterior + calibrated per-prover likelihoods + Shannon entropy) + \`DempsterShaferArbiter\` (belief-mass combination, HighConflict trip at k > 0.95) + \`ParetoArbiter\` (4-axis multi-objective frontier). **Exchange** — formats 2 → **6**: + TPTP / SMT-LIB / SMTCoq (stub bridge) / Lambdapi. Round-trip + cross-format translation where semantics overlap. **Wire schema** — aspirational text → **12 entities + 7 relationships** formally specified at [\`docs/architecture/VERISIM-ER-SCHEMA.md\`](docs/architecture/VERISIM-ER-SCHEMA.md) + Cap'n Proto schema [\`crates/echidna-wire/schemas/verisim_er.capnp\`](crates/echidna-wire/schemas/verisim_er.capnp) @0xe4dc7b1f01a06001. Crosswalk Rust struct ↔ Cap'n Proto ↔ ClickHouse table enumerated. **Type-discipline embedding (42 disciplines)** — pre-existing \`src/rust/disciplines/TypeDiscipline\` (41 variants) extended with owner-listed \`Ceremonial\` as the 42nd variant. New \`MarkerRegistry\` (138 canonical markers across all 42, per-adapter scoped) + \`detect_disciplines\` entry point. **Integrated into \`Corpus::reindex\`** so all 17 corpus adapters automatically tag every entry with detected disciplines via the existing \`reindex()\` calls. Storage: \`discipline:<tag>\` strings inside \`axiom_usage.other\` (zero serde break). Owner-listed 9 disciplines all covered: linear / affine / dependent / equality (via Refinement+Dependent markers) / ceremonial / dyadic / tropical / choreographic / epistemic. Full spec at [\`docs/architecture/TYPE-DISCIPLINE-EMBEDDING.md\`](docs/architecture/TYPE-DISCIPLINE-EMBEDDING.md) with TypeLL / Katagoria / VCL-UT / Panll crosswalk. **Multi-language integration**: - **Rust**: directly wired (all surfaces). - **Julia**: new \`src/julia/corpus_loader.jl\` + \`saturation_synonyms.jl\` with \`entry_disciplines()\` + \`discipline_feature_vector()\` helpers for GNN training feature engineering. \`run_training.jl\` / \`training/train.jl\` / \`training/dataloader.jl\` / \`models/neural_solver.jl\` deliberately NOT touched (wave3 + GNN-trigger ownership). - **Chapel**: hook spec at [\`docs/architecture/CHAPEL-SATURATION-HOOKS.md\`](docs/architecture/CHAPEL-SATURATION-HOOKS.md) — 3-hook integration (corpus goal injection / arbiter kind selection / cross-prover semantic dispatch) deferred to post-wave3 PR. **Documentation (humans + machines)**: - README.adoc, EXPLAINME.adoc, wiki Home/Architecture/Getting-Started/Guides/FAQ/Troubleshooting all reflect the new surface with file:line citations. - \`.machine_readable/6a2/{STATE,META,ECOSYSTEM,NEUROSYM}.a2ml\` updated additively. - CHANGELOG comprehensive Unreleased entry. - Saturation ADR at \`docs/decisions/2026-06-01-saturation-campaign.md\`. - Handover lane doc at \`docs/handover/PROVER-CORPUS-SATURATION-LANE.md\` (collision-avoidance with wave3). - **9 RSR-template substitution gaps closed** (CODE_OF_CONDUCT.md / SECURITY.md / AUTHORS.md placeholder emails + GitLab→GitHub prose + PGP fingerprint embedded). **Justfile recipes**: \`corpus-ingest-saturation\`, \`corpus-stats-all\`, \`synonym-load-test\`, \`test-saturation\`, \`arbiter-smoke\`, \`er-schema-drift-check\`. ## Test plan - [x] \`cargo check --lib\` clean (~5–24s) - [x] \`cargo test --lib -- corpus:: disciplines:: verification::{bayesian,dempster_shafer,pareto}_arbiter exchange::{tptp,smtlib,smtcoq,lambdapi} suggest::synonyms\` — **all passing**: 119 corpus+disciplines + 17 arbiter + 24 exchange + 6 synonyms = 166+ saturation-campaign tests green, 1 ignored heuristic-limit (\`corpus::dafny::tests::detects_datatype_and_extern\` — body-less extern-method limitation documented in CORPUS-ADAPTERS.md) - [x] Zero collisions with \`wave3/161-162-bench-telemetry-corpus\` — every commit in this branch touched only new files or surgical additive edits per the handover exclusion list - [x] All commits GPG-signed with \`4A03639C1EB1F86C7F0C97A91835A14A2867091E\` - [x] All new \`.rs\` files carry SPDX-FileCopyrightText for the owner per the pre-commit hook - [x] cargo check after Corpus::reindex extension: clean ## Commit chain \`f73ee00\` handover → \`46a7408\` corpus+synonyms+seeds → \`6019860\` arbiter trio → \`3828056\` E-R/CORPUS-ADAPTERS/ADR → \`d05dfff\` synonyms wiring → \`4a0b068\` Cap'n Proto → \`c61140c\` smtlib fix → \`85c1b8c\` test greenup → \`cb8caff\` template gaps → \`8b73c61\` doc sweep → \`46f02b2\` typing embedding. ## Deferred - **GNN first training run** — risks deleting wave3 baselines; infrastructure ready, needs owner trigger - 6 backlog corpus adapters (naproche / mathcomp / iris / cubical_agda / tlaps / pvs / naturalproofs / alphaproof) — marginal benefit now <10%, listed in CORPUS-ADAPTERS.md backlog - Chapel-side wiring of the 3 hooks — gated on wave3 merge - SMT portfolio expansion beyond Tier-1 default set 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 6fb5bd3 commit cced305

82 files changed

Lines changed: 20316 additions & 27 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.machine_readable/6a2/ECOSYSTEM.a2ml‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,3 +42,37 @@ url = "http://echidna-nesy.flycast:8090 (private 6PN — auto-wake via .flycast)
4242
health-endpoint = "/api/health"
4343
grace-period = "90s"
4444
cold-start-note = "Isabelle Main heap ~1-2GB maps at first use; Julia JIT runs on first inference. Minimum 90s grace."
45+
46+
# ─────────────────────────────────────────────────────────────────────────────
47+
# Saturation campaign 2026-06-01 — external corpus / vocab / exchange sources
48+
# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.md
49+
# ─────────────────────────────────────────────────────────────────────────────
50+
51+
[corpus-sources]
52+
lean_mathlib4 = "https://github.com/leanprover-community/mathlib4"
53+
isabelle_afp = "https://www.isa-afp.org/"
54+
metamath_setmm = "https://github.com/metamath/set.mm"
55+
mizar_mml = "http://mizar.org/version/8.1.14/mml/"
56+
hol_light = "https://github.com/jrh13/hol-light"
57+
hol4 = "https://github.com/HOL-Theorem-Prover/HOL"
58+
dafny_examples = "https://github.com/dafny-lang/dafny"
59+
why3_toccata = "https://gitlab.inria.fr/why3/why3"
60+
fstar_examples = "https://github.com/FStarLang/FStar"
61+
acl2_books = "https://github.com/acl2/acl2"
62+
tptp_problems = "https://tptp.org/"
63+
smtlib_benchmarks = "https://smt-lib.org/benchmarks.shtml"
64+
proofnet = "https://github.com/zhangir-azerbayev/ProofNet"
65+
minif2f = "https://github.com/openai/miniF2F"
66+
67+
[vocab-sources]
68+
msc2020 = "https://msc2020.org/"
69+
wordnet = "https://wordnet.princeton.edu/"
70+
conceptnet = "https://conceptnet.io/"
71+
72+
[proof-exchange-standards]
73+
tptp_iltp = "https://tptp.org/"
74+
smtlib_v2 = "https://smt-lib.org/"
75+
opentheory = "http://www.gilith.com/research/opentheory/"
76+
dedukti = "https://deducteam.github.io/"
77+
lambdapi = "https://github.com/Deducteam/lambdapi"
78+
smtcoq = "https://github.com/smtcoq/smtcoq"

‎.machine_readable/6a2/META.a2ml‎

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,3 +31,75 @@ secondary = ["Chapel", "Deno", "Guix", "Nix"]
3131
graphql = 8081
3232
grpc = 50051
3333
rest = 8000
34+
35+
# ─────────────────────────────────────────────────────────────────────────────
36+
# Saturation campaign 2026-06-01 — additive surface declaration
37+
# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.md
38+
# ─────────────────────────────────────────────────────────────────────────────
39+
40+
[saturation-campaign]
41+
design-principle = "Saturation campaign 2026-06-01 — push corpus/vocab/arbitration to marginal-benefit limit while preserving heuristic-adapter quality contract"
42+
43+
[saturation-campaign.new-modules]
44+
corpus = [
45+
"src/rust/corpus/isabelle.rs",
46+
"src/rust/corpus/metamath.rs",
47+
"src/rust/corpus/mizar.rs",
48+
"src/rust/corpus/hol_light.rs",
49+
"src/rust/corpus/hol4.rs",
50+
"src/rust/corpus/dafny.rs",
51+
"src/rust/corpus/why3.rs",
52+
"src/rust/corpus/fstar.rs",
53+
"src/rust/corpus/acl2_books.rs",
54+
"src/rust/corpus/tptp.rs",
55+
"src/rust/corpus/smtlib.rs",
56+
"src/rust/corpus/proofnet.rs",
57+
"src/rust/corpus/minif2f.rs",
58+
]
59+
verification = [
60+
"src/rust/verification/bayesian_arbiter.rs",
61+
"src/rust/verification/dempster_shafer.rs",
62+
"src/rust/verification/pareto_arbiter.rs",
63+
]
64+
exchange = [
65+
"src/rust/exchange/tptp.rs",
66+
"src/rust/exchange/smtlib.rs",
67+
"src/rust/exchange/smtcoq.rs",
68+
"src/rust/exchange/lambdapi.rs",
69+
]
70+
71+
[saturation-campaign.new-data]
72+
synonyms = [
73+
"data/synonyms/isabelle_afp.toml",
74+
"data/synonyms/metamath.toml",
75+
"data/synonyms/mizar.toml",
76+
"data/synonyms/hol_light.toml",
77+
"data/synonyms/hol4.toml",
78+
"data/synonyms/dafny.toml",
79+
"data/synonyms/why3.toml",
80+
"data/synonyms/fstar.toml",
81+
"data/synonyms/acl2.toml",
82+
"data/synonyms/_msc2020.toml",
83+
"data/synonyms/_wordnet_math.toml",
84+
"data/synonyms/_conceptnet_seed.toml",
85+
]
86+
87+
[saturation-campaign.new-docs]
88+
docs = [
89+
"docs/architecture/VERISIM-ER-SCHEMA.md",
90+
"docs/CORPUS-ADAPTERS.md",
91+
"docs/decisions/2026-06-01-saturation-campaign.md",
92+
"docs/handover/PROVER-CORPUS-SATURATION-LANE.md",
93+
]
94+
95+
[saturation-campaign.new-schemas]
96+
schemas = [
97+
"crates/echidna-wire/schemas/verisim_er.capnp",
98+
]
99+
100+
[saturation-campaign.testing]
101+
new-tests-passing = 139
102+
heuristic-limit-ignored = 1
103+
heuristic-limit-ignored-list = [
104+
"corpus::dafny::tests::detects_datatype_and_extern",
105+
]

‎.machine_readable/6a2/NEUROSYM.a2ml‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -243,3 +243,17 @@ report-format = "JSON (AssailReport)"
243243
proof-obligations-check = "panic-attack (code-only grep; no comments)"
244244
banned-patterns = ["believe-me", "unsafeCoerce", "Admitted", "sorry"]
245245
neurosym-rules-file = "standards-repo/neurosym-a2ml/hypatia-ruleset.json"
246+
247+
# === SATURATION CAMPAIGN 2026-06-01 — arbitration + cross-prover index ===
248+
# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.md
249+
# Additive — preserves all existing operation-definitions / type-system / hypatia-config keys.
250+
251+
[arbitration-extension]
252+
bayesian = "src/rust/verification/bayesian_arbiter.rs"
253+
dempster_shafer = "src/rust/verification/dempster_shafer.rs"
254+
pareto = "src/rust/verification/pareto_arbiter.rs"
255+
256+
[cross-prover-semantic-index]
257+
msc2020_codes_count = 87
258+
wordnet_lemmas_count = "~80"
259+
conceptnet_edges_count = "~55"

‎.machine_readable/6a2/STATE.a2ml‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1291,3 +1291,56 @@ not-done = [
12911291
"#77 CI-infra jam is estate-owned (active estate-wide remediation), not collapsible from this repo.",
12921292
"MSRV + Julia Integration remain red on main as separate non-required baseline rot — not in scope of #85; file dedicated issues only if they later become gating.",
12931293
]
1294+
1295+
# ═══════════════════════════════════════════════════════════════════════════════
1296+
# Saturation campaign 2026-06-01 — corpus / vocab / arbitration / exchange surface
1297+
# Additive snapshot of the surface delivered by branch prover-corpus-saturation.
1298+
# Existing prover_count / trust_pipeline / gnn_status fields preserved verbatim.
1299+
# ═══════════════════════════════════════════════════════════════════════════════
1300+
1301+
[saturation-surface]
1302+
last_revised = "2026-06-01"
1303+
1304+
corpus_adapters_count = 17 # was 4
1305+
corpus_adapters_list = [
1306+
"agda", "coq", "lean", "idris2",
1307+
"isabelle", "metamath", "mizar", "hol_light", "hol4",
1308+
"dafny", "why3", "fstar", "acl2_books",
1309+
"tptp", "smtlib", "proofnet", "minif2f",
1310+
]
1311+
1312+
synonym_tables_count = "14 per-prover + 3 cross-prover dictionaries"
1313+
synonym_tables_list = [
1314+
"agda", "coq", "lean4", "idris2",
1315+
"isabelle", "isabelle_afp", "metamath", "mizar",
1316+
"hol_light", "hol4", "dafny", "why3", "fstar", "acl2",
1317+
"_msc2020", "_wordnet_math", "_conceptnet_seed",
1318+
]
1319+
1320+
arbitration_mechanisms_count = 4 # was 1
1321+
arbitration_mechanisms_list = [
1322+
"portfolio (majority-vote)",
1323+
"bayesian",
1324+
"dempster_shafer",
1325+
"pareto",
1326+
]
1327+
1328+
exchange_bridges_count = 6 # was 2
1329+
exchange_bridges_list = [
1330+
"opentheory", "dedukti", "tptp", "smtlib", "smtcoq", "lambdapi",
1331+
]
1332+
1333+
er_schema_status = "formalised"
1334+
er_schema_doc_path = "docs/architecture/VERISIM-ER-SCHEMA.md"
1335+
er_schema_capnp_path = "crates/echidna-wire/schemas/verisim_er.capnp"
1336+
1337+
[saturation-campaign]
1338+
date = "2026-06-01"
1339+
branch = "prover-corpus-saturation"
1340+
status = "complete"
1341+
adr = "docs/decisions/2026-06-01-saturation-campaign.md"
1342+
handover = "docs/handover/PROVER-CORPUS-SATURATION-LANE.md"
1343+
commits = [
1344+
"f73ee00", "46a7408", "6019860", "3828056", "d05dfff",
1345+
"4a0b068", "c61140c", "85c1b8c", "cb8caff",
1346+
]

‎AUTHORS.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
<!--
2+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
23
SPDX-License-Identifier: MPL-2.0
34
SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
45
-->

‎CHANGELOG.md‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
2+
<!-- SPDX-License-Identifier: MPL-2.0 -->
13
# Changelog
24

35
All notable changes to ECHIDNA will be documented in this file.
@@ -7,6 +9,45 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
79

810
## [Unreleased]
911

12+
### Added — Saturation campaign 2026-06-01
13+
14+
Branch `prover-corpus-saturation` (commits f73ee00..cb8caff). Owner-directed marginal-benefit push across corpus, vocabulary, arbitration, exchange, and wire-schema surfaces. See `docs/decisions/2026-06-01-saturation-campaign.md`.
15+
16+
- **13 new corpus adapters** under `src/rust/corpus/` (`isabelle`, `metamath`, `mizar`, `hol_light`, `hol4`, `dafny`, `why3`, `fstar`, `acl2_books`, `tptp`, `smtlib`, `proofnet`, `minif2f`). Total corpus adapter coverage: 4 → **17** (4.25×). See `docs/CORPUS-ADAPTERS.md`.
17+
- **9 new per-prover synonym TOMLs** (`isabelle_afp`, `metamath`, `mizar`, `hol_light`, `hol4`, `dafny`, `why3`, `fstar`, `acl2`). Total: 5 → **14** per-prover tables.
18+
- **3 cross-prover taxonomic dictionaries** (underscore-prefix): `_msc2020.toml` (87 codes), `_wordnet_math.toml` (~80 lemmas), `_conceptnet_seed.toml` (~55 edges, offline-resilient).
19+
- **3 new arbitration mechanisms** under `src/rust/verification/`: `bayesian_arbiter` (log-odds posterior), `dempster_shafer` (HighConflict trip at k > 0.95), `pareto_arbiter` (4-axis Pareto frontier).
20+
- **4 new exchange bridges** under `src/rust/exchange/`: `tptp`, `smtlib`, `smtcoq` (stub bridge), `lambdapi`.
21+
- **Formal VeriSim E-R schema** at `docs/architecture/VERISIM-ER-SCHEMA.md` (12 entities + 7 relationships, crosswalk Rust↔Cap'n Proto↔ClickHouse) + Cap'n Proto wire schema `crates/echidna-wire/schemas/verisim_er.capnp` (@0xe4dc7b1f01a06001).
22+
- **Chapel + Julia integration hooks** at `docs/architecture/CHAPEL-SATURATION-HOOKS.md` + `docs/architecture/JULIA-SATURATION-HOOKS.md` (specifications only — wave3 chapel + GNN-training-trigger files deliberately untouched).
23+
- **New Julia helper modules** `src/julia/corpus_loader.jl` + `src/julia/saturation_synonyms.jl` (bridge Rust corpus JSON + saturation synonym TOMLs into the GNN training pipeline).
24+
- **Saturation campaign ADR** at `docs/decisions/2026-06-01-saturation-campaign.md`.
25+
- **Handover lane doc** at `docs/handover/PROVER-CORPUS-SATURATION-LANE.md` (collision-avoidance contract with `wave3/161-162-bench-telemetry-corpus`).
26+
- **Corpus adapter index** at `docs/CORPUS-ADAPTERS.md`.
27+
- **Justfile recipes**: `corpus-ingest-saturation`, `corpus-stats-all`, `synonym-load-test`, `test-saturation`, `arbiter-smoke`, `er-schema-drift-check`.
28+
- **139 new unit tests** across the saturation modules (1 ignored heuristic-limit).
29+
30+
### Changed
31+
32+
- `src/rust/suggest/synonyms.rs`: `load_all` extended to 14 provers; new `CrossProverDicts` + `load_cross_prover_dicts()` + `SynonymTable::merge_external()`.
33+
- `src/rust/corpus/mod.rs`, `verification/mod.rs`, `exchange/mod.rs`: register new modules (additive).
34+
- Module-level doc comments on `corpus/mod.rs`, `verification/mod.rs`, `verisim_bridge.rs` cite the new schemas + arbiters.
35+
36+
### Documentation
37+
38+
- Wiki updated (Home, Architecture, Getting-Started, Guides, FAQ, Troubleshooting) to reflect the new surface.
39+
- README.adoc + EXPLAINME.adoc updated with new headline counts + per-module references.
40+
- Machine-readable metadata under `.machine_readable/6a2/` (STATE / META / ECOSYSTEM / NEUROSYM) updated additively.
41+
- 9 RSR-template substitution gaps closed in CODE_OF_CONDUCT.md / SECURITY.md / AUTHORS.md.
42+
43+
### Verification
44+
45+
- `cargo check --lib` clean (~24s).
46+
- `cargo test --lib -- corpus:: verification::{bayesian,dempster_shafer,pareto}_arbiter exchange::{tptp,smtlib,smtcoq,lambdapi}`: **139 passed, 0 failed, 1 ignored** (corpus::dafny::tests::detects_datatype_and_extern — heuristic body-less-extern-method limitation).
47+
- Zero collisions with `wave3/161-162-bench-telemetry-corpus`.
48+
49+
---
50+
1051
## [2.3.0] - 2026-06-01
1152

1253
### Added

‎CODE_OF_CONDUCT.md‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
<!--
2+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
23
SPDX-License-Identifier: MPL-2.0
34
SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors
45
-->
@@ -45,7 +46,7 @@ Project maintainers have the right and responsibility to remove, edit, or reject
4546

4647
This Code of Conduct applies within all project spaces, including:
4748

48-
- GitLab repositories (code, issues, merge requests, wiki)
49+
- GitHub repository (code, issues, pull requests, wiki) and any mirror (e.g. GitLab CI mirror)
4950
- Project communication channels (mailing lists, chat, forums)
5051
- Official project events (conferences, meetups, workshops)
5152
- Social media when representing the project

‎EXPLAINME.adoc‎

Lines changed: 39 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,39 @@ ____
4040
* Integrity hashing: `src/rust/integrity/` (SHAKE3-512, BLAKE3).
4141
* Sandboxed execution: `src/rust/executor/` (Podman / bubblewrap /
4242
unsandboxed-with-opt-in).
43-
* Cross-prover exchange: `src/rust/exchange/` (OpenTheory + Dedukti).
43+
* Cross-prover exchange: `src/rust/exchange/` (OpenTheory, Dedukti,
44+
TPTP, SMT-LIB, SMTCoq, Lambdapi — six formats; see
45+
link:src/rust/exchange/mod.rs[`src/rust/exchange/mod.rs:11`]).
46+
* Arbitration: four mechanisms turn multi-prover outcomes into a
47+
single decision —
48+
link:src/rust/verification/portfolio.rs[`portfolio.rs`] (majority
49+
vote),
50+
link:src/rust/verification/bayesian_arbiter.rs[`bayesian_arbiter.rs`]
51+
(log-odds posterior),
52+
link:src/rust/verification/dempster_shafer.rs[`dempster_shafer.rs`]
53+
(mass-function combination with explicit ignorance), and
54+
link:src/rust/verification/pareto_arbiter.rs[`pareto_arbiter.rs`]
55+
(multi-objective dominance with tiebreak).
56+
* Corpus ingest: 17 adapters under
57+
link:src/rust/corpus/[`src/rust/corpus/`] cover 17 distinct proof
58+
languages — agda / coq / lean / idris2 (pre-2026-04) plus isabelle
59+
/ metamath / mizar / hol_light / hol4 / dafny / why3 / fstar /
60+
acl2_books / tptp / smtlib / proofnet / minif2f added in the
61+
2026-06-01 saturation campaign. Index:
62+
link:docs/CORPUS-ADAPTERS.md[`docs/CORPUS-ADAPTERS.md`].
63+
* Cross-prover vocabulary: per-prover synonym TOMLs under
64+
link:data/synonyms/[`data/synonyms/`] plus three taxonomic
65+
dictionaries — `_msc2020.toml` (87 MSC2020 codes),
66+
`_wordnet_math.toml` (~80 WordNet 3.1 math lemmas), and
67+
`_conceptnet_seed.toml` (~55 ConceptNet 5.7 edges) — used by the
68+
`echidna suggest` variant tester.
69+
* Shared data dictionary between echidna and its long-term memory
70+
store: the formal E-R schema at
71+
link:docs/architecture/VERISIM-ER-SCHEMA.md[`docs/architecture/VERISIM-ER-SCHEMA.md`]
72+
with Cap'n Proto wire format
73+
link:crates/echidna-wire/schemas/verisim_er.capnp[`crates/echidna-wire/schemas/verisim_er.capnp`].
74+
12 first-class entities + 7 first-class relationships, each with
75+
Rust struct + VeriSimDB table + Cap'n Proto schema + PK/FK set.
4476

4577
*Caveat*:
4678
"Operational" means `ProverBackend` trait-implemented and shells out
@@ -140,10 +172,14 @@ Rust trust-pipeline properties; see `proofs/agda/`.
140172
| Path | What's there
141173

142174
| `src/rust/provers/` | `ProverKind` enum + per-backend `ProverBackend` impls (see link:docs/PROVER_COUNT.md[`docs/PROVER_COUNT.md`] for the live tier table)
143-
| `src/rust/verification/` | Trust pipeline (portfolio, certificates, axioms, confidence, mutation, pareto, statistics)
175+
| `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`)
176+
| `src/rust/corpus/` | 17 corpus adapters (see link:docs/CORPUS-ADAPTERS.md[`docs/CORPUS-ADAPTERS.md`])
144177
| `src/rust/integrity/` | Solver-binary integrity (SHAKE3-512, BLAKE3)
145178
| `src/rust/executor/` | Sandboxed solver execution (Podman, bubblewrap)
146-
| `src/rust/exchange/` | Cross-prover proof exchange (OpenTheory, Dedukti)
179+
| `src/rust/exchange/` | Cross-prover proof exchange — six formats (OpenTheory, Dedukti, TPTP, SMT-LIB, SMTCoq, Lambdapi)
180+
| `data/synonyms/` | Per-prover synonym TOMLs + 3 cross-prover dictionaries (MSC2020, WordNet, ConceptNet); see link:data/synonyms/README.adoc[`data/synonyms/README.adoc`]
181+
| `docs/architecture/VERISIM-ER-SCHEMA.md` | Formal E-R schema — shared data dictionary echidna ↔ long-term memory store
182+
| `crates/echidna-wire/schemas/verisim_er.capnp` | Cap'n Proto wire format for the E-R schema
147183
| `src/rust/dispatch.rs` | Full trust-hardening dispatch pipeline
148184
| `src/rust/agent/` | Agentic proof search (actor model)
149185
| `src/rust/gnn/` | GNN integration (graph construction, embeddings, guided search)

‎Justfile‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -966,3 +966,60 @@ design-search problem="brouwer-leq" iterations="2000" top="10":
966966
# Run the parallel-swarm design-search
967967
design-swarm problem="brouwer-leq" agents="4" iterations="800":
968968
cargo run --bin echidna -- design swarm {{problem}} --agents {{agents}} --iterations {{iterations}} --broadcast-every 50
969+
970+
# ─────────────────────────────────────────────────────────────────────
971+
# Saturation campaign 2026-06-01 — recipes for the new corpus / vocab /
972+
# arbiter / exchange surface. See docs/decisions/2026-06-01-saturation-
973+
# campaign.md and docs/CORPUS-ADAPTERS.md.
974+
# ─────────────────────────────────────────────────────────────────────
975+
976+
# Ingest a project tree via one of the 13 new corpus adapters
977+
# (isabelle / metamath / mizar / hol_light / hol4 / dafny / why3 /
978+
# fstar / acl2_books / tptp / smtlib / proofnet / minif2f).
979+
corpus-ingest-saturation adapter root:
980+
cargo run --bin echidna -- corpus ingest --root {{root}} --adapter {{adapter}}
981+
982+
# Run the corpus-stats summary across all 17 adapter outputs found under
983+
# data/corpus/*.json (skips any missing without failing).
984+
corpus-stats-all:
985+
@for f in data/corpus/*.json; do \
986+
[ -f "$f" ] || continue; \
987+
echo "--- $f"; \
988+
cargo run --bin echidna --quiet -- corpus stats --index "$f" 2>/dev/null || echo " (skipped)"; \
989+
done
990+
991+
# Load every per-prover synonym TOML + the 3 cross-prover dictionaries
992+
# (_msc2020 / _wordnet_math / _conceptnet_seed) and report counts.
993+
synonym-load-test:
994+
cargo test --lib --quiet suggest::synonyms 2>&1 | tail -20
995+
996+
# Run the saturation-campaign cargo tests only (139 cases + 1 ignored).
997+
test-saturation:
998+
cargo test --lib -- \
999+
corpus:: \
1000+
verification::bayesian_arbiter \
1001+
verification::dempster_shafer \
1002+
verification::pareto_arbiter \
1003+
exchange::tptp \
1004+
exchange::smtlib \
1005+
exchange::smtcoq \
1006+
exchange::lambdapi \
1007+
suggest::synonyms
1008+
1009+
# Smoke-test the arbiter trio with synthetic evidence.
1010+
# Prints posterior verdict from each of: Bayesian, Dempster-Shafer, Pareto.
1011+
arbiter-smoke:
1012+
cargo run --bin echidna --quiet -- arbiter smoke 2>/dev/null || \
1013+
echo "(arbiter-smoke CLI not yet wired — see src/rust/verification/{bayesian,dempster_shafer,pareto}_arbiter.rs for unit-test entry points)"
1014+
1015+
# Validate that the E-R schema doc + Cap'n Proto schema are
1016+
# byte-identical with the recorded SHA in .machine_readable/er-schema.sha256.
1017+
# (CI gate planned — see docs/architecture/VERISIM-ER-SCHEMA.md
1018+
# "Drift detection".)
1019+
er-schema-drift-check:
1020+
@echo "Checking E-R schema drift..."
1021+
@sha256sum docs/architecture/VERISIM-ER-SCHEMA.md \
1022+
crates/echidna-wire/schemas/verisim_er.capnp \
1023+
| sha256sum | head -c 64
1024+
@echo " (current combined hash; compare against .machine_readable/er-schema.sha256 when CI gate lands)"
1025+

0 commit comments

Comments
 (0)