fix: eliminate all clippy warnings and errors across entire codebase

- Mark FFI extern "C" functions as unsafe (14 errors fixed)
- Fix all 110+ clippy warnings: strip_prefix, &PathBuf→&Path,
  Default impls, field initializers, redundant closures, etc.
- Add missing ProverKind variants to test helpers (18 new backends)
- Add Criterion benchmark dependency
- Fix Coq test for missing stdlib environment
- 391 tests passing, 0 clippy warnings on --all-targets

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

Cargo.lock

@@ -89,6 +89,11 @@ proptest = "1"
 tokio-test = "0.4"
 which = "7"
 pretty_assertions = "1"
+criterion = { version = "0.5", features = ["html_reports"] }
+
+[[bench]]
+name = "proof_benchmarks"
+harness = false
 
 [workspace]
 members = [

Cargo.toml

@@ -20,7 +20,7 @@ fn bench_simple_arithmetic(c: &mut Criterion) {
 fn bench_proof_state(c: &mut Criterion) {
     c.bench_function("proof_state_creation", |b| {
         b.iter(|| {
-            let hypotheses = vec!["H1: P".to_string(), "H2: Q".to_string()];
+            let hypotheses = ["H1: P".to_string(), "H2: Q".to_string()];
             let conclusion = "P /\\ Q";
             // Simulate proof state construction
             black_box(hypotheses.len() + conclusion.len())

benches/proof_benchmarks.rs

@@ -5,7 +5,6 @@
 
 use echidna::aspect::{
     AggregationStrategy, Aspect, AspectTagger, CompositeTagger, NeuralTagger, RuleBasedTagger,
-    TheoremFeatures,
 };
 use echidna::core::Term;
 

examples/aspect_tagging_demo.rs

@@ -124,7 +124,7 @@ impl ContextAgent {
     }
 
     pub fn start_actor() -> Addr<Self> {
-        SyncArbiter::start(1, || ContextAgent::new())
+        SyncArbiter::start(1, ContextAgent::new)
     }
 }
 
@@ -184,7 +184,7 @@ impl LemmaAgent {
     }
 
     pub fn start_actor() -> Addr<Self> {
-        SyncArbiter::start(1, || LemmaAgent::new())
+        SyncArbiter::start(1, LemmaAgent::new)
     }
 }