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 {
18 contract: PathBuf,
19 /// Report obligation-id denominators instead of validating:
20 /// `N obligations, M with id, K referenced`. Counts come through the
21 /// same deserialization every other pv command uses, which is what
22 /// makes them evidence that a consumer reads the key (#3314).
23 #[arg(long)]
24 check_ids: bool,
25 },
26 /// Execute cross_check_command per row of a parity-matrix contract (SEMANTIC gate)
27 #[command(name = "check-parity")]
28 CheckParity { contract: PathBuf },
29 /// Generate Rust trait + test scaffolding from a contract
30 Scaffold {
31 contract: PathBuf,
32 #[arg(long)]
33 r#trait: bool,
34 #[arg(short, long)]
35 output: Option<PathBuf>,
36 },
37 /// Extract kernel equations from `PyTorch` source into YAML
38 #[command(name = "extract-pytorch")]
39 ExtractPytorch {
40 target: String,
41 #[arg(short, long)]
42 output: Option<PathBuf>,
43 },
44 /// Generate Rust `debug_assert!()` from YAML contracts
45 Codegen {
46 #[arg(default_value = "contracts")]
47 contract_dir: PathBuf,
48 /// Output Rust file path
49 #[arg(short, long)]
50 output: Option<PathBuf>,
51 },
52 /// Generate Kani proof harnesses from a contract
53 Kani { contract: PathBuf },
54 /// Generate probar property tests from a contract
55 Probar {
56 contract: PathBuf,
57 /// Path to binding registry YAML (generates wired tests)
58 #[arg(long)]
59 binding: Option<PathBuf>,
60 },
61 /// Show contract status (equations, obligations, coverage)
62 Status {
63 /// Path to the contract YAML file
64 contract: PathBuf,
65 },
66 /// Run traceability audit on a contract
67 Audit {
68 /// Path to the contract YAML file
69 contract: PathBuf,
70 /// Path to binding registry YAML (adds binding audit)
71 #[arg(long)]
72 binding: Option<PathBuf>,
73 /// Show Coq proof tier per obligation
74 #[arg(long)]
75 coq: bool,
76 /// Show Flux shape coverage per obligation
77 #[arg(long)]
78 flux: bool,
79 },
80 /// Diff two contract versions and suggest semver bump
81 Diff {
82 /// Path to the old contract YAML file
83 old: PathBuf,
84 /// Path to the new contract YAML file
85 new: PathBuf,
86 },
87 /// Census the contract corpus: one cardinality, by_anchoring, by_entity_type (ONT-001 ONT-1)
88 Census {
89 /// Directory containing contract YAML files
90 #[arg(default_value = "contracts")]
91 contract_dir: PathBuf,
92 /// Output format. ONT-001 §5 ONT-1's probe runs `--format json`.
93 #[arg(long, value_enum, default_value_t = CensusFormat::Table)]
94 format: CensusFormat,
95 /// Deprecated alias for `--format json`, kept because
96 /// scripts/check_ont_ratchet.sh derives its consumer probe from this surface.
97 #[arg(long)]
98 json: bool,
99 },
100 /// Extract the corpus as RDF: contracts.nt (sorted N-Triples, no blank nodes) and shapes.ttl (ONT-001 ONT-4b, R-15, R-18)
101 Extract {
102 /// Directory containing contract YAML files
103 #[arg(default_value = "contracts")]
104 contract_dir: PathBuf,
105 /// Write nothing; exit 1 if the tracked files differ from a fresh extraction (what CI runs)
106 #[arg(long)]
107 check: bool,
108 /// With `--release-*`: write the corpus graph PLUS the release evidence to this N-Triples file, and leave
109 /// the tracked contracts.nt / shapes.ttl untouched (aprender#3715)
110 #[arg(long)]
111 out: Option<PathBuf>,
112 #[command(flatten)]
113 release: Box<ReleaseArgs>,
114 },
115 /// Show cross-contract obligation coverage report
116 Coverage {
117 /// Directory containing contract YAML files
118 #[arg(default_value = "contracts")]
119 contract_dir: PathBuf,
120 /// Path to binding registry YAML (adds binding coverage)
121 #[arg(long)]
122 binding: Option<PathBuf>,
123 /// Include fuzz coverage data
124 #[arg(long)]
125 fuzz: bool,
126 /// Reverse coverage: scan crate dir for unbound pub fns
127 #[arg(long)]
128 reverse: Option<PathBuf>,
129 /// Enforcement quality: scan crate source for contract call sites and classify E0/E1/E2
130 #[arg(long)]
131 enforcement: Option<PathBuf>,
132 },
133 /// Generate all artifacts (scaffold, kani, probar) to disk
134 Generate {
135 /// Path to the contract YAML file
136 contract: PathBuf,
137 /// Output directory for generated files
138 #[arg(short, long, default_value = "generated")]
139 output: PathBuf,
140 /// Path to binding registry YAML (generates wired tests)
141 #[arg(long)]
142 binding: Option<PathBuf>,
143 /// Generate CONTRACT-README.md (requires --binding)
144 #[arg(long)]
145 readme: bool,
146 /// Generate .github/workflows/contracts.yml
147 #[arg(long)]
148 ci: bool,
149 },
150 /// Show contract dependency graph
151 Graph {
152 /// Directory containing contract YAML files
153 #[arg(default_value = "contracts")]
154 contract_dir: PathBuf,
155 /// Output format: text (default), dot, json, or mermaid
156 #[arg(long, default_value = "text")]
157 format: String,
158 },
159 /// Display equations from a contract
160 Equations {
161 contract: PathBuf,
162 #[arg(long, default_value = "text")]
163 format: String,
164 },
165 /// Generate Lean 4 definitions and theorem stubs
166 Lean {
167 contract: PathBuf,
168 #[arg(long)]
169 output_dir: Option<PathBuf>,
170 },
171 /// Report Lean 4 proof status across contracts
172 LeanStatus {
173 /// Path to a contract YAML file or directory of contracts
174 #[arg(default_value = "contracts")]
175 path: PathBuf,
176 },
177 /// Report hierarchical proof levels (L1–L5) across contracts
178 ProofStatus {
179 /// Path to a contract YAML file or directory of contracts
180 #[arg(default_value = "contracts")]
181 path: PathBuf,
182 /// Path to binding registry YAML (adds binding coverage)
183 #[arg(long)]
184 binding: Option<PathBuf>,
185 /// L5 gate: before counting a binding as implemented, verify its
186 /// `function` actually exists in source (scanned from the given root,
187 /// default `.`). Phantom "implemented" bindings are downgraded, so L5
188 /// means "verified as implemented", not self-declared.
189 #[arg(long, num_args = 0..=1, default_missing_value = ".")]
190 verify_bindings: Option<PathBuf>,
191 /// Output format: text (default) or json
192 #[arg(long, default_value = "text")]
193 format: String,
194 /// Show per-obligation verification table
195 #[arg(long)]
196 table: bool,
197 /// Filter: kernel|registry|model-family|pattern|schema
198 #[arg(long)]
199 kind: Option<String>,
200 },
201 /// Run all contract quality gates (validate + audit + score)
202 Lint {
203 /// Directory containing contract YAML files
204 #[arg(default_value = "contracts")]
205 contract_dir: PathBuf,
206 /// Minimum composite score threshold (default: 0.0 = no score gate)
207 #[arg(long, default_value = "0.0")]
208 min_score: f64,
209 /// Path to binding registry YAML
210 #[arg(long)]
211 binding: Option<PathBuf>,
212 /// Output format: text (default), json, sarif, github
213 #[arg(short, long)]
214 format: Option<String>,
215 /// Minimum severity to report: error, warning, info
216 #[arg(long)]
217 severity: Option<String>,
218 /// Promote warnings to errors
219 #[arg(long)]
220 strict: bool,
221 /// Suppress specific finding IDs (comma-separated)
222 #[arg(long)]
223 suppress: Option<String>,
224 /// Suppress all findings for a rule (comma-separated)
225 #[arg(long)]
226 suppress_rule: Option<String>,
227 /// Suppress all findings matching a file path (comma-separated)
228 #[arg(long)]
229 suppress_file: Option<String>,
230 /// Override rule severity (e.g. PV-AUD-001=info)
231 #[arg(long)]
232 rule: Vec<String>,
233 /// Path to .pv.toml config file
234 #[arg(long)]
235 config: Option<PathBuf>,
236 /// Only lint contracts changed since base ref (e.g. main, HEAD~5)
237 #[arg(long = "diff")]
238 diff_ref: Option<String>,
239 /// Record quality trend snapshot
240 #[arg(long)]
241 trend: bool,
242 /// Show quality trend history
243 #[arg(long)]
244 show_trend: bool,
245 /// Bypass lint cache
246 #[arg(long)]
247 no_cache: bool,
248 /// Show cache hit/miss statistics
249 #[arg(long)]
250 cache_stats: bool,
251 /// Show auto-fix suggestions (dry run)
252 #[arg(long)]
253 suggest: bool,
254 /// Suppress findings in baseline SARIF file
255 #[arg(long)]
256 baseline: Option<PathBuf>,
257 /// Apply deterministic auto-fixes
258 #[arg(long)]
259 fix: bool,
260 /// Re-lint on file change (polling)
261 #[arg(long)]
262 watch: bool,
263 /// Show aggregate contract coverage metric
264 #[arg(long)]
265 coverage: bool,
266 /// Minimum coverage percentage (exit 1 if below)
267 #[arg(long)]
268 min_coverage: Option<f64>,
269 /// Path to crate directory for reverse coverage gate
270 #[arg(long)]
271 crate_dir: Option<PathBuf>,
272 /// Minimum enforcement level: basic, standard, strict, proven
273 #[arg(long)]
274 min_level: Option<String>,
275 /// Explain a lint rule in detail (e.g. PV-ENF-001)
276 #[arg(long)]
277 explain: Option<String>,
278 /// Enable strict test-binding gate (PV-VER-002): cross-checks every
279 /// `falsification_tests[].test` cargo invocation against `#[test]` fns
280 /// in the source tree. Catches drift classes that PV-VER-001 misses
281 /// (suffix drift, module-path drift, convention drift, "or equivalent"
282 /// placeholders). Default emits Warning; combine with `--strict` to
283 /// promote to Error and fail CI. Issue #1510.
284 #[arg(long)]
285 strict_test_binding: bool,
286 /// Git ref whose `lint-baseline.json` is the `armed_gates` comparand (ONT-001 section 3.9). Default:
287 /// merge-base(HEAD, origin/main), else the origin/main tip; with neither, NOT CHECKED is printed.
288 #[arg(long)]
289 armed_baseline_ref: Option<String>,
290 /// Run ONE named gate and report only it (ONT-001 section 5 ONT-2b): `--gate sigma`.
291 #[arg(long)]
292 gate: Option<String>,
293 /// With `--gate shapes`: grade only this shape family (the shape and every `<id>.*` shape), armed
294 /// whatever `armed_shapes` says (aprender#3715: `--shape release-readiness-v1`).
295 #[arg(long)]
296 shape: Option<String>,
297 #[command(flatten)]
298 release: Box<ReleaseArgs>,
299 },
300 /// Score contracts or a codebase directory
301 Score {
302 /// Path to a contract YAML file or directory of contracts
303 #[arg(default_value = "contracts")]
304 path: PathBuf,
305 /// Path to binding registry YAML
306 #[arg(long)]
307 binding: Option<PathBuf>,
308 /// Output format: text (default) or json
309 #[arg(short, long, default_value = "text")]
310 format: String,
311 /// Minimum score threshold (exit 1 if below)
312 #[arg(long)]
313 min_score: Option<f64>,
314 /// Show aggregate summary only (no per-contract detail)
315 #[arg(long)]
316 summary: bool,
317 /// Show top N gaps by impact (default: 5)
318 #[arg(long, default_value = "5")]
319 top_gaps: usize,
320 /// Custom weights as JSON
321 #[arg(long)]
322 weights: Option<String>,
323 /// Exit with status 1 if any contract below --min-score
324 #[arg(long)]
325 exit_code: bool,
326 /// Show 10-dimension `PVScore` (geometric mean)
327 #[arg(long)]
328 pvscore: bool,
329 },
330 /// Search contracts by intent, regex, or literal match
331 Query(crate::query_args::QueryArgs),
332 /// Generate type invariant trait + Kani preservation harnesses
333 Invariants { contract: PathBuf },
334 /// Generate Coq theorem stubs from a contract
335 Coq { contract: PathBuf },
336 /// Generate libfuzzer fuzz targets from a contract
337 Fuzz { contract: PathBuf },
338 /// Generate MIRAI annotations from a contract
339 Mirai { contract: PathBuf },
340 /// Generate Flux refinement types from a contract
341 Flux { contract: PathBuf },
342 /// Generate TLA+ specification from contract dependency DAG
343 Tla {
344 /// Directory containing contract YAML files
345 #[arg(default_value = "contracts")]
346 contract_dir: PathBuf,
347 },
348 /// Generate mdBook pages for contracts
349 Book {
350 /// Directory containing contract YAML files
351 #[arg(default_value = "contracts")]
352 contract_dir: PathBuf,
353 /// Output directory for generated pages
354 #[arg(short, long, default_value = "book/src/contracts")]
355 output: PathBuf,
356 /// Also update book/src/SUMMARY.md with contract links
357 #[arg(long)]
358 update_summary: bool,
359 /// Path to SUMMARY.md (default: book/src/SUMMARY.md)
360 #[arg(long)]
361 summary_path: Option<PathBuf>,
362 },
363 /// Infer contracts and bindings for unbound functions in a crate
364 Infer {
365 /// Path to the crate directory to scan
366 crate_dir: PathBuf,
367 /// Path to binding registry YAML
368 #[arg(long)]
369 binding: PathBuf,
370 /// Directory containing contract YAML files
371 #[arg(long, default_value = "contracts")]
372 contract_dir: PathBuf,
373 /// Maximum number of suggestions to show
374 #[arg(long, default_value = "20")]
375 top: usize,
376 },
377 /// Remove enforcement level lock from a contract (requires --reason)
378 Unlock {
379 /// Path to the contract YAML file
380 contract: PathBuf,
381 /// Mandatory reason for unlocking (audit trail)
382 #[arg(long)]
383 reason: String,
384 },
385 /// Compute roofline ceilings from contract equations
386 Roofline {
387 #[arg(long, default_value = "contracts")]
388 contract_dir: PathBuf,
389 /// Total model parameters (e.g. 7000000000 for 7B)
390 #[arg(long)]
391 params: u64,
392 /// Bits per weight (2, 4, 8, 16, 32)
393 #[arg(long, default_value = "4")]
394 bits: u32,
395 /// Hardware profile: apple-m, a100
396 #[arg(long, default_value = "apple-m")]
397 hardware: String,
398 /// Output format: text (default) or json
399 #[arg(short, long, default_value = "text")]
400 format: String,
401 },
402 /// Validate a pipeline contract (cross-repo verification)
403 Pipeline {
404 /// Path to the pipeline YAML file
405 pipeline: PathBuf,
406 /// Output format: text (default) or json
407 #[arg(short, long, default_value = "text")]
408 format: String,
409 },
410 /// Fleet-wide contract enforcement (kaizen loop)
411 Kaizen {
412 #[arg(long, default_value = "contracts")]
413 contract_dir: PathBuf,
414 #[arg(long)]
415 src_root: Option<PathBuf>,
416 #[arg(long)]
417 repo: Option<String>,
418 #[arg(long)]
419 dry_run: bool,
420 #[arg(long)]
421 codegen: bool,
422 #[arg(long)]
423 fix: bool,
424 #[arg(long)]
425 json: bool,
426 #[arg(long)]
427 min_score: Option<f64>,
428 },
429 /// Produce whole-model proof certificate (runs verify-pipeline + verify-structure)
430 Certify {
431 #[arg(default_value = "contracts")]
432 contract_dir: PathBuf,
433 #[arg(long)]
434 config: Option<PathBuf>,
435 #[arg(short, long)]
436 output: Option<PathBuf>,
437 },
438 /// Verify model architecture structure matches contracts
439 #[command(name = "verify-structure")]
440 VerifyStructure {
441 #[arg(default_value = "contracts")]
442 contract_dir: PathBuf,
443 #[arg(long)]
444 config: Option<PathBuf>,
445 #[arg(long)]
446 model: Option<PathBuf>,
447 },
448 /// Verify compositional shape flow across contract dependency graph
449 #[command(name = "verify-pipeline")]
450 VerifyPipeline {
451 #[arg(default_value = "contracts")]
452 contract_dir: PathBuf,
453 #[arg(long, default_value = "text")]
454 format: String,
455 },
456 /// Generate a Rust test that verifies all bound functions exist
457 VerifyBindings {
458 /// Path to binding.yaml
459 binding: PathBuf,
460 /// Output file path (default: stdout)
461 #[arg(short, long)]
462 output: Option<PathBuf>,
463 /// Crate name for test label
464 #[arg(long)]
465 crate_name: Option<String>,
466 },
467 /// Migrate old-format contract YAMLs to current schema (GH-67)
468 Migrate {
469 #[arg(default_value = "contracts")]
470 contract_dir: PathBuf,
471 #[arg(long)]
472 dry_run: bool,
473 },
474}
475
476/// `pv census` output format (ONT-001 ONT-1).
477#[derive(Debug, Clone, Copy, PartialEq, Eq, clap::ValueEnum)]
478pub enum CensusFormat {
479 /// Human-readable table.
480 Table,
481 /// The bytes `contracts/census.json` carries.
482 Json,
483}
484
485/// aprender#3715 — the release subject `extract:release-evidence` reads, for `pv lint --gate shapes` and
486/// `pv extract`. All absent → no release graph. `--release-version` and `--release-commit` come together; the
487/// rest need them.
488#[derive(clap::Args, Debug, Default, Clone)]
489pub struct ReleaseArgs {
490 /// The release version whose evidence `release-readiness-v1` grades
491 #[arg(long)]
492 pub release_version: Option<String>,
493 /// The release commit (MC), full 40-hex: the dogfood receipt's commit, and the receipts' unless --receipts-commit
494 #[arg(long)]
495 pub release_commit: Option<String>,
496 /// T-4 only: the sha the committed receipts were measured at, after R7 proved the tree equal modulo evidence/
497 #[arg(long)]
498 pub receipts_commit: Option<String>,
499 /// The per-host model receipts (default: evidence/dogfood/models/<version>/)
500 #[arg(long)]
501 pub receipts: Option<PathBuf>,
502 /// The per-host kernel-diff receipts (default: evidence/dogfood/kernels/<version>/)
503 #[arg(long)]
504 pub kernel_receipts: Option<PathBuf>,
505 /// The dogfood receipt R5 judged (without it the release has no dogfood receipt, which is a violation)
506 #[arg(long)]
507 pub dogfood_receipt: Option<PathBuf>,
508 /// The tokenizer-parity receipts, apr vs the pinned llama.cpp (default: evidence/dogfood/tokenizer/<version>/)
509 #[arg(long)]
510 pub tokenizer_receipts: Option<PathBuf>,
511}
512
513impl ReleaseArgs {
514 /// Did the caller pass any release flag at all?
515 #[must_use]
516 pub fn any(&self) -> bool {
517 self.release_version.is_some()
518 || self.release_commit.is_some()
519 || self.receipts_commit.is_some()
520 || self.receipts.is_some()
521 || self.kernel_receipts.is_some()
522 || self.dogfood_receipt.is_some()
523 || self.tokenizer_receipts.is_some()
524 }
525
526 /// The subject, or `None` when no flag was passed. A partial set is refused, never completed by a default.
527 pub fn subject(
528 &self,
529 ) -> Result<Option<provable_contracts::ontology::extract::release_inputs::Subject>, String>
530 {
531 use provable_contracts::ontology::extract::release_inputs::Subject;
532 if !self.any() {
533 return Ok(None);
534 }
535 let (Some(v), Some(c)) = (&self.release_version, &self.release_commit) else {
536 return Err(
537 "--release-version and --release-commit are both required with any --release-*, \
538 --receipts*, --kernel-receipts or --dogfood-receipt flag"
539 .into(),
540 );
541 };
542 let mut s = Subject::new(v, c).map_err(|e| e.to_string())?;
543 if let Some(rc) = &self.receipts_commit {
544 s = s.with_receipts_commit(rc).map_err(|e| e.to_string())?;
545 }
546 s.receipts_dir.clone_from(&self.receipts);
547 s.kernel_receipts_dir.clone_from(&self.kernel_receipts);
548 s.dogfood_receipt.clone_from(&self.dogfood_receipt);
549 s.tokenizer_receipts_dir
550 .clone_from(&self.tokenizer_receipts);
551 Ok(Some(s))
552 }
553}