feat(verisim): thread obligation_class + add cross-prover search layer

Two follow-ons to the S4 write-side wiring (60d2e75):

(1) obligation_class threading
   verify_proof now delegates to a private verify_proof_with_class that
   takes Option<&str>. verify_proof_verisim_guided threads the class it
   already knows, so recorded ProofAttempt rows are attributed to the
   right obligation_class instead of "unknown" — otherwise the very MV
   `mv_prover_success_by_class` would be polluted with rows that the
   advisor itself produced.

(2) Cross-prover search layer (vcl_ut::cross_prover_search_names)
   Audit revealed the original "replace 72 search_theorems stubs"
   plan was the wrong shape: vcl_ut::execute_cross_prover already
   queries VeriSimDB's /api/v1/search/text. The 72 backends with
   `Ok(vec![])` are not stubs — they correctly report "no native
   search command" because their underlying provers don't ship one.

   Cross-prover semantics belong one layer up. Added a thin helper
   that wraps the existing executor and projects results to Vec<String>
   matching the trait shape, then wired it into the three call sites
   (CLI search command, REST /api/search, REPL :search). One query
   covers every prover that ever recorded an attempt.

   Available in default builds as a no-op stub (Ok(vec![])) so callers
   don't need their own cfg ladder.

Roadmap (docs/ROADMAP.md):
- Stage 4d marked done with rationale for keeping the per-backend stubs
- Endpoint table updated to reflect cross-prover layer
- "What is blocking" entry: Verisim schema is fixed; remaining S4 work
  is ops (CI standup + production loop observation), not design

Tests: +3 (test_verify_proof_with_class_threads_class_to_inner +
test_cross_prover_search_names_empty_pattern + _unreachable_returns_empty).
Total 905 lib tests pass with --features verisim, 872 default.

Pre-existing tests/common/mod.rs ProverConfig field rot (project_root,
sandbox) blocks integration suite and is unrelated to this change.

Author: hyperpolymath

docs/ROADMAP.md

@@ -69,7 +69,14 @@ 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           [86/91 done; 5 suggest_tactics stubs remain]
-    4d  search_theorems template            72 stubs remain, query Verisim
+    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`).
+                                             The 72 backend `Ok(vec![])` returns are
+                                             correct: they report "no native search
+                                             command" — cross-prover semantics live
+                                             one layer up where Verisim covers all
+                                             provers in one query.]
 
 Stage 5  Distributed & fast                 scale + specialised hardware
     5a  Cap'n Proto IPC                     Rust ↔ Julia, :8090
@@ -104,7 +111,7 @@ Stage 8  Self‑verified                      ECHIDNA proves ECHIDNA
 
 | Claim | Today | End‑state target |
 |---|---|---|
-| "Every important solver" | **128 ProverKind variants** (89 external prover bindings + 39 TypeChecker disciplines routed through TypedWasm); **5 `suggest_tactics` stubs**; **72 `search_theorems` stubs** | **All variants with real `suggest_tactics` (GNN‑ranked top‑k) and `search_theorems` (queries Verisim by `goal_hash`) — no `Ok(vec![])` returns anywhere** |
+| "Every important solver" | **128 ProverKind variants** (89 external prover bindings + 39 TypeChecker disciplines routed through TypedWasm); **5 `suggest_tactics` stubs**; **72 backends with empty native search but a cross-prover Verisim fallback at the dispatcher layer (CLI/REST/REPL)** | **All variants with real `suggest_tactics` (GNN‑ranked top‑k); per-backend search reflects each prover's native capability while cross-prover queries are served from Verisim by `goal_hash`** |
 | "Vocab at 2.5 M" | 255 K | **~1 M canonical tokens** after Mathport + Iris + VST + Flyspeck + HoTT absorption, with **online growth** adding tokens during training |
 | "Chapel fully supported" | 2 files, POC only | **`dispatch.rs` picks Chapel‑parallel dispatch by config**; runtime init + cancellation + error propagation wired; ≥1 OoM speedup on portfolio solves |
 | "Cap'n Proto serialisation" | 0 `.capnp` files | **`crates/echidna-wire/`** contains schemas for ProofState / Goal / Tactic / EmbeddingRequest / RankingResponse; IPC on :8090 is Cap'n Proto; JSON retained only as debug fallback |
@@ -161,8 +168,14 @@ What **is** blocking and needs Opus + cross‑repo input:
   Vec<ProofRecord>` and `async fn prover_success_by_class(class) ->
   Vec<(ProverKind, f32)>`) but the schema for `ProofRecord` and `class`
   lives in the Verisim repo and must be agreed there before echidna
