impl SpecFalsificationReport {
#[provable_contracts_macros::contract("pmat-core.yaml", equation = "check_compliance")]
pub fn display(&self) {
use crate::cli::colors as c;
let file_display = self.target_file.display();
println!("{}", c::header(&format!("Falsifying: {}", file_display)));
let p0 = self.verdicts.iter().filter(|v| v.claim.priority == ClaimPriority::P0Critical).count();
let p1 = self.verdicts.iter().filter(|v| v.claim.priority == ClaimPriority::P1High).count();
let p2 = self.verdicts.iter().filter(|v| v.claim.priority == ClaimPriority::P2Low).count();
println!(
"Extracted: {} falsifiable claims ({}{} P0{}, {}{} P1{}, {}{} P2{})",
c::number(&self.summary.total_claims.to_string()),
c::RED, p0, c::RESET,
c::YELLOW, p1, c::RESET,
c::DIM, p2, c::RESET,
);
println!();
for (i, verdict) in self.verdicts.iter().enumerate() {
let status_icon = match &verdict.status {
VerdictStatus::Survived => &format!("{}SURVIVED{}", c::GREEN, c::RESET),
VerdictStatus::Falsified => &format!("{}FALSIFIED{}", c::RED, c::RESET),
VerdictStatus::Unfalsifiable => &format!("{}UNFALSIFIABLE{}", c::YELLOW, c::RESET),
VerdictStatus::Inconclusive => &format!("{}INCONCLUSIVE{}", c::YELLOW, c::RESET),
};
println!(
"{}[{}/{}]{} {} {} (line {}{}{})",
c::DIM, i + 1, self.summary.total_claims, c::RESET,
verdict.claim.priority,
status_icon,
c::CYAN, verdict.claim.source_line, c::RESET,
);
let display_text = crate::utils::string_truncate::truncate_with_ellipsis(
&verdict.claim.original_text,
97,
);
println!(" {}\"{}\"{}",c::DIM, display_text, c::RESET);
println!(" Category: {}", c::label(&verdict.claim.category.to_string()));
for ev in &verdict.evidence {
let icon = if ev.contradiction_score >= 0.8 {
format!("{}✗{}", c::RED, c::RESET)
} else if ev.contradiction_score >= 0.4 {
format!("{}?{}", c::YELLOW, c::RESET)
} else {
format!("{}✓{}", c::GREEN, c::RESET)
};
println!(" {} {} → {}", icon, c::dim(&ev.check), ev.finding);
}
println!();
}
println!("{}", c::subheader("Summary:"));
println!(" Total claims: {}", c::number(&self.summary.total_claims.to_string()));
let survived_pct = if self.summary.total_claims > 0 {
self.summary.survived as f64 / self.summary.total_claims as f64 * 100.0
} else { 0.0 };
println!(
" {}Survived{}: {} ({})",
c::GREEN, c::RESET,
c::number(&self.summary.survived.to_string()),
c::pct(survived_pct, 80.0, 50.0),
);
let falsified_pct = if self.summary.total_claims > 0 {
self.summary.falsified as f64 / self.summary.total_claims as f64 * 100.0
} else { 0.0 };
println!(
" {}Falsified{}: {} ({:.1}%)",
c::RED, c::RESET,
c::number(&self.summary.falsified.to_string()),
falsified_pct,
);
println!(" {}Unfalsifiable{}: {}", c::YELLOW, c::RESET, c::number(&self.summary.unfalsifiable.to_string()));
println!(" {}Inconclusive{}: {}", c::DIM, c::RESET, c::number(&self.summary.inconclusive.to_string()));
println!();
let health_color = if self.summary.health_score >= 0.8 { c::GREEN } else if self.summary.health_score >= 0.5 { c::YELLOW } else { c::RED };
println!(" Spec health: {}{:.2}{}", health_color, self.summary.health_score, c::RESET);
}
#[provable_contracts_macros::contract("pmat-core.yaml", equation = "check_compliance")]
pub fn to_json(&self) -> Result<String> {
serde_json::to_string_pretty(self).context("Failed to serialize report")
}
}