Skip to content

QUICKSTART-USER.adoc

Latest commit

 

History

History
237 lines (176 loc) · 6.34 KB

QUICKSTART-USER.adoc

File metadata and controls

237 lines (176 loc) · 6.34 KB
Raw

ECHIDNA: Quickstart Guide

Neurosymbolic theorem-proving platform with a trust-hardened verification pipeline and sandboxed solver execution. The full backend roster — Tier-1 core through Tier-10 — is in docs/PROVER_COUNT.md.

This guide is for a user who wants to verify a proof. For developer setup see QUICKSTART-DEV.adoc; for release / packaging see QUICKSTART-MAINTAINER.adoc.

Table of Contents

Prerequisites

Tool Version Install

Rust

nightly (>= 1.80)

asdf install rust nightly or https://rustup.rs

just

>= 1.0

cargo install just or https://just.systems

Podman

>= 4.0

dnf install podman / apt install podman — preferred sandbox

pkg-config + openssl-devel

system

dnf install pkg-config openssl-devel / apt install pkg-config libssl-dev

Optional, by component (only needed if you exercise that surface):

  • Idris2 >= 0.7.0 — ABI definitions in src/abi/

  • Zig >= 0.13.0 — FFI bridge in ffi/zig/, src/zig_ffi/

  • Julia >= 1.10 — ML layer in src/julia/

  • Chapel — optional parallel proof dispatch in src/chapel/ (built behind --features chapel)

  • Deno >= 2.0 — ReScript / AffineScript UI in src/rescript/, src/ui/

Run just doctor to see what is and isn’t present; just heal offers to install missing pieces non-destructively.

Clone and build

git clone https://github.com/hyperpolymath/echidna.git
cd echidna

just build       # or: cargo build

Expected shape (version + timing vary):

   Compiling echidna vX.Y.Z (...)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in NNs

The on-disk version lives in Cargo.toml and CHANGELOG.md; this doc deliberately does not pin it.

Run tests

just test          # all rust tests (unit + tests/)
just test-all      # adds integration suites where present
just test-integration   # only the integration tree under tests/

The current test-count summary is whatever `cargo test’s own trailing line reports; counts are not pinned in docs to avoid drift. Many integration tests are gated on external solver binaries and skip cleanly when absent (see Troubleshooting).

Launch the REPL

cargo run -- interactive          # primary entry point
# or via Justfile:
just run interactive

The CLI subcommand is interactive (clap-routed in src/rust/main.rs). It accepts --prover <KIND> and --neural to preselect a backend and turn on neural premise selection. Inside the session, the REPL slash-commands are listed by :help.

Launch the API server

# Bind to localhost:8081 (the binary default) with CORS enabled
cargo run -- server --cors
# or pin a port explicitly
cargo run -- server --port 8000 --host 127.0.0.1 --cors

Then in another terminal:

# Health (no version line — call `cargo run -- --version` for that)
curl http://127.0.0.1:8081/api/health

# List Tier-1 core provers
curl http://127.0.0.1:8081/api/provers

# Refutation demo (Z3) — asserts a contradiction, expects success:true
# ECHIDNA proves by refutation: success ⟺ unsat.
# A satisfiable assertion correctly returns success:false (assert the
# negation of your goal to check a validity obligation instead).
curl -X POST http://127.0.0.1:8081/api/prove \
  -H 'Content-Type: application/json' \
  -d '{"prover":"Z3",
       "content":"(set-logic QF_LIA)\n(declare-const x Int)\n(assert (and (> x 0) (< x 0)))\n(check-sat)\n",
       "timeout":30}'
# Expected: {"success":true,"goals":0,"message":"Proof verified successfully"}

The full route table is in src/rust/server.rs. Separate GraphQL / gRPC / REST interface crates live under src/interfaces/ on dedicated ports (8081 / 50051 / 8000 respectively); they share the same dispatch path.

For a no-build browser UI, open src/ui/public/prove.html directly and point the "API base" field at the running server.

Build container image

# Minimal image (core dependencies only)
just container-build

# Full image (additional provers + Julia)
just container-build-full

Per-prover Wave-3 images live under .containerization/Containerfile.wave3 and are built by the weekly cron in .github/workflows/container-ci.yml with stub-sentinel detection on each cell.

Quick reference

Command Purpose

just build

Build debug binary

just build-release

Build optimised release binary

just test

Run Rust tests

just test-all

Run all Rust + integration suites

just lint

REUSE + rustfmt + clippy

just fmt

Format Rust code in place

just pre-commit

fmt-check + lint + test

cargo run — interactive

Launch interactive REPL

cargo run — server --cors

Launch HTTP API server (default port 8081)

cargo run — list-provers

List ProverKind variants available on this build

just container-build

Build minimal Podman image

just assail

panic-attacker security scan (requires the panic-attack CLI)

just doctor

Verify required toolchain is on PATH

just heal

Offer to install missing tools

just tour

Guided walkthrough of the repo

just help-me

Onboarding subset of recipes

just --list

Every recipe in the Justfile

Troubleshooting

openssl-sys build failure

Install openssl-devel (Fedora) or libssl-dev (Debian/Ubuntu).

cargo: command not found

Install Rust via asdf install rust nightly or https://rustup.rs.

integration tests fail with "binary not found"

Many tests shell out to external solvers (z3, cvc5, coqc, …). Either install the needed binary or restrict to unit tests with cargo test --lib. See docs/SUPPORTED_PROVERS.md for the Tier-1 install hints.

POST /api/prove returns "Failed to spawn …​ process"

Same root cause: the prover binary isn’t on PATH inside the server’s environment. Install it or pick a different prover field. Other backends remain available.

Container build fails

Ensure Podman is installed (podman --version). ECHIDNA uses Podman, not Docker — see Containerfile rather than Dockerfile.