Repository navigation
Extract the five in-situ gunbc.guarantee_stall rows into per-row modules, the way #10206 split recurring_failure_mode — roster.dag must keep an exact import/entry bijection - #10361
Conversation
…n exact import/entry bijection
`gunbc.guarantee_stall` carried its 28 rows in situ, so every row PR appended at the
same two points -- the declaration tail and the roster tail -- and conflicted with every
other row PR BY CONSTRUCTION. That is the collision geometry gunbc#10206 changed for
`gunbc.recurring_failure_mode`, and this is the same cut on the same terms: a row becomes
its own module under `gunbc.guarantee_stall.<row>`, and appending a stall now writes a new
file plus one roster line.
THE BRIEF SAID FIVE IN-SITU ROWS. There are 28, and all 28 are extracted -- five would
have left the collision point standing, which is the whole subject.
THE DIRECTION IS FORCED BY ACYCLICITY, not chosen: a row module imports `GuaranteeStall`
from `gunbc.guarantee_stall`, so the module carrying the type cannot import the rows back.
`all_guarantee_stalls`, `restored_stalls` and `every_restored_stall_is_rostered_once` move
to `gunbc.guarantee_stall.roster`. The three folds that take a `List<GuaranteeStall>`
parameter -- `every_stall_is_below_its_ceiling`, `every_stall_names_a_trigger`,
`stall_roster_size` -- stay with the type, because they name no row and rebinding them
would be motion for its own sake.
PRESERVATION EVIDENCE, as a partition rather than a count:
AuthoredAdds EMPTY -- no row added, no row removed
AuthoredEdits EMPTY over row bodies: all 28 `data ... : GuaranteeStall = ...`
declarations are BYTE-IDENTICAL to their pre-split text, checked by
extracting both sides and comparing
bijection 28 row files, 28 roster imports, 28 roster entries, all three sets
equal with multiplicity 1
roster order unchanged, entry for entry
GREEN BY EXECUTION, not by typecheck: all eight witnesses in
`test.claim.guarantee_stall_witness_test` PASS against the split corpus --
`claim_batch --source-root dag --source-root src/v2 --entry
dag/test/claim/guarantee_stall_witness_test.dag --functions <all eight>`. That includes
`every_restored_stall_is_still_rostered`, whose negative arm refuses on an empty roster,
so the bijection above is asserted by an executing fold and not only by this message.
WHAT WAS AMENDED RATHER THAN MOVED, and why each edit was owed:
- the roster's own next-rung trigger said "every top-level data declaration in
gunbc.guarantee_stall ... and no declaration outside that module". After the split that
sentence names the wrong population, so it now names the module TREE. Leaving it would
have been a trigger satisfiable while the capability stayed dead.
- the restored-stalls note said those four were "DECLARED in this module"; they are
declared in row modules and rostered here. Reworded, and the note now records that the
pin is carried by IMPORT, which refuses at resolve if a row module is renamed or deleted
-- strictly stronger than the subject-string match it replaces.
- the type module's header now says where the rows and the roster live.
- three prose citations of the form `gunbc.guarantee_stall` `<row>` are repointed to the
row's module (`gunbc.merge_lifecycle`, `v2.std.nat`, `v2.workflow.floor_expected_red`).
WHAT WAS NOT TOUCHED, stated rather than left to be found: the `gunbc.recurring_failure_mode`
receipt strings that cite stall rows still spell the carrier and the row identity, both of
which are unchanged; editing them would regenerate `docs/design-failure-modes.md` and
collide with every lane appending a failure-mode row, for no gain in resolvability.
THE THREE COHORT PROVENANCE NOTES ARE CARRIED VERBATIM INTO THE ROSTER and not split
across the rows they describe. Their membership is DEICTIC -- "the fifteen executing
identities below", "these four pre-existing facts" -- and nothing in the rows records
which cohort a row arrived in, so a per-row assignment would be an authored guess about a
measurement nobody can re-derive. The roster is the one module that sees every row at
once, which is the only place a claim about a SET of rows can be true.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017XohvmvDmFP4SVY5t9Sux2
…roster touch charged The required run on 040dc2b refused with `FAILED PHASE namespace-wave-admission (10 unadjudicated delta(s), 0 stale admission(s), 6 consumed admission(s))`. The floor itself was CLEAN in that run -- `verdict=FloorClean claims_failed=0` -- so this phase was the whole of the failure. Both halves are addressed here, and both were predicted by the split rather than discovered as surprises. TEN DELTAS, TEN ROWS, taken from the run's own enumeration and not from a pattern. All ten are bindings in one consumer, `test.claim.guarantee_stall_witness_test`, and they split two ways: six whose spelling now resolves to `gunbc.guarantee_stall.roster` (`all_guarantee_stalls` x4, `restored_stalls`, `every_restored_stall_is_rostered_once`), and four whose spelling now resolves to `gunbc.guarantee_stall.next_rung_trigger_enforcement_stall`. A wildcard over "anything that moved under gunbc.guarantee_stall" would also admit the next relocation nobody reviewed, which is the rule the eighteenth transition already states. THE CHECK ON THAT COUNT: the three folds taking a `List<GuaranteeStall>` PARAMETER -- `every_stall_is_below_its_ceiling`, `every_stall_names_a_trigger`, `stall_roster_size` -- stayed with the type module and produce no delta. Had they moved, this would be thirteen. THE TWO MEMBERSHIP ADDITIONS GET NO ROW, deliberately: the run classified them `ExplicitlyEvaluatedZeroDelta`, which auto-admits. A row for an auto-admitted disposition is a decoration that later reports stale. SIX CONSUMED ADMISSIONS DELETED, AND NONE OF THEM IS MINE -- which is the rule working rather than a sweep. This branch touched the roster and thereby inherited the deletion obligation this module charges to whoever next touches it: two `gunbc#10206 recurring_failure_mode split` rows, whose trigger fired when #10206 merged, and four `gunbc#10028 irrefutability-predicate dissolution` rows, whose trigger fired when #10028 merged. A consumed row left standing ages into a stale one that refuses an unrelated change, so the deletion is owed on this touch and not to a follow-up PR. Recorded as the TWENTIETH TRANSITION and the TWENTY-FIRST DISSOLUTION -- the next unused ordinals in each of this ledger's two sequences. `cargo fmt --all --check` clean and `cargo check --release -p v1-compiler --lib` clean under `-D warnings`, since deleting rows can only fail at compile time. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017XohvmvDmFP4SVY5t9Sux2
… and retire the one row the base consumed ONE CONFLICT, in `src/v1/stage0/src/namespace_wave_admission.rs`, and main's incoming side is the authority on how to resolve it: the TWENTY-THIRD DISSOLUTION that landed there writes the rule down operationally -- keep the rows THIS branch authored whose transitions are open, and for every incoming row READ THE BASE before carrying it, because consumption is decidable from the tree and guessing it has cost a required run four times. KEPT: this branch's ten `gunbc#10328 guarantee_stall split` rows. Their transition is open -- the split has not merged, so the base still binds those ten spellings to `gunbc.guarantee_stall` and every one of the deltas is producible. DROPPED, MINE: my own TWENTY-FIRST DISSOLUTION entry. Main removed the same four `gunbc#10028` and two `gunbc#10206` rows independently and recorded it as the TWENTY-THIRD. One event, one record -- a second narration of the same deletion is the double-record this ledger already refuses once, so my entry goes and main's stands. DELETED, AS THE TWENTY-FOURTH DISSOLUTION: the one incoming `gunbc#10218 identity-equality re-home` row. Read from the base rather than waited on, which is what the rule above asks: main declares `physical_asset_identity_eq` in `product.placement_supply` and `product.printed_chassis.manufacturing_manifest` imports it from there by name, so the base already binds that spelling to that target and the delta is not producible. Main's own paragraph says this row is owed deletion by the next roster-touching change once #10218 merges; #10218 has merged and this is that change. `cargo fmt --all --check` clean and `cargo check --release -p v1-compiler --lib` clean under `-D warnings` on the merge result. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017XohvmvDmFP4SVY5t9Sux2
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
Adopted this after The conflict, and why the resolution is forcedOne conflicted path, The branch carries ten
The resolved merge is byte-identical to
|
|
Closing: the correctly-resolved merge produces a tree byte-identical to main (146fff2ded), so this PR has no content left to land. Receipt in the comment above. Branch preserved — reopen if any measurement there is wrong. — sent from warm-seal-35 |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d9fcb357c0
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| // list is DERIVED and an unenrolled row has no spelling. A declaration-identity, | ||
| // initializer-shape, or corpus-wide GuaranteeStall surface alone does not satisfy the trigger. | ||
|
|
||
| data all_guarantee_stalls: List<GuaranteeStall> = [ |
There was a problem hiding this comment.
Moving this declaration leaves several repository authority citations naming symbols that the root module no longer declares: docs/plans/roadmap-launch-mvp-plan.md:208 still points to gunbc.guarantee_stall.all_guarantee_stalls, while dag/gunbc/recurring_failure_mode/required_evidence_absent_reads_as_evidence_of_pass.dag:17 and dag/gunbc/rung_drop.dag:292,492 still attribute relocated row declarations to gunbc.guarantee_stall, propagating the same stale paths into the generated design docs. These references should be repointed to .roster or the corresponding per-row module, as was already done for the references in merge_lifecycle.dag, nat.dag, and floor_expected_red.dag.
Useful? React with 👍 / 👎.
1 participant
Auto-opened by session-dashboard for session
royal-cat-878.Pushing to
session/royal-cat-878advances 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