Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
86 changes: 86 additions & 0 deletions dag/gunbc/floor_arm_set_consumer_seed_growth.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,86 @@
module gunbc.floor_arm_set_consumer_seed_growth

import gunbc.roadmap_model { RoadmapNodeId }
import gunbc.seed_growth { SeedGrowthJustification }
import std.decl_ref { DeclarationRef, WholeDeclaration }

// FORWARD-FREEZE RECEIPT for the hand Rust that makes the required floor honest on the
// stale-match class (gunbc#11194; gunbc#11256, restoring gunbc#11252's invocation half and adding
// the dependents half on top of it). gunbc.seed_growth_admission
// seed_growth_forward_freeze_policy_note makes unenumerated hand growth in src/v1 a stop-line,
// so every added declaration is enumerated below; modified items keep their names and are not
// netted (ExistingSeedItemModified: ModuleDeclarationRecord, collect_reference_occurrences and
// record_from_module in declaration_index.rs; run_required_wave_admission; run_required_floor
// and changed_and_enrolled_witness_identities_with_index; assemble_prepared_subject_closure and
// prepare_repository_closure; the two run_required_floor call sites in bin/claim_executor.rs).
//
// WHY IT IS ADMITTED AGAINST THE v1 FREEZE, BY PURPOSE. gunbc.v1_maintenance_standing
// v1_seed_standing admits a change when it serves the v2 self-host program, and the required floor
// is the INSTRUMENT that guards that program. Today `check_match` refuses a non-exhaustive match
// under `gunbc compile` and on NO required lane: the floor prepares the gate closure plus what the
// diff names, so a match that goes stale because its coproduct grew an arm in another module has
// an empty diff at the match site and is never Strict-prepared. gunbc#11194 was caught by a person
// reading arms. This change makes a real wall reachable on the required path for that class, in
// both of its directions, through the ONE preparation the floor already runs -- no second
// checker, no second Strict path, no builtin, no admission row, no public export.
//
// WHY IT IS RUST AND NOT .dag. The consumption relation is `declaring_candidates` over
// `ModuleDeclarationRecord`, a host-only carrier (gunbc.declaration_index_seed_growth CLASS A:
// the input type is host Rust and there is no .dag per-module record yet). The selector is a pure
// fold over two of those indexes and FOLLOWS that carrier's migration rather than forking it. The
// base side is reconstructed from git blobs, which is the scm lane's acquisition boundary (CLASS
// B). The DECISIONS the selector makes are modeled in v2.workflow.floor_subject_seed
// (`arm_set_match_read_disposition`, `arm_set_match_consumer_binding`, the seed grounds and the
// typed out-of-root dispositions), and the host is their wire rendering.
//
// HAND-ITEM DELTA is derived from the diff by gunbc.rust_item_host_observation and is not
// restated here. The test items are enumerated because they are hand declarations in the seed;
// the executed red among them is arm_growth_selects_the_untouched_match_consumer_and_strict_
// preparation_refuses_it, the #11194 shape end to end, with its positive control beside it.
data floor_arm_set_consumer_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef { module_path: "v1_compiler.namespace_wave_admission", decl_name: "BaselineReconstruction", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.namespace_wave_admission", decl_name: "reconstruct_base_index", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.namespace_wave_admission", decl_name: "ArmSetChange", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.namespace_wave_admission", decl_name: "ArmConsumerBinding", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.namespace_wave_admission", decl_name: "ArmSetMatchConsumer", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.namespace_wave_admission", decl_name: "ArmSetConsumerSelection", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.namespace_wave_admission", decl_name: "arm_set_changed_match_consumers", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "module_name_is_or_is_contained_by", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "FloorDiffProjections", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "CompileSubjectSeeds", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "ArmSetConsumerPlanning", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "arm_set_consumer_planning", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "module_seeds_from_touched_entry_files", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "floor_source_roots_workspace_relative", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "path_under_floor_roots", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "helper_fn_file_seeds_its_authored_module", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "helper_fn_file_outside_floor_roots_is_a_typed_disposition_not_a_seed", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "helper_fn_file_without_module_header_refuses_rather_than_skipping", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "ARM_X_BASE", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "ARM_X_HEAD", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "ARM_Y", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "ARM_W", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "ARM_Z", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "REC_BASE", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "REC_HEAD", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "REC_USER", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "WORKSPACE_CWD", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "enter_workspace_cwd", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "leave_workspace_cwd", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "arm_set_fixture", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "arm_set_index", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "arm_set_selection", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "consumers_of", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "arm_growth_selects_the_untouched_match_consumer_and_strict_preparation_refuses_it", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "arm_growth_consumer_with_a_wildcard_is_planned_and_prepares_clean", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "a_type_change_with_no_match_consumers_plans_nothing_extra", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "a_diff_with_no_arm_set_change_plans_nothing_extra", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "arm_removal_selects_the_consumer_that_still_names_the_arm", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner.changed_witness_projection_tests", decl_name: "a_module_seed_is_segment_bounded", field: WholeDeclaration }
],
reason: "A required floor that never Strict-prepares an untouched module cannot run check_match on it, so a coproduct growing an arm elsewhere makes an exhaustive match silently stale (gunbc#11194). Two halves: seed the touched module (dependency direction, gunbc#11252) and seed the match-bearing consumers of a coproduct whose arm set changed between the floor's own resolved diff base and head (dependents direction), derived from the wave-admission consumption relation -- declaring_candidates over the parse phase's DeclarationIndex, lifted by two record fields (per-coproduct arm sets, match-arm constructor occurrences) and never a second relation -- and prepared through the SAME closure path. reconstruct_base_index is the wall's own base-side reconstruction lifted so both callers share it, parametrised on the window because the wall compares against the merge base with origin/main and the floor against v2.workflow.floor_diff_observe's baseline. module_name_is_or_is_contained_by is the segment-bounded rule for module-name seeds (a.b seeds a.b and a.b.c, never a.bc); gate PREFIXES stay textual as site disposition reads them. Out-of-root touched files and consumers are typed rows, not counts.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "The selector, its records and the planning enum follow gunbc.declaration_index_seed_growth's first step: the moment the per-module declaration record is a .dag carrier, arm_set_changed_match_consumers is an ordinary fold over it beside declaring_candidates and moves with them, and v2.workflow.floor_subject_seed consumes it directly instead of being mirrored. reconstruct_base_index follows the scm lane with git_stdout and base_records: when a typed repository-read transport can supply a file's text at a ref. The seed-list plumbing in run_required_floor and module_name_is_or_is_contained_by dissolve when preparation is a modeled operation over PreparedSubjectSeedGround rather than two string lists. The tests are the evidence and retire only as regression controls when the wall climbs; a fixture that greens when the invocation lands flips to a permanent control, it does not retire.",
current_boundary: "Reachable only from the required floor's planning row (run_required_floor, witnesses lane) and from the wall's own runner. Decides nothing for gunbc compile, claim_batch or any per-entry path. Widens the prepared subject by exactly the touched modules and the match-bearing consumers of changed coproducts, each announced with its ground on the run's own receipt line, and narrows nothing: a base that cannot be reconstructed on a CI commit REFUSES the floor rather than planning blind, and a local run without a diff baseline reports the projection unevaluated exactly as the changed-witness projection already does."
}
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@ data check_reachable_only_from_an_entry_point_the_context_never_calls: Recurring
"THE DUPLICATEMODULE PLANT WAS REFUSED AS A DISCRIMINATOR, AND THAT REFUSAL IS THE INSTRUMENT. Two files claiming one module panic in `insert_module_path` over the FULL index BEFORE the keep filter, so it is a corpus-wide detector that would red-line even with a narrow compiled subject. It would have looked like a spanning subject while answering a different question -- this thread's failure mode, caught in the probe, against the more dramatic answer. Strict-prepare SIGKILL of the keep set was reported and was not allowed to reverse membership: membership is what answers whether the unplanned witness is in the compiled subject, whether or not that compile completes.",

