feat(provers): finish T1 GNN coverage + sweep T2 (35 backends) (#136)

## Summary

Completes the Tier-1 GNN-routing surface and extends to all of Tier-2
per `docs/PROVER_COUNT.md`. Builds on #135 (which wired 5 Tier-1
backends earlier today).

| Wave | Backends | Tier |
|---|---|---|
| T1 finisher | altergo, eprover | 1 |
| T2 sweep | acl2, agsyhol, aprove, athena, cameleer, cbmc, chuffed,
csi, dreal, glpk, HOL4, hol_light, imandra, iprover, key, lash, leo3,
metamath, metitarski, minizinc, minlog, mizar, nuprl, ortools, princess,
PVS, satallax, scip, spass, tlaps, twee, twelf, why3 | 2 |

**Coverage progression**: session start 8/91 → after #135 13/91 → after
this **46/91** (all of Tier-1 + all of Tier-2).

## Notable per-backend decisions

- **6 empty-vec backends** (aprove, csi, iprover, metitarski, princess,
twee) had `_state, _limit` returning `Ok(vec![])`. Wired with empty
hints so GNN apply-tactics surface when enabled.
- **dreal** had a redundant `if !neural_enabled { return Ok(vec![]) }`
guard; removed since `gnn_augment_tactics` already gates on
`neural_enabled`.
- **5 backends** (hol4, hol_light, mizar, cbmc, dreal) had a redundant
`suggestions.truncate(limit)` before `Ok(suggestions)`; dropped since
the helper enforces `limit`.
- **HOL4 / PVS** use uppercase prover-name strings matching their
existing `Tactic::Custom { prover: ... }` usage.
- All 33 T2 files use plain `&self.config` (no sub-config wrapper).

## Test plan

- [x] `cargo build --lib` clean
- [x] `cargo build --tests` clean
- [x] `cargo test --test gnn_augment_integration` → **46 passed; 0
failed** in 0.25s (was 11)
- [x] `docs/handover/S5-VERIFICATION-RUNBOOK.md` Step 1 expected count
bumped 11 → 46
- [ ] CI rust-ci / Live-Provers / MVP Smoke green

## Follow-up

Remaining unwired: ~53 Tier-3 / Tier-4 / niche backends. `coq.rs` in
particular is unwired while `rocq.rs` is — same logical prover,
different file. Will be addressed in a follow-up sweep alongside ROADMAP
§S5 + PROVER_COUNT.md doc close-out.

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

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/handover/S5-VERIFICATION-RUNBOOK.md

@@ -28,12 +28,17 @@ Spawns an in-process mock HTTP server and asserts:
 
 - `GnnClient::health_status()` returns the richer payload (model_path, vocab_size,
   training_records_received).
-- For each of rocq, lean, agda, isabelle, z3 (the S5 pilot) plus idris2, fstar,
-  cvc5, vampire, dafny (the Tier-1 extension): `suggest_tactics` returns
-  `Tactic::Custom { command: "apply", args: ["lemma_foo"] }` as the first tactic,
-  proving the `/gnn/rank` wire format is consumed correctly by every backend.
-
-Expected output: `test result: ok. 11 passed; 0 failed`.
+- For each of rocq, lean, agda, isabelle, z3 (the S5 pilot), idris2, fstar,
+  cvc5, vampire, dafny (the Tier-1 extension), altergo, eprover (the Tier-1
+  finisher), and the 33 Tier-2 backends (acl2, agsyhol, aprove, athena,
+  cameleer, cbmc, chuffed, csi, dreal, glpk, HOL4, hol_light, imandra, iprover,
+  key, lash, leo3, metamath, metitarski, minizinc, minlog, mizar, nuprl,
+  ortools, princess, PVS, satallax, scip, spass, tlaps, twee, twelf, why3):
+  `suggest_tactics` returns `Tactic::Custom { command: "apply", args: ["lemma_foo"] }`
+  as the first tactic, proving the `/gnn/rank` wire format is consumed
+  correctly by every backend.
+
+Expected output: `test result: ok. 46 passed; 0 failed`.
 
 ---
 

src/rust/provers/acl2.rs

@@ -1550,7 +1550,7 @@ impl ProverBackend for ACL2Backend {
             args: vec![],
         });
 
-        Ok(suggestions.into_iter().take(limit).collect())
+        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

@@ -161,13 +161,13 @@ impl ProverBackend for AgsyholBackend {
         self.to_tptp(state)
     }
 
