Cargo.toml

# SPDX-License-Identifier: PMPL-1.0-or-later

[package]
name = "echidna"
version = "2.1.0"
edition = "2021"
authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
license = "PMPL-1.0-or-later"
description = "Neurosymbolic theorem proving platform with multi-prover support"
repository = "https://github.com/hyperpolymath/echidna"

[lib]
name = "echidna"
path = "src/rust/lib.rs"

[[bin]]
name = "echidna"
path = "src/rust/main.rs"

[dependencies]
# Async runtime
tokio = { version = "1", features = ["full"] }
async-trait = "0.1"
futures = "0.3"

# Serialization
serde = { version = "1", features = ["derive"] }
serde_json = "1"
toml = "0.8"

# Error handling
anyhow = "1"
thiserror = "2"

# CLI
clap = { version = "4", features = ["derive"] }
colored = "3"
indicatif = "0.18"

# Logging
tracing = "0.1"
tracing-subscriber = { version = "0.3", features = ["env-filter"] }

# Web/HTTP
axum = { version = "0.7", features = ["macros"] }
tower = "0.5"
tower-http = { version = "0.6", features = ["cors", "trace"] }
reqwest = { version = "0.12", default-features = false, features = ["json", "rustls-tls"] }

# Actor framework
actix = "0.13"

# Parsing
nom = "7"

# REPL
rustyline = "15"

# Hashing (BLAKE3 for speed, SHAKE3-512 via tiny-keccak for provenance)
blake3 = "1"
tiny-keccak = { version = "2", features = ["shake"] }

# UUID
uuid = { version = "1", features = ["v4", "serde"] }

# Lazy statics
lazy_static = "1"

# VeriSimDB integration (optional — behind "verisim" feature)
ciborium = { version = "0.2", optional = true }

# Chrono for timestamps
chrono = { version = "0.4", features = ["serde"] }

# Random number generation (for resilience jitter)
rand = "0.8"

# Temporary files (used by prover backends to invoke external solvers)
tempfile = "3"

# Math coprocessor — number theory + exact arithmetic.  Permissive licences
# (Apache-2.0 / MIT) compatible with PMPL-1.0-or-later / MPL-2.0 fallback.
num-bigint = "0.4"
num-integer = "0.1"
num-traits = "0.2"

# Tensor coprocessor — dense linear algebra (BSD-3-Clause, MPL-2.0 compat).
nalgebra = "0.33"

# Crypto coprocessor.  blake3 already declared above; sha2 was previously
# gated behind `verisim` — un-gate so the Crypto backend can use it.
sha2 = "0.10"

# Ed25519 signature verification (Apache-2.0 / MIT, MPL-2.0 compat).
ed25519-dalek = { version = "2", default-features = false, features = ["std"] }

# DSP coprocessor — FFT/IFFT (Apache-2.0 / MIT).
rustfft = "6"

# TypedWasm engine — standalone crate at crates/typed_wasm.
# Provides the pure parse/analyse engine; provers/typed_wasm.rs is a thin
# adapter that maps its `Analysis` onto echidna core types, and routes the
# 39 *TypeChecker discipline variants through discipline-specific TypeInfo.
typed-wasm = { path = "crates/typed_wasm" }

# Canonical Term / Goal / ProofState / Tactic / TypeInfo types.
# Extracted so vcl-ut (and any other proof-exchange client) can share them
# without pulling in the full echidna binary. The `core` and `types`
# modules in this crate are re-exported from lib.rs so downstream
# `use crate::core::*` / `use crate::types::*` paths keep working.
echidna-core = { path = "crates/echidna-core" }

[features]
default = []
chapel = []       # Enable Chapel parallel proof search (requires Zig FFI library)
flint = []        # Enable FLINT CAS coprocessor (requires system libflint, LGPL-3)
spark = []        # Enable SPARK-verified axiom-policy (requires libechidna_spark from GPRbuild)
verisim = [     # Enable VeriSimDB persistent proof storage (8-modality octads)
    "dep:ciborium",
]
# Enable the live-prover test suite (tests/live_prover_suite.rs). Gated so that
# `cargo test` on a machine without prover binaries does NOT fail — the suite
# auto-skips missing binaries, but the feature flag keeps it out of the default
# test run to avoid confusing output. CI enables it in live-provers.yml.
# Also enables VeriSimDB for L3 test hygiene (emit outcome records).
live-provers = ["verisim"]

[dev-dependencies]
proptest = "1"
tokio-test = "0.4"
which = "7"
pretty_assertions = "1"
criterion = { version = "0.5", features = ["html_reports"] }

[[bench]]
name = "proof_benchmarks"
harness = false

[[bench]]
name = "routing_benchmarks"
harness = false

[workspace]
members = [
    "crates/echidna-core",
    "crates/echidna-core-spark",
    "crates/echidna-mcp",
    "crates/echidna-wire",
    "crates/typed_wasm",
    "src/interfaces/graphql",
    "src/interfaces/grpc",
    "src/interfaces/rest",
]
exclude = [
    "echidnabot",
    "fuzz",
]