-  can wire reads.
-- **`search_theorems`** — 72 stubs, all blocked behind S4 contract.
+  can wire reads. **Status as of 2026-04-27**: the Verisim schema is in
+  fact fixed (`ProofAttempt` row → ClickHouse `proof_attempts` →
+  `mv_prover_success_by_class` MV) and both echidna read paths
+  (`query_prover_success_by_class` via `VeriSimAdvisor`,
+  `cross_prover_search_names` via `vcl_ut`) and the write path
+  (`spawn_record_attempt` from dispatch exits) are now wired. Remaining
+  S4 work is ops/runtime: standing up VeriSimDB in CI and observing the
+  loop close in production.
 
 ## 5. Agent‑tier guidance
 

src/rust/dispatch.rs

@@ -350,7 +350,11 @@ impl ProverDispatcher {
         } else {
             fallback_prover
         };
-        self.verify_proof(prover, content).await
+        // Thread the class to the inner so the recorded ProofAttempt is
+        // attributed to the right obligation_class — otherwise the very
+        // statistics this dispatch consults would be polluted with
+        // "unknown" rows.
+        self.verify_proof_with_class(prover, content, Some(obligation_class)).await
     }
 
     /// Dispatch with LLM-guided optimisation
@@ -399,11 +403,32 @@ impl ProverDispatcher {
         self.verify_proof(fallback_prover, content).await
     }
 
