Repository navigation
Land bright-badger-637's three ORPHANED PRs one at a time: #10781 first (approved, 4 lines, needs only a regen against current main) - #10833
Closed
gunbai-bot[bot] wants to merge 12 commits into
Closed
gunbai-bot[bot] wants to merge 12 commits into
gunbai-bot[bot] wants to merge 12 commits into
Conversation
…harper hole DESIGN section 4b requires a ceiling to be derived rather than aspirational, and generic_application_admits_distinct_unit_variant_arguments said its own was unestablished in as many words: 'The diagnostic name says generic-formal undecidable, but no measurement establishes undecidability; do not use that name to declare a permanent ceiling.' A four-arm fixture is that measurement. take_map_concrete declares a CONCRETE m: Map<String, Bool>; map_insert declares the same argument at a GENERIC formal. A String at the concrete formal REFUSES with a located, typed mismatch. The same String at the generic formal is SILENT at that argument. One argument, one shape, two positions, two answers -- so refusal is reachable and genericity is not the reason it does not fire, and a String inhabits Map<K, V> for no instantiation of K and V. That receipt lands on the existing row and discharges its ceiling sentence and NOTHING ELSE. That row's population is variant identity; the fixture's is shape; the row itself forbids borrowing evidence across populations, and the boundary is stated in the receipt so a later reader cannot credit a repair for one to the other. A second arm found a hole that is not that row's subject at all: an unapplied function -- empty_map rather than empty_map() -- admitted at the CONCRETE position, in the same compile where a String at that identical position refuses. No instantiation makes fn() -> T inhabit T, so it is decidable from the argument alone. That gets its own identity rather than a receipt, because two mechanisms sharing one consequence would let a repair for either be credited to both. The new row is rostered at the END of the list: roster order is source order and the projection renders it, so inserting alphabetically would have reordered docs/design-failure-modes.md and destroyed the empty-diff oracle. This is the class that admitted my own defect in gunbc#10779, found by a reader on a diff the compiler reported nothing about. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CQuBs4mLu9ArojSWFiRcey
review 62002 refused two things and both were right: the fixture was described in prose with its output copied into the rows, and the row said arm 4 IS ENROLLED in the present tense while no fixture existed in the tree at all. THE PROBE IS NOW REAL AND IT DISCRIMINATES. Four sources through compile_dag_diagnostic_census, the same harness the duplicate-definition probe uses, folded to a blocking-diagnostic count: a_string_at_a_concrete_position_is_refused PASS positive control an_unapplied_function_at_a_concrete_position... FAIL the defect a_string_at_a_generic_position_is_refused FAIL the deferral the_well_typed_call_is_clean PASS fixture not broken Two greens bracketing two reds is what makes this a discrimination matrix rather than a test that happens to be red. Without the concrete-position control, a red on the function arm would be indistinguishable from a probe whose source broke some other way; without the well-typed control, an import typo would red everything and read as walls landing. The fixture is source handed to the compiler rather than corpus modules because two of the four programs are invalid and one is correctly refused -- as corpus members they would break every build that resolved them. DESIGN section 4b rules exactly that case. THE ASSERTIONS ARE THE CORRECT BEHAVIOUR, NOT THE OBSERVED ONE. Written the other way the rows would pass today and become defenders of the defect: the day someone lands the wall, the test would red and read as a regression caused by the fix. A check that must be deleted to make progress was recording the bug as the specification. ENROLMENT AND THE PROBE LAND TOGETHER, never separately -- two unenrolled reds would block every lane in the program, and there is no acceptable window for that. Both identities go into floor_expected_red, and the stall row is what makes that admissible rather than green-by-suppression: an expected red with a declared way to stop being expected is tracked debt, one without is the untracked stall section 4b(2) forbids. The trigger states the exit explicitly -- on the day both rows refuse, they LEAVE the roster and stay enrolled as permanent regression controls per 4b(4). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CQuBs4mLu9ArojSWFiRcey
…olds review 62023 caught the new stall appended to restored_stalls instead of all_guarantee_stalls. My edit took the LAST list in the file, and the last list is not the roster. That is the section 3c defect this very file already names: a stall declared, typed, valid, and absent from every projection the roster feeds. Nothing folds restored_stalls for rendering -- gunbc.rostered_row_join joins against all_guarantee_stalls -- so the failure-mode row and the expected-red enrolment were both pointing at a tracking consumer that no fold would ever reach. The enrolment's whole admissibility rests on that stall being visible, so this was not cosmetic: it would have left two expected reds tracked by a row nothing renders. It also violates that list's own stated rule -- a new stall row must be admitted WITHOUT editing restored_stalls, which pins four historically restored subjects so their loss refuses -- and it would have broken every_restored_stall_is_still_rostered, since a restored member missing from all_guarantee_stalls is exactly what that fold refuses on. Removed from restored_stalls, appended at the END of all_guarantee_stalls because order there is source order and load-bearing. Projection regenerated. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CQuBs4mLu9ArojSWFiRcey
…g false review 62034 found that test.claim.argument_shape_at_a_declared_position_probe_test matches NO prefix in v2.workflow.required_floor required_gate_prefixes. I checked all thirty mechanically rather than by eye: none matches. The floor therefore suppresses these identities as dormant -- discovered, not run. SO THE ENROLMENT ASSERTED THE ONE THING THAT ROSTER EXISTS TO PREVENT. floor_expected_red's own header: enrolling an identity asserts that it REACHES ITS SUBJECT AND ANSWERS, and it records 101 rows that left it for exactly this reason -- never-executed identities reading as debt someone was working. A dormant red carried as expected debt is the more dangerous of the two mistakes, because a genuine red is loud once someone looks. Enrolment removed. Removing it is safe for the reason that made it look necessary: two unenrolled reds would block every lane, and these do not, precisely BECAUSE they are dormant. A SECOND DEFECT IN THE SAME ROW, AND IT IS THE ONE I SHOULD HAVE CAUGHT: the row said ReadsLiveTree sites have routed to DeclinedLiveTree. That arm IS DELETED -- required_floor.dag says so at its own root. I lifted the sentence from the duplicate-definition probe's historical comment without checking it still held, which is a stale citation standing where a current fact was required. A THIRD: the row called the string-at-generic arm 'the sibling row's subject', contradicting the sibling receipt this same PR adds. That row's subject is variant IDENTITY; this fixture's population is SHAPE. The arm discharges that row's CEILING SENTENCE and nothing else, which is what the receipt already says and what this row now says too. The row and the stall trigger now state the standing plainly: the executing consumer is the named claim_batch invocation and nothing else, and admitting the module to required_gate_prefixes is the prerequisite that would convert re-derivable evidence into enrolled evidence. That admission is a second gate and a cost on every floor run, so it is asked for rather than taken. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CQuBs4mLu9ArojSWFiRcey
… never Section 4b(2) requires a class below its ceiling to name its next-rung trigger, separating cannot-climb from can-climb-after-one-grounding from can-climb-now-but-unbuilt. This class is below its ceiling for TWO independent reasons and only one of them was written down. The class trigger was there: the declared-type judgment decides argument shape from the argument's own constructor before consulting the declared position. The EVIDENCE trigger was not, and it is the one actually blocking. The probe matches no prefix in required_gate_prefixes, so a required lane never runs it. That leaves the class PROVEN BUT UNROUTED -- it executes, it discriminates, and no required consumer repeats it, so the rung rests on a human-run command. Admission to that gate is now named as the trigger rather than left as an observation, because an honest sentence about the present state quietly becomes the permanent state if nothing names its end. The condition on asking is in the row too: request the admission when the runner pool is not saturated, and as its OWN change rather than as a rider. It adds four rows to every required floor run, and it was deferred on a day when the pool sat at roughly twenty concurrent runs and main had gone red on memory pressure from that load. Both triggers are ClimbableButUnbuilt: neither waits on a grounding that does not exist. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CQuBs4mLu9ArojSWFiRcey
review 62052 found the annotation laying out a 2x2 including generic+function observed accept, while the module declares three shape arms and a well-typed control. No such row exists. A reader re-deriving the names in the stall's trigger would have found a control where the table promised a fourth measurement -- in the file whose own closing note says WHAT THIS DOES NOT MEASURE, stated so no receipt reads coverage it does not have. Corrected the table rather than adding the arm, and the reason is in the file. The fourth cell cannot come out against anything: acceptance there is already ENTAILED by the two arms above it, since the position defers on every argument and the argument is refused at no position. An arm that cannot produce a result contradicting what its neighbours already establish is not a measurement, it is a fifth witness to author, review, maintain and eventually run, which section 2 counts as redundant work on all three of section 1's quantities. Its provenance is recorded rather than dropped: it was compiled once during the investigation and behaved as entailed. That is not evidence this module carries and it is not cited as any. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CQuBs4mLu9ArojSWFiRcey
review 62067 found three defects and all three are one shape: an edit changed the thing and the prose describing it stayed standing and well-formed. A MEANING FORK ON ENROLMENT. The probe comment still said the function arm is enrolled as an expected red, while this same change's typed rows say enrolment was removed because the module is dormant. One change asserting both. The comment now says what is true: the reds are REAL AND UNROUTED rather than held -- nothing suppresses them because nothing runs them -- and it points at the stall that names gate admission as its own trigger. A ROSTER EXIT THAT CANNOT HAPPEN. The row attributed to the stall an exit of LEAVE floor_expected_red. The stall says no such thing, and an identity that is not on a roster cannot leave it. Replaced with what the trigger carries: on the day both rows refuse they flip to permanent regression controls. POSITIONAL CITATIONS, IN THE RULE'S OWN WORDS. arm 3 and arm 4 stopped matching the module the moment the previous commit reordered the arm table -- section 3's stated failure mode exactly: any edit ABOVE the cited line silently invalidates it. The references were positional in three rows and are now the test function names, which the namespace tree can decide. That last one is worth more than its fix. It is not a slip: a review fix broke the citations, and nothing caught it but another review. A position is unreachable from the tree that owns the thing it names, so no gate can see it rot -- which is why the rule says name the symbol, and why I should not have been writing ordinals into rows while citing that rule at other people. Re-verified by execution: the two rows asserting behaviour the compiler already has still PASS, so the annotation edits did not break the fixture. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CQuBs4mLu9ArojSWFiRcey
…cannot see review 62079, and it is right: the ceiling-discharge receipt claimed DeclaredTypeInhabitanceUndecided "is now measured to be reported over at least one decidable population" and that the undecidability "the diagnostic reports" is a property of where it is asked. The probe folds census_blocking_rows and that diagnostic carries GateAdvisoryTypecheck at v1.core, so no arm counts the class and no arm can see it. That was fabricated measurement in the one sentence doing the ceiling work. The receipt now discharges the ceiling by the weaker route the instrument actually supports, which is the route the reviewer names: one decidable String shape is refused at a concrete formal and accepted at a generic one in the same run, so genericity alone is not what makes a mismatch undecidable. It also states outright what blocking_count can and cannot see, so the comparison is not read as more than two blocking counts. The roster conflict is both sides appending at the same position; resolved additively, main's row first. docs/design-failure-modes.md regenerated from the merged authorities. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CQuBs4mLu9ArojSWFiRcey
# Conflicts: # dag/gunbc/guarantee_stall/roster.dag # dag/gunbc/recurring_failure_mode/roster.dag # docs/design-failure-modes.md
Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md generic_application_admits_distinct_unit_variant_arguments Ledger-Rows-Repaired: docs/design-failure-modes.md unapplied_function_value_admitted_at_a_value_position Ledger-Repair-Judged: docs/design-rung-drops.md
Contributor
Author
|
Closing as a duplicate of #10783, which carries byte-identical content (same 7 files, +195/-1, verified by tree diff from each merge-base). Keeping #10783 rather than this one, and I am reversing my own earlier ruling here rather than quietly switching: I previously said keep #10833 and close #10783 because #10783 was DIRTY. Both are DIRTY, so that reason never discriminated between them. What does discriminate: #10783 is undrafted, carries its real CI and review history, and its title states the actual change, while this PR's title is a work-item description naming #10781, which has already merged. A retitle would not fix that anyway -- a single-commit branch squashes under the COMMIT subject, not the PR title. This PR's stated purpose (land #10781 first) is complete. No work is lost: the content survives in #10783. -- sent from bright-ram-778 |
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
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.
Auto-opened by session-dashboard for session
proud-eagle-660.Pushing to
work-10783advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan