diff --git a/.machine_readable/6a2/ANCHOR.a2ml b/.machine_readable/6a2/ANCHOR.a2ml index d32f616f..dec155a1 100644 --- a/.machine_readable/6a2/ANCHOR.a2ml +++ b/.machine_readable/6a2/ANCHOR.a2ml @@ -1,3 +1,4 @@ +# SPDX-License-Identifier: MPL-2.0 # ⚓ ANCHOR: rsr-template-repo # Canonical authority and project recalibration trigger for rsr-template-repo. # Template from: https://github.com/hyperpolymath/standards diff --git a/.machine_readable/contractiles/bust/bust.k9.ncl b/.machine_readable/contractiles/bust/bust.k9.ncl index bc1585ab..3bd9674b 100644 --- a/.machine_readable/contractiles/bust/bust.k9.ncl +++ b/.machine_readable/contractiles/bust/bust.k9.ncl @@ -51,6 +51,10 @@ let base = import "../_base.ncl" in allow_filesystem_write = true, # drills may write transient state (tmp dirs, test DBs) allow_subprocess = true, injection_scope = 'system_under_test_only, + # Hunt-tier files must declare whether a cryptographic signature + # is required. Bust trident runs in CI on every PR; signatures + # are enforced at the trident-runner layer, not in-band. + signature_required = true, }, }, diff --git a/Cargo.lock b/Cargo.lock index 2182c837..6cd1335e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -130,7 +130,7 @@ version = "1.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc" dependencies = [ - "windows-sys 0.61.2", + "windows-sys 0.60.2", ] [[package]] @@ -141,7 +141,7 @@ checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d" dependencies = [ "anstyle", "once_cell_polyfill", - "windows-sys 0.61.2", + "windows-sys 0.60.2", ] [[package]] @@ -684,7 +684,7 @@ version = "3.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "faf9468729b8cbcea668e36183cb69d317348c2e08e994829fb56ebfdfbaac34" dependencies = [ - "windows-sys 0.61.2", + "windows-sys 0.52.0", ] [[package]] @@ -1291,7 +1291,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" dependencies = [ "libc", - "windows-sys 0.61.2", + "windows-sys 0.52.0", ] [[package]] @@ -1613,11 +1613,11 @@ checksum = "fc0fef456e4baa96da950455cd02c081ca953b141298e41db3fc7e36b1da849c" [[package]] name = "home" -version = "0.5.12" +version = "0.5.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cc627f471c528ff0c4a49e1d5e60450c8f6461dd6d10ba9dcd3a61d3dff7728d" +checksum = "589533453244b0995c858700322199b2becb13b627df2851f64a2775d024abcf" dependencies = [ - "windows-sys 0.61.2", + "windows-sys 0.59.0", ] [[package]] @@ -1792,23 +1792,21 @@ dependencies = [ [[package]] name = "icu_collections" -version = "2.2.0" +version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2984d1cd16c883d7935b9e07e44071dca8d917fd52ecc02c04d5fa0b5a3f191c" +checksum = "db2fa452206ebee18c4b5c2274dbf1de17008e874b4dc4f0aea9d01ca79e4526" dependencies = [ "displaydoc", - "potential_utf", - "utf8_iter", "yoke", "zerofrom", "zerovec", ] [[package]] -name = "icu_locale_core" -version = "2.2.0" +name = "icu_locid" +version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "92219b62b3e2b4d88ac5119f8904c10f8f61bf7e95b640d25ba3075e6cac2c29" +checksum = "13acbb8371917fc971be86fc8057c41a64b521c184808a698c02acc242dbf637" dependencies = [ "displaydoc", "litemap", @@ -1817,61 +1815,99 @@ dependencies = [ "zerovec", ] +[[package]] +name = "icu_locid_transform" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "01d11ac35de8e40fdeda00d9e1e9d92525f3f9d887cdd7aa81d727596788b54e" +dependencies = [ + "displaydoc", + "icu_locid", + "icu_locid_transform_data", + "icu_provider", + "tinystr", + "zerovec", +] + +[[package]] +name = "icu_locid_transform_data" +version = "1.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7515e6d781098bf9f7205ab3fc7e9709d34554ae0b21ddbcb5febfa4bc7df11d" + [[package]] name = "icu_normalizer" -version = "2.2.0" +version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c56e5ee99d6e3d33bd91c5d85458b6005a22140021cc324cea84dd0e72cff3b4" +checksum = "19ce3e0da2ec68599d193c93d088142efd7f9c5d6fc9b803774855747dc6a84f" dependencies = [ + "displaydoc", "icu_collections", "icu_normalizer_data", "icu_properties", "icu_provider", "smallvec", + "utf16_iter", + "utf8_iter", + "write16", "zerovec", ] [[package]] name = "icu_normalizer_data" -version = "2.2.0" +version = "1.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da3be0ae77ea334f4da67c12f149704f19f81d1adf7c51cf482943e84a2bad38" +checksum = "c5e8338228bdc8ab83303f16b797e177953730f601a96c25d10cb3ab0daa0cb7" [[package]] name = "icu_properties" -version = "2.2.0" +version = "1.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bee3b67d0ea5c2cca5003417989af8996f8604e34fb9ddf96208a033901e70de" +checksum = "93d6020766cfc6302c15dbbc9c8778c37e62c14427cb7f6e601d849e092aeef5" dependencies = [ + "displaydoc", "icu_collections", - "icu_locale_core", + "icu_locid_transform", "icu_properties_data", "icu_provider", - "zerotrie", + "tinystr", "zerovec", ] [[package]] name = "icu_properties_data" -version = "2.2.0" +version = "1.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e2bbb201e0c04f7b4b3e14382af113e17ba4f63e2c9d2ee626b720cbce54a14" +checksum = "85fb8799753b75aee8d2a21d7c14d9f38921b54b3dbda10f5a3c7a7b82dba5e2" [[package]] name = "icu_provider" -version = "2.2.0" +version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "139c4cf31c8b5f33d7e199446eff9c1e02decfc2f0eec2c8d71f65befa45b421" +checksum = "6ed421c8a8ef78d3e2dbc98a973be2f3770cb42b606e3ab18d6237c4dfde68d9" dependencies = [ "displaydoc", - "icu_locale_core", + "icu_locid", + "icu_provider_macros", + "stable_deref_trait", + "tinystr", "writeable", "yoke", "zerofrom", - "zerotrie", "zerovec", ] +[[package]] +name = "icu_provider_macros" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ec89e9337638ecdc08744df490b221a7399bf8d164eb52a665454e60e075ad6" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "id-arena" version = "2.3.0" @@ -1897,9 +1933,9 @@ dependencies = [ [[package]] name = "idna_adapter" -version = "1.2.1" +version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3acae9609540aa318d1bc588455225fb2085b9ed0c4f6bd0d9d5bcd86f1a0344" +checksum = "daca1df1c957320b2cf139ac61e7bd64fed304c5040df000a745aa1de3b4ef71" dependencies = [ "icu_normalizer", "icu_properties", @@ -1954,7 +1990,7 @@ checksum = "3640c1c38b8e4e43584d8df18be5fc6b0aa314ce6ebf51b53313d4306cca8e46" dependencies = [ "hermit-abi", "libc", - "windows-sys 0.61.2", + "windows-sys 0.52.0", ] [[package]] @@ -2025,9 +2061,9 @@ checksum = "32a66949e030da00e8c7d4434b251670a91556f4144941d37452769c25d58a53" [[package]] name = "litemap" -version = "0.8.2" +version = "0.7.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "92daf443525c4cce67b150400bc2316076100ce0b3686209eb8cf3c31612e6f0" +checksum = "23fb14cb19457329c82206317a5663005a4d404783dc74f4252769b0d5f42856" [[package]] name = "lock_api" @@ -2234,7 +2270,7 @@ version = "0.50.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7957b9740744892f114936ab4a57b3f487491bbeafaf8083688b16841a4240e5" dependencies = [ - "windows-sys 0.61.2", + "windows-sys 0.59.0", ] [[package]] @@ -2552,15 +2588,6 @@ version = "1.13.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c33a9471896f1c69cecef8d20cbe2f7accd12527ce60845ff44c153bb2a21b49" -[[package]] -name = "potential_utf" -version = "0.1.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0103b1cef7ec0cf76490e969665504990193874ea05c85ff9bab8b911d0a0564" -dependencies = [ - "zerovec", -] - [[package]] name = "ppv-lite86" version = "0.2.21" @@ -3098,7 +3125,7 @@ dependencies = [ "errno", "libc", "linux-raw-sys", - "windows-sys 0.61.2", + "windows-sys 0.52.0", ] [[package]] @@ -3462,7 +3489,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3a766e1110788c36f4fa1c2b71b387a7815aa65f88ce0229841826633d93723e" dependencies = [ "libc", - "windows-sys 0.61.2", + "windows-sys 0.60.2", ] [[package]] @@ -3594,7 +3621,7 @@ dependencies = [ "getrandom 0.4.2", "once_cell", "rustix", - "windows-sys 0.61.2", + "windows-sys 0.52.0", ] [[package]] @@ -3637,9 +3664,9 @@ dependencies = [ [[package]] name = "tinystr" -version = "0.8.3" +version = "0.7.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c8323304221c2a851516f22236c5722a72eaa19749016521d6dff0824447d96d" +checksum = "9117f5d4db391c1cf6927e7bea3db74b9a1c1add8f7eda9ffd5364f40f57b82f" dependencies = [ "displaydoc", "zerovec", @@ -4109,6 +4136,12 @@ dependencies = [ "serde", ] +[[package]] +name = "utf16_iter" +version = "1.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c8232dd3cdaed5356e0f716d285e4b40b932ac434100fe9b7e0e8e935b9e6246" + [[package]] name = "utf8_iter" version = "1.0.4" @@ -4388,7 +4421,7 @@ version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" dependencies = [ - "windows-sys 0.61.2", + "windows-sys 0.52.0", ] [[package]] @@ -4729,11 +4762,17 @@ dependencies = [ "wasmparser", ] +[[package]] +name = "write16" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d1890f4022759daae28ed4fe62859b1236caebfc61ede2f63ed4e695f3f6d936" + [[package]] name = "writeable" -version = "0.6.3" +version = "0.5.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ffae5123b2d3fc086436f8834ae3ab053a283cfac8fe0a0b8eaae044768a4c4" +checksum = "1e9df38ee2d2c3c5948ea468a8406ff0db0b29ae1ffde1bcf20ef305bcc95c51" [[package]] name = "yansi" @@ -4743,10 +4782,11 @@ checksum = "cfe53a6657fd280eaa890a3bc59152892ffa3e30101319d168b781ed6529b049" [[package]] name = "yoke" -version = "0.8.2" +version = "0.7.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "abe8c5fda708d9ca3df187cae8bfb9ceda00dd96231bed36e445a1a48e66f9ca" +checksum = "120e6aef9aa629e3d4f52dc8cc43a015c7724194c97dfaf45180d2daf2b77f40" dependencies = [ + "serde", "stable_deref_trait", "yoke-derive", "zerofrom", @@ -4754,9 +4794,9 @@ dependencies = [ [[package]] name = "yoke-derive" -version = "0.8.2" +version = "0.7.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "de844c262c8848816172cef550288e7dc6c7b7814b4ee56b3e1553f275f1858e" +checksum = "2380878cad4ac9aac1e2435f3eb4020e8374b5f13c296cb75b4620ff8e229154" dependencies = [ "proc-macro2", "quote", @@ -4811,22 +4851,11 @@ version = "1.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b97154e67e32c85465826e8bcc1c59429aaaf107c1e4a9e53c8d8ccd5eff88d0" -[[package]] -name = "zerotrie" -version = "0.2.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0f9152d31db0792fa83f70fb2f83148effb5c1f5b8c7686c3459e361d9bc20bf" -dependencies = [ - "displaydoc", - "yoke", - "zerofrom", -] - [[package]] name = "zerovec" -version = "0.11.6" +version = "0.10.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "90f911cbc359ab6af17377d242225f4d75119aec87ea711a880987b18cd7b239" +checksum = "aa2b893d79df23bfb12d5461018d408ea19dfafe76c2c7ef6d4eba614f8ff079" dependencies = [ "yoke", "zerofrom", @@ -4835,9 +4864,9 @@ dependencies = [ [[package]] name = "zerovec-derive" -version = "0.11.3" +version = "0.10.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "625dc425cab0dca6dc3c3319506e6593dcb08a9f387ea3b284dbd52a92c40555" +checksum = "6eafa6dfb17584ea3e2bd6e76e0cc15ad7af12b09abdd1ca55961bed9b1063c6" dependencies = [ "proc-macro2", "quote", diff --git a/README.adoc b/README.adoc index 97121ffd..fc392b43 100644 --- a/README.adoc +++ b/README.adoc @@ -5,34 +5,44 @@ image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/echidna"] image:https://img.shields.io/badge/License-PMPL--1.0-blue.svg[License: PMPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] -image:https://img.shields.io/badge/Provers-128-green.svg[Provers: 128] -image:https://img.shields.io/badge/Tests-917%2B-brightgreen.svg[Tests: 917+] +image:https://img.shields.io/badge/Provers-12_core_/_79_advertised-green.svg[Provers: 12 core / 79 advertised] +image:https://img.shields.io/badge/Tests-1059-brightgreen.svg[Tests: 1059] image:https://api.thegreenwebfoundation.org/greencheckimage/nesy-prover.dev[Green Hosting,link="https://www.thegreenwebfoundation.org/green-web-check/?url=nesy-prover.dev"] *E*xtensible *C*ognitive *H*ybrid *I*ntelligence for *D*eductive *N*eural *A*ssistance -A neurosymbolic theorem proving platform with 128 prover backends, -trust-hardened verification pipeline, and multi-objective proof search. - -== Leadership Position - -ECHIDNA holds a **unique leadership position** in the theorem proving ecosystem as: - -* **The only system with 128+ prover backends** (vs 1 for Isabelle, Coq, Lean, Z3, etc.) -* **The only system actively solving cross-prover arbitration** (mathematical object identity resolution) -* **The only neurosymbolic hybrid architecture** (combining AI and symbolic reasoning) -* **The only system with 7-stage trust pipeline** (comprehensive verification infrastructure) -* **The only system integrating OpenTheory + Dedukti** (universal proof exchange) -* **The largest vocabulary management** (992K+ terms across mathematical domains) -* **The most comprehensive axiom tracking** (4 danger levels across 128 provers) -* **The only Bayesian confidence scoring** (across multiple independent provers) - -Our **prevailing advantage** comes from this unique combination that no other system can match. +A neurosymbolic theorem proving platform with a trust-hardened +verification pipeline, multi-objective proof search, and 100+ prover +backend implementations. + +== Prover Surface + +ECHIDNA's `ProverKind` enum has 141 variants and the repository ships +102 backend implementation files. The advertised roster +(`ProverKind::all()`) is 79 backends. The REST API +(`GET /api/provers`) exposes the 12-prover **core** set +(`ProverKind::all_core()`) by default. See +link:docs/SUPPORTED_PROVERS.md[`docs/SUPPORTED_PROVERS.md`] for the +core list, required external binaries, and how to surface additional +backends through the API. + +== Distinguishing Features + +* **Trust-hardened pipeline** — every proof passes through solver + integrity verification, axiom tracking, certificate checking, and + Bayesian confidence scoring before the result is returned. +* **Cross-prover arbitration** — mathematical object identity resolution + across heterogeneous prover backends. +* **Neurosymbolic architecture** — Julia ML layer suggests tactics; + formal provers always have the final word. +* **OpenTheory + Dedukti integration** — universal proof exchange. +* **Axiom-usage tracking** — four danger levels (Safe, Noted, Warning, + Reject) applied uniformly across every backend. == Overview -ECHIDNA orchestrates 128 theorem provers, SMT solvers, first-order ATPs, and -constraint solvers through a unified Rust core. Every proof result passes +ECHIDNA orchestrates theorem provers, SMT solvers, first-order ATPs, +and constraint solvers through a unified Rust core. Every proof result passes through a trust-hardening pipeline that checks solver integrity, tracks axiom usage, verifies proof certificates, and assigns a 5-level confidence score. @@ -41,34 +51,34 @@ always have the final word. ECHIDNA never produces unsound proofs. == Features -=== 128 Prover Backends - -[cols="1,4", options="header"] -|=== -| Tier | Provers - -| *Tier 1: Interactive Proof Assistants* -| Agda, Coq/Rocq, Lean 4, Isabelle/HOL, Idris2, F* - -| *Tier 2: SMT Solvers* -| Z3, CVC5, Alt-Ergo - -| *Tier 3: Auto-Active Verifiers* -| Dafny, Why3 - -| *Tier 4: Specialised* -| Metamath, HOL Light, Mizar, HOL4, PVS, ACL2, TLAPS, Twelf, Nuprl, Minlog, Imandra - -| *Tier 5: First-Order ATPs* -| Vampire, E Prover, SPASS - -| *Tier 6: Constraint / Optimisation Solvers* -| GLPK, SCIP, MiniZinc, Chuffed, OR-Tools -|=== - -All 128 backends implement the `ProverBackend` trait: parse, verify, export, -tactic suggestion, and theorem search. File extension detection covers 30+ -formats (`.v`, `.lean`, `.smt2`, `.tptp`, `.dfy`, `.mzn`, etc.). +=== Prover Backends + +The 12-prover **core** set exposed via `GET /api/provers`: + +* *Interactive proof assistants*: Agda, Coq, Lean 4, Isabelle/HOL, + HOL Light, HOL4, Mizar, PVS, ACL2 +* *SMT solvers*: Z3, CVC5 +* *Pure-Rust in-process*: Metamath (no external binary needed) + +`ProverKind::all()` advertises a further 67 backends including +interactive provers (Idris2, Lean3, F\*, Rocq), first-order ATPs +(Vampire, E Prover, SPASS, iProver, Prover9, Zipperposition), +SAT/SMT (CaDiCaL, Kissat, MiniSat, OpenSMT, SmtRat, AltErgo, dReal, +Princess), auto-active verifiers (Dafny, Why3, F\*, Cameleer, Liquid +Haskell, GNATprove, Stainless), constraint/optimisation (GLPK, SCIP, +MiniZinc, Chuffed, OR-Tools), model checkers (SPIN, NuSMV, TLC, Alloy, +Prism, UPPAAL, Storm, ProB), C/hardware verifiers (CBMC, SeaHorn, +Frama-C, ABC, Viper, KeY, GPUVerify, Faial), security protocol tools +(Tamarin, ProVerif, EasyCrypt, CryptoVerif), and specialised systems +(TLAPS, Twelf, Nuprl, Minlog, Imandra, KeYmaeraX, MetiTarski, Cubical +Agda, MizAR, Dedukti, Boogie, Athena, Naproche, Matita, Arend, Mercury, +λProlog, Nitpick, Nunchaku, Leo III, Satallax, Lash, agsyHOL, mleanCoP, +ileanCoP, NanoCoP, MetTeL2, ELK, Konclude, TypedWasm, UPPAAL Stratego). + +All advertised backends implement the `ProverBackend` trait: parse, +verify, export, tactic suggestion, and theorem search. File extension +detection covers 30+ formats (`.v`, `.lean`, `.smt2`, `.tptp`, `.dfy`, +`.mzn`, etc.). === Trust & Safety Hardening (v1.5) @@ -175,7 +185,7 @@ cd echidna just build # or: cargo build -# Run all tests (917+ passing) +# Run all tests (1059 passing on default build) just test # or: cargo test @@ -183,6 +193,33 @@ just test just run ---- +=== Prove your first goal + +[source,bash] +---- +# Install at least one solver — Z3 is the smallest dependency +sudo apt install z3 # Debian/Ubuntu (or `brew install z3`) + +# Start the REST API server with CORS enabled +cargo run --bin echidna -- server --cors + +# In another terminal, POST a satisfiable SMT-LIB goal +curl -X POST http://127.0.0.1:8081/api/prove \ + -H 'Content-Type: application/json' \ + -d '{"prover":"Z3", + "content":"(set-logic QF_LIA)\n(declare-const x Int)\n(assert (> x 0))\n(check-sat)\n", + "timeout":30}' +# → {"success":true,"goals":1,"message":"Proof verified successfully"} +---- + +For a minimal browser UI, open `src/ui/public/prove.html` directly in +any modern browser and point the "API base" field at the running +server. No build step is required. + +See link:docs/SUPPORTED_PROVERS.md[`docs/SUPPORTED_PROVERS.md`] for the +12-prover core set, required binaries, and how to expose additional +backends through the API. + === Using Podman Container [source,bash] @@ -205,7 +242,7 @@ podman run -it echidna:latest [source] ---- src/rust/ - provers/ # 128 prover backend implementations (ProverBackend trait) + provers/ # 102 prover backend implementation files (ProverBackend trait) verification/ # Trust-hardening subsystem portfolio.rs # SMT portfolio solving / cross-checking certificates.rs # Proof certificate checking (Alethe, DRAT/LRAT, TSTP) @@ -268,11 +305,11 @@ println!("Verified: {}, Trust: {}", result.verified, result.trust_level); == Test Suite -917+ library tests passing (`cargo test --lib --features verisim`, 2 ignored). +1059 library tests passing on the default build +(`cargo test --lib`, 2 ignored). The `--features verisim` build adds +further integration tests for the VeriSim bridge. -* 884 tests default build (`cargo test --lib`) -* 917 tests with VeriSim integration (`--features verisim`) -* Smoke E2E integration tests across all prover backends +* Smoke E2E integration tests across the core prover backends * Property-based tests (PropTest) * Criterion benchmarks across all critical paths diff --git a/audits/assail-classifications.a2ml b/audits/assail-classifications.a2ml index 05d5d396..22ae0baa 100644 --- a/audits/assail-classifications.a2ml +++ b/audits/assail-classifications.a2ml @@ -1,12 +1,17 @@ -# identity: echidna-assail-classifications -; SPDX-License-Identifier: MPL-2.0 -; Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -; -; Classification registry for panic-attack assail findings that are confirmed -; legitimate patterns and should not be treated as actionable weak-points. -; -; Format mirrors the panic-attack user-classification registry protocol. -; Cross-reference: audits/audit-ffi-boundary.md +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Classification registry for panic-attack assail findings that are confirmed +# legitimate patterns and should not be treated as actionable weak-points. +# +# Format mirrors the panic-attack user-classification registry protocol. +# Cross-reference: audits/audit-ffi-boundary.md + +[metadata] +name = "echidna-assail-classifications" +project = "echidna" +version = "1.0.0" +schema_version = "1.0.0" (assail-classifications diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl index f6b339ca..3165f868 100644 --- a/container/deploy.k9.ncl +++ b/container/deploy.k9.ncl @@ -3,6 +3,16 @@ K9! # deploy.k9.ncl — ECHIDNA deployment component (Hunt level) let component_pedigree = { + # Top-level identity fields — duplicated from metadata so the K9 + # validator (which inspects the literal `pedigree = { ... }` block + # at the toplevel of the file rather than the resolved Nickel value) + # can locate name / version / security_level without resolving the + # `component_pedigree` indirection. + name = "echidna-deploy", + version = "1.5.0", + schema_version = "1.0.0", + security_level = 'Hunt, + signature_required = true, metadata = { name = "echidna-deploy", version = "1.5.0", @@ -99,7 +109,23 @@ echo "K9: Rollback complete." } in { - pedigree = component_pedigree, + # The K9 validator does a literal text-scan over the toplevel + # `pedigree = { ... }` block and does not resolve Nickel let-bindings, + # so the identity fields (name / version / security_level) must appear + # inside the inline record here even though they are also present in + # the `component_pedigree` binding used by the runtime consumer. + pedigree = { + name = "echidna-deploy", + version = "1.5.0", + schema_version = "1.0.0", + security_level = 'Hunt, + signature_required = true, + metadata = component_pedigree.metadata, + target = component_pedigree.target, + security = component_pedigree.security, + validation = component_pedigree.validation, + recipes = component_pedigree.recipes, + }, deployment = deployment, scripts = scripts, required_level = 'Hunt, diff --git a/docs/SUPPORTED_PROVERS.md b/docs/SUPPORTED_PROVERS.md new file mode 100644 index 00000000..fe3b9de7 --- /dev/null +++ b/docs/SUPPORTED_PROVERS.md @@ -0,0 +1,94 @@ + + +# Supported Provers + +ECHIDNA implements 100+ prover backends, but the surface a new user +encounters is deliberately smaller. This document is the source of truth +for what works out of the box. + +## What the API actually exposes + +`GET /api/provers` returns 12 **core** provers (`ProverKind::all_core()` +in `src/rust/provers/mod.rs:689`). These are the only ones the bundled +UI (`src/ui/public/prove.html`) and the REST clients see by default: + +| Prover | Kind | Required binary | Install hint | +|------------|---------------------------------------|-----------------|-------------------------------------------------------------------------------------------------| +| Agda | Dependent ITP | `agda` | `cabal install Agda` or distro package | +| Coq | Calculus of Inductive Constructions | `coqc` | `opam install coq` (or Coq Platform installer) | +| Lean | Lean 4 | `lean`, `lake` | `elan` toolchain manager: | +| Isabelle | Higher-order logic | `isabelle` | | +| Z3 | SMT solver | `z3` | `apt install z3` / `brew install z3` / release tarball | +| CVC5 | SMT solver | `cvc5` | | +| Metamath | Pure-Rust in-process checker | *(none)* | Works without external binary — pure-Rust implementation in `src/rust/provers/metamath.rs` | +| HOL Light | Classical higher-order logic | `hol_light` | OCaml + HOL Light: | +| Mizar | Tarski–Grothendieck set theory | `mizf`, `verifier` | | +| PVS | Prototype Verification System | `pvs` | | +| ACL2 | Applicative Common Lisp | `acl2` | | +| HOL4 | HOL family theorem prover | `hol` | | + +ECHIDNA does **not** install or bundle these binaries. When a binary is +missing, the corresponding `POST /api/prove` call returns a structured +error (e.g. `"Failed to spawn Z3 process: \"z3\""`) — it does not crash +the server and the other 11 provers remain available. + +## Quickstart: prove your first goal + +```bash +# 1. Install Z3 (smallest dependency, ~5 MB) +sudo apt install z3 # Debian/Ubuntu +brew install z3 # macOS + +# 2. Build and run the server +cargo run --bin echidna -- server --cors + +# 3. In another terminal — health check +curl http://127.0.0.1:8081/api/health +# → {"status":"ok","version":"2.1.0"} + +# 4. Prove a satisfiable SMT-LIB goal +curl -X POST http://127.0.0.1:8081/api/prove \ + -H 'Content-Type: application/json' \ + -d '{ + "prover": "Z3", + "content": "(set-logic QF_LIA)\n(declare-const x Int)\n(assert (> x 0))\n(check-sat)\n", + "timeout": 30 + }' +# → {"success":true,"goals":1,"message":"Proof verified successfully"} +``` + +For a browser UI, open `src/ui/public/prove.html` directly in any +modern browser and point the "API base" field at the running server. +No build step is required. + +## Beyond the core 12 + +`ProverKind::all()` lists 67 additional backends (79 total — 12 core +plus 67 extended) with full +`ProverBackend` trait implementations (real subprocess invocation, not +stubs), spanning interactive provers (Idris2, Lean3, F\*), first-order +ATPs (Vampire, E, SPASS), constraint/SAT solvers (MiniSat, CaDiCaL, +Kissat, MiniZinc), model checkers (SPIN, NuSMV, TLC, UPPAAL), +auto-active verifiers (Dafny, Why3), security tools (Tamarin, ProVerif, +CryptoVerif, EasyCrypt), and more. + +These are reachable via the Rust API: + +```rust +use echidna::provers::{ProverFactory, ProverKind, ProverConfig}; +let backend = ProverFactory::create(ProverKind::Vampire, ProverConfig::default())?; +``` + +They are deliberately not in `all_core()` because each adds an external +binary dependency and most users do not need them. To expose extra +backends through the REST API, edit `src/rust/provers/mod.rs:689` and +add the relevant `ProverKind` variants to `all_core()`. + +The full `ProverKind` enum has 141 variants. The delta between 141 and +79 covers dialect variants (e.g. `Lean3` alongside `Lean`, `Rocq` +alongside `Coq`, `IsabelleZF` alongside `Isabelle`) and experimental +adapters not yet promoted to the canonical roster. They have +implementation files but are not exercised by the default test suite. diff --git a/src/rust/agent/swarm.rs b/src/rust/agent/swarm.rs index 35dac24b..a2fcb420 100644 --- a/src/rust/agent/swarm.rs +++ b/src/rust/agent/swarm.rs @@ -105,8 +105,8 @@ struct Adopt { fn lex_better(a: &[i64], b: &[i64]) -> bool { let n = a.len().max(b.len()); for i in 0..n { - let ai = a.get(i).copied().unwrap_or_else(|| 0); - let bi = b.get(i).copied().unwrap_or_else(|| 0); + let ai = a.get(i).copied().unwrap_or(0); + let bi = b.get(i).copied().unwrap_or(0); if ai < bi { return true; } @@ -123,8 +123,8 @@ fn lex_strictly_better_by(a: &[i64], b: &[i64], threshold: i64) -> bool { // qualifies; for threshold > 0, the gap must reach that size. let n = a.len().max(b.len()); for i in 0..n { - let ai = a.get(i).copied().unwrap_or_else(|| 0); - let bi = b.get(i).copied().unwrap_or_else(|| 0); + let ai = a.get(i).copied().unwrap_or(0); + let bi = b.get(i).copied().unwrap_or(0); if ai < bi { return (bi - ai) >= threshold; } @@ -142,8 +142,8 @@ fn delta_scalar(from: &[i64], to: &[i64]) -> f64 { let n = from.len().max(to.len()); let mut delta = 0.0; for i in 0..n { - let f = from.get(i).copied().unwrap_or_else(|| 0) as f64; - let t = to.get(i).copied().unwrap_or_else(|| 0) as f64; + let f = from.get(i).copied().unwrap_or(0) as f64; + let t = to.get(i).copied().unwrap_or(0) as f64; let w = (1000_f64).powi((n - i - 1) as i32); delta += w * (t - f); } @@ -247,7 +247,7 @@ where if neighbours.is_empty() { break; } - let pick = rng.gen_range(0..neighbours.len()); + let pick = rng.random_range(0..neighbours.len()); let cand = neighbours[pick].clone(); let cand_e = problem.energy(&cand); @@ -256,7 +256,7 @@ where } else { let de = delta_scalar(¤t_e, &cand_e); let p: f64 = (-de / temp).exp(); - rng.gen::() < p + rng.random::() < p }; if accept { diff --git a/src/rust/coprocessor/graphics.rs b/src/rust/coprocessor/graphics.rs index 4569c3c0..a745eb80 100644 --- a/src/rust/coprocessor/graphics.rs +++ b/src/rust/coprocessor/graphics.rs @@ -104,7 +104,7 @@ fn render_proof_graph(nodes: &[(String, String)], edges: &[(String, String)]) -> } // Compute approximate depth: longest incoming edge chain (BFS from sources). let depths = compute_depths(nodes, edges); - let row_count = (depths.iter().copied().max().unwrap_or_else(|| 0) + 1) as usize; + let row_count = (depths.iter().copied().max().unwrap_or(0) + 1) as usize; let cell_w = 160usize; let cell_h = 60usize; let width = cell_w * n.max(1); diff --git a/src/rust/coprocessor/math.rs b/src/rust/coprocessor/math.rs index 5c817f93..ab38f526 100644 --- a/src/rust/coprocessor/math.rs +++ b/src/rust/coprocessor/math.rs @@ -384,7 +384,9 @@ fn fib_fast_doubling(n: u64) -> BigUint { let (a, b) = helper(n / 2); let c = &a * (BigUint::from(2u32) * &b - &a); let d = &a * &a + &b * &b; - if n.is_multiple_of(2) { + // MSRV 1.85: cannot use `u64::is_multiple_of` (stabilised in 1.87). + #[allow(clippy::manual_is_multiple_of)] + if n % 2 == 0 { (c, d) } else { let e = &c + &d; diff --git a/src/rust/corpus/octad.rs b/src/rust/corpus/octad.rs index 6ad5e291..bb69d46b 100644 --- a/src/rust/corpus/octad.rs +++ b/src/rust/corpus/octad.rs @@ -355,6 +355,16 @@ fn axiom_usage_from_tensor(t: &DeclTensor) -> super::AxiomUsage { } } +pub(crate) fn to_hex(bytes: impl AsRef<[u8]>) -> String { + use std::fmt::Write; + let bytes = bytes.as_ref(); + let mut s = String::with_capacity(bytes.len() * 2); + for b in bytes { + write!(s, "{:02x}", b).expect("write to String never fails"); + } + s +} + fn octad_key(adapter: &str, qualified: &str, statement: &str) -> String { let mut h = Sha256::new(); h.update(adapter.as_bytes()); @@ -362,7 +372,7 @@ fn octad_key(adapter: &str, qualified: &str, statement: &str) -> String { h.update(qualified.as_bytes()); h.update(b"|"); h.update(statement.as_bytes()); - format!("{:x}", h.finalize()) + to_hex(h.finalize()) } fn cross_prover_key(qualified: &str) -> String { @@ -372,7 +382,7 @@ fn cross_prover_key(qualified: &str) -> String { let tail = qualified.rsplit('.').next().unwrap_or(qualified); let mut h = Sha256::new(); h.update(tail.as_bytes()); - format!("{:x}", h.finalize()) + to_hex(h.finalize()) } fn content_hash_of(entry: &CorpusEntry) -> String { @@ -384,7 +394,7 @@ fn content_hash_of(entry: &CorpusEntry) -> String { if let Some(p) = &entry.proof { h.update(p.as_bytes()); } - format!("{:x}", h.finalize()) + to_hex(h.finalize()) } fn hash_provenance(parent: &str, event: &str, timestamp: &str, file: &str, line: usize) -> String { @@ -398,7 +408,7 @@ fn hash_provenance(parent: &str, event: &str, timestamp: &str, file: &str, line: h.update(file.as_bytes()); h.update(b"|"); h.update(line.to_string().as_bytes()); - format!("{:x}", h.finalize()) + to_hex(h.finalize()) } // =========================================================================== diff --git a/src/rust/exchange/dedukti.rs b/src/rust/exchange/dedukti.rs index 186e2776..abd6ab0c 100644 --- a/src/rust/exchange/dedukti.rs +++ b/src/rust/exchange/dedukti.rs @@ -291,7 +291,7 @@ impl DeduktiExporter { .trim_start_matches("Type") .trim() .parse::() - .unwrap_or_else(|_| 0); + .unwrap_or(0); Term::Type(level) } else { // Simple identifier diff --git a/src/rust/gnn/client.rs b/src/rust/gnn/client.rs index 4bf0c08d..55a43643 100644 --- a/src/rust/gnn/client.rs +++ b/src/rust/gnn/client.rs @@ -345,7 +345,11 @@ impl GnnClient { let node_labels: Vec = graph.nodes.iter().map(|n| n.label.clone()).collect(); - let feature_dim = graph.nodes.first().map(|n| n.features.len()).unwrap_or_else(|| 0); + let feature_dim = graph + .nodes + .first() + .map(|n| n.features.len()) + .unwrap_or_else(|| 0); let goal_node_idx = graph .goal_node_id diff --git a/src/rust/gnn/embeddings.rs b/src/rust/gnn/embeddings.rs index 22e9c3a7..ddb29dfb 100644 --- a/src/rust/gnn/embeddings.rs +++ b/src/rust/gnn/embeddings.rs @@ -123,7 +123,7 @@ impl TermFeatureExtractor { } else { let total: usize = symbols .iter() - .map(|s| self.symbol_frequencies.get(s).copied().unwrap_or_else(|| 0)) + .map(|s| self.symbol_frequencies.get(s).copied().unwrap_or(0)) .sum(); (total as f32) / (symbols.len() as f32 * self.max_frequency as f32) }; @@ -364,13 +364,16 @@ fn term_depth(term: &Term) -> usize { | Term::Meta(_) => 0, Term::App { func, args } => { let func_depth = term_depth(func); - let max_arg = args.iter().map(term_depth).max().unwrap_or_else(|| 0); + let max_arg = args.iter().map(term_depth).max().unwrap_or(0); 1 + func_depth.max(max_arg) }, Term::Lambda { param_type, body, .. } => { - let pt = param_type.as_ref().map(|t| term_depth(t)).unwrap_or_else(|| 0); + let pt = param_type + .as_ref() + .map(|t| term_depth(t)) + .unwrap_or_else(|| 0); 1 + pt.max(term_depth(body)) }, Term::Pi { @@ -395,7 +398,7 @@ fn term_depth(term: &Term) -> usize { .iter() .map(|(_, t)| term_depth(t)) .max() - .unwrap_or_else(|| 0); + .unwrap_or(0); 1 + s.max(b) }, Term::Fix { ty, body, .. } => { diff --git a/src/rust/gnn/graph.rs b/src/rust/gnn/graph.rs index 51c67f7a..213376a9 100644 --- a/src/rust/gnn/graph.rs +++ b/src/rust/gnn/graph.rs @@ -227,7 +227,7 @@ impl ProofGraphBuilder { .map(|(idx, node)| (node.id, idx)) .collect(); - let max_depth = self.nodes.iter().map(|n| n.term_depth).max().unwrap_or_else(|| 0); + let max_depth = self.nodes.iter().map(|n| n.term_depth).max().unwrap_or(0); let num_subterms = self .nodes .iter() diff --git a/src/rust/learning/design_search.rs b/src/rust/learning/design_search.rs index 174ce74d..bd1b4cc3 100644 --- a/src/rust/learning/design_search.rs +++ b/src/rust/learning/design_search.rs @@ -103,8 +103,8 @@ pub struct AnnealResult { fn lex_cmp(a: &[i64], b: &[i64]) -> std::cmp::Ordering { let n = a.len().max(b.len()); for i in 0..n { - let ai = a.get(i).copied().unwrap_or_else(|| 0); - let bi = b.get(i).copied().unwrap_or_else(|| 0); + let ai = a.get(i).copied().unwrap_or(0); + let bi = b.get(i).copied().unwrap_or(0); match ai.cmp(&bi) { std::cmp::Ordering::Equal => continue, other => return other, @@ -120,8 +120,8 @@ fn delta_energy(from: &[i64], to: &[i64]) -> f64 { let n = from.len().max(to.len()); let mut delta: f64 = 0.0; for i in 0..n { - let f = from.get(i).copied().unwrap_or_else(|| 0) as f64; - let t = to.get(i).copied().unwrap_or_else(|| 0) as f64; + let f = from.get(i).copied().unwrap_or(0) as f64; + let t = to.get(i).copied().unwrap_or(0) as f64; // Weight: 1000^(n-i-1). The first coord dominates by a // factor of 1000 per position. let w = (1000_f64).powi((n - i - 1) as i32); @@ -156,7 +156,7 @@ pub fn anneal(problem: &P, config: &AnnealConfig) -> AnnealRes if neighbours.is_empty() { break; } - let pick = rng.gen_range(0..neighbours.len()); + let pick = rng.random_range(0..neighbours.len()); let cand = neighbours[pick].clone(); let cand_e = problem.energy(&cand); @@ -170,7 +170,7 @@ pub fn anneal(problem: &P, config: &AnnealConfig) -> AnnealRes std::cmp::Ordering::Greater => { let de = delta_energy(¤t_e, &cand_e); let p: f64 = (-de / temp).exp(); - rng.gen::() < p + rng.random::() < p }, }; diff --git a/src/rust/proof_encoding.rs b/src/rust/proof_encoding.rs index c1e713d9..87440458 100644 --- a/src/rust/proof_encoding.rs +++ b/src/rust/proof_encoding.rs @@ -52,7 +52,7 @@ pub fn proof_identity(theorem_name: &str, goal: &Goal, prover: ProverKind) -> St prover, ); let hash = Sha256::digest(input.as_bytes()); - format!("{:x}", hash) + crate::corpus::octad::to_hex(hash) } /// Generate a goal-only identity (prover-agnostic). @@ -62,7 +62,7 @@ pub fn proof_identity(theorem_name: &str, goal: &Goal, prover: ProverKind) -> St pub fn goal_identity(theorem_name: &str, goal: &Goal) -> String { let input = format!("echidna:v1:goal:{}:{}", theorem_name, goal.target,); let hash = Sha256::digest(input.as_bytes()); - format!("{:x}", hash) + crate::corpus::octad::to_hex(hash) } /// Generate a session identity for ephemeral proof attempts. @@ -72,7 +72,7 @@ pub fn goal_identity(theorem_name: &str, goal: &Goal) -> String { pub fn session_identity(goal_id: &str, timestamp: i64) -> String { let input = format!("echidna:v1:session:{}:{}", goal_id, timestamp,); let hash = Sha256::digest(input.as_bytes()); - format!("{:x}", hash) + crate::corpus::octad::to_hex(hash) } /// Estimate the CBOR-encoded size of a ProofState without allocating. diff --git a/src/rust/provers/agda.rs b/src/rust/provers/agda.rs index 8d9f3563..550dafd7 100644 --- a/src/rust/provers/agda.rs +++ b/src/rust/provers/agda.rs @@ -90,7 +90,7 @@ impl AgdaBackend { body: Box::new(self.agda_to_term(body)), }, AgdaTerm::Set(level) => Term::Universe(*level), - AgdaTerm::Hole(name) => Term::Meta(name.parse().unwrap_or_else(|_| 0)), + AgdaTerm::Hole(name) => Term::Meta(name.parse().unwrap_or(0)), } } diff --git a/src/rust/provers/dafny.rs b/src/rust/provers/dafny.rs index 72665163..53f4405e 100644 --- a/src/rust/provers/dafny.rs +++ b/src/rust/provers/dafny.rs @@ -20,8 +20,7 @@ impl DafnyBackend { /// Generate a minimal valid Dafny program with assertions for the goal and axioms. fn to_input_format(&self, state: &ProofState) -> Result { - let mut s = - String::from("// SPDX-License-Identifier: MPL-2.0\nmethod EchidnaGoal() {\n"); + let mut s = String::from("// SPDX-License-Identifier: MPL-2.0\nmethod EchidnaGoal() {\n"); // Add axioms as assume statements for (i, ax) in state.context.axioms.iter().enumerate() { diff --git a/src/rust/server.rs b/src/rust/server.rs index a607ffbc..b685aa67 100644 --- a/src/rust/server.rs +++ b/src/rust/server.rs @@ -338,6 +338,8 @@ async fn agent_plan_handler( /// - octad-storage (VeriSimDB): Persist proof artifacts as octad entities /// - scanning (Hypatia): Trigger re-verification after codebase changes async fn groove_manifest() -> Json { + let core_count = echidna::ProverKind::all_core().len(); + let advertised_count = echidna::ProverKind::all().len(); Json(json!({ "groove_version": "1", "service_id": "echidna", @@ -345,17 +347,22 @@ async fn groove_manifest() -> Json { "capabilities": { "theorem_proving": { "type": "theorem-proving", - "description": "Neurosymbolic theorem proving with 48 prover backends", + "description": format!( + "Neurosymbolic theorem proving — {} core / {} advertised prover backends", + core_count, advertised_count + ), "protocol": "http", - "endpoint": "/api/v1/prove", + "endpoint": "/api/prove", "requires_auth": false, "panel_compatible": true } }, "consumes": ["octad-storage", "scanning"], "endpoints": { - "api": "http://localhost:9000/api", - "health": "http://localhost:9000/api/health" + "provers": "/api/provers", + "prove": "/api/prove", + "verify": "/api/verify", + "health": "/api/health" }, "health": "/api/health", "applicability": ["individual", "team"] @@ -947,7 +954,11 @@ async fn get_session_state( let session = session.lock().await; Ok(Json(SessionStateResponse { - goals: session.state.as_ref().map(|s| s.goals.len()).unwrap_or_else(|| 0), + goals: session + .state + .as_ref() + .map(|s| s.goals.len()) + .unwrap_or_else(|| 0), complete: session .state .as_ref() diff --git a/src/rust/suggest/extractor.rs b/src/rust/suggest/extractor.rs index ad229772..4f80748e 100644 --- a/src/rust/suggest/extractor.rs +++ b/src/rust/suggest/extractor.rs @@ -144,7 +144,7 @@ fn find_tactic_sites_isabelle(source: &str) -> Vec { .unwrap_or("") .trim_matches(|c: char| !c.is_alphanumeric() && c != '_'); if !name.is_empty() { - let col = line.find(name).unwrap_or_else(|| 0) + 1; + let col = line.find(name).unwrap_or(0) + 1; sites.push(TacticSite { line: line_no, col, @@ -164,7 +164,7 @@ fn find_tactic_sites_isabelle(source: &str) -> Vec { .unwrap_or("") .trim_matches(|c: char| !c.is_alphanumeric() && c != '_'); if !name.is_empty() { - let col = line.find(name).unwrap_or_else(|| 0) + 1; + let col = line.find(name).unwrap_or(0) + 1; sites.push(TacticSite { line: line_no, col, @@ -180,7 +180,7 @@ fn find_tactic_sites_isabelle(source: &str) -> Vec { .unwrap_or("") .trim_matches(|c: char| !c.is_alphanumeric() && c != '_'); if !name.is_empty() { - let col = line.find(name).unwrap_or_else(|| 0) + 1; + let col = line.find(name).unwrap_or(0) + 1; sites.push(TacticSite { line: line_no, col, @@ -252,7 +252,7 @@ fn find_tactic_sites_coq(source: &str) -> Vec { ] .contains(&name) { - let col = line.find(name).unwrap_or_else(|| 0) + 1; + let col = line.find(name).unwrap_or(0) + 1; sites.push(TacticSite { line: line_no, col, @@ -335,7 +335,7 @@ fn find_tactic_sites_lean4(source: &str) -> Vec { .next() .unwrap_or(""); if !name.is_empty() { - let col = line.find(name).unwrap_or_else(|| 0) + 1; + let col = line.find(name).unwrap_or(0) + 1; sites.push(TacticSite { line: line_no, col, @@ -353,7 +353,7 @@ fn find_tactic_sites_lean4(source: &str) -> Vec { if !name.is_empty() && !["where", "fun", "have", "show", "exact", "rfl", "done"].contains(&name) { - let col = line.find(name).unwrap_or_else(|| 0) + 1; + let col = line.find(name).unwrap_or(0) + 1; sites.push(TacticSite { line: line_no, col, @@ -423,7 +423,7 @@ fn find_tactic_sites_idris2(source: &str) -> Vec { || name.starts_with("exact") || name.starts_with("Refl") { - let col = line.find(name).unwrap_or_else(|| 0) + 1; + let col = line.find(name).unwrap_or(0) + 1; sites.push(TacticSite { line: line_no, col, @@ -482,7 +482,7 @@ fn find_tactic_sites_agda(source: &str) -> Vec { for word in line.split_whitespace() { let name = word.trim_matches(|c: char| !c.is_alphanumeric() && c != '_' && c != '\''); if ["refl", "sym", "trans", "cong", "subst"].contains(&name) { - let col = line.find(name).unwrap_or_else(|| 0) + 1; + let col = line.find(name).unwrap_or(0) + 1; sites.push(TacticSite { line: line_no, col, diff --git a/src/rust/vcl_ut.rs b/src/rust/vcl_ut.rs index 60458c13..30d15eff 100644 --- a/src/rust/vcl_ut.rs +++ b/src/rust/vcl_ut.rs @@ -398,7 +398,7 @@ impl QueryExecutor { .get("safety_report") .and_then(|sr| sr.get("max_level")) .and_then(|ml| ml.as_u64()) - .unwrap_or_else(|| 0); + .unwrap_or(0); let valid = body.get("valid").and_then(|v| v.as_bool()).unwrap_or(true); @@ -803,7 +803,7 @@ fn search_result_to_entry(value: &serde_json::Value) -> Option .and_then(|v| v.as_str()) .unwrap_or("unknown") .to_string(), - time_ms: value.get("time_ms").and_then(|v| v.as_u64()).unwrap_or_else(|| 0), + time_ms: value.get("time_ms").and_then(|v| v.as_u64()).unwrap_or(0), aspects: value .get("aspects") .or_else(|| value.get("document").and_then(|d| d.get("aspects"))) diff --git a/src/rust/verification/proof.rs b/src/rust/verification/proof.rs index 38ef4d25..bc901918 100644 --- a/src/rust/verification/proof.rs +++ b/src/rust/verification/proof.rs @@ -52,7 +52,7 @@ use crate::provers::ProverKind; /// entity from the E-R perspective. pub fn theorem_identity(theorem_name: &str) -> String { let input = format!("echidna:v1:theorem:{}", theorem_name); - format!("{:x}", Sha256::digest(input.as_bytes())) + crate::corpus::octad::to_hex(Sha256::digest(input.as_bytes())) } // ═══════════════════════════════════════════════════════════════════════ diff --git a/src/rust/verisim_bridge.rs b/src/rust/verisim_bridge.rs index e90f1d36..22330dff 100644 --- a/src/rust/verisim_bridge.rs +++ b/src/rust/verisim_bridge.rs @@ -976,7 +976,7 @@ fn hash_provenance_record( timestamp, serde_json::to_string(data).unwrap_or_default(), ); - format!("{:x}", Sha256::digest(input.as_bytes())) + crate::corpus::octad::to_hex(Sha256::digest(input.as_bytes())) } /// Base64-encode bytes (no padding, URL-safe). @@ -989,8 +989,8 @@ fn base64_encode(bytes: &[u8]) -> String { for chunk in bytes.chunks(3) { let b0 = chunk[0] as u32; - let b1 = chunk.get(1).copied().unwrap_or_else(|| 0) as u32; - let b2 = chunk.get(2).copied().unwrap_or_else(|| 0) as u32; + let b1 = chunk.get(1).copied().unwrap_or(0) as u32; + let b2 = chunk.get(2).copied().unwrap_or(0) as u32; let triple = (b0 << 16) | (b1 << 8) | b2; result.push(ALPHABET[((triple >> 18) & 0x3F) as usize] as char); diff --git a/src/ui/public/prove.html b/src/ui/public/prove.html new file mode 100644 index 00000000..2c2a11d4 --- /dev/null +++ b/src/ui/public/prove.html @@ -0,0 +1,279 @@ + + + + + + + ECHIDNA — Prove + + + +
+