-    /// Dispatch a proof verification request through the trust-hardening pipeline
+    /// Dispatch a proof verification request through the trust-hardening pipeline.
+    ///
+    /// Public entry point. Records dispatch attempts in VeriSimDB (when
+    /// `feature = "verisim"` and a writer is attached) with `obligation_class`
+    /// = `"unknown"`, since the public API does not carry class metadata.
+    /// Callers that *do* know the class (`verify_proof_verisim_guided`,
+    /// future LLM-guided dispatch with classification) should call
+    /// `verify_proof_with_class` directly.
     pub async fn verify_proof(
         &self,
         prover_kind: ProverKind,
         content: &str,
+    ) -> Result<DispatchResult> {
+        self.verify_proof_with_class(prover_kind, content, None).await
+    }
+
+    /// Inner dispatch implementation that takes an optional `obligation_class`
+    /// for VeriSimDB attribution. Crate-private — public callers go through
+    /// `verify_proof` (no class) or `verify_proof_verisim_guided` (class
+    /// already known).
+    pub(crate) async fn verify_proof_with_class(
+        &self,
+        prover_kind: ProverKind,
+        content: &str,
+        #[cfg_attr(not(feature = "verisim"), allow(unused_variables))]
+        obligation_class: Option<&str>,
     ) -> Result<DispatchResult> {
         let start = Instant::now();
 
@@ -442,7 +467,13 @@ impl ProverDispatcher {
                     None
                 };
                 #[cfg(feature = "verisim")]
-                self.spawn_record_attempt(prover_kind, None, &outcome, elapsed_ms, None);
+                self.spawn_record_attempt(
+                    prover_kind,
+                    None,
+                    &outcome,
+                    elapsed_ms,
+                    obligation_class,
+                );
                 return Ok(DispatchResult {
                     verified: false,
                     trust_level: TrustLevel::Level1,
@@ -559,7 +590,7 @@ impl ProverDispatcher {
             state.goals.first(),
             &outcome,
             prover_elapsed_ms,
-            None,
+            obligation_class,
         );
 
         Ok(DispatchResult {
@@ -1244,6 +1275,26 @@ mod tests {
         assert_eq!(attempt.obligation_class, "unknown");
     }
 
+    #[cfg(feature = "verisim")]
+    #[tokio::test]
+    async fn test_verify_proof_with_class_threads_class_to_inner() {
+        // The inner accepts an obligation_class which gets attributed to the
+        // ProofAttempt row. We can't observe the row without VeriSimDB, but we
+        // can confirm the call typechecks and returns Ok end-to-end.
+        let dispatcher = ProverDispatcher::new();
+        let result = dispatcher
+            .verify_proof_with_class(
+                ProverKind::Z3,
+                "(set-logic QF_LIA)\n(assert (> x 0))\n(check-sat)",
+                Some("smoke-test"),
+            )
+            .await;
+        assert!(
+            result.is_ok(),
+            "verify_proof_with_class must complete with Some(class)"
+        );
+    }
+
     #[cfg(feature = "verisim")]
     #[tokio::test]
     async fn test_verify_proof_with_unreachable_writer_still_returns_ok() {

src/rust/main.rs

@@ -458,6 +458,31 @@ async fn search_command(
         }
     }
 
+    // After per-backend search, add a cross-prover layer: query VeriSimDB
+    // for matches across every prover that has ever recorded an attempt.
+    // This compensates for backends without a native search command (the
+    // 70+ that legitimately return Vec::new() because their underlying
+    // prover doesn't ship a `Search`-equivalent). No-op without the
+    // `verisim` feature; logs and continues on Verisim outage.
+    let verisim_url = std::env::var("VERISIM_URL")
+        .unwrap_or_else(|_| "http://localhost:8080".to_string());
+    match echidna::vcl_ut::cross_prover_search_names(&verisim_url, &pattern, limit).await {
+        Ok(cross) if !cross.is_empty() => {
+            formatter.section("\nCross-prover (VeriSimDB) Results:")?;
+            total_results += cross.len();
+            for (i, result) in cross.iter().take(limit).enumerate() {
+                formatter.result(&format!("  {}. {}", i + 1, result))?;
+            }
+            if cross.len() > limit {
+                formatter.info(&format!("  ... and {} more results", cross.len() - limit))?;
+            }
+        }
+        Ok(_) => {}
+        Err(e) => {
+            warn!("Cross-prover search failed: {}", e);
+        }
+    }
+
     formatter.info(&format!("\nTotal results found: {}", total_results))?;
 
     Ok(())

src/rust/repl/proof.rs

@@ -517,7 +517,17 @@ async fn search_theorems(state: &ReplState, pattern: &str) -> Result<()> {
     println!("{}", format!("Searching for: {}", pattern).cyan());
     println!();
 
-    let results = state.prover.search_theorems(pattern).await?;
+    let mut results = state.prover.search_theorems(pattern).await?;
+
+    // Cross-prover layer: append VeriSimDB matches so backends without a
+    // native search command still surface relevant theorems. No-op in
+    // default builds (no verisim feature). Errors are silent at REPL —
+    // search is a soft query and a writer outage shouldn't kill the loop.
+    let verisim_url = std::env::var("VERISIM_URL")
+        .unwrap_or_else(|_| "http://localhost:8080".to_string());
+    if let Ok(cross) = echidna::vcl_ut::cross_prover_search_names(&verisim_url, pattern, 20).await {
+        results.extend(cross);
+    }
 
     if results.is_empty() {
         println!("  (no results)");

src/rust/vcl_ut.rs

@@ -869,6 +869,77 @@ fn octad_to_entry(octad: &OctadPayload) -> QueryResultEntry {
     }
 }
 
+// ═══════════════════════════════════════════════════════════════════════
+// Cross-prover convenience helpers — match the per-backend trait shape so
+// front-ends (CLI, REST, REPL) can append cross-prover results to the
+// per-backend aggregation without rebuilding a CrossProverQueryBuilder.
+// ═══════════════════════════════════════════════════════════════════════
+
+/// Query VeriSimDB for theorems matching a free-text pattern, across all
+/// provers, returning bare names that can be folded into a per-backend
+/// `search_theorems` aggregation.
+///
+/// Uses VeriSimDB's `/api/v1/search/text` (the same endpoint
+/// `execute_cross_prover` calls) and projects each `QueryResultEntry` to
+/// its `theorem_name`. Empty names are filtered. The query runs at
+/// `TypeLevel::Cardinality` (Level 7) so the `limit` is enforced
+/// type-safely.
+///
+/// **Failure mode**: returns `Ok(vec![])` when VeriSimDB is unreachable,
+/// returns 4xx/5xx, or has no matches. Errors from the executor itself
+/// (TypeLL validation, query construction) propagate. Callers that want
+/// strict failure semantics should use `QueryExecutor::execute` directly.
+///
+/// **Layering**: this is the dispatcher-layer counterpart to a backend's
+/// `search_theorems`. The 70+ backends whose native search is empty
+/// (`Ok(vec![])`) are not stubs to be filled — they correctly report
+/// "no native prover-specific search". Cross-prover semantics belong
+/// here, where one query covers every prover that has ever recorded a
+/// matching attempt.
+#[cfg(feature = "verisim")]
+pub async fn cross_prover_search_names(
+    verisim_url: &str,
+    pattern: &str,
+    limit: usize,
+) -> Result<Vec<String>> {
+    if pattern.trim().is_empty() {
+        return Ok(vec![]);
+    }
+    let executor = QueryExecutor::new(verisim_url);
+    let query = CrossProverQueryBuilder::new(TypeLevel::Cardinality)
+        .cross_prover_search(pattern)
+        .with_limit(limit)
+        .build()?;
+
+    match executor.execute(&query).await {
+        Ok(result) => Ok(result
+            .entries
+            .into_iter()
+            .filter_map(|e| {
+                let name = e.theorem_name.trim().to_string();
+                if name.is_empty() {
+                    None
+                } else {
+                    Some(name)
+                }
+            })
+            .collect()),
+        Err(_) => Ok(vec![]),
+    }
+}
+
+/// Build a no-op cross-prover search shim for the no-verisim default
+/// build, so callers don't need their own `#[cfg]` ladder. Always
+/// returns `Ok(vec![])`.
+#[cfg(not(feature = "verisim"))]
+pub async fn cross_prover_search_names(
+    _verisim_url: &str,
+    _pattern: &str,
+    _limit: usize,
+) -> Result<Vec<String>> {
+    Ok(vec![])
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -981,4 +1052,33 @@ mod tests {
         assert_eq!(result.count, 0);
         assert_eq!(result.verified_level, TypeLevel::ResultType);
     }
+
+    #[tokio::test]
+    async fn test_cross_prover_search_names_empty_pattern() {
+        // Empty / whitespace patterns short-circuit to empty without
+        // touching VeriSimDB at all — useful for callers that pass an
+        // un-validated CLI argument.
+        let names =
+            cross_prover_search_names("http://127.0.0.1:1", "", 10).await.unwrap();
+        assert!(names.is_empty());
+        let names =
+            cross_prover_search_names("http://127.0.0.1:1", "   ", 10).await.unwrap();
+        assert!(names.is_empty());
+    }
+
+    #[tokio::test]
+    async fn test_cross_prover_search_names_unreachable_returns_empty() {
+        // A real pattern against an unreachable VeriSimDB must return Ok(vec![])
+        // — search is a soft query, an outage cannot kill the caller.
+        // Without the verisim feature this is a no-op stub that also returns
+        // Ok(vec![]), so the same assertion holds in both build modes.
+        let names = cross_prover_search_names(
+            "http://127.0.0.1:1",
+            "associativity",
+            5,
+        )
+        .await
+        .unwrap();
+        assert!(names.is_empty());
+    }
 }