hyperpolymath
diff --git a/‎CLAUDE.md‎
Lines changed: 74 additions & 121 deletions b/‎CLAUDE.md‎
Lines changed: 74 additions & 121 deletions
@@ -1,25 +1,28 @@
 # CLAUDE.md
 
-This document provides guidelines and context for working with Claude Code on the ECHIDNA project.
+Guidelines and context for working with Claude Code on the ECHIDNA project.
 
 ## Project Overview
 
-**ECHIDNA** (Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance) is a trust-hardened neurosymbolic theorem proving platform supporting 128 prover backends with a comprehensive verification pipeline.
+**ECHIDNA** (Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance) is a trust-hardened neurosymbolic theorem-proving platform with a polyglot backend surface and a comprehensive verification pipeline.
 
-**Repository**: https://github.com/hyperpolymath/echidna
-**Version**: 2.3.0 (see `CHANGELOG.md`; release-tag publication tracked in `docs/handover/TODO.md`)
-**License**: MPL-2.0
-**Architecture overview**: [`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md)
-**Canonical prover count**: [`docs/PROVER_COUNT.md`](docs/PROVER_COUNT.md) (128 total, 12 core)
-**Environment variables**: [`docs/ENV-VARS.md`](docs/ENV-VARS.md)
+- **Repository**: https://github.com/hyperpolymath/echidna
+- **Version + release history**: [`CHANGELOG.md`](CHANGELOG.md) (single source of truth; do not duplicate version strings elsewhere)
+- **License**: MPL-2.0
+- **Architecture overview**: [`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md)
+- **Canonical prover count + tier table**: [`docs/PROVER_COUNT.md`](docs/PROVER_COUNT.md)
+- **Environment variables**: [`docs/ENV-VARS.md`](docs/ENV-VARS.md)
+- **RSR / CCCP compliance statement**: [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc)
+- **Receipts for README claims**: [`EXPLAINME.adoc`](EXPLAINME.adoc)
+- **Contributor guide**: [`CONTRIBUTING.adoc`](CONTRIBUTING.adoc)
 
 ## Repository Structure
 
 ```
 echidna/
 ├── src/
-│   ├── rust/               # Rust core (128 provers, trust pipeline)
-│   │   ├── provers/        # 128 prover backend implementations
+│   ├── rust/               # Rust core + ProverKind enum + ProverFactory
+│   │   ├── provers/        # Per-backend ProverBackend impls (see docs/PROVER_COUNT.md for the tier table)
 │   │   ├── verification/   # Trust pipeline (portfolio, certificates, axioms, confidence, mutation, pareto, statistics)
 │   │   ├── integrity/      # Solver binary integrity (SHAKE3-512, BLAKE3)
 │   │   ├── executor/       # Sandboxed solver execution (Podman, bubblewrap)
@@ -40,13 +43,17 @@ echidna/
 │   │   ├── graphql/        # GraphQL (async-graphql, port 8081)
 │   │   ├── grpc/           # gRPC (tonic, port 50051)
 │   │   └── rest/           # REST (axum + OpenAPI, port 8000)
+│   ├── abi/                # Idris2 formal ABI (EchidnaABI.TacticRecord, …)
+│   ├── chapel/             # Optional parallel proof dispatch (--features chapel)
 │   ├── julia/              # Julia ML components
-│   └── rescript/           # ReScript UI (10 files — migration to AffineScript-TEA in progress)
-├── .machine_readable/      # A2ML metadata (STATE.a2ml, META.a2ml, ECOSYSTEM.a2ml, …)
-├── .github/workflows/      # 17 CI/CD workflows
+│   ├── rescript/, src/ui/  # UI — ReScript → AffineScript-TEA migration in flight
+│   └── zig_ffi/, ffi/zig/  # Zig FFI bridge (C-ABI surface for backends)
+├── .machine_readable/      # A2ML metadata, contractiles (MUST/ADJUST/TRUST/INTENT)
+├── .github/workflows/      # CI/CD workflows
+├── .containerization/      # Per-prover image tree (Containerfile.wave3)
 ├── Cargo.toml              # Rust workspace root
-├── Justfile                # Primary build system
-└── Containerfile           # Podman container
+├── Justfile                # Primary build system (RSR-H14)
+└── Containerfile           # Podman container (RSR-H15; do not use Dockerfile)
 ```
 
 ## Working with Claude Code
@@ -72,28 +79,26 @@ Follow conventional commit format:
 
 ### Tech Stack
 
