Repository navigation
Namespace admissions: split ConsumedByMerge from UnmatchedAdmission — cleanup billed to the roster, not bystanders - #9824
Merged
Merged
Conversation
… the cleanup bill moves from bystanders to the roster The eighth-dissolution class made a wall. A consumed row (its admitted relocation already holds at the base — positive proof against the base index, singleton binding equal to the row's declared target) is a typed receipt that refuses nothing for unrelated runs; an unmatched row still refuses. Deletion of consumed rows is enforced on the roster file's own next touch — which every future relocation PR performs by construction. Retired by: admissions bound to the delta content they admit, never resident on main (the capability that makes a stale-able row unwritable; waits on the declaration-index carrier). AdmissionSubject::Binding gains its relocation target (the consumption proof's referent). Evidence: RED (unmatched row refuses and never acquires an expiry — reds the fallthrough implementation), positive control (consumed row typed, run stays admitted), one-run discriminator, and the ambiguous-base guard on the singleton requirement. 45/45 in tests/namespace_wave_admission.rs; clippy --all-targets green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QhdaHkmZPoQoeUWz5V2mzF
…sumed-admission # Conflicts: # src/v1/stage0/src/namespace_wave_admission.rs
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 31, 2026
…s imported Two repairs, both surfaced by composing with main rather than by any defect in either side alone. The merge with main brought #9824, which added a `target` field to AdmissionSubject::Binding: the module the admission's own PR moved the name TO, and the referent of the consumption proof. Our two SPARK-PAIR-0 P0-C3a rows predate that field, so git merged both sides cleanly and the tree did not compile. The value is verified rather than copied from our own label -- spark_serving_linger_probe_words is declared in dag/gunbc/spark/serving_observe.dag, whose module line is gunbc.spark.serving_observe. serving_execution_schedule.dag matched SparkServingUserUnitActivityAddress at four sites without naming it in its import block. Peer modules list it explicitly, so it is now listed here. This is import hygiene, not a resolution repair: the module resolved and typechecked before the change -- measured, by reaching evaluation and failing on a call-contract mismatch, which occurs after resolution.
gunbai-bot Bot
added a commit
that referenced
this pull request
Aug 31, 2026
…vation carries its projection, the rows become an axis product, and the artifact stops answering for a plan it never made (P0-C3, dry) (#9763) * Spark row production leaves artifact assembly, and members bind to the rows derived from them (P0-C3a, dry) SPARK-PAIR-0 P0-C3a, part of the dry observation-to-plan bridge. No host mutation. This does NOT claim the C3 exit receipt. TWO INDEPENDENT BREAKS make P0-WET unreachable: the CLI passes an unobserved Spark axis, AND the generic artifact set spark_serving_typed_actions to scheduled_rows_empty() unconditionally. Repairing either alone changes nothing. This closes the second and makes the first possible; the first is still open. ROWS ARE A FACT ABOUT AN OBSERVATION, NOT ABOUT AN ARTIFACT. Row production and artifact assembly were fused, so reaching Spark rows meant calling the Spark-specific artifact builder, which brings its own timers, caps, observed_slots: [] and an unobserved fabric population -- two subjects, two baselines, two leases and an arbitrary winner. spark_serving_scheduled_rows_for is extracted; both the slice helper and the generic artifact derive from it. All four unobserved guards are preserved verbatim: each names a probe whose silence would read as "the member is absent", and absence is what makes membership_reconcile plan an ADDITION. MEMBERS AND ROWS ARE ONE CARRIER. The artifact took observed_spark and the schedule as two independent parameters, so a caller could hand it members from one observation and rows planned from another. observed_spark feeds the observed BASELINE, and the baseline is what apply re-checks to decide the plan still applies -- so that disagreement would have been invisible at exactly the moment it mattered. SparkServingAxisProduct is sole_constructor and only the row producer mints it. THE MINT TAKES PROBES, NOT A FINISHED PROJECTION. A first version accepted the projection as a parameter, which reopened the class #9754 closed one field over: nothing stopped a caller pairing srv5's readback with a projection built for srv6. The mint now takes the four probe observations and builds the projection from readback.host, so the host is not a caller's to supply. THE SUBSTRATE REFUSED MY FIRST DESIGN AND IT WAS RIGHT. Having the artifact call the row producer closed an import cycle -- gunbc.fleet_converge_plan -> spark.serving_converge_apply -> spark.serving_converge_plan already runs the other way. Artifact assembly consumes already-planned axis products. THE ARTIFACT'S OPTIONAL CARRIED A FACT THAT CANNOT HAPPEN. It answered Absent when content_hash_of_value did not return the Fnv1a64 arm -- an absorbing arm in the narrowing direction, since an unrecognised hash became "there is no plan artifact", read by every caller as nothing to converge. content_hash_atom dissolves it. THE LINGER ARGV FORK IS CLOSED: it had two spellings, one per transport, free to drift the first time loginctl moves, and now has one home. The three-valued reader added beside it serves the unified observation producer. It is NOT a repair of serving_converge_slice_wet: an earlier version of this commit claimed the slice collapsed "unobserved" into "disabled", and that claim was FALSE. The slice refuses on all three unobserved cases -- transport refusal, nonzero exit, malformed stdout -- before reaching any boolean translation, setting LingerUnobserved with zero planned rows. The claim was inferred from a Bool? in a signature rather than from the control flow, and is retracted here rather than left standing in history. KNOWN NOT DONE, so this does not overstate its rung: the production path does not yet run ONE probe transaction. In spark_serving_observe_host_via_locus the readback uses the via-locus leg while the projection helpers use the other leg, and is-active and the runtime receipt are each probed twice. The honest wording is that readback and projection are constructed during one enclosing call, not that one transaction owns every capture. The axis carrier is also a pair rather than a disposition: it cannot distinguish a non-Spark subject from an unobserved one and has no refusal arm, which is why fleet_converge_plan_artifact's Refused arm currently has no producer. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018dHefbXnLiW1XNs2vVxhwj * wip axis disposition * wip axis controls * P0-C3: the axis names its own host and an unprobed Spark is not a non-Spark * hoist annotation to module grain * witness call sites: the axis is tagged for the host being planned * cli axis arm: witnesses * apply refuses an enrolled Spark it did not observe: the plan-side guard did not reach this path * apply-path refusal extracted to a witnessable decision, with its control * close the apply spark-admission match * the empty spark population is not constructible for an enrolled Spark * exact-consumer control for the apply interlock * typed artifact refusal, one exhaustive axis match, projections deleted * enrollment is one classification read by both CLIs * probe transaction carrier: one host, one attempt, one locus, one capture per leg * the mint is the admission * one acquisition per host: the sub-observers become pure reads of captures * close the observed-facts match at the slice site * rename the carrier capture: SparkServingProbeCapture was already taken by terminal health * restore the terminal-health import name * argv derived from the leg, provenance survives projection, linger read once * bind the extracted parameter names * the planned axis carries an opaque transaction-bound payload * thread provenance through the projection; provenance minted through one function * correction A and B: total assembler, honest claim subjects * retire the endpoint consumer row for the deleted direct probe leg * mint provenance through its single constructor inside observe too * balance the apply body after the merge * the scope predicates gained the arm #9746 added * the capture carries a request and a typed outcome; coverage is required; enrollment names only enrollment * rejoin the split annotation block * guard the empty digest population instead of pattern-matching an empty literal * carrier witnesses: coverage, typed outcomes, and the mislabel counterexample made unwritable * the missing-leg claim reads the refusal, not a forged transaction * string_contains is a builtin * the observation attempt is derived from the sealed context, the host and the phase * phase identity controls * seal the host-observation mint to the transaction projectors and one named fixture * the fixture's real module path * sealed mints, provenance as a sum, and an exhaustive prerequisite question * restore the phase declarations swallowed by the provenance rewrite * bind the facts provenance from the context * the axis production route consumes one sealed observation * the bound plan carries the provenance value and its mint is sealed * the witness reads the provenance value * the annotation states the construction that is now present, and names the one exception * the witness reaches the sealed mints through its two admitted fixtures * the post-apply replan is its own transaction under its own phase * drop the brace left by the extracted replan body * post-apply phase and provenance-arm controls * the per-host receipt carries the acquisition it came from * receipt controls * adjudicate the linger-argv consolidation as two exact wave-admission rows * typed identity lives in the transaction; every provenance projector takes only it * wip: transaction carries full acquisition identity * wip: one hermetic acquisition fixture authority * wip: single planning route, one fixture authority * wip: acquisition receipt sum carried and rendered by the production line * wip: prove the acquisition receipt by consumption through spark_serving_report_body_lines * wip: typed observation request names one identity for attempt and refusal * fix: field value must follow its name on one line; restore displaced annotations * fix: witness consumes computed rows; generic-artifact claim takes its axis from the one route * fix: axis route reads the typed refusal request * fix: the fixture imports the calls actually needed; bare references were resolving without loading * wip: hermetic-only fixture mint, typed transaction refusal, coverage record, branded attempt identity * wip: delete the bare-projection artifact route; slice takes the observation whole * wip: capture shapers drive the production projectors to chosen states * file resolved_reference_outside_execution_closure as a recurring failure mode * wip: fixture owns the one admitted request mint route * wip: report claims build observations through the production transaction route * restore the axis route the artifact cut over-removed; slice witness plans through the generic artifact * witness claims enter the row producer and the observation route; linger's third state is earned from a capture * fix module paths and the two remaining splice call sites * arity fix on the refusal renderer * the converged host is assembled from probe output the projectors read * slice and role claims observe a converged host through the captures * c3 claims observe the converged host * name the positional binders in the content-hash match * the runtime receipt echoes the identity digest the projector compares * the unit read echoes the desired unit wire, so the content member converges by bytes * split the conjoined slice claim so a red names which fact broke * one artifact assembler: the generic body writes the typed-actions line its own wall reads * the schedule-carrying claims observe a drifting host, so the equality cannot hold by emptiness * the deleted assembler's imports go with it * seal the fixture chain transitively and execute its admission wall * the control pair varies exactly one fact: whether the roster names the caller * regenerate the design projections from the merged roster * the control pair calls the same function; only the roster differs * regenerate the projections after the main merge * fourth shrink: the XL-0N row dissolved when its own PR merged * close the import block the conflict boundary split * the assembler stays total: the merge reintroduced the absorbing Optional this branch dissolved * the rebuilt artifact literal carries the field main added * the relocated spelling names where it went, and the matched variant is imported Two repairs, both surfaced by composing with main rather than by any defect in either side alone. The merge with main brought #9824, which added a `target` field to AdmissionSubject::Binding: the module the admission's own PR moved the name TO, and the referent of the consumption proof. Our two SPARK-PAIR-0 P0-C3a rows predate that field, so git merged both sides cleanly and the tree did not compile. The value is verified rather than copied from our own label -- spark_serving_linger_probe_words is declared in dag/gunbc/spark/serving_observe.dag, whose module line is gunbc.spark.serving_observe. serving_execution_schedule.dag matched SparkServingUserUnitActivityAddress at four sites without naming it in its import block. Peer modules list it explicitly, so it is now listed here. This is import hygiene, not a resolution repair: the module resolved and typechecked before the change -- measured, by reaching evaluation and failing on a call-contract mismatch, which occurs after resolution. * the outcome census is one traversal, and the linger question short-circuits Two cost-shape repairs from review 57946. The review named them as canonical- query violations; the defects are real but they are §6 bare-minimum-cost, and recording the mechanism correctly matters because the two readings send a reader to different remedies. spark_serving_acquisition_receipt_of built its three outcome counters as three `length(filter(...))` passes over one capture list, each filter calling its own Bool predicate that exhaustively matched the same closed outcome. Three traversals and three matches to answer one question -- the copied-accumulator shape DESIGN §6 says is always fixed regardless of the realized n, since n tracks the probe roster and is not time-stable. One fold now answers all three, bound once at the use site, and the match stays exhaustive so a fourth outcome arm still fails to compile rather than being silently counted as neither. The three predicates are deleted; they had one caller each. spark_serving_projection_linger_enabled asked an existence question as `length(filter(...)) > 0`, which builds the whole filtered list before comparing. It now uses `any`, which short-circuits. Behaviour preserved by execution, not by inspection: the observation transaction roster is 23/23 and the observe roster is 68/68, including changed_capture_outcomes_move_the_line_the_report_emits, which is the discriminating claim for outcome counting. Review 57946's third finding is NOT addressed here because it is wrong, and the roster's own gate is what settles it rather than an argument. See the PR reply. --------- 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>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 2, 2026
…nd record the dead arm that makes it unbounded #9824 moved the transition-admission roster's cleanup bill off bystanders and put the deletion obligation in one arm: a consumed row refuses on the first change whose diff touches the roster's own source file. That arm cannot fire. `run_required_wave_admission` derives `roster_touched` from the head side returned by `diff_sides`, whose final act retains only paths satisfying `in_sweep_scope` — a predicate that opens by requiring a `.dag` suffix — while `ADMISSION_ROSTER_REL_PATH` names a `.rs` file. So `roster_touched` is false on every production run and `consumed_due` in `claim_executor::report_wave_admission_outcome` can never be true. The repository already executes the discriminating fact: the last assertion of `a_rename_contributes_its_source_to_the_base_side_and_its_destination_to_the_head_side` says a `src/v1/stage0/src` path enters neither side of the diff. Two ledger rows, no behaviour change: - `gunbc.rung_drop namespace_admission_consumed_row_deletion` — previous rung 2, temporary rung 1, with the population (the rows for which `admission_consumed_at_base` holds; at this head, exactly the two RLM-2b rows, consumed since the commit that authored them) and a restoration trigger stated as the CAPABILITY plus what it must be sufficient for. It corrects #9824's declared window rather than restating it: "roster-use bounded" is false in execution, so the window is unbounded, full stop. - `gunbc.recurring_failure_mode incidental_denominator_as_wall` — a second receipt at the inverted polarity. The existing specimen is a filter that accidentally keeps an operation safe; this one accidentally kills a declared wall. Same mechanism, same recognition rule unamended, so no new class is minted. The lifetime record behind the population is re-derived by `git log` over `src/v1/stage0/src/namespace_wave_admission.rs`, reading added and removed `label:` lines per commit — named rather than transcribed. DESIGN.md and docs/design-ledgers.md are the projections; regenerated with `generated_artifact_gate.dag --function main_wet`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Et86vcNb8YdMQSSPc3pbhR
gunbai-bot Bot
added a commit
that referenced
this pull request
Sep 2, 2026
…nd record the dead arm that makes it unbounded (#10007) * Declare the namespace admission consumed-row window as a rung drop, and record the dead arm that makes it unbounded #9824 moved the transition-admission roster's cleanup bill off bystanders and put the deletion obligation in one arm: a consumed row refuses on the first change whose diff touches the roster's own source file. That arm cannot fire. `run_required_wave_admission` derives `roster_touched` from the head side returned by `diff_sides`, whose final act retains only paths satisfying `in_sweep_scope` — a predicate that opens by requiring a `.dag` suffix — while `ADMISSION_ROSTER_REL_PATH` names a `.rs` file. So `roster_touched` is false on every production run and `consumed_due` in `claim_executor::report_wave_admission_outcome` can never be true. The repository already executes the discriminating fact: the last assertion of `a_rename_contributes_its_source_to_the_base_side_and_its_destination_to_the_head_side` says a `src/v1/stage0/src` path enters neither side of the diff. Two ledger rows, no behaviour change: - `gunbc.rung_drop namespace_admission_consumed_row_deletion` — previous rung 2, temporary rung 1, with the population (the rows for which `admission_consumed_at_base` holds; at this head, exactly the two RLM-2b rows, consumed since the commit that authored them) and a restoration trigger stated as the CAPABILITY plus what it must be sufficient for. It corrects #9824's declared window rather than restating it: "roster-use bounded" is false in execution, so the window is unbounded, full stop. - `gunbc.recurring_failure_mode incidental_denominator_as_wall` — a second receipt at the inverted polarity. The existing specimen is a filter that accidentally keeps an operation safe; this one accidentally kills a declared wall. Same mechanism, same recognition rule unamended, so no new class is minted. The lifetime record behind the population is re-derived by `git log` over `src/v1/stage0/src/namespace_wave_admission.rs`, reading added and removed `label:` lines per commit — named rather than transcribed. DESIGN.md and docs/design-ledgers.md are the projections; regenerated with `generated_artifact_gate.dag --function main_wet`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Et86vcNb8YdMQSSPc3pbhR * Retire the drop by its trigger: #10014 restored the capability the row was declared for The row's restoration trigger names a capability — the consumed-row deletion obligation observed by a mechanism that EXECUTES on the required path — and gunbc#10014 (962d928) delivered it: `diff_sides` reports what a change touched once and unfiltered, each consumer applies its own scope at its own point of use, and the verdict moved onto the wall as `wave_admission_refusal`. §4b(3) retires a drop by its trigger and by nothing else, so this one is retired the day it was declared. The row is kept rather than deleted, because the window was real: it ran from gunbc#9824 on 2026-08-31, when the obligation was declared over an arm that could not fire, to #10014 today. `docs/design-ledgers.md` renders the whole roster and still carries it in full; DESIGN.md's "ones standing today" list is `standing_rung_drops()`, which filters the `Retired` arm, so the bullet correctly disappears from the document loaded on every turn. Landing it as `Standing` would have published a claim already known to be false into that document — the exact harm `RungDropStanding` was introduced to prevent. One evidence obligation is named on the restored capability rather than left to be rediscovered: the obligation is observed by a PAIR of executing probes, not yet by a single one walking a real diff through to a refusal. That is evidence owed on a capability that exists, so it is recorded as an obligation and is neither a new drop nor a next-rung trigger. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Et86vcNb8YdMQSSPc3pbhR --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Sep 12, 2026
…'s
A sibling lane landed the identical gunbc#11137 row deletion first, so
src/v1/stage0/src/namespace_wave_admission.rs conflicted. Resolved to MAIN's
version of that file verbatim, which is this file's own documented convention for
the case -- the note above the thirty-fourth entry records "THIS BRANCH'S OWN
DISSOLUTION ENTRY FOR THE gunbc#10324 ROWS IS DROPPED, NOT RENUMBERED" for exactly
this collision. My THIRTY-SIXTH DISSOLUTION entry is therefore dropped rather than
renumbered or merged alongside.
TAKING MAIN'S SIDE IS NOT A SHORTCUT HERE, IT IS THE BETTER AUTHORITY. gunbc#11165
("Derive admission consumption from exact candidate sets") landed in the same range
and rewrote the retirement note itself, so main's copy carries the mechanism
owner's own words plus the evaluator change behind them. Taking my side would have
reverted that code.
AND #11165 ANSWERS THE QUESTION MY DISSOLUTION RECORDED AS UNVERIFIED. I noted that
the row reported STALE where #9824's ConsumedByMerge looked applicable, said I had
read none of that code, and left it to the mechanism's owner. Their note gives the
cause: "The old sentence predicted CONSUMED for a two-member result that the
singleton proof could never accept" -- the consumed proof required a singleton
candidate set and this row's was two-member. The symptom was real, the restraint
was right, and the repair belonged where it landed.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012xQnkeiJ1pnEpMgqh3dE1e
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.
Authorized by the XL-N manager after the eighth dissolution: the consumed-by-merge/author-error split in the namespace admission roster, so the roster's cleanup cost stops being billed to bystanders.
The defect (mechanism named in the authorizing exchange):
NAMESPACE_TRANSITION_ADMISSIONSis main-resident, and adjudication is bidirectional — every row must match a delta. A relocating PR's rows are required at instant N (its own CI) and poisonous at instant N+1 (after its squash-merge, base+head both carry the relocation, so the rows can never match again) — and the resulting stale refusal reds every unrelated PR until a hand-cut dissolution lands (eight so far; #9797, #9820). Consumed-by-merge and author-error rendered as one diagnostic with opposite owners and opposite remedies.The bystander cost, caught in the act while this fix was being built: #9823 (quick-eagle-249's MachineShape construction-wall repair — a lane with nothing to do with the roster) went red on the exact five #9784 rows, and cleared with no change of its own once #9820's dissolution merged. The bill is itemized: one CI round plus a diagnosis cycle — the failure presented as the payer's own PR being broken, and that diagnosis time appears in no dissolution count. The same run's floor executed correctly (planned 3249 = executed 3249, its changed witness passed), isolating the roster as the only defect. Under this PR's split those five rows would have been typed
ConsumedByMergeand #9823 would never have seen them.The split — decidable, so a wall: an unused row is typed
ConsumedByMergeonly on the positive proofadmission_consumed_at_base: the base itself already satisfies the admitted relocation (Binding: the base binds the exact (module, declaration, spelling) to a singleton set equal to the row's declaredtarget; Membership: the base membership already carries the target). Everything else unused remains anUnmatchedAdmissionrefusal — the consumed arm is unreachable by fallthrough.AdmissionSubject::Bindinggains the relocationtargetfield as the proof's referent (a relocation admission that cannot say where the name went is not one).Where the deletion obligation lands, and the honest window: a consumed row refuses nothing for unrelated runs (typed receipt, printed in every run), and the phase fails when the run's own diff touches the roster file (
ADMISSION_ROSTER_REL_PATH) while consumed rows stand — every future relocation PR touches that file by construction, so consumed rows persist, visible, at most until the roster's next use. That is enforcement at the next touch, not a scheduled sweep; stated plainly: wall-clock unbounded, roster-use bounded, bystander-invisible.Retired by (the capability, not an artifact): admissions bound to the delta content they admit, adjudicated per run and never resident on main — which makes a stale-able row unwritable. That waits on the declaration-index
.dagcarrier; this PR is the interim wall and names its own successor.Evidence (tests/namespace_wave_admission.rs, 45/45 green; clippy --all-targets green):
an_unmatched_row_refuses_and_is_never_typed_consumed— a row provable against neither side must land instale_admissionsand NOT inconsumed_admissions; under the wrong implementation (consumed as the else-arm of "matched no delta") the second assertion reds, so the pair discriminates on the split itself.a_consumed_row_is_typed_and_does_not_red_an_unrelated_run.one_run_separates_a_consumed_row_from_an_unmatched_one— one run, both rows, exactly one in each vec.an_ambiguous_base_binding_is_not_consumption— an ambiguous base binding does not prove consumption and still refuses.The five live #9784 roster rows gain their
target(gunbc.boot_artifact); after #9820 (the eighth dissolution) merges, this branch rebases onto the emptied roster. Not merged by me — XL-N runs the census.🤖 Generated with Claude Code
https://claude.ai/code/session_01QhdaHkmZPoQoeUWz5V2mzF