feat(corpus): resolved & expanded training corpus (700K+ proofs) (#25)

This PR resolves the issues from the closed #23. 

Key changes:
- Fixed syntax errors in Mizar and Isabelle extraction scripts.
- Resolved ID conflicts in the Dafny corpus.
- Expanded UNIFIED training corpus to 702,099 proofs.
- Expanded model vocabulary to 141,517 terms.
- Verified with full test suite (613/613 passing).
- Cleaned git history of accidentally tracked large stale files.

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).