aprender_contracts_cli/
lib.rs

1//! `pv` -- provable-contracts CLI.
2//!
3//! The command surface lives here rather than in `main.rs` so that something
4//! other than the `pv` binary can reach it: `apr pv <cmd>` and `pv <cmd>` now
5//! call the same [`dispatch`].
6
7pub mod cli;
8pub mod commands;
9pub mod contract_walk;
10pub mod json_obj;
11pub mod query_args;
12
13// `PathBuf` is imported rather than fully qualified because the `#[cfg(test)]`
14// include modules below open with `use super::*` and take it from here — as
15// they did from `main.rs` before the command surface moved into this library.
16use std::path::PathBuf;
17use std::str::FromStr;
18
19use clap::Parser;
20use cli::Commands;
21
22/// Glance form, printed by `pv -V`. One line, and it names the tool.
23///
24/// clap renders `{name} {version}`, so this yields
25/// `pv 0.63.0 (aprender provable-contracts verifier)`. The bare semver stays the
26/// SECOND whitespace field because `scripts/pv_bin.sh` reads it positionally to
27/// prove a resolved binary was built from HEAD.
28const SHORT_VERSION: &str = concat!(
29    env!("CARGO_PKG_VERSION"),
30    " (aprender provable-contracts verifier)"
31);
32
33/// Full form, printed by `pv --version`.
34///
35/// Four things claim the name `pv` on a developer box: `pv(1)` the pipe viewer
36/// from every distro, the `pv` crate on crates.io (also a pipe viewer, first
37/// published 2019), this binary, and — until #2553 — the aprender facade. The
38/// operator settled that this tool KEEPS the name (2026-08-21), which makes this
39/// string the mitigation the project relies on, so it rules the others out by
40/// name rather than merely describing itself. See #2559 and
41/// `tests/version_identity.rs`.
42const LONG_VERSION: &str = concat!(
43    env!("CARGO_PKG_VERSION"),
44    " (aprender provable-contracts verifier)\n",
45    "crate aprender-contracts-cli — ",
46    env!("CARGO_PKG_REPOSITORY"),
47    "\n",
48    "Verifies YAML contracts under contracts/; run `pv --help` for the command surface.\n",
49    "This is NOT pv(1), the pipe viewer (distro package `pv`, or the `pv` crate on crates.io)."
50);
51
52/// Top-level CLI argument parser for the `pv` command
53#[derive(Parser)]
54#[command(
55    name = "pv",
56    about = "provable-contracts — papers to provable Rust kernels",
57    version = SHORT_VERSION,
58    long_version = LONG_VERSION
59)]
60pub struct Cli {
61    /// The command to run
62    #[command(subcommand)]
63    pub command: Commands,
64
65    /// Suppress non-essential output
66    #[arg(short, long, global = true)]
67    pub quiet: bool,
68
69    /// Verbose output
70    #[arg(short, long, global = true)]
71    pub verbose: bool,
72}
73
74/// Dispatch a parsed CLI subcommand to its handler.
75///
76/// Public so `apr pv` executes the identical code path rather than a copy of
77/// it. The `pv` binary keeps shipping under its own name -- that is a decided
78/// design, not an oversight -- but the command surface lived in a `main.rs`,
79/// importable by nothing, so `apr pv` could not exist.
80///
81/// # Errors
82/// Propagates whatever the selected subcommand returns.
83#[allow(clippy::too_many_lines)]
84pub fn dispatch(command: Commands) -> Result<(), Box<dyn std::error::Error>> {
85    match command {
86        Commands::Explain {
87            contract,
88            format,
89            binding,
90        } => commands::explain::run(&contract, binding.as_deref(), &format),
91        Commands::Validate { contract } => commands::validate::run(&contract),
92        Commands::CheckParity { contract } => commands::check_parity::run(&contract),
93        Commands::Scaffold {
94            contract,
95            r#trait,
96            output,
97        } => commands::scaffold::run(&contract, r#trait, output.as_deref()),
98        Commands::ExtractPytorch { target, output } => {
99            commands::extract::run(&target, output.as_deref())
100        }
101        Commands::Codegen {
102            contract_dir,
103            output,
104        } => commands::codegen::run(&contract_dir, output.as_deref()),
105        Commands::Kani { contract } => commands::kani::run(&contract),
106        Commands::Probar { contract, binding } => {
107            commands::probar::run(&contract, binding.as_deref())
108        }
109        Commands::Status { contract } => commands::status::run(&contract),
110        Commands::Audit {
111            contract, binding, ..
112        } => commands::audit::run(&contract, binding.as_deref()),
113        Commands::Diff { old, new } => commands::diff::run(&old, &new),
114        Commands::Coverage {
115            contract_dir,
116            binding,
117            fuzz,
118            reverse,
119            enforcement,
120        } => commands::coverage::run(
121            &contract_dir,
122            binding.as_deref(),
123            fuzz,
124            reverse.as_deref(),
125            enforcement.as_deref(),
126        ),
127        Commands::Generate {
128            contract,
129            output,
130            binding,
131            readme,
132            ci,
133        } => commands::generate::run(&contract, &output, binding.as_deref(), readme, ci),
134        Commands::Graph {
135            contract_dir,
136            format,
137        } => match commands::graph::GraphFormat::from_str(&format) {
138            Ok(fmt) => commands::graph::run(&contract_dir, fmt),
139            Err(e) => Err(e.into()),
140        },
141        Commands::Equations { contract, format } => {
142            match commands::equations::OutputFormat::from_str(&format) {
143                Ok(fmt) => commands::equations::run(&contract, fmt),
144                Err(e) => Err(e.into()),
145            }
146        }
147        Commands::Lean {
148            contract,
149            output_dir,
150        } => commands::lean::run(&contract, output_dir.as_deref()),
151        Commands::LeanStatus { path } => commands::lean_status::run(&path),
152        Commands::ProofStatus {
153            path,
154            binding,
155            verify_bindings,
156            format,
157            table,
158            kind,
159        } => commands::proof_status::run(
160            &path,
161            binding.as_deref(),
162            verify_bindings.as_deref(),
163            &format,
164            table,
165            kind.as_deref(),
166        ),
167        Commands::Lint {
168            contract_dir,
169            min_score,
170            binding,
171            format,
172            severity,
173            strict,
174            suppress,
175            suppress_rule,
176            suppress_file,
177            rule,
178            config,
179            diff_ref,
180            trend,
181            show_trend,
182            no_cache,
183            cache_stats,
184            coverage,
185            min_coverage,
186            crate_dir,
187            min_level,
188            explain,
189            watch,
190            strict_test_binding,
191            ..
192        } => {
193            if let Some(ref rule_id) = explain {
194                commands::lint::explain_rule(rule_id);
195                return Ok(());
196            }
197            commands::lint::run(
198                &contract_dir,
199                binding.as_deref(),
200                min_score,
201                format.as_deref(),
202                severity.as_deref(),
203                strict,
204                suppress.as_deref(),
205                suppress_rule.as_deref(),
206                suppress_file.as_deref(),
207                &rule,
208                config.as_deref(),
209                diff_ref.as_deref(),
210                trend,
211                show_trend,
212                no_cache,
213                cache_stats,
214                coverage,
215                min_coverage,
216                crate_dir.as_deref(),
217                min_level.as_deref(),
218                watch,
219                strict_test_binding,
220            )
221        }
222        Commands::Score {
223            path,
224            binding,
225            format,
226            min_score,
227            summary,
228            top_gaps,
229            weights,
230            pvscore,
231            ..
232        } => commands::score::run(
233            &path,
234            binding.as_deref(),
235            &format,
236            min_score,
237            summary,
238            top_gaps,
239            weights.as_deref(),
240            pvscore,
241        ),
242        Commands::Query(q) => commands::query::run(&commands::query::QueryCliParams {
243            contract_dir: &q.contract_dir,
244            query_str: &q.query,
245            regex: q.regex,
246            literal: q.literal,
247            case_sensitive: q.case_sensitive,
248            limit: q.limit,
249            obligation: q.obligation.as_deref(),
250            min_score: q.min_score,
251            min_level: q.min_level,
252            depends_on: q.depends_on.as_deref(),
253            depended_by: q.depended_by.as_deref(),
254            unproven: q.unproven,
255            show_score: q.score,
256            show_graph: q.graph,
257            show_paper: q.paper,
258            show_proof_status: q.proof_status,
259            show_binding: q.binding_info,
260            binding_gaps: q.binding_gaps,
261            show_diff: q.diff,
262            show_pagerank: q.pagerank,
263            show_call_sites: q.call_sites,
264            show_violations: q.violations,
265            show_coverage_map: q.coverage_map,
266            project_filter: q.project.as_deref(),
267            include_project: q.include_project.as_deref(),
268            tier: q.tier,
269            class: q.class,
270            kind: q.kind.as_deref(),
271            all_projects: q.all_projects,
272            rebuild_index: q.rebuild_index,
273            binding: q.binding.as_deref(),
274            format: &q.format,
275            exit_code: q.exit_code,
276        }),
277        Commands::Invariants { contract } => commands::invariants::run(&contract),
278        Commands::Coq { contract } => commands::coq::run(&contract),
279        Commands::Fuzz { contract } => commands::fuzz::run(&contract),
280        Commands::Mirai { contract } => commands::mirai::run(&contract),
281        Commands::Flux { contract } => commands::flux::run(&contract),
282        Commands::Tla { contract_dir } => commands::tla::run(&contract_dir),
283        Commands::Book {
284            contract_dir,
285            output,
286            update_summary,
287            summary_path,
288        } => commands::book::run(
289            &contract_dir,
290            &output,
291            update_summary,
292            summary_path.as_deref(),
293        ),
294        Commands::Infer {
295            crate_dir,
296            binding,
297            contract_dir,
298            top,
299        } => commands::infer::run(&crate_dir, &binding, &contract_dir, top),
300        Commands::Unlock { contract, reason } => commands::unlock::run(&contract, &reason),
301        Commands::Roofline {
302            contract_dir,
303            params,
304            bits,
305            hardware,
306            format,
307        } => commands::roofline::run(&contract_dir, params, bits, &hardware, &format),
308        Commands::Pipeline { pipeline, format } => commands::pipeline::run(&pipeline, &format),
309        Commands::Kaizen {
310            contract_dir,
311            src_root,
312            repo,
313            dry_run,
314            codegen,
315            fix,
316            json,
317            min_score,
318        } => {
319            let default_root = PathBuf::from("..");
320            let root = src_root.as_deref().unwrap_or(&default_root);
321            commands::kaizen::run(
322                &contract_dir,
323                root,
324                repo.as_deref(),
325                dry_run || !fix, // default to dry-run unless --fix
326                codegen || fix,  // --fix implies --codegen
327                fix,
328                json,
329                min_score,
330            )
331        }
332        Commands::VerifyBindings {
333            binding,
334            output,
335            crate_name,
336        } => commands::verify_bindings::run(&binding, output.as_deref(), crate_name.as_deref()),
337        Commands::Certify {
338            contract_dir,
339            config,
340            output,
341        } => commands::certify::run(&contract_dir, config.as_deref(), output.as_deref()),
342        Commands::VerifyStructure {
343            contract_dir,
344            config,
345            model,
346        } => commands::verify_structure::run(&contract_dir, config.as_deref(), model.as_deref()),
347        Commands::VerifyPipeline {
348            contract_dir,
349            format,
350        } => {
351            commands::verify_pipeline::run(&contract_dir, &format);
352            Ok(())
353        }
354        Commands::Migrate {
355            contract_dir,
356            dry_run,
357        } => commands::migrate::run(&contract_dir, dry_run),
358    }
359}
360
361/// Parse `argv` and run one command, exiting non-zero on failure. This is the
362/// whole of the standalone `pv` binary.
363pub fn run() {
364    let cli = Cli::parse();
365    let _ = (cli.quiet, cli.verbose); // Flags accepted; used by subcommands via Cli struct
366
367    if let Err(e) = dispatch(cli.command) {
368        eprintln!("error: {e}");
369        std::process::exit(1);
370    }
371}
372
373#[cfg(test)]
374#[path = "../tests/includes/version_identity_unit.rs"]
375mod version_identity_unit;
376
377#[cfg(test)]
378#[path = "../tests/includes/dispatch_tests.rs"]
379mod dispatch_tests;
380
381#[cfg(test)]
382#[path = "../tests/includes/dispatch_query_tests.rs"]
383mod dispatch_query_tests;
aprender_contracts_cli/lib.rs

aprender_contracts_cli/
lib.rs