-    async fn suggest_tactics(&self, _state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
+    async fn suggest_tactics(&self, state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
         let tactics = vec![Tactic::Custom {
             prover: "agsyhol".to_string(),
             command: "timeout".to_string(),
             args: vec![format!("{}", self.config.timeout)],
         }];
-        Ok(tactics.into_iter().take(limit).collect())
+        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

@@ -212,7 +212,7 @@ impl ProverBackend for AltErgoBackend {
         self.to_altergo(state)
     }
 
-    async fn suggest_tactics(&self, _state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
+    async fn suggest_tactics(&self, state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
         // Alt-Ergo is an SMT solver; suggestions are option-level strategy hints
         // rather than interactive proof tactics.
         let tactics = vec![
@@ -238,7 +238,7 @@ impl ProverBackend for AltErgoBackend {
                 args: vec!["--sat-solver CDCL-Tableaux".to_string()],
             },
         ];
-        Ok(tactics.into_iter().take(limit).collect())
+        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/aprove.rs

@@ -168,8 +168,8 @@ impl ProverBackend for AProVEBackend {
         self.to_trs(state)
     }
 
-    async fn suggest_tactics(&self, _state: &ProofState, _limit: usize) -> Result<Vec<Tactic>> {
-        Ok(vec![])
+    async fn suggest_tactics(&self, state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
+        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "aprove", vec![], limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/athena.rs

@@ -108,7 +108,7 @@ impl ProverBackend for AthenaBackend {
             .map(String::from)
             .unwrap_or_default())
     }
-    async fn suggest_tactics(&self, _state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
+    async fn suggest_tactics(&self, state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
         // Athena is a multi-logic deduction language. Its core reasoning
         // methods map onto the following canonical proof steps.
         let tactics = vec![
@@ -136,7 +136,7 @@ impl ProverBackend for AthenaBackend {
             },
             Tactic::Simplify,
         ];
-        Ok(tactics.into_iter().take(limit).collect())
+        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/cameleer.rs

@@ -131,7 +131,7 @@ impl ProverBackend for CameleerBackend {
             .unwrap_or_default())
     }
 
-    async fn suggest_tactics(&self, _state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
+    async fn suggest_tactics(&self, state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
         // Cameleer is a deductive verification tool for OCaml programs; it
         // lowers to Why3. Suggestions are Gospel contract annotations and
         // Why3 proof hints rather than interactive proof tactics.
@@ -163,7 +163,7 @@ impl ProverBackend for CameleerBackend {
                 args: vec!["split_vc".to_string()],
             },
         ];
-        Ok(tactics.into_iter().take(limit).collect())
+        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "cameleer", tactics, limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/cbmc.rs

@@ -414,8 +414,8 @@ impl ProverBackend for CBMCBackend {
         self.to_c_source(state)
     }
 
-    async fn suggest_tactics(&self, _state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
-        let mut tactics = vec![
+    async fn suggest_tactics(&self, state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
+        let tactics = vec![
             Tactic::Custom {
                 prover: "cbmc".to_string(),
                 command: "set_unwind_bound".to_string(),
@@ -433,8 +433,7 @@ impl ProverBackend for CBMCBackend {
             },
         ];
 
-        tactics.truncate(limit);
-        Ok(tactics)
+        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "cbmc", tactics, limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/chuffed.rs

@@ -136,7 +136,7 @@ impl ProverBackend for ChuffedBackend {
     async fn export(&self, state: &ProofState) -> Result<String> {
         self.to_input_format(state)
     }
-    async fn suggest_tactics(&self, _state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
+    async fn suggest_tactics(&self, state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
         // Chuffed is a lazy-clause-generation CP solver. Suggestions are
         // MiniZinc solve annotations and propagation strategy hints.
         let tactics = vec![
@@ -162,7 +162,7 @@ impl ProverBackend for ChuffedBackend {
                 args: vec!["--prop-fifo".to_string()],
             },
         ];
-        Ok(tactics.into_iter().take(limit).collect())
+        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "chuffed", tactics, limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/csi.rs

@@ -164,11 +164,12 @@ impl ProverBackend for CSIBackend {
         self.to_trs(state)
     }
 
-    async fn suggest_tactics(&self, _state: &ProofState, _limit: usize) -> Result<Vec<Tactic>> {
+    async fn suggest_tactics(&self, state: &ProofState, limit: usize) -> Result<Vec<Tactic>> {
         // CSI is a fully automated TRS confluence/termination solver.
         // It has no user-facing tactic language — correctness certificates
-        // are produced internally. Returning empty is correct behaviour.
-        Ok(vec![])
+        // are produced internally. GNN-ranked premises (when enabled) are
+        // still surfaced as apply hints; otherwise the result is empty.
+        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "csi", vec![], limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {