From 52a0d54bbf7842a8d8ce9961a7bdefad9dadb5ba Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 18 Oct 2026 22:36:22 +0700 Subject: [PATCH] tri test: refuse vacuous passes -- report.t27 reads the "vacuous passes N of M" line (Closes #10497) `tri test ` ran `t27c test-report` and passed any report whose tests all passed and at least one ran. It never read the line `vacuous passes N of M (passed with 0 runtime asserts executed)`, and report.t27 classified it LINE_OTHER, so a spec whose every test executed 0 runtime asserts passed `tri test`. report.t27 now reads it (the rule is .t27; the Rust is glue): - LINE_VACUOUS (`vacuous passes N of M`), LINE_VACUOUS_NAME (`0 VACUOUS`), LINE_VACUOUS_UNKNOWN (`vacuous passes unknown`), and parsers vacuous_passes (N) and vacuous_of (M). - V_VACUOUS: N > 0. The VACUOUS lines name the tests. - V_UNCOUNTED: `unknown`, the counting build did not compile, so a vacuous pass cannot be ruled out. - Fail closed: M must be the report's pass total, N <= M, and N must be the number of VACUOUS names; VACUOUS names with no summary line (a cut report) are refused. - A report with no vacuous line at all (a t27c older than #6509) keeps the reading it always had. A FAIL is still read before a vacuous pass, so `tri mutate plant` keeps naming the killed tests. - 9 new tests (22 in all, 0 vacuous), including a negative control; the old LINE_OTHER test for the vacuous line now expects LINE_VACUOUS. Glue: report_summary in cli/tri/src/main.rs appends `, vacuous: ` to the one greppable line (3 lines changed, 0 net). gen/rust/tri/test/report.rs is regenerated with `t27c gen-rust`; the seal is saved and verifies MATCH. Co-Authored-By: Claude Sonnet 5.5 --- .trinity/seals/test_TriTestReport.json | 19 +- cli/tri/src/main.rs | 6 +- gen/rust/tri/test/report.rs | 158 ++++++++++-- specs/tri/test/report.t27 | 320 ++++++++++++++++++++++--- 4 files changed, 442 insertions(+), 61 deletions(-) diff --git a/.trinity/seals/test_TriTestReport.json b/.trinity/seals/test_TriTestReport.json index afb2de71a0..313aee7319 100644 --- a/.trinity/seals/test_TriTestReport.json +++ b/.trinity/seals/test_TriTestReport.json @@ -1,24 +1,25 @@ { - "built_by": "t27c-bootstrap@0.5.2+5d5d2cdef", + "built_by": "t27c-bootstrap@0.5.2+9b556b7c3", "closure": [], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:74674d3e38f3f62b92020f64892cf374e8def374e40e3c0089015b554f12fd8b", - "gen_hash_rust": "sha256:1de6c6f3a0ed67d11ff54d090d90429164ffa82c95756dc19c2286c8f6060697", - "gen_hash_verilog": "sha256:06d3c6e9febf8fd3f6c0cbe5a7a1fa71d9cac27dec668e4c85dc3d3c1beda9bc", - "gen_hash_zig": "sha256:a3ee9cd2ebbd6997c908463e3f3f2cda151186b679f4e78941f3c9770523d053", + "gen_hash_c": "sha256:78443d20e32fb0315cc175fae2dd319ad16ea89cd60888beac7c1fa3f8b512fb", + "gen_hash_rust": "sha256:0abbc039d04a1e3f093e2033a42df39c5e1ab3481347a14d96b5813eb228adf6", + "gen_hash_verilog": "sha256:b020c9c384bf2d7ae051f7f80cd2eb03c3afc33a77ad779e0eb26b11129d6493", + "gen_hash_zig": "sha256:5efb8d5404a6c7b616da08eaf2624ab361ff20b6261763cb4bac2b3792be1983", "module": "TriTestReport", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-09T15:00:22Z", + "sealed_at": "2026-10-18T15:33:49Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:2e781b2dc9d841f0c6482e06a328ac2c27a1c74bad71d847c283cf9111c62bd0", + "spec_hash": "sha256:f648fe411cdcc610536e6268baa64798ceabef7bb8b600991cd4c431236aef5b", "spec_path": "specs/tri/test/report.t27", "tests": { "failed": 0, "failing": [], "forced": false, - "passed": 13, - "total": 13 + "passed": 22, + "total": 22, + "vacuous": 0 }, "toolchain": { "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", diff --git a/cli/tri/src/main.rs b/cli/tri/src/main.rs index 50a456cb7f..89ccae1e9b 100644 --- a/cli/tri/src/main.rs +++ b/cli/tri/src/main.rs @@ -1016,10 +1016,10 @@ pub(crate) fn report_names(t: &'static str, k: u8) -> String { (0..report::count(t, k)).map(|n| &t[report::name_from(t, k, n)..report::name_to(t, k, n)]).collect::>().join(", ") } -/// The one greppable line: `tests: N, pass: P, fail: F (names)`, or `, BLOCKED: `. +/// The one greppable line: `tests: N, pass: P, fail: F (names)`, or `, BLOCKED: `, or `, vacuous: ` (#10497). pub(crate) fn report_summary(t: &'static str) -> String { - let (b, f, n) = (report_names(t, report::LINE_BLOCKED), report_names(t, report::LINE_FAIL_NAME), |k| report::total(t, k)); - let tail = if !b.is_empty() { format!(", BLOCKED: {b}") } else if !f.is_empty() { format!(" ({f})") } else { String::new() }; + let (b, f, v, n) = (report_names(t, report::LINE_BLOCKED), report_names(t, report::LINE_FAIL_NAME), report_names(t, report::LINE_VACUOUS_NAME), |k| report::total(t, k)); + let tail = if !b.is_empty() { format!(", BLOCKED: {b}") } else if !f.is_empty() { format!(" ({f})") } else if !v.is_empty() { format!(", vacuous: {v}") } else { String::new() }; format!("tests: {}, pass: {}, fail: {}{tail}", n(report::LINE_TESTS), n(report::LINE_PASS), n(report::LINE_FAIL)) } diff --git a/gen/rust/tri/test/report.rs b/gen/rust/tri/test/report.rs index d4e5b2304c..3a804ba0d7 100644 --- a/gen/rust/tri/test/report.rs +++ b/gen/rust/tri/test/report.rs @@ -1,6 +1,6 @@ // Generated from .t27 spec // DO NOT EDIT — generated by t27c -// NOT LOWERED BY THIS BACKEND: 13 test(s), 1 invariant(s), 0 function(s) with no body. +// NOT LOWERED BY THIS BACKEND: 22 test(s), 1 invariant(s), 0 function(s) with no body. // This backend emits declarations only. The spec's checks live in // the Zig and Verilog outputs; do not read this file as verified. @@ -18,6 +18,12 @@ pub const LINE_FAIL_NAME: u8 = 5; pub const LINE_PASS_NAME: u8 = 6; +pub const LINE_VACUOUS: u8 = 7; + +pub const LINE_VACUOUS_NAME: u8 = 8; + +pub const LINE_VACUOUS_UNKNOWN: u8 = 9; + pub const MAX_TOTAL_DIGITS: usize = 18; pub const V_GREEN: u8 = 0; @@ -38,6 +44,10 @@ pub const V_EXIT_GREEN: u8 = 7; pub const V_EXIT_UNREAD: u8 = 8; +pub const V_VACUOUS: u8 = 9; + +pub const V_UNCOUNTED: u8 = 10; + pub fn is_blank(c: u8) -> bool { return ((c == 32) || ((c >= 9) && (c <= 13))); } @@ -106,6 +116,63 @@ pub fn names_after(text: &'static str, at: usize, end: usize, word: &'static str return (is_blank(text.as_bytes()[((at + word.len())) as usize]) == false); } +pub fn digits_end(text: &'static str, k: usize, end: usize) -> usize { + let mut e: usize = k; + while (((e < end) && (text.as_bytes()[(e) as usize] >= 48)) && (text.as_bytes()[(e) as usize] <= 57)) { + e = (e + 1); + } + return e; +} + +pub fn number_at(text: &'static str, from: usize, end: usize) -> u64 { + let mut k: usize = from; + let mut value: u64 = 0; + while (((k < end) && (text.as_bytes()[(k) as usize] >= 48)) && (text.as_bytes()[(k) as usize] <= 57)) { + value = ((value * 10) + ((text.as_bytes()[(k) as usize] as u64) - 48)); + k = (k + 1); + } + return value; +} + +pub fn vacuous_digits(text: &'static str, at: usize, end: usize) -> usize { + if (opens_with(text, at, end, " vacuous passes ") == false) { + return (end + 1); + } + let n_from: usize = (at + 18); + let n_to: usize = digits_end(text, n_from, end); + if ((n_to == n_from) || ((n_to - n_from) > MAX_TOTAL_DIGITS)) { + return (end + 1); + } + if (opens_with(text, n_to, end, " of ") == false) { + return (end + 1); + } + let m_to: usize = digits_end(text, (n_to + 4), end); + if ((m_to == (n_to + 4)) || ((m_to - (n_to + 4)) > MAX_TOTAL_DIGITS)) { + return (end + 1); + } + if ((m_to < end) && (is_blank(text.as_bytes()[(m_to) as usize]) == false)) { + return (end + 1); + } + return n_from; +} + +pub fn vacuous_unknown(text: &'static str, at: usize, end: usize) -> bool { + if (opens_with(text, at, end, " vacuous passes unknown") == false) { + return false; + } + return (((at + 25) == end) || is_blank(text.as_bytes()[((at + 25)) as usize])); +} + +pub fn vacuous_name_line(text: &'static str, at: usize, end: usize) -> bool { + if (opens_with(text, at, end, " 0 ") == false) { + return false; + } + if ((end - at) < 21) { + return false; + } + return opens_with(text, (end - 10), end, " VACUOUS"); +} + pub fn line_kind(text: &'static str, at: usize, end: usize) -> u8 { if opens_with(text, at, end, " BLOCKED ") { return LINE_BLOCKED; @@ -125,6 +192,15 @@ pub fn line_kind(text: &'static str, at: usize, end: usize) -> u8 { if names_after(text, at, end, " pass ") { return LINE_PASS_NAME; } + if (vacuous_digits(text, at, end) != (end + 1)) { + return LINE_VACUOUS; + } + if vacuous_unknown(text, at, end) { + return LINE_VACUOUS_UNKNOWN; + } + if vacuous_name_line(text, at, end) { + return LINE_VACUOUS_NAME; + } return LINE_OTHER; } @@ -167,13 +243,23 @@ pub fn total(text: &'static str, kind: u8) -> u64 { word = " FAIL"; } let end: usize = line_end(text, at); - let mut k: usize = total_digits(text, at, end, word); - let mut value: u64 = 0; - while (((k < end) && (text.as_bytes()[(k) as usize] >= 48)) && (text.as_bytes()[(k) as usize] <= 57)) { - value = ((value * 10) + ((text.as_bytes()[(k) as usize] as u64) - 48)); - k = (k + 1); + return number_at(text, total_digits(text, at, end, word), end); +} + +pub fn vacuous_passes(text: &'static str) -> u64 { + let at: usize = line_of(text, LINE_VACUOUS, 0); + let end: usize = line_end(text, at); + return number_at(text, vacuous_digits(text, at, end), end); +} + +pub fn vacuous_of(text: &'static str) -> u64 { + let at: usize = line_of(text, LINE_VACUOUS, 0); + let end: usize = line_end(text, at); + let n_from: usize = vacuous_digits(text, at, end); + if (n_from > end) { + return 0; } - return value; + return number_at(text, (digits_end(text, n_from, end) + 4), end); } pub fn name_from(text: &'static str, kind: u8, n: u64) -> usize { @@ -184,12 +270,42 @@ pub fn name_from(text: &'static str, kind: u8, n: u64) -> usize { if (kind == LINE_BLOCKED) { return (at + 11); } + if (kind == LINE_VACUOUS_NAME) { + return (at + 10); + } return (at + 8); } pub fn name_to(text: &'static str, kind: u8, n: u64) -> usize { let from: usize = name_from(text, kind, n); - return trimmed_end(text, from, line_end(text, from)); + let mut to: usize = line_end(text, from); + if ((kind == LINE_VACUOUS_NAME) && (to >= (from + 10))) { + to = (to - 10); + } + return trimmed_end(text, from, to); +} + +pub fn vacuous_read(text: &'static str) -> u8 { + if (count(text, LINE_VACUOUS_UNKNOWN) > 0) { + return V_UNCOUNTED; + } + if (count(text, LINE_VACUOUS) == 0) { + if (count(text, LINE_VACUOUS_NAME) > 0) { + return V_NAMES_DISAGREE; + } + return V_GREEN; + } + let n: u64 = vacuous_passes(text); + if ((vacuous_of(text) != total(text, LINE_PASS)) || (n > vacuous_of(text))) { + return V_TOTALS_DISAGREE; + } + if (count(text, LINE_VACUOUS_NAME) != n) { + return V_NAMES_DISAGREE; + } + if (n > 0) { + return V_VACUOUS; + } + return V_GREEN; } pub fn read(text: &'static str) -> u8 { @@ -213,7 +329,11 @@ pub fn read(text: &'static str) -> u8 { if (tests == 0) { return V_NO_TEST; } - return V_GREEN; + return vacuous_read(text); +} + +pub fn is_verdict(v: u8) -> bool { + return (((v <= V_NO_TEST) || (v == V_VACUOUS)) || (v == V_UNCOUNTED)); } pub fn verdict(text: &'static str, exited_ok: bool) -> u8 { @@ -224,23 +344,19 @@ pub fn verdict(text: &'static str, exited_ok: bool) -> u8 { if ((r == V_FAILED) || (r == V_BLOCKED)) { return r; } - if ((r == V_GREEN) || (r == V_NO_TEST)) { + if is_verdict(r) { return V_EXIT_GREEN; } return V_EXIT_UNREAD; } -pub fn is_verdict(v: u8) -> bool { - return (v <= V_NO_TEST); -} - pub fn passes(v: u8) -> bool { return (v == V_GREEN); } pub fn why(v: u8) -> &'static str { if (v == V_GREEN) { - return "green: it built, at least one test ran, and none failed"; + return "green: it built, at least one test ran, none failed, and none passed without executing a runtime assert"; } if (v == V_FAILED) { return "a test FAILs"; @@ -255,13 +371,19 @@ pub fn why(v: u8) -> &'static str { return "t27c test-report printed no tests / pass / FAIL totals and no BLOCKED line"; } if (v == V_TOTALS_DISAGREE) { - return "t27c test-report's totals do not add up: pass + FAIL is not tests"; + return "t27c test-report's totals do not add up: pass + FAIL is not tests, or the vacuous passes are not of the passes"; } if (v == V_NAMES_DISAGREE) { - return "t27c test-report counts a number of FAIL that is not the number of FAIL names it lists"; + return "t27c test-report counts a number of FAIL (or of vacuous passes) that is not the number of names it lists"; } if (v == V_EXIT_GREEN) { - return "t27c test-report exited non-zero, yet its report reads green or ran no test; a run that disagrees with itself is not a pass"; + return "t27c test-report exited non-zero, yet its report reads green, vacuous or empty; a run that disagrees with itself is not a pass"; + } + if (v == V_VACUOUS) { + return "a test passed vacuously: it executed 0 runtime asserts, so its pass certifies nothing (T730); the VACUOUS lines name it"; + } + if (v == V_UNCOUNTED) { + return "t27c could not count the runtime asserts (its counting build did not compile), so a vacuous pass cannot be ruled out"; } return "t27c test-report exited non-zero and no report could be read from its output"; } diff --git a/specs/tri/test/report.t27 b/specs/tri/test/report.t27 index a09aa44672..00796c5aca 100644 --- a/specs/tri/test/report.t27 +++ b/specs/tri/test/report.t27 @@ -17,8 +17,11 @@ ; pass P ; FAIL F ; invariants I proved -- ... (an invariant is checked at compile time; it is not a test) -; and after the totals, per-test assert counts whose lines start with a number or '-'. -; Two rules: +; and after the totals, per-test assert counts whose lines start with a number or '-' (#6509): +; 0 VACUOUS (a test that passed and executed 0 runtime asserts; T730) +; vacuous passes N of M (passed with 0 runtime asserts executed) (M passes, N of them vacuous) +; vacuous passes unknown (the counting build did not compile: ...) (nothing could be counted) +; Three rules: ; fail closed -- a report with no totals and no BLOCKED line, totals that do not add up ; (pass + FAIL != tests), or a FAIL count that is not the number of FAIL names it lists, is not a ; verdict: it is an error, never a pass. @@ -26,6 +29,11 @@ ; on both. A red report with a non-zero exit is that red verdict. A non-zero exit with a report that ; reads green (or ran no test) disagrees with itself, and a non-zero exit with no readable report is ; an error: neither is a pass. +; no vacuous pass (#10497) -- a test that passes with 0 runtime asserts executed certifies nothing, so a +; report with N > 0 in its `vacuous passes N of M` line is not green: V_VACUOUS, and the VACUOUS lines +; name the tests. `unknown` is V_UNCOUNTED: nobody counted, so a vacuous pass cannot be ruled out. A +; report with no such line at all comes from a t27c older than #6509; there is nothing to read, so +; it keeps the reading it always had. ; Fixtures are test-report's real text for specs/ternary/gft_relu.t27 (2026-10-08, t27c from master). ; ASCII only (L3) ; phi^2 + 1/phi^2 = 3 | TRINITY @@ -40,12 +48,15 @@ pub const LINE_PASS : u8 = 3; pub const LINE_FAIL : u8 = 4; pub const LINE_FAIL_NAME : u8 = 5; pub const LINE_PASS_NAME : u8 = 6; +pub const LINE_VACUOUS : u8 = 7; +pub const LINE_VACUOUS_NAME : u8 = 8; +pub const LINE_VACUOUS_UNKNOWN : u8 = 9; // A total of more digits than this is not one t27c printed; 18 digits always fit in u64. pub const MAX_TOTAL_DIGITS : usize = 18; -// The verdict on one run. GREEN, FAILED, BLOCKED and NO_TEST are verdicts about the tests; the codes -// from NO_TOTALS up say the report itself cannot be believed. +// The verdict on one run. GREEN, FAILED, BLOCKED, NO_TEST, VACUOUS and UNCOUNTED are verdicts about the +// tests; the codes from NO_TOTALS up to EXIT_UNREAD say the report itself cannot be believed. pub const V_GREEN : u8 = 0; pub const V_FAILED : u8 = 1; pub const V_BLOCKED : u8 = 2; @@ -55,9 +66,11 @@ pub const V_TOTALS_DISAGREE : u8 = 5; pub const V_NAMES_DISAGREE : u8 = 6; pub const V_EXIT_GREEN : u8 = 7; pub const V_EXIT_UNREAD : u8 = 8; +pub const V_VACUOUS : u8 = 9; +pub const V_UNCOUNTED : u8 = 10; /// The kinds and verdicts are numbered as the glue and the tests below name them. -invariant the_kinds_and_verdicts_are_numbered { assert LINE_OTHER == 0 and LINE_PASS_NAME == 6 and V_GREEN == 0 and V_NO_TEST == 3 and V_EXIT_UNREAD == 8 and MAX_TOTAL_DIGITS == 18; } +invariant the_kinds_and_verdicts_are_numbered { assert LINE_OTHER == 0 and LINE_PASS_NAME == 6 and LINE_VACUOUS_UNKNOWN == 9 and V_GREEN == 0 and V_NO_TEST == 3 and V_EXIT_UNREAD == 8 and V_UNCOUNTED == 10 and MAX_TOTAL_DIGITS == 18; } /// Whitespace as a regex's \s reads ASCII: space, tab, newline, vertical tab, form feed, return. pub fn is_blank(c: u8) -> bool { @@ -118,8 +131,60 @@ pub fn names_after(text: string, at: usize, end: usize, word: string) -> bool { return is_blank(text[at + word.len]) == false; } +/// The end of the digits that start at k, never past end. +pub fn digits_end(text: string, k: usize, end: usize) -> usize { + var e : usize = k; + while (e < end and text[e] >= 48 and text[e] <= 57) { + e = e + 1; + } + return e; +} + +/// The number whose digits start at `from` on a line that ends at `end`; 0 when from is not a digit +/// (from = end + 1 is how total_digits and vacuous_digits say "not this line"). +pub fn number_at(text: string, from: usize, end: usize) -> u64 { + var k : usize = from; + var value : u64 = 0; + while (k < end and text[k] >= 48 and text[k] <= 57) { + value = value * 10 + ((text[k] as u64) - 48); + k = k + 1; + } + return value; +} + +/// The summary line ` vacuous passes N of M`, then the end of the line or a blank (t27c adds +/// ` (passed with 0 runtime asserts executed)`); N and M are 1 to MAX_TOTAL_DIGITS digits. Returns the +/// offset of N's digits, or end + 1 when the line is not that summary. +pub fn vacuous_digits(text: string, at: usize, end: usize) -> usize { + if (opens_with(text, at, end, " vacuous passes ") == false) { return end + 1; } + const n_from : usize = at + 18; + const n_to : usize = digits_end(text, n_from, end); + if (n_to == n_from or n_to - n_from > MAX_TOTAL_DIGITS) { return end + 1; } + if (opens_with(text, n_to, end, " of ") == false) { return end + 1; } + const m_to : usize = digits_end(text, n_to + 4, end); + if (m_to == n_to + 4 or m_to - (n_to + 4) > MAX_TOTAL_DIGITS) { return end + 1; } + if (m_to < end and is_blank(text[m_to]) == false) { return end + 1; } + return n_from; +} + +/// The summary line when nothing could be counted: ` vacuous passes unknown`, then the end of the line +/// or a blank (t27c adds ` (the counting build did not compile: )`). +pub fn vacuous_unknown(text: string, at: usize, end: usize) -> bool { + if (opens_with(text, at, end, " vacuous passes unknown") == false) { return false; } + return at + 25 == end or is_blank(text[at + 25]); +} + +/// A vacuous test's line ` 0 VACUOUS`: the count 0 right-aligned in 6 columns, a name of +/// one or more characters, three spaces, the word, the end of the line. +pub fn vacuous_name_line(text: string, at: usize, end: usize) -> bool { + if (opens_with(text, at, end, " 0 ") == false) { return false; } + if (end - at < 21) { return false; } + return opens_with(text, end - 10, end, " VACUOUS"); +} + /// The kind of the line text[at..end]. A total is tried before a name, so ` pass 3` is a total -/// and ` pass pos` a name; the per-test assert lines (` 1 pos`) are OTHER. +/// and ` pass pos` a name; the per-test assert lines (` 1 pos`) are OTHER, except a vacuous one +/// (` 0 pos VACUOUS`) and the vacuous-pass summary lines. pub fn line_kind(text: string, at: usize, end: usize) -> u8 { if (opens_with(text, at, end, " BLOCKED ")) { return LINE_BLOCKED; } if (total_digits(text, at, end, " tests") != end + 1) { return LINE_TESTS; } @@ -127,6 +192,9 @@ pub fn line_kind(text: string, at: usize, end: usize) -> u8 { if (total_digits(text, at, end, " FAIL") != end + 1) { return LINE_FAIL; } if (names_after(text, at, end, " FAIL ")) { return LINE_FAIL_NAME; } if (names_after(text, at, end, " pass ")) { return LINE_PASS_NAME; } + if (vacuous_digits(text, at, end) != end + 1) { return LINE_VACUOUS; } + if (vacuous_unknown(text, at, end)) { return LINE_VACUOUS_UNKNOWN; } + if (vacuous_name_line(text, at, end)) { return LINE_VACUOUS_NAME; } return LINE_OTHER; } @@ -165,31 +233,67 @@ pub fn total(text: string, kind: u8) -> u64 { if (kind == LINE_PASS) { word = " pass"; } if (kind == LINE_FAIL) { word = " FAIL"; } const end : usize = line_end(text, at); - var k : usize = total_digits(text, at, end, word); - var value : u64 = 0; - while (k < end and text[k] >= 48 and text[k] <= 57) { - value = value * 10 + ((text[k] as u64) - 48); - k = k + 1; - } - return value; + return number_at(text, total_digits(text, at, end, word), end); +} + +/// N of the first ` vacuous passes N of M` line: the passes that executed 0 runtime asserts; 0 when +/// there is no such line. +pub fn vacuous_passes(text: string) -> u64 { + const at : usize = line_of(text, LINE_VACUOUS, 0); + const end : usize = line_end(text, at); + return number_at(text, vacuous_digits(text, at, end), end); } -/// Where the n-th name of a name kind (LINE_FAIL_NAME, LINE_PASS_NAME, or LINE_BLOCKED's why) starts; -/// text.len when there is no such line, so text[name_from..name_to] is then empty. +/// M of that line: the passes it counted; 0 when there is no such line. +pub fn vacuous_of(text: string) -> u64 { + const at : usize = line_of(text, LINE_VACUOUS, 0); + const end : usize = line_end(text, at); + const n_from : usize = vacuous_digits(text, at, end); + if (n_from > end) { return 0; } + return number_at(text, digits_end(text, n_from, end) + 4, end); +} + +/// Where the n-th name of a name kind (LINE_FAIL_NAME, LINE_PASS_NAME, LINE_VACUOUS_NAME, or +/// LINE_BLOCKED's why) starts; text.len when there is no such line, so text[name_from..name_to] is then +/// empty. pub fn name_from(text: string, kind: u8, n: u64) -> usize { const at : usize = line_of(text, kind, n); if (at == text.len + 1) { return text.len; } if (kind == LINE_BLOCKED) { return at + 11; } + if (kind == LINE_VACUOUS_NAME) { return at + 10; } return at + 8; } -/// Where that name ends: its line's end without trailing blanks. +/// Where that name ends: its line's end without trailing blanks (and without the ` VACUOUS` of a +/// vacuous line). pub fn name_to(text: string, kind: u8, n: u64) -> usize { const from : usize = name_from(text, kind, n); - return trimmed_end(text, from, line_end(text, from)); + var to : usize = line_end(text, from); + if (kind == LINE_VACUOUS_NAME and to >= from + 10) { to = to - 10; } + return trimmed_end(text, from, to); +} + +/// What the vacuous-pass summary of a report whose tests all passed and at least one ran says (#10497). +/// `unknown` (the counting build did not compile) is UNCOUNTED. No summary line is GREEN: that is a t27c +/// from before #6509, which counted no asserts, and its reports have always been read as they are; but +/// VACUOUS names with no summary are a report cut short, not an old one. The summary must be of this +/// report's passes (M = pass, N <= M) and N must be the number of VACUOUS names listed above it; N > 0 is +/// VACUOUS. +pub fn vacuous_read(text: string) -> u8 { + if (count(text, LINE_VACUOUS_UNKNOWN) > 0) { return V_UNCOUNTED; } + if (count(text, LINE_VACUOUS) == 0) { + if (count(text, LINE_VACUOUS_NAME) > 0) { return V_NAMES_DISAGREE; } + return V_GREEN; + } + const n : u64 = vacuous_passes(text); + if (vacuous_of(text) != total(text, LINE_PASS) or n > vacuous_of(text)) { return V_TOTALS_DISAGREE; } + if (count(text, LINE_VACUOUS_NAME) != n) { return V_NAMES_DISAGREE; } + if (n > 0) { return V_VACUOUS; } + return V_GREEN; } -/// The report's verdict, its exit code left aside. BLOCKED anywhere wins: the spec never built. +/// The report's verdict, its exit code left aside. BLOCKED anywhere wins: the spec never built. A FAIL +/// is read before a vacuous pass, so a mutant that fails a test stays FAILED whatever else it passed. pub fn read(text: string) -> u8 { if (count(text, LINE_BLOCKED) > 0) { return V_BLOCKED; } if (count(text, LINE_TESTS) == 0 or count(text, LINE_PASS) == 0 or count(text, LINE_FAIL) == 0) { return V_NO_TOTALS; } @@ -199,7 +303,12 @@ pub fn read(text: string) -> u8 { if (count(text, LINE_FAIL_NAME) != failed) { return V_NAMES_DISAGREE; } if (failed > 0) { return V_FAILED; } if (tests == 0) { return V_NO_TEST; } - return V_GREEN; + return vacuous_read(text); +} + +/// A verdict about the tests, not an error about the report. +pub fn is_verdict(v: u8) -> bool { + return v <= V_NO_TEST or v == V_VACUOUS or v == V_UNCOUNTED; } /// The verdict on one run: the text's, and the exit only says what an unbelievable report means. A @@ -209,30 +318,28 @@ pub fn verdict(text: string, exited_ok: bool) -> u8 { const r : u8 = read(text); if (exited_ok) { return r; } if (r == V_FAILED or r == V_BLOCKED) { return r; } - if (r == V_GREEN or r == V_NO_TEST) { return V_EXIT_GREEN; } + if (is_verdict(r)) { return V_EXIT_GREEN; } return V_EXIT_UNREAD; } -/// A verdict about the tests, not an error about the report. -pub fn is_verdict(v: u8) -> bool { - return v <= V_NO_TEST; -} - -/// `tri test` passes only on GREEN: it built, at least one test ran, and none failed. +/// `tri test` passes only on GREEN: it built, at least one test ran, none failed, and none passed +/// without executing a runtime assert. pub fn passes(v: u8) -> bool { return v == V_GREEN; } /// What a verdict means, for the line the glue prints. pub fn why(v: u8) -> string { - if (v == V_GREEN) { return "green: it built, at least one test ran, and none failed"; } + if (v == V_GREEN) { return "green: it built, at least one test ran, none failed, and none passed without executing a runtime assert"; } if (v == V_FAILED) { return "a test FAILs"; } if (v == V_BLOCKED) { return "BLOCKED: the spec never built, so no test ran"; } if (v == V_NO_TEST) { return "no test ran: the spec has no `test` block (an invariant is proved at compile time; it is not a test)"; } if (v == V_NO_TOTALS) { return "t27c test-report printed no tests / pass / FAIL totals and no BLOCKED line"; } - if (v == V_TOTALS_DISAGREE) { return "t27c test-report's totals do not add up: pass + FAIL is not tests"; } - if (v == V_NAMES_DISAGREE) { return "t27c test-report counts a number of FAIL that is not the number of FAIL names it lists"; } - if (v == V_EXIT_GREEN) { return "t27c test-report exited non-zero, yet its report reads green or ran no test; a run that disagrees with itself is not a pass"; } + if (v == V_TOTALS_DISAGREE) { return "t27c test-report's totals do not add up: pass + FAIL is not tests, or the vacuous passes are not of the passes"; } + if (v == V_NAMES_DISAGREE) { return "t27c test-report counts a number of FAIL (or of vacuous passes) that is not the number of names it lists"; } + if (v == V_EXIT_GREEN) { return "t27c test-report exited non-zero, yet its report reads green, vacuous or empty; a run that disagrees with itself is not a pass"; } + if (v == V_VACUOUS) { return "a test passed vacuously: it executed 0 runtime asserts, so its pass certifies nothing (T730); the VACUOUS lines name it"; } + if (v == V_UNCOUNTED) { return "t27c could not count the runtime asserts (its counting build did not compile), so a vacuous pass cannot be ruled out"; } return "t27c test-report exited non-zero and no report could be read from its output"; } @@ -418,11 +525,41 @@ test each_line_is_read_as_its_kind { assert line_kind(" BLOCKED x", 0, 12) == LINE_BLOCKED; assert line_kind(" BLOCKED x", 0, 11) == LINE_OTHER; assert line_kind(" 1 pos", 0, 13) == LINE_OTHER; - assert line_kind(" vacuous passes 0 of 3", 0, 24) == LINE_OTHER; + assert line_kind(" vacuous passes 0 of 3", 0, 24) == LINE_VACUOUS; assert line_kind(" FAIL negz", 0, 11) == LINE_OTHER; assert line_kind("", 0, 0) == LINE_OTHER; } +// Scenario (#10497): the vacuous-pass lines t27c prints after the per-test assert counts -- the summary +// (`N of M`, or `unknown`) and a vacuous test's own line -- each have their kind, and a line that is +// almost one is OTHER. +test the_vacuous_lines_are_read_as_their_kind { + const s : string = " vacuous passes 1 of 4 (passed with 0 runtime asserts executed)"; + assert line_kind(s, 0, s.len) == LINE_VACUOUS; + const u : string = " vacuous passes unknown (the counting build did not compile: x)"; + assert line_kind(u, 0, u.len) == LINE_VACUOUS_UNKNOWN; + assert line_kind(" vacuous passes unknown", 0, 25) == LINE_VACUOUS_UNKNOWN; + assert line_kind(" vacuous passes unknownx", 0, 26) == LINE_OTHER; + assert line_kind(" vacuous passes 12 of 345", 0, 27) == LINE_VACUOUS; + assert line_kind(" vacuous passes 1 of", 0, 22) == LINE_OTHER; + assert line_kind(" vacuous passes of 4", 0, 22) == LINE_OTHER; + assert line_kind(" vacuous passes x of 4", 0, 24) == LINE_OTHER; + assert line_kind(" vacuous passes 1 of 4x", 0, 25) == LINE_OTHER; + assert line_kind(" vacuous passes 1 of 4", 0, 25) == LINE_OTHER; + assert line_kind(" vacuous passes 1 of 4", 0, 25) == LINE_OTHER; + assert line_kind(" vacuous passes 1 of 4", 0, 23) == LINE_OTHER; + assert line_kind(" vacuous passes 1234567890123456789 of 4", 0, 42) == LINE_OTHER; + assert line_kind(" vacuous passes 123456789012345678 of 4", 0, 41) == LINE_VACUOUS; + assert line_kind(" 0 negz VACUOUS", 0, 24) == LINE_VACUOUS_NAME; + assert line_kind(" 0 a VACUOUS", 0, 21) == LINE_VACUOUS_NAME; + assert line_kind(" 0 VACUOUS", 0, 20) == LINE_OTHER; + assert line_kind(" 1 negz VACUOUS", 0, 24) == LINE_OTHER; + assert line_kind(" 0 negz", 0, 14) == LINE_OTHER; + assert line_kind(" 0 negz VACUOUS ", 0, 25) == LINE_OTHER; + assert line_kind(" ? negz (passed, not counted)", 0, 38) == LINE_OTHER; + assert line_kind(" - negz (failed, not counted)", 0, 38) == LINE_OTHER; +} + // Scenario: a total of 18 digits is read, 19 is not a total, and a total with no digits is not one. test a_total_has_one_to_18_digits { assert total_digits(" tests 123456789012345678", 0, 28, " tests") == 10; @@ -503,6 +640,124 @@ test the_failing_set_is_the_expected_set_or_nothing { assert named(two, LINE_FAIL_NAME, "pos\npos3", 1) == false; } +// Scenario (#10497): 4 tests pass and each executed at least one runtime assert -- `vacuous passes 0 of 4` +// -- so the run is green and `tri test` passes it. The summary is read: it is the one line of its kind. +test no_vacuous_pass_is_green { + const r : string = "--- test report: s.t27 ---\n\n tests 4\n pass 4\n FAIL 0\n rate 100.0%\n\n runtime asserts executed, per test (#6509; a pass with 0 is vacuous, T730):\n 1 pos\n 2 negz\n 1 zero\n 1 pos2\n vacuous passes 0 of 4 (passed with 0 runtime asserts executed)\n"; + assert count(r, LINE_VACUOUS) == 1; + assert count(r, LINE_VACUOUS_NAME) == 0; + assert count(r, LINE_VACUOUS_UNKNOWN) == 0; + assert vacuous_passes(r) == 0; + assert vacuous_of(r) == 4; + assert read(r) == V_GREEN; + assert verdict(r, true) == V_GREEN; + assert passes(verdict(r, true)) == true; +} + +// Scenario (#10497): the same run with one test that passed and executed 0 runtime asserts -- `vacuous +// passes 1 of 4` -- is refused, whatever the exit, and the VACUOUS line names the test. +test a_vacuous_pass_is_refused_and_named { + const r : string = "--- test report: s.t27 ---\n\n tests 4\n pass 4\n FAIL 0\n rate 100.0%\n\n runtime asserts executed, per test (#6509; a pass with 0 is vacuous, T730):\n 1 pos\n 0 negz VACUOUS\n 1 zero\n 1 pos2\n vacuous passes 1 of 4 (passed with 0 runtime asserts executed)\n"; + assert vacuous_passes(r) == 1; + assert vacuous_of(r) == 4; + assert count(r, LINE_VACUOUS_NAME) == 1; + assert same_names(r, LINE_VACUOUS_NAME, "negz", 1) == true; + assert name_to(r, LINE_VACUOUS_NAME, 0) - name_from(r, LINE_VACUOUS_NAME, 0) == 4; + assert count(r, LINE_PASS_NAME) == 0; + assert read(r) == V_VACUOUS; + assert verdict(r, true) == V_VACUOUS; + assert passes(verdict(r, true)) == false; + assert is_verdict(V_VACUOUS) == true; + assert verdict(r, false) == V_EXIT_GREEN; + assert passes(verdict(r, false)) == false; +} + +// Scenario (#10497): t27c's real text for a spec with 3 tests, one of which asserts and two of which run +// no assert (measured 2026-10-18); both vacuous tests are named, in report order. +test every_vacuous_test_is_named { + const r : string = "--- test report: v.t27 ---\n\n tests 3\n pass 3\n FAIL 0\n rate 100.0%\n\n runtime asserts executed, per test (#6509; a pass with 0 is vacuous, T730):\n 1 checked_one\n 0 vacuous_one VACUOUS\n 0 vacuous_two VACUOUS\n vacuous passes 2 of 3 (passed with 0 runtime asserts executed)\n"; + assert vacuous_passes(r) == 2; + assert vacuous_of(r) == 3; + assert count(r, LINE_VACUOUS_NAME) == 2; + assert is_entry(r, name_from(r, LINE_VACUOUS_NAME, 0), name_to(r, LINE_VACUOUS_NAME, 0), "vacuous_one\nvacuous_two", 0) == true; + assert is_entry(r, name_from(r, LINE_VACUOUS_NAME, 1), name_to(r, LINE_VACUOUS_NAME, 1), "vacuous_one\nvacuous_two", 1) == true; + assert same_names(r, LINE_VACUOUS_NAME, "vacuous_one\nvacuous_two", 2) == true; + assert same_names(r, LINE_VACUOUS_NAME, "vacuous_one", 1) == false; + assert named(r, LINE_VACUOUS_NAME, "checked_one", 0) == false; + assert name_from(r, LINE_VACUOUS_NAME, 2) == r.len; + assert name_to(r, LINE_VACUOUS_NAME, 2) == r.len; + assert read(r) == V_VACUOUS; +} + +// Scenario (#10497): a report with no vacuous-pass line at all is what a t27c from before #6509 printed +// (no per-test counts). There is nothing to read, so it keeps the reading it always had: GREEN. +test a_report_without_the_vacuous_line_keeps_the_old_reading { + const r : string = "--- test report: s.t27 ---\n\n tests 4\n pass 4\n FAIL 0\n rate 100.0%\n"; + assert count(r, LINE_VACUOUS) == 0; + assert vacuous_passes(r) == 0; + assert vacuous_of(r) == 0; + assert read(r) == V_GREEN; + assert verdict(r, true) == V_GREEN; + assert verdict(r, false) == V_EXIT_GREEN; +} + +// Scenario (#10497): `unknown` means the counting build did not compile and no assert was counted, so +// nothing says the passes were not vacuous. That is not a pass. +test an_uncounted_report_is_refused { + const r : string = "--- test report: s.t27 ---\n\n tests 2\n pass 2\n FAIL 0\n rate 100.0%\n\n runtime asserts executed, per test (#6509; a pass with 0 is vacuous, T730):\n ? a (passed, not counted)\n ? b (passed, not counted)\n vacuous passes unknown (the counting build did not compile: error: x)\n"; + assert count(r, LINE_VACUOUS_UNKNOWN) == 1; + assert count(r, LINE_VACUOUS) == 0; + assert vacuous_passes(r) == 0; + assert read(r) == V_UNCOUNTED; + assert verdict(r, true) == V_UNCOUNTED; + assert passes(verdict(r, true)) == false; + assert is_verdict(V_UNCOUNTED) == true; + assert verdict(r, false) == V_EXIT_GREEN; +} + +// Scenario (#10497): negative control. Take away what t27c counted and the same run reads green again, so +// it is the vacuous-pass lines that refuse the run. Leave the VACUOUS line without its summary (a report +// cut short), or make the summary say 0 while a test is listed vacuous, and the run is not believed. +test only_the_vacuous_lines_refuse_a_run { + const head : string = "--- test report: s.t27 ---\n\n tests 2\n pass 2\n FAIL 0\n"; + const cut : string = "--- test report: s.t27 ---\n\n tests 2\n pass 2\n FAIL 0\n\n runtime asserts executed, per test (#6509; a pass with 0 is vacuous, T730):\n 1 a\n 0 b VACUOUS\n"; + const lie : string = "--- test report: s.t27 ---\n\n tests 2\n pass 2\n FAIL 0\n\n runtime asserts executed, per test (#6509; a pass with 0 is vacuous, T730):\n 1 a\n 0 b VACUOUS\n vacuous passes 0 of 2 (passed with 0 runtime asserts executed)\n"; + const truth : string = "--- test report: s.t27 ---\n\n tests 2\n pass 2\n FAIL 0\n\n runtime asserts executed, per test (#6509; a pass with 0 is vacuous, T730):\n 1 a\n 0 b VACUOUS\n vacuous passes 1 of 2 (passed with 0 runtime asserts executed)\n"; + assert read(head) == V_GREEN; + assert read(truth) == V_VACUOUS; + assert read(cut) == V_NAMES_DISAGREE; + assert read(lie) == V_NAMES_DISAGREE; + assert passes(read(cut)) == false; + assert passes(read(lie)) == false; + assert passes(read(truth)) == false; + assert passes(read(head)) == true; +} + +// Scenario (#10497): a vacuous summary that is not of this report's passes, or that counts more vacuous +// passes than passes, or that lists a different number of VACUOUS names than it counts, is an error, not +// a pass and not a verdict about the tests. +test a_vacuous_summary_that_does_not_add_up_is_an_error { + assert read("\n tests 4\n pass 4\n FAIL 0\n vacuous passes 5 of 4\n") == V_TOTALS_DISAGREE; + assert read("\n tests 4\n pass 4\n FAIL 0\n vacuous passes 1 of 3\n") == V_TOTALS_DISAGREE; + assert read("\n tests 4\n pass 4\n FAIL 0\n vacuous passes 1 of 5\n") == V_TOTALS_DISAGREE; + assert read("\n tests 4\n pass 4\n FAIL 0\n 0 a VACUOUS\n vacuous passes 2 of 4\n") == V_NAMES_DISAGREE; + assert read("\n tests 4\n pass 4\n FAIL 0\n 0 a VACUOUS\n 0 b VACUOUS\n vacuous passes 1 of 4\n") == V_NAMES_DISAGREE; + assert is_verdict(V_TOTALS_DISAGREE) == false; + assert is_verdict(V_NAMES_DISAGREE) == false; + assert verdict("\n tests 4\n pass 4\n FAIL 0\n vacuous passes 5 of 4\n", false) == V_EXIT_UNREAD; +} + +// Scenario (#10497): a FAIL is read before a vacuous pass, so a mutant that fails a test is FAILED (and +// `tri mutate plant` names it) whatever else the run passed vacuously. +test a_failing_test_outranks_a_vacuous_pass { + const r : string = "--- test report: s.t27 ---\n FAIL negz\n\n tests 4\n pass 3\n FAIL 1\n\n runtime asserts executed, per test (#6509; a pass with 0 is vacuous, T730):\n 1 pos\n - negz (failed, not counted)\n 0 zero VACUOUS\n 1 pos2\n vacuous passes 1 of 3 (passed with 0 runtime asserts executed)\n"; + assert read(r) == V_FAILED; + assert verdict(r, true) == V_FAILED; + assert verdict(r, false) == V_FAILED; + assert count(r, LINE_FAIL_NAME) == 1; + assert count(r, LINE_VACUOUS_NAME) == 1; +} + // Scenario: each verdict has its own words, and the green one is not an error's. test each_verdict_says_what_it_means { assert why(V_GREEN)[0] == 103; @@ -514,4 +769,7 @@ test each_verdict_says_what_it_means { assert why(V_NAMES_DISAGREE)[17] == 99; assert why(V_EXIT_GREEN)[32] == 44; assert why(V_EXIT_UNREAD)[32] == 32; + assert why(V_VACUOUS)[0] == 97; + assert why(V_VACUOUS)[7] == 112; + assert why(V_UNCOUNTED)[5] == 99; }