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

karpal_verify/
command.rs
