Repository navigation
Conversation
…ve the operator both controls, and let the unwired one refuse by name The operator asked for a capacity visualization AND control in the daily workspace -- turn a machine down, cut off a provider. This is the authority both halves read. WHERE A CONTROL HAS TO BIND TO BE REAL. Both axes meet at dispatch_selection provider_inventory_for_instance, which returns the ProviderInventory that selection resolves against. So cutting a runtime REMOVES ITS OFFER: the resolved selection has no constructor for a provider that made no offer, which is structural impossibility rather than a gate. A check placed after selection would concede that the selected-then-rejected state is writable. TWO AXES, NOT ONE ENABLED FLAG. Turning a machine down and cutting a runtime are different questions. Fusing them makes the smaller action unavailable -- an operator wanting Codex off everywhere would have to take hosts down to get it. They are two withdrawal rosters over two subject types. WITHDRAWAL, NOT ENABLEMENT. Rows name what is CUT OFF, so an unlisted subject is active. The inverse makes the roster load-bearing for ordinary operation: a host absent through an authoring slip goes dark. Withdrawal fails toward capacity remaining available, which is the recoverable direction -- too much capacity is a cost, too little is an outage. THE CONTROL NAMES ITS AXIS EXPLICITLY (operator ruling 2026-08-23). "Cut off a provider" could mean the runtime or one account binding, and the conflation is silent in the worst direction: an operator meaning "cut this Claude account" who gets Claude cut entirely discovers it as missing capacity, not as a refusal, because both readings are well-formed. So both controls exist from this first version and the unwired account axis REFUSES with a typed ControlUnbound carrying the axis and its trigger. An absent control would read as "not applicable here" -- the not-applicable-versus-malformed conflation. The axis is not hypothetical: a credentials update performing an active-slot swap restarted a live container on 2026-08-22, so it is already being operated by hand without a control. The decision takes its rosters as ARGUMENTS, with the global readers as thin wrappers, because the live rosters are empty and must stay empty -- a decision reading them directly would leave every refusal arm unreachable by any fixture, making the witnesses decoration that is cited as coverage. Green by execution, seven witnesses, plus the mutation proof: collapsing CapacityRefusedProviderWithdrawn into the host arm turns a_downed_host_and_a_cut_runtime_do_not_share_one_answer red while a_withdrawal_does_not_leak_to_its_siblings stays green. Corpus parse gate rc=0, 0 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
… plans, and the gate that makes a cut real lands at the offer (review 54905) Two changes: the review 54905 repair, and the consumer that makes this authority non-inert. THE REPAIR, AND IT WAS THE FAIL-CLOSED FAILURE IN MY OWN DIFF. apply_capacity_control returned ControlApplied for CutHost, CutProviderRuntime, RestoreHost and RestoreProviderRuntime while actuating nothing -- the rosters are module-scope data rows, so a caller that cut srv3 and then read host_is_withdrawn(srv3) saw false immediately after being told the cut succeeded. The sibling witness asserting the rosters stay empty made the two claims jointly inconsistent by construction. That is DESIGN section 5 fabricated plausible output, and the existing witnesses could not see it because they compared outcome strings to each other rather than joining the control to the roster reader. WHAT ACTUALLY HAPPENS IS PLANNING, SO THE VOCABULARY NOW SAYS SO. ControlApplied is deleted; ControlPlanned carries the roster edit that would effect the request. Withdrawing capacity means authoring a row and committing it -- deliberately, so a withdrawal faces review like any other change to what the fleet does -- which is the same plan/apply split the fleet converge path already uses. The reviewer's proposed witness is now in tree in both directions: plan a cut, then READ THE ROSTER. Mutation proof that it discriminates: relabelling the planned arm "applied:" turns planning_a_cut_does_not_withdraw_anything_by_itself red. On the second finding, the Bool predicates are KEPT and the reason is recorded on them. Present => true / Absent => false is predicate dissolution and would block in std, but both callers -- the counts and the dispatch gate -- want the boolean and not the row, so dissolving would push a match over an Option whose payload is discarded into every call site. The Option readers are exported beside them. THE GATE. provider_inventory_for_instance now filters offers through the capacity authority, so a withdrawn host or runtime MAKES NO OFFER and ResolvedProviderSelection has no constructor for it. The declared inventory keeps its own function so the gate has an unfiltered denominator, and the withdrawn offers are returned separately: an inventory emptied by withdrawal and one empty because nothing is installed are different facts with opposite remedies, and a bare filter renders both as the same empty list -- the empty-observation narrow. capacity_admission collided with std.materialization_ladder; renamed to fleet_capacity_admission rather than aliased, since two spellings in one namespace is the fork. Green by execution: 9 control witnesses, 4 gate witnesses proving the gate CUTS (fixture-authored withdrawal, since the live rosters are empty and a gate reading them directly could only ever be witnessed neutral), plus 4 pre-existing dispatch_selection witnesses still green. Corpus parse gate rc=0, 0 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
…he same roster the dispatch gate reads The operator asked for live fleet info on the daily workspace. This is the panel. IT READS gunbc.fleet_capacity_control DIRECTLY, not a display copy. That is the whole difference between a control and a cockpit: a panel with its own roster drifts from the thing it claims to steer, and the drift is invisible because both sides stay internally consistent. WHAT IT SHOWS: a summary line (active hosts, active runtimes, committed slots), a row per host carrying committed width and per-slot memory ceiling with its capacity standing, and a row per provider runtime. Live values today: 4 of 4 hosts, 3 of 3 runtimes, 22 slots committed at 16 GiB each. EVERY NUMBER IS LABELLED COMMITTED RATHER THAN OBSERVED, IN THE RENDERED OUTPUT AND NOT ONLY IN A COMMENT. runner_slot_allocation states that srv3/srv4's width of 6 is a provisioning target -- two slots that do not exist yet -- while srv1/srv2's 5 matches live. A reader summing an unqualified column gets 22 for a fleet running 20, and a capacity decision made on that number is wrong on the only axis the panel exists to inform. An annotation cannot carry the qualifier because no operator reads the source. The withdrawn-slots line is ABSENT when nothing is withdrawn rather than reading zero: a standing "0 withdrawn" row is noise on every ordinary day and trains the reader to skip the row where a non-zero number finally matters. A DEFECT THE WITNESSES CAUGHT, WORTH RECORDING BECAUSE OF WHAT IT WOULD HAVE DONE. fleet_capacity_withdrawn_line bound its subtraction across a line break, so the second operand parsed as a separate term and the count was 22 rather than 0 -- the panel would have announced "22 slots withdrawn by operator control" on every page load, a fabricated claim on the operator's main surface, while the fleet was fully active. Found by nothing_withdrawn_means_no_withdrawn_line, not by reading. Green by execution, five witnesses. The load-bearing one serializes the ACTUAL daily workspace document and finds the panel in the HTML -- a witness over the fragment alone would prove it builds and say nothing about whether it is composed into the page. The slot total is asserted as a relation against gunbc_runner_slots_per_host rather than against the literal 22, so it goes red on a panel that silently stopped reading the allocation authority. Corpus parse gate rc=0, 0 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
…is per host, and report the unmeasured one as unmeasured The panel showed four hosts and a total. A total is the one number that cannot answer the question an operator actually has -- what unblocks more capacity -- because a committed width is a MINIMUM OVER AXES and the surviving number discards which axis produced it. THE AXES ARE NOT INTERCHANGEABLE PURCHASES. Where memory binds the remedy is DIMMs; where cores bind it is a different machine. A reader given only a fleet total assumes one story across four hosts. THIS IS ABOUT TO MATTER MUCH MORE THAN IT DOES TODAY, which is why it is authored now rather than after someone reads a total wrong. Measured now, memory binds everywhere and the column looks redundant. Once the CPU axis lands (gunbc#8976, relayed by warm-tern-755) srv1/srv3/srv4 become core-bound at 21 while srv2 stays memory-bound at 5 -- its 64 GiB DIMM install failed training and was reverted, so it holds 8x16 GiB where the others hold 8x64 -- and the single total becomes two unrelated stories at 68 committed against 20 running. THE UNMEASURED AXIS IS REPORTED AS UNMEASURED, NOT AS ADMITTING EVERYTHING. Disk returns DiskWidthUnconstrained on every host, and runner_slot_allocation's own reason string is explicit that this is "an unmeasured axis, not a measured all-clear". Rendering it as admitting any width would turn an absence of observation into a positive clearance. It is excluded from the BINDING set by construction: an axis that states no width cannot be at the minimum. host_binding_width_axes returns a LIST rather than a winner, because a tie is real information -- two axes at the same number means relieving either alone buys nothing -- and picking one would have to break the tie arbitrarily. TWO RAW LENGTHS BECAME DERIVED RESERVATIONS. The first revision wrote min-width 5rem and 9rem, which would have been the only untokened lengths in the stylesheet and would need re-tuning by eye whenever a label grew. They now derive the longest string each column can wear plus a gutter, following roadmap_component dispatch_reserved_width exactly. The metric column resolves to 35ch from "bound by memory · disk unmeasured"; a new host or a longer phrase moves it by derivation. CSS digest re-pinned to b6df98adc93f7077, derived by execution on this tree per the convention in that file -- never chosen -- with a re-pin note naming the rule family and its behavioral receipts. Green by execution: an unmeasured axis is not reported as binding, the binding axis sits at the committed width (asserted as a relation against gunbc_runner_slots_per_host, so a label authored independently of the arithmetic would go red), the panel renders it for every host, and the digest pin holds. Corpus parse gate rc=0, 0 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
… declaration: srv2's nominal bytes were another vendor's
main's last failing witness is fleet_intent_memory.srv2_population_matches_bmc_memory_summary.
It passes under `gunbc run --entry` and fails under the required floor, with both
sides of its equality computing exactly 137438953472 in isolation -- so the
witness is arithmetically correct in both populations and only RESOLUTION differs.
THE SPECIMEN. `stick_capacity_bytes` was declared twice, and the two declarations
are two different facts:
extdeps.memory.sk_hynix 17179869184 (16 GiB, HMA82GR7AFR4N-VK and -R8N)
extdeps.memory.samsung 34359738368 (32 GiB, M386A4G40DM0-CPB)
Each was referenced BARE inside its own module. Whichever wins decides what
hma82gr7afr4n_vk_catalog.capacity_bytes is, and srv2's nominal total multiplies
it by eight. Under the floor Samsung wins, Hynix rows read 32 GiB, srv2 nominal
becomes 8x32 rather than 137438953472, and srv3 stays correct because Samsung's
value was right for Samsung's part. Every observed fact fits.
THE MECHANISM, PROVEN BY DISCRIMINATING PAIR RATHER THAN INFERRED. A four-module
fixture under the ENTRY-major resolver, both runs identical but for closure
membership:
fx.owner data shared_value = 111
fn owner_reads_its_own() { shared_value } <- bare ref, OWN local decl
fx.stranger data shared_value = 222
fx.puller imports fx.stranger <- drags it into the closure
stranger in closure -> owner_reads_its_own() = 222 WRONG, silent, no diagnostic
stranger absent -> owner_reads_its_own() = 111 correct
A MODULE CANNOT RELIABLY READ ITS OWN LOCAL DECLARATION. It is silent, it yields
a wrong NUMBER rather than a refusal (DESIGN 5's fabricated plausible output), and
it reproduces in the NARROW four-module pool -- not only under the floor's wide one.
WHAT THIS CHANGE DOES, AND WHAT IT DOES NOT. It removes the SPECIMEN: two facts
sharing one spelling is a DESIGN 3 violation on its own terms, resolver defect or
not. Both files already carried a capacity suffix (`stick_capacity_bytes_64g`), so
the repair follows local convention rather than inventing one -- `_16g` and `_32g`,
both verified unused corpus-wide first.
It does NOT fix the mechanism. The next colliding pair reproduces it silently, and
the census says the exposure is 643 duplicated fn/data names and 84 duplicated type
names. That wall is separate work; the fixture above is its RED and already executes.
A wall scoped to bare CROSS-MODULE references would NOT catch these sites -- they are
local references -- so the candidate set has to include local declarations.
EVIDENCE, AND ITS LIMIT STATED. The witness returns `true` under `--entry` after this
change -- but it did BEFORE it too, so that is a REGRESSION CONTROL, not proof. The
floor is the only consumer that reproduces the failure, so CI is the evidence and this
commit does not claim the close ahead of it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017HBx8dnz3oCiiHXoSBdtH2
…ome, no consumer, and no declaration `git add -A` swept `.fx/fx/*.dag` into the previous commit. Six files I authored as a throwaway probe and never intended to land. Removing them rather than keeping them, and the reasoning matters more than the six files: REVIEW READ THEM CHARITABLY AND THAT READING WAS TOO KIND. Review 54981 described them as "the discriminating probe fixtures for that same ambiguity class... matching DESIGN's authorable RED at the fixture boundary discipline". They are the right SHAPE for that, and the pair genuinely executes -- but nothing in the repository runs them. `.fx/` sits outside both floor source roots (`dag`, `src/v2`), so the required floor never discovers them. An artifact whose only property is that it LOOKS like a fixture is the inert-lens tier DESIGN 6 names: coverage by illusion. WHAT THEY WOULD HAVE ADDED IF THEY HAD BEEN IN SCOPE, which is the sharper reason: `fx.owner` and `fx.stranger` each declare `shared_value`, so the fixture introduces A NEW DUPLICATED NAME to the corpus -- one more instance of the exact defect this PR removes. And `fx.root` declares `owner_binds_its_own_local_declaration`, which returns FALSE by construction because that is the bug it demonstrates. A witness that must stay red is not a thing to leave lying in an undeclared directory where a later change to the floor's roots would enroll it. NEITHER RISK IS LIVE TODAY -- `.fx/` is out of scope, verified -- but "out of scope by accident" is not a home. Undeclared, unrun, and unowned is the experimental residue DESIGN 6 tells reviewers to presume against, and the author's own charitable label is not the denominator. The fixture is preserved outside the tree and lands WITH the wall it is the RED for, in a real home with an executing consumer, or not at all. This PR is the specimen repair -- two renames -- and its diff now says exactly that. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017HBx8dnz3oCiiHXoSBdtH2
…olumn it was authored for is now live Resolved the one conflict in runner_slot_allocation as a UNION rather than a choice. Both sides added functions at the same point and neither supersedes the other: main (#8976) added host_cpu_admitted_width and made the width a minimum over three axes; this branch added the model that says WHICH axis bound it. The union is not merely both texts. host_width_axes had to gain the CPU axis, because a binding-axis fold that enumerated only memory and disk would report "bound by memory" for a host whose width came from cores -- naming a cause that did not produce the number, which is worse than reporting no cause at all. THE COLUMN WAS AUTHORED FOR A FUTURE THAT ARRIVED DURING THE MERGE. Its own annotation said the axes would diverge once the CPU ruling landed; it landed. Measured on the merged tree: srv1/srv3/srv4 are core-bound at 21, srv2 is memory-bound at 5 on its reverted DIMMs, and the panel now reads 68 slots committed against 20 running. That is two unrelated stories behind one total, which is exactly what the column exists to keep an operator from misreading. One witness was FALSIFIED by the merge and was fixed rather than relaxed: an_unmeasured_axis_is_not_reported_as_binding asserted srv1 was memory-bound, which stopped being true. Its axis-naming half moved into a new, stronger witness -- srv1_and_srv2_are_bound_by_different_axes -- which is the discriminating one: a label function naming a single axis for the whole fleet passes every other assertion in the file and fails this one. CSS digest re-derived on the MERGED tree per that file's own resolution note (a digest pins emitted bytes, and a merge is the one moment when the bytes belong to a tree neither side built). It holds at b6df98adc93f7077 -- the longest metric label is still "bound by memory · disk unmeasured" at 35ch, so the derived column reservation did not move. NOTE, NOT MINE: the corpus-wide parse gate now refuses on dag/test/claim/build_cache_endpoint_observe_test.dag -- a section 4c annotation inside a declaration body, last touched by #8976, which this branch does not modify. Reported to that lane; recorded here so a reader does not attribute it to this merge. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
…ole floor at preparation Main is parse-broken and it is mine. #8976 landed a four-line // block INSIDE the match body of witness_retired_runner_slot_owner_refuses. DESIGN §4c admits standalone leading blocks attached to MODULE-SCOPE declarations and nothing else, so an annotation indented into a declaration body is a located parse refusal. WHAT IT COSTS IS OUT OF ALL PROPORTION TO WHAT IT IS. It refuses at PREPARATION, before any witness runs, so the floor reports: required-ci: floor refused: subject=949e339137b087a8 modules_resolved=3827 modules_excluded=4 required-ci: FAILED PHASE floor Not one failing row -- every witness in the corpus taken down by a comment's indentation. It also breaks the local corpus-wide parse gate several lanes use before pushing, which is how silent-bear-842 found it: their branch went rc=0 to rc=1 across a merge in which they changed nothing near it. The annotation is hoisted above the declaration unchanged in substance, and extended to record where the check does and does not live -- because that is the part worth keeping. --required-cited-symbol parses the whole corpus and passed this file CLEAN, twice, before I pushed #8976. Annotation grain is enforced in the floor's preparation, not in that census, so a green parse is not evidence that an annotation is placed legally. That is the second time in one night this lane shipped on a local check that could not see the defect class it was being trusted for; the first was a line break after `data X: Type =`, which cited-symbol DID catch. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…plan and apply Slot standup had its own path: a provisioning plan nobody reviewed, no lease, no member-set fingerprint, no CAS against an observed baseline. Timers and caps already flowed through membership_reconcile and slots did not, so the fleet had two ways to change a host and only one of them was gated. A width change landing through the ungated one is unreviewed by construction. This routes slots through the same spine: - observed_slots joins host, timers, caps and spark in observed_baseline_text, the member-set fingerprint and the plan subject, so a slot roster that drifts between plan and apply now fails the CAS instead of applying a stale plan. - fleet_converge_slot_family resolves the deploy row ONCE and both the review lines and the apply script derive from it. Resolving twice would let a reviewer approve one membership while apply executed another, with both halves internally consistent and the bundle hash unable to see the difference. - slot ADD is emitted into apply.sh. Slot directories live under the runner user's own /opt/actions-runner, which is the principal converge already runs as -- unlike cap drop-ins under /etc/systemd, which stay plan-output-only because they belong to the deploy principal. - REMOVE and CHANGE emit nothing, because runner_slot_member_ownership returns Absent for every observed slot: no provenance signal yet distinguishes a gunbc-placed directory from a stranger's. Reconcile yields MemberRemovalRefused, the refusals are rendered for the reviewer, and nothing deletes a directory whose ownership was never established. - An unmodeled host refuses in both projections: a REFUSED line in plan.txt, and an exit 1 in apply.sh. Silence would be indistinguishable from "this host had nothing to do", which is the fabricated plausible output at the actuation seam. - It counts as one refusal, not zero. Zero reads as "nothing was refused on this axis", so the most severe state would have looked like the cleanest one. The CLI observes slots for real. RunnerSlotsUnobserved refuses the plan and the apply rather than being rendered as an empty roster -- an empty roster reconciles to ADD EVERY SLOT against a machine whose population nobody read. srv1 and srv2 gain deploy rows, which is what made the width authority actionable on half the fleet: gunbc_runner_slots_per_host could say srv1 carries twenty-one and there was no provisioning target to hand it to. Addresses were read over SSH, not assumed -- the lane started with .183/.184, which are the BMC addresses, and an ssh_target pointing at a management controller fails looking like an unreachable host rather than a wrong row. Two witnesses stop pinning six. They asserted a literal copied from the tree the day they were written, so the CPU-axis change turned them red without anything about the property they name having changed -- a change detector, not a check (DESIGN 5). What survives is the relation: the instance roster is exactly as long as the declared count, at any width. The fleet-wide row asserts an INEQUALITY against the memory budget rather than equality, because runner_count is the minimum over memory, CPU and disk while declared_runner_count_for is the memory axis alone -- since the CPU axis binds first on srv1, srv3 and srv4 the two legitimately differ, and equality would have been both wrong and vacuous. Also carries the section 4c annotation hoist from #8989, without which the floor refuses at preparation and no witness in this PR can execute.
Four defects the local required-floor caught, three mechanical and one that is the interesting kind. RunnerSlotsUnobserved carried a host field. observe_runner_slot_members_wet runs LocalExec against whatever machine it is on and has NO WAY TO NAME THAT MACHINE, so the only thing that field could ever hold at the observation site was a fabricated value -- and what I wrote was "" as HostIdentity. That is a fabrication at a REFUSAL seam, which is the worst place for one: the arm exists to say "I could not read this host", and it was answering with an identity it had invented. It did not typecheck, and the reason is worth recording rather than just fixing. HostIdentity is a branded NonEmptyStr, so the empty string is not one -- the carrier's own shape refused the fabrication that a reviewer would otherwise have had to catch by reading. Construction over validation, working as specified. The field is REMOVED rather than filled. The observation reports only the cause it actually established; the caller, which knows which host it is converging, supplies the identity. runner_slot_converge_verdict already took host as a parameter, so nothing downstream loses information. The module's own note claimed "RunnerSlotsUnobserved carries the host and the cause". That is now false, so it is corrected in place rather than left standing -- a note describing a field that no longer exists is the stale-citation class, and it would have been the first thing the next author trusted. Mechanical, same run: - trim was called unqualified and unimported; it is std.algebra trim(s:). - spark_serving_fleet_converge_apply_shell was a second call site of fleet_converge_apply_shell that the signature change missed. Threaded rather than defaulted -- passing [] there would have made the spark path silently emit no slot section while looking like it had one.
…ndex instead of writing one down The CPU-axis change (#8976) turned seven witnesses red. Seven of the eight failures on main are this, and they are ONE defect rather than seven, which is what makes retyping the numbers the wrong repair. EVERY FAILING FIXTURE PICKED AN INDEX THAT WAS OUTSIDE THE COMMITTED POPULATION AT WIDTH 5-6 AND IS INSIDE IT AT 21. a_width_above_the_committed_ceiling_is_refused_not_silently_unfulfilled asked for width 7 against a ceiling of 6. At a ceiling of 21, seven is an ordinary in-range request the plan correctly fulfils. a_github_runner_in_a_fabric_slot_refuses_instead_of_reading_converged required srv1 [1, 6] to refuse. Slot 6 was outside srv1's five-wide population; at twenty-one it is an ordinary committed member. an_identity_outside_the_committed_population_is_refused_not_classified read srv1-06 and srv3-07 as outside. Both are now inside. introducing_the_fabric_slot_deregisters_no_live_runner pinned github_count == 5, which was 6 committed less 1 fabric. srv4_enables_six_named_runner_instances pinned the roster at six AND asserted srv4-07 is absent -- two measurements of the same day, falsified together. So the refusal arms did not move. The fixtures silently stopped discriminating: each chose an out-of-range index by writing down a number that happened to be out of range at the width of the day. Retyping 7 as 22 re-arms the identical landmine one width later -- a fixture whose RED depends on a number nobody derived is a change detector wearing a property's name (DESIGN 5: a measurement copied from the same current tree is not an oracle). Each now derives its discriminator: committed + 1 for an out-of-range index, committed - 1 for the GitHub count after the fabric carve, runner_count for the roster length. They discriminate at any width. TWO CLAUSES DELIBERATELY UNTOUCHED, because they are the informative half. srv3-99 is outside at any plausible width. And every srv3-06 clause passed through the width move without noticing: srv3-06 refuses because it is the AUTHORED fabric identity, not because of where it sits relative to a width. runner_slot_allocation was built that way precisely so a width change could not silently relabel a slot that may be running work, and this is that defence observed surviving a real width change rather than only asserted. ONE DELIBERATE NON-GENERALIZATION. introducing_the_fabric_slot_deregisters_no_live_runner says committed - 1, not committed - host_fabric_slot_count. The general form is true for ANY number of fabric members including zero, and that conservation is already asserted by slot_purposes_partition_every_host_committed_width. THIS row is about the specific carve -- srv3 gives up exactly one slot -- and writing it generally would leave that claim asserted nowhere. Two further rows of this class are already repaired in #8992 (witness_srv3_deploy_row_names_six_slots, witness_srv4_runner_count_six_materialization_target).
…ist (#8989) that unblocks the floor
desired_runner_slot_members mapped runner_instance_names straight through, so desired was 1..runner_count and nothing asked what any of those slots was FOR. gunbc.runner_slot_allocation authors srv3-06 as SlotServesFabricExecution, so the desired set proposed installing a GitHub Actions runner ON TOP OF THE FABRIC EXECUTION SLOT -- and reconcile would have classified it as an ordinary missing member, so apply would have done it with no refusal anywhere. That is the count-as-authority failure runner_slot_allocation exists to prevent, reintroduced one layer above it. Its own note records the first occurrence: purpose was derived by comparing index against count, so the fabric slot MOVED WITH THE WIDTH -- at width 7, srv3-07 would have become fabric and srv3-06 would have been silently handed back to Actions, relabelling a slot that may be running work. The carve was made an AUTHORED identity so a width change could not do that. This module consumed the width and ignored the carve, arriving at the same outcome by the other road. THE FILTER IS ON THE FABRIC ROLE, NOT ON COMMITTED MEMBERSHIP, and the first version of this fix got that wrong in a way worth recording. Filtering on runner_slot_membership asks the allocation authority whether each index falls within the host's committed width. That is the question runner_count already answered, and it returns ZERO desired members for any host the fleet model does not know. The reconcile fixtures in this module's witness file deliberately plant a synthetic deploy row (host_label "wfix") precisely so their expected counts are literals authored beside a known input rather than a restatement of the live fleet. Routing desired through the global width authority would have silently emptied those fixtures and turned four exact-count assertions GREEN BY VACUITY -- manufacturing the change-detector failure this lane spent the night removing, in the same session. So width still comes from the deploy row, which already derives it from gunbc_runner_slots_per_host, and this function removes exactly the identities that are spoken for. Two questions, two answers: how many slots does this host carry, and which of them are Actions runners. It works on INDICES rather than rendered names, so the fabric identity is compared as an identity and never by parsing a slot number back out of a string it was just formatted into. Two witnesses: srv3-06 is absent from the desired set while srv3-05 and srv3-07 are present, and the positive control that only the fabric host loses a target -- srv3 desires committed - 1, every other host desires its full committed width. The control matters because the first assertion alone is satisfied by a desired set that is simply too small.
…equired runner_slot_provision_plan takes an ActionsRunnerBinaryArtifact -- a release PLUS a published Linux arch -- and fleet_converge_slot_family handed it actions_runner_release_2_334_0, which is the bare ActionsRunnerRelease. Six witnesses errored with `no field 'arch' on type 'ActionsRunnerRelease'`, including four of the five converge witnesses this branch added. THE ARCH IS DERIVED, NOT AUTHORED. The fix is not a literal Aarch64 in a production module: the fleet's architecture is a fact of the cited CPU catalog, so it reads altra_max_m12830_catalog.architecture -- the same authority host_cpu_admitted_width already reads for core count. A host that is not an M128-30 therefore cannot silently inherit this arch, because the premise it rests on is named. actions_runner_binary_artifact_for_arch returns an option, since an arch with no published runner binary is a real state. That gets its own refusal arm -- SlotFamilyArtifactUnpublished -- rendered as a REFUSED line in plan.txt, counted as a refusal rather than as zero, and emitted as an exit 1 in apply.sh. It does not fall through to a default artifact, which would install some other architecture's binary. The two witness fixtures made the same mistake and are corrected the same way, matching the pattern the older witnesses in that file already used. WORTH RECORDING ABOUT HOW THIS SURFACED. A wrong argument type on a cross-module call produced NO diagnostic at parse and none at typecheck; it surfaced only as a runtime error inside the floor fold. That is the ordinary compiler floor DESIGN 4b requires -- applications bind in exact bijection, fields exist -- and it did not hold here. Filed as a separate finding; this commit only repairs the caller. It also vindicates the advice not to keep pushing over an in-flight run (fierce-hawk-734): this branch had two cancelled runs and zero completed ones, so the only thing supporting it was my argument that it should pass, and the argument was wrong.
…ts instead CI caught a real regression in my own witness after merging main. WHAT BROKE. The row asserted the panel's total equals srv1 * 2 + srv3 * 2 -- true only while the fleet was two symmetric pairs. #8976 made CPU an admission axis and the symmetry ended: srv1/srv3/srv4 became core-bound while srv2 stayed memory-bound on 8x16 GiB, because its 64 GiB upgrade failed training and was reverted. The doubling was never the property under test; it was a shortcut that happened to hold, and it turned a genuine fleet asymmetry into a red on a witness about summing. That the witness went red is correct behaviour -- it noticed the fleet changed shape. What was wrong is what it asserted. THE ATTRIBUTION, checked rather than assumed, because a red on my branch after merging main is exactly the case where blaming main is convenient. Main's own run 32621117917 at 13db52a fails EIGHT rows (fleet_intent_memory, runner_capacity_plan x2, runner_host_deploy, runner_slot_allocation x2, runner_slot_provision x2 -- all downstream of the same reverted DIMM upgrade). My branch failed NINE. The one difference is this row, and it is mine. THE FIX names all four hosts. That keeps the join the row exists to make -- the panel's total must equal the allocation authority's per-host widths -- while carrying no assumption about which hosts resemble each other, so a future asymmetry moves the number without reding the row. It also stays a real oracle rather than collapsing to measure() == measure(): the right side reads gunbc.runner_slot_allocation, a different authority from the panel fold on the left. Summing the panel's own fold on both sides would have been the quiet way to make this green and would have asserted nothing. Verified: this row and the three others in the file return true. The remaining eight failures are main's and predate this branch. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
…ative assertion (review 55040) Non-blocking review finding, and it is the absorbing fallback in my own witness file, so it is worth fixing rather than noting. empty_workspace_html matched the emission and returned "" on EmitRejected. That is ⊥-as-answer conflated with ⊥-as-ignorance: every !string_contains assertion in this file is SATISFIED by the empty string, so a total serialization failure would have rendered the negative rows green, while the positive rows could not distinguish "the panel is missing from the page" from "nothing serialized at all". Two states with opposite remedies collapsed into one answer, and the collapse fails in the quiet direction. Three changes, none of which widen: The emission is now its own function returning the typed result, so the refusal is available rather than discarded at the point of use. The rejected arm carries the reason instead of vanishing, prefixed with a marker no assertion in this file searches for -- so a positive assertion fails on it, the text names what happened, and the marker cannot accidentally satisfy an assertion either. The refusal gets its own row. Without one it is only ever observed indirectly, through whichever assertion happens to notice the page is not what it expected, and the ledger would read "the panel is absent" for a run where nothing was emitted. the_workspace_actually_serializes makes it a finding with its own name. The one row carrying a negative assertion over the HTML now also rests on the emission having succeeded. The reviewer's second note -- host_is_withdrawn / provider_is_withdrawn being Present => true / Absent => false -- I am leaving as it stands, and the reviewer read it the way I intended: both real callers want the Bool, the Option accessors are exported beside them, and dissolving the predicate would push a discarding match into every call site. The module already flags the tension; that is the honest state rather than a resolved one. Verified: all four rows over the serialized workspace return true. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf
…ns the indexing contract Both replacements in this file assert list_length(names) == runner_count and nothing else. A GENERATOR EMITTING ONE NAME N TIMES SATISFIES THAT PERFECTLY while deploying a single runner N ways -- N units all pointing at one slot directory, one registration name contending with itself. The count check cannot see it, because the count is right. Found by silent-bear-842, who independently rewrote these rows and asked what a length assertion does NOT cover before shipping rather than after. It is a hole in my rows, not a refinement of them. roster_names_are_distinct is a named function rather than an inlined clause because it belongs beside every length claim in this file, not just the one that prompted it. Applied to all three rosters. THE INDEXING CONTRACT IS BACK, ON GROUND THAT CANNOT MOVE. The rows this file used to carry asserted srv3-01 and srv3-06 by name: one-based, zero-padded, last index equals count. Those were real claims and I deleted them along with the width literals they were entangled with, because every index expectation was a function of a width the CPU axis then moved. Re-deriving them from the width would have made them vacuous -- the enumerator checked against itself. An AUTHORED runner_count breaks that circle. Three is a number the allocation authority never produced and never will, so the fixture pins one-basedness, zero-padding and the count-to-last-index relation without consulting the fleet at all. That is the planted-fixture side of the split ruled by swift-badger-524: a fixture authoring its own input SHOULD carry literals, and only a probe aimed at a live authority must derive its discriminator. MEASURED DISCRIMINATING RATHER THAN ASSUMED. silent-bear-842 planted a one-off in runner_instance_names (mapping over runner_count - 1) and both length rows returned false, so the chain from width to count to names crosses a real enumerator these rows do notice. That planted-defect measurement is the method I named as this class's next-rung trigger in my own census and then did not run.
…nto probe/future-main
…ess-census' into probe/future-main
…lots' into probe/future-main
Contributor
|
Closing: this was a local throwaway probe branch that the dashboard auto-opened as a draft PR. It contains merges of three other lanes' branches (#8987, #8992, #8998) into mine purely to answer one question locally — whether my capacity panel's widths survive those PRs landing. They do: widths stay 21/5/21/21, total 68, and my witnesses stay green. Nothing here is intended to merge. — sent from silent-bear-842 |
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.
Auto-opened by session-dashboard for session
silent-bear-842.Pushing to
probe/future-mainadvances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan