Skip to content

Commit 6ee5c64

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
Claude/echidna mcp (#34)
Co-authored-by: Claude <noreply@anthropic.com>
1 parent 6c07c3d commit 6ee5c64

32 files changed

Lines changed: 1247 additions & 138 deletions

‎src/rust/provers/alloy.rs‎

Lines changed: 42 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -228,14 +228,24 @@ impl ProverBackend for AlloyBackend {
228228
}
229229

230230
async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
231-
let content = tokio::fs::read_to_string(path)
231+
let content = tokio::fs::read_to_string(&path)
232232
.await
233233
.context("Failed to read Alloy file")?;
234-
self.parse_string(&content).await
234+
let mut state = self.parse_string(&content).await?;
235+
state.metadata.insert(
236+
"source_path".to_string(),
237+
serde_json::Value::String(path.to_string_lossy().into_owned()),
238+
);
239+
Ok(state)
235240
}
236241

237242
async fn parse_string(&self, content: &str) -> Result<ProofState> {
238-
self.parse_alloy(content)
243+
let mut state = self.parse_alloy(content)?;
244+
state.metadata.insert(
245+
"alloy_source".to_string(),
246+
serde_json::Value::String(content.to_string()),
247+
);
248+
Ok(state)
239249
}
240250

241251
async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result<TacticResult> {
@@ -293,7 +303,35 @@ impl ProverBackend for AlloyBackend {
293303
}
294304

295305
async fn verify_proof(&self, state: &ProofState) -> Result<bool> {
296-
let alloy_code = self.to_alloy(state)?;
306+
// Prefer the original .als source; `to_alloy(state)` round-trips
307+
// through the generic Term IR and cannot reconstruct real models.
308+
if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) {
309+
let output = tokio::time::timeout(
310+
tokio::time::Duration::from_secs(self.config.timeout),
311+
Command::new(&self.config.executable)
312+
.arg(path)
313+
.stdout(Stdio::piped())
314+
.stderr(Stdio::piped())
315+
.output(),
316+
)
317+
.await
318+
.map_err(|_| anyhow!("Alloy timed out after {} seconds", self.config.timeout))?
319+
.context("Failed to execute Alloy")?;
320+
let stdout = String::from_utf8_lossy(&output.stdout);
321+
let stderr = String::from_utf8_lossy(&output.stderr);
322+
let combined = format!("{}\n{}", stdout, stderr);
323+
return self.parse_result(&combined);
324+
}
325+
326+
let alloy_code = if let Some(src) = state
327+
.metadata
328+
.get("alloy_source")
329+
.and_then(|v| v.as_str())
330+
{
331+
src.to_string()
332+
} else {
333+
self.to_alloy(state)?
334+
};
297335

298336
// Write Alloy to a temporary file
299337
let tmp_dir =

‎src/rust/provers/cbmc.rs‎

Lines changed: 54 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -246,14 +246,24 @@ impl ProverBackend for CBMCBackend {
246246
}
247247

248248
async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
249-
let content = tokio::fs::read_to_string(path)
249+
let content = tokio::fs::read_to_string(&path)
250250
.await
251251
.context("Failed to read C source file")?;
252-
self.parse_string(&content).await
252+
let mut state = self.parse_string(&content).await?;
253+
state.metadata.insert(
254+
"source_path".to_string(),
255+
serde_json::Value::String(path.to_string_lossy().into_owned()),
256+
);
257+
Ok(state)
253258
}
254259

255260
async fn parse_string(&self, content: &str) -> Result<ProofState> {
256-
self.parse_c_source(content)
261+
let mut state = self.parse_c_source(content)?;
262+
state.metadata.insert(
263+
"cbmc_source".to_string(),
264+
serde_json::Value::String(content.to_string()),
265+
);
266+
Ok(state)
257267
}
258268

