Repository navigation
Enrollment cannot hold a claim that was never decided: the other two non-verdict outcomes - #8959
Merged
Merged
Conversation
added 5 commits
August 23, 2026 00:30
… non-verdict outcomes An expected-red witness that THREW, or that answered with something that is not a Bool, was counted as "known-red held". Held asserts the claim RAN AND FAILED as predicted; neither of those produced a verdict for the enrollment to agree with. The harm is that a known-red witness which ROTS -- errors on every run instead of executing -- is indistinguishable from one still doing its job, forever, and its enrollment never comes up for review. THIS FILE ALREADY SETTLED THE PRINCIPLE. A previous repair split budget interruption and unresolved host tools out of Held, and wrote the rule down: "Enrollment cannot hold a claim that was never decided." A runtime error is not a semantic verdict either, and the principle does not distinguish being cut off at a budget from throwing. That repair covered two of the four non-verdict outcomes and left two folded. AND IT DESCRIBED ITSELF AS HAVING COVERED ALL OF THEM. The doc comment on CiWitnessVerdict::from_outcome claimed "the counting side already refuses exactly that absorption", while expected_red_arm still read `Fail | NotBool | RuntimeError => Held`. That sentence is corrected here rather than quietly widened: an unexecuted claim standing where an executed one appeared to be is why nobody looked again. TWO SITES, NOT ONE. claim_disposition (outcome -> disposition) and expected_red_arm (the console/counting path) are two derivations over one row. Fixing only the first would have made the ledger and the console disagree -- a new cross-derivation disagreement created by the fix for a cross-derivation disagreement. The correct dispositions were not missing vocabulary: ObservationUnreadable- BeforeVerdict and RuntimeErroredBeforeVerdict already existed and were already used, one line away in the same match, for the unenrolled case. Expectation is simply no longer consulted for outcomes that produced no verdict. WIRED TO BLOCK, WHICH WAS NEARLY THE DEFECT IN THE FIX. The two new collections are read by required_floor_outcome_is_clean. Without that they would have been populated, printed, and never consulted -- counted coverage that gates nothing. The "SEVEN CAUSES" count in that predicate's doc comment is now NINE; that sentence warns that it went stale once before, and it had. HOW THIS WAS FOUND: not by review. The terminal-ledger cross-check on gunbc#8909 refused a real floor run, naming one identity whose seed disposition disagreed with the grammar's derivation. V1 SEED ADMISSION: defect repair under the purpose test -- the floor's known-red accounting decides whether required CI is green, and an enrollment that holds an undecided claim is a fail-open in the mechanism the v2 self-host program depends on for its own verification. BLAST RADIUS IS NOT YET MEASURED AND THIS PR IS THE INSTRUMENT: the count of enrolled identities that reclassify is exactly what the required run now reports, per new counters. Read them before merging.
…ntinuations Review 54894 caught both new `format!` literals rendering with a hard newline and ~26 leading spaces mid-sentence. The diagnostics were correct and unreadable, which for a message whose whole job is to tell an author which enrollment rotted is most of its value gone. THE MECHANISM IS MINE, NOT RUSTFMT'S. I wrote these through a Python heredoc, and inside a Python `"""..."""` literal a backslash followed by a newline is a PYTHON line continuation: it consumed the backslash and left the source indentation as literal spaces in the Rust string. The Rust continuation I believed I had written never existed. This is the same defect class as review 54771 earlier today, reached by a different route -- there I mangled a string by hand, here my authoring tool did it while I read the intended text rather than the produced text. VERIFIED IN THE COMPILED BINARY, not in the source, because the source is exactly what misled me the first time: `strings` on the built claim_executor now shows both messages as single-spaced prose across every continuation boundary. Also re-checked that every `\` continuation in the touched region is preceded by a space, since a missing one silently joins two words.
…t caught me `ExpectedRedPartitionInexact` refused the run: held=35 ... roster=207, with 172 identities in neither arm it knew about. The invariant's own comment says it "fails loudly if a later edit adds a third arm that quietly swallows rows", and that is precisely what it did to this change, one site short of complete. The sum is now eight-way and the refusal names all eight. The comment records that it caught this edit, because an invariant whose value is demonstrated is worth more than one whose value is asserted. WHAT THE REFUSAL MEASURED, which is the reason this PR exists: roster 207 · held 35 · now_passing 0 · budget_refused 0 · passed_over_budget 0 host_tool_unresolved 0 · host_effect_refused 0 RUNTIME-ERRORED 172 · observation-unreadable 0 172 of 207 enrolled expected-red identities — 83% of the roster — are held open by claims that THREW and never produced a verdict. Before this change every one of them counted as `known-red held`, i.e. as a witness running and failing exactly as predicted. That is DESIGN §5's absorbing fallback with a receipt: the deficit's frequency was zero BY CONSTRUCTION, so it never ranked for fixing, and the roster grew a graveyard nobody could see. The question of whether those 172 share one root cause was not merely unanswered, it was unaskable. NOT PUSHED YET AND NOT READY TO MERGE. These two arms are wired into `required_floor_outcome_is_clean`, so as it stands this reds the floor for every lane. Staging the 172 is a decision above this diff.
TWO CHANGES, AND THE SECOND IS WHAT MAKES THIS SHIPPABLE. 1. THE CAUSE CENSUS. 172 throws is not 172 defects until something says whether they share a root, and seeding a 172-row roster for what may be one fix would render a concentrated defect as distributed debt — worse than the absorbing counter it replaces, because it reads as honest accounting while being wrong about the SHAPE of the problem, and every later reader prices 172 repairs against a single cause. So the throws are grouped in-process by a normalized signature (first twelve whitespace-separated tokens, capped) and reported largest-class-first on the `[floor-known-red-causes]` line. Normalized rather than verbatim because identities, paths and offsets differ per row and would make every throw its own "cause" — precisely the answer the census exists to avoid assuming. Printed beside the known-red summary, which is reached on every run, rather than inside the partition refusal — that refusal returns before the per-identity report runs, so on exactly the run where the evidence matters it was computed and dropped. That is how the first measurement arrived as counts with no identities. 2. THE TWO ARMS NO LONGER GATE. `required_floor_outcome_is_clean` is back to seven causes. Reporting the distinction honestly and BLOCKING on it are separate decisions with separate owners: blocking reds lanes that have nothing to do with the defect, which needs an approved design and a shadow phase rather than an author's judgement. The reporting half does not have to wait for that. The de-collapse itself is unchanged and is the actual repair: enrolment stops discarding `RuntimeErroredBeforeVerdict` / `ObservationUnreadableBeforeVerdict`, two dispositions the code already had and already used correctly for unenrolled rows. The distinction was being destroyed on exactly the rows nobody watches. The exactness partition stays eight-way — it must account for every enrolled identity whether or not the arms gate, and it is the invariant that caught this change one site short.
…47-known-red-nonverdict
briansrls
pushed a commit
that referenced
this pull request
Aug 23, 2026
…e roster edit handed off Three things, in the order they were found. THE PARSE ERROR IS MINE AND IT IS THE PLAINEST FORM OF THE FAILURE. The four per-host DIMM expectations were written as `data X: HostDimmExpectation =` with the initializer on the NEXT line, which the grammar does not take. CI refused the whole module index. I pushed .dag I had never compiled -- typecheck-by-eye is not a consumer, and DESIGN says so in as many words. Initializers are now on one line and this branch is verified locally before pushing rather than after. THE SATURATING SEARCH BOUND IS AN ABSORBING FALLBACK, AND RAISING 8 TO 40 WOULD HAVE LEFT IT. admitted_width_charging folded a bounded range and returned the last admissible element, so a host admitting MORE than the bound got the bound back as a number indistinguishable from a real measurement. That is not hypothetical: it fired. From the 2026-08-22 upgrade until now, srv3 and srv4 admitted 29 against a bound of 8 and reported exactly 8, so two of tonight's six failures were rows comparing the bound to itself. The deficit never surfaced as itself -- it arrived as an unrelated inequality, which is exactly the frequency-zeroing DESIGN 5 describes. The fold now answers a typed verdict: WidthSearchFound when the largest admissible width is strictly inside the range, WidthSearchSaturated naming the host and the bound when the top is still admissible -- at which point the search has not measured a width, it has run out of room to look. The Int projection converts saturation to -1 rather than to the bound, so an assertion fails loudly instead of passing at the ceiling. THE RANGE IS A PARAMETER SO THE REFUSAL HAS AN AUTHORABLE RED. No real host admits 40, so a saturation arm written only against the standard range could never be driven red by any input -- permanently green by construction, and worse than absent because it would be cited as coverage. DESIGN 4b says to ask whether the RED is authorable BEFORE writing the check, and to judge that against what a FIXTURE may author rather than what the corpus contains. admitted_width_search_within takes the range and its top, so saturation_refuses_rather_than_reporting_the_ceiling hands srv3 a range of 1..3 and gets the refusal, with a positive control on srv2 that stops the arm being satisfied by refusing always. no_enrolled_host_saturates_the_standard_search_bound is the quiet guard beside it: mechanism exists, reachable from this operation's own denominator, currently unoccupied, and red the day a host outgrows 40. THE SIX-ROW EXPECTED-RED UN-ENROLMENT IS DROPPED AND HANDED TO #8959, which needs the same nine-element list edited to present anything but a red and needs none of this lane's memory knowledge. Two lanes editing one shared row is a conflict neither wanted; the witnesses stay put in both diffs and only the enrolment moves. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Aug 23, 2026
Merged
briansrls
pushed a commit
that referenced
this pull request
Aug 23, 2026
…dated are re-derived (#8976) * CPU becomes an admission axis, and the widths the DIMM upgrade invalidated are re-derived Main is red. #8947 replaced srv3/srv4's usable-RAM row -- a 125 GiB conservative lower bound borrowed from a 2026-07-16 srv3 reading -- with measured /proc/meminfo MemTotal of about 502 GiB, and left nine floor claims asserting the widths the old bound produced. This fixes all nine plus two more that would have broken next, and lands the CPU axis they cannot be honestly closed without. WHY THE CPU AXIS IS IN THIS DIFF AND NOT A FOLLOW-UP. host_memory_admitted_width answers what MEMORY admits, and 29 is now the true answer on srv3/srv4. But gunbc_runner_slots_per_host took a minimum over memory and disk only, and disk is DiskWidthUnconstrained on both -- so the minimum degenerated to memory alone and a corrected 29 would have COMMITTED 29 runners on a 128-core machine. The honest literal is only safe beside a CPU term. Either both land or neither does. host_cpu_admitted_width = cited cores / cores per slot = 128 / 6 = 21 Cores are read from extdeps.cpu.ampere altra_max_m12830_catalog rather than written down, so a host that is not an M128-30 cannot silently inherit the width; that the fleet IS uniform is checked by fleet_processor_verdicts rather than assumed here. CORES PER SLOT NOW DERIVES INSTEAD OF BEING AUTHORED. It was a literal 8 with no stated relation to the 16 GiB MemoryMax beside it, so the two could drift and only an author's memory tied them together. It is now ceil(memory_max / 3 GB) = 6, at the 1 core : 3 GiB shape the operator adopted 2026-08-23 -- the arm64 ratio Ubicloud publishes across its whole standard profile, adopted because a published provider catalog is a real reference and an invented number is not. Rounding is UP because that yields FEWER slots (128/6 = 21, not 128/5 = 25) and over-admitting is the harmful error. The wall's cores conjunct changes with it: it was `== 8`, a literal restating a literal twenty lines above -- the measure() == measure() shape that module's own oracle note says it purged -- and is now the relation cores * per_core >= memory_max, which a wrong rounding direction fails. SRV1 AND SRV2 GET THEIR FIRST MEASURED MemTotal, which is what puts srv1 at 21. srv1 reads 502.24 GiB and srv2 134314512384 bytes, both over SSH 2026-08-23, srv2 corroborated by its own docker daemon. srv2's lands about 96 MiB ABOVE the bound it replaces -- the bound was not merely loose there, it was on the wrong side, and a lower bound that is too high is not conservative at all. That retires the last consumer of gunbc_ci_conservative_lower_bound_usable_ram, so it is DELETED and its scaffold disposition discharged to Terminal: no arm remains in which one host's measurement answers for another's. The HostUsableRamConservativeLowerBound VARIANT stays -- nothing constructs it today, and an arm nothing currently occupies is a quiet guard rather than a dead one. host usable memory cpu committed srv1 502.24 GiB 27 21 21 srv2 125.09 GiB 5 21 5 srv3 502.25 GiB 29 21 21 srv4 502.25 GiB 29 21 21 Memory bound every host in this fleet's history until yesterday and now binds only srv2, whose 64 GiB install failed training and was reverted. THE TWO REAL DEFECTS, as against the stale claims. installed_bom_reconcile's two live-population rows routed srv1's observation through a local uniform_expectation() that hardcoded the Hynix catalog, so when #8947 moved srv1's production expectation to Samsung the row moved and the copy did not. Fixed by removing the seat rather than the copy: the four per-host expectations are now named data in fleet_physical_inventory and the witness imports srv1_dimm_expectation. uniform_expectation survives for the constructed fixtures, which legitimately author their own. WHAT THE STALE CLAIMS TAUGHT, since five of them needed rewriting rather than renumbering. The control-plane placement pair's answer INVERTED: the 2 GiB probe now costs srv3/srv4 a memory slot and srv1 nothing, and reaches the COMMITMENT only on srv2, because everywhere else CPU binds well below memory. The sessions-charge demonstration moved from srv1 to srv2 -- both its arms conserve on srv1 now, so the discrimination was gone, and relaxing the assertion until it passed would have silently retired a live claim whose example had grown out of it. And admitted_width_charging searched 1..8 under a comment calling that "wider than any host can reach", which stopped being true at 502 GiB: an outgrown search bound returns its own ceiling, so every host would have reported exactly 8 and the rows would have compared the bound to itself. Two witnesses that were passing on main are updated because this change breaks them, and one is renamed for cause: runner_slot_allocation_committed_widths_MATCH_MEMORY_ADMISSION stated a coincidence as a law. Committed equalled admitted only while memory bound every host, and a name that encodes a coincidence teaches the next reader the wrong invariant. CORRECTING THE LITERALS DOES NOT DISSOLVE THE SECOND REPRESENTATION. host_memory_admitted_width still authors four numbers that derived_width_reproduces_every_authored_literal then re-derives and joins to them -- validation standing where construction was available. The construction fix is for the function to CALL that derivation, and it is blocked on an import cycle: gunbc.ci_floor_measurement imports runner_slot_allocation for the slot shape, so runner_slot_allocation cannot import the measurement. Breaking it means moving the slot shape to its own authority across roughly twenty-five files, and stays a separate change. This leaves a corrected copy where an uncorrected one stood. Six samsung_dram_module rows are removed from floor_expected_red -- an edit to a nine-element list, not a deletion of it; the three still-red rows stay. The witnesses themselves are kept as permanent regression controls. No CPU reservation is modeled. Every core is offered to slots, so the host, its kernel and the session containers on srv1/srv2 are charged nothing on that axis -- a real gap, confined to CPU, where oversubscription degrades throughput rather than triggering the OOM kill that makes memory unforgiving. Dissolve-on is recorded. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Parse repair, a typed refusal for the saturating width search, and the roster edit handed off Three things, in the order they were found. THE PARSE ERROR IS MINE AND IT IS THE PLAINEST FORM OF THE FAILURE. The four per-host DIMM expectations were written as `data X: HostDimmExpectation =` with the initializer on the NEXT line, which the grammar does not take. CI refused the whole module index. I pushed .dag I had never compiled -- typecheck-by-eye is not a consumer, and DESIGN says so in as many words. Initializers are now on one line and this branch is verified locally before pushing rather than after. THE SATURATING SEARCH BOUND IS AN ABSORBING FALLBACK, AND RAISING 8 TO 40 WOULD HAVE LEFT IT. admitted_width_charging folded a bounded range and returned the last admissible element, so a host admitting MORE than the bound got the bound back as a number indistinguishable from a real measurement. That is not hypothetical: it fired. From the 2026-08-22 upgrade until now, srv3 and srv4 admitted 29 against a bound of 8 and reported exactly 8, so two of tonight's six failures were rows comparing the bound to itself. The deficit never surfaced as itself -- it arrived as an unrelated inequality, which is exactly the frequency-zeroing DESIGN 5 describes. The fold now answers a typed verdict: WidthSearchFound when the largest admissible width is strictly inside the range, WidthSearchSaturated naming the host and the bound when the top is still admissible -- at which point the search has not measured a width, it has run out of room to look. The Int projection converts saturation to -1 rather than to the bound, so an assertion fails loudly instead of passing at the ceiling. THE RANGE IS A PARAMETER SO THE REFUSAL HAS AN AUTHORABLE RED. No real host admits 40, so a saturation arm written only against the standard range could never be driven red by any input -- permanently green by construction, and worse than absent because it would be cited as coverage. DESIGN 4b says to ask whether the RED is authorable BEFORE writing the check, and to judge that against what a FIXTURE may author rather than what the corpus contains. admitted_width_search_within takes the range and its top, so saturation_refuses_rather_than_reporting_the_ceiling hands srv3 a range of 1..3 and gets the refusal, with a positive control on srv2 that stops the arm being satisfied by refusing always. no_enrolled_host_saturates_the_standard_search_bound is the quiet guard beside it: mechanism exists, reachable from this operation's own denominator, currently unoccupied, and red the day a host outgrows 40. THE SIX-ROW EXPECTED-RED UN-ENROLMENT IS DROPPED AND HANDED TO #8959, which needs the same nine-element list edited to present anything but a red and needs none of this lane's memory knowledge. Two lanes editing one shared row is a conflict neither wanted; the witnesses stay put in both diffs and only the enrolment moves. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Four consequences of the width change, found by running the floor instead of reasoning about it A local floor run on this branch found five failures. Four are consequences of this lane's own change and are repaired here. The fifth is #8947's and is diagnosed below rather than guessed at. THE RETIRED-SLOT FIXTURE WAS PINNED TO AN INDEX THE FLEET GREW PAST. build_cache_endpoint_observe's witness_retired_runner_slot_owner_refuses fed the decoder a cgroup path naming srv1-10 and asserted the lifecycle came back Retired. That held while srv1 committed five slots. It commits twenty-one now, so slot ten is DESIRED and the fixture silently stopped being a specimen of the thing it is named for. Bumping it to a larger literal would have the identical defect on the next width change -- the same trap this branch already hit in a different costume, where a search bound's comment called 8 "wider than any host can reach". The index is now computed as one past what the host actually commits, and the assertion checks the PROPERTY the decoder decides -- slot_index > committed width, which is what retired MEANS -- rather than an equality that has to be retyped whenever the fleet moves. TWO BOUND-ARM CONTROLS LOST THEIR SUBJECT WHEN srv2 WAS PROMOTED. Both reached HostUsableRamConservativeLowerBound through srv2, and every enrolled host now carries its own measured MemTotal, so nothing in the fleet sits on that arm. They are re-pointed at a constructed fixture, NOT deleted. Three questions decide whether a guard should exist and only the first two matter: the mechanism exists, and it is reachable from what a fixture may author. Only current occupancy is zero, which is a quiet guard rather than a dead one -- a fifth host enrolled tomorrow with no read of its own lands on exactly this arm. A new row asserts the complementary fact the fixtures can no longer carry: every enrolled host is on the measured arm, which reds if one is ever demoted back to a borrowed figure. ONE ROW MIXED A FIXTURE HOST WITH A LIVE POOL. allocation_conserves_when_pools_fit passed a 125 GiB literal as the host while drawing runner_pool from srv1's live budget. Those agreed only while srv1 happened to be a 125 GiB machine; after the upgrade the literal described a different computer than the pool did. It reds for the mismatch, not for anything about conservation. The host figure now comes from the host the row names. AND ONE FORK THAT WOULD HAVE SILENTLY EATEN THIS WHOLE CHANGE, found while reading the provisioning path rather than by any test. RunnerHostDeploy.runner_count was a hand-authored 6 on srv3 and srv4, answering the same question as gunbc_runner_slots_per_host. With the literal in place, allocation would say 21 and PROVISIONING WOULD STILL HAVE STOOD UP SIX -- the model and the materialization path disagreeing about the fleet with no diagnostic anywhere, which is precisely the roster-versus-prose failure width_is_a_minimum_over_axes_note records for srv4. It now derives from the width authority. Width is decided by the admission axes and materialization CONSUMES that decision; a deploy row is not a place to re-decide it. Recorded in the same note, because a reader seeing two derived rows will assume the fleet is covered: srv1 and srv2 have NO RunnerHostDeploy row at all. srv1's move from five slots to twenty-one still has no provisioning path. Pre-existing, not closed here, and not silent any more. THE FIFTH FAILURE IS NOT REPAIRED AND NOT GUESSED AT. fleet_intent_memory.srv2_population_matches_bmc_memory_summary is #8947's, and it has a measured diagnosis rather than a theory: run directly against its own entry it returns TRUE, and it fails only under the whole-corpus floor. Both sides compute exactly 137438953472 in isolation. That localizes it to cross-module name resolution under the full module population -- the class this very test file's ambiguous_type_name_import_note already documents, where a targeted compile resolves a closure that never loads the homonym and reports clean while the floor loads both and refuses. My earlier hypothesis -- that extdeps.memory.sk_hynix and extdeps.memory.samsung both defining stick_capacity_bytes was the mechanism -- is REFUTED as stated: a probe importing both still reads the Hynix capacity as 16 GiB. Right class, wrong reproduction; two modules is too small a population to trigger it. Left for its own change rather than repaired blind, and it is not a regression of this branch. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Aug 23, 2026
Merged
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 24, 2026
…fication The dispatching session supplied the true cause and it is better than the one this probe reconstructed: the brief was differenced against gunbc#9020's BRANCH HEAD, which carries the resolution repair. Verified here rather than taken on report -- run 32680784546 (c767f4c) reads passed=10619 known_red_runtime_errored=43 against the base's 10520 / 142, exactly -99/+99, with `planned` identical at 10791 on both. That last equality is what let the mistake survive a sanity check: an equal planned population reads as an equal baseline and is not one. Section 2 previously attributed the 99 to the HELD -> RUNTIME-ERRORED reclassification in ec2f3c3 (#8959). That reclassification is real and is why this population is visible at all, but it is not where the brief's figure came from, and asserting a wrong cause in the document that exists to correct a wrong cause is the same defect one layer in. The old attribution is kept as a marked correction rather than deleted, because a reader who saw the first version needs to find out it moved. Section 1 is unchanged and was correct: there is still no regression in the named range. The carrier is deliberately NOT pre-adjusted to 43. Writing a branch's number into a row measured on main would commit the fix-carrying-baseline error a second time, inside the artifact documenting it. The PopulationBasis arm names the run and commit, so the row is re-measured when #9020 lands. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 25, 2026
… and confined at identity grain (#9095) * The floor's non-verdict expected-red population, sized and given a next-rung trigger The brief this lands under reported 99 witnesses going PASSED to RUNTIME-ERRORED across 330f63c..5482863 with the floor still green. Measured against the runs those two commits produced, nothing changed in that range: both are green, both report known_red_runtime_errored=142 over the SAME 142 identities (extracted and diffed), both roster joins read roster=177 still_red=177, and the range's diff does not touch floor_expected_red.dag. The described transition could not have occurred either -- an unenrolled runtime error is already a gating conjunct via outcome.failures, and an enrolled identity that passes reports known_red_now_passing, also gating. The real event is a HELD to RUNTIME-ERRORED reclassification, on 2026-08-23 in ec2f3c3 (#8959): known_red_held fell 208 to 36 while runtime_errored appeared at 164. That commit revealed rot rather than causing it. What survives from the brief is its second clause, and it is real: 142 enrolled identities produce no verdict on every run and the floor reports failed=0. required_floor_outcome_is_clean deliberately omits known_red_runtime_errored and known_red_observation_unreadable, and that call is not disputed here -- the arm's own comment reserves the change for an approved design. What was missing beside it is the DESIGN 4b(2) obligation: a class parked below its ceiling must name its next-rung trigger and size its population, and neither existed. gunbc.floor_non_verdict_enrollment carries both. The population is measured (119 name not in the loaded index, 13 type error, 9 undefined variable, 1 call contract mismatch) and declared through a PopulationBasis arm as a one-run snapshot rather than a bound, because nothing counts a witness that starts throwing tomorrow. The dominant cause was checked by hand rather than assumed: four unresolved names all ARE declared in the corpus, and the witnesses referencing them declare no import -- the refusal is correct and the witness is unimportable, which is why the trigger makes population repayment a precondition of the gating conjunct rather than a follow-up. The witness asserts the census sums to the measured total, that no declared cause sits at zero, and that the basis is still the snapshot arm -- so the next-rung transition cannot be asserted by editing one row. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The carrier's declaration RHS lives on the declaration's own line `data <name>: <Type> =` followed by a newline before the expression is a parse error in .dag -- "expected expression, found Newline" -- and three rows in the new carrier were wrapped that way. Measured, not guessed: the module index refused the file with that diagnostic on a remote dispatch, and with the rows unwrapped all three witness functions evaluate and return true. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The 99 came from a fix-carrying baseline, not from the #8959 reclassification The dispatching session supplied the true cause and it is better than the one this probe reconstructed: the brief was differenced against gunbc#9020's BRANCH HEAD, which carries the resolution repair. Verified here rather than taken on report -- run 32680784546 (c767f4c) reads passed=10619 known_red_runtime_errored=43 against the base's 10520 / 142, exactly -99/+99, with `planned` identical at 10791 on both. That last equality is what let the mistake survive a sanity check: an equal planned population reads as an equal baseline and is not one. Section 2 previously attributed the 99 to the HELD -> RUNTIME-ERRORED reclassification in ec2f3c3 (#8959). That reclassification is real and is why this population is visible at all, but it is not where the brief's figure came from, and asserting a wrong cause in the document that exists to correct a wrong cause is the same defect one layer in. The old attribution is kept as a marked correction rather than deleted, because a reader who saw the first version needs to find out it moved. Section 1 is unchanged and was correct: there is still no regression in the named range. The carrier is deliberately NOT pre-adjusted to 43. Writing a branch's number into a row measured on main would commit the fix-carrying-baseline error a second time, inside the artifact documenting it. The PopulationBasis arm names the run and commit, so the row is re-measured when #9020 lands. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Freeze the non-verdict population's growth at identity grain: the composition was below floor RULING (operator, relayed via the dispatching session): the observation arm is not the defect. known_red_runtime_errored and known_red_observation_unreadable say something TRUE -- this enrolled claim produced no Boolean verdict. What was wrong is the COMPOSITION: required_floor_outcome_is_clean consulted neither, so the floor returned CLEAN while an enrolled expected-red assertion had ceased to assert anything. A diagnostic can describe the evidence truthfully while the gate draws a false conclusion from it. Per seam: routing is mitigatable, printing the count is mitigatable, printing failed=0 without distinguishing verdict incompleteness is a misleading projection, and returning clean over an enrolled claim that produced no verdict is BELOW FLOOR. Below floor is not a rung, so this could not wait on the population being repaid, and the previous revision's 4b(2) row understated it. WHAT ENROLMENT ADMITS: a known SEMANTIC VERDICT, not permission for the subject to stop evaluating. Without a wall the expected-red arm absorbs an arbitrary regression strictly INSIDE the enrolled population -- yesterday the witness answered false, today it throws before reaching its assertion, no verdict exists, floor stays clean. An UNENROLLED witness that throws already gates through the ordinary failure path, so the absorption was never repo-wide and this commit does not claim it was. THE WALL IS A GROWTH FREEZE, NOT A GATE ON THE POPULATION. v2.workflow.floor_non_verdict carries the 142 identities; admission is that ADDED is empty. 142 -> 43 -> 0 is admitted in any order; 142 -> 143 refuses; and a swap that repairs one identity while a different one begins throwing refuses even though the count never moves. That last case is why both sides are compared as IDENTITY SETS -- a count cannot see a swap, and a repaired witness must not buy permission for an unrelated witness to lose its verdict. It has its own witness, asserting the length equality beside the refusal so the discrimination cannot be read as an artifact of differing sizes. TWO DESIGN DECISIONS THAT ARE NOT ARBITRARY. The polarity is unenrolled-blocks, so an EMPTY roster is the strictest state and a roster read failure cannot flatter a run -- the opposite polarity rebuilds the absorbing-fallback shape inside the mechanism written to close one. And repaid does NOT gate, deliberately breaking symmetry with floor_route_gap's stale-row refusal: copying it would red the floor on the merge that repairs 99 of these (gunbc#9020), which is how a repository teaches people not to repair debt. Added is walled; repaid is announced per identity with its remedy. A non-verdict row not also in floor_expected_red is REFUSED, not warned. Only enrolled identities reach these arms, so such a row can never fire -- unreachable, not empty -- and DESIGN is explicit that a check whose red cannot be authored is a decoration, worse than absent because it is cited as coverage. FloorAdmittedWithNonVerdictDebt separates unexpected_failures from verdict_incomplete on the top line. `failed=0` is a sentence a reader can finish alone and finishes wrongly; that misreading is what dispatched this whole lane against a regression that did not exist. Evidence: cargo check clean; four admission witnesses return true by execution (unchanged admitted, repayment admitted with repaid=2/added=0, growth refused with added=1, and the equal-count swap refused with added=1 and repaid=1); the roster evaluates. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The admission is one pure function of two identity sets, with its red on the seed path The decision was taken INLINE IN TWO ARMS, which is two places one rule could drift from the modeled admission it mirrors. It is now taken once, after the fold, over two identity sets: the arms only RECORD what they observed. That was prompted as a way to make the seed testable and turned out to remove a real second-representation seam. THE SEED PATH NOW HAS A DISCRIMINATING RED, which the previous commit did not have -- its four witnesses exercised the MODELED admission, and a mirror can be wrong in ways its carrier cannot see. Five unit tests drive growth, repayment, the equal-count swap, and the empty roster through the Rust that actually gates. MUTATION-CONTROLLED, because five green tests establish nothing on their own: stuck-admit (always true) -> 3 of 5 FAIL count-based (added.len() <= repaid.len()) -> 4 PASS, 1 FAILS restored -> 5 pass The second mutant is the load-bearing measurement. A count-based admission passes every test except the swap, which is exactly the claim the design rests on: a count cannot see one identity repaired while a different one begins producing no verdict, and only the identity-grain comparison refuses that trade. Without that single case the mutant ships green. THE MIRROR'S RUNG IS NAMED rather than left implicit. There are now two implementations of one rule -- v2.workflow.floor_non_verdict_admission and v1_compiler.cli_run non_verdict_admission -- so the carrier records the seed half as MITIGATABLE with its next-rung trigger being derivation from the carrier, the same framing v1_compiler.required_regen_host already carries for its hand-mirrored ordering. The class rung is the minimum across paths, so it is mitigatable. RESIDUAL GAP, NAMED: none of this reaches the wiring from a real thrown witness into the observed set. That path is still unexercised. It is narrower than "the seed wall is untested" and it is not zero. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Repayment and roster deletion are one act; and the hand-Rust growth gets its receipt Both findings in review 55361 are correct. Neither is argued with. FINDING 1 -- THE STALE ROW WAS A LIVE EXEMPTION. stale_non_verdict shipped report-only under my argument that refusing it "punishes the fix", and the reviewer found the hole: the identity is repaired, the row stays, and if that witness later stops producing a verdict again it is ALREADY ROSTERED, so the exact regression this wall exists to refuse is admitted in silence. Repayment without deletion turns a bounded debt row into a permanent licence -- the absorbing fallback wearing the word "diagnostic". Refusing does not punish a repair; it requires the repair to be COMPLETE, the run names every row to delete, and this is the discipline stale_route_gap and the expected-red staleness join already enforce. The asymmetry was the error and consistency with them is the repair. Worth recording that the asymmetry had an argument behind it and was endorsed before a reviewer found the hole -- an endorsement is not a proof. FINDING 2 -- THE FORWARD-FREEZE ROW WAS MISSING. Verified against the tree rather than taken on report: gunbc.seed_growth_admission seed_growth_forward_freeze_policy_note requires every PR adding hand-written src/v1 Rust to enumerate exact item identity, .dag authority, why Rust is still needed, owning lane, deletion trigger, current boundary, hand-item delta and hand-LOC delta, and rules unenumerated hand growth a stop-line with no netting of deletions against additions. This change added hand Rust and authored no row. floor_non_verdict_seed_growth_justification now carries it: +8 citable items (three production, five discriminating unit tests), measured deltas of +195 cli_run.rs, +65 claim_executor.rs, +85 in the new test file, lane v1-hand-queue-drain, trigger the self-emitted claim executor, boundary named end to end. The two new RequiredFloorOutcome fields, the added conjuncts, the roster read and the report lines are deliberately NOT listed: none adds a declaration, so their disposition is ExistingSeedItemModified and listing them would net modifications into an addition census. The row is registered in the closed roster in seed_growth_admission. Evidence: build clean; 5/5 seed admission tests; the seed-growth roster well-formedness gate returns true over the extended roster (closed, well-formed, no duplicate DeclarationRef keys); the carrier witness returns true. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The roster needs a reachability edge, and the note that should have prevented this did not CI refused during floor preparation: `floor_non_verdict_roster: no declaration named 'v2.workflow.floor_non_verdict.floor_non_verdict_roster' in this execution's loaded index`. The host evaluates roster functions in v2.workflow.required_floor's frame, so a roster module reaches the loaded index only via an import edge there. Mine had none. THE FIX IS ONE LINE. What is worth recording is that required_floor.dag ALREADY CARRIED TWO PARAGRAPHS documenting this exact failure happening twice before, saying precisely what would go wrong and why -- and I read that file, added a roster, and reproduced it a third time. A prose note that has now failed to prevent the thing it describes on three consecutive occasions is not a wall; it is a record of a mechanism defect. The list is a hand-maintained reachability closure that nothing derives and nothing checks, and its violation surfaces only from a full CI run. So the third paragraph says that, rather than adding a fourth warning: the structural repair is for the host's roster evaluations to derive reachability from the qualified names they call, at which point the import list and all three paragraphs delete together. THE POLARITY IS WHY THIS WAS LOUD. The roster read fails closed, so a missing edge stops the floor instead of yielding an empty roster. Under the opposite polarity this same omission would have produced a silently permissive wall -- the exact failure mode this PR exists to close, reintroduced by an oversight nobody would have seen. AND THE FAILURE IS THE DOCUMENTED CLASS, on its own author: "not in this execution's loaded index" is the same diagnostic behind 119 of the 142 identities this roster carries. The witnesses in that population reference declarations that exist while declaring no import; so did I. Evidence: required_floor's closure compiles with the edge -- exit 0, 0 blocking errors, 126 advisory. The host's own roster read is exercised by CI, which is the test that failed and is the test that has to pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Name the axis the wall does not confine: the roster itself is not compared against the base The dispatching session, relaying its second reader, asked whether R (subset of) B is enforced. Checked against the implementation rather than my description of it: it is not. non_verdict_admission takes observed and roster-at-head, and no base reference exists anywhere in that path. So a change that makes a NEW identity stop producing a verdict may add its row IN THE SAME CHANGE, satisfy both executing arms, and be admitted — the roster legalising the regression it exists to bound. That is review 55361's finding (the row becomes the permission) reached through authorship instead of through survival. NO MECHANISM CHANGES HERE. The wall does exactly what it did when CI went green. What was defective was the CLAIM: the module was named a growth freeze and the title said "frozen against growth at identity grain", from which a reader concludes growth is refused. That is rung inflation in DESIGN 4b(1)'s exact sense — worse than sitting low, because an inflated class never ranks for climbing — and it was false in the artifact independent of whether the conjunct ever lands. So the header now opens with what is confined and what is not, BEFORE it describes the admission, and the title says confines rather than freezes. TWO AXES, ONE EXECUTES. Observed-vs-roster is walled by execution every run: growth refuses, stale exemptions refuse, both at identity grain. Roster-vs-base-roster is not walled at all — mitigatable, confined by review diligence, which is strictly weaker. The class rung stays the minimum across axes and paths. NEXT-RUNG TRIGGER, and it is specified at identity grain for the same reason the executing arm is: the floor reads the roster at the merge base and refuses when the head roster is not a subset of it, established against a discriminating red. Not satisfied by counting rows — an addition and a deletion in one change leave every count unmoved. WHY THE CONJUNCT IS NOT IN THIS PR: reading the base roster means evaluating a .dag module out of a git blob in a separate resolve context. That is real machinery deserving its own discriminating red, not a paragraph bolted onto a change already at full approval with green CI. AND THE HONEST ACCOUNT OF WHY THE HOLE EXISTS, which is the reader's framing and better than mine: the admission was SPECIFIED against a base OBSERVATION, and substituting the roster for it is what makes the wall runnable in a single pass. The substitution is sound exactly to the degree the roster cannot be grown freely, so R (subset of) B is the condition that makes the cheap design safe rather than a nicety on top of it. Evidence: required_floor's closure compiles at 0 blocking errors (126 advisory); the carrier's closure at 0 blocking errors (276 advisory). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The growth trigger names the target-base tip, not the merge base A precisely-wrong trigger is worse than a vague one, because someone implements exactly what it says. The previous text named the MERGE BASE as the future authority for the roster-growth law. It is the wrong baseline, and the failure is an admission rather than a spelling. EXEMPTION RESURRECTION. M = {a} at the merge base. Main later repairs `a` and deletes its row, so the current base tip carries B = {}. A stale branch reintroduces `a` and it throws: H = {a}, O = {a}. Then O = H passes and H subset-of M PASSES — readmitting an exemption main has already paid off. H subset-of B fails, which is the law actually wanted. The mirror is a false red: a row main legitimately adds after the fork sits in B and in the composed result but not in M, so a subset-of-M rule refuses a branch that did nothing wrong. So the law is H subset-of B — the roster in the COMPOSED RESULT is a subset of the roster at that result's CURRENT TARGET-BASE PARENT — and the trigger now says so, in both the carrier and the roster header, with the counterexample beside it so the next author cannot re-derive the weaker rule from the stronger sentence. CONSEQUENCE FOR THE CUT'S SHAPE, recorded because it changes how the follow-up is scoped: a BRANCH-HEAD-ONLY RUN CANNOT ESTABLISH THIS LAW. It needs the composed result AND that result's base parent, which is strictly stronger than "read the roster at another commit". The trigger also pins the receipt the cut must carry — target_base_sha, composed_result_sha, base_roster_identity_set, result_roster_identity_set, added_exemptions = result - base — and requires the same read-failure polarity the executing arms already have. NO MECHANISM CHANGES. The two executing axes are untouched and the "confined at identity grain" claim is unaffected; only the future authority named in the trigger was wrong. Amended in this PR rather than deferred to the follow-up because the head had already moved for the main integration, so the approval cycle was already reset and the marginal cost was zero. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The no-import story does not cover the whole bucket: six of the eight are inside it An independent census (valiant-lynx-227, run 32743601436) partitions the erroring modules 53 declaring NO import against 8 that declare imports and error anyway. Cross-joining that against this carrier's own cause census — which neither lane had done — puts SIX of those eight inside the `no declaration named` bucket. The bucket is not homogeneous, and §5's four hand-checked names, all lacking imports, leave the impression that it is. ONE OF THE SIX READ IN FULL, so the second shape is evidence and not inference: v2.lens.vacuity_test fails on `nat_add_left_identity_input` while declaring ten imports, among them v2.test.nat_semiring.rung_5 — a module that REFERENCES that name but is not the module that DECLARES it (v2.std.algebra_laws.nat_semiring). Importing a module does not transitively supply the names its own declarations reach for. So the second shape is an INCOMPLETE import set, not an absent one. THE CONCLUSION IS UNCHANGED AND SLIGHTLY STRENGTHENED: both shapes are authored defects, both repaired by adding the import that declares the referenced name, neither is a floor scope defect. "Widen the scope" is still the wrong trigger. What moves is the repairer's expectation, which matters to the lane inheriting the backlog. The remaining five are established only as "declares imports AND lands in this bucket"; their specific missing imports are unread, and the row says so. ALSO RECORDED: the census reached me first as "142 rows but 133 distinct, 9 appearing twice" — which would have meant this roster carried nine stale exemptions. False, and instructively so: the floor COLUMN-PADS the identity, so short names are followed by spaces before `ERROR in`, and an extraction using `[^ ]*` cannot cross that padding. The pattern silently selected for long identifiers and dropped exactly nine rows. The nine were MISSED, not duplicated — sign inverted, the same shape as the brief this document exists to correct. Two independent diagnoses converged on the padding cause. The durable rule: a distinct-vs-total discrepancy is a tell about the READER before it is a tell about the population, and the control is to count with a different pattern than the one that extracts. AND THE CAUSE CENSUS IS DECLARED A CLAIM, NOT A RECEIPT. The floor log carries no cause text beside the ERROR row, so the 119/13/9/1 partition cannot be checked by anyone unwilling to re-run a floor that OOMs in a session container — unverifiable by construction. Printing the cause beside the identity is a smaller change than this wall and would have made the false alarm impossible; it is a separate subject, and until it lands the partition is a claim. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The modeled authority still said repaid never gates: one rule, two answers Review 55515, correct. When stale_non_verdict was flipped to gating after review 55361, the reversal reached the roster header, the seed's field doc and the gate conjunct — and missed the docstring on v2.workflow.floor_non_verdict_admission non_verdict_repaid, which went on saying "Reported, never gating: a repaid row must not red the run that repaid it". That left two authorities stating OPPOSITE RULES about one admission, inside the module whose whole subject is single authority, in a PR whose body cites review 55361 for exactly this class. The mechanism was never wrong — the executing code has refused stale rows since that fix — which is precisely why the sentence survived: nothing that runs reads it. FIXED IN BOTH PLACES, because the reviewer found one instance and there were two. The docstring now states the rule and records that it was reversed and why. The PR body's "repaid does not gate" paragraph carried the same stale claim and is corrected as a struck-through amendment rather than a silent rewrite — a reader of the earlier revision saw the reversed claim, and quietly replacing it would hide the drift instead of recording it. SWEPT FOR OTHERS: grepped every carrier, the seed, the probe document and the PR body for surviving assertions that repaid or stale does not gate. The only remaining hit is the verbatim quote of the original brief in the probe document, which is a quotation and stays. WHAT THIS IS AN INSTANCE OF, recorded because it is the day's recurring shape: prose asserting more or other than the mechanism does. Every defect found in this PR has been that — the failed=0 line, the diagnostic stale row, the growth-freeze title, the merge-base trigger, and now a docstring left behind by its own reversal. None was a coding error. All were caught by someone checking a claim against the tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Drop the "65 distinct signatures" figure: it counted names, not causes valiant-lynx-227 found that the floor's [floor-known-red-causes] census keys on the FIRST TWELVE WORDS OF THE MESSAGE PROSE, and that prose embeds the missing NAME. So `no declaration named 'srv3_install_hang_no_router_lease_ms'` and `no declaration named 'extdeps_cargo_build_module'` are two distinct signatures. It reports ~65 for a population with roughly four actual causes — an artifact of the key, reading as "many roots" when the truth is "one root, many names". A plan sized off it is sized wrong, toward heterogeneity, when this population is mostly one repair. The same line is SILENTLY TRUNCATED AT 20: the printed rows sum to 93 of 142 identities, with 49 identities and 45 signatures dropped and nothing saying so. WHAT THIS DOES AND DOES NOT REACH, and the boundary is the derivation rather than luck. The 119/13/9/1 partition was folded over the 142 PER-IDENTITY KNOWN-RED-RUNTIME-ERRORED lines and sums exactly to 142 — neither prose-keyed nor truncated — so it stands. The population count and the identity set stand too; the executed set match settles both. What does not survive is any DISTINCTNESS or HETEROGENEITY claim, which is precisely the one figure this document took from that line. It is deleted rather than annotated, because an artifact carried with a caveat is still cited as a count. ALSO CORRECTED, IN MY OWN FAVOUR, WHICH IS WHY IT IS WORTH WRITING DOWN: an earlier revision of this document called the partition "a claim, not a receipt" and "unverifiable by construction", on the assumption I had hand-derived it. That was too harsh and is now scoped to what is actually unverifiable — there is no per-identity cause field, so the partition cannot be JOINED BACK to identities by a reader, which is a narrower and truer statement than "unverifiable". The root — ClaimOutcome::RuntimeError carrying message: String built by format! over an already-closed 27-arm InterpError, so a typed cause is destroyed at the witness boundary and guessed back by word-slicing at the reporting site — is being repaired under its own item and is not held by this PR. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the probe board, keep the finding on the carrier: the measurement corpus was bankrupted under this PR Main landed #9132 (bankrupt the measurement corpus) while this branch was open, under an operator ruling this change is directly subject to: name the instrument, never transcribe its output. 164 files and 44,736 lines went out of docs/probes/, every .sh/.py instrument kept. docs/probes/expected_red_non_verdict_population_2026-08-24.md is a transcription board of exactly the class that ruling deletes. After merging main it was the ONLY file left in that directory -- one document re-establishing a corpus main had just emptied, on the same day, which is the attractor DESIGN section 3 names rather than a document that happened to survive. It is deleted here. WHAT IS NOT LOST, and why the deletion is not a coverage cut. The measurement never depended on the board: floor_non_verdict_cause_census and floor_non_verdict_measured_total are typed rows, and floor_non_verdict_population_basis carries MeasuredOnOneRun { run, head_commit }, so every figure names the run and head it was taken on. That is the receipt-vs- figure distinction a markdown board structurally cannot carry, which is the ruling's own argument for the cut. WHAT MOVED. One irreducible fact in the board was rationale rather than measurement and had no other home: the dispatched brief -- 99 witnesses PASSED -> RUNTIME-ERRORED across 330f63c..5482863 with the floor reporting failed=0 -- is false in its first half, shown by an identity-set diff, because the 99 were baselined against a branch head already carrying the fix and so were compared to a tree they never ran in. The carrier's existing prose REFERRED to that false regression without ever stating it; it now states it once, as a section 4c annotation on the declaration it explains. A first draft of that annotation also restated the fix-carrying baseline the preceding block already covers, and was trimmed to the half that was actually missing. RESIDUE, checked against the three classes #9132 declared for its own cut and found empty here: no .gitignore un-ignore row, no prose note in any module, and no witness asserting the filename. Nothing in the tree references the deleted path, so this leaves none of the debt that commit declared for itself. Verified: the module parses and evaluates after the annotation -- floor_non_verdict_measured_total returns 142, the host refusing only on its exit-code contract (an Int is not a ProcessExit), which it can raise only after computing the value. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Make the modeled admission say what its consumer does, and re-measure the hand-Rust receipt (review 55577) Two findings, both verified against the code before fixing. ONE: THE MODEL DISAGREED WITH ITS ONLY CONSUMER, AND I CAUSED IT. `non_verdict_admits` -- modeled in v2.workflow.floor_non_verdict_admission and mirrored in v1_compiler.cli_run -- answered `added.is_empty()`. The executing gate `required_floor_outcome_is_clean` has nine conjuncts, two of which are `non_verdict_unenrolled.is_empty()` (the added arm) AND `stale_non_verdict.is_empty()` (the repaid arm). So the canonical model said ADMIT exactly where its consumer said REFUSE. The provenance matters because it is not an oversight in the original design: it is the divergence review 55361 opened. That review correctly argued stale rows must gate, I made the GATE gate, and I did not carry the change into the model or its tests. DESIGN section 3 is the point -- a modeled authority whose consumer disagrees is worse than no model, because it is cited as the rule while something else enforces a different one. WHAT WAS RIGHT ABOUT THE OLD RULE AND WHAT WAS WRONG. The rationale for admitting repayment was that refusing it would red the merge that repairs the population (#9020 repays 99 in one landing). Right about the goal, wrong about the subject: what refuses is not the repayment, it is the roster row LEFT BEHIND asserting a debt that no longer exists. Repaying and deleting the row are one act, which is already how the #9020 merge-order deletion was planned. So both paths now admit iff added and repaid are BOTH empty, and both suites gain a control -- repayment WITH the row deleted is admitted. Without that pair the tests cannot discriminate "stale rows refuse" from "repayment refuses", which are opposite rules; the pair fails in opposite directions if either is wrong. TWO: THE HAND-RUST RECEIPT WAS STALE. It read +195 in cli_run.rs and +65 in claim_executor.rs and omitted claim_executor's deletions entirely. Measured by git diff --numstat against origin/main at this head: +203/-0 cli_run.rs, +60/-5 claim_executor.rs, +102/-0 the test file. The forward-freeze policy exists to make hand growth checkable, and a receipt measured once and not re-measured as the change grew is a figure rather than a receipt -- the row now says so and says it must be re-measured on every push touching those files. Also removed a blank line between one annotation block and the declaration it attaches to, matching the convention every other annotation in that file follows (DESIGN section 4c attaches annotations to a declaration). This is NOT claimed as a fix for anything: a discriminating control through the actual parse sweep, with and without the blank line, produced identical output, so the form was not what any gate was refusing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Retire the prose that still states the rule the reversal replaced, and the citation naming a test that no longer exists (review 55591) The reported finding, plus two of the same class the sweep for it found. REPORTED: the `observed_repaid` fixture comment still read "Must be admitted -- refusing it would red the merge that repairs the population", directly above the test that now asserts the opposite. Fixed, and it now says WHY the refusal is not a penalty on repayment: what refuses is the roster row left standing, not the repayment, and the deleted-row form is admitted by the fixture below it. FOUND BY SWEEPING FOR THE CLASS RATHER THAN THE INSTANCE: (1) The same defect in the Rust mirror. `non_verdict_admits`'s docstring still described the retired asymmetry -- "so a caller cannot accidentally admit on `repaid` -- the asymmetry between the two is the content of this wall" -- sitting directly above a body that now refuses on both arms. Rewritten to state both refusal reasons, with the correction dated. (2) A STALE CITATION, and this one would have shipped silently. `floor_non_verdict_seed_growth_justification` cited `repayment_is_admitted_and_reported_per_identity`, which the previous commit RENAMED. That is a DESIGN section 3 fabricated symbol -- and the mechanism that used to catch it, the cited-symbol census, was removed from CI on 2026-08-23, so nothing in the repository would have refused it. Verified the whole file by hand instead: all 12 DeclarationRefs resolve to a definition in the tree. The new control test is added as a cited row, since a hand-authored seed item that is not enumerated is exactly what the forward-freeze policy refuses. Receipt re-measured, as the row itself now requires on every push touching these files: +210/-1 cli_run.rs, +60/-5 claim_executor.rs, +102/-0 the test file. THE PATTERN, recorded because it is now four for four in this PR: every defect found here has been PROSE CLAIMING SOMETHING OTHER THAN WHAT THE MECHANISM DOES -- the failed=0 headline, the "diagnostic" stale row, the growth-freeze title, the merge-base trigger, this docstring, this fixture comment, this citation. Not one was a coding error. That is the cost DESIGN section 4c prices when it calls prose commentary modeling debt: it cannot be mechanically joined to the code it describes, so a reversal updates the assertion and leaves every sentence about it standing. Verified by execution: both witnesses return true. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- 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>
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
1 participant
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.
What
An expected-red witness that threw, or that answered with something that is not a
Bool, was counted asknown-red held.Heldasserts the claim ran and failed as predicted; neither of those produced a verdict for the enrollment to agree with.The harm is concrete: a known-red witness that rots — errors on every run instead of executing — is indistinguishable from one still doing its job, forever, and its enrollment never comes up for review.
This file already settled the principle
A previous repair split budget interruption and unresolved host tools out of
Heldand wrote the rule down:A runtime error is not a semantic verdict either, and the principle does not distinguish being cut off at a budget from throwing. That repair covered two of the four non-verdict outcomes and left two folded — and then described itself as having covered all of them:
while
expected_red_armstill readFail | NotBool | RuntimeError => Held. That sentence is corrected here rather than quietly widened: an unexecuted claim standing where an executed one appeared to be is why nobody looked again.Two sites, not one
claim_disposition(outcome → disposition) andexpected_red_arm(console/counting) are two derivations over one row. Fixing only the first would have made the ledger and the console disagree — a new cross-derivation disagreement created by the fix for a cross-derivation disagreement.The correct dispositions were not missing vocabulary:
ObservationUnreadableBeforeVerdictandRuntimeErroredBeforeVerdictalready existed and were already used, one line away in the samematch, for the unenrolled case. Expectation is simply no longer consulted for outcomes that produced no verdict.Wired to block — which was nearly the defect in the fix
The two new collections are read by
required_floor_outcome_is_clean. Without that they would have been populated, printed, and never consulted — counted coverage that gates nothing. TheSEVEN CAUSEScount in that predicate's doc comment is nowNINE; that sentence warns it went stale once before, and it had.How it was found
Not by review. The terminal-ledger cross-check on #8909 refused a real floor run, naming one identity whose seed disposition disagreed with the grammar's derivation:
That identity is enrolled as expected-red in
floor_expected_red_chunk_00as a bare roster row with no recorded reason. Run locally it returnstrue.Blast radius is NOT yet measured, and this PR is the instrument
The count of enrolled identities that reclassify out of
heldis exactly what the required run now reports, viaknown_red_runtime_errored=/known_red_observation_unreadable=and per-identityKNOWN-RED-RUNTIME-ERRORED/KNOWN-RED-OBSERVATION-UNREADABLElines. Read those before merging. I could not size it beforehand: the row-level evidence lives intarget/required_floor_terminal_ledger.partial.tsvand nothing uploads it — which is the sharpest argument #8877 has.v1 seed admission
Defect repair under the purpose test. The floor's known-red accounting decides whether required CI is green, so an enrollment that holds an undecided claim is a fail-open in the mechanism the v2 self-host program depends on for its own verification.
Expected CI state
This branches off main, which is currently red on the inherited
v1_compiler_emit_rust.rsregen drift (#8691's owed second fixed-point pass, repair owned by snappy-tern-856). A regen failure naming that file is not this diff. Judge this PR on its floor phase and its new counters.