aprender_contracts_cli/cli.rs
1use std::path::PathBuf;
2
3use clap::Subcommand;
4
5/// Available subcommands for the `pv` CLI
6#[derive(Subcommand, Clone, Debug)]
7pub enum Commands {
8 /// Explain a contract in detail
9 Explain {
10 contract: PathBuf,
11 #[arg(long, default_value = "text")]
12 format: String,
13 #[arg(long)]
14 binding: Option<PathBuf>,
15 },
16 /// Validate a YAML kernel contract
17 Validate { contract: PathBuf },
18 /// Execute cross_check_command per row of a parity-matrix contract (SEMANTIC gate)
19 #[command(name = "check-parity")]
20 CheckParity { contract: PathBuf },
21 /// Generate Rust trait + test scaffolding from a contract
22 Scaffold {
23 contract: PathBuf,
24 #[arg(long)]
25 r#trait: bool,
26 #[arg(short, long)]
27 output: Option<PathBuf>,
28 },
29 /// Extract kernel equations from `PyTorch` source into YAML
30 #[command(name = "extract-pytorch")]
31 ExtractPytorch {
32 target: String,
33 #[arg(short, long)]
34 output: Option<PathBuf>,
35 },
36 /// Generate Rust `debug_assert!()` from YAML contracts
37 Codegen {
38 #[arg(default_value = "contracts")]
39 contract_dir: PathBuf,
40 /// Output Rust file path
41 #[arg(short, long)]
42 output: Option<PathBuf>,
43 },
44 /// Generate Kani proof harnesses from a contract
45 Kani { contract: PathBuf },
46 /// Generate probar property tests from a contract
47 Probar {
48 contract: PathBuf,
49 /// Path to binding registry YAML (generates wired tests)
50 #[arg(long)]
51 binding: Option<PathBuf>,
52 },
53 /// Show contract status (equations, obligations, coverage)
54 Status {
55 /// Path to the contract YAML file
56 contract: PathBuf,
57 },
58 /// Run traceability audit on a contract
59 Audit {
60 /// Path to the contract YAML file
61 contract: PathBuf,
62 /// Path to binding registry YAML (adds binding audit)
63 #[arg(long)]
64 binding: Option<PathBuf>,
65 /// Show Coq proof tier per obligation
66 #[arg(long)]
67 coq: bool,
68 /// Show Flux shape coverage per obligation
69 #[arg(long)]
70 flux: bool,
71 },
72 /// Diff two contract versions and suggest semver bump
73 Diff {
74 /// Path to the old contract YAML file
75 old: PathBuf,
76 /// Path to the new contract YAML file
77 new: PathBuf,
78 },
79 /// Show cross-contract obligation coverage report
80 Coverage {
81 /// Directory containing contract YAML files
82 #[arg(default_value = "contracts")]
83 contract_dir: PathBuf,
84 /// Path to binding registry YAML (adds binding coverage)
85 #[arg(long)]
86 binding: Option<PathBuf>,
87 /// Include fuzz coverage data
88 #[arg(long)]
89 fuzz: bool,
90 /// Reverse coverage: scan crate dir for unbound pub fns
91 #[arg(long)]
92 reverse: Option<PathBuf>,
93 /// Enforcement quality: scan crate source for contract call sites and classify E0/E1/E2
94 #[arg(long)]
95 enforcement: Option<PathBuf>,
96 },
97 /// Generate all artifacts (scaffold, kani, probar) to disk
98 Generate {
99 /// Path to the contract YAML file
100 contract: PathBuf,
101 /// Output directory for generated files
102 #[arg(short, long, default_value = "generated")]
103 output: PathBuf,
104 /// Path to binding registry YAML (generates wired tests)
105 #[arg(long)]
106 binding: Option<PathBuf>,
107 /// Generate CONTRACT-README.md (requires --binding)
108 #[arg(long)]
109 readme: bool,
110 /// Generate .github/workflows/contracts.yml
111 #[arg(long)]
112 ci: bool,
113 },
114 /// Show contract dependency graph
115 Graph {
116 /// Directory containing contract YAML files
117 #[arg(default_value = "contracts")]
118 contract_dir: PathBuf,
119 /// Output format: text (default), dot, json, or mermaid
120 #[arg(long, default_value = "text")]
121 format: String,
122 },
123 /// Display equations from a contract
124 Equations {
125 contract: PathBuf,
126 #[arg(long, default_value = "text")]
127 format: String,
128 },
129 /// Generate Lean 4 definitions and theorem stubs
130 Lean {
131 contract: PathBuf,
132 #[arg(long)]
133 output_dir: Option<PathBuf>,
134 },
135 /// Report Lean 4 proof status across contracts
136 LeanStatus {
137 /// Path to a contract YAML file or directory of contracts
138 #[arg(default_value = "contracts")]
139 path: PathBuf,
140 },
141 /// Report hierarchical proof levels (L1–L5) across contracts
142 ProofStatus {
143 /// Path to a contract YAML file or directory of contracts
144 #[arg(default_value = "contracts")]
145 path: PathBuf,
146 /// Path to binding registry YAML (adds binding coverage)
147 #[arg(long)]
148 binding: Option<PathBuf>,
149 /// L5 gate: before counting a binding as implemented, verify its
150 /// `function` actually exists in source (scanned from the given root,
151 /// default `.`). Phantom "implemented" bindings are downgraded, so L5
152 /// means "verified as implemented", not self-declared.
153 #[arg(long, num_args = 0..=1, default_missing_value = ".")]
154 verify_bindings: Option<PathBuf>,
155 /// Output format: text (default) or json
156 #[arg(long, default_value = "text")]
157 format: String,
158 /// Show per-obligation verification table
159 #[arg(long)]
160 table: bool,
161 /// Filter: kernel|registry|model-family|pattern|schema
162 #[arg(long)]
163 kind: Option<String>,
164 },
165 /// Run all contract quality gates (validate + audit + score)
166 Lint {
167 /// Directory containing contract YAML files
168 #[arg(default_value = "contracts")]
169 contract_dir: PathBuf,
170 /// Minimum composite score threshold (default: 0.0 = no score gate)
171 #[arg(long, default_value = "0.0")]
172 min_score: f64,
173 /// Path to binding registry YAML
174 #[arg(long)]
175 binding: Option<PathBuf>,
176 /// Output format: text (default), json, sarif, github
177 #[arg(short, long)]
178 format: Option<String>,
179 /// Minimum severity to report: error, warning, info
180 #[arg(long)]
181 severity: Option<String>,
182 /// Promote warnings to errors
183 #[arg(long)]
184 strict: bool,
185 /// Suppress specific finding IDs (comma-separated)
186 #[arg(long)]
187 suppress: Option<String>,
188 /// Suppress all findings for a rule (comma-separated)
189 #[arg(long)]
190 suppress_rule: Option<String>,
191 /// Suppress all findings matching a file path (comma-separated)
192 #[arg(long)]
193 suppress_file: Option<String>,
194 /// Override rule severity (e.g. PV-AUD-001=info)
195 #[arg(long)]
196 rule: Vec<String>,
197 /// Path to .pv.toml config file
198 #[arg(long)]
199 config: Option<PathBuf>,
200 /// Only lint contracts changed since base ref (e.g. main, HEAD~5)
201 #[arg(long = "diff")]
202 diff_ref: Option<String>,
203 /// Record quality trend snapshot
204 #[arg(long)]
205 trend: bool,
206 /// Show quality trend history
207 #[arg(long)]
208 show_trend: bool,
209 /// Bypass lint cache
210 #[arg(long)]
211 no_cache: bool,
212 /// Show cache hit/miss statistics
213 #[arg(long)]
214 cache_stats: bool,
215 /// Show auto-fix suggestions (dry run)
216 #[arg(long)]
217 suggest: bool,
218 /// Suppress findings in baseline SARIF file
219 #[arg(long)]
220 baseline: Option<PathBuf>,
221 /// Apply deterministic auto-fixes
222 #[arg(long)]
223 fix: bool,
224 /// Re-lint on file change (polling)
225 #[arg(long)]
226 watch: bool,
227 /// Show aggregate contract coverage metric
228 #[arg(long)]
229 coverage: bool,
230 /// Minimum coverage percentage (exit 1 if below)
231 #[arg(long)]
232 min_coverage: Option<f64>,
233 /// Path to crate directory for reverse coverage gate
234 #[arg(long)]
235 crate_dir: Option<PathBuf>,
236 /// Minimum enforcement level: basic, standard, strict, proven
237 #[arg(long)]
238 min_level: Option<String>,
239 /// Explain a lint rule in detail (e.g. PV-ENF-001)
240 #[arg(long)]
241 explain: Option<String>,
242 /// Enable strict test-binding gate (PV-VER-002): cross-checks every
243 /// `falsification_tests[].test` cargo invocation against `#[test]` fns
244 /// in the source tree. Catches drift classes that PV-VER-001 misses
245 /// (suffix drift, module-path drift, convention drift, "or equivalent"
246 /// placeholders). Default emits Warning; combine with `--strict` to
247 /// promote to Error and fail CI. Issue #1510.
248 #[arg(long)]
249 strict_test_binding: bool,
250 },
251 /// Score contracts or a codebase directory
252 Score {
253 /// Path to a contract YAML file or directory of contracts
254 #[arg(default_value = "contracts")]
255 path: PathBuf,
256 /// Path to binding registry YAML
257 #[arg(long)]
258 binding: Option<PathBuf>,
259 /// Output format: text (default) or json
260 #[arg(short, long, default_value = "text")]
261 format: String,
262 /// Minimum score threshold (exit 1 if below)
263 #[arg(long)]
264 min_score: Option<f64>,
265 /// Show aggregate summary only (no per-contract detail)
266 #[arg(long)]
267 summary: bool,
268 /// Show top N gaps by impact (default: 5)
269 #[arg(long, default_value = "5")]
270 top_gaps: usize,
271 /// Custom weights as JSON
272 #[arg(long)]
273 weights: Option<String>,
274 /// Exit with status 1 if any contract below --min-score
275 #[arg(long)]
276 exit_code: bool,
277 /// Show 10-dimension `PVScore` (geometric mean)
278 #[arg(long)]
279 pvscore: bool,
280 },
281 /// Search contracts by intent, regex, or literal match
282 Query(crate::query_args::QueryArgs),
283 /// Generate type invariant trait + Kani preservation harnesses
284 Invariants { contract: PathBuf },
285 /// Generate Coq theorem stubs from a contract
286 Coq { contract: PathBuf },
287 /// Generate libfuzzer fuzz targets from a contract
288 Fuzz { contract: PathBuf },
289 /// Generate MIRAI annotations from a contract
290 Mirai { contract: PathBuf },
291 /// Generate Flux refinement types from a contract
292 Flux { contract: PathBuf },
293 /// Generate TLA+ specification from contract dependency DAG
294 Tla {
295 /// Directory containing contract YAML files
296 #[arg(default_value = "contracts")]
297 contract_dir: PathBuf,
298 },
299 /// Generate mdBook pages for contracts
300 Book {
301 /// Directory containing contract YAML files
302 #[arg(default_value = "contracts")]
303 contract_dir: PathBuf,
304 /// Output directory for generated pages
305 #[arg(short, long, default_value = "book/src/contracts")]
306 output: PathBuf,
307 /// Also update book/src/SUMMARY.md with contract links
308 #[arg(long)]
309 update_summary: bool,
310 /// Path to SUMMARY.md (default: book/src/SUMMARY.md)
311 #[arg(long)]
312 summary_path: Option<PathBuf>,
313 },
314 /// Infer contracts and bindings for unbound functions in a crate
315 Infer {
316 /// Path to the crate directory to scan
317 crate_dir: PathBuf,
318 /// Path to binding registry YAML
319 #[arg(long)]
320 binding: PathBuf,
321 /// Directory containing contract YAML files
322 #[arg(long, default_value = "contracts")]
323 contract_dir: PathBuf,
324 /// Maximum number of suggestions to show
325 #[arg(long, default_value = "20")]
326 top: usize,
327 },
328 /// Remove enforcement level lock from a contract (requires --reason)
329 Unlock {
330 /// Path to the contract YAML file
331 contract: PathBuf,
332 /// Mandatory reason for unlocking (audit trail)
333 #[arg(long)]
334 reason: String,
335 },
336 /// Compute roofline ceilings from contract equations
337 Roofline {
338 #[arg(long, default_value = "contracts")]
339 contract_dir: PathBuf,
340 /// Total model parameters (e.g. 7000000000 for 7B)
341 #[arg(long)]
342 params: u64,
343 /// Bits per weight (2, 4, 8, 16, 32)
344 #[arg(long, default_value = "4")]
345 bits: u32,
346 /// Hardware profile: apple-m, a100
347 #[arg(long, default_value = "apple-m")]
348 hardware: String,
349 /// Output format: text (default) or json
350 #[arg(short, long, default_value = "text")]
351 format: String,
352 },
353 /// Validate a pipeline contract (cross-repo verification)
354 Pipeline {
355 /// Path to the pipeline YAML file
356 pipeline: PathBuf,
357 /// Output format: text (default) or json
358 #[arg(short, long, default_value = "text")]
359 format: String,
360 },
361 /// Fleet-wide contract enforcement (kaizen loop)
362 Kaizen {
363 #[arg(long, default_value = "contracts")]
364 contract_dir: PathBuf,
365 #[arg(long)]
366 src_root: Option<PathBuf>,
367 #[arg(long)]
368 repo: Option<String>,
369 #[arg(long)]
370 dry_run: bool,
371 #[arg(long)]
372 codegen: bool,
373 #[arg(long)]
374 fix: bool,
375 #[arg(long)]
376 json: bool,
377 #[arg(long)]
378 min_score: Option<f64>,
379 },
380 /// Produce whole-model proof certificate (runs verify-pipeline + verify-structure)
381 Certify {
382 #[arg(default_value = "contracts")]
383 contract_dir: PathBuf,
384 #[arg(long)]
385 config: Option<PathBuf>,
386 #[arg(short, long)]
387 output: Option<PathBuf>,
388 },
389 /// Verify model architecture structure matches contracts
390 #[command(name = "verify-structure")]
391 VerifyStructure {
392 #[arg(default_value = "contracts")]
393 contract_dir: PathBuf,
394 #[arg(long)]
395 config: Option<PathBuf>,
396 #[arg(long)]
397 model: Option<PathBuf>,
398 },
399 /// Verify compositional shape flow across contract dependency graph
400 #[command(name = "verify-pipeline")]
401 VerifyPipeline {
402 #[arg(default_value = "contracts")]
403 contract_dir: PathBuf,
404 #[arg(long, default_value = "text")]
405 format: String,
406 },
407 /// Generate a Rust test that verifies all bound functions exist
408 VerifyBindings {
409 /// Path to binding.yaml
410 binding: PathBuf,
411 /// Output file path (default: stdout)
412 #[arg(short, long)]
413 output: Option<PathBuf>,
414 /// Crate name for test label
415 #[arg(long)]
416 crate_name: Option<String>,
417 },
418 /// Migrate old-format contract YAMLs to current schema (GH-67)
419 Migrate {
420 #[arg(default_value = "contracts")]
421 contract_dir: PathBuf,
422 #[arg(long)]
423 dry_run: bool,
424 },
425}