Skip to content

EXPLAINME.adoc

Latest commit

 

History

History
203 lines (170 loc) · 9.29 KB

EXPLAINME.adoc

File metadata and controls

203 lines (170 loc) · 9.29 KB
Raw

ECHIDNA — Show Me The Receipts

Table of Contents

The README makes claims. This file shows where to look for the evidence: source files, runnable commands, canonical-count docs. It is deliberately count-free at the prose level — every number lives in exactly one place and is referenced from here.

How to read this file

Each section quotes a claim from README.adoc, then names the file or command that backs it up. If you want a specific number, run the command; if you want the canonical version of a tier or count, follow the link.

Trust pipeline and prover surface

ECHIDNA orchestrates 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.

— README section "Overview"

Evidence:

  • Backend tiering, count semantics (variants vs. impl files vs. advertised vs. core), and live answers to "how many backends" live in docs/PROVER_COUNT.md.

  • ProverBackend trait: src/rust/provers/mod.rs — pub enum ProverKind, pub fn all(), pub fn all_core().

  • Trust pipeline: src/rust/verification/ (portfolio, certificates, axiom_tracker, confidence, mutation, pareto, statistics) and src/rust/dispatch.rs.

  • Integrity hashing: src/rust/integrity/ (SHAKE3-512, BLAKE3).

  • Sandboxed execution: src/rust/executor/ (Podman / bubblewrap / unsandboxed-with-opt-in).

  • Cross-prover exchange: src/rust/exchange/ (OpenTheory, Dedukti, TPTP, SMT-LIB, SMTCoq, Lambdapi — six formats; see src/rust/exchange/mod.rs:11).

  • Arbitration: four mechanisms turn multi-prover outcomes into a single decision — portfolio.rs (majority vote), bayesian_arbiter.rs (log-odds posterior), dempster_shafer.rs (mass-function combination with explicit ignorance), and pareto_arbiter.rs (multi-objective dominance with tiebreak).

  • Corpus ingest: 17 adapters under 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: docs/CORPUS-ADAPTERS.md.

  • Cross-prover vocabulary: per-prover synonym TOMLs under 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 echidna suggest variant tester.

  • Shared data dictionary between echidna and its long-term memory store: the formal E-R schema at docs/architecture/VERISIM-ER-SCHEMA.md with Cap’n Proto wire format crates/echidna-wire/schemas/verisim_er.capnp. 12 first-class entities + 7 first-class relationships, each with Rust struct + VeriSimDB table + Cap’n Proto schema + PK/FK set.

Caveat: "Operational" means ProverBackend trait-implemented and shells out to a real external binary; it does NOT mean every live subprocess path has been exercised in CI against non-trivial goals. The test suite mixes in-process mocked-prover scenarios with binary-shelled-out paths; the split is documented in tests/ and in docs/PROVER_COUNT.md.

Caveat (binaries): Running Tier-1 backends requires the corresponding external binaries on the host (coqc, lean, agda, isabelle, idris2, z3, cvc5, …). These are not bundled. The Wave-3 Containerfile.wave3 lineage gives reproducible per-prover images; the weekly cron in container-ci.yml builds each Tier-3 image and runs a stub-sentinel detection step so a silently-degraded image red-flags rather than masquerading as healthy.

Test surface

The test surface spans unit tests inside src/rust/ and integration suites under tests/, supplemented by property tests, criterion benchmarks, and Idris2 ABI type-checks. Current counts are not embedded here — cargo test --lib, cargo test --tests, and CHANGELOG.md carry the live numbers.

— README section "Test Suite"

Evidence (commands):

# Library unit tests
cargo test --lib

# Integration suites
cargo test --tests

# Property tests (PropTest)
cargo test --test property_tests

# Criterion benchmarks
cargo bench

# Idris2 ABI type-check (zero believe_me / postulate / admit
# in src/abi/ enforced by `.github/workflows/idris2-abi-ci.yml`)
idris2 --build src/abi/echidnaabi.ipkg

Evidence (recent counts): rough function-count from grep -rE '\s*\[test\]|\s*\[tokio::test\]':

  • src/rust/: ~1.1k unit-test functions

  • tests/: ~400 integration / property / interface functions

Numbers above are floors and drift as work lands; `cargo test’s own summary line is the only post-build truth.

Technology Choices

Technology Where to look

Rust (core)

src/rust/, crates/echidna-*

Julia 1.10+

src/julia/ — ML inference, tactic prediction, premise selection

Idris2

src/abi/ — type-level ABI specifications + totality proofs (zero believe_me)

Zig

ffi/zig/, src/zig_ffi/ — C-ABI FFI layer, hex/base64 primitives

Chapel

src/chapel/ — optional parallel proof dispatch with per-prover cwd/filename hooks

ReScript /
AffineScript

src/rescript/, src/ui/ — UI components; migration to AffineScript-TEA tracked alongside affinescript/stdlib primitives

Dogfooded across the estate

ECHIDNA uses the hyperpolymath ABI / FFI standard (Idris2 + Zig) — same pattern that runs in proven, burble, and gossamer.

ECHIDNA-specific anchors:

  • src/abi/EchidnaABI/ — Idris2 formal contracts. TacticRecord.idr pins the GNN→Chapel cross-FFI suggestion format with a fixed-point ConfidenceFP encoding plus reflexivity, antisymmetry, in-range round-trip, and clamp round-trip lemmas — all total, no escapes.

  • ffi/zig/ — Zig FFI layer (C-ABI compatibility for all wired backends).

  • generated/abi/ — auto-generated C headers from the Idris2 ABI.

The Agda meta-checker provides independent formal verification of the Rust trust-pipeline properties; see proofs/agda/.

File map: key modules

Path What’s there

src/rust/provers/

ProverKind enum + per-backend ProverBackend impls (see docs/PROVER_COUNT.md 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 docs/CORPUS-ADAPTERS.md)

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 data/synonyms/README.adoc

docs/architecture/VERISIM-ER-SCHEMA.md

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

src/rust/agent/

Agentic proof search (actor model)

src/rust/gnn/

GNN integration (graph construction, embeddings, guided search)

src/rust/neural.rs

Neural premise selection (tactic prediction)

src/rust/core.rs

Core types (Term, ProofState, Tactic, Goal, Context, Theorem)

src/rust/server.rs

HTTP API server (GraphQL, gRPC, REST)

src/rust/repl.rs

Interactive REPL

src/interfaces/

API interfaces (GraphQL, gRPC, REST with real prover invocation)

src/julia/

ML layer (logistic-regression tactic prediction)

src/rescript/, src/ui/

UI components — migration to AffineScript-TEA in progress

src/abi/

Idris2 formal specifications (ABI contracts + totality proofs)

ffi/zig/, src/zig_ffi/

Zig FFI implementation

proofs/agda/

Agda meta-checker (independent verification of trust properties)

tests/

Integration / property / interface test suites

Questions?

Open an issue at https://github.com/hyperpolymath/echidna/issues for questions about backend implementation, trust pipeline architecture, formal verification approach, or GNN-guided proof search.