Skip to content

PR: feat: make structural enumeration the CLI verify default #42 #48

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
metasmile merged 2 commits into from
Aug 23, 2026
Merged

PR: feat: make structural enumeration the CLI verify default #42 #48

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
78cfc16
refactor: enforce reporter count invariant and fix empty failure head…
metasmile Aug 23, 2026
0f76154
fix: report remaining present failure rows in the capped list #42
metasmile Aug 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
59 changes: 38 additions & 21 deletions src/report/reporter.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,22 @@ pub trait ReporterCapable: Send + Sync {
) -> bool;
}

// ============================================================================
// Count helpers
// ============================================================================

/// Split an evaluation list into passed/failed counts against the raw total.
/// The invariant passed <= total is enforced loudly: a silent usize wrap in
/// release would corrupt verification counts.
fn split_counts(total: usize, evaluations: &[Evaluation]) -> (usize, usize) {
let passed = evaluations.iter().filter(|e| e.passed).count();
assert!(
passed <= total,

@metasmile metasmile Aug 23, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The invariant is enforced with assert!, which panics. The trait returns bool rather than Result, so a panic is the loudest available signal for a caller-side contract violation, and it is preferable to a silent usize wrap in release. This is a reasonable design choice; documenting it in the trait doc comment (already done) is sufficient.

"reporter invariant violated: passed ({passed}) exceeds raw total ({total})"
);
(passed, total - passed)
}

// ============================================================================
// CSV Reporter
// ============================================================================
Expand All @@ -52,8 +68,7 @@ impl ReporterCapable for CsvReporter {
total: usize,
evaluations: &[Evaluation],
) -> bool {
let passed_count = evaluations.iter().filter(|e| e.passed).count();
let failed_count = total - passed_count;
let (passed_count, failed_count) = split_counts(total, evaluations);

// Print metadata as comments
println!("# target: {}", target);
Expand Down Expand Up @@ -110,8 +125,7 @@ impl ReporterCapable for TraceReporter {
total: usize,
evaluations: &[Evaluation],
) -> bool {
let passed_count = evaluations.iter().filter(|e| e.passed).count();
let failed_count = total - passed_count;
let (passed_count, failed_count) = split_counts(total, evaluations);
let started_at = chrono::Utc::now();

println!(
Expand Down Expand Up @@ -192,8 +206,7 @@ impl ReporterCapable for TextReporter {
total: usize,
evaluations: &[Evaluation],
) -> bool {
let passed_count = evaluations.iter().filter(|e| e.passed).count();
let failed_count = total - passed_count;
let (passed_count, failed_count) = split_counts(total, evaluations);

println!("target: {}", target);
println!("total: {}", total);
Expand All @@ -202,21 +215,26 @@ impl ReporterCapable for TextReporter {
println!();

if failed_count > 0 {
println!("Failures:");
// Cap the detail listing: the full list can be gigabytes for
// sparse spaces (e.g. 432K invalid rv32imcb encodings each
// carrying the cross-mapping description). The summary lines
// above remain authoritative; the cap keeps the log usable.
// The summary lines above are authoritative; the detail listing
// is capped (the full list can be gigabytes for sparse spaces).
const MAX_PRINTED_FAILURES: usize = 25;
for (i, e) in evaluations.iter().filter(|e| !e.passed).enumerate() {
if i == MAX_PRINTED_FAILURES {
println!(
" ... and {} more failures",
failed_count - MAX_PRINTED_FAILURES
);
break;
let failed_rows: Vec<&Evaluation> =
evaluations.iter().filter(|e| !e.passed).collect();
if !failed_rows.is_empty() {
println!("Failures:");
for (i, e) in failed_rows.iter().enumerate() {
if i == MAX_PRINTED_FAILURES {
// failed_count includes structurally absent combinations
// in the structural pipeline; the remaining present
// rows are the accurate unprinted detail.
println!(
" ... and {} more failures",
failed_rows.len() - MAX_PRINTED_FAILURES
);
break;
}
println!(" [FAIL] {:?} — {}", e.combination.values, e.reason);
}
println!(" [FAIL] {:?} — {}", e.combination.values, e.reason);
}
}

Expand Down Expand Up @@ -275,8 +293,7 @@ impl ReporterCapable for JsonReporter {
total: usize,
evaluations: &[Evaluation],
) -> bool {
let passed_count = evaluations.iter().filter(|e| e.passed).count();
let failed_count = total - passed_count;
let (passed_count, failed_count) = split_counts(total, evaluations);
let origin = format!("ev/{}", env!("CARGO_PKG_VERSION"));
let timestamp = chrono::Utc::now().to_rfc3339();
let spec_hash = spec_hash.to_string();
Expand Down