feat: implement ECHIDNA Phase 2 — interactive sessions & tactic suggestions

Connect PanLL to ECHIDNA's real session-based REST API (port 8000, /api/v1/)
for interactive proof sessions with ML-powered tactic suggestions. Fix the
default URL from the GraphQL port (:8080) to the REST port (:8000).

- Model: add echidnaProofStatus (6 states), extend echidnaSessionState with
  prover/goal/status/proofScript/timeElapsed/errorMessage, add args to
  echidnaTacticSuggestion, add tacticInput/sessionLoading to echidnaState
- Rust: 4 new Tauri commands (create_session, get_session, apply_tactic,
  suggest_tactics) with 2 unit tests for URL construction and serialisation
- TauriCmd: 4 TEA command wrappers for session lifecycle
- Update: 3 JSON parsers (parseEchidnaSession, parseTacticResponse,
  parseTacticSuggestions), replace all 8 Phase 1 stubs with real handlers,
  auto-request suggestions after session creation and tactic application
- PaneN: 6 new UI components — session controls, status badge (colour-coded),
  goal list (active goal highlighted), manual tactic input, suggestion ribbon
  (clickable chips sorted by confidence), proof script history
- Tests: 13 new tests covering all session/tactic message handlers (24 total)

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

Author: hyperpolymath

src-tauri/src/main.rs

@@ -1314,7 +1314,7 @@ fn verisimdb_get_entity(entity_id: String) -> Result<String, String> {
 // ECHIDNA Theorem Prover Backend
 // ===========================================================================
 
-const DEFAULT_ECHIDNA_URL: &str = "http://localhost:8080/api";
+const DEFAULT_ECHIDNA_URL: &str = "http://localhost:8000/api/v1";
 
 /// Resolve the ECHIDNA API base URL from environment or default.
 /// Override with ECHIDNA_URL env var for non-default deployments.
@@ -1460,6 +1460,118 @@ fn echidna_search_theorems(query: String) -> Result<String, String> {
     }
 }
 
