ci: infra cleanup (MSRV + julia-cache + rustdoc + fmt) (#48)

## Summary

Three-commit cleanup of pre-existing CI infrastructure debt that
surfaced while merging #47. None of these touch product logic.

- `ci(rust)`: bump MSRV `1.75 → 1.85` (Cargo.lock v4 needs ≥1.78) and
`julia-actions/cache v2 → v3.1.0` (v2 pulled in the deprecated
`actions/cache@0c45773b` and GitHub auto-fails such runs).
- `docs(rustdoc)`: fix 20 `unresolved-link` errors that `RUSTDOCFLAGS=-D
warnings` turns hard. Two patterns — math notation `k[vars]` / `w[n]` /
`set[T]` etc. escaped to `\[...\]`; bracketed code spans like ``
[`prover_kind`] `` whose target was not in scope had the brackets
dropped (kept the code span). Files in `coprocessor/`, `provers/`,
`disciplines/mod.rs`, `gnn/{client,guided_search}.rs`.
- `style`: `cargo fmt --all` (150 files). Pure formatting; reproduce
locally with `cargo fmt --all`.

## Test plan

- [ ] CI green on this branch (Rust CI Test Suite / Documentation /
Julia Integration / MSRV)
- [ ] No diff vs `cargo fmt --all` after merge
- [ ] `cargo doc --no-deps --all-features` clean with `RUSTDOCFLAGS=-D
warnings`
- [ ] Clippy still red — `cargo clippy --all-targets --all-features --
-D warnings` reports 29 errors (unused imports, dead code, idiomatic
suggestions). Left for a follow-up; surface area is wider than this PR's
scope.

Author: hyperpolymath

crates/echidna-core-spark/src/axiom_tracker.rs

@@ -78,8 +78,9 @@ use creusot_contracts::*;
 /// 3. **Reject caps at Level1** — `DangerLevel::Reject` input to
 ///    [`compute_trust_level`] always yields `Level1`.
 ///    Discharged by the `#[ensures]` on [`compute_trust_level`].
-#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
-#[derive(serde::Serialize, serde::Deserialize)]
+#[derive(
+    Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, serde::Serialize, serde::Deserialize,
+)]
 pub enum TrustLevel {
     /// Large-TCB system, unchecked result, or uses dangerous axioms.
     Level1 = 1,
@@ -134,7 +135,11 @@ impl TrustLevel {
         ensures(result == a || result == b)
     )]
     pub fn min_level(a: TrustLevel, b: TrustLevel) -> TrustLevel {
-        if a <= b { a } else { b }
+        if a <= b {
+            a
+        } else {
+            b
+        }
     }
 
     /// Returns the maximum (higher-trust) of two `TrustLevel` values.
@@ -151,7 +156,11 @@ impl TrustLevel {
         ensures(result == a || result == b)
     )]
     pub fn max_level(a: TrustLevel, b: TrustLevel) -> TrustLevel {
-        if a >= b { a } else { b }
+        if a >= b {
+            a
+        } else {
+            b
+        }
     }
 }
 
@@ -171,8 +180,7 @@ impl std::fmt::Display for TrustLevel {
 /// A deliberately minimal enum that covers the distinctions the trust
 /// algorithm cares about without pulling in the full 105-variant
 /// `ProverKind` from the main `echidna` crate.
-#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
-#[derive(serde::Serialize, serde::Deserialize)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
 pub enum ProverClass {
     /// Small-kernel proof assistant (Lean4, Coq, Isabelle, Agda, Metamath,
     /// HOLLight, HOL4, Idris2, F*, Twelf, Nuprl, Minlog).
@@ -187,8 +195,7 @@ pub enum ProverClass {
 ///
 /// This mirrors `TrustFactors` in `confidence.rs` but uses [`ProverClass`]
 /// instead of the full `ProverKind` enum, keeping the crate self-contained.
-#[derive(Debug, Clone)]
-#[derive(serde::Serialize, serde::Deserialize)]
+#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)]
 pub struct TrustFactors {
     /// Class of prover that produced the result.
     pub prover_class: ProverClass,
@@ -362,12 +369,10 @@ pub mod impl_invariants {
     // only exercised at test time — hence the allow.
     #[allow(unused_imports)]
     use crate::{
-        TrustLevel, TrustFactors, ProverClass,
-        combine_trust, clamp_trust, compute_trust_level,
-        axiom_tracker::DangerLevel,
+        axiom_tracker::DangerLevel, clamp_trust, combine_trust, compute_trust_level, ProverClass,
+        TrustFactors, TrustLevel,
     };
 
-
     // -----------------------------------------------------------------------
     // Property: TrustLevel is totally ordered (Level1 < Level2 < … < Level5)
     // -----------------------------------------------------------------------
@@ -454,7 +459,10 @@ pub mod impl_invariants {
                 for &c in &levels {
                     let lhs = combine_trust(combine_trust(a, b), c);
                     let rhs = combine_trust(a, combine_trust(b, c));
-                    assert_eq!(lhs, rhs, "combine_trust not associative for {a:?}, {b:?}, {c:?}");
+                    assert_eq!(
+                        lhs, rhs,
+                        "combine_trust not associative for {a:?}, {b:?}, {c:?}"
+                    );
                 }
             }
         }
@@ -475,7 +483,7 @@ pub mod impl_invariants {
     fn po5_reject_danger_always_level1() {
         let factors = TrustFactors {
             prover_class: ProverClass::SmallKernel,
-            confirming_provers: 10,      // maximum cross-checking
+            confirming_provers: 10, // maximum cross-checking
             has_certificate: true,
             certificate_verified: true,
             worst_axiom_danger: DangerLevel::Reject,
@@ -502,7 +510,7 @@ pub mod impl_invariants {
             has_certificate: true,
             certificate_verified: true,
             worst_axiom_danger: DangerLevel::Safe,
-            solver_integrity_ok: false,   // <-- integrity failure
+            solver_integrity_ok: false, // <-- integrity failure
         };
         assert_eq!(
             compute_trust_level(&factors),
@@ -570,7 +578,7 @@ pub mod impl_invariants {
     /// for documentation purposes).
     #[test]
     fn po9_compute_trust_level_range() {
-        use crate::axiom_tracker::DangerLevel::{Safe, Noted, Warning, Reject};
+        use crate::axiom_tracker::DangerLevel::{Noted, Reject, Safe, Warning};
         use crate::TrustLevel::{Level1, Level5};
         let danger_levels = [Safe, Noted, Warning, Reject];
         let prover_classes = [

crates/echidna-core-spark/src/lib.rs

@@ -331,9 +331,9 @@ pub fn weighted_rank(
     let score = |idx: usize| -> f64 {
         let c = &candidates[idx];
         trust_w * (c.objectives.trust_level.value() as f64)
-            - time_w  * (c.objectives.proof_time_ms as f64)
-            - mem_w   * (c.objectives.memory_bytes  as f64)
-            - steps_w * (c.objectives.proof_steps   as f64)
+            - time_w * (c.objectives.proof_time_ms as f64)
+            - mem_w * (c.objectives.memory_bytes as f64)
+            - steps_w * (c.objectives.proof_steps as f64)
     };
     let mut indices: Vec<usize> = (0..candidates.len()).collect();
     // Descending score — higher is better.
@@ -388,10 +388,7 @@ pub mod impl_invariants {
                 for &m in &[0u64, 1024, 1 << 20] {
                     for &s in &[0u64, 1, 100] {
                         let o = obj(t, lvl, m, s);
-                        assert!(
-                            !dominates(&o, &o),
-                            "dominates is not irreflexive at {o:?}"
-                        );
+                        assert!(!dominates(&o, &o), "dominates is not irreflexive at {o:?}");
                     }
                 }
             }
@@ -494,12 +491,9 @@ pub mod impl_invariants {
                 }
             }
             assert_eq!(
-                cs[i].is_pareto_optimal,
-                !dominated,
+                cs[i].is_pareto_optimal, !dominated,
                 "completeness violation at {}: optimal_flag={} but actually-dominated={}",
-                cs[i].id,
-                cs[i].is_pareto_optimal,
-                dominated
+                cs[i].id, cs[i].is_pareto_optimal, dominated
             );
         }
     }
@@ -518,8 +512,8 @@ pub mod impl_invariants {
         let n = cs.len();
         for i in 0..n {
             if !cs[i].is_pareto_optimal {
-                let has_dominator = (0..n)
-                    .any(|j| j != i && dominates(&cs[j].objectives, &cs[i].objectives));
+                let has_dominator =
+                    (0..n).any(|j| j != i && dominates(&cs[j].objectives, &cs[i].objectives));
                 assert!(
                     has_dominator,
                     "dichotomy violation at {}: not optimal but no dominator",
@@ -535,7 +529,7 @@ pub mod impl_invariants {
     fn po_p7a_best_time_on_frontier() {
         use TrustLevel::*;
         let mut cs = vec![
-            cand("fast", 10, Level1, 1_000_000, 1000),       // best time
+            cand("fast", 10, Level1, 1_000_000, 1000), // best time
             cand("trusted", 5000, Level5, 100_000, 50),
             cand("balanced", 1000, Level3, 200_000, 100),
         ];
@@ -553,7 +547,7 @@ pub mod impl_invariants {
         use TrustLevel::*;
         let mut cs = vec![
             cand("fast", 10, Level1, 1_000_000, 1000),
-            cand("trusted", 5000, Level5, 100_000, 50),     // best trust
+            cand("trusted", 5000, Level5, 100_000, 50), // best trust
             cand("balanced", 1000, Level3, 200_000, 100),
         ];
         let _frontier = compute(&mut cs);
@@ -569,7 +563,7 @@ pub mod impl_invariants {
         use TrustLevel::*;
         let mut cs = vec![
             cand("fast", 10, Level1, 1_000_000, 1000),
-            cand("lean_mem", 5000, Level3, 1, 50),           // best memory
+            cand("lean_mem", 5000, Level3, 1, 50), // best memory
             cand("balanced", 1000, Level3, 200_000, 100),
         ];
         let _frontier = compute(&mut cs);
@@ -585,7 +579,7 @@ pub mod impl_invariants {
         use TrustLevel::*;
         let mut cs = vec![
             cand("verbose", 10, Level1, 1_000_000, 1000),
-            cand("terse", 5000, Level3, 500_000, 1),         // best steps
+            cand("terse", 5000, Level3, 500_000, 1), // best steps
             cand("balanced", 1000, Level3, 200_000, 100),
         ];
         let _frontier = compute(&mut cs);
@@ -602,9 +596,9 @@ pub mod impl_invariants {
         use TrustLevel::*;
         let cs = vec![
             cand("a", 100, Level2, 100_000, 10),
-            cand("b", 200, Level5, 50_000,  5),
+            cand("b", 200, Level5, 50_000, 5),
             cand("c", 300, Level3, 200_000, 50),
-            cand("d", 50,  Level1, 10_000,  1),
+            cand("d", 50, Level1, 10_000, 1),
         ];
         let ranked = weighted_rank(&cs, 1.0, 0.001, 0.0, 0.0);
         assert_eq!(ranked.len(), cs.len(), "length must equal input length");

crates/echidna-core-spark/src/pareto.rs

@@ -176,17 +176,32 @@ pub struct Universe {
 impl Universe {
     /// Predicative cumulative `Type level`.
     pub fn ty(level: usize) -> Self {
-        Self { level, cumulative: true, impredicative: false, homotopy_level: None }
+        Self {
+            level,
+            cumulative: true,
+            impredicative: false,
+            homotopy_level: None,
+        }
     }
 
     /// Impredicative proposition universe (`Prop`).
     pub fn prop() -> Self {
-        Self { level: 0, cumulative: false, impredicative: true, homotopy_level: Some(1) }
+        Self {
+            level: 0,
+            cumulative: false,
+            impredicative: true,
+            homotopy_level: Some(1),
+        }
     }
 
     /// HoTT n-type universe at the given homotopy level.
     pub fn hott(level: usize, n: u8) -> Self {
-        Self { level, cumulative: true, impredicative: false, homotopy_level: Some(n) }
+        Self {
+            level,
+            cumulative: true,
+            impredicative: false,
+            homotopy_level: Some(n),
+        }
     }
 }
 
@@ -456,7 +471,12 @@ mod tests {
     #[test]
     fn hypothesis_with_type_info_roundtrips() {
         use crate::core::Hypothesis;
-        let h = Hypothesis { name: "h".into(), ty: Term::Const("Nat".to_string()), body: None, type_info: Some(TypeInfo::new().with_multiplicity(Multiplicity::Linear)) };
+        let h = Hypothesis {
+            name: "h".into(),
+            ty: Term::Const("Nat".to_string()),
+            body: None,
+            type_info: Some(TypeInfo::new().with_multiplicity(Multiplicity::Linear)),
+        };
         let json = serde_json::to_string(&h).expect("serialize");
         assert!(json.contains("Linear"));
         let back: Hypothesis = serde_json::from_str(&json).expect("deserialize");

crates/echidna-core/src/types.rs

@@ -136,14 +136,14 @@ impl EchidnaMcp {
                     stderr: String::new(),
                 };
                 return serde_json::to_string_pretty(&result).unwrap_or_default();
-            }
+            },
         };
 
         let stdout = String::from_utf8_lossy(&output.stdout).into_owned();
         let stderr = String::from_utf8_lossy(&output.stderr).into_owned();
 
-        let verified = stdout.contains("\"level\": \"success\"")
-            || stdout.contains("\"level\":\"success\"");
+        let verified =
+            stdout.contains("\"level\": \"success\"") || stdout.contains("\"level\":\"success\"");
         let message = extract_first_message(&stdout).unwrap_or_else(|| {
             if stderr.is_empty() {
                 "(no output)".to_string()
@@ -196,7 +196,7 @@ impl EchidnaMcp {
                     stdout.trim().to_string()
                 };
                 CheckProverResult { available, message }
-            }
+            },
             Err(e) => CheckProverResult {
                 available: false,
                 message: format!("Failed to invoke echidna: {e}"),
@@ -224,7 +224,8 @@ impl EchidnaMcp {
                     stdout
                 } else {
                     // Wrap plain-text listing as a simple result object.
-                    let lines: Vec<&str> = stdout.lines().filter(|l| !l.trim().is_empty()).collect();
+                    let lines: Vec<&str> =
+                        stdout.lines().filter(|l| !l.trim().is_empty()).collect();
                     let provers: HashMap<String, String> = lines
                         .iter()
                         .map(|l| (l.trim().to_string(), String::new()))
@@ -235,20 +236,20 @@ impl EchidnaMcp {
                     };
                     serde_json::to_string_pretty(&result).unwrap_or_default()
                 }
-            }
+            },
             Ok(output) => {
                 let stderr = String::from_utf8_lossy(&output.stderr).into_owned();
                 let result = serde_json::json!({
                     "error": format!("echidna list-provers failed: {}", stderr.trim())
                 });
                 serde_json::to_string_pretty(&result).unwrap_or_default()
-            }
+            },
             Err(e) => {
                 let result = serde_json::json!({
                     "error": format!("Failed to invoke echidna: {e}")
                 });
                 serde_json::to_string_pretty(&result).unwrap_or_default()
-            }
+            },
         }
     }
 }

crates/echidna-mcp/src/main.rs

@@ -37,9 +37,9 @@ pub mod gnn_capnp {
 
 // Ergonomic re-exports under shorter names.
 pub use common_capnp as common;
+pub use gnn_capnp as gnn;
 pub use proof_capnp as proof;
 pub use prover_capnp as prover;
-pub use gnn_capnp as gnn;
 
 #[cfg(test)]
 mod smoke {
@@ -64,7 +64,10 @@ mod smoke {
         )
         .unwrap();
         let root = reader.get_root::<proof::proof_goal::Reader>().unwrap();
-        assert_eq!(root.get_request_id().unwrap().to_str().unwrap(), "test-req-0");
+        assert_eq!(
+            root.get_request_id().unwrap().to_str().unwrap(),
+            "test-req-0"
+        );
         assert_eq!(root.get_schema_version(), 1);
         assert_eq!(root.get_timeout_ms(), 300_000);
     }

crates/echidna-wire/src/lib.rs

@@ -1009,8 +1009,11 @@ region.get Small[99] .val
         );
         let analysis = analyse(VALID_TWASM, &ti).unwrap();
         // No BoundsProof, NullSafe, EffectSafe, LifetimeSafe obligations
-        let levels: HashSet<SafetyLevel> =
-            analysis.obligations.iter().map(|o| o.level.clone()).collect();
+        let levels: HashSet<SafetyLevel> = analysis
+            .obligations
+            .iter()
+            .map(|o| o.level.clone())
+            .collect();
         assert!(!levels.contains(&SafetyLevel::BoundsProof));
         assert!(!levels.contains(&SafetyLevel::EffectSafe));
         assert!(levels.contains(&SafetyLevel::Linear));