feat(provers): extend GNN-ranking from 5 to 10 Tier-1 backends (#135)

## Summary

Extends `gnn_augment_tactics` (the S5 sprint wrapper that prepends
GNN-ranked apply tactics ahead of heuristic hints) from the 5 pilot
backends (rocq / lean / agda / isabelle / z3, commit c8a4f25) to the
remaining five **Tier-1** backends per the canonical tier table in
`docs/PROVER_COUNT.md`:

| Backend | Type | Surface |
|---|---|---|
| idris2 | interactive dependent types | uses `state.context.theorems` |
| fstar | interactive + SMT | canned tactic list |
| cvc5 | SMT | uses `self.config.base` (cvc5 wraps `ProverConfig`) |
| vampire | FOL ATP | strategy scheduling |
| dafny | auto-active verifier | shape-driven heuristics |

After this PR: **10 of 12 Tier-1 backends are GNN-routed** (altergo +
eprover remain — split into a follow-up so this PR stays atomic).

The wrapper preserves behaviour when the Julia GNN service is
unavailable (`gnn_api_url` None or `neural_enabled` false → returns raw
heuristic hints).

## Test plan

- [x] `cargo build --lib` clean
- [x] `cargo test --test gnn_augment_integration` → `11 passed; 0
failed` (was 6)
- [ ] CI rust-ci / Live-Provers / MVP Smoke green
- [ ] `docs/handover/S5-VERIFICATION-RUNBOOK.md` Step 1 manual re-run
when next reviewer touches the runbook

## ROADMAP impact

§S5 status will progress from \"mostly done — GNN wired into the 5 pilot
backends\" to \"core Tier-1 surface complete — 10 of 12 GNN-wired,
altergo + eprover queued\". Roadmap update deferred to a follow-up doc
PR to keep this one tightly scoped.

🤖 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,11 +28,12 @@ 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: `suggest_tactics` returns
+- 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. 6 passed; 0 failed`.
+Expected output: `test result: ok. 11 passed; 0 failed`.
 
 ---
 

src/rust/provers/cvc5.rs

@@ -696,7 +696,7 @@ impl ProverBackend for CVC5Backend {
         Ok(output)
     }
 
-    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 mut tactics = vec![Tactic::Custom {
             prover: "cvc5".to_string(),
             command: "check-sat".to_string(),
@@ -719,7 +719,7 @@ impl ProverBackend for CVC5Backend {
                 args: vec![],
             });
         }
-        Ok(tactics.into_iter().take(limit).collect())
+        Ok(crate::provers::gnn_augment_tactics(&self.config.base, state, "cvc5", tactics, limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/dafny.rs

@@ -329,7 +329,7 @@ impl ProverBackend for DafnyBackend {
             _ => {},
         }
 
-        Ok(suggestions.into_iter().take(limit).collect())
+        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "dafny", suggestions, limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/fstar.rs

@@ -215,7 +215,7 @@ impl ProverBackend for FStarBackend {
     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>> {
         // F* supports both a tactic DSL (Tactics monad) and SMT-backed
         // verification. The canonical first-pass tactics are listed below.
         let tactics = vec![
@@ -248,7 +248,7 @@ impl ProverBackend for FStarBackend {
             Tactic::Assumption,
             Tactic::Reflexivity,
         ];
-        Ok(tactics.into_iter().take(limit).collect())
+        Ok(super::gnn_augment_tactics(&self.config, state, "fstar", tactics, limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/idris2.rs

@@ -956,7 +956,10 @@ impl ProverBackend for Idris2Backend {
             });
         }
 
-        Ok(suggestions.into_iter().take(limit).collect())
+        Ok(
+            crate::provers::gnn_augment_tactics(&self.config, state, "idris2", suggestions, limit)
+                .await,
+        )
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/vampire.rs

@@ -236,7 +236,7 @@ impl ProverBackend for VampireBackend {
         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>> {
         // Vampire is a fully-automated first-order ATP and proof checker.
         // Suggestions are strategy and scheduling options passed to the binary.
         let tactics = vec![
@@ -267,7 +267,7 @@ impl ProverBackend for VampireBackend {
             },
             Tactic::Simplify,
         ];
-        Ok(tactics.into_iter().take(limit).collect())
+        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "vampire", tactics, limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

tests/gnn_augment_integration.rs

@@ -2,8 +2,9 @@
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 //! Integration test: mock HTTP server proves the GNN wire format works and
-//! that the 5 key backends (rocq, lean, agda, isabelle, z3) consume
-//! `/gnn/rank` and prepend model-derived apply tactics.
+//! that the 10 GNN-augmented Tier-1 backends (rocq, lean, agda, isabelle, z3
+//! from the S5 pilot, plus idris2, fstar, cvc5, vampire, dafny extending it)
+//! consume `/gnn/rank` and prepend model-derived apply tactics.
 //!
 //! No Julia installation needed — the mock server is an in-process axum
 //! server bound to a random port.  Run with:
@@ -203,3 +204,33 @@ async fn test_z3_gnn_wires_top_premise() {
     let base_url = spawn_mock_gnn_server().await;
     assert_top_tactic_is_apply(ProverKind::Z3, "z3", &base_url).await;
 }
+
+#[tokio::test]
+async fn test_idris2_gnn_wires_top_premise() {
+    let base_url = spawn_mock_gnn_server().await;
+    assert_top_tactic_is_apply(ProverKind::Idris2, "idris2", &base_url).await;
+}
+
+#[tokio::test]
+async fn test_fstar_gnn_wires_top_premise() {
+    let base_url = spawn_mock_gnn_server().await;
+    assert_top_tactic_is_apply(ProverKind::FStar, "fstar", &base_url).await;
+}
+
+#[tokio::test]
+async fn test_cvc5_gnn_wires_top_premise() {
+    let base_url = spawn_mock_gnn_server().await;
+    assert_top_tactic_is_apply(ProverKind::CVC5, "cvc5", &base_url).await;
+}
+
+#[tokio::test]
+async fn test_vampire_gnn_wires_top_premise() {
+    let base_url = spawn_mock_gnn_server().await;
+    assert_top_tactic_is_apply(ProverKind::Vampire, "vampire", &base_url).await;
+}
+
+#[tokio::test]
+async fn test_dafny_gnn_wires_top_premise() {
+    let base_url = spawn_mock_gnn_server().await;
+    assert_top_tactic_is_apply(ProverKind::Dafny, "dafny", &base_url).await;
+}