Skip to content

Commit 6c52e7f

Browse files
claudeclaude
committed
docs: add canonical human-readable ARCHITECTURE.md
Closes Audit-A new-doc gap #1: TOPOLOGY.md and STATE-VISUALIZER.adoc were stale duplicates trying to be the architecture overview, both were deleted in the version-archaeology pass. This file fills the gap with a current component map, trust-pipeline walkthrough, and polyglot source layout. https://claude.ai/code/session_01YPqu7gti4azBach6ZvpRFJ
1 parent b22ce8e commit 6c52e7f

1 file changed

Lines changed: 160 additions & 0 deletions

File tree

‎docs/ARCHITECTURE.md‎

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
1+
<!-- SPDX-License-Identifier: MPL-2.0 -->
2+
<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
3+
4+
# ECHIDNA Architecture
5+
6+
**Status**: canonical human-readable overview. Lives alongside the machine-readable
7+
[`.machine_readable/6a2/META.a2ml`](../.machine_readable/6a2/META.a2ml) (architecture
8+
decisions) and [`STATE.a2ml`](../.machine_readable/6a2/STATE.a2ml) (current state).
9+
Last revised: 2026-05-26.
10+
11+
ECHIDNA — Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance —
12+
is the reasoning substrate of the hyperpolymath ecosystem. Two non-negotiable
13+
invariants govern every design choice:
14+
15+
1. **ML suggests; provers verify.** Neural components rank, route, and propose;
16+
formal provers carry the trust. A wrong suggestion is a wasted CPU cycle,
17+
not a wrong proof.
18+
2. **Trust is checked, not asserted.** Solver binaries are SHAKE3-512 / BLAKE3
19+
integrity-checked before invocation; certificates are independently
20+
reproduced where formats allow (Alethe, DRAT/LRAT, TSTP).
21+
22+
## Component map
23+
24+
```
25+
┌─────────────────────────────────────────────────────────────────────────┐
26+
│ UI Layer │
27+
│ AffineScript-TEA (migrating from src/rescript/), served by Deno │
28+
└──────────────────────────────┬──────────────────────────────────────────┘
29+
│ HTTP / WebSocket (Cap'n Proto, planned L1)
30+
┌──────────────────────────────▼──────────────────────────────────────────┐
31+
│ Rust Core (src/rust/, crates/) │
32+
│ │
33+
│ ┌──────────┐ ┌──────────────┐ ┌────────────────┐ ┌──────────────┐ │
34+
│ │ CLI/REPL │ │ REST / GraphQL│ │ gRPC │ │ FFI (Zig) │ │
35+
│ │ (main.rs)│ │ (axum :8000) │ │ (tonic :50051)│ │ (16 exports) │ │
36+
│ └────┬─────┘ └──────┬────────┘ └──────┬────────┘ └──────┬───────┘ │
37+
│ └────────────────┴──────────────────┴────────────────┘ │
38+
│ │ │
39+
│ ▼ │
40+
│ ┌──────────────────────────────────────┐ │
41+
│ │ ProverDispatcher (dispatch.rs) │ │
42+
│ │ — selects backend, owns trust loop │ │
43+
│ └──┬───────────────────────────────┬───┘ │
44+
│ │ │ │
45+
│ ┌─────────────▼────────────┐ ┌─────────────▼───────────────────┐ │
46+
│ │ Trust pipeline │ │ 128 ProverKind backends │ │
47+
│ │ (verification/) │ │ (provers/) │ │
48+
│ │ - integrity │ │ 89 external prover bindings │ │
49+
│ │ - portfolio │ │ 39 TypeChecker disciplines │ │
50+
│ │ - certificates │ │ via TypedWasm Sigma │ │
51+
│ │ - axiom tracker │ │ │ │
52+
│ │ - confidence │ │ Tier 1: 12 core (REST default) │ │
53+
│ │ - mutation │ │ Tier 2–10: by capability │ │
54+
│ │ - pareto │ └──────────────────────────────────┘ │
55+
│ │ - statistics │ │
56+
│ └───────────────────────────┘ │
57+
│ │
58+
│ ┌────────────────────────┐ ┌────────────────────────┐ │
59+
│ │ Agentic search │ │ GNN client │ │
60+
│ │ (agent/, actor model) │───►│ (gnn/client.rs) │ │
61+
│ └────────────────────────┘ └─────────┬──────────────┘ │
62+
└─────────────────────────────────────────────┼────────────────────────────┘
63+
│ POST /gnn/rank
64+
│ POST /training/update
65+
│ POST /gnn/health
66+
┌───────────────────────────▼───────────────────────────┐
67+
│ Julia ML sidecar (src/julia/) — port 8090 │
68+
│ api/server.jl (canonical entry) │
69+
│ - load_gnn_model → models/neural/gnn_ranker │
70+
│ - PROVER_DOMAIN_WEIGHTS (online from /training/update)│
71+
│ - cosine fallback (model_loaded == false) │
72+
└───────────────────────┬───────────────────────────────┘
73+
│
74+
▼
75+
VeriSimDB
76+
(cross-repo; verisim REST :8080)
77+
historical proof_attempts table,
78+
mv_prover_success_by_class
79+
```
80+
81+
## Tier overview
82+
83+
ECHIDNA carries **128 ProverKind variants**. The exposed surface depends on tier:
84+
85+
- **Tier 1 (12 core)** — the default REST `/api/verify` surface: Coq/Rocq, Lean 4,
86+
Agda, Isabelle/HOL, Idris 2, F*, Z3, CVC5, Alt-Ergo, Dafny, Vampire, E Prover.
87+
- **Tier 2–10** — 116 additional backends: ATPs, SMT, model checkers, constraint
88+
solvers, niche provers, ecosystem type-checkers. Available via explicit
89+
`ProverKind` selection in CLI / REPL / GraphQL but not auto-routed.
90+
91+
See [`PROVER_COUNT.md`](PROVER_COUNT.md) for the canonical tier table and
92+
per-prover capabilities.
93+
94+
## Trust pipeline walkthrough
95+
96+
Each `verify_proof` call passes through (under `--features verisim`, eventually
97+
in default builds; see [`handover/TODO.md`](handover/TODO.md) for current state):
98+
99+
1. **Integrity** (`integrity/`) — solver binary SHAKE3-512 + BLAKE3 against
100+
`config/solver-manifest.toml`.
101+
2. **Dispatch** (`dispatch.rs`) — `ProverDispatcher::select_prover` picks the
102+
backend; under `with_verisim`, `VeriSimAdvisor` queries
103+
`mv_prover_success_by_class` for historical success-rate hints.
104+
3. **Sandbox** (`executor/`) — Podman or bubblewrap process containment.
105+
4. **Portfolio cross-check** (`verification/portfolio.rs`) — for SMT, run two
106+
independent solvers; ✓ if both agree.
107+
5. **Certificate verification** (`verification/certificates.rs`) — replay
108+
Alethe / DRAT-LRAT / TSTP independently of the originating solver.
109+
6. **Axiom tracking** (`verification/axiom_tracker.rs`) — 4 danger levels
110+
(Safe, Noted, Warning, Reject).
111+
7. **Confidence** (`verification/confidence.rs`) — 5-tier Bayesian trust score.
112+
8. **Mutation testing** (`verification/mutation.rs`) — for specifications.
113+
9. **Pareto** (`verification/pareto.rs`) — multi-objective frontier across
114+
speed / trust / certificate availability.
115+
10. **Statistics** (`verification/statistics.rs`) — per-(prover, domain) success
116+
rates; exported to `/training/update` for online ML weight updates.
117+
11. **Outcome emission** (`dispatch.rs::spawn_record_attempt`, gated on
118+
`with_verisim_writer`) — fire-and-forget write to VeriSimDB
119+
`proof_attempts`, closes the learning loop.
120+
121+
## Polyglot source layout
122+
123+
`src/` holds one subdirectory per language. The split is intentional — see
124+
[`RSR_COMPLIANCE.adoc`](../RSR_COMPLIANCE.adoc) §"Out-of-template adaptations".
125+
126+
| Path | Language | Role |
127+
|---|---|---|
128+
| `src/rust/` | Rust | Core: backends, dispatch, trust pipeline, CLI, REPL, server |
129+
| `crates/` | Rust | Extracted workspace members (`echidna-core`, `-mcp`, `-wire`, `-core-spark`, `typed_wasm`) |
130+
| `src/julia/` | Julia | ML sidecar (GNN, logistic regression, training, eval) |
131+
| `src/abi/` | Idris 2 | Formal ABI proofs (16 modules, zero `believe_me`) |
132+
| `src/idris/` | Idris 2 | UI validator |
133+
| `src/chapel/` | Chapel | Parallel proof search (L2.1 live; L2.2+ gated) |
134+
| `src/zig_ffi/` | Zig | Chapel-bridge FFI shim |
135+
| `ffi/zig/` | Zig | Overlay / tentacles / boj sources |
136+
| `src/ada/` | Ada + SPARK | Formal companion library |
137+
| `src/rescript/` | ReScript → AffineScript | UI (migration in progress) |
138+
| `src/ui/` | static assets | Public UI files |
139+
| `src/interfaces/` | Rust | GraphQL, gRPC, REST workspace crates |
140+
141+
## Internal IPC
142+
143+
Today: HTTP + JSON between Rust core and Julia sidecar on port 8090.
144+
Endpoints — `POST /gnn/rank`, `POST /gnn/embed`, `POST /training/update`,
145+
`POST /gnn/health`, plus `POST /reload` (planned port from the orphaned
146+
`api_server.jl`).
147+
148+
Planned (Stage 5a / L1): Cap'n Proto over Unix domain socket; HTTP+JSON
149+
retained only as debug fallback. See [`docs/handover/L1-CAPNPROTO-PROMPT.md`](handover/L1-CAPNPROTO-PROMPT.md).
150+
151+
## Where to go next
152+
153+
- [`docs/ROADMAP.md`](ROADMAP.md) — canonical stage map and sprint targets.
154+
- [`docs/handover/STATE.md`](handover/STATE.md) — running session log.
155+
- [`docs/handover/HANDOVER-INDEX.md`](handover/HANDOVER-INDEX.md) — guide to the
156+
handover/ prompt suite.
157+
- [`docs/ENV-VARS.md`](ENV-VARS.md) — every environment variable the system
158+
reads, with defaults.
159+
- [`docs/PROVER_COUNT.md`](PROVER_COUNT.md) — canonical tier table.
160+
- [`.machine_readable/6a2/STATE.a2ml`](../.machine_readable/6a2/STATE.a2ml) — machine-readable state, regenerated each sprint.

0 commit comments

Comments
 (0)