feat(integration): wire MetaController into AgentCore + server

AgentCore:
- Add meta_controller: Arc<MetaController> field; pass through new()
- process_goal() now calls meta_controller.plan() instead of router.select()
- run_preconditions() executes coprocessor ops before the prover fires;
  outcomes are injected into ProofState::metadata under "coprocessor.<aspect>"
  keys so backends and tactic suggesters see pre-computed witnesses
- record_outcome() feeds every QED/failure back to the StatisticsTracker
  so Bayesian routing converges toward what works for each (prover, domain)
- Router retained for backward-compat reflection path; MetaController is
  the primary planning path going forward

Server:
- AppState gains meta_controller: Arc<MetaController>; constructed once at
  server startup so the Bayesian stats accumulate across all requests
- POST /api/agent/plan endpoint: accepts { aspects, preferred_prover,
  candidates, default_timeout_ms }, returns the MetaController's Plan
  (chosen prover, coprocessor preconditions, Bayesian timeout estimate,
  rationale).  Clients can inspect the plan before submitting a full proof.

872 tests green, 0 clippy errors.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

src/rust/agent/mod.rs

@@ -11,6 +11,7 @@
 use anyhow::Result;
 use serde::{Deserialize, Serialize};
 use std::collections::VecDeque;
+use std::sync::Arc;
 use tokio::sync::RwLock;
 use tracing::{debug, info, warn};
 
@@ -24,6 +25,7 @@ pub mod meta_controller; // Coordinates prover × coprocessor × goal-aspect
 pub mod planner;
 pub mod router;
 
+use meta_controller::{MetaController, PlanOutcome};
 use memory::ProofMemory;
 use planner::Planner;
 use router::ProverRouter;
