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/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/dag/test/claim/discovery_census_witness_test.dag b/dag/test/claim/discovery_census_witness_test.dag index 50fcbd93854..0a18f3d9a0b 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,9 @@ 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 DeclinedLongModule { matched_prefix: _ } => false DeclinedFixtureMember { matched_prefix: _ } => false @@ -333,6 +356,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 +376,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/dag/test/claim/scm/scm_repository_envelope_witness_test.dag b/dag/test/claim/scm/scm_repository_envelope_witness_test.dag index 0cbab737d5d..4442dc6d16d 100644 --- a/dag/test/claim/scm/scm_repository_envelope_witness_test.dag +++ b/dag/test/claim/scm/scm_repository_envelope_witness_test.dag @@ -61,7 +61,7 @@ import gunbc.scm.repository_envelope { // THIS DECLARATION DOES NOT CHANGE WHETHER THESE CLAIMS EXECUTE, AND TWO EARLIER REVISIONS OF THIS // ANNOTATION SAID IT DID. Both are retracted here against the source rather than against a rerun. // -// THE FLOOR'S AUTOMATIC ROUTE IS A COLUMN-ZERO TEXT SCAN (`witness_file_from_source`, v1 seed): +// THE FLOOR'S AUTOMATIC ROUTE WAS A COLUMN-ZERO TEXT SCAN (former v1 seed scanner): // a line must `starts_with("data ")` AND contain BOTH `LiveTreeDisposition` AND `ReadsLiveTree`. // An undeclared module matches nothing, so `reads_live_tree` is false and the module is ROUTED. // A module declaring SubstrateInputsOnly also matches nothing -- the second token is absent -- so it diff --git a/docs/plans/witness-execution-closure.md b/docs/plans/witness-execution-closure.md index 5e54b55d954..39d226d6777 100644 --- a/docs/plans/witness-execution-closure.md +++ b/docs/plans/witness-execution-closure.md @@ -12,7 +12,7 @@ This document is the finding and the receipt. The change itself is in ## The measurement -Counted with the floor's own rule (`cli_run` `witness_file_from_source`: a column-zero +Counted with the floor's former Rust scanner (a column-zero `test fn `, and a column-zero `data … LiveTreeDisposition … ReadsLiveTree`), on `4cec10f66a3`: | population | identities | files | @@ -59,7 +59,7 @@ did not need a new lane. It needed the stale prediction deleted. `reads_live_tree` was derived twice, by methods that cannot agree except by coincidence: -- `cli_run` `witness_file_from_source` — a **syntactic text scan** for the declaration line. +- the former `cli_run` floor scanner — a **syntactic text scan** for the declaration line. - `cli_run` `reads_live_tree_effective` — reads the same declaration, then falls through to `effect_reach_derived_reads_live_tree_for_entry`, a **semantic effect-reachability derivation** over the entry's import closure. @@ -218,3 +218,99 @@ 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 + +**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 + 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 + 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 ffd62e06fc5..c7fe811ee44 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -1171,15 +1171,21 @@ 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, \ - and no `*_test.dag` entry offered zero sites (v2.workflow.floor_discovery_producer \ - refuses a barren or misplaced sidecar upstream of this line)", + "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 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, 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 e12c5eb4223..adddfbde55b 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, @@ -35646,6 +35653,24 @@ pub struct PreparedRepository { pub subject_digest: String, pub modules_resolved: usize, pub modules_excluded: usize, + /// 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` and the measured release on the discovery-authority phase line + /// (`full_inventory_release_rss_kb_before` / `_trim_reclaimed_kb` / `_rss_kb_after`). + 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 + /// the prepared closure, keeping the two pre-offer dispositions distinguishable. + pub discovery_exclusions: HashMap, } /// Shared view of one admitted source. Holds the same `Rc` preparation already @@ -35803,6 +35828,8 @@ fn register_floor_prepared_authority_guard( pub struct PreparedSubject { pub sources: Vec>, pub inventory: Vec, + pub full_inventory: Vec, + pub discovery_exclusions: HashMap, pub subject_digest: String, pub modules_resolved: usize, pub modules_excluded: usize, @@ -35847,6 +35874,14 @@ pub fn assemble_prepared_subject_closure( closure: Option<(&MultiEntryIndex, &[String])>, ) -> Result { let full_index = build_module_index(source_roots); + let full_inventory: Vec = full_index + .iter() + .map(|(module_path, source)| PreparedSourceView { + module_path: module_path.clone(), + source: source.clone(), + }) + .collect(); + let mut discovery_exclusions: HashMap = HashMap::new(); let index: ModuleSourceIndex = match closure { None => full_index, Some((entry_index, prefixes)) => { @@ -35994,17 +36029,18 @@ 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())) { + discovery_exclusions.insert(module_path.clone(), matched.clone()); continue; } // WHICH `test` DECLS A SOURCE ENROLLS IS NOT DECIDED HERE. Preparation admits the // source and keeps its bytes beside its module name; the required floor hands both to // `v2.workflow.floor_discovery_producer` (`discover_floor_rows_for_source`), the one // authority for discovery, sidecar placement and barren sidecars. A Rust scan used to - // stand here (`witness_file_from_source`) and disagreed with that authority on + // stand here and disagreed with that authority on // placement — deleted, DESIGN §3. inventory.push(PreparedSourceView { module_path: module_path.clone(), @@ -36021,6 +36057,8 @@ pub fn assemble_prepared_subject_closure( Ok(PreparedSubject { sources, inventory, + full_inventory, + discovery_exclusions, subject_digest, modules_resolved, modules_excluded, @@ -36058,6 +36096,8 @@ pub fn prepare_repository_closure( let PreparedSubject { sources, inventory, + full_inventory, + discovery_exclusions, subject_digest, modules_resolved, modules_excluded, @@ -36071,6 +36111,8 @@ pub fn prepare_repository_closure( subject_digest, modules_resolved, modules_excluded, + full_inventory, + discovery_exclusions, }, inventory, )) @@ -36715,6 +36757,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` @@ -36854,6 +36913,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, @@ -37387,8 +37458,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; @@ -37396,6 +37482,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, @@ -37403,29 +37491,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}"))?; } @@ -37594,6 +37693,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] @@ -37625,7 +37801,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); @@ -37636,17 +37820,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" ); } @@ -37855,7 +38041,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 71a17c891dc..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 { @@ -2351,23 +2343,31 @@ 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)), )?; drop(gate_entry_index); - // THE PREPARED SOURCES THE DISCOVERY AUTHORITY WILL JUDGE, captured here because + // THE FULL INDEX THE DISCOVERY AUTHORITY WILL JUDGE, captured here because the prepared + // graph is intentionally only the required gate closure. Declaration discovery is a + // corpus-wide question: fold the one modeled producer over every indexed source, finalize + // once, then classify rows by whether preparation admitted their module. // `prepared_sources` is moved into the guard on the next line. Rc clones of what preparation // already holds -- path, module and bytes -- never a second corpus. - let discovery_sources: Vec = prepared_sources + let prepared_module_paths: HashSet = prepared_sources .iter() - .map(|view| FloorDiscoverySource { - path: view.source.path.replace('\\', "/"), - module_path: view.module_path.clone(), - source: view.source.clone(), - }) + .map(|view| view.module_path.clone()) .collect(); + // 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 _floor_prepared_guard = register_floor_prepared_authority_guard(prepared_sources); // WARM THE MODULE-PATH INDEX HERE, because otherwise ONE ARBITRARY CLAIM PAYS FOR IT. // @@ -2832,7 +2832,7 @@ pub fn run_required_floor( // interpreter, and again here in Rust, applying the same prefix test to explain the // difference between sites offered and claims returned. Between the two sat an interpreted // fold whose only product was a population this host could compute directly from facts it - // already held in `prepared.witness_files`. + // already returned by the modeled discovery producer. // // THE AUTHORED FACTS STAY AUTHORED. `long_home_prefixes`, the claim budget and the warn // threshold are still read from `v2.workflow.required_floor`, so the prefix list and both @@ -2844,11 +2844,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 @@ -2893,29 +2896,33 @@ pub fn run_required_floor( // ── the witness roster, as the `.dag` discovery authority answers it ────────────────── // // ONE AUTHORITY FOR "WHAT DOES THE FLOOR DISCOVER". The roster used to be projected by a - // Rust text scan (`witness_file_from_source`, deleted) that was filename-blind, while + // Rust text scan that was filename-blind, while // `v2.workflow.floor_discovery_producer` -- reached only by claim_batch -- refused a // `test`-marked decl outside a `*_test.dag` sidecar. Two answers to one question (DESIGN // section 3), measured on main 2026-08-29: five files, 39 test fns, refused on one path and // executed on the other. The floor now folds the producer's own per-file authority over the - // sources it prepared and takes that fold's rows as the roster; Rust threads values and + // full module index and takes that fold's rows as the declared roster; Rust threads values and // decides nothing. Every refusal the producer carries -- misplaced test decl, barren sidecar, // misplaced wire contract, malformed live_tree_disposition row -- therefore stops THIS line, // with the producer's own reason text. // - // The subject is the prepared inventory, not a filesystem walk: what the gate closure - // admitted is exactly what the fold judges, so an entry the floor could plan and an entry the - // authority never saw cannot come apart. Row admission (`witness_row_excluded_from_discovery`) + // The subject is preparation's full index, not a filesystem walk or a Rust declaration scan. + // The prepared closure and exclusion map then classify producer-returned identities without + // rebuilding the population. Row admission (`witness_row_excluded_from_discovery`) // is the discovery-corpus mode's policy and is deliberately NOT applied here -- see // `floor_discovery_row_admission_policy_note` in the producer. 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()), @@ -2931,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); @@ -2957,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 { @@ -2979,15 +2986,31 @@ pub fn run_required_floor( }), } } + drop(module_for_path); + // 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_sources.len(), + 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 @@ -3112,12 +3135,15 @@ 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(); + // 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(); let mut storage_agreement_rows: Vec = Vec::new(); @@ -3137,14 +3163,44 @@ 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" + )); + } + if !prepared_module_paths.contains(&file.module_path) { + let disposition = match discovery_exclusions.get(&file.module_path) { + Some(matched_substring) => { + RequiredFloorDisposition::DeclinedDiscoveryExcluded { + matched_substring: matched_substring.clone(), + } + } + None => RequiredFloorDisposition::DeclinedOutsideGateClosure, + }; + disposition_rows.push(RequiredFloorDispositionRow { + identity, + disposition, + }); + continue; + } + sites_offered += 1; 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 { @@ -3156,7 +3212,6 @@ pub fn run_required_floor( continue; } if let Some(prefix) = fixture_prefix { - fixture_declined += 1; disposition_rows.push(RequiredFloorDispositionRow { identity, disposition: RequiredFloorDisposition::DeclinedFixtureMember { @@ -3178,7 +3233,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 { @@ -3190,29 +3244,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, @@ -3228,8 +3273,24 @@ 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. + // 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. + // + // The modeled producer has already enumerated all identities from the full index. Rows whose + // modules preparation did not admit were classified in that same loop, so there is no second + // declaration scan or complement population to append here. `sites_offered` keeps its old + // meaning — identities inside the prepared subject — beside the corpus-wide `declared`. + // 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 @@ -3237,41 +3298,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. + // + // 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. // - // 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 + // 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 ); @@ -3758,6 +3875,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, @@ -4943,8 +5063,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 @@ -4979,7 +5099,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() @@ -5119,7 +5242,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)?; @@ -5136,6 +5263,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", } } @@ -5145,8 +5274,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/std/live_tree.dag b/src/v2/std/live_tree.dag index 390d2b970b2..ad0b6e8afaa 100644 --- a/src/v2/std/live_tree.dag +++ b/src/v2/std/live_tree.dag @@ -1,6 +1,6 @@ module v2.std.live_tree -data live_tree_disposition_note: String = "Declared witness input-domain disposition (ROADMAP 2-host-scaffold-classifier-defork): a witness entry declares whether its evaluation reads the live host tree (filesystem/corpus state outside its resolved substrate closure). The single authority is a `data live_tree_disposition: LiveTreeDisposition = ...` row in the WITNESS ENTRY FILE itself - entry grain, so the fact holds no matter where the read hides behind imports. This dissolves the interim floor:host_scaffold marker and the Rust text classifier witness_test_fn_uses_live_host_scan (deleted with this model). TWO CONSUMERS READ THIS FACT AND THEY DEFAULT SILENCE IN OPPOSITE DIRECTIONS, and an earlier revision of this row stated one of them as though it were the fact. WHAT IS TRUE: v1_compiler.cli_run parse_entry_live_tree_disposition, which feeds AFFECTED-SET SELECTION, treats an undeclared entry as ReadsLiveTree, so it never predict-skips. WHAT WAS OMITTED: v1_compiler.cli_run witness_file_from_source, the REQUIRED FLOOR's own scan and the consumer that decides whether a witness EXECUTES, fires only on a column-zero data line naming both LiveTreeDisposition and ReadsLiveTree - so on that path UNDECLARED MEANS EXECUTES. Neither reading is wrong on its own terms and that is exactly the section 3 defect: a fact with two authorities has none. The omission was load-bearing rather than cosmetic, because a reader consulting this row to answer *what happens to a witness that declares nothing* was told the fail-closed half and would conclude the witness is withheld, which is false of the consumer that runs it. A ROW THAT DECLARES SubstrateInputsOnly WHILE ACTUALLY READING LIVE STATE IS RE-CHECKED BY NOTHING, and this row previously said otherwise. It named *the nightly affected-set falsifier (predict-only cold run)* as the enforcement, promising that a lying row surfaces as a counted divergence within one cadence window. THAT CADENCE DOES NOT EXIST: falsifier.yml was deleted by the 2026-08-15 floor cut (gunbc#8283) and the repository carries three workflows, none of which runs a predict-only cold comparison. The sentence was true when written and became false when the cadence died, with nothing to notice - the stale-present-tense class DESIGN records, in an authority a reader consults first. THE SURVIVING BACKSTOP IS v2.std.effect_reach, AND IT IS NOT A SUBSTITUTE FOR THE DECLARATION. reads_live_tree_effective takes the declared answer first and falls through to effect_reach_derived_reads_live_tree_for_entry only when the row says SubstrateInputsOnly, so the derivation is the only thing standing between a lying row and a predict-skip. Its detection ceiling is declared at effect_reach_detection_ceiling and executed by the fixture pair effect_reach_conjunction_loses_a_closure_that_reads_with_no_path_literal: it classifies a closure as host-reading only when a repository path literal and a host-sink call shape BOTH occur somewhere in it, independently, so a closure that performs a real Filesystem.Read and names no path derives NOT-live. The consequence is the one that matters here and it runs the other way from the usual objection that an authored declaration duplicates a derivable fact: the derivation does not derive this fact, so the fail-closed undeclared default on the selection path is load-bearing rather than redundant, and replacing the declaration with the derivation would be a scope narrowing wearing a construction argument. STAMPING THE SILENT POPULATION WAS BUILT AND DROPPED, recorded here so the next reader does not re-propose it as though it were untried: the change existed in full - 520 witness files carrying no disposition row, each stamped, with silence made a typed located refusal on BOTH consumers so no default survived for them to disagree about - and it was discarded before review because the required floor's decline arm, the consumer that made a truthful ReadsLiveTree stamp cost anything, was already being deleted at its root in an open change. Hand-authoring 520 rows for a consumer scheduled to disappear is the redundant work DESIGN section 2 prices, and the ordering the brief assumed was backwards: the arm's deletion is what makes a truthful stamp free, so it is the enabling event and not the reward. WHAT WOULD REVIVE THE QUESTION is not the population growing but the SELECTION consumer acquiring an enforcement it does not have - if a lying SubstrateInputsOnly row can be caught again, what a silent file means becomes decidable and worth deciding; until then a stamp asserts a fact nothing checks." +data live_tree_disposition_note: String = "Declared witness input-domain disposition (ROADMAP 2-host-scaffold-classifier-defork): a witness entry declares whether its evaluation reads the live host tree (filesystem/corpus state outside its resolved substrate closure). The single authority is a `data live_tree_disposition: LiveTreeDisposition = ...` row in the WITNESS ENTRY FILE itself - entry grain, so the fact holds no matter where the read hides behind imports. This dissolves the interim floor:host_scaffold marker and the Rust text classifier witness_test_fn_uses_live_host_scan (deleted with this model). TWO CONSUMERS READ THIS FACT AND THEY DEFAULT SILENCE IN OPPOSITE DIRECTIONS, and an earlier revision of this row stated one of them as though it were the fact. WHAT IS TRUE: v1_compiler.cli_run parse_entry_live_tree_disposition, which feeds AFFECTED-SET SELECTION, treats an undeclared entry as ReadsLiveTree, so it never predict-skips. WHAT WAS OMITTED: the REQUIRED FLOOR's former Rust scan, the consumer that decided whether a witness EXECUTES, fired only on a column-zero data line naming both LiveTreeDisposition and ReadsLiveTree - so on that path UNDECLARED MEANT EXECUTES. Neither reading was wrong on its own terms and that is exactly the section 3 defect: a fact with two authorities has none. The omission was load-bearing rather than cosmetic, because a reader consulting this row to answer *what happens to a witness that declares nothing* was told the fail-closed half and would conclude the witness was withheld, which was false of the consumer that ran it. A ROW THAT DECLARES SubstrateInputsOnly WHILE ACTUALLY READING LIVE STATE IS RE-CHECKED BY NOTHING, and this row previously said otherwise. It named *the nightly affected-set falsifier (predict-only cold run)* as the enforcement, promising that a lying row surfaces as a counted divergence within one cadence window. THAT CADENCE DOES NOT EXIST: falsifier.yml was deleted by the 2026-08-15 floor cut (gunbc#8283) and the repository carries three workflows, none of which runs a predict-only cold comparison. The sentence was true when written and became false when the cadence died, with nothing to notice - the stale-present-tense class DESIGN records, in an authority a reader consults first. THE SURVIVING BACKSTOP IS v2.std.effect_reach, AND IT IS NOT A SUBSTITUTE FOR THE DECLARATION. reads_live_tree_effective takes the declared answer first and falls through to effect_reach_derived_reads_live_tree_for_entry only when the row says SubstrateInputsOnly, so the derivation is the only thing standing between a lying row and a predict-skip. Its detection ceiling is declared at effect_reach_detection_ceiling and executed by the fixture pair effect_reach_conjunction_loses_a_closure_that_reads_with_no_path_literal: it classifies a closure as host-reading only when a repository path literal and a host-sink call shape BOTH occur somewhere in it, independently, so a closure that performs a real Filesystem.Read and names no path derives NOT-live. The consequence is the one that matters here and it runs the other way from the usual objection that an authored declaration duplicates a derivable fact: the derivation does not derive this fact, so the fail-closed undeclared default on the selection path is load-bearing rather than redundant, and replacing the declaration with the derivation would be a scope narrowing wearing a construction argument. STAMPING THE SILENT POPULATION WAS BUILT AND DROPPED, recorded here so the next reader does not re-propose it as though it were untried: the change existed in full - 520 witness files carrying no disposition row, each stamped, with silence made a typed located refusal on BOTH consumers so no default survived for them to disagree about - and it was discarded before review because the required floor's decline arm, the consumer that made a truthful ReadsLiveTree stamp cost anything, was already being deleted at its root in an open change. Hand-authoring 520 rows for a consumer scheduled to disappear is the redundant work DESIGN section 2 prices, and the ordering the brief assumed was backwards: the arm's deletion is what makes a truthful stamp free, so it is the enabling event and not the reward. WHAT WOULD REVIVE THE QUESTION is not the population growing but the SELECTION consumer acquiring an enforcement it does not have - if a lying SubstrateInputsOnly row can be caught again, what a silent file means becomes decidable and worth deciding; until then a stamp asserts a fact nothing checks." data live_tree_disposition_stamp_provenance: String = "Migration stamp provenance (2026-07-11, machine-stamped batch): the initial corpus-wide SubstrateInputsOnly rows were stamped from the deleted entry-text classifier's verdict (entry file contains none of: floor:host_scaffold, layer_import_facts, _live(, _facts_live(, filesystem_read) - ENTRY-TEXT GRAIN, so they inherit that classifier's declared blind spot: a live read hidden behind an import was invisible to it (the former cli_run.rs cross-file deficit). A stamped row is therefore machine-vouched, not author-vouched. ENFORCEMENT: NONE. This row named the nightly affected-set falsifier (counted divergence within one cadence window) as what catches a wrong stamp; falsifier.yml was deleted by the 2026-08-15 floor cut and nothing replaced it, so the sentence was true when written and became false when the workflow died. THE CONSEQUENCE IS SPECIFIC TO THIS ROW AND IS WHY IT MATTERS MORE THAN THE PROSE FIX: the batch below is MACHINE-vouched rather than author-vouched, and it inherits the deleted classifier's declared blind spot - a live read hidden behind an import was invisible to entry-text scanning. So every stamp carrying that blind spot was admitted on the promise that a cadence would catch it if wrong, and that promise is now UNMET rather than merely unfulfilled: no consumer verifies a stamp, and a stamp that was wrong on the day it was written is still wrong and still unobserved. The surviving derivation is not the catcher either - reads_live_tree_effective reaches v2.std.effect_reach only for a row already claiming SubstrateInputsOnly, and that classifier's own ceiling row files three bounds on what it can detect. Dissolves-at: G2 call-reachability live-read classification (import-closure walk over LiveReadCarrier registry + fn-arrow DependencyView) per docs/plans/live-read-witness-classification-design.md — when stamps can be re-derived from proven runtime-read closure." diff --git a/src/v2/workflow/floor_discovery_producer.dag b/src/v2/workflow/floor_discovery_producer.dag index d33b4bd6e21..65cc299de13 100644 --- a/src/v2/workflow/floor_discovery_producer.dag +++ b/src/v2/workflow/floor_discovery_producer.dag @@ -525,7 +525,7 @@ fn floor_discovery_apply_wire_contract_sidecar_rules( // prepared inventory (cli_run required_floor_runner) // // Before this seam existed the required floor enrolled its roster from a SECOND scanner in Rust -// (cli_run.rs witness_file_from_source), filename-blind, so a `test`-marked decl outside a +// (the former cli_run.rs floor scanner), filename-blind, so a `test`-marked decl outside a // sidecar was refused on the claim_batch path and executed on the floor -- two authorities for // one fact (DESIGN section 3), measured on main 2026-08-29: five files, 39 test fns. That scanner // is deleted; the floor's roster is this fold's answer. diff --git a/src/v2/workflow/floor_naming_hygiene.dag b/src/v2/workflow/floor_naming_hygiene.dag index c2afb22a717..6c7110b101a 100644 --- a/src/v2/workflow/floor_naming_hygiene.dag +++ b/src/v2/workflow/floor_naming_hygiene.dag @@ -161,7 +161,7 @@ fn floor_discovery_scan_test_decl_names(content: String) -> List { // <- discover_floor_witness_roster, whose entire caller // set is claim_batch and the discovery-corpus mode // cli_run.rs scan_test_decl_lines `test fn ` / `test data ` -// cli_run.rs witness_file_from_source `test fn ` / `test data ` -- and THIS is the required +// former cli_run.rs floor scanner `test fn ` / `test data ` -- and THIS is the required // floor's roster, via assemble_prepared_subject. It read // `test fn ` ONLY until the repair recorded below; that // divergence is what forked this one fact three ways @@ -176,7 +176,7 @@ fn floor_discovery_scan_test_decl_names(content: String) -> List { // home and only its consumer moved. // // WHAT LANDED NEXT (2026-08-29), AND IT RETIRES THE ROSTER ROW ABOVE: cli_run.rs -// witness_file_from_source is DELETED. The required floor no longer scans at all -- it folds +// The Rust floor scanner is DELETED. The required floor no longer scans at all -- it folds // v2.workflow.floor_discovery_producer discover_floor_rows_for_source over its prepared sources // and takes that fold's rows as its roster, so the barren check, the placement rule and the scan // reach the floor through ONE consumer of this module. The measured fork that forced it: the @@ -188,7 +188,7 @@ fn floor_discovery_scan_test_decl_names(content: String) -> List { // that does not exist yet. // // THAT SEPARATE REPAIR HAS LANDED, and the population it named is the population it closed. -// witness_file_from_source recognised `test fn ` and not `test data `, so every `test data` +// The old Rust scanner recognised `test fn ` and not `test data `, so every `test data` // claim was dropped from the required floor's roster -- including from files the floor // otherwise enrolled. Measured over both source roots at 3bbd53c05a and re-measured unchanged // when the repair landed: 40 decls in 15 files (34 in 13 files carrying no `test fn` at all, 6 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..00ee6945f7c 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,23 +58,44 @@ 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 -// blockers were closed before this root deletion. The `witness_file_from_source` scan remains: -// live-tree disposition still feeds affected-set eligibility even though it no longer gates +// blockers were closed before this root deletion. The live-tree disposition remains: +// it still feeds affected-set eligibility even though it no longer gates // floor admission. // // A NOTE ON WHAT DID *NOT* MOVE: `live_tree_disposition` itself is not deleted and is not // 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.