From 018a5bfa487bb4a188f21438e5be7feda35ee763 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 5 Oct 2026 19:32:56 +0100 Subject: [PATCH 1/2] feat: echidna prove --output json, echidna-core client crate, Zig FFI CI - `echidna prove --output json` prints exactly one echidna.prove.result/1 object (JCS-canonical I-JSON) on stdout; logs go to stderr. Statuses map from ProverOutcome (verified/failed/error/timeout/unknown). trust.confidence is null unless receipt-backed (epistemic-types receipt/warrant pattern). Human output stays the default. Golden-byte unit tests for every status, planted non-canonical mutants, and end-to-end binary tests (TypedWasm). - echidna-core 0.2.0: ProverKind moved in (re-exported from echidna, no source change), prove_result contract type with strict parser, and the trust kernel re-exported as echidna_core::trust. README documents the git-dependency recipe and stability policy. - ffi/zig compiles again (opaque Handle, page allocator, no libc) and is gated by a new zig-ffi-ci.yml: zig fmt, zig build test, and the cicd-suite unified-api-adapter purity check. tentacles.zig no longer uses std.io; poll_events gained tests. - chapel-ci: zig build -Dcpu=baseline (fixes SIGILL on main). - rust-ci: check/clippy/test with --workspace (crate tests never ran). - Idris2 ABI: %default total in Gnn and TacticRecord. - CREUSOT-SETUP.adoc: remove false hard-gate/done claims; record why Creusot does not run in CI. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/actions.lock | 9 + .github/workflows/chapel-ci.yml | 4 +- .github/workflows/rust-ci.yml | 10 +- .github/workflows/zig-ffi-ci.yml | 62 + CHANGELOG.adoc | 33 + Cargo.lock | 6 +- .../echidna-core-creusot/CREUSOT-SETUP.adoc | 76 +- crates/echidna-core/Cargo.toml | 14 +- crates/echidna-core/README.adoc | 59 + crates/echidna-core/src/lib.rs | 32 +- crates/echidna-core/src/prove_result.rs | 367 +++++ crates/echidna-core/src/prover_kind.rs | 1297 +++++++++++++++++ docs/PROVE-RESULT-CONTRACT.adoc | 115 ++ docs/wikis/Home.md | 6 +- ffi/zig/src/boj.zig | 4 +- ffi/zig/src/capnp_bridge.zig | 24 +- ffi/zig/src/main.zig | 70 +- ffi/zig/src/provers/atp.zig | 4 +- ffi/zig/src/provers/declarative.zig | 14 +- ffi/zig/src/provers/vcl_ut.zig | 4 +- ffi/zig/src/tentacles.zig | 47 +- ffi/zig/src/typell.zig | 4 +- ffi/zig/test/benchmark.zig | 10 +- ffi/zig/test/core_native_test.zig | 11 +- ffi/zig/test/integration_test.zig | 10 +- src/abi/EchidnaABI/Gnn.idr | 2 + src/abi/EchidnaABI/TacticRecord.idr | 2 + src/rust/lib.rs | 1 + src/rust/main.rs | 150 +- src/rust/prove_contract.rs | 202 +++ src/rust/provers/mod.rs | 1280 +--------------- src/rust/provers/outcome.rs | 73 + tests/prove_output_json.rs | 151 ++ 33 files changed, 2732 insertions(+), 1421 deletions(-) create mode 100644 .github/workflows/zig-ffi-ci.yml create mode 100644 crates/echidna-core/README.adoc create mode 100644 crates/echidna-core/src/prove_result.rs create mode 100644 crates/echidna-core/src/prover_kind.rs create mode 100644 docs/PROVE-RESULT-CONTRACT.adoc create mode 100644 src/rust/prove_contract.rs create mode 100644 tests/prove_output_json.rs diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 8110298e..ce95a606 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -92,6 +92,10 @@ workflows: - 'actions/checkout@v7.0.1' '.github/workflows/workflow-linter.yml': - 'actions/checkout@v7.0.1' + '.github/workflows/zig-ffi-ci.yml': + - 'actions/checkout@v7.0.1' + - 'hyperpolymath/cicd-suite@main' + - 'mlugg/setup-zig@v2.2.1' dependencies: 'actions/attest-build-provenance@v4.2.2': ref: 'v4.2.2' @@ -172,6 +176,11 @@ dependencies: commit: 'sha1-0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d' owner_id: 75048950 repo_id: 623796603 + 'hyperpolymath/cicd-suite@main': + ref: 'main' + commit: 'sha1-d9ebcf99ad4593611b4fa0e18f09b03801f200e8' + owner_id: 6759885 + repo_id: 1326697643 'mlugg/setup-zig@v2.2.1': ref: 'v2.2.1' commit: 'sha1-d1434d08867e3ee9daa34448df10607b98908d29' diff --git a/.github/workflows/chapel-ci.yml b/.github/workflows/chapel-ci.yml index 600b405c..bcb6c0d1 100644 --- a/.github/workflows/chapel-ci.yml +++ b/.github/workflows/chapel-ci.yml @@ -123,7 +123,7 @@ jobs: version: 0.14.0 - name: Build Zig FFI library (with Chapel stubs) - run: cd src/zig_ffi && zig build -Doptimize=ReleaseSafe + run: cd src/zig_ffi && zig build -Doptimize=ReleaseSafe -Dcpu=baseline # baseline: the artifact runs on another runner (SIGILL otherwise) - name: Run Zig FFI tests (stub mode) run: cd src/zig_ffi && zig build test @@ -219,7 +219,7 @@ jobs: - name: Build Zig FFI without stubs (links against real Chapel) run: | cd src/zig_ffi - zig build -Doptimize=ReleaseSafe -Dstubs=false + zig build -Doptimize=ReleaseSafe -Dcpu=baseline -Dstubs=false - name: Build Rust with real Chapel library run: | diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index b3abae4e..acdafcc8 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -104,16 +104,16 @@ jobs: # first push it happens, instead of silently re-resolving (which # masked the echidna#92 / echidna PR #128 dependabot major-bump # break for 24h). See standards#295. - run: cargo check --locked --all-targets + run: cargo check --locked --workspace --all-targets - name: Cargo fmt run: cargo fmt --all -- --check - name: Cargo clippy - run: cargo clippy --locked --all-targets -- -D warnings + run: cargo clippy --locked --workspace --all-targets -- -D warnings test: - timeout-minutes: 20 + timeout-minutes: 30 name: rust-ci / Cargo test runs-on: ubuntu-latest needs: [detect, check] @@ -149,7 +149,9 @@ jobs: - name: Run tests # `--locked` — see Cargo check above. - run: cargo test --locked --all-targets + # `--workspace`: without it only the root package is tested, so the + # echidna-core (prove-result contract) and trust-kernel tests never ran. + run: cargo test --locked --workspace --all-targets - name: Write summary if: always() diff --git a/.github/workflows/zig-ffi-ci.yml b/.github/workflows/zig-ffi-ci.yml new file mode 100644 index 00000000..2d783fb9 --- /dev/null +++ b/.github/workflows/zig-ffi-ci.yml @@ -0,0 +1,62 @@ +# This workflow is managed by gh actions-lock. +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Zig FFI CI for echidna (ffi/zig): format, unit tests, and the estate +# unified-api-adapter purity check (no std.fs / std.io in any .zig file). +# +# Before 2026-10-05 ffi/zig was built by no workflow and did not compile on +# any Zig release (opaque Handle with fields, implicit libc). This job keeps +# it compiling and tested. The library targets that link against the Rust +# libechidna.so (integration tests, benchmarks) are not built here. +# +# Zig is pinned to 0.15.2, the version ffi/zig/build.zig is written for. +name: Zig FFI CI + +on: + push: + branches: [main] + pull_request: + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + zig-ffi: + name: zig-ffi / fmt + test (ffi/zig) + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - name: Checkout repository + uses: actions/checkout@v7.0.1 + with: + persist-credentials: false + + - name: Install Zig + uses: mlugg/setup-zig@v2.2.1 + with: + version: 0.15.2 + + - name: zig fmt --check + run: zig fmt --check ffi/zig/src ffi/zig/test ffi/zig/build.zig + + - name: zig build test + working-directory: ffi/zig + run: zig build test --summary all + + unified-api-adapter: + name: zig-ffi / unified-api-adapter purity + runs-on: ubuntu-latest + timeout-minutes: 5 + steps: + - name: Checkout repository + uses: actions/checkout@v7.0.1 + with: + persist-credentials: false + + - name: Zig unified-api-adapter check (hyperpolymath/cicd-suite) + uses: hyperpolymath/cicd-suite/actions/zig-unified-api-adapter-check@main diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 267aaaa9..0c1e751e 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -8,6 +8,39 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Added — integrations 2026-10-05 + +* *`+echidna prove --output json+`*: prints exactly one +`+echidna.prove.result/1+` object (JCS-canonical I-JSON) on stdout, logs +to stderr. Statuses `+verified+` / `+failed+` / `+error+` / `+timeout+` / +`+unknown+`, mapped from `+ProverOutcome+`; `+trust.confidence+` is +`+null+` unless receipt-backed. Human output stays the default. See +`+docs/PROVE-RESULT-CONTRACT.adoc+`. +* *`+echidna-core+` 0.2.0* is consumable by clients (echidnabot, +proof-burrower): adds `+ProverKind+` (moved from `+echidna::provers+`, +re-exported there, no source change for ECHIDNA), the +`+echidna.prove.result/1+` type with a strict parser, and the trust +kernel as `+echidna_core::trust+`. Git-dependency recipe and stability +policy in `+crates/echidna-core/README.adoc+`. +* *`+ffi/zig+` builds and is tested in CI* (`+zig-ffi-ci.yml+`, Zig +0.15.2): it previously compiled on no Zig release. Pure Zig (page +allocator, no libc); the estate unified-api-adapter purity check +(`+hyperpolymath/cicd-suite+`) runs on every PR. + +==== Fixed — integrations 2026-10-05 + +* ci(chapel): build the Zig FFI with `+-Dcpu=baseline+`; the artifact +runs on a different runner, and native-CPU code crashed there with +SIGILL in "Rust Build with Chapel Feature". +* ci(rust): check, clippy and test now run with `+--workspace+`; before, +only the root package was tested, so `+echidna-core+` and the trust +kernel tests never ran in CI. +* abi: `+EchidnaABI.Gnn+` and `+EchidnaABI.TacticRecord+` now declare +`+%default total+` (both already type-check total). +* docs(creusot): `+CREUSOT-SETUP.adoc+` no longer claims the Creusot job +is a hard gate or that milestones 8c-M1..M3 are done; it records why +Creusot does not run in CI. + ==== Changed * *Licence: `+AGPL-3.0-or-later+` → `+MPL-2.0+` for code and the diff --git a/Cargo.lock b/Cargo.lock index 81af6998..0bf8ea74 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1108,10 +1108,14 @@ dependencies = [ [[package]] name = "echidna-core" -version = "0.1.0" +version = "0.2.0" dependencies = [ + "anyhow", + "echidna-core-creusot", "serde", "serde_json", + "serde_json_canonicalizer", + "strum 0.28.0", ] [[package]] diff --git a/crates/echidna-core-creusot/CREUSOT-SETUP.adoc b/crates/echidna-core-creusot/CREUSOT-SETUP.adoc index fe1fda25..a8ec4206 100644 --- a/crates/echidna-core-creusot/CREUSOT-SETUP.adoc +++ b/crates/echidna-core-creusot/CREUSOT-SETUP.adoc @@ -92,19 +92,40 @@ contract. All obligations in `+impl_invariants+` are designed to discharge quickly (< 30 s each on a modern workstation). -=== 6 — CI integration - -`+.github/workflows/formal-verification.yml+` runs two jobs, both merge -gates: - -* `+stable-tests+`: `+cargo test -p echidna-core-creusot+` on stable Rust -(~10 s). -* `+creusot-verify+`: `+cargo +nightly creusot+` with Why3 + Z3 -discharge. Requires `+apt-get install why3 z3 alt-ergo+` in the runner -(Ubuntu 22.04+). - -Both were promoted to hard gates in Stage 8c-M3 (no -`+continue-on-error+`). +=== 6 — CI integration (what actually runs) + +`+.github/workflows/formal-verification.yml+` has two jobs: + +* `+stable-tests+`: `+cargo test -p echidna-core-creusot+` on stable Rust. +It runs on pull requests that touch this crate, and the crate's tests +also run in the workspace test job of `+rust-ci.yml+`. It checks the +stable-Rust mirror of each stated obligation. It does not run Creusot. +* `+creusot-verify+`: manual only (`+workflow_dispatch+`). It has never +discharged an obligation. + +==== Why Creusot does not run in CI (measured 2026-10-05) + +. *The annotations do not compile under Creusot's macros.* +`+cargo check -p echidna-core-creusot --features creusot+` fails with +34 errors: `+creusot_contracts+` is unresolved (it is not a +dependency), so `+ensures+`, `+requires+`, `+invariant+`, `+pure+` and +`+snapshot!+` are unknown. No obligation has ever reached Why3. +. *The toolchain pin is stale.* `+rust-toolchain.toml+` pins +`+nightly-2024-05-01+`, which predates current Creusot releases. +. *The install path in this guide is wrong for current Creusot.* Creusot +is installed with its own `+INSTALL+` script, which provisions Why3 and +`+why3find+` through opam; `+cargo install creusot+` does not do that. +. *Adding `+creusot-contracts+` as an optional dependency would put a +nightly-only crate in `+Cargo.lock+`*, which the stable `+--locked+` +build and `+cargo audit+` also read. + +What it would take: pick one Creusot release, pin its nightly here and in +the workflow, add `+creusot-contracts+` behind the `+creusot+` feature, +rewrite the annotations against that release's logic syntax until +`+cargo creusot+` type-checks them, install Creusot with its `+INSTALL+` +script in the job, and only then make `+creusot-verify+` run on pull +requests. Until a dispatch run discharges every obligation, call the +annotations *stated, not proved*. === Annotation style @@ -124,36 +145,23 @@ no-ops on stable Rust. |=== |Milestone |Contents |Status |8c-M1 |`+rust-toolchain.toml+`, `+formal-verification.yml+`, -`+just verify-trust-pipeline+` |*done* +`+just verify-trust-pipeline+` |files exist; toolchain pin stale |8c-M2 |`+dominates+` marked `+#[pure]+`; `+compute+` ensures with -`+^candidates+`; inner-loop `+#[invariant]+` for `+dominated+` |*done* +`+^candidates+`; inner-loop `+#[invariant]+` for `+dominated+` +|annotations written, never type-checked by Creusot |8c-M3 |Outer-loop invariant (`+snapshot!+` + prefix classification); -Why3 CI hard gate |*done* +Why3 CI hard gate |annotations written; *no CI gate* (see above) |=== -All three milestones are complete. The `+compute+` function now carries -the full two-level invariant structure: - -* *Outer*: `+snapshot!(candidates)+` at entry + `+#[invariant]+` -asserting -[loweralpha] -. objectives unchanged for all k, (b) `+is_pareto_optimal[k]+` correctly -set for k < i. -* *Inner*: `+dominated == (∃ k < j, k ≠ i : dominates(k, i))+`. - -The CI workflow (`+formal-verification.yml+`) is a hard gate: both -`+stable-tests+` and `+creusot-verify+` must pass for a merge. If the -nightly pin drifts, bump `+rust-toolchain.toml+` + the workflow’s -`+toolchain:+` field together. - -This keeps the crate buildable on stable Rust at all times while still -expressing every proof obligation in machine-verifiable syntax. +An earlier version of this table marked all three milestones done and +described both jobs as hard merge gates. That was not true: no obligation +has been discharged (see "Why Creusot does not run in CI"). === References * Creusot repository: https://github.com/creusot-rs/creusot * Why3 documentation: https://www.why3.org/ -* SPARK Adoption Plan: `+docs/design/SPARK_ADOPTION_PLAN.adoc+` +* SPARK Adoption Plan: `+docs/design/SPARK_ADOPTION_PLAN.adoc+` (historical; this crate is Creusot, not SPARK) * Echidna ROADMAP Stage 8c: `+docs/ROADMAP.adoc+` diff --git a/crates/echidna-core/Cargo.toml b/crates/echidna-core/Cargo.toml index 5aaddcfa..52bd8015 100644 --- a/crates/echidna-core/Cargo.toml +++ b/crates/echidna-core/Cargo.toml @@ -2,13 +2,23 @@ [package] name = "echidna-core" -version = "0.1.0" +version = "0.2.0" edition = "2021" authors = ["Jonathan D.A. Jewell "] license = "MPL-2.0" -description = "Canonical Term / Goal / ProofState / Tactic types for ECHIDNA, re-used by vcl-ut and any future proof-exchange client without depending on the full echidna binary." +description = "Canonical ECHIDNA client types: Term / Goal / ProofState / Tactic, ProverKind, the echidna.prove.result/1 contract and the trust kernel, without depending on the full echidna binary." repository = "https://github.com/hyperpolymath/echidna" [dependencies] serde = { version = "1", features = ["derive"] } serde_json = "1" +# ProverKind::from_str keeps its historical anyhow::Error error type. +anyhow = "1" +# ProverKind derives strum::EnumIter. +strum = { version = "0.28.0", features = ["derive"] } +# JCS (RFC 8785) canonical JSON for the echidna.prove.result/1 contract. +serde_json_canonicalizer = "0.3" +# Trust kernel (TrustLevel, compute_trust_level, axiom scanner), re-exported +# as echidna_core::trust. Path dependency inside this repository; a git +# dependency on echidna-core resolves it from the same commit. +echidna-core-creusot = { path = "../echidna-core-creusot", version = "0.1.0" } diff --git a/crates/echidna-core/README.adoc b/crates/echidna-core/README.adoc new file mode 100644 index 00000000..7da97bf9 --- /dev/null +++ b/crates/echidna-core/README.adoc @@ -0,0 +1,59 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += echidna-core + +The types a client of ECHIDNA needs, without the full `echidna` crate: + +[cols="1,3",options="header"] +|=== +| Module | Contents + +| `core`, `types` | `Term`, `Goal`, `ProofState`, `Tactic`, `TypeInfo`. +| `prover_kind` | `ProverKind`, the backend enumeration, with `FromStr` and `Display`. +| `prove_result` | `ProveResult`, the `echidna.prove.result/1` contract printed by `echidna prove --output json` (see `docs/PROVE-RESULT-CONTRACT.adoc`), with a JCS serialiser and a strict parser. +| `trust` | The trust kernel re-exported from `echidna-core-creusot`: `TrustLevel`, `TrustFactors`, `ProverClass`, `compute_trust_level`, `combine_trust`, `axiom_tracker`, `pareto`. +|=== + +`echidna` re-exports these, so `echidna::ProverKind` and +`echidna::provers::ProverKind` are the same type as +`echidna_core::ProverKind`. + +== Using it from another repository + +The crate is not published to crates.io. Depend on it from git, pinned to a +full commit SHA so the build is reproducible: + +[source,toml] +---- +[dependencies] +echidna-core = { git = "https://github.com/hyperpolymath/echidna", rev = "" } +---- + +Cargo finds the crate inside the repository by name. Its path dependency on +`echidna-core-creusot` resolves from the same commit, so nothing else is +needed. Do not use a `path = "../echidna/..."` dependency in a published +repository: it only builds on a machine with that checkout. + +Dependencies it brings: `serde`, `serde_json`, `anyhow`, `strum`, +`serde_json_canonicalizer`, and `echidna-core-creusot` (which needs only +`serde`). + +== Stability + +The crate follows Semantic Versioning, read the Cargo way for 0.x: a change +in the minor number (0.2 to 0.3) may break, a change in the patch number +does not. + +* Stable from 0.2.0: the module paths above, the `ProverKind` variant + names (they are its serde form), the `ProveResult` fields and the + `echidna.prove.result/1` wire format, and the `trust` items listed above. +* Adding a `ProverKind` variant is not breaking for ECHIDNA's purposes; keep + a wildcard arm when you match on it. +* The trust kernel's Creusot annotations are stated, not proved (see + `crates/echidna-core-creusot/CREUSOT-SETUP.adoc`). Its behaviour is + covered by stable-Rust tests. + +== History + +* 0.2.0 (2026-10-05): added `prover_kind`, `prove_result` and `trust`. + `ProverKind` moved here from `echidna::provers`; nothing was removed. +* 0.1.0: `core` and `types`. diff --git a/crates/echidna-core/src/lib.rs b/crates/echidna-core/src/lib.rs index f6bafb83..b38e2596 100644 --- a/crates/echidna-core/src/lib.rs +++ b/crates/echidna-core/src/lib.rs @@ -3,15 +3,37 @@ //! ECHIDNA canonical type surface. //! //! Holds the types that any client of ECHIDNA (local or over the wire) must -//! agree on: [`core::Term`], [`core::Goal`], [`core::ProofState`], -//! [`core::Tactic`], and the optional [`types::TypeInfo`] decoration. +//! agree on: //! -//! Kept minimal on purpose — only `serde` and `serde_json`. Downstream crates -//! (`echidna` itself, `vcl-ut`, future clients) depend on this crate rather -//! than duplicating the definitions. +//! - [`core::Term`], [`core::Goal`], [`core::ProofState`], [`core::Tactic`] +//! and the optional [`types::TypeInfo`] decoration; +//! - [`prover_kind::ProverKind`], the backend enumeration; +//! - [`prove_result::ProveResult`], the `echidna.prove.result/1` contract +//! printed by `echidna prove --output json`; +//! - [`trust`], the trust kernel (trust levels, axiom scanner), re-exported +//! from `echidna-core-creusot`. +//! +//! Kept small on purpose. Downstream crates (`echidna` itself, `vcl-ut`, +//! echidnabot, proof-burrower) depend on this crate rather than duplicating +//! the definitions. See `crates/echidna-core/README.adoc` for the stability +//! policy and the git-dependency recipe. //! //! Internal cross-references (`crate::core::Term`, `crate::types::TypeInfo`) //! work unchanged because both modules live in this crate. pub mod core; +pub mod prove_result; +pub mod prover_kind; pub mod types; + +/// The ECHIDNA trust kernel: [`trust::TrustLevel`], [`trust::compute_trust_level`], +/// [`trust::axiom_tracker`] and [`trust::pareto`]. +/// +/// Re-exported unchanged from `echidna-core-creusot`. Its Creusot +/// annotations are stated, not proved; the stable-Rust tests mirror them. +pub mod trust { + pub use echidna_core_creusot::*; +} + +pub use prove_result::{ProveResult, ProveStatus, ProveTrust}; +pub use prover_kind::ProverKind; diff --git a/crates/echidna-core/src/prove_result.rs b/crates/echidna-core/src/prove_result.rs new file mode 100644 index 00000000..b37c0631 --- /dev/null +++ b/crates/echidna-core/src/prove_result.rs @@ -0,0 +1,367 @@ +// SPDX-License-Identifier: MPL-2.0 + +//! The `echidna.prove.result/1` contract. +//! +//! `echidna prove --output json` prints exactly one line on stdout: +//! a JCS-canonical (RFC 8785) I-JSON (RFC 7493) object of this shape +//! (shown wrapped; keys appear in JCS order on the wire): +//! +//! ```json +//! {"duration_ms":12,"echidna_version":"2.3.0","goal":"probe.thy", +//! "message":"PROVED in 12ms","prover":"Isabelle", +//! "schema":"echidna.prove.result/1","status":"verified", +//! "trust":{"axioms":[],"confidence":null}} +//! ``` +//! +//! This module holds the type both sides use: ECHIDNA serialises it with +//! [`ProveResult::to_jcs`], and consumers (proof-burrower, echidnabot) can +//! parse it strictly with [`ProveResult::parse`]. +//! +//! ## Receipt, not warrant +//! +//! `trust.confidence` is a number only when a receipt-backed computation +//! produced it, such as an independently checked proof certificate. A +//! single-prover run that checked no certificate reports `null`, never a +//! guessed score. The distinction follows the factive / non-factive split +//! of `hyperpolymath/epistemic-types` (`FactiveModality`): a receipt is +//! transported proof, a warrant is only evidence. This crate copies that +//! distinction as a pattern; it does not depend on the Agda library. +//! +//! ## Versioning +//! +//! Adding a field is backwards compatible (consumers must ignore unknown +//! fields). Removing, renaming or retyping a field needs a new schema +//! identifier (`echidna.prove.result/2`). + +use serde::{Deserialize, Serialize}; +use std::fmt; + +/// The schema identifier this module emits and accepts. +pub const SCHEMA: &str = "echidna.prove.result/1"; + +/// Largest integer I-JSON (RFC 7493 §2.2) guarantees to round-trip: 2^53 − 1. +pub const MAX_SAFE_INTEGER: u64 = (1u64 << 53) - 1; + +/// The verdict of one prove run. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)] +#[serde(rename_all = "lowercase")] +pub enum ProveStatus { + /// The backend established the goal. + Verified, + /// The backend ran to completion and did not establish the goal. + Failed, + /// ECHIDNA or the backend could not run, or the input was rejected. + Error, + /// The backend exceeded its time budget. + Timeout, + /// The run finished without a usable answer (for example, the premises + /// were inconsistent, so a "proof" would be vacuous). + Unknown, +} + +impl ProveStatus { + /// Every status, in contract order. + pub const ALL: [ProveStatus; 5] = [ + ProveStatus::Verified, + ProveStatus::Failed, + ProveStatus::Error, + ProveStatus::Timeout, + ProveStatus::Unknown, + ]; + + /// The wire string of this status. + pub fn as_str(self) -> &'static str { + match self { + ProveStatus::Verified => "verified", + ProveStatus::Failed => "failed", + ProveStatus::Error => "error", + ProveStatus::Timeout => "timeout", + ProveStatus::Unknown => "unknown", + } + } +} + +/// What a verdict rests on. +#[derive(Debug, Clone, PartialEq, Default, Serialize, Deserialize)] +pub struct ProveTrust { + /// Receipt-backed confidence in `[0, 1]`, or `None` (`null`) when no + /// receipt-backed figure exists. See the module docs. + pub confidence: Option, + /// Axioms and escape hatches (`sorry`, `Admitted`, ...) found in the + /// input, sorted and de-duplicated. + pub axioms: Vec, +} + +/// One `echidna.prove.result/1` object. +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] +pub struct ProveResult { + /// Always [`SCHEMA`]. + pub schema: String, + /// The verdict. + pub status: ProveStatus, + /// The backend, as ECHIDNA names it (`ProverKind` variant name), or the + /// empty string when no backend could be selected. + pub prover: String, + /// The goal ECHIDNA was asked to prove: the proof file path as given. + pub goal: String, + /// Wall-clock time of the backend check, in milliseconds. + pub duration_ms: u64, + /// Human-readable diagnostic; may be empty. + pub message: String, + /// What the verdict rests on. + pub trust: ProveTrust, + /// The ECHIDNA version that emitted this object. + pub echidna_version: String, +} + +/// Why a value cannot be emitted, or a payload is not a valid result. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum ProveResultError { + /// `duration_ms` exceeds [`MAX_SAFE_INTEGER`]. + UnsafeInteger(u64), + /// `trust.confidence` is NaN, infinite, or outside `[0, 1]`. + BadConfidence, + /// The payload is empty. + Empty, + /// The payload holds more than one line. + ExtraOutput, + /// The payload is not valid JSON. + NotJson(String), + /// The payload is JSON but not byte-identical to its RFC 8785 form. + NotCanonical, + /// The object names a different schema. + WrongSchema(String), + /// The object does not have the contract's shape. + Shape(String), +} + +impl fmt::Display for ProveResultError { + /// Render the error as a one-line diagnostic. + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + ProveResultError::UnsafeInteger(n) => { + write!(f, "duration_ms {n} exceeds the I-JSON safe range") + }, + ProveResultError::BadConfidence => { + write!( + f, + "trust.confidence must be a finite number in [0, 1] or null" + ) + }, + ProveResultError::Empty => write!(f, "empty payload"), + ProveResultError::ExtraOutput => write!(f, "more than one line"), + ProveResultError::NotJson(e) => write!(f, "not JSON: {e}"), + ProveResultError::NotCanonical => write!(f, "not JCS-canonical (RFC 8785)"), + ProveResultError::WrongSchema(s) => write!(f, "unsupported schema {s:?}"), + ProveResultError::Shape(e) => write!(f, "wrong shape: {e}"), + } + } +} + +impl std::error::Error for ProveResultError {} + +impl ProveResult { + /// Build a result with the current [`SCHEMA`]. + /// + /// `duration_ms` saturates at [`MAX_SAFE_INTEGER`] and `axioms` are + /// sorted and de-duplicated, so the output is deterministic for the + /// same inputs. + pub fn new( + status: ProveStatus, + prover: impl Into, + goal: impl Into, + duration_ms: u64, + message: impl Into, + mut trust: ProveTrust, + echidna_version: impl Into, + ) -> Self { + trust.axioms.sort(); + trust.axioms.dedup(); + ProveResult { + schema: SCHEMA.to_string(), + status, + prover: prover.into(), + goal: goal.into(), + duration_ms: duration_ms.min(MAX_SAFE_INTEGER), + message: message.into(), + trust, + echidna_version: echidna_version.into(), + } + } + + /// Serialise to the one-line JCS-canonical I-JSON form (no newline). + /// + /// Fails rather than emit a value outside I-JSON: an integer beyond + /// 2^53 − 1, or a non-finite or out-of-range confidence. + pub fn to_jcs(&self) -> Result { + if self.duration_ms > MAX_SAFE_INTEGER { + return Err(ProveResultError::UnsafeInteger(self.duration_ms)); + } + if let Some(c) = self.trust.confidence { + if !c.is_finite() || !(0.0..=1.0).contains(&c) { + return Err(ProveResultError::BadConfidence); + } + } + // JCS output has no raw newlines (control characters in strings + // are escaped), so this is always exactly one line. + serde_json_canonicalizer::to_string(self) + .map_err(|e| ProveResultError::Shape(e.to_string())) + } + + /// Parse and validate a payload as exactly one result object. + /// + /// One trailing newline is allowed. The line must be JSON, must equal + /// its own RFC 8785 canonical form byte for byte (which rules out + /// duplicate keys and unsafe integers), must name [`SCHEMA`], and must + /// carry every field with the right type. Unknown extra fields are + /// tolerated. + pub fn parse(payload: &str) -> Result { + let line = payload.strip_suffix('\n').unwrap_or(payload); + if line.is_empty() { + return Err(ProveResultError::Empty); + } + if line.contains('\n') { + return Err(ProveResultError::ExtraOutput); + } + let value: serde_json::Value = + serde_json::from_str(line).map_err(|e| ProveResultError::NotJson(e.to_string()))?; + let canonical = serde_json_canonicalizer::to_string(&value) + .map_err(|e| ProveResultError::NotJson(e.to_string()))?; + if canonical != line { + return Err(ProveResultError::NotCanonical); + } + match value.get("schema").and_then(|s| s.as_str()) { + Some(SCHEMA) => {}, + Some(other) => return Err(ProveResultError::WrongSchema(other.to_string())), + None => { + return Err(ProveResultError::Shape( + "missing string field `schema`".into(), + )) + }, + } + serde_json::from_value(value).map_err(|e| ProveResultError::Shape(e.to_string())) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + /// A fixed sample used by the golden tests. + fn sample(status: ProveStatus) -> ProveResult { + ProveResult::new( + status, + "Isabelle", + "probe.thy", + 12, + "", + ProveTrust { + confidence: None, + axioms: vec!["sorry".into()], + }, + "2.3.0", + ) + } + + /// Every status serialises to the exact golden JCS bytes and parses back. + #[test] + fn golden_jcs_bytes_for_every_status() { + for status in ProveStatus::ALL { + let expected = format!( + r#"{{"duration_ms":12,"echidna_version":"2.3.0","goal":"probe.thy","message":"","prover":"Isabelle","schema":"echidna.prove.result/1","status":"{}","trust":{{"axioms":["sorry"],"confidence":null}}}}"#, + status.as_str() + ); + let got = sample(status).to_jcs().unwrap(); + assert_eq!(got, expected); + assert_eq!(ProveResult::parse(&got).unwrap(), sample(status)); + } + } + + /// Escapes and non-ASCII text still yield one canonical line. + #[test] + fn output_is_its_own_canonical_form() { + let mut r = sample(ProveStatus::Failed); + r.message = "line one\nline \"two\" \u{e9}".into(); + r.trust.confidence = Some(0.5); + let out = r.to_jcs().unwrap(); + assert!(!out.contains('\n')); + let reparsed: serde_json::Value = serde_json::from_str(&out).unwrap(); + assert_eq!(serde_json_canonicalizer::to_string(&reparsed).unwrap(), out); + assert_eq!(ProveResult::parse(&out).unwrap(), r); + } + + /// Planted mutants (reordered keys, whitespace, duplicates, extra lines, wrong schema) are refused. + #[test] + fn planted_non_canonical_payloads_are_rejected() { + let good = sample(ProveStatus::Verified).to_jcs().unwrap(); + // Reordered keys. + let reordered = good.replacen( + r#"{"duration_ms":12,"echidna_version":"2.3.0""#, + r#"{"echidna_version":"2.3.0","duration_ms":12"#, + 1, + ); + assert_ne!(reordered, good); + assert_eq!( + ProveResult::parse(&reordered), + Err(ProveResultError::NotCanonical) + ); + // Whitespace. + let spaced = good.replacen(':', ": ", 1); + assert_eq!( + ProveResult::parse(&spaced), + Err(ProveResultError::NotCanonical) + ); + // Duplicate key. + assert_eq!( + ProveResult::parse(r#"{"a":1,"a":2}"#), + Err(ProveResultError::NotCanonical) + ); + // Extra line, empty, wrong schema. + assert_eq!( + ProveResult::parse(&format!("notice\n{good}")), + Err(ProveResultError::ExtraOutput) + ); + assert_eq!(ProveResult::parse("\n"), Err(ProveResultError::Empty)); + let wrong = good.replace("echidna.prove.result/1", "echidna.prove.result/9"); + assert!(matches!( + ProveResult::parse(&wrong), + Err(ProveResultError::WrongSchema(_)) + )); + } + + /// Values outside I-JSON or the confidence range are not emitted. + #[test] + fn out_of_range_values_are_refused() { + let mut r = sample(ProveStatus::Verified); + r.duration_ms = MAX_SAFE_INTEGER + 1; + assert_eq!( + r.to_jcs(), + Err(ProveResultError::UnsafeInteger(MAX_SAFE_INTEGER + 1)) + ); + let mut r = sample(ProveStatus::Verified); + r.trust.confidence = Some(f64::NAN); + assert_eq!(r.to_jcs(), Err(ProveResultError::BadConfidence)); + r.trust.confidence = Some(1.5); + assert_eq!(r.to_jcs(), Err(ProveResultError::BadConfidence)); + } + + /// `new` saturates the duration and sorts and de-duplicates axioms. + #[test] + fn constructor_saturates_and_normalises() { + let r = ProveResult::new( + ProveStatus::Verified, + "Lean", + "a.lean", + u64::MAX, + "", + ProveTrust { + confidence: None, + axioms: vec!["sorry".into(), "Classical.choice".into(), "sorry".into()], + }, + "x", + ); + assert_eq!(r.duration_ms, MAX_SAFE_INTEGER); + assert_eq!(r.trust.axioms, vec!["Classical.choice", "sorry"]); + assert!(r.to_jcs().is_ok()); + } +} diff --git a/crates/echidna-core/src/prover_kind.rs b/crates/echidna-core/src/prover_kind.rs new file mode 100644 index 00000000..d5290928 --- /dev/null +++ b/crates/echidna-core/src/prover_kind.rs @@ -0,0 +1,1297 @@ +// SPDX-License-Identifier: MPL-2.0 + +//! The [`ProverKind`] enumeration: every prover backend ECHIDNA knows about. +//! +//! Moved here from `echidna::provers` (2026-10-05) so that clients such as +//! echidnabot and proof-burrower can name a backend with the same type +//! ECHIDNA uses, without depending on the full `echidna` crate. +//! `echidna::provers::ProverKind` and `echidna::ProverKind` re-export this +//! type, so existing ECHIDNA code is unchanged. +//! +//! Stability: variant names are part of the wire format (serde uses the +//! variant name). Adding a variant is a minor change; renaming or removing +//! one is a breaking change. The enum is not `#[non_exhaustive]` because +//! ECHIDNA matches on it exhaustively; downstream code should keep a +//! wildcard arm. + +#![allow(dead_code)] + +use serde::{Deserialize, Serialize}; + +/// Enumeration of all supported provers +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, strum::EnumIter)] +pub enum ProverKind { + // Tier 1: Original + SMT solvers + Agda, + Coq, + Lean, + Isabelle, + Z3, + CVC5, + + // Tier 2: "Big Six" completion + Metamath, + HOLLight, + Mizar, + + // Tier 3: Additional coverage + PVS, + ACL2, + + // Tier 4: Advanced + HOL4, + + // Extended: Additional provers + Idris2, + /// Lean 3 — sibling prover to Lean 4 (not a version of it). + /// mathlib3 preserves a substantial corpus that never fully ported + /// to mathlib4; port-pairs between mathlib3 and mathlib4 give the + /// arbiter ready-made cross-system evidence for the same theorem. + Lean3, + + // Tier 5: First-Order ATPs + Vampire, + EProver, + SPASS, + AltErgo, + + // Tier 5b: Higher-Order ATPs + Leo3, + Satallax, + Lash, + AgsyHOL, + + // Tier 5c: Frontier First-Order ATPs + IProver, + Princess, + Twee, + MetiTarski, + CSI, + AProVE, + + // Tier 5d: Hybrid systems / differential dynamic logic + KeYmaeraX, + + // Tier 5e: Real-algebraic decision (CAD / virtual substitution) + Qepcad, + Redlog, + + // Tier 5f: Connection-method classical / intuitionistic / lean kernel + MleanCoP, + IleanCoP, + NanoCoP, + + // Tier 5g: Tableau-prover generator for arbitrary modal logics + MetTeL2, + + // Tier 5h: Description-logic reasoners (OWL EL / OWL DL). + // ELK is the EL-profile specialist; Konclude handles full SROIQ. + ELK, + Konclude, + + // Tier 5i: Probabilistic model checking (modern PRISM successor). + Storm, + + // Tier 5j: B-method / Event-B model checker. + ProB, + + // Tier 5k: Computational-cryptography proof assistant + // (game-based, interactive). + EasyCrypt, + + // Tier 5l: Computational-cryptography automated prover + // (game-hopping, complementary to EasyCrypt). + CryptoVerif, + + // Tier 6: Dependent types + effects, auto-active, orchestration + FStar, + Dafny, + Why3, + + // Tier 6b: Refinement-types + SPARK auto-active + GNATprove, // SPARK/Ada — Why3 + Z3/CVC5/Alt-Ergo backend + Stainless, // Scala / Inox refinement-types + LiquidHaskell, // GHC plugin refinement-types + + // Tier 7: Specialized / niche + TLAPS, + Twelf, + Nuprl, + Minlog, + Imandra, + + // Tier 8: Constraint solvers + GLPK, + SCIP, + MiniZinc, + Chuffed, + ORTools, + + // Prover oracles (internal structural validators) + TypedWasm, + + // Tier 9: Model checkers and program verifiers + SPIN, + CBMC, + SeaHorn, + + // Tier 9: SAT Solvers + CaDiCaL, + Kissat, + MiniSat, + + // Tier 9: Model checkers (extended) + NuSMV, + TLC, + Alloy, + Prism, + UPPAAL, + + // Tier 9: Program verifiers (deductive) + FramaC, + + // Tier 9: Permission-based program verifiers + Viper, + + // Tier 9: Security protocol verifiers + Tamarin, + ProVerif, + + // Tier 9: Deductive Java verifiers (JavaDL + JML) + KeY, + + // Tier 10: Delta-complete SMT solvers + DReal, + + // Tier 10: Logic synthesis & hardware verification + ABC, + + // Tier 10: GPU kernel verification + /// GPUVerify — verifies CUDA/OpenCL kernels for data races and barrier + /// divergence. Translates GPU kernels to Boogie/BPL then uses Z3/CVC4 + /// as the backend SMT solver. Input: `.cu` (CUDA) or `.cl` (OpenCL). + GPUVerify, + /// Faial — detects data races in GPU parallel kernels via access pattern + /// analysis. Lighter-weight than GPUVerify; focuses on CUDA shared-memory + /// race freedom without a Boogie translation step. + Faial, + + // Tier 11: HP type-checker ecosystem. These dispatch through one + // unified HPEcosystemBackend that routes to the real HP upstreams + // (TypeLL, Katagoria, tropical-resource-typing). They are + // type-discipline views rather than separate binaries. + // + // Exhaustive enumeration of every type discipline we intend to support. + // Adding a variant here is cheap (dispatch-level only); the goal is to + // never have to re-open this enum once the ecosystem grows. See + // `src/rust/disciplines/` for the family grouping and katagoria pipeline. + TypeLL, + KatagoriaVerifier, + TropicalTypeChecker, + ChoreographicTypeChecker, + EpistemicTypeChecker, + EchoTypeChecker, + SessionTypeChecker, + ModalTypeChecker, + QTTTypeChecker, + EffectRowTypeChecker, + DependentTypeChecker, + RefinementTypeChecker, + // Foundations + OrdinaryTypeChecker, + // Polymorphism family + PhantomTypeChecker, + PolymorphicTypeChecker, + ExistentialTypeChecker, + HigherKindedTypeChecker, + RowTypeChecker, + // Subtyping family + SubtypingTypeChecker, + IntersectionTypeChecker, + UnionTypeChecker, + GradualTypeChecker, + // Dependent / refinement family (siblings of Dependent/Refinement) + HoareTypeChecker, + IndexedTypeChecker, + // Substructural family (siblings / specialisations of QTT) + LinearTypeChecker, + AffineTypeChecker, + RelevantTypeChecker, + OrderedTypeChecker, + UniquenessTypeChecker, + // Mutability / capability family + ImmutableTypeChecker, + CapabilityTypeChecker, + BunchedTypeChecker, + // Modal family (siblings of Modal/Epistemic) + TemporalTypeChecker, + ProvabilityTypeChecker, + // Effects / coeffects family (siblings of EffectRow) + ImpureTypeChecker, + CoeffectTypeChecker, + ProbabilisticTypeChecker, + // Process / communication family (siblings of Session/Choreographic/Echo) + DyadicTypeChecker, + // Homotopy foundations + HomotopyTypeChecker, + CubicalTypeChecker, + /// Nominal logic / HOAS / λ-tree syntax dispatcher. Added 2026-04-18 as + /// an honest one-time correction — nominal logic was missed in the + /// original 40-variant exhaustive enumeration. See + /// `src/rust/disciplines/mod.rs :: TypeDiscipline::Nominal` for the + /// full rationale. + NominalTypeChecker, + /// Abella — classical Axis-1 prover for nominal logic / HOAS. + /// Two-level logic (λProlog specification + sequent reasoning with + /// the ∇ generic quantifier). Sibling to Twelf in logical framework + /// style but with distinct proof theory. + Abella, + /// Dedukti — universal λΠ-modulo framework. Already in echidna as + /// a proof-exchange format (`src/rust/exchange/dedukti.rs`); this + /// variant adds the prover-as-solver role (invoking `dkcheck` / + /// `lambdapi` to typecheck a `.dk` source end-to-end). + Dedukti, + /// Cameleer — OCaml front-end for Why3 via GOSPEL contracts. + /// Thin pipeline over Why3's solver fleet; own variant so the + /// OCaml-proofs niche gets its own corpus slot and port-pairs + /// with F*/Dafny are trackable for the arbiter. + Cameleer, + /// ACL2s — sibling dialect to ACL2 with richer type annotations. + /// Different binary, different default libraries, different + /// tactic distributions; separate variant keeps the corpus slot + /// distinct from ACL2 proper. + ACL2s, + /// Isabelle/ZF — Isabelle with Zermelo-Fraenkel set-theory + /// object logic. Same `isabelle` binary as Isabelle/HOL but + /// different session name and stdlib; distinct proof style + /// and theorem namespace warrant a distinct slot. + IsabelleZF, + /// Boogie — intermediate verification language standalone + /// backend. Currently reached via Viper; exposing directly lets + /// echidna consume `.bpl` programs without a Viper wrapper + /// (e.g. Dafny-generated output, Chalice, VCC front-ends). + Boogie, + // Phase 4 "variety" batch (2026-04-18) — from the prover story's + // unique-and-unusual + pure-variety lists. Each genuinely distinct + // from what echidna already covers; skipping Coq-variants + // (Edukera, Bedrock2, CompCert) and F*-libraries (LowStar) since + // those don't warrant new ProverKind slots. + /// Naproche — controlled natural-language (ForTheL) proof checker. + /// Only text-style prover in echidna's roster; token distribution + /// unlike any other. + Naproche, + /// Matita — Bologna's Calculus of Inductive Constructions variant. + /// Coq-adjacent but semantically distinct enough to deserve its + /// own corpus slot. + Matita, + /// Arend — JetBrains's cubical HoTT prover. Distinct from Cubical + /// Agda in having path primitives as first-class syntax and IDE + /// tooling. Co-serves `TypeDiscipline::Cubical`. + Arend, + /// Athena — Arkoudas's denotational-proof-language with + /// intermixed deductive and computational phases. + Athena, + /// λProlog — higher-order logic programming with HOAS (Teyjus / + /// Elpi implementations). Co-serves `TypeDiscipline::Nominal` + /// alongside Abella. + LambdaProlog, + /// Mercury — pure logic programming with static types and modes. + /// Proof-adjacent via termination and determinism proofs. + Mercury, + /// Nitpick — Isabelle-integrated counter-example finder. + /// Produces refutations; corpus records are negative-class data + /// balancing the otherwise positive-only proof corpus. + Nitpick, + /// Nunchaku — standalone model / counter-example finder for HOL. + /// Sibling to Nitpick; same negative-class story but not + /// Isabelle-coupled, wider input format range. + Nunchaku, + /// Cubical Agda — Agda in --cubical mode; HIT, univalence, path types. + CubicalAgda, + /// Zipperposition — first-order + higher-order ATP (TPTP/TSTP output). + Zipperposition, + /// Prover9 — equational/clause-based ATP (McCune); pairs with Mace4. + Prover9, + /// OpenSMT — SMT solver with Craig interpolant generation. + OpenSmt, + /// SMT-RAT — nonlinear arithmetic SMT (NIA/NRA) from RWTH Aachen. + SmtRat, + /// Rocq — the 2024 Coq community rename; detects `rocq` binary first. + Rocq, + /// UPPAAL Stratego — strategy synthesis + stochastic model checking. + UppaalStratego, + /// MizAR — automated reasoning integrated with the Mizar Mathematical Library. + MizAR, +} + +impl ProverKind { + /// True if this kind is served by the unified HP-ecosystem backend. + pub fn is_hp_ecosystem(&self) -> bool { + matches!( + self, + ProverKind::TypeLL + | ProverKind::KatagoriaVerifier + | ProverKind::TropicalTypeChecker + | ProverKind::ChoreographicTypeChecker + | ProverKind::EpistemicTypeChecker + | ProverKind::EchoTypeChecker + | ProverKind::SessionTypeChecker + | ProverKind::ModalTypeChecker + | ProverKind::QTTTypeChecker + | ProverKind::EffectRowTypeChecker + | ProverKind::DependentTypeChecker + | ProverKind::RefinementTypeChecker + | ProverKind::OrdinaryTypeChecker + | ProverKind::PhantomTypeChecker + | ProverKind::PolymorphicTypeChecker + | ProverKind::ExistentialTypeChecker + | ProverKind::HigherKindedTypeChecker + | ProverKind::RowTypeChecker + | ProverKind::SubtypingTypeChecker + | ProverKind::IntersectionTypeChecker + | ProverKind::UnionTypeChecker + | ProverKind::GradualTypeChecker + | ProverKind::HoareTypeChecker + | ProverKind::IndexedTypeChecker + | ProverKind::LinearTypeChecker + | ProverKind::AffineTypeChecker + | ProverKind::RelevantTypeChecker + | ProverKind::OrderedTypeChecker + | ProverKind::UniquenessTypeChecker + | ProverKind::ImmutableTypeChecker + | ProverKind::CapabilityTypeChecker + | ProverKind::BunchedTypeChecker + | ProverKind::TemporalTypeChecker + | ProverKind::ProvabilityTypeChecker + | ProverKind::ImpureTypeChecker + | ProverKind::CoeffectTypeChecker + | ProverKind::ProbabilisticTypeChecker + | ProverKind::DyadicTypeChecker + | ProverKind::HomotopyTypeChecker + | ProverKind::CubicalTypeChecker + | ProverKind::NominalTypeChecker + ) + } +} + +impl std::str::FromStr for ProverKind { + type Err = anyhow::Error; + + fn from_str(s: &str) -> Result { + match s.to_lowercase().as_str() { + "agda" => Ok(ProverKind::Agda), + "coq" => Ok(ProverKind::Coq), + "lean" => Ok(ProverKind::Lean), + "isabelle" => Ok(ProverKind::Isabelle), + "z3" => Ok(ProverKind::Z3), + "cvc5" => Ok(ProverKind::CVC5), + "metamath" => Ok(ProverKind::Metamath), + "hollight" | "hol-light" => Ok(ProverKind::HOLLight), + "mizar" => Ok(ProverKind::Mizar), + "pvs" => Ok(ProverKind::PVS), + "acl2" => Ok(ProverKind::ACL2), + "hol4" => Ok(ProverKind::HOL4), + "idris2" | "idris" => Ok(ProverKind::Idris2), + "lean3" | "lean-3" | "lean3-legacy" | "mathlib3" => Ok(ProverKind::Lean3), + "vampire" => Ok(ProverKind::Vampire), + "eprover" | "e" => Ok(ProverKind::EProver), + "spass" => Ok(ProverKind::SPASS), + "altergo" | "alt-ergo" => Ok(ProverKind::AltErgo), + "leo3" | "leo-iii" | "leo-3" => Ok(ProverKind::Leo3), + "satallax" => Ok(ProverKind::Satallax), + "lash" => Ok(ProverKind::Lash), + "agsyhol" | "agsy-hol" => Ok(ProverKind::AgsyHOL), + "iprover" | "iprover-eq" => Ok(ProverKind::IProver), + "princess" => Ok(ProverKind::Princess), + "twee" => Ok(ProverKind::Twee), + "metitarski" | "metit" => Ok(ProverKind::MetiTarski), + "csi" => Ok(ProverKind::CSI), + "aprove" => Ok(ProverKind::AProVE), + "keymaerax" | "keymaera-x" | "keymaera_x" | "kyx" => Ok(ProverKind::KeYmaeraX), + "qepcad" | "qepcad-b" | "qepcad_b" => Ok(ProverKind::Qepcad), + "redlog" => Ok(ProverKind::Redlog), + "mleancop" | "mlean-cop" | "mlean_cop" => Ok(ProverKind::MleanCoP), + "ileancop" | "ilean-cop" | "ilean_cop" => Ok(ProverKind::IleanCoP), + "nanocop" | "nano-cop" | "nano_cop" => Ok(ProverKind::NanoCoP), + "mettel2" | "mettel-2" | "mettel" => Ok(ProverKind::MetTeL2), + "elk" | "elk-reasoner" => Ok(ProverKind::ELK), + "konclude" => Ok(ProverKind::Konclude), + "storm" | "stormpy" | "storm-checker" => Ok(ProverKind::Storm), + "prob" | "probcli" | "prob-cli" => Ok(ProverKind::ProB), + "easycrypt" | "easy-crypt" | "ec-prover" => Ok(ProverKind::EasyCrypt), + "cryptoverif" | "crypto-verif" | "cryptoverif-prover" => Ok(ProverKind::CryptoVerif), + "fstar" | "f*" | "f-star" => Ok(ProverKind::FStar), + "dafny" => Ok(ProverKind::Dafny), + "why3" => Ok(ProverKind::Why3), + "gnatprove" | "spark" | "ada" => Ok(ProverKind::GNATprove), + "stainless" | "scala-stainless" => Ok(ProverKind::Stainless), + "liquid" | "liquid-haskell" | "liquidhaskell" | "lh" => Ok(ProverKind::LiquidHaskell), + "tlaps" | "tla+" => Ok(ProverKind::TLAPS), + "twelf" => Ok(ProverKind::Twelf), + "nuprl" => Ok(ProverKind::Nuprl), + "minlog" => Ok(ProverKind::Minlog), + "imandra" => Ok(ProverKind::Imandra), + "glpk" => Ok(ProverKind::GLPK), + "scip" => Ok(ProverKind::SCIP), + "minizinc" | "mzn" => Ok(ProverKind::MiniZinc), + "chuffed" => Ok(ProverKind::Chuffed), + "ortools" | "or-tools" => Ok(ProverKind::ORTools), + "typedwasm" | "typed-wasm" | "typed_wasm" | "twasm" => Ok(ProverKind::TypedWasm), + "spin" | "promela" => Ok(ProverKind::SPIN), + "cbmc" | "c-bounded" => Ok(ProverKind::CBMC), + "seahorn" | "sea" | "sea-horn" => Ok(ProverKind::SeaHorn), + "cadical" => Ok(ProverKind::CaDiCaL), + "kissat" => Ok(ProverKind::Kissat), + "minisat" | "mini-sat" => Ok(ProverKind::MiniSat), + "nusmv" | "nuxmv" => Ok(ProverKind::NuSMV), + "tlc" | "tlc2" => Ok(ProverKind::TLC), + "alloy" => Ok(ProverKind::Alloy), + "prism" => Ok(ProverKind::Prism), + "uppaal" | "verifyta" => Ok(ProverKind::UPPAAL), + "framac" | "frama-c" | "frama_c" | "wp" => Ok(ProverKind::FramaC), + "viper" | "silicon" | "carbon" => Ok(ProverKind::Viper), + "tamarin" | "tamarin-prover" | "spthy" => Ok(ProverKind::Tamarin), + "proverif" | "pv" => Ok(ProverKind::ProVerif), + "key" | "key-project" | "javadl" => Ok(ProverKind::KeY), + "dreal" | "d-real" | "dreal4" => Ok(ProverKind::DReal), + "abc" | "berkeley-abc" => Ok(ProverKind::ABC), + "gpuverify" | "gpu-verify" | "gpu_verify" => Ok(ProverKind::GPUVerify), + "faial" | "faial-drf" => Ok(ProverKind::Faial), + "typell" | "type-ll" | "typell-kernel" => Ok(ProverKind::TypeLL), + "katagoria" | "katagoriaverifier" | "katagoria-verifier" => { + Ok(ProverKind::KatagoriaVerifier) + }, + "tropicaltypechecker" | "tropical" | "tropical-type-checker" => { + Ok(ProverKind::TropicalTypeChecker) + }, + "choreographictypechecker" | "choreographic" => { + Ok(ProverKind::ChoreographicTypeChecker) + }, + "epistemictypechecker" | "epistemic" => Ok(ProverKind::EpistemicTypeChecker), + "echotypechecker" | "echo" => Ok(ProverKind::EchoTypeChecker), + "sessiontypechecker" | "session" => Ok(ProverKind::SessionTypeChecker), + "modaltypechecker" | "modal" => Ok(ProverKind::ModalTypeChecker), + "qtttypechecker" | "qtt" | "quantitative" => Ok(ProverKind::QTTTypeChecker), + "effectrowtypechecker" | "effect-row" | "effectrow" => { + Ok(ProverKind::EffectRowTypeChecker) + }, + "dependenttypechecker" | "dependent" => Ok(ProverKind::DependentTypeChecker), + "refinementtypechecker" | "refinement" => Ok(ProverKind::RefinementTypeChecker), + "ordinarytypechecker" | "ordinary" | "simple" | "simply-typed" | "stlc" => { + Ok(ProverKind::OrdinaryTypeChecker) + }, + "phantomtypechecker" | "phantom" => Ok(ProverKind::PhantomTypeChecker), + "polymorphictypechecker" | "polymorphic" | "systemf" | "system-f" | "parametric" => { + Ok(ProverKind::PolymorphicTypeChecker) + }, + "existentialtypechecker" | "existential" | "packed" => { + Ok(ProverKind::ExistentialTypeChecker) + }, + "higherkindedtypechecker" | "higher-kinded" | "higherkinded" | "hkt" | "hk" => { + Ok(ProverKind::HigherKindedTypeChecker) + }, + "rowtypechecker" | "row" | "row-polymorphic" | "row-polymorphism" => { + Ok(ProverKind::RowTypeChecker) + }, + "subtypingtypechecker" | "subtyping" | "sub" => Ok(ProverKind::SubtypingTypeChecker), + "intersectiontypechecker" | "intersection" | "inter" => { + Ok(ProverKind::IntersectionTypeChecker) + }, + "uniontypechecker" | "union" => Ok(ProverKind::UnionTypeChecker), + "gradualtypechecker" | "gradual" | "gradual-typing" => { + Ok(ProverKind::GradualTypeChecker) + }, + "hoaretypechecker" | "hoare" | "hoare-types" => Ok(ProverKind::HoareTypeChecker), + "indexedtypechecker" | "indexed" | "indexed-monad" | "indexed-monads" => { + Ok(ProverKind::IndexedTypeChecker) + }, + "lineartypechecker" | "linear" | "linear-types" => Ok(ProverKind::LinearTypeChecker), + "affinetypechecker" | "affine" | "affine-types" => Ok(ProverKind::AffineTypeChecker), + "relevanttypechecker" | "relevant" | "relevant-types" => { + Ok(ProverKind::RelevantTypeChecker) + }, + "orderedtypechecker" | "ordered" | "ordered-logic" | "no-exchange" => { + Ok(ProverKind::OrderedTypeChecker) + }, + "uniquenesstypechecker" | "uniqueness" | "unique" | "unique-types" => { + Ok(ProverKind::UniquenessTypeChecker) + }, + "immutabletypechecker" | "immutable" | "frozen" | "const-types" => { + Ok(ProverKind::ImmutableTypeChecker) + }, + "capabilitytypechecker" | "capability" | "cap" | "capability-types" => { + Ok(ProverKind::CapabilityTypeChecker) + }, + "bunchedtypechecker" | "bunched" | "bi" | "bi-logic" | "separation" => { + Ok(ProverKind::BunchedTypeChecker) + }, + "temporaltypechecker" | "temporal" | "ltl" | "ctl" => { + Ok(ProverKind::TemporalTypeChecker) + }, + "provabilitytypechecker" | "provability" | "lob" | "löb" | "gl" => { + Ok(ProverKind::ProvabilityTypeChecker) + }, + "impuretypechecker" | "impure" | "effect-tracked" => Ok(ProverKind::ImpureTypeChecker), + "coeffecttypechecker" | "coeffect" | "graded-context" | "coeffects" => { + Ok(ProverKind::CoeffectTypeChecker) + }, + "probabilistictypechecker" | "probabilistic" | "prob-types" => { + Ok(ProverKind::ProbabilisticTypeChecker) + }, + "dyadictypechecker" | "dyadic" | "binary-channel" | "dyadic-session" => { + Ok(ProverKind::DyadicTypeChecker) + }, + "homotopytypechecker" | "homotopy" | "hott" => Ok(ProverKind::HomotopyTypeChecker), + "cubicaltypechecker" | "cubical" | "cubical-tt" => Ok(ProverKind::CubicalTypeChecker), + "nominaltypechecker" | "nominal" | "hoas" | "lambda-tree" => { + Ok(ProverKind::NominalTypeChecker) + }, + "abella" => Ok(ProverKind::Abella), + "dedukti" | "dkcheck" | "lambdapi" => Ok(ProverKind::Dedukti), + "cameleer" | "gospel" => Ok(ProverKind::Cameleer), + "acl2s" | "acl2-s" => Ok(ProverKind::ACL2s), + "isabellezf" | "isabelle-zf" | "isabelle/zf" | "zf" => Ok(ProverKind::IsabelleZF), + "boogie" | "bpl" => Ok(ProverKind::Boogie), + "naproche" | "forthel" | "ftl" => Ok(ProverKind::Naproche), + "matita" => Ok(ProverKind::Matita), + "arend" => Ok(ProverKind::Arend), + "athena" => Ok(ProverKind::Athena), + "lambdaprolog" | "lambda-prolog" | "teyjus" | "elpi" => Ok(ProverKind::LambdaProlog), + "mercury" | "mmc" => Ok(ProverKind::Mercury), + "nitpick" => Ok(ProverKind::Nitpick), + "nunchaku" => Ok(ProverKind::Nunchaku), + "cubicalagda" | "cubical-agda" | "agda-cubical" => Ok(ProverKind::CubicalAgda), + "zipperposition" => Ok(ProverKind::Zipperposition), + "prover9" => Ok(ProverKind::Prover9), + "opensmt" | "open-smt" => Ok(ProverKind::OpenSmt), + "smtrat" | "smt-rat" => Ok(ProverKind::SmtRat), + "rocq" | "rocq-compile" => Ok(ProverKind::Rocq), + "uppaal-stratego" | "stratego" => Ok(ProverKind::UppaalStratego), + "mizar-ar" | "mizatp" | "mizar-atp" => Ok(ProverKind::MizAR), + _ => Err(anyhow::anyhow!("Unknown prover: {}", s)), + } + } +} + +impl std::fmt::Display for ProverKind { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "{:?}", self) + } +} + +impl ProverKind { + /// All core provers for 1.0 (12 total) + pub fn all_core() -> Vec { + vec![ + ProverKind::Agda, + ProverKind::Coq, + ProverKind::Lean, + ProverKind::Isabelle, + ProverKind::Z3, + ProverKind::CVC5, + ProverKind::Metamath, + ProverKind::HOLLight, + ProverKind::Mizar, + ProverKind::PVS, + ProverKind::ACL2, + ProverKind::HOL4, + ] + } + + /// All provers including extended coverage + pub fn all() -> Vec { + let mut provers = Self::all_core(); + provers.extend_from_slice(&[ + ProverKind::Idris2, + ProverKind::Lean3, + ProverKind::Vampire, + ProverKind::EProver, + ProverKind::SPASS, + ProverKind::AltErgo, + ProverKind::FStar, + ProverKind::Dafny, + ProverKind::Why3, + ProverKind::TLAPS, + ProverKind::Twelf, + ProverKind::Nuprl, + ProverKind::Minlog, + ProverKind::Imandra, + ProverKind::GLPK, + ProverKind::SCIP, + ProverKind::MiniZinc, + ProverKind::Chuffed, + ProverKind::ORTools, + ProverKind::TypedWasm, + ProverKind::SPIN, + ProverKind::CBMC, + ProverKind::SeaHorn, + ProverKind::CaDiCaL, + ProverKind::Kissat, + ProverKind::MiniSat, + ProverKind::NuSMV, + ProverKind::TLC, + ProverKind::Alloy, + ProverKind::Prism, + ProverKind::UPPAAL, + ProverKind::FramaC, + ProverKind::Viper, + ProverKind::Tamarin, + ProverKind::ProVerif, + ProverKind::KeY, + ProverKind::DReal, + ProverKind::ABC, + ProverKind::GPUVerify, + ProverKind::Faial, + ProverKind::CubicalAgda, + ProverKind::Zipperposition, + ProverKind::Prover9, + ProverKind::OpenSmt, + ProverKind::SmtRat, + ProverKind::Rocq, + ProverKind::UppaalStratego, + ProverKind::MizAR, + ProverKind::IProver, + ProverKind::Princess, + ProverKind::Twee, + ProverKind::MetiTarski, + ProverKind::CSI, + ProverKind::AProVE, + ProverKind::KeYmaeraX, + ProverKind::Qepcad, + ProverKind::Redlog, + ProverKind::MleanCoP, + ProverKind::IleanCoP, + ProverKind::NanoCoP, + ProverKind::MetTeL2, + ProverKind::ELK, + ProverKind::Konclude, + ProverKind::Storm, + ProverKind::ProB, + ProverKind::EasyCrypt, + ProverKind::CryptoVerif, + ]); + provers + } + + /// Get complexity rating (1-5, lower is easier) + pub fn complexity(&self) -> u8 { + match self { + ProverKind::Metamath => 2, + ProverKind::Agda => 3, + ProverKind::HOLLight => 3, + ProverKind::Mizar => 3, + ProverKind::Lean => 3, + ProverKind::Coq => 3, + ProverKind::Isabelle => 4, + ProverKind::Z3 => 2, + ProverKind::CVC5 => 2, + ProverKind::PVS => 4, + ProverKind::ACL2 => 4, + ProverKind::HOL4 => 5, + ProverKind::Idris2 => 3, + ProverKind::Lean3 => 3, // Same complexity as Lean 4. + ProverKind::Abella => 3, // Two-level logic, HOAS proof state. + ProverKind::Dedukti => 3, // λΠ-modulo framework. + ProverKind::Cameleer => 2, // Thin OCaml→Why3 pipeline. + ProverKind::ACL2s => 4, // Sibling to ACL2. + ProverKind::IsabelleZF => 4, // Sibling to Isabelle/HOL. + ProverKind::Boogie => 2, // Intermediate verification language. + ProverKind::Naproche => 3, // Controlled-NL parsing non-trivial. + ProverKind::Matita => 3, // CIC variant, same family as Coq. + ProverKind::Arend => 3, // Cubical HoTT. + ProverKind::Athena => 4, // Denotational + rewriting engine. + ProverKind::LambdaProlog => 3, // HOAS logic programming. + ProverKind::Mercury => 3, // Logic programming with types/modes. + ProverKind::Nitpick => 2, // Isabelle-wrapped counter-example finder. + ProverKind::Nunchaku => 2, // Standalone counter-example finder. + ProverKind::CubicalAgda => 4, // Cubical HoTT; harder than plain Agda. + ProverKind::Zipperposition => 2, // Automated ATP. + ProverKind::Prover9 => 2, // Classic equational ATP. + ProverKind::OpenSmt => 2, // SMT solver. + ProverKind::SmtRat => 3, // Nonlinear arithmetic needs careful encoding. + ProverKind::Rocq => 3, // Same as Coq. + ProverKind::UppaalStratego => 4, // Strategy synthesis is hard. + ProverKind::MizAR => 3, // Mizar with ATP assist. + ProverKind::Vampire => 2, // Automated, relatively simple + ProverKind::EProver => 2, // Similar to Vampire + ProverKind::SPASS => 2, // Automated FOL + ProverKind::AltErgo => 2, // SMT + FOL + + ProverKind::FStar => 3, // Dependent types + effects + ProverKind::Dafny => 2, // Auto-active + ProverKind::Why3 => 3, // Multi-prover orchestration + ProverKind::GNATprove => 3, // SPARK auto-active via Why3 backends + ProverKind::Stainless => 3, // Scala/Inox refinement types + ProverKind::LiquidHaskell => 3, // GHC plugin refinement types + ProverKind::TLAPS => 4, // TLA+ proof system + ProverKind::Twelf => 4, // Logical framework + ProverKind::Nuprl => 4, // Constructive type theory + ProverKind::Minlog => 4, // Minimal logic + ProverKind::Imandra => 3, // ML-based reasoning + ProverKind::GLPK => 2, // LP solver + ProverKind::SCIP => 3, // MINLP solver + ProverKind::MiniZinc => 2, // Constraint modelling + ProverKind::Chuffed => 2, // CP solver + ProverKind::ORTools => 2, // Constraint/optimization solver + ProverKind::TypedWasm => 3, // Internal oracle, structural analysis + ProverKind::SPIN => 3, // Model checker, Promela language + ProverKind::CBMC => 2, // Bounded model checker, C input + ProverKind::SeaHorn => 2, // LLVM-based verifier, abstract interpretation + CHC + ProverKind::CaDiCaL => 1, // SAT solver, DIMACS CNF + ProverKind::Kissat => 1, // SAT solver, DIMACS CNF + ProverKind::MiniSat => 1, // SAT solver, DIMACS CNF + ProverKind::NuSMV => 3, // Symbolic model checker, SMV language + ProverKind::TLC => 3, // TLA+ model checker + ProverKind::Alloy => 3, // Relational model finder + ProverKind::Prism => 3, // Probabilistic model checker + ProverKind::UPPAAL => 3, // Timed automata model checker + ProverKind::FramaC => 3, // Deductive C verifier (ACSL + WP) + ProverKind::Viper => 3, // Permission-based verifier (Silver + Silicon/Carbon) + ProverKind::Tamarin => 3, // Security protocol verifier, multiset rewriting + ProverKind::ProVerif => 2, // Automated protocol verifier, applied pi-calculus + ProverKind::KeY => 3, // Deductive Java verifier (JavaDL + JML), auto + interactive + ProverKind::DReal => 2, // Automated delta-complete SMT solver, NRA + ProverKind::ABC => 2, // Automated hardware verification, AIG-based + ProverKind::GPUVerify => 2, // Automated GPU kernel verifier (Boogie/Z3 backend) + ProverKind::Faial => 2, // Lightweight GPU race detector (access pattern analysis) + // Phase 1a: Higher-order ATPs + ProverKind::Leo3 => 3, // Leo III HOL-to-TPTP translator + ATP + ProverKind::Satallax => 3, // Satallax HOL-based ATP + ProverKind::Lash => 3, // Lash higher-order prover + ProverKind::AgsyHOL => 4, // Agsy HOL dependent-type prover + // Phase 1b: Frontier first-order provers + ProverKind::IProver => 2, // Competitive ATP, standard FOL + ProverKind::Princess => 3, // LA-extended ATP + ProverKind::Twee => 2, // Equational only, deterministic + ProverKind::MetiTarski => 3, // Transcendental function encoding + ProverKind::CSI => 3, // TRS/CTRS parsing + CPF output + ProverKind::AProVE => 3, // TRS/XTC parsing + ProverKind::KeYmaeraX => 4, // dL + hybrid programs + tactic language + ProverKind::Qepcad => 4, // CAD doubly-exponential in variable count + ProverKind::Redlog => 3, // virtual substitution + CAD + ProverKind::MleanCoP => 3, // classical connection-method + equality + ProverKind::IleanCoP => 3, // intuitionistic connection-method + ProverKind::NanoCoP => 3, // small-kernel connection-method + ProverKind::MetTeL2 => 4, // JVM tableau-generator + spec config + // Phase 4: DL + probabilistic + B-method + computational crypto + ProverKind::ELK => 3, // consequence-based EL kernel + ProverKind::Konclude => 4, // full SROIQ tableau saturation + ProverKind::Storm => 3, // numerical fixed-point computation + ProverKind::ProB => 3, // B-method semantics + constraint engine + ProverKind::EasyCrypt => 4, // probabilistic relational HL + tactics + ProverKind::CryptoVerif => 4, // game-hopping + indistinguishability lib + // HP type-checker ecosystem: complexity 3 — they are real + // type-checkers with non-trivial unification/elaboration. + // Heavier disciplines (HoTT/Cubical, Hoare) rate 4. + ProverKind::TypeLL + | ProverKind::KatagoriaVerifier + | ProverKind::TropicalTypeChecker + | ProverKind::ChoreographicTypeChecker + | ProverKind::EpistemicTypeChecker + | ProverKind::EchoTypeChecker + | ProverKind::SessionTypeChecker + | ProverKind::ModalTypeChecker + | ProverKind::QTTTypeChecker + | ProverKind::EffectRowTypeChecker + | ProverKind::DependentTypeChecker + | ProverKind::RefinementTypeChecker + | ProverKind::PhantomTypeChecker + | ProverKind::PolymorphicTypeChecker + | ProverKind::ExistentialTypeChecker + | ProverKind::HigherKindedTypeChecker + | ProverKind::RowTypeChecker + | ProverKind::SubtypingTypeChecker + | ProverKind::IntersectionTypeChecker + | ProverKind::UnionTypeChecker + | ProverKind::GradualTypeChecker + | ProverKind::IndexedTypeChecker + | ProverKind::LinearTypeChecker + | ProverKind::AffineTypeChecker + | ProverKind::RelevantTypeChecker + | ProverKind::OrderedTypeChecker + | ProverKind::UniquenessTypeChecker + | ProverKind::ImmutableTypeChecker + | ProverKind::CapabilityTypeChecker + | ProverKind::BunchedTypeChecker + | ProverKind::TemporalTypeChecker + | ProverKind::ProvabilityTypeChecker + | ProverKind::ImpureTypeChecker + | ProverKind::CoeffectTypeChecker + | ProverKind::ProbabilisticTypeChecker + | ProverKind::DyadicTypeChecker => 3, + // Heavier disciplines: Hoare triples (SL proofs), HoTT (univalence), + // Cubical (interval primitives). + ProverKind::HoareTypeChecker + | ProverKind::HomotopyTypeChecker + | ProverKind::CubicalTypeChecker + | ProverKind::NominalTypeChecker => 4, + // Baseline: simply-typed lambda calculus — cheap to check. + ProverKind::OrdinaryTypeChecker => 2, + } + } + + /// Get tier (1-5) + pub fn tier(&self) -> u8 { + match self { + ProverKind::Agda + | ProverKind::Coq + | ProverKind::Lean + | ProverKind::Isabelle + | ProverKind::Z3 + | ProverKind::CVC5 => 1, + + ProverKind::Metamath | ProverKind::HOLLight | ProverKind::Mizar => 2, + + ProverKind::PVS | ProverKind::ACL2 => 3, + + ProverKind::HOL4 => 4, + + // Extended tier (same as Tier 1 in capability) + ProverKind::Idris2 => 1, + ProverKind::Lean3 => 1, // Sibling to Lean 4. + // Tier 7 niche: specialized proof framework for HOAS / nominal. + ProverKind::Abella => 2, + ProverKind::Dedukti => 2, // Logical framework tier. + ProverKind::Cameleer => 2, // Auto-active via Why3. + ProverKind::ACL2s => 3, // Sibling to ACL2 (tier 3). + ProverKind::IsabelleZF => 1, // Sibling to Isabelle (tier 1). + ProverKind::Boogie => 5, // Deductive program verifier tier. + ProverKind::Naproche => 2, // Specialised, text-style. + ProverKind::Matita => 1, // Coq-adjacent, Tier 1 capability. + ProverKind::Arend => 1, // Cubical HoTT, Tier 1. + ProverKind::Athena => 4, // Niche framework. + ProverKind::LambdaProlog => 4, // Logical framework / HOAS. + ProverKind::Mercury => 4, // Specialised logic programming. + ProverKind::Nitpick => 5, // Counter-example finder tier. + ProverKind::Nunchaku => 5, // Counter-example finder tier. + ProverKind::CubicalAgda => 2, // Tier 2: HoTT proof assistant. + ProverKind::Zipperposition => 3, // Tier 3: HO-ATP. + ProverKind::Prover9 => 4, // Tier 4: classic ATP. + ProverKind::OpenSmt => 3, // Tier 3: interpolant SMT. + ProverKind::SmtRat => 5, // Tier 5: research NL SMT. + ProverKind::Rocq => 1, // Tier 1: Coq rename. + ProverKind::UppaalStratego => 4, // Tier 4: strategy synthesis. + ProverKind::MizAR => 3, // Tier 3: ATP-assisted Mizar. + + // Tier 5: First-Order ATPs + ProverKind::Vampire => 5, + ProverKind::EProver => 5, + ProverKind::SPASS => 5, + ProverKind::AltErgo => 5, + + // Tier 6: Dependent types + effects, auto-active + ProverKind::FStar => 1, // Small kernel, dependent types + ProverKind::Dafny => 2, // Auto-active (relies on Boogie->Z3) + ProverKind::Why3 => 2, // Multi-prover orchestration + ProverKind::GNATprove => 4, // SPARK — small-kernel via Why3 + ProverKind::Stainless => 3, // Scala refinement types + ProverKind::LiquidHaskell => 3, // GHC refinement types + + // Tier 7: Specialized / niche + ProverKind::TLAPS => 2, + ProverKind::Twelf => 4, + ProverKind::Nuprl => 4, + ProverKind::Minlog => 4, + ProverKind::Imandra => 2, + + // Tier 8: Constraint solvers + ProverKind::GLPK => 5, + ProverKind::SCIP => 5, + ProverKind::MiniZinc => 5, + ProverKind::Chuffed => 5, + ProverKind::ORTools => 5, + ProverKind::TypedWasm => 1, // Internal oracle, tier 1 capability + + // Tier 9: Model checkers and program verifiers + ProverKind::SPIN => 5, + ProverKind::CBMC => 5, + ProverKind::SeaHorn => 5, + + // Tier 9: SAT Solvers + ProverKind::CaDiCaL => 5, + ProverKind::Kissat => 5, + ProverKind::MiniSat => 5, + + // Tier 9: Model checkers (extended) + ProverKind::NuSMV => 5, + ProverKind::TLC => 5, + ProverKind::Alloy => 5, + ProverKind::Prism => 5, + ProverKind::UPPAAL => 5, + ProverKind::FramaC => 5, // Deductive program verifier + ProverKind::Viper => 5, // Permission-based program verifier + ProverKind::Tamarin => 5, // Security protocol verifier + ProverKind::ProVerif => 5, // Security protocol verifier (automated) + ProverKind::KeY => 5, // Deductive Java verifier + ProverKind::DReal => 5, // Delta-complete SMT solver (NRA/ODE) + ProverKind::ABC => 5, // Logic synthesis & hardware verification + ProverKind::GPUVerify => 5, // GPU kernel verifier (CUDA/OpenCL → Boogie → Z3) + ProverKind::Faial => 5, // Lightweight GPU data-race detector + // Phase 1a: Higher-order ATPs + ProverKind::Leo3 => 5, // Tier 5: HOL-to-TPTP translator + ProverKind::Satallax => 5, // Tier 5: HOL-based ATP + ProverKind::Lash => 5, // Tier 5: higher-order ATP + ProverKind::AgsyHOL => 5, // Tier 5: HOL dependent-type prover + // Phase 1b: Frontier first-order provers + ProverKind::IProver => 2, // Trust tier 2 (TPTP FOL) + ProverKind::Princess => 2, // Trust tier 2 (TPTP + LA) + ProverKind::Twee => 3, // Trust tier 3 (deterministic equational) + ProverKind::MetiTarski => 2, // Trust tier 2 (TPTP + transcendental) + ProverKind::CSI => 2, // Trust tier 2 (TRS/CPF) + ProverKind::AProVE => 2, // Trust tier 2 (TRS/XTC) + ProverKind::KeYmaeraX => 2, // Trust tier 2 (dL; QE delegated to external CAS) + ProverKind::Qepcad => 2, // Trust tier 2 (CAD; no machine-checked certificate) + ProverKind::Redlog => 2, // Trust tier 2 (parallel to QEPCAD) + ProverKind::MleanCoP => 2, // Trust tier 2 (classical leanCoP kernel) + ProverKind::IleanCoP => 3, // Trust tier 3 (intuitionistic kernel; small + checkable) + ProverKind::NanoCoP => 3, // Trust tier 3 (small kernel — Level-4 cohort) + ProverKind::MetTeL2 => 2, // Trust tier 2 (generated tableau correct by construction; spec unverified) + // Phase 4: DL + probabilistic + B-method + computational crypto. + ProverKind::ELK => 3, // Trust tier 3 (consequence-based, peer-reviewed soundness) + ProverKind::Konclude => 3, // Trust tier 3 (peer-reviewed tableau kernel) + ProverKind::Storm => 2, // Trust tier 2 (DD/symbolic engines, no certificate) + ProverKind::ProB => 2, // Trust tier 2 (constraint-based BMC, validated for railway) + ProverKind::EasyCrypt => 3, // Trust tier 3 (small kernel + Why3/SMT for VC discharge) + ProverKind::CryptoVerif => 3, // Trust tier 3 (small game-hopping engine, peer-reviewed) + // HP ecosystem — tier 11 (beyond the existing 10-tier scheme + // but placed as 3 here to share the ML guidance budget with + // dependent/interactive provers). + ProverKind::TypeLL + | ProverKind::KatagoriaVerifier + | ProverKind::TropicalTypeChecker + | ProverKind::ChoreographicTypeChecker + | ProverKind::EpistemicTypeChecker + | ProverKind::EchoTypeChecker + | ProverKind::SessionTypeChecker + | ProverKind::ModalTypeChecker + | ProverKind::QTTTypeChecker + | ProverKind::EffectRowTypeChecker + | ProverKind::DependentTypeChecker + | ProverKind::RefinementTypeChecker + | ProverKind::OrdinaryTypeChecker + | ProverKind::PhantomTypeChecker + | ProverKind::PolymorphicTypeChecker + | ProverKind::ExistentialTypeChecker + | ProverKind::HigherKindedTypeChecker + | ProverKind::RowTypeChecker + | ProverKind::SubtypingTypeChecker + | ProverKind::IntersectionTypeChecker + | ProverKind::UnionTypeChecker + | ProverKind::GradualTypeChecker + | ProverKind::HoareTypeChecker + | ProverKind::IndexedTypeChecker + | ProverKind::LinearTypeChecker + | ProverKind::AffineTypeChecker + | ProverKind::RelevantTypeChecker + | ProverKind::OrderedTypeChecker + | ProverKind::UniquenessTypeChecker + | ProverKind::ImmutableTypeChecker + | ProverKind::CapabilityTypeChecker + | ProverKind::BunchedTypeChecker + | ProverKind::TemporalTypeChecker + | ProverKind::ProvabilityTypeChecker + | ProverKind::ImpureTypeChecker + | ProverKind::CoeffectTypeChecker + | ProverKind::ProbabilisticTypeChecker + | ProverKind::DyadicTypeChecker + | ProverKind::HomotopyTypeChecker + | ProverKind::CubicalTypeChecker + | ProverKind::NominalTypeChecker => 3, + } + } + + /// Get expected implementation time in weeks + pub fn implementation_time(&self) -> f32 { + match self { + ProverKind::Metamath => 1.5, + ProverKind::Z3 | ProverKind::CVC5 => 1.0, + ProverKind::HOLLight | ProverKind::Mizar => 2.0, + ProverKind::Agda | ProverKind::Lean | ProverKind::Coq => 2.5, + ProverKind::Isabelle => 3.0, + ProverKind::PVS | ProverKind::ACL2 => 3.5, + ProverKind::HOL4 => 4.0, + ProverKind::Idris2 => 2.5, + ProverKind::Lean3 => 1.0, // Thin fork of Lean 4 backend. + ProverKind::Abella => 2.0, // New parser, HOAS proof state model. + ProverKind::Dedukti => 1.5, // Extends existing exchange module. + ProverKind::Cameleer => 1.0, // Thin wrapper over Why3. + ProverKind::ACL2s => 1.0, // Thin fork of ACL2. + ProverKind::IsabelleZF => 1.0, // Thin variant of Isabelle. + ProverKind::Boogie => 1.5, // Extract from Viper internals. + ProverKind::Naproche => 2.0, // Controlled-NL parser wrapper. + ProverKind::Matita => 2.0, // Coq-parser fork. + ProverKind::Arend => 2.0, // Cubical parser + elaborator. + ProverKind::Athena => 2.5, // Rich denotational framework. + ProverKind::LambdaProlog => 2.0, // HOAS parser + unifier. + ProverKind::Mercury => 2.0, // Logic programming interpreter bridge. + ProverKind::Nitpick => 1.0, // Thin wrapper over Isabelle. + ProverKind::Nunchaku => 1.5, // Standalone counter-example tool. + ProverKind::CubicalAgda => 2.5, // Thin fork of Agda backend. + ProverKind::Zipperposition => 1.5, // TSTP-output ATP. + ProverKind::Prover9 => 1.5, // Simple output parsing. + ProverKind::OpenSmt => 1.5, // SMT-LIB2 like CVC5. + ProverKind::SmtRat => 1.5, // Same pattern. + ProverKind::Rocq => 1.0, // Alias for Coq. + ProverKind::UppaalStratego => 2.0, // Fork of UPPAAL backend. + ProverKind::MizAR => 2.0, // Mizar ATP integration. + ProverKind::Vampire => 1.5, // Automated, TPTP format + ProverKind::EProver => 1.5, // Similar to Vampire + ProverKind::SPASS => 1.5, // DFG format + ProverKind::AltErgo => 1.5, // Native format + + ProverKind::FStar => 2.5, // Dependent types + effects + ProverKind::Dafny => 2.0, // Auto-active, Boogie pipeline + ProverKind::Why3 => 2.0, // Multi-prover + ProverKind::GNATprove => 3.0, // SPARK toolchain wrapping + ProverKind::Stainless => 2.5, // Scala JVM + ProverKind::LiquidHaskell => 2.5, // GHC plugin + ProverKind::TLAPS => 2.5, // TLA+ specific + ProverKind::Twelf => 3.0, // LF framework + ProverKind::Nuprl => 3.0, // Constructive type theory + ProverKind::Minlog => 2.5, // Minimal logic + ProverKind::Imandra => 2.0, // ML-based + ProverKind::GLPK => 1.0, // LP API + ProverKind::SCIP => 1.5, // MINLP API + ProverKind::MiniZinc => 1.0, // Constraint modelling + ProverKind::Chuffed => 1.0, // CP solver + ProverKind::ORTools => 1.5, // Constraint/optimization + ProverKind::TypedWasm => 2.0, // Internal oracle + ProverKind::SPIN => 1.5, // Model checker + ProverKind::CBMC => 1.5, // Bounded model checker + ProverKind::SeaHorn => 1.5, // LLVM-based CHC verifier + ProverKind::CaDiCaL => 1.0, // SAT solver, DIMACS CNF + ProverKind::Kissat => 1.0, // SAT solver, DIMACS CNF + ProverKind::MiniSat => 1.0, // SAT solver, DIMACS CNF + ProverKind::NuSMV => 1.5, // Symbolic model checker + ProverKind::TLC => 1.5, // TLA+ model checker + ProverKind::Alloy => 1.5, // Relational model finder + ProverKind::Prism => 1.5, // Probabilistic model checker + ProverKind::UPPAAL => 1.5, // Timed automata model checker + ProverKind::FramaC => 1.5, // Deductive C verifier + ProverKind::Viper => 2.0, // Permission-based verifier (Silver + two backends) + ProverKind::Tamarin => 2.0, // Security protocol verifier (.spthy) + ProverKind::ProVerif => 1.5, // Automated protocol verifier (.pv) + ProverKind::KeY => 2.0, // Deductive Java verifier (JavaDL + JML) + ProverKind::DReal => 1.0, // Automated SMT solver, SMT-LIB input + ProverKind::ABC => 1.5, // Hardware verification, AIGER/BLIF input + ProverKind::GPUVerify => 1.5, // GPU kernel verifier, CUDA/OpenCL input + ProverKind::Faial => 1.0, // Lightweight GPU race detector, CUDA input + ProverKind::IProver => 1.5, // First-order ATP with SZS output + ProverKind::Princess => 1.5, // SMT-based first-order solver + ProverKind::Twee => 1.5, // Equational logic (Knuth-Bendix) + ProverKind::MetiTarski => 1.5, // Transcendental arithmetic extension + ProverKind::CSI => 2.0, // Confluence/termination checker + ProverKind::AProVE => 2.0, // Automated termination verifier + ProverKind::KeYmaeraX => 2.5, // Hybrid systems / differential dynamic logic + ProverKind::Qepcad => 2.5, // CAD / real quantifier elimination + ProverKind::Redlog => 2.0, // REDUCE-CAS QE frontend + ProverKind::MleanCoP => 1.5, // Classical connection-method + ProverKind::IleanCoP => 2.0, // Intuitionistic connection-method + ProverKind::NanoCoP => 1.5, // Lean-kernel connection-method + ProverKind::MetTeL2 => 2.5, // Modal-logic tableau generator + // Phase 4: DL + probabilistic + B-method + computational crypto. + ProverKind::ELK => 1.5, // OWL EL classifier + ProverKind::Konclude => 2.0, // OWL DL tableau reasoner + ProverKind::Storm => 2.0, // Probabilistic model checker (PRISM successor) + ProverKind::ProB => 2.0, // B-method / Event-B model checker + ProverKind::EasyCrypt => 2.5, // Game-based crypto proofs + ProverKind::CryptoVerif => 2.5, // Automated computational-crypto prover + ProverKind::Leo3 => 2.5, // Higher-order ATP + ProverKind::Satallax => 2.5, // Higher-order ATP + ProverKind::Lash => 2.5, // Higher-order ATP + ProverKind::AgsyHOL => 2.5, // Higher-order ATP + ProverKind::TypeLL + | ProverKind::KatagoriaVerifier + | ProverKind::TropicalTypeChecker + | ProverKind::ChoreographicTypeChecker + | ProverKind::EpistemicTypeChecker + | ProverKind::EchoTypeChecker + | ProverKind::SessionTypeChecker + | ProverKind::ModalTypeChecker + | ProverKind::QTTTypeChecker + | ProverKind::EffectRowTypeChecker + | ProverKind::DependentTypeChecker + | ProverKind::RefinementTypeChecker + | ProverKind::OrdinaryTypeChecker + | ProverKind::PhantomTypeChecker + | ProverKind::PolymorphicTypeChecker + | ProverKind::ExistentialTypeChecker + | ProverKind::HigherKindedTypeChecker + | ProverKind::RowTypeChecker + | ProverKind::SubtypingTypeChecker + | ProverKind::IntersectionTypeChecker + | ProverKind::UnionTypeChecker + | ProverKind::GradualTypeChecker + | ProverKind::HoareTypeChecker + | ProverKind::IndexedTypeChecker + | ProverKind::LinearTypeChecker + | ProverKind::AffineTypeChecker + | ProverKind::RelevantTypeChecker + | ProverKind::OrderedTypeChecker + | ProverKind::UniquenessTypeChecker + | ProverKind::ImmutableTypeChecker + | ProverKind::CapabilityTypeChecker + | ProverKind::BunchedTypeChecker + | ProverKind::TemporalTypeChecker + | ProverKind::ProvabilityTypeChecker + | ProverKind::ImpureTypeChecker + | ProverKind::CoeffectTypeChecker + | ProverKind::ProbabilisticTypeChecker + | ProverKind::DyadicTypeChecker + | ProverKind::HomotopyTypeChecker + | ProverKind::CubicalTypeChecker + | ProverKind::NominalTypeChecker => 2.0, // HP ecosystem + } + } + + /// Default executable name for this prover (what to look for on PATH) + pub fn default_executable(&self) -> &'static str { + match self { + ProverKind::Agda => "agda", + ProverKind::Coq => "coqc", + ProverKind::Lean => "lean", + ProverKind::Isabelle => "isabelle", + ProverKind::Z3 => "z3", + ProverKind::CVC5 => "cvc5", + ProverKind::Metamath => "metamath", + ProverKind::HOLLight => "ocaml", + ProverKind::Mizar => "mizf", + ProverKind::PVS => "pvs", + ProverKind::ACL2 => "acl2", + ProverKind::HOL4 => "hol", + ProverKind::Idris2 => "idris2", + ProverKind::Lean3 => "lean3", + ProverKind::Abella => "abella", + ProverKind::Dedukti => "dkcheck", + ProverKind::Cameleer => "cameleer", + ProverKind::ACL2s => "acl2s", + ProverKind::IsabelleZF => "isabelle", // Same binary, different session. + ProverKind::Boogie => "boogie", + ProverKind::Naproche => "naproche", + ProverKind::Matita => "matitac", + ProverKind::Arend => "arend", + ProverKind::Athena => "athena", + ProverKind::LambdaProlog => "tjsim", + ProverKind::Mercury => "mmc", + ProverKind::Nitpick => "isabelle", // Shared binary via `isabelle process -e nitpick`. + ProverKind::Nunchaku => "nunchaku", + ProverKind::Vampire => "vampire", + ProverKind::EProver => "eprover", + ProverKind::SPASS => "SPASS", + ProverKind::AltErgo => "alt-ergo", + + ProverKind::FStar => "fstar.exe", + ProverKind::Dafny => "dafny", + ProverKind::Why3 => "why3", + ProverKind::GNATprove => "gnatprove", + ProverKind::Stainless => "stainless", + ProverKind::LiquidHaskell => "liquid", + ProverKind::TLAPS => "tlapm", + ProverKind::Twelf => "twelf-server", + ProverKind::Nuprl => "nuprl", + ProverKind::Minlog => "minlog", + ProverKind::Imandra => "imandra", + ProverKind::GLPK => "glpsol", + ProverKind::SCIP => "scip", + ProverKind::MiniZinc => "minizinc", + ProverKind::Chuffed => "fzn-chuffed", + ProverKind::ORTools => "ortools_solve", + ProverKind::TypedWasm => "idris2", // Validates via Idris2 ABI + ProverKind::SPIN => "spin", + ProverKind::CBMC => "cbmc", + ProverKind::SeaHorn => "sea", // SeaHorn verification framework CLI + ProverKind::CaDiCaL => "cadical", // CaDiCaL SAT solver + ProverKind::Kissat => "kissat", // Kissat SAT solver + ProverKind::MiniSat => "minisat", // MiniSat SAT solver + ProverKind::NuSMV => "nuXmv", // nuXmv / NuSMV model checker + ProverKind::TLC => "tlc2", // TLA+ model checker (Java) + ProverKind::Alloy => "alloy", // Alloy Analyzer (Java JAR) + ProverKind::Prism => "prism", // PRISM probabilistic model checker + ProverKind::UPPAAL => "verifyta", // UPPAAL verification engine + ProverKind::FramaC => "frama-c", // Frama-C platform (WP plugin) + ProverKind::Viper => "silicon", // Viper Silicon verifier (default backend) + ProverKind::Tamarin => "tamarin-prover", // Tamarin security protocol prover + ProverKind::ProVerif => "proverif", // ProVerif protocol verifier + ProverKind::KeY => "key", // KeY Java verifier (Java, headless mode) + ProverKind::DReal => "dreal", // dReal delta-complete SMT solver + ProverKind::ABC => "abc", // Berkeley ABC logic synthesis system + ProverKind::GPUVerify => "gpuverify", // GPUVerify CUDA/OpenCL kernel verifier + ProverKind::Faial => "faial-drf", // Faial data-race freedom checker + ProverKind::CubicalAgda => "agda", + ProverKind::Zipperposition => "zipperposition", + ProverKind::Prover9 => "prover9", + ProverKind::OpenSmt => "opensmt", + ProverKind::SmtRat => "smtrat", + ProverKind::Rocq => "rocq", + ProverKind::UppaalStratego => "stratego", + ProverKind::MizAR => "mizar-atp", + ProverKind::IProver => "iprover", + ProverKind::Princess => "princess", + ProverKind::Twee => "twee", + ProverKind::MetiTarski => "metit", + ProverKind::CSI => "csi", + ProverKind::AProVE => "aprove", + ProverKind::KeYmaeraX => "keymaerax", + ProverKind::Qepcad => "qepcad", + ProverKind::Redlog => "redcsl", + ProverKind::MleanCoP => "mleancop", + ProverKind::IleanCoP => "ileancop", + ProverKind::NanoCoP => "nanocop", + ProverKind::MetTeL2 => "mettel2", + ProverKind::ELK => "elk", + ProverKind::Konclude => "konclude", + ProverKind::Storm => "storm", + ProverKind::ProB => "probcli", + ProverKind::EasyCrypt => "easycrypt", + ProverKind::CryptoVerif => "cryptoverif", + ProverKind::Leo3 => "leo3", + ProverKind::Satallax => "satallax", + ProverKind::Lash => "lash", + ProverKind::AgsyHOL => "agsyhol", + // HP ecosystem — all route through the TypeLL kernel CLI; + // the discipline field on HPEcosystemBackend selects the + // actual upstream (typell / katagoria / tropical-resource-typing). + ProverKind::TypeLL => "typell", + ProverKind::KatagoriaVerifier => "katagoria", + ProverKind::TropicalTypeChecker => "tropical-type-check", + ProverKind::ChoreographicTypeChecker => "typell", + ProverKind::EpistemicTypeChecker => "typell", + ProverKind::EchoTypeChecker => "typell", + ProverKind::SessionTypeChecker => "typell", + ProverKind::ModalTypeChecker => "typell", + ProverKind::QTTTypeChecker => "typell", + ProverKind::EffectRowTypeChecker => "typell", + ProverKind::DependentTypeChecker => "typell", + ProverKind::RefinementTypeChecker => "typell", + ProverKind::OrdinaryTypeChecker + | ProverKind::PhantomTypeChecker + | ProverKind::PolymorphicTypeChecker + | ProverKind::ExistentialTypeChecker + | ProverKind::HigherKindedTypeChecker + | ProverKind::RowTypeChecker + | ProverKind::SubtypingTypeChecker + | ProverKind::IntersectionTypeChecker + | ProverKind::UnionTypeChecker + | ProverKind::GradualTypeChecker + | ProverKind::HoareTypeChecker + | ProverKind::IndexedTypeChecker + | ProverKind::LinearTypeChecker + | ProverKind::AffineTypeChecker + | ProverKind::RelevantTypeChecker + | ProverKind::OrderedTypeChecker + | ProverKind::UniquenessTypeChecker + | ProverKind::ImmutableTypeChecker + | ProverKind::CapabilityTypeChecker + | ProverKind::BunchedTypeChecker + | ProverKind::TemporalTypeChecker + | ProverKind::ProvabilityTypeChecker + | ProverKind::ImpureTypeChecker + | ProverKind::CoeffectTypeChecker + | ProverKind::ProbabilisticTypeChecker + | ProverKind::DyadicTypeChecker + | ProverKind::HomotopyTypeChecker + | ProverKind::CubicalTypeChecker + | ProverKind::NominalTypeChecker => "typell", + } + } +} diff --git a/docs/PROVE-RESULT-CONTRACT.adoc b/docs/PROVE-RESULT-CONTRACT.adoc new file mode 100644 index 00000000..1644c404 --- /dev/null +++ b/docs/PROVE-RESULT-CONTRACT.adoc @@ -0,0 +1,115 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += The `echidna.prove.result/1` contract +:toc: macro + +`echidna prove --output json` prints the result of one prove run as +machine-readable JSON. proof-burrower and echidnabot consume it; any other +client may. Human output stays the default: without `--output json`, +`echidna prove` behaves exactly as before. + +toc::[] + +== Shape + +Exactly one line on stdout, terminated by one newline. The line is a single +JCS-canonical (RFC 8785) I-JSON (RFC 7493) object: + +[source,json] +---- +{"duration_ms":1,"echidna_version":"","goal":"ok.twasm","message":"PROVED in 0ms","prover":"TypedWasm","schema":"echidna.prove.result/1","status":"verified","trust":{"axioms":[],"confidence":null}} +---- + +[cols="1,1,4",options="header"] +|=== +| Field | Type | Meaning + +| `schema` | string | Always `echidna.prove.result/1`. +| `status` | string | `verified`, `failed`, `error`, `timeout` or `unknown` (below). +| `prover` | string | The backend, as its `ProverKind` variant name (`Lean`, `Isabelle`, `TypedWasm`, ...). Empty when no backend could be selected. +| `goal` | string | The proof file path, exactly as given on the command line. +| `duration_ms` | integer | Wall-clock time of reading, parsing and checking, in milliseconds. Saturates at 2^53 − 1. +| `message` | string | Human-readable diagnostic. For a completed check it is the outcome (`PROVED in 12ms`, `NO_PROOF_FOUND in 40ms`, `TIMEOUT after 300s`, ...); for an `error` it is the error chain. +| `trust.confidence` | number or null | A receipt-backed confidence in [0, 1], or `null`. See <>. +| `trust.axioms` | array of strings | Axioms and escape hatches (`sorry`, `Admitted`, `postulate`, ...) that ECHIDNA's axiom tracker found in the input, sorted and de-duplicated. +| `echidna_version` | string | The version of the `echidna` binary that printed the object. +|=== + +Logs go to stderr in this mode. With `--diagnose`, the failure diagnostic +for a run that was not `verified` also goes to stderr. + +== Status mapping + +Each backend check returns a `ProverOutcome` +(`src/rust/provers/outcome.rs`). `ProverOutcome::prove_status` maps it: + +[cols="2,1,3",options="header"] +|=== +| `ProverOutcome` | `status` | Why + +| `Proved` | `verified` | The backend established the goal. +| `NoProofFound` | `failed` | The backend ran to completion without establishing it. +| `Timeout` | `timeout` | The configured budget ran out; retry with a larger `--timeout`. +| `InconsistentPremises` | `unknown` | Anything follows from inconsistent premises, so this is neither a usable proof nor a refutation. +| `InvalidInput`, `UnsupportedFeature`, `ProverError`, `SystemError` | `error` | The input, the backend or the system failed. +|=== + +Failures before the check (no backend for the file extension, unreadable +file, parse failure, backend construction failure) are also `error` +objects. stdout never carries anything but the one object. + +== Exit code + +`0` when `status` is `verified`, `1` otherwise. This matches the human mode, +which also exits 1 on a failed proof. + +[[receipt]] +== Receipt, not warrant + +`trust.confidence` is a number only when a receipt-backed computation +produced it, such as an independently checked proof certificate. The +`echidna prove` path checks a single backend and verifies no certificate, +so today it always reports `null`. It never reports a guessed or +model-derived score as confidence. + +This follows the factive / non-factive distinction of +`hyperpolymath/epistemic-types` (`FactiveModality`): a receipt is +transported proof, a warrant is only evidence. ECHIDNA copies the +distinction as a pattern; it does not depend on the Agda library. + +== Consuming it from Rust + +The type, the serialiser and a strict parser live in `echidna-core` +(`echidna_core::prove_result`), so a client does not need to re-implement +them: + +[source,rust] +---- +use echidna_core::prove_result::{ProveResult, ProveStatus}; + +let result = ProveResult::parse(&stdout)?; // rejects non-canonical input +if result.status == ProveStatus::Verified { /* ... */ } +---- + +See `crates/echidna-core/README.adoc` for the git-dependency recipe. + +== Detecting support + +Older binaries do not have the flag. A client can run `echidna prove --help` +and look for an `--output` token, as proof-burrower does. + +== Versioning + +Adding a field is compatible: consumers must ignore unknown fields. +Removing, renaming or retyping a field, or adding a status value, needs a +new schema identifier (`echidna.prove.result/2`). + +== Status of this feature + +* Implemented: `src/rust/prove_contract.rs`, `src/rust/main.rs` + (`prove_json_command`), `crates/echidna-core/src/prove_result.rs`. +* Tested: golden JCS bytes for every status (`echidna-core` and + `prove_contract` unit tests); planted non-canonical payloads are + rejected; end-to-end runs of the real binary for `verified`, `failed` + and `error` (`tests/prove_output_json.rs`). `timeout` and `unknown` are + covered only by the golden unit tests, because no backend that runs + without an external prover produces them. diff --git a/docs/wikis/Home.md b/docs/wikis/Home.md index 8ac9331e..a601a9c5 100644 --- a/docs/wikis/Home.md +++ b/docs/wikis/Home.md @@ -46,7 +46,7 @@ commit. | 12 core backends (`GET /api/provers`) | implemented, wired, live-tested (T1/T2 live-prover matrices green) | — | | Wider backend surface (see [`docs/PROVER_COUNT.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVER_COUNT.adoc)) | implemented | Tier-4 backends are mock-only; the HP-ecosystem type-checker backends call `typell --discipline` / `tropical-type-check`, which upstream does not provide, so they are **not wired** | | Trust pipeline (integrity, certificates, axioms, confidence, mutation, Pareto, statistics) | implemented, wired into `dispatch.rs`, unit-tested | not proved | -| Idris2 ABI (`src/abi/`) | type-checked, CI-gated (`idris2-abi-ci.yml`) | — | +| Idris2 ABI (`src/abi/`) | type-checked, totality-checked (`%default total` in every packaged module), CI-gated (`idris2-abi-ci.yml`, runs when `src/abi/` changes) | `CapnSchemas.idr` and `NeSyAssistTesting.idr` are outside the package, so CI does not check them | | Dogfood proof corpus (`proofs/{coq,lean,agda}`) | CI-gated (`dogfood-proofs-ci.yml`) | — | | Agda meta-checker | implemented | its workflow was in `startup_failure` on `main` | | Creusot trust kernel (`crates/echidna-core-creusot`) | annotations **stated**; stable-Rust test mirror runs in CI | **not proved**: no obligation has been discharged; the Creusot job is manual-only | @@ -56,7 +56,9 @@ commit. | REST / gRPC / GraphQL servers | implemented; server boot gate green | — | | UI | static shell (`just serve-ui`, Bun) | AffineScript-TEA compile pipeline not wired (`just build-ui` fails on purpose) | | ID minting (`echidna::ids`) | UUIDv7 record ids: implemented, wired, tested. UUIDv8 content ids (SHA-256 over JCS): implemented, tested | content ids not yet used for goals/corpus/octads | -| `echidna prove --output json` (`echidna.prove.result/1`) | — | not implemented yet | +| `echidna prove --output json` (`echidna.prove.result/1`, [contract](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVE-RESULT-CONTRACT.adoc)) | implemented, wired, tested: golden JCS bytes for all five statuses; end-to-end runs of the binary for `verified` / `failed` / `error` (TypedWasm backend, no external prover) | `timeout` / `unknown` only unit-tested; `trust.confidence` is always `null` on this path (no certificate is checked) | +| `echidna-core` client crate (`ProverKind`, prove-result type, trust kernel) | implemented, tested; git-dependency recipe in `crates/echidna-core/README.adoc` | not published to crates.io; echidnabot not yet switched to it | +| Zig FFI (`ffi/zig`) | builds and unit-tested in CI on Zig 0.15.2 (`zig-ffi-ci.yml`); unified-api-adapter purity check passing | `src/main.zig` exports are template examples (`echidna_process` does nothing); the Rust-linked integration tests and benchmarks are not built in CI | | Containers | built in CI | publication not verified | | Forge mirrors | GitLab, Codeberg, SourceHut, Radicle succeed | Bitbucket, Disroot, Gitea mirror jobs fail | diff --git a/ffi/zig/src/boj.zig b/ffi/zig/src/boj.zig index 42d6f3ff..bddcda30 100644 --- a/ffi/zig/src/boj.zig +++ b/ffi/zig/src/boj.zig @@ -582,7 +582,9 @@ test "BoJ: version and error buffer" { test "BoJ: callbacks" { const Counter = struct { var count: u32 = 0; - fn handler(_: c_int, _: c_int) callconv(.c) void { count += 1; } + fn handler(_: c_int, _: c_int) callconv(.c) void { + count += 1; + } }; Counter.count = 0; _ = echidna_boj_register_on_status_change(Counter.handler); diff --git a/ffi/zig/src/capnp_bridge.zig b/ffi/zig/src/capnp_bridge.zig index 09a0d247..01f83100 100644 --- a/ffi/zig/src/capnp_bridge.zig +++ b/ffi/zig/src/capnp_bridge.zig @@ -22,13 +22,13 @@ const BRIDGE_VERSION = "0.1.0"; // ─── Status codes ───────────────────────────────────────────────────────────── pub const CapnpStatus = enum(c_int) { - ok = 0, - not_connected = -1, + ok = 0, + not_connected = -1, stub_not_implemented = -2, - invalid_param = -3, - io_error = -4, - connect_failed = -6, - unknown_error = -99, + invalid_param = -3, + io_error = -4, + connect_failed = -6, + unknown_error = -99, }; // ─── Thread-local error storage ─────────────────────────────────────────────── @@ -178,12 +178,12 @@ export fn echidna_capnp_status_message( } const generic: []const u8 = switch (status) { - 0 => "ok", - -1 => "not connected", - -2 => "stub not implemented (L1 wave 1 pending)", - -3 => "invalid parameter", - -4 => "I/O error", - -6 => "connect failed", + 0 => "ok", + -1 => "not connected", + -2 => "stub not implemented (L1 wave 1 pending)", + -3 => "invalid parameter", + -4 => "I/O error", + -6 => "connect failed", -99 => "unknown error", else => "unrecognised status code", }; diff --git a/ffi/zig/src/main.zig b/ffi/zig/src/main.zig index 554b5a65..9448074e 100644 --- a/ffi/zig/src/main.zig +++ b/ffi/zig/src/main.zig @@ -11,11 +11,16 @@ const std = @import("std"); const VERSION = "0.1.0"; const BUILD_INFO = "ECHIDNA built with Zig " ++ @import("builtin").zig_version_string; -/// Thread-local error storage -threadlocal var last_error: ?[]const u8 = null; +/// Thread-local error storage. Messages are static, NUL-terminated string +/// literals, so `echidna_last_error` can hand them to C without allocating. +threadlocal var last_error: ?[:0]const u8 = null; + +/// Pure-Zig allocator for library state. No libc: the FFI's only C contract +/// is the C calling convention of its exports. +const allocator = std.heap.page_allocator; /// Set the last error message -fn setError(msg: []const u8) void { +fn setError(msg: [:0]const u8) void { last_error = msg; } @@ -37,14 +42,19 @@ pub const Result = enum(c_int) { null_pointer = 4, }; -/// Library handle (opaque to prevent direct access) -pub const Handle = opaque { - // Internal state hidden from C - allocator: std.mem.Allocator, +/// Library handle as C sees it: an opaque pointer. +pub const Handle = opaque {}; + +/// Internal state behind a `Handle`; never visible across the C ABI. +const State = struct { initialized: bool, - // Add your fields here }; +/// Recover the internal state from a C handle. +fn state(handle: *Handle) *State { + return @ptrCast(@alignCast(handle)); +} + //============================================================================== // Library Lifecycle //============================================================================== @@ -52,27 +62,20 @@ pub const Handle = opaque { /// Initialize the library /// Returns a handle, or null on failure export fn echidna_init() ?*Handle { - const allocator = std.heap.c_allocator; - - const handle = allocator.create(Handle) catch { + const st = allocator.create(State) catch { setError("Failed to allocate handle"); return null; }; - // Initialize handle - handle.* = .{ - .allocator = allocator, - .initialized = true, - }; + st.* = .{ .initialized = true }; clearError(); - return handle; + return @ptrCast(st); } /// Free the library handle export fn echidna_free(handle: ?*Handle) void { - const h = handle orelse return; - const allocator = h.allocator; + const h = state(handle orelse return); // Clean up resources h.initialized = false; @@ -87,10 +90,10 @@ export fn echidna_free(handle: ?*Handle) void { /// Process data (example operation) export fn echidna_process(handle: ?*Handle, input: u32) Result { - const h = handle orelse { + const h = state(handle orelse { setError("Null handle"); return .null_pointer; - }; + }); if (!h.initialized) { setError("Handle not initialized"); @@ -111,10 +114,10 @@ export fn echidna_process(handle: ?*Handle, input: u32) Result { /// Get a string result (example) /// Caller must free the returned string export fn echidna_get_string(handle: ?*Handle) ?[*:0]const u8 { - const h = handle orelse { + const h = state(handle orelse { setError("Null handle"); return null; - }; + }); if (!h.initialized) { setError("Handle not initialized"); @@ -122,7 +125,7 @@ export fn echidna_get_string(handle: ?*Handle) ?[*:0]const u8 { } // Example: allocate and return a string - const result = h.allocator.dupeZ(u8, "Example result") catch { + const result = allocator.dupeZ(u8, "Example result") catch { setError("Failed to allocate string"); return null; }; @@ -134,7 +137,6 @@ export fn echidna_get_string(handle: ?*Handle) ?[*:0]const u8 { /// Free a string allocated by the library export fn echidna_free_string(str: ?[*:0]const u8) void { const s = str orelse return; - const allocator = std.heap.c_allocator; const slice = std.mem.span(s); allocator.free(slice); @@ -150,10 +152,10 @@ export fn echidna_process_array( buffer: ?[*]const u8, len: u32, ) Result { - const h = handle orelse { + const h = state(handle orelse { setError("Null handle"); return .null_pointer; - }; + }); const buf = buffer orelse { setError("Null buffer"); @@ -184,10 +186,8 @@ export fn echidna_process_array( export fn echidna_last_error() ?[*:0]const u8 { const err = last_error orelse return null; - // Return C string (static storage, no need to free) - const allocator = std.heap.c_allocator; - const c_str = allocator.dupeZ(u8, err) catch return null; - return c_str.ptr; + // Static storage: the caller must not free it. + return err.ptr; } //============================================================================== @@ -209,17 +209,17 @@ export fn echidna_build_info() [*:0]const u8 { //============================================================================== /// Callback function type (C ABI) -pub const Callback = *const fn (u64, u32) callconv(.C) u32; +pub const Callback = *const fn (u64, u32) callconv(.c) u32; /// Register a callback export fn echidna_register_callback( handle: ?*Handle, callback: ?Callback, ) Result { - const h = handle orelse { + const h = state(handle orelse { setError("Null handle"); return .null_pointer; - }; + }); const cb = callback orelse { setError("Null callback"); @@ -244,7 +244,7 @@ export fn echidna_register_callback( /// Check if handle is initialized export fn echidna_is_initialized(handle: ?*Handle) u32 { - const h = handle orelse return 0; + const h = state(handle orelse return 0); return if (h.initialized) 1 else 0; } diff --git a/ffi/zig/src/provers/atp.zig b/ffi/zig/src/provers/atp.zig index 07f857be..3191d39f 100644 --- a/ffi/zig/src/provers/atp.zig +++ b/ffi/zig/src/provers/atp.zig @@ -140,8 +140,8 @@ export fn atp_set_result(handle: c_int, szs_status: c_int) c_int { atp_sessions[idx].szs_status = @enumFromInt(szs_status); atp_sessions[idx].state = switch (szs_status) { - 0 => .found_proof, // Theorem - 1 => .found_counter, // CounterSatisfiable + 0 => .found_proof, // Theorem + 1 => .found_counter, // CounterSatisfiable 4 => .timeout, 5 => .gave_up, else => .err, diff --git a/ffi/zig/src/provers/declarative.zig b/ffi/zig/src/provers/declarative.zig index d9c11ea1..5843be1d 100644 --- a/ffi/zig/src/provers/declarative.zig +++ b/ffi/zig/src/provers/declarative.zig @@ -138,13 +138,13 @@ export fn verify_reset(handle: c_int) c_int { /// Get kernel size for a declarative prover. export fn verify_kernel_size(solver_kind: c_int) c_int { return switch (solver_kind) { - 6 => @intFromEnum(KernelSize.tiny), // Metamath - 8 => @intFromEnum(KernelSize.medium), // Mizar - 9 => @intFromEnum(KernelSize.large), // PVS - 10 => @intFromEnum(KernelSize.large), // ACL2 - 19 => @intFromEnum(KernelSize.external), // TLAPS - 20 => @intFromEnum(KernelSize.small), // Twelf - 24 => @intFromEnum(KernelSize.medium), // Imandra + 6 => @intFromEnum(KernelSize.tiny), // Metamath + 8 => @intFromEnum(KernelSize.medium), // Mizar + 9 => @intFromEnum(KernelSize.large), // PVS + 10 => @intFromEnum(KernelSize.large), // ACL2 + 19 => @intFromEnum(KernelSize.external), // TLAPS + 20 => @intFromEnum(KernelSize.small), // Twelf + 24 => @intFromEnum(KernelSize.medium), // Imandra else => -1, }; } diff --git a/ffi/zig/src/provers/vcl_ut.zig b/ffi/zig/src/provers/vcl_ut.zig index e4144fec..cb87e9de 100644 --- a/ffi/zig/src/provers/vcl_ut.zig +++ b/ffi/zig/src/provers/vcl_ut.zig @@ -190,9 +190,7 @@ export fn vqlut_parse( // Classify effect based on operation query_sessions[idx].effect = switch (@as(QueryOp, @enumFromInt(operation))) { - .find_proof, .find_similar, .cross_prover_search, - .provenance_trace, .temporal_history, .dependency_graph, - .axiom_usage, .tactic_stats => .read_only, + .find_proof, .find_similar, .cross_prover_search, .provenance_trace, .temporal_history, .dependency_graph, .axiom_usage, .tactic_stats => .read_only, }; return 0; diff --git a/ffi/zig/src/tentacles.zig b/ffi/zig/src/tentacles.zig index 9f9bda30..fa071d36 100644 --- a/ffi/zig/src/tentacles.zig +++ b/ffi/zig/src/tentacles.zig @@ -305,20 +305,21 @@ export fn echidna_tentacles_get_global_stage() callconv(.c) c_int { export fn echidna_tentacles_poll_events(out_ptr: [*]u8, out_len: *usize) callconv(.c) c_int { if (!g_initialised) return ERR_NOT_INIT; - // Build JSON array of agent states + // Build JSON array of agent states. Formatting goes through + // std.fmt.bufPrint into a fixed buffer: no stream or filesystem module, per the + // estate unified-api-adapter purity check. var buf: [MAX_EVENT_BUF]u8 = undefined; - var stream = std.io.fixedBufferStream(&buf); - var writer = stream.writer(); + var pos: usize = 0; - writer.writeAll("[") catch return ERR_BUFFER_TOO_SMALL; + pos += (std.fmt.bufPrint(buf[pos..], "[", .{}) catch return ERR_BUFFER_TOO_SMALL).len; for (0..AGENT_COUNT) |i| { - if (i > 0) writer.writeAll(",") catch return ERR_BUFFER_TOO_SMALL; + if (i > 0) pos += (std.fmt.bufPrint(buf[pos..], ",", .{}) catch return ERR_BUFFER_TOO_SMALL).len; const a = &g_agents[i]; const id_enum: TentacleId = @enumFromInt(@as(c_int, @intCast(i))); - writer.print( + pos += (std.fmt.bufPrint(buf[pos..], \\{{"id":{d},"name":"{s}","status":{d},"phase":{d},"stage":{d},"busy":{s},"hasTask":{s},"hasError":{s}}} , .{ i, @@ -329,12 +330,12 @@ export fn echidna_tentacles_poll_events(out_ptr: [*]u8, out_len: *usize) callcon if (a.status == .busy) "true" else "false", if (a.task_len > 0) "true" else "false", if (a.error_len > 0) "true" else "false", - }) catch return ERR_BUFFER_TOO_SMALL; + }) catch return ERR_BUFFER_TOO_SMALL).len; } - writer.writeAll("]") catch return ERR_BUFFER_TOO_SMALL; + pos += (std.fmt.bufPrint(buf[pos..], "]", .{}) catch return ERR_BUFFER_TOO_SMALL).len; - const written = stream.pos; + const written = pos; if (written > out_len.*) return ERR_BUFFER_TOO_SMALL; @memcpy(out_ptr[0..written], buf[0..written]); @@ -415,3 +416,31 @@ export fn echidna_tentacles_last_error() callconv(.c) ?[*]const u8 { export fn echidna_tentacles_agent_count() callconv(.c) c_int { return AGENT_COUNT; } + +// ============================================================================ +// Tests +// ============================================================================ + +test "poll_events emits a JSON array with one object per agent" { + try std.testing.expectEqual(ERR_NOT_INIT, echidna_tentacles_poll_events(undefined, undefined)); + + try std.testing.expectEqual(@as(c_int, 0), echidna_tentacles_init()); + defer echidna_tentacles_shutdown(); + + var out: [MAX_EVENT_BUF]u8 = undefined; + var len: usize = out.len; + try std.testing.expectEqual(@as(c_int, 0), echidna_tentacles_poll_events(&out, &len)); + + const json = out[0..len]; + try std.testing.expect(json[0] == '[' and json[len - 1] == ']'); + try std.testing.expectEqual(@as(usize, AGENT_COUNT), std.mem.count(u8, json, "\"id\":")); +} + +test "poll_events reports a too-small output buffer" { + try std.testing.expectEqual(@as(c_int, 0), echidna_tentacles_init()); + defer echidna_tentacles_shutdown(); + + var out: [4]u8 = undefined; + var len: usize = out.len; + try std.testing.expectEqual(ERR_BUFFER_TOO_SMALL, echidna_tentacles_poll_events(&out, &len)); +} diff --git a/ffi/zig/src/typell.zig b/ffi/zig/src/typell.zig index 14b0e76c..5f883d44 100644 --- a/ffi/zig/src/typell.zig +++ b/ffi/zig/src/typell.zig @@ -480,7 +480,9 @@ test "TypeLL: version and error" { test "TypeLL: callbacks" { const Counter = struct { var count: u32 = 0; - fn handler(_: c_int, _: c_int) callconv(.c) void { count += 1; } + fn handler(_: c_int, _: c_int) callconv(.c) void { + count += 1; + } }; Counter.count = 0; _ = echidna_typell_register_on_status_change(Counter.handler); diff --git a/ffi/zig/test/benchmark.zig b/ffi/zig/test/benchmark.zig index 7dfa818f..29a799ea 100644 --- a/ffi/zig/test/benchmark.zig +++ b/ffi/zig/test/benchmark.zig @@ -48,11 +48,11 @@ const BUF_SIZE: usize = 131072; // 128KB — large enough for all operations /// Prover names for table output (must match ProverKind ordinals 0..29). const prover_names = [_][]const u8{ - "Agda", "Coq", "Lean", "Isabelle", "Z3", "CVC5", - "Metamath", "HOL Light", "Mizar", "PVS", "ACL2", "HOL4", - "Idris2", "Vampire", "E Prover", "SPASS", "Alt-Ergo", "F*", - "Dafny", "Why3", "TLAPS", "Twelf", "Nuprl", "Minlog", - "Imandra", "GLPK", "SCIP", "MiniZinc", "Chuffed", "OR-Tools", + "Agda", "Coq", "Lean", "Isabelle", "Z3", "CVC5", + "Metamath", "HOL Light", "Mizar", "PVS", "ACL2", "HOL4", + "Idris2", "Vampire", "E Prover", "SPASS", "Alt-Ergo", "F*", + "Dafny", "Why3", "TLAPS", "Twelf", "Nuprl", "Minlog", + "Imandra", "GLPK", "SCIP", "MiniZinc", "Chuffed", "OR-Tools", }; // ============================================================================ diff --git a/ffi/zig/test/core_native_test.zig b/ffi/zig/test/core_native_test.zig index d53da23f..dcc3d027 100644 --- a/ffi/zig/test/core_native_test.zig +++ b/ffi/zig/test/core_native_test.zig @@ -59,12 +59,11 @@ test "ProverKind: out-of-range returns null" { test "ProverKind: name strings are non-empty" { const provers = [_]core.ProverKind{ - .agda, .coq, .lean, .isabelle, .z3, .cvc5, - .metamath, .hol_light, .mizar, .pvs, .acl2, - .hol4, .idris2, .vampire, .eprover, .spass, - .alt_ergo, .fstar, .dafny, .why3, .tlaps, - .twelf, .nuprl, .minlog, .imandra, .glpk, - .scip, .minizinc, .chuffed, .ortools, + .agda, .coq, .lean, .isabelle, .z3, .cvc5, + .metamath, .hol_light, .mizar, .pvs, .acl2, .hol4, + .idris2, .vampire, .eprover, .spass, .alt_ergo, .fstar, + .dafny, .why3, .tlaps, .twelf, .nuprl, .minlog, + .imandra, .glpk, .scip, .minizinc, .chuffed, .ortools, }; for (provers) |pk| { const n = std.mem.span(pk.name()); diff --git a/ffi/zig/test/integration_test.zig b/ffi/zig/test/integration_test.zig index 2cbf967d..4fb8c38e 100644 --- a/ffi/zig/test/integration_test.zig +++ b/ffi/zig/test/integration_test.zig @@ -149,11 +149,11 @@ test "point: echidna_prover_count returns 30" { test "point: echidna_prover_name valid kinds" { const expected_names = [_][]const u8{ - "Agda", "Coq", "Lean", "Isabelle", "Z3", "CVC5", - "Metamath", "HOL Light", "Mizar", "PVS", "ACL2", "HOL4", - "Idris2", "Vampire", "E Prover", "SPASS", "Alt-Ergo", "F*", - "Dafny", "Why3", "TLAPS", "Twelf", "Nuprl", "Minlog", - "Imandra", "GLPK", "SCIP", "MiniZinc", "Chuffed", "OR-Tools", + "Agda", "Coq", "Lean", "Isabelle", "Z3", "CVC5", + "Metamath", "HOL Light", "Mizar", "PVS", "ACL2", "HOL4", + "Idris2", "Vampire", "E Prover", "SPASS", "Alt-Ergo", "F*", + "Dafny", "Why3", "TLAPS", "Twelf", "Nuprl", "Minlog", + "Imandra", "GLPK", "SCIP", "MiniZinc", "Chuffed", "OR-Tools", }; for (expected_names, 0..) |expected, i| { const name = echidna_prover_name(@intCast(i)); diff --git a/src/abi/EchidnaABI/Gnn.idr b/src/abi/EchidnaABI/Gnn.idr index e6175c98..bf0fe004 100644 --- a/src/abi/EchidnaABI/Gnn.idr +++ b/src/abi/EchidnaABI/Gnn.idr @@ -20,6 +20,8 @@ import Data.So %default total +%default total + ------------------------------------------------------------------------ -- Node and Edge Kind Enumerations ------------------------------------------------------------------------ diff --git a/src/abi/EchidnaABI/TacticRecord.idr b/src/abi/EchidnaABI/TacticRecord.idr index 12ed4d14..531b6054 100644 --- a/src/abi/EchidnaABI/TacticRecord.idr +++ b/src/abi/EchidnaABI/TacticRecord.idr @@ -32,6 +32,8 @@ import Data.So %default total +%default total + ------------------------------------------------------------------------ -- Fixed-Point Confidence Encoding ------------------------------------------------------------------------ diff --git a/src/rust/lib.rs b/src/rust/lib.rs index 987d1af1..3edf88d6 100644 --- a/src/rust/lib.rs +++ b/src/rust/lib.rs @@ -36,6 +36,7 @@ pub mod parsers; #[cfg(feature = "verisim")] pub mod proof_encoding; // CBOR encoding + proof identity hashing pub mod proof_search; // Chapel parallel proof search (optional feature) +pub mod prove_contract; // `echidna prove --output json`: the echidna.prove.result/1 producer pub mod provers; pub mod suggest; // Mechanical tactic-variant finder (echidna suggest verb) pub mod vcl_ut; diff --git a/src/rust/main.rs b/src/rust/main.rs index b6674d6d..33e5f686 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -24,6 +24,15 @@ mod server; use output::{OutputFormat, OutputFormatter}; use repl::DiagnosticsREPL; +/// Result form of `echidna prove`. +#[derive(Clone, Copy, Debug, PartialEq, Eq, clap::ValueEnum)] +enum ProveOutput { + /// Human-readable report (the default). + Human, + /// One `echidna.prove.result/1` JSON object on stdout. + Json, +} + /// ECHIDNA - Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance #[derive(Parser)] #[command(name = "echidna")] @@ -88,6 +97,12 @@ enum Commands { /// One of: none (default), bwrap, podman. #[arg(long, default_value = "none")] sandbox: String, + + /// Result form. `human` (default) prints the usual report; `json` + /// prints exactly one `echidna.prove.result/1` object (JCS-canonical + /// I-JSON) on stdout and sends logs to stderr. + #[arg(long, value_enum, default_value_t = ProveOutput::Human)] + output: ProveOutput, }, /// Verify an existing proof @@ -364,8 +379,16 @@ async fn main() -> Result<()> { // Parse CLI arguments let cli = Cli::parse(); - // Initialize tracing - init_tracing(cli.verbose); + // Initialize tracing. With `prove --output json`, stdout carries only the + // result object, so logs go to stderr. + let json_stdout = matches!( + cli.command, + Commands::Prove { + output: ProveOutput::Json, + .. + } + ); + init_tracing(cli.verbose, json_stdout); // Disable colors if requested if cli.no_color { @@ -387,6 +410,33 @@ async fn main() -> Result<()> { diagnose, project_root, sandbox, + output: ProveOutput::Json, + } => { + prove_json_command( + file, + prover, + timeout, + neural, + executable, + library, + diagnose, + project_root, + sandbox, + ) + .await; + }, + + Commands::Prove { + file, + prover, + timeout, + neural, + executable, + library, + diagnose, + project_root, + sandbox, + output: ProveOutput::Human, } => { prove_command( file, @@ -482,8 +532,8 @@ async fn main() -> Result<()> { Ok(()) } -/// Initialize tracing/logging -fn init_tracing(verbose: bool) { +/// Initialize tracing/logging; logs go to stderr when `to_stderr` is set. +fn init_tracing(verbose: bool, to_stderr: bool) { use tracing_subscriber::filter::EnvFilter; use tracing_subscriber::{fmt, prelude::*}; @@ -493,10 +543,14 @@ fn init_tracing(verbose: bool) { EnvFilter::new("echidna=info,warn") }; - tracing_subscriber::registry() - .with(filter) - .with(fmt::layer()) - .init(); + let registry = tracing_subscriber::registry().with(filter); + if to_stderr { + registry + .with(fmt::layer().with_writer(std::io::stderr)) + .init(); + } else { + registry.with(fmt::layer()).init(); + } } /// Prove command implementation @@ -562,6 +616,86 @@ async fn prove_command( Ok(()) } +/// `echidna prove --output json`: print one `echidna.prove.result/1` object. +/// +/// Every failure, including a missing backend or unreadable file, becomes an +/// `error` result rather than a non-JSON message. Exits 0 when the status is +/// `verified` and 1 otherwise. With `--diagnose`, the diagnostic report for a +/// non-verified run goes to stderr. +#[allow(clippy::too_many_arguments)] +async fn prove_json_command( + file: PathBuf, + prover_kind: Option, + timeout: u64, + neural: bool, + executable: Option, + library: Vec, + diagnose: bool, + project_root: Option, + sandbox: String, +) { + use echidna::prove_contract::{self, ProveStatus}; + + let goal = file.display().to_string(); + let start = std::time::Instant::now(); + let since = + |start: std::time::Instant| u64::try_from(start.elapsed().as_millis()).unwrap_or(u64::MAX); + + let kind = match detect_prover(prover_kind, &file) { + Ok(k) => k, + Err(e) => { + let r = prove_contract::result_from_error(prover_kind, &goal, &e, since(start)); + emit_prove_result(&r); + }, + }; + let backend = match create_config( + kind, + timeout, + neural, + executable, + library, + project_root, + &sandbox, + ) + .and_then(|config| { + echidna::provers::ProverFactory::create(kind, config) + .context("Failed to create prover backend") + }) { + Ok(b) => b, + Err(e) => { + let r = prove_contract::result_from_error(Some(kind), &goal, &e, since(start)); + emit_prove_result(&r); + }, + }; + + let (result, outcome) = prove_contract::run_detailed(kind, &*backend, &file).await; + if let (true, Some(outcome)) = (diagnose && result.status != ProveStatus::Verified, outcome) { + eprintln!("--- Proof Failure Diagnostic ---"); + eprintln!("{}", diagnose_from_outcome(kind, &outcome).display()); + } + emit_prove_result(&result); +} + +/// Print `result` as its one JCS line on stdout and exit (0 iff verified). +/// +/// If the value cannot be serialised (it never should), a minimal `error` +/// object is printed instead, so stdout always carries one contract object. +fn emit_prove_result(result: &echidna::prove_contract::ProveResult) -> ! { + use echidna::prove_contract::{self, ProveStatus}; + let line = result.to_jcs().unwrap_or_else(|e| { + let e = anyhow::anyhow!("could not serialise prove result: {e}"); + prove_contract::result_from_error(None, &result.goal, &e, 0) + .to_jcs() + .expect("an error result with no numbers out of range serialises") + }); + println!("{line}"); + std::process::exit(if result.status == ProveStatus::Verified { + 0 + } else { + 1 + }); +} + /// Run `check()` on the prover and display a structured diagnostic report. /// /// Called after a failed `verify_proof()` when `--diagnose` is active. diff --git a/src/rust/prove_contract.rs b/src/rust/prove_contract.rs new file mode 100644 index 00000000..446d4eef --- /dev/null +++ b/src/rust/prove_contract.rs @@ -0,0 +1,202 @@ +// SPDX-License-Identifier: MPL-2.0 + +//! Producer side of the `echidna.prove.result/1` contract. +//! +//! `echidna prove --output json` runs one backend check and prints +//! one [`ProveResult`] as JCS-canonical I-JSON on stdout. The type and its +//! serialiser live in `echidna-core` ([`echidna_core::prove_result`]) so +//! consumers share them; this module turns a backend run into that value. +//! +//! See `docs/PROVE-RESULT-CONTRACT.adoc` for the contract and the status +//! mapping. + +use std::path::Path; +use std::time::Instant; + +pub use echidna_core::prove_result::{ProveResult, ProveStatus, ProveTrust, SCHEMA}; + +use crate::provers::{ProverBackend, ProverKind, ProverOutcome}; +use crate::verification::axiom_tracker::AxiomTracker; + +/// The version string this build writes into `echidna_version`. +pub const ECHIDNA_VERSION: &str = env!("CARGO_PKG_VERSION"); + +/// Names of the axioms and escape hatches the tracker finds in `content`. +/// +/// Uses ECHIDNA's source-level [`AxiomTracker`] for `kind`; returns the +/// constructs only (sorted and de-duplicated by [`ProveResult::new`]). +pub fn axioms_in(kind: ProverKind, content: &str) -> Vec { + AxiomTracker::new() + .scan(kind, content) + .into_iter() + .map(|u| u.construct) + .collect() +} + +/// Build the result for a backend run that produced `outcome`. +/// +/// `confidence` stays `null`: a single-prover check verifies no proof +/// certificate, so there is no receipt-backed figure to report. +pub fn result_from_outcome( + kind: ProverKind, + goal: &str, + outcome: &ProverOutcome, + duration_ms: u64, + axioms: Vec, +) -> ProveResult { + ProveResult::new( + outcome.prove_status(), + kind.to_string(), + goal, + duration_ms, + outcome.to_string(), + ProveTrust { + confidence: None, + axioms, + }, + ECHIDNA_VERSION, + ) +} + +/// Build the `error` result for a run that failed before the backend check +/// (no backend for the file, unreadable or unparsable input, ...). +/// +/// `kind` is the backend if one was selected; otherwise `prover` is empty. +pub fn result_from_error( + kind: Option, + goal: &str, + err: &anyhow::Error, + duration_ms: u64, +) -> ProveResult { + ProveResult::new( + ProveStatus::Error, + kind.map(|k| k.to_string()).unwrap_or_default(), + goal, + duration_ms, + format!("{err:#}"), + ProveTrust::default(), + ECHIDNA_VERSION, + ) +} + +/// Parse `file` with `backend`, run its rich check, and build the result. +/// +/// Never fails: every failure becomes an `error` result. `duration_ms` +/// covers parsing plus the backend check. +pub async fn run(kind: ProverKind, backend: &dyn ProverBackend, file: &Path) -> ProveResult { + run_detailed(kind, backend, file).await.0 +} + +/// Like [`run`], and also return the backend's [`ProverOutcome`] when the +/// check itself ran (for `--diagnose`). +pub async fn run_detailed( + kind: ProverKind, + backend: &dyn ProverBackend, + file: &Path, +) -> (ProveResult, Option) { + let goal = file.display().to_string(); + let start = Instant::now(); + let elapsed = || u64::try_from(start.elapsed().as_millis()).unwrap_or(u64::MAX); + + let content = match crate::provers::bounded_read_proof_file(file).await { + Ok(c) => c, + Err(e) => return (result_from_error(Some(kind), &goal, &e, elapsed()), None), + }; + let state = match backend.parse_file(file.to_path_buf()).await { + Ok(s) => s, + Err(e) => { + let e = e.context("Failed to parse proof file"); + return (result_from_error(Some(kind), &goal, &e, elapsed()), None); + }, + }; + let outcome = match backend.check(&state).await { + Ok(o) => o, + Err(e) => { + let e = e.context("Failed to verify proof"); + return (result_from_error(Some(kind), &goal, &e, elapsed()), None); + }, + }; + let result = result_from_outcome(kind, &goal, &outcome, elapsed(), axioms_in(kind, &content)); + (result, Some(outcome)) +} + +#[cfg(test)] +mod tests { + use super::*; + + /// Expected JCS line for a given status and message, with fixed fields. + fn golden(status: &str, prover: &str, message: &str, axioms: &str) -> String { + format!( + r#"{{"duration_ms":7,"echidna_version":"{ECHIDNA_VERSION}","goal":"g.lean","message":"{message}","prover":"{prover}","schema":"echidna.prove.result/1","status":"{status}","trust":{{"axioms":[{axioms}],"confidence":null}}}}"# + ) + } + + /// Golden JCS bytes for every contract status, via the outcome path. + #[test] + fn golden_output_for_each_outcome_status() { + let cases = [ + ( + ProverOutcome::Proved { elapsed_ms: 7 }, + "verified", + "PROVED in 7ms", + ), + ( + ProverOutcome::NoProofFound { + elapsed_ms: 7, + reason: None, + }, + "failed", + "NO_PROOF_FOUND in 7ms", + ), + ( + ProverOutcome::Timeout { limit_secs: 3 }, + "timeout", + "TIMEOUT after 3s", + ), + ( + ProverOutcome::InconsistentPremises { detail: None }, + "unknown", + "INCONSISTENT_PREMISES", + ), + ( + ProverOutcome::SystemError { + detail: "lean not found".into(), + }, + "error", + "SYSTEM_ERROR: lean not found", + ), + ]; + for (outcome, status, message) in cases { + let r = result_from_outcome( + ProverKind::Lean, + "g.lean", + &outcome, + 7, + vec!["sorry".into(), "sorry".into()], + ); + assert_eq!( + r.to_jcs().unwrap(), + golden(status, "Lean", message, r#""sorry""#) + ); + } + } + + /// A pre-check failure is an `error` with the full error chain. + #[test] + fn golden_output_for_pre_check_error() { + let e = anyhow::anyhow!("no such file").context("Failed to parse proof file"); + let r = result_from_error(None, "g.lean", &e, 7); + assert_eq!( + r.to_jcs().unwrap(), + golden("error", "", "Failed to parse proof file: no such file", "") + ); + } + + /// The tracker's findings reach `trust.axioms`. + #[test] + fn axioms_are_reported_from_the_input() { + let found = axioms_in(ProverKind::Lean, "theorem t : 1 = 1 := by\n sorry\n"); + assert!(found.iter().any(|a| a == "sorry"), "{found:?}"); + assert!(axioms_in(ProverKind::Lean, "theorem t : 1 = 1 := rfl\n").is_empty()); + } +} diff --git a/src/rust/provers/mod.rs b/src/rust/provers/mod.rs index 32baaa5b..a9e78bd3 100644 --- a/src/rust/provers/mod.rs +++ b/src/rust/provers/mod.rs @@ -123,1283 +123,9 @@ pub mod why3; pub mod z3; pub mod zipperposition; -/// Enumeration of all supported provers -#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, strum::EnumIter)] -pub enum ProverKind { - // Tier 1: Original + SMT solvers - Agda, - Coq, - Lean, - Isabelle, - Z3, - CVC5, - - // Tier 2: "Big Six" completion - Metamath, - HOLLight, - Mizar, - - // Tier 3: Additional coverage - PVS, - ACL2, - - // Tier 4: Advanced - HOL4, - - // Extended: Additional provers - Idris2, - /// Lean 3 — sibling prover to Lean 4 (not a version of it). - /// mathlib3 preserves a substantial corpus that never fully ported - /// to mathlib4; port-pairs between mathlib3 and mathlib4 give the - /// arbiter ready-made cross-system evidence for the same theorem. - Lean3, - - // Tier 5: First-Order ATPs - Vampire, - EProver, - SPASS, - AltErgo, - - // Tier 5b: Higher-Order ATPs - Leo3, - Satallax, - Lash, - AgsyHOL, - - // Tier 5c: Frontier First-Order ATPs - IProver, - Princess, - Twee, - MetiTarski, - CSI, - AProVE, - - // Tier 5d: Hybrid systems / differential dynamic logic - KeYmaeraX, - - // Tier 5e: Real-algebraic decision (CAD / virtual substitution) - Qepcad, - Redlog, - - // Tier 5f: Connection-method classical / intuitionistic / lean kernel - MleanCoP, - IleanCoP, - NanoCoP, - - // Tier 5g: Tableau-prover generator for arbitrary modal logics - MetTeL2, - - // Tier 5h: Description-logic reasoners (OWL EL / OWL DL). - // ELK is the EL-profile specialist; Konclude handles full SROIQ. - ELK, - Konclude, - - // Tier 5i: Probabilistic model checking (modern PRISM successor). - Storm, - - // Tier 5j: B-method / Event-B model checker. - ProB, - - // Tier 5k: Computational-cryptography proof assistant - // (game-based, interactive). - EasyCrypt, - - // Tier 5l: Computational-cryptography automated prover - // (game-hopping, complementary to EasyCrypt). - CryptoVerif, - - // Tier 6: Dependent types + effects, auto-active, orchestration - FStar, - Dafny, - Why3, - - // Tier 6b: Refinement-types + SPARK auto-active - GNATprove, // SPARK/Ada — Why3 + Z3/CVC5/Alt-Ergo backend - Stainless, // Scala / Inox refinement-types - LiquidHaskell, // GHC plugin refinement-types - - // Tier 7: Specialized / niche - TLAPS, - Twelf, - Nuprl, - Minlog, - Imandra, - - // Tier 8: Constraint solvers - GLPK, - SCIP, - MiniZinc, - Chuffed, - ORTools, - - // Prover oracles (internal structural validators) - TypedWasm, - - // Tier 9: Model checkers and program verifiers - SPIN, - CBMC, - SeaHorn, - - // Tier 9: SAT Solvers - CaDiCaL, - Kissat, - MiniSat, - - // Tier 9: Model checkers (extended) - NuSMV, - TLC, - Alloy, - Prism, - UPPAAL, - - // Tier 9: Program verifiers (deductive) - FramaC, - - // Tier 9: Permission-based program verifiers - Viper, - - // Tier 9: Security protocol verifiers - Tamarin, - ProVerif, - - // Tier 9: Deductive Java verifiers (JavaDL + JML) - KeY, - - // Tier 10: Delta-complete SMT solvers - DReal, - - // Tier 10: Logic synthesis & hardware verification - ABC, - - // Tier 10: GPU kernel verification - /// GPUVerify — verifies CUDA/OpenCL kernels for data races and barrier - /// divergence. Translates GPU kernels to Boogie/BPL then uses Z3/CVC4 - /// as the backend SMT solver. Input: `.cu` (CUDA) or `.cl` (OpenCL). - GPUVerify, - /// Faial — detects data races in GPU parallel kernels via access pattern - /// analysis. Lighter-weight than GPUVerify; focuses on CUDA shared-memory - /// race freedom without a Boogie translation step. - Faial, - - // Tier 11: HP type-checker ecosystem. These dispatch through one - // unified HPEcosystemBackend that routes to the real HP upstreams - // (TypeLL, Katagoria, tropical-resource-typing). They are - // type-discipline views rather than separate binaries. - // - // Exhaustive enumeration of every type discipline we intend to support. - // Adding a variant here is cheap (dispatch-level only); the goal is to - // never have to re-open this enum once the ecosystem grows. See - // `src/rust/disciplines/` for the family grouping and katagoria pipeline. - TypeLL, - KatagoriaVerifier, - TropicalTypeChecker, - ChoreographicTypeChecker, - EpistemicTypeChecker, - EchoTypeChecker, - SessionTypeChecker, - ModalTypeChecker, - QTTTypeChecker, - EffectRowTypeChecker, - DependentTypeChecker, - RefinementTypeChecker, - // Foundations - OrdinaryTypeChecker, - // Polymorphism family - PhantomTypeChecker, - PolymorphicTypeChecker, - ExistentialTypeChecker, - HigherKindedTypeChecker, - RowTypeChecker, - // Subtyping family - SubtypingTypeChecker, - IntersectionTypeChecker, - UnionTypeChecker, - GradualTypeChecker, - // Dependent / refinement family (siblings of Dependent/Refinement) - HoareTypeChecker, - IndexedTypeChecker, - // Substructural family (siblings / specialisations of QTT) - LinearTypeChecker, - AffineTypeChecker, - RelevantTypeChecker, - OrderedTypeChecker, - UniquenessTypeChecker, - // Mutability / capability family - ImmutableTypeChecker, - CapabilityTypeChecker, - BunchedTypeChecker, - // Modal family (siblings of Modal/Epistemic) - TemporalTypeChecker, - ProvabilityTypeChecker, - // Effects / coeffects family (siblings of EffectRow) - ImpureTypeChecker, - CoeffectTypeChecker, - ProbabilisticTypeChecker, - // Process / communication family (siblings of Session/Choreographic/Echo) - DyadicTypeChecker, - // Homotopy foundations - HomotopyTypeChecker, - CubicalTypeChecker, - /// Nominal logic / HOAS / λ-tree syntax dispatcher. Added 2026-04-18 as - /// an honest one-time correction — nominal logic was missed in the - /// original 40-variant exhaustive enumeration. See - /// `src/rust/disciplines/mod.rs :: TypeDiscipline::Nominal` for the - /// full rationale. - NominalTypeChecker, - /// Abella — classical Axis-1 prover for nominal logic / HOAS. - /// Two-level logic (λProlog specification + sequent reasoning with - /// the ∇ generic quantifier). Sibling to Twelf in logical framework - /// style but with distinct proof theory. - Abella, - /// Dedukti — universal λΠ-modulo framework. Already in echidna as - /// a proof-exchange format (`src/rust/exchange/dedukti.rs`); this - /// variant adds the prover-as-solver role (invoking `dkcheck` / - /// `lambdapi` to typecheck a `.dk` source end-to-end). - Dedukti, - /// Cameleer — OCaml front-end for Why3 via GOSPEL contracts. - /// Thin pipeline over Why3's solver fleet; own variant so the - /// OCaml-proofs niche gets its own corpus slot and port-pairs - /// with F*/Dafny are trackable for the arbiter. - Cameleer, - /// ACL2s — sibling dialect to ACL2 with richer type annotations. - /// Different binary, different default libraries, different - /// tactic distributions; separate variant keeps the corpus slot - /// distinct from ACL2 proper. - ACL2s, - /// Isabelle/ZF — Isabelle with Zermelo-Fraenkel set-theory - /// object logic. Same `isabelle` binary as Isabelle/HOL but - /// different session name and stdlib; distinct proof style - /// and theorem namespace warrant a distinct slot. - IsabelleZF, - /// Boogie — intermediate verification language standalone - /// backend. Currently reached via Viper; exposing directly lets - /// echidna consume `.bpl` programs without a Viper wrapper - /// (e.g. Dafny-generated output, Chalice, VCC front-ends). - Boogie, - // Phase 4 "variety" batch (2026-04-18) — from the prover story's - // unique-and-unusual + pure-variety lists. Each genuinely distinct - // from what echidna already covers; skipping Coq-variants - // (Edukera, Bedrock2, CompCert) and F*-libraries (LowStar) since - // those don't warrant new ProverKind slots. - /// Naproche — controlled natural-language (ForTheL) proof checker. - /// Only text-style prover in echidna's roster; token distribution - /// unlike any other. - Naproche, - /// Matita — Bologna's Calculus of Inductive Constructions variant. - /// Coq-adjacent but semantically distinct enough to deserve its - /// own corpus slot. - Matita, - /// Arend — JetBrains's cubical HoTT prover. Distinct from Cubical - /// Agda in having path primitives as first-class syntax and IDE - /// tooling. Co-serves `TypeDiscipline::Cubical`. - Arend, - /// Athena — Arkoudas's denotational-proof-language with - /// intermixed deductive and computational phases. - Athena, - /// λProlog — higher-order logic programming with HOAS (Teyjus / - /// Elpi implementations). Co-serves `TypeDiscipline::Nominal` - /// alongside Abella. - LambdaProlog, - /// Mercury — pure logic programming with static types and modes. - /// Proof-adjacent via termination and determinism proofs. - Mercury, - /// Nitpick — Isabelle-integrated counter-example finder. - /// Produces refutations; corpus records are negative-class data - /// balancing the otherwise positive-only proof corpus. - Nitpick, - /// Nunchaku — standalone model / counter-example finder for HOL. - /// Sibling to Nitpick; same negative-class story but not - /// Isabelle-coupled, wider input format range. - Nunchaku, - /// Cubical Agda — Agda in --cubical mode; HIT, univalence, path types. - CubicalAgda, - /// Zipperposition — first-order + higher-order ATP (TPTP/TSTP output). - Zipperposition, - /// Prover9 — equational/clause-based ATP (McCune); pairs with Mace4. - Prover9, - /// OpenSMT — SMT solver with Craig interpolant generation. - OpenSmt, - /// SMT-RAT — nonlinear arithmetic SMT (NIA/NRA) from RWTH Aachen. - SmtRat, - /// Rocq — the 2024 Coq community rename; detects `rocq` binary first. - Rocq, - /// UPPAAL Stratego — strategy synthesis + stochastic model checking. - UppaalStratego, - /// MizAR — automated reasoning integrated with the Mizar Mathematical Library. - MizAR, -} - -impl ProverKind { - /// True if this kind is served by the unified HP-ecosystem backend. - pub fn is_hp_ecosystem(&self) -> bool { - matches!( - self, - ProverKind::TypeLL - | ProverKind::KatagoriaVerifier - | ProverKind::TropicalTypeChecker - | ProverKind::ChoreographicTypeChecker - | ProverKind::EpistemicTypeChecker - | ProverKind::EchoTypeChecker - | ProverKind::SessionTypeChecker - | ProverKind::ModalTypeChecker - | ProverKind::QTTTypeChecker - | ProverKind::EffectRowTypeChecker - | ProverKind::DependentTypeChecker - | ProverKind::RefinementTypeChecker - | ProverKind::OrdinaryTypeChecker - | ProverKind::PhantomTypeChecker - | ProverKind::PolymorphicTypeChecker - | ProverKind::ExistentialTypeChecker - | ProverKind::HigherKindedTypeChecker - | ProverKind::RowTypeChecker - | ProverKind::SubtypingTypeChecker - | ProverKind::IntersectionTypeChecker - | ProverKind::UnionTypeChecker - | ProverKind::GradualTypeChecker - | ProverKind::HoareTypeChecker - | ProverKind::IndexedTypeChecker - | ProverKind::LinearTypeChecker - | ProverKind::AffineTypeChecker - | ProverKind::RelevantTypeChecker - | ProverKind::OrderedTypeChecker - | ProverKind::UniquenessTypeChecker - | ProverKind::ImmutableTypeChecker - | ProverKind::CapabilityTypeChecker - | ProverKind::BunchedTypeChecker - | ProverKind::TemporalTypeChecker - | ProverKind::ProvabilityTypeChecker - | ProverKind::ImpureTypeChecker - | ProverKind::CoeffectTypeChecker - | ProverKind::ProbabilisticTypeChecker - | ProverKind::DyadicTypeChecker - | ProverKind::HomotopyTypeChecker - | ProverKind::CubicalTypeChecker - | ProverKind::NominalTypeChecker - ) - } -} - -impl std::str::FromStr for ProverKind { - type Err = anyhow::Error; - - fn from_str(s: &str) -> Result { - match s.to_lowercase().as_str() { - "agda" => Ok(ProverKind::Agda), - "coq" => Ok(ProverKind::Coq), - "lean" => Ok(ProverKind::Lean), - "isabelle" => Ok(ProverKind::Isabelle), - "z3" => Ok(ProverKind::Z3), - "cvc5" => Ok(ProverKind::CVC5), - "metamath" => Ok(ProverKind::Metamath), - "hollight" | "hol-light" => Ok(ProverKind::HOLLight), - "mizar" => Ok(ProverKind::Mizar), - "pvs" => Ok(ProverKind::PVS), - "acl2" => Ok(ProverKind::ACL2), - "hol4" => Ok(ProverKind::HOL4), - "idris2" | "idris" => Ok(ProverKind::Idris2), - "lean3" | "lean-3" | "lean3-legacy" | "mathlib3" => Ok(ProverKind::Lean3), - "vampire" => Ok(ProverKind::Vampire), - "eprover" | "e" => Ok(ProverKind::EProver), - "spass" => Ok(ProverKind::SPASS), - "altergo" | "alt-ergo" => Ok(ProverKind::AltErgo), - "leo3" | "leo-iii" | "leo-3" => Ok(ProverKind::Leo3), - "satallax" => Ok(ProverKind::Satallax), - "lash" => Ok(ProverKind::Lash), - "agsyhol" | "agsy-hol" => Ok(ProverKind::AgsyHOL), - "iprover" | "iprover-eq" => Ok(ProverKind::IProver), - "princess" => Ok(ProverKind::Princess), - "twee" => Ok(ProverKind::Twee), - "metitarski" | "metit" => Ok(ProverKind::MetiTarski), - "csi" => Ok(ProverKind::CSI), - "aprove" => Ok(ProverKind::AProVE), - "keymaerax" | "keymaera-x" | "keymaera_x" | "kyx" => Ok(ProverKind::KeYmaeraX), - "qepcad" | "qepcad-b" | "qepcad_b" => Ok(ProverKind::Qepcad), - "redlog" => Ok(ProverKind::Redlog), - "mleancop" | "mlean-cop" | "mlean_cop" => Ok(ProverKind::MleanCoP), - "ileancop" | "ilean-cop" | "ilean_cop" => Ok(ProverKind::IleanCoP), - "nanocop" | "nano-cop" | "nano_cop" => Ok(ProverKind::NanoCoP), - "mettel2" | "mettel-2" | "mettel" => Ok(ProverKind::MetTeL2), - "elk" | "elk-reasoner" => Ok(ProverKind::ELK), - "konclude" => Ok(ProverKind::Konclude), - "storm" | "stormpy" | "storm-checker" => Ok(ProverKind::Storm), - "prob" | "probcli" | "prob-cli" => Ok(ProverKind::ProB), - "easycrypt" | "easy-crypt" | "ec-prover" => Ok(ProverKind::EasyCrypt), - "cryptoverif" | "crypto-verif" | "cryptoverif-prover" => Ok(ProverKind::CryptoVerif), - "fstar" | "f*" | "f-star" => Ok(ProverKind::FStar), - "dafny" => Ok(ProverKind::Dafny), - "why3" => Ok(ProverKind::Why3), - "gnatprove" | "spark" | "ada" => Ok(ProverKind::GNATprove), - "stainless" | "scala-stainless" => Ok(ProverKind::Stainless), - "liquid" | "liquid-haskell" | "liquidhaskell" | "lh" => Ok(ProverKind::LiquidHaskell), - "tlaps" | "tla+" => Ok(ProverKind::TLAPS), - "twelf" => Ok(ProverKind::Twelf), - "nuprl" => Ok(ProverKind::Nuprl), - "minlog" => Ok(ProverKind::Minlog), - "imandra" => Ok(ProverKind::Imandra), - "glpk" => Ok(ProverKind::GLPK), - "scip" => Ok(ProverKind::SCIP), - "minizinc" | "mzn" => Ok(ProverKind::MiniZinc), - "chuffed" => Ok(ProverKind::Chuffed), - "ortools" | "or-tools" => Ok(ProverKind::ORTools), - "typedwasm" | "typed-wasm" | "typed_wasm" | "twasm" => Ok(ProverKind::TypedWasm), - "spin" | "promela" => Ok(ProverKind::SPIN), - "cbmc" | "c-bounded" => Ok(ProverKind::CBMC), - "seahorn" | "sea" | "sea-horn" => Ok(ProverKind::SeaHorn), - "cadical" => Ok(ProverKind::CaDiCaL), - "kissat" => Ok(ProverKind::Kissat), - "minisat" | "mini-sat" => Ok(ProverKind::MiniSat), - "nusmv" | "nuxmv" => Ok(ProverKind::NuSMV), - "tlc" | "tlc2" => Ok(ProverKind::TLC), - "alloy" => Ok(ProverKind::Alloy), - "prism" => Ok(ProverKind::Prism), - "uppaal" | "verifyta" => Ok(ProverKind::UPPAAL), - "framac" | "frama-c" | "frama_c" | "wp" => Ok(ProverKind::FramaC), - "viper" | "silicon" | "carbon" => Ok(ProverKind::Viper), - "tamarin" | "tamarin-prover" | "spthy" => Ok(ProverKind::Tamarin), - "proverif" | "pv" => Ok(ProverKind::ProVerif), - "key" | "key-project" | "javadl" => Ok(ProverKind::KeY), - "dreal" | "d-real" | "dreal4" => Ok(ProverKind::DReal), - "abc" | "berkeley-abc" => Ok(ProverKind::ABC), - "gpuverify" | "gpu-verify" | "gpu_verify" => Ok(ProverKind::GPUVerify), - "faial" | "faial-drf" => Ok(ProverKind::Faial), - "typell" | "type-ll" | "typell-kernel" => Ok(ProverKind::TypeLL), - "katagoria" | "katagoriaverifier" | "katagoria-verifier" => { - Ok(ProverKind::KatagoriaVerifier) - }, - "tropicaltypechecker" | "tropical" | "tropical-type-checker" => { - Ok(ProverKind::TropicalTypeChecker) - }, - "choreographictypechecker" | "choreographic" => { - Ok(ProverKind::ChoreographicTypeChecker) - }, - "epistemictypechecker" | "epistemic" => Ok(ProverKind::EpistemicTypeChecker), - "echotypechecker" | "echo" => Ok(ProverKind::EchoTypeChecker), - "sessiontypechecker" | "session" => Ok(ProverKind::SessionTypeChecker), - "modaltypechecker" | "modal" => Ok(ProverKind::ModalTypeChecker), - "qtttypechecker" | "qtt" | "quantitative" => Ok(ProverKind::QTTTypeChecker), - "effectrowtypechecker" | "effect-row" | "effectrow" => { - Ok(ProverKind::EffectRowTypeChecker) - }, - "dependenttypechecker" | "dependent" => Ok(ProverKind::DependentTypeChecker), - "refinementtypechecker" | "refinement" => Ok(ProverKind::RefinementTypeChecker), - "ordinarytypechecker" | "ordinary" | "simple" | "simply-typed" | "stlc" => { - Ok(ProverKind::OrdinaryTypeChecker) - }, - "phantomtypechecker" | "phantom" => Ok(ProverKind::PhantomTypeChecker), - "polymorphictypechecker" | "polymorphic" | "systemf" | "system-f" | "parametric" => { - Ok(ProverKind::PolymorphicTypeChecker) - }, - "existentialtypechecker" | "existential" | "packed" => { - Ok(ProverKind::ExistentialTypeChecker) - }, - "higherkindedtypechecker" | "higher-kinded" | "higherkinded" | "hkt" | "hk" => { - Ok(ProverKind::HigherKindedTypeChecker) - }, - "rowtypechecker" | "row" | "row-polymorphic" | "row-polymorphism" => { - Ok(ProverKind::RowTypeChecker) - }, - "subtypingtypechecker" | "subtyping" | "sub" => Ok(ProverKind::SubtypingTypeChecker), - "intersectiontypechecker" | "intersection" | "inter" => { - Ok(ProverKind::IntersectionTypeChecker) - }, - "uniontypechecker" | "union" => Ok(ProverKind::UnionTypeChecker), - "gradualtypechecker" | "gradual" | "gradual-typing" => { - Ok(ProverKind::GradualTypeChecker) - }, - "hoaretypechecker" | "hoare" | "hoare-types" => Ok(ProverKind::HoareTypeChecker), - "indexedtypechecker" | "indexed" | "indexed-monad" | "indexed-monads" => { - Ok(ProverKind::IndexedTypeChecker) - }, - "lineartypechecker" | "linear" | "linear-types" => Ok(ProverKind::LinearTypeChecker), - "affinetypechecker" | "affine" | "affine-types" => Ok(ProverKind::AffineTypeChecker), - "relevanttypechecker" | "relevant" | "relevant-types" => { - Ok(ProverKind::RelevantTypeChecker) - }, - "orderedtypechecker" | "ordered" | "ordered-logic" | "no-exchange" => { - Ok(ProverKind::OrderedTypeChecker) - }, - "uniquenesstypechecker" | "uniqueness" | "unique" | "unique-types" => { - Ok(ProverKind::UniquenessTypeChecker) - }, - "immutabletypechecker" | "immutable" | "frozen" | "const-types" => { - Ok(ProverKind::ImmutableTypeChecker) - }, - "capabilitytypechecker" | "capability" | "cap" | "capability-types" => { - Ok(ProverKind::CapabilityTypeChecker) - }, - "bunchedtypechecker" | "bunched" | "bi" | "bi-logic" | "separation" => { - Ok(ProverKind::BunchedTypeChecker) - }, - "temporaltypechecker" | "temporal" | "ltl" | "ctl" => { - Ok(ProverKind::TemporalTypeChecker) - }, - "provabilitytypechecker" | "provability" | "lob" | "löb" | "gl" => { - Ok(ProverKind::ProvabilityTypeChecker) - }, - "impuretypechecker" | "impure" | "effect-tracked" => Ok(ProverKind::ImpureTypeChecker), - "coeffecttypechecker" | "coeffect" | "graded-context" | "coeffects" => { - Ok(ProverKind::CoeffectTypeChecker) - }, - "probabilistictypechecker" | "probabilistic" | "prob-types" => { - Ok(ProverKind::ProbabilisticTypeChecker) - }, - "dyadictypechecker" | "dyadic" | "binary-channel" | "dyadic-session" => { - Ok(ProverKind::DyadicTypeChecker) - }, - "homotopytypechecker" | "homotopy" | "hott" => Ok(ProverKind::HomotopyTypeChecker), - "cubicaltypechecker" | "cubical" | "cubical-tt" => Ok(ProverKind::CubicalTypeChecker), - "nominaltypechecker" | "nominal" | "hoas" | "lambda-tree" => { - Ok(ProverKind::NominalTypeChecker) - }, - "abella" => Ok(ProverKind::Abella), - "dedukti" | "dkcheck" | "lambdapi" => Ok(ProverKind::Dedukti), - "cameleer" | "gospel" => Ok(ProverKind::Cameleer), - "acl2s" | "acl2-s" => Ok(ProverKind::ACL2s), - "isabellezf" | "isabelle-zf" | "isabelle/zf" | "zf" => Ok(ProverKind::IsabelleZF), - "boogie" | "bpl" => Ok(ProverKind::Boogie), - "naproche" | "forthel" | "ftl" => Ok(ProverKind::Naproche), - "matita" => Ok(ProverKind::Matita), - "arend" => Ok(ProverKind::Arend), - "athena" => Ok(ProverKind::Athena), - "lambdaprolog" | "lambda-prolog" | "teyjus" | "elpi" => Ok(ProverKind::LambdaProlog), - "mercury" | "mmc" => Ok(ProverKind::Mercury), - "nitpick" => Ok(ProverKind::Nitpick), - "nunchaku" => Ok(ProverKind::Nunchaku), - "cubicalagda" | "cubical-agda" | "agda-cubical" => Ok(ProverKind::CubicalAgda), - "zipperposition" => Ok(ProverKind::Zipperposition), - "prover9" => Ok(ProverKind::Prover9), - "opensmt" | "open-smt" => Ok(ProverKind::OpenSmt), - "smtrat" | "smt-rat" => Ok(ProverKind::SmtRat), - "rocq" | "rocq-compile" => Ok(ProverKind::Rocq), - "uppaal-stratego" | "stratego" => Ok(ProverKind::UppaalStratego), - "mizar-ar" | "mizatp" | "mizar-atp" => Ok(ProverKind::MizAR), - _ => Err(anyhow::anyhow!("Unknown prover: {}", s)), - } - } -} - -impl std::fmt::Display for ProverKind { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "{:?}", self) - } -} - -impl ProverKind { - /// All core provers for 1.0 (12 total) - pub fn all_core() -> Vec { - vec![ - ProverKind::Agda, - ProverKind::Coq, - ProverKind::Lean, - ProverKind::Isabelle, - ProverKind::Z3, - ProverKind::CVC5, - ProverKind::Metamath, - ProverKind::HOLLight, - ProverKind::Mizar, - ProverKind::PVS, - ProverKind::ACL2, - ProverKind::HOL4, - ] - } - - /// All provers including extended coverage - pub fn all() -> Vec { - let mut provers = Self::all_core(); - provers.extend_from_slice(&[ - ProverKind::Idris2, - ProverKind::Lean3, - ProverKind::Vampire, - ProverKind::EProver, - ProverKind::SPASS, - ProverKind::AltErgo, - ProverKind::FStar, - ProverKind::Dafny, - ProverKind::Why3, - ProverKind::TLAPS, - ProverKind::Twelf, - ProverKind::Nuprl, - ProverKind::Minlog, - ProverKind::Imandra, - ProverKind::GLPK, - ProverKind::SCIP, - ProverKind::MiniZinc, - ProverKind::Chuffed, - ProverKind::ORTools, - ProverKind::TypedWasm, - ProverKind::SPIN, - ProverKind::CBMC, - ProverKind::SeaHorn, - ProverKind::CaDiCaL, - ProverKind::Kissat, - ProverKind::MiniSat, - ProverKind::NuSMV, - ProverKind::TLC, - ProverKind::Alloy, - ProverKind::Prism, - ProverKind::UPPAAL, - ProverKind::FramaC, - ProverKind::Viper, - ProverKind::Tamarin, - ProverKind::ProVerif, - ProverKind::KeY, - ProverKind::DReal, - ProverKind::ABC, - ProverKind::GPUVerify, - ProverKind::Faial, - ProverKind::CubicalAgda, - ProverKind::Zipperposition, - ProverKind::Prover9, - ProverKind::OpenSmt, - ProverKind::SmtRat, - ProverKind::Rocq, - ProverKind::UppaalStratego, - ProverKind::MizAR, - ProverKind::IProver, - ProverKind::Princess, - ProverKind::Twee, - ProverKind::MetiTarski, - ProverKind::CSI, - ProverKind::AProVE, - ProverKind::KeYmaeraX, - ProverKind::Qepcad, - ProverKind::Redlog, - ProverKind::MleanCoP, - ProverKind::IleanCoP, - ProverKind::NanoCoP, - ProverKind::MetTeL2, - ProverKind::ELK, - ProverKind::Konclude, - ProverKind::Storm, - ProverKind::ProB, - ProverKind::EasyCrypt, - ProverKind::CryptoVerif, - ]); - provers - } - - /// Get complexity rating (1-5, lower is easier) - pub fn complexity(&self) -> u8 { - match self { - ProverKind::Metamath => 2, - ProverKind::Agda => 3, - ProverKind::HOLLight => 3, - ProverKind::Mizar => 3, - ProverKind::Lean => 3, - ProverKind::Coq => 3, - ProverKind::Isabelle => 4, - ProverKind::Z3 => 2, - ProverKind::CVC5 => 2, - ProverKind::PVS => 4, - ProverKind::ACL2 => 4, - ProverKind::HOL4 => 5, - ProverKind::Idris2 => 3, - ProverKind::Lean3 => 3, // Same complexity as Lean 4. - ProverKind::Abella => 3, // Two-level logic, HOAS proof state. - ProverKind::Dedukti => 3, // λΠ-modulo framework. - ProverKind::Cameleer => 2, // Thin OCaml→Why3 pipeline. - ProverKind::ACL2s => 4, // Sibling to ACL2. - ProverKind::IsabelleZF => 4, // Sibling to Isabelle/HOL. - ProverKind::Boogie => 2, // Intermediate verification language. - ProverKind::Naproche => 3, // Controlled-NL parsing non-trivial. - ProverKind::Matita => 3, // CIC variant, same family as Coq. - ProverKind::Arend => 3, // Cubical HoTT. - ProverKind::Athena => 4, // Denotational + rewriting engine. - ProverKind::LambdaProlog => 3, // HOAS logic programming. - ProverKind::Mercury => 3, // Logic programming with types/modes. - ProverKind::Nitpick => 2, // Isabelle-wrapped counter-example finder. - ProverKind::Nunchaku => 2, // Standalone counter-example finder. - ProverKind::CubicalAgda => 4, // Cubical HoTT; harder than plain Agda. - ProverKind::Zipperposition => 2, // Automated ATP. - ProverKind::Prover9 => 2, // Classic equational ATP. - ProverKind::OpenSmt => 2, // SMT solver. - ProverKind::SmtRat => 3, // Nonlinear arithmetic needs careful encoding. - ProverKind::Rocq => 3, // Same as Coq. - ProverKind::UppaalStratego => 4, // Strategy synthesis is hard. - ProverKind::MizAR => 3, // Mizar with ATP assist. - ProverKind::Vampire => 2, // Automated, relatively simple - ProverKind::EProver => 2, // Similar to Vampire - ProverKind::SPASS => 2, // Automated FOL - ProverKind::AltErgo => 2, // SMT + FOL - - ProverKind::FStar => 3, // Dependent types + effects - ProverKind::Dafny => 2, // Auto-active - ProverKind::Why3 => 3, // Multi-prover orchestration - ProverKind::GNATprove => 3, // SPARK auto-active via Why3 backends - ProverKind::Stainless => 3, // Scala/Inox refinement types - ProverKind::LiquidHaskell => 3, // GHC plugin refinement types - ProverKind::TLAPS => 4, // TLA+ proof system - ProverKind::Twelf => 4, // Logical framework - ProverKind::Nuprl => 4, // Constructive type theory - ProverKind::Minlog => 4, // Minimal logic - ProverKind::Imandra => 3, // ML-based reasoning - ProverKind::GLPK => 2, // LP solver - ProverKind::SCIP => 3, // MINLP solver - ProverKind::MiniZinc => 2, // Constraint modelling - ProverKind::Chuffed => 2, // CP solver - ProverKind::ORTools => 2, // Constraint/optimization solver - ProverKind::TypedWasm => 3, // Internal oracle, structural analysis - ProverKind::SPIN => 3, // Model checker, Promela language - ProverKind::CBMC => 2, // Bounded model checker, C input - ProverKind::SeaHorn => 2, // LLVM-based verifier, abstract interpretation + CHC - ProverKind::CaDiCaL => 1, // SAT solver, DIMACS CNF - ProverKind::Kissat => 1, // SAT solver, DIMACS CNF - ProverKind::MiniSat => 1, // SAT solver, DIMACS CNF - ProverKind::NuSMV => 3, // Symbolic model checker, SMV language - ProverKind::TLC => 3, // TLA+ model checker - ProverKind::Alloy => 3, // Relational model finder - ProverKind::Prism => 3, // Probabilistic model checker - ProverKind::UPPAAL => 3, // Timed automata model checker - ProverKind::FramaC => 3, // Deductive C verifier (ACSL + WP) - ProverKind::Viper => 3, // Permission-based verifier (Silver + Silicon/Carbon) - ProverKind::Tamarin => 3, // Security protocol verifier, multiset rewriting - ProverKind::ProVerif => 2, // Automated protocol verifier, applied pi-calculus - ProverKind::KeY => 3, // Deductive Java verifier (JavaDL + JML), auto + interactive - ProverKind::DReal => 2, // Automated delta-complete SMT solver, NRA - ProverKind::ABC => 2, // Automated hardware verification, AIG-based - ProverKind::GPUVerify => 2, // Automated GPU kernel verifier (Boogie/Z3 backend) - ProverKind::Faial => 2, // Lightweight GPU race detector (access pattern analysis) - // Phase 1a: Higher-order ATPs - ProverKind::Leo3 => 3, // Leo III HOL-to-TPTP translator + ATP - ProverKind::Satallax => 3, // Satallax HOL-based ATP - ProverKind::Lash => 3, // Lash higher-order prover - ProverKind::AgsyHOL => 4, // Agsy HOL dependent-type prover - // Phase 1b: Frontier first-order provers - ProverKind::IProver => 2, // Competitive ATP, standard FOL - ProverKind::Princess => 3, // LA-extended ATP - ProverKind::Twee => 2, // Equational only, deterministic - ProverKind::MetiTarski => 3, // Transcendental function encoding - ProverKind::CSI => 3, // TRS/CTRS parsing + CPF output - ProverKind::AProVE => 3, // TRS/XTC parsing - ProverKind::KeYmaeraX => 4, // dL + hybrid programs + tactic language - ProverKind::Qepcad => 4, // CAD doubly-exponential in variable count - ProverKind::Redlog => 3, // virtual substitution + CAD - ProverKind::MleanCoP => 3, // classical connection-method + equality - ProverKind::IleanCoP => 3, // intuitionistic connection-method - ProverKind::NanoCoP => 3, // small-kernel connection-method - ProverKind::MetTeL2 => 4, // JVM tableau-generator + spec config - // Phase 4: DL + probabilistic + B-method + computational crypto - ProverKind::ELK => 3, // consequence-based EL kernel - ProverKind::Konclude => 4, // full SROIQ tableau saturation - ProverKind::Storm => 3, // numerical fixed-point computation - ProverKind::ProB => 3, // B-method semantics + constraint engine - ProverKind::EasyCrypt => 4, // probabilistic relational HL + tactics - ProverKind::CryptoVerif => 4, // game-hopping + indistinguishability lib - // HP type-checker ecosystem: complexity 3 — they are real - // type-checkers with non-trivial unification/elaboration. - // Heavier disciplines (HoTT/Cubical, Hoare) rate 4. - ProverKind::TypeLL - | ProverKind::KatagoriaVerifier - | ProverKind::TropicalTypeChecker - | ProverKind::ChoreographicTypeChecker - | ProverKind::EpistemicTypeChecker - | ProverKind::EchoTypeChecker - | ProverKind::SessionTypeChecker - | ProverKind::ModalTypeChecker - | ProverKind::QTTTypeChecker - | ProverKind::EffectRowTypeChecker - | ProverKind::DependentTypeChecker - | ProverKind::RefinementTypeChecker - | ProverKind::PhantomTypeChecker - | ProverKind::PolymorphicTypeChecker - | ProverKind::ExistentialTypeChecker - | ProverKind::HigherKindedTypeChecker - | ProverKind::RowTypeChecker - | ProverKind::SubtypingTypeChecker - | ProverKind::IntersectionTypeChecker - | ProverKind::UnionTypeChecker - | ProverKind::GradualTypeChecker - | ProverKind::IndexedTypeChecker - | ProverKind::LinearTypeChecker - | ProverKind::AffineTypeChecker - | ProverKind::RelevantTypeChecker - | ProverKind::OrderedTypeChecker - | ProverKind::UniquenessTypeChecker - | ProverKind::ImmutableTypeChecker - | ProverKind::CapabilityTypeChecker - | ProverKind::BunchedTypeChecker - | ProverKind::TemporalTypeChecker - | ProverKind::ProvabilityTypeChecker - | ProverKind::ImpureTypeChecker - | ProverKind::CoeffectTypeChecker - | ProverKind::ProbabilisticTypeChecker - | ProverKind::DyadicTypeChecker => 3, - // Heavier disciplines: Hoare triples (SL proofs), HoTT (univalence), - // Cubical (interval primitives). - ProverKind::HoareTypeChecker - | ProverKind::HomotopyTypeChecker - | ProverKind::CubicalTypeChecker - | ProverKind::NominalTypeChecker => 4, - // Baseline: simply-typed lambda calculus — cheap to check. - ProverKind::OrdinaryTypeChecker => 2, - } - } - - /// Get tier (1-5) - pub fn tier(&self) -> u8 { - match self { - ProverKind::Agda - | ProverKind::Coq - | ProverKind::Lean - | ProverKind::Isabelle - | ProverKind::Z3 - | ProverKind::CVC5 => 1, - - ProverKind::Metamath | ProverKind::HOLLight | ProverKind::Mizar => 2, - - ProverKind::PVS | ProverKind::ACL2 => 3, - - ProverKind::HOL4 => 4, - - // Extended tier (same as Tier 1 in capability) - ProverKind::Idris2 => 1, - ProverKind::Lean3 => 1, // Sibling to Lean 4. - // Tier 7 niche: specialized proof framework for HOAS / nominal. - ProverKind::Abella => 2, - ProverKind::Dedukti => 2, // Logical framework tier. - ProverKind::Cameleer => 2, // Auto-active via Why3. - ProverKind::ACL2s => 3, // Sibling to ACL2 (tier 3). - ProverKind::IsabelleZF => 1, // Sibling to Isabelle (tier 1). - ProverKind::Boogie => 5, // Deductive program verifier tier. - ProverKind::Naproche => 2, // Specialised, text-style. - ProverKind::Matita => 1, // Coq-adjacent, Tier 1 capability. - ProverKind::Arend => 1, // Cubical HoTT, Tier 1. - ProverKind::Athena => 4, // Niche framework. - ProverKind::LambdaProlog => 4, // Logical framework / HOAS. - ProverKind::Mercury => 4, // Specialised logic programming. - ProverKind::Nitpick => 5, // Counter-example finder tier. - ProverKind::Nunchaku => 5, // Counter-example finder tier. - ProverKind::CubicalAgda => 2, // Tier 2: HoTT proof assistant. - ProverKind::Zipperposition => 3, // Tier 3: HO-ATP. - ProverKind::Prover9 => 4, // Tier 4: classic ATP. - ProverKind::OpenSmt => 3, // Tier 3: interpolant SMT. - ProverKind::SmtRat => 5, // Tier 5: research NL SMT. - ProverKind::Rocq => 1, // Tier 1: Coq rename. - ProverKind::UppaalStratego => 4, // Tier 4: strategy synthesis. - ProverKind::MizAR => 3, // Tier 3: ATP-assisted Mizar. - - // Tier 5: First-Order ATPs - ProverKind::Vampire => 5, - ProverKind::EProver => 5, - ProverKind::SPASS => 5, - ProverKind::AltErgo => 5, - - // Tier 6: Dependent types + effects, auto-active - ProverKind::FStar => 1, // Small kernel, dependent types - ProverKind::Dafny => 2, // Auto-active (relies on Boogie->Z3) - ProverKind::Why3 => 2, // Multi-prover orchestration - ProverKind::GNATprove => 4, // SPARK — small-kernel via Why3 - ProverKind::Stainless => 3, // Scala refinement types - ProverKind::LiquidHaskell => 3, // GHC refinement types - - // Tier 7: Specialized / niche - ProverKind::TLAPS => 2, - ProverKind::Twelf => 4, - ProverKind::Nuprl => 4, - ProverKind::Minlog => 4, - ProverKind::Imandra => 2, - - // Tier 8: Constraint solvers - ProverKind::GLPK => 5, - ProverKind::SCIP => 5, - ProverKind::MiniZinc => 5, - ProverKind::Chuffed => 5, - ProverKind::ORTools => 5, - ProverKind::TypedWasm => 1, // Internal oracle, tier 1 capability - - // Tier 9: Model checkers and program verifiers - ProverKind::SPIN => 5, - ProverKind::CBMC => 5, - ProverKind::SeaHorn => 5, - - // Tier 9: SAT Solvers - ProverKind::CaDiCaL => 5, - ProverKind::Kissat => 5, - ProverKind::MiniSat => 5, - - // Tier 9: Model checkers (extended) - ProverKind::NuSMV => 5, - ProverKind::TLC => 5, - ProverKind::Alloy => 5, - ProverKind::Prism => 5, - ProverKind::UPPAAL => 5, - ProverKind::FramaC => 5, // Deductive program verifier - ProverKind::Viper => 5, // Permission-based program verifier - ProverKind::Tamarin => 5, // Security protocol verifier - ProverKind::ProVerif => 5, // Security protocol verifier (automated) - ProverKind::KeY => 5, // Deductive Java verifier - ProverKind::DReal => 5, // Delta-complete SMT solver (NRA/ODE) - ProverKind::ABC => 5, // Logic synthesis & hardware verification - ProverKind::GPUVerify => 5, // GPU kernel verifier (CUDA/OpenCL → Boogie → Z3) - ProverKind::Faial => 5, // Lightweight GPU data-race detector - // Phase 1a: Higher-order ATPs - ProverKind::Leo3 => 5, // Tier 5: HOL-to-TPTP translator - ProverKind::Satallax => 5, // Tier 5: HOL-based ATP - ProverKind::Lash => 5, // Tier 5: higher-order ATP - ProverKind::AgsyHOL => 5, // Tier 5: HOL dependent-type prover - // Phase 1b: Frontier first-order provers - ProverKind::IProver => 2, // Trust tier 2 (TPTP FOL) - ProverKind::Princess => 2, // Trust tier 2 (TPTP + LA) - ProverKind::Twee => 3, // Trust tier 3 (deterministic equational) - ProverKind::MetiTarski => 2, // Trust tier 2 (TPTP + transcendental) - ProverKind::CSI => 2, // Trust tier 2 (TRS/CPF) - ProverKind::AProVE => 2, // Trust tier 2 (TRS/XTC) - ProverKind::KeYmaeraX => 2, // Trust tier 2 (dL; QE delegated to external CAS) - ProverKind::Qepcad => 2, // Trust tier 2 (CAD; no machine-checked certificate) - ProverKind::Redlog => 2, // Trust tier 2 (parallel to QEPCAD) - ProverKind::MleanCoP => 2, // Trust tier 2 (classical leanCoP kernel) - ProverKind::IleanCoP => 3, // Trust tier 3 (intuitionistic kernel; small + checkable) - ProverKind::NanoCoP => 3, // Trust tier 3 (small kernel — Level-4 cohort) - ProverKind::MetTeL2 => 2, // Trust tier 2 (generated tableau correct by construction; spec unverified) - // Phase 4: DL + probabilistic + B-method + computational crypto. - ProverKind::ELK => 3, // Trust tier 3 (consequence-based, peer-reviewed soundness) - ProverKind::Konclude => 3, // Trust tier 3 (peer-reviewed tableau kernel) - ProverKind::Storm => 2, // Trust tier 2 (DD/symbolic engines, no certificate) - ProverKind::ProB => 2, // Trust tier 2 (constraint-based BMC, validated for railway) - ProverKind::EasyCrypt => 3, // Trust tier 3 (small kernel + Why3/SMT for VC discharge) - ProverKind::CryptoVerif => 3, // Trust tier 3 (small game-hopping engine, peer-reviewed) - // HP ecosystem — tier 11 (beyond the existing 10-tier scheme - // but placed as 3 here to share the ML guidance budget with - // dependent/interactive provers). - ProverKind::TypeLL - | ProverKind::KatagoriaVerifier - | ProverKind::TropicalTypeChecker - | ProverKind::ChoreographicTypeChecker - | ProverKind::EpistemicTypeChecker - | ProverKind::EchoTypeChecker - | ProverKind::SessionTypeChecker - | ProverKind::ModalTypeChecker - | ProverKind::QTTTypeChecker - | ProverKind::EffectRowTypeChecker - | ProverKind::DependentTypeChecker - | ProverKind::RefinementTypeChecker - | ProverKind::OrdinaryTypeChecker - | ProverKind::PhantomTypeChecker - | ProverKind::PolymorphicTypeChecker - | ProverKind::ExistentialTypeChecker - | ProverKind::HigherKindedTypeChecker - | ProverKind::RowTypeChecker - | ProverKind::SubtypingTypeChecker - | ProverKind::IntersectionTypeChecker - | ProverKind::UnionTypeChecker - | ProverKind::GradualTypeChecker - | ProverKind::HoareTypeChecker - | ProverKind::IndexedTypeChecker - | ProverKind::LinearTypeChecker - | ProverKind::AffineTypeChecker - | ProverKind::RelevantTypeChecker - | ProverKind::OrderedTypeChecker - | ProverKind::UniquenessTypeChecker - | ProverKind::ImmutableTypeChecker - | ProverKind::CapabilityTypeChecker - | ProverKind::BunchedTypeChecker - | ProverKind::TemporalTypeChecker - | ProverKind::ProvabilityTypeChecker - | ProverKind::ImpureTypeChecker - | ProverKind::CoeffectTypeChecker - | ProverKind::ProbabilisticTypeChecker - | ProverKind::DyadicTypeChecker - | ProverKind::HomotopyTypeChecker - | ProverKind::CubicalTypeChecker - | ProverKind::NominalTypeChecker => 3, - } - } - - /// Get expected implementation time in weeks - pub fn implementation_time(&self) -> f32 { - match self { - ProverKind::Metamath => 1.5, - ProverKind::Z3 | ProverKind::CVC5 => 1.0, - ProverKind::HOLLight | ProverKind::Mizar => 2.0, - ProverKind::Agda | ProverKind::Lean | ProverKind::Coq => 2.5, - ProverKind::Isabelle => 3.0, - ProverKind::PVS | ProverKind::ACL2 => 3.5, - ProverKind::HOL4 => 4.0, - ProverKind::Idris2 => 2.5, - ProverKind::Lean3 => 1.0, // Thin fork of Lean 4 backend. - ProverKind::Abella => 2.0, // New parser, HOAS proof state model. - ProverKind::Dedukti => 1.5, // Extends existing exchange module. - ProverKind::Cameleer => 1.0, // Thin wrapper over Why3. - ProverKind::ACL2s => 1.0, // Thin fork of ACL2. - ProverKind::IsabelleZF => 1.0, // Thin variant of Isabelle. - ProverKind::Boogie => 1.5, // Extract from Viper internals. - ProverKind::Naproche => 2.0, // Controlled-NL parser wrapper. - ProverKind::Matita => 2.0, // Coq-parser fork. - ProverKind::Arend => 2.0, // Cubical parser + elaborator. - ProverKind::Athena => 2.5, // Rich denotational framework. - ProverKind::LambdaProlog => 2.0, // HOAS parser + unifier. - ProverKind::Mercury => 2.0, // Logic programming interpreter bridge. - ProverKind::Nitpick => 1.0, // Thin wrapper over Isabelle. - ProverKind::Nunchaku => 1.5, // Standalone counter-example tool. - ProverKind::CubicalAgda => 2.5, // Thin fork of Agda backend. - ProverKind::Zipperposition => 1.5, // TSTP-output ATP. - ProverKind::Prover9 => 1.5, // Simple output parsing. - ProverKind::OpenSmt => 1.5, // SMT-LIB2 like CVC5. - ProverKind::SmtRat => 1.5, // Same pattern. - ProverKind::Rocq => 1.0, // Alias for Coq. - ProverKind::UppaalStratego => 2.0, // Fork of UPPAAL backend. - ProverKind::MizAR => 2.0, // Mizar ATP integration. - ProverKind::Vampire => 1.5, // Automated, TPTP format - ProverKind::EProver => 1.5, // Similar to Vampire - ProverKind::SPASS => 1.5, // DFG format - ProverKind::AltErgo => 1.5, // Native format - - ProverKind::FStar => 2.5, // Dependent types + effects - ProverKind::Dafny => 2.0, // Auto-active, Boogie pipeline - ProverKind::Why3 => 2.0, // Multi-prover - ProverKind::GNATprove => 3.0, // SPARK toolchain wrapping - ProverKind::Stainless => 2.5, // Scala JVM - ProverKind::LiquidHaskell => 2.5, // GHC plugin - ProverKind::TLAPS => 2.5, // TLA+ specific - ProverKind::Twelf => 3.0, // LF framework - ProverKind::Nuprl => 3.0, // Constructive type theory - ProverKind::Minlog => 2.5, // Minimal logic - ProverKind::Imandra => 2.0, // ML-based - ProverKind::GLPK => 1.0, // LP API - ProverKind::SCIP => 1.5, // MINLP API - ProverKind::MiniZinc => 1.0, // Constraint modelling - ProverKind::Chuffed => 1.0, // CP solver - ProverKind::ORTools => 1.5, // Constraint/optimization - ProverKind::TypedWasm => 2.0, // Internal oracle - ProverKind::SPIN => 1.5, // Model checker - ProverKind::CBMC => 1.5, // Bounded model checker - ProverKind::SeaHorn => 1.5, // LLVM-based CHC verifier - ProverKind::CaDiCaL => 1.0, // SAT solver, DIMACS CNF - ProverKind::Kissat => 1.0, // SAT solver, DIMACS CNF - ProverKind::MiniSat => 1.0, // SAT solver, DIMACS CNF - ProverKind::NuSMV => 1.5, // Symbolic model checker - ProverKind::TLC => 1.5, // TLA+ model checker - ProverKind::Alloy => 1.5, // Relational model finder - ProverKind::Prism => 1.5, // Probabilistic model checker - ProverKind::UPPAAL => 1.5, // Timed automata model checker - ProverKind::FramaC => 1.5, // Deductive C verifier - ProverKind::Viper => 2.0, // Permission-based verifier (Silver + two backends) - ProverKind::Tamarin => 2.0, // Security protocol verifier (.spthy) - ProverKind::ProVerif => 1.5, // Automated protocol verifier (.pv) - ProverKind::KeY => 2.0, // Deductive Java verifier (JavaDL + JML) - ProverKind::DReal => 1.0, // Automated SMT solver, SMT-LIB input - ProverKind::ABC => 1.5, // Hardware verification, AIGER/BLIF input - ProverKind::GPUVerify => 1.5, // GPU kernel verifier, CUDA/OpenCL input - ProverKind::Faial => 1.0, // Lightweight GPU race detector, CUDA input - ProverKind::IProver => 1.5, // First-order ATP with SZS output - ProverKind::Princess => 1.5, // SMT-based first-order solver - ProverKind::Twee => 1.5, // Equational logic (Knuth-Bendix) - ProverKind::MetiTarski => 1.5, // Transcendental arithmetic extension - ProverKind::CSI => 2.0, // Confluence/termination checker - ProverKind::AProVE => 2.0, // Automated termination verifier - ProverKind::KeYmaeraX => 2.5, // Hybrid systems / differential dynamic logic - ProverKind::Qepcad => 2.5, // CAD / real quantifier elimination - ProverKind::Redlog => 2.0, // REDUCE-CAS QE frontend - ProverKind::MleanCoP => 1.5, // Classical connection-method - ProverKind::IleanCoP => 2.0, // Intuitionistic connection-method - ProverKind::NanoCoP => 1.5, // Lean-kernel connection-method - ProverKind::MetTeL2 => 2.5, // Modal-logic tableau generator - // Phase 4: DL + probabilistic + B-method + computational crypto. - ProverKind::ELK => 1.5, // OWL EL classifier - ProverKind::Konclude => 2.0, // OWL DL tableau reasoner - ProverKind::Storm => 2.0, // Probabilistic model checker (PRISM successor) - ProverKind::ProB => 2.0, // B-method / Event-B model checker - ProverKind::EasyCrypt => 2.5, // Game-based crypto proofs - ProverKind::CryptoVerif => 2.5, // Automated computational-crypto prover - ProverKind::Leo3 => 2.5, // Higher-order ATP - ProverKind::Satallax => 2.5, // Higher-order ATP - ProverKind::Lash => 2.5, // Higher-order ATP - ProverKind::AgsyHOL => 2.5, // Higher-order ATP - ProverKind::TypeLL - | ProverKind::KatagoriaVerifier - | ProverKind::TropicalTypeChecker - | ProverKind::ChoreographicTypeChecker - | ProverKind::EpistemicTypeChecker - | ProverKind::EchoTypeChecker - | ProverKind::SessionTypeChecker - | ProverKind::ModalTypeChecker - | ProverKind::QTTTypeChecker - | ProverKind::EffectRowTypeChecker - | ProverKind::DependentTypeChecker - | ProverKind::RefinementTypeChecker - | ProverKind::OrdinaryTypeChecker - | ProverKind::PhantomTypeChecker - | ProverKind::PolymorphicTypeChecker - | ProverKind::ExistentialTypeChecker - | ProverKind::HigherKindedTypeChecker - | ProverKind::RowTypeChecker - | ProverKind::SubtypingTypeChecker - | ProverKind::IntersectionTypeChecker - | ProverKind::UnionTypeChecker - | ProverKind::GradualTypeChecker - | ProverKind::HoareTypeChecker - | ProverKind::IndexedTypeChecker - | ProverKind::LinearTypeChecker - | ProverKind::AffineTypeChecker - | ProverKind::RelevantTypeChecker - | ProverKind::OrderedTypeChecker - | ProverKind::UniquenessTypeChecker - | ProverKind::ImmutableTypeChecker - | ProverKind::CapabilityTypeChecker - | ProverKind::BunchedTypeChecker - | ProverKind::TemporalTypeChecker - | ProverKind::ProvabilityTypeChecker - | ProverKind::ImpureTypeChecker - | ProverKind::CoeffectTypeChecker - | ProverKind::ProbabilisticTypeChecker - | ProverKind::DyadicTypeChecker - | ProverKind::HomotopyTypeChecker - | ProverKind::CubicalTypeChecker - | ProverKind::NominalTypeChecker => 2.0, // HP ecosystem - } - } - - /// Default executable name for this prover (what to look for on PATH) - pub fn default_executable(&self) -> &'static str { - match self { - ProverKind::Agda => "agda", - ProverKind::Coq => "coqc", - ProverKind::Lean => "lean", - ProverKind::Isabelle => "isabelle", - ProverKind::Z3 => "z3", - ProverKind::CVC5 => "cvc5", - ProverKind::Metamath => "metamath", - ProverKind::HOLLight => "ocaml", - ProverKind::Mizar => "mizf", - ProverKind::PVS => "pvs", - ProverKind::ACL2 => "acl2", - ProverKind::HOL4 => "hol", - ProverKind::Idris2 => "idris2", - ProverKind::Lean3 => "lean3", - ProverKind::Abella => "abella", - ProverKind::Dedukti => "dkcheck", - ProverKind::Cameleer => "cameleer", - ProverKind::ACL2s => "acl2s", - ProverKind::IsabelleZF => "isabelle", // Same binary, different session. - ProverKind::Boogie => "boogie", - ProverKind::Naproche => "naproche", - ProverKind::Matita => "matitac", - ProverKind::Arend => "arend", - ProverKind::Athena => "athena", - ProverKind::LambdaProlog => "tjsim", - ProverKind::Mercury => "mmc", - ProverKind::Nitpick => "isabelle", // Shared binary via `isabelle process -e nitpick`. - ProverKind::Nunchaku => "nunchaku", - ProverKind::Vampire => "vampire", - ProverKind::EProver => "eprover", - ProverKind::SPASS => "SPASS", - ProverKind::AltErgo => "alt-ergo", - - ProverKind::FStar => "fstar.exe", - ProverKind::Dafny => "dafny", - ProverKind::Why3 => "why3", - ProverKind::GNATprove => "gnatprove", - ProverKind::Stainless => "stainless", - ProverKind::LiquidHaskell => "liquid", - ProverKind::TLAPS => "tlapm", - ProverKind::Twelf => "twelf-server", - ProverKind::Nuprl => "nuprl", - ProverKind::Minlog => "minlog", - ProverKind::Imandra => "imandra", - ProverKind::GLPK => "glpsol", - ProverKind::SCIP => "scip", - ProverKind::MiniZinc => "minizinc", - ProverKind::Chuffed => "fzn-chuffed", - ProverKind::ORTools => "ortools_solve", - ProverKind::TypedWasm => "idris2", // Validates via Idris2 ABI - ProverKind::SPIN => "spin", - ProverKind::CBMC => "cbmc", - ProverKind::SeaHorn => "sea", // SeaHorn verification framework CLI - ProverKind::CaDiCaL => "cadical", // CaDiCaL SAT solver - ProverKind::Kissat => "kissat", // Kissat SAT solver - ProverKind::MiniSat => "minisat", // MiniSat SAT solver - ProverKind::NuSMV => "nuXmv", // nuXmv / NuSMV model checker - ProverKind::TLC => "tlc2", // TLA+ model checker (Java) - ProverKind::Alloy => "alloy", // Alloy Analyzer (Java JAR) - ProverKind::Prism => "prism", // PRISM probabilistic model checker - ProverKind::UPPAAL => "verifyta", // UPPAAL verification engine - ProverKind::FramaC => "frama-c", // Frama-C platform (WP plugin) - ProverKind::Viper => "silicon", // Viper Silicon verifier (default backend) - ProverKind::Tamarin => "tamarin-prover", // Tamarin security protocol prover - ProverKind::ProVerif => "proverif", // ProVerif protocol verifier - ProverKind::KeY => "key", // KeY Java verifier (Java, headless mode) - ProverKind::DReal => "dreal", // dReal delta-complete SMT solver - ProverKind::ABC => "abc", // Berkeley ABC logic synthesis system - ProverKind::GPUVerify => "gpuverify", // GPUVerify CUDA/OpenCL kernel verifier - ProverKind::Faial => "faial-drf", // Faial data-race freedom checker - ProverKind::CubicalAgda => "agda", - ProverKind::Zipperposition => "zipperposition", - ProverKind::Prover9 => "prover9", - ProverKind::OpenSmt => "opensmt", - ProverKind::SmtRat => "smtrat", - ProverKind::Rocq => "rocq", - ProverKind::UppaalStratego => "stratego", - ProverKind::MizAR => "mizar-atp", - ProverKind::IProver => "iprover", - ProverKind::Princess => "princess", - ProverKind::Twee => "twee", - ProverKind::MetiTarski => "metit", - ProverKind::CSI => "csi", - ProverKind::AProVE => "aprove", - ProverKind::KeYmaeraX => "keymaerax", - ProverKind::Qepcad => "qepcad", - ProverKind::Redlog => "redcsl", - ProverKind::MleanCoP => "mleancop", - ProverKind::IleanCoP => "ileancop", - ProverKind::NanoCoP => "nanocop", - ProverKind::MetTeL2 => "mettel2", - ProverKind::ELK => "elk", - ProverKind::Konclude => "konclude", - ProverKind::Storm => "storm", - ProverKind::ProB => "probcli", - ProverKind::EasyCrypt => "easycrypt", - ProverKind::CryptoVerif => "cryptoverif", - ProverKind::Leo3 => "leo3", - ProverKind::Satallax => "satallax", - ProverKind::Lash => "lash", - ProverKind::AgsyHOL => "agsyhol", - // HP ecosystem — all route through the TypeLL kernel CLI; - // the discipline field on HPEcosystemBackend selects the - // actual upstream (typell / katagoria / tropical-resource-typing). - ProverKind::TypeLL => "typell", - ProverKind::KatagoriaVerifier => "katagoria", - ProverKind::TropicalTypeChecker => "tropical-type-check", - ProverKind::ChoreographicTypeChecker => "typell", - ProverKind::EpistemicTypeChecker => "typell", - ProverKind::EchoTypeChecker => "typell", - ProverKind::SessionTypeChecker => "typell", - ProverKind::ModalTypeChecker => "typell", - ProverKind::QTTTypeChecker => "typell", - ProverKind::EffectRowTypeChecker => "typell", - ProverKind::DependentTypeChecker => "typell", - ProverKind::RefinementTypeChecker => "typell", - ProverKind::OrdinaryTypeChecker - | ProverKind::PhantomTypeChecker - | ProverKind::PolymorphicTypeChecker - | ProverKind::ExistentialTypeChecker - | ProverKind::HigherKindedTypeChecker - | ProverKind::RowTypeChecker - | ProverKind::SubtypingTypeChecker - | ProverKind::IntersectionTypeChecker - | ProverKind::UnionTypeChecker - | ProverKind::GradualTypeChecker - | ProverKind::HoareTypeChecker - | ProverKind::IndexedTypeChecker - | ProverKind::LinearTypeChecker - | ProverKind::AffineTypeChecker - | ProverKind::RelevantTypeChecker - | ProverKind::OrderedTypeChecker - | ProverKind::UniquenessTypeChecker - | ProverKind::ImmutableTypeChecker - | ProverKind::CapabilityTypeChecker - | ProverKind::BunchedTypeChecker - | ProverKind::TemporalTypeChecker - | ProverKind::ProvabilityTypeChecker - | ProverKind::ImpureTypeChecker - | ProverKind::CoeffectTypeChecker - | ProverKind::ProbabilisticTypeChecker - | ProverKind::DyadicTypeChecker - | ProverKind::HomotopyTypeChecker - | ProverKind::CubicalTypeChecker - | ProverKind::NominalTypeChecker => "typell", - } - } -} +/// Enumeration of all supported provers; defined in `echidna-core` and +/// re-exported here so existing `crate::provers::ProverKind` paths keep working. +pub use echidna_core::prover_kind::ProverKind; /// Configuration for a prover backend #[derive(Debug, Clone, Serialize, Deserialize)] diff --git a/src/rust/provers/outcome.rs b/src/rust/provers/outcome.rs index 11c1bbde..8439e0bc 100644 --- a/src/rust/provers/outcome.rs +++ b/src/rust/provers/outcome.rs @@ -143,6 +143,27 @@ impl ProverOutcome { pub fn has_suspect_premises(&self) -> bool { matches!(self, ProverOutcome::InconsistentPremises { .. }) } + + /// Map this outcome onto the `echidna.prove.result/1` status. + /// + /// `Proved` is `verified`; `NoProofFound` is `failed`; `Timeout` is + /// `timeout`; input, prover and system failures are `error`. + /// `InconsistentPremises` is `unknown`: anything follows from + /// inconsistent premises, so the run is neither a usable proof nor a + /// refutation of the goal. + pub fn prove_status(&self) -> echidna_core::ProveStatus { + use echidna_core::ProveStatus; + match self { + ProverOutcome::Proved { .. } => ProveStatus::Verified, + ProverOutcome::NoProofFound { .. } => ProveStatus::Failed, + ProverOutcome::Timeout { .. } => ProveStatus::Timeout, + ProverOutcome::InconsistentPremises { .. } => ProveStatus::Unknown, + ProverOutcome::InvalidInput { .. } + | ProverOutcome::UnsupportedFeature { .. } + | ProverOutcome::ProverError { .. } + | ProverOutcome::SystemError { .. } => ProveStatus::Error, + } + } } impl fmt::Display for ProverOutcome { @@ -377,4 +398,56 @@ mod tests { assert_eq!(o, &d, "round-trip failed for {}", o); } } + + /// Every outcome variant maps to the documented prove-result status. + #[test] + fn prove_status_mapping_covers_every_variant() { + use echidna_core::ProveStatus as S; + let cases = [ + (ProverOutcome::Proved { elapsed_ms: 1 }, S::Verified), + ( + ProverOutcome::NoProofFound { + elapsed_ms: 1, + reason: None, + }, + S::Failed, + ), + (ProverOutcome::Timeout { limit_secs: 1 }, S::Timeout), + ( + ProverOutcome::InconsistentPremises { detail: None }, + S::Unknown, + ), + ( + ProverOutcome::InvalidInput { + reason: "x".into(), + location: None, + }, + S::Error, + ), + ( + ProverOutcome::UnsupportedFeature { + feature: "x".into(), + }, + S::Error, + ), + ( + ProverOutcome::ProverError { + detail: "x".into(), + exit_code: Some(2), + }, + S::Error, + ), + (ProverOutcome::SystemError { detail: "x".into() }, S::Error), + ]; + for (outcome, want) in &cases { + assert_eq!(outcome.prove_status(), *want, "{outcome}"); + } + // Every contract status is produced by at least one outcome. + for s in S::ALL { + assert!( + cases.iter().any(|(_, w)| *w == s), + "unreachable status {s:?}" + ); + } + } } diff --git a/tests/prove_output_json.rs b/tests/prove_output_json.rs new file mode 100644 index 00000000..5110bfea --- /dev/null +++ b/tests/prove_output_json.rs @@ -0,0 +1,151 @@ +// SPDX-License-Identifier: MPL-2.0 + +//! End-to-end tests of `echidna prove --output json` (the +//! `echidna.prove.result/1` contract) against the real binary. +//! +//! The TypedWasm backend is pure Rust, so `verified` and `failed` runs need +//! no external prover. `error` is produced by a missing file and by a file +//! with no detectable backend. `timeout` and `unknown` need a backend that +//! times out or reports inconsistent premises; they are covered by the +//! golden tests in `src/rust/prove_contract.rs` and `echidna-core`. + +use echidna_core::prove_result::{ProveResult, ProveStatus, SCHEMA}; +use std::path::Path; +use std::process::{Command, Output}; + +const OK_TWASM: &str = "region Particles { x: f32; y: f32; mass: f64 } [1024]\n\ +effect Particles { read; write }\n\ +region.get Particles[0] .x\n\ +linear.acquire Particles\n\ +linear.release Particles\n"; + +const BAD_TWASM: &str = "region Foo { bar: i32 } [10]\nregion.get Foo[0] .nonexistent\n"; + +/// Run the echidna binary with `args` in `dir`. +fn echidna(dir: &Path, args: &[&str]) -> Output { + Command::new(env!("CARGO_BIN_EXE_echidna")) + .current_dir(dir) + .args(args) + .output() + .expect("run echidna") +} + +/// Assert the contract's stdout shape and return the parsed result. +fn contract_result(out: &Output) -> ProveResult { + let stdout = String::from_utf8(out.stdout.clone()).expect("stdout is UTF-8"); + assert!( + stdout.ends_with('\n'), + "stdout must end with one newline: {stdout:?}" + ); + assert_eq!( + stdout.matches('\n').count(), + 1, + "exactly one line: {stdout:?}" + ); + // parse() also checks the line is byte-identical to its JCS form. + let r = ProveResult::parse(&stdout).unwrap_or_else(|e| panic!("{e}: {stdout:?}")); + assert_eq!(r.schema, SCHEMA); + assert_eq!(r.echidna_version, env!("CARGO_PKG_VERSION")); + r +} + +/// A proof the TypedWasm checker accepts is `verified` and exits 0. +#[test] +fn verified_run_prints_one_canonical_object() { + let dir = tempfile::tempdir().unwrap(); + std::fs::write(dir.path().join("ok.twasm"), OK_TWASM).unwrap(); + let out = echidna( + dir.path(), + &[ + "prove", + "ok.twasm", + "--prover", + "typed-wasm", + "--output", + "json", + ], + ); + let r = contract_result(&out); + assert_eq!(r.status, ProveStatus::Verified); + assert_eq!(r.prover, "TypedWasm"); + assert_eq!(r.goal, "ok.twasm"); + assert_eq!(r.trust.confidence, None); + assert_eq!(out.status.code(), Some(0)); +} + +/// A proof the checker rejects is `failed` and exits 1. +#[test] +fn failed_run_is_reported_as_failed() { + let dir = tempfile::tempdir().unwrap(); + std::fs::write(dir.path().join("bad.twasm"), BAD_TWASM).unwrap(); + let out = echidna( + dir.path(), + &[ + "prove", + "bad.twasm", + "--prover", + "typed-wasm", + "--output", + "json", + ], + ); + assert_eq!(contract_result(&out).status, ProveStatus::Failed); + assert_eq!(out.status.code(), Some(1)); +} + +/// A missing file is an `error` object, not a non-JSON message. +#[test] +fn missing_file_is_an_error_object() { + let dir = tempfile::tempdir().unwrap(); + let out = echidna( + dir.path(), + &[ + "prove", + "nope.twasm", + "--prover", + "typed-wasm", + "--output", + "json", + ], + ); + let r = contract_result(&out); + assert_eq!(r.status, ProveStatus::Error); + assert!(!r.message.is_empty()); + assert_eq!(out.status.code(), Some(1)); +} + +/// No detectable backend is an `error` object with an empty `prover`. +#[test] +fn undetectable_backend_is_an_error_object() { + let dir = tempfile::tempdir().unwrap(); + std::fs::write(dir.path().join("x.unknownext"), "x").unwrap(); + let out = echidna(dir.path(), &["prove", "x.unknownext", "--output", "json"]); + let r = contract_result(&out); + assert_eq!(r.status, ProveStatus::Error); + assert_eq!(r.prover, ""); + assert_eq!(out.status.code(), Some(1)); +} + +/// Without `--output json` the human report is unchanged. +#[test] +fn human_output_stays_the_default() { + let dir = tempfile::tempdir().unwrap(); + std::fs::write(dir.path().join("ok.twasm"), OK_TWASM).unwrap(); + let out = echidna( + dir.path(), + &["prove", "ok.twasm", "--prover", "typed-wasm", "--no-color"], + ); + let stdout = String::from_utf8_lossy(&out.stdout); + assert!(stdout.contains("Proof verified successfully"), "{stdout}"); + assert!(ProveResult::parse(&stdout).is_err()); + assert_eq!(out.status.code(), Some(0)); +} + +/// `prove --help` advertises `--output`, which is how consumers detect it. +#[test] +fn help_advertises_the_output_flag() { + let dir = tempfile::tempdir().unwrap(); + let out = echidna(dir.path(), &["prove", "--help"]); + let help = String::from_utf8_lossy(&out.stdout); + assert!(help.split_whitespace().any(|t| t == "--output"), "{help}"); +} From 2d76e1ee20b39c619d86d5e2d5aa5965e862115b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 5 Oct 2026 19:36:33 +0100 Subject: [PATCH 2/2] fix(ffi/zig): make Handle an extern struct, drop pointer casts Hypatia flagged the @ptrCast/@alignCast used to recover internal state from an opaque handle (CWE-704). An extern struct with C-compatible fields needs no casts; C still treats the pointer as opaque. Co-Authored-By: Claude Opus 5.5 --- ffi/zig/src/main.zig | 40 +++++++++++++++++----------------------- 1 file changed, 17 insertions(+), 23 deletions(-) diff --git a/ffi/zig/src/main.zig b/ffi/zig/src/main.zig index 9448074e..7df0597c 100644 --- a/ffi/zig/src/main.zig +++ b/ffi/zig/src/main.zig @@ -42,19 +42,13 @@ pub const Result = enum(c_int) { null_pointer = 4, }; -/// Library handle as C sees it: an opaque pointer. -pub const Handle = opaque {}; - -/// Internal state behind a `Handle`; never visible across the C ABI. -const State = struct { +/// Library handle. C code treats it as an opaque pointer; it is an +/// `extern struct` (C layout, C-compatible fields only) so the library can +/// allocate and use it directly, with no pointer or alignment casts. +pub const Handle = extern struct { initialized: bool, }; -/// Recover the internal state from a C handle. -fn state(handle: *Handle) *State { - return @ptrCast(@alignCast(handle)); -} - //============================================================================== // Library Lifecycle //============================================================================== @@ -62,20 +56,20 @@ fn state(handle: *Handle) *State { /// Initialize the library /// Returns a handle, or null on failure export fn echidna_init() ?*Handle { - const st = allocator.create(State) catch { + const handle = allocator.create(Handle) catch { setError("Failed to allocate handle"); return null; }; - st.* = .{ .initialized = true }; + handle.* = .{ .initialized = true }; clearError(); - return @ptrCast(st); + return handle; } /// Free the library handle export fn echidna_free(handle: ?*Handle) void { - const h = state(handle orelse return); + const h = handle orelse return; // Clean up resources h.initialized = false; @@ -90,10 +84,10 @@ export fn echidna_free(handle: ?*Handle) void { /// Process data (example operation) export fn echidna_process(handle: ?*Handle, input: u32) Result { - const h = state(handle orelse { + const h = handle orelse { setError("Null handle"); return .null_pointer; - }); + }; if (!h.initialized) { setError("Handle not initialized"); @@ -114,10 +108,10 @@ export fn echidna_process(handle: ?*Handle, input: u32) Result { /// Get a string result (example) /// Caller must free the returned string export fn echidna_get_string(handle: ?*Handle) ?[*:0]const u8 { - const h = state(handle orelse { + const h = handle orelse { setError("Null handle"); return null; - }); + }; if (!h.initialized) { setError("Handle not initialized"); @@ -152,10 +146,10 @@ export fn echidna_process_array( buffer: ?[*]const u8, len: u32, ) Result { - const h = state(handle orelse { + const h = handle orelse { setError("Null handle"); return .null_pointer; - }); + }; const buf = buffer orelse { setError("Null buffer"); @@ -216,10 +210,10 @@ export fn echidna_register_callback( handle: ?*Handle, callback: ?Callback, ) Result { - const h = state(handle orelse { + const h = handle orelse { setError("Null handle"); return .null_pointer; - }); + }; const cb = callback orelse { setError("Null callback"); @@ -244,7 +238,7 @@ export fn echidna_register_callback( /// Check if handle is initialized export fn echidna_is_initialized(handle: ?*Handle) u32 { - const h = state(handle orelse return 0); + const h = handle orelse return 0; return if (h.initialized) 1 else 0; }