@@ -121,6 +123,12 @@ pub struct AgentCore {
     /// Planner (decomposes goals into sub-goals)
     planner: Box<dyn Planner>,
 
+    /// MetaController — aspect-aware (prover × coprocessor) planner with
+    /// Pareto-frontier ranking and Bayesian timeout estimation.  Supersedes
+    /// the raw ProverRouter for goal dispatch; the router is retained for
+    /// the backward-compat reflection path (`reflect_on_success/failure`).
+    meta_controller: Arc<MetaController>,
+
     /// Prover router (selects best prover for a goal)
     router: ProverRouter,
 
@@ -167,10 +175,16 @@ impl Default for AgentConfig {
 }
 
 impl AgentCore {
-    /// Create a new agent core
+    /// Create a new agent core.
+    ///
+    /// `meta_controller` is the shared (prover × coprocessor) planner.  Pass
+    /// `Arc::new(MetaController::new())` for a standalone controller, or share
+    /// one that already has a `StatisticsTracker` plugged in (via
+    /// `MetaController::with_stats`) so outcomes feed a persistent learning loop.
     pub fn new(
         memory: Box<dyn ProofMemory>,
         planner: Box<dyn Planner>,
+        meta_controller: Arc<MetaController>,
         router: ProverRouter,
         provers: Vec<Box<dyn ProverBackend>>,
         config: AgentConfig,
@@ -179,6 +193,7 @@ impl AgentCore {
             goal_queue: RwLock::new(VecDeque::new()),
             memory,
             planner,
+            meta_controller,
             router,
             provers,
             config,
@@ -323,47 +338,69 @@ impl AgentCore {
             return Ok(GoalResult::Decomposed { sub_goals });
         }
 
-        // Step 3: Select prover
-        let prover_kind = goal
-            .preferred_prover
-            .unwrap_or_else(|| self.router.select(&goal));
+        // Step 3: Plan — MetaController selects the prover and queues coprocessor
+        // preconditions whose results will be available to the prover as proof
+        // context (ProofState::metadata).  Falls back gracefully to Z3 when no
+        // aspect routing matches or no stats exist.
+        let plan = self.meta_controller.plan(&goal).await;
+        let precondition_outcomes = self
+            .meta_controller
+            .run_preconditions(&plan)
+            .await
+            .unwrap_or_default();
+
+        // Use the MetaController's chosen prover, falling back to the
+        // router if that prover is not in our local pool.
+        let prover_kind = if self.provers.iter().any(|p| p.kind() == plan.prover) {
+            plan.prover
+        } else {
+            self.router.select(&goal)
+        };
 
         let prover = self
             .provers
             .iter()
             .find(|p| p.kind() == prover_kind)
             .ok_or_else(|| anyhow::anyhow!("Prover {:?} not available", prover_kind))?;
 
-        // Step 4: Get tactic suggestions (neural guidance)
+        // Step 4: Seed ProofState metadata with coprocessor witness data so
+        // the prover backend and tactic suggester can see pre-computed facts
+        // (e.g. factorizations, Gröbner bases, crypto verifications).
+        // Keys follow the convention "coprocessor.<aspect>".
+        let mut metadata: std::collections::HashMap<String, serde_json::Value> = Default::default();
+        for (pre, outcome) in plan
+            .coprocessor_preconditions
+            .iter()
+            .zip(precondition_outcomes.iter())
+        {
+            if let Ok(v) = serde_json::to_value(outcome) {
+                metadata.insert(format!("coprocessor.{}", pre.aspect), v);
+            }
+        }
+
+        // Step 5: Get tactic suggestions (neural guidance), using the
+        // context-enriched initial state so the suggestion model sees the
+        // coprocessor witnesses.
+        let initial_state = ProofState {
+            goals: vec![goal.goal.clone()],
+            context: Default::default(),
+            proof_script: vec![],
+            metadata: metadata.clone(),
+        };
         let tactics = if self.config.neural_enabled {
-            prover
-                .suggest_tactics(
-                    &ProofState {
-                        goals: vec![goal.goal.clone()],
-                        context: Default::default(),
-                        proof_script: vec![],
-                        metadata: Default::default(),
-                    },
-                    5,
-                )
-                .await?
+            prover.suggest_tactics(&initial_state, 5).await?
         } else {
-            vec![Tactic::Assumption] // Fallback
+            vec![Tactic::Assumption]
         };
 
-        // Step 5: Try tactics against the chosen backend.
+        // Step 6: Try tactics against the chosen backend.
         //
         // Each candidate is applied via the `ProverBackend::apply_tactic`
         // FFI and the resulting state either yields the full proof (QED),
         // advances the state (Success — we fall through to next tactic,
         // keeping this step-thin), or errors out.
         let start = std::time::Instant::now();
-        let mut current_state = ProofState {
-            goals: vec![goal.goal.clone()],
-            context: Default::default(),
-            proof_script: vec![],
-            metadata: Default::default(),
-        };
+        let mut current_state = initial_state;
 
         for tactic in tactics {
             debug!("Trying tactic {:?} for goal {}", tactic, goal.goal.id);
@@ -372,6 +409,9 @@ impl AgentCore {
                 Ok(TacticResult::QED) => {
                     current_state.proof_script.push(tactic.clone());
                     let time_ms = start.elapsed().as_millis() as u64;
+                    self.meta_controller
+                        .record_outcome(&plan, &goal, PlanOutcome::Success, time_ms)
+                        .await;
                     return Ok(GoalResult::Proved {
                         proof: current_state,
                         prover: prover_kind,
@@ -391,6 +431,10 @@ impl AgentCore {
             }
         }
 
+        let elapsed_ms = start.elapsed().as_millis() as u64;
+        self.meta_controller
+            .record_outcome(&plan, &goal, PlanOutcome::Failure, elapsed_ms)
+            .await;
         Ok(GoalResult::Failed {
             reason: "No tactic succeeded".to_string(),
             prover: Some(prover_kind),

src/rust/server.rs

@@ -14,7 +14,9 @@ use axum::{
     Json, Router,
 };
 use colored::Colorize;
-use echidna::core::{ProofState, Tactic, TacticResult};
+use echidna::agent::meta_controller::{MetaController, Plan};
+use echidna::agent::AgenticGoal;
+use echidna::core::{Goal, ProofState, Tactic, TacticResult, Term};
 use echidna::dispatch::ProverDispatcher;
 use echidna::{ProverBackend, ProverConfig, ProverKind};
 use reqwest::Client;
@@ -37,6 +39,11 @@ struct AppState {
     ml_client: Client,
     /// Julia ML API base URL
     ml_api_url: String,
+    /// MetaController — shared (prover × coprocessor) planner with persistent
+    /// StatisticsTracker.  Survives request boundaries so the Bayesian routing
+    /// state accumulates across the server's lifetime.  All handlers that
+    /// perform goal-aware dispatch share this single instance.
+    meta_controller: Arc<MetaController>,
 }
 
 /// A proof session
@@ -74,10 +81,13 @@ pub async fn start_server(port: u16, host: String, enable_cors: bool) -> Result<
         },
     }
 
+    let meta_controller = Arc::new(MetaController::new());
+
     let state = AppState {
         sessions: Arc::new(RwLock::new(HashMap::new())),
         ml_client,
         ml_api_url,
+        meta_controller,
     };
 
     // Build router
@@ -99,6 +109,7 @@ pub async fn start_server(port: u16, host: String, enable_cors: bool) -> Result<
         .route("/api/session/:id/apply", post(apply_tactic_handler))
         .route("/api/session/:id/tree", get(get_proof_tree))
         // Additional UI-specific endpoints
+        .route("/api/agent/plan", post(agent_plan_handler))
         .route("/api/aspect-tags", get(get_aspect_tags))
         .route("/api/tactics/suggest", post(suggest_tactics_ui))
         .route("/api/theorems/search", get(search_theorems_ui))
@@ -157,6 +168,99 @@ pub async fn start_server(port: u16, host: String, enable_cors: bool) -> Result<
     Ok(())
 }
 
+// ========== Agent Planning ==========
+
+/// Request to `POST /api/agent/plan`.
+///
+/// Asks the MetaController to plan a proof attempt: which prover to use,
+/// which coprocessor preconditions to run first, and the Bayesian-estimated
+/// timeout.  The response is a `Plan` that callers can inspect before
+/// deciding whether to submit a full `/api/verify` or `/api/prove` request.
+///
+/// `aspects` drive the coprocessor routing (e.g. `"arithmetic.factorisation"`
+/// triggers a Math precondition; `"algebra.groebner.basis"` triggers Singular).
+/// `preferred_prover` and `candidates` are both optional — omitting both lets
+/// the Pareto ranker pick freely from Z3 as the default.
+#[derive(Debug, Deserialize)]
+struct AgentPlanRequest {
+    /// Goal aspect tags (e.g. `["arithmetic.factorisation", "crypto.hash.sha256"]`).
+    #[serde(default)]
+    aspects: Vec<String>,
+
+    /// Client's preferred prover, if any.  Overridden by Pareto ranking when
+    /// `candidates` is non-empty.
+    preferred_prover: Option<ProverKind>,
+
+    /// Candidate provers to rank.  When empty, `preferred_prover` (or Z3)
+    /// is selected directly without Pareto scoring.
+    #[serde(default)]
+    candidates: Vec<ProverKind>,
+
+    /// Default timeout hint (ms) used when no historical data is available.
+    #[serde(default = "default_timeout_ms")]
+    default_timeout_ms: u64,
+}
+
+fn default_timeout_ms() -> u64 {
+    30_000
+}
+
+/// `POST /api/agent/plan` — return a MetaController plan for the given goal aspects.
+///
+/// Does not execute any provers or coprocessors; it only plans.  Callers use
+/// the returned `coprocessor_preconditions` to understand what computational
+/// preparation the system recommends before submitting the proof content.
+async fn agent_plan_handler(
+    State(state): State<AppState>,
+    Json(req): Json<AgentPlanRequest>,
+) -> impl IntoResponse {
+    // Build a minimal AgenticGoal from the request metadata.  The goal target
+    // is a placeholder (`Term::Const("?")`) because planning doesn't inspect
+    // the proof content — only the aspects and prover preferences matter here.
+    use echidna::agent::Priority;
+    let goal = AgenticGoal {
+        goal: Goal {
+            id: uuid::Uuid::new_v4().to_string(),
+            target: Term::Const("?".to_string()),
+            hypotheses: vec![],
+        },
+        priority: Priority::Medium,
+        attempts: 0,
+        max_attempts: 3,
+        preferred_prover: req.preferred_prover,
+        aspects: req.aspects,
+        parent: None,
+    };
+
+    let plan: Plan = if req.candidates.is_empty() {
+        state.meta_controller.plan(&goal).await
+    } else {
+        use echidna::verification::confidence::TrustLevel;
+        state
+            .meta_controller
+            .plan_with_pareto(
+                &goal,
+                &req.candidates,
+                req.default_timeout_ms,
+                TrustLevel::Level2,
+            )
+            .await
+    };
+
+    Json(json!({
+        "prover": format!("{:?}", plan.prover),
+        "estimated_timeout_ms": plan.estimated_timeout_ms,
+        "rationale": plan.rationale,
+        "coprocessor_preconditions": plan.coprocessor_preconditions
+            .iter()
+            .map(|p| json!({
+                "kind": format!("{:?}", p.kind),
+                "aspect": p.aspect,
+            }))
+            .collect::<Vec<_>>(),
+    }))
+}
+
 // ========== Groove Discovery ==========
 
 /// Groove capability manifest for ECHIDNA.
@@ -691,6 +795,15 @@ async fn search_handler(
         }
     }
 
+    // Cross-prover layer (see main.rs::search_command for rationale).
+    // Folds VeriSimDB matches into the same response so REST clients
+    // see results from backends without native search commands too.
+    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, 50).await {
+        all_results.extend(cross);
+    }
+
     let count = all_results.len();
     Ok(Json(SearchResponse {
         results: all_results,