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 {
92            contract,
93            check_ids,
94        } => commands::validate::run(&contract, check_ids),
95        Commands::CheckParity { contract } => commands::check_parity::run(&contract),
96        Commands::Scaffold {
97            contract,
98            r#trait,
99            output,
100        } => commands::scaffold::run(&contract, r#trait, output.as_deref()),
101        Commands::ExtractPytorch { target, output } => {
102            commands::extract::run(&target, output.as_deref())
103        }
104        Commands::Codegen {
105            contract_dir,
106            output,
107        } => commands::codegen::run(&contract_dir, output.as_deref()),
108        Commands::Kani { contract } => commands::kani::run(&contract),
109        Commands::Probar { contract, binding } => {
110            commands::probar::run(&contract, binding.as_deref())
111        }
112        Commands::Status { contract } => commands::status::run(&contract),
113        Commands::Audit {
114            contract, binding, ..
115        } => commands::audit::run(&contract, binding.as_deref()),
116        Commands::Diff { old, new } => commands::diff::run(&old, &new),
117        Commands::Census {
118            contract_dir,
119            format,
120            json,
121        } => {
122            let as_json = json || matches!(format, cli::CensusFormat::Json);
123            commands::census::run(&contract_dir, as_json)
124        }
125        Commands::Coverage {
126            contract_dir,
127            binding,
128            fuzz,
129            reverse,
130            enforcement,
131        } => commands::coverage::run(
132            &contract_dir,
133            binding.as_deref(),
134            fuzz,
135            reverse.as_deref(),
136            enforcement.as_deref(),
137        ),
138        Commands::Generate {
139            contract,
140            output,
141            binding,
142            readme,
143            ci,
144        } => commands::generate::run(&contract, &output, binding.as_deref(), readme, ci),
145        Commands::Graph {
146            contract_dir,
147            format,
148        } => match commands::graph::GraphFormat::from_str(&format) {
149            Ok(fmt) => commands::graph::run(&contract_dir, fmt),
150            Err(e) => Err(e.into()),
151        },
152        Commands::Equations { contract, format } => {
153            match commands::equations::OutputFormat::from_str(&format) {
154                Ok(fmt) => commands::equations::run(&contract, fmt),
155                Err(e) => Err(e.into()),
156            }
157        }
158        Commands::Lean {
159            contract,
160            output_dir,
161        } => commands::lean::run(&contract, output_dir.as_deref()),
162        Commands::LeanStatus { path } => commands::lean_status::run(&path),
163        Commands::ProofStatus {
164            path,
165            binding,
166            verify_bindings,
167            format,
168            table,
169            kind,
170        } => commands::proof_status::run(
171            &path,
172            binding.as_deref(),
173            verify_bindings.as_deref(),
174            &format,
175            table,
176            kind.as_deref(),
177        ),
178        Commands::Lint {
179            contract_dir,
180            min_score,
181            binding,
182            format,
183            severity,
184            strict,
185            suppress,
186            suppress_rule,
187            suppress_file,
188            rule,
189            config,
190            diff_ref,
191            trend,
192            show_trend,
193            no_cache,
194            cache_stats,
195            coverage,
196            min_coverage,
197            crate_dir,
198            min_level,
199            explain,
200            watch,
201            strict_test_binding,
202            ..
203        } => {
204            if let Some(ref rule_id) = explain {
205                commands::lint::explain_rule(rule_id);
206                return Ok(());
207            }
208            commands::lint::run(
209                &contract_dir,
210                binding.as_deref(),
211                min_score,
212                format.as_deref(),
213                severity.as_deref(),
214                strict,
215                suppress.as_deref(),
216                suppress_rule.as_deref(),
217                suppress_file.as_deref(),
218                &rule,
219                config.as_deref(),
220                diff_ref.as_deref(),
221                trend,
222                show_trend,
223                no_cache,
224                cache_stats,
225                coverage,
226                min_coverage,
227                crate_dir.as_deref(),
228                min_level.as_deref(),
229                watch,
230                strict_test_binding,
231            )
232        }
233        Commands::Score {
234            path,
235            binding,
236            format,
237            min_score,
238            summary,
239            top_gaps,
240            weights,
241            pvscore,
242            ..
243        } => commands::score::run(
244            &path,
245            binding.as_deref(),
246            &format,
247            min_score,
248            summary,
249            top_gaps,
250            weights.as_deref(),
251            pvscore,
252        ),
253        Commands::Query(q) => commands::query::run(&commands::query::QueryCliParams {
254            contract_dir: &q.contract_dir,
255            query_str: &q.query,
256            regex: q.regex,
257            literal: q.literal,
258            case_sensitive: q.case_sensitive,
259            limit: q.limit,
260            obligation: q.obligation.as_deref(),
261            min_score: q.min_score,
262            min_level: q.min_level,
263            depends_on: q.depends_on.as_deref(),
264            depended_by: q.depended_by.as_deref(),
265            unproven: q.unproven,
266            show_score: q.score,
267            show_graph: q.graph,
268            show_paper: q.paper,
269            show_proof_status: q.proof_status,
270            show_binding: q.binding_info,
271            binding_gaps: q.binding_gaps,
272            show_diff: q.diff,
273            show_pagerank: q.pagerank,
274            show_call_sites: q.call_sites,
275            show_violations: q.violations,
276            show_coverage_map: q.coverage_map,
277            project_filter: q.project.as_deref(),
278            include_project: q.include_project.as_deref(),
279            tier: q.tier,
280            class: q.class,
281            kind: q.kind.as_deref(),
282            all_projects: q.all_projects,
283            rebuild_index: q.rebuild_index,
284            binding: q.binding.as_deref(),
285            format: &q.format,
286            exit_code: q.exit_code,
287        }),
288        Commands::Invariants { contract } => commands::invariants::run(&contract),
289        Commands::Coq { contract } => commands::coq::run(&contract),
290        Commands::Fuzz { contract } => commands::fuzz::run(&contract),
291        Commands::Mirai { contract } => commands::mirai::run(&contract),
292        Commands::Flux { contract } => commands::flux::run(&contract),
293        Commands::Tla { contract_dir } => commands::tla::run(&contract_dir),
294        Commands::Book {
295            contract_dir,
296            output,
297            update_summary,
298            summary_path,
299        } => commands::book::run(
300            &contract_dir,
301            &output,
302            update_summary,
303            summary_path.as_deref(),
304        ),
305        Commands::Infer {
306            crate_dir,
307            binding,
308            contract_dir,
309            top,
310        } => commands::infer::run(&crate_dir, &binding, &contract_dir, top),
311        Commands::Unlock { contract, reason } => commands::unlock::run(&contract, &reason),
312        Commands::Roofline {
313            contract_dir,
314            params,
315            bits,
316            hardware,
317            format,
318        } => commands::roofline::run(&contract_dir, params, bits, &hardware, &format),
319        Commands::Pipeline { pipeline, format } => commands::pipeline::run(&pipeline, &format),
320        Commands::Kaizen {
321            contract_dir,
322            src_root,
323            repo,
324            dry_run,
325            codegen,
326            fix,
327            json,
328            min_score,
329        } => {
330            let default_root = PathBuf::from("..");
331            let root = src_root.as_deref().unwrap_or(&default_root);
332            commands::kaizen::run(
333                &contract_dir,
334                root,
335                repo.as_deref(),
336                dry_run || !fix, // default to dry-run unless --fix
337                codegen || fix,  // --fix implies --codegen
338                fix,
339                json,
340                min_score,
341            )
342        }
343        Commands::VerifyBindings {
344            binding,
345            output,
346            crate_name,
347        } => commands::verify_bindings::run(&binding, output.as_deref(), crate_name.as_deref()),
348        Commands::Certify {
349            contract_dir,
350            config,
351            output,
352        } => commands::certify::run(&contract_dir, config.as_deref(), output.as_deref()),
353        Commands::VerifyStructure {
354            contract_dir,
355            config,
356            model,
357        } => commands::verify_structure::run(&contract_dir, config.as_deref(), model.as_deref()),
358        Commands::VerifyPipeline {
359            contract_dir,
360            format,
361        } => commands::verify_pipeline::run(&contract_dir, &format),
362        Commands::Migrate {
363            contract_dir,
364            dry_run,
365        } => commands::migrate::run(&contract_dir, dry_run),
366    }
367}
368
369/// Parse `argv` and run one command, exiting non-zero on failure. This is the
370/// whole of the standalone `pv` binary.
371pub fn run() {
372    let cli = Cli::parse();
373    let _ = (cli.quiet, cli.verbose); // Flags accepted; used by subcommands via Cli struct
374
375    if let Err(e) = dispatch(cli.command) {
376        // PVL-1 (PMAT-1099): a refused EMPTY corpus is a DECLINE — exit 2 and the
377        // `decline:` (exit 2, nothing was measured), `reject:` (exit 1, measured and
378        // failed) or `error:` — PVL-001 §0's vocabulary, one definition in
379        // contract_walk::verdict_for so the word and the exit code cannot drift.
380        let code = contract_walk::exit_code_for(e.as_ref());
381        let verdict = contract_walk::verdict_for(e.as_ref());
382        eprintln!("{verdict}: {e}");
383        std::process::exit(code);
384    }
385}
386
387#[cfg(test)]
388#[path = "../tests/includes/version_identity_unit.rs"]
389mod version_identity_unit;
390
391#[cfg(test)]
392#[path = "../tests/includes/dispatch_tests.rs"]
393mod dispatch_tests;
394
395#[cfg(test)]
396#[path = "../tests/includes/dispatch_query_tests.rs"]
397mod dispatch_query_tests;
aprender_contracts_cli/lib.rs

aprender_contracts_cli/
lib.rs
