feat(provers): close GNN-ranking arc — Tier-3/niche sweep (53) + doc close-out (#137)

## Summary

Closes the GNN-routing arc started in S5 (commit c8a4f25) and continued
via #135 (Tier-1 ext 5) + #136 (Tier-1 finisher 2 + Tier-2 sweep 33).
Wires the remaining **53 Tier-3 / niche / placeholder backends** that
have `suggest_tactics` impls and ships the matching doc close-out across
PROVER_COUNT.md, ROADMAP.md, and the S5 verification runbook.

After this PR (post-#136 merge / rebase), **every backend in
`ProverKind` with a `suggest_tactics` impl prepends GNN-ranked apply
tactics ahead of its heuristic hints** when the Julia `/gnn/rank`
service is reachable — and no-ops gracefully otherwise. End-state target
met for §S5.

## Coverage progression

| Session step | Wired | Notes |
|---|---|---|
| pre-session | 5 | S5 pilot: rocq, lean, agda, isabelle, z3 |
| fb3db5a (earlier) | +3 | abella, easycrypt, keymaerax |
| #135 | +5 | Tier-1 extension: idris2, fstar, cvc5, vampire, dafny |
| #136 | +35 | Tier-1 finisher (altergo, eprover) + Tier-2 sweep (33) |
| **this PR** | **+53** | Tier-3 / niche / placeholder sweep |

## Backends in this PR (53)

abc, acl2s, alloy, arend, boogie, cadical, **coq** *(separate from
rocq)*, cryptoverif, cubical_agda, dedukti, elk, faial, framac,
gnatprove, gpuverify, **hp_ecosystem** *(routes 40 HP disciplines)*,
ileancop, isabelle_zf, kissat, konclude, lambda_prolog, lean3,
liquid_haskell *(name: `liquid-haskell`)*, matita, mercury, mettel2,
minisat, mizar_ar, mleancop, nanocop, naproche, nitpick, nunchaku,
nusmv, opensmt, prism, prob, prover9, proverif, qepcad, redlog, seahorn,
smtrat, spin_checker *(name: `spin`)*, stainless, storm, tamarin, tlc,
**typed_wasm** *(routes 39 TypeChecker disciplines)*, uppaal,
uppaal_stratego, viper, zipperposition

## Doc close-out

- **`docs/PROVER_COUNT.md`**: TL;DR table updated to reflect full GNN
coverage; version-drift log adds v2.3; last-revised bumped to
2026-05-30.
- **`docs/ROADMAP.md`** §4 stage 4c: GNN-ranking surface marked
COMPLETE; §S5 status flipped to "done 2026-05-30 ✓"; "what is not
blocking" line updated.
- **`docs/handover/S5-VERIFICATION-RUNBOOK.md`**: replaces hardcoded "11
passed" with a formula tied to test-file content, so future additions
don't require a runbook edit.

## Test plan

- [x] `cargo build --lib` clean
- [x] `cargo build --tests` clean (1m 53s)
- [x] `cargo test --test gnn_augment_integration` → **64 passed; 0
failed** in 0.37s (was 11). After rebase onto post-#136 main, becomes
99.
- [ ] CI rust-ci / Live-Provers / MVP Smoke green
- [ ] Will need rebase after #136 merges (clean — independent file sets,
test-file insertion-order conflict resolves automatically)

## Follow-up

Remaining work toward genuine GNN-derived suggestions (not just
wire-format):
1. **S2 hardware training** — `just train-cpu`/`train` on the 553MB /
66,674-proof corpus to populate `models/neural/`. Owner has hardware; PC
setup pending.
2. **Native search expansion** (Stage 4d) — currently 16 of 91 backends
have native theorem search; the other 72 rely on Verisim cross-prover
fallback at the dispatcher.

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

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

Author: hyperpolymath

docs/PROVER_COUNT.md

@@ -5,7 +5,7 @@
 
 **Status**: canonical. Cite this file when documenting backend coverage in any
 other doc. Other surfaces that quoted historical counts (12, 30, 48, 105) are
-being updated to point here. Last revised: 2026-05-26.
+being updated to point here. Last revised: 2026-05-30.
 
 ## TL;DR
 
@@ -15,7 +15,8 @@ being updated to point here. Last revised: 2026-05-26.
 | External prover bindings (separate binary or library) | 89 |
 | `TypeChecker` disciplines routed via TypedWasm Sigma | 39 |
 | Exposed by default REST API (`Tier 1` / core) | **12** |
-| With real `suggest_tactics` (not stub) | 91 of 91 (5 of 91 still use heuristic only; GNN-ranked is target end-state) |
+| With real `suggest_tactics` (not stub) | **91 of 91** |
+| Routing tactic suggestions through `gnn_augment_tactics` | **all backends with `suggest_tactics`** (S5 pilot 5 + Tier-1 extension 5 + Tier-1 finisher 2 + Tier-2 sweep 33 + Tier-3/niche sweep 53 — full coverage as of 2026-05-30; gracefully no-ops when `gnn_api_url` is None or `neural_enabled` is false) |
 | With native search command | 16 of 91 (72 return `Ok(vec![])` — cross-prover search via `VeriSimAdvisor` covers them) |
 | Trust pipeline integrity-hashed | All Tier 1; Tier 2 incrementally |
 
@@ -47,6 +48,13 @@ History of the count drift:
 - v2.1 (May 2026): **105** after Wave-3 (Tamarin, ProVerif, Twelf, OR-Tools).
 - v2.2 (May 2026): **128** after 39 TypeChecker disciplines were Sigma-routed
   through TypedWasm (commit `c4bc272` and follow-on).
+- v2.3 (May 2026): same **128** declared, but `gnn_augment_tactics` now wraps
+  every backend with `suggest_tactics` (S5 pilot c8a4f25 + #135 Tier-1 extension
+  + #136 Tier-1 finisher + Tier-2 sweep + Tier-3/niche sweep). Wiring is a
+  no-op when the Julia `/gnn/rank` service is unreachable; once trained
+  weights land (`models/neural/`), every backend automatically returns
+  model-derived premise-apply tactics at the top of its `suggest_tactics`
+  list.
 
 Documents in this repo predating each milestone often quote the count current
 to their authoring date. When in doubt, **trust this file** and

docs/ROADMAP.md

@@ -69,9 +69,15 @@ Stage 3  Learning loop closes               model improves from outcomes
 Stage 4  Interaction layer honest           every declared ProverKind works
     4a  typed_wasm → crates/typed_wasm      [done 2026‑04‑22 ✓]
     4b  39 TypeChecker variant dispatch     [done 2026‑04‑22 ✓, all Sigma‑routed]
-    4c  tactic synthesis template           [91/91 real impl ✓; 5 still heuristic-only —
-                                             GNN-ranking is the end-state target;
-                                             see docs/PROVER_COUNT.md]
+    4c  tactic synthesis template           [91/91 real impl ✓; GNN-ranking surface
+                                             COMPLETE 2026‑05‑30 — every backend with
+                                             suggest_tactics now routes through
+                                             gnn_augment_tactics (S5 pilot + Tier-1
+                                             ext + Tier-1 finisher + Tier-2 sweep +
+                                             Tier-3/niche sweep). Helper no-ops when
+                                             Julia /gnn/rank is unreachable. End-state
+                                             target met; remaining S2 dependency is
+                                             real trained weights at models/neural/]
     4d  search_theorems template            [done 2026‑04‑27 ✓ — cross-prover layer
                                              added at dispatcher (CLI/REST/REPL all
                                              call `vcl_ut::cross_prover_search_names`).
@@ -139,7 +145,7 @@ and start the self‑learning loop closure.
 | S2 | 2a / 2c | Run training on the fixed corpus; record new MRR; commit `metrics_baseline.jsonl` | **Hardware / you** | gated by S1 (S1 ✓; S2 hardware step still to run) |
 | S3 | 4a / 4b | Extract `typed_wasm` to `crates/typed_wasm/`; route 39 TypeChecker variants through Sigma parameters | **Opus‑design + Sonnet‑impl** | **done 2026‑04‑22 ✓** |
 | S4 | 3a / 3b | Wire Verisim cross‑prover read paths (`goal_hash` queries + `mv_prover_success_by_class` + hypatia loop) | **Opus‑design + Sonnet‑impl** | **wired 2026‑04‑27 ✓** — read paths (`query_prover_success_by_class` via `VeriSimAdvisor`, `cross_prover_search_names` via `vcl_ut`) + write path (`spawn_record_attempt`) + end-to-end test (`tests/s4_loop_closure.rs`, `just test-s4-loop`); CI workflow filing gated on `ghcr-publish.yml` in `verisimdb` upstream (runbook holds the YAML) |
-| S5 | 4c / 4d (pilot) | Tactic synthesis template for 5 high‑value provers (coq, lean, agda, isabelle, z3) using the GNN | **Opus‑design + Sonnet‑impl** | **mostly done** — `suggest_tactics` is 91/91 real; `gnn_augment_tactics` wired into the 5 pilot backends (rocq/lean/agda/isabelle/z3) per c4bc272; remaining 5 heuristic-only backends are the GNN-ranked end-state target |
+| S5 | 4c / 4d (pilot) | Tactic synthesis template for 5 high‑value provers (coq, lean, agda, isabelle, z3) using the GNN | **Opus‑design + Sonnet‑impl** | **done 2026‑05‑30 ✓** — `suggest_tactics` is 91/91 real; `gnn_augment_tactics` wired into ALL backends with `suggest_tactics` (S5 pilot 5 in c8a4f25, Tier-1 extension 5 in #135, Tier-1 finisher 2 + Tier-2 sweep 33 in #136, Tier-3/niche sweep 53 in this PR). Wiring is a no-op when Julia /gnn/rank is unreachable; once S2 trained weights land at `models/neural/`, every backend automatically returns model-derived premise-apply tactics |
 
 After S1–S5 land, the roadmap's next sprint takes up Stage 5 (IPC +
 Chapel + Tier‑4 CI) and Stage 8 begins in parallel.
@@ -162,7 +168,9 @@ What is **not** blocking and can move now:
 - **Phase 1a** (Leo3, Satallax, Lash, AgsyHOL) — done 2026‑04‑26 ✓
 - **Phase 1b** (IProver, Princess, Twee, MetiTarski, CSI, AProVE) — done ✓
 - **S3** (typed_wasm + 39 TypeChecker Sigma routing) — done ✓
-- **`suggest_tactics`** — 86/91 real implementations; only 5 stubs left
+- **`suggest_tactics`** — 91/91 real implementations ✓; every backend now
+  routes through `gnn_augment_tactics` (no-op until S2 weights land at
+  `models/neural/`)
 
 What **is** blocking and needs Opus + cross‑repo input:
 

docs/handover/S5-VERIFICATION-RUNBOOK.md

@@ -28,17 +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), 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):
+- For every backend in `ProverKind` whose `suggest_tactics` is wired through
+  `gnn_augment_tactics` (S5 pilot 5 + Tier-1 extension 5 + Tier-1 finisher 2 +
+  Tier-2 sweep 33 + Tier-3/niche sweep 53 — full coverage as of 2026-05-30):
   `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.
+  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`.
+Expected output: `test result: ok. N passed; 0 failed` where N is
+`1 (health) + |gnn_augment_tactics call-sites|`. The exact count tracks the
+test functions in `tests/gnn_augment_integration.rs`; do not hardcode it in
+new docs.
 
 ---
 

src/rust/provers/abc.rs

@@ -740,8 +740,8 @@ impl ProverBackend for AbcBackend {
         self.to_abc_script(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![
             // PDR (IC3) — most commonly used complete verification engine
             Tactic::Custom {
                 prover: "abc".to_string(),
@@ -780,8 +780,7 @@ impl ProverBackend for AbcBackend {
             },
         ];
 
-        tactics.truncate(limit);
-        Ok(tactics)
+        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "abc", tactics, limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/acl2s.rs

@@ -125,7 +125,7 @@ impl ProverBackend for Acl2sBackend {
             .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>> {
         // ACL2s (ACL2 Sedan) is a pedagogical IDE for ACL2. Its proof strategy
         // hints are ACL2 :hints keyword arguments and defthm patterns.
         let tactics = vec![
@@ -151,7 +151,7 @@ impl ProverBackend for Acl2sBackend {
             },
             Tactic::Simplify,
         ];
-        Ok(tactics.into_iter().take(limit).collect())
+        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "acl2s", tactics, limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/alloy.rs

@@ -362,8 +362,8 @@ impl ProverBackend for AlloyBackend {
         self.to_alloy(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: "alloy".to_string(),
                 command: "add_assertion".to_string(),
@@ -381,8 +381,7 @@ impl ProverBackend for AlloyBackend {
             },
         ];
 
-        tactics.truncate(limit);
-        Ok(tactics)
+        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "alloy", tactics, limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/arend.rs

@@ -109,7 +109,7 @@ impl ProverBackend for ArendBackend {
             .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>> {
         // Arend is a proof assistant based on Homotopy Type Theory (HoTT).
         // It uses term-mode proofs with the following common combinators.
         let tactics = vec![
@@ -141,7 +141,7 @@ impl ProverBackend for ArendBackend {
             },
             Tactic::Assumption,
         ];
-        Ok(tactics.into_iter().take(limit).collect())
+        Ok(crate::provers::gnn_augment_tactics(&self.config, state, "arend", tactics, limit).await)
     }
 
     async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {

src/rust/provers/boogie.rs

@@ -133,7 +133,7 @@ impl ProverBackend for BoogieBackend {
             .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>> {
         // Boogie is an intermediate verification language; it delegates to
         // an SMT solver (typically Z3). Suggestions are annotation and
         // specification hints rather than interactive tactics.
@@ -165,7 +165,7 @@ impl ProverBackend for BoogieBackend {
                 args: vec!["/proverOpt:O:smt.qi.max_multi_patterns=1000".to_string()],
             },
         ];
-        Ok(tactics.into_iter().take(limit).collect())
+        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

@@ -399,8 +399,8 @@ impl ProverBackend for CaDiCaLBackend {
         Ok(Self::to_dimacs(num_vars, &clauses))
     }
 
-    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: "cadical".to_string(),
                 command: "add-clause".to_string(),
@@ -419,8 +419,7 @@ impl ProverBackend for CaDiCaLBackend {
             Tactic::Simplify,
         ];
 
-        tactics.truncate(limit);
-        Ok(tactics)
+        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/coq.rs

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