-- **Rust**: Core logic, 128 prover backends, trust pipeline, CLI, REPL, API servers
-- **Julia**: ML inference (tactic prediction, premise selection, port 8090)
-- **AffineScript + Deno** (canonical; migration in progress from `src/rescript/`): UI served by Deno
-- **Chapel**: Optional parallel proof dispatch
+- **Rust**: Core logic, prover backends, trust pipeline, CLI, REPL, API servers
+- **Julia**: ML inference (tactic prediction, premise selection)
+- **Idris2**: Formal ABI specifications + totality proofs (`src/abi/`); zero `believe_me`, zero postulates, zero admits, enforced by `idris2-abi-ci.yml`
+- **Zig**: C-ABI FFI bridge (`ffi/zig/`, `src/zig_ffi/`)
+- **Chapel**: Optional parallel proof dispatch (`--features chapel`)
+- **AffineScript + Deno** (canonical UI target; ReScript components are being ported)
 
-### Prover Support (105 Total - ALL IMPLEMENTED)
+### Prover Support
 
-- **Interactive Proof Assistants**: Agda, Coq/Rocq, Lean 4, Isabelle/HOL, Idris2, F*
-- **SMT Solvers**: Z3, CVC5, Alt-Ergo
-- **Auto-Active Verifiers**: Dafny, Why3
-- **Specialised**: Metamath, HOL Light, Mizar, HOL4, PVS, ACL2, TLAPS, Twelf, Nuprl, Minlog, Imandra
-- **First-Order ATPs**: Vampire, E Prover, SPASS
-- **Constraint Solvers**: GLPK, SCIP, MiniZinc, Chuffed, OR-Tools
+Backend tiers, member lists, and the canonical answer to "how many provers?" all live in [`docs/PROVER_COUNT.md`](docs/PROVER_COUNT.md). The Tier-1 _core_ set is exposed by default through `GET /api/provers`; the rest are reachable via `ProverKind` and the dispatch pipeline. Do not duplicate counts in this file — they drift.
 
 ### Trust & Safety Pipeline
 
-The v1.5 trust hardening added:
+The trust-hardening pipeline applies the following checks before any proof result leaves the dispatcher:
+
 1. Solver binary integrity verification (SHAKE3-512 + BLAKE3)
 2. SMT portfolio solving / cross-checking
-3. Proof certificate checking (Alethe, DRAT/LRAT, TSTP)
+3. Proof certificate checking (Alethe, DRAT/LRAT, TSTP, Lean4 kernel, Coq kernel)
 4. Axiom usage tracking (4 danger levels: Safe, Noted, Warning, Reject)
-5. Solver sandboxing (Podman, bubblewrap, none)
+5. Solver sandboxing (Podman, bubblewrap, unsandboxed-with-explicit-opt-in)
 6. 5-level trust hierarchy for confidence scoring
 7. Mutation testing for specifications
 8. Prover dispatch pipeline
@@ -103,7 +108,7 @@ The v1.5 trust hardening added:
 
 ### Key Components
 
-- `src/rust/provers/mod.rs`: ProverBackend trait, ProverKind enum (128 variants), ProverFactory
+- `src/rust/provers/mod.rs`: `ProverBackend` trait, `ProverKind` enum, `ProverFactory`
 - `src/rust/dispatch.rs`: Full trust-hardening dispatch pipeline
 - `src/rust/verification/`: Portfolio, certificates, axiom tracker, confidence, mutation, pareto, statistics
 - `src/rust/integrity/`: Solver binary integrity (SHAKE3-512, BLAKE3)
@@ -112,113 +117,61 @@ The v1.5 trust hardening added:
 - `src/rust/core.rs`: Core types (Term, ProofState, Tactic, Goal, Context, Theorem)
 - `src/rust/gnn/`: GNN integration (graph construction, embeddings, inference client, guided search)
 - `src/rust/agent/`: Agentic proof search (actor model)
+- `src/abi/EchidnaABI/`: Idris2 ABI specifications + totality proofs (TacticRecord, AxiomTracker, Gnn, Provers, CapnSchemas)
 
 ### Current Status
 
-**Completed (v2.0.0)**:
-- 105/128 prover backends across 10 tiers
-- Trust & safety hardening (13 tasks complete)
-- 638+ tests passing (528 unit + 38 integration + 21 property + interface)
-- 3 API interfaces (GraphQL, gRPC, REST) with real prover backend invocation
-- Agda meta-checker: 30+ formally verified trust pipeline properties
-- Criterion benchmarks: 13 functions covering all critical paths
-- FFI bridge: complete C-compatible API for all 128 provers
-- Julia ML layer (logistic regression, MRR 0.66)
-- 26 CI/CD workflows (including Agda meta-checker)
-- Zig FFI layer (4 shared libraries)
-- Idris2 ABI formal proofs (16 modules, zero believe_me)
-- 0 clippy warnings, 0 compiler errors on stable Rust
-
-**v2.1 (GNN Integration)**:
-- GNN proof graph construction (7 node kinds, 8 edge kinds)
-- 32-dim local term embeddings + GNN inference client
-- GNN-guided proof search (hybrid GNN + symbolic scoring)
-- Julia /gnn/rank endpoint with cosine fallback
-- Idris2 formal proofs: 7 GNN properties (0 believe_me)
-- 28 new tests, 0 clippy warnings
-
-**Next (v2.2+)** (precise status):
-
-- **Chapel → Rust C FFI bridge (L2.1 + L2.2 done; L2.3+ gated)**. Zig shim
-  (`src/zig_ffi/`) and the rewritten Chapel metalayer (`src/chapel/`) sit
-  behind `--features chapel`. L2.1 is wired: `ChapelParallelSearch`
-  (`proof_search.rs`) is invoked by `dispatch.rs::verify_proof_parallel`
-  and reachable on the live `/api/verify_parallel` route, with graceful
-  sequential fallback. `just build-chapel-ffi && cargo build --features
-  chapel` builds and links standalone; `cargo test --features chapel`
-  passes including the chapel-gated `test_verify_proof_parallel_chapel_path`
-  (7/7). L2.2 lands 2026-05-30 with the #133 rehabilitation arc: the
-  `.chpl` sources now compile cleanly under chpl 2.3.0 / 2.8.0 (static
-  library — apt Chapel ships `CHPL_LIB_PIC=none` only, dynamic awaits
-  a PIC-runtime CI image), `chapel-ci.yml` chapel-build + zig-ffi are
-  strict (no continue-on-error), `just chapel-build` / `chapel-smoke` /
-  `chapel-test` recipes exist, and `parallelProofSearchSpeculative`
-  ships first-success-wins atomic-CAS semantics next to the existing
-  best-of `parallelProofSearch`. `proofs/agda/ParallelSoundness.agda`
-  formalises the aggregation invariants (soundness, completeness,
-  cancellation-safety) with zero postulate/admit/believe_me — see
-  `docs/decisions/2026-05-30-chapel-rehabilitation.md` for the rollout
-  decision. Build reproducibility was fixed 2026-05-18: `build.rs` now
-  `rerun-if-changed` on the built Zig artifact (was order-dependent on
-  recipe vs prior `cargo` run), and `build.zig` bundles compiler-rt (was
-  failing the non-Zig link with `undefined symbol: __zig_probe_stack`).
-  L2.3 (cancel-token through `tryProver` for mid-flight preemption) is
-  the next sub-wave; L2.4 mutation parallelism / L2.5 multi-locale /
-  L2.6 numeric hot paths / L2.7 bench remain hard-gated on L1 Cap'n
-  Proto and (for L2.5) a cluster runtime — see `docs/handover/TODO.md`.
-  Direct Rust↔Chapel goes through Zig (no shortcut path).
-
-- **Train GNN/Transformer on larger corpus (Flux.jl, scaffold-only)**.
-  Flux.jl is declared in `src/julia/Project.toml` and imported across
-  9 files; ~1.4k LoC of training scaffolds exist
-  (`train_advanced_models.jl`, `training/train.jl`,
-  `models/neural_solver.jl`). **Never invoked on real data**:
-  `models/neural/` does not exist, `models/model_metadata.txt` reads
-  `0 words, 0 classes`, and `src/julia/api/gnn_endpoint.jl:40-114`
-  falls back to cosine similarity when no trained model is found.
-  Corpus ready: `training_data/` 553 MB, 66,674 proofs / 179,933 tactics
-  across 16 prover systems — untouched.
-
-Note: Tamarin (`provers/tamarin.rs`, 596 LoC, 5 tests) and ProVerif
-(`provers/proverif.rs`, 800 LoC, 8 tests) were previously listed under
-v2.2+ as "bridge" work — in fact both are already shipped real backends
-inside the 105 prover count. Remaining Wave-3 work for these is corpus
-fixtures (`.spthy` / `.pv` samples) and CI provisioning of upstream
-binaries, tracked in `docs/handover/TODO.md`.
+The authoritative status surface is [`CHANGELOG.md`](CHANGELOG.md) (released versions) plus the git log + open issues (in-flight work). Do not duplicate version-keyed status here — it drifts.
+
+Shape, by area:
+
+- **Trust pipeline**: solver integrity, certificate checking, axiom tracking, sandboxing, mutation testing, Pareto ranking, Bayesian confidence — wired into `dispatch.rs`.
+- **Idris2 ABI**: `EchidnaABI.TacticRecord` (fixed-point confidence, total-order proofs, in-range round-trip lemmas) + sibling modules; type-checked on every push by `idris2-abi-ci.yml`.
+- **GNN integration**: graph construction (7 node kinds, 8 edge kinds), 32-dim local term embeddings, GNN inference client, hybrid GNN + symbolic scoring, Julia `/gnn/rank` with cosine fallback.
+- **Chapel parallel layer (`--features chapel`)**: `ChapelParallelSearch` invoked by `dispatch.rs::verify_proof_parallel`; per-prover cwd/filename hooks in `tryProver`; L2.3 cancel-token preemption shipped; `parallelProofSearchSpeculative` (first-success-wins atomic-CAS) alongside best-of `parallelProofSearch`; `proofs/agda/ParallelSoundness.agda` formalises soundness, completeness, and cancellation-safety with zero postulate / admit / believe_me. L2.4+ (mutation parallelism, multi-locale, numeric hot paths, bench) gated on L1 Cap'n Proto and (for L2.5) a cluster runtime — see [`docs/handover/TODO.md`](docs/handover/TODO.md).
+- **Wave-3 container infrastructure**: per-prover images in `.containerization/Containerfile.wave3`; weekly cron in `container-ci.yml` runs stub-sentinel detection across all 8 Tier-3 cells.
+- **Julia ML layer**: logistic-regression tactic prediction shipped; Flux.jl scaffolds for GNN/Transformer training present but not yet trained on real data — corpus ready under `training_data/`.
+- **Migrations in flight**: ReScript → AffineScript-TEA (UI); npm → Deno (`echidna-playground`); CI workflow consolidation under the governance ruleset.
 
 ## Useful Commands
 
 ```bash
-# Build System (Justfile is PRIMARY)
+# Build System (Justfile is PRIMARY — RSR-H14)
 just build              # Build the project
-just test               # Run tests (638+)
+just test               # Run tests
 just check              # Run all quality checkers
+just doctor             # Verify toolchain
+just heal               # Auto-install missing tools
+just tour               # Codebase tour
 
-# Cargo commands
+# Cargo
 cargo build             # Build Rust code
 cargo test              # Run all tests
-cargo test --lib        # Unit tests only (232)
-cargo test --test integration_tests  # Integration tests (38)
-
-# Container Management (Podman, not Docker)
-podman build -f Containerfile .   # Build container
-podman run echidna                # Run container
-
-# Quality Checks
-cargo clippy                      # Rust lints
-cargo fmt --check                 # Format check
+cargo test --lib        # Unit tests only
+cargo test --tests      # Integration suites
+cargo bench             # Criterion benchmarks
+cargo clippy            # Rust lints
+cargo fmt --check       # Format check
+
+# Idris2 ABI
+idris2 --build src/abi/echidnaabi.ipkg   # Type-check the ABI package
+
+# Container Management (Podman, not Docker — RSR-H15)
+podman build -f Containerfile .          # Minimal image
+podman run echidna                        # Run minimal image
+# Per-prover images live under .containerization/Containerfile.wave3
 ```
 
 ## Critical Constraints
 
