FLEET-RESOURCE-0A: one runner-width producer, the memory-per-vCPU convention read from the survey, CtrlBuild deleted

[gunbai-bot]

First stage of FLEET-RESOURCE-0 (gunbc-owned runner and compile-resource convergence). Model only — no host mutation, nothing converges to a host.

1. One runner-width producer

RunnerHostDeployment.runner_count consumed gunbc.fleet_host_budget declared_runner_count_for while gunbc.runner_slot_allocation gunbc_runner_slots_per_host (the min over memory/CPU/disk) was the documented derivation.

Correction to an earlier version of this body: those two did not disagree. gunbc_runner_pool_budget_for = slots × memory_max and gunbc_ci_runner_cgroup_memory_cap is memory_max, so declared_runner_count_for = floor(slots·k ÷ k) = slots. It was a semantic round trip, not a competing authority. The deletion is behaviour-preserving.

Underneath sits a §3 nickname worth naming: gunbc_runner_pool_budget_for is named as supply and computes demand. The genuine supply function runner_slice_cap(host, overhead, session_slice, headroom, compile_pool) lives in the same module. That nickname is why host_memory_admitted_width is an authored literal table — the memory axis has no supply-side denominator, and deriving one from the budget would close a loop, since the budget derives from the width. Repairing it needs the derivation hoisted above runner_slot_allocation. That's FleetHostResourceAllocation, not this PR.

2. The 1:3 ratio is surveyed, not authored

byte_size(3000000000) deleted; gunbc_runner_memory_per_core() reads memory_per_vcpu from gunbc.runner_shape_census against the Ubicloud aarch64 catalog.

GitHub Actions is deliberately not a second source, and the census says so rather than this PR asserting it: GHA's aarch64 catalog reads 4/vCPU where uniform and carries two non-integral sizes (arm-5core at 14, arm-64core at 208), so memory_per_vcpu refuses on it. Averaging the survey would mint a figure no vendor publishes.

Correction — an earlier revision of this section and its annotation were wrong on both halves, and the error was load-bearing. They claimed no vendor page states whether its "GB" is decimal or binary, and adopted gibibytes on that basis, citing an operator ruling of 2026-08-30. There is no such ruling; I wrote it. And the basis was stated: extdeps.cloud.ubicloud quotes its catalog as QuotedDecimalGigabytes. What discarded it was the census — per_vcpu_magnitude rebuilt every ratio as QuotedWithoutBasis, so each consumer had to re-guess an answer the rows already carried. See §7.

3. A zero-memory slot shape now refuses explicitly

The identity in §1 holds only for memory_max > 0 — measure_fit_count_floor returns 0 at a zero divisor. So the deleted round trip was carrying a zero-cap refusal by accident. The derived path would still refuse (cores_per_slot → 0 → ZeroRunnerWidth), but gunbc_runner_slots_per_host consults host_held_runner_width first, and srv2's held 5 never looks at the slot shape. RunnerSlotShapeStanding states it, checked before the held arm.

The RED is authorable because the standing takes the shape as a parameter — gunbc_runner_slot_desired() is fixed, so without that parameter the check would be permanently green by construction and cited as coverage while proving nothing. Positive control included.

4. The per-slot CPU ceiling reaches systemd

cores_per_slot decided how many units to create and then vanished. Measured on the hosts: srv1 and srv2 carry MemoryMax as their only resource line — CPUWeight [not set], CPUQuota infinity, AllowedCPUs empty. The CPUWeight=100 in systemd_unit_file_witness_test is on no host, and wouldn't be a ceiling if it were.

extdeps.systemd gains CPUQuota, valued as DirectiveCpuTime { threads } rather than the general percentage arm systemd_directive_value_grain filed as latent — that filing's obstacle ("a fraction of a host figure this repository does not hold") doesn't apply, since CPUQuota is CPU-time-per-wall-second where 100% is one CPU by definition. The memory half of that filing stays open.

The knob rides ConvergeTarget's existing property-generic per-slot mechanism, which per_slot_tasks_max already uses; its own declaration declines the ~96-site rename to PerSlotUnitProperty and binds it to the HostAxisBundle P3 lane.

The ceiling is a function of where compiler work is charged. runner_cpu_boundary_for consumes the compile-pool topology and refuses under CompilePoolSliceDeclared, because compile_pool_bytes_for charges that pool in bytes only and 21 × 6 = 126 of 128 leaves nothing for it. The topology flip cannot land without rederiving width and ceiling together.

RunnerCpuBoundary has exactly one constructor. An earlier revision carried DisjointCpuSet; review 57675 showed it converged successfully while realizing nothing, so it was deleted rather than answered with a refusal — §4b ranks construction above proof. Trigger to reinstate: an AllowedCPUs directive and a producer that assigns disjoint sets.

5. build_tokens stops being nproc

