feat(frontier): --watch skips a spec whose four gen hashes did not change

.trinity/seals/verified_VerifiedWatch.json

@@ -1,24 +1,24 @@
 {
-  "built_by": "t27c-bootstrap@0.5.2+760a7871c",
+  "built_by": "t27c-bootstrap@0.5.2+5d45445e",
   "closure": [],
   "config": "gen=c,rust,verilog,zig;tests=zig",
-  "gen_hash_c": "sha256:73aa6d59f711757d1f8038859d6f5469fa343f099337f2e86cf870369507d81e",
-  "gen_hash_rust": "sha256:6cf94bd1884e9674e997fa9d4ed5718f1fd7502bc686334a168353e44aca45cd",
-  "gen_hash_verilog": "sha256:9e9a0aa116e3746831c7d64cb7176ac3d23bb31eb78c5fcbb16b873ecbd8cdf2",
-  "gen_hash_zig": "sha256:eeb8d565e32427095f0390120f7a072d3c393d017147c01dacfef3ad6448a07b",
+  "gen_hash_c": "sha256:686c7ba03754c08421b05e5002e1ffe383dac15c97180197e4fa33d15280665e",
+  "gen_hash_rust": "sha256:f7ca0ba2e14e2796590bb7e029a977d94581949f6b55f8f17ea58a3626371a35",
+  "gen_hash_verilog": "sha256:2ee4782fae92463f809f345e6acc9a4f98140d2270819017750017edbbe34b8c",
+  "gen_hash_zig": "sha256:618c60b430c618c76bca33cd429024775215afa30096187ef002177f258554cb",
   "module": "VerifiedWatch",
   "ring": 12,
   "seal_schema": 2,
-  "sealed_at": "2026-10-11T07:26:02Z",
+  "sealed_at": "2026-10-18T05:34:30Z",
   "sealed_by": "t27c-bootstrap@0.5.2",
-  "spec_hash": "sha256:565124edea485e32be951c6188490489aff66073a6c95adf748bef740d48be5c",
+  "spec_hash": "sha256:c00a263202a3b4f299cb9b96b515f6bda0470117bfc003ff227a83b467b4e0b5",
   "spec_path": "specs/verified/watch.t27",
   "tests": {
     "failed": 0,
     "failing": [],
     "forced": false,
-    "passed": 3,
-    "total": 3,
+    "passed": 5,
+    "total": 5,
     "vacuous": 0
   },
   "toolchain": {

bootstrap/gen/rust/verified/watch.rs

@@ -1,6 +1,6 @@
 // Generated from .t27 spec
 // DO NOT EDIT — generated by t27c
-// NOT LOWERED BY THIS BACKEND: 3 test(s), 1 invariant(s), 0 function(s) with no body.
+// NOT LOWERED BY THIS BACKEND: 5 test(s), 2 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.
 
@@ -29,3 +29,13 @@ pub fn watch_take(affected: u32) -> u32 {
     return affected;
 }
 
+pub fn watch_skip(recorded: bool, computable: bool, same_gen: bool) -> bool {
+    if (recorded == false) {
+        return false;
+    }
+    if (computable == false) {
+        return false;
+    }
+    return same_gen;
+}
+

bootstrap/src/service.rs

@@ -5687,7 +5687,7 @@ pub fn run_frontier(list: bool, reseal: bool, audit: Option<u32>, watch: bool) -
     }
     if poisoned > 0 { anyhow::bail!("{poisoned} reused verdict(s) disagree with their rerun (specs/verified/verdict_audit.t27)") }
     // --watch (#8737 H5): rerun every spec whose closure digest changed since the last look (watch.t27).
-    let mut last: std::collections::HashMap<String, String> = Default::default();
+    let (mut last, mut gens): (std::collections::HashMap<String, String>, std::collections::HashMap<String, [String; 4]>) = Default::default(); // gens (#10237): the four gen hashes at the first look or last rerun; a moved digest over unchanged ones is not rerun (watch_skip), its digest is still recorded
     // #8821: stat every file the last walk read, before walking, and walk only when one moved (watch_walk)
     let stat = |p: &str| { use std::os::unix::fs::MetadataExt; std::fs::metadata(p).map(|m| (m.mtime(), m.mtime_nsec(), m.len(), m.ino())).unwrap_or_default() };
     let mut seen: std::collections::HashMap<String, (i64, i64, u64, u64)> = Default::default();
@@ -5697,16 +5697,16 @@ pub fn run_frontier(list: bool, reseal: bool, audit: Option<u32>, watch: bool) -
         seen = looked;
         DIG.with(|m| m.borrow_mut().clear());
         let now: Vec<(String, String)> = specs.iter().map(|p| (p.clone(), digest(p, 0))).collect();
-        let changed: Vec<&(String, String)> = now.iter().filter(|(p, d)| wt::watch_rerun(last.contains_key(p), last.get(p) != Some(d))).collect();
+        let (changed, skipped): (Vec<&(String, String)>, Vec<&(String, String)>) = { let cand: Vec<&(String, String)> = now.iter().filter(|(p, d)| wt::watch_rerun(last.contains_key(p), last.get(p) != Some(d))).collect(); let gn = crate::suite::par_in_order(&cand, |c| gen_cached(&c.0, &tc)); let (a, b): (Vec<_>, Vec<_>) = cand.into_iter().zip(gn).partition(|(c, g)| !wt::watch_skip(gens.contains_key(&c.0), g.is_some(), g.as_ref() == gens.get(&c.0))); (a.into_iter().map(|x| x.0).collect(), b.into_iter().map(|x| x.0).collect()) };
         // #8852: reruns side by side, specs sharing a file stem on one worker (test_report names its scratch dir by stem and pid)
         let batch: Vec<&(String, String)> = changed.iter().take(wt::watch_take(changed.len() as u32) as usize).copied().collect();
         let mut stems: Vec<(String, Vec<usize>)> = Vec::new();
         for (i, (p, _)) in batch.iter().enumerate() { let st = Path::new(p).file_stem().map(|x| x.to_string_lossy().into_owned()).unwrap_or_default(); match stems.iter_mut().find(|g| g.0 == st) { Some(g) => g.1.push(i), None => stems.push((st, vec![i])) } }
         // #8956: each verdict prints the moment its rerun ends, from the worker that ran it; the digests are recorded after
         let done = crate::suite::par_in_order(&stems, |g| g.1.iter().map(|&i| { let p = &batch[i].0; let r = crate::test_report::run(Path::new(p), Path::new("specs")); println!("{} {p}: {} of {} pass{}", if r.blocked.is_some() { "BLOCKED" } else if r.failed > 0 { "FAIL" } else { "ok" }, r.passed, r.total, r.blocked.as_deref().map(|b| format!(" -- {}", b.lines().next().unwrap_or(""))).unwrap_or_default()); i }).collect::<Vec<_>>());
-        for i in done.into_iter().flatten() { let (p, d) = batch[i]; last.insert(p.clone(), d.clone()); }
+        for i in done.into_iter().flatten() { let (p, d) = batch[i]; last.insert(p.clone(), d.clone()); if let Some(g) = gen_cached(p, &tc) { gens.insert(p.clone(), g); } } for (p, d) in &skipped { last.insert(p.clone(), d.clone()); }
         if changed.len() as u32 > wt::WATCH_BATCH { println!("watch: {} more changed specs wait for the next look", changed.len() as u32 - wt::WATCH_BATCH) }
-        for (p, d) in &now { last.entry(p.clone()).or_insert_with(|| d.clone()); }
+        if last.is_empty() { for (p, g) in specs.iter().zip(crate::suite::par_in_order(&specs, |p| gen_cached(p, &tc))) { if let Some(g) = g { gens.insert(p.clone(), g); } } } for (p, d) in &now { last.entry(p.clone()).or_insert_with(|| d.clone()); }
         std::thread::sleep(std::time::Duration::from_millis(wt::WATCH_POLL_MS as u64));
     }
     Ok(())