+/// POST /proofs — create a new interactive proof session.
+/// Sends `{"goal": goal, "prover": prover}` and returns the ProofResponse JSON
+/// with session ID, initial goals, and status (201 Created).
+#[tauri::command]
+fn echidna_create_session(goal: String, prover: String) -> Result<String, String> {
+    let url = format!("{}/proofs", echidna_url());
+    let client = reqwest::blocking::Client::builder()
+        .timeout(std::time::Duration::from_secs(30))
+        .build()
+        .map_err(|e| format!("HTTP client error: {}", e))?;
+
+    let payload = json!({ "goal": goal, "prover": prover });
+
+    match client.post(&url).json(&payload).send() {
+        Ok(resp) => {
+            let status = resp.status();
+            let body = resp.text().unwrap_or_default();
+            if status.is_success() {
+                Ok(body)
+            } else {
+                Err(format!("Session creation failed ({}): {}", status, body))
+            }
+        }
+        Err(e) => Err(format!("Session creation request failed: {}", e)),
+    }
+}
+
+/// GET /proofs/{id} — retrieve the current state of a proof session.
+/// Returns the ProofResponse JSON with goals, status, and applied tactics.
+#[tauri::command]
+fn echidna_get_session(session_id: String) -> Result<String, String> {
+    let url = format!("{}/proofs/{}", echidna_url(), session_id);
+    let client = reqwest::blocking::Client::builder()
+        .timeout(std::time::Duration::from_secs(10))
+        .build()
+        .map_err(|e| format!("HTTP client error: {}", e))?;
+
+    match client.get(&url).send() {
+        Ok(resp) => {
+            let status = resp.status();
+            let body = resp.text().unwrap_or_default();
+            if status.is_success() {
+                Ok(body)
+            } else {
+                Err(format!("Get session failed ({}): {}", status, body))
+            }
+        }
+        Err(e) => Err(format!("Get session request failed: {}", e)),
+    }
+}
+
+/// POST /proofs/{id}/tactics — apply a tactic to an active proof session.
+/// Sends `{"name": name, "args": args}` and returns the TacticResponse JSON
+/// with success flag and updated proof state.
+#[tauri::command]
+fn echidna_apply_tactic(
+    session_id: String,
+    name: String,
+    args: Vec<String>,
+) -> Result<String, String> {
+    let url = format!("{}/proofs/{}/tactics", echidna_url(), session_id);
+    let client = reqwest::blocking::Client::builder()
+        .timeout(std::time::Duration::from_secs(30))
+        .build()
+        .map_err(|e| format!("HTTP client error: {}", e))?;
+
+    let payload = json!({ "name": name, "args": args });
+
+    match client.post(&url).json(&payload).send() {
+        Ok(resp) => {
+            let status = resp.status();
+            let body = resp.text().unwrap_or_default();
+            if status.is_success() {
+                Ok(body)
+            } else {
+                Err(format!("Apply tactic failed ({}): {}", status, body))
+            }
+        }
+        Err(e) => Err(format!("Apply tactic request failed: {}", e)),
+    }
+}
+
+/// GET /proofs/{id}/tactics/suggest?limit=N — request ML-powered tactic suggestions.
+/// The ML advisor (Julia :8090) generates suggestions with confidence scores,
+/// falling back to prover heuristics if the advisor is unavailable.
+#[tauri::command]
+fn echidna_suggest_tactics(session_id: String, limit: usize) -> Result<String, String> {
+    let url = format!(
+        "{}/proofs/{}/tactics/suggest?limit={}",
+        echidna_url(),
+        session_id,
+        limit
+    );
+    let client = reqwest::blocking::Client::builder()
+        .timeout(std::time::Duration::from_secs(15))
+        .build()
+        .map_err(|e| format!("HTTP client error: {}", e))?;
+
+    match client.get(&url).send() {
+        Ok(resp) => {
+            let status = resp.status();
+            let body = resp.text().unwrap_or_default();
+            if status.is_success() {
+                Ok(body)
+            } else {
+                Err(format!("Tactic suggestions failed ({}): {}", status, body))
+            }
+        }
+        Err(e) => Err(format!("Tactic suggestions request failed: {}", e)),
+    }
+}
+
 #[cfg(test)]
 mod echidna_tests {
     use super::*;
@@ -1479,6 +1591,47 @@ mod echidna_tests {
         // Clean up so other tests aren't affected.
         std::env::remove_var("ECHIDNA_URL");
     }
+
+    #[test]
+    fn echidna_session_url_construction() {
+        std::env::remove_var("ECHIDNA_URL");
+        let base = echidna_url();
+        let session_url = format!("{}/proofs/{}", base, "test-session-123");
+        assert_eq!(
+            session_url,
+            "http://localhost:8000/api/v1/proofs/test-session-123"
+        );
+
+        let tactic_url = format!("{}/proofs/{}/tactics", base, "sess-abc");
+        assert_eq!(
+            tactic_url,
+            "http://localhost:8000/api/v1/proofs/sess-abc/tactics"
+        );
+
+        let suggest_url = format!(
+            "{}/proofs/{}/tactics/suggest?limit={}",
+            base, "sess-abc", 5
+        );
+        assert_eq!(
+            suggest_url,
+            "http://localhost:8000/api/v1/proofs/sess-abc/tactics/suggest?limit=5"
+        );
+    }
+
+    #[test]
+    fn echidna_prover_serialisation() {
+        let payload = json!({ "goal": "forall x, x + 0 = x", "prover": "lean4" });
+        let obj = payload.as_object().unwrap();
+        assert_eq!(obj.get("goal").unwrap().as_str().unwrap(), "forall x, x + 0 = x");
+        assert_eq!(obj.get("prover").unwrap().as_str().unwrap(), "lean4");
+
+        let tactic_payload = json!({ "name": "intro", "args": ["x", "y"] });
+        let tobj = tactic_payload.as_object().unwrap();
+        assert_eq!(tobj.get("name").unwrap().as_str().unwrap(), "intro");
+        let args = tobj.get("args").unwrap().as_array().unwrap();
+        assert_eq!(args.len(), 2);
+        assert_eq!(args[0].as_str().unwrap(), "x");
+    }
 }
 
 fn main() {
@@ -1508,6 +1661,10 @@ fn main() {
             echidna_prove,
             echidna_verify,
             echidna_search_theorems,
+            echidna_create_session,
+            echidna_get_session,
+            echidna_apply_tactic,
+            echidna_suggest_tactics,
         ])
         .setup(|app| {
             #[cfg(debug_assertions)]

src/Model.res

@@ -318,25 +318,43 @@ type echidnaDispatchResult = {
 }
 
 /// A tactic suggestion from the ECHIDNA ML advisor.
-/// Phase 2 — type defined now, handler returns model unchanged.
+/// Includes tactic name, arguments, confidence score, aspect tags, and description.
+/// The ML advisor (Julia :8090) or prover fallback populates these.
 type echidnaTacticSuggestion = {
   tactic: string,
+  args: array<string>,
   confidence: float,
   aspectTags: array<string>,
   description: string,
 }
 
-/// Interactive proof session state.
-/// Phase 2 — type defined now, handler returns model unchanged.
+/// ECHIDNA proof session status — maps to the ProofResponse status field
+/// from the ECHIDNA REST API (/api/v1/proofs).
+type echidnaProofStatus =
+  | Pending       // Session created, awaiting first tactic
+  | InProgress    // Tactics being applied, goals remaining
+  | ProofSuccess  // All goals discharged
+  | ProofFailed   // Proof attempt failed
+  | ProofTimeout  // Solver timed out
+  | ProofError    // Internal error during proof
+
+/// Interactive proof session state — mirrors ECHIDNA's ProofResponse.
+/// Tracks session identity, prover, goals, applied tactics, and timing.
 type echidnaSessionState = {
   sessionId: string,
+  prover: string,
+  goal: string,
+  status: echidnaProofStatus,
   goals: array<string>,
+  proofScript: array<string>,
   complete: bool,
   tacticsApplied: array<string>,
+  timeElapsed: option<float>,
+  errorMessage: option<string>,
 }
 
 /// ECHIDNA backend state — tracks connection, prover catalog, proof lifecycle,
-/// interactive session (Phase 2), and tactic suggestions (Phase 2).
+/// interactive session, and tactic suggestions.
 type echidnaState = {
   connected: bool,
   endpoint: string,
@@ -350,6 +368,8 @@ type echidnaState = {
   selectedProver: option<string>,
   proofInput: string,
   menuExpanded: bool,
+  tacticInput: string,
+  sessionLoading: bool,
 }
 
 /// The complete Model
@@ -511,7 +531,7 @@ let init = (): model => {
   },
   echidna: {
     connected: false,
-    endpoint: "http://localhost:8080/api",
+    endpoint: "http://localhost:8000/api/v1",
     version: None,
     provers: [],
     lastProofResult: None,
@@ -522,6 +542,8 @@ let init = (): model => {
     selectedProver: None,
     proofInput: "",
     menuExpanded: false,
+    tacticInput: "",
+    sessionLoading: false,
   },
   humidity: Medium,
   viewMode: DarkStart,

src/Msg.res

@@ -146,14 +146,16 @@ type echidnaMsg =
   // Theorem search
   | SearchTheorems(string)
   | SearchResult(result<string, string>)
-  // Interactive sessions (Phase 2 — stub)
+  // Interactive sessions
   | CreateSession
   | SessionCreated(result<string, string>)
-  | ApplyTactic(string)
+  | ApplyTactic(string, array<string>)
   | TacticApplied(result<string, string>)
   | GetSessionState
   | SessionStateLoaded(result<string, string>)
-  // Tactic suggestions (Phase 2 — stub)
+  | CancelSession
+  | UpdateTacticInput(string)
+  // Tactic suggestions
   | RequestTacticSuggestions
   | TacticSuggestionsLoaded(result<string, string>)
   // UI state