Repository navigation
A deployment plan carries one decision per member because the roster derives it, not because a caller assembled it - #10717
Merged
Merged
Conversation
…derives it, not because a caller assembled it Every release deployment plan contains exactly one decision for each required member; omission and duplication are unrepresentable at the production planning seam, and effect ordering is derived from the deployment's roster rather than caller-supplied. #10696 introduced that invariant and did not yet structurally guarantee it. A five-slot record closed the accepted-empty-plan hole for five members and could not extend past them -- the deployment owns eleven artifacts, and a shape costing one named slot in three places per member stops paying around there. Decisions are now MAPPED from the deployment's own member roster: map is total and order-preserving over its input, so the list cannot omit a member, hold two decisions about one, or order them differently from the authority. THE FIRST ROSTER DRAFT REOPENED THE EXACT HOLE IT REPLACED, and the fix is why derive_member_plan takes functions rather than a list. It kept derive_effects(decisions: List<MemberDecision>, ...) and relied on convention about who calls it; the TYPE still admitted a hand-built empty list, which derives a plan with no rows and an accepted empty plan. The only way to obtain a plan is now to hand over the roster and the desired/observed functions -- the caller never builds the list at all. ReleaseEffectPlan is sole_constructor, so the hole is closed from the construction side too: no module can write ReleaseEffectPlan { target, rows: [] } and hand an empty population to the emitter. NEGATIVE COMPILER EVIDENCE, both measured on this tree, neither enrolled as a runtime witness because the invalid states are unconstructible and such a witness would be permanently green: - delete the DirectoryRoot arm of member_observe desired_member_identity -> non-exhaustive match: missing variant(s) DirectoryRoot - write ReleaseEffectPlan { target, rows: [] } outside its module -> sole_constructor type 'ReleaseEffectPlan' cannot be constructed outside its defining module Positive control: apply closure resolves with zero diagnostics; emit 59/59; identity 11/11. THREE DIRECTORY ROOTS JOIN THE ROSTER, taking the frontier from three of eleven owned artifacts to six. A root's identity is its OWNING PRINCIPAL, not its presence: presence is already carried by ObservedMember, and what presence cannot say is whether a directory that exists belongs to the principal that must write it. A root does not restart the serve process -- roots are prerequisites, not inputs, and a process actually broken by a missing root is already stale on its own account. TWO DEFECTS THIS FOUND, both caught by execution rather than by reading: plan_mutation_of folded from a KeepMember init, making a member with NO ROW indistinguishable from one explicitly kept -- absence of knowledge rendered as a decision to do nothing. The lookup is typed now, and the emitter reads MemberNotInPlan as "emit what the apply-all era emitted", never as a skip. identity_member_of_step answers WHICH MEMBER a step is, and two consumers needed opposite things from it: deployment_apply_plan excludes a step from the membership reconcile when the step's commands come from emit_release_member_effects, while apply_step_effects asks whether the plan gates the step. Those coincided until a root, whose identity decides WHETHER but whose command still comes from its own upsert, broke the coincidence -- silently removing all three roots from the reconcile. Split into step_renders_its_own_member_commands. Two pre-existing witnesses caught it; nothing in the types did. RETIRED: a_decision_in_the_wrong_slot_refuses_the_plan, with the slots it policed. A climb normally keeps its discriminating red (DESIGN 4b), but that rule turns on whether the red stays authorable, and this one does not -- at the corpus boundary or in a fixture -- because expressing it requires handing the derivation a decision list, the call that no longer exists. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019iXPtAqzPaNBZbaaM5rxrY
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
briansrls
added a commit
that referenced
this pull request
Sep 7, 2026
…quired parse phase refused every branch (#10719) main is parse-red at 59a692a and has been since that merge. The required run's parse phase refuses before the floor executes, so EVERY branch cut from current main fails for a reason its own diff does not contain -- observed on PR #10717, whose six changed files are all under dag/gunbc/live_deploy and dag/test/claim/live_deploy. src/v2/lens/unit_modeling.dag:148:1 src/v2/lens/testgen.dag:2164:1 source annotation names no subject: no module item follows it Section 4c admits a standalone leading `//` block attached to a MODULE-SCOPE DECLARATION. Both notes were the last line of their file, so nothing followed them to attach to. The citations themselves are correct -- gunbc.guarantee_stall.unit_modeling_carrier_totality_stall and gunbc.guarantee_stall.testgen_anchor_generator_totality_stall both exist -- and each describes the `construction_justification` declaration immediately above it, whose WallAfterGrounding class is exactly the thing section 4b(2) obliges to name a next-rung trigger. So each note moves above the declaration it describes. Nothing is deleted and no citation changes; the annotation simply leads its subject instead of trailing it. WHY THIS IS ITS OWN PR: PR #10717 is under a keep-it-tightly-scoped ruling, and folding an unrelated two-file repair into it would be the scope creep that ruling exists to prevent. This also unblocks every other branch, not only that one. Verified by execution: both entries resolve with zero diagnostics through `gunbc run`, the strict route that produced the refusal. Claude-Session: https://claude.ai/code/session_019iXPtAqzPaNBZbaaM5rxrY Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <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
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.
Acceptance
Why now rather than later
#10696 introduced this invariant and did not yet structurally guarantee it. The five-slot record closed the accepted-empty-plan hole for five members and could not extend past them — the deployment owns eleven artifacts, and a shape costing one named slot in three places per member stops paying around there. The carrier still has few consumers and no follow-on work has accumulated on the weaker interface, so the migration is local now and would not stay that way.
The structural change
Decisions are mapped from the deployment's own member roster.
mapis total and order-preserving, so the list cannot omit a member, hold two decisions about one, or order them differently from the authority.The first roster draft reopened the exact hole it replaced. It kept
derive_effects(decisions: List<MemberDecision>, …)and relied on a convention about who calls it — but the type still admitted a hand-built empty list, which derives a plan with no rows and an accepted empty plan.derive_member_plannow takes the roster and the desired/observed functions, so the caller never builds the list at all.ReleaseEffectPlanis additionallysole_constructor, closing the hole from the construction side.Negative compiler evidence
Both measured on this tree. Neither is enrolled as a runtime witness: the invalid states are unconstructible, so such a witness would be permanently green and cited as coverage it does not provide.
DirectoryRootarm ofmember_observedesired_member_identitynon-exhaustive match: missing variant(s) DirectoryRootReleaseEffectPlan { target, rows: [] }outside its modulesole_constructor type 'ReleaseEffectPlan' cannot be constructed outside its defining modulePositive control: apply closure resolves with zero diagnostics; emit 59/59; identity 11/11.
Three roots join the roster (3 of 11 → 6 of 11)
A root's identity is its owning principal, not its presence — presence is already carried by
ObservedMember, and what presence cannot say is whether a directory that exists belongs to the principal that must write it. A root does not restart the serve process: roots are prerequisites, not inputs, and a process actually broken by a missing root is already stale on its own account.Two defects this surfaced, both caught by execution rather than reading
plan_mutation_offolded from aKeepMemberinit, making a member with no row indistinguishable from one explicitly kept — absence of knowledge rendered as a decision to do nothing. The lookup is typed now, and the emitter readsMemberNotInPlanas "emit what the apply-all era emitted", never as a skip.identity_member_of_stephad two consumers needing opposite things.deployment_apply_planexcludes a step from the membership reconcile when its commands come fromemit_release_member_effects;apply_step_effectsasks whether the plan gates the step. Those coincided until a directory root — whose identity decides whether but whose command still comes from its own upsert — broke the coincidence, silently removing all three roots from the reconcile. Two pre-existing witnesses caught it; nothing in the types did.One retirement, and why it is a deletion
a_decision_in_the_wrong_slot_refuses_the_planwent with the slots it policed. A climb normally keeps its discriminating red (DESIGN §4b), but that rule turns on whether the red stays authorable — and this one does not, at the corpus boundary or in a fixture, because expressing it requires handing the derivation a decision list, which is the call that no longer exists.Scope
No timer identities, thin actuator, publication-helper changes, or performance work. The remaining five owned artifacts (four unit members, one Tailscale route) stay on the apply-all path and contribute no member — a kind that names no member emits exactly as it does today.
🤖 Generated with Claude Code
https://claude.ai/code/session_019iXPtAqzPaNBZbaaM5rxrY