Claude/echidna mcp

src/rust/provers/alloy.rs

@@ -228,14 +228,24 @@ impl ProverBackend for AlloyBackend {
     }
 
     async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
-        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<ProofState> {
-        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<TacticResult> {
@@ -293,7 +303,35 @@ impl ProverBackend for AlloyBackend {
     }
 
     async fn verify_proof(&self, state: &ProofState) -> Result<bool> {
-        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 =

src/rust/provers/cbmc.rs

@@ -246,14 +246,24 @@ impl ProverBackend for CBMCBackend {
     }
 
     async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
-        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<ProofState> {
-        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<TacticResult> {
@@ -321,7 +331,47 @@ impl ProverBackend for CBMCBackend {
     }
 
     async fn verify_proof(&self, state: &ProofState) -> Result<bool> {
-        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::<u32>().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::<u32>().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),

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<ProofState> {
-        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<ProofState> {
         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<bool> {
-        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())

src/rust/provers/dafny.rs

@@ -55,11 +55,20 @@ impl ProverBackend for DafnyBackend {
             .to_string())
     }
     async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
-        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<ProofState> {
         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<bool> {
-        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())

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<ProofState> {
         // 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<bool> {
+        // 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);