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

[hyperpolymath]

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 seam(echidnabot): GraphQL contract mismatch — client queries 3 ops that the server does not expose #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

• cargo build -p echidna-graphql — clean
• cargo test -p echidna-graphql — 8/8 new tests pass
• 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

[github-actions]

🔍 Hypatia Security Scan

Findings: 246 issues detected

Severity	Count
🔴 Critical	12
🟠 High	75
🟡 Medium	159

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in agda-meta-checker.yml",
    "type": "missing_timeout_minutes",
    "file": "agda-meta-checker.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cargo-audit.yml",
    "type": "missing_timeout_minutes",
    "file": "cargo-audit.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in chapel-ci.yml",
    "type": "missing_timeout_minutes",
    "file": "chapel-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in chapel-ci.yml",
    "type": "missing_timeout_minutes",
    "file": "chapel-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in chapel-ci.yml",
    "type": "missing_timeout_minutes",
    "file": "chapel-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in chapel-ci.yml",
    "type": "missing_timeout_minutes",
    "file": "chapel-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence