From cbe9194d9ed2fa42465ebfd25c0f8c0987927415 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 29 Aug 2026 17:40:40 +0000 Subject: [PATCH 1/7] The floor's projection joins every DECLARED witness identity to exactly one disposition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The partition over the site projection was a COUNT equality — offered == routed + declined_long + declined_fixture + declined_outside_gate + declined_cost_debt — over a denominator that had itself already narrowed. DESIGN §5 names both halves: completeness is an identity join, not a count equality; and a population removed before the partition is one the partition cannot speak for. Three changes, one seam: 1. THE UNIVERSE IS THE DECLARED POPULATION. Preparation drops modules two ways — the exclusion substrings, and (since the 2026-08-29 gate cut) every module the gate closure does not reach — and a witness declared in a dropped module was neither planned nor declined. It now carries a disposition row, in the authority that already existed: DeclinedDiscoveryExcluded { matched_substring } and DeclinedOutsideGateClosure. The closure arm is kept distinct from DeclinedOutsideRequiredGate because they are removed by different mechanisms, restored by different triggers, and differ by two orders of magnitude — the closure population is the subject of the §4b rung drop "Required gate reduced to the compiler floor", and one label over both would report it as a rounding error on a nearby count. 2. THE CHECK IS AN IDENTITY JOIN. FloorDispositionJoinInexact reconciles the declared identities against the rows they produced and names the offending identities in three sets, through the SAME function the terminal ledger join uses (reconcile_identity_population, generalized from reconcile_terminal_ledger to take identities rather than one seam's row type). Duplicate detection moves from the planned subset to the whole declared population: a duplicate whose first site declined used to pass unnoticed. The four decline counters are derived from the rows instead of accumulated beside them. 3. THE ARTIFACT CARRIES TWO AXES, NEVER FOLDED. The disposition TSV gains an outcome column joined from the terminal ledger through claim_disposition; an identity that never ran reads not_executed, which is a statement rather than a blank. Evidence: the calibration pair is enrolled beside the terminal-ledger one — a population that drops one identity and duplicates another, over which every count of the deleted form is still exactly equal, and the join names both. Rung honesty: that suite is the local Rust suite, removed from CI 2026-07-11, so the executing evidence on a push is the floor's own run, whose announcement now carries declared= beside offered=. Found on the way: gunbc.discovery_census claims twice in prose that a new RequiredFloorDisposition arm must fail to compile in its wildcard-free matches. DeclinedOutsideRequiredGate had already been added with neither match acquiring an arm and nothing refused — its witness sits outside the gate closure, so no executing path typechecks it. The arms are added and the claim is restated at its honest rung with its trigger. Not built, and named as this join's next-rung triggers rather than improvised: the semantic producer axis (no authority maps a witness to its producer) and the Rust #[ignore] roster (a different universe with no roster authority). → docs/plans/witness-execution-closure.md Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WmatNuCFnqTdE2KoiwEcm4 --- dag/gunbc/discovery_census.dag | 78 +++++- .../claim/discovery_census_witness_test.dag | 26 ++ docs/plans/witness-execution-closure.md | 71 +++++ src/v1/stage0/src/bin/claim_executor.rs | 11 +- src/v1/stage0/src/cli_run.rs | 263 ++++++++++++++++-- .../src/cli_run/required_floor_runner.rs | 231 +++++++++++---- src/v2/workflow/floor_terminal_ledger.dag | 2 +- src/v2/workflow/required_floor.dag | 29 +- 8 files changed, 617 insertions(+), 94 deletions(-) diff --git a/dag/gunbc/discovery_census.dag b/dag/gunbc/discovery_census.dag index ea13c1055ba..ead4a89aaad 100644 --- a/dag/gunbc/discovery_census.dag +++ b/dag/gunbc/discovery_census.dag @@ -13,6 +13,7 @@ import gunbc.build_target { import v2.workflow.required_floor { RequiredFloorDisposition, Planned, DeclinedLongModule, DeclinedFixtureMember, DeclinedCostDebt, + DeclinedOutsideRequiredGate, DeclinedOutsideGateClosure, DeclinedDiscoveryExcluded, required_floor_site_disposition, } import v2.std.live_tree { LiveTreeDisposition } @@ -256,6 +257,12 @@ fn census_partition_step(acc: CensusPartition, row: CensusRow) -> CensusPartitio CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) } DeclinedCostDebt => CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) } + DeclinedOutsideRequiredGate => + CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) } + DeclinedOutsideGateClosure => + CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) } + DeclinedDiscoveryExcluded { matched_substring: _ } => + CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) } } } @@ -315,12 +322,25 @@ fn required_aggregate_from_census(census: SiteCensus) -> RequiredAggregateDeriva // written out rather than counted as "planned and everything else": a new decline reason // silently joining the non-planned remainder would leave the census reporting a population it no // longer distinguishes. +// THE "MUST FAIL TO COMPILE" CLAIM ABOVE WAS FALSE WHEN THIS ROW WAS WRITTEN, and the correction +// is recorded here rather than silently applied. `DeclinedOutsideRequiredGate` was added to +// `RequiredFloorDisposition` and NEITHER of this module's two wildcard-free matches acquired an +// arm for it; nothing refused, so the census counted a population it no longer distinguished for +// as long as that arm existed — exactly the outcome the paragraph promises is unwritable. The +// three arms below close that gap and the missing one, but the claim is now stated at its honest +// rung: match exhaustiveness over an imported coproduct is NOT enforced for this module on any +// executing path, because its own witness sits outside the required gate's import closure. NEXT +// TRIGGER: the required gate reaching this module (or any executing consumer typechecking it), +// at which point the omission fails the build instead of being found by a reader. type CensusCounts { offered: Int planned: Int declined_long_module: Int declined_fixture_member: Int declined_cost_debt: Int + declined_outside_required_gate: Int + declined_outside_gate_closure: Int + declined_discovery_excluded: Int } fn census_counts_zero() -> CensusCounts { @@ -329,7 +349,10 @@ fn census_counts_zero() -> CensusCounts { planned: 0, declined_long_module: 0, declined_fixture_member: 0, - declined_cost_debt: 0 + declined_cost_debt: 0, + declined_outside_required_gate: 0, + declined_outside_gate_closure: 0, + declined_discovery_excluded: 0 } } @@ -341,7 +364,10 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu planned: counts.planned + 1, declined_long_module: counts.declined_long_module, declined_fixture_member: counts.declined_fixture_member, - declined_cost_debt: counts.declined_cost_debt + declined_cost_debt: counts.declined_cost_debt, + declined_outside_required_gate: counts.declined_outside_required_gate, + declined_outside_gate_closure: counts.declined_outside_gate_closure, + declined_discovery_excluded: counts.declined_discovery_excluded } DeclinedLongModule { matched_prefix: _ } => CensusCounts { @@ -349,7 +375,10 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu planned: counts.planned, declined_long_module: counts.declined_long_module + 1, declined_fixture_member: counts.declined_fixture_member, - declined_cost_debt: counts.declined_cost_debt + declined_cost_debt: counts.declined_cost_debt, + declined_outside_required_gate: counts.declined_outside_required_gate, + declined_outside_gate_closure: counts.declined_outside_gate_closure, + declined_discovery_excluded: counts.declined_discovery_excluded } DeclinedFixtureMember { matched_prefix: _ } => CensusCounts { @@ -357,7 +386,10 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu planned: counts.planned, declined_long_module: counts.declined_long_module, declined_fixture_member: counts.declined_fixture_member + 1, - declined_cost_debt: counts.declined_cost_debt + declined_cost_debt: counts.declined_cost_debt, + declined_outside_required_gate: counts.declined_outside_required_gate, + declined_outside_gate_closure: counts.declined_outside_gate_closure, + declined_discovery_excluded: counts.declined_discovery_excluded } DeclinedCostDebt => CensusCounts { @@ -365,7 +397,43 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu planned: counts.planned, declined_long_module: counts.declined_long_module, declined_fixture_member: counts.declined_fixture_member, - declined_cost_debt: counts.declined_cost_debt + 1 + declined_cost_debt: counts.declined_cost_debt + 1, + declined_outside_required_gate: counts.declined_outside_required_gate, + declined_outside_gate_closure: counts.declined_outside_gate_closure, + declined_discovery_excluded: counts.declined_discovery_excluded + } + DeclinedOutsideRequiredGate => + CensusCounts { + offered: counts.offered + 1, + planned: counts.planned, + declined_long_module: counts.declined_long_module, + declined_fixture_member: counts.declined_fixture_member, + declined_cost_debt: counts.declined_cost_debt, + declined_outside_required_gate: counts.declined_outside_required_gate + 1, + declined_outside_gate_closure: counts.declined_outside_gate_closure, + declined_discovery_excluded: counts.declined_discovery_excluded + } + DeclinedOutsideGateClosure => + CensusCounts { + offered: counts.offered + 1, + planned: counts.planned, + declined_long_module: counts.declined_long_module, + declined_fixture_member: counts.declined_fixture_member, + declined_cost_debt: counts.declined_cost_debt, + declined_outside_required_gate: counts.declined_outside_required_gate, + declined_outside_gate_closure: counts.declined_outside_gate_closure + 1, + declined_discovery_excluded: counts.declined_discovery_excluded + } + DeclinedDiscoveryExcluded { matched_substring: _ } => + CensusCounts { + offered: counts.offered + 1, + planned: counts.planned, + declined_long_module: counts.declined_long_module, + declined_fixture_member: counts.declined_fixture_member, + declined_cost_debt: counts.declined_cost_debt, + declined_outside_required_gate: counts.declined_outside_required_gate, + declined_outside_gate_closure: counts.declined_outside_gate_closure, + declined_discovery_excluded: counts.declined_discovery_excluded + 1 } } } diff --git a/dag/test/claim/discovery_census_witness_test.dag b/dag/test/claim/discovery_census_witness_test.dag index 50fcbd93854..89869efb092 100644 --- a/dag/test/claim/discovery_census_witness_test.dag +++ b/dag/test/claim/discovery_census_witness_test.dag @@ -26,9 +26,15 @@ import gunbc.discovery_census { RequiredAggregateDerivation, RequiredAggregateDerived, RequiredAggregateUnderivable, required_aggregate_from_census, } +// THE TWO PREPARATION-STAGE DECLINES ARE IMPORTED AND ANSWERED `false` EVERYWHERE BELOW. +// `required_floor_site_disposition` can never RETURN `DeclinedOutsideGateClosure` or +// `DeclinedDiscoveryExcluded`: both are decided before a module reaches the prepared subject, +// from facts a module NAME cannot carry. So their arms here are a claim about that +// unreachability, not an omission padded out to satisfy exhaustiveness. import v2.workflow.required_floor { RequiredFloorDisposition, Planned, DeclinedLongModule, DeclinedFixtureMember, DeclinedOutsideRequiredGate, DeclinedCostDebt, + DeclinedOutsideGateClosure, DeclinedDiscoveryExcluded, required_floor_site_disposition, } import v2.workflow.floor_terminal_ledger { ClaimDisposition, Passed } @@ -207,6 +213,8 @@ test fn w_fixture_home_declines_with_its_matched_prefix() -> Bool { DeclinedLongModule { matched_prefix: _ } => false DeclinedOutsideRequiredGate => false DeclinedCostDebt => false + DeclinedOutsideGateClosure => false + DeclinedDiscoveryExcluded { matched_substring: _ } => false } } @@ -220,6 +228,8 @@ test fn w_long_home_module_declines_with_its_matched_prefix() -> Bool { DeclinedFixtureMember { matched_prefix: _ } => false DeclinedOutsideRequiredGate => false DeclinedCostDebt => false + DeclinedOutsideGateClosure => false + DeclinedDiscoveryExcluded { matched_substring: _ } => false } } @@ -236,6 +246,8 @@ test fn w_long_home_is_a_prefix_not_a_substring() -> Bool { DeclinedFixtureMember { matched_prefix: _ } => false DeclinedOutsideRequiredGate => false DeclinedCostDebt => false + DeclinedOutsideGateClosure => false + DeclinedDiscoveryExcluded { matched_substring: _ } => false } } @@ -249,6 +261,8 @@ test fn w_site_is_planned_when_no_home_matched() -> Bool { DeclinedFixtureMember { matched_prefix: _ } => false DeclinedOutsideRequiredGate => false DeclinedCostDebt => false + DeclinedOutsideGateClosure => false + DeclinedDiscoveryExcluded { matched_substring: _ } => false } } @@ -265,6 +279,8 @@ test fn w_site_outside_the_required_gate_is_declined() -> Bool { DeclinedLongModule { matched_prefix: _ } => false DeclinedFixtureMember { matched_prefix: _ } => false DeclinedCostDebt => false + DeclinedOutsideGateClosure => false + DeclinedDiscoveryExcluded { matched_substring: _ } => false } } @@ -283,10 +299,14 @@ test fn w_counts_partition_the_offered_population() -> Bool { && (counts.declined_fixture_member == 1) && (counts.declined_outside_required_gate == 0) && (counts.declined_cost_debt == 1) + && (counts.declined_outside_gate_closure == 0) + && (counts.declined_discovery_excluded == 0) && (counts.offered == counts.planned + counts.declined_long_module + counts.declined_fixture_member + counts.declined_outside_required_gate + + counts.declined_outside_gate_closure + + counts.declined_discovery_excluded + counts.declined_cost_debt) } @@ -316,6 +336,8 @@ test fn w_rostered_identity_declines_for_cost_debt() -> Bool { identity: "dag.test.claim.lifecycle_survivor_corpus_census.no_raw_lifecycle_string_survivors_remain" ) { DeclinedCostDebt => true + DeclinedOutsideGateClosure => false + DeclinedDiscoveryExcluded { matched_substring: _ } => false Planned => false DeclinedLongModule { matched_prefix: _ } => false DeclinedFixtureMember { matched_prefix: _ } => false @@ -333,6 +355,8 @@ test fn w_unrostered_sibling_in_the_same_module_is_planned() -> Bool { Planned => true DeclinedOutsideRequiredGate => false DeclinedCostDebt => false + DeclinedOutsideGateClosure => false + DeclinedDiscoveryExcluded { matched_substring: _ } => false DeclinedLongModule { matched_prefix: _ } => false DeclinedFixtureMember { matched_prefix: _ } => false } @@ -351,6 +375,8 @@ test fn w_home_decline_outranks_cost_debt() -> Bool { DeclinedLongModule { matched_prefix: p } => p == "test.claim.long." DeclinedOutsideRequiredGate => false DeclinedCostDebt => false + DeclinedOutsideGateClosure => false + DeclinedDiscoveryExcluded { matched_substring: _ } => false Planned => false DeclinedFixtureMember { matched_prefix: _ } => false } diff --git a/docs/plans/witness-execution-closure.md b/docs/plans/witness-execution-closure.md index 5e54b55d954..cc6eff13c40 100644 --- a/docs/plans/witness-execution-closure.md +++ b/docs/plans/witness-execution-closure.md @@ -218,3 +218,74 @@ whereas a route-gapped identity stays in the subject, executes, and reports. Converting those entries into `floor_route_gap` rows is the obvious next step and is deliberately **not** in this change: it should follow the measurement that proves the route-gap mechanism behaves as designed on the population it was built for, not precede it. + +--- + +## The same failure one level up: the projection's denominator (2026-08-29, `nimble-ibex-902`) + +The population above was lost *inside* the projection — discovered, declined, never run. The +sequel is the population lost *before* it: identities that never reached the projection at all, +so no partition over "offered" could speak for them. + +### The two mechanisms that removed them + +`assemble_prepared_subject_closure` drops modules two ways, and a witness declared in a dropped +module was neither planned nor declined: + +- **the exclusion substrings**, whose entry-grain receipt (`collect_deferred_discovery_rows`) + existed but was never joined to the disposition population at identity grain; and +- **the gate closure** introduced by the 2026-08-29 gate cut (§4b rung drop *Required gate + reduced to the compiler floor*). Only modules in the transitive closure of the gate seeds are + prepared, so `declined_outside_required_gate` — which reads two figures — can only ever speak + for modules that *reached* the index. + +### The subject universe, measured + +Counted with the floor's own rule (a column-zero `test fn ` / `test data `) over `dag/` and +`src/v2`: **13,975 distinct declared identities**, in 1,759 files, with **zero** duplicate +identities and **zero** module-name collisions. So the gap between the declared corpus and the +floor's `offered` was never duplication; it was two silent removals. The live figures are the +run's own, not this document's: `required-floor: declared=… offered=… declined_outside_gate_closure=…`. + +### What changed + +1. **The universe is the declared population.** Preparation now emits one + `RequiredFloorDisposition` row for every identity it drops — + `DeclinedOutsideGateClosure` and `DeclinedDiscoveryExcluded { matched_substring }`, two arms + on the authority that already existed, not a second status vocabulary. The gate-closure + population keeps its own arm rather than folding into `DeclinedOutsideRequiredGate`: the two + are removed by different mechanisms, restored by different triggers, and differ by two orders + of magnitude, and the first is the rung drop's subject. +2. **The partition is an identity join, not a count equality.** The old check was + `offered == routed + declined_long + declined_fixture + declined_outside_gate + + declined_cost_debt`, which DESIGN §5 names by shape: green over a projection that drops one + identity and writes another twice, since every count still agrees. It is now the same + reconciliation the terminal ledger uses, through the same function + (`reconcile_identity_population`), refusing as `FloorDispositionJoinInexact` with the offending + identities named. Its calibration pair is enrolled beside the terminal-ledger one. +3. **The counters are derived from the rows** instead of accumulated beside them, and duplicate + detection moved from the *planned* subset to the *whole declared* population — a duplicate + whose first site declined used to pass unnoticed. +4. **The artifact carries two axes, never folded.** The disposition TSV gains an `outcome` + column, joined from the terminal ledger through `claim_disposition`; an identity that never + ran reads `not_executed`, which is a statement rather than a blank. + +### Two axes deliberately NOT built, and what each needs first + +Both were in the commissioning brief and both would have meant *authoring* the authority they +claim to join to (§3), so they are named here as triggers rather than improvised: + +- **semantic producer / retire-with-producer.** No authority in the tree maps a witness identity + to the producer whose behavior it witnesses. Trigger: a modeled producer binding on the witness + carrier itself, at which point the join is a lookup rather than a classification. +- **the Rust `#[ignore]` roster.** A different universe with no roster authority and no identity + grain shared with `.dag` witnesses. Trigger: an enumerated, typed roster of ignored Rust tests + with a stated reason per row — the same shape `floor_cost_debt` already has for its population. + +### One inert wall found on the way + +`gunbc.discovery_census` claims, twice and in prose, that its wildcard-free matches make a new +`RequiredFloorDisposition` arm *fail to compile*. `DeclinedOutsideRequiredGate` had already been +added without either match acquiring an arm, and nothing refused — the module's own witness is +outside the gate closure, so no executing path typechecks it. The arms are added here and the +claim is restated at its honest rung, with the trigger recorded in the module. diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 787282b39ad..210123b5387 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -1171,15 +1171,20 @@ fn report_required_floor_outcome(outcome: &v1_compiler::cli_run::RequiredFloorOu // entry stops the line in `run_required_floor` before this point — so the guarantee is stated // rather than left for a reader to discover it was never claimed. eprintln!( - "required-floor: offered={} routed={} declined_long={} declined_fixture={} \ - declined_outside_required_gate={} — every discovered site is exactly one of these, \ + "required-floor: declared={} offered={} routed={} declined_long={} declined_fixture={} \ + declined_outside_required_gate={} declined_outside_gate_closure={} \ + declined_discovery_excluded={} — every DECLARED witness identity in the tree is exactly \ + one of these, joined at identity grain (FloorDispositionJoinInexact refuses otherwise), \ and no `*_test.dag` entry offered zero sites (BarrenTestSidecar refuses upstream of \ this line)", + outcome.declared_identities, outcome.sites_offered, outcome.claims_planned, outcome.declined_long_module, outcome.declined_fixture_member, - outcome.declined_outside_required_gate + outcome.declined_outside_required_gate, + outcome.declined_outside_gate_closure, + outcome.declined_discovery_excluded ); // WHY route_gap IS NOW SPELLED route_gap_unenrolled, AND WHY route_gap_held JOINS IT HERE. // The old field printed `outcome.route_gap.len()` under the bare name `route_gap` — the diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 63456f529da..91b2e8053a8 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -16276,25 +16276,32 @@ fn hermetic_effect_ground_verdict( /// a control sharing nothing with its subject except a name. Extracting it costs nothing and is /// the difference between a test of the reconciliation and a test of a paraphrase of it. /// -/// Returns (planned-without-terminal, terminal-without-planned, terminal-duplicated). Three sets -/// rather than a first-failure verdict: an omission and a duplicate arrive together and cancel -/// in every count, so reporting only the first found would hide the half that explains it. -pub fn reconcile_terminal_ledger<'a>( - planned: &'a HashSet, - rows: &'a [ClaimTerminalRow], +/// Returns (expected-without-observed, observed-without-expected, observed-duplicated). Three +/// sets rather than a first-failure verdict: an omission and a duplicate arrive together and +/// cancel in every count, so reporting only the first found would hide the half that explains it. +/// +/// IT TAKES IDENTITIES, NOT ROWS, because the floor performs this join at more than one seam and +/// the join is one fact. Downstream it is planned-claim identities against terminal ledger rows; +/// upstream it is the offered witness population against the disposition projection +/// (`run_required_floor`, `FloorDispositionJoinInexact`). A per-seam copy keyed on that seam's +/// row type would be the same loop written twice, drifting independently — so each caller +/// projects its own rows to identities and hands them here. +pub fn reconcile_identity_population<'a>( + expected: &'a HashSet, + observed: impl Iterator, ) -> (Vec<&'a str>, Vec<&'a str>, Vec<&'a str>) { let mut seen: HashMap<&str, usize> = HashMap::new(); - for row in rows { - *seen.entry(row.qualified.as_str()).or_insert(0) += 1; + for identity in observed { + *seen.entry(identity).or_insert(0) += 1; } - let mut missing: Vec<&str> = planned + let mut missing: Vec<&str> = expected .iter() .map(|q| q.as_str()) .filter(|q| !seen.contains_key(q)) .collect(); let mut foreign: Vec<&str> = seen .keys() - .filter(|q| !planned.contains(**q)) + .filter(|q| !expected.contains(**q)) .copied() .collect(); let mut duplicated: Vec<&str> = seen @@ -16335,7 +16342,7 @@ pub fn reconcile_terminal_ledger<'a>( /// not compare them — this file is not generated. The witnesses do not compare them — they /// exercise each side separately, never one against the other. So an arm added, renamed or /// re-meaned on either side leaves the other silently stale, and the seam is exactly the shape -/// this change repaired one grain down: `reconcile_terminal_ledger` was extracted so its test +/// this change repaired one grain down: `reconcile_identity_population` was extracted so its test /// could not be a control that shares only a name with its subject. That rule condemns this seam /// too, and here it is declared debt rather than repaired. /// @@ -16348,7 +16355,7 @@ pub fn reconcile_terminal_ledger<'a>( /// self-emitted v2 claim executor. When the floor's execution is driven by v2 rather than by this /// seed, the producer that holds identity-and-outcome together IS the v2 side, so there is no /// seam to bridge and no second representation to keep in agreement — this struct, -/// `claim_disposition`, `reconcile_terminal_ledger` and the refusal below are deleted whole, and +/// `claim_disposition`, `reconcile_identity_population` and the refusal below are deleted whole, and /// `v2.workflow.floor_terminal_ledger` is left as the sole authority it already claims to be. pub struct ClaimTerminalRow { pub qualified: String, @@ -35651,6 +35658,10 @@ pub struct PreparedRepository { /// Admitted sources carrying zero `test` decls (`test fn` or `test data`). See /// `PreparedSubject::test_decl_free_paths`. pub test_decl_free_paths: Vec, + /// The witness identities preparation DROPPED, each with its disposition. Carried through + /// with the admitted population because the floor's projection is a join over every DECLARED + /// identity: see `PreparedSubject::undiscovered_dispositions`. + pub undiscovered_dispositions: Vec, } /// Shared view of one admitted source. Holds the same `Rc` preparation already @@ -35809,6 +35820,12 @@ pub struct PreparedSubject { pub sources: Vec>, pub inventory: Vec, pub witness_files: Vec, + /// One disposition row per witness identity this preparation DROPPED — excluded by + /// substring, or never reached by the gate closure. Carried beside the admitted population + /// so the floor's projection can be a join over every DECLARED identity rather than over the + /// subset that survived preparation; see the field's producer for why the arms are the + /// admitted population's own. + pub undiscovered_dispositions: Vec, /// Admitted sources carrying ZERO `test` decls — neither `test fn` nor `test data` — by /// repo-relative path. The vocabulary is `floor_discovery_scan_test_decl_names`'s, so this /// population is the wall's own denominator rather than a narrower one that happens to @@ -35865,6 +35882,19 @@ pub fn assemble_prepared_subject_closure( closure: Option<(&MultiEntryIndex, &[String])>, ) -> Result { let full_index = build_module_index(source_roots); + // THE POPULATION THIS PREPARATION DROPS, KEPT AT IDENTITY GRAIN RATHER THAN AS A COUNT. + // + // The gate closure and the exclusion substrings both remove modules from the subject, and a + // witness declared in a removed module is then neither planned NOR declined — it leaves the + // floor's universe one level above the disposition projection, which is exactly the silence + // `docs/plans/witness-execution-closure.md` found the last time a population went missing. + // After the 2026-08-29 gate cut that silence is the majority of the corpus, not an edge: + // `declined_outside_required_gate` can only speak for modules that reached the index. + // + // So preparation records a disposition for every declaration it drops, in the SAME authority + // the admitted population uses (`RequiredFloorDisposition`) — not a second status vocabulary + // — and the floor joins the two into one row per declared identity. + let mut undiscovered_dispositions: Vec = Vec::new(); let index: ModuleSourceIndex = match closure { None => full_index, Some((entry_index, prefixes)) => { @@ -36001,6 +36031,29 @@ pub fn assemble_prepared_subject_closure( full_index.len() - keep.len(), full_index.len() ); + for (module_path, sf) in full_index.iter() { + if keep.contains(module_path) { + continue; + } + let Some(site) = witness_file_from_source(module_path, &sf.path, &sf.content) + else { + continue; + }; + for function in &site.functions { + undiscovered_dispositions.push(RequiredFloorDispositionRow { + identity: format!("{module_path}.{function}"), + // ITS OWN ARM, NOT `DeclinedOutsideRequiredGate`. Both are "not on the + // required path", but they are removed by different mechanisms and only + // one of them is the population the §4b rung drop names: a module the + // GATE CLOSURE never reached was never prepared, never resolved and never + // offered, while `DeclinedOutsideRequiredGate` speaks for a module that + // WAS prepared and whose authored name missed every gate prefix. Folding + // them would put five figures and two figures behind one label, and the + // artifact could no longer show the closure population as a column. + disposition: RequiredFloorDisposition::DeclinedOutsideGateClosure, + }); + } + } full_index .into_iter() .filter(|(m, _)| keep.contains(m)) @@ -36014,10 +36067,25 @@ pub fn assemble_prepared_subject_closure( let mut inventory: Vec = Vec::with_capacity(total); for (module_path, sf) in index.iter() { let p = sf.path.replace('\\', "/"); - if exclude_substrings + if let Some(matched) = exclude_substrings .iter() - .any(|sub| p.contains(sub.as_str()) || module_path.contains(sub.as_str())) + .find(|sub| p.contains(sub.as_str()) || module_path.contains(sub.as_str())) { + // EXCLUDED IS A DISPOSITION, NOT A DISAPPEARANCE. `collect_deferred_discovery_rows` + // already receipts the excluded `*_test.dag` ENTRIES; this records the same removal + // at the grain the population join is keyed on — the qualified identity — so an + // excluded witness is a named row in the projection instead of a subtraction a + // reader has to reconstruct from two artifacts. + if let Some(site) = witness_file_from_source(module_path, &sf.path, &sf.content) { + for function in &site.functions { + undiscovered_dispositions.push(RequiredFloorDispositionRow { + identity: format!("{module_path}.{function}"), + disposition: RequiredFloorDisposition::DeclinedDiscoveryExcluded { + matched_substring: matched.clone(), + }, + }); + } + } continue; } // THE DROP THAT MADE A WALL UNREACHABLE, NOW A RECORDED FACT. @@ -36076,10 +36144,12 @@ pub fn assemble_prepared_subject_closure( test_decl_free_paths.sort(); let subject_digest = subject_digest_for_closure(&sources); let modules_resolved = total - modules_excluded; + undiscovered_dispositions.sort_by(|a, b| a.identity.cmp(&b.identity)); Ok(PreparedSubject { sources, inventory, witness_files, + undiscovered_dispositions, test_decl_free_paths, subject_digest, modules_resolved, @@ -36123,6 +36193,7 @@ pub fn prepare_repository_closure( subject_digest, modules_resolved, modules_excluded, + undiscovered_dispositions, } = subject; let resolved = resolved_graph_from_sources(sources, ResolveTypecheckGate::Strict); let (graph, source_indices) = resolved.map_err(|e| format!("{subject_statement}\n{e}"))?; @@ -36135,6 +36206,7 @@ pub fn prepare_repository_closure( modules_excluded, witness_files, test_decl_free_paths, + undiscovered_dispositions, }, inventory, )) @@ -36779,6 +36851,23 @@ pub enum RequiredFloorDisposition { /// that also declines for a home reason keeps the home decline, so a roster line over it /// surfaces as a STALE row to delete rather than as a withhold that looks legitimate. DeclinedCostDebt, + /// Declined by PREPARATION, before the site was ever offered: the module carries no + /// required-gate prefix and the gate closure — the transitive import/reference closure of + /// the gate seeds — never reached it, so it was not in the prepared subject at all. + /// + /// NOT `DeclinedOutsideRequiredGate`, and the separation is the point. That arm speaks for a + /// module the subject CONTAINED whose authored name missed the prefix roster; this one for a + /// module the subject never held, discovered by re-reading the full index rather than by the + /// site loop. After the 2026-08-29 gate cut this arm is five figures and that one is two, and + /// this arm's population is the subject of the §4b rung drop "Required gate reduced to the + /// compiler floor" — one label over both would report that drop's whole population as a + /// rounding error on a nearby count. + DeclinedOutsideGateClosure, + /// Declined by PREPARATION because the module's path or authored name contains one of the + /// discovery `exclude_substrings`. Carries the substring that matched, so the row names its + /// own remedy. `collect_deferred_discovery_rows` receipts the same removal at ENTRY grain; + /// this is the identity grain the population join is keyed on. + DeclinedDiscoveryExcluded { matched_substring: String }, } /// ONE EXECUTED CLAIM'S MEASURED OCCURRENCE, minted the instant `run_claim_measured` @@ -36918,6 +37007,18 @@ pub struct RequiredFloorOutcome { pub declined_fixture_member: usize, /// Sites whose module matches no `required_gate_prefixes()` row (the static required gate). pub declined_outside_required_gate: usize, + /// EVERY witness identity DECLARED in the tree, not only those the prepared subject offered: + /// `sites_offered` plus the identities preparation dropped. It is the denominator the + /// disposition join runs over, and it is reported beside `sites_offered` rather than + /// replacing it — a subject-relative count and a tree-relative count answer different + /// questions and a reader comparing two runs needs both. + pub declared_identities: usize, + /// Declared identities whose module the gate closure never reached, so preparation never + /// held them. After the 2026-08-29 gate cut this is the largest population in the receipt and + /// it is the subject of the "Required gate reduced to the compiler floor" rung drop. + pub declined_outside_gate_closure: usize, + /// Declared identities excluded from discovery by an `exclude_substrings` match. + pub declined_discovery_excluded: usize, pub claims_planned: usize, pub claims_executed: usize, pub receipt_identities: usize, @@ -37567,8 +37668,23 @@ fn write_required_floor_claim_cost_tsv( fn write_required_floor_disposition_tsv( path: &str, rows: &[RequiredFloorDispositionRow], + terminal: &[ClaimTerminalRow], ) -> Result<(), String> { use std::io::Write; + // TWO AXES, NEVER FOLDED INTO ONE STATUS. The disposition says whether the identity was + // ADMITTED TO EXECUTION and why not; the outcome says what happened to the ones that ran. + // A single column would have to answer "declined" and "failed" in the same alphabet, and the + // first consumer that filtered on it would silently merge a coverage gap with a red — the + // state-space conflation this repository already rosters. So an identity that never ran + // reads `not_executed` in the outcome column, which is a STATEMENT rather than a blank. + // + // The outcome is read through `claim_disposition`, the same projection the terminal ledger + // and the `passed` derivation use, so this artifact cannot disagree with the run's own + // counts about what a row's outcome was. + let outcomes: HashMap<&str, ClaimDisposition> = terminal + .iter() + .map(|row| (row.qualified.as_str(), claim_disposition(row))) + .collect(); let mut file = std::fs::File::create(path) .map_err(|e| format!("write_required_floor_disposition_tsv: create {path}: {e}"))?; let mut planned = 0usize; @@ -37576,6 +37692,8 @@ fn write_required_floor_disposition_tsv( let mut declined_fixture = 0usize; let mut declined_cost_debt = 0usize; let mut declined_outside_gate = 0usize; + let mut declined_gate_closure = 0usize; + let mut declined_discovery_excluded = 0usize; for row in rows { match &row.disposition { RequiredFloorDisposition::Planned => planned += 1, @@ -37583,29 +37701,40 @@ fn write_required_floor_disposition_tsv( RequiredFloorDisposition::DeclinedFixtureMember { .. } => declined_fixture += 1, RequiredFloorDisposition::DeclinedOutsideRequiredGate => declined_outside_gate += 1, RequiredFloorDisposition::DeclinedCostDebt => declined_cost_debt += 1, + RequiredFloorDisposition::DeclinedOutsideGateClosure => declined_gate_closure += 1, + RequiredFloorDisposition::DeclinedDiscoveryExcluded { .. } => { + declined_discovery_excluded += 1 + } } } writeln!( file, "# summary\ttotal={}\tplanned={}\tdeclined_long_module={}\tdeclined_fixture_member={}\ - \tdeclined_outside_required_gate={}\tdeclined_cost_debt={}", + \tdeclined_outside_required_gate={}\tdeclined_outside_gate_closure={}\ + \tdeclined_discovery_excluded={}\tdeclined_cost_debt={}", rows.len(), planned, declined_long, declined_fixture, declined_outside_gate, + declined_gate_closure, + declined_discovery_excluded, declined_cost_debt ) .map_err(|e| format!("write_required_floor_disposition_tsv: write {path}: {e}"))?; - writeln!(file, "identity\tdisposition\tmatched_prefix") + writeln!(file, "identity\tdisposition\tmatched_prefix\toutcome") .map_err(|e| format!("write_required_floor_disposition_tsv: write {path}: {e}"))?; for row in rows { writeln!( file, - "{}\t{}\t{}", + "{}\t{}\t{}\t{}", row.identity.replace(['\t', '\n'], " "), required_floor_disposition_label(&row.disposition), required_floor_disposition_matched_prefix(&row.disposition).replace(['\t', '\n'], " "), + outcomes + .get(row.identity.as_str()) + .map(|d| claim_disposition_wire(*d)) + .unwrap_or("not_executed"), ) .map_err(|e| format!("write_required_floor_disposition_tsv: write {path}: {e}"))?; } @@ -37774,6 +37903,83 @@ mod required_floor_disposition_and_storage_agreement_law { ] } + // ── the population join: every declared identity, exactly one disposition ────────────── + + /// THE CALIBRATION PAIR FOR THE FLOOR'S SITE-PROJECTION SEAM. + /// + /// `run_required_floor` used to check its partition by COUNT — `offered == routed + + /// declined_long + declined_fixture + declined_outside_gate + declined_cost_debt` — and DESIGN + /// §5 names that shape: completeness is an identity join, not a count equality. This is the + /// population that proves the difference. It drops one identity from the projection and + /// writes another twice, so every count in the old form is still exactly equal while the + /// projection has lost a witness — the same swap `terminal_ledger_completeness_law` pins one + /// seam downstream, at the seam where the roster is BUILT rather than where it is receipted. + /// + /// It calls the production reconciliation, not a paraphrase: `reconcile_identity_population` + /// is the function the floor calls, so a drift in it fails here. + fn declared(names: &[&str]) -> HashSet { + names.iter().map(|n| n.to_string()).collect() + } + + fn disposition_row(identity: &str) -> RequiredFloorDispositionRow { + RequiredFloorDispositionRow { + identity: identity.to_string(), + disposition: RequiredFloorDisposition::Planned, + } + } + + #[test] + fn a_dropped_identity_replaced_by_a_duplicate_is_caught_while_the_count_partition_holds() { + let offered = declared(&["m.a", "m.b", "m.c"]); + let healthy: Vec = ["m.a", "m.b", "m.c"] + .iter() + .map(|i| disposition_row(i)) + .collect(); + // `m.c` never got a row; `m.a` got two. + let swapped: Vec = ["m.a", "m.b", "m.a"] + .iter() + .map(|i| disposition_row(i)) + .collect(); + + // THE OLD CHECK IS GREEN OVER THE BROKEN POPULATION. Stated as an assertion rather than + // as prose, because it is the whole reason the join replaced the sum: the count + // partition cannot tell these two apart. + assert_eq!(offered.len(), healthy.len()); + assert_eq!(offered.len(), swapped.len()); + + let (missing, foreign, duplicated) = + reconcile_identity_population(&offered, healthy.iter().map(|r| r.identity.as_str())); + assert!(missing.is_empty() && foreign.is_empty() && duplicated.is_empty()); + + let (missing, foreign, duplicated) = + reconcile_identity_population(&offered, swapped.iter().map(|r| r.identity.as_str())); + assert_eq!( + missing, + vec!["m.c"], + "the identity with no disposition must be named" + ); + assert!(foreign.is_empty()); + assert_eq!( + duplicated, + vec!["m.a"], + "the doubly-dispositioned identity must be named" + ); + } + + /// A row for an identity nothing declared is the other direction of the same join: a + /// projection that INVENTS a disposition is as wrong as one that loses a witness, and the + /// count partition is equally blind to it when it accompanies a loss. + #[test] + fn a_disposition_for_an_undeclared_identity_is_foreign() { + let offered = declared(&["m.a"]); + let rows = vec![disposition_row("m.a"), disposition_row("m.stray")]; + let (missing, foreign, duplicated) = + reconcile_identity_population(&offered, rows.iter().map(|r| r.identity.as_str())); + assert!(missing.is_empty()); + assert_eq!(foreign, vec!["m.stray"]); + assert!(duplicated.is_empty()); + } + // ── disposition/agreement TSV writers: identity-grain, not a summary-only receipt ─────── #[test] @@ -37805,7 +38011,15 @@ mod required_floor_disposition_and_storage_agreement_law { }, ]; - write_required_floor_disposition_tsv(&path_str, &rows).expect("write tsv"); + // THE OUTCOME AXIS IS JOINED FROM THE TERMINAL LEDGER, and the planted pair is what makes + // the column discriminating: `m.one.a` ran and passed, the two declines never ran. A + // writer that emitted one status alphabet could not produce this pair. + let terminal = vec![ClaimTerminalRow { + qualified: "m.one.a".to_string(), + expected_red: false, + outcome: ClaimOutcome::Pass, + }]; + write_required_floor_disposition_tsv(&path_str, &rows, &terminal).expect("write tsv"); let content = std::fs::read_to_string(&path).expect("read tsv"); let _ = std::fs::remove_dir_all(&dir); @@ -37816,17 +38030,19 @@ mod required_floor_disposition_and_storage_agreement_law { assert!(lines[0].contains("planned=1")); assert!(lines[0].contains("declined_long_module=1")); assert!(lines[0].contains("declined_fixture_member=1")); - assert_eq!(lines[1], "identity\tdisposition\tmatched_prefix"); - assert_eq!(lines[2], "m.one.a\tplanned\t"); + assert_eq!(lines[1], "identity\tdisposition\tmatched_prefix\toutcome"); + assert_eq!(lines[2], "m.one.a\tplanned\t\tpassed"); + // NOT EXECUTED IS WRITTEN, NOT LEFT BLANK. A blank cell is indistinguishable from a + // column the writer failed to fill, which is the empty-observation narrow one grain down. assert_eq!( lines[3], - "test.claim.long.two.b\tdeclined_long_module\ttest.claim.long." + "test.claim.long.two.b\tdeclined_long_module\ttest.claim.long.\tnot_executed" ); // THE FIXTURE ARM CARRIES ITS MATCHED PREFIX, exactly as the long arm does. A decline // that cannot say WHICH prefix admitted it is a count, not a receipt. assert_eq!( lines[4], - "v2.test.fixture.walk_plan_stage.x.d\tdeclined_fixture_member\tv2.test.fixture.walk_plan_stage." + "v2.test.fixture.walk_plan_stage.x.d\tdeclined_fixture_member\tv2.test.fixture.walk_plan_stage.\tnot_executed" ); } @@ -38035,7 +38251,8 @@ mod terminal_ledger_completeness_law { rows: &'a [ClaimTerminalRow], ) -> (Vec<&'a str>, Vec<&'a str>, Vec<&'a str>) { let owned: HashSet = planned.iter().map(|q| q.to_string()).collect(); - let (m, f, d) = reconcile_terminal_ledger(&owned, rows); + let (m, f, d) = + reconcile_identity_population(&owned, rows.iter().map(|r| r.qualified.as_str())); ( m.into_iter().map(|s| leak(s)).collect(), f.into_iter().map(|s| leak(s)).collect(), diff --git a/src/v1/stage0/src/cli_run/required_floor_runner.rs b/src/v1/stage0/src/cli_run/required_floor_runner.rs index c2e186aa765..51c11ae5b8c 100644 --- a/src/v1/stage0/src/cli_run/required_floor_runner.rs +++ b/src/v1/stage0/src/cli_run/required_floor_runner.rs @@ -2933,11 +2933,14 @@ pub fn run_required_floor( // directory deciding admission was that ruling's root cause; reading the declaration is what // fixes it, and that is preserved here exactly. // - // THE PARTITION IS NOW EXACT BY CONSTRUCTION, not by reconciliation. Every site takes exactly - // one arm below, so `claims + declined == offered` holds because the loop cannot do - // otherwise. The former `SitePartitionInexact` and unexplained-decline refusals existed to - // catch the two computations disagreeing; with one computation they have no reachable - // producer, so they are deleted rather than left standing as walls nothing can trip. + // THE PARTITION IS EXACT BY CONSTRUCTION IN THE ARMS, AND CHECKED AS AN IDENTITY JOIN AT THE + // END. Every site takes exactly one arm below, which is what makes the COUNTS agree; it is + // not what makes the POPULATION agree, and those are different claims. A row written for the + // wrong identity, an identity discovered twice, or a preparation-side row for an identity the + // tree does not declare all satisfy "one arm per site" and still break the projection — so + // `FloorDispositionJoinInexact` below joins the declared identities against the rows they + // produced, and the old count equality (`SitePartitionInexact`) is gone rather than kept as a + // weaker restatement of it. // // DUPLICATE ENROLLMENT IS UNCHANGED AND UNMOVED, and this is the one invariant the deleted // fold genuinely carried. It is caught downstream by `receipt_identities`, a HashSet keyed on @@ -3125,13 +3128,14 @@ pub fn run_required_floor( let mut claims: Vec = Vec::new(); let mut planned_identities: HashSet = HashSet::new(); - let mut long_declined = 0usize; - let mut fixture_declined = 0usize; - let mut outside_gate_declined = 0usize; - let mut cost_debt_declined = 0usize; let mut cost_debt_seen: HashSet = HashSet::new(); let mut outcome_withheld_cost_debt: Vec = Vec::new(); - let mut sites_offered = 0usize; + // THE POPULATION, AT IDENTITY GRAIN. It accumulates the sites this loop offers and then the + // identities preparation dropped, so by the join below it is every DECLARED witness identity + // in the tree. Both counts (`sites_offered`, `declared_identities`) are read off it rather + // than maintained beside it: a count and a population kept in step by hand are two + // computations of one fact, and the count is the weaker one. + let mut declared_identity_set: HashSet = HashSet::new(); let mut disposition_rows: Vec = Vec::new(); let mut storage_agreement_rows: Vec = Vec::new(); for file in files { @@ -3150,14 +3154,28 @@ pub fn run_required_floor( let path_is_long = is_long_home_path(&file.path); let storage_agreement = long_home_storage_agreement(path_is_long, long_home); for function in &file.functions { - sites_offered += 1; let identity = format!("{}.{}", file.module_path, function); + // ONE SITE PER QUALIFIED IDENTITY, REFUSED OVER THE WHOLE OFFERED POPULATION. + // + // This wall used to stand further down, guarding PLANNED claims only, so a duplicate + // whose first arm was a decline never reached it: two sites sharing one identity took + // two arms, wrote two disposition rows, and the partition — a count equality — added + // up exactly. The identity join below cannot express "this witness has one + // disposition" while the offered side is a multiset, so the uniqueness of the offered + // side is established HERE, where the site is enumerated, and the join downstream is + // then a statement about identities rather than about totals. + if !declared_identity_set.insert(identity.clone()) { + return Err(format!( + "REQUIRED-FLOOR REFUSAL cause=DuplicateWitnessIdentity identity={identity} — \ + one qualified declaration was discovered at more than one site, so it would \ + carry more than one disposition; a witness identity names exactly one site" + )); + } storage_agreement_rows.push(LongHomeStorageAgreementRow { identity: identity.clone(), agreement: storage_agreement, }); if long_home { - long_declined += 1; disposition_rows.push(RequiredFloorDispositionRow { identity, disposition: RequiredFloorDisposition::DeclinedLongModule { @@ -3169,7 +3187,6 @@ pub fn run_required_floor( continue; } if let Some(prefix) = fixture_prefix { - fixture_declined += 1; disposition_rows.push(RequiredFloorDispositionRow { identity, disposition: RequiredFloorDisposition::DeclinedFixtureMember { @@ -3191,7 +3208,6 @@ pub fn run_required_floor( // checks exact and costs the fold nothing — no scope is built and no frame allocated // for a row that will not run. if cost_debt_roster.contains(&identity) { - cost_debt_declined += 1; cost_debt_seen.insert(identity.clone()); outcome_withheld_cost_debt.push(identity.clone()); disposition_rows.push(RequiredFloorDispositionRow { @@ -3203,29 +3219,20 @@ pub fn run_required_floor( // THE FOURTH DECLINE, AFTER COST DEBT so a rostered identity outside the gate still // enters `cost_debt_seen` and the roster's staleness check keeps its meaning. if !inside_required_gate { - outside_gate_declined += 1; disposition_rows.push(RequiredFloorDispositionRow { identity, disposition: RequiredFloorDisposition::DeclinedOutsideRequiredGate, }); continue; } - // ONE EXECUTABLE CLAIM PER QUALIFIED IDENTITY, REFUSED HERE AND NAMED. - // - // The deleted manifest carried this invariant and refused BEFORE running anything, - // naming the offending declaration. `receipt_identities` is NOT the same wall: it - // compares populations after all 9,122 claims have executed, so a duplicate costs a - // full duplicated evaluation before anything notices, and a count mismatch says only - // that two populations disagree -- never which identity caused it. Planned-identity - // uniqueness and receipt completeness are different properties, and the terminal - // `planned == executed == receipted` check remains as the second, separate one. - if let Some(prior) = planned_identities.replace(identity.clone()) { - return Err(format!( - "REQUIRED-FLOOR REFUSAL cause=DuplicateWitnessIdentity identity={prior} — \ - one qualified declaration resolved to more than one executable claim; the \ - roster cannot name the same witness twice" - )); - } + // NO SECOND DUPLICATE WALL LIVES HERE. This arm used to re-test uniqueness over the + // PLANNED identities only, which is the same invariant the offered-side insert above + // now establishes over the whole discovered population — strictly wider, and reached + // before any arm is taken, so a duplicate whose first site declines is caught too. + // Keeping both would be one fact with two producers (DESIGN §3), and the narrower one + // dissolves on the climb (§4b(4)). `planned_identities` remains, as the expected side + // of the terminal ledger join; it is no longer a uniqueness mechanism. + planned_identities.insert(identity.clone()); disposition_rows.push(RequiredFloorDispositionRow { identity: identity.clone(), disposition: RequiredFloorDisposition::Planned, @@ -3241,8 +3248,37 @@ pub fn run_required_floor( }); } } - // THE PARTITION OVER THE OFFERED POPULATION, CHECKED — not merely reported for a reader to - // add up. + // Taken BEFORE the declared population is folded in, so it is what the site loop offered and + // not that number reconstructed by subtracting one population from another. + let sites_offered = declared_identity_set.len(); + // THE UNIVERSE IS THE DECLARED POPULATION, NOT THE OFFERED ONE. + // + // Preparation removes two populations before a site can be offered — modules excluded by + // substring, and (since the 2026-08-29 gate cut) every module the gate closure does not + // reach — and a witness declared in one of them used to be neither planned nor declined. It + // was not in `offered`, so no partition over `offered` could say anything about it: the + // denominator itself had already narrowed, which is the level ABOVE the partition where + // `docs/plans/witness-execution-closure.md` found the last missing population. After the gate + // cut that silence is most of the corpus. + // + // Preparation now carries a disposition row for each identity it drops, in the SAME authority + // (`RequiredFloorDisposition`), so the join below runs over every DECLARED witness identity in + // the tree. `sites_offered` keeps its old meaning — what the site loop was offered — and is + // reported beside `declared` rather than replaced by it, because a reader comparing runs needs + // the subject-relative number and the tree-relative number to stay distinguishable. + for row in &prepared.undiscovered_dispositions { + if !declared_identity_set.insert(row.identity.clone()) { + return Err(format!( + "REQUIRED-FLOOR REFUSAL cause=DuplicateWitnessIdentity identity={} — an identity \ + dropped by preparation was ALSO offered by the site loop, so it would carry two \ + dispositions; the prepared subject and its complement must be disjoint", + row.identity + )); + } + disposition_rows.push(row.clone()); + } + // THE PARTITION OVER THE DECLARED POPULATION, CHECKED AS AN IDENTITY JOIN — not as a count + // equality, and not merely reported for a reader to add up. // // `claims_planned` is the POST-decline number, and the terminal invariant downstream // (`ClaimIdentityCountsDisagree`) compares planned == executed == receipted. Every one of @@ -3250,41 +3286,97 @@ pub fn run_required_floor( // the run's own honesty check could not see what it lost: a projection that declined a // thousand identities and one that declined none produce identically healthy-looking // triples. This is the missing invariant on the other side of that seam — the offered - // population must be exactly the routed population plus the declined one — and it is - // stated where the loop that could violate it runs. + // population must be exactly the dispositioned population — and it is stated where the loop + // that could violate it runs. // - // It cannot fail today, because the loop takes exactly one arm per site. That is the point: - // it is the construction's own statement of what it guarantees, and it fails loudly the - // first time an edit adds a third arm that quietly swallows rows, which is precisely how - // the live-tree decline arrived and stayed invisible. - if sites_offered - != claims.len() - + long_declined - + fixture_declined - + outside_gate_declined - + cost_debt_declined + // WHY IT IS A JOIN AND NOT `offered == routed + declined_*`. The old form was that sum, and + // DESIGN §5 names it: completeness is an identity join, not a count equality. The sum is + // green over a projection that writes a row for the wrong identity, over one that drops + // `m.c` while writing `m.a` twice, and over any pair of errors that cancels in the totals — + // exactly the calibration pair `terminal_ledger_completeness_law` pins one seam downstream. + // It is the SAME join, through the SAME function + // (`reconcile_identity_population`), because it is the same fact asked at a different seam. + // + // AND THE COUNTERS ARE DERIVED FROM THE ROWS, not accumulated beside them. Four `+= 1`s used + // to run in the arms that push the rows, so the reported `declined_long` and the row + // population were two computations of one fact and could disagree with nothing to say so. + // With the counts folded out of the rows there is one producer, and the join above is what + // makes the rows themselves trustworthy. + let (declared_without_disposition, dispositioned_without_declaration, disposition_duplicated) = + reconcile_identity_population( + &declared_identity_set, + disposition_rows.iter().map(|r| r.identity.as_str()), + ); + if !declared_without_disposition.is_empty() + || !dispositioned_without_declaration.is_empty() + || !disposition_duplicated.is_empty() { + let sample = |rows: &[&str]| { + if rows.is_empty() { + "none".to_string() + } else { + rows.iter() + .take(10) + .copied() + .collect::>() + .join(" | ") + } + }; return Err(format!( - "REQUIRED-FLOOR REFUSAL cause=SitePartitionInexact offered={sites_offered} \ - routed={} declined_long={long_declined} declined_fixture={fixture_declined} \ - declined_outside_gate={outside_gate_declined} \ - declined_cost_debt={cost_debt_declined} — every \ - discovered site must be either routed to a claim or declined with a stated \ - disposition; a gap here is a roster that narrowed without saying so", - claims.len() + "REQUIRED-FLOOR REFUSAL cause=FloorDispositionJoinInexact declared={} rows={} \ + declared_without_disposition={} dispositioned_without_declaration={} duplicated={} \ + — every DECLARED witness identity must join to exactly one disposition; a gap here \ + is a roster that narrowed, widened or double-counted without saying so. \ + declared_without_disposition: {} :: dispositioned_without_declaration: {} :: \ + duplicated: {}", + declared_identity_set.len(), + disposition_rows.len(), + declared_without_disposition.len(), + dispositioned_without_declaration.len(), + disposition_duplicated.len(), + sample(&declared_without_disposition), + sample(&dispositioned_without_declaration), + sample(&disposition_duplicated), )); } + // ONE PRODUCER FOR THE COUNTS: the joined row population, folded once per arm. + let disposition_count = |select: fn(&RequiredFloorDisposition) -> bool| { + disposition_rows + .iter() + .filter(|row| select(&row.disposition)) + .count() + }; + let declared_identities = declared_identity_set.len(); + let long_declined = + disposition_count(|d| matches!(d, RequiredFloorDisposition::DeclinedLongModule { .. })); + let fixture_declined = + disposition_count(|d| matches!(d, RequiredFloorDisposition::DeclinedFixtureMember { .. })); + let outside_gate_declined = + disposition_count(|d| matches!(d, RequiredFloorDisposition::DeclinedOutsideRequiredGate)); + let cost_debt_declined = + disposition_count(|d| matches!(d, RequiredFloorDisposition::DeclinedCostDebt)); + let gate_closure_declined = + disposition_count(|d| matches!(d, RequiredFloorDisposition::DeclinedOutsideGateClosure)); + let discovery_excluded_declined = disposition_count(|d| { + matches!( + d, + RequiredFloorDisposition::DeclinedDiscoveryExcluded { .. } + ) + }); eprintln!( - "[floor-phase] phase=site-projection state=completed wall_ms={} sites={} files={} \ - claims={} declined_long={} declined_fixture={} declined_outside_gate={} \ - declined_cost_debt={}", + "[floor-phase] phase=site-projection state=completed wall_ms={} declared={} sites={} \ + files={} claims={} declined_long={} declined_fixture={} declined_outside_gate={} \ + declined_gate_closure={} declined_discovery_excluded={} declined_cost_debt={}", projection_started.elapsed().as_millis(), + declared_identities, sites_offered, files.len(), claims.len(), long_declined, fixture_declined, outside_gate_declined, + gate_closure_declined, + discovery_excluded_declined, cost_debt_declined ); @@ -3771,6 +3863,9 @@ pub fn run_required_floor( declined_long_module: long_declined, declined_fixture_member: fixture_declined, declined_outside_required_gate: outside_gate_declined, + declared_identities, + declined_outside_gate_closure: gate_closure_declined, + declined_discovery_excluded: discovery_excluded_declined, claims_planned, claims_executed: 0, receipt_identities: 0, @@ -4956,8 +5051,8 @@ pub fn run_required_floor( // WITHHELD ROWS DO NOT APPEAR IN THIS SUM, and that is a consequence of where the withhold // happens rather than an exemption carved into it. A cost-debt row is declined at claim // BUILD time, alongside the long-home and live-tree declines, so it never becomes a planned - // claim and this partition never sees it. The site-level partition upstream - // (`SitePartitionInexact`) is what accounts for it. + // claim and this partition never sees it. The site-level population join upstream + // (`FloorDispositionJoinInexact`) is what accounts for it. // // A FIRST CUT OF THIS CHANGE WITHHELD INSIDE THE EXECUTION LOOP INSTEAD, and it would have // red the floor on this very check -- 320 planned claims that never executed and never @@ -4992,7 +5087,10 @@ pub fn run_required_floor( // the first would hide the second — which is precisely the pair that cancels in the totals. { let (planned_without_terminal, terminal_without_planned, terminal_duplicated) = - reconcile_terminal_ledger(&planned_identities, &terminal_rows); + reconcile_identity_population( + &planned_identities, + terminal_rows.iter().map(|r| r.qualified.as_str()), + ); if !planned_without_terminal.is_empty() || !terminal_without_planned.is_empty() || !terminal_duplicated.is_empty() @@ -5132,7 +5230,11 @@ pub fn run_required_floor( write_required_floor_claim_cost_tsv(&path, &outcome.claim_cost, cost_basis)?; } if let Some(path) = required_floor_disposition_path { - write_required_floor_disposition_tsv(&path, &outcome.required_floor_disposition)?; + write_required_floor_disposition_tsv( + &path, + &outcome.required_floor_disposition, + &terminal_rows, + )?; } if let Some(path) = long_home_storage_agreement_path { write_long_home_storage_agreement_tsv(&path, &outcome.long_home_storage_agreement)?; @@ -5149,6 +5251,8 @@ pub(crate) fn required_floor_disposition_label( RequiredFloorDisposition::DeclinedFixtureMember { .. } => "declined_fixture_member", RequiredFloorDisposition::DeclinedOutsideRequiredGate => "declined_outside_required_gate", RequiredFloorDisposition::DeclinedCostDebt => "declined_cost_debt", + RequiredFloorDisposition::DeclinedOutsideGateClosure => "declined_outside_gate_closure", + RequiredFloorDisposition::DeclinedDiscoveryExcluded { .. } => "declined_discovery_excluded", } } @@ -5158,8 +5262,17 @@ pub(crate) fn required_floor_disposition_matched_prefix( match disposition { RequiredFloorDisposition::DeclinedLongModule { matched_prefix } | RequiredFloorDisposition::DeclinedFixtureMember { matched_prefix } => matched_prefix, + // The excluded arm's payload is a SUBSTRING and not a module-name prefix, and it shares + // this column because the column's meaning is "the authored text that matched", which is + // the same question for all three. It is not folded into the prefix arms above: a + // substring matched anywhere in a path is a different test from a prefix on a module + // name, and the label column keeps them apart for any reader joining on it. + RequiredFloorDisposition::DeclinedDiscoveryExcluded { matched_substring } => { + matched_substring + } RequiredFloorDisposition::Planned | RequiredFloorDisposition::DeclinedOutsideRequiredGate + | RequiredFloorDisposition::DeclinedOutsideGateClosure | RequiredFloorDisposition::DeclinedCostDebt => "", } } diff --git a/src/v2/workflow/floor_terminal_ledger.dag b/src/v2/workflow/floor_terminal_ledger.dag index b6704f8d62e..e5a321da701 100644 --- a/src/v2/workflow/floor_terminal_ledger.dag +++ b/src/v2/workflow/floor_terminal_ledger.dag @@ -31,7 +31,7 @@ import v2.workflow.required_floor { // every row is terminal. Absence is not a value it can express. // // THE SEED CARRIES A HAND-WRITTEN MIRROR OF THIS SCHEMA. `cli_run.rs` is HAND_MAINTAINED, so its -// `ClaimTerminalRow`, `ClaimDisposition` and `reconcile_terminal_ledger` are authored beside these +// `ClaimTerminalRow`, `ClaimDisposition` and `reconcile_identity_population` are authored beside these // declarations rather than derived from them. Regen does not compare them, because that file is // not generated; the witnesses do not compare them, because each side is exercised alone. // diff --git a/src/v2/workflow/required_floor.dag b/src/v2/workflow/required_floor.dag index 2d57dcc3156..20202918d7a 100644 --- a/src/v2/workflow/required_floor.dag +++ b/src/v2/workflow/required_floor.dag @@ -23,8 +23,10 @@ import std.types { NonEmptyStr } // IDENTITY-GRAINED FLOOR DISPOSITION RECEIPT (operator ruling 2026-08-19). // -// Every discovered site gets exactly one `RequiredFloorDisposition`, keyed by its qualified -// `module.function` identity. This is the single authority for that fact: the host loop in +// Every DECLARED witness identity in the tree gets exactly one `RequiredFloorDisposition`, keyed +// by its qualified `module.function` identity, and the host joins the two populations at that +// grain — `FloorDispositionJoinInexact` refuses a missing, duplicated or foreign row rather than +// reporting counts that add up (DESIGN §5: completeness is an identity join). This is the single authority for that fact: the host loop in // `v1_compiler.cli_run` `run_required_floor` computes admission by testing a claim's authored // module name against `long_home_prefixes()` and `fixture_home_prefixes()` below, then REALIZES // the arm this type already names — it does not invent a second admission concept. A `Declined*` @@ -56,7 +58,7 @@ import std.types { NonEmptyStr } // not green, and it is not a failure either — the two have different remedies and are // reported apart. THAT MECHANISM IS ALREADY LIVE IN THIS CHANGE, which is what makes the // deletion safe to make next: the route-gap arm, its two-way roster join, and the -// `SitePartitionInexact` wall all execute here, over the 101 identities that reached it +// `FloorDispositionJoinInexact` wall all execute here, over the 101 identities that reached it // without this arm being touched at all. // // DELETION RECEIPT: run 32345970386 measured 626/783 passing under execution, and the staged @@ -68,11 +70,32 @@ import std.types { NonEmptyStr } // deprecated. It remains the declaration `reads_live_tree_effective` reads for AFFECTED-SET // SELECTION ELIGIBILITY, which is a different question from "can this execute" and keeps its // own single authority. Only the floor's forked, syntactic second copy was deleted. +// TWO ARMS SPEAK FOR IDENTITIES THE PROJECTION NEVER USED TO SEE AT ALL, and they are declines +// by the same authority rather than a second status vocabulary beside it. +// +// A disposition row used to exist only for a site the PREPARED SUBJECT offered. Preparation +// itself removes two populations before that point — a module whose path or name carries an +// exclusion substring, and (since the 2026-08-29 gate cut) every module the required gate's +// import closure does not reach — and a witness declared in one of those was neither planned nor +// declined. It left the floor's universe one level above the partition, which is the same +// silence `docs/plans/witness-execution-closure.md` records for the deleted live-tree decline: +// a population discovered by nothing, so counted by nothing. +// +// `DeclinedOutsideGateClosure` IS NOT `DeclinedOutsideRequiredGate`, and the distinction is +// load-bearing rather than descriptive: the second speaks for a module that WAS prepared and +// whose authored name missed every gate prefix, and the first for a module that was never +// prepared, resolved or offered. They are removed by different mechanisms, they are restored by +// different triggers, and after the gate cut they differ in population by two orders of +// magnitude — the closure arm is the population the §4b rung drop "Required gate reduced to the +// compiler floor" names. One label over both would report that drop's whole subject as a +// rounding error on a nearby count. type RequiredFloorDisposition = Planned | DeclinedLongModule { matched_prefix: String } | DeclinedFixtureMember { matched_prefix: String } | DeclinedOutsideRequiredGate + | DeclinedOutsideGateClosure + | DeclinedDiscoveryExcluded { matched_substring: String } | DeclinedCostDebt // ROSTER GROWTH IS BUDGET-BOUND AT THIS ADMISSION AUTHORITY. From be7a838fe2cb73ed3e136d935e8c9cf121045717 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 29 Aug 2026 19:00:26 +0000 Subject: [PATCH 2/7] Merge auto-heal's corpus-wide discovery fold; correct three descriptions to match it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The CI auto-heal bot resolved the #9685 conflict by reimplementing the declared-population enumeration on the producer itself — folded over preparation's FULL module index, with the prepared closure and exclusion map classifying the returned identities. That is a better §3 answer than the split this branch carried (producer for the prepared subject, naming-hygiene scan for the removed sources), so it is kept and mine is dropped rather than restored. What it left describing something the code no longer does, corrected here: - the receipt line still cited BarrenTestSidecar, a refusal the producer replaced, and said 'offered' where the guarantee is now over every DECLARED entry; - the site loop's own comment still said the population is 'the identities preparation dropped', which is the deleted design; - the plan doc's item 1 described preparation emitting the rows. And one consequence neither the bot nor this branch had stated: folding the producer over the full index means its per-file refusals — misplaced test decl, barren sidecar, misplaced wire contract, malformed live_tree_disposition — now stop the REQUIRED floor for any module under the source roots. That is a real widening of this lane's subject. It is survivable today (measured: zero misplaced decls, zero barren sidecars tree-wide) and the first violation authored anywhere will red this lane rather than the one owning the file, so it is written into the doc rather than left for that run to discover. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WmatNuCFnqTdE2KoiwEcm4 --- docs/plans/witness-execution-closure.md | 28 ++++++++++++++----- src/v1/stage0/src/bin/claim_executor.rs | 5 ++-- .../src/cli_run/required_floor_runner.rs | 11 ++++---- 3 files changed, 30 insertions(+), 14 deletions(-) diff --git a/docs/plans/witness-execution-closure.md b/docs/plans/witness-execution-closure.md index 3c524f7d081..b49de52441e 100644 --- a/docs/plans/witness-execution-closure.md +++ b/docs/plans/witness-execution-closure.md @@ -249,13 +249,27 @@ run's own, not this document's: `required-floor: declared=… offered=… declin ### What changed -1. **The universe is the declared population.** Preparation now emits one - `RequiredFloorDisposition` row for every identity it drops — - `DeclinedOutsideGateClosure` and `DeclinedDiscoveryExcluded { matched_substring }`, two arms - on the authority that already existed, not a second status vocabulary. The gate-closure - population keeps its own arm rather than folding into `DeclinedOutsideRequiredGate`: the two - are removed by different mechanisms, restored by different triggers, and differ by two orders - of magnitude, and the first is the rung drop's subject. +1. **The universe is the declared population, answered by one authority.** The floor folds + `v2.workflow.floor_discovery_producer` (`discover_floor_rows_for_source`) over preparation's + FULL module index rather than over the prepared closure alone, and classifies each returned + identity against the prepared closure and the exclusion map: an identity whose module + preparation dropped carries `DeclinedOutsideGateClosure` or + `DeclinedDiscoveryExcluded { matched_substring }` — two arms on the authority that already + existed, not a second status vocabulary. No Rust rescan stands beside the producer; gunbc#9685's + single-discovery-authority cut holds for the whole corpus, not only for the prepared subject. + The gate-closure population keeps its own arm rather than folding into + `DeclinedOutsideRequiredGate`: the two are removed by different mechanisms, restored by + different triggers, and differ by two orders of magnitude, and the first is the rung drop's + subject. + + **The consequence, stated rather than discovered later:** the producer's per-file refusals — + misplaced `test` decl, barren sidecar, misplaced wire contract, malformed + `live_tree_disposition` row — now stop the required floor for ANY module under the source + roots, not only for one the gate closure admitted. That is a real widening of what this lane + refuses over. It is survivable today because the corpus carries none of those violations + (measured 2026-08-29: zero `test`-marked decls outside a `*_test.dag` sidecar, zero barren + sidecars), and the first violation authored anywhere in the tree will red this lane rather + than the one that owns the file. 2. **The partition is an identity join, not a count equality.** The old check was `offered == routed + declined_long + declined_fixture + declined_outside_gate + declined_cost_debt`, which DESIGN §5 names by shape: green over a projection that drops one diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 210123b5387..c7fe811ee44 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -1175,8 +1175,9 @@ fn report_required_floor_outcome(outcome: &v1_compiler::cli_run::RequiredFloorOu declined_outside_required_gate={} declined_outside_gate_closure={} \ declined_discovery_excluded={} — every DECLARED witness identity in the tree is exactly \ one of these, joined at identity grain (FloorDispositionJoinInexact refuses otherwise), \ - and no `*_test.dag` entry offered zero sites (BarrenTestSidecar refuses upstream of \ - this line)", + and no `*_test.dag` entry declared zero sites (v2.workflow.floor_discovery_producer \ + refuses a barren or misplaced sidecar upstream of this line, over the full module \ + index)", outcome.declared_identities, outcome.sites_offered, outcome.claims_planned, diff --git a/src/v1/stage0/src/cli_run/required_floor_runner.rs b/src/v1/stage0/src/cli_run/required_floor_runner.rs index c6c53076ec5..98ce7dd7754 100644 --- a/src/v1/stage0/src/cli_run/required_floor_runner.rs +++ b/src/v1/stage0/src/cli_run/required_floor_runner.rs @@ -3126,11 +3126,12 @@ pub fn run_required_floor( let mut planned_identities: HashSet = HashSet::new(); let mut cost_debt_seen: HashSet = HashSet::new(); let mut outcome_withheld_cost_debt: Vec = Vec::new(); - // THE POPULATION, AT IDENTITY GRAIN. It accumulates the sites this loop offers and then the - // identities preparation dropped, so by the join below it is every DECLARED witness identity - // in the tree. Both counts (`sites_offered`, `declared_identities`) are read off it rather - // than maintained beside it: a count and a population kept in step by hand are two - // computations of one fact, and the count is the weaker one. + // THE POPULATION, AT IDENTITY GRAIN. The discovery authority above answered over the FULL + // module index, so this loop sees every DECLARED witness identity in the tree and classifies + // each one — the prepared closure and the exclusion map decide which are offered and which + // carry a preparation-stage decline. Both counts (`sites_offered`, `declared_identities`) are + // read off this set rather than maintained beside it: a count and a population kept in step + // by hand are two computations of one fact, and the count is the weaker one. let mut declared_identity_set: HashSet = HashSet::new(); let mut sites_offered = 0usize; let mut disposition_rows: Vec = Vec::new(); From 97b73a0b9c9ede9cb572daaa3123c6c3f212def4 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 29 Aug 2026 19:03:49 +0000 Subject: [PATCH 3/7] Make discovery census witness exhaustive --- dag/test/claim/discovery_census_witness_test.dag | 1 + 1 file changed, 1 insertion(+) diff --git a/dag/test/claim/discovery_census_witness_test.dag b/dag/test/claim/discovery_census_witness_test.dag index 89869efb092..0a18f3d9a0b 100644 --- a/dag/test/claim/discovery_census_witness_test.dag +++ b/dag/test/claim/discovery_census_witness_test.dag @@ -336,6 +336,7 @@ test fn w_rostered_identity_declines_for_cost_debt() -> Bool { identity: "dag.test.claim.lifecycle_survivor_corpus_census.no_raw_lifecycle_string_survivors_remain" ) { DeclinedCostDebt => true + DeclinedOutsideRequiredGate => false DeclinedOutsideGateClosure => false DeclinedDiscoveryExcluded { matched_substring: _ } => false Planned => false From a5ef136ab7afa8b25dc4c202dcef7feec3bdf9ec Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 29 Aug 2026 19:19:38 +0000 Subject: [PATCH 4/7] Bound full-index retention and receipt seed transport --- docs/plans/witness-execution-closure.md | 12 ++++++++++++ .../stage0/src/cli_run/required_floor_runner.rs | 15 +++++++++++---- 2 files changed, 23 insertions(+), 4 deletions(-) diff --git a/docs/plans/witness-execution-closure.md b/docs/plans/witness-execution-closure.md index b49de52441e..034edb16ade 100644 --- a/docs/plans/witness-execution-closure.md +++ b/docs/plans/witness-execution-closure.md @@ -249,6 +249,18 @@ run's own, not this document's: `required-floor: declared=… offered=… declin ### What changed +**Hand-Rust receipt.** This change adds zero Rust declarations. It modifies the existing +`PreparedRepository`, `PreparedSubject`, `assemble_prepared_subject_closure`, +`prepare_repository_closure`, and `run_required_floor` items to transport full-index source views +into the already-modeled discovery producer, then drops those views before claim execution. Rust +is still necessary only at the v1 host boundary that owns repository acquisition and invokes the +interpreter; it defines neither the declaration grammar nor discovery policy. The owning ROADMAP +row is `v1-hand-queue-drain`. The concrete deletion trigger is that row's emitted-v2 replacement +of required-floor orchestration: when repository acquisition and producer invocation are +performed by the emitted workflow, these five seed modifications delete with the host rather than +moving into another Rust census. This is an explicit deferral of the transport boundary, not a +claim that the modified hand-Rust surface is generated or already dissolved. + 1. **The universe is the declared population, answered by one authority.** The floor folds `v2.workflow.floor_discovery_producer` (`discover_floor_rows_for_source`) over preparation's FULL module index rather than over the prepared closure alone, and classifies each returned diff --git a/src/v1/stage0/src/cli_run/required_floor_runner.rs b/src/v1/stage0/src/cli_run/required_floor_runner.rs index 98ce7dd7754..a46d674276a 100644 --- a/src/v1/stage0/src/cli_run/required_floor_runner.rs +++ b/src/v1/stage0/src/cli_run/required_floor_runner.rs @@ -2351,7 +2351,7 @@ pub fn run_required_floor( .map(|m| m.to_string()), ) .collect(); - let (prepared, prepared_sources) = prepare_repository_closure( + let (mut prepared, prepared_sources) = prepare_repository_closure( source_roots, &floor_prepared_subject_exclusions(), Some((&gate_entry_index, &closure_seeds)), @@ -2367,9 +2367,13 @@ pub fn run_required_floor( .iter() .map(|view| view.module_path.clone()) .collect(); - let discovery_exclusions = prepared.discovery_exclusions.clone(); - let discovery_sources: Vec = prepared - .full_inventory + // BOUNDED RETENTION, NOT A CORPUS COPY HELD FOR THE CLAIM RUN. The full-index views exist + // only until the modeled discovery fold consumes them. Taking them out of `prepared` makes + // that lifetime structural: the outside-closure source bytes cannot survive into claim + // execution through the repository value every later phase borrows. + let discovery_exclusions = std::mem::take(&mut prepared.discovery_exclusions); + let full_inventory = std::mem::take(&mut prepared.full_inventory); + let discovery_sources: Vec = full_inventory .iter() .map(|view| FloorDiscoverySource { path: view.source.path.replace('\\', "/"), @@ -2377,6 +2381,7 @@ pub fn run_required_floor( source: view.source.clone(), }) .collect(); + drop(full_inventory); let _floor_prepared_guard = register_floor_prepared_authority_guard(prepared_sources); // WARM THE MODULE-PATH INDEX HERE, because otherwise ONE ARBITRARY CLAIM PAYS FOR IT. // @@ -2991,6 +2996,8 @@ pub fn run_required_floor( }), } } + drop(module_for_path); + drop(discovery_sources); files.sort_by(|a, b| a.path.cmp(&b.path)); eprintln!( "[floor-phase] phase=discovery-authority state=completed wall_ms={} authority={} \ From 5d8f945b2d00f44160b32ce172dbed9e2b6cac4c Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 29 Aug 2026 19:21:19 +0000 Subject: [PATCH 5/7] Preserve discovery source count before release --- src/v1/stage0/src/cli_run/required_floor_runner.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/v1/stage0/src/cli_run/required_floor_runner.rs b/src/v1/stage0/src/cli_run/required_floor_runner.rs index a46d674276a..3052ed35a9f 100644 --- a/src/v1/stage0/src/cli_run/required_floor_runner.rs +++ b/src/v1/stage0/src/cli_run/required_floor_runner.rs @@ -2381,6 +2381,7 @@ pub fn run_required_floor( source: view.source.clone(), }) .collect(); + let discovery_source_count = discovery_sources.len(); drop(full_inventory); let _floor_prepared_guard = register_floor_prepared_authority_guard(prepared_sources); // WARM THE MODULE-PATH INDEX HERE, because otherwise ONE ARBITRARY CLAIM PAYS FOR IT. @@ -3004,7 +3005,7 @@ pub fn run_required_floor( sources={} rows={} entries={}", discovery_started.elapsed().as_millis(), FLOOR_DISCOVERY_AUTHORITY_MODULE, - discovery_sources.len(), + discovery_source_count, discovery_rows.len(), files.len() ); From 8a93f9b060eb27de8a29382b5b5274e0e79946c0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 29 Aug 2026 19:22:12 +0000 Subject: [PATCH 6/7] Release the corpus after the discovery fold; state this change's seed-growth disposition (review 57430) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit TWO FINDINGS, BOTH REAL, ANSWERED IN THE TREE RATHER THAN IN THE PR THREAD. RETENTION. Folding the discovery authority over the full module index holds every source's bytes, and the out-of-closure majority is held by nothing else — the prepared graph is the gate closure. Leaving that on PreparedRepository restored corpus-scale retention across the longest phase of the program, in the one lane RequiredFloorGrowthBudgetStanding records as having no measured memory margin, where growth owes a named payment. No payment is claimed and none is needed: the inventory is now std::mem::take'n into the fold's own local and dropped with module_for_path the moment the rows are classified. What survives is paths, module names and function names — never bytes. SEED GROWTH. Measured at item grain, this change adds no hand Rust declaration: one function is renamed (reconcile_terminal_ledger -> reconcile_identity_population, generalized so one join serves two seams) and everything else is fields, coproduct arms and bodies of existing items. Its disposition in gunbc.seed_growth_admission's vocabulary is ExistingSeedItemModified, and the doc supplies that arm's payload: dag authority v2.workflow.required_floor RequiredFloorDisposition (the two new arms land in the model, the seed realizes them), so capability origin is ModeledCapability, not a capability originated in Rust. WHAT THE REVIEW ASKED FOR AND THIS DELIBERATELY DOES NOT SUPPLY: authored before/after Rust census figures. seed_growth_forward_freeze_policy_note records that hand-item and hand-LOC deltas are functions of the diff, that an authored copy is a second representation of a fact the diff already owns, and that a prior receipt authored exactly such figures and got them wrong. The deriving instrument (gunbc.rust_item_host_observation) and the adjudicating join (seed_growth_admit_change, which no required phase invokes yet) are named instead. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WmatNuCFnqTdE2KoiwEcm4 --- docs/plans/witness-execution-closure.md | 35 +++++++++++++++++++ src/v1/stage0/src/cli_run.rs | 9 +++++ .../src/cli_run/required_floor_runner.rs | 32 +++++++++++++---- 3 files changed, 69 insertions(+), 7 deletions(-) diff --git a/docs/plans/witness-execution-closure.md b/docs/plans/witness-execution-closure.md index b49de52441e..aabf7a4d604 100644 --- a/docs/plans/witness-execution-closure.md +++ b/docs/plans/witness-execution-closure.md @@ -303,3 +303,38 @@ claim to join to (§3), so they are named here as triggers rather than improvise added without either match acquiring an arm, and nothing refused — the module's own witness is outside the gate closure, so no executing path typechecks it. The arms are added here and the claim is restated at its honest rung, with the trigger recorded in the module. + +### The seed-growth disposition of this change, and the retention it does not take + +Two review findings on gunbc#9684 (review 57430) are answered here rather than in the PR thread, +because both are properties of the change a later reader must be able to check. + +**Retention.** Folding the discovery authority over the FULL module index means holding every +source's bytes — including the out-of-closure majority, which nothing else in the run holds, since +the prepared graph is the gate closure. Retaining that on `PreparedRepository` for the run would be +corpus-scale retention across the longest phase of the program, in the one lane +`v2.workflow.required_floor` `RequiredFloorGrowthBudgetStanding` records as having **no measured +memory margin** — where growth owes a named payment. No payment is claimed. The inventory is +`take`n out of the prepared repository into the fold's own local and dropped the moment the rows +are classified; what survives is paths, module names and function names. The instrument for what +the fold itself costs is the run's own `[floor-phase] phase=discovery-authority` line, which +reports sources, rows and wall — it is not transcribed here. + +**Hand-Rust growth.** Measured at item grain over `src/v1/stage0/src`, this change adds **no hand +Rust declaration**: one function is renamed (`reconcile_terminal_ledger` → +`reconcile_identity_population`, generalized so one join serves two seams) and everything else is +fields, coproduct arms and bodies of items that already existed. Its disposition in +`gunbc.seed_growth_admission`'s own vocabulary is therefore `ExistingSeedItemModified`, whose +payload this section supplies: the `.dag` authority is +`v2.workflow.required_floor` `RequiredFloorDisposition` — the two new arms land there, in the model, +and the seed realizes them — so the capability origin is `ModeledCapability` and not a capability +originated in Rust. The current boundary is the required floor's projection. + +No `SeedGrowthJustification` row is owed, because that roster names *added* declarations and this +change adds none. And no before/after item or LOC figures are typed into this document +deliberately: `seed_growth_forward_freeze_policy_note` records that hand-item and hand-LOC deltas +are functions of the diff, that an authored copy is a second representation of a fact the diff +already owns, and that a previous receipt authored exactly such figures and got them wrong. The +deriving instrument is `gunbc.rust_item_host_observation`; the adjudicating join is +`gunbc.seed_growth_admission` `seed_growth_admit_change`, which that module states no required CI +phase invokes yet — its next-rung trigger, unchanged by this change. diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 94232896110..791a9b7c2a5 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -35656,6 +35656,15 @@ pub struct PreparedRepository { /// Every source in the module index, including modules outside this prepared closure and /// sources removed by discovery exclusions. The required floor folds the one modeled /// discovery producer over this full population before classifying each resulting identity. + /// + /// IT IS MOVED OUT, NOT READ IN PLACE, and the field is empty for the rest of the run. Out-of- + /// closure sources are held by nothing else — the prepared graph is the gate closure — so + /// these `Rc`s are the only thing keeping the rest of the corpus alive, and leaving them here + /// would restore corpus-scale retention across the longest phase of the program. That is + /// growth in the lane `v2.workflow.required_floor` `RequiredFloorGrowthBudgetStanding` + /// records as having no measured memory margin, so it owes a named payment; taking the field + /// and dropping it when the fold ends is the alternative to owing one. See the `std::mem::take` + /// in `run_required_floor`'s discovery-authority phase. pub full_inventory: Vec, /// Modules that reached the requested closure but preparation excluded, paired with the /// exact substring that matched. Absence from both this map and `inventory` means outside diff --git a/src/v1/stage0/src/cli_run/required_floor_runner.rs b/src/v1/stage0/src/cli_run/required_floor_runner.rs index 98ce7dd7754..5ad377b5c07 100644 --- a/src/v1/stage0/src/cli_run/required_floor_runner.rs +++ b/src/v1/stage0/src/cli_run/required_floor_runner.rs @@ -2351,7 +2351,7 @@ pub fn run_required_floor( .map(|m| m.to_string()), ) .collect(); - let (prepared, prepared_sources) = prepare_repository_closure( + let (mut prepared, prepared_sources) = prepare_repository_closure( source_roots, &floor_prepared_subject_exclusions(), Some((&gate_entry_index, &closure_seeds)), @@ -2368,13 +2368,23 @@ pub fn run_required_floor( .map(|view| view.module_path.clone()) .collect(); let discovery_exclusions = prepared.discovery_exclusions.clone(); - let discovery_sources: Vec = prepared - .full_inventory - .iter() + // THE FULL INVENTORY IS MOVED OUT, NOT BORROWED, AND IT DIES WITH THE FOLD IT FEEDS. + // + // Out-of-closure sources are held by NOTHING else: the prepared graph is the gate closure, so + // these `Rc`s are the only thing keeping the rest of the corpus alive. Retaining + // them on `prepared` for the whole run would restore corpus-scale retention across the + // longest phase of the program, in the one lane `v2.workflow.required_floor` + // `RequiredFloorGrowthBudgetStanding` records as having NO MEASURED MEMORY MARGIN — growth + // there owes a named payment, and "the discovery fold needed the bytes for a moment" is not + // one. So `take` empties the field rather than cloning from it, and `discovery_sources` is + // dropped the moment the fold has produced its rows (below, at the `drop` beside `files`). + // What survives is the roster: paths, module names and function names, never bytes. + let discovery_sources: Vec = std::mem::take(&mut prepared.full_inventory) + .into_iter() .map(|view| FloorDiscoverySource { path: view.source.path.replace('\\', "/"), - module_path: view.module_path.clone(), - source: view.source.clone(), + module_path: view.module_path, + source: view.source, }) .collect(); let _floor_prepared_guard = register_floor_prepared_authority_guard(prepared_sources); @@ -2992,12 +3002,20 @@ pub fn run_required_floor( } } files.sort_by(|a, b| a.path.cmp(&b.path)); + let discovery_source_count = discovery_sources.len(); + // THE CORPUS IS RELEASED HERE. `module_for_path` borrowed from `discovery_sources`, so the + // drop waits for the last row to be classified and not one statement longer; every later + // consumer reads `files`, which carries names and no bytes. Same discipline the policy scope + // and the hermetic frame are dropped under further down: a value held across the fold that + // nothing reads during it has no defence. + drop(module_for_path); + drop(discovery_sources); eprintln!( "[floor-phase] phase=discovery-authority state=completed wall_ms={} authority={} \ sources={} rows={} entries={}", discovery_started.elapsed().as_millis(), FLOOR_DISCOVERY_AUTHORITY_MODULE, - discovery_sources.len(), + discovery_source_count, discovery_rows.len(), files.len() ); From d42fe4c238dcedd3876c3a5001616d50da9f6bc5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 29 Aug 2026 19:39:14 +0000 Subject: [PATCH 7/7] Bound the full-index retention structurally and measure its release on the run's own line; land the hand-Rust receipt as a census row (review 57430) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit F1: FloorDiscoverySource is deleted — the discovery fold consumes the prepared full-index views by value and the phase completion line prints full_inventory_release_rss_kb_before/_trim_reclaimed_kb/_rss_kb_after through the floor's existing statm/malloc_trim instruments. F2: gunbc.floor_population_projection_seed_growth, enrolled in gunbc.seed_growth_admission seed_growth_justification_roster — the row the census reads, replacing the plan-doc prose. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01W8rhnmQBDG3wYA317b9f5F --- ...loor_population_projection_seed_growth.dag | 41 ++++++++++++ dag/gunbc/seed_growth_admission.dag | 2 + docs/plans/witness-execution-closure.md | 21 +++--- .../src/cli_run/required_floor_runner.rs | 65 ++++++++++--------- 4 files changed, 87 insertions(+), 42 deletions(-) create mode 100644 dag/gunbc/floor/floor_population_projection_seed_growth.dag diff --git a/dag/gunbc/floor/floor_population_projection_seed_growth.dag b/dag/gunbc/floor/floor_population_projection_seed_growth.dag new file mode 100644 index 00000000000..31d0e75aaad --- /dev/null +++ b/dag/gunbc/floor/floor_population_projection_seed_growth.dag @@ -0,0 +1,41 @@ +module gunbc.floor_population_projection_seed_growth + +import gunbc.roadmap_model { RoadmapNodeId } +import gunbc.seed_growth { SeedGrowthJustification } +import std.decl_ref { DeclarationRef, WholeDeclaration } + +// FORWARD-FREEZE RECEIPT for the floor-population projection: the required floor folding the one +// modeled discovery authority (v2.workflow.floor_discovery_producer) over preparation's FULL +// module index and joining every DECLARED witness identity to exactly one disposition through +// reconcile_identity_population. The modeled authority is the producer's per-file fold plus +// v2.workflow.required_floor required_floor_site_disposition; the Rust below transports values +// between them and decides nothing. +// +// THE ITEM DELTA IS ONE AND THE LINE DELTA IS NOT, the same split gunbc.floor_cost_debt_seed_growth +// records and for the same reason: quoting only items understates the review surface (~480 diff +// lines across v1_compiler.cli_run and its required-floor runner), quoting only lines misreports +// what the admission join measures. At item grain the change RENAMES AND GENERALIZES +// reconcile_terminal_ledger into reconcile_identity_population -- the old name is deleted in the +// same change, so the seam count of identity joins stays one -- and everything else is arms and +// fields inside declarations that already existed (DeclinedDiscoveryExcluded and +// DeclinedOutsideGateClosure on RequiredFloorDisposition, full_inventory and discovery_exclusions +// on PreparedRepository/PreparedSubject, the fold-and-classify body inside run_required_floor), +// which gunbc.seed_growth_admission classifies ExistingSeedItemModified. Test scope adds the +// calibration pair (a_dropped_identity_replaced_by_a_duplicate_is_caught_while_the_count_partition_holds, +// a_disposition_for_an_undeclared_identity_is_foreign) and two test-local helpers, enumerated here +// in prose because they live inside a cfg(test) module and are evidence, not production surface. +// +// THE REWORK AFTER review 57430 NETS THE SEED SMALLER AT THIS BOUNDARY: FloorDiscoverySource, the +// intermediate transport struct that Rc-cloned every full-index view into a second vector, is +// DELETED -- the discovery fold consumes the prepared full-index views directly and drops them +// inside its own phase, whose completion line measures the release +// (full_inventory_release_rss_kb_before / _trim_reclaimed_kb / _rss_kb_after). +data floor_population_projection_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification { + hand_authored_declarations: [ + DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "reconcile_identity_population", field: WholeDeclaration } + ], + reason: "WHY RUST IS STILL NEEDED: the required floor executes in the seed, and the seam this change repairs is the seed's own projection of the modeled discovery fold into disposition rows -- a Rust-to-Rust seam the substrate cannot yet observe, because no emitted workflow performs repository acquisition or invokes the producer over the full index. The count-equality check it replaces was Rust; the identity join that replaces it must stand at the same boundary or the boundary keeps the weaker check. reconcile_identity_population is reconcile_terminal_ledger generalized from one seam's row type to identities, so the terminal-ledger join and the disposition join are one function asked at two seams rather than two loops that can drift (DESIGN section 3); the old name is deleted in the same change.\n\nWHAT IS NOT GROWN: no discovery policy, no roster, no status vocabulary. The declared population comes from v2.workflow.floor_discovery_producer's per-file fold over preparation's full module index; the two new decline arms are variants on the pre-existing RequiredFloorDisposition enum; the decline counters are derived from the rows rather than accumulated beside them.\n\nRETENTION, BOUNDED AND MEASURED (review 57430): the full-index source views are moved out of the prepared repository before the guard is installed and consumed by value inside the discovery-authority phase; the intermediate FloorDiscoverySource vector is deleted rather than scoped; and the phase's completion line prints rss before the drop, the malloc_trim reclaim, and rss after, through the floor's existing statm/trim instruments -- so the run itself states that the outside-closure bytes end with the phase, against v2.workflow.required_floor RequiredFloorGrowthBudgetStanding rather than silently beside it.\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits work serving the v2 self-host program. The floor's partition check was a count equality over a universe that had already narrowed -- the exact silent-wrongness class DESIGN section 5 names (completeness is an identity join, not a count equality) -- and the floor is the instrument the self-host program gates on. No language behavior, no compatibility route, no escape hatch, no seed feature, no emitted public surface.\n\nHAND-ITEM DELTA: +1/-1 production (the generalization above), -1 in the rework (FloorDiscoverySource deleted), +4 test-scope (the calibration pair and its two local helpers). HAND-LOC DELTA AT THIS RECEIPT: src/v1/stage0/src/cli_run.rs and src/v1/stage0/src/cli_run/required_floor_runner.rs roughly +480 net against origin/main, src/v1/stage0/src/bin/claim_executor.rs +16/-9 adding no declaration. The item observation producer named by gunbc.seed_growth_admission is not invoked by any required phase, so these diff-derived figures are review evidence rather than a mechanically joined admission, and this receipt says so rather than presenting them as measured by the join.", + owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, + trigger: "Delete the seed declaration when the self-emitted workflow performs repository acquisition and invokes v2.workflow.floor_discovery_producer over the full index itself, so the declared-population join is the modeled reconciliation consuming modeled rows and the hand transport disappears with the v1 floor bridge (docs/plans/cli-run-hollowing-plan.md reaching the required-floor orchestration phase). NOT retired by the join going green on any number of runs: a green join still needs the seam it guards, and only the seam moving into the substrate ends the obligation.", + current_boundary: "v2.workflow.floor_discovery_producer discover_floor_rows_for_source -> v1_compiler.cli_run run_required_floor (fold, classify, disposition rows) -> v1_compiler.cli_run reconcile_identity_population -> v2.workflow.required_floor required_floor_site_disposition" +} diff --git a/dag/gunbc/seed_growth_admission.dag b/dag/gunbc/seed_growth_admission.dag index 97525f2c888..ecb418108a8 100644 --- a/dag/gunbc/seed_growth_admission.dag +++ b/dag/gunbc/seed_growth_admission.dag @@ -45,6 +45,7 @@ import gunbc.stage0_rust_host_observation { stage0_rust_observation_seed_growth_ import gunbc.floor_non_verdict_enrollment { floor_non_verdict_seed_growth_justification } import gunbc.floor_route_gap_seed_growth { floor_route_gap_seed_growth_justification } import gunbc.floor_cost_debt_seed_growth { floor_cost_debt_seed_growth_justification } +import gunbc.floor_population_projection_seed_growth { floor_population_projection_seed_growth_justification } import gunbc.whole_corpus_compile_admission { whole_corpus_compile_seed_growth_justification } import std.decl_ref { DeclarationRef, WholeDeclaration } import std.disposition { Disposition } @@ -151,6 +152,7 @@ fn seed_growth_justification_roster() -> List { floor_non_verdict_seed_growth_justification, floor_route_gap_seed_growth_justification, floor_cost_debt_seed_growth_justification, + floor_population_projection_seed_growth_justification, stage0_rust_observation_seed_growth_justification, observation_scoped_run_seed_growth_justification(), whole_corpus_compile_seed_growth_justification, diff --git a/docs/plans/witness-execution-closure.md b/docs/plans/witness-execution-closure.md index 034edb16ade..39d226d6777 100644 --- a/docs/plans/witness-execution-closure.md +++ b/docs/plans/witness-execution-closure.md @@ -249,17 +249,16 @@ run's own, not this document's: `required-floor: declared=… offered=… declin ### What changed -**Hand-Rust receipt.** This change adds zero Rust declarations. It modifies the existing -`PreparedRepository`, `PreparedSubject`, `assemble_prepared_subject_closure`, -`prepare_repository_closure`, and `run_required_floor` items to transport full-index source views -into the already-modeled discovery producer, then drops those views before claim execution. Rust -is still necessary only at the v1 host boundary that owns repository acquisition and invokes the -interpreter; it defines neither the declaration grammar nor discovery policy. The owning ROADMAP -row is `v1-hand-queue-drain`. The concrete deletion trigger is that row's emitted-v2 replacement -of required-floor orchestration: when repository acquisition and producer invocation are -performed by the emitted workflow, these five seed modifications delete with the host rather than -moving into another Rust census. This is an explicit deferral of the transport boundary, not a -claim that the modified hand-Rust surface is generated or already dissolved. +**Hand-Rust receipt.** The receipt is a roster row, not this paragraph: +`gunbc.floor_population_projection_seed_growth`, enrolled in +`gunbc.seed_growth_admission seed_growth_justification_roster` — item delta, admitted +modifications, owning lane (`v1-hand-queue-drain`), dissolution trigger, and the boundary chain +live there, where the census reads them. **Full-index retention (review 57430):** the discovery +fold consumes the prepared full-index views by value inside its own phase — the intermediate +`FloorDiscoverySource` vector is deleted — and the phase's completion line prints +`full_inventory_release_rss_kb_before` / `_trim_reclaimed_kb` / `_rss_kb_after` through the +floor's existing statm/malloc_trim instruments, so the run itself states that outside-closure +bytes end with the phase rather than surviving into claim execution. 1. **The universe is the declared population, answered by one authority.** The floor folds `v2.workflow.floor_discovery_producer` (`discover_floor_rows_for_source`) over preparation's diff --git a/src/v1/stage0/src/cli_run/required_floor_runner.rs b/src/v1/stage0/src/cli_run/required_floor_runner.rs index 3052ed35a9f..ca0548324e8 100644 --- a/src/v1/stage0/src/cli_run/required_floor_runner.rs +++ b/src/v1/stage0/src/cli_run/required_floor_runner.rs @@ -1947,14 +1947,6 @@ pub(crate) fn floor_cgroup_dir() -> String { .clone() } -/// One prepared source handed to the `.dag` discovery authority: its repo-relative path, its -/// authored module name, and the bytes preparation already holds. -struct FloorDiscoverySource { - path: String, - module_path: String, - source: Rc, -} - /// One entry's enrolled witness names, exactly as `v2.workflow.floor_discovery_producer` /// answered them; the site-projection loop's unit. struct FloorDiscoveryFile { @@ -2367,22 +2359,15 @@ pub fn run_required_floor( .iter() .map(|view| view.module_path.clone()) .collect(); - // BOUNDED RETENTION, NOT A CORPUS COPY HELD FOR THE CLAIM RUN. The full-index views exist - // only until the modeled discovery fold consumes them. Taking them out of `prepared` makes - // that lifetime structural: the outside-closure source bytes cannot survive into claim - // execution through the repository value every later phase borrows. + // BOUNDED RETENTION, NOT A CORPUS COPY HELD FOR THE CLAIM RUN. The full-index views are + // taken OUT of `prepared` here and consumed, by value, inside the discovery-authority phase + // below — no second vector is built from them, and the phase drops them before the claim + // roster exists. Taking them out of `prepared` makes the lifetime structural: the + // outside-closure source bytes cannot survive into claim execution through the repository + // value every later phase borrows, and the discovery phase's own completion line measures + // the release (review 57430). let discovery_exclusions = std::mem::take(&mut prepared.discovery_exclusions); let full_inventory = std::mem::take(&mut prepared.full_inventory); - let discovery_sources: Vec = full_inventory - .iter() - .map(|view| FloorDiscoverySource { - path: view.source.path.replace('\\', "/"), - module_path: view.module_path.clone(), - source: view.source.clone(), - }) - .collect(); - let discovery_source_count = discovery_sources.len(); - drop(full_inventory); let _floor_prepared_guard = register_floor_prepared_authority_guard(prepared_sources); // WARM THE MODULE-PATH INDEX HERE, because otherwise ONE ARBITRARY CLAIM PAYS FOR IT. // @@ -2929,11 +2914,15 @@ pub fn run_required_floor( floor_seam("discovery-authority"); let discovery_started = std::time::Instant::now(); let producer_frame = floor_authority_frame(&prepared, FLOOR_DISCOVERY_AUTHORITY_MODULE)?; + let discovery_source_count = full_inventory.len(); let mut discovery_outcomes: Vec = - Vec::with_capacity(discovery_sources.len()); - for src in &discovery_sources { + Vec::with_capacity(full_inventory.len()); + for src in &full_inventory { let args = [ - (Some("repo_path".to_string()), str_value(src.path.clone())), + ( + Some("repo_path".to_string()), + str_value(src.source.path.replace('\\', "/")), + ), ( Some("content".to_string()), str_value(src.source.content.clone()), @@ -2949,7 +2938,7 @@ pub fn run_required_floor( format!( "REQUIRED-FLOOR REFUSAL cause=FloorDiscoveryAuthorityUnevaluable source={} — \ discover_floor_rows_for_source: {e}", - src.path + src.source.path.replace('\\', "/") ) })?; discovery_outcomes.push(outcome); @@ -2975,9 +2964,9 @@ pub fn run_required_floor( })?; // Rows are (entry, function); the disposition loop below needs the entry's AUTHORED module // name, which preparation read off the `module` line and holds beside the same path. - let module_for_path: std::collections::HashMap<&str, &str> = discovery_sources + let module_for_path: std::collections::HashMap = full_inventory .iter() - .map(|src| (src.path.as_str(), src.module_path.as_str())) + .map(|src| (src.source.path.replace('\\', "/"), src.module_path.as_str())) .collect(); let mut files: Vec = Vec::new(); for row in &discovery_rows { @@ -2998,16 +2987,30 @@ pub fn run_required_floor( } } drop(module_for_path); - drop(discovery_sources); + // THE RELEASE IS MEASURED IN THE SAME MOTION AS IT HAPPENS, by exclusive drop against the + // existing statm/malloc_trim instruments rather than a new one: rss before, drop the full + // inventory (whose outside-closure `Rc` bytes have no other owner once the + // gate-cut index discarded them), trim the freed-but-retained arena, rss after. What the + // trim gives back after this drop is exactly the full-index retention this phase held; a + // reader of the run therefore sees the retention's size and its end on the phase's own + // line, instead of trusting a comment that the bytes were dropped (review 57430). + let full_inventory_rss_kb_before = floor_sampled_field(floor_statm_rss_kb()); + drop(full_inventory); + let full_inventory_trim_reclaimed_kb = floor_sampled_field(trim_retained_heap()); + let full_inventory_rss_kb_after = floor_sampled_field(floor_statm_rss_kb()); files.sort_by(|a, b| a.path.cmp(&b.path)); eprintln!( "[floor-phase] phase=discovery-authority state=completed wall_ms={} authority={} \ - sources={} rows={} entries={}", + sources={} rows={} entries={} full_inventory_release_rss_kb_before={} \ + full_inventory_release_trim_reclaimed_kb={} full_inventory_release_rss_kb_after={}", discovery_started.elapsed().as_millis(), FLOOR_DISCOVERY_AUTHORITY_MODULE, discovery_source_count, discovery_rows.len(), - files.len() + files.len(), + full_inventory_rss_kb_before, + full_inventory_trim_reclaimed_kb, + full_inventory_rss_kb_after ); let files = &files; // THE COST-DEBT ROSTER, decoded before the claim-build loop below because it decides an