fix(ci): apply cargo fmt (Rust CI red on main) + drop stale verisim TODO note (#305)

## Summary
- Rust CI on main is red **solely** on `cargo fmt --check` (run
28736074839). This applies rustfmt output: mechanical line-wraps of the
`gnn_augment_tactics` call site across 62 prover backends plus
`src/interfaces/graphql/{resolvers,schema}.rs`.
- Removes the stale `docs/handover/TODO.md` entry claiming `--features
verisim` fails with 22 errors — `cargo check --lib --features verisim`
now compiles clean (0 errors, 6m02s). Closes #245.

## Why it matters
The L3→L1 Cap'n Proto hand-off gate (TODO.md P-gates) requires Tier-1
green on main for ≥7 days; this fmt red was blocking that clock from
starting.

## Verification
- `cargo fmt --check` clean after change
- `cargo check --lib` clean (formatting-only Rust changes)

Closes #245

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

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

Author: hyperpolymath

docs/handover/TODO.md

@@ -167,7 +167,6 @@ Existing POC: `chapel_poc/parallel_proof_search.chpl` (420 LoC) + the self-linki
 - **TypeDiscipline deep native wiring** (phase-2 deferred) — per-discipline proof encoding, Idris2 validator tagging, family-aware GNN features, per-discipline integration tests under `tests/disciplines/`, Katagoria fixture round-trip, per-discipline dispatch scoring.
 - **HP type-checker ecosystem backends** — 13 corpus-only provers (KatagoriaVerifier, Modal/Session/Choreographic/Epistemic/Refinement/Echo/Dependent/QTT/Effect-Row/Tropical/TypeLL etc.) need Rust backends shelling out to the HP stack (Ephapax, Wokelang, AffineScript) — corpus contributes to vocab/training only until backends wire up dispatch.
 - **CR-1..CR-10 cross-repo tests** from standards `TESTING-TAXONOMY.adoc` — notably CR-2 foreign-enum exhaustive-match lint, CR-3 FFI roundtrip over all variants, CR-6 upstream-HEAD sentinel.
-- **`verisim` feature compile errors** — `cargo check --lib --features verisim` fails with 22 errors (missing `warn` import, unresolved `Goal`/`theorem`, private-field access in `VeriSimDBClient`). Unrelated to main build; gate off by default.
 - **Remaining CI infra failures** — Mirror to Git Forges Radicle SSH key unset; Instant Sync `.git-private-farm` bad credentials. Tokens human-owned — see `YOUR-ACTIONS-todo.md §0c`.
 
 ## Non-goals (explicit)

src/interfaces/graphql/resolvers.rs

@@ -637,10 +637,8 @@ impl EchidnaContext {
                             .iter()
                             .filter_map(|s| {
                                 let name = s["tactic"].as_str()?;
-                                let confidence =
-                                    s["confidence"].as_f64().unwrap_or(0.5);
-                                let explanation =
-                                    s["explanation"].as_str().map(|t| t.to_string());
+                                let confidence = s["confidence"].as_f64().unwrap_or(0.5);
+                                let explanation = s["explanation"].as_str().map(|t| t.to_string());
                                 Some(crate::schema::SuggestedTactic {
                                     tactic: name.to_string(),
                                     confidence,

src/interfaces/graphql/schema.rs

@@ -483,11 +483,7 @@ impl QueryRoot {
     /// list-query for the common single-prover case. Backend construction
     /// + a `version()` probe is the strongest "available right now"
     /// signal we can give without actually dispatching a proof.
-    async fn prover_status(
-        &self,
-        _ctx: &Context<'_>,
-        prover: String,
-    ) -> Result<ProverStatusInfo> {
+    async fn prover_status(&self, _ctx: &Context<'_>, prover: String) -> Result<ProverStatusInfo> {
         let core_kind = match CoreProverKind::from_str(&prover) {
             Ok(k) => k,
             Err(e) => {
@@ -1115,7 +1111,10 @@ mod tests {
     /// `/api/verify` handler emits must map onto a distinct enum variant.
     #[test]
     fn verify_outcome_from_rest_str_covers_taxonomy() {
-        assert_eq!(VerifyOutcome::from_rest_str("PROVED"), VerifyOutcome::Proved);
+        assert_eq!(
+            VerifyOutcome::from_rest_str("PROVED"),
+            VerifyOutcome::Proved
+        );
         assert_eq!(
             VerifyOutcome::from_rest_str("NO_PROOF_FOUND"),
             VerifyOutcome::NoProofFound
@@ -1128,7 +1127,10 @@ mod tests {
             VerifyOutcome::from_rest_str("UNSUPPORTED_FEATURE"),
             VerifyOutcome::UnsupportedFeature
         );
-        assert_eq!(VerifyOutcome::from_rest_str("TIMEOUT"), VerifyOutcome::Timeout);
+        assert_eq!(
+            VerifyOutcome::from_rest_str("TIMEOUT"),
+            VerifyOutcome::Timeout
+        );
         assert_eq!(
             VerifyOutcome::from_rest_str("INCONSISTENT_PREMISES"),
             VerifyOutcome::InconsistentPremises
@@ -1142,10 +1144,7 @@ mod tests {
             VerifyOutcome::from_rest_str("WAT"),
             VerifyOutcome::SystemError
         );
-        assert_eq!(
-            VerifyOutcome::from_rest_str(""),
-            VerifyOutcome::SystemError
-        );
+        assert_eq!(VerifyOutcome::from_rest_str(""), VerifyOutcome::SystemError);
     }
 
     /// `loose_status` covers the four labels echidnabot's existing
@@ -1256,7 +1255,10 @@ mod tests {
         "#;
         let resp = schema.execute(Request::new(query)).await;
         // Unknown prover -> resolver Err -> top-level GraphQL error.
-        assert!(!resp.errors.is_empty(), "expected an error for unknown prover");
+        assert!(
+            !resp.errors.is_empty(),
+            "expected an error for unknown prover"
+        );
         assert!(resp.errors[0].message.contains("Unknown prover"));
     }
 
@@ -1328,9 +1330,16 @@ mod tests {
             }
         "#;
         let resp = schema.execute(Request::new(q)).await;
-        assert!(resp.errors.is_empty(), "introspection errors: {:?}", resp.errors);
+        assert!(
+            resp.errors.is_empty(),
+            "introspection errors: {:?}",
+            resp.errors
+        );
         let body = serde_json::to_string(&resp.data).unwrap();
-        assert!(body.contains("\"verifyProof\""), "missing verifyProof mutation");
+        assert!(
+            body.contains("\"verifyProof\""),
+            "missing verifyProof mutation"
+        );
         assert!(
             body.contains("\"suggestTactics\""),
             "missing new suggestTactics mutation"
@@ -1353,7 +1362,10 @@ mod tests {
         let resp = schema.execute(Request::new(q)).await;
         assert!(resp.errors.is_empty());
         let body = serde_json::to_string(&resp.data).unwrap();
-        assert!(body.contains("\"proverStatus\""), "missing proverStatus query");
+        assert!(
+            body.contains("\"proverStatus\""),
+            "missing proverStatus query"
+        );
         assert!(
             body.contains("\"suggestTacticsByProofId\""),
             "missing renamed suggestTacticsByProofId query"

src/rust/provers/acl2.rs

@@ -1550,7 +1550,10 @@ impl ProverBackend for ACL2Backend {
             args: vec![],
         });
 
-        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "acl2", suggestions, limit).await)
+        Ok(
+            crate::provers::gnn_augment_tactics(&self.config, state, "acl2", suggestions, limit)
+                .await,
+        )
     }
 
     async fn search_theorems(&self, pattern: &str) -> Result<Vec<String>> {

src/rust/provers/agsyhol.rs

@@ -167,7 +167,10 @@ impl ProverBackend for AgsyholBackend {
             command: "timeout".to_string(),
             args: vec![format!("{}", self.config.timeout)],
         }];
-        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "agsyhol", tactics, limit).await)
+        Ok(
+            crate::provers::gnn_augment_tactics(&self.config, state, "agsyhol", tactics, limit)
+                .await,
+        )
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/altergo.rs

@@ -238,7 +238,10 @@ impl ProverBackend for AltErgoBackend {
                 args: vec!["--sat-solver CDCL-Tableaux".to_string()],
             },
         ];
-        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "altergo", tactics, limit).await)
+        Ok(
+            crate::provers::gnn_augment_tactics(&self.config, state, "altergo", tactics, limit)
+                .await,
+        )
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/athena.rs

@@ -136,7 +136,10 @@ impl ProverBackend for AthenaBackend {
             },
             Tactic::Simplify,
         ];
-        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "athena", tactics, limit).await)
+        Ok(
+            crate::provers::gnn_augment_tactics(&self.config, state, "athena", tactics, limit)
+                .await,
+        )
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/boogie.rs

@@ -165,7 +165,10 @@ impl ProverBackend for BoogieBackend {
                 args: vec!["/proverOpt:O:smt.qi.max_multi_patterns=1000".to_string()],
             },
         ];
-        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "boogie", tactics, limit).await)
+        Ok(
+            crate::provers::gnn_augment_tactics(&self.config, state, "boogie", tactics, limit)
+                .await,
+        )
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/cadical.rs

@@ -419,7 +419,10 @@ impl ProverBackend for CaDiCaLBackend {
             Tactic::Simplify,
         ];
 
-        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "cadical", tactics, limit).await)
+        Ok(
+            crate::provers::gnn_augment_tactics(&self.config, state, "cadical", tactics, limit)
+                .await,
+        )
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/cameleer.rs

@@ -163,7 +163,10 @@ impl ProverBackend for CameleerBackend {
                 args: vec!["split_vc".to_string()],
             },
         ];
-        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "cameleer", tactics, limit).await)
+        Ok(
+            crate::provers::gnn_augment_tactics(&self.config, state, "cameleer", tactics, limit)
+                .await,
+        )
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {