Repository navigation
Refuse the floor_expected_red / witness_deferral_freeze intersection - #8494
Merged
Merged
Conversation
38 identities across 24 entries were simultaneously enrolled in floor_expected_red's known-red roster (removable only by observing a pass) and path-deferred in witness_deferral_freeze as LegacyFrozenPathDeferral (declared never-executed) — a contradictory classification, since the required floor already treats each of these identities as an executing, known-red subject. Two changes: 1. A construction wall (expected_red_freeze_intersection) wired into run_required_floor in src/v1/stage0/src/cli_run.rs. It re-derives floor_expected_red_roster and frozen_path_deferrals' qualified identities (via each row's own entry's module line, never the path string) fresh at run time, and refuses the required floor with a located, counted diagnostic naming the exact colliding identities and the git head the collision was observed at if the intersection is ever nonempty again. Covered by three tests: a planted-collision RED control, a disjoint-rosters green control, and a qualified- identity resolution unit test. 2. Retirement of the current intersection with a receipt. All 38 colliding identities are removed from witness_deferral_freeze.dag: 15 entries had every function collide and are deleted whole; 9 entries had only some functions collide and keep their remaining, non-colliding functions frozen. Every retired entry already carries an independently executing consumer via floor_expected_red, so retirement removes no coverage. A single combined shrink-log entry (2026-08-19) records the computation, the disposition split, and the new wall as the recurrence-prevention mechanism, per DESIGN.md §5's rule that one obligation may cover several artifacts sharing the same terminal disposition and triggering observation. Re-derived fresh at commit 063a604: 0 collisions remain between the 306-identity floor_expected_red_roster and the edited 129-row frozen_path_deferrals. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dn14wmGgun1WFTDGZgEf1f
# Conflicts: # dag/gunbc/witness_deferral_freeze.dag
briansrls
pushed a commit
that referenced
this pull request
Aug 25, 2026
…oster both walls read (#9145) Two walls read frozen_path_deferrals -- expected_red_freeze_intersection and route_gap_freeze_intersection, both in v1_compiler.cli_run -- each refusing an identity simultaneously frozen here and enrolled in a roster asserting the required floor executes it. They landed five days apart and only one landed against an empty population. NOT A NEW PRINCIPLE. It is DESIGN's own admission test seen from the arming side rather than the phase-enrolment side it is stated on: "the admission test is whether every red is closable by the author who caused it at the moment they caused it". A wall armed over an already-non-empty population fails it by construction -- the author who causes the red is whoever pushes next, and the row that makes it red was authored elsewhere. SATISFIED #8494 521d4cf 2026-08-19: 38 colliding rows deleted and the wall wired in ONE diff. VIOLATED #9114 96cd1bf 2026-08-24 14:10: armed over a population of 4. Retired by #9133. WHY THE VIOLATION IS NOT CARELESSNESS, which is the reason the row is worth reading rather than a caution to recall. #9049 (664b339) enrolled the four identities at 14:09 -- SIXTY SECONDS earlier -- and is an ancestor of #9114, so the arming commit's base already carried them. Sixty seconds is far less than a witnesses run, so #9114's green was established against a base WITHOUT the collision and it landed on a base WITH it. Neither author could see the contradiction from inside their own change: #9049 added rows to a roster no wall yet guarded, #9114 armed a wall it had correctly measured as empty. The union was red and neither half was. So the test is NOT "count the population before arming" -- that would have changed nothing here. It is that a wall's green must be established on the base the wall LANDS on. The satisfied instance got that for free by clearing and arming in one diff, leaving no interval in which another change could enter the population. RUNG AND TRIGGER (DESIGN 4b(2)), written as a trigger rather than a ceiling because an unnamed stall and a real ceiling read identically. The class sits at mitigatable, held by a one-diff discipline nothing enforces. No roster-shaped check can climb it: at the moment #9114 was authored and reviewed its governed population was genuinely empty, so no state in either roster could have been refused, and a check over authored rows would be a ratchet. The next-rung trigger is named at the layer the defect lives on -- up-to-date-with-base before merge, strict required checks or a merge queue, which makes "green on the base it lands on" true by construction. That is an operator decision and the row does NOT assert how it is configured today; the setting was not readable when it was written. HOME. Proposed for v2.workflow.required_floor; the walls are not there and it names neither, so a row there asserting how they landed would be authority substitution. This file is the one roster both walls read, already names one of them, and already carries both polarities as shrink-log entries -- so the row joins facts in the file rather than importing them, and avoids hand-LOC growth in the frozen seed. Re-derivable: join floor_route_gap_roster (110 entries) against frozen_path_deferrals (128 rows, 614 qualified identities), qualifying every frozen row through its own entry's module line and not its path string -- 4 of 614 at 8ab8a8e, matching the wall's count=4. Corroborated on this branch: frozen_path_deferral_identity_count returns 610, which is 614 less the 4 #9133 retired. Verified: the module parses and evaluates after the annotation. Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
expected_red_freeze_intersection, wired intorun_required_floorinsrc/v1/stage0/src/cli_run.rs) that re-derivesfloor_expected_red_rosterandfrozen_path_deferrals' qualified identities fresh at run time and refuses the required floor with a located, counted diagnostic (naming the colliding identities and the git head observed) if any identity is ever simultaneously known-red and path-deferred as never-executed.dag/gunbc/witness_deferral_freeze.dag(15 whole-row deletions, 9 partial function-list trims), with a single combined shrink-log entry recording the computation and rationale, per DESIGN.md §5's rule that one obligation may cover several artifacts sharing the same terminal disposition and triggering observation.floor_expected_red, so no coverage is lost.Verification
floor_expected_red_rosterat commit063a604e0099c56c3e0a1f72af60d7a6199d1f0b: 0 collisions (306-identity roster vs. edited 129-row freeze file).gunbc runparses/evaluates the edited.dagmodule cleanly (only refuses on the expected non-ProcessExitexit-code wrapper, not a parse/type error).cargo build -p v1-compiler --bin gunbcsucceeds.Test plan
cargo test -p v1-compiler expected_red_freeze_intersectioncargo test -p v1-compiler frozen_path_deferral_qualified_identitiesgunbc runagainst the editedwitness_deferral_freeze.dagmodule🤖 Generated with Claude Code
https://claude.ai/code/session_01Dn14wmGgun1WFTDGZgEf1f