"A WRITTEN COVERAGE CLAIM ABOUT THIS NEIGHBOUR WAS FALSIFIED BY THE SAME MEASUREMENT. `gunbc.bare_name_fork_lens` header asserts that `the floor's whole-corpus preparation contains both` declarers of a forked bare name. The producer that falsifies it, and the identity-level observation, live on [[stale_claim_survives_its_own_correct_edit]] -- not a second copy of that census. Merge-path standing of `gunbc.bare_name_fork_lens` is that same row. The inert-lens specimen there is the `FloorGlobalInvariantRow` `declaration_identity_uniqueness`: named, fixture-tested, prefix-matched, and still never invoked -- this row's recognition rule one level up. Ceiling: wire the existing reader, then widen `decl_facts` for variant constructors; exhaustiveness over an unprepared match still needs `check_match_exhaustiveness` over a Strict-prepared module (dependents walk), which is this row's invocation shape, not a lens-bound climb.",

"RUNG found at 1, mitigatable: the checker is real and blocking when invoked; required CI did not invoke it on the live subject. THE CLASS HAS TWO HALVES AND THEY ARE RETIRED TOGETHER OR NOT AT ALL. The INVOCATION half: the required floor's prepared subject includes the authored module of every path in `touched_entry_files` (`module_seeds_from_touched_entry_files` joins `closure_module_seeds` in `run_required_floor`) and refuses a Strict-resolve hard diagnostic, including `NonExhaustiveMatch` -- sufficient for a helper-fn or type-decl edit in the file that carries the stale match. The DEPENDENTS half: the same seed list gains the match-bearing consumers of every coproduct whose arm set differs between the resolved diff base and head (`arm_set_changed_match_consumers` over the parse phase's `DeclarationIndex` and its base-side reconstruction, `v2.workflow.floor_subject_seed` `SeedArmSetChangedMatchConsumer`), so an untouched importer whose match went stale because an arm grew ELSEWHERE is Strict-prepared through the same mechanism and refuses there. CEILING 2, mechanically preventable, reached only when BOTH halves execute on the required lane; the receipts for each are the `[floor-phase] phase=touched-entry-compile-subject` and `[floor-phase] phase=arm-set-changed-consumers` lines of the run that carries them, and the discriminating red is the two-module fixture executed by `arm_growth_selects_the_untouched_match_consumer_and_strict_preparation_refuses_it`. What is NOT covered, stated as the bound: a consumer outside the floor's source roots (a `src/v1` `.dag` mirror), and a consumer whose match names the arm through the flat bare channel with an empty candidate set -- both are planned when reachable and COUNTED on the receipt line, never silently dropped.",
],

