feat(provers): close out GNN-ranking surface — Tier-3/niche sweep (53)

This closes the GNN-routing arc started in S5 (commit c8a4f25) and
extended via #135 (Tier-1 5) + #136 (Tier-1 finisher 2 + Tier-2 33).
Every backend in `ProverKind` that has a `suggest_tactics` impl now
prepends GNN-ranked apply tactics ahead of its heuristic hints when
the Julia `/gnn/rank` service is reachable, and is a no-op otherwise.

Tier-3 / niche sweep (53 backends)
----------------------------------
abc, acl2s, alloy, arend, boogie, cadical, coq, cryptoverif,
cubical_agda, dedukti, elk, faial, framac, gnatprove, gpuverify,
hp_ecosystem, ileancop, isabelle_zf, kissat, konclude, lambda_prolog,
lean3, 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, stainless, storm, tamarin, tlc, typed_wasm, uppaal,
uppaal_stratego, viper, zipperposition

Notable:

- `coq.rs` (CoqBackend) is separate from `rocq.rs` (RocqBackend) —
  same logical prover, different files. Wired both.
- `typed_wasm.rs` is the Sigma router for the 39 TypeChecker
  disciplines; wired at the router level so all 39 dispatches benefit.
- `hp_ecosystem.rs` is the unified backend for ~40 HP type-checker
  disciplines; wired once at the router level. ProverKind dispatch
  uses TypeLL/KatagoriaVerifier — tested with TypeLL.
- `liquid_haskell.rs` uses `"liquid-haskell"` (hyphen) and
  `spin_checker.rs` uses `"spin"` for `Tactic::Custom { prover: ... }`;
  tests assert those literal strings.

Tests
-----
`tests/gnn_augment_integration.rs` extended from 11 (pre-#136) to 64
(this branch). Each test asserts the GNN helper's `Tactic::Custom`
prepend appears at index 0 of `suggest_tactics`. All 64 pass in 0.37s
against the in-process mock. After rebasing onto post-#136 main the
count will become 99 (#136 adds 35).

Doc close-out
-------------
- `docs/PROVER_COUNT.md`: TL;DR table now reflects full GNN coverage;
  version-drift log adds v2.3 entry; "Last revised" → 2026-05-30.
- `docs/ROADMAP.md` §4 stage 4c: marks GNN-ranking surface COMPLETE;
  §S5: status flipped from "mostly done" to "done 2026-05-30 ✓";
  "What is not blocking" line updated to reflect the routing
  end-state. Remaining S2 dependency is real trained weights at
  `models/neural/` — the wiring is in place to consume them.
- `docs/handover/S5-VERIFICATION-RUNBOOK.md`: replaces the hardcoded
  "11 passed" with a formula tied to the test-file content, so future
  additions don't require a runbook edit.

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>> {