fix(provers): extend source_path pattern to 32 remaining lossy backends

Applies the same parse_file → stash "source_path", parse_string →
stash "{prover}_source", verify_proof → prefer-metadata-before-IR
fix to the rest of the LOSSY_ROUNDTRIP backends: alloy, cbmc, chuffed,
dafny, dreal, framac, fstar, glpk, hol_light, idris2, imandra,
isabelle, key, lean, minizinc, minlog, mizar, nuprl, nusmv, ortools,
prism, proverif, scip, seahorn, spin_checker, tamarin, tlaps, tlc,
twelf, uppaal, viper, why3.

Non-trivial adaptations required to preserve semantics:

- idris2: Idris 2 resolves the top-level module name from CWD like
  Agda, so the source_path branch spawns with current_dir set to
  the file's parent and passes the bare filename.
- seahorn: already had a seahorn_input_file escape hatch for pre-
  compiled .bc/.ll bitcode; source_path becomes the primary
  preference with the existing hatch and the IR reconstruction as
  successive fallbacks.
- cbmc/framac: the --unwind / -wp-* metadata knobs were hoisted
  above the source_path branch so every path honours the user's
  bound overrides.
- prism/tlc: these write two files (model + properties/cfg).  The
  source_path branch passes the real model file verbatim; the
  multi-file generation fallback stays intact behind the if-let.
- isabelle/mizar: both already had partial source stashing
  (raw_thy_content, source_path).  Normalised to the canonical
  source_path + {prover}_source convention; Mizar's is_complete()
  short-circuit was moved below the source-backed branches so real
  files are not rejected for having open goals in our IR.
- acl2: ACL2 reads input on stdin — the source_path branch opens
  the real file as Stdio::from(File) rather than piping string
  content, matching the existing lossy-path invocation shape.

No trait signatures changed; every fallback path remains byte-for-
byte identical behind an if-let guard.  Full workspace build, the
625-test unit suite, and `cargo clippy --lib --bin echidna` all
remain green.

Phase 3 closes out the broken-backend audit that started with the
Z3/CVC5/Coq MVP fixes: 39 backends now prefer their original source
over the lossy Term-IR round-trip.

https://claude.ai/code/session_01NaC5RXjTyr5xg9XXUa2FCC

Author: claude

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);