REWORK #9684 after review 57430 (REQUEST_CHANGES): bound the full-corpus retention or declare its payment; add the hand-Rust receipt

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,31 +364,76 @@ 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 {
         offered: counts.offered + 1,
         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 {
         offered: counts.offered + 1,
         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 {
         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 + 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
       }
   }
 }

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"
+}

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<SeedGrowthJustification> {
     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,

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
   }

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