feat(api/graphql): add verifyProof + suggestTactics(prover/context/goalState) + proverStatus (closes #180) (#188)

## Summary

Resolves the echidna ↔ echidnabot GraphQL contract mismatch surfaced in
#180 by adding the three operations the echidnabot client expects, plus
surfacing the typed REST `/api/verify` taxonomy (`outcome`, optional
`mode` / `smtStatus`) through GraphQL so future clients no longer need
to round-trip via REST to disambiguate Timeout vs NoProofFound.

## New GraphQL operations

| Operation | Kind | Signature | Returns |
|---|---|---|---|
| `verifyProof` | mutation | `(prover: String!, content: String!)` |
`VerifyProofResult!` |
| `suggestTactics` | mutation | `(prover: String!, context: String!,
goalState: String!)` | `[SuggestedTactic!]!` |
| `proverStatus` | query | `(prover: String!)` | `ProverStatusInfo!` |

## New GraphQL types

- `VerifyOutcome` (enum: `PROVED` / `NO_PROOF_FOUND` / `INVALID_INPUT` /
`UNSUPPORTED_FEATURE` / `TIMEOUT` / `INCONSISTENT_PREMISES` /
`PROVER_ERROR` / `SYSTEM_ERROR`) — mirrors the REST `/api/verify`
`outcome` field
- `VerifyProofResult` — `status` + `message` + `proverOutput` +
`durationMs` + `artifacts` (echidnabot client's existing
`VerifyProofData` shape), **plus** `outcome` + `mode` + `smtStatus` (the
typed REST taxonomy newly threaded through)
- `SuggestedTactic` — `tactic` + `confidence` + `explanation` (matches
echidnabot's `TacticSuggestionData`)
- `ProverStatusInfo` — `available` + `message`

## Breaking change

The existing **query** `suggestTactics(proofId, limit)` has been renamed
to `suggestTacticsByProofId(proofId, limit)` to free the
`suggestTactics` name for the new **mutation** the echidnabot client
expects.

- Argument shape and return type (`[Tactic!]!`) are unchanged.
- Any consumer issuing `query { suggestTactics(proofId: ..., limit: ...)
}` must update the operation name to `suggestTacticsByProofId`. The new
`suggestTactics(prover, context, goalState)` on `MutationRoot` is the
only `suggestTactics` field after this PR.
- `interfaces/README.md` updated to reflect the new GraphQL surface.

## DRY

- `verifyProof` delegates to the same `ProverFactory::create` +
`parse_string` + `verify_proof` chain that backs REST `/api/verify`, so
behaviour matches by construction.
- `suggestTactics` (for-goal) tries the Julia ML coprocessor first and
falls back to backend-native suggestions — same pattern as the existing
session-based `suggest_tactics` path, just without requiring a
`proof_id`.

## Tests

`+8` in `src/interfaces/graphql/schema.rs::tests`:

1. `verify_outcome_from_rest_str_covers_taxonomy` — every REST taxon
round-trips to a distinct enum variant
2. `verify_outcome_loose_status_matches_client` — `loose_status()`
aligns with echidnabot's `parse_proof_status`
3. `verify_proof_mutation_unknown_prover_returns_system_error` —
end-to-end execution; structured `SYSTEM_ERROR` outcome
4. `prover_status_unknown_prover_reports_unavailable` — query path;
`available: false` + populated message
5. `suggest_tactics_mutation_unknown_prover_errors` — top-level GraphQL
error (non-null list has no in-band error slot)
6. `suggest_tactics_is_a_mutation` — guard against accidental kind
drift; `suggestTactics` on QueryRoot must not resolve
7. `suggest_tactics_by_proof_id_is_a_query` — renamed legacy query still
registered on QueryRoot
8. `introspection_exposes_all_three_new_operations` — the contract
assertion #180 asked for

Baseline lib tests unchanged: **1070 passed** (`cargo test --lib -p
echidna`).

## Don't-touched

- GraphQL playground / introspection guards
- Existing mutations `submitProof` / `applyTactic` / `cancelProof`
- Existing queries `provers` / `proofState` / `listProofs` / `health`
- REST handlers (already had the typed taxonomy; this PR is
GraphQL-only)
- echidnabot client (separate follow-up to consume the new typed
`outcome`)

## Test plan

- [x] `cargo build -p echidna-graphql` — clean
- [x] `cargo test -p echidna-graphql` — 8/8 new tests pass
- [x] `cargo test --lib -p echidna` — 1070 baseline tests still pass
- [ ] Manual: spin up server, hit `verifyProof` + `suggestTactics` +
`proverStatus` from echidnabot client in `EchidnaApiMode::Graphql`
(deferred — needs a follow-up in echidnabot for the typed `outcome`
consumption)

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/interfaces/README.md

@@ -10,9 +10,14 @@ This directory contains all interface implementations for ECHIDNA theorem provin
 - **Playground:** http://localhost:8081/
 - **Features:**
   - Type-safe schema with all 17 provers
-  - Queries: provers, proof_state, list_proofs, suggest_tactics
-  - Mutations: submit_proof, apply_tactic, cancel_proof
-  - Subscriptions: proof_updates (planned)
+  - Queries: `provers`, `proofState`, `listProofs`,
+    `suggestTacticsByProofId` (renamed from `suggestTactics` 2026-06-01,
+    issue #180), `proverStatus`, `health`
+  - Mutations: `submitProof`, `applyTactic`, `cancelProof`,
+    `verifyProof` (synchronous one-shot, returns typed `VerifyOutcome` +
+    optional `mode` / `smtStatus`), `suggestTactics(prover, context,
+    goalState)` (ad-hoc, ML-backed)
+  - Subscriptions: `proofUpdates` (planned)
 
 ### gRPC (`grpc/`)
 - **Framework:** Rust + tonic + Protocol Buffers

src/interfaces/graphql/resolvers.rs

@@ -6,6 +6,7 @@ use echidna::core::{
 };
 use echidna::provers::{ProverBackend, ProverConfig, ProverFactory, ProverKind as CoreProverKind};
 use std::collections::HashMap;
+use std::str::FromStr;
 use std::sync::Arc;
 use tokio::sync::{Mutex, RwLock};
 
@@ -594,6 +595,90 @@ impl EchidnaContext {
         Ok(result)
     }
 
+    /// Suggest tactics for an ad-hoc `(prover, context, goal_state)` triple
+    /// without requiring an existing proof session.
+    ///
+    /// Added 2026-06-01 for the `suggestTactics(prover, context,
+    /// goalState)` mutation (issue #180). The signature mirrors the
+    /// echidnabot client's expectation. Tries the Julia ML coprocessor
+    /// first; falls back to constructing a one-shot prover backend and
+    /// calling its `suggest_tactics` against a fresh parse of the goal.
+    pub async fn suggest_tactics_for_goal(
+        &self,
+        prover: &str,
+        context: &str,
+        goal_state: &str,
+        limit: usize,
+    ) -> anyhow::Result<Vec<crate::schema::SuggestedTactic>> {
+        // Parse the free-form prover string (same alias set as the REST handler).
+        let core_kind = CoreProverKind::from_str(prover)
+            .map_err(|e| anyhow::anyhow!("Unknown prover '{}': {}", prover, e))?;
+
+        // Try Julia ML first — the new shape ships `prover`/`context`/`goal`
+        // directly so the bridge can use whichever it prefers.
+        let ml_req = serde_json::json!({
+            "goal": goal_state,
+            "context": context,
+            "prover": format!("{:?}", core_kind),
+            "top_k": limit,
+        });
+
+        if let Ok(resp) = self
+            .ml_client
+            .post(format!("{}/suggest", self.ml_api_url))
+            .json(&ml_req)
+            .send()
+            .await
+        {
+            if resp.status().is_success() {
+                if let Ok(ml_resp) = resp.json::<serde_json::Value>().await {
+                    if let Some(arr) = ml_resp["suggestions"].as_array() {
+                        let suggestions: Vec<crate::schema::SuggestedTactic> = arr
+                            .iter()
+                            .filter_map(|s| {
+                                let name = s["tactic"].as_str()?;
+                                let confidence =
+                                    s["confidence"].as_f64().unwrap_or(0.5);
+                                let explanation =
+                                    s["explanation"].as_str().map(|t| t.to_string());
+                                Some(crate::schema::SuggestedTactic {
+                                    tactic: name.to_string(),
+                                    confidence,
+                                    explanation,
+                                })
+                            })
+                            .collect();
+
+                        if !suggestions.is_empty() {
+                            return Ok(suggestions);
+                        }
+                    }
+                }
+            }
+        }
+
+        // Fallback: spin up a one-shot prover backend and ask it.
+        let config = ProverConfig::default();
+        let backend = ProverFactory::create(core_kind, config)?;
+        // Prefer goal_state if non-empty (matches the REST `/api/suggest`
+        // fallback that the echidnabot client uses).
+        let content = if !goal_state.trim().is_empty() {
+            goal_state
+        } else {
+            context
+        };
+        let state = backend.parse_string(content).await?;
+        let tactics = backend.suggest_tactics(&state, limit).await?;
+        Ok(tactics
+            .into_iter()
+            .map(|t| crate::schema::SuggestedTactic {
+                tactic: format!("{:?}", t),
+                confidence: 0.5,
+                explanation: Some("Backend heuristic suggestion".to_string()),
+            })
+            .collect())
+    }
+
     pub async fn suggest_tactics(
         &self,
         proof_id: &str,