feat(cli): wire --diagnose flag into verify and prove subcommands

When --diagnose is set and a proof fails, emit_diagnostic() calls
prover.check() (which returns a ProverOutcome) then maps it through
diagnose_from_outcome() to produce a DiagnosticReport with failure
classification, human-readable explanation, and ordered suggestions.

Adds diagnose_from_outcome(prover, outcome) to proof_failure.rs —
maps all 8 ProverOutcome variants to FailureKind without a second
raw-output prover invocation. The --diagnose flag is available on
both `echidna verify` and `echidna prove`.

Usage: echidna verify --diagnose myproof.smt2 --prover z3

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

Author: hyperpolymath

src/rust/diagnostics/mod.rs

@@ -9,4 +9,4 @@ pub mod proof_failure;
 pub use corpus_monitor::{CorpusMetrics, CorpusMonitor};
 pub use health::{HealthStatus, ProverHealth, ModelHealth, CorpusHealth, DegradationMode};
 pub use gnn_training::{GnnTrainingMetrics, load_training_metrics, update_health_with_metrics};
-pub use proof_failure::{diagnose, DiagnosticReport, FailureKind, SourceLocation};
+pub use proof_failure::{diagnose, diagnose_from_outcome, DiagnosticReport, FailureKind, SourceLocation};

src/rust/diagnostics/proof_failure.rs

@@ -17,7 +17,7 @@
 
 use std::fmt;
 
-use crate::provers::ProverKind;
+use crate::provers::{outcome::ProverOutcome, ProverKind};
 
 /// Taxonomy of proof failure causes.
 #[derive(Debug, Clone, PartialEq, Eq)]
@@ -204,6 +204,70 @@ pub fn diagnose(prover: ProverKind, raw_output: &str) -> DiagnosticReport {
     }
 }
 
+/// Produce a `DiagnosticReport` from a `ProverOutcome` returned by `check()`.
+///
+/// This avoids a second prover invocation: if the caller already has a
+/// `ProverOutcome` (e.g. from `--diagnose` mode which calls `check()` instead
+/// of `verify_proof()`), map it directly into a report without re-running.
+pub fn diagnose_from_outcome(prover: ProverKind, outcome: &ProverOutcome) -> DiagnosticReport {
+    let kind = match outcome {
+        ProverOutcome::Proved { .. } => {
+            // Should not reach diagnose on success, but handle gracefully.
+            return DiagnosticReport {
+                prover,
+                kind: FailureKind::Unknown { raw_output: "Proved — no failure to diagnose.".into() },
+                explanation: "The prover succeeded. No diagnostic needed.".into(),
+                suggestions: vec![],
+                raw_excerpt: String::new(),
+            };
+        },
+        ProverOutcome::NoProofFound { reason, .. } => FailureKind::UnsolvedGoal {
+            goal_summary: reason.clone(),
+        },
+        ProverOutcome::Timeout { limit_secs } => FailureKind::Timeout {
+            limit_secs: Some(*limit_secs),
+        },
+        ProverOutcome::InvalidInput { reason, location } => FailureKind::SyntaxError {
+            message: reason.clone(),
+            location: location.map(|offset| SourceLocation {
+                file: None,
+                line: None,
+                column: Some(offset as u32),
+            }),
+        },
+        ProverOutcome::UnsupportedFeature { feature } => FailureKind::ConfigError {
+            detail: format!("Unsupported feature: {}", feature),
+        },
+        ProverOutcome::InconsistentPremises { detail } => FailureKind::UnsolvedGoal {
+            goal_summary: Some(
+                detail.clone().unwrap_or_else(|| {
+                    "Premise set is inconsistent — proof is vacuously true.".into()
+                }),
+            ),
+        },
+        ProverOutcome::ProverError { detail, exit_code } => FailureKind::ProverCrash {
+            exit_code: *exit_code,
+            stderr_excerpt: detail.clone(),
+        },
+        ProverOutcome::SystemError { detail } => FailureKind::ConfigError {
+            detail: detail.clone(),
+        },
+    };
+
+    let (explanation, suggestions) = explain_and_suggest(prover, &kind);
+    let raw_excerpt = match outcome {
+        ProverOutcome::NoProofFound { reason, .. } => reason.clone().unwrap_or_default(),
+        ProverOutcome::ProverError { detail, .. } => detail.clone(),
+        ProverOutcome::SystemError { detail } => detail.clone(),
+        ProverOutcome::InvalidInput { reason, .. } => reason.clone(),
+        ProverOutcome::UnsupportedFeature { feature } => feature.clone(),
+        ProverOutcome::InconsistentPremises { detail } => detail.clone().unwrap_or_default(),
+        _ => String::new(),
+    };
+
+    DiagnosticReport { prover, kind, explanation, suggestions, raw_excerpt }
+}
+
 // ---------------------------------------------------------------------------
 // Per-prover diagnostic parsers
 // ---------------------------------------------------------------------------

src/rust/main.rs

@@ -7,7 +7,10 @@
 
 use anyhow::{Context, Result};
 use clap::{Parser, Subcommand};
-use echidna::{ProverConfig, ProverKind};
+use echidna::{
+    diagnostics::proof_failure::diagnose_from_outcome, provers::ProverBackend, ProverConfig,
+    ProverKind,
+};
 use indicatif::{ProgressBar, ProgressStyle};
 use std::path::PathBuf;
 use tracing::{info, warn};
@@ -66,6 +69,10 @@ enum Commands {
         /// Library paths
         #[arg(long)]
         library: Vec<PathBuf>,
+
+        /// On failure, run diagnostics and explain why the proof failed
+        #[arg(long)]
+        diagnose: bool,
     },
 
     /// Verify an existing proof
@@ -88,6 +95,10 @@ enum Commands {
         /// Library paths
         #[arg(long)]
         library: Vec<PathBuf>,
+
+        /// On failure, run diagnostics and explain why the proof failed
+        #[arg(long)]
+        diagnose: bool,
     },
 
     /// Search theorem libraries
@@ -172,9 +183,10 @@ async fn main() -> Result<()> {
             neural,
             executable,
             library,
+            diagnose,
         } => {
             prove_command(
-                file, prover, timeout, neural, executable, library, &formatter,
+                file, prover, timeout, neural, executable, library, diagnose, &formatter,
             )
             .await?;
         },
@@ -185,8 +197,9 @@ async fn main() -> Result<()> {
             timeout,
             executable,
             library,
+            diagnose,
         } => {
-            verify_command(file, prover, timeout, executable, library, &formatter).await?;
+            verify_command(file, prover, timeout, executable, library, diagnose, &formatter).await?;
         },
 
         Commands::Search {
@@ -246,40 +259,29 @@ async fn prove_command(
     neural: bool,
     executable: Option<PathBuf>,
     library: Vec<PathBuf>,
+    diagnose: bool,
     formatter: &OutputFormatter,
 ) -> Result<()> {
     info!("Starting proof for: {}", file.display());
 
-    // Detect or use specified prover
     let kind = detect_prover(prover_kind, &file)?;
-
-    // Create prover configuration
     let config = create_config(kind, timeout, neural, executable, library)?;
-
-    // Create prover backend
     let prover = echidna::provers::ProverFactory::create(kind, config)
         .context("Failed to create prover backend")?;
 
-    // Show progress
     let pb = create_progress_bar("Parsing proof file...");
-
-    // Parse the proof file
     let state = prover
         .parse_file(file.clone())
         .await
         .context("Failed to parse proof file")?;
 
     pb.set_message("Verifying proof...");
-
-    // Verify the proof
     let result = prover
         .verify_proof(&state)
         .await
         .context("Failed to verify proof")?;
-
     pb.finish_and_clear();
 
-    // Output result
     if result {
         formatter.success(&format!(
             "✓ Proof verified successfully for {}",
@@ -292,57 +294,70 @@ async fn prove_command(
             file.display()
         ))?;
         formatter.output_proof_state(&state)?;
+        if diagnose {
+            emit_diagnostic(kind, &*prover, &state, formatter).await;
+        }
         std::process::exit(1);
     }
 
     Ok(())
 }
 
+/// Run `check()` on the prover and display a structured diagnostic report.
+///
+/// Called after a failed `verify_proof()` when `--diagnose` is active.
+/// Uses the richer `ProverOutcome` returned by `check()` to produce an
+/// actionable report via `diagnose_from_outcome`.
+async fn emit_diagnostic(
+    kind: ProverKind,
+    prover: &dyn ProverBackend,
+    state: &echidna::core::ProofState,
+    formatter: &OutputFormatter,
+) {
+    let outcome = match prover.check(state).await {
+        Ok(o) => o,
+        Err(e) => {
+            let _ = formatter.error(&format!("[diagnose] could not run check(): {}", e));
+            return;
+        },
+    };
+    let report = diagnose_from_outcome(kind, &outcome);
+    let _ = formatter.info("\n--- Proof Failure Diagnostic ---");
+    let _ = formatter.info(&report.display());
+}
+
 /// Verify command implementation
 async fn verify_command(
     file: PathBuf,
     prover_kind: Option<ProverKind>,
     timeout: u64,
     executable: Option<PathBuf>,
     library: Vec<PathBuf>,
+    diagnose: bool,
     formatter: &OutputFormatter,
 ) -> Result<()> {
     info!("Verifying proof: {}", file.display());
 
-    // Detect or use specified prover
     let kind = detect_prover(prover_kind, &file)?;
-
-    // Create prover configuration
     let config = create_config(kind, timeout, true, executable, library)?;
-
-    // Create prover backend
     let prover = echidna::provers::ProverFactory::create(kind, config)
         .context("Failed to create prover backend")?;
 
-    // Show progress
     let pb = create_progress_bar("Parsing proof file...");
-
-    // Parse the proof file
     let state = prover
         .parse_file(file.clone())
         .await
         .context("Failed to parse proof file")?;
 
     pb.set_message("Verifying proof...");
-
-    // Verify the proof
     let result = prover
         .verify_proof(&state)
         .await
         .context("Failed to verify proof")?;
-
     pb.finish_and_clear();
 
-    // Output result
     if result {
         formatter.success(&format!("✓ Proof is valid: {}", file.display()))?;
-
-        // Show proof statistics
         formatter.info(&format!("Goals: {}", state.goals.len()))?;
         formatter.info(&format!("Tactics: {}", state.proof_script.len()))?;
         formatter.info(&format!(
@@ -351,6 +366,9 @@ async fn verify_command(
         ))?;
     } else {
         formatter.error(&format!("✗ Proof is invalid: {}", file.display()))?;
+        if diagnose {
+            emit_diagnostic(kind, &*prover, &state, formatter).await;
+        }
         std::process::exit(1);
     }