ECHIDNA — Prove

+
Minimum-viable REST client. Start the server with + cargo run -- server --cors and aim this page at it.
+
+ +
+
+
+
+ + +
+
+ unknown +
+
+ + + + +
+
+ + +
+
+ + +
+
+ + + +
+ examples: + Z3 SAT + Z3 UNSAT +
+ + + +
+ +
+
+ RESULT + idle +
+
+ goals: — + elapsed: — ms +
+ + 
// no request yet
+
+
+ + + + diff --git a/tests/panic_attack_props.rs b/tests/panic_attack_props.rs index 24d5411c..4b6f71b4 100644 --- a/tests/panic_attack_props.rs +++ b/tests/panic_attack_props.rs @@ -363,3 +363,140 @@ mod pareto_props { } } } + +// ── Module 5: metamath_parser_props ────────────────────────────────────────── +// +// The Metamath backend is the only prover with an in-process pure-Rust +// parser, so it is also the only one we can panic-attack without an +// external binary. The contract under test is simple: `parse_string` +// must either succeed or return an `Err`; it must never panic, abort, +// or take unbounded time on arbitrary input. Discovered while sweeping +// the API surface that several valid-looking `.mm` fixtures parse to +// an empty `ProofState`; the property below pins the weaker (no-panic) +// invariant while the parser bug is investigated. + +mod metamath_parser_props { + use echidna::provers::metamath::MetamathBackend; + use echidna::provers::{ProverBackend, ProverConfig}; + use proptest::prelude::*; + + fn backend() -> MetamathBackend { + MetamathBackend::new(ProverConfig::default()) + } + + proptest! { + // Arbitrary ASCII input must not panic. Tokenizer / scope-stack / + // statement-parser paths all see the input here. + #[test] + fn prop_parse_string_ascii_no_panic(s in "[\\x20-\\x7e\\n\\t]{0,512}") { + let rt = tokio::runtime::Runtime::new().expect("runtime"); + let backend = backend(); + // We intentionally do not assert Ok/Err — only the absence of + // panic and that any returned `ProofState` is well-formed. + let _ = rt.block_on(backend.parse_string(&s)); + } + } + + proptest! { + // Mixed-binary input including `$` punctuation, comment markers, + // and unbalanced braces. Pin against parser panics on real-world + // garbage that a user might POST to `/api/prove`. + #[test] + fn prop_parse_string_mixed_no_panic(s in ".{0,512}") { + let rt = tokio::runtime::Runtime::new().expect("runtime"); + let backend = backend(); + let _ = rt.block_on(backend.parse_string(&s)); + } + } + + proptest! { + // Bounded-size keyword-heavy input — biases the parser towards + // exercising the `$c / $v / $a / $p / $f / ${ $}` branches. + #[test] + fn prop_parse_string_keyword_heavy_no_panic( + tokens in proptest::collection::vec( + prop_oneof![ + Just("$c".to_string()), + Just("$v".to_string()), + Just("$a".to_string()), + Just("$p".to_string()), + Just("$f".to_string()), + Just("$e".to_string()), + Just("${".to_string()), + Just("$}".to_string()), + Just("$.".to_string()), + Just("$(".to_string()), + Just("$)".to_string()), + "[a-z]{1,8}".prop_map(String::from), + ], + 0..40, + ), + ) { + let rt = tokio::runtime::Runtime::new().expect("runtime"); + let backend = backend(); + let src = tokens.join(" "); + let _ = rt.block_on(backend.parse_string(&src)); + } + } +} + +// ── Module 6: prover_kind_props ────────────────────────────────────────────── +// +// `ProverKind` is the JSON surface of `/api/prove`. Its serde +// round-trip is on every request path, so the invariant +// "serialize ∘ deserialize = id" must hold for every variant. +// Otherwise a request with a valid prover name could fail at the +// edge even though `ProverFactory::create` would have accepted it. + +mod prover_kind_props { + use echidna::provers::ProverKind; + use proptest::prelude::*; + + fn arb_prover_kind() -> impl Strategy { + // Restrict to the canonical roster — `all()` is what + // `ProverFactory::create` is contracted to support. + let kinds = ProverKind::all(); + (0..kinds.len()).prop_map(move |i| kinds[i]) + } + + proptest! { + #[test] + fn prop_serde_roundtrip(kind in arb_prover_kind()) { + let json = serde_json::to_string(&kind).expect("serialize"); + let back: ProverKind = serde_json::from_str(&json).expect("deserialize"); + prop_assert_eq!(kind, back, "ProverKind {:?} did not round-trip via JSON", kind); + } + } + + proptest! { + #[test] + fn prop_tier_in_bounds(kind in arb_prover_kind()) { + let tier = kind.tier(); + prop_assert!((1..=10).contains(&tier), + "tier() returned {} for {:?}, expected 1..=10", tier, kind); + } + } + + proptest! { + #[test] + fn prop_complexity_in_bounds(kind in arb_prover_kind()) { + let c = kind.complexity(); + prop_assert!((1..=5).contains(&c), + "complexity() returned {} for {:?}, expected 1..=5", c, kind); + } + } + + #[test] + fn all_core_is_subset_of_all() { + let core = ProverKind::all_core(); + let all = ProverKind::all(); + for k in &core { + assert!( + all.contains(k), + "ProverKind::{:?} in all_core() but not in all() — \ + the core set must be a subset of the advertised roster", + k + ); + } + } +} diff --git a/training_data/proof_states_mathcomp.a2ml b/training_data/proof_states_mathcomp.a2ml index 99f4f63c..835d9780 100644 --- a/training_data/proof_states_mathcomp.a2ml +++ b/training_data/proof_states_mathcomp.a2ml @@ -4,6 +4,8 @@ # mathcomp proof-state records (Coq/ssreflect training data) [metadata] +name = "echidna-training-proof-states-mathcomp" +project = "echidna" id_range = "200000-223901" extraction_date = "2026-04-20T08:30:19" total_proofs = 23902 diff --git a/training_data/stats_mathcomp.a2ml b/training_data/stats_mathcomp.a2ml index c7a1e758..f569e9ae 100644 --- a/training_data/stats_mathcomp.a2ml +++ b/training_data/stats_mathcomp.a2ml @@ -3,6 +3,8 @@ # mathcomp extraction statistics [metadata] +name = "echidna-training-stats-mathcomp" +project = "echidna" id_range = "200000-223901" extraction_date = "2026-04-20T08:30:19" total_proofs = 23902 diff --git a/training_data/stats_tptp.a2ml b/training_data/stats_tptp.a2ml index fabbe2a6..b2d2c56b 100644 --- a/training_data/stats_tptp.a2ml +++ b/training_data/stats_tptp.a2ml @@ -3,6 +3,8 @@ # TPTP extraction statistics [metadata] +name = "echidna-training-stats-tptp" +project = "echidna" id_range = "70000-148530" extraction_date = "2026-04-18T08:38:10" total_proofs = 78531 diff --git a/training_data/tactics_mathcomp.a2ml b/training_data/tactics_mathcomp.a2ml index 1dfd20ad..11666846 100644 --- a/training_data/tactics_mathcomp.a2ml +++ b/training_data/tactics_mathcomp.a2ml @@ -4,6 +4,8 @@ # mathcomp tactic records (ssreflect tactics per step) [metadata] +name = "echidna-training-mathcomp" +project = "echidna" id_range = "200000-223901" extraction_date = "2026-04-20T08:30:19" total_proofs = 23902 diff --git a/training_data/tactics_tptp.a2ml b/training_data/tactics_tptp.a2ml index 1a1096ee..2c3f4547 100644 --- a/training_data/tactics_tptp.a2ml +++ b/training_data/tactics_tptp.a2ml @@ -4,6 +4,8 @@ # TPTP tactic records (one per proof-state) [metadata] +name = "echidna-training-tptp" +project = "echidna" id_range = "70000-148530" extraction_date = "2026-04-18T08:38:10" total_proofs = 78531