test: implement 6 agentic integration tests, fix TypedWasm match exhaustiveness

- Replace 6 todo!() stubs with real tests: proof memory storage/retrieval,
  prover router learning, goal decomposition, agent queue priority,
  memory failure tracking, router aspect scoring
- Make ProverStats fields + success_rate() pub for test assertions
- Make AgentCore::next_goal() pub for queue priority testing
- Add TypedWasm arms to all ProverKind match statements in test helpers
- Fix prover count assertion (30→dynamic) for ProverFactory smoke test

Test results: 387 passed, 0 failed, 16 ignored (up from 352/22)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/rust/agent/mod.rs

@@ -199,7 +199,7 @@ impl AgentCore {
     }
 
     /// Get the next goal from the queue
-    async fn next_goal(&self) -> Option<AgenticGoal> {
+    pub async fn next_goal(&self) -> Option<AgenticGoal> {
         let mut queue = self.goal_queue.write().await;
         queue.pop_front()
     }

src/rust/agent/router.rs

@@ -19,20 +19,21 @@ use super::AgenticGoal;
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct ProverStats {
     /// Total attempts
-    attempts: u32,
+    pub attempts: u32,
 
     /// Successful proofs
-    successes: u32,
+    pub successes: u32,
 
     /// Failures
-    failures: u32,
+    pub failures: u32,
 
     /// Total time (milliseconds)
-    total_time_ms: u64,
+    pub total_time_ms: u64,
 }
 
 impl ProverStats {
-    fn new() -> Self {
+    /// Create new empty stats
+    pub fn new() -> Self {
         ProverStats {
             attempts: 0,
             successes: 0,
@@ -42,7 +43,7 @@ impl ProverStats {
     }
 
     /// Success rate (0.0 - 1.0)
-    fn success_rate(&self) -> f64 {
+    pub fn success_rate(&self) -> f64 {
         if self.attempts == 0 {
             0.5 // No data, assume 50%
         } else {

tests/agentic_integration.rs

@@ -116,27 +116,199 @@ impl ProverBackend for MockProver {
 }
 
 #[tokio::test]
-#[ignore = "Requires API updates to SqliteMemory"]
 async fn test_proof_memory_storage_and_retrieval() {
-    todo!("API updates needed for SqliteMemory")
+    let tmp = TempDir::new().unwrap();
+    let memory = SqliteMemory::new(tmp.path().join("test.db"));
+    memory.init().await.unwrap();
+
+    let goal = AgenticGoal {
+        goal: Goal {
+            id: "mem_test".to_string(),
+            target: Term::Var("P".to_string()),
+            hypotheses: vec![],
+        },
+        priority: Priority::Medium,
+        attempts: 0,
+        max_attempts: 3,
+        preferred_prover: None,
+        aspects: vec!["logic".to_string()],
+        parent: None,
+    };
+
+    let proof = echidna::core::ProofState {
+        goals: vec![],
+        context: Default::default(),
+        proof_script: vec![],
+        metadata: Default::default(),
+    };
+
+    // Store a success
+    memory
+        .store_success(&goal, &proof, ProverKind::Coq, 250)
+        .await
+        .unwrap();
+
+    // Retrieve successes
+    let successes = memory.get_successes().await.unwrap();
+    assert_eq!(successes.len(), 1);
+    assert_eq!(successes[0].goal_id, "mem_test");
+    assert_eq!(successes[0].prover, ProverKind::Coq);
+    assert_eq!(successes[0].time_ms, 250);
+    assert_eq!(successes[0].aspects, vec!["logic".to_string()]);
+
+    // Check stats
+    let stats = memory.stats().await.unwrap();
+    assert_eq!(stats.total_proofs, 1);
+    assert_eq!(stats.total_failures, 0);
+    assert!((stats.success_rate - 1.0).abs() < f64::EPSILON);
+    assert!((stats.avg_proof_time_ms - 250.0).abs() < f64::EPSILON);
 }
 
 #[tokio::test]
-#[ignore = "Requires API updates to ProverRouter"]
 async fn test_prover_router_learning() {
-    todo!("API updates needed for ProverRouter")
+    let router = ProverRouter::new();
+
+    let goal = AgenticGoal {
+        goal: Goal {
+            id: "router_test".to_string(),
+            target: Term::Var("X".to_string()),
+            hypotheses: vec![],
+        },
+        priority: Priority::Medium,
+        attempts: 0,
+        max_attempts: 3,
+        preferred_prover: None,
+        aspects: vec!["arithmetic".to_string()],
+        parent: None,
+    };
+
+    // Record several Z3 successes for arithmetic
+    for _ in 0..5 {
+        router.record_success(&goal, ProverKind::Z3).await;
+    }
+
+    // Record Coq failures for arithmetic
+    for _ in 0..5 {
+        router.record_failure(&goal, ProverKind::Coq).await;
+    }
+
+    // Verify global stats reflect the history
+    let stats = router.get_all_stats().await;
+    let z3_stats = stats.get(&ProverKind::Z3).unwrap();
+    assert_eq!(z3_stats.successes, 5);
+    assert_eq!(z3_stats.failures, 0);
+    assert!((z3_stats.success_rate() - 1.0).abs() < f64::EPSILON);
+
+    let coq_stats = stats.get(&ProverKind::Coq).unwrap();
+    assert_eq!(coq_stats.successes, 0);
+    assert_eq!(coq_stats.failures, 5);
+    assert!((coq_stats.success_rate() - 0.0).abs() < f64::EPSILON);
 }
 
 #[tokio::test]
-#[ignore = "Requires API updates to RulePlanner"]
 async fn test_goal_decomposition() {
-    todo!("API updates needed for RulePlanner")
+    let planner = RulePlanner::new();
+
+    // Create an implication goal: A → B
+    let impl_goal = AgenticGoal {
+        goal: Goal {
+            id: "impl_test".to_string(),
+            target: Term::Pi {
+                param: "x".to_string(),
+                param_type: Box::new(Term::Var("A".to_string())),
+                body: Box::new(Term::Var("B".to_string())),
+            },
+            hypotheses: vec![],
+        },
+        priority: Priority::High,
+        attempts: 0,
+        max_attempts: 3,
+        preferred_prover: None,
+        aspects: vec!["logic".to_string()],
+        parent: None,
+    };
+
+    let sub_goals = planner.decompose(&impl_goal).await.unwrap();
+    assert!(!sub_goals.is_empty(), "Implication should decompose into sub-goals");
+
+    // The conclusion sub-goal should target B
+    let conclusion = &sub_goals[0];
+    assert_eq!(conclusion.goal.id, "impl_test_conclusion");
+    assert_eq!(conclusion.parent, Some("impl_test".to_string()));
+
+    // A non-decomposable goal should return empty
+    let atomic_goal = AgenticGoal {
+        goal: Goal {
+            id: "atomic_test".to_string(),
+            target: Term::Var("X".to_string()),
+            hypotheses: vec![],
+        },
+        priority: Priority::Low,
+        attempts: 0,
+        max_attempts: 3,
+        preferred_prover: None,
+        aspects: vec![],
+        parent: None,
+    };
+
+    // Non-decomposable goals return themselves as-is (vec![goal.clone()])
+    let no_sub = planner.decompose(&atomic_goal).await.unwrap();
+    assert_eq!(no_sub.len(), 1, "Atomic goal returns itself unchanged");
+    assert_eq!(no_sub[0].goal.id, "atomic_test");
 }
 
 #[tokio::test]
-#[ignore = "Requires API updates to AgentCore"]
 async fn test_agent_queue_priority() {
-    todo!("API updates needed for AgentCore")
+    let prover: Box<dyn ProverBackend> = Box::new(MockProver::new(ProverKind::Z3, true));
+    let tmp = TempDir::new().unwrap();
+    let memory = SqliteMemory::new(tmp.path().join("queue_test.db"));
+    memory.init().await.unwrap();
+    let planner = RulePlanner::new();
+    let router = ProverRouter::new();
+
+    let config = AgentConfig::default();
+    let agent = AgentCore::new(
+        Box::new(memory),
+        Box::new(planner),
+        router,
+        vec![prover],
+        config,
+    );
+
+    // Add goals with different priorities
+    let make_goal = |id: &str, priority: Priority| AgenticGoal {
+        goal: Goal {
+            id: id.to_string(),
+            target: Term::Var("X".to_string()),
+            hypotheses: vec![],
+        },
+        priority,
+        attempts: 0,
+        max_attempts: 3,
+        preferred_prover: None,
+        aspects: vec![],
+        parent: None,
+    };
+
+    agent.add_goal(make_goal("low", Priority::Low)).await.unwrap();
+    agent.add_goal(make_goal("high", Priority::High)).await.unwrap();
+    agent.add_goal(make_goal("critical", Priority::Critical)).await.unwrap();
+    agent.add_goal(make_goal("medium", Priority::Medium)).await.unwrap();
+
+    // Critical should come first (highest priority at front)
+    let first = agent.next_goal().await.expect("Should have a goal");
+    assert_eq!(first.goal.id, "critical");
+
+    let second = agent.next_goal().await.expect("Should have a goal");
+    assert_eq!(second.goal.id, "high");
+
+    let third = agent.next_goal().await.expect("Should have a goal");
+    assert_eq!(third.goal.id, "medium");
+
+    let fourth = agent.next_goal().await.expect("Should have a goal");
+    assert_eq!(fourth.goal.id, "low");
+
+    assert!(agent.next_goal().await.is_none(), "Queue should be empty");
 }
 
 #[test]
@@ -200,15 +372,121 @@ fn test_explanation_generation() {
 }
 
 #[tokio::test]
-#[ignore = "Requires API updates to SqliteMemory"]
 async fn test_memory_failure_tracking() {
-    todo!("API updates needed for SqliteMemory")
+    let tmp = TempDir::new().unwrap();
+    let memory = SqliteMemory::new(tmp.path().join("failure_test.db"));
+    memory.init().await.unwrap();
+
+    let goal1 = AgenticGoal {
+        goal: Goal {
+            id: "fail1".to_string(),
+            target: Term::Var("P".to_string()),
+            hypotheses: vec![],
+        },
+        priority: Priority::High,
+        attempts: 1,
+        max_attempts: 3,
+        preferred_prover: Some(ProverKind::Coq),
+        aspects: vec!["inductive".to_string()],
+        parent: None,
+    };
+
+    let goal2 = AgenticGoal {
+        goal: Goal {
+            id: "fail2".to_string(),
+            target: Term::Var("Q".to_string()),
+            hypotheses: vec![],
+        },
+        priority: Priority::Medium,
+        attempts: 1,
+        max_attempts: 3,
+        preferred_prover: None,
+        aspects: vec!["arithmetic".to_string()],
+        parent: None,
+    };
+
+    // Store failures
+    memory.store_failure(&goal1, "timeout".to_string()).await.unwrap();
+    memory.store_failure(&goal2, "unsupported tactic".to_string()).await.unwrap();
+
+    // Verify failures stored
+    let failures = memory.get_failures().await.unwrap();
+    assert_eq!(failures.len(), 2);
+    assert_eq!(failures[0].goal_id, "fail1");
+    assert_eq!(failures[0].reason, "timeout");
+    assert_eq!(failures[0].prover, Some(ProverKind::Coq));
+    assert_eq!(failures[1].goal_id, "fail2");
+    assert_eq!(failures[1].reason, "unsupported tactic");
+
+    // Stats should show 0% success rate
+    let stats = memory.stats().await.unwrap();
+    assert_eq!(stats.total_proofs, 0);
+    assert_eq!(stats.total_failures, 2);
+    assert!((stats.success_rate - 0.0).abs() < f64::EPSILON);
 }
 
 #[tokio::test]
-#[ignore = "Requires API updates to ProverRouter"]
 async fn test_router_aspect_scoring() {
-    todo!("API updates needed for ProverRouter")
+    let router = ProverRouter::new();
+
+    // Build history: Z3 is great at arithmetic, Coq is great at inductive
+    let arith_goal = AgenticGoal {
+        goal: Goal {
+            id: "arith".to_string(),
+            target: Term::Var("N".to_string()),
+            hypotheses: vec![],
+        },
+        priority: Priority::Medium,
+        attempts: 0,
+        max_attempts: 3,
+        preferred_prover: None,
+        aspects: vec!["arithmetic".to_string()],
+        parent: None,
+    };
+
+    let inductive_goal = AgenticGoal {
+        goal: Goal {
+            id: "induct".to_string(),
+            target: Term::Var("P".to_string()),
+            hypotheses: vec![],
+        },
+        priority: Priority::Medium,
+        attempts: 0,
+        max_attempts: 3,
+        preferred_prover: None,
+        aspects: vec!["inductive".to_string()],
+        parent: None,
+    };
+
+    // Z3 succeeds on arithmetic
+    for _ in 0..10 {
+        router.record_success(&arith_goal, ProverKind::Z3).await;
+    }
+
+    // Coq succeeds on inductive
+    for _ in 0..10 {
+        router.record_success(&inductive_goal, ProverKind::Coq).await;
+    }
+
+    // Z3 fails on inductive
+    for _ in 0..10 {
+        router.record_failure(&inductive_goal, ProverKind::Z3).await;
+    }
+
+    // Verify aspect-specific routing works
+    let all_stats = router.get_all_stats().await;
+
+    // Z3 global: 10 successes (arithmetic) + 10 failures (inductive) = 20 attempts
+    let z3 = all_stats.get(&ProverKind::Z3).unwrap();
+    assert_eq!(z3.successes, 10);
+    assert_eq!(z3.failures, 10);
+    assert!((z3.success_rate() - 0.5).abs() < f64::EPSILON);
+
+    // Coq global: 10 successes (inductive), 0 failures = 100% success
+    let coq = all_stats.get(&ProverKind::Coq).unwrap();
+    assert_eq!(coq.successes, 10);
+    assert_eq!(coq.failures, 0);
+    assert!((coq.success_rate() - 1.0).abs() < f64::EPSILON);
 }
 
 #[test]