evidence: [],
Expand Down
4 changes: 3 additions & 1 deletion dag/gunbc/seed_growth_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ import gunbc.bootstrap_operation_seed_growth {
}
import gunbc.generated_artifact_boundary_seed_growth { generated_artifact_boundary_seed_growth_justification }
import gunbc.joint_claim_join_seed_growth { joint_claim_join_seed_growth_justification }
import gunbc.floor_arm_set_consumer_seed_growth { floor_arm_set_consumer_seed_growth_justification }
import gunbc.regen_convergence_seed_growth { regen_convergence_seed_growth_justification }
import gunbc.dag_artifact_identity_seed_growth { dag_artifact_identity_seed_growth_justification }
import gunbc.witness_runtime_cause_seed_growth { witness_runtime_cause_seed_growth_justification }
Expand Down Expand Up @@ -261,7 +262,8 @@ fn seed_growth_justification_roster() -> List<SeedGrowthJustification> {
required_lane_judgment_seed_growth_justification,
param_binder_seed_growth_justification,
live_tree_stamp_detector_seed_growth_justification,
joint_claim_join_seed_growth_justification
joint_claim_join_seed_growth_justification,
floor_arm_set_consumer_seed_growth_justification
]
}

Expand Down
10 changes: 10 additions & 0 deletions src/v1/stage0/src/bin/claim_executor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1103,10 +1103,17 @@ fn run() -> Result<ExitCode, ExitCode> {
if required_ci_phase_selected(RequiredCiPhase::Floor, required_ci_lane) {
eprintln!("required-ci: phase floor (one prepared subject, one fold)");
let commit = std::env::var("GITHUB_SHA").unwrap_or_else(|_| "local".to_string());
// THE PARSE PHASE'S INDEX IS LENT TO THE FLOOR'S PLANNING ROW, the same way the
// wave-admission phase reads it: the match-bearing consumers of a coproduct whose
// arm set changed are derived from that index and its base-side reconstruction,
// never from a second corpus walk. `None` here means the parse refused (the line
// is already stopped) and the floor refuses the planning row rather than planning
// blind.
match v1_compiler::cli_run::run_required_floor(
&source_roots,
&commit,
v1_compiler::cli_run::ShardStyle::single_shard(),
head_index.as_ref(),
) {
Ok(outcome) => {
report_required_floor_outcome(&outcome);
Expand Down Expand Up @@ -1520,10 +1527,13 @@ fn run() -> Result<ExitCode, ExitCode> {

if required_floor_mode {
let commit = std::env::var("GITHUB_SHA").unwrap_or_else(|_| "local".to_string());
// The standalone floor entry runs no parse phase, so no declaration index exists to
// lend; on a CI commit the floor refuses its planning row rather than planning blind.
return match v1_compiler::cli_run::run_required_floor(
&source_roots,
&commit,
v1_compiler::cli_run::ShardStyle::single_shard(),
None,
) {
Ok(outcome) => {
report_required_floor_outcome(&outcome);
Expand Down
Loading
Loading