From 72587ae7f162317e44a21cbf12850a3aac242bdb Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 28 Apr 2026 15:46:15 +0000 Subject: [PATCH] chore(audit): clear lib+test warnings, fix prober dispatch bug, sync GraphQL ProverKind MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Cargo `--lib --tests` and `cargo clippy --lib --tests` now run clean (0 warnings, 0 errors). 1460 unit + integration tests pass. Real bugs found and fixed: * `provers::mod::from_str`: `"prob"` alias was double-claimed. Line 525 routes it to `ProverKind::ProB` (B-method model checker); a later arm also tried to claim it for `ProverKind::ProbabilisticTypeChecker` (unreachable). Removed the dead alias — `prob-types` and `probabilistic` still reach the type-checker. * `gnn::fallback_monitor::record_fallback`: comment claimed "exponential moving average" with an unused `ema_weight = 0.2` local, but the formula is a cumulative arithmetic mean (and tests assert cumulative-mean values). Updated the comment to reflect actual behaviour and dropped the dead variable; SLA semantics unchanged. * `dispatch::cross_check_dispatch`: the cross-checker filter held the `health_status` `MutexGuard` across an `await` (clippy `await_holding_lock`). Restructured into an explicit scope so the guard is released before any await. * GraphQL workspace member did not compile: `cargo check -p echidna-graphql` reported 28 missing `ProverKind` variants. Synced `schema.rs` enum + `core_to_gql` + `gql_to_core`, `resolvers.rs` `ProverKindExt::{from_core,to_core}`, and `ffi_wrapper.rs` ordinals 113-140 with the core enum. (Mizar/MizAR are intentionally distinct.) Compliance fix: * `deno.json` license was `MIT OR AGPL-3.0-or-later` — project policy per CLAUDE.md is `PMPL-1.0-or-later` (explicitly "not AGPL"). Diagnostics fields preserved as ML acronyms: * `ModelHealth.{last_validation_nDCG, last_validation_MRR, nDCG_meets_threshold}` and `GnnTrainingMetrics.{nDCG, MRR}` now carry an `#[allow(non_snake_case)]` with a comment explaining that these field names match the JSON keys emitted by the Julia training pipeline (`src/julia/train_and_evaluate.jl`). Renaming would have silently broken the cross-language contract. Resilience accessors: * Exposed `CircuitBreaker::name(&self) -> &str` and `Bulkhead::config(&self) -> &BulkheadConfig` so the previously dead-but-stored fields are usable for diagnostics output. Remaining clippy items (mechanical): unused imports, doc list indentation, a few `field_reassign_with_default` cases (kept as-is with `#[allow(...)]` where the alternative is uglier), and type aliases for two complex closure-box types. Out of scope (left untouched): pre-existing `cargo fmt` drift across ~820 files, `cargo test --workspace` requires `protoc` (gRPC build), docs/* license-string drift in historical release notes, ROADMAP- acknowledged ReScript→AffineScript migration. https://claude.ai/code/session_01F6HnUof5QEwmf9nzbM8nc8 --- deno.json | 2 +- src/interfaces/graphql/ffi_wrapper.rs | 56 ++++++++++++++++ src/interfaces/graphql/resolvers.rs | 56 ++++++++++++++++ src/interfaces/graphql/schema.rs | 84 ++++++++++++++++++++++++ src/rust/agent/swarm.rs | 3 +- src/rust/coprocessor/audio.rs | 4 +- src/rust/coprocessor/fpga.rs | 2 +- src/rust/coprocessor/io.rs | 2 +- src/rust/coprocessor/math.rs | 2 +- src/rust/coprocessor/physics.rs | 4 +- src/rust/coprocessor/singular.rs | 2 +- src/rust/corpus/agda.rs | 2 +- src/rust/corpus/coq.rs | 3 +- src/rust/corpus/metrics.rs | 21 +++--- src/rust/corpus/mod.rs | 1 + src/rust/diagnostics/corpus_monitor.rs | 36 +++++----- src/rust/diagnostics/fallback_monitor.rs | 2 +- src/rust/diagnostics/gnn_training.rs | 6 +- src/rust/diagnostics/health.rs | 6 ++ src/rust/diagnostics/proof_failure.rs | 25 +++---- src/rust/dispatch.rs | 27 ++++---- src/rust/fault_tolerance/resilience.rs | 10 +++ src/rust/gnn/fallback_monitor.rs | 4 +- src/rust/learning/buchholz_rank.rs | 2 +- src/rust/learning/daemon.rs | 8 ++- src/rust/learning/design_search.rs | 2 + src/rust/main.rs | 1 + src/rust/provers/acl2.rs | 2 +- src/rust/provers/dafny.rs | 2 +- src/rust/provers/liquid_haskell.rs | 4 +- src/rust/provers/mod.rs | 2 +- src/rust/provers/princess.rs | 2 +- src/rust/provers/prob.rs | 5 +- src/rust/server.rs | 8 +-- src/rust/suggest/extractor.rs | 4 +- src/rust/suggest/tester.rs | 3 +- src/rust/suggest/variant.rs | 2 + tests/agentic_integration.rs | 2 - tests/neural_property_tests.rs | 4 +- tests/p2p_property_tests.rs | 6 +- tests/panic_attack_props.rs | 6 +- tests/stage1_integration_test.rs | 1 + 42 files changed, 320 insertions(+), 106 deletions(-) diff --git a/deno.json b/deno.json index 301212a..41cf90f 100644 --- a/deno.json +++ b/deno.json @@ -3,7 +3,7 @@ "name": "@echidna/provers", "version": "0.1.0", "description": "ECHIDNA - Neurosymbolic Theorem Proving Platform", - "license": "MIT OR AGPL-3.0-or-later", + "license": "PMPL-1.0-or-later", "compilerOptions": { "allowJs": false, diff --git a/src/interfaces/graphql/ffi_wrapper.rs b/src/interfaces/graphql/ffi_wrapper.rs index dbab4a0..92b5a52 100644 --- a/src/interfaces/graphql/ffi_wrapper.rs +++ b/src/interfaces/graphql/ffi_wrapper.rs @@ -288,6 +288,34 @@ pub fn prover_kind_to_ffi(kind: &crate::schema::ProverKind) -> u8 { crate::schema::ProverKind::Rocq => 110, crate::schema::ProverKind::UppaalStratego => 111, crate::schema::ProverKind::MizAR => 112, + crate::schema::ProverKind::GPUVerify => 113, + crate::schema::ProverKind::Faial => 114, + crate::schema::ProverKind::Leo3 => 115, + crate::schema::ProverKind::Satallax => 116, + crate::schema::ProverKind::Lash => 117, + crate::schema::ProverKind::AgsyHOL => 118, + crate::schema::ProverKind::IProver => 119, + crate::schema::ProverKind::Princess => 120, + crate::schema::ProverKind::Twee => 121, + crate::schema::ProverKind::MetiTarski => 122, + crate::schema::ProverKind::CSI => 123, + crate::schema::ProverKind::AProVE => 124, + crate::schema::ProverKind::GNATprove => 125, + crate::schema::ProverKind::Stainless => 126, + crate::schema::ProverKind::LiquidHaskell => 127, + crate::schema::ProverKind::KeYmaeraX => 128, + crate::schema::ProverKind::Qepcad => 129, + crate::schema::ProverKind::Redlog => 130, + crate::schema::ProverKind::MleanCoP => 131, + crate::schema::ProverKind::IleanCoP => 132, + crate::schema::ProverKind::NanoCoP => 133, + crate::schema::ProverKind::MetTeL2 => 134, + crate::schema::ProverKind::ELK => 135, + crate::schema::ProverKind::Konclude => 136, + crate::schema::ProverKind::Storm => 137, + crate::schema::ProverKind::ProB => 138, + crate::schema::ProverKind::EasyCrypt => 139, + crate::schema::ProverKind::CryptoVerif => 140, } } @@ -407,6 +435,34 @@ pub fn ffi_to_prover_kind(ordinal: u8) -> Option { 110 => Some(crate::schema::ProverKind::Rocq), 111 => Some(crate::schema::ProverKind::UppaalStratego), 112 => Some(crate::schema::ProverKind::MizAR), + 113 => Some(crate::schema::ProverKind::GPUVerify), + 114 => Some(crate::schema::ProverKind::Faial), + 115 => Some(crate::schema::ProverKind::Leo3), + 116 => Some(crate::schema::ProverKind::Satallax), + 117 => Some(crate::schema::ProverKind::Lash), + 118 => Some(crate::schema::ProverKind::AgsyHOL), + 119 => Some(crate::schema::ProverKind::IProver), + 120 => Some(crate::schema::ProverKind::Princess), + 121 => Some(crate::schema::ProverKind::Twee), + 122 => Some(crate::schema::ProverKind::MetiTarski), + 123 => Some(crate::schema::ProverKind::CSI), + 124 => Some(crate::schema::ProverKind::AProVE), + 125 => Some(crate::schema::ProverKind::GNATprove), + 126 => Some(crate::schema::ProverKind::Stainless), + 127 => Some(crate::schema::ProverKind::LiquidHaskell), + 128 => Some(crate::schema::ProverKind::KeYmaeraX), + 129 => Some(crate::schema::ProverKind::Qepcad), + 130 => Some(crate::schema::ProverKind::Redlog), + 131 => Some(crate::schema::ProverKind::MleanCoP), + 132 => Some(crate::schema::ProverKind::IleanCoP), + 133 => Some(crate::schema::ProverKind::NanoCoP), + 134 => Some(crate::schema::ProverKind::MetTeL2), + 135 => Some(crate::schema::ProverKind::ELK), + 136 => Some(crate::schema::ProverKind::Konclude), + 137 => Some(crate::schema::ProverKind::Storm), + 138 => Some(crate::schema::ProverKind::ProB), + 139 => Some(crate::schema::ProverKind::EasyCrypt), + 140 => Some(crate::schema::ProverKind::CryptoVerif), _ => None, } } diff --git a/src/interfaces/graphql/resolvers.rs b/src/interfaces/graphql/resolvers.rs index 14a5dba..cd49a2b 100644 --- a/src/interfaces/graphql/resolvers.rs +++ b/src/interfaces/graphql/resolvers.rs @@ -218,6 +218,34 @@ impl ProverKindExt for crate::schema::ProverKind { CoreProverKind::Rocq => crate::schema::ProverKind::Rocq, CoreProverKind::UppaalStratego => crate::schema::ProverKind::UppaalStratego, CoreProverKind::MizAR => crate::schema::ProverKind::MizAR, + CoreProverKind::GPUVerify => crate::schema::ProverKind::GPUVerify, + CoreProverKind::Faial => crate::schema::ProverKind::Faial, + CoreProverKind::Leo3 => crate::schema::ProverKind::Leo3, + CoreProverKind::Satallax => crate::schema::ProverKind::Satallax, + CoreProverKind::Lash => crate::schema::ProverKind::Lash, + CoreProverKind::AgsyHOL => crate::schema::ProverKind::AgsyHOL, + CoreProverKind::IProver => crate::schema::ProverKind::IProver, + CoreProverKind::Princess => crate::schema::ProverKind::Princess, + CoreProverKind::Twee => crate::schema::ProverKind::Twee, + CoreProverKind::MetiTarski => crate::schema::ProverKind::MetiTarski, + CoreProverKind::CSI => crate::schema::ProverKind::CSI, + CoreProverKind::AProVE => crate::schema::ProverKind::AProVE, + CoreProverKind::GNATprove => crate::schema::ProverKind::GNATprove, + CoreProverKind::Stainless => crate::schema::ProverKind::Stainless, + CoreProverKind::LiquidHaskell => crate::schema::ProverKind::LiquidHaskell, + CoreProverKind::KeYmaeraX => crate::schema::ProverKind::KeYmaeraX, + CoreProverKind::Qepcad => crate::schema::ProverKind::Qepcad, + CoreProverKind::Redlog => crate::schema::ProverKind::Redlog, + CoreProverKind::MleanCoP => crate::schema::ProverKind::MleanCoP, + CoreProverKind::IleanCoP => crate::schema::ProverKind::IleanCoP, + CoreProverKind::NanoCoP => crate::schema::ProverKind::NanoCoP, + CoreProverKind::MetTeL2 => crate::schema::ProverKind::MetTeL2, + CoreProverKind::ELK => crate::schema::ProverKind::ELK, + CoreProverKind::Konclude => crate::schema::ProverKind::Konclude, + CoreProverKind::Storm => crate::schema::ProverKind::Storm, + CoreProverKind::ProB => crate::schema::ProverKind::ProB, + CoreProverKind::EasyCrypt => crate::schema::ProverKind::EasyCrypt, + CoreProverKind::CryptoVerif => crate::schema::ProverKind::CryptoVerif, } } @@ -336,6 +364,34 @@ impl ProverKindExt for crate::schema::ProverKind { crate::schema::ProverKind::Rocq => CoreProverKind::Rocq, crate::schema::ProverKind::UppaalStratego => CoreProverKind::UppaalStratego, crate::schema::ProverKind::MizAR => CoreProverKind::MizAR, + crate::schema::ProverKind::GPUVerify => CoreProverKind::GPUVerify, + crate::schema::ProverKind::Faial => CoreProverKind::Faial, + crate::schema::ProverKind::Leo3 => CoreProverKind::Leo3, + crate::schema::ProverKind::Satallax => CoreProverKind::Satallax, + crate::schema::ProverKind::Lash => CoreProverKind::Lash, + crate::schema::ProverKind::AgsyHOL => CoreProverKind::AgsyHOL, + crate::schema::ProverKind::IProver => CoreProverKind::IProver, + crate::schema::ProverKind::Princess => CoreProverKind::Princess, + crate::schema::ProverKind::Twee => CoreProverKind::Twee, + crate::schema::ProverKind::MetiTarski => CoreProverKind::MetiTarski, + crate::schema::ProverKind::CSI => CoreProverKind::CSI, + crate::schema::ProverKind::AProVE => CoreProverKind::AProVE, + crate::schema::ProverKind::GNATprove => CoreProverKind::GNATprove, + crate::schema::ProverKind::Stainless => CoreProverKind::Stainless, + crate::schema::ProverKind::LiquidHaskell => CoreProverKind::LiquidHaskell, + crate::schema::ProverKind::KeYmaeraX => CoreProverKind::KeYmaeraX, + crate::schema::ProverKind::Qepcad => CoreProverKind::Qepcad, + crate::schema::ProverKind::Redlog => CoreProverKind::Redlog, + crate::schema::ProverKind::MleanCoP => CoreProverKind::MleanCoP, + crate::schema::ProverKind::IleanCoP => CoreProverKind::IleanCoP, + crate::schema::ProverKind::NanoCoP => CoreProverKind::NanoCoP, + crate::schema::ProverKind::MetTeL2 => CoreProverKind::MetTeL2, + crate::schema::ProverKind::ELK => CoreProverKind::ELK, + crate::schema::ProverKind::Konclude => CoreProverKind::Konclude, + crate::schema::ProverKind::Storm => CoreProverKind::Storm, + crate::schema::ProverKind::ProB => CoreProverKind::ProB, + crate::schema::ProverKind::EasyCrypt => CoreProverKind::EasyCrypt, + crate::schema::ProverKind::CryptoVerif => CoreProverKind::CryptoVerif, } } } diff --git a/src/interfaces/graphql/schema.rs b/src/interfaces/graphql/schema.rs index 1d8e2a3..cb23e8d 100644 --- a/src/interfaces/graphql/schema.rs +++ b/src/interfaces/graphql/schema.rs @@ -123,6 +123,34 @@ pub enum ProverKind { Rocq, UppaalStratego, MizAR, + GPUVerify, + Faial, + Leo3, + Satallax, + Lash, + AgsyHOL, + IProver, + Princess, + Twee, + MetiTarski, + CSI, + AProVE, + GNATprove, + Stainless, + LiquidHaskell, + KeYmaeraX, + Qepcad, + Redlog, + MleanCoP, + IleanCoP, + NanoCoP, + MetTeL2, + ELK, + Konclude, + Storm, + ProB, + EasyCrypt, + CryptoVerif, } /// Status of a proof attempt @@ -567,6 +595,34 @@ fn core_to_gql(kind: &CoreProverKind) -> ProverKind { CoreProverKind::Rocq => ProverKind::Rocq, CoreProverKind::UppaalStratego => ProverKind::UppaalStratego, CoreProverKind::MizAR => ProverKind::MizAR, + CoreProverKind::GPUVerify => ProverKind::GPUVerify, + CoreProverKind::Faial => ProverKind::Faial, + CoreProverKind::Leo3 => ProverKind::Leo3, + CoreProverKind::Satallax => ProverKind::Satallax, + CoreProverKind::Lash => ProverKind::Lash, + CoreProverKind::AgsyHOL => ProverKind::AgsyHOL, + CoreProverKind::IProver => ProverKind::IProver, + CoreProverKind::Princess => ProverKind::Princess, + CoreProverKind::Twee => ProverKind::Twee, + CoreProverKind::MetiTarski => ProverKind::MetiTarski, + CoreProverKind::CSI => ProverKind::CSI, + CoreProverKind::AProVE => ProverKind::AProVE, + CoreProverKind::GNATprove => ProverKind::GNATprove, + CoreProverKind::Stainless => ProverKind::Stainless, + CoreProverKind::LiquidHaskell => ProverKind::LiquidHaskell, + CoreProverKind::KeYmaeraX => ProverKind::KeYmaeraX, + CoreProverKind::Qepcad => ProverKind::Qepcad, + CoreProverKind::Redlog => ProverKind::Redlog, + CoreProverKind::MleanCoP => ProverKind::MleanCoP, + CoreProverKind::IleanCoP => ProverKind::IleanCoP, + CoreProverKind::NanoCoP => ProverKind::NanoCoP, + CoreProverKind::MetTeL2 => ProverKind::MetTeL2, + CoreProverKind::ELK => ProverKind::ELK, + CoreProverKind::Konclude => ProverKind::Konclude, + CoreProverKind::Storm => ProverKind::Storm, + CoreProverKind::ProB => ProverKind::ProB, + CoreProverKind::EasyCrypt => ProverKind::EasyCrypt, + CoreProverKind::CryptoVerif => ProverKind::CryptoVerif, } } @@ -685,5 +741,33 @@ fn gql_to_core(kind: &ProverKind) -> CoreProverKind { ProverKind::Rocq => CoreProverKind::Rocq, ProverKind::UppaalStratego => CoreProverKind::UppaalStratego, ProverKind::MizAR => CoreProverKind::MizAR, + ProverKind::GPUVerify => CoreProverKind::GPUVerify, + ProverKind::Faial => CoreProverKind::Faial, + ProverKind::Leo3 => CoreProverKind::Leo3, + ProverKind::Satallax => CoreProverKind::Satallax, + ProverKind::Lash => CoreProverKind::Lash, + ProverKind::AgsyHOL => CoreProverKind::AgsyHOL, + ProverKind::IProver => CoreProverKind::IProver, + ProverKind::Princess => CoreProverKind::Princess, + ProverKind::Twee => CoreProverKind::Twee, + ProverKind::MetiTarski => CoreProverKind::MetiTarski, + ProverKind::CSI => CoreProverKind::CSI, + ProverKind::AProVE => CoreProverKind::AProVE, + ProverKind::GNATprove => CoreProverKind::GNATprove, + ProverKind::Stainless => CoreProverKind::Stainless, + ProverKind::LiquidHaskell => CoreProverKind::LiquidHaskell, + ProverKind::KeYmaeraX => CoreProverKind::KeYmaeraX, + ProverKind::Qepcad => CoreProverKind::Qepcad, + ProverKind::Redlog => CoreProverKind::Redlog, + ProverKind::MleanCoP => CoreProverKind::MleanCoP, + ProverKind::IleanCoP => CoreProverKind::IleanCoP, + ProverKind::NanoCoP => CoreProverKind::NanoCoP, + ProverKind::MetTeL2 => CoreProverKind::MetTeL2, + ProverKind::ELK => CoreProverKind::ELK, + ProverKind::Konclude => CoreProverKind::Konclude, + ProverKind::Storm => CoreProverKind::Storm, + ProverKind::ProB => CoreProverKind::ProB, + ProverKind::EasyCrypt => CoreProverKind::EasyCrypt, + ProverKind::CryptoVerif => CoreProverKind::CryptoVerif, } } diff --git a/src/rust/agent/swarm.rs b/src/rust/agent/swarm.rs index 80640ac..aa4caab 100644 --- a/src/rust/agent/swarm.rs +++ b/src/rust/agent/swarm.rs @@ -34,7 +34,7 @@ use serde::{Deserialize, Serialize}; use tokio::sync::{mpsc, Mutex}; use tokio::task::JoinSet; -use crate::learning::design_search::{AnnealConfig, AnnealResult, DesignProblem}; +use crate::learning::design_search::{AnnealConfig, DesignProblem}; /// Configuration for a swarm run. #[derive(Debug, Clone, Serialize, Deserialize)] @@ -152,6 +152,7 @@ fn delta_scalar(from: &[i64], to: &[i64]) -> f64 { /// Run a swarm over `problem`. Returns the global best across agents /// plus per-agent reports. +#[allow(clippy::type_complexity, clippy::needless_range_loop)] pub async fn run_swarm

(problem: Arc

, config: SwarmConfig) -> SwarmResult where P: DesignProblem + Send + Sync + 'static, diff --git a/src/rust/coprocessor/audio.rs b/src/rust/coprocessor/audio.rs index aef39b1..72f83a0 100644 --- a/src/rust/coprocessor/audio.rs +++ b/src/rust/coprocessor/audio.rs @@ -80,7 +80,7 @@ fn dispatch_sync(op: CoprocessorOp) -> Result { duration_ms, sample_rate, } => { - if sample_rate < 8_000 || sample_rate > 192_000 { + if !(8_000..=192_000).contains(&sample_rate) { return Ok(CoprocessorOutcome::Failure(format!( "AudioSineWave: sample_rate {} outside [8000, 192000]", sample_rate @@ -97,7 +97,7 @@ fn dispatch_sync(op: CoprocessorOp) -> Result { CoprocessorOutcome::Hex(hex(&wav_pack(&pcm, sample_rate))) } CoprocessorOp::AudioCompletionChime { sample_rate } => { - if sample_rate < 8_000 || sample_rate > 192_000 { + if !(8_000..=192_000).contains(&sample_rate) { return Ok(CoprocessorOutcome::Failure(format!( "AudioCompletionChime: sample_rate {} outside [8000, 192000]", sample_rate diff --git a/src/rust/coprocessor/fpga.rs b/src/rust/coprocessor/fpga.rs index ee1726f..d9313a8 100644 --- a/src/rust/coprocessor/fpga.rs +++ b/src/rust/coprocessor/fpga.rs @@ -13,7 +13,7 @@ //! `yosys -p "synth -top " `, and returns the netlist //! output. Fail with a clear diagnostic if yosys is not on PATH. -use anyhow::{anyhow, Result}; +use anyhow::Result; use async_trait::async_trait; use std::io::Write; use std::process::Stdio; diff --git a/src/rust/coprocessor/io.rs b/src/rust/coprocessor/io.rs index 50c54a2..219785a 100644 --- a/src/rust/coprocessor/io.rs +++ b/src/rust/coprocessor/io.rs @@ -13,7 +13,7 @@ //! Path arguments are passed verbatim — caller is responsible for any path //! sanitisation (the prover-side trust pipeline does this before dispatch). -use anyhow::{anyhow, Result}; +use anyhow::Result; use async_trait::async_trait; use sha2::{Digest, Sha256}; use tokio::fs; diff --git a/src/rust/coprocessor/math.rs b/src/rust/coprocessor/math.rs index 4879b99..fed28b2 100644 --- a/src/rust/coprocessor/math.rs +++ b/src/rust/coprocessor/math.rs @@ -391,7 +391,7 @@ 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 % 2 == 0 { + if n.is_multiple_of(2) { (c, d) } else { let e = &c + &d; diff --git a/src/rust/coprocessor/physics.rs b/src/rust/coprocessor/physics.rs index a51fe6a..7ce0859 100644 --- a/src/rust/coprocessor/physics.rs +++ b/src/rust/coprocessor/physics.rs @@ -129,7 +129,9 @@ fn rk4_step(kernel: &str, params: &[f64], x: &[f64], dt: f64) -> std::result::Re Ok(next) } -fn build_kernel(name: &str, params: &[f64]) -> std::result::Result Vec>, String> { +type KernelFn = Box Vec>; + +fn build_kernel(name: &str, params: &[f64]) -> std::result::Result { match name { "harmonic-oscillator" => { if params.len() != 1 { diff --git a/src/rust/coprocessor/singular.rs b/src/rust/coprocessor/singular.rs index c71d1cb..54b8608 100644 --- a/src/rust/coprocessor/singular.rs +++ b/src/rust/coprocessor/singular.rs @@ -104,7 +104,7 @@ fn extract_generators(output: &str, ideal_name: &str) -> Vec { .filter_map(|line| { let line = line.trim(); if line.starts_with(&prefix) { - line.splitn(2, '=').nth(1).map(|s| s.to_string()) + line.split_once('=').map(|x| x.1).map(|s| s.to_string()) } else { None } diff --git a/src/rust/corpus/agda.rs b/src/rust/corpus/agda.rs index 4714ec6..bc82edc 100644 --- a/src/rust/corpus/agda.rs +++ b/src/rust/corpus/agda.rs @@ -24,7 +24,7 @@ #![allow(dead_code)] -use std::collections::{HashMap, HashSet}; +use std::collections::HashSet; use std::path::{Path, PathBuf}; use anyhow::{Context, Result}; diff --git a/src/rust/corpus/coq.rs b/src/rust/corpus/coq.rs index 4ed6844..2397234 100644 --- a/src/rust/corpus/coq.rs +++ b/src/rust/corpus/coq.rs @@ -561,7 +561,7 @@ fn top_level_colon(s: &str) -> Option { '}' => depth_brace -= 1, ':' if depth_paren == 0 && depth_bracket == 0 && depth_brace == 0 => { // Skip `::` (Coq has it for cons in some scopes). - let mut next_idx = i + ':'.len_utf8(); + let next_idx = i + ':'.len_utf8(); if next_idx < s.len() && s[next_idx..].starts_with(':') { continue; } @@ -569,7 +569,6 @@ fn top_level_colon(s: &str) -> Option { if next_idx < s.len() && s[next_idx..].starts_with('=') { continue; } - let _ = next_idx; return Some(i); } _ => {} diff --git a/src/rust/corpus/metrics.rs b/src/rust/corpus/metrics.rs index 951c8b3..843b8c5 100644 --- a/src/rust/corpus/metrics.rs +++ b/src/rust/corpus/metrics.rs @@ -11,15 +11,15 @@ //! //! Metric families: //! -//! * **Size**: statement token count, proof token count, -//! declaration line count +//! * **Size**: statement token count, proof token count, +//! declaration line count //! * **Connectivity**: forward fan-out (dep count), reverse fan-in -//! (dependents count), proof-depth -//! * **Shape**: recursive vs structural (heuristic from proof -//! body), pattern-match clauses count, has-where -//! * **Hazards**: one float per hazard class (0.0 / 1.0) -//! * **K-elim**: heuristic for `--without-K` violations -//! (Agda: indices unification on data ctors) +//! (dependents count), proof-depth +//! * **Shape**: recursive vs structural (heuristic from proof +//! body), pattern-match clauses count, has-where +//! * **Hazards**: one float per hazard class (0.0 / 1.0) +//! * **K-elim**: heuristic for `--without-K` violations +//! (Agda: indices unification on data ctors) //! //! All metrics are **derivable from the parsed corpus** without //! re-reading source files. They're computed in `Corpus::compute_metrics` @@ -31,7 +31,7 @@ use std::collections::HashMap; use serde::{Deserialize, Serialize}; -use super::{Corpus, CorpusEntry, DeclKind}; +use super::{Corpus, DeclKind}; /// Fixed-shape metrics tensor per entry. #[derive(Debug, Clone, Default, Serialize, Deserialize)] @@ -135,6 +135,7 @@ impl Corpus { } } +#[allow(clippy::field_reassign_with_default)] fn metrics_for( corpus: &Corpus, idx: usize, @@ -305,7 +306,7 @@ fn compute_proof_depth( #[cfg(test)] mod tests { use super::*; - use crate::corpus::{AxiomUsage, ModuleEntry}; + use crate::corpus::{AxiomUsage, CorpusEntry, ModuleEntry}; use std::path::PathBuf; fn three_entry_corpus() -> Corpus { diff --git a/src/rust/corpus/mod.rs b/src/rust/corpus/mod.rs index b3b673e..be4e82e 100644 --- a/src/rust/corpus/mod.rs +++ b/src/rust/corpus/mod.rs @@ -300,6 +300,7 @@ impl Corpus { } /// Summary counts. + #[allow(clippy::field_reassign_with_default)] pub fn stats(&self) -> CorpusStats { let mut stats = CorpusStats::default(); stats.modules = self.modules.len(); diff --git a/src/rust/diagnostics/corpus_monitor.rs b/src/rust/diagnostics/corpus_monitor.rs index 557b714..b9851a0 100644 --- a/src/rust/diagnostics/corpus_monitor.rs +++ b/src/rust/diagnostics/corpus_monitor.rs @@ -77,25 +77,23 @@ impl CorpusMonitor { // Scan for premises_*.jsonl files match fs::read_dir(path) { Ok(entries) => { - for entry in entries { - if let Ok(entry) = entry { - let path = entry.path(); - let filename = path - .file_name() - .and_then(|n| n.to_str()) - .unwrap_or(""); - - if filename.starts_with("premises_") && filename.ends_with(".jsonl") { - if let Ok(metadata) = fs::metadata(&path) { - total_size_bytes += metadata.len(); - - // Count lines (proofs) in the file - if let Ok(content) = fs::read_to_string(&path) { - let line_count = content.lines().count(); - total_proofs += line_count; - // Estimate premises as 2-3 per proof on average - total_premises += line_count * 2; - } + for entry in entries.flatten() { + let path = entry.path(); + let filename = path + .file_name() + .and_then(|n| n.to_str()) + .unwrap_or(""); + + if filename.starts_with("premises_") && filename.ends_with(".jsonl") { + if let Ok(metadata) = fs::metadata(&path) { + total_size_bytes += metadata.len(); + + // Count lines (proofs) in the file + if let Ok(content) = fs::read_to_string(&path) { + let line_count = content.lines().count(); + total_proofs += line_count; + // Estimate premises as 2-3 per proof on average + total_premises += line_count * 2; } } } diff --git a/src/rust/diagnostics/fallback_monitor.rs b/src/rust/diagnostics/fallback_monitor.rs index 8d0793d..e92f076 100644 --- a/src/rust/diagnostics/fallback_monitor.rs +++ b/src/rust/diagnostics/fallback_monitor.rs @@ -77,7 +77,7 @@ impl FallbackMonitor { self.cache_hits += 1; } - if invocation.met_sla == false { + if !invocation.met_sla { self.sla_violations += 1; } diff --git a/src/rust/diagnostics/gnn_training.rs b/src/rust/diagnostics/gnn_training.rs index 4dc5290..cf194e4 100644 --- a/src/rust/diagnostics/gnn_training.rs +++ b/src/rust/diagnostics/gnn_training.rs @@ -6,7 +6,11 @@ use std::fs; use std::path::Path; use chrono::{DateTime, Utc}; -/// Metrics exported from GNN training pipeline +/// Metrics exported from GNN training pipeline. +// +// Field names match the JSON keys produced by `src/julia/train_and_evaluate.jl` +// (`"nDCG"`, `"MRR"`) — standard learning-to-rank acronyms. +#[allow(non_snake_case)] #[derive(Debug, Clone, Serialize, Deserialize)] pub struct GnnTrainingMetrics { pub timestamp: String, diff --git a/src/rust/diagnostics/health.rs b/src/rust/diagnostics/health.rs index b9fea11..8020ed1 100644 --- a/src/rust/diagnostics/health.rs +++ b/src/rust/diagnostics/health.rs @@ -52,6 +52,12 @@ impl From for CircuitBreakerStateSnapshot { } /// Health of GNN model +// +// Field names use ML metric acronyms (nDCG, MRR) intentionally — these match +// the JSON keys emitted by the Julia training pipeline (see +// `src/julia/train_and_evaluate.jl`) and are the conventional spellings in +// learning-to-rank literature. +#[allow(non_snake_case)] #[derive(Debug, Clone, Serialize, Deserialize)] pub struct ModelHealth { pub is_loaded: bool, diff --git a/src/rust/diagnostics/proof_failure.rs b/src/rust/diagnostics/proof_failure.rs index d33851e..f7bc9d1 100644 --- a/src/rust/diagnostics/proof_failure.rs +++ b/src/rust/diagnostics/proof_failure.rs @@ -344,11 +344,10 @@ fn diagnose_z3(output: &str) -> FailureKind { }; } // Timeout - if output.contains("timeout") || output.contains("unknown") { - if output.trim() == "unknown" || output.lines().any(|l| l.trim() == "unknown") { + if (output.contains("timeout") || output.contains("unknown")) + && (output.trim() == "unknown" || output.lines().any(|l| l.trim() == "unknown")) { return FailureKind::Timeout { limit_secs: None }; } - } // Satisfiable (not a proof) if output.lines().any(|l| l.trim() == "sat") { let model = output @@ -574,10 +573,10 @@ fn explain_and_suggest(prover: ProverKind, kind: &FailureKind) -> (String, Vec ( format!( - "ECHIDNA expected the {} output to match '{}', but saw '{}...' instead. \ + "ECHIDNA expected the {:?} output to match '{}', but saw '{}...' instead. \ This typically means ECHIDNA's backend parser does not recognise \ the prover's actual output format.", - format!("{:?}", prover), expected_pattern, + prover, expected_pattern, actual_prefix.chars().take(60).collect::() ), vec![ @@ -820,8 +819,8 @@ fn extract_lean4_location(output: &str) -> Option { // Lean 4: "foo/Bar.lean:12:5: error: ..." for line in output.lines() { let parts: Vec<&str> = line.splitn(4, ':').collect(); - if parts.len() >= 3 { - if parts[0].ends_with(".lean") { + if parts.len() >= 3 + && parts[0].ends_with(".lean") { let lineno = parts[1].parse().ok(); let colno = parts[2].parse().ok(); return Some(SourceLocation { @@ -830,7 +829,6 @@ fn extract_lean4_location(output: &str) -> Option { column: colno, }); } - } } None } @@ -841,7 +839,7 @@ fn extract_idris2_location(output: &str) -> Option { let parts: Vec<&str> = line.splitn(4, ':').collect(); if parts.len() >= 3 && parts[0].ends_with(".idr") { let lineno = parts[1].parse().ok(); - let colno = parts[2].trim_start().split_whitespace().next().and_then(|s| s.parse().ok()); + let colno = parts[2].split_whitespace().next().and_then(|s| s.parse().ok()); return Some(SourceLocation { file: Some(parts[0].to_string()), line: lineno, @@ -860,7 +858,7 @@ fn first_n(s: &str, n: usize) -> String { s.chars().take(n).collect() } -fn extract_line_containing<'a>(output: &'a str, needle: &str) -> Option { +fn extract_line_containing(output: &str, needle: &str) -> Option { output .lines() .find(|l| l.contains(needle)) @@ -877,11 +875,8 @@ mod tests { #[test] fn test_diagnose_eprover_parse_mismatch() { - // Simulate the old bug where ECHIDNA checked '#' but EProver emits '%' - let output = "% Proof found!\n% SZS status Unsatisfiable\n"; - // The fixed parser correctly identifies this as a success, so if diagnose - // is called it means the verify path failed for another reason. - // For the bug case, simulate raw output that used '#' + // Simulate the old bug where ECHIDNA checked '#' but EProver emits '%'. + // For the bug case, simulate raw output that used '#'. let buggy_output = "# Proof found!\n# SZS status Unsatisfiable\n"; let report = diagnose(ProverKind::EProver, buggy_output); // The buggy output doesn't have '%' so it hits the BackendBug branch diff --git a/src/rust/dispatch.rs b/src/rust/dispatch.rs index fc6b005..a7de681 100644 --- a/src/rust/dispatch.rs +++ b/src/rust/dispatch.rs @@ -739,18 +739,21 @@ impl ProverDispatcher { _ => 0, // ReadOnly / Minimal already returned above }; - let health = self.health_status.lock().unwrap(); - let available_cross_checkers: Vec = additional_provers - .iter() - .filter(|p| { - let prover_name = format!("{:?}", p); - health.prover_health.get(&prover_name) - .map_or(true, |h| h.is_available) - }) - .take(max_cross_checkers) - .copied() - .collect(); - drop(health); + let available_cross_checkers: Vec = { + let health = self.health_status.lock().unwrap(); + additional_provers + .iter() + .filter(|p| { + let prover_name = format!("{p:?}"); + health + .prover_health + .get(&prover_name) + .is_none_or(|h| h.is_available) + }) + .take(max_cross_checkers) + .copied() + .collect() + }; // Run additional provers for cross-checking let mut all_agree = primary_result.verified; diff --git a/src/rust/fault_tolerance/resilience.rs b/src/rust/fault_tolerance/resilience.rs index 35d167b..9039d43 100644 --- a/src/rust/fault_tolerance/resilience.rs +++ b/src/rust/fault_tolerance/resilience.rs @@ -178,6 +178,11 @@ impl CircuitBreaker { *self.state.lock().unwrap() } + /// Identifier for this breaker (typically the prover/backend name). + pub fn name(&self) -> &str { + &self.name + } + pub fn failure_count(&self) -> u32 { self.failure_count.load(Ordering::SeqCst) } @@ -298,6 +303,11 @@ impl Bulkhead { self.current_permits.load(Ordering::SeqCst) } + /// Configuration this bulkhead was constructed with. + pub fn config(&self) -> &BulkheadConfig { + &self.config + } + pub fn is_available(&self) -> bool { self.available_permits() > 0 } diff --git a/src/rust/gnn/fallback_monitor.rs b/src/rust/gnn/fallback_monitor.rs index 4376c9f..1db9025 100644 --- a/src/rust/gnn/fallback_monitor.rs +++ b/src/rust/gnn/fallback_monitor.rs @@ -3,7 +3,6 @@ use serde::{Deserialize, Serialize}; use std::sync::{Arc, Mutex}; -use std::time::Instant; /// Configuration for fallback SLA monitoring #[derive(Debug, Clone, Serialize, Deserialize)] @@ -105,8 +104,7 @@ impl FallbackMonitor { if let Ok(mut metrics) = self.metrics.lock() { metrics.total_invocations += 1; - // Update latency statistics (exponential moving average) - let ema_weight = 0.2; // Weight for new value + // Update latency statistics (cumulative arithmetic mean over all invocations) let invocations = metrics.total_invocations as f64; metrics.avg_latency_ms = (metrics.avg_latency_ms * (invocations - 1.0) + latency_ms as f64) diff --git a/src/rust/learning/buchholz_rank.rs b/src/rust/learning/buchholz_rank.rs index 18454b3..c6461cc 100644 --- a/src/rust/learning/buchholz_rank.rs +++ b/src/rust/learning/buchholz_rank.rs @@ -25,7 +25,7 @@ //! capability gap) //! * **bpsi** — how to rank `bpsi ν α`: //! - PsiRank: `psi-rank ν (rank α)` (the existing -//! `osuc (ω-rank ν ⊕ rank α)`) +//! `osuc (ω-rank ν ⊕ rank α)`) //! - PsiRankPlain: `ω-rank ν ⊕ rank α` //! - OsucOmegaPlus: `osuc (ω-rank ν) ⊕ rank α` //! * **bOmega** — how to rank `bOmega ν`: diff --git a/src/rust/learning/daemon.rs b/src/rust/learning/daemon.rs index c1fb3aa..6401e48 100644 --- a/src/rust/learning/daemon.rs +++ b/src/rust/learning/daemon.rs @@ -145,9 +145,11 @@ impl Daemon { }); if outcome.proof_found { - let mut fresh = ProofState::default(); - fresh.goals = chosen.state.goals.clone(); - fresh.proof_script = outcome.best_script.clone(); + let fresh = ProofState { + goals: chosen.state.goals.clone(), + proof_script: outcome.best_script.clone(), + ..ProofState::default() + }; let variants = self.generator.emit_variants(&fresh); self.push_variants(variants); } diff --git a/src/rust/learning/design_search.rs b/src/rust/learning/design_search.rs index 563d7dd..b81e3ef 100644 --- a/src/rust/learning/design_search.rs +++ b/src/rust/learning/design_search.rs @@ -435,6 +435,7 @@ pub mod brouwer { /// - `LimBelow`: requires `∀ k. f k ≤ osuc (olim f)` (which we /// can produce), but that gives `olim f ≤ osuc (olim f)`, not /// `osuc x ≤ osuc (olim f)`. We've lost the link to `x`. + /// /// `LimBelow` is useful for *other* lemmas, but not this one. fn mono_osuc_ok(s: &LeqState) -> bool { if s.ctors.contains(&Ctor::CongSuc) { @@ -455,6 +456,7 @@ pub mod brouwer { /// available; even `CongSuc` alone is insufficient because /// the `olim f ⊕ -` case has the same `≤-lim` blocker as /// `osuc-mono-≤`. + /// /// Hand-trace omitted; same shape as `mono_osuc_ok`. `CongSuc` /// alone does NOT unblock `⊕-mono-≤-right`. fn mono_oplus_right_ok(s: &LeqState) -> bool { diff --git a/src/rust/main.rs b/src/rust/main.rs index 7e5bd21..2a1a4f9 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -489,6 +489,7 @@ fn init_tracing(verbose: bool) { } /// Prove command implementation +#[allow(clippy::too_many_arguments)] async fn prove_command( file: PathBuf, prover_kind: Option, diff --git a/src/rust/provers/acl2.rs b/src/rust/provers/acl2.rs index f52536f..bb9ba4c 100644 --- a/src/rust/provers/acl2.rs +++ b/src/rust/provers/acl2.rs @@ -1421,7 +1421,7 @@ impl ProverBackend for ACL2Backend { .output() .await .context("Failed to run ACL2")?; - if state.metadata.get("source_path").is_none() { + if !state.metadata.contains_key("source_path") { let _ = tokio::fs::remove_file(&path).await; } let output_str = String::from_utf8_lossy(&output.stdout); diff --git a/src/rust/provers/dafny.rs b/src/rust/provers/dafny.rs index e081724..974717c 100644 --- a/src/rust/provers/dafny.rs +++ b/src/rust/provers/dafny.rs @@ -126,7 +126,7 @@ impl DafnyBackend { let rest = &line[ensures_start + 7..].trim(); // Find the end: either ; or { or newline let goal_text = rest - .split(|c| c == ';' || c == '{' || c == '\n') + .split([';', '{', '\n']) .next() .unwrap_or(rest) .trim(); diff --git a/src/rust/provers/liquid_haskell.rs b/src/rust/provers/liquid_haskell.rs index 9ae8826..5cf13cc 100644 --- a/src/rust/provers/liquid_haskell.rs +++ b/src/rust/provers/liquid_haskell.rs @@ -43,8 +43,8 @@ impl LiquidHaskellBackend { if let Some(g) = state.goals.first() { let cond = self.term_to_haskell_expr(&g.target); - s.push_str(&format!("{{-@ goal :: {{ v: Bool | v == True }} @-}}\n")); - s.push_str(&format!("goal :: Bool\n")); + s.push_str("{-@ goal :: { v: Bool | v == True } @-}\n"); + s.push_str("goal :: Bool\n"); s.push_str(&format!("goal = {}\n", cond)); } diff --git a/src/rust/provers/mod.rs b/src/rust/provers/mod.rs index 30ff4ab..cad3f2b 100644 --- a/src/rust/provers/mod.rs +++ b/src/rust/provers/mod.rs @@ -642,7 +642,7 @@ impl std::str::FromStr for ProverKind { "coeffecttypechecker" | "coeffect" | "graded-context" | "coeffects" => { Ok(ProverKind::CoeffectTypeChecker) }, - "probabilistictypechecker" | "probabilistic" | "prob" | "prob-types" => { + "probabilistictypechecker" | "probabilistic" | "prob-types" => { Ok(ProverKind::ProbabilisticTypeChecker) }, "dyadictypechecker" | "dyadic" | "binary-channel" | "dyadic-session" => { diff --git a/src/rust/provers/princess.rs b/src/rust/provers/princess.rs index be4eca1..1206df2 100644 --- a/src/rust/provers/princess.rs +++ b/src/rust/provers/princess.rs @@ -152,7 +152,7 @@ impl ProverBackend for PrincessBackend { async fn verify_proof(&self, state: &ProofState) -> Result { let tptp = self.to_tptp(state)?; let mut child = Command::new(&self.config.executable) - .args(&["-inputFormat=tptp"]) + .args(["-inputFormat=tptp"]) .stdin(Stdio::piped()) .stdout(Stdio::piped()) .stderr(Stdio::piped()) diff --git a/src/rust/provers/prob.rs b/src/rust/provers/prob.rs index 0d17588..f0adf8a 100644 --- a/src/rust/provers/prob.rs +++ b/src/rust/provers/prob.rs @@ -84,10 +84,7 @@ impl ProBBackend { b.push_str("PROPERTIES\n "); let joined = state .context - .axioms - .iter() - .cloned() - .collect::>() + .axioms.to_vec() .join(" &\n "); b.push_str(&joined); b.push('\n'); diff --git a/src/rust/server.rs b/src/rust/server.rs index 4bf07c1..a98530c 100644 --- a/src/rust/server.rs +++ b/src/rust/server.rs @@ -620,12 +620,8 @@ async fn verify_raw_handler( })); } - let (ext, program, args, interpret): ( - &str, - &str, - Vec, - fn(i32, &str, &str) -> (bool, String), - ) = match req.prover { + type Interpret = fn(i32, &str, &str) -> (bool, String); + let (ext, program, args, interpret): (&str, &str, Vec, Interpret) = match req.prover { echidna::provers::ProverKind::Z3 => ( "smt2", "z3", diff --git a/src/rust/suggest/extractor.rs b/src/rust/suggest/extractor.rs index b63acb0..eaf035a 100644 --- a/src/rust/suggest/extractor.rs +++ b/src/rust/suggest/extractor.rs @@ -150,7 +150,7 @@ fn find_tactic_sites_isabelle(source: &str) -> Vec { } // rule: if let Some(rest) = line.find("rule:").map(|i| &line[i + 5..]) { - let name = rest.trim().split_whitespace().next().unwrap_or("").trim_matches(|c: char| !c.is_alphanumeric() && c != '_'); + let name = rest.split_whitespace().next().unwrap_or("").trim_matches(|c: char| !c.is_alphanumeric() && c != '_'); if !name.is_empty() { let col = line.find(name).unwrap_or(0) + 1; sites.push(TacticSite { line: line_no, col, name: name.to_string() }); @@ -209,7 +209,7 @@ fn find_tactic_sites_coq(source: &str) -> Vec { let line_no = line_idx + 1; let t = line.trim(); // Coq: bare tactic at start of line (after optional spaces/`- ` bullet) - let t_nobullet = t.trim_start_matches(|c: char| c == '-' || c == '+' || c == '*' || c == ' '); + let t_nobullet = t.trim_start_matches(['-', '+', '*', ' ']); let name = t_nobullet.split(|c: char| !c.is_alphanumeric() && c != '_').next().unwrap_or(""); if !name.is_empty() && !["Proof", "Qed", "Defined", "Admitted", "Abort", "Lemma", "Theorem"].contains(&name) { let col = line.find(name).unwrap_or(0) + 1; diff --git a/src/rust/suggest/tester.rs b/src/rust/suggest/tester.rs index 8a3d28e..822f57d 100644 --- a/src/rust/suggest/tester.rs +++ b/src/rust/suggest/tester.rs @@ -11,7 +11,7 @@ use std::time::Duration; use anyhow::Result; use tokio::task::JoinSet; -use crate::provers::{ProverBackend, ProverConfig, ProverFactory}; +use crate::provers::{ProverConfig, ProverFactory}; use crate::ProverKind; use super::variant::Variant; @@ -78,7 +78,6 @@ pub async fn test_all_variants( while pending < max_parallel { match iter.next() { Some((idx, variant)) => { - let budget = budget; set.spawn(async move { let outcome = test_single_variant(prover, &variant, budget).await; (idx, VariantResult { variant, outcome }) diff --git a/src/rust/suggest/variant.rs b/src/rust/suggest/variant.rs index d4a17bd..4ecc17f 100644 --- a/src/rust/suggest/variant.rs +++ b/src/rust/suggest/variant.rs @@ -133,7 +133,9 @@ pub fn levenshtein(a: &str, b: &str) -> u32 { if n == 0 { return m as u32; } if m == 0 { return n as u32; } let mut dp = vec![vec![0u32; m + 1]; n + 1]; + #[allow(clippy::needless_range_loop)] for i in 0..=n { dp[i][0] = i as u32; } + #[allow(clippy::needless_range_loop)] for j in 0..=m { dp[0][j] = j as u32; } for i in 1..=n { for j in 1..=m { diff --git a/tests/agentic_integration.rs b/tests/agentic_integration.rs index cb07fbb..7939bed 100644 --- a/tests/agentic_integration.rs +++ b/tests/agentic_integration.rs @@ -6,14 +6,12 @@ use echidna::agent::{ explanations::ExplanationGenerator, memory::{ProofMemory, SqliteMemory}, - meta_controller::MetaController, planner::{Planner, RulePlanner}, router::ProverRouter, AgentConfig, AgentCore, AgenticGoal, Priority, }; use echidna::core::{Goal, Term}; use echidna::provers::{ProverBackend, ProverKind}; -use std::sync::Arc; use tempfile::TempDir; /// Mock prover for testing diff --git a/tests/neural_property_tests.rs b/tests/neural_property_tests.rs index d11d3f8..b342ab1 100644 --- a/tests/neural_property_tests.rs +++ b/tests/neural_property_tests.rs @@ -13,8 +13,8 @@ mod common; -use echidna::provers::{ProverConfig, ProverFactory, ProverKind}; -use echidna::verification::axiom_tracker::{AxiomTracker, DangerLevel}; +use echidna::provers::ProverKind; +use echidna::verification::axiom_tracker::DangerLevel; use echidna::verification::confidence::{compute_trust_level, TrustFactors, TrustLevel}; use proptest::prelude::*; diff --git a/tests/p2p_property_tests.rs b/tests/p2p_property_tests.rs index 6aec319..547c49c 100644 --- a/tests/p2p_property_tests.rs +++ b/tests/p2p_property_tests.rs @@ -43,7 +43,7 @@ fn arb_term(depth: u32) -> impl Strategy { leaf, // App: func applied to 1-3 args ( - "[a-z][a-z0-9]{0,5}".prop_map(|s| Term::Const(s)), + "[a-z][a-z0-9]{0,5}".prop_map(Term::Const), prop::collection::vec(arb_term(0), 1..4), ) .prop_map(|(func, args)| Term::App { @@ -60,8 +60,8 @@ fn arb_proof_state() -> impl Strategy { |goals| { let goals = goals .into_iter() - .enumerate() - .map(|(_i, (id, target))| Goal { + + .map(|(id, target)| Goal { id, hypotheses: vec![], target, diff --git a/tests/panic_attack_props.rs b/tests/panic_attack_props.rs index 0fb444e..4b1d217 100644 --- a/tests/panic_attack_props.rs +++ b/tests/panic_attack_props.rs @@ -120,8 +120,10 @@ mod term_props { }) .collect(); let len = goals.len(); - let mut ps = ProofState::default(); - ps.goals = goals; + let ps = ProofState { + goals, + ..ProofState::default() + }; prop_assert_eq!( ps.goals.len(), len, "Expected {} goals, got {}", n, ps.goals.len() diff --git a/tests/stage1_integration_test.rs b/tests/stage1_integration_test.rs index eaddd07..b7bb20b 100644 --- a/tests/stage1_integration_test.rs +++ b/tests/stage1_integration_test.rs @@ -197,6 +197,7 @@ mod stage1_integration { // future fixture-based tests). // ───────────────────────────────────────────────────────────────────────────── #[cfg(test)] +#[allow(dead_code)] mod fixtures { pub const SIMPLE_LEAN4_PROOF: &str = r#" theorem simple_arithmetic : 2 + 2 = 4 := by