aprender_contracts_cli/commands/
status.rs

1use std::path::Path;
2
3use provable_contracts::schema::parse_contract;
4
5pub fn run(path: &Path) -> Result<(), Box<dyn std::error::Error>> {
6    let contract = parse_contract(path)?;
7
8    println!(
9        "Contract: {} v{}",
10        contract.metadata.description, contract.metadata.version
11    );
12    println!("References: {}", contract.metadata.references.len());
13    println!("Equations: {}", contract.equations.len());
14    println!("Proof obligations: {}", contract.proof_obligations.len());
15    println!(
16        "Falsification tests: {}",
17        contract.falsification_tests.len()
18    );
19    // #2504: `contracts/publish-workspace-v1.yaml` holds four FALSIFY-PUB-*
20    // entries under a top-level `falsification:` key that is NOT
21    // `falsification_tests`. Before the schema captured that block, this
22    // command printed "Falsification tests: 0" and stopped — the reader was
23    // told the count and never told where the entries went. Say it out loud.
24    let legacy = contract.legacy_falsification_entries();
25    if legacy > 0 {
26        println!(
27            "  ...plus {legacy} entr{} in the legacy top-level `falsification:` block, \
28             which NO pv gate enforces{}",
29            if legacy == 1 { "y" } else { "ies" },
30            if contract.falsification_tests.is_empty() {
31                " — this contract is INERT: it reads as enforced and enforces nothing"
32            } else {
33                ""
34            }
35        );
36    }
37    println!("Kani harnesses: {}", contract.kani_harnesses.len());
38
39    if let Some(ref gate) = contract.qa_gate {
40        println!("QA gate: {} ({})", gate.name, gate.id);
41    } else {
42        println!("QA gate: not defined");
43    }
44
45    Ok(())
46}
aprender_contracts_cli/commands/status.rs

aprender_contracts_cli/commands/
status.rs