It was stored raw and converged into the jobserver's token count, so compile concurrency written to every host was every hardware thread — 128 — while extdeps.jobserver already carried the installed daemon's formula, cited from its defaults. Calling it yields 120 on srv1 and 62 on srv2; 62 is exactly what that daemon's own header predicts for srv2, which is the corroboration that this is the installer's intent. An absent citation refuses.

Known follow-up, not resolved here: this correction does not repair the acute starvation it sits next to — a correctly sized pool still leaks to zero, because permits are held by killable clients and returned only cooperatively. Per the FLEET-RESOURCE acute ruling this field must not stay a normal RunnerHostDeployment field; it moves behind a bounded LegacyHostJobserverBridge or is deleted with the old root at cutover. Raw nproc under a rung drop is explicitly not an option.

6. CtrlBuild deleted

Along with the build_wrapper carrier: one consumer, linked_cache_interface already expresses the relation, BakedInImage/NoBuildWrapper had none — so removing only the variant would leave a permanently-Absent field where an authority used to be.

Not closed by this PR

• host_memory_admitted_width is still a per-host literal table (25/5/29/29) — see the layering argument in §1.
• host_held_runner_width still returns a literal 5 for srv2 by host-name comparison; a declared operator hold awaiting a call on refusal vs a §4b rung drop.
• Session containers carry CPUWeight, not a CPU ceiling, so host CPU conservation is not closed by per-runner quotas alone.

7. The ratio was read as bytes (fixes the floor red on 22abdb48)

The floor refused five witnesses. Root cause, measured by rendering the deploy manifest rather than inferred: gunbc_runner_memory_per_core returned gibibyte(quoted_numeral(q)) into a declared -> ByteSize. It typechecked, and the value was Measure { count: 3 } — three bytes per core. cores_per_slot became 5,726,623,062, host_cpu_admitted_width divided to zero, and every host reached deployment=refused cause=zero_runner_width. The same instrument now shows srv1/srv3/srv4 at 21 runners, per_slot_cpu_quota=600%, build_tokens=120, with srv2 refusing on its pre-existing session denominator.

The basis now travels with the ratio. sample_quoted_basis folds the sampled rows' basis exactly as sample_unit_label already folds their unit word, and the conversion is the extdeps authority's own quoted_magnitude_bytes, which refuses on a genuinely basis-less sample instead of letting a consumer substitute one. The unstated and mixed arms still degrade to the basis-less magnitude — that is the honest reading when a sample really does not agree.

The refusing arms now refuse. Every non-uniform reading mapped to byte_size(0) and relied on the zero travelling three functions to surface as ZeroRunnerWidth. That is an absorbing arm wearing a refusal's name, and it is precisely why a unit bug presented as a fleet-wide width of zero under a diagnostic naming neither the ratio nor the conversion. RunnerMemoryPerCoreResolution, RunnerCoresPerSlotResolution and CpuAdmittedWidth carry the cause; ci_runner_placement refuses by name on RunnerCoreRatioUnresolved; the CPU axis reports AxisUnmeasured rather than admitting a width it could not compute.

Correcting a claim in an earlier revision of this body. It said "the live path is honest", which is true of one path and not of the wider production surface. gunbc_runner_slots_per_host still returns Int, and it is consumed directly by four RunnerHostDeploy data rows — where it becomes the materialization target, so an unresolved ratio rendered as zero would change the desired runner population from the host's admitted roster to an empty one — and by host_axis_caps, as the upper bound of the runner-unit roster whose system-control shadows get reverted, where a zero produces no reverts and can leave stale effective caps in place. Removal ownership refuses destructive teardown, which contains the harm, but the plan would still be answering the wrong question. The placement path is honest; the width chain is not, and that is what the stacked cascade exists to close.

runner_memory_per_core_of takes the reading as a parameter, for the same reason §3's standing does: a zero-argument derivation over the live census can only be exercised on whatever the survey currently says, so its refusing arms would be permanently unreachable and a check on them would be a decoration. Two REDs (basis-less uniform reading; absent survey) plus a positive control pinning the vendor's 3 GB decimal — which doubles as the regression control, since reading that numeral as gibibytes or failing to convert it both go red there.

Filed, not fixed here: the wall under all of this is inert

std.measure declares type Measure<Q, S, M> { count: M }. Q and S appear in no field — they are phantom, so ByteSize = Measure<Memory, One, Nat> and Gibibyte = Measure<Memory, Gibi, Nat> have identical representations, and the declared-return path admitted the pair.

Narrowing an earlier version of this claim. It said the two "unify freely", which is stronger than what was measured and is false: test.claim.declared_type_inhabitance_direct_call_witness already refuses Wrapper<KindB> at a Wrapper<KindA> parameter with K phantom and the representations identical, so applied-argument identity is enforced on at least one direct-call path. The accurate claim is that it was lost on the declared-return path, and the complete expected-type matrix is not yet measured.

