tri test: refuse vacuous passes -- report.t27 reads the "vacuous passes N of M" line (Closes #10497)

.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",

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::<Vec<_>>().join(", ")
 }
 
-/// The one greppable line: `tests: N, pass: P, fail: F (names)`, or `, BLOCKED: <why>`.
+/// The one greppable line: `tests: N, pass: P, fail: F (names)`, or `, BLOCKED: <why>`, or `, vacuous: <names>` (#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))
 }
 

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";
 }