-- **NO PYTHON** - use Julia for ML/data, Rust for systems, ReScript for apps
-- **RSR/CCCP Compliance Required** - follow Rhodium Standard Repository guidelines
-- **Justfile PRIMARY** - never use Make or other build systems
-- **Podman not Docker** - always use Podman for containers
-- **License**: MPL-2.0 (not AGPL, not dual MIT/Palimpsest)
-- **Author**: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+- **No Python** outside `salt/` (RSR-H4) — Julia for ML, Rust for systems, AffineScript/ReScript for UI.
+- **RSR / CCCP compliance** — see [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc) for the full hard-rule list and out-of-template adaptations.
+- **Justfile primary** (RSR-H14) — Just is the build entry point; no Make.
+- **Podman not Docker** (RSR-H15) — always Podman; `Containerfile` (not `Dockerfile`); `.containerization/Containerfile.wave3` for per-prover images.
+- **License**: MPL-2.0 across the documentation surface (intentional doc stance; see [`feedback_echidna_license_docs_mpl_intentional`](https://github.com/hyperpolymath/echidna/issues?q=license) — historical drift on individual files is owner-managed and not reconciled in routine PRs).
+- **Author**: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>.
 
 ---
 
-**Last Updated**: 2026-03-23
-**Maintained By**: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+**Maintained by**: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>.
+This file is kept count-free and date-free in prose; CHANGELOG.md and the git log carry the live timeline.