specs/verified/watch.t27

@@ -30,6 +30,13 @@
 ; The batch. A save to a hub (types.t27 is imported by hundreds of specs) changes many digests at once. At
 ; most WATCH_BATCH specs are rerun per look, in path order, and the rest are counted and stay changed, so
 ; the next look takes them; the loop never goes quiet on a change it has not rerun.
+; --
+; Same code, no rerun (#10237). The closure digest hashes source text, so a comment or a blank line moves it
+; while the four generated outputs (Zig, Verilog, C, Rust; gen_hash_cache.t27) stay byte-identical -- and a
+; rerun of a spec whose generated code did not change cannot change its verdict, it only costs about 2 s. A
+; spec whose digest moved is rerun only when its four gen hashes differ from the ones recorded at its first
+; look or last rerun. A spec with no recorded or no computable gen hashes is rerun (fail open to a rerun,
+; never to silence). A skipped spec still has its digest recorded, so the next look does not see it as changed.
 ; phi^2 + 1/phi^2 = 3 | TRINITY
 
 module VerifiedWatch;
@@ -58,6 +65,13 @@ pub fn watch_take(affected: u32) -> u32 {
     return affected;
 }
 
+/// A spec whose digest moved is NOT rerun only when its gen hashes were recorded, are computable now, and are unchanged.
+pub fn watch_skip(recorded: bool, computable: bool, same_gen: bool) -> bool {
+    if (recorded == false) { return false; }
+    if (computable == false) { return false; }
+    return same_gen;
+}
+
 test watch_rerun_only_a_changed_spec_seen_before {
     assert watch_rerun(true, true) == true;
     assert watch_rerun(true, false) == false;
@@ -82,7 +96,29 @@ test watch_take_caps_a_hub_save {
     assert watch_take(0) == 0;
 }
 
+test watch_skip_only_when_the_generated_code_is_provably_the_same {
+    // a comment edit: recorded, computable, identical gen hashes -> no rerun
+    assert watch_skip(true, true, true) == true;
+    // an expression edit: the gen hashes moved -> rerun
+    assert watch_skip(true, true, false) == false;
+}
+
+test negative_control_watch_skip_fails_open_to_a_rerun {
+    // no recorded gen hashes, or none computable now: never silence, even if "same" were claimed
+    assert watch_skip(false, true, true) == false;
+    assert watch_skip(true, false, true) == false;
+    assert watch_skip(false, false, true) == false;
+    assert watch_skip(false, false, false) == false;
+}
+
 invariant the_watch_stays_responsive {
     assert WATCH_POLL_MS >= 100 and WATCH_POLL_MS <= 2000;
     assert WATCH_BATCH >= 1;
 }
+
+invariant a_skip_needs_all_three_facts {
+    assert watch_skip(true, true, true) == true;
+    assert watch_skip(true, true, false) == false;
+    assert watch_skip(true, false, false) == false;
+    assert watch_skip(false, false, false) == false;
+}