diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index eec1312b59f..c84a6ccb2a3 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -1265,7 +1265,12 @@ fn report_wave_admission_outcome( eprintln!("required-ci: namespace-wave-admission NotEvaluated — {reason}"); Some("namespace-wave-admission (NotEvaluated)".to_string()) } - nwa::WaveAdmissionOutcome::Adjudicated { base, head, report } => { + nwa::WaveAdmissionOutcome::Adjudicated { + base, + head, + report, + roster_touched, + } => { let p = &report.population; eprintln!( "required-ci: namespace-wave-admission base={base} head={head} \ @@ -1289,11 +1294,23 @@ fn report_wave_admission_outcome( for stale in &report.stale_admissions { eprintln!("required-ci: namespace-wave-admission STALE ADMISSION {stale}"); } + for consumed in &report.consumed_admissions { + eprintln!("required-ci: namespace-wave-admission CONSUMED ADMISSION {consumed}"); + } let unadjudicated = nwa::report_unadjudicated(report); - // A STALE ADMISSION REFUSES TOO. A row that matches no delta is a permission - // standing over nothing, and leaving it means the roster stops being a fact about - // the corpus and becomes a list someone forgot to prune. - if unadjudicated.is_empty() && report.stale_admissions.is_empty() { + // AN UNMATCHED ADMISSION REFUSES. A row provable against neither side is a + // permission standing over nothing — author error, and leaving it means the roster + // stops being a fact about the corpus. + // + // A CONSUMED ADMISSION REFUSES ONLY THE ROSTER'S OWN PATH. Its relocation already + // holds at the base (a positive proof, printed above), so for an unrelated run it is + // an inert typed receipt; billing its cleanup to that run was the externalized + // degradation eight dissolution PRs paid for. The deletion is due — and enforced — + // on the first change that touches the roster file itself, which every future + // relocation PR does by construction. The window is honest: consumed rows persist, + // visible in every run's receipts, until the roster's next touch. + let consumed_due = *roster_touched && !report.consumed_admissions.is_empty(); + if unadjudicated.is_empty() && report.stale_admissions.is_empty() && !consumed_due { eprintln!( "required-ci: namespace-wave-admission ADMITTED — every delta is \ auto-admitted or named by a transition admission" @@ -1301,9 +1318,16 @@ fn report_wave_admission_outcome( return None; } Some(format!( - "namespace-wave-admission ({} unadjudicated delta(s), {} stale admission(s))", + "namespace-wave-admission ({} unadjudicated delta(s), {} stale admission(s), {} \ + consumed admission(s){})", unadjudicated.len(), - report.stale_admissions.len() + report.stale_admissions.len(), + report.consumed_admissions.len(), + if consumed_due { + " due for deletion on this roster-touching change" + } else { + "" + } )) } } diff --git a/src/v1/stage0/src/namespace_wave_admission.rs b/src/v1/stage0/src/namespace_wave_admission.rs index d0ea3011442..92a18466c91 100644 --- a/src/v1/stage0/src/namespace_wave_admission.rs +++ b/src/v1/stage0/src/namespace_wave_admission.rs @@ -244,6 +244,13 @@ pub enum AdmissionSubject { module: &'static str, in_declaration: &'static str, spelling: &'static str, + /// Where the relocated spelling now resolves — the module the admission's own PR moved + /// the name TO. Not consulted by delta matching (the delta subject carries no target); + /// it is the referent of the CONSUMPTION proof: after the admitting PR merges, the base + /// itself binds the spelling to exactly this module, which is the positive, decidable + /// fact that separates a consumed row from an author-error row. A row that cannot name + /// where its name went is not an admission of a relocation. + target: &'static str, }, } @@ -261,6 +268,7 @@ pub fn admission_subject_matches(pattern: &AdmissionSubject, subject: &DeltaSubj module, in_declaration, spelling, + target: _, }, DeltaSubject::Binding { module: observed_module, @@ -285,7 +293,8 @@ pub fn admission_subject_render(subject: &AdmissionSubject) -> String { module, in_declaration, spelling, - } => format!("binding {module}::{in_declaration} `{spelling}`"), + target, + } => format!("binding {module}::{in_declaration} `{spelling}` -> {target}"), } } @@ -473,6 +482,13 @@ pub struct WaveAdmissionReport { pub deltas: Vec, /// Admission rows that matched no delta in this run. pub stale_admissions: Vec, + /// Rows whose admitted relocation the BASE already satisfies — consumed by their own merge. + /// Typed receipts, never refusals for an unrelated run: the deletion obligation they carry + /// stands on the roster's own next touch (see the executor's roster-touched arm). Entered + /// only on the POSITIVE proof `admission_consumed_at_base`, never as the else-arm of "did + /// not match a delta" — a row provable against neither side stays an UnmatchedAdmission + /// refusal in `stale_admissions`. + pub consumed_admissions: Vec, } /// The wall's verdict: every delta is either auto-admitted or named by an admission. @@ -874,24 +890,85 @@ pub fn adjudicate( } } } - let stale_admissions = admissions - .iter() - .enumerate() - .filter(|(i, _)| !used.contains(i)) - .map(|(_, a)| { - format!( + // ── THE UNUSED-ROW SPLIT ── + // + // Consumed-by-merge and author-error were one refusal for eight roster generations, and the + // conflation billed the cleanup to bystanders: a row is REQUIRED at instant N (its own PR's + // CI) and poisonous at instant N+1 (everyone else's), because after the squash-merge base and + // head both carry the relocation and the row can never match a delta again. Eight dissolution + // PRs (#9797 the seventh, #9820 the eighth) each spent hours of unrelated-lane red as the + // roster's garbage collector — externalized degradation (DESIGN §5). + // + // The two states are decidable apart, so this is a wall, not a ratchet: a consumed row's + // admitted relocation ALREADY HOLDS AT THE BASE (`admission_consumed_at_base`, a positive + // check against the base index), while an author-error row is provable against neither side. + // Only the proven arm is typed ConsumedByMerge; everything else unused still refuses as an + // UnmatchedAdmission. The consumed arm does not widen: it is unreachable by fallthrough. + // + // RETIRED BY: admissions bound to the delta content they admit, adjudicated per run and never + // resident on main — the capability that makes a stale-able row unwritable. Until that + // carrier exists, consumed rows persist as typed receipts and their deletion is enforced on + // the roster file's own next touch. + let mut stale_admissions = Vec::new(); + let mut consumed_admissions = Vec::new(); + for (i, a) in admissions.iter().enumerate() { + if used.contains(&i) { + continue; + } + if admission_consumed_at_base(a, base, &base_membership) { + consumed_admissions.push(format!( + "{} ({} {}) already satisfied at the base — consumed by its own merge; deletion \ + is owed on the roster's next touch", + a.label, + disposition_label(a.disposition), + admission_subject_render(&a.subject) + )); + } else { + stale_admissions.push(format!( "{} ({} {}) matches no delta in this run", a.label, disposition_label(a.disposition), admission_subject_render(&a.subject) - ) - }) - .collect(); + )); + } + } WaveAdmissionReport { population, deltas, stale_admissions, + consumed_admissions, + } +} + +/// The POSITIVE consumption proof: the base itself already satisfies the admitted relocation. +/// +/// Binding rows: the base binds (module, in_declaration, spelling) to EXACTLY the admitted +/// target — a singleton set equal to it, not merely containing it. Membership rows: the base +/// module's direct membership already carries the target. Anything less provable is not +/// consumption; the caller refuses it as an UnmatchedAdmission. +fn admission_consumed_at_base( + a: &TransitionAdmission, + base: &DeclarationIndex, + base_membership: &BTreeMap>, +) -> bool { + match &a.subject { + AdmissionSubject::Membership { module, target } => base_membership + .get(*module) + .is_some_and(|members| members.contains(*target)), + AdmissionSubject::Binding { + module, + in_declaration, + spelling, + target, + } => { + let Some(record) = index_get(base, module) else { + return false; + }; + let rows = binding_rows(base, record); + rows.get(&((*in_declaration).to_string(), (*spelling).to_string())) + .is_some_and(|set| set.len() == 1 && set.contains(*target)) + } } } @@ -1085,9 +1162,19 @@ pub enum WaveAdmissionOutcome { base: String, head: String, report: WaveAdmissionReport, + /// Whether this run's diff touches the admission roster's own source file. Consumed + /// rows are inert receipts for every other run; on this path their deletion is DUE, and + /// the executor refuses until the touching change removes them. This is what moves the + /// cleanup bill from bystanders to the roster: the next relocation PR by construction + /// touches this file and therefore cannot land while consumed rows stand. + roster_touched: bool, }, } +/// The roster's own source path, as the diff names it — the subject of the consumed-row +/// deletion obligation. +pub const ADMISSION_ROSTER_REL_PATH: &str = "src/v1/stage0/src/namespace_wave_admission.rs"; + /// Run git in the workspace and return stdout with TRAILING whitespace removed, or a refusal /// naming the command. /// @@ -1295,6 +1382,12 @@ pub fn run_required_wave_admission( } } + let roster_touched = head_touched.iter().any(|p| p == ADMISSION_ROSTER_REL_PATH); let report = adjudicate(&base_index, head_index, NAMESPACE_TRANSITION_ADMISSIONS); - Ok(WaveAdmissionOutcome::Adjudicated { base, head, report }) + Ok(WaveAdmissionOutcome::Adjudicated { + base, + head, + report, + roster_touched, + }) } diff --git a/src/v1/stage0/tests/namespace_wave_admission.rs b/src/v1/stage0/tests/namespace_wave_admission.rs index 8ab59c6f0cf..9d848ee1d3f 100644 --- a/src/v1/stage0/tests/namespace_wave_admission.rs +++ b/src/v1/stage0/tests/namespace_wave_admission.rs @@ -435,6 +435,7 @@ fn an_exact_transition_admission_admits_that_delta_and_only_that_delta() { module: "probe.consumer", in_declaration: "use_it", spelling: "widget", + target: "probe.other", }, disposition: NamespaceDeltaDisposition::TargetChanged, }]; @@ -485,6 +486,7 @@ const AUTHORED_LIKE_PRODUCTION: &[TransitionAdmission] = &[TransitionAdmission { module: "probe.consumer", in_declaration: "use_it", spelling: "widget", + target: "probe.other", }, disposition: NamespaceDeltaDisposition::TargetChanged, }]; @@ -555,6 +557,7 @@ fn a_row_naming_the_empty_module_refuses_rather_than_admitting_silently() { module: "", in_declaration: "", spelling: "", + target: "", }, disposition: NamespaceDeltaDisposition::TargetChanged, }]; @@ -595,6 +598,7 @@ fn an_admission_naming_a_different_subject_does_not_admit_and_reports_stale() { module: "probe.consumer", in_declaration: "use_it", spelling: "gadget", + target: "probe.other", }, disposition: NamespaceDeltaDisposition::TargetChanged, }]; @@ -1605,3 +1609,179 @@ fn deleting_a_type_a_variant_payload_field_still_names_is_still_unresolvedness() report.deltas ); } + +// ── THE CONSUMED/UNMATCHED SPLIT (the eighth-dissolution class made a wall) ── +// +// Eight roster generations conflated consumed-by-merge with author-error in one stale refusal, +// billing the cleanup to whichever unrelated PR pushed next. The split's evidence is the three +// arms below: the RED (an unmatched row still refuses, and specifically does NOT acquire an +// expiry), the positive control (a provably consumed row is typed and refuses nothing), and the +// discriminator (one run holding both rows lands exactly one in each vec — two arms that agree +// on every tested input are one arm). + +/// THE RED, run against the split itself: a row provable against neither side must refuse as an +/// UnmatchedAdmission. The revert arm is the second assertion — under the wrong implementation +/// (ConsumedByMerge as the else-arm of "matched no delta"), this row would land in +/// `consumed_admissions` and vanish from `stale_admissions`, so the pair of assertions +/// discriminates on the split and not on anything beneath it. +#[test] +fn an_unmatched_row_refuses_and_is_never_typed_consumed() { + let sides = [ + ("home.dag", HOME), + ("other.dag", OTHER), + ("consumer.dag", CONSUMER_IMPORTS_HOME), + ]; + let admissions = [TransitionAdmission { + label: "matches-nothing-anywhere", + subject: AdmissionSubject::Binding { + module: "probe.consumer", + in_declaration: "use_it", + spelling: "gadget", + target: "probe.other", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }]; + let report = compare_with("unmatched_never_consumed", &sides, &sides, &admissions); + assert!( + report + .stale_admissions + .iter() + .any(|s| s.contains("matches-nothing-anywhere")), + "an author-error row must refuse as an UnmatchedAdmission: {:?}", + report.stale_admissions + ); + assert!( + report.consumed_admissions.is_empty(), + "the consumed arm must be unreachable by fallthrough — a row provable against neither \ + side acquired an expiry: {:?}", + report.consumed_admissions + ); +} + +/// THE POSITIVE CONTROL: the base already binds the spelling to exactly the admitted target +/// (the relocation merged), so the row is typed ConsumedByMerge and refuses nothing. +#[test] +fn a_consumed_row_is_typed_and_does_not_red_an_unrelated_run() { + let sides = [ + ("home.dag", HOME), + ("other.dag", OTHER), + ("consumer.dag", CONSUMER_IMPORTS_OTHER), + ]; + let report = compare_with( + "consumed_row_inert", + &sides, + &sides, + AUTHORED_LIKE_PRODUCTION, + ); + assert!( + report + .consumed_admissions + .iter() + .any(|c| c.contains("authored-in-a-const")), + "a row whose relocation the base already satisfies must be typed consumed: stale={:?} \ + consumed={:?}", + report.stale_admissions, + report.consumed_admissions + ); + assert!( + report.stale_admissions.is_empty(), + "a consumed row must not also refuse: {:?}", + report.stale_admissions + ); + assert!( + report_unadjudicated(&report).is_empty(), + "the unrelated run itself must stay admitted" + ); +} + +/// THE DISCRIMINATOR: one run holding a consumed row AND an unmatched row must land exactly one +/// in each vec. A split whose arms cannot be separated on one input is one arm. +#[test] +fn one_run_separates_a_consumed_row_from_an_unmatched_one() { + let sides = [ + ("home.dag", HOME), + ("other.dag", OTHER), + ("consumer.dag", CONSUMER_IMPORTS_OTHER), + ]; + let admissions = [ + TransitionAdmission { + label: "consumed-here", + subject: AdmissionSubject::Binding { + module: "probe.consumer", + in_declaration: "use_it", + spelling: "widget", + target: "probe.other", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "unmatched-here", + subject: AdmissionSubject::Binding { + module: "probe.consumer", + in_declaration: "use_it", + spelling: "gadget", + target: "probe.other", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + ]; + let report = compare_with("split_discriminator", &sides, &sides, &admissions); + assert_eq!( + report + .consumed_admissions + .iter() + .filter(|c| c.contains("consumed-here")) + .count(), + 1, + "consumed={:?}", + report.consumed_admissions + ); + assert_eq!( + report + .stale_admissions + .iter() + .filter(|s| s.contains("unmatched-here")) + .count(), + 1, + "stale={:?}", + report.stale_admissions + ); + assert!( + !report + .consumed_admissions + .iter() + .any(|c| c.contains("unmatched-here")), + "the unmatched row leaked into the consumed arm: {:?}", + report.consumed_admissions + ); +} + +/// A row whose spelling the base binds AMBIGUOUSLY (two declarers) is not provably consumed — +/// the singleton-set requirement is load-bearing, not decoration. +#[test] +fn an_ambiguous_base_binding_is_not_consumption() { + let sides = [ + ("home.dag", HOME), + ("other.dag", OTHER), + ("consumer.dag", CONSUMER_IMPORTS_BOTH), + ]; + let report = compare_with( + "ambiguous_not_consumed", + &sides, + &sides, + AUTHORED_LIKE_PRODUCTION, + ); + assert!( + report.consumed_admissions.is_empty(), + "an ambiguous base binding must not prove consumption: {:?}", + report.consumed_admissions + ); + assert!( + report + .stale_admissions + .iter() + .any(|s| s.contains("authored-in-a-const")), + "the unprovable row must still refuse: {:?}", + report.stale_admissions + ); +}