diff --git a/.claude/settings.local.json b/.claude/settings.local.json index c83a93a..a7669cd 100644 --- a/.claude/settings.local.json +++ b/.claude/settings.local.json @@ -3,7 +3,9 @@ "allow": [ "Bash(iwconfig)", "Bash(nmcli radio:*)", - "Bash(nmcli:*)" + "Bash(nmcli:*)", + "Bash(git restore *)", + "Bash(rm -f tests/live_goals/.broken.aux tests/live_goals/.identity.aux tests/live_goals/Identity.agdai tests/live_goals/broken.glob)" ] } } diff --git a/Cargo.lock b/Cargo.lock index 922f5b4..4b5f36b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -196,7 +196,7 @@ dependencies = [ "futures-util", "handlebars", "http", - "indexmap 2.14.0", + "indexmap", "mime", "multer", "num-traits", @@ -263,7 +263,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3e3ef112905abea9dea592fc868a6873b10ebd3f983e83308f995d6284e9ba41" dependencies = [ "bytes", - "indexmap 2.14.0", + "indexmap", "serde", "serde_json", ] @@ -286,28 +286,6 @@ dependencies = [ "windows-sys 0.61.2", ] -[[package]] -name = "async-stream" -version = "0.3.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b5a71a6f37880a80d1d7f19efd781e4b5de42c88f0722cc13bcb6cc2cfe8476" -dependencies = [ - "async-stream-impl", - "futures-core", - "pin-project-lite", -] - -[[package]] -name = "async-stream-impl" -version = "0.3.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c7c24de15d275a1ecfd47a380fb4d5ec9bfe0933f309ed5e705b775596a3574d" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] - [[package]] name = "async-trait" version = "0.1.89" @@ -370,7 +348,7 @@ dependencies = [ "serde_urlencoded", "sync_wrapper", "tokio", - "tower 0.5.3", + "tower", "tower-layer", "tower-service", "tracing", @@ -406,7 +384,7 @@ dependencies = [ "sync_wrapper", "tokio", "tokio-tungstenite", - "tower 0.5.3", + "tower", "tower-layer", "tower-service", "tracing", @@ -1027,7 +1005,7 @@ dependencies = [ "tokio", "tokio-test", "toml", - "tower 0.5.3", + "tower", "tower-http", "tracing", "tracing-subscriber", @@ -1079,7 +1057,8 @@ dependencies = [ "tokio", "tokio-stream", "tonic", - "tonic-build", + "tonic-prost", + "tonic-prost-build", "tracing", "tracing-subscriber", "uuid", @@ -1112,7 +1091,7 @@ dependencies = [ "serde_json", "thiserror", "tokio", - "tower 0.5.3", + "tower", "tower-http", "tracing", "tracing-subscriber", @@ -1434,7 +1413,7 @@ dependencies = [ "futures-core", "futures-sink", "http", - "indexmap 2.14.0", + "indexmap", "slab", "tokio", "tokio-util", @@ -1468,12 +1447,6 @@ dependencies = [ "thiserror", ] -[[package]] -name = "hashbrown" -version = "0.12.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" - [[package]] name = "hashbrown" version = "0.15.5" @@ -1639,7 +1612,7 @@ dependencies = [ "libc", "percent-encoding", "pin-project-lite", - "socket2 0.6.3", + "socket2", "system-configuration", "tokio", "tower-service", @@ -1786,16 +1759,6 @@ dependencies = [ "icu_properties", ] -[[package]] -name = "indexmap" -version = "1.9.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99" -dependencies = [ - "autocfg", - "hashbrown 0.12.3", -] - [[package]] name = "indexmap" version = "2.14.0" @@ -2263,12 +2226,13 @@ dependencies = [ [[package]] name = "petgraph" -version = "0.7.1" +version = "0.8.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3672b37090dbd86368a4145bc067582552b29c27377cad4e0a306c97f9bd7772" +checksum = "8701b58ea97060d5e5b155d383a69952a60943f0e6dfe30b04c287beb0b27455" dependencies = [ "fixedbitset", - "indexmap 2.14.0", + "hashbrown 0.15.5", + "indexmap", ] [[package]] @@ -2417,8 +2381,8 @@ dependencies = [ "bit-vec", "bitflags", "num-traits", - "rand 0.9.4", - "rand_chacha 0.9.0", + "rand", + "rand_chacha", "rand_xorshift", "regex-syntax", "rusty-fork", @@ -2428,9 +2392,9 @@ dependencies = [ [[package]] name = "prost" -version = "0.13.5" +version = "0.14.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2796faa41db3ec313a31f7624d9286acf277b52de526150b7e69f3debf891ee5" +checksum = "d2ea70524a2f82d518bce41317d0fae74151505651af45faf1ffbd6fd33f0568" dependencies = [ "bytes", "prost-derive", @@ -2438,19 +2402,20 @@ dependencies = [ [[package]] name = "prost-build" -version = "0.13.5" +version = "0.14.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "be769465445e8c1474e9c5dac2018218498557af32d9ed057325ec9a41ae81bf" +checksum = "343d3bd7056eda839b03204e68deff7d1b13aba7af2b2fd16890697274262ee7" dependencies = [ "heck", "itertools 0.14.0", "log", "multimap", - "once_cell", "petgraph", "prettyplease", "prost", "prost-types", + "pulldown-cmark", + "pulldown-cmark-to-cmark", "regex", "syn", "tempfile", @@ -2458,9 +2423,9 @@ dependencies = [ [[package]] name = "prost-derive" -version = "0.13.5" +version = "0.14.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8a56d757972c98b346a9b766e3f02746cde6dd1cd1d1d563472929fdd74bec4d" +checksum = "27c6023962132f4b30eb4c172c91ce92d933da334c59c23cddee82358ddafb0b" dependencies = [ "anyhow", "itertools 0.14.0", @@ -2471,13 +2436,33 @@ dependencies = [ [[package]] name = "prost-types" -version = "0.13.5" +version = "0.14.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "52c2c1bf36ddb1a1c396b3601a3cec27c2462e45f07c386894ec3ccf5332bd16" +checksum = "8991c4cbdb8bc5b11f0b074ffe286c30e523de90fee5ba8132f1399f23cb3dd7" dependencies = [ "prost", ] +[[package]] +name = "pulldown-cmark" +version = "0.13.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c3a14896dfa883796f1cb410461aef38810ea05f2b2c33c5aded3649095fdad" +dependencies = [ + "bitflags", + "memchr", + "unicase", +] + +[[package]] +name = "pulldown-cmark-to-cmark" +version = "22.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "50793def1b900256624a709439404384204a5dc3a6ec580281bfaac35e882e90" +dependencies = [ + "pulldown-cmark", +] + [[package]] name = "quick-error" version = "1.2.3" @@ -2497,7 +2482,7 @@ dependencies = [ "quinn-udp", "rustc-hash", "rustls", - "socket2 0.6.3", + "socket2", "thiserror", "tokio", "tracing", @@ -2513,7 +2498,7 @@ dependencies = [ "bytes", "getrandom 0.3.4", "lru-slab", - "rand 0.9.4", + "rand", "ring", "rustc-hash", "rustls", @@ -2534,7 +2519,7 @@ dependencies = [ "cfg_aliases", "libc", "once_cell", - "socket2 0.6.3", + "socket2", "tracing", "windows-sys 0.60.2", ] @@ -2570,35 +2555,14 @@ dependencies = [ "nibble_vec", ] -[[package]] -name = "rand" -version = "0.8.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5ca0ecfa931c29007047d1bc58e623ab12e5590e8c7cc53200d5202b69266d8a" -dependencies = [ - "libc", - "rand_chacha 0.3.1", - "rand_core 0.6.4", -] - [[package]] name = "rand" version = "0.9.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea" dependencies = [ - "rand_chacha 0.9.0", - "rand_core 0.9.5", -] - -[[package]] -name = "rand_chacha" -version = "0.3.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" -dependencies = [ - "ppv-lite86", - "rand_core 0.6.4", + "rand_chacha", + "rand_core", ] [[package]] @@ -2608,16 +2572,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb" dependencies = [ "ppv-lite86", - "rand_core 0.9.5", -] - -[[package]] -name = "rand_core" -version = "0.6.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" -dependencies = [ - "getrandom 0.2.17", + "rand_core", ] [[package]] @@ -2635,7 +2590,7 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "513962919efc330f829edb2535844d1b912b0fbe2ca165d613e4e8788bb05a5a" dependencies = [ - "rand_core 0.9.5", + "rand_core", ] [[package]] @@ -2750,7 +2705,7 @@ dependencies = [ "tokio", "tokio-native-tls", "tokio-rustls", - "tower 0.5.3", + "tower", "tower-http", "tower-service", "url", @@ -2877,15 +2832,6 @@ dependencies = [ "zeroize", ] -[[package]] -name = "rustls-pemfile" -version = "2.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dce314e5fee3f39953d46bb63bb8a46d40c2f8fb7cc5a3b6cab2bde9721d6e50" -dependencies = [ - "rustls-pki-types", -] - [[package]] name = "rustls-pki-types" version = "1.14.1" @@ -3183,16 +3129,6 @@ version = "1.15.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03" -[[package]] -name = "socket2" -version = "0.5.10" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e22376abed350d73dd1cd119b57ffccad95b4e585a7cda43e286245ce23c0678" -dependencies = [ - "libc", - "windows-sys 0.52.0", -] - [[package]] name = "socket2" version = "0.6.3" @@ -3404,7 +3340,7 @@ dependencies = [ "parking_lot", "pin-project-lite", "signal-hook-registry", - "socket2 0.6.3", + "socket2", "tokio-macros", "windows-sys 0.61.2", ] @@ -3524,7 +3460,7 @@ version = "0.22.27" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "41fe8c660ae4257887cf66394862d21dbca4a6ddd26f04a3560410406a2f819a" dependencies = [ - "indexmap 2.14.0", + "indexmap", "serde", "serde_spanned", "toml_datetime 0.6.11", @@ -3538,7 +3474,7 @@ version = "0.25.11+spec-1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b59c4d22ed448339746c59b905d24568fcbb3ab65a500494f7b8c3e97739f2b" dependencies = [ - "indexmap 2.14.0", + "indexmap", "toml_datetime 1.1.1+spec-1.1.0", "toml_parser", "winnow 1.0.2", @@ -3561,13 +3497,12 @@ checksum = "5d99f8c9a7727884afe522e9bd5edbfc91a3312b36a77b5fb8926e4c31a41801" [[package]] name = "tonic" -version = "0.12.3" +version = "0.14.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "877c5b330756d856ffcc4553ab34a5684481ade925ecc54bcd1bf02b1d0d4d52" +checksum = "fec7c61a0695dc1887c1b53952990f3ad2e3a31453e1f49f10e75424943a93ec" dependencies = [ - "async-stream", "async-trait", - "axum 0.7.9", + "axum 0.8.9", "base64", "bytes", "h2", @@ -3579,13 +3514,12 @@ dependencies = [ "hyper-util", "percent-encoding", "pin-project", - "prost", - "rustls-pemfile", - "socket2 0.5.10", + "socket2", + "sync_wrapper", "tokio", "tokio-rustls", "tokio-stream", - "tower 0.4.13", + "tower", "tower-layer", "tower-service", "tracing", @@ -3593,36 +3527,41 @@ dependencies = [ [[package]] name = "tonic-build" -version = "0.12.3" +version = "0.14.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9557ce109ea773b399c9b9e5dca39294110b74f1f342cb347a80d1fce8c26a11" +checksum = "1882ac3bf5ef12877d7ed57aad87e75154c11931c2ba7e6cde5e22d63522c734" dependencies = [ "prettyplease", "proc-macro2", - "prost-build", - "prost-types", "quote", "syn", ] [[package]] -name = "tower" -version = "0.4.13" +name = "tonic-prost" +version = "0.14.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b8fa9be0de6cf49e536ce1851f987bd21a43b771b09473c3549a6c853db37c1c" +checksum = "a55376a0bbaa4975a3f10d009ad763d8f4108f067c7c2e74f3001fb49778d309" dependencies = [ - "futures-core", - "futures-util", - "indexmap 1.9.3", - "pin-project", - "pin-project-lite", - "rand 0.8.6", - "slab", - "tokio", - "tokio-util", - "tower-layer", - "tower-service", - "tracing", + "bytes", + "prost", + "tonic", +] + +[[package]] +name = "tonic-prost-build" +version = "0.14.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f3144df636917574672e93d0f56d7edec49f90305749c668df5101751bb8f95a" +dependencies = [ + "prettyplease", + "proc-macro2", + "prost-build", + "prost-types", + "quote", + "syn", + "tempfile", + "tonic-build", ] [[package]] @@ -3633,9 +3572,12 @@ checksum = "ebe5ef63511595f1344e2d5cfa636d973292adc0eec1f0ad45fae9f0851ab1d4" dependencies = [ "futures-core", "futures-util", + "indexmap", "pin-project-lite", + "slab", "sync_wrapper", "tokio", + "tokio-util", "tower-layer", "tower-service", "tracing", @@ -3654,7 +3596,7 @@ dependencies = [ "http-body", "iri-string", "pin-project-lite", - "tower 0.5.3", + "tower", "tower-layer", "tower-service", "tracing", @@ -3751,7 +3693,7 @@ dependencies = [ "http", "httparse", "log", - "rand 0.9.4", + "rand", "sha1", "thiserror", ] @@ -3853,7 +3795,7 @@ version = "5.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2fcc29c80c21c31608227e0912b2d7fddba57ad76b606890627ba8ee7964e993" dependencies = [ - "indexmap 2.14.0", + "indexmap", "serde", "serde_json", "utoipa-gen", @@ -4043,7 +3985,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bb0e353e6a2fbdc176932bbaab493762eb1255a7900fe0fea1a2f96c296cc909" dependencies = [ "anyhow", - "indexmap 2.14.0", + "indexmap", "wasm-encoder", "wasmparser", ] @@ -4056,7 +3998,7 @@ checksum = "47b807c72e1bac69382b3a6fb3dbe8ea4c0ed87ff5629b8685ae6b9a611028fe" dependencies = [ "bitflags", "hashbrown 0.15.5", - "indexmap 2.14.0", + "indexmap", "semver", ] @@ -4403,7 +4345,7 @@ checksum = "b7c566e0f4b284dd6561c786d9cb0142da491f46a9fbed79ea69cdad5db17f21" dependencies = [ "anyhow", "heck", - "indexmap 2.14.0", + "indexmap", "prettyplease", "syn", "wasm-metadata", @@ -4434,7 +4376,7 @@ checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2" dependencies = [ "anyhow", "bitflags", - "indexmap 2.14.0", + "indexmap", "log", "serde", "serde_derive", @@ -4453,7 +4395,7 @@ checksum = "ecc8ac4bc1dc3381b7f59c34f00b67e18f910c2c0f50015669dde7def656a736" dependencies = [ "anyhow", "id-arena", - "indexmap 2.14.0", + "indexmap", "log", "semver", "serde", @@ -4589,7 +4531,7 @@ dependencies = [ "crossbeam-utils", "displaydoc", "flate2", - "indexmap 2.14.0", + "indexmap", "memchr", "thiserror", "zopfli", diff --git a/src/interfaces/grpc/Cargo.toml b/src/interfaces/grpc/Cargo.toml index adcd2d1..2bc8e43 100644 --- a/src/interfaces/grpc/Cargo.toml +++ b/src/interfaces/grpc/Cargo.toml @@ -18,8 +18,9 @@ path = "main.rs" [dependencies] # gRPC -tonic = "0.12" -prost = "0.13" +tonic = "0.14" +tonic-prost = "0.14" +prost = "0.14" tokio = { version = "1.41", features = ["full"] } tokio-stream = "0.1" @@ -45,7 +46,7 @@ uuid = { version = "1.11", features = ["v4", "serde"] } async-trait = "0.1" [build-dependencies] -tonic-build = "0.12" +tonic-prost-build = "0.14" [dev-dependencies] -tonic = { version = "0.12", features = ["tls"] } +tonic = { version = "0.14", features = ["tls-ring"] } diff --git a/src/interfaces/grpc/build.rs b/src/interfaces/grpc/build.rs index b0d2f93..818364c 100644 --- a/src/interfaces/grpc/build.rs +++ b/src/interfaces/grpc/build.rs @@ -1,6 +1,6 @@ // SPDX-License-Identifier: PMPL-1.0-or-later fn main() -> Result<(), Box> { - tonic_build::compile_protos("proto/echidna.proto")?; + tonic_prost_build::compile_protos("proto/echidna.proto")?; Ok(()) } diff --git a/src/interfaces/grpc/ffi_wrapper.rs b/src/interfaces/grpc/ffi_wrapper.rs index 4ac6e38..2d39533 100644 --- a/src/interfaces/grpc/ffi_wrapper.rs +++ b/src/interfaces/grpc/ffi_wrapper.rs @@ -2,12 +2,9 @@ // gRPC FFI Wrapper - Connects gRPC interface to ECHIDNA Rust core via Zig FFI use std::ffi::{CString, CStr}; -use std::os::raw::{c_int, c_void}; +use std::os::raw::c_int; use anyhow::{Result, anyhow}; -// Re-export FFI types from core -pub use echidna::ffi::{FfiStatus, FfiStringSlice, FfiOwnedString, FfiProverConfig}; - // External Zig FFI functions (from libechidna_ffi.so) extern "C" { pub fn echidna_init() -> c_int; @@ -32,7 +29,7 @@ pub fn init_ffi() -> Result<()> { let err_msg = if err_ptr.is_null() { "Unknown FFI initialization error".to_string() } else { - CStr::from_ptr(err_ptr).to_string_lossy().into_owned() + CStr::from_ptr(err_ptr.cast()).to_string_lossy().into_owned() }; return Err(anyhow!("FFI initialization failed: {}", err_msg)); } @@ -47,7 +44,7 @@ pub fn get_version() -> Result { if ptr.is_null() { return Err(anyhow!("FFI version pointer is null")); } - let version = CStr::from_ptr(ptr).to_string_lossy().into_owned(); + let version = CStr::from_ptr(ptr.cast()).to_string_lossy().into_owned(); Ok(version) } } @@ -59,7 +56,7 @@ pub fn get_last_error() -> Result { if ptr.is_null() { return Err(anyhow!("No error message available")); } - let error = CStr::from_ptr(ptr).to_string_lossy().into_owned(); + let error = CStr::from_ptr(ptr.cast()).to_string_lossy().into_owned(); Ok(error) } } @@ -88,7 +85,7 @@ pub fn destroy_prover(handle: i32) -> Result<()> { pub fn parse_string(handle: i32, content: &str) -> Result<()> { unsafe { let c_content = CString::new(content)?; - let rc = echidna_parse_string(handle, c_content.as_ptr(), content.len()); + let rc = echidna_parse_string(handle, c_content.as_ptr().cast(), content.len()); if rc != 0 { let error = get_last_error()?; return Err(anyhow!("Parse failed: {}", error)); @@ -109,7 +106,7 @@ pub fn verify_proof(handle: i32) -> Result { pub fn apply_tactic(handle: i32, tactic: &str) -> Result { unsafe { let c_tactic = CString::new(tactic)?; - let rc = echidna_apply_tactic(handle, c_tactic.as_ptr(), tactic.len()); + let rc = echidna_apply_tactic(handle, c_tactic.as_ptr().cast(), tactic.len()); Ok(rc == 0) } } diff --git a/src/interfaces/grpc/main.rs b/src/interfaces/grpc/main.rs index 33e17c8..d8418da 100644 --- a/src/interfaces/grpc/main.rs +++ b/src/interfaces/grpc/main.rs @@ -1,7 +1,7 @@ // SPDX-License-Identifier: PMPL-1.0-or-later // ECHIDNA gRPC Server - wired to core -use echidna::core::{Tactic as CoreTactic, TacticResult as CoreTacticResult, Term}; +use echidna::core::{Tactic as CoreTactic, TacticResult, Term}; use echidna::provers::{ProverBackend, ProverConfig, ProverFactory, ProverKind as CoreProverKind}; use echidna_proto::v1::proof_service_server::{ProofService, ProofServiceServer}; use echidna_proto::v1::*; @@ -10,8 +10,8 @@ use std::sync::Arc; use tokio::sync::{Mutex, RwLock}; use tonic::{transport::Server, Request, Response, Status}; -// Import FFI wrapper -use crate::ffi_wrapper; +// FFI wrapper module — file lives next to main.rs. +mod ffi_wrapper; pub mod echidna_proto { pub mod v1 { @@ -22,11 +22,15 @@ pub mod echidna_proto { /// Wrapper for FFI-based prover backend struct FfiProverBackend { handle: i32, + config: ProverConfig, } impl FfiProverBackend { pub fn new(handle: i32) -> Self { - FfiProverBackend { handle } + FfiProverBackend { + handle, + config: ProverConfig::default(), + } } } @@ -38,15 +42,29 @@ impl ProverBackend for FfiProverBackend { ) -> anyhow::Result { let content = std::fs::read_to_string(&path)?; ffi_wrapper::parse_string(self.handle, &content)?; - Ok(echidna::core::ProofState::new(content)) + let mut state = echidna::core::ProofState::new(Term::Hole(content.clone())); + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + state.metadata.insert( + "ffi_source".to_string(), + serde_json::Value::String(content), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> anyhow::Result { ffi_wrapper::parse_string(self.handle, content)?; - Ok(echidna::core::ProofState::new(content.to_string())) + let mut state = echidna::core::ProofState::new(Term::Hole(content.to_string())); + state.metadata.insert( + "ffi_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } - async fn verify_proof(&self, state: &echidna::core::ProofState) -> anyhow::Result { + async fn verify_proof(&self, _state: &echidna::core::ProofState) -> anyhow::Result { ffi_wrapper::verify_proof(self.handle) } @@ -57,7 +75,7 @@ impl ProverBackend for FfiProverBackend { ) -> anyhow::Result { let tactic_str = format!("{:?}", tactic); if ffi_wrapper::apply_tactic(self.handle, &tactic_str)? { - Ok(TacticResult::Success(Box::new(state.clone()))) + Ok(TacticResult::Success(state.clone())) } else { Ok(TacticResult::Error("Tactic failed".to_string())) } @@ -65,7 +83,7 @@ impl ProverBackend for FfiProverBackend { async fn suggest_tactics( &self, - state: &echidna::core::ProofState, + _state: &echidna::core::ProofState, limit: usize, ) -> anyhow::Result> { let tactic_names = ffi_wrapper::suggest_tactics(self.handle, limit)?; @@ -80,7 +98,13 @@ impl ProverBackend for FfiProverBackend { Ok(tactics) } - async fn export(&self, state: &echidna::core::ProofState) -> anyhow::Result { + async fn search_theorems(&self, _pattern: &str) -> anyhow::Result> { + // FFI layer doesn't expose theorem search yet; return empty so the + // gRPC service can still satisfy the trait contract. + Ok(Vec::new()) + } + + async fn export(&self, _state: &echidna::core::ProofState) -> anyhow::Result { ffi_wrapper::export_proof(self.handle) } @@ -92,6 +116,14 @@ impl ProverBackend for FfiProverBackend { // This is a bit simplified - in a real implementation we'd track the kind CoreProverKind::Lean // Default, would need to be set during creation } + + fn config(&self) -> &ProverConfig { + &self.config + } + + fn set_config(&mut self, config: ProverConfig) { + self.config = config; + } } struct ProofSession { @@ -167,7 +199,9 @@ impl ProofService for ProofServiceImpl { let session = ProofSession { prover_kind: core_kind, prover: Box::new(FfiProverBackend::new(handle)), - state: Some(echidna::core::ProofState::new(req.goal.clone())), + state: Some(echidna::core::ProofState::new(Term::Hole( + req.goal.clone(), + ))), goal: req.goal.clone(), status, history: vec![], @@ -377,7 +411,7 @@ impl ProofService for ProofServiceImpl { .map_err(|e| Status::internal(e.to_string()))?; let success = match &result { - CoreTacticResult::Success(new_state) => { + TacticResult::Success(new_state) => { let complete = new_state.is_complete(); session.state = Some(new_state.clone()); session.history.push(format!("{:?}", tactic)); @@ -386,14 +420,14 @@ impl ProofService for ProofServiceImpl { } true }, - CoreTacticResult::QED => { + TacticResult::QED => { session.status = ProofStatus::Success as i32; if let Some(s) = session.state.as_mut() { s.goals.clear(); } true }, - CoreTacticResult::Error(_) => false, + TacticResult::Error(_) => false, }; let elapsed = session.start_time.elapsed().as_secs_f64(); @@ -413,7 +447,7 @@ impl ProofService for ProofServiceImpl { proof_script: script, time_elapsed: Some(elapsed), error_message: match &result { - CoreTacticResult::Error(msg) => Some(msg.clone()), + TacticResult::Error(msg) => Some(msg.clone()), _ => None, }, }), diff --git a/tests/live_goals/.gitignore b/tests/live_goals/.gitignore new file mode 100644 index 0000000..12869af --- /dev/null +++ b/tests/live_goals/.gitignore @@ -0,0 +1,8 @@ +# Coq compilation artifacts — generated when coqc runs on .v fixtures. +*.vo +*.vok +*.vos +*.glob +.*.aux +# Agda compilation artifacts +*.agdai diff --git a/tests/live_goals/Broken.agda b/tests/live_goals/Broken.agda new file mode 100644 index 0000000..b173e0d --- /dev/null +++ b/tests/live_goals/Broken.agda @@ -0,0 +1,5 @@ +-- Type error: claims A → B from no premise. +module Broken where + +bogus : (A : Set) -> (B : Set) -> A -> B +bogus A B x = x diff --git a/tests/live_goals/Identity.agda b/tests/live_goals/Identity.agda new file mode 100644 index 0000000..8e30dfc --- /dev/null +++ b/tests/live_goals/Identity.agda @@ -0,0 +1,4 @@ +module Identity where + +id : (A : Set) -> A -> A +id A x = x diff --git a/tests/live_goals/broken.v b/tests/live_goals/broken.v new file mode 100644 index 0000000..3f22961 --- /dev/null +++ b/tests/live_goals/broken.v @@ -0,0 +1,3 @@ +(* Type error: claims `True -> False` and proves with `exact I`. *) +Theorem broken : True -> False. +Proof. intro H. exact I. Qed. diff --git a/tests/live_goals/contradiction.smt2 b/tests/live_goals/contradiction.smt2 new file mode 100644 index 0000000..2e55821 --- /dev/null +++ b/tests/live_goals/contradiction.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_LIA) +(declare-const x Int) +; Satisfiable assertion — SAT, so verify_proof reports "not verified". +(assert (= x 1)) +(check-sat) diff --git a/tests/live_goals/identity.v b/tests/live_goals/identity.v new file mode 100644 index 0000000..be8fdd2 --- /dev/null +++ b/tests/live_goals/identity.v @@ -0,0 +1,2 @@ +Theorem identity : forall (P : Prop), P -> P. +Proof. intros P H. exact H. Qed. diff --git a/tests/live_goals/tautology.smt2 b/tests/live_goals/tautology.smt2 new file mode 100644 index 0000000..17a94ad --- /dev/null +++ b/tests/live_goals/tautology.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_LIA) +(declare-const x Int) +; Negation of a tautology (x = 0 ∨ x ≠ 0) — UNSAT means the tautology holds, +; which is what ECHIDNA's verify_proof reports as "verified". +(assert (not (or (= x 0) (not (= x 0))))) +(check-sat) diff --git a/tests/live_goals/trivial.dfg b/tests/live_goals/trivial.dfg new file mode 100644 index 0000000..2b15ff3 --- /dev/null +++ b/tests/live_goals/trivial.dfg @@ -0,0 +1,17 @@ +begin_problem(Trivial). +list_of_descriptions. +name({*Trivial*}). +author({*ECHIDNA test suite*}). +status(unsatisfiable). +description({*p implies p — discharged by resolution*}). +end_of_list. +list_of_symbols. +predicates[(p,0)]. +end_of_list. +list_of_formulae(axioms). +formula(p). +end_of_list. +list_of_formulae(conjectures). +formula(p). +end_of_list. +end_problem. diff --git a/tests/live_goals/trivial.mm b/tests/live_goals/trivial.mm new file mode 100644 index 0000000..230b58c --- /dev/null +++ b/tests/live_goals/trivial.mm @@ -0,0 +1,8 @@ +$( Minimal Metamath database — single $a (axiom) plus a $p (proof) that just + re-states the axiom. metamath's "verify proof *" reports + "All proofs in the database were verified" on success. $) +$c wff $. +$c p $. +wp $a wff p $. +th $p wff p $= + wp $. diff --git a/tests/live_prover_verify.rs b/tests/live_prover_verify.rs new file mode 100644 index 0000000..99b98e1 --- /dev/null +++ b/tests/live_prover_verify.rs @@ -0,0 +1,173 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// +// ECHIDNA — Live-Prover Verify Roundtrip Test Suite +// +// The Phase 3 backend fix (commits `ac209ee`, `b1258da`, `940e940`) reworked +// every lossy `verify_proof` so it prefers the original source over the +// Term-IR round-trip. The 625-test unit suite stubs solver binaries, so a +// regression in that fix would not be caught there. This suite runs the +// real `prove_command` pipeline (parse_file → verify_proof) against +// per-prover fixtures in `tests/live_goals/` and asserts both a positive +// verdict on a valid proof and a negative verdict on a broken one. +// +// Auto-skip semantics match `tests/live_prover_suite.rs`: when the binary +// isn't on PATH the test prints SKIP and returns Ok so developers without +// every prover installed don't see spurious failures. CI +// (.github/workflows/live-provers.yml) enables the feature per tier with +// the matching binary provisioned. +// +// Covered (apt-installable MVP): Z3, CVC5, Coq, Agda, Metamath, SPASS. +// Uncovered (need manual install, exercised inside Containerfile.mcp): +// Lean 4, Isabelle, F*, Mizar. + +#![cfg(feature = "live-provers")] + +use std::path::{Path, PathBuf}; + +use echidna::provers::{ProverBackend, ProverConfig, ProverFactory, ProverKind}; + +/// Locate a binary on PATH. Returns `None` when absent (auto-skip signal). +fn binary_on_path(name: &str) -> Option { + which::which(name).ok() +} + +/// `ProverConfig` pointing at the real binary with a tight timeout. +/// The short timeout keeps a misbehaving backend from stalling the matrix. +fn live_config(executable: &Path) -> ProverConfig { + ProverConfig { + executable: executable.to_path_buf(), + library_paths: vec![], + args: vec![], + timeout: 30, + neural_enabled: false, + } +} + +/// Instantiate a live backend. Returns `None` when the binary is absent. +fn try_live_backend(kind: ProverKind, exe: &str) -> Option> { + let resolved = binary_on_path(exe)?; + let config = live_config(&resolved); + ProverFactory::create(kind, config).ok() +} + +/// Fixture path relative to the crate root. +fn fixture(name: &str) -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("tests") + .join("live_goals") + .join(name) +} + +/// Run parse_file + verify_proof end-to-end against a fixture. +/// Returns `Ok(verified)`; `None` is caller's signal that the binary is +/// absent. Any *error* from the pipeline fails the test — the pipeline +/// should produce `Ok(true/false)`, never propagate an error for a +/// well-formed input/invalid-proof distinction. +async fn verify_fixture( + kind: ProverKind, + exe: &str, + fixture_name: &str, +) -> Option { + let backend = try_live_backend(kind, exe)?; + let path = fixture(fixture_name); + let state = backend + .parse_file(path.clone()) + .await + .unwrap_or_else(|e| panic!("{:?}: parse_file({:?}) failed: {e}", kind, path)); + let verified = backend + .verify_proof(&state) + .await + .unwrap_or_else(|e| panic!("{:?}: verify_proof({:?}) failed: {e}", kind, path)); + Some(verified) +} + +/// One positive + one negative assertion in the shape every MVP prover +/// test uses below. Skip (returning without panicking) when the binary +/// isn't on PATH. +async fn check_pair( + kind: ProverKind, + exe: &str, + good: &str, + bad: &str, +) { + let Some(ok) = verify_fixture(kind, exe, good).await else { + eprintln!("SKIP: {exe} not on PATH ({good}/{bad})"); + return; + }; + assert!( + ok, + "{kind:?}: expected verified=true for {good}, got false — \ + the source_path stash pattern regressed or the solver rejected the fixture", + ); + // Negative case is optional: some fixtures for some backends can't be + // reliably "broken" in a way the solver rejects quickly. Run only if + // the fixture exists. + if fixture(bad).exists() { + let bad_verdict = verify_fixture(kind, exe, bad) + .await + .expect("binary was present for good fixture, must be present for bad"); + assert!( + !bad_verdict, + "{kind:?}: expected verified=false for {bad}, got true — \ + the broken fixture unexpectedly type-checks", + ); + } +} + +// ============================================================================ +// SMT solvers (shared fixtures — same SMT-LIB works for Z3 and CVC5) +// ============================================================================ + +#[tokio::test(flavor = "multi_thread")] +async fn verify_roundtrip_z3() { + check_pair(ProverKind::Z3, "z3", "tautology.smt2", "contradiction.smt2").await; +} + +#[tokio::test(flavor = "multi_thread")] +async fn verify_roundtrip_cvc5() { + check_pair(ProverKind::CVC5, "cvc5", "tautology.smt2", "contradiction.smt2").await; +} + +// ============================================================================ +// Interactive proof assistants +// ============================================================================ + +#[tokio::test(flavor = "multi_thread")] +async fn verify_roundtrip_coq() { + check_pair(ProverKind::Coq, "coqc", "identity.v", "broken.v").await; +} + +#[tokio::test(flavor = "multi_thread")] +async fn verify_roundtrip_agda() { + check_pair(ProverKind::Agda, "agda", "Identity.agda", "Broken.agda").await; +} + +// ============================================================================ +// Specialised +// ============================================================================ + +#[tokio::test(flavor = "multi_thread")] +async fn verify_roundtrip_metamath() { + // Metamath's negative case (a deliberately broken .mm) would need a + // non-trivial database to construct. Positive-only for now — the + // CLI shells out to `metamath; verify proof *` and only accepts the + // "All proofs verified" banner. + check_pair(ProverKind::Metamath, "metamath", "trivial.mm", "__no_bad_fixture__").await; +} + +// ============================================================================ +// First-order ATP +// ============================================================================ + +#[tokio::test(flavor = "multi_thread")] +async fn verify_roundtrip_spass() { + // SPASS binary installs as /usr/bin/SPASS (uppercase) on Debian-derived + // distros. `which` is case-sensitive, so try both. + let exe = if binary_on_path("SPASS").is_some() { + "SPASS" + } else { + "spass" + }; + check_pair(ProverKind::SPASS, exe, "trivial.dfg", "__no_bad_fixture__").await; +}