karpal_verify/
command.rs

1#[cfg(not(feature = "std"))]
2use alloc::{string::String, vec::Vec};
3#[cfg(feature = "std")]
4use std::{path::Path, string::String, vec::Vec};
5
6/// External prover backend command kind.
7#[derive(Debug, Clone, Copy, PartialEq, Eq)]
8pub enum CommandKind {
9    Smt,
10    Lean,
11}
12
13/// Command-line configuration for an SMT solver.
14#[derive(Debug, Clone, PartialEq, Eq)]
15pub struct SmtConfig {
16    pub executable: String,
17    pub args: Vec<String>,
18}
19
20impl Default for SmtConfig {
21    fn default() -> Self {
22        Self {
23            executable: "z3".into(),
24            args: vec!["-smt2".into()],
25        }
26    }
27}
28
29impl SmtConfig {
30    pub fn new(executable: impl Into<String>) -> Self {
31        Self {
32            executable: executable.into(),
33            args: Vec::new(),
34        }
35    }
36
37    pub fn with_arg(mut self, arg: impl Into<String>) -> Self {
38        self.args.push(arg.into());
39        self
40    }
41}
42
43/// How Lean verification should be executed.
44#[derive(Debug, Clone, PartialEq, Eq)]
45pub enum LeanDriver {
46    Direct,
47    LakeEnv,
48    LakeBuild,
49}
50
51/// Command-line configuration for Lean 4.
52#[derive(Debug, Clone, PartialEq, Eq)]
53pub struct LeanConfig {
54    pub executable: String,
55    pub args: Vec<String>,
56    pub driver: LeanDriver,
57    pub lake_executable: String,
58    pub lake_args: Vec<String>,
59}
60
61impl Default for LeanConfig {
62    fn default() -> Self {
63        Self {
64            executable: "lean".into(),
65            args: Vec::new(),
66            driver: LeanDriver::Direct,
67            lake_executable: "lake".into(),
68            lake_args: Vec::new(),
69        }
70    }
71}
72
73impl LeanConfig {
74    pub fn new(executable: impl Into<String>) -> Self {
75        Self {
76            executable: executable.into(),
77            ..Self::default()
78        }
79    }
80
81    pub fn with_arg(mut self, arg: impl Into<String>) -> Self {
82        self.args.push(arg.into());
83        self
84    }
85
86    pub fn with_driver(mut self, driver: LeanDriver) -> Self {
87        self.driver = driver;
88        self
89    }
90
91    pub fn with_lake_executable(mut self, executable: impl Into<String>) -> Self {
92        self.lake_executable = executable.into();
93        self
94    }
95
96    pub fn with_lake_arg(mut self, arg: impl Into<String>) -> Self {
97        self.lake_args.push(arg.into());
98        self
99    }
100}
101
102/// Dry-run invocation plan for an external tool.
103#[derive(Debug, Clone, PartialEq, Eq)]
104pub struct InvocationPlan {
105    pub kind: CommandKind,
106    pub executable: String,
107    pub args: Vec<String>,
108    pub working_directory: Option<String>,
109    pub input_files: Vec<String>,
110}
111
112impl InvocationPlan {
113    pub fn render_shell(&self) -> String {
114        let joined = self
115            .args
116            .iter()
117            .map(|arg| shell_escape(arg))
118            .collect::<Vec<_>>()
119            .join(" ");
120        if joined.is_empty() {
121            self.executable.clone()
122        } else {
123            format!("{} {}", self.executable, joined)
124        }
125    }
126}
127
128#[cfg(feature = "std")]
129impl InvocationPlan {
130    pub fn smt(config: &SmtConfig, script: impl AsRef<Path>) -> Self {
131        let script = script.as_ref().to_path_buf();
132        let mut args = config.args.clone();
133        args.push(script.to_string_lossy().into_owned());
134        Self {
135            kind: CommandKind::Smt,
136            executable: config.executable.clone(),
137            args,
138            working_directory: script.parent().map(path_to_string),
139            input_files: vec![path_to_string(&script)],
140        }
141    }
142
143    pub fn lean(config: &LeanConfig, module: impl AsRef<Path>) -> Self {
144        let module = module.as_ref().to_path_buf();
145        match config.driver {
146            LeanDriver::Direct => {
147                let mut args = config.args.clone();
148                args.push(module.to_string_lossy().into_owned());
149                Self {
150                    kind: CommandKind::Lean,
151                    executable: config.executable.clone(),
152                    args,
153                    working_directory: module.parent().map(path_to_string),
154                    input_files: vec![path_to_string(&module)],
155                }
156            }
157            LeanDriver::LakeEnv => {
158                let lean_dir = module.parent().unwrap_or_else(|| Path::new("."));
159                let root = lean_dir.parent().unwrap_or(lean_dir);
160                let relative_module = module
161                    .strip_prefix(root)
162                    .unwrap_or(&module)
163                    .to_string_lossy()
164                    .into_owned();
165                let mut args = config.lake_args.clone();
166                args.push("env".into());
167                args.push(config.executable.clone());
168                args.extend(config.args.iter().cloned());
169                args.push(relative_module);
170                Self {
171                    kind: CommandKind::Lean,
172                    executable: config.lake_executable.clone(),
173                    args,
174                    working_directory: Some(path_to_string(root)),
175                    input_files: vec![
176                        path_to_string(&module),
177                        path_to_string(&root.join("lakefile.lean")),
178                        path_to_string(&root.join("lean-toolchain")),
179                    ],
180                }
181            }
182            LeanDriver::LakeBuild => {
183                let lean_dir = module.parent().unwrap_or_else(|| Path::new("."));
184                let root = lean_dir.parent().unwrap_or(lean_dir);
185                let module_target = module
186                    .file_stem()
187                    .and_then(|stem| stem.to_str())
188                    .unwrap_or("Main")
189                    .to_string();
190                let mut args = config.lake_args.clone();
191                args.push("build".into());
192                args.push(module_target);
193                Self {
194                    kind: CommandKind::Lean,
195                    executable: config.lake_executable.clone(),
196                    args,
197                    working_directory: Some(path_to_string(root)),
198                    input_files: vec![
199                        path_to_string(&module),
200                        path_to_string(&root.join("lakefile.lean")),
201                        path_to_string(&root.join("lean-toolchain")),
202                    ],
203                }
204            }
205        }
206    }
207}
208
209#[cfg(feature = "std")]
210fn path_to_string(path: &Path) -> String {
211    path.to_string_lossy().into_owned()
212}
213
214fn shell_escape(arg: &str) -> String {
215    if arg
216        .chars()
217        .all(|c| c.is_ascii_alphanumeric() || matches!(c, '/' | '-' | '_' | '.' | ':'))
218    {
219        arg.to_string()
220    } else {
221        format!("'{}'", arg.replace('\'', "'\\''"))
222    }
223}
224
225#[cfg(test)]
226mod tests {
227    use super::*;
228
229    #[test]
230    fn shell_render_quotes_complex_args() {
231        let plan = InvocationPlan {
232            kind: CommandKind::Lean,
233            executable: "lean".into(),
234            args: vec!["My File.lean".into()],
235            working_directory: None,
236            input_files: vec!["My File.lean".into()],
237        };
238        assert!(plan.render_shell().contains("'My File.lean'"));
239    }
240
241    #[cfg(feature = "std")]
242    #[test]
243    fn smt_plan_includes_script_path() {
244        let plan = InvocationPlan::smt(
245            &SmtConfig::default(),
246            std::path::PathBuf::from("out/test.smt2"),
247        );
248        assert_eq!(plan.kind, CommandKind::Smt);
249        assert!(plan.input_files[0].ends_with("test.smt2"));
250    }
251
252    #[cfg(feature = "std")]
253    #[test]
254    fn lean_project_plan_uses_lake_from_project_root() {
255        let plan = InvocationPlan::lean(
256            &LeanConfig::default().with_driver(LeanDriver::LakeEnv),
257            std::path::PathBuf::from("target/verify/lean/KarpalVerify.lean"),
258        );
259        assert_eq!(plan.kind, CommandKind::Lean);
260        assert_eq!(plan.executable, "lake");
261        assert_eq!(plan.working_directory.as_deref(), Some("target/verify"));
262        assert_eq!(plan.args, vec!["env", "lean", "lean/KarpalVerify.lean"]);
263        assert!(
264            plan.input_files
265                .iter()
266                .any(|path| path.ends_with("lakefile.lean"))
267        );
268        assert!(
269            plan.input_files
270                .iter()
271                .any(|path| path.ends_with("lean-toolchain"))
272        );
273    }
274
275    #[cfg(feature = "std")]
276    #[test]
277    fn lean_project_plan_can_use_lake_build() {
278        let plan = InvocationPlan::lean(
279            &LeanConfig::default().with_driver(LeanDriver::LakeBuild),
280            std::path::PathBuf::from("target/verify/lean/KarpalVerify.lean"),
281        );
282        assert_eq!(plan.kind, CommandKind::Lean);
283        assert_eq!(plan.executable, "lake");
284        assert_eq!(plan.working_directory.as_deref(), Some("target/verify"));
285        assert_eq!(plan.args, vec!["build", "KarpalVerify"]);
286        assert!(
287            plan.input_files
288                .iter()
289                .any(|path| path.ends_with("lakefile.lean"))
290        );
291        assert!(
292            plan.input_files
293                .iter()
294                .any(|path| path.ends_with("lean-toolchain"))
295        );
296    }
297}
karpal_verify/command.rs

karpal_verify/
command.rs