That module's own prose claims the opposite: carrying them as two Measure types at two Scales "makes the comparison a conversion the author must write ... which is the same resolution ByteBasis reaches by validation and this reaches by construction."

Stated at the grain the evidence supports. The universal Measure guarantee is not established across expected-type paths. Two specimens prove two open paths — the declared-return Gibibyte → ByteSize, and a resolution coproduct reaching a one-field measure parameter through a call. At least one direct-call applied-argument path is closed. Other quantity, scale and clock-basis applications are at risk but unmeasured until the expected-type matrix runs. The class-wide rung is outside the ladder, because §4b takes the minimum over in-scope paths and the minimum is silent — but "every distinction is structurally open" is more than has been measured, and an earlier revision of this section said it. Whether the repair is a checker change or a modeling one (scale as a field, or distinct nominal types) decides the shape of the fix, so it is filed as its own lane rather than widened into this PR.

[gunbai-bot]

Correction to this PR's stated justification

The change stands; the reason given for it is wrong, and I'd rather correct it than let it merge on a false premise (including past an approval that cited it).

What the PR body claims: that declared_runner_count_for and gunbc_runner_slots_per_host are two producers that disagree — "21 committed against a memory admission of 25/29".

What is actually true: they were identical by construction.

gunbc_runner_pool_budget_for(host) = gunbc_runner_slice_cap_declared(host)
                                   = gunbc_runner_slots_per_host(host) × gunbc_runner_slot_desired().memory_max

gunbc_ci_runner_cgroup_memory_cap  = gunbc_runner_slot_desired().memory_max      (ci_floor_measurement.dag:18)

declared_runner_count_for(host)    = floor(pool_budget ÷ gunbc_ci_runner_cgroup_memory_cap)
                                   = floor(slots × memory_max ÷ memory_max)
                                   = gunbc_runner_slots_per_host(host)

It multiplied by a constant and divided by the same constant to return its own input. The 25/29 figures belong to host_memory_admitted_width, a different function; I attached them to the wrong symbol.

So the deletion is right for a stronger reason. Not a competing authority — a §5 tautology, the measure() == measure() shape: a second name whose entire content was a round trip. It also means the change is behaviour-preserving for runner_count, which is the correct expectation to review against rather than the numeric shift the body implies.

The underlying defect is §3 nicknaming, and it is worth naming here because it is what the next PR in this lane has to repair: gunbc_runner_pool_budget_for is named as a supply fact — what a host makes available to runners — while its body computes demand, what the committed slots sum to. The genuine supply-side function lives in the same module (fleet_host_budget.dag:358 runner_slice_cap(host, overhead, session_slice, headroom, compile_pool)) and is wired at :435; the nickname shadows it wherever "budget" is asked for.

That nickname is also why host_memory_admitted_width is an authored literal table (25/5/29/29) rather than a derivation: the memory axis has no supply-side denominator wired to it. The literal is what keeps the graph acyclic — deriving the axis from the pool budget would close the loop, since the budget is itself derived from the width. Repairing it in place is therefore impossible without a cycle; the derivation's inputs live above runner_slot_allocation, so it has to be hoisted into one host-keyed allocation value. That is FLEET-RESOURCE-0A's FleetHostResourceAllocation, and this is the argument for it from the tree rather than from the design note.

No code change accompanies this comment — the diff is unchanged and I am not re-litigating the approval, only the sentence it was granted against.

— sent from eager-ram-258

[gunbai-bot]

review 57675 (REQUEST_CHANGES) — fixed in 22abdb4882

The finding is correct and the annotation defending the arm was wrong. runner_cpu_boundary_knobs answered DisjointCpuSet with an empty knob list, so a deployment carrying that boundary converged successfully while the host was told no CPU ceiling at all. That is fail-open under §5 — the line doesn't stop, nothing is typed or located — and the "unemitted" string in the manifest is a receipt label, not a refusal on the operational path. My comment claimed emitting nothing was the honest arm; emitting nothing is only honest if something refuses, and nothing did.

I took the deletion rather than the refusal, of the two remedies you offered. §4b ranks them: construction over proof. Propagating a typed refusal through convergence leaves the invalid state writable and makes safety depend on that refusal executing — mechanically preventable. Deleting the constructor means no Accepted program can carry a boundary this emitter cannot realize — structurally impossible, and the smaller change.

RunnerCpuBoundary now has exactly one constructor, so runner_cpu_boundary_knobs and runner_cpu_boundary_text are total with no arm that realizes nothing. Every representable boundary emits a knob.

The distinction the variant recorded survives as an annotation — which is where a promise nobody can construct belongs — with the trigger for reinstating it stated as a conjunction: an AllowedCPUs= directive in extdeps.systemd and a producer that assigns disjoint sets. Both, because either alone reproduces exactly the unrealizable state this deletion removes.

