diff --git a/src/interfaces/README.md b/src/interfaces/README.md index 25f41b3d..8af0a0c1 100644 --- a/src/interfaces/README.md +++ b/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 diff --git a/src/interfaces/graphql/resolvers.rs b/src/interfaces/graphql/resolvers.rs index 88b17e1b..4feee593 100644 --- a/src/interfaces/graphql/resolvers.rs +++ b/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> { + // 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::().await { + if let Some(arr) = ml_resp["suggestions"].as_array() { + let suggestions: Vec = 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, diff --git a/src/interfaces/graphql/schema.rs b/src/interfaces/graphql/schema.rs index 10eee71d..387a5117 100644 --- a/src/interfaces/graphql/schema.rs +++ b/src/interfaces/graphql/schema.rs @@ -3,7 +3,9 @@ use async_graphql::{Context, Enum, Object, Result, SimpleObject}; use echidna::core::{Tactic as CoreTactic, TacticResult as CoreTacticResult, Term}; -use echidna::provers::ProverKind as CoreProverKind; +use echidna::provers::{ProverConfig, ProverFactory, ProverKind as CoreProverKind}; +use std::str::FromStr; +use std::time::Instant; use crate::resolvers::EchidnaContext; @@ -201,6 +203,131 @@ pub struct ProverInfo { pub available: bool, } +// ============================================================================= +// Types added 2026-06-01 for echidnabot ↔ echidna seam (issue #180). +// +// These mirror the typed taxonomy now surfaced by REST `/api/verify` +// (`outcome`, optional `mode` / `smt_status`) and the suggestion shape +// the echidnabot Julia-ML client expects (`tactic` / `confidence` / +// `explanation`). +// ============================================================================= + +/// Typed outcome from a verifyProof call. +/// +/// Mirrors the `outcome` field on REST `/api/verify` so GraphQL clients +/// can distinguish e.g. `Timeout` from `NoProofFound` without parsing +/// strings. Added 2026-06-01 (issue #180). +#[derive(Debug, Clone, Copy, Enum, Eq, PartialEq)] +pub enum VerifyOutcome { + /// Prover returned a verified proof. + Proved, + /// Prover finished without a proof. + NoProofFound, + /// Input could not be parsed or was empty. + InvalidInput, + /// Prover does not support a feature in the input. + UnsupportedFeature, + /// Prover exhausted its time budget. + Timeout, + /// Premises are mutually inconsistent. + InconsistentPremises, + /// Prover exited with an error. + ProverError, + /// Echidna-side error (FFI / I/O / sandbox). + SystemError, +} + +impl VerifyOutcome { + /// Map the REST `outcome: String` representation onto the enum. + pub fn from_rest_str(s: &str) -> VerifyOutcome { + match s.to_uppercase().as_str() { + "PROVED" => VerifyOutcome::Proved, + "NO_PROOF_FOUND" => VerifyOutcome::NoProofFound, + "INVALID_INPUT" => VerifyOutcome::InvalidInput, + "UNSUPPORTED_FEATURE" => VerifyOutcome::UnsupportedFeature, + "TIMEOUT" => VerifyOutcome::Timeout, + "INCONSISTENT_PREMISES" => VerifyOutcome::InconsistentPremises, + "PROVER_ERROR" => VerifyOutcome::ProverError, + _ => VerifyOutcome::SystemError, + } + } + + /// Loose status string for echidnabot's existing GraphQL deserializer, + /// which calls `parse_proof_status` and maps `"VERIFIED" | "PASS" | + /// "SUCCESS"` → `Verified`, `"FAILED" | "FAIL"` → `Failed`, etc. + pub fn loose_status(self) -> &'static str { + match self { + VerifyOutcome::Proved => "VERIFIED", + VerifyOutcome::NoProofFound => "FAILED", + VerifyOutcome::InvalidInput => "FAILED", + VerifyOutcome::UnsupportedFeature => "ERROR", + VerifyOutcome::Timeout => "TIMEOUT", + VerifyOutcome::InconsistentPremises => "ERROR", + VerifyOutcome::ProverError => "ERROR", + VerifyOutcome::SystemError => "ERROR", + } + } +} + +/// Result of the `verifyProof` mutation. +/// +/// The `status`, `message`, `proverOutput`, `durationMs`, and `artifacts` +/// fields match echidnabot's existing client-side `VerifyProofData`. The +/// `outcome`, `mode`, and `smtStatus` fields surface the typed REST +/// taxonomy so future clients no longer need to round-trip via `/api/verify` +/// to disambiguate Timeout vs NoProofFound. +#[derive(Debug, Clone, SimpleObject)] +pub struct VerifyProofResult { + /// Loose status string for backward compatibility with echidnabot's + /// existing client (`"VERIFIED" | "FAILED" | "TIMEOUT" | "ERROR"`). + pub status: String, + /// Human-readable message. + pub message: String, + /// Captured stdout/stderr from the prover backend. + pub prover_output: String, + /// Wall-clock duration in milliseconds. + pub duration_ms: u64, + /// Output artifacts (proof certificates, intermediate files). + pub artifacts: Vec, + /// Typed outcome — see `VerifyOutcome`. + pub outcome: VerifyOutcome, + /// Optional dispatch mode (e.g. `"smt-query"` for raw SMT-LIB). + pub mode: Option, + /// Optional SMT solver status (`"sat" | "unsat" | "unknown"`). + pub smt_status: Option, +} + +/// A single suggested tactic from the Julia ML coprocessor (or fallback). +/// +/// Distinct from the existing `Tactic` SimpleObject (which is returned by +/// `suggestTacticsByProofId`) — that one carries `name`/`args`/`description`, +/// this one carries the rank-aware `tactic`/`confidence`/`explanation` shape +/// the echidnabot client expects. +#[derive(Debug, Clone, SimpleObject)] +pub struct SuggestedTactic { + /// The tactic name (e.g. `"intro"`, `"apply foo"`). + pub tactic: String, + /// Confidence score from the ML coprocessor in `[0.0, 1.0]`. + pub confidence: f64, + /// Optional natural-language explanation for the suggestion. + pub explanation: Option, +} + +/// Per-prover status, as returned by the `proverStatus` query. +/// +/// Complements the existing `provers` list-query, which returns availability +/// for every prover. Use `proverStatus` when you only care about a single +/// prover and want to avoid the full list cost. +#[derive(Debug, Clone, SimpleObject)] +pub struct ProverStatusInfo { + /// True when the prover backend is constructable and its executable + /// is reachable. + pub available: bool, + /// Diagnostic message — version string when available, error text + /// when not. + pub message: Option, +} + pub struct QueryRoot; #[Object] @@ -315,8 +442,17 @@ impl QueryRoot { Ok(proofs) } - /// Get suggested tactics for a proof state - async fn suggest_tactics( + /// Get suggested tactics for an existing proof session by ID. + /// + /// **Renamed 2026-06-01 (issue #180)**: this operation used to be + /// exposed as `suggestTactics`. It was renamed to + /// `suggestTacticsByProofId` to free the `suggestTactics` name for the + /// new mutation that the echidnabot client expects (which takes + /// `prover`/`context`/`goalState` and returns + /// `[SuggestedTactic]`). Callers that were using the old + /// `query { suggestTactics(proofId, limit) }` shape must update to + /// `query { suggestTacticsByProofId(proofId, limit) }`. + async fn suggest_tactics_by_proof_id( &self, ctx: &Context<'_>, proof_id: String, @@ -341,6 +477,50 @@ impl QueryRoot { .collect()) } + /// Per-prover availability/health. + /// + /// Added 2026-06-01 for issue #180. Complements the `provers` + /// list-query for the common single-prover case. Backend construction + /// + a `version()` probe is the strongest "available right now" + /// signal we can give without actually dispatching a proof. + async fn prover_status( + &self, + _ctx: &Context<'_>, + prover: String, + ) -> Result { + let core_kind = match CoreProverKind::from_str(&prover) { + Ok(k) => k, + Err(e) => { + return Ok(ProverStatusInfo { + available: false, + message: Some(format!("Unknown prover '{}': {}", prover, e)), + }); + }, + }; + + let config = ProverConfig::default(); + let backend = match ProverFactory::create(core_kind, config) { + Ok(b) => b, + Err(e) => { + return Ok(ProverStatusInfo { + available: false, + message: Some(format!("Failed to construct backend: {}", e)), + }); + }, + }; + + match backend.version().await { + Ok(v) => Ok(ProverStatusInfo { + available: true, + message: Some(v), + }), + Err(e) => Ok(ProverStatusInfo { + available: false, + message: Some(format!("Version probe failed: {}", e)), + }), + } + } + /// Health check async fn health(&self) -> String { "OK".to_string() @@ -462,6 +642,144 @@ impl MutationRoot { let mut sessions = echidna_ctx.sessions.write().await; Ok(sessions.remove(&proof_id).is_some()) } + + /// Synchronous one-shot proof verification. + /// + /// Added 2026-06-01 (issue #180). Matches the echidnabot client's + /// `verifyProof(prover, content)` signature and returns the same + /// fields the client already deserializes (`status`, `message`, + /// `proverOutput`, `durationMs`, `artifacts`), plus the typed + /// `outcome` / `mode` / `smtStatus` fields that surface the REST + /// `/api/verify` taxonomy through GraphQL. + /// + /// `prover` is a free-form string parsed via `CoreProverKind::from_str` + /// (same set of aliases as the REST handler). Unknown prover names + /// produce a `SystemError` outcome rather than a GraphQL error so the + /// client gets a structured response in every case. + async fn verify_proof( + &self, + _ctx: &Context<'_>, + prover: String, + content: String, + ) -> Result { + let started = Instant::now(); + + let core_kind = match CoreProverKind::from_str(&prover) { + Ok(k) => k, + Err(e) => { + let duration_ms = started.elapsed().as_millis() as u64; + return Ok(VerifyProofResult { + status: VerifyOutcome::SystemError.loose_status().to_string(), + message: format!("Unknown prover '{}': {}", prover, e), + prover_output: String::new(), + duration_ms, + artifacts: Vec::new(), + outcome: VerifyOutcome::SystemError, + mode: None, + smt_status: None, + }); + }, + }; + + let config = ProverConfig::default(); + let backend = match ProverFactory::create(core_kind, config) { + Ok(b) => b, + Err(e) => { + let duration_ms = started.elapsed().as_millis() as u64; + return Ok(VerifyProofResult { + status: VerifyOutcome::SystemError.loose_status().to_string(), + message: format!("Failed to construct backend: {}", e), + prover_output: String::new(), + duration_ms, + artifacts: Vec::new(), + outcome: VerifyOutcome::SystemError, + mode: None, + smt_status: None, + }); + }, + }; + + // Parse — failures map onto INVALID_INPUT, matching REST semantics. + let state = match backend.parse_string(&content).await { + Ok(s) => s, + Err(_) => { + let duration_ms = started.elapsed().as_millis() as u64; + return Ok(VerifyProofResult { + status: VerifyOutcome::InvalidInput.loose_status().to_string(), + message: "Parse failed".to_string(), + prover_output: String::new(), + duration_ms, + artifacts: Vec::new(), + outcome: VerifyOutcome::InvalidInput, + mode: None, + smt_status: None, + }); + }, + }; + + match backend.verify_proof(&state).await { + Ok(valid) => { + let duration_ms = started.elapsed().as_millis() as u64; + let outcome = if valid { + VerifyOutcome::Proved + } else { + VerifyOutcome::NoProofFound + }; + Ok(VerifyProofResult { + status: outcome.loose_status().to_string(), + message: if valid { + "Proof verified successfully".to_string() + } else { + "Proof verification failed".to_string() + }, + prover_output: String::new(), + duration_ms, + artifacts: Vec::new(), + outcome, + mode: None, + smt_status: None, + }) + }, + Err(e) => { + let duration_ms = started.elapsed().as_millis() as u64; + Ok(VerifyProofResult { + status: VerifyOutcome::ProverError.loose_status().to_string(), + message: format!("Verification error: {}", e), + prover_output: String::new(), + duration_ms, + artifacts: Vec::new(), + outcome: VerifyOutcome::ProverError, + mode: None, + smt_status: None, + }) + }, + } + } + + /// Request tactic suggestions for an ad-hoc goal, without a proof + /// session. + /// + /// **Added 2026-06-01 (issue #180)**. Matches the echidnabot client's + /// `suggestTactics(prover, context, goalState)` signature. The + /// previous query named `suggestTactics(proofId, limit)` has been + /// renamed to `suggestTacticsByProofId` (see that resolver's docstring). + /// + /// This is a mutation rather than a query because it can trigger + /// expensive ML-coprocessor work, mirroring the client's contract. + async fn suggest_tactics( + &self, + ctx: &Context<'_>, + prover: String, + context: String, + goal_state: String, + ) -> Result> { + let echidna_ctx = ctx.data::()?; + let suggestions = echidna_ctx + .suggest_tactics_for_goal(&prover, &context, &goal_state, 5) + .await + .map_err(|e| async_graphql::Error::new(e.to_string()))?; + Ok(suggestions) + } } // ========== Helpers ========== @@ -776,3 +1094,277 @@ fn gql_to_core(kind: &ProverKind) -> CoreProverKind { ProverKind::CryptoVerif => CoreProverKind::CryptoVerif, } } + +// ============================================================================= +// Tests for the operations added/renamed for echidnabot ↔ echidna seam (#180). +// ============================================================================= + +#[cfg(test)] +mod tests { + use super::*; + use crate::resolvers::EchidnaContext; + use async_graphql::{EmptySubscription, Request, Schema, Value}; + + fn build_schema() -> Schema { + Schema::build(QueryRoot, MutationRoot, EmptySubscription) + .data(EchidnaContext::new()) + .finish() + } + + /// `verify_outcome_from_rest_str` round-trip — every taxon the REST + /// `/api/verify` handler emits must map onto a distinct enum variant. + #[test] + fn verify_outcome_from_rest_str_covers_taxonomy() { + assert_eq!(VerifyOutcome::from_rest_str("PROVED"), VerifyOutcome::Proved); + assert_eq!( + VerifyOutcome::from_rest_str("NO_PROOF_FOUND"), + VerifyOutcome::NoProofFound + ); + assert_eq!( + VerifyOutcome::from_rest_str("INVALID_INPUT"), + VerifyOutcome::InvalidInput + ); + assert_eq!( + VerifyOutcome::from_rest_str("UNSUPPORTED_FEATURE"), + VerifyOutcome::UnsupportedFeature + ); + assert_eq!(VerifyOutcome::from_rest_str("TIMEOUT"), VerifyOutcome::Timeout); + assert_eq!( + VerifyOutcome::from_rest_str("INCONSISTENT_PREMISES"), + VerifyOutcome::InconsistentPremises + ); + assert_eq!( + VerifyOutcome::from_rest_str("PROVER_ERROR"), + VerifyOutcome::ProverError + ); + // Unknown / non-canonical falls through to SystemError. + assert_eq!( + VerifyOutcome::from_rest_str("WAT"), + VerifyOutcome::SystemError + ); + assert_eq!( + VerifyOutcome::from_rest_str(""), + VerifyOutcome::SystemError + ); + } + + /// `loose_status` covers the four labels echidnabot's existing + /// `parse_proof_status` already maps onto `ProofStatus`. + #[test] + fn verify_outcome_loose_status_matches_client() { + assert_eq!(VerifyOutcome::Proved.loose_status(), "VERIFIED"); + assert_eq!(VerifyOutcome::NoProofFound.loose_status(), "FAILED"); + assert_eq!(VerifyOutcome::Timeout.loose_status(), "TIMEOUT"); + assert_eq!(VerifyOutcome::ProverError.loose_status(), "ERROR"); + } + + /// `verifyProof` mutation — unknown prover names return a structured + /// `SystemError` outcome rather than a GraphQL error, so the client + /// always gets the contract-shaped response. + #[tokio::test] + async fn verify_proof_mutation_unknown_prover_returns_system_error() { + let schema = build_schema(); + let query = r#" + mutation { + verifyProof(prover: "definitely-not-a-prover", content: "x") { + status + outcome + message + durationMs + artifacts + mode + smtStatus + } + } + "#; + let resp = schema.execute(Request::new(query)).await; + assert!(resp.errors.is_empty(), "errors: {:?}", resp.errors); + + let data = match resp.data { + Value::Object(ref m) => m, + other => panic!("expected object, got {:?}", other), + }; + let vp = match data.get("verifyProof").expect("verifyProof field") { + Value::Object(m) => m, + other => panic!("expected object, got {:?}", other), + }; + + assert_eq!(vp.get("status"), Some(&Value::String("ERROR".to_string()))); + match vp.get("outcome") { + Some(Value::Enum(name)) => assert_eq!(name.as_str(), "SYSTEM_ERROR"), + other => panic!("expected enum SYSTEM_ERROR, got {:?}", other), + } + // mode/smtStatus should be null on this error path. + assert!(matches!(vp.get("mode"), Some(Value::Null))); + assert!(matches!(vp.get("smtStatus"), Some(Value::Null))); + // artifacts is an empty list, not null. + assert!(matches!(vp.get("artifacts"), Some(Value::List(v)) if v.is_empty())); + } + + /// `proverStatus` query — same SystemError-shape behaviour for an + /// unknown prover string (available: false, message populated). + #[tokio::test] + async fn prover_status_unknown_prover_reports_unavailable() { + let schema = build_schema(); + let query = r#" + query { + proverStatus(prover: "no-such-prover") { + available + message + } + } + "#; + let resp = schema.execute(Request::new(query)).await; + assert!(resp.errors.is_empty(), "errors: {:?}", resp.errors); + + let data = match resp.data { + Value::Object(ref m) => m, + other => panic!("expected object, got {:?}", other), + }; + let ps = match data.get("proverStatus").expect("proverStatus field") { + Value::Object(m) => m, + other => panic!("expected object, got {:?}", other), + }; + assert_eq!(ps.get("available"), Some(&Value::Boolean(false))); + match ps.get("message") { + Some(Value::String(msg)) => assert!( + msg.contains("Unknown prover"), + "message should mention unknown prover, got: {}", + msg + ), + other => panic!("expected non-null message, got {:?}", other), + } + } + + /// `suggestTactics(prover, context, goalState)` mutation — same + /// SystemError path for unknown provers: the call fails *before* + /// dialing the ML coprocessor, so the response shape stays + /// `errors`-populated (a GraphQL error is acceptable here because + /// the client expects `[SuggestedTactic!]!`, a non-null list, and + /// has no field to encode "unknown prover"). + #[tokio::test] + async fn suggest_tactics_mutation_unknown_prover_errors() { + let schema = build_schema(); + let query = r#" + mutation { + suggestTactics(prover: "no-such-prover", context: "", goalState: "x") { + tactic + confidence + explanation + } + } + "#; + let resp = schema.execute(Request::new(query)).await; + // Unknown prover -> resolver Err -> top-level GraphQL error. + assert!(!resp.errors.is_empty(), "expected an error for unknown prover"); + assert!(resp.errors[0].message.contains("Unknown prover")); + } + + /// `suggestTactics(prover, context, goalState)` is a *mutation*, not + /// a query — guard against accidental kind drift (the rename trick + /// only works if the new operation lives on MutationRoot, freeing + /// the QueryRoot name). + #[tokio::test] + async fn suggest_tactics_is_a_mutation() { + let schema = build_schema(); + // Same name, but issued as a *query* — must fail with "Unknown + // field" because the query root no longer exposes it. + let query = r#" + query { + suggestTactics(prover: "coq", context: "", goalState: "x") { + tactic + } + } + "#; + let resp = schema.execute(Request::new(query)).await; + assert!( + !resp.errors.is_empty(), + "suggestTactics on QueryRoot must not resolve" + ); + } + + /// `suggestTacticsByProofId` — the renamed legacy query — must + /// continue to exist on QueryRoot so callers can update their + /// schema with a pure name change. + #[tokio::test] + async fn suggest_tactics_by_proof_id_is_a_query() { + let schema = build_schema(); + // Missing session ID, so we expect an error from the resolver + // body (not a "field not found" error) — that's how we know + // the field is registered. + let query = r#" + query { + suggestTacticsByProofId(proofId: "no-such-session", limit: 1) { + name + } + } + "#; + let resp = schema.execute(Request::new(query)).await; + assert!(!resp.errors.is_empty()); + let msg = &resp.errors[0].message; + assert!( + msg.contains("Session not found") || msg.contains("session"), + "expected a session-not-found error from the resolver, got: {}", + msg + ); + } + + /// Schema introspection — all three new operations must show up + /// under the right roots with the expected argument names. This is + /// the "contract assertion" the issue body asked for. + #[tokio::test] + async fn introspection_exposes_all_three_new_operations() { + let schema = build_schema(); + + // Mutations: verifyProof + suggestTactics (new shape). + let q = r#" + { + __type(name: "MutationRoot") { + fields { + name + args { name type { name kind ofType { name kind } } } + } + } + } + "#; + let resp = schema.execute(Request::new(q)).await; + assert!(resp.errors.is_empty(), "introspection errors: {:?}", resp.errors); + let body = serde_json::to_string(&resp.data).unwrap(); + assert!(body.contains("\"verifyProof\""), "missing verifyProof mutation"); + assert!( + body.contains("\"suggestTactics\""), + "missing new suggestTactics mutation" + ); + // verifyProof must take (prover, content); suggestTactics must + // take (prover, context, goalState). + assert!(body.contains("\"prover\"")); + assert!(body.contains("\"content\"")); + assert!(body.contains("\"context\"")); + assert!(body.contains("\"goalState\"")); + + // Queries: proverStatus + suggestTacticsByProofId. + let q = r#" + { + __type(name: "QueryRoot") { + fields { name args { name } } + } + } + "#; + let resp = schema.execute(Request::new(q)).await; + assert!(resp.errors.is_empty()); + let body = serde_json::to_string(&resp.data).unwrap(); + assert!(body.contains("\"proverStatus\""), "missing proverStatus query"); + assert!( + body.contains("\"suggestTacticsByProofId\""), + "missing renamed suggestTacticsByProofId query" + ); + // The query-side `suggestTactics` (old name) must NOT exist on QueryRoot. + // Crude but sufficient: assert that the literal `"name":"suggestTactics"` + // pair does not appear among the QueryRoot fields (it would otherwise + // shadow the new mutation by introspection ambiguity). + assert!( + !body.contains("\"name\":\"suggestTactics\""), + "old suggestTactics query must be renamed away from QueryRoot" + ); + } +}