|
| 1 | +// SPDX-FileCopyrightText: 2026 ECHIDNA Project Team |
| 2 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 3 | + |
| 4 | +//! Alt-Ergo backend |
| 5 | +//! |
| 6 | +//! Alt-Ergo is an SMT solver with native support for polymorphic first-order logic. |
| 7 | +//! Designed for program verification (Why3, Frama-C integration). |
| 8 | +//! |
| 9 | +//! Features: |
| 10 | +//! - Polymorphic first-order logic |
| 11 | +//! - Built-in theories (arithmetic, arrays, records, ADTs) |
| 12 | +//! - Native Alt-Ergo format or SMT-LIB2 |
| 13 | +//! - Excellent integration with Why3 |
| 14 | +
|
| 15 | +use async_trait::async_trait; |
| 16 | +use anyhow::{Context, Result}; |
| 17 | +use std::path::PathBuf; |
| 18 | +use std::process::Stdio; |
| 19 | +use tokio::io::{AsyncReadExt, AsyncWriteExt}; |
| 20 | +use tokio::process::Command; |
| 21 | + |
| 22 | +use super::{ProverBackend, ProverConfig, ProverKind}; |
| 23 | +use crate::core::{Goal, ProofState, Tactic, TacticResult}; |
| 24 | + |
| 25 | +/// Alt-Ergo theorem prover backend |
| 26 | +pub struct AltErgoBackend { |
| 27 | + config: ProverConfig, |
| 28 | +} |
| 29 | + |
| 30 | +impl AltErgoBackend { |
| 31 | + pub fn new(config: ProverConfig) -> Self { |
| 32 | + AltErgoBackend { config } |
| 33 | + } |
| 34 | + |
| 35 | + /// Convert proof state to Alt-Ergo native format |
| 36 | + fn to_altergo(&self, state: &ProofState) -> Result<String> { |
| 37 | + let mut ae = String::new(); |
| 38 | + |
| 39 | + // Alt-Ergo native format |
| 40 | + ae.push_str("(* Generated by ECHIDNA *)\n\n"); |
| 41 | + |
| 42 | + // Axioms |
| 43 | + for (i, axiom) in state.context.axioms.iter().enumerate() { |
| 44 | + ae.push_str(&format!("axiom axiom_{} : {};\n", i, axiom)); |
| 45 | + } |
| 46 | + |
| 47 | + ae.push_str("\n"); |
| 48 | + |
| 49 | + // Goal |
| 50 | + if let Some(goal) = state.goals.first() { |
| 51 | + ae.push_str(&format!("goal conjecture : {};\n", goal.statement)); |
| 52 | + } |
| 53 | + |
| 54 | + Ok(ae) |
| 55 | + } |
| 56 | + |
| 57 | + /// Convert to SMT-LIB2 format (alternative) |
| 58 | + fn to_smtlib2(&self, state: &ProofState) -> Result<String> { |
| 59 | + let mut smt = String::new(); |
| 60 | + |
| 61 | + smt.push_str("(set-logic ALL)\n"); |
| 62 | + |
| 63 | + // Axioms |
| 64 | + for axiom in &state.context.axioms { |
| 65 | + smt.push_str(&format!("(assert {})\n", axiom)); |
| 66 | + } |
| 67 | + |
| 68 | + // Goal (negated for refutation) |
| 69 | + if let Some(goal) = state.goals.first() { |
| 70 | + smt.push_str(&format!("(assert (not {}))\n", goal.statement)); |
| 71 | + } |
| 72 | + |
| 73 | + smt.push_str("(check-sat)\n"); |
| 74 | + |
| 75 | + Ok(smt) |
| 76 | + } |
| 77 | + |
| 78 | + /// Parse Alt-Ergo output |
| 79 | + fn parse_result(&self, output: &str) -> Result<bool> { |
| 80 | + // Alt-Ergo output patterns: |
| 81 | + // - "Valid" = proof succeeded |
| 82 | + // - "I don't know" or "Unknown" = inconclusive |
| 83 | + // - "Timeout" = timeout |
| 84 | + |
| 85 | + if output.contains("Valid") |
| 86 | + || output.contains("unsat") // SMT-LIB2 mode |
| 87 | + { |
| 88 | + Ok(true) |
| 89 | + } else if output.contains("Invalid") |
| 90 | + || output.contains("sat") // SMT-LIB2 mode |
| 91 | + { |
| 92 | + Ok(false) |
| 93 | + } else { |
| 94 | + Err(anyhow::anyhow!( |
| 95 | + "Alt-Ergo inconclusive: {}", |
| 96 | + output.lines().take(10).collect::<Vec<_>>().join("\n") |
| 97 | + )) |
| 98 | + } |
| 99 | + } |
| 100 | +} |
| 101 | + |
| 102 | +#[async_trait] |
| 103 | +impl ProverBackend for AltErgoBackend { |
| 104 | + fn kind(&self) -> ProverKind { |
| 105 | + ProverKind::AltErgo |
| 106 | + } |
| 107 | + |
| 108 | + async fn version(&self) -> Result<String> { |
| 109 | + let output = Command::new(&self.config.executable) |
| 110 | + .arg("--version") |
| 111 | + .output() |
| 112 | + .await |
| 113 | + .context("Failed to run alt-ergo --version")?; |
| 114 | + |
| 115 | + let stdout = String::from_utf8_lossy(&output.stdout); |
| 116 | + Ok(stdout.lines().next().unwrap_or("unknown").trim().to_string()) |
| 117 | + } |
| 118 | + |
| 119 | + async fn parse_file(&self, path: PathBuf) -> Result<ProofState> { |
| 120 | + let content = tokio::fs::read_to_string(path) |
| 121 | + .await |
| 122 | + .context("Failed to read proof file")?; |
| 123 | + self.parse_string(&content).await |
| 124 | + } |
| 125 | + |
| 126 | + async fn parse_string(&self, content: &str) -> Result<ProofState> { |
| 127 | + // Parse Alt-Ergo native format |
| 128 | + let mut state = ProofState::default(); |
| 129 | + |
| 130 | + for line in content.lines() { |
| 131 | + let line = line.trim(); |
| 132 | + if line.is_empty() || line.starts_with("(*") { |
| 133 | + continue; |
| 134 | + } |
| 135 | + |
| 136 | + if line.starts_with("axiom ") { |
| 137 | + if let Some(formula) = line.strip_prefix("axiom ").and_then(|s| s.strip_suffix(";")) { |
| 138 | + if let Some((_, body)) = formula.split_once(':') { |
| 139 | + state.context.axioms.push(body.trim().to_string()); |
| 140 | + } |
| 141 | + } |
| 142 | + } else if line.starts_with("goal ") { |
| 143 | + if let Some(formula) = line.strip_prefix("goal ").and_then(|s| s.strip_suffix(";")) { |
| 144 | + if let Some((_, body)) = formula.split_once(':') { |
| 145 | + state.goals.push(Goal { |
| 146 | + statement: body.trim().to_string(), |
| 147 | + context: state.context.clone(), |
| 148 | + }); |
| 149 | + } |
| 150 | + } |
| 151 | + } |
| 152 | + } |
| 153 | + |
| 154 | + Ok(state) |
| 155 | + } |
| 156 | + |
| 157 | + async fn apply_tactic(&self, _state: &ProofState, _tactic: &Tactic) -> Result<TacticResult> { |
| 158 | + Err(anyhow::anyhow!( |
| 159 | + "Alt-Ergo is fully automated - interactive tactics not supported" |
| 160 | + )) |
| 161 | + } |
| 162 | + |
| 163 | + async fn verify_proof(&self, state: &ProofState) -> Result<bool> { |
| 164 | + // Use native Alt-Ergo format |
| 165 | + let ae_code = self.to_altergo(state)?; |
| 166 | + |
| 167 | + let mut child = Command::new(&self.config.executable) |
| 168 | + .arg("--timeout").arg(format!("{}", self.config.timeout)) |
| 169 | + .arg("--produce-models") // Enable model generation |
| 170 | + .arg("-") // Read from stdin |
| 171 | + .stdin(Stdio::piped()) |
| 172 | + .stdout(Stdio::piped()) |
| 173 | + .stderr(Stdio::piped()) |
| 174 | + .spawn() |
| 175 | + .context("Failed to spawn Alt-Ergo process")?; |
| 176 | + |
| 177 | + if let Some(mut stdin) = child.stdin.take() { |
| 178 | + stdin.write_all(ae_code.as_bytes()).await?; |
| 179 | + stdin.flush().await?; |
| 180 | + drop(stdin); |
| 181 | + } |
| 182 | + |
| 183 | + let output = tokio::time::timeout( |
| 184 | + tokio::time::Duration::from_secs(self.config.timeout + 5), |
| 185 | + child.wait_with_output(), |
| 186 | + ) |
| 187 | + .await |
| 188 | + .context("Alt-Ergo timed out")??; |
| 189 | + |
| 190 | + let stdout = String::from_utf8_lossy(&output.stdout); |
| 191 | + self.parse_result(&stdout) |
| 192 | + } |
| 193 | + |
| 194 | + async fn export(&self, state: &ProofState) -> Result<String> { |
| 195 | + self.to_altergo(state) |
| 196 | + } |
| 197 | + |
| 198 | + async fn suggest_tactics(&self, _state: &ProofState, _limit: usize) -> Result<Vec<Tactic>> { |
| 199 | + Ok(vec![]) |
| 200 | + } |
| 201 | + |
| 202 | + async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> { |
| 203 | + Ok(vec![]) |
| 204 | + } |
| 205 | + |
| 206 | + fn config(&self) -> &ProverConfig { |
| 207 | + &self.config |
| 208 | + } |
| 209 | + |
| 210 | + fn set_config(&mut self, config: ProverConfig) { |
| 211 | + self.config = config; |
| 212 | + } |
| 213 | +} |
0 commit comments