Cargo.toml

# SPDX-License-Identifier: MPL-2.0

[package]
name = "echidna"
version = "2.3.0"
edition = "2021"
authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
license = "MPL-2.0"
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 = "1.1"

# 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.8", features = ["macros"] }
tower = "0.5"
tower-http = { version = "0.7", features = ["cors", "trace"] }
reqwest = { version = "0.12", default-features = false, features = ["json", "rustls-tls"] }

# Actor framework
actix = "0.13"

# Parsing
nom = "8"

# REPL
rustyline = "18"

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

# UUID — minted only through src/rust/ids.rs: v7 record ids, v8 content ids.
uuid = { version = "1.25.0", features = ["v7", "v8", "serde"] }
# JCS (RFC 8785) canonical JSON, for ids::content_id. The estate's own
# ijson-jcs crate is not public, so this public build cannot depend on it.
serde_json_canonicalizer = "0.3"

# Lazy statics
lazy_static = "1"
strum = { version = "0.28.0", features = ["derive"] }

# 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.10"

# 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 MPL-2.0 / MPL-2.0 fallback.
num-bigint = "0.5"
num-integer = "0.1"
num-traits = "0.2"

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

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

# 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 = "8"
pretty_assertions = "1"
criterion = { version = "0.8", features = ["html_reports"] }

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

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

[workspace]
members = [
    "crates/echidna-core",
    "crates/echidna-core-creusot",
    "crates/echidna-mcp",
    "crates/echidna-wire",
    "crates/typed_wasm",
    "src/interfaces/graphql",
    "src/interfaces/grpc",
    "src/interfaces/rest",
]
exclude = [
    "fuzz",
    # The governance workflow builds this external checker in a nested checkout.
    ".standards-js/tools/js-runtimes",
]