Repository navigation
Make the quarantine partition disjoint (111 + 5 + 313 = 429), and correct the run id for the eight that tipped - #8634
Merged
Merged
Conversation
The rung-drop declaration is the one artifact whose entire job is making the
coverage loss loud, and its total was an estimate. Two independent derivations
now agree exactly, and both are written down so the figure can be re-checked
rather than trusted.
ROUTE A -- the two floor runs on main, differenced:
pre 32177951514 planned=9420 passed=8951 known_red=367 stale=5 refused=102
post 32193032348 planned=8997 passed=8638 known_red=358 stale=0 refused=0
313 + 9 + 102 + 5 = 429 identities left the floor.
ROUTE B -- the source: 429 `test fn` across the 38 modules #8457 relocated.
The 6-identity gap against planned (423) is six identities that LANDED between
the two runs, stated so the next reader does not read 423 as the answer.
Two counts that were circulating at once are settled with it: the module count
is 38 (21 + 16 + 1), and the problem population is 107 -- 102 BudgetInterrupted
plus the 5 that PASSED over budget. Different observations, different remedies.
WHAT IS STILL NOT DERIVED is named rather than assumed: which individual
identities make up the 313. The floor reports per-identity outcomes only as log
lines, and a scraped log is not an oracle. That needs an identity-grained
receipt from the floor, not a better scrape.
AND ONE FINDING THE QUARANTINE PRODUCED BY ACCIDENT, recorded because every
decomposition PR scheduled on this lane will hit it: a cost figure here is not a
property of its witness. emitter_nested_refinement_cast_witness_test
single_refinement_carrier_emits_no_unsupported_cast cost 746ms pre and 45941ms
post, unchanged in itself, with its own sibling at 763ms -- the relocation took
out every earlier caller of compile_dag_rust_emit_check, so the one-time
build_module_path_index_from_witness_roots construction landed on the first
survivor and made it main's only failure. Splitting or relocating a module MOVES
its shared fixed cost onto the next survivor rather than removing it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0185Q2N7fp1i5WPJLNpMBu47
…ouble-counted
Both sides landed a correction to the same rung-drop declaration within the hour,
and neither is simply right. main (tidy-lark-471's external review) had the
roster arithmetic I did not: the delta is 111, not 108, and the roster carries
358 while the line said 361. Those are taken verbatim.
But main's partition -- "111 enrolled, 111 over-budget, 207 healthy" -- sums to
429 only by counting the 102 rows that are BOTH enrolled here AND over budget on
both sides of the sum. Enrolment and cost are independent axes. The partition is
now taken on enrolment alone, with the cost facts stated inside each part, and
the pre-quarantine run partitions the roster exactly (469 = 367 held red + 97
budget-refused + 5 passed over budget), so every part is checkable:
111 enrolled and removed = 9 held red + 97 budget-refused + 5 passed-over-budget
5 unenrolled and budget-refused (that run reported 102; only 97 were enrolled)
313 passing when relocated, of which 9 later tipped once wave 1 removed the
slow head, leaving 304 never observed over budget
111 + 5 + 313 = 429, and grep -c '^test fn' over the 38 modules is also 429.
It also records that the problem population is not one number: 107 at quarantine
time, 116 including the rows that tipped afterwards, 102 for the interrupted
rows alone. Several were circulating at once because they answer different
questions.
My own competing partition and the "TWO NUMBERS THIS SETTLES" paragraph are
deleted rather than kept beside main's -- two partitions of one population in
one file is the dual authority this carrier exists to prevent. What survives
from my side is the second derivation (run-counter differencing, which
reproduces the same split without reading the tree), the statement that identity
grain is NOT derived and needs a receipt from the floor rather than a better log
scrape, and the fixed-cost relocation finding.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0185Q2N7fp1i5WPJLNpMBu47
…section Operator ruling, 2026-08-18. Three corrections, all to wording this file already carried, none to code. 1. THE LAW WAS STATED TOO WIDE, and that was this note's own error. It said every restoration receipt is confounded until the shared authority is paid in preparation. The true statement is narrower: a restoration receipt is confounded WHEN CHANGING THE POPULATION CHANGES WHICH CLAIM PAYS AN UNREPORTED LAZY SHARED FILL. Preparation is the remedy for that one class, and #8470 has already applied it to the concrete module-path-index instance. It is not the remedy for closure pollution, fixture/live-index coupling, repeated end-to-end crossings, duplicate coverage, whole-tree censuses, or genuine size-scaling cost -- separate classes with separate owning layers. Generalizing one confounder into a universal prerequisite would have serialized four lanes behind one that is already partly done. 2. 97 AND 102 ARE BOTH CORRECT AND NAME DIFFERENT SETS. Writing either as a bare `budget_refused` is what made the earlier accounts read as contradictory, so the intersection is now spelled out: budget-interrupted, global 102 enrolled here AND budget-interrupted 97 unenrolled AND budget-interrupted 5 enrolled here AND completed-over-budget (stale_quarantine) 5 3. TWO CLAIMS THAT READ STRONGER THAN THEY ARE. This block is supporting evidence for the identity-grained receipt, not a substitute for it -- aggregate arithmetic is exact and says nothing about WHICH identities. And `budget_refused=0` on the post run is not the population disappearing; it is the floor no longer executing it. The 116 identities ever observed over budget or failing are still owed a remeasurement against a cause. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0185Q2N7fp1i5WPJLNpMBu47
…rammar rebuild quiet-bee-353 measured it on gunbc#8478 (remote executor, release claim_batch) rather than reasoning about it. Folding the file from nineteen grammar builds to two did not pay -- 210.9s for the two folded claims against ~208s for the fourteen they replaced -- so the fold was reverted and the file left byte-identical to main. Solving the terms out of those runs: a dag_grammar() construction is ~0.5s and a single three-line parse through the interpreted frontend is ~12s. The apparatus is not the cost. The parse is. Two consequences, both recorded on the carrier that made the claim: The arrow row must NOT be planned as a witness-side repair. Twelve seconds to parse three lines is a frontend cost-shape defect, and it is plausibly the real subject behind several rows in this quarantine rather than an evaluation-context tax. "No witness has yet been found that is genuinely slow" is no longer established. That sentence is corrected rather than deleted because it was load-bearing for how this entire lane was planned -- it licensed treating every relocated row as an apparatus problem. The two measured extremes (71s -> 70-85ms, 12s -> 31ms) remain apparatus. That the residue is apparatus does not follow and is now open. Same class, same session, what DID measure and is green by execution: e0308 nine witnesses 2450ms -> five 1346ms, emitted lib.rs three -> two 561ms. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0185Q2N7fp1i5WPJLNpMBu47
…he counters tidy-lark-471's catch, handed over rather than pushed by them so that two sessions do not edit one paragraph; #8480 closes into this. I verified it against the run counters rather than taking it: 32186963581 planned=9228 passed=8859 known_red_held=361 failed=8 32189985063 planned=8995 passed=8636 known_red_held=358 failed=1 32193032348 planned=8997 passed=8638 known_red_held=358 failed=1 Only one run observed eight. The straggler attribution to 32193032348 stands. The error was in the text I rewrote and I carried it through unchanged, which is the point worth recording: this file's own SECOND WAVE paragraph named 32186963581 correctly the whole time, so one file gave two accounts of one population and three rewrites -- sleek-moth-351's, tidy-lark-471's, mine -- walked past the contradiction. sharp-raven-273 and quiet-ibex-39 each measured the mismatch independently before it was fixed. The note now says the counters decide it, not the neighbouring sentence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0185Q2N7fp1i5WPJLNpMBu47
…ver leave Derived, not suspected. 358 enrolled identities here, 669 frozen rows over 147 entries in gunbc.witness_deferral_freeze, intersection 40 at identity grain. This roster is admissible ONLY because it is temporary, and its only removal path is OBSERVING a row pass. Those 40 sit in files the freeze defers, so nothing executes them, so they can never be observed passing, so the self-emptying rule cannot fire for them ever. Two carriers each behaving correctly compose into permanent residents of a roster whose entire defence is that it is not a skip list -- and neither carrier can see the other, so nothing reported it. The freeze's arms already say a deferred row is NOT covered; this file already says an indefinite row is a defect nobody owns wearing a receipt. The join was simply never taken. The intersection should refuse rather than be counted: enrolment here and path-deferral there are contradictory claims about one identity. Surfaced by quiet-bee-353 chasing two reds in dag_add_emit_round_trip_test and confirming them pre-existing against MAIN's head 5ee2572 -- all seven claims run detached, verdicts identical to their branch, so not caused by their diff. At 2ms and 7ms they are not a cost row at all. They are a real defect nobody has been looking at because nothing runs the file, which is precisely what the deferral was hiding and what the join makes visible. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0185Q2N7fp1i5WPJLNpMBu47
still-wolf-510 refuted it against a live run, and they are right. I asserted that 40 identities enrolled here and path-deferred in witness_deferral_freeze can never leave this roster because nothing executes them. That was an assumption about a mechanism I did not read. The required floor excludes by AUTHORED MODULE NAME via long_home_prefixes. It never consults the freeze. The freeze is an ADMISSION standing -- whether a row may remain without an executing consumer -- and the floor gate tolerates LegacyFrozenPathDeferral. It does not suppress execution. Frozen path and discovered module are independent facts. Verified on green main run 32201531653: planned=9022 executed=9022 passed=8664 known_red_held=358 failed=0, with intersection members present in the output -- test.claim.ci_exclusion_proof.ci_exclusion_proof_sentinel FAILED in 13640ns, a row executing and held exactly as enrolled. They can leave the moment they pass. The defect is real but inverted and much smaller: the FREEZE rows are stale, asserting path-deferral for identities that have an executing consumer. The disposition is to retire those freeze rows with a receipt, not to find the roster rows a cadence. The construction wall still earns its place -- the intersection is a contradiction whichever way it resolves, and nothing detects it today. Kept rather than quietly rewritten, because the error is this file's own subject: I joined two carriers correctly and then read one carrier's meaning off its name instead of its mechanism -- the stale-citation class -- while correcting three other people's counts in the same file. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0185Q2N7fp1i5WPJLNpMBu47
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.
Summary
src/v2/workflow/floor_expected_red.dag's declared rung-drop block stated apopulation that did not partition. It read 111 enrolled, 111 over budget, 207
healthy — which sums to 429 only by counting the 102 rows that are BOTH enrolled
here AND budget-interrupted on both sides of the sum. Enrolment and cost are
independent axes; the earlier text treated them as one.
This corrects the block to a disjoint partition taken on enrolment, with the cost
facts stated inside each part:
It also fixes a wrong run id that survived three rewrites of this block, including
mine: the eight that tipped were observed in
32186963581, not32189985063. Therun counters decide it without reading any prose —
32186963581 failed=8 known_red_held=361,32189985063 failed=1 known_red_held=358,32193032348 failed=1 known_red_held=358. Only one run observed eight. The SECOND WAVE paragraphlower in the same file named the right one the whole time: one file, two accounts of
one population, which is why the counters and not the neighbouring sentence are the
authority here.
And it separates three figures that were circulating as if they were one, because
each names a different set and none may be written as a bare
budget_refused:102 budget-interrupted globally · 107 over-budget-or-failing at quarantine time
(102 + 5 passed-over-budget) · 116 including the 9 that tipped afterwards.
Why this matters beyond the file
Per DESIGN §4b, a rung drop must declare a bounded population, and per the
floor_expected_redshrink-monotonicity thread, sharp-raven-273's monotone-shrinkwall reads this carrier as its baseline. A stale or non-disjoint count here is
load-bearing for work that is not mine. A bounded population is the one thing a rung
drop must not round.
Attribution
The 358/111 corrections are tidy-lark-471's external review, not mine. The
disjointness defect and the run-id correction are mine, and both were found by
re-deriving the partition rather than re-reading the prose.
Test plan
git diff origin/main...HEAD -- <file> | grep -E '^[+-]' | grep -v '^[+-][[:space:]]*//'returns empty — no non-comment line is added or removed. 134 insertions,
14 deletions, all
//.//block on a module-scope declaration(DESIGN §4c admits exactly this form; trailing and in-body forms refuse).
target/release/gunbcin this worktree, and awhole-tree build or floor run is a CI job rather than a session job under the fleet
resource policy. Parse and floor verification are relied on from CI on this PR.
grep -c '^test fn'over the 38relocated modules) and against the named run counters. None is copied from another
session's measurement.
Work item:
fix floor over budget tests(dashboard work item — no GitHub issue to close).