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

aprender_contracts_cli/
lib.rs
