style: apply cargo fmt

Author: hyperpolymath

benches/proof_benchmarks.rs

@@ -14,9 +14,9 @@ use echidna::verification::axiom_tracker::AxiomTracker;
 use echidna::verification::confidence::{compute_trust_level, TrustFactors, TrustLevel};
 use echidna::verification::mutation::MutationTester;
 use echidna::verification::pareto::{ParetoFrontier, ProofCandidate, ProofObjective};
+use echidna::verification::portfolio::PortfolioConfidence;
 use echidna::verification::statistics::StatisticsTracker;
 use echidna::verification::DangerLevel;
-use echidna::verification::portfolio::PortfolioConfidence;
 
 use std::collections::HashMap;
 
@@ -192,7 +192,11 @@ fn bench_trust_computation(c: &mut Criterion) {
 /// Benchmark axiom danger scanning
 fn bench_axiom_scanning(c: &mut Criterion) {
     let test_contents = [
-        ("clean_lean", ProverKind::Lean, "theorem foo : True := trivial"),
+        (
+            "clean_lean",
+            ProverKind::Lean,
+            "theorem foo : True := trivial",
+        ),
         (
             "sorry_lean",
             ProverKind::Lean,
@@ -237,10 +241,7 @@ fn bench_mutation_generation(c: &mut Criterion) {
                     args: vec![
                         Term::App {
                             func: Box::new(Term::Const("add".to_string())),
-                            args: vec![
-                                Term::Var("x".to_string()),
-                                Term::Const("0".to_string()),
-                            ],
+                            args: vec![Term::Var("x".to_string()), Term::Const("0".to_string())],
                         },
                         Term::Var("x".to_string()),
                     ],
@@ -258,27 +259,23 @@ fn bench_mutation_generation(c: &mut Criterion) {
 fn bench_pareto_frontier(c: &mut Criterion) {
     let mut group = c.benchmark_group("pareto_frontier");
     for n_points in [10, 50, 100] {
-        group.bench_with_input(
-            BenchmarkId::from_parameter(n_points),
-            &n_points,
-            |b, &n| {
-                b.iter(|| {
-                    let mut candidates: Vec<ProofCandidate> = (0..n)
-                        .map(|i| ProofCandidate {
-                            id: format!("candidate_{i}"),
-                            objectives: ProofObjective {
-                                proof_time_ms: (i as u64) * 100,
-                                trust_level: TrustLevel::Level3,
-                                memory_bytes: (n as u64 - i as u64) * 1024,
-                                proof_steps: i * 5,
-                            },
-                            is_pareto_optimal: false,
-                        })
-                        .collect();
-                    black_box(ParetoFrontier::compute(&mut candidates))
-                })
-            },
-        );
+        group.bench_with_input(BenchmarkId::from_parameter(n_points), &n_points, |b, &n| {
+            b.iter(|| {
+                let mut candidates: Vec<ProofCandidate> = (0..n)
+                    .map(|i| ProofCandidate {
+                        id: format!("candidate_{i}"),
+                        objectives: ProofObjective {
+                            proof_time_ms: (i as u64) * 100,
+                            trust_level: TrustLevel::Level3,
+                            memory_bytes: (n as u64 - i as u64) * 1024,
+                            proof_steps: i * 5,
+                        },
+                        is_pareto_optimal: false,
+                    })
+                    .collect();
+                black_box(ParetoFrontier::compute(&mut candidates))
+            })
+        });
     }
     group.finish();
 }
@@ -329,11 +326,7 @@ criterion_group!(
     bench_prover_detection,
 );
 
-criterion_group!(
-    trust_benches,
-    bench_trust_computation,
-    bench_axiom_scanning,
-);
+criterion_group!(trust_benches, bench_trust_computation, bench_axiom_scanning,);
 
 criterion_group!(
     verification_benches,

benches/routing_benchmarks.rs

@@ -57,10 +57,9 @@ fn bench_routing_decision_latency(c: &mut Criterion) {
             |b, content| {
                 b.iter(|| {
                     // Deterministic hash-based prover selection — the routing hot path.
-                    let hash: usize = content
-                        .as_bytes()
-                        .iter()
-                        .fold(0usize, |acc, &byte| acc.wrapping_mul(31).wrapping_add(byte as usize));
+                    let hash: usize = content.as_bytes().iter().fold(0usize, |acc, &byte| {
+                        acc.wrapping_mul(31).wrapping_add(byte as usize)
+                    });
                     let provers = black_box(ProverKind::all());
                     let selected = provers[hash % provers.len()];
                     black_box(selected)
@@ -239,9 +238,7 @@ fn bench_agentic_config_throughput(c: &mut Criterion) {
     // Benchmark: clone from existing config.
     let base_config = AgentConfig::default();
     group.bench_function("agent_config_clone", |b| {
-        b.iter(|| {
-            black_box(base_config.clone())
-        })
+        b.iter(|| black_box(base_config.clone()))
     });
 
     // Benchmark: JSON serialisation (used for config logging and audit).

src/rust/agent/actors.rs

@@ -248,28 +248,32 @@ fn collect_lemma_candidates(term: &Term, out: &mut Vec<String>, cap: usize) {
             if !out.contains(name) {
                 out.push(name.clone());
             }
-        }
+        },
         Term::App { func, args } => {
             collect_lemma_candidates(func, out, cap);
             for a in args {
                 collect_lemma_candidates(a, out, cap);
             }
-        }
-        Term::Pi { param_type, body, .. } => {
+        },
+        Term::Pi {
+            param_type, body, ..
+        } => {
             collect_lemma_candidates(param_type, out, cap);
             collect_lemma_candidates(body, out, cap);
-        }
-        Term::Lambda { param_type, body, .. } => {
+        },
+        Term::Lambda {
+            param_type, body, ..
+        } => {
             if let Some(pt) = param_type {
                 collect_lemma_candidates(pt, out, cap);
             }
             collect_lemma_candidates(body, out, cap);
-        }
+        },
         Term::Let { value, body, .. } => {
             collect_lemma_candidates(value, out, cap);
             collect_lemma_candidates(body, out, cap);
-        }
-        _ => {}
+        },
+        _ => {},
     }
 }
 

src/rust/agent/mod.rs

@@ -376,17 +376,17 @@ impl AgentCore {
                         prover: prover_kind,
                         time_ms,
                     });
-                }
+                },
                 Ok(TacticResult::Success(new_state)) => {
                     current_state = new_state;
                     current_state.proof_script.push(tactic.clone());
-                }
+                },
                 Ok(TacticResult::Error(msg)) => {
                     debug!("Tactic {:?} rejected: {}", tactic, msg);
-                }
+                },
                 Err(e) => {
                     debug!("Backend error on tactic {:?}: {}", tactic, e);
-                }
+                },
             }
         }
 

src/rust/core.rs

@@ -150,8 +150,7 @@ impl fmt::Display for Term {
 }
 
 /// Current state of a proof
-#[derive(Debug, Clone, Serialize, Deserialize)]
-#[derive(Default)]
+#[derive(Debug, Clone, Serialize, Deserialize, Default)]
 pub struct ProofState {
     /// Current goals to prove
     pub goals: Vec<Goal>,
@@ -283,7 +282,6 @@ pub enum TacticResult {
     QED,
 }
 
-
 impl fmt::Display for Definition {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         write!(f, "{} : {} = {}", self.name, self.ty, self.body)

src/rust/disciplines/mod.rs

@@ -68,9 +68,7 @@ use crate::provers::ProverKind;
 ///
 /// Order is stable; inserting a new variant should always append, never
 /// re-order, because downstream consumers serialise by discriminant.
-#[derive(
-    Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize,
-)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize)]
 pub enum TypeDiscipline {
     // Entry points / kernels.
     TypeLl,
@@ -224,14 +222,12 @@ impl TypeDiscipline {
         match self {
             D::TypeLl | D::Katagoria => EntryPoint,
             D::Ordinary => Foundation,
-            D::Phantom | D::Polymorphic | D::Existential | D::HigherKinded | D::Row => {
-                Polymorphism
-            }
+            D::Phantom | D::Polymorphic | D::Existential | D::HigherKinded | D::Row => Polymorphism,
             D::Subtyping | D::Intersection | D::Union | D::Gradual => Subtyping,
             D::Dependent | D::Refinement | D::Hoare | D::Indexed => DependentRefinement,
             D::Qtt | D::Linear | D::Affine | D::Relevant | D::Ordered | D::Uniqueness => {
                 Substructural
-            }
+            },
             D::Immutable | D::Capability | D::Bunched => MutabilityCapability,
             D::Modal | D::Epistemic | D::Temporal | D::Provability => Modal,
             D::EffectRow | D::Impure | D::Coeffect | D::Probabilistic => EffectsCoeffects,
@@ -419,7 +415,7 @@ impl TypeDiscipline {
             // that have explicit STLC tutorials.
             D::Ordinary => {
                 vec![P::Agda, P::Coq, P::Lean, P::Isabelle, P::Idris2, P::FStar]
-            }
+            },
 
             // Polymorphism family.
             D::Polymorphic => vec![
@@ -436,9 +432,7 @@ impl TypeDiscipline {
             D::Existential => vec![P::Agda, P::Coq, P::Lean, P::Idris2, P::FStar],
             D::HigherKinded => vec![P::Agda, P::Coq, P::Lean, P::Idris2, P::FStar],
             D::Row => vec![], // Koka-native; none in echidna's classical lineup.
-            D::Phantom => vec![
-                P::Agda, P::Coq, P::Lean, P::Idris2, P::FStar, P::Dafny,
-            ],
+            D::Phantom => vec![P::Agda, P::Coq, P::Lean, P::Idris2, P::FStar, P::Dafny],
 
             // Subtyping family.
             D::Subtyping => vec![P::FStar, P::Dafny],
@@ -473,15 +467,13 @@ impl TypeDiscipline {
             // Modal family.
             D::Modal => vec![P::Isabelle], // Isabelle/ModalHOL + other instances.
             D::Epistemic => vec![], // DEL / S5 tooling lives outside echidna's current lineup.
-            D::Temporal => vec![
-                P::NuSMV, P::TLC, P::SPIN, P::UPPAAL, P::Prism, P::TLAPS,
-            ],
+            D::Temporal => vec![P::NuSMV, P::TLC, P::SPIN, P::UPPAAL, P::Prism, P::TLAPS],
             D::Provability => vec![], // GL logic, mostly research.
 
             // Effects / coeffects.
             D::EffectRow => vec![P::FStar], // F* effect algebras.
             D::Impure => vec![P::FStar, P::Dafny], // Stateful-program verifiers.
-            D::Coeffect => vec![], // Granule; not in echidna.
+            D::Coeffect => vec![],          // Granule; not in echidna.
             D::Probabilistic => vec![P::Prism, P::DReal],
 
             // Process / communication — the HP stack is specifically here
@@ -584,8 +576,7 @@ mod tests {
 
     #[test]
     fn tags_are_unique() {
-        let mut tags: Vec<&'static str> =
-            TypeDiscipline::ALL.iter().map(|d| d.tag()).collect();
+        let mut tags: Vec<&'static str> = TypeDiscipline::ALL.iter().map(|d| d.tag()).collect();
         tags.sort_unstable();
         let before = tags.len();
         tags.dedup();

src/rust/dispatch.rs

@@ -14,8 +14,8 @@ use tracing::{info, warn};
 
 use crate::integrity::solver_integrity::{IntegrityChecker, IntegrityStatus};
 use crate::llm::LlmAdvisor;
-use crate::provers::{ProverConfig, ProverFactory, ProverKind};
 use crate::provers::outcome::{classify_anyhow_error, ProverOutcome};
+use crate::provers::{ProverConfig, ProverFactory, ProverKind};
 use crate::verification::axiom_tracker::{AxiomTracker, AxiomUsage, DangerLevel};
 use crate::verification::confidence::{compute_trust_level, TrustFactors, TrustLevel};
 
@@ -256,7 +256,7 @@ impl ProverDispatcher {
                     outcome,
                     diagnostics,
                 });
-            }
+            },
         };
 
         // Step 3: Run the rich `check()` variant — gives us a full outcome
@@ -586,19 +586,14 @@ mod tests {
 
     #[test]
     fn test_prover_selection_agda() {
-        let prover = ProverDispatcher::select_prover(
-            "module MyModule where\ndata Nat : Set where",
-            None,
-        );
+        let prover =
+            ProverDispatcher::select_prover("module MyModule where\ndata Nat : Set where", None);
         assert_eq!(prover, ProverKind::Agda);
     }
 
     #[test]
     fn test_prover_selection_isabelle() {
-        let prover = ProverDispatcher::select_prover(
-            "theory MyTheory\nimports Main",
-            None,
-        );
+        let prover = ProverDispatcher::select_prover("theory MyTheory\nimports Main", None);
         assert_eq!(prover, ProverKind::Isabelle);
     }