diff --git a/dag/gunbc/executor_schedule_retention.dag b/dag/gunbc/executor_schedule_retention.dag new file mode 100644 index 00000000000..0be70769eff --- /dev/null +++ b/dag/gunbc/executor_schedule_retention.dag @@ -0,0 +1,21 @@ +module gunbc.executor_schedule_retention + +data schedule_retention_policy_note: String = "The v1 claim executor holds the WHOLE batch schedule before it runs a witness, so per-module retention is EXACT, not heuristic: each module's retained typed state (typed-module result, normalize/ownership diagnostic memos, parse-body entry in the process-shared MultiEntryIndex) is refcounted by the number of remaining scheduled entries whose closure reaches it, and dropped the moment that count hits zero. Derived from declared inputs (the schedule x the module-graph closure); no threshold, no recency heuristic, no GC. DESIGN grounding: S2 (drop dead weight is the master move), S4 (a heuristic is never necessary in a closed system - the schedule exists, so retention is computed not guessed), S5 (fail-closed). Authority: this carrier; the Rust realization in cli_run.rs mirrors each fact below and schedule_retention_policy_matches_modeled_authority reds on drift - the extdeps.realization.resolved_graph SizeBounded-cap lockstep pattern applied to a policy. Dissolution trigger: the cross-entry typed-module-memo ladder SpacePacked eviction (PR-beta), the same trigger floor_drain_retention_test.dag's Never/ScopeExit note carries." + +data schedule_retention_tunable_count: Int = 0 + +data schedule_retention_tunable_count_note: String = "Zero by construction: the retention rule is the schedule's remaining demand, full stop - no threshold, no recency, no confidence dial. Mirrored by SCHEDULE_RETENTION_TUNABLE_COUNT in cli_run.rs; a nonzero here (a smuggled heuristic - S5's confidence-threshold tell) must move BOTH surfaces and face review." + +data schedule_retention_grain_is_per_module: Bool = true + +data schedule_retention_heads_stay_resident: Bool = true + +data schedule_retention_heads_note: String = "Heads (the whole-pool parse snapshot and the bare/qualified census layers) are NOT per-module state and are never evicted - the #6848 bare-name census requires the whole-pool heads resident for the run's lifetime (heads-only parse #6956/#6972 precedent). Held by construction: only per-module cache keys are recorded for eviction." + +data schedule_retention_retain_on_unknown: Bool = true + +data schedule_retention_retain_on_unknown_note: String = "When reachability CANNOT be computed for a cached module (a provenance gap), the safe arm is RETAIN - correctness-fail-closed but memory-fail-open - so it is a typed, per-module, COUNTED RetentionUnknown row, never a silent retain-everything (that absorbing fallback is a T-as-ignorance widen whose frequency the corpus would never see, S5)." + +data schedule_retention_underflow_refuses: Bool = true + +data schedule_retention_underflow_note: String = "A decrement past zero (a scheduled entry demands state the refcount said was fully consumed) is a schedule-derivation defect and REFUSES, typed and located - the mechanism never serves a wrong verdict against evicted state. Content-key recompute-on-miss is the correctness license; the refusal is the loudness that keeps a derivation bug from hiding." diff --git a/dag/test/claim/executor_schedule_retention_test.dag b/dag/test/claim/executor_schedule_retention_test.dag new file mode 100644 index 00000000000..fda8b431d9e --- /dev/null +++ b/dag/test/claim/executor_schedule_retention_test.dag @@ -0,0 +1,22 @@ +module test.claim.executor_schedule_retention + +import gunbc.executor_schedule_retention { + schedule_retention_tunable_count, + schedule_retention_grain_is_per_module, + schedule_retention_heads_stay_resident, + schedule_retention_retain_on_unknown, + schedule_retention_underflow_refuses, +} + +data witness_note: String = "In-corpus consumer of the schedule-derived retention policy carrier: asserts the modeled policy facts by execution (green-by-execution). The Rust realization in cli_run.rs mirrors these same facts and a Rust lockstep witness (schedule_retention_policy_matches_modeled_authority) pins the two together, so a policy edit that forgets either side reds." + +test fn schedule_retention_exposes_no_tunables() -> Bool { + schedule_retention_tunable_count == 0 +} + +test fn schedule_retention_policy_is_fail_closed() -> Bool { + schedule_retention_grain_is_per_module + && schedule_retention_heads_stay_resident + && schedule_retention_retain_on_unknown + && schedule_retention_underflow_refuses +} diff --git a/docs/probes/witness_entry_eligibility_census.tsv b/docs/probes/witness_entry_eligibility_census.tsv index 22ecd198491..b43239194db 100644 --- a/docs/probes/witness_entry_eligibility_census.tsv +++ b/docs/probes/witness_entry_eligibility_census.tsv @@ -1,4 +1,4 @@ -# witness_entry_eligibility_census stamp=2026-07-23T19:48Z grain=entry_closure roots=witness_layer_roots(test.dag with test fn/data) +# witness_entry_eligibility_census stamp=2026-07-24T00:55Z grain=entry_closure roots=witness_layer_roots(test.dag with test fn/data) entry module_path subject_module subject_decl disposition retained_or_ineligible_reason first_error_class execution_leg dag/test/claim/accelerator_demo_execution_witness_test.dag test.claim.accelerator_demo_execution_witness test.claim.accelerator_demo_execution_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg dag/test/claim/accelerator_demo_gpu_witness_test.dag test.claim.accelerator_demo_gpu_witness test.claim.accelerator_demo_gpu_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg @@ -99,6 +99,7 @@ dag/test/claim/emit_host_gate_verdicts_test.dag test.claim.emit_host_gate_verdic dag/test/claim/emit_host_gate_witness_test.dag test.claim.emit_host_gate_witness test.claim.emit_host_gate_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg dag/test/claim/emit_host_typed_smoke_test.dag test.claim.emit_host_typed_smoke_test test.claim.emit_host_typed_smoke_test witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg dag/test/claim/exec_arg_limit_witness_test.dag test.claim.exec_arg_limit_witness test.claim.exec_arg_limit_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg +dag/test/claim/executor_schedule_retention_test.dag test.claim.executor_schedule_retention test.claim.executor_schedule_retention witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg dag/test/claim/extdeps_anemia_grounding_witness_test.dag test.claim.extdeps_anemia_grounding_witness test.claim.extdeps_anemia_grounding_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg dag/test/claim/extdeps_dpkg_witness_test.dag test.claim.extdeps_dpkg_witness test.claim.extdeps_dpkg_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg dag/test/claim/extdeps_git_diff_name_status_witness_test.dag test.claim.extdeps_git_diff_name_status_witness test.claim.extdeps_git_diff_name_status_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg diff --git a/docs/probes/witness_entry_eligibility_histogram.txt b/docs/probes/witness_entry_eligibility_histogram.txt index 83625daeacd..ed51f488b4e 100644 --- a/docs/probes/witness_entry_eligibility_histogram.txt +++ b/docs/probes/witness_entry_eligibility_histogram.txt @@ -1,6 +1,6 @@ -# witness_entry_eligibility_histogram stamp=2026-07-23T19:48Z total_entries=880 +# witness_entry_eligibility_histogram stamp=2026-07-24T00:55Z total_entries=881 disposition reason count -InterpretedRetained BulkFlipPendingCensusIncomplete 700 +InterpretedRetained BulkFlipPendingCensusIncomplete 701 EmitIneligible OfflineLocalRecipe 82 EmitIneligible LongLaneScheduled 64 InterpretedRetained EmitOnDemandFamilyGrain 26 diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index d57c326b57f..ae779d93e05 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -3847,6 +3847,19 @@ pub fn import_closure_live_paths_with_facts( import_closure_from_adjacency(entry_path, &facts.adjacency) } +/// Like `import_closure_live_paths_with_facts` but over the WIDER `selection_adjacency` +/// (import + strict reference edges) — so a module reached cross-entry only through a +/// bare-reference edge is still refcounted by schedule-derived retention. Over-retaining +/// (the safe direction: never premature-evict a reference-reached module into a +/// recompute-on-miss) and equally cheap: a BFS over prebuilt adjacency, no per-entry +/// source loading, no #6848 both-closure fixpoint. +pub(crate) fn selection_closure_live_paths_with_facts( + entry_path: &str, + facts: &ModuleGraphFactsLive, +) -> Vec { + import_closure_from_adjacency(entry_path, &facts.selection_adjacency) +} + impl ModuleGraphFactsLive { /// Repo-relative paths of every declared module in the facts scan — the existence /// set for refuse-vs-answer decisions (a module can be absent from `adjacency` @@ -5527,6 +5540,14 @@ pub struct MultiEntryIndex { ), >, >, + /// Schedule-derived per-module retention bookkeeping (v1-run-stability M2 — the + /// retention keystone). Armed at the start of a private-index (`cross_worker_store + /// == None`) discovery run from the schedule's per-entry closures, driven per + /// entry-completion in `run_discovery_rows`. `None` when unarmed (Adaptive shared + /// store, single-claim paths, tests): retention stays the pre-M2 process-lifetime + /// hold, so the mechanism is strictly additive. Authority: modeled policy in + /// `dag/gunbc/executor_schedule_retention.dag`, mirrored above. + schedule_retention: RefCell>, } pub fn new_shared_typecheck_caches() -> Arc> { @@ -5645,6 +5666,7 @@ fn new_multi_entry_index_shell( normalize_diag_cache: RefCell::new(std::collections::HashMap::new()), ownership_diag_cache: RefCell::new(std::collections::HashMap::new()), resolved_graph_memo: RefCell::new(HashMap::new()), + schedule_retention: RefCell::new(None), source_roots: source_roots.to_vec(), pool_parse: RefCell::new(None), pool_qualified_fill: RefCell::new(None), @@ -5996,6 +6018,670 @@ fn note_interface_hash( ); } +// ───────────────────────────────────────────────────────────────────────────── +// Schedule-derived retention (v1-run-stability throughline M2 — the retention +// keystone). The executor holds the WHOLE batch schedule before it runs a witness, +// so per-module retention can be EXACT: refcount each module's retained typed state +// by the number of remaining scheduled entries whose closure reaches it, and drop it +// the moment that count hits zero. The policy is DERIVED from declared inputs (the +// schedule × the module-graph closure) — no threshold, no recency heuristic, no GC. +// +// Authority is the modeled carrier `dag/gunbc/executor_schedule_retention.dag`; the +// consts below MIRROR it and `schedule_retention_policy_matches_modeled_authority` +// (this module's tests) reds on drift — the `extdeps.realization.resolved_graph` +// `SizeBounded`-cap lockstep pattern applied to a policy instead of a number. +// +// Correctness license (why evicting typed state can never yield a wrong verdict): +// the typed-module cache is CONTENT-keyed, so a later entry that reaches an evicted +// module simply recomputes it (cache miss → identical result). The interpreter never +// reads typed envs at eval (#5892: floor GREEN with envs evicted, RED with items +// evicted). Eviction therefore frees bytes without touching meaning; the only risk +// it must guard is a SCHEDULE-DERIVATION defect, which it refuses loudly (below). +// ───────────────────────────────────────────────────────────────────────────── + +/// Single-authority mirror of the modeled policy fact +/// `gunbc.executor_schedule_retention.schedule_retention_tunable_count` +/// (`dag/gunbc/executor_schedule_retention.dag`). Zero by construction: the retention +/// rule is the schedule's remaining demand, full stop. A nonzero here would be a +/// smuggled heuristic (DESIGN §4/§5) and must move BOTH surfaces and face review. +/// Kept in lockstep by `schedule_retention_policy_matches_modeled_authority`. +const SCHEDULE_RETENTION_TUNABLE_COUNT: i64 = 0; + +/// Measurement control (RED #1): with `GUNBC_SCHEDULE_RETENTION_EVICT=0` the schedule +/// still ARMS and COUNTS (refcounts, RetentionUnknown, decrement-underflow refusals) +/// but drops nothing — reproducing today's pegged peak so the mechanism's effect on +/// RSS is measurable both directions. This is NOT a §5 escape hatch: it bypasses no +/// fail-closed refusal (RetentionUnknown still retains-and-counts; a schedule +/// underflow still refuses) — it only chooses whether the freed-by-schedule bytes are +/// actually released, the retain-all pole being exactly the pre-M2 behavior. +fn schedule_retention_evict_enabled() -> bool { + !matches!( + std::env::var("GUNBC_SCHEDULE_RETENTION_EVICT") + .ok() + .as_deref(), + Some("0") | Some("false") | Some("off") + ) +} + +/// The cache keys one module holds in the process-shared `MultiEntryIndex`, recorded +/// as the module reconciles so eviction drops exactly its per-module state — never a +/// head (the whole-pool parse snapshot and census layers are not per-module state and +/// are never recorded here, so `schedule_retention_heads_stay_resident` holds by +/// construction). +#[derive(Default, Clone)] +struct ModuleCacheKeys { + /// Content keys under which this module's typed result lives in `typed_module_cache`. + typed_keys: HashSet, + /// Raw `span.file` keys under which this module lives in the parse / normalize-diag + /// / ownership-diag / source-hash caches (all keyed by the same raw file path). + raw_files: HashSet, +} + +/// One entry-completion's eviction decision — applied to the index caches by the +/// caller (this struct owns no cache handles, so it stays a pure, unit-testable +/// bookkeeper; the RED controls exercise it in isolation). +#[derive(Default, Debug, PartialEq, Eq)] +pub struct ScheduleEvictionBatch { + pub typed_keys: Vec, + pub raw_files: Vec, + /// The module names dropped this step (for the located receipt line). + pub module_names: Vec, +} + +/// Schedule-derived per-module retention bookkeeping (pure). Refcount is keyed by +/// REPO-RELATIVE MODULE PATH — the identity `selection_closure_live_paths_with_facts` +/// (arming, a cheap prebuilt-adjacency BFS) and `workspace_relative_repo_path` +/// (reconcile's `decl_file`) both produce. A path-form mismatch between those two — +/// the only latent hazard — degrades to "retain + count as RetentionUnknown", never +/// to a wrong verdict (proven aligned on a live index by +/// `schedule_eviction_end_to_end_on_real_index`). +pub struct ScheduleRetention { + /// module path → remaining scheduled entries whose closure reaches it. + refcount: std::collections::HashMap, + /// entry path → the closure module paths it reaches (stored at arm time so the + /// per-entry decrement uses the SAME paths arming counted). + entry_closures: std::collections::HashMap>, + /// module path → its recorded cache keys (filled as modules reconcile; a cache + /// hit re-records idempotently so a module first cached under an earlier entry + /// still carries its keys when its refcount finally reaches zero). + cache_keys: std::collections::HashMap, + /// names already counted as RetentionUnknown (cached but reachability-uncomputable) + /// — counted once, retained forever (never evicted). + unknown_counted: HashSet, + schedule_evictions: u64, + retention_unknown: u64, + /// Assembled `ResolvedGraph`s dropped from `resolved_graph_memo` on entry completion + /// (Fact #4): each strong-`Rc`-pins the very `TypedModule`s per-module eviction drops, + /// so without this the module bytes never free ("strong Rc pins from elsewhere"). + resolved_graph_evictions: u64, + /// Measurement pole (RED #1): false ⇒ compute everything, drop nothing. + evict_enabled: bool, +} + +impl ScheduleRetention { + /// Arm from each DISTINCT scheduled entry's closure module names. `refcount[name]` + /// becomes the count of entries whose closure contains `name`. Entries whose + /// closure could not be computed are simply absent — their modules become + /// `RetentionUnknown` (retained + counted) at reconcile, the fail-closed arm. + pub fn armed(per_entry: Vec<(String, Vec)>, evict_enabled: bool) -> Self { + let mut refcount: std::collections::HashMap = + std::collections::HashMap::new(); + let mut entry_closures: std::collections::HashMap> = + std::collections::HashMap::new(); + for (entry, names) in per_entry { + for name in &names { + *refcount.entry(name.clone()).or_insert(0) += 1; + } + // Last distinct occurrence wins; rows are grouped by entry so an entry + // appears once, but be robust to a repeat by keeping the widest closure. + entry_closures + .entry(entry) + .and_modify(|existing| { + if names.len() > existing.len() { + *existing = names.clone(); + } + }) + .or_insert(names); + } + ScheduleRetention { + refcount, + entry_closures, + cache_keys: std::collections::HashMap::new(), + unknown_counted: HashSet::new(), + schedule_evictions: 0, + retention_unknown: 0, + resolved_graph_evictions: 0, + evict_enabled, + } + } + + /// Record a module's cache keys as it reconciles (hit or miss; idempotent). A + /// module whose name the arming never reached is a provenance gap: count it ONCE + /// as `RetentionUnknown` and retain it — never silently drop, never widen to + /// retain-everything (that absorbing fallback is the §5 review-reject). + pub fn record_module(&mut self, name: &str, typed_key: &str, raw_file: &str) { + if !self.refcount.contains_key(name) && self.unknown_counted.insert(name.to_string()) { + self.retention_unknown += 1; + } + let entry = self.cache_keys.entry(name.to_string()).or_default(); + if !typed_key.is_empty() { + entry.typed_keys.insert(typed_key.to_string()); + } + if !raw_file.is_empty() { + entry.raw_files.insert(raw_file.to_string()); + } + } + + /// One scheduled entry finished: decrement each of its closure names, collect the + /// names that reached zero (no remaining entry can read them) with their recorded + /// cache keys for the caller to drop. A decrement of a name already at zero means a + /// scheduled entry demands state the refcount said was fully consumed — a + /// schedule-derivation defect — and REFUSES, typed and located (never a silent + /// wrong verdict against evicted state). `RetentionUnknown` names carry no refcount + /// entry, so they are never decremented and never evicted. + pub fn entry_completed(&mut self, entry: &str) -> Result { + let names = match self.entry_closures.get(entry) { + Some(names) => names.clone(), + None => return Ok(ScheduleEvictionBatch::default()), + }; + self.decrement_closure(entry, &names) + } + + /// Test injection for RED #3: run the decrement over an EXPLICIT closure, so a + /// synthetic corruption (an entry reaching a module the arming under-counted) can + /// exercise the underflow refusal — a state the consistent stored-closure path + /// cannot reach in production (refcount is derived from the same closures it + /// decrements), which is the whole point: the wall is unreachable by construction + /// and refuses if a future refactor ever breaches it. + #[cfg(test)] + pub fn force_entry_completed_for_test( + &mut self, + entry: &str, + names: &[String], + ) -> Result { + self.decrement_closure(entry, names) + } + + fn decrement_closure( + &mut self, + entry: &str, + names: &[String], + ) -> Result { + let mut batch = ScheduleEvictionBatch::default(); + for name in names { + let name = name.clone(); + let Some(rc) = self.refcount.get_mut(&name) else { + // Not refcounted (RetentionUnknown or never armed): retained. + continue; + }; + if *rc == 0 { + return Err(format!( + "SCHEDULE-RETENTION REFUSAL cause=RefcountUnderflow module='{name}' \ + entry='{entry}' — a scheduled entry's closure reaches a module whose \ + retention refcount was already zero (its state may have been evicted). \ + The schedule derivation under-counted this module's demand; refusing \ + rather than serving a verdict against missing state (DESIGN §5)." + )); + } + *rc -= 1; + if *rc == 0 { + // Keep the (name → 0) entry resident rather than removing it: a later + // decrement of an under-counted module then hits the `*rc == 0` arm + // above and REFUSES, instead of silently reading as "never armed". The + // map is bounded by module count, so retaining zeros is free. + if self.evict_enabled { + if let Some(keys) = self.cache_keys.remove(&name) { + batch.typed_keys.extend(keys.typed_keys); + batch.raw_files.extend(keys.raw_files); + } + batch.module_names.push(name); + self.schedule_evictions += 1; + } + } + } + Ok(batch) + } + + pub fn schedule_evictions(&self) -> u64 { + self.schedule_evictions + } + pub fn retention_unknown(&self) -> u64 { + self.retention_unknown + } + pub fn resolved_graph_evictions(&self) -> u64 { + self.resolved_graph_evictions + } + pub fn note_graph_eviction(&mut self) { + self.resolved_graph_evictions += 1; + } + /// Number of distinct modules the arming refcounted — for the unconditional + /// ARMED receipt line. + pub fn refcount_len(&self) -> usize { + self.refcount.len() + } +} + +/// Arm schedule-derived retention over a discovery run's WHOLE schedule (`rows` = every +/// scheduled entry's rows). Called ONCE by the drain caller (Serial: the single run; Adaptive +/// width=1: before the entry-group loop) so refcounts span the whole batch and a shared module +/// survives until its last consumer — NOT per `run_discovery_rows` call, which would hand the +/// Adaptive inline drain a one-entry schedule per group (refcount 1 on the whole closure → the +/// entries=1 cold-recompute churn). Only the private index path (`cross_worker_store == None`) +/// arms — the serial + adaptive-width-1 inline drains that share the long-lived process index +/// whose typed mass this bounds. The Adaptive plural/shared-store worker path keeps its current +/// behavior (typed results live in the byte store whose scheduled eviction is the PR-β +/// `SpacePacked` follow-on) — a declared, typed frontier, never a silent widen. A per-entry +/// closure that cannot be computed is skipped (its modules become counted `RetentionUnknown` at +/// reconcile), so arming never fails the run. +fn index_arm_schedule_retention(index: &MultiEntryIndex, rows: &[DiscoveryRow]) { + if index.cross_worker_store.is_some() { + return; + } + let mut per_entry: Vec<(String, Vec)> = Vec::new(); + let mut seen: HashSet<&str> = HashSet::new(); + for row in rows { + if !seen.insert(row.entry.as_str()) { + continue; + } + // CHEAP closure: a BFS over the prebuilt selection adjacency (import + strict + // reference edges; no per-entry source loading, no #6848 both-closure fixpoint + // walk) — keyed by the repo-relative path the reconcile loop records + // (`decl_file`). The prior `collect_both_closure_module_names_for_entry` + // front-loaded the source-loading fixpoint for every distinct entry (the + // compiler-affected worst case is ~694), a cost the affected-set path otherwise + // skips or defers. The wider selection tier over-retains (never premature-evicts + // a reference-reached module into a recompute-on-miss); a module reached by no + // edge at all surfaces as counted RetentionUnknown at reconcile (retained, §5). + let paths = selection_closure_live_paths_with_facts(&row.entry, &index.module_graph_facts); + per_entry.push((row.entry.clone(), paths)); + } + let evict_enabled = schedule_retention_evict_enabled(); + let entries = per_entry.len(); + if !evict_enabled { + // Loud, once per armed run: an accidentally-set env must not silently revert the + // M2 memory win in CI. Without this line the receipt's `schedule_evictions=0` is + // the only tell, and a zero reads as "nothing to evict" rather than "eviction off". + eprintln!( + "[floor-drain] SCHEDULE-RETENTION EVICTION DISABLED \ + (GUNBC_SCHEDULE_RETENTION_EVICT=0): arming + counting only, dropping NOTHING — \ + the retain-all measurement pole (pre-M2 process-lifetime retention). \ + schedule_evictions will be 0 BY CONSTRUCTION; unset the env to restore eviction." + ); + } + let sr = ScheduleRetention::armed(per_entry, evict_enabled); + // Unconditional ARMED receipt: proves schedule-derived retention is LIVE on this run, + // so a later `schedule_evictions=0` reads as "shared closure held resident" rather + // than "never armed" (the private-index serial regime is the only one that arms). + eprintln!( + "[floor-drain] schedule-retention ARMED: entries={entries} \ + modules_refcounted={} evict_enabled={evict_enabled}", + sr.refcount_len() + ); + *index.schedule_retention.borrow_mut() = Some(sr); +} + +/// Record a reconciled module's cache keys with the armed schedule retention (no-op +/// when unarmed). Called from the reconcile loop where the authored name, content +/// key, and raw file are all in hand. +fn index_record_schedule_module( + index: &MultiEntryIndex, + name: &str, + typed_key: &str, + raw_file: &str, +) { + if let Some(sr) = index.schedule_retention.borrow_mut().as_mut() { + sr.record_module(name, typed_key, raw_file); + } +} + +/// Drive one entry-completion: decrement the entry's closure refcounts, drop the +/// per-module state that reached zero from every per-module cache (typed, parse, +/// normalize-diag, ownership-diag, source-hash), AND drop the entry's assembled +/// `ResolvedGraph` from `resolved_graph_memo` (keyed by `subject`) — the graph strong- +/// `Rc`-pins the same modules, so without it the per-module eviction frees no bytes +/// (Fact #4 / the brief's "strong Rc pins from elsewhere"). Heads are never touched. A +/// schedule underflow propagates as a typed, located refusal. Emits an unconditional +/// per-entry progress line so a timed-out walk still shows eviction working (the early- +/// receipt discipline — the walk-end receipt never lands on a step-cap death). +fn index_schedule_entry_completed( + index: &MultiEntryIndex, + entry: &str, + subject: Option<&str>, +) -> Result<(), String> { + let batch = { + let mut slot = index.schedule_retention.borrow_mut(); + match slot.as_mut() { + Some(sr) => sr.entry_completed(entry)?, + None => return Ok(()), + } + }; + if !batch.typed_keys.is_empty() { + let mut cache = index.typed_module_cache.borrow_mut(); + for key in &batch.typed_keys { + cache.remove(key); + } + } + if !batch.raw_files.is_empty() { + let mut parse = index.parse_cache.borrow_mut(); + let mut norm = index.normalize_diag_cache.borrow_mut(); + let mut own = index.ownership_diag_cache.borrow_mut(); + let mut src = index.source_hash_by_file.borrow_mut(); + for file in &batch.raw_files { + parse.remove(file); + norm.remove(file); + own.remove(file); + src.remove(file); + } + } + // Drop the completed entry's assembled graph. The entry's own `InterpContext` still + // holds it until the next resolve, so this only removes the memo's pin; a rare later + // entry with the identical closure re-resolves (a memo miss, cost only). + let graph_evicted = match subject { + Some(subj) => index + .resolved_graph_memo + .borrow_mut() + .remove(subj) + .is_some(), + None => false, + }; + let (sched_evictions, retention_unknown, graph_evictions) = { + let mut slot = index.schedule_retention.borrow_mut(); + match slot.as_mut() { + Some(sr) => { + if graph_evicted { + sr.note_graph_eviction(); + } + ( + sr.schedule_evictions(), + sr.retention_unknown(), + sr.resolved_graph_evictions(), + ) + } + None => (0, 0, 0), + } + }; + // Unconditional (not floor_verbose-gated) so the receipt survives a step-cap timeout. + eprintln!( + "[floor-drain] schedule-retention: entry='{entry}' evicted_modules={} evicted_graph={} \ + schedule_evictions={sched_evictions} graph_evictions={graph_evictions} \ + retention_unknown={retention_unknown} typed_cache={} resolved_graphs={}", + batch.module_names.len(), + graph_evicted as u8, + index.typed_module_cache.borrow().len(), + index.resolved_graph_memo.borrow().len(), + ); + Ok(()) +} + +#[cfg(test)] +mod schedule_retention_red_controls { + use super::{ScheduleRetention, SCHEDULE_RETENTION_TUNABLE_COUNT}; + + /// Locate the modeled retention-policy carrier by walking up from the crate + /// manifest dir until `dag/gunbc/executor_schedule_retention.dag` appears — the + /// same workspace-anchoring the resolved-graph cap lockstep test uses. + fn read_modeled_policy() -> String { + let mut dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")); + loop { + let candidate = dir.join("dag/gunbc/executor_schedule_retention.dag"); + if candidate.exists() { + return std::fs::read_to_string(&candidate) + .expect("read executor_schedule_retention.dag"); + } + if !dir.pop() { + panic!( + "could not locate dag/gunbc/executor_schedule_retention.dag from manifest dir" + ); + } + } + } + + fn modeled_int(dag: &str, name: &str) -> i64 { + let line = dag + .lines() + .find(|l| l.trim_start().starts_with(&format!("data {name}:"))) + .unwrap_or_else(|| panic!("modeled `data {name}` not found")); + line.split('=') + .nth(1) + .and_then(|rhs| rhs.trim().parse::().ok()) + .unwrap_or_else(|| panic!("modeled `{name}` is not a bare Int")) + } + + fn modeled_bool(dag: &str, name: &str) -> bool { + let line = dag + .lines() + .find(|l| l.trim_start().starts_with(&format!("data {name}:"))) + .unwrap_or_else(|| panic!("modeled `data {name}` not found")); + line.split('=') + .nth(1) + .map(|rhs| rhs.trim() == "true") + .unwrap() + } + + /// LOCKSTEP: the Rust realization mirrors the modeled policy authority. Reds if the + /// modeled `.dag` and the Rust drift — the `resolved_graph` `SizeBounded`-cap + /// lockstep pattern applied to the policy (its "no tunables" fact and fail-closed + /// shape). + #[test] + fn schedule_retention_policy_matches_modeled_authority() { + let dag = read_modeled_policy(); + assert_eq!( + modeled_int(&dag, "schedule_retention_tunable_count"), + SCHEDULE_RETENTION_TUNABLE_COUNT, + "Rust SCHEDULE_RETENTION_TUNABLE_COUNT drifted from the modeled policy — a \ + nonzero tunable count is a smuggled heuristic (DESIGN §4/§5); move BOTH and \ + face review" + ); + // The fail-closed policy shape the mechanism realizes (asserted true in the model). + for flag in [ + "schedule_retention_grain_is_per_module", + "schedule_retention_heads_stay_resident", + "schedule_retention_retain_on_unknown", + "schedule_retention_underflow_refuses", + ] { + assert!(modeled_bool(&dag, flag), "modeled {flag} must be true"); + } + } + + /// GREEN: eviction fires exactly at refcount zero. A shared module survives until + /// its LAST scheduled entry; an entry-unique module drops the moment its entry + /// completes. Heads are never recorded here, so they are never evicted. + #[test] + fn schedule_eviction_drops_at_refcount_zero() { + // entry a: {shared, a_only}; entry b: {shared, b_only} + let mut sr = ScheduleRetention::armed( + vec![ + ("a".to_string(), vec!["shared".into(), "a_only".into()]), + ("b".to_string(), vec!["shared".into(), "b_only".into()]), + ], + true, + ); + sr.record_module("shared", "tk_shared", "f_shared"); + sr.record_module("a_only", "tk_a", "f_a"); + sr.record_module("b_only", "tk_b", "f_b"); + + // Finishing a drops a_only (rc 1→0); shared stays (rc 2→1). + let batch_a = sr.entry_completed("a").expect("no underflow"); + assert_eq!(batch_a.module_names, vec!["a_only".to_string()]); + assert_eq!(batch_a.typed_keys, vec!["tk_a".to_string()]); + assert_eq!(sr.schedule_evictions(), 1); + + // Finishing b drops shared (rc 1→0) and b_only. + let batch_b = sr.entry_completed("b").expect("no underflow"); + let mut got: Vec = batch_b.module_names.clone(); + got.sort(); + assert_eq!(got, vec!["b_only".to_string(), "shared".to_string()]); + assert_eq!(sr.schedule_evictions(), 3); + assert_eq!(sr.retention_unknown(), 0); + } + + /// RED #1 (eviction-disabled control): with `evict_enabled=false` the schedule + /// still arms, records, counts, and REFUSES underflow — but drops nothing, so peak + /// retention is the pre-M2 process-lifetime hold. This is the control run that + /// reproduces today's peak to prove the mechanism moves RSS. + #[test] + fn schedule_eviction_disabled_retains_everything_but_still_counts() { + let mut sr = ScheduleRetention::armed( + vec![("a".to_string(), vec!["m".into()])], + false, // eviction disabled (measurement pole) + ); + sr.record_module("m", "tk", "f"); + sr.record_module("orphan", "tk_o", "f_o"); // not in any closure → RetentionUnknown + let batch = sr.entry_completed("a").expect("no underflow"); + assert!(batch.module_names.is_empty(), "disabled pole drops nothing"); + assert_eq!(sr.schedule_evictions(), 0); + assert_eq!( + sr.retention_unknown(), + 1, + "counting still on with eviction off" + ); + } + + /// RED #3 (reachability corruption → typed refusal): a schedule whose arming + /// under-counted a module's demand (a later entry reaches state the refcount said + /// was fully consumed) REFUSES, typed and located — never a silent wrong verdict + /// against evicted state. + #[test] + fn schedule_underflow_refuses_typed() { + // `m` is armed for ONE entry but reached by TWO — a corrupted (too-low) count. + let mut sr = ScheduleRetention::armed( + vec![ + ("a".to_string(), vec!["m".into()]), + ("b".to_string(), vec![]), // b's closure was mis-derived to omit m + ], + true, + ); + // Hand b the closure it REALLY reaches (includes m) to simulate the corruption. + // (In production the two come from one arming source; this forces the underflow.) + sr.entry_completed("a").expect("first consume ok"); // m: 1→0, evicted + let err = sr + .force_entry_completed_for_test("b", &["m".to_string()]) + .expect_err("underflow must refuse"); + assert!( + err.contains("RefcountUnderflow") && err.contains("module='m'"), + "refusal must be typed and located, got: {err}" + ); + } + + /// RED #4 (RetentionUnknown counted): a module cached but reached by no scheduled + /// entry's closure (a provenance gap) shows up as a nonzero, per-module count — + /// retained, visible, prioritizable — never absorbed into a silent retain-all. + #[test] + fn retention_unknown_is_counted_per_module_once() { + let mut sr = ScheduleRetention::armed(vec![("a".to_string(), vec!["known".into()])], true); + sr.record_module("known", "tk", "f"); + sr.record_module("gap", "tk_g", "f_g"); + sr.record_module("gap", "tk_g2", "f_g2"); // re-record same gap: counted once + assert_eq!(sr.retention_unknown(), 1); + // The gap is never decremented/evicted: finishing `a` leaves it retained. + let batch = sr.entry_completed("a").expect("no underflow"); + assert!(!batch.module_names.contains(&"gap".to_string())); + } + + /// END-TO-END WIRING (real index, real closure computation, real cache eviction): + /// two entries sharing one library module. Arm from the schedule, resolve both + /// entries (populating the process-shared caches through the actual reconcile + /// path that records each module), then drive per-entry completion. The + /// shared module survives entry A's completion (still reachable by B) and drops + /// only when B completes — proving the mechanism frees real per-module state on a + /// live `MultiEntryIndex`, not just in the pure bookkeeper above. + #[test] + fn schedule_eviction_end_to_end_on_real_index() { + // Probe corpus must live UNDER the workspace root — path normalization + // refuses anything outside it. `target/` is gitignored, so it stays clean. + let dir = super::workspace_root() + .join("target") + .join(format!("sched_ret_probe_{}_e2e", std::process::id())); + let _ = std::fs::remove_dir_all(&dir); + std::fs::create_dir_all(&dir).expect("mkdir probe corpus"); + std::fs::write( + dir.join("shared_lib.dag"), + "module sched_ret_probe.shared_lib\n\ndata shared_val: Int = 7\n", + ) + .unwrap(); + std::fs::write( + dir.join("entry_a.dag"), + "module sched_ret_probe.entry_a\n\nimport sched_ret_probe.shared_lib { shared_val }\n\ndata a_val: Int = shared_val\n", + ) + .unwrap(); + std::fs::write( + dir.join("entry_b.dag"), + "module sched_ret_probe.entry_b\n\nimport sched_ret_probe.shared_lib { shared_val }\n\ndata b_val: Int = shared_val\n", + ) + .unwrap(); + + let root = dir.to_string_lossy().to_string(); + let entry_a = dir.join("entry_a.dag").to_string_lossy().to_string(); + let entry_b = dir.join("entry_b.dag").to_string_lossy().to_string(); + let index = super::build_multi_entry_index(&[root.clone()]); + + let rows = vec![ + super::DiscoveryRow { + label: "a".into(), + entry: entry_a.clone(), + function: "a_probe".into(), + reads_live_tree: false, + }, + super::DiscoveryRow { + label: "b".into(), + entry: entry_b.clone(), + function: "b_probe".into(), + reads_live_tree: false, + }, + ]; + super::index_arm_schedule_retention(&index, &rows); + super::resolve_entry_with_index(&index, &entry_a).expect("resolve a"); + super::resolve_entry_with_index(&index, &entry_b).expect("resolve b"); + + // Both closures reconciled → all three modules cached, and each entry's + // assembled ResolvedGraph is memoized (the strong-Rc pin Fact #4 drops). + let full = super::typed_module_cache_len_for_test(&index); + assert_eq!(full, 3, "entry_a + entry_b + shared_lib cached"); + let subj_a = super::subject_digest_for_closure( + &super::load_sources_for_entry_with_pool(&index, &entry_a).unwrap(), + ); + let subj_b = super::subject_digest_for_closure( + &super::load_sources_for_entry_with_pool(&index, &entry_b).unwrap(), + ); + let graphs_full = super::index_retention_snapshot(&index).resolved_graph_memo_entries; + assert!( + graphs_full >= 2, + "each entry's ResolvedGraph memoized (got {graphs_full})" + ); + + // Completing A drops entry_a's unique module AND its ResolvedGraph pin (Fact #4). + super::index_schedule_entry_completed(&index, &entry_a, Some(&subj_a)).expect("complete a"); + assert_eq!( + super::typed_module_cache_len_for_test(&index), + 2, + "entry_a evicted; shared_lib + entry_b remain" + ); + assert_eq!( + super::index_retention_snapshot(&index).resolved_graph_memo_entries, + graphs_full - 1, + "entry_a's ResolvedGraph dropped" + ); + + // Completing B drops entry_b AND the now-unreachable shared_lib (+ B's graph). + super::index_schedule_entry_completed(&index, &entry_b, Some(&subj_b)).expect("complete b"); + assert_eq!( + super::typed_module_cache_len_for_test(&index), + 0, + "shared_lib survived until its last entry, then dropped" + ); + + let snap = super::index_retention_snapshot(&index); + assert_eq!(snap.schedule_evictions, 3); + assert_eq!(snap.retention_unknown, 0); + assert_eq!( + snap.resolved_graph_memo_entries, 0, + "both entries' ResolvedGraphs evicted — the pin is released" + ); + + let _ = std::fs::remove_dir_all(&dir); + } +} + /// Interim width=1 floor-drain retention (v1-run-stability throughline, parent /// governor lane): instrument accumulation + host-budget entry cap on the private /// `typed_module_cache` only. Whole-row eviction here is a counted safety backstop, @@ -6010,6 +6696,12 @@ pub struct IndexRetentionSnapshot { pub ownership_diag_cache_entries: usize, pub intern_table_entries: usize, pub typed_cache_evictions: u64, + /// Schedule-derived per-module evictions (v1-run-stability M2): modules dropped + /// because no remaining scheduled entry's closure reached them. + pub schedule_evictions: u64, + /// Counted `RetentionUnknown` rows: modules cached but reachability-uncomputable, + /// retained (correctness-fail-closed) — visible and prioritizable, never absorbed. + pub retention_unknown: u64, pub peak_rss_bytes: Option, } @@ -6098,6 +6790,18 @@ pub fn index_retention_snapshot(index: &MultiEntryIndex) -> IndexRetentionSnapsh ownership_diag_cache_entries: index.ownership_diag_cache.borrow().len(), intern_table_entries: index.intern_table.borrow().index.len(), typed_cache_evictions: index.typed_cache_evictions.get(), + schedule_evictions: index + .schedule_retention + .borrow() + .as_ref() + .map(|s| s.schedule_evictions()) + .unwrap_or(0), + retention_unknown: index + .schedule_retention + .borrow() + .as_ref() + .map(|s| s.retention_unknown()) + .unwrap_or(0), peak_rss_bytes: peak_rss_vhwm_bytes(), } } @@ -6130,6 +6834,8 @@ fn retention_snapshot_peak( .max(b.ownership_diag_cache_entries), intern_table_entries: a.intern_table_entries.max(b.intern_table_entries), typed_cache_evictions: a.typed_cache_evictions.max(b.typed_cache_evictions), + schedule_evictions: a.schedule_evictions.max(b.schedule_evictions), + retention_unknown: a.retention_unknown.max(b.retention_unknown), peak_rss_bytes: match (a.peak_rss_bytes, b.peak_rss_bytes) { (Some(x), Some(y)) => Some(x.max(y)), (Some(x), None) => Some(x), @@ -6172,12 +6878,15 @@ fn emit_floor_drain_receipt( eprintln!( "[floor-drain] receipt: groups={total_groups} \ typed_cache_peak={} parse_cache_peak={} resolved_memo_peak={} \ - intern_table_peak={} evictions={} peak_rss={} cap_entries={}", + intern_table_peak={} evictions={} schedule_evictions={} retention_unknown={} \ + peak_rss={} cap_entries={}", peaks.typed_module_cache_entries, peaks.parse_cache_entries, peaks.resolved_graph_memo_entries, peaks.intern_table_entries, peaks.typed_cache_evictions, + peaks.schedule_evictions, + peaks.retention_unknown, peaks .peak_rss_bytes .map(|b| b.to_string()) @@ -7541,6 +8250,18 @@ fn reconcile_with_typed_cache( }; let cached = index_get_typed(index, &typed_key)?; let was_cache_hit = cached.is_some(); + // Record this module's cache keys with the armed schedule retention + // (idempotent; hit or miss) so its state can be dropped exactly when no + // remaining scheduled entry reaches it. Keyed by `decl_file` — the same + // repo-relative path form the arming refcount uses (import_closure_live_ + // paths_with_facts). `span.file` is the raw key the parse / normalize-diag + // / ownership-diag / source-hash caches use. + index_record_schedule_module( + index, + &decl_file, + &typed_key, + &resolved.module.span.file, + ); let parent_diags = if was_cache_hit { Rc::new(im::Vector::new()) } else { @@ -8839,6 +9560,74 @@ pub fn run_claim_measured( (outcome, receipt) } +/// Single-binary claim execution (v1-run-stability M2 companion, Deliverable 2): run a +/// batch of claims IN-PROCESS rather than spawning a `claim_batch` child (the +/// `tools.host_prelude.run_gunbc_claims` transport). Claims are grouped by entry so +/// each closure resolves exactly once — the pooled property claim_batch's +/// one-child-per-call already had — and every claim keeps `run_claim_measured`'s +/// per-witness discipline (subject key, eval deadline, the operator 5 s fast-lane +/// law). The declared `execution_mode` threads through unchanged: an in-process claim +/// keeps EXACTLY its declared effect envelope — it never silently widens into the +/// caller's environment (envelope honesty). +/// +/// This is the vehicle the `run_gunbc_claims_pooled_note` reserved ("the child dies +/// and frees"): folding claims into the long-lived executor is safe ONLY because +/// schedule-derived eviction (this module) now bounds the retention the child used to +/// reclaim by dying. Returns `true` iff every claim passed — the same conjunction +/// claim_batch computes — with a per-claim PASS/FAIL line so the in-process verdict is +/// as legible as the child's. Proven verdict-identical to the spawn path by +/// `claim_in_process_matches_spawn_verdict` (RED control #2). +pub fn run_claims_in_process( + source_roots: &[String], + claims: &[(String, String)], + execution_mode: v1_interpreter::ExecutionMode, +) -> bool { + // Group by entry, preserving first-appearance order (stable PASS/FAIL log). + let mut order: Vec = Vec::new(); + let mut by_entry: std::collections::HashMap> = + std::collections::HashMap::new(); + for (entry, function) in claims { + if !by_entry.contains_key(entry) { + order.push(entry.clone()); + by_entry.insert(entry.clone(), Vec::new()); + } + by_entry + .get_mut(entry) + .expect("entry inserted above") + .push(function.clone()); + } + let mut all_passed = true; + for entry in &order { + let functions = &by_entry[entry]; + let (graph, source_indices) = match resolve_entry_graph(source_roots, entry) { + Ok(pair) => pair, + Err(msg) => { + println!("FAIL ({msg})"); + all_passed = false; + continue; + } + }; + let ctx = make_eval_context(&graph, source_indices, execution_mode); + // Subject identity for the per-witness discipline: entry-derived (this path's + // own subjects; the discovery corpus's content-subject drives a cross-run memo + // this in-process transport does not share). + let closure_subject = format!("in-process-claim:{entry}"); + for function in functions { + let (outcome, _receipt) = run_claim_measured(&ctx, &closure_subject, function); + // Frame exit: the eval memo must not retain values across claims sharing + // this ctx (byte-unbounded, the 20GiB-class kills — same as the gate path). + v1_interpreter::eval_call_memo_frame_exit(&ctx); + if outcome == ClaimOutcome::Pass { + println!("PASS {function}"); + } else { + println!("FAIL {function} ({outcome:?})"); + all_passed = false; + } + } + } + all_passed +} + /// Completion-side budget enforcement: the cooperative deadline polls every 4096 /// eval_expr dispatches, so a witness whose time is spent in few dispatches (native /// builtin-heavy) can finish over budget without ever hitting a poll. A Pass that @@ -14090,6 +14879,9 @@ fn run_discovery_corpus_with_options_inner( let floor_stream = floor_stream_enabled(); return match width_policy { DiscoveryWidthPolicy::Serial => { + // Arm retention over the WHOLE serial schedule (all rows) before the single drain + // call — a shared module stays resident until its last scheduled entry consumes it. + index_arm_schedule_retention(&index, &rows); let summary = run_discovery_rows( &rows, &index, @@ -14192,6 +14984,14 @@ fn run_discovery_corpus_with_options_inner( let total_groups = groups.len(); let mut drain_prev = index_retention_snapshot(&index); let mut drain_peaks = drain_prev; + // Arm retention over the WHOLE batch schedule (every group's rows) ONCE, before + // the inline drain — NOT per group. The drain reuses the one process-shared index + // across all entry-groups, so a shared compiler-core module reached by many + // entries keeps a refcount > 1 and stays resident until its LAST consumer's entry + // completes; only an entry's genuinely-unique tail evicts when that entry finishes. + // Per-group arming instead gave each entry a one-entry schedule (refcount 1 on the + // whole closure), evicting and cold-recomputing the shared core once per entry. + index_arm_schedule_retention(&index, &rows); for (group_idx, group_indices) in groups.into_iter().enumerate() { let group_rows: Vec = group_indices.iter().map(|&i| rows[i].clone()).collect(); @@ -14719,6 +15519,19 @@ fn run_discovery_rows( } // Existence set for the entry_file_touched refuse-vs-answer decision, built once per shard. let module_graph_declared_paths = index.module_graph_facts.declared_repo_paths(); + // Schedule-derived retention is armed by the CALLER over the WHOLE batch schedule + // (Serial: the single call; Adaptive width=1: once before the entry-group loop), so a + // shared module's refcount spans every entry that reaches it and it stays resident until + // its genuinely-last consumer. Arming here (per `run_discovery_rows` call) would hand the + // Adaptive inline drain a ONE-ENTRY schedule per group — refcount 1 on every module, + // evicted the instant its entry finished — collapsing "keep shared state until last use" + // into "cold-recompute the shared closure once per entry" (the entries=1 churn that held + // batch-3 wall over budget while RSS was already bounded). Rows are sorted by entry, so an + // entry's rows are contiguous and, once passed, the entry can never be read again; the + // per-entry completion below decrements against the caller-armed refcount (a no-op when + // unarmed — the plural/shared-store worker path). + // The entry whose per-module state becomes unreachable once `row.entry` moves on. + let mut schedule_prev_entry: Option = None; let mut current_entry: Option = None; let mut current_closure_subject: Option = None; let mut ctx: Option = None; @@ -14747,6 +15560,20 @@ fn run_discovery_rows( ); } for row in rows { + // Schedule-derived eviction: when the entry advances, the previous entry's + // rows are all behind us (rows are sorted by entry), so its per-module state + // can never be read again — drop everything no remaining entry's closure + // reaches. A schedule underflow refuses here (typed, located). + if schedule_prev_entry.as_deref() != Some(row.entry.as_str()) { + if let Some(prev) = schedule_prev_entry.take() { + // `current_closure_subject` still holds the PREVIOUS entry's subject here + // (it is reassigned only in the resolve block below), so it keys the + // previous entry's ResolvedGraph for eviction; None when that entry was + // skip-before-resolved (no graph to drop). + index_schedule_entry_completed(index, &prev, current_closure_subject.as_deref())?; + } + schedule_prev_entry = Some(row.entry.clone()); + } // Applied only: PredictOnly must resolve + run cold and record via the post-resolve // would_skip path (falsifier semantics — docs/plans/affected-set-differential-falsifier.md). if selection == NodeFrontierSelectionMode::Applied && entry_fast_skip.contains(&row.entry) { @@ -14999,6 +15826,10 @@ fn run_discovery_rows( // Per-shard input-size receipt: distinct modules in THIS shard's union closure, counted from the // graphs resolved above rather than from the thread's typecheck-miss counter (see the field doc // on `DiscoverySummary::roster_closure_nodes` for why the counter is not bounded to this window). + // The final entry's rows are done — its state is now unreachable too. + if let Some(prev) = schedule_prev_entry.take() { + index_schedule_entry_completed(index, &prev, current_closure_subject.as_deref())?; + } summary.roster_closure_nodes = closure_modules.len(); Ok(summary) } diff --git a/src/v1/stage0/tests/claim_in_process_equivalence.rs b/src/v1/stage0/tests/claim_in_process_equivalence.rs new file mode 100644 index 00000000000..55364e98931 --- /dev/null +++ b/src/v1/stage0/tests/claim_in_process_equivalence.rs @@ -0,0 +1,115 @@ +//! RED control #2 (v1-run-stability M2, Deliverable 2 — single-binary claim +//! execution): a claim's verdict is IDENTICAL whether it runs in-process +//! (`cli_run::run_claims_in_process`) or via the spawned `claim_batch` child. Proven +//! both directions on the same corpus slice — a passing claim is `true` / exit 0 on +//! both paths; a failing claim is `false` / nonzero on both (the discriminating red). +//! This retires the risk the in-process fold-in of the `run_gunbc_claims` transport +//! carries: folding claims into the executor must not change a single verdict. +#![cfg(unix)] + +use std::path::PathBuf; +use std::process::Command; + +fn workspace_root() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .parent() + .and_then(|p| p.parent()) + .and_then(|p| p.parent()) + .expect("repo root") + .to_path_buf() +} + +fn claim_batch_bin() -> PathBuf { + std::env::var_os("CARGO_BIN_EXE_claim_batch") + .map(PathBuf::from) + .unwrap_or_else(|| { + workspace_root().join( + std::env::var("PROFILE") + .map(|p| format!("target/{p}/claim_batch")) + .unwrap_or_else(|_| "target/debug/claim_batch".to_string()), + ) + }) +} + +/// Write a tiny probe corpus under the workspace's `target/` (gitignored, and under +/// the workspace root so path normalization accepts it). Returns (source_root_abs, +/// entry_abs, entry_relpath). +fn write_probe_corpus() -> (String, String, String) { + let dir = workspace_root() + .join("target") + .join(format!("claim_d2_probe_{}", std::process::id())); + let _ = std::fs::remove_dir_all(&dir); + std::fs::create_dir_all(&dir).expect("mkdir probe corpus"); + std::fs::write( + dir.join("probe.dag"), + "module claim_d2_probe.probe\n\nfn pass_claim() -> Bool { true }\n\nfn fail_claim() -> Bool { false }\n", + ) + .expect("write probe"); + let root = dir.to_string_lossy().to_string(); + let entry_abs = dir.join("probe.dag").to_string_lossy().to_string(); + let entry_rel = entry_abs + .strip_prefix(&format!("{}/", workspace_root().to_string_lossy())) + .unwrap_or(&entry_abs) + .to_string(); + let root_rel = root + .strip_prefix(&format!("{}/", workspace_root().to_string_lossy())) + .unwrap_or(&root) + .to_string(); + (root_rel, entry_abs, entry_rel) +} + +/// Spawn-path verdict: run one claim through the `claim_batch` child, return whether +/// it passed (exit 0). +fn spawn_verdict(root_rel: &str, entry_rel: &str, function: &str) -> bool { + let bin = claim_batch_bin(); + assert!(bin.exists(), "claim_batch missing at {}", bin.display()); + let status = Command::new(&bin) + .current_dir(workspace_root()) + .args([ + "--source-root", + root_rel, + "--entry", + entry_rel, + "--function", + function, + "--claim-run", + ]) + .status() + .expect("spawn claim_batch"); + status.success() +} + +#[test] +fn claim_in_process_matches_spawn_verdict() { + let (root_rel, entry_abs, entry_rel) = write_probe_corpus(); + + for (function, expected) in [("pass_claim", true), ("fail_claim", false)] { + // In-process path (the new single-binary vehicle). + let in_process = v1_compiler::cli_run::run_claims_in_process( + &[root_rel.clone()], + &[(entry_abs.clone(), function.to_string())], + v1_compiler::v1_interpreter::ExecutionMode::Hermetic, + ); + // Spawn path (the child that folds away). + let spawned = spawn_verdict(&root_rel, &entry_rel, function); + + assert_eq!( + in_process, expected, + "in-process verdict for {function} should be {expected}" + ); + assert_eq!( + spawned, expected, + "spawn verdict for {function} should be {expected}" + ); + assert_eq!( + in_process, spawned, + "in-process and spawn verdicts must be identical for {function}" + ); + } + + let _ = std::fs::remove_dir_all( + workspace_root() + .join("target") + .join(format!("claim_d2_probe_{}", std::process::id())), + ); +} diff --git a/src/v2/compiler/self_host/witness_entry_eligibility_census.dag b/src/v2/compiler/self_host/witness_entry_eligibility_census.dag index 0dd57e8bfa8..2154b282332 100644 --- a/src/v2/compiler/self_host/witness_entry_eligibility_census.dag +++ b/src/v2/compiler/self_host/witness_entry_eligibility_census.dag @@ -36,7 +36,7 @@ data witness_entry_eligibility_census_histogram_path: String = "docs/probes/witn data witness_entry_eligibility_census_carrier_path_dissolve_on: String = "cli_run/emit HAND-RUST rel literals mirror these rows until load-time projection (review 41784); delete mirrors when wired" -data witness_entry_eligibility_census_entry_count: Int = 880 +data witness_entry_eligibility_census_entry_count: Int = 881 data witness_entry_eligibility_census_stamp: String = "2026-07-23T16:10Z" diff --git a/src/v2/test/claim/self_host/witness_entry_eligibility_census_test.dag b/src/v2/test/claim/self_host/witness_entry_eligibility_census_test.dag index 356ba3b3869..e1a060e9c99 100644 --- a/src/v2/test/claim/self_host/witness_entry_eligibility_census_test.dag +++ b/src/v2/test/claim/self_host/witness_entry_eligibility_census_test.dag @@ -12,11 +12,11 @@ import v2.compiler.self_host.witness_bulk_routing { } import v2.std.algebra { length } -data witness_entry_eligibility_census_test_note: String = "Census receipt: full witness_layer_roots roster (880 entry closures; floor >=600 via witness_entry_eligibility_census_meets_floor) strictly exceeds the 16-entry stratified sample. Discovery exclusions do not shrink the census carrier — explicit-roster grains (execution/, long/, etc.) still need leg rows. ROADMAP 2a 744 totality is the bulk-flip dissolve trigger, not this Lane B landing witness. COUNT 876 -> 880 (CI floor endgame, 2026-07-23): +1 for cheap_gate_pool_test.dag (this PR) AND +3 healing main's latent census drift — main declared 876 while its live find was 879, undetected because affected-set selection skips this witness on PRs that do not touch its closure; this plumbing PR's affected set is the first to run it against the drifted tree. The count lives in four hand-synced copies (this literal, the note, witness_entry_eligibility_census_entry_count, the committed TSV rows) — a §3 parallel-representation the emit transport reconciles at regen but no CI witness walls between regens; restructuring is main's carrier, out of this PR's scope." +data witness_entry_eligibility_census_test_note: String = "Census receipt: full witness_layer_roots roster (881 entry closures; floor >=600 via witness_entry_eligibility_census_meets_floor) strictly exceeds the 16-entry stratified sample. Discovery exclusions do not shrink the census carrier — explicit-roster grains (execution/, long/, etc.) still need leg rows. ROADMAP 2a 744 totality is the bulk-flip dissolve trigger, not this Lane B landing witness. COUNT 876 -> 880 (CI floor endgame, 2026-07-23): +1 for cheap_gate_pool_test.dag (this PR) AND +3 healing main's latent census drift — main declared 876 while its live find was 879, undetected because affected-set selection skips this witness on PRs that do not touch its closure; this plumbing PR's affected set is the first to run it against the drifted tree. The count lives in four hand-synced copies (this literal, the note, witness_entry_eligibility_census_entry_count, the committed TSV rows) — a §3 parallel-representation the emit transport reconciles at regen but no CI witness walls between regens; restructuring is main's carrier, out of this PR's scope. COUNT 880 -> 881 (schedule-retention M2, 2026-07-24): +1 for executor_schedule_retention_test.dag, this PR's new in-corpus witness; the test literal and note were the two hand-synced copies the regen transport does not touch, and this PR's affected set is the first to run this witness against the bumped module constant." test fn witness_entry_eligibility_census_count_holds() -> Bool { witness_entry_eligibility_census_meets_floor() - && witness_entry_eligibility_census_entry_count == 880 + && witness_entry_eligibility_census_entry_count == 881 && witness_entry_eligibility_census_entry_count > witness_bulk_entry_count_expected && length(xs: witness_bulk_routing_sample_roster) == witness_bulk_entry_count_expected }