259269
async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result<TacticResult> {
@@ -321,7 +331,47 @@ impl ProverBackend for CBMCBackend {
321331
}
322332

323333
async fn verify_proof(&self, state: &ProofState) -> Result<bool> {
324-
let c_source = self.to_c_source(state)?;
334+
// Determine unwind bound from metadata or use default
335+
let unwind = state
336+
.metadata
337+
.get("cbmc_unwind_bound")
338+
.and_then(|v| v.as_str())
339+
.and_then(|s| s.parse::<u32>().ok())
340+
.unwrap_or(self.unwind_bound);
341+
342+
// Prefer the original .c source — `to_c_source(state)` round-trips
343+
// through the generic Term IR and silently mangles anything real.
344+
if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) {
345+
let output = tokio::time::timeout(
346+
tokio::time::Duration::from_secs(self.config.timeout + 10),
347+
Command::new(&self.config.executable)
348+
.arg("--unwind")
349+
.arg(format!("{}", unwind))
350+
.arg(path)
351+
.stdout(Stdio::piped())
352+
.stderr(Stdio::piped())
353+
.output(),
354+
)
355+
.await
356+
.map_err(|_| {
357+
anyhow!(
358+
"CBMC verification timed out after {} seconds",
359+
self.config.timeout
360+
)
361+
})?
362+
.context("Failed to execute CBMC")?;
363+
let stdout = String::from_utf8_lossy(&output.stdout);
364+
let stderr = String::from_utf8_lossy(&output.stderr);
365+
let combined = format!("{}\n{}", stdout, stderr);
366+
return self.parse_result(&combined);
367+
}
368+
369+
let c_source = if let Some(src) = state.metadata.get("cbmc_source").and_then(|v| v.as_str())
370+
{
371+
src.to_string()
372+
} else {
373+
self.to_c_source(state)?
374+
};
325375

326376
// Write C source to a temporary file (CBMC requires a file)
327377
let tmp_dir =
@@ -331,14 +381,6 @@ impl ProverBackend for CBMCBackend {
331381
.await
332382
.context("Failed to write temporary C file")?;
333383

334-
// Determine unwind bound from metadata or use default
335-
let unwind = state
336-
.metadata
337-
.get("cbmc_unwind_bound")
338-
.and_then(|v| v.as_str())
339-
.and_then(|s| s.parse::<u32>().ok())
340-
.unwrap_or(self.unwind_bound);
341-
342384
// Run cbmc with unwind bound
343385
let output = tokio::time::timeout(
344386
tokio::time::Duration::from_secs(self.config.timeout + 10),

‎src/rust/provers/chuffed.rs‎

Lines changed: 39 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -46,11 +46,20 @@ impl ProverBackend for ChuffedBackend {
4646
Ok("chuffed".to_string())
4747
}
4848
async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
49-
self.parse_string(&tokio::fs::read_to_string(path).await?)
50-
.await
49+
let content = tokio::fs::read_to_string(&path).await?;
50+
let mut state = self.parse_string(&content).await?;
51+
state.metadata.insert(
52+
"source_path".to_string(),
53+
serde_json::Value::String(path.to_string_lossy().into_owned()),
54+
);
55+
Ok(state)
5156
}
5257
async fn parse_string(&self, content: &str) -> Result<ProofState> {
5358
let mut state = ProofState::default();
59+
state.metadata.insert(
60+
"chuffed_source".to_string(),
61+
serde_json::Value::String(content.to_string()),
62+
);
5463
for line in content.lines() {
5564
let l = line.trim();
5665
if !l.is_empty() && !l.starts_with("%") {
@@ -74,7 +83,34 @@ impl ProverBackend for ChuffedBackend {
7483
Err(anyhow::anyhow!("Chuffed: CP solver, not interactive"))
7584
}
7685
async fn verify_proof(&self, state: &ProofState) -> Result<bool> {
77-
let input = self.to_input_format(state)?;
86+
// Prefer the original FlatZinc source — reconstructing from the
87+
// Term IR via `to_input_format` loses all constraint structure.
88+
if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) {
89+
let output = tokio::time::timeout(
90+
tokio::time::Duration::from_secs(self.config.timeout + 5),
91+
Command::new(&self.config.executable)
92+
.arg(path)
93+
.stdout(Stdio::piped())
94+
.stderr(Stdio::piped())
95+
.output(),
96+
)
97+
.await
98+
.context("Chuffed timed out")??;
99+
return self.parse_result(&format!(
100+
"{}\n{}",
101+
String::from_utf8_lossy(&output.stdout),
102+
String::from_utf8_lossy(&output.stderr)
103+
));
104+
}
105+
let input = if let Some(src) = state
106+
.metadata
107+
.get("chuffed_source")
108+
.and_then(|v| v.as_str())
109+
{
110+
src.to_string()
111+
} else {
112+
self.to_input_format(state)?
113+
};
78114
let mut child = Command::new(&self.config.executable)
79115
.stdin(Stdio::piped())
80116
.stdout(Stdio::piped())

‎src/rust/provers/dafny.rs‎

Lines changed: 34 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -55,11 +55,20 @@ impl ProverBackend for DafnyBackend {
5555
.to_string())
5656
}
5757
async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
58-
self.parse_string(&tokio::fs::read_to_string(path).await?)
59-
.await
58+
let content = tokio::fs::read_to_string(&path).await?;
59+
let mut state = self.parse_string(&content).await?;
60+
state.metadata.insert(
61+
"source_path".to_string(),
62+
serde_json::Value::String(path.to_string_lossy().into_owned()),
63+
);
64+
Ok(state)
6065
}
6166
async fn parse_string(&self, content: &str) -> Result<ProofState> {
6267
let mut state = ProofState::default();
68+
state.metadata.insert(
69+
"dafny_source".to_string(),
70+
serde_json::Value::String(content.to_string()),
71+
);
6372
for line in content.lines() {
6473
let l = line.trim();
6574
if l.is_empty() || l.starts_with("//") {
@@ -86,7 +95,29 @@ impl ProverBackend for DafnyBackend {
8695
))
8796
}
8897
async fn verify_proof(&self, state: &ProofState) -> Result<bool> {
89-
let input = self.to_input_format(state)?;
98+
if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) {
99+
let output = tokio::time::timeout(
100+
tokio::time::Duration::from_secs(self.config.timeout + 5),
101+
Command::new(&self.config.executable)
102+
.arg("verify")
103+
.arg(path)
104+
.stdout(Stdio::piped())
105+
.stderr(Stdio::piped())
106+
.output(),
107+
)
108+
.await
109+
.context("Dafny timed out")??;
110+
return self.parse_result(&format!(
111+
"{}\n{}",
112+
String::from_utf8_lossy(&output.stdout),
113+
String::from_utf8_lossy(&output.stderr)
114+
));
115+
}
116+
let input = if let Some(src) = state.metadata.get("dafny_source").and_then(|v| v.as_str()) {
117+
src.to_string()
118+
} else {
119+
self.to_input_format(state)?
120+
};
90121
let mut child = Command::new(&self.config.executable)
91122
.stdin(Stdio::piped())
92123
.stdout(Stdio::piped())

‎src/rust/provers/dreal.rs‎

Lines changed: 37 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -316,13 +316,23 @@ impl ProverBackend for DRealBackend {
316316
.await
317317
.with_context(|| format!("Failed to read dReal SMT-LIB file: {:?}", path))?;
318318

319-
self.parse_string(&content).await
319+
let mut state = self.parse_string(&content).await?;
320+
state.metadata.insert(
321+
"source_path".to_string(),
322+
serde_json::Value::String(path.to_string_lossy().into_owned()),
323+
);
324+
Ok(state)
320325
}
321326

322327
async fn parse_string(&self, content: &str) -> Result<ProofState> {
323328
// Reuse the Z3 SMT-LIB parser since dReal accepts SMT-LIB 2.0 format
324329
let mut parser = SmtParser::new(content);
325-
parser.parse()
330+
let mut state = parser.parse()?;
331+
state.metadata.insert(
332+
"dreal_source".to_string(),
333+
serde_json::Value::String(content.to_string()),
334+
);
335+
Ok(state)
326336
}
327337

328338
/// dReal is a fully automated solver — interactive tactic application is
@@ -337,6 +347,31 @@ impl ProverBackend for DRealBackend {
337347
}
338348

339349
async fn verify_proof(&self, state: &ProofState) -> Result<bool> {
350+
// Prefer the original SMT-LIB source — `build_verification_query`
351+
// reconstructs from the parsed Term IR, which is lossy for any
352+
// non-trivial dReal problem.
353+
if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) {
354+
let source = tokio::fs::read_to_string(path).await?;
355+
let result = self.execute_command(&source).await?;
356+
return match result {
357+
DRealResult::Unsat => Ok(true),
358+
DRealResult::DeltaSat(_) => Ok(false),
359+
DRealResult::Unknown => Ok(false),
360+
DRealResult::Error(e) => bail!("dReal verification error: {}", e),
361+
DRealResult::Output(_) => Ok(false),
362+
};
363+
}
364+
if let Some(source) = state.metadata.get("dreal_source").and_then(|v| v.as_str()) {
365+
let result = self.execute_command(source).await?;
366+
return match result {
367+
DRealResult::Unsat => Ok(true),
368+
DRealResult::DeltaSat(_) => Ok(false),
369+
DRealResult::Unknown => Ok(false),
370+
DRealResult::Error(e) => bail!("dReal verification error: {}", e),
371+
DRealResult::Output(_) => Ok(false),
372+
};
373+
}
374+
340375
// Trivial cases: no goals or all goals are true
341376
if state.goals.is_empty() {
342377
return Ok(true);

0 commit comments

Comments
 (0)