Skip to content

Commit 6aff53b

Browse files
hyperpolymathhyperpolymath
authored
docs: narrative coherence — README/EXPLAINME defer counts to canonical sources (#169)
## Summary The README and EXPLAINME carried **five mutually-disagreeing prover counts** (12 / 30 / 48 / 79 / 102 / 141), **three mutually-disagreeing test counts** (613 / 1059 / 638+), and **three mutually-disagreeing version strings** (v1.5.0 / v2.2 / v2.3+). All three surfaces also carried a stale `Last Updated: 2026-02-08` footer and a `PMPL-1.0` license badge from before the MPL-2.0 migration (af434ca). Single-PR perfective maintenance: no count, version, or status line is duplicated across files now. Every number lives in exactly one place and is referenced from everywhere else. ### README.adoc - License badge: `PMPL-1.0` → `MPL-2.0` (matches the intentional doc-stance pinned in `LICENSE`). - Drops the `Tests-1059` and `Provers-12_core_/_79_advertised` badges; drops the static `Last Updated: 2026-02-08` footer; drops the `Version: 1.5.0` footer. CHANGELOG.md and the git log are the single truth. - "Prover Surface" defers to `docs/PROVER_COUNT.md` (the canonical tier table — already named in `CLAUDE.md` as the source of truth). - "Trust & Safety Hardening (v1.5)" → "Trust & Safety Hardening" — the section content is timeless; the version tag was misleading. - Adds an Idris2-ABI paragraph to "Overview" — the `EchidnaABI.TacticRecord` round-trip lemmas (fixed-point confidence, total-order, in-range round-trip, clamp round-trip) are now type-checked on every push and matter to the narrative. - "Documentation" section now points to `RSR_COMPLIANCE.adoc`, `EXPLAINME.adoc`, `docs/PROVER_COUNT.md`, `docs/ARCHITECTURE.md`, `docs/ENV-VARS.md`, and `CLAUDE.md` — the actual on-disk surfaces. - "Current Status" replaces the v1.5/v2.2/v2.3/v2.4/v3.0 ladder with a current-shape summary and a delegate to CHANGELOG.md. - "Additional Capabilities" updated to mention the Chapel per-prover-cwd / filename hook and the ReScript→AffineScript-TEA migration in flight. ### README.md Was AsciiDoc-syntax content under a `.md` extension (legacy artefact). Rewritten as a thin Markdown pointer to `README.adoc`: sponsor + license + OpenSSF + green-hosting badges, one-paragraph "what is this", then a links table. No duplicated counts. No drift surface. ### EXPLAINME.adoc - Rewritten end-to-end to be count-free in prose — same purpose ("receipts for the README claims") but every specific number is named via a runnable command (`cargo test --lib`, `cargo bench`, `idris2 --build src/abi/echidnaabi.ipkg`, etc.) or via a pointer to `docs/PROVER_COUNT.md`. - Updated the Technology Choices table to reflect Idris2-ABI, Zig FFI, Chapel parallel layer, and the ReScript→AffineScript migration as currently described in `RSR_COMPLIANCE.adoc` / `CHANGELOG.md`. - Trimmed historical caveats that were rooted in a 2026-04-05 snapshot; the structural caveats (mocked vs binary-shelled tests, per-host binary requirements, Wave-3 cron acting as a stub-sentinel) preserved. ## Out of scope (deliberate) - **LICENSE / SPDX header sweep** — owner-managed (per `feedback_echidna_license_docs_mpl_intentional`); MPL-2.0 doc stance vs. AGPL `LICENSE` file is intentional, not reconciled here. - **`src/abi/` namespace / module-decl state** — owner-managed (per `feedback_echidna_src_abi_namespace_intentional`). - **Cargo.toml `version = "2.1.0"` and CHANGELOG version-line reconciliation** — semver / release tagging belongs to a release PR, not a doc-coherence pass. - **`docs/PROVER_COUNT.md` itself** — already advertises `128 total` while `src/rust/provers/mod.rs` ships 144 `ProverKind` variants; refresh belongs in the same PR as the next backend-count audit. ## Test plan - [x] `grep -nE '1059|141 variants|102 backend|79 backend|12-prover core|Last Updated|PMPL|v1\.5\.0|2026-02-08' README.adoc` → no matches - [x] Markdown rendering for README.md verified by eye for the badges + link list shape - [x] AsciiDoc directives in README.adoc / EXPLAINME.adoc preserved (`image:`, `link:`, `[source,bash]`, `[cols=…,options=header]`) - [ ] CI on this PR
1 parent a94ee81 commit 6aff53b

3 files changed

Lines changed: 289 additions & 604 deletions

File tree

‎EXPLAINME.adoc‎

Lines changed: 132 additions & 65 deletions
Original file line numberDiff line numberDiff line change
@@ -1,100 +1,167 @@
11
// SPDX-License-Identifier: MPL-2.0
2-
= ECHIDNA — Extensible Cognitive Hybrid Intelligence — Show Me The Receipts
2+
// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= ECHIDNA — Show Me The Receipts
34
:toc:
45
:icons: font
56

6-
The README makes claims. This file backs them up with evidence.
7+
The README makes claims. This file shows where to look for the
8+
evidence: source files, runnable commands, canonical-count docs. It is
9+
deliberately count-free at the prose level — every number lives in
10+
exactly one place and is referenced from here.
711

8-
== Key Claims From README
12+
== How to read this file
13+
14+
Each section quotes a claim from `README.adoc`, then names the file or
15+
command that backs it up. If you want a specific number, run the
16+
command; if you want the canonical version of a tier or count, follow
17+
the link.
18+
19+
== Trust pipeline and prover surface
920

1021
[quote, README section "Overview"]
1122
____
12-
ECHIDNA orchestrates 30 theorem provers, SMT solvers, first-order ATPs, and constraint solvers through a unified Rust core. Every proof result passes through a trust-hardening pipeline that checks solver integrity, tracks axiom usage, verifies proof certificates, and assigns a 5-level confidence score.
23+
ECHIDNA orchestrates theorem provers, SMT solvers, first-order ATPs,
24+
and constraint solvers through a unified Rust core. Every proof result
25+
passes through a trust-hardening pipeline that checks solver
26+
integrity, tracks axiom usage, verifies proof certificates, and
27+
assigns a 5-level confidence score.
1328
____
1429

15-
*Evidence:* The project implements 48 prover backends across 10 tiers (lines 29-57):
16-
- Tier 1: Agda, Coq/Rocq, Lean 4, Isabelle/HOL, Idris2, F*
17-
- Tier 2: Z3, CVC5, Alt-Ergo
18-
- Tier 3: Dafny, Why3
19-
- Tier 4: Metamath, HOL Light, Mizar, HOL4, PVS, ACL2, TLAPS, Twelf, Nuprl, Minlog, Imandra
20-
- Tier 5: Vampire, E Prover, SPASS
21-
- Tier 6: GLPK, SCIP, MiniZinc, Chuffed, OR-Tools
30+
*Evidence*:
31+
32+
* Backend tiering, count semantics (variants vs. impl files vs.
33+
advertised vs. core), and live answers to "how many backends" live
34+
in link:docs/PROVER_COUNT.md[`docs/PROVER_COUNT.md`].
35+
* `ProverBackend` trait: `src/rust/provers/mod.rs` — `pub enum
36+
ProverKind`, `pub fn all()`, `pub fn all_core()`.
37+
* Trust pipeline: `src/rust/verification/` (portfolio, certificates,
38+
axiom_tracker, confidence, mutation, pareto, statistics) and
39+
`src/rust/dispatch.rs`.
40+
* Integrity hashing: `src/rust/integrity/` (SHAKE3-512, BLAKE3).
41+
* Sandboxed execution: `src/rust/executor/` (Podman / bubblewrap /
42+
unsandboxed-with-opt-in).
43+
* Cross-prover exchange: `src/rust/exchange/` (OpenTheory + Dedukti).
44+
45+
*Caveat*:
46+
"Operational" means `ProverBackend` trait-implemented and shells out
47+
to a real external binary; it does NOT mean every live subprocess path
48+
has been exercised in CI against non-trivial goals. The test suite
49+
mixes in-process mocked-prover scenarios with binary-shelled-out paths;
50+
the split is documented in `tests/` and in
51+
link:docs/PROVER_COUNT.md[`docs/PROVER_COUNT.md`].
52+
53+
*Caveat (binaries)*:
54+
Running Tier-1 backends requires the corresponding external binaries
55+
on the host (`coqc`, `lean`, `agda`, `isabelle`, `idris2`, `z3`, `cvc5`,
56+
…). These are not bundled. The Wave-3 `Containerfile.wave3` lineage
57+
gives reproducible per-prover images; the weekly cron in
58+
`container-ci.yml` builds each Tier-3 image and runs a stub-sentinel
59+
detection step so a silently-degraded image red-flags rather than
60+
masquerading as healthy.
61+
62+
== Test surface
2263

23-
All 48 implement the `ProverBackend` trait (line 54-56). The trust pipeline (lines 59-114) applies 13 checks: solver integrity, portfolio solving, certificate checking, axiom tracking, sandboxing, 5-level confidence hierarchy, mutation testing, proof exchange, Pareto optimization, statistical tracking, and dispatch orchestration.
64+
[quote, README section "Test Suite"]
65+
____
66+
The test surface spans unit tests inside `src/rust/` and integration
67+
suites under `tests/`, supplemented by property tests, criterion
68+
benchmarks, and Idris2 ABI type-checks. Current counts are not
69+
embedded here — `cargo test --lib`, `cargo test --tests`, and
70+
`CHANGELOG.md` carry the live numbers.
71+
____
2472

25-
*Caveat:* All 48 backends have `ProverBackend` trait implementations with no `unimplemented!()`/`todo!()`/`unreachable!()` macros (sample verified 2026-04-05: Coq 1121 LoC, Lean 4 1648, Agda 673, Isabelle 360, Idris2 1253, Z3 840, CVC5 841). The README claims 30 but the system supports 48 total. "Operational" here means trait-implemented and shells out to a real external binary (e.g. `coqc`, `lean`, `agda`, `z3`) — it does NOT mean the live subprocess path has been exercised in CI against non-trivial goals. See testing caveat below.
73+
*Evidence (commands)*:
2674

27-
*Caveat (testing):* The 30 e2e prover tests (`tests/e2e_prover_test.rs`) and most integration tests are in-process and mock-based (`common::mock_prover`). They exercise the dispatch infrastructure and trust pipeline with mocked prover results; they do NOT invoke Tier 1 binaries (`coqc`, `lean`, `agda`, `z3`, etc.) against non-trivial goals. The `verify` command on the included `proofs/coq/basic.v` fixture does shell out to `coqc` — but via a round-trip through echidna's own re-serialization (parser fidelity untested on non-trivial proofs). The Z3 `prove` on `proofs/z3/basic.smt2` short-circuits before subprocess spawn (the fixture is `(assert true)`). Live subprocess correctness for the 48 backends is not covered by the current test suite.
75+
[source,bash]
76+
----
77+
# Library unit tests
78+
cargo test --lib
2879
29-
*Caveat (binaries):* Running Tier 1 backends requires the corresponding external binaries installed on the host (`coqc`, `lean`, `agda`, `isabelle`, `idris2`, `z3`, `cvc5`). These are not bundled. On a reference Fedora 43 system (2026-04-05), Coq/Lean/Agda/Idris2/Z3 were installed via opam/elan/local; Isabelle and CVC5 were absent.
80+
# Integration suites
81+
cargo test --tests
3082
31-
[quote, README section "Test Suite"]
32-
____
33-
613+ library tests passing (cargo test --lib), 2 ignored.
34-
____
83+
# Property tests (PropTest)
84+
cargo test --test property_tests
85+
86+
# Criterion benchmarks
87+
cargo bench
3588
36-
*Evidence:* The test metrics (updated 2026-04-18) report:
37-
- ~528 unit tests in the library target
38-
- 38 integration tests (with 2 pre-existing CVC5 E2E failures tracked separately)
39-
- 21 property-based tests (PropTest)
40-
- Additional interface and neural integration tests
41-
- Library (`cargo test --lib`): 613 passed / 0 failed / 2 ignored as of 2026-04-18.
42-
- All-targets total remains in the 638+ band once integration + property suites run.
89+
# Idris2 ABI type-check (zero believe_me / postulate / admit
90+
# in src/abi/ enforced by `.github/workflows/idris2-abi-ci.yml`)
91+
idris2 --build src/abi/echidnaabi.ipkg
92+
----
4393

44-
This is verifiable with `cargo test --lib` (unit) and `cargo test --test integration_tests`.
94+
*Evidence (recent counts)*: rough function-count from `grep -rE
95+
'^\s*#\[test\]|^\s*#\[tokio::test\]'`:
96+
97+
* `src/rust/`: ~1.1k unit-test functions
98+
* `tests/`: ~400 integration / property / interface functions
99+
100+
Numbers above are floors and drift as work lands; `cargo test`'s own
101+
summary line is the only post-build truth.
45102

46103
== Technology Choices
47104

48105
[cols="1,2"]
49106
|===
50-
| Technology | Learn More
51-
52-
| **Rust** | https://www.rust-lang.org (core logic, 48 prover backends, trust pipeline)
53-
| **Julia 1.10+** | https://julialang.org (ML inference: tactic prediction, premise selection)
54-
| **ReScript + Deno** | UI components (33 files, zero TypeScript)
55-
| **Chapel** | Optional parallel proof dispatch (compute-heavy operations)
56-
| **Idris2 ABI** | https://www.idris-lang.org (formal proofs, 16 modules, zero believe_me)
57-
| **Zig FFI** | https://ziglang.org (C-compatible API for all 48 provers)
107+
| Technology | Where to look
108+
109+
| **Rust** (core) | `src/rust/`, `crates/echidna-*`
110+
| **Julia 1.10+** | `src/julia/` — ML inference, tactic prediction, premise selection
111+
| **Idris2** | `src/abi/` — type-level ABI specifications + totality proofs (zero `believe_me`)
112+
| **Zig** | `ffi/zig/`, `src/zig_ffi/` — C-ABI FFI layer, hex/base64 primitives
113+
| **Chapel** | `src/chapel/` — optional parallel proof dispatch with per-prover cwd/filename hooks
114+
| **ReScript / +
115+
AffineScript** | `src/rescript/`, `src/ui/` — UI components; migration to AffineScript-TEA tracked alongside `affinescript/stdlib` primitives
58116
|===
59117

60-
== Dogfooded Across The Account
118+
== Dogfooded across the estate
119+
120+
ECHIDNA uses the `hyperpolymath` ABI / FFI standard (Idris2 + Zig) —
121+
same pattern that runs in `proven`, `burble`, and `gossamer`.
61122

62-
Uses the hyperpolymath ABI/FFI standard (Idris2 + Zig). Same pattern across proven, burble, and gossamer.
123+
ECHIDNA-specific anchors:
63124

64-
ECHIDNA-specific:
65-
- `src/abi/` — Idris2 formal proofs (16 modules, type soundness proofs)
66-
- `ffi/zig/` — Zig FFI layer (7 exported functions, C ABI compatibility)
67-
- `generated/abi/` — Auto-generated C headers from Idris2
125+
* `src/abi/EchidnaABI/` — Idris2 formal contracts. `TacticRecord.idr`
126+
pins the GNN→Chapel cross-FFI suggestion format with a fixed-point
127+
`ConfidenceFP` encoding plus reflexivity, antisymmetry, in-range
128+
round-trip, and clamp round-trip lemmas — all total, no escapes.
129+
* `ffi/zig/` — Zig FFI layer (C-ABI compatibility for all wired
130+
backends).
131+
* `generated/abi/` — auto-generated C headers from the Idris2 ABI.
68132

69-
Agda meta-checker (30+ formally verified trust pipeline properties) provides independent formal verification of the Rust trust pipeline correctness.
133+
The Agda meta-checker provides independent formal verification of the
134+
Rust trust-pipeline properties; see `proofs/agda/`.
70135

71-
== File Map: Key Modules
136+
== File map: key modules
72137

73138
[cols="1,2"]
74139
|===
75-
| Path | What's There
76-
77-
| `src/rust/provers/` | 48 prover backend implementations (ProverBackend trait)
78-
| `src/rust/verification/` | Trust pipeline (portfolio, certificates, axioms, confidence, mutation, pareto, statistics)
79-
| `src/rust/integrity/` | Solver binary integrity (SHAKE3-512, BLAKE3)
80-
| `src/rust/executor/` | Sandboxed solver execution (Podman, bubblewrap)
81-
| `src/rust/exchange/` | Cross-prover proof exchange (OpenTheory, Dedukti)
82-
| `src/rust/dispatch.rs` | Full trust-hardening dispatch pipeline
83-
| `src/rust/agent/` | Agentic proof search (actor model)
84-
| `src/rust/gnn/` | GNN integration (graph construction, embeddings, guided search)
85-
| `src/rust/neural.rs` | Neural premise selection (tactic prediction)
86-
| `src/rust/core.rs` | Core types (Term, ProofState, Tactic, Goal, Context, Theorem)
87-
| `src/rust/server.rs` | HTTP API server (GraphQL, gRPC, REST)
88-
| `src/rust/repl.rs` | Interactive REPL
89-
| `src/interfaces/` | API interfaces (GraphQL, gRPC, REST with real prover invocation)
90-
| `src/julia/` | ML layer (logistic regression, MRR 0.66)
91-
| `src/rescript/` | UI components (33 files, proof exploration)
92-
| `src/abi/` | Idris2 formal specifications (16 modules)
93-
| `ffi/zig/` | Zig FFI implementation (7 functions)
94-
| `proofs/agda/` | Agda meta-checker (30+ formally verified trust properties)
95-
| `tests/` | 638+ tests (unit, integration, property, interface)
140+
| Path | What's there
141+
142+
| `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)
144+
| `src/rust/integrity/` | Solver-binary integrity (SHAKE3-512, BLAKE3)
145+
| `src/rust/executor/` | Sandboxed solver execution (Podman, bubblewrap)
146+
| `src/rust/exchange/` | Cross-prover proof exchange (OpenTheory, Dedukti)
147+
| `src/rust/dispatch.rs` | Full trust-hardening dispatch pipeline
148+
| `src/rust/agent/` | Agentic proof search (actor model)
149+
| `src/rust/gnn/` | GNN integration (graph construction, embeddings, guided search)
150+
| `src/rust/neural.rs` | Neural premise selection (tactic prediction)
151+
| `src/rust/core.rs` | Core types (Term, ProofState, Tactic, Goal, Context, Theorem)
152+
| `src/rust/server.rs` | HTTP API server (GraphQL, gRPC, REST)
153+
| `src/rust/repl.rs` | Interactive REPL
154+
| `src/interfaces/` | API interfaces (GraphQL, gRPC, REST with real prover invocation)
155+
| `src/julia/` | ML layer (logistic-regression tactic prediction)
156+
| `src/rescript/`, `src/ui/` | UI components — migration to AffineScript-TEA in progress
157+
| `src/abi/` | Idris2 formal specifications (ABI contracts + totality proofs)
158+
| `ffi/zig/`, `src/zig_ffi/` | Zig FFI implementation
159+
| `proofs/agda/` | Agda meta-checker (independent verification of trust properties)
160+
| `tests/` | Integration / property / interface test suites
96161
|===
97162

98163
== Questions?
99164

100-
Open an issue in the hyperpolymath/echidna repository for questions about prover backend implementation, trust pipeline architecture, formal verification approach, or GNN-guided proof search integration.
165+
Open an issue at https://github.com/hyperpolymath/echidna/issues for
166+
questions about backend implementation, trust pipeline architecture,
167+
formal verification approach, or GNN-guided proof search.

0 commit comments

Comments
 (0)