Same commit also repairs the sentence above the type, which still read that DisjointCpuSet "is modeled rather than omitted" — a note describing a deleted authority in the present tense, which is the contamination this lane already flagged once in gunbc.fleet_intent.

— sent from eager-ram-258

[gunbai-bot]

Addressed in the next push, and the general claim checked rather than assumed.

The local point is right, and I took a better route than the one suggested. sample_quoted_basis_eq is gone, along with SampleBasisAccum and sample_quoted_basis_step. The predicate existed only to fold basis unanimity, and an accumulator-versus-element comparison carries an asymmetry it then has to describe: the first row is privileged, so the accumulator needed a seen flag beside the value purely to give "not yet seen" a meaning. Counting each arm removes the predicate, the accumulator type and the flag together — three declarations become two, and order-independence becomes structural instead of argued. Refusal behaviour is unchanged: any unstated row, or both bases present, still degrades to the basis-less magnitude that quoted_magnitude_bytes refuses.

The general claim does not hold, and I would rather say so than comply silently. There is no predicate-dissolution rule in DESIGN.md or docs/design-ledgers.md — I checked both. And the idiom is the corpus norm in the most load-bearing layer there is: std.effect_grant verb_eq and std.induction recursion_shape_eq are nested exhaustive matches over nullary coproducts returning true/false, character for character the shape objected to. If that is blocking substrate debt, it is std's and fleet-wide; it is not something this PR introduced, and a bounded disposition naming this one function as the debt would have been a false record.

Worth flagging for the same reviewer's attention, since it is the substantive type-system defect on this branch and outranks the predicate: gunbc_runner_slot_allocation_wall_holds was passing two coproducts into parameters declared as one-field measures (hardware_thread_count_value, byte_size_count). It typechecked, and the required floor stayed green over 3,136 witnesses. That is repaired in f2eda971, and the specimen is recorded — explicitly not claimed as enrolled — because test.claim.declared_type_inhabitance_direct_call_witness already refuses distinct unapplied constructors through a call, so this is not the general call-argument case and the discriminator is unmeasured.

— sent from eager-ram-258

[gunbai-bot]

The matrix ran, and the cause is located. chunk_24's annotation deliberately declines to name a mechanism and lists the candidates as coproduct producer, transparent alias expansion, generic application identity, cross-module resolution, or an interaction. Measured on synthetic source with no std.measure, no alias, no coproduct and no module boundary, it is generic application identity — specifically the type ARGUMENT, and only the argument.

Run with a locally built gunbc against compile_dag_diagnostic_census, counting diagnostics of any class (not just DeclaredTypeNotInhabited, which matters — see the instrument note below):

source shape	diagnostics	verdict
-> Int { "x" } — literal, non-generic	1	refused
-> Int { produces_string() } — call result, non-generic	1	refused
-> Box<TagA> { 5 } — wrong constructor head	1	refused
-> Box<TagA> { produces_a() } — matching argument (positive control)	0	correctly admitted
-> Box<TagB> { produces_a() } — phantom parameter, wrong argument	0	admitted
-> Box<TagB> { produces_a() } — parameter used in a field, wrong argument	0	admitted

where type Box<T> = MkBox { n: Int } (phantom) or MkBox { v: T } (used), and TagA/TagB are distinct empty records.

So declared-return inhabitance is checked for non-generic types — in literal and call-result position alike — and is checked for the generic type constructor. It is not checked for the type argument. Whether the parameter is phantom or carried in a field makes no difference, which kills my own starting hypothesis.

That is exactly the incident's shape: Gibibyte and ByteSize are both applications of Measure differing only in type arguments, so fn gunbc_runner_memory_per_core() -> ByteSize { gibibyte(...) } had nothing left to check. It also explains why the sibling direct-call witness already refuses distinct unapplied constructors — that path compares heads, which is checked.

Two candidates are falsified, not merely unselected. It is not the coproduct producer and not cross-module resolution: neither appears in any fixture above, and the defect reproduces without them. Alias expansion is likewise unnecessary. The minimal reproduction is six lines of source with one type parameter.

An instrument note that changes how these fixtures should be read. violation_count(..., wanted: "DeclaredTypeNotInhabited") returned 0 for a blatant -> Int { "not an int" }, while the total-diagnostic count for that same source was 1. The compiler refuses it under a different class name. So a > 0 assertion on that specific class can read as "admitted" when the program was in fact refused, and the four fixtures in chunk_24 inherit that hazard. Counting all classes, plus a positive control that must be non-zero, is what made this matrix trustworthy — without the blatant control I would have reported "phantom parameters are ignored" from three zeros that were measuring nothing.

I have not modified this PR. The fixtures are held for enrollment as a follow-up so this stays merge-ready.

— sent from eager-ram-258