From b612c720f4431a7c9fb8caf93d017b4ff62ae301 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 12:36:04 +0700 Subject: [PATCH] feat(frontier): --watch skips a spec whose four gen hashes did not change (Closes #10237) The watch loop reran every spec whose closure digest moved, and the digest hashes source text: a comment or a blank line moves it while the Zig, Verilog, C and Rust outputs stay byte-identical, so the rerun (about 2 s) could not change the verdict. specs/verified/watch.t27 gains watch_skip(recorded, computable, same_gen), with tests and a negative control: a spec with no recorded or no computable gen hashes is rerun (fail open to a rerun, never to silence). The loop records each spec's four gen hashes (gen_cached, the cache the digest already keys) at the first look and after every rerun, and supplies the three booleans. A skipped spec still has its digest recorded, so the next look does not see it as changed again. The hand-written Rust is net zero lines (4 added, 4 deleted). Co-Authored-By: Claude Sonnet 5.5 --- .trinity/seals/verified_VerifiedWatch.json | 18 +++++------ bootstrap/gen/rust/verified/watch.rs | 12 +++++++- bootstrap/src/service.rs | 8 ++--- specs/verified/watch.t27 | 36 ++++++++++++++++++++++ 4 files changed, 60 insertions(+), 14 deletions(-) diff --git a/.trinity/seals/verified_VerifiedWatch.json b/.trinity/seals/verified_VerifiedWatch.json index 6858f58d01..a947fe3c88 100644 --- a/.trinity/seals/verified_VerifiedWatch.json +++ b/.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": { diff --git a/bootstrap/gen/rust/verified/watch.rs b/bootstrap/gen/rust/verified/watch.rs index 7c57869118..11544c4b89 100644 --- a/bootstrap/gen/rust/verified/watch.rs +++ b/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; +} + diff --git a/bootstrap/src/service.rs b/bootstrap/src/service.rs index 884c1756cf..8d6537a3a2 100644 --- a/bootstrap/src/service.rs +++ b/bootstrap/src/service.rs @@ -5687,7 +5687,7 @@ pub fn run_frontier(list: bool, reseal: bool, audit: Option, 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 = Default::default(); + let (mut last, mut gens): (std::collections::HashMap, std::collections::HashMap) = 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 = Default::default(); @@ -5697,16 +5697,16 @@ pub fn run_frontier(list: bool, reseal: bool, audit: Option, 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)> = 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::>()); - 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(()) diff --git a/specs/verified/watch.t27 b/specs/verified/watch.t27 index 2a52cac942..1fae15ee5a 100644 --- a/specs/verified/watch.t27 +++ b/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; +}