#[cfg(test)]
use std::path::PathBuf;
use std::process;
use clap::Parser;
mod cli;
mod commands;
mod contract_walk;
mod query_args;
use cli::Commands;
#[derive(Parser)]
#[command(
name = "pv",
about = "provable-contracts — papers to provable Rust kernels",
version
)]
struct Cli {
#[command(subcommand)]
command: Commands,
#[arg(short, long, global = true)]
quiet: bool,
#[arg(short, long, global = true)]
verbose: bool,
}
#[allow(clippy::too_many_lines)]
fn run_command(command: Commands) -> Result<(), Box<dyn std::error::Error>> {
match command {
Commands::Explain {
contract,
format,
binding,
} => commands::explain::run(&contract, binding.as_deref(), &format),
Commands::Validate { contract } => commands::validate::run(&contract),
Commands::CheckParity { contract } => commands::check_parity::run(&contract),
Commands::Scaffold {
contract,
r#trait,
output,
} => commands::scaffold::run(&contract, r#trait, output.as_deref()),
Commands::ExtractPytorch { target, output } => {
commands::extract::run(&target, output.as_deref())
}
Commands::Codegen {
contract_dir,
output,
} => commands::codegen::run(&contract_dir, output.as_deref()),
Commands::Kani { contract } => commands::kani::run(&contract),
Commands::Probar { contract, binding } => {
commands::probar::run(&contract, binding.as_deref())
}
Commands::Status { contract } => commands::status::run(&contract),
Commands::Audit {
contract, binding, ..
} => commands::audit::run(&contract, binding.as_deref()),
Commands::Diff { old, new } => commands::diff::run(&old, &new),
Commands::Coverage {
contract_dir,
binding,
fuzz,
reverse,
enforcement,
} => commands::coverage::run(
&contract_dir,
binding.as_deref(),
fuzz,
reverse.as_deref(),
enforcement.as_deref(),
),
Commands::Generate {
contract,
output,
binding,
readme,
ci,
} => commands::generate::run(&contract, &output, binding.as_deref(), readme, ci),
Commands::Graph {
contract_dir,
format,
} => match commands::graph::GraphFormat::from_str(&format) {
Ok(fmt) => commands::graph::run(&contract_dir, fmt),
Err(e) => Err(e.into()),
},
Commands::Equations { contract, format } => {
match commands::equations::OutputFormat::from_str(&format) {
Ok(fmt) => commands::equations::run(&contract, fmt),
Err(e) => Err(e.into()),
}
}
Commands::Lean {
contract,
output_dir,
} => commands::lean::run(&contract, output_dir.as_deref()),
Commands::LeanStatus { path } => commands::lean_status::run(&path),
Commands::ProofStatus {
path,
binding,
verify_bindings,
format,
table,
kind,
} => commands::proof_status::run(
&path,
binding.as_deref(),
verify_bindings.as_deref(),
&format,
table,
kind.as_deref(),
),
Commands::Lint {
contract_dir,
min_score,
binding,
format,
severity,
strict,
suppress,
suppress_rule,
suppress_file,
rule,
config,
diff_ref,
trend,
show_trend,
no_cache,
cache_stats,
coverage,
min_coverage,
crate_dir,
min_level,
explain,
watch,
strict_test_binding,
..
} => {
if let Some(ref rule_id) = explain {
commands::lint::explain_rule(rule_id);
return Ok(());
}
commands::lint::run(
&contract_dir,
binding.as_deref(),
min_score,
format.as_deref(),
severity.as_deref(),
strict,
suppress.as_deref(),
suppress_rule.as_deref(),
suppress_file.as_deref(),
&rule,
config.as_deref(),
diff_ref.as_deref(),
trend,
show_trend,
no_cache,
cache_stats,
coverage,
min_coverage,
crate_dir.as_deref(),
min_level.as_deref(),
watch,
strict_test_binding,
)
}
Commands::Score {
path,
binding,
format,
min_score,
summary,
top_gaps,
weights,
pvscore,
..
} => commands::score::run(
&path,
binding.as_deref(),
&format,
min_score,
summary,
top_gaps,
weights.as_deref(),
pvscore,
),
Commands::Query(q) => commands::query::run(&commands::query::QueryCliParams {
contract_dir: &q.contract_dir,
query_str: &q.query,
regex: q.regex,
literal: q.literal,
case_sensitive: q.case_sensitive,
limit: q.limit,
obligation: q.obligation.as_deref(),
min_score: q.min_score,
min_level: q.min_level,
depends_on: q.depends_on.as_deref(),
depended_by: q.depended_by.as_deref(),
unproven: q.unproven,
show_score: q.score,
show_graph: q.graph,
show_paper: q.paper,
show_proof_status: q.proof_status,
show_binding: q.binding_info,
binding_gaps: q.binding_gaps,
show_diff: q.diff,
show_pagerank: q.pagerank,
show_call_sites: q.call_sites,
show_violations: q.violations,
show_coverage_map: q.coverage_map,
project_filter: q.project.as_deref(),
include_project: q.include_project.as_deref(),
tier: q.tier,
class: q.class,
kind: q.kind.as_deref(),
all_projects: q.all_projects,
rebuild_index: q.rebuild_index,
binding: q.binding.as_deref(),
format: &q.format,
exit_code: q.exit_code,
}),
Commands::Invariants { contract } => commands::invariants::run(&contract),
Commands::Coq { contract } => commands::coq::run(&contract),
Commands::Fuzz { contract } => commands::fuzz::run(&contract),
Commands::Mirai { contract } => commands::mirai::run(&contract),
Commands::Flux { contract } => commands::flux::run(&contract),
Commands::Tla { contract_dir } => commands::tla::run(&contract_dir),
Commands::Book {
contract_dir,
output,
update_summary,
summary_path,
} => commands::book::run(
&contract_dir,
&output,
update_summary,
summary_path.as_deref(),
),
Commands::Infer {
crate_dir,
binding,
contract_dir,
top,
} => commands::infer::run(&crate_dir, &binding, &contract_dir, top),
Commands::Unlock { contract, reason } => commands::unlock::run(&contract, &reason),
Commands::Roofline {
contract_dir,
params,
bits,
hardware,
format,
} => commands::roofline::run(&contract_dir, params, bits, &hardware, &format),
Commands::Pipeline { pipeline, format } => commands::pipeline::run(&pipeline, &format),
Commands::Kaizen {
contract_dir,
src_root,
repo,
dry_run,
codegen,
fix,
json,
min_score,
} => {
let default_root = std::path::PathBuf::from("..");
let root = src_root.as_deref().unwrap_or(&default_root);
commands::kaizen::run(
&contract_dir,
root,
repo.as_deref(),
dry_run || !fix, codegen || fix, fix,
json,
min_score,
)
}
Commands::VerifyBindings {
binding,
output,
crate_name,
} => commands::verify_bindings::run(&binding, output.as_deref(), crate_name.as_deref()),
Commands::Certify {
contract_dir,
config,
output,
} => commands::certify::run(&contract_dir, config.as_deref(), output.as_deref()),
Commands::VerifyStructure {
contract_dir,
config,
model,
} => commands::verify_structure::run(&contract_dir, config.as_deref(), model.as_deref()),
Commands::VerifyPipeline {
contract_dir,
format,
} => {
commands::verify_pipeline::run(&contract_dir, &format);
Ok(())
}
Commands::Migrate {
contract_dir,
dry_run,
} => commands::migrate::run(&contract_dir, dry_run),
}
}
fn main() {
let cli = Cli::parse();
let _ = (cli.quiet, cli.verbose);
if let Err(e) = run_command(cli.command) {
eprintln!("error: {e}");
process::exit(1);
}
}
#[cfg(test)]
#[path = "../tests/includes/dispatch_tests.rs"]
mod dispatch_tests;
#[cfg(test)]
#[path = "../tests/includes/dispatch_query_tests.rs"]
mod dispatch_query_tests;