diff --git a/src/rust/provers/alloy.rs b/src/rust/provers/alloy.rs index a0a76ec..fcde4b5 100644 --- a/src/rust/provers/alloy.rs +++ b/src/rust/provers/alloy.rs @@ -228,14 +228,24 @@ impl ProverBackend for AlloyBackend { } async fn parse_file(&self, path: PathBuf) -> Result { - let content = tokio::fs::read_to_string(path) + let content = tokio::fs::read_to_string(&path) .await .context("Failed to read Alloy file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { - self.parse_alloy(content) + let mut state = self.parse_alloy(content)?; + state.metadata.insert( + "alloy_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result { @@ -293,7 +303,35 @@ impl ProverBackend for AlloyBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { - let alloy_code = self.to_alloy(state)?; + // Prefer the original .als source; `to_alloy(state)` round-trips + // through the generic Term IR and cannot reconstruct real models. + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .map_err(|_| anyhow!("Alloy timed out after {} seconds", self.config.timeout))? + .context("Failed to execute Alloy")?; + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + let combined = format!("{}\n{}", stdout, stderr); + return self.parse_result(&combined); + } + + let alloy_code = if let Some(src) = state + .metadata + .get("alloy_source") + .and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_alloy(state)? + }; // Write Alloy to a temporary file let tmp_dir = diff --git a/src/rust/provers/cbmc.rs b/src/rust/provers/cbmc.rs index 45301b7..a28f3d3 100644 --- a/src/rust/provers/cbmc.rs +++ b/src/rust/provers/cbmc.rs @@ -246,14 +246,24 @@ impl ProverBackend for CBMCBackend { } async fn parse_file(&self, path: PathBuf) -> Result { - let content = tokio::fs::read_to_string(path) + let content = tokio::fs::read_to_string(&path) .await .context("Failed to read C source file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { - self.parse_c_source(content) + let mut state = self.parse_c_source(content)?; + state.metadata.insert( + "cbmc_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result { @@ -321,7 +331,47 @@ impl ProverBackend for CBMCBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { - let c_source = self.to_c_source(state)?; + // Determine unwind bound from metadata or use default + let unwind = state + .metadata + .get("cbmc_unwind_bound") + .and_then(|v| v.as_str()) + .and_then(|s| s.parse::().ok()) + .unwrap_or(self.unwind_bound); + + // Prefer the original .c source — `to_c_source(state)` round-trips + // through the generic Term IR and silently mangles anything real. + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 10), + Command::new(&self.config.executable) + .arg("--unwind") + .arg(format!("{}", unwind)) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .map_err(|_| { + anyhow!( + "CBMC verification timed out after {} seconds", + self.config.timeout + ) + })? + .context("Failed to execute CBMC")?; + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + let combined = format!("{}\n{}", stdout, stderr); + return self.parse_result(&combined); + } + + let c_source = if let Some(src) = state.metadata.get("cbmc_source").and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_c_source(state)? + }; // Write C source to a temporary file (CBMC requires a file) let tmp_dir = @@ -331,14 +381,6 @@ impl ProverBackend for CBMCBackend { .await .context("Failed to write temporary C file")?; - // Determine unwind bound from metadata or use default - let unwind = state - .metadata - .get("cbmc_unwind_bound") - .and_then(|v| v.as_str()) - .and_then(|s| s.parse::().ok()) - .unwrap_or(self.unwind_bound); - // Run cbmc with unwind bound let output = tokio::time::timeout( tokio::time::Duration::from_secs(self.config.timeout + 10), diff --git a/src/rust/provers/chuffed.rs b/src/rust/provers/chuffed.rs index ea7a63d..0d56abc 100644 --- a/src/rust/provers/chuffed.rs +++ b/src/rust/provers/chuffed.rs @@ -46,11 +46,20 @@ impl ProverBackend for ChuffedBackend { Ok("chuffed".to_string()) } async fn parse_file(&self, path: PathBuf) -> Result { - self.parse_string(&tokio::fs::read_to_string(path).await?) - .await + let content = tokio::fs::read_to_string(&path).await?; + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "chuffed_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let l = line.trim(); if !l.is_empty() && !l.starts_with("%") { @@ -74,7 +83,34 @@ impl ProverBackend for ChuffedBackend { Err(anyhow::anyhow!("Chuffed: CP solver, not interactive")) } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + // Prefer the original FlatZinc source — reconstructing from the + // Term IR via `to_input_format` loses all constraint structure. + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("Chuffed timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state + .metadata + .get("chuffed_source") + .and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .stdin(Stdio::piped()) .stdout(Stdio::piped()) diff --git a/src/rust/provers/dafny.rs b/src/rust/provers/dafny.rs index a7c26e6..82f99ae 100644 --- a/src/rust/provers/dafny.rs +++ b/src/rust/provers/dafny.rs @@ -55,11 +55,20 @@ impl ProverBackend for DafnyBackend { .to_string()) } async fn parse_file(&self, path: PathBuf) -> Result { - self.parse_string(&tokio::fs::read_to_string(path).await?) - .await + let content = tokio::fs::read_to_string(&path).await?; + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "dafny_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let l = line.trim(); if l.is_empty() || l.starts_with("//") { @@ -86,7 +95,29 @@ impl ProverBackend for DafnyBackend { )) } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg("verify") + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("Dafny timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state.metadata.get("dafny_source").and_then(|v| v.as_str()) { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .stdin(Stdio::piped()) .stdout(Stdio::piped()) diff --git a/src/rust/provers/dreal.rs b/src/rust/provers/dreal.rs index 285f423..1e080c7 100644 --- a/src/rust/provers/dreal.rs +++ b/src/rust/provers/dreal.rs @@ -316,13 +316,23 @@ impl ProverBackend for DRealBackend { .await .with_context(|| format!("Failed to read dReal SMT-LIB file: {:?}", path))?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { // Reuse the Z3 SMT-LIB parser since dReal accepts SMT-LIB 2.0 format let mut parser = SmtParser::new(content); - parser.parse() + let mut state = parser.parse()?; + state.metadata.insert( + "dreal_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } /// dReal is a fully automated solver — interactive tactic application is @@ -337,6 +347,31 @@ impl ProverBackend for DRealBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { + // Prefer the original SMT-LIB source — `build_verification_query` + // reconstructs from the parsed Term IR, which is lossy for any + // non-trivial dReal problem. + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let source = tokio::fs::read_to_string(path).await?; + let result = self.execute_command(&source).await?; + return match result { + DRealResult::Unsat => Ok(true), + DRealResult::DeltaSat(_) => Ok(false), + DRealResult::Unknown => Ok(false), + DRealResult::Error(e) => bail!("dReal verification error: {}", e), + DRealResult::Output(_) => Ok(false), + }; + } + if let Some(source) = state.metadata.get("dreal_source").and_then(|v| v.as_str()) { + let result = self.execute_command(source).await?; + return match result { + DRealResult::Unsat => Ok(true), + DRealResult::DeltaSat(_) => Ok(false), + DRealResult::Unknown => Ok(false), + DRealResult::Error(e) => bail!("dReal verification error: {}", e), + DRealResult::Output(_) => Ok(false), + }; + } + // Trivial cases: no goals or all goals are true if state.goals.is_empty() { return Ok(true); diff --git a/src/rust/provers/framac.rs b/src/rust/provers/framac.rs index 18afc22..5a89bb2 100644 --- a/src/rust/provers/framac.rs +++ b/src/rust/provers/framac.rs @@ -541,11 +541,21 @@ impl ProverBackend for FramaCBackend { let content = tokio::fs::read_to_string(&path) .await .with_context(|| format!("Failed to read ACSL-annotated C file: {:?}", path))?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { - self.parse_acsl_source(content) + let mut state = self.parse_acsl_source(content)?; + state.metadata.insert( + "framac_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result { @@ -667,20 +677,6 @@ impl ProverBackend for FramaCBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { - if state.goals.is_empty() { - return Ok(true); - } - - let acsl_source = self.to_acsl_source(state)?; - - // Write ACSL-annotated C source to a temporary file - let tmp_dir = - tempfile::tempdir().context("Failed to create temporary directory for Frama-C")?; - let tmp_file = tmp_dir.path().join("program.c"); - tokio::fs::write(&tmp_file, &acsl_source) - .await - .context("Failed to write temporary ACSL-annotated C file")?; - // Read WP prover from metadata (may have been changed via tactic) let wp_prover = state .metadata @@ -703,6 +699,64 @@ impl ProverBackend for FramaCBackend { }) .unwrap_or(self.wp_timeout); + // Prefer the original ACSL-annotated .c file; `to_acsl_source` is + // lossy for anything beyond trivial function stubs. + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 10), + Command::new(&self.config.executable) + .arg("-wp") + .arg("-wp-prover") + .arg(wp_prover) + .arg("-wp-timeout") + .arg(format!("{}", wp_timeout)) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .map_err(|_| { + anyhow!( + "Frama-C WP verification timed out after {} seconds", + self.config.timeout + ) + })? + .context("Failed to execute Frama-C")?; + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + let combined = format!("{}\n{}", stdout, stderr); + return Self::parse_wp_result(&combined); + } + + if state.goals.is_empty() + && state + .metadata + .get("framac_source") + .and_then(|v| v.as_str()) + .is_none() + { + return Ok(true); + } + + let acsl_source = if let Some(src) = state + .metadata + .get("framac_source") + .and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_acsl_source(state)? + }; + + // Write ACSL-annotated C source to a temporary file + let tmp_dir = + tempfile::tempdir().context("Failed to create temporary directory for Frama-C")?; + let tmp_file = tmp_dir.path().join("program.c"); + tokio::fs::write(&tmp_file, &acsl_source) + .await + .context("Failed to write temporary ACSL-annotated C file")?; + // Run: frama-c -wp -wp-prover -wp-timeout let output = tokio::time::timeout( tokio::time::Duration::from_secs(self.config.timeout + 10), diff --git a/src/rust/provers/fstar.rs b/src/rust/provers/fstar.rs index 1a26c42..7153320 100644 --- a/src/rust/provers/fstar.rs +++ b/src/rust/provers/fstar.rs @@ -115,14 +115,23 @@ impl ProverBackend for FStarBackend { } async fn parse_file(&self, path: PathBuf) -> Result { - let content = tokio::fs::read_to_string(path) + let content = tokio::fs::read_to_string(&path) .await .context("Failed to read F* file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "fstar_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let line = line.trim(); if line.is_empty() || line.starts_with("//") || line.starts_with("(*") { @@ -155,7 +164,28 @@ impl ProverBackend for FStarBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("F* timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state.metadata.get("fstar_source").and_then(|v| v.as_str()) { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .stdin(Stdio::piped()) .stdout(Stdio::piped()) diff --git a/src/rust/provers/glpk.rs b/src/rust/provers/glpk.rs index ca8a567..d3ee5c2 100644 --- a/src/rust/provers/glpk.rs +++ b/src/rust/provers/glpk.rs @@ -51,11 +51,20 @@ impl ProverBackend for GLPKBackend { .to_string()) } async fn parse_file(&self, path: PathBuf) -> Result { - self.parse_string(&tokio::fs::read_to_string(path).await?) - .await + let content = tokio::fs::read_to_string(&path).await?; + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "glpk_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let l = line.trim(); if !l.is_empty() && !l.starts_with("/*") { @@ -79,7 +88,29 @@ impl ProverBackend for GLPKBackend { Err(anyhow::anyhow!("GLPK: not an interactive prover")) } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg("--lp") + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("GLPK timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state.metadata.get("glpk_source").and_then(|v| v.as_str()) { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .arg("--lp") .stdin(Stdio::piped()) diff --git a/src/rust/provers/hol_light.rs b/src/rust/provers/hol_light.rs index 17bb3a8..87d9fff 100644 --- a/src/rust/provers/hol_light.rs +++ b/src/rust/provers/hol_light.rs @@ -422,7 +422,12 @@ impl ProverBackend for HolLightBackend { .await .with_context(|| format!("Failed to read file: {:?}", path))?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { @@ -483,6 +488,10 @@ impl ProverBackend for HolLightBackend { "definitions".to_string(), serde_json::json!(file.definitions.len()), ); + meta.insert( + "hol_light_source".to_string(), + serde_json::Value::String(content.to_string()), + ); meta }, }) @@ -527,6 +536,33 @@ impl ProverBackend for HolLightBackend { async fn verify_proof(&self, state: &ProofState) -> Result { info!("Verifying HOL Light proof"); + // Prefer the original .ml source — `export_to_hol(state)` loses + // structure for any non-trivial file. + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let load_cmd = format!("#use \"{}\";;", path); + let result = self.execute_command(&load_cmd).await; + return match result { + Ok(output) => Ok(output.contains("Theorem") || !output.contains("Exception")), + Err(_) => Ok(false), + }; + } + if let Some(source) = state + .metadata + .get("hol_light_source") + .and_then(|v| v.as_str()) + { + let temp_dir = std::env::temp_dir(); + let temp_file = temp_dir.join(format!("echidna_{}.ml", uuid::Uuid::new_v4())); + fs::write(&temp_file, source).await?; + let load_cmd = format!("#use \"{}\";;", temp_file.display()); + let result = self.execute_command(&load_cmd).await; + let _ = fs::remove_file(&temp_file).await; + return match result { + Ok(output) => Ok(output.contains("Theorem") || !output.contains("Exception")), + Err(_) => Ok(false), + }; + } + if state.goals.is_empty() { return Ok(true); } diff --git a/src/rust/provers/idris2.rs b/src/rust/provers/idris2.rs index f45d4f5..00ecac9 100644 --- a/src/rust/provers/idris2.rs +++ b/src/rust/provers/idris2.rs @@ -478,7 +478,12 @@ impl ProverBackend for Idris2Backend { let content = tokio::fs::read_to_string(&path) .await .context("Failed to read Idris 2 file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { @@ -595,11 +600,16 @@ impl ProverBackend for Idris2Backend { context.theorems = theorems; let goals = self.extract_goals(content).await?; + let mut metadata = HashMap::new(); + metadata.insert( + "idris2_source".to_string(), + serde_json::Value::String(content.to_string()), + ); Ok(ProofState { goals, context, proof_script: Vec::new(), - metadata: HashMap::new(), + metadata, }) } @@ -781,6 +791,39 @@ impl ProverBackend for Idris2Backend { } async fn verify_proof(&self, state: &ProofState) -> Result { + // Prefer the original .idr file — `export(state)` reconstructs + // from the Term IR and loses most of Idris 2's QTT structure. + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let p = std::path::Path::new(path); + let mut cmd = Command::new(&self.config.executable); + if let Some(parent) = p.parent() { + cmd.current_dir(parent); + } + let output = cmd + .arg("--check") + .arg(p.file_name().map(std::path::Path::new).unwrap_or(p)) + .output() + .await?; + return Ok(output.status.success()); + } + if let Some(source) = state.metadata.get("idris2_source").and_then(|v| v.as_str()) { + let temp_dir = std::env::temp_dir().join(format!( + "echidna_idris2_{}", + uuid::Uuid::new_v4() + )); + tokio::fs::create_dir_all(&temp_dir).await?; + let temp_file = temp_dir.join("Verify.idr"); + tokio::fs::write(&temp_file, source).await?; + let output = Command::new(&self.config.executable) + .arg("--check") + .arg(&temp_file) + .current_dir(&temp_dir) + .output() + .await?; + let _ = tokio::fs::remove_dir_all(&temp_dir).await; + return Ok(output.status.success()); + } + // Generate Idris 2 code and type-check it let temp_dir = std::env::temp_dir().join("echidna_idris2"); tokio::fs::create_dir_all(&temp_dir).await?; diff --git a/src/rust/provers/imandra.rs b/src/rust/provers/imandra.rs index 522fdec..8689b11 100644 --- a/src/rust/provers/imandra.rs +++ b/src/rust/provers/imandra.rs @@ -51,11 +51,20 @@ impl ProverBackend for ImandraBackend { .to_string()) } async fn parse_file(&self, path: PathBuf) -> Result { - self.parse_string(&tokio::fs::read_to_string(path).await?) - .await + let content = tokio::fs::read_to_string(&path).await?; + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "imandra_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let l = line.trim(); if !l.is_empty() && !l.starts_with("(*") { @@ -79,7 +88,32 @@ impl ProverBackend for ImandraBackend { Err(anyhow::anyhow!("Imandra: use verify/instance")) } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("Imandra timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state + .metadata + .get("imandra_source") + .and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .stdin(Stdio::piped()) .stdout(Stdio::piped()) diff --git a/src/rust/provers/isabelle.rs b/src/rust/provers/isabelle.rs index 3fab082..bc9e9c6 100644 --- a/src/rust/provers/isabelle.rs +++ b/src/rust/provers/isabelle.rs @@ -342,7 +342,12 @@ impl ProverBackend for IsabelleBackend { let content = tokio::fs::read_to_string(&path) .await .context("Failed to read theory file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { @@ -393,6 +398,10 @@ impl ProverBackend for IsabelleBackend { "raw_thy_content".to_string(), serde_json::Value::String(content.to_string()), ); + metadata.insert( + "isabelle_source".to_string(), + serde_json::Value::String(content.to_string()), + ); metadata.insert( "theory_name".to_string(), serde_json::Value::String(theory_name), diff --git a/src/rust/provers/key.rs b/src/rust/provers/key.rs index a8e16b0..d99f364 100644 --- a/src/rust/provers/key.rs +++ b/src/rust/provers/key.rs @@ -405,11 +405,11 @@ impl ProverBackend for KeyBackend { let ext = path.extension().and_then(|e| e.to_str()).unwrap_or(""); - match ext { + let mut state = match ext { "key" => { // Parse .key proof problem file let (goals, axioms) = self.parse_key_file(&content); - let state = ProofState { + ProofState { goals: if goals.is_empty() { vec![Goal { id: "key_goal_0".to_string(), @@ -424,13 +424,12 @@ impl ProverBackend for KeyBackend { ..Default::default() }, ..Default::default() - }; - Ok(state) + } }, "java" => { // Parse JML-annotated Java source let goals = self.parse_jml_annotations(&content); - let state = ProofState { + ProofState { goals: if goals.is_empty() { vec![Goal { id: "java_goal_0".to_string(), @@ -441,14 +440,24 @@ impl ProverBackend for KeyBackend { goals }, ..Default::default() - }; - Ok(state) + } }, - _ => Err(anyhow!( - "Unsupported file extension '{}' for KeY backend — expected .key or .java", - ext - )), - } + _ => { + return Err(anyhow!( + "Unsupported file extension '{}' for KeY backend — expected .key or .java", + ext + )); + }, + }; + state.metadata.insert( + "key_source".to_string(), + serde_json::Value::String(content.clone()), + ); + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } /// Parse a proof problem from a raw string (assumes `.key` format) @@ -482,7 +491,7 @@ impl ProverBackend for KeyBackend { goals }; - let state = ProofState { + let mut state = ProofState { goals: computed_goals, context: crate::core::Context { axioms, @@ -490,6 +499,10 @@ impl ProverBackend for KeyBackend { }, ..Default::default() }; + state.metadata.insert( + "key_source".to_string(), + serde_json::Value::String(content.to_string()), + ); Ok(state) } @@ -612,7 +625,34 @@ impl ProverBackend for KeyBackend { /// Spawns the KeY prover in headless/batch mode, feeds it the proof problem, /// and parses the output for "Proof closed" (success) or "open goals" (failure). async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_key_format(state)?; + // Prefer the original .key/.java file — `to_key_format(state)` is + // lossy for anything beyond trivial goals. + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .args(["--auto", "--no-gui"]) + .args(["--max-steps", &self.max_steps.to_string()]) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("KeY verification timed out")??; + let combined = format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + ); + return self.parse_result(&combined); + } + + let input = if let Some(src) = state.metadata.get("key_source").and_then(|v| v.as_str()) { + src.to_string() + } else { + self.to_key_format(state)? + }; let mut child = Command::new(&self.config.executable) .args(["--auto", "--no-gui"]) diff --git a/src/rust/provers/lean.rs b/src/rust/provers/lean.rs index 04bcbf1..3e49779 100644 --- a/src/rust/provers/lean.rs +++ b/src/rust/provers/lean.rs @@ -1177,7 +1177,15 @@ impl ProverBackend for LeanBackend { }, }; - let state = self.build_proof_state(&declarations, &tactic_state); + let mut state = self.build_proof_state(&declarations, &tactic_state); + state.metadata.insert( + "lean_source".to_string(), + serde_json::Value::String(content.clone()), + ); + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); Ok(state) } @@ -1216,7 +1224,11 @@ impl ProverBackend for LeanBackend { }, }; - let state = self.build_proof_state(&declarations, &tactic_state); + let mut state = self.build_proof_state(&declarations, &tactic_state); + state.metadata.insert( + "lean_source".to_string(), + serde_json::Value::String(content.to_string()), + ); Ok(state) } @@ -1303,6 +1315,31 @@ impl ProverBackend for LeanBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { + // Prefer the original .lean file — the Term IR round-trip loses + // tactic structure that Lean's elaborator depends on. + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let result = self.run_lean(&["--run", path]).await; + return match result { + Ok(_) => Ok(true), + Err(_) => Ok(false), + }; + } + if let Some(source) = state.metadata.get("lean_source").and_then(|v| v.as_str()) { + let temp_file = std::env::temp_dir() + .join(format!("echidna_lean_verify_{}.lean", uuid::Uuid::new_v4())); + tokio::fs::write(&temp_file, source) + .await + .context("Failed to write temporary file")?; + let result = self + .run_lean(&["--run", &temp_file.to_string_lossy()]) + .await; + let _ = tokio::fs::remove_file(&temp_file).await; + return match result { + Ok(_) => Ok(true), + Err(_) => Ok(false), + }; + } + if state.goals.is_empty() { return Ok(true); } diff --git a/src/rust/provers/minizinc.rs b/src/rust/provers/minizinc.rs index e5f5e5b..4d6f627 100644 --- a/src/rust/provers/minizinc.rs +++ b/src/rust/provers/minizinc.rs @@ -57,11 +57,20 @@ impl ProverBackend for MiniZincBackend { .to_string()) } async fn parse_file(&self, path: PathBuf) -> Result { - self.parse_string(&tokio::fs::read_to_string(path).await?) - .await + let content = tokio::fs::read_to_string(&path).await?; + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "minizinc_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let l = line.trim(); if !l.is_empty() && !l.starts_with("%") { @@ -87,7 +96,34 @@ impl ProverBackend for MiniZincBackend { )) } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg("--solver") + .arg("gecode") + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("MiniZinc timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state + .metadata + .get("minizinc_source") + .and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .arg("--solver") .arg("gecode") diff --git a/src/rust/provers/minlog.rs b/src/rust/provers/minlog.rs index 7e52b11..374f78a 100644 --- a/src/rust/provers/minlog.rs +++ b/src/rust/provers/minlog.rs @@ -43,11 +43,20 @@ impl ProverBackend for MinlogBackend { Ok("minlog".to_string()) } async fn parse_file(&self, path: PathBuf) -> Result { - self.parse_string(&tokio::fs::read_to_string(path).await?) - .await + let content = tokio::fs::read_to_string(&path).await?; + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "minlog_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let l = line.trim(); if !l.is_empty() && !l.starts_with(";;") { @@ -71,7 +80,32 @@ impl ProverBackend for MinlogBackend { Err(anyhow::anyhow!("Minlog: use proof terms")) } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("Minlog timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state + .metadata + .get("minlog_source") + .and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .stdin(Stdio::piped()) .stdout(Stdio::piped()) diff --git a/src/rust/provers/mizar.rs b/src/rust/provers/mizar.rs index eaaa140..f0de9ce 100644 --- a/src/rust/provers/mizar.rs +++ b/src/rust/provers/mizar.rs @@ -422,11 +422,16 @@ impl ProverBackend for MizarBackend { }); } + let mut metadata = HashMap::new(); + metadata.insert( + "mizar_source".to_string(), + serde_json::Value::String(content.to_string()), + ); Ok(ProofState { goals, context, proof_script: vec![], - metadata: HashMap::new(), + metadata, }) } @@ -544,10 +549,11 @@ impl ProverBackend for MizarBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { - if !state.is_complete() { - return Ok(false); - } - + // Prefer the original .miz file — `export_to_mizar(state)` is + // lossy for anything beyond trivial theorems. The previous + // `is_complete()` short-circuit produced spurious false results + // when parse_string left open goals (Mizar's own checker is the + // authority, not our IR). if let Some(serde_json::Value::String(path)) = state.metadata.get("source_path") { let path = Path::new(path); if path.exists() { @@ -556,6 +562,22 @@ impl ProverBackend for MizarBackend { } } + if let Some(source) = state.metadata.get("mizar_source").and_then(|v| v.as_str()) { + let temp_dir = std::env::temp_dir(); + let temp_file = temp_dir.join(format!("echidna_{}.miz", uuid::Uuid::new_v4())); + let mut file = fs::File::create(&temp_file).await?; + file.write_all(source.as_bytes()).await?; + file.sync_all().await?; + drop(file); + let result = self.verify_file(&temp_file).await?; + let _ = fs::remove_file(&temp_file).await; + return Ok(result.success); + } + + if !state.is_complete() { + return Ok(false); + } + let mizar_content = self.export_to_mizar(state)?; let temp_dir = std::env::temp_dir(); diff --git a/src/rust/provers/nuprl.rs b/src/rust/provers/nuprl.rs index 39171e3..06b9c67 100644 --- a/src/rust/provers/nuprl.rs +++ b/src/rust/provers/nuprl.rs @@ -43,11 +43,20 @@ impl ProverBackend for NuprlBackend { Ok("nuprl".to_string()) } async fn parse_file(&self, path: PathBuf) -> Result { - self.parse_string(&tokio::fs::read_to_string(path).await?) - .await + let content = tokio::fs::read_to_string(&path).await?; + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "nuprl_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let l = line.trim(); if !l.is_empty() && !l.starts_with("(*") { @@ -71,7 +80,28 @@ impl ProverBackend for NuprlBackend { Err(anyhow::anyhow!("Nuprl: use refinement tactics")) } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("Nuprl timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state.metadata.get("nuprl_source").and_then(|v| v.as_str()) { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .stdin(Stdio::piped()) .stdout(Stdio::piped()) diff --git a/src/rust/provers/nusmv.rs b/src/rust/provers/nusmv.rs index c464b40..b279a1c 100644 --- a/src/rust/provers/nusmv.rs +++ b/src/rust/provers/nusmv.rs @@ -234,14 +234,24 @@ impl ProverBackend for NuSMVBackend { } async fn parse_file(&self, path: PathBuf) -> Result { - let content = tokio::fs::read_to_string(path) + let content = tokio::fs::read_to_string(&path) .await .context("Failed to read SMV file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { - self.parse_smv(content) + let mut state = self.parse_smv(content)?; + state.metadata.insert( + "nusmv_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result { @@ -303,7 +313,29 @@ impl ProverBackend for NuSMVBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { - let smv_code = self.to_smv(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .map_err(|_| anyhow!("NuSMV timed out after {} seconds", self.config.timeout))? + .context("Failed to execute NuSMV")?; + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + let combined = format!("{}\n{}", stdout, stderr); + return self.parse_result(&combined); + } + let smv_code = if let Some(src) = state.metadata.get("nusmv_source").and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_smv(state)? + }; // Write SMV to a temporary file (nuXmv requires a file) let tmp_dir = diff --git a/src/rust/provers/ortools.rs b/src/rust/provers/ortools.rs index 929f960..3a9295b 100644 --- a/src/rust/provers/ortools.rs +++ b/src/rust/provers/ortools.rs @@ -43,11 +43,20 @@ impl ProverBackend for ORToolsBackend { Ok("or-tools".to_string()) } async fn parse_file(&self, path: PathBuf) -> Result { - self.parse_string(&tokio::fs::read_to_string(path).await?) - .await + let content = tokio::fs::read_to_string(&path).await?; + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "ortools_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let l = line.trim(); if !l.is_empty() && !l.starts_with("//") { @@ -73,7 +82,32 @@ impl ProverBackend for ORToolsBackend { )) } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("OR-Tools timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state + .metadata + .get("ortools_source") + .and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .stdin(Stdio::piped()) .stdout(Stdio::piped()) diff --git a/src/rust/provers/prism.rs b/src/rust/provers/prism.rs index 41c34cf..c26de4b 100644 --- a/src/rust/provers/prism.rs +++ b/src/rust/provers/prism.rs @@ -237,14 +237,24 @@ impl ProverBackend for PrismBackend { } async fn parse_file(&self, path: PathBuf) -> Result { - let content = tokio::fs::read_to_string(path) + let content = tokio::fs::read_to_string(&path) .await .context("Failed to read PRISM file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { - self.parse_prism(content) + let mut state = self.parse_prism(content)?; + state.metadata.insert( + "prism_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result { @@ -306,6 +316,49 @@ impl ProverBackend for PrismBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { + // Prefer the original .pm/.prism file — reconstructing both + // model and properties from the Term IR is lossy. + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .map_err(|_| anyhow!("PRISM timed out after {} seconds", self.config.timeout))? + .context("Failed to execute PRISM")?; + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + let combined = format!("{}\n{}", stdout, stderr); + return self.parse_result(&combined); + } + if let Some(src) = state.metadata.get("prism_source").and_then(|v| v.as_str()) { + let tmp_dir = + tempfile::tempdir().context("Failed to create temporary directory for PRISM")?; + let model_file = tmp_dir.path().join("model.pm"); + tokio::fs::write(&model_file, src) + .await + .context("Failed to write temporary PRISM model file")?; + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout), + Command::new(&self.config.executable) + .arg(&model_file) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .map_err(|_| anyhow!("PRISM timed out after {} seconds", self.config.timeout))? + .context("Failed to execute PRISM")?; + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + let combined = format!("{}\n{}", stdout, stderr); + return self.parse_result(&combined); + } + let model_code = self.to_prism_model(state)?; let props_code = self.to_prism_properties(state); diff --git a/src/rust/provers/proverif.rs b/src/rust/provers/proverif.rs index ef82793..721a6c5 100644 --- a/src/rust/provers/proverif.rs +++ b/src/rust/provers/proverif.rs @@ -434,14 +434,24 @@ impl ProverBackend for ProVerifBackend { } async fn parse_file(&self, path: PathBuf) -> Result { - let content = tokio::fs::read_to_string(path) + let content = tokio::fs::read_to_string(&path) .await .context("Failed to read .pv file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { - self.parse_pv(content) + let mut state = self.parse_pv(content)?; + state.metadata.insert( + "proverif_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } async fn apply_tactic(&self, _state: &ProofState, tactic: &Tactic) -> Result { @@ -455,7 +465,37 @@ impl ProverBackend for ProVerifBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { - let pv_code = self.to_pv(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 10), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .map_err(|_| { + anyhow!( + "ProVerif verification timed out after {} seconds", + self.config.timeout + ) + })? + .context("Failed to execute proverif")?; + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + let combined = format!("{}\n{}", stdout, stderr); + return self.parse_result(&combined); + } + let pv_code = if let Some(src) = state + .metadata + .get("proverif_source") + .and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_pv(state)? + }; // Write .pv to a temporary file (proverif requires a file path) let tmp_dir = diff --git a/src/rust/provers/scip.rs b/src/rust/provers/scip.rs index 02c2815..eeec392 100644 --- a/src/rust/provers/scip.rs +++ b/src/rust/provers/scip.rs @@ -51,11 +51,20 @@ impl ProverBackend for SCIPBackend { .to_string()) } async fn parse_file(&self, path: PathBuf) -> Result { - self.parse_string(&tokio::fs::read_to_string(path).await?) - .await + let content = tokio::fs::read_to_string(&path).await?; + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "scip_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let l = line.trim(); if !l.is_empty() && !l.starts_with("\\") { @@ -79,7 +88,29 @@ impl ProverBackend for SCIPBackend { Err(anyhow::anyhow!("SCIP: not an interactive prover")) } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg("-f") + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("SCIP timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state.metadata.get("scip_source").and_then(|v| v.as_str()) { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .stdin(Stdio::piped()) .stdout(Stdio::piped()) diff --git a/src/rust/provers/seahorn.rs b/src/rust/provers/seahorn.rs index f5b5f68..83adeed 100644 --- a/src/rust/provers/seahorn.rs +++ b/src/rust/provers/seahorn.rs @@ -369,13 +369,13 @@ impl ProverBackend for SeaHornBackend { async fn parse_file(&self, path: PathBuf) -> Result { let extension = path.extension().and_then(|e| e.to_str()).unwrap_or(""); - match extension { + let mut state = match extension { "c" | "h" => { // Parse C source to extract assertions and assumptions let content = tokio::fs::read_to_string(&path) .await .context("Failed to read C source file for SeaHorn")?; - self.parse_string(&content).await + self.parse_string(&content).await? }, "bc" | "ll" => { // LLVM bitcode / IR — we cannot parse assertions directly, @@ -389,17 +389,29 @@ impl ProverBackend for SeaHornBackend { "seahorn_input_type".to_string(), serde_json::Value::String(extension.to_string()), ); - Ok(state) + state }, - _ => Err(anyhow!( - "SeaHorn: unsupported file extension '.{}' (expected .c, .bc, or .ll)", - extension - )), - } + _ => { + return Err(anyhow!( + "SeaHorn: unsupported file extension '.{}' (expected .c, .bc, or .ll)", + extension + )); + }, + }; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { - self.parse_c_source(content) + let mut state = self.parse_c_source(content)?; + state.metadata.insert( + "seahorn_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result { @@ -520,11 +532,25 @@ impl ProverBackend for SeaHornBackend { let tmp_dir = tempfile::tempdir().context("Failed to create temporary directory for SeaHorn")?; - let input_path = if let Some(serde_json::Value::String(file_path)) = + let input_path = if let Some(path) = + state.metadata.get("source_path").and_then(|v| v.as_str()) + { + PathBuf::from(path) + } else if let Some(serde_json::Value::String(file_path)) = state.metadata.get("seahorn_input_file") { // Use the referenced input file directly (bitcode or C source) PathBuf::from(file_path) + } else if let Some(src) = state + .metadata + .get("seahorn_source") + .and_then(|v| v.as_str()) + { + let tmp_file = tmp_dir.path().join("program.c"); + tokio::fs::write(&tmp_file, src) + .await + .context("Failed to write temporary C file for SeaHorn")?; + tmp_file } else { // Generate C source from proof state let c_source = self.to_c_source(state)?; diff --git a/src/rust/provers/spin_checker.rs b/src/rust/provers/spin_checker.rs index d44944a..711c17c 100644 --- a/src/rust/provers/spin_checker.rs +++ b/src/rust/provers/spin_checker.rs @@ -218,14 +218,24 @@ impl ProverBackend for SpinBackend { } async fn parse_file(&self, path: PathBuf) -> Result { - let content = tokio::fs::read_to_string(path) + let content = tokio::fs::read_to_string(&path) .await .context("Failed to read Promela file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { - self.parse_promela(content) + let mut state = self.parse_promela(content)?; + state.metadata.insert( + "spin_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result { @@ -288,7 +298,35 @@ impl ProverBackend for SpinBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { - let promela_code = self.to_promela(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 10), + Command::new(&self.config.executable) + .arg("-run") + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .map_err(|_| { + anyhow!( + "SPIN verification timed out after {} seconds", + self.config.timeout + ) + })? + .context("Failed to execute SPIN")?; + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + let combined = format!("{}\n{}", stdout, stderr); + return self.parse_result(&combined); + } + let promela_code = if let Some(src) = state.metadata.get("spin_source").and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_promela(state)? + }; // Write Promela to a temporary file (spin -run requires a file) let tmp_dir = diff --git a/src/rust/provers/tamarin.rs b/src/rust/provers/tamarin.rs index c4a1dfb..c507dc8 100644 --- a/src/rust/provers/tamarin.rs +++ b/src/rust/provers/tamarin.rs @@ -286,14 +286,24 @@ impl ProverBackend for TamarinBackend { } async fn parse_file(&self, path: PathBuf) -> Result { - let content = tokio::fs::read_to_string(path) + let content = tokio::fs::read_to_string(&path) .await .context("Failed to read .spthy file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { - self.parse_spthy(content) + let mut state = self.parse_spthy(content)?; + state.metadata.insert( + "tamarin_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result { @@ -370,7 +380,38 @@ impl ProverBackend for TamarinBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { - let spthy_code = self.to_spthy(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 10), + Command::new(&self.config.executable) + .arg("--prove") + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .map_err(|_| { + anyhow!( + "Tamarin verification timed out after {} seconds", + self.config.timeout + ) + })? + .context("Failed to execute tamarin-prover")?; + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + let combined = format!("{}\n{}", stdout, stderr); + return self.parse_result(&combined); + } + let spthy_code = if let Some(src) = state + .metadata + .get("tamarin_source") + .and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_spthy(state)? + }; // Write .spthy to a temporary file (tamarin-prover requires a file) let tmp_dir = diff --git a/src/rust/provers/tlaps.rs b/src/rust/provers/tlaps.rs index 5d2fdd2..f4ef4a1 100644 --- a/src/rust/provers/tlaps.rs +++ b/src/rust/provers/tlaps.rs @@ -53,11 +53,20 @@ impl ProverBackend for TLAPSBackend { .to_string()) } async fn parse_file(&self, path: PathBuf) -> Result { - self.parse_string(&tokio::fs::read_to_string(path).await?) - .await + let content = tokio::fs::read_to_string(&path).await?; + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "tlaps_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let l = line.trim(); if l.is_empty() @@ -88,7 +97,28 @@ impl ProverBackend for TLAPSBackend { Err(anyhow::anyhow!("TLAPS: use OBVIOUS/BY/QED")) } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("TLAPS timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state.metadata.get("tlaps_source").and_then(|v| v.as_str()) { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .stdin(Stdio::piped()) .stdout(Stdio::piped()) diff --git a/src/rust/provers/tlc.rs b/src/rust/provers/tlc.rs index 580bdaa..2b7463b 100644 --- a/src/rust/provers/tlc.rs +++ b/src/rust/provers/tlc.rs @@ -224,14 +224,24 @@ impl ProverBackend for TLCBackend { } async fn parse_file(&self, path: PathBuf) -> Result { - let content = tokio::fs::read_to_string(path) + let content = tokio::fs::read_to_string(&path) .await .context("Failed to read TLA+ file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { - self.parse_tla(content) + let mut state = self.parse_tla(content)?; + state.metadata.insert( + "tlc_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result { @@ -294,7 +304,31 @@ impl ProverBackend for TLCBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { - let tla_code = self.to_tla(state)?; + // Prefer the original .tla file — `to_tla(state)` is lossy. + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .map_err(|_| anyhow!("TLC timed out after {} seconds", self.config.timeout))? + .context("Failed to execute TLC")?; + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + let combined = format!("{}\n{}", stdout, stderr); + return self.parse_result(&combined); + } + + let tla_code = if let Some(src) = state.metadata.get("tlc_source").and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_tla(state)? + }; let cfg_code = self.to_cfg(state); // Write TLA+ and CFG to temporary files diff --git a/src/rust/provers/twelf.rs b/src/rust/provers/twelf.rs index 03b3dbe..2c5cff7 100644 --- a/src/rust/provers/twelf.rs +++ b/src/rust/provers/twelf.rs @@ -43,11 +43,20 @@ impl ProverBackend for TwelfBackend { Ok("twelf".to_string()) } async fn parse_file(&self, path: PathBuf) -> Result { - self.parse_string(&tokio::fs::read_to_string(path).await?) - .await + let content = tokio::fs::read_to_string(&path).await?; + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "twelf_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let l = line.trim(); if !l.is_empty() && !l.starts_with("%") { @@ -71,7 +80,28 @@ impl ProverBackend for TwelfBackend { Err(anyhow::anyhow!("Twelf: use LF declarations")) } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("Twelf timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state.metadata.get("twelf_source").and_then(|v| v.as_str()) { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .stdin(Stdio::piped()) .stdout(Stdio::piped()) diff --git a/src/rust/provers/uppaal.rs b/src/rust/provers/uppaal.rs index 0716b43..1ecc4a3 100644 --- a/src/rust/provers/uppaal.rs +++ b/src/rust/provers/uppaal.rs @@ -249,14 +249,24 @@ impl ProverBackend for UppaalBackend { } async fn parse_file(&self, path: PathBuf) -> Result { - let content = tokio::fs::read_to_string(path) + let content = tokio::fs::read_to_string(&path) .await .context("Failed to read UPPAAL XML file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { - self.parse_uppaal_xml(content) + let mut state = self.parse_uppaal_xml(content)?; + state.metadata.insert( + "uppaal_source".to_string(), + serde_json::Value::String(content.to_string()), + ); + Ok(state) } async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result { @@ -322,7 +332,32 @@ impl ProverBackend for UppaalBackend { } async fn verify_proof(&self, state: &ProofState) -> Result { - let xml_code = self.to_uppaal_xml(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout), + Command::new(&self.config.executable) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .map_err(|_| anyhow!("UPPAAL timed out after {} seconds", self.config.timeout))? + .context("Failed to execute verifyta")?; + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + let combined = format!("{}\n{}", stdout, stderr); + return self.parse_result(&combined); + } + let xml_code = if let Some(src) = state + .metadata + .get("uppaal_source") + .and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_uppaal_xml(state)? + }; let query_code = self.to_query_file(state); // Write model and queries to temporary files diff --git a/src/rust/provers/viper.rs b/src/rust/provers/viper.rs index 80dff15..515d9c9 100644 --- a/src/rust/provers/viper.rs +++ b/src/rust/provers/viper.rs @@ -134,10 +134,15 @@ impl ProverBackend for ViperBackend { } async fn parse_file(&self, path: PathBuf) -> Result { - let content = tokio::fs::read_to_string(path) + let content = tokio::fs::read_to_string(&path) .await .context("Failed to read proof file")?; - self.parse_string(&content).await + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } /// Parse a Silver (.vpr) program into a ProofState. @@ -146,6 +151,10 @@ impl ProverBackend for ViperBackend { /// into goals. Comments (// and /* */) are skipped. async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "viper_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let line = line.trim(); @@ -220,7 +229,32 @@ impl ProverBackend for ViperBackend { /// the configured timeout. Both Silicon and Carbon are supported via /// the `--backend` flag (configurable through extra args). async fn verify_proof(&self, state: &ProofState) -> Result { - let silver_code = self.to_silver(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg("--timeout") + .arg(format!("{}", self.config.timeout)) + .args(&self.config.args) + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("Viper timed out")??; + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + return self + .parse_result(&stdout) + .or_else(|_| self.parse_result(&stderr)); + } + let silver_code = if let Some(src) = state.metadata.get("viper_source").and_then(|v| v.as_str()) + { + src.to_string() + } else { + self.to_silver(state)? + }; let mut child = Command::new(&self.config.executable) .arg("--timeout") diff --git a/src/rust/provers/why3.rs b/src/rust/provers/why3.rs index c136b16..3c75838 100644 --- a/src/rust/provers/why3.rs +++ b/src/rust/provers/why3.rs @@ -56,11 +56,20 @@ impl ProverBackend for Why3Backend { .to_string()) } async fn parse_file(&self, path: PathBuf) -> Result { - self.parse_string(&tokio::fs::read_to_string(path).await?) - .await + let content = tokio::fs::read_to_string(&path).await?; + let mut state = self.parse_string(&content).await?; + state.metadata.insert( + "source_path".to_string(), + serde_json::Value::String(path.to_string_lossy().into_owned()), + ); + Ok(state) } async fn parse_string(&self, content: &str) -> Result { let mut state = ProofState::default(); + state.metadata.insert( + "why3_source".to_string(), + serde_json::Value::String(content.to_string()), + ); for line in content.lines() { let l = line.trim(); if l.is_empty() || l.starts_with("(*") { @@ -89,7 +98,31 @@ impl ProverBackend for Why3Backend { Err(anyhow::anyhow!("Why3: use built-in transformations")) } async fn verify_proof(&self, state: &ProofState) -> Result { - let input = self.to_input_format(state)?; + if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) { + let output = tokio::time::timeout( + tokio::time::Duration::from_secs(self.config.timeout + 5), + Command::new(&self.config.executable) + .arg("prove") + .arg("-P") + .arg("z3") + .arg(path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .output(), + ) + .await + .context("Why3 timed out")??; + return self.parse_result(&format!( + "{}\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + )); + } + let input = if let Some(src) = state.metadata.get("why3_source").and_then(|v| v.as_str()) { + src.to_string() + } else { + self.to_input_format(state)? + }; let mut child = Command::new(&self.config.executable) .arg("prove") .arg("-P")