karpal_verify/
command.rs

1// Copyright (C) 2026 Industrial Algebra
2// SPDX-License-Identifier: Apache-2.0
3
4#[cfg(not(feature = "std"))]
5use alloc::{string::String, vec::Vec};
6#[cfg(feature = "std")]
7use std::{path::Path, string::String, vec::Vec};
8
9/// External prover backend command kind.
10#[derive(Debug, Clone, Copy, PartialEq, Eq)]
11pub enum CommandKind {
12    Smt,
13    Lean,
14    Kani,
15}
16
17/// Command-line configuration for an SMT solver.
18#[derive(Debug, Clone, PartialEq, Eq)]
19pub struct SmtConfig {
20    pub executable: String,
21    pub args: Vec<String>,
22}
23
24impl Default for SmtConfig {
25    fn default() -> Self {
26        Self {
27            executable: "z3".into(),
28            args: vec!["-smt2".into()],
29        }
30    }
31}
32
33impl SmtConfig {
34    pub fn new(executable: impl Into<String>) -> Self {
35        Self {
36            executable: executable.into(),
37            args: Vec::new(),
38        }
39    }
40
41    pub fn with_arg(mut self, arg: impl Into<String>) -> Self {
42        self.args.push(arg.into());
43        self
44    }
45}
46
47/// How Lean verification should be executed.
48#[derive(Debug, Clone, PartialEq, Eq)]
49pub enum LeanDriver {
50    Direct,
51    LakeEnv,
52    LakeBuild,
53}
54
55/// Command-line configuration for Lean 4.
56#[derive(Debug, Clone, PartialEq, Eq)]
57pub struct LeanConfig {
58    pub executable: String,
59    pub args: Vec<String>,
60    pub driver: LeanDriver,
61    pub lake_executable: String,
62    pub lake_args: Vec<String>,
63}
64
65impl Default for LeanConfig {
66    fn default() -> Self {
67        Self {
68            executable: "lean".into(),
69            args: Vec::new(),
70            driver: LeanDriver::Direct,
71            lake_executable: "lake".into(),
72            lake_args: Vec::new(),
73        }
74    }
75}
76
77impl LeanConfig {
78    pub fn new(executable: impl Into<String>) -> Self {
79        Self {
80            executable: executable.into(),
81            ..Self::default()
82        }
83    }
84
85    pub fn with_arg(mut self, arg: impl Into<String>) -> Self {
86        self.args.push(arg.into());
87        self
88    }
89
90    pub fn with_driver(mut self, driver: LeanDriver) -> Self {
91        self.driver = driver;
92        self
93    }
94
95    pub fn with_lake_executable(mut self, executable: impl Into<String>) -> Self {
96        self.lake_executable = executable.into();
97        self
98    }
99
100    pub fn with_lake_arg(mut self, arg: impl Into<String>) -> Self {
101        self.lake_args.push(arg.into());
102        self
103    }
104}
105
106/// Command-line configuration for Kani bounded model checking.
107#[derive(Debug, Clone, PartialEq, Eq)]
108pub struct KaniConfig {
109    pub executable: String,
110    pub args: Vec<String>,
111}
112
113impl Default for KaniConfig {
114    fn default() -> Self {
115        Self {
116            executable: "kani".into(),
117            args: Vec::new(),
118        }
119    }
120}
121
122impl KaniConfig {
123    pub fn new(executable: impl Into<String>) -> Self {
124        Self {
125            executable: executable.into(),
126            args: Vec::new(),
127        }
128    }
129
130    pub fn with_arg(mut self, arg: impl Into<String>) -> Self {
131        self.args.push(arg.into());
132        self
133    }
134}
135
136/// Dry-run invocation plan for an external tool.
137#[derive(Debug, Clone, PartialEq, Eq)]
138pub struct InvocationPlan {
139    pub kind: CommandKind,
140    pub executable: String,
141    pub args: Vec<String>,
142    pub working_directory: Option<String>,
143    pub input_files: Vec<String>,
144}
145
146impl InvocationPlan {
147    pub fn render_shell(&self) -> String {
148        let joined = self
149            .args
150            .iter()
151            .map(|arg| shell_escape(arg))
152            .collect::<Vec<_>>()
153            .join(" ");
154        if joined.is_empty() {
155            self.executable.clone()
156        } else {
157            format!("{} {}", self.executable, joined)
158        }
159    }
160}
161
162#[cfg(feature = "std")]
163impl InvocationPlan {
164    pub fn smt(config: &SmtConfig, script: impl AsRef<Path>) -> Self {
165        let script = script.as_ref().to_path_buf();
166        let working_directory = working_directory_for(&script);
167        let mut args = config.args.clone();
168        args.push(path_arg_for_working_directory(
169            &script,
170            working_directory.as_deref(),
171        ));
172        Self {
173            kind: CommandKind::Smt,
174            executable: config.executable.clone(),
175            args,
176            working_directory,
177            input_files: vec![path_to_string(&script)],
178        }
179    }
180
181    pub fn lean(config: &LeanConfig, module: impl AsRef<Path>) -> Self {
182        let module = module.as_ref().to_path_buf();
183        match config.driver {
184            LeanDriver::Direct => {
185                let working_directory = working_directory_for(&module);
186                let mut args = config.args.clone();
187                args.push(path_arg_for_working_directory(
188                    &module,
189                    working_directory.as_deref(),
190                ));
191                Self {
192                    kind: CommandKind::Lean,
193                    executable: config.executable.clone(),
194                    args,
195                    working_directory,
196                    input_files: vec![path_to_string(&module)],
197                }
198            }
199            LeanDriver::LakeEnv => {
200                let lean_dir = module.parent().unwrap_or_else(|| Path::new("."));
201                let root = lean_dir.parent().unwrap_or(lean_dir);
202                let relative_module = module
203                    .strip_prefix(root)
204                    .unwrap_or(&module)
205                    .to_string_lossy()
206                    .into_owned();
207                let mut args = config.lake_args.clone();
208                args.push("env".into());
209                args.push(config.executable.clone());
210                args.extend(config.args.iter().cloned());
211                args.push(relative_module);
212                Self {
213                    kind: CommandKind::Lean,
214                    executable: config.lake_executable.clone(),
215                    args,
216                    working_directory: Some(path_to_string(root)),
217                    input_files: vec![
218                        path_to_string(&module),
219                        path_to_string(&root.join("lakefile.lean")),
220                        path_to_string(&root.join("lean-toolchain")),
221                    ],
222                }
223            }
224            LeanDriver::LakeBuild => {
225                let lean_dir = module.parent().unwrap_or_else(|| Path::new("."));
226                let root = lean_dir.parent().unwrap_or(lean_dir);
227                let module_target = module
228                    .file_stem()
229                    .and_then(|stem| stem.to_str())
230                    .unwrap_or("Main")
231                    .to_string();
232                let mut args = config.lake_args.clone();
233                args.push("build".into());
234                args.push(module_target);
235                Self {
236                    kind: CommandKind::Lean,
237                    executable: config.lake_executable.clone(),
238                    args,
239                    working_directory: Some(path_to_string(root)),
240                    input_files: vec![
241                        path_to_string(&module),
242                        path_to_string(&root.join("lakefile.lean")),
243                        path_to_string(&root.join("lean-toolchain")),
244                    ],
245                }
246            }
247        }
248    }
249
250    pub fn kani(config: &KaniConfig, harness: impl AsRef<Path>, harness_name: &str) -> Self {
251        let harness = harness.as_ref().to_path_buf();
252        let working_directory = working_directory_for(&harness);
253        let mut args = config.args.clone();
254        args.push("--harness".into());
255        args.push(harness_name.into());
256        args.push(path_arg_for_working_directory(
257            &harness,
258            working_directory.as_deref(),
259        ));
260        Self {
261            kind: CommandKind::Kani,
262            executable: config.executable.clone(),
263            args,
264            working_directory,
265            input_files: vec![path_to_string(&harness)],
266        }
267    }
268}
269
270#[cfg(feature = "std")]
271fn working_directory_for(path: &Path) -> Option<String> {
272    path.parent()
273        .filter(|parent| !parent.as_os_str().is_empty())
274        .map(path_to_string)
275}
276
277#[cfg(feature = "std")]
278fn path_arg_for_working_directory(path: &Path, working_directory: Option<&str>) -> String {
279    if working_directory.is_some() {
280        path.file_name()
281            .and_then(|file_name| file_name.to_str())
282            .map(String::from)
283            .unwrap_or_else(|| path_to_string(path))
284    } else {
285        path_to_string(path)
286    }
287}
288
289#[cfg(feature = "std")]
290fn path_to_string(path: &Path) -> String {
291    path.to_string_lossy().into_owned()
292}
293
294fn shell_escape(arg: &str) -> String {
295    if arg
296        .chars()
297        .all(|c| c.is_ascii_alphanumeric() || matches!(c, '/' | '-' | '_' | '.' | ':'))
298    {
299        arg.to_string()
300    } else {
301        format!("'{}'", arg.replace('\'', "'\\''"))
302    }
303}
304
305#[cfg(test)]
306mod tests {
307    use super::*;
308
309    #[test]
310    fn shell_render_quotes_complex_args() {
311        let plan = InvocationPlan {
312            kind: CommandKind::Lean,
313            executable: "lean".into(),
314            args: vec!["My File.lean".into()],
315            working_directory: None,
316            input_files: vec!["My File.lean".into()],
317        };
318        assert!(plan.render_shell().contains("'My File.lean'"));
319    }
320
321    #[cfg(feature = "std")]
322    #[test]
323    fn smt_plan_includes_script_path() {
324        let plan = InvocationPlan::smt(
325            &SmtConfig::default(),
326            std::path::PathBuf::from("out/test.smt2"),
327        );
328        assert_eq!(plan.kind, CommandKind::Smt);
329        assert!(plan.input_files[0].ends_with("test.smt2"));
330    }
331
332    #[cfg(feature = "std")]
333    #[test]
334    fn lean_project_plan_uses_lake_from_project_root() {
335        let plan = InvocationPlan::lean(
336            &LeanConfig::default().with_driver(LeanDriver::LakeEnv),
337            std::path::PathBuf::from("target/verify/lean/KarpalVerify.lean"),
338        );
339        assert_eq!(plan.kind, CommandKind::Lean);
340        assert_eq!(plan.executable, "lake");
341        assert_eq!(plan.working_directory.as_deref(), Some("target/verify"));
342        assert_eq!(plan.args, vec!["env", "lean", "lean/KarpalVerify.lean"]);
343        assert!(
344            plan.input_files
345                .iter()
346                .any(|path| path.ends_with("lakefile.lean"))
347        );
348        assert!(
349            plan.input_files
350                .iter()
351                .any(|path| path.ends_with("lean-toolchain"))
352        );
353    }
354
355    #[cfg(feature = "std")]
356    #[test]
357    fn lean_project_plan_can_use_lake_build() {
358        let plan = InvocationPlan::lean(
359            &LeanConfig::default().with_driver(LeanDriver::LakeBuild),
360            std::path::PathBuf::from("target/verify/lean/KarpalVerify.lean"),
361        );
362        assert_eq!(plan.kind, CommandKind::Lean);
363        assert_eq!(plan.executable, "lake");
364        assert_eq!(plan.working_directory.as_deref(), Some("target/verify"));
365        assert_eq!(plan.args, vec!["build", "KarpalVerify"]);
366        assert!(
367            plan.input_files
368                .iter()
369                .any(|path| path.ends_with("lakefile.lean"))
370        );
371        assert!(
372            plan.input_files
373                .iter()
374                .any(|path| path.ends_with("lean-toolchain"))
375        );
376    }
377
378    #[cfg(feature = "std")]
379    #[test]
380    fn kani_plan_invokes_standalone_kani_for_generated_harness() {
381        let plan = InvocationPlan::kani(
382            &KaniConfig::default(),
383            std::path::PathBuf::from("target/verify/kani/sum_assoc.rs"),
384            "sum_assoc",
385        );
386        assert_eq!(plan.kind, CommandKind::Kani);
387        assert_eq!(plan.executable, "kani");
388        assert_eq!(plan.args, vec!["--harness", "sum_assoc", "sum_assoc.rs"]);
389        assert_eq!(
390            plan.working_directory.as_deref(),
391            Some("target/verify/kani")
392        );
393        assert!(plan.input_files[0].ends_with("sum_assoc.rs"));
394    }
395}
karpal_verify/command.rs

karpal_verify/
command.rs
