feat: add GNN integration for proof search guidance (v2.1.0)

Implement Graph Neural Network integration across Rust core, Julia ML
server, and Idris2 ABI. The GNN module enables neural-guided proof
search by converting proof states into typed directed graphs, computing
local embeddings, and ranking premises via GNN inference.

Rust GNN module (src/rust/gnn/):
- graph.rs: ProofGraphBuilder with 7 node kinds, 8 edge kinds, recursive
  term expansion, constant deduplication, shared-structure detection
- embeddings.rs: 32-dim feature vectors with node/term kind one-hot,
  symbol frequency, structural complexity; cosine similarity
- client.rs: HTTP client for Julia GNN server with graceful degradation
- guided_search.rs: hybrid GNN+symbolic scoring (70/30 default weights),
  tactic inference, embedding cache, search statistics

Julia GNN endpoint (src/julia/api/gnn_endpoint.jl):
- POST /gnn/rank with sparse graph parsing and cosine fallback
- GET /gnn/health for model availability checks

Idris2 formal proofs (src/abi/EchidnaABI/Gnn.idr):
- 7 proven properties: feature dim positivity, adjacency consistency,
  node/edge kind injectivity, depth monotonicity, DependsOn/UsefulFor
  duality, combined score boundedness
- 0 believe_me, 0 postulates

28 new tests (556 total), 0 clippy warnings, #![forbid(unsafe_code)].

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

CLAUDE.md

@@ -7,7 +7,7 @@ This document provides guidelines and context for working with Claude Code on th
 **ECHIDNA** (Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance) is a trust-hardened neurosymbolic theorem proving platform supporting 48 prover backends with a comprehensive verification pipeline.
 
 **Repository**: https://github.com/hyperpolymath/echidna
-**Version**: 2.0.0
+**Version**: 2.1.0
 **License**: PMPL-1.0-or-later
 
 ## Repository Structure
@@ -23,7 +23,8 @@ echidna/
 │   │   ├── exchange/       # Cross-prover proof exchange (OpenTheory, Dedukti)
 │   │   ├── dispatch.rs     # Full trust-hardening dispatch pipeline
 │   │   ├── agent/          # Agentic proof search (actor model)
-│   │   ├── neural.rs       # Neural premise selection
+│   │   ├── gnn/            # GNN integration (graph construction, embeddings, client, guided search)
+│   │   ├── neural.rs       # Neural premise selection (text-based, complements GNN)
 │   │   ├── aspect.rs       # Aspect tagging
 │   │   ├── core.rs         # Core types (Term, ProofState, Tactic, Goal)
 │   │   ├── parsers/        # Proof file parsers
@@ -107,6 +108,7 @@ The v1.5 trust hardening added:
 - `src/rust/executor/`: Sandboxed solver execution
 - `src/rust/exchange/`: OpenTheory, Dedukti proof exchange
 - `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)
 
 ### Current Status
@@ -125,8 +127,16 @@ The v1.5 trust hardening added:
 - Idris2 ABI formal proofs (16 modules, zero believe_me)
 - 0 clippy warnings, 0 compiler errors on stable Rust
 
-**Next (v2.1+)**:
-- Deep learning models (Transformers via Flux.jl)
+**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+)**:
+- Train GNN/Transformer on larger corpus (Flux.jl)
 - Chapel → Rust C FFI bridge
 - Tamarin/ProVerif bridge
 

Cargo.lock

@@ -2,7 +2,7 @@
 
 [package]
 name = "echidna"
-version = "2.0.0"
+version = "2.1.0"
 edition = "2021"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
 license = "PMPL-1.0-or-later"

Cargo.toml

@@ -151,9 +151,64 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 * [x] 528 unit tests (was 232), 38 integration, 21 property-based
 * [x] 0 clippy warnings, 0 compiler errors on stable Rust
 
-=== Remaining (v2.1+)
+== v2.1 -- GNN Integration (IN PROGRESS)
+
+=== GNN Proof Graph Construction (COMPLETE)
+* [x] Proof graph builder (`src/rust/gnn/graph.rs`): converts ProofState to typed directed graph
+* [x] 7 node kinds (Goal, Hypothesis, Premise, Subterm, TypeExpr, Binder, Constant)
+* [x] 8 edge kinds (Contains, References, Implies, HasType, BindsOver, SharedStructure, DependsOn, UsefulFor)
+* [x] Recursive term expansion with configurable depth limit
+* [x] Constant deduplication across terms
+* [x] Shared-structure edge detection between premises (Jaccard similarity)
+* [x] Sparse adjacency matrix export for Julia GNN encoder
+
+=== GNN Term Embeddings (COMPLETE)
+* [x] Local feature extraction (`src/rust/gnn/embeddings.rs`): 32-dim feature vectors
+* [x] Node kind one-hot + term kind one-hot + structural features
+* [x] Symbol frequency counting (normalised across graph)
+* [x] Standalone term embedding with cosine similarity
+* [x] Two-pass feature extraction (frequency counting then encoding)
+
+=== GNN Inference Client (COMPLETE)
+* [x] HTTP client (`src/rust/gnn/client.rs`) for Julia ML server
+* [x] JSON serialisation matching Julia TheoremGraph format
+* [x] Graceful degradation when server unavailable
+* [x] Health check, rank, and embed endpoints
+
+=== GNN-Guided Proof Search (COMPLETE)
+* [x] Hybrid search strategy (`src/rust/gnn/guided_search.rs`)
+* [x] GNN + symbolic score combination with configurable weights (default 70/30)
+* [x] Tactic inference from premise names (Apply, Rewrite, Induction, Cases)
+* [x] Premise embedding cache for repeated queries
+* [x] Search statistics tracking (total calls, GNN vs fallback)
+
+=== Julia GNN Server Endpoints (COMPLETE)
+* [x] POST /gnn/rank endpoint (`src/julia/api/gnn_endpoint.jl`)
+* [x] GET /gnn/health endpoint
+* [x] Cosine similarity fallback when model not trained
+* [x] Route registration for existing API server
+
+=== Idris2 Formal Proofs for GNN (COMPLETE)
+* [x] `src/abi/EchidnaABI/Gnn.idr`: 7 proven properties
+* [x] Feature dimension positivity proof
+* [x] Sparse adjacency length consistency
+* [x] Node/edge kind index injectivity (no collisions)
+* [x] Depth expansion monotonicity (termination)
+* [x] DependsOn/UsefulFor duality
+* [x] Combined score boundedness
+* [x] 0 believe_me, 0 postulates
+
+=== Testing (COMPLETE)
+* [x] 28 new unit tests for GNN module
+* [x] 0 clippy warnings on GNN code
+* [x] `#![forbid(unsafe_code)]` on all GNN modules
+
+=== Remaining (v2.1)
 * [ ] Train GNN encoder on proof graphs (Flux.jl)
 * [ ] Train Transformer premise selector
+* [ ] Wire GNN scores into ProverDispatcher confidence
+
+=== Remaining (v2.2+)
 * [ ] Chapel -> Rust C FFI bridge
 * [ ] OpenCyc domain knowledge integration
 * [ ] Tamarin/ProVerif bridge for cipherbot