style: cargo fmt (toolchain drift after 2026-07-01 re-pin) (#296)

Reformats the Rust tree with `cargo fmt` under the re-pinned toolchain
(rustc 1.95.0 / rustfmt 1.9.0), addressing the formatting drift that has
been failing the **Cargo fmt** job of Rust CI on `main` (run 28516280339
class failures) since the 2026-07-01 re-pin (#292).

Before: `cargo fmt --check` reported 129 diffs across 85 files. This PR
commits the fmt output for **21 of those 85 files** — pure
whitespace/wrapping changes, no semantic edits.

**Partial-scope caveat**: the remaining 64 files (all of
`src/rust/provers/*.rs` in the fmt set, plus
`src/interfaces/graphql/{schema,resolvers}.rs`) also have fmt drift, but
their headers carry a non-canonical owner line (`ECHIDNA Project Team`,
no `Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>`), so the repo
pre-commit licence hook rejects them. Licence-header edits are
owner-gated (per CLAUDE.md: historical drift on individual files is
owner-managed, not reconciled in routine PRs), so those files are
excluded here and the `Cargo fmt` job will remain red until their
headers are owner-reconciled (or fmt-committed by the owner). Full list
in the PR discussion below if needed; `src/rust/main.rs` was never in
the fmt set.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Author: hyperpolymath

src/rust/corpus/acl2_books.rs

@@ -320,9 +320,7 @@ fn classify_form(form: &str, line: usize, pf: &mut ParsedFile) {
     match head {
         "in-package" => {
             // (in-package "X")
-            let pkg = raw_arg1
-                .trim_matches('"')
-                .to_string();
+            let pkg = raw_arg1.trim_matches('"').to_string();
             if !pkg.is_empty() && pf.module_name.is_none() {
                 pf.module_name = Some(pkg);
             }
@@ -446,11 +444,9 @@ fn normalise_ws(s: &str) -> String {
 
 /// Tokenise on whitespace and Lisp syntactic glue.
 fn tokenise_idents(s: &str) -> Vec<&str> {
-    s.split(|c: char| {
-        c.is_whitespace() || matches!(c, '(' | ')' | '\'' | '`' | ',' | '"')
-    })
-    .filter(|t| !t.is_empty())
-    .collect()
+    s.split(|c: char| c.is_whitespace() || matches!(c, '(' | ')' | '\'' | '`' | ',' | '"'))
+        .filter(|t| !t.is_empty())
+        .collect()
 }
 
 fn flag_hazards(text: &str, hz: &mut AxiomUsage) {
@@ -565,11 +561,12 @@ mod tests {
 ";
         let pf = parse_acl2_file(src);
         assert!(pf.imports.iter().any(|i| i == "std/lists/top"));
-        assert!(pf
-            .imports
+        assert!(pf.imports.iter().any(|i| i == "arithmetic/top-with-meta"));
+        let one = pf
+            .decls
             .iter()
-            .any(|i| i == "arithmetic/top-with-meta"));
-        let one = pf.decls.iter().find(|d| d.name == "*one*").expect("defconst");
+            .find(|d| d.name == "*one*")
+            .expect("defconst");
         assert_eq!(one.kind, DeclKind::Module);
     }
 }

src/rust/corpus/dafny.rs

@@ -340,9 +340,7 @@ fn parse_dafny_file(raw: &str) -> ParsedFile {
             if let Some(after) = rest.strip_prefix(&prefix) {
                 let name = after
                     .chars()
-                    .take_while(|c| {
-                        c.is_alphanumeric() || *c == '_' || *c == '\'' || *c == '?'
-                    })
+                    .take_while(|c| c.is_alphanumeric() || *c == '_' || *c == '\'' || *c == '?')
                     .collect::<String>();
                 if name.is_empty() {
                     continue;
@@ -577,7 +575,8 @@ mod tests {
 
     #[test]
     fn detects_assume_hazard() {
-        let src = "module M {\n  lemma Sketchy()\n    ensures false\n  {\n    assume false;\n  }\n}\n";
+        let src =
+            "module M {\n  lemma Sketchy()\n    ensures false\n  {\n    assume false;\n  }\n}\n";
         let pf = parse_dafny_file(src);
         assert_eq!(pf.decls.len(), 1);
         assert_eq!(pf.decls[0].name, "Sketchy");
@@ -586,11 +585,7 @@ mod tests {
             "assume should set postulate hazard: {:?}",
             pf.decls[0].axiom_usage
         );
-        assert!(pf.decls[0]
-            .axiom_usage
-            .other
-            .iter()
-            .any(|s| s == "assume"));
+        assert!(pf.decls[0].axiom_usage.other.iter().any(|s| s == "assume"));
     }
 
     // Known heuristic-adapter limitation 2026-06-01: body-less `extern method`

src/rust/corpus/fstar.rs

@@ -545,12 +545,18 @@ type color =\n\
         let names: Vec<(&str, DeclKind)> =
             pf.decls.iter().map(|d| (d.name.as_str(), d.kind)).collect();
         assert!(
-            names.iter().any(|(n, k)| *n == "foo" && *k == DeclKind::Function),
-            "expected foo function, got {:?}", names
+            names
+                .iter()
+                .any(|(n, k)| *n == "foo" && *k == DeclKind::Function),
+            "expected foo function, got {:?}",
+            names
         );
         assert!(
-            names.iter().any(|(n, k)| *n == "color" && *k == DeclKind::Data),
-            "expected color data, got {:?}", names
+            names
+                .iter()
+                .any(|(n, k)| *n == "color" && *k == DeclKind::Data),
+            "expected color data, got {:?}",
+            names
         );
     }
 
@@ -566,11 +572,19 @@ assume Ax_no_lt : forall x. x >= 0\n\
 let cheat (x: nat) : nat = admit ()\n\
 ";
         let pf = parse_fstar_file(src);
-        let sketchy = pf.decls.iter().find(|d| d.name == "sketchy").expect("sketchy");
+        let sketchy = pf
+            .decls
+            .iter()
+            .find(|d| d.name == "sketchy")
+            .expect("sketchy");
         assert_eq!(sketchy.kind, DeclKind::Postulate);
         assert!(sketchy.axiom_usage.postulate);
 
-        let ax = pf.decls.iter().find(|d| d.name == "Ax_no_lt").expect("Ax_no_lt");
+        let ax = pf
+            .decls
+            .iter()
+            .find(|d| d.name == "Ax_no_lt")
+            .expect("Ax_no_lt");
         assert_eq!(ax.kind, DeclKind::Postulate);
         assert!(ax.axiom_usage.postulate);
 

src/rust/corpus/hol_light.rs

@@ -459,7 +459,10 @@ mod tests {
         assert_eq!(d.kind, DeclKind::Function);
         assert!(d.statement.contains("m + n"));
         let proof = d.proof.as_deref().unwrap_or("");
-        assert!(proof.contains("MESON_TAC"), "proof missing tactics: {proof}");
+        assert!(
+            proof.contains("MESON_TAC"),
+            "proof missing tactics: {proof}"
+        );
     }
 
     #[test]

src/rust/corpus/isabelle.rs

@@ -307,35 +307,31 @@ fn parse_isabelle_file(raw: &str) -> ParsedFile {
 
         match kw {
             Some(k) if is_theorem_like(k) => {
-                let (consumed, decl) =
-                    parse_theorem_like(&lines, &raw_lines, i, line_no, k);
+                let (consumed, decl) = parse_theorem_like(&lines, &raw_lines, i, line_no, k);
                 if let Some(d) = decl {
                     pf.decls.push(d);
                 }
                 i += consumed.max(1);
                 continue;
             },
             Some(k) if is_definition_like(k) => {
-                let (consumed, decl) =
-                    parse_definition_like(&lines, &raw_lines, i, line_no, k);
+                let (consumed, decl) = parse_definition_like(&lines, &raw_lines, i, line_no, k);
                 if let Some(d) = decl {
                     pf.decls.push(d);
                 }
                 i += consumed.max(1);
                 continue;
             },
             Some(k) if is_data_like(k) => {
-                let (consumed, decl) =
-                    parse_data_like(&lines, &raw_lines, i, line_no, k);
+                let (consumed, decl) = parse_data_like(&lines, &raw_lines, i, line_no, k);
                 if let Some(d) = decl {
                     pf.decls.push(d);
                 }
                 i += consumed.max(1);
                 continue;
             },
             Some("record") => {
-                let (consumed, decl) =
-                    parse_data_like(&lines, &raw_lines, i, line_no, "record");
+                let (consumed, decl) = parse_data_like(&lines, &raw_lines, i, line_no, "record");
                 if let Some(mut d) = decl {
                     d.kind = DeclKind::Record;
                     pf.decls.push(d);
@@ -344,8 +340,7 @@ fn parse_isabelle_file(raw: &str) -> ParsedFile {
                 continue;
             },
             Some(k @ ("axiomatization" | "axiom" | "consts")) => {
-                let (consumed, decl) =
-                    parse_postulate_like(&lines, &raw_lines, i, line_no, k);
+                let (consumed, decl) = parse_postulate_like(&lines, &raw_lines, i, line_no, k);
                 if let Some(d) = decl {
                     pf.decls.push(d);
                 }
@@ -357,8 +352,7 @@ fn parse_isabelle_file(raw: &str) -> ParsedFile {
                 // Module-like DeclKind for sub-entries (Module is
                 // reserved for the file-level entry), so map to
                 // Function. Document keyword in the statement.
-                let (consumed, decl) =
-                    parse_definition_like(&lines, &raw_lines, i, line_no, k);
+                let (consumed, decl) = parse_definition_like(&lines, &raw_lines, i, line_no, k);
                 if let Some(d) = decl {
                     pf.decls.push(d);
                 }
@@ -477,8 +471,8 @@ fn parse_theorem_like(
     kw: &str,
 ) -> (usize, Option<DraftDecl>) {
     let first = lines[start].trim_start();
-    let name = extract_decl_name(first, kw)
-        .unwrap_or_else(|| format!("<anonymous-{}-L{}>", kw, line_no));
+    let name =
+        extract_decl_name(first, kw).unwrap_or_else(|| format!("<anonymous-{}-L{}>", kw, line_no));
 
     // Statement: accumulate lines until we see a proof opener
     // (`proof`, `by`, `apply`, `using`, `unfolding`, `including`,

src/rust/corpus/metamath.rs

@@ -232,9 +232,7 @@ fn lex(src: &str) -> Vec<Token> {
         let is_ws = matches!(c, b' ' | b'\t' | b'\r' | b'\n');
         if is_ws {
             if let Some(s) = tok_start.take() {
-                let text = std::str::from_utf8(&bytes[s..i])
-                    .unwrap_or("")
-                    .to_string();
+                let text = std::str::from_utf8(&bytes[s..i]).unwrap_or("").to_string();
                 if !text.is_empty() {
                     out.push(Token {
                         text,
@@ -381,15 +379,18 @@ fn parse_mm_file(raw: &str) -> ParsedFile {
             }
             match kw {
                 "$c" | "$v" => {
-                    pf.options.push(format!("{}@{} {}", kw, line, payload.join(" ")));
+                    pf.options
+                        .push(format!("{}@{} {}", kw, line, payload.join(" ")));
                 },
                 "$d" => {
-                    pf.options.push(format!("$d@{} {}", line, payload.join(" ")));
+                    pf.options
+                        .push(format!("$d@{} {}", line, payload.join(" ")));
                 },
                 _ => {
                     // labelled forms reached without a preceding label
                     // (malformed); record as option for visibility.
-                    pf.options.push(format!("{}@{} (no label) {}", kw, line, payload.join(" ")));
+                    pf.options
+                        .push(format!("{}@{} (no label) {}", kw, line, payload.join(" ")));
                 },
             }
             i = j;
@@ -509,7 +510,10 @@ mod tests {
 
         let ax = pf.decls.iter().find(|d| d.name == "ax-mp").unwrap();
         assert_eq!(ax.kind, DeclKind::Postulate);
-        assert!(ax.axiom_usage.postulate, "ax-mp should be flagged as postulate");
+        assert!(
+            ax.axiom_usage.postulate,
+            "ax-mp should be flagged as postulate"
+        );
 
         let id = pf.decls.iter().find(|d| d.name == "id").unwrap();
         assert_eq!(id.kind, DeclKind::Function);
@@ -540,12 +544,7 @@ mod tests {
 
     #[test]
     fn scope_block_qualifies_label() {
-        let src = concat!(
-            "$c wff $.\n",
-            "${\n",
-            "inner $a wff bar $.\n",
-            "$}\n",
-        );
+        let src = concat!("$c wff $.\n", "${\n", "inner $a wff bar $.\n", "$}\n",);
         let pf = parse_mm_file(src);
         let inner = pf.decls.iter().find(|d| d.name == "inner").unwrap();
         assert!(

src/rust/corpus/minif2f.rs

@@ -149,7 +149,7 @@ fn opening_tokens(ext: &str) -> &'static [&'static str] {
 /// Terminator tokens that end a proof body.
 fn terminators(ext: &str) -> &'static [&'static str] {
     match ext {
-        "lean" => &[],            // blank-line terminated; no `qed`
+        "lean" => &[], // blank-line terminated; no `qed`
         "thy" => &["qed", "done", "."],
         "ml" => &[";;"],
         "mm" => &["$."],
@@ -170,7 +170,12 @@ fn match_opening<'a>(line: &'a str, ext: &str) -> Option<(usize, String)> {
             let name: String = rest
                 .chars()
                 .take_while(|c| {
-                    !c.is_whitespace() && *c != '(' && *c != ':' && *c != '{' && *c != '[' && *c != ','
+                    !c.is_whitespace()
+                        && *c != '('
+                        && *c != ':'
+                        && *c != '{'
+                        && *c != '['
+                        && *c != ','
                 })
                 .collect();
             if !name.is_empty() {
@@ -306,7 +311,8 @@ mod tests {
 
     #[test]
     fn parses_lean_mathd_theorem() {
-        let src = "theorem mathd_algebra_42 (x : \u{211d}) (h : x + 1 = 2) : x = 1 := by\n  linarith\n";
+        let src =
+            "theorem mathd_algebra_42 (x : \u{211d}) (h : x + 1 = 2) : x = 1 := by\n  linarith\n";
         let decls = parse_uniform(src, "lean");
         assert_eq!(decls.len(), 1);
         assert_eq!(decls[0].name, "mathd_algebra_42");
@@ -343,22 +349,14 @@ mod tests {
         let decls = parse_uniform(src, "v");
         assert_eq!(decls.len(), 1);
         assert_eq!(decls[0].name, "amc_1985_p10");
-        assert!(decls[0]
-            .proof
-            .as_deref()
-            .unwrap()
-            .contains("reflexivity"));
+        assert!(decls[0].proof.as_deref().unwrap().contains("reflexivity"));
     }
 
     #[test]
     fn flags_empty_body() {
         let src = "theorem mathd_empty : True\n";
         let decls = parse_uniform(src, "lean");
         assert_eq!(decls.len(), 1);
-        assert!(decls[0]
-            .axiom_usage
-            .other
-            .iter()
-            .any(|t| t == "empty_body"));
+        assert!(decls[0].axiom_usage.other.iter().any(|t| t == "empty_body"));
     }
 }