Repository navigation
Per-host runner capacity decision: width as a minimum over axes, sessions charged by residency - #7891
Merged
Merged
Conversation
…nd overhead charged per host
The fleet ran one allocation row for four machines: 5 slots x 16GiB
MemoryMax everywhere, one fixed-overhead number, and a conservation wall
that charged zero for sessions on every host. That shape could not say
"this host is different", so the only way to widen srv3/srv4 was to widen
srv1/srv2 too — which their RAM cannot carry.
MEASURED BASIS FOR 14GiB. 186 floor-job cgroup peaks from 2026-08-05 plus
five sampled days back to 2026-07-16, read from the [calibration]
floor_peak_post receipts the ci job emits. Successful runs peak at p50
10.32GiB / max 10.96GiB; no run in the sample reached the 16GiB
MemoryMax. Four of 186 reached exactly 15.0GiB, which is MemoryHigh —
throttle pins, censored lower bounds rather than demand, and the reason
the cap does not fall further. MemoryHigh lands at 13GiB, 1GiB above the
already-measured 12GiB gunbc_floor_minimum_viable_armed_budget that
claim_executor enforces at arm time, and above the worst p90 in the
sample (12.94GiB, 2026-07-30).
PER-HOST WIDTH, DERIVED NOT AUTHORED. srv1/srv2 5 slots, srv3/srv4 7.
Neither number is a target: both are the largest width the conservation
wall passes once the two per-host facts are charged, and they move if
either fact is corrected.
TWO FAIL-OPENS IN THE WALL, BOTH LIVE:
- session_pool was byte_size(0) for every host, unconditionally. srv1
and srv2 carry an InteractiveSessionCompiles instance
(build_cache_desired_instances) and owe a 20GiB reservation the wall
could not see. At the previous 5 x 16GiB they summed to 123.8GiB
against 125GiB usable — 1.2GiB of real margin, reported as room for
two more slots. Raising the fleet-wide width without this fix would
have overcommitted them by ~17GiB through a wall returning true.
Which hosts carry sessions is now read from the deployed-instance
roster, never re-listed.
- conservation checked against the 128GiB DIMM nominal rather than the
125GiB OS-usable authority, a 3GiB overstatement that
fleet_host_memory_nominal_vs_usable_note exists to forbid. It decides
an admission at exactly this width: an 8th 14GiB slot passes against
nominal and fails against usable.
OVERHEAD SPLIT INTO TWO KINDS OF FACT. The old row was a single fleet-wide
HostFixedOverheadMeasured of 17179869184 — 2^34, a round power of two,
with no observation behind the constructor that claims one. Now:
HostFixedOverheadAllowance for srv1/srv2 (16GiB, unchanged, an operator
allowance for deployments the model does not describe) and
HostFixedOverheadMeasured for srv3/srv4, derived as MemTotal minus the
2026-07-16 arm-time MemAvailable high-water on srv3-08 (run 29537878075)
= 6017638400 bytes, an upper bound on non-reclaimable residency.
Unclassified hosts refuse rather than inheriting either.
The single Scaffold splits with it, into two successors that correctly do
NOT yet exist: gunbc_ci_managed_host_quiescent_meminfo_read and
gunbc_ci_legacy_host_modeled_residents. An earlier revision of this change
misread the old gunbc_ci_per_service_overhead bind as a defect for naming
a declaration that has never been written, and re-bound both scaffolds to
rows this module already declares. That inverts the mechanism:
v2.lens.disposition_redundancy counts a violation when a bind target is
PRESENT, so an absent successor is the normal state of outstanding debt
and the repair would have turned two honest markers into two false claims
that the debt was paid. Only the grain was wrong — one successor for one
fleet-wide number, where there are now two facts closing on different
events. v2/lens/disposition_redundancy_test tracks both marks; its
fires-on-successor-present control still expects 1, so it continues to
discriminate bind-matching from mark-counting.
ALSO: srv4 joins gunbc_committed_runner_slot_allocations — it has carried
fleet work since 2026-07-22 while absent from the roster that says what
its slots are. runner_slice_cap is now derived as slots x MemoryMax, so
guaranteed mode holds by construction instead of by a hand-maintained
second literal. host_converge_slice1's review-41089 gap closes by its own
trigger: declared_runner_count takes a HostIdentity, no interim shim.
NOT CLOSED, AND GATING: srv4's 500GB NVMe. runner_deployment_plan models
RAM only, so the solver's 7 is a memory verdict; srv4_runner_host_deploy
stays pinned at 5 and its note is corrected (it cited a RAM-derived 10
from the retired 8GiB x 10 shape). Slots 06/07 must not be provisioned on
srv4 on the strength of the plan alone. Width INCREASE also remains
unmodeled — converge drains only — so landing this changes the declared
intent, not the live hosts.
Witnesses: conservation gains four discriminating controls, including one
proving the old zero-session wall would have admitted the srv1 overcommit
the new one refuses. Three change-detector assertions that retyped byte
literals from the row twenty lines above them are replaced by relations
between independently derived quantities; witness_srv3_symmetric_to_srv1
is superseded by an assertion that srv3 outbudgets srv1 by exactly the
overhead gap, which is strictly stronger than the inequality.
SWAP, ruled and deliberately not modeled further (operator, 2026-08-05):
MemorySwapMax stays 32GiB/slot, so widening takes srv3/srv4 from 160 to
224GiB of declared ceiling — 48% of srv4's 500GB NVMe. Accepted: nothing
else runs on these hosts. That settles SIZING and leaves BACKING exactly
where it was: gunbc.host_swap_backing still derives UnknownRefused for all
four hosts because no one has read /proc/swaps, and a green MemorySwapMax
over an unobserved swap device is the presupposition failure that module
exists to make representable. The two are different facts and this ruling
answers only one of them; no per-host swap row is authored here.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Bugbot is not enabled for your account, so this pull request was not reviewed. Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs. |
DECLARED_RUNNER_SLOT_MEMORY_HIGH_BYTES is a §7 seed-retained hand-Rust mirror of gunbc.runner_slot_allocation gunbc_runner_slot_desired().memory_high, and its doc comment cites that row's literal verbatim. The per-host allocation ruling moved the authority 16106127360 -> 13958643712, so without this the constant is a stale duplicate AND its citation is false — in the same commit that made it so. Only binds on UNCAPPED hosts: read_host_budget_bytes prefers cgroup memory.high, and every fleet slot has one, so production never reaches this arm. That is what makes the staleness quiet rather than harmless — it surfaces exactly where caps are not yet applied, which after this ruling means srv3/srv4 slots 06/07 before converge lands, and dev machines. dissolve-on unchanged: v2 emit of stage0 host-budget constants from the allocation authority, which retires the mirror instead of re-syncing it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…unread file on macOS Two macOS defects, both the same shape: code asserting a fact about a platform it never checked. THE LIVE ONE. memory_governor::read_host_budget_bytes ended with (mem_total_bytes(), "/proc/meminfo MemTotal".to_string()) — the label composed unconditionally beside a read that returns None whenever /proc/meminfo is absent, which on Darwin is always. Every local run printed `source=/proc/meminfo MemTotal` on a machine with no /proc: a source attribution for a read that never happened, next to a value never obtained. Loud, so nothing was concealed, but fabricated provenance — the section 5 plausible-output shape applied to a diagnostic — and unreadable in the way that matters, since "MemTotal said something we distrusted" and "there is no MemTotal here" rendered identically. It now reports `unavailable: no readable /proc/meminfo on this host (target_os=macos)`. The trailing "falling back to a host-shared signal" goes too: on this arm there is no signal at all, and the source field already names what was used. THE MODELING, which is the point rather than the one-line fix. extdeps.linux.procfs: procfs as a cited Linux kernel interface (proc.5), the four paths this repository reads, and kernel_provides_procfs as a TOTAL match over the existing closed std.os.types.KernelFamily — so adding a kernel forces an answer instead of defaulting. Absence of /proc on Darwin is not a failed read, a permission problem, or an unreachable host; ObservationVerdict's Inaccessible and UnknownRefused both misfit, because the producer exists and the host is the machine running the code. It is a category error about which kernel is running, decidable in advance. LinuxGuestOnWindows answers true deliberately: WSL2 runs a real Linux kernel, and treating it as Windows would refuse observations the host can serve. gunbc.host_budget_source: the closed set of places the governor's budget can come from, replacing a free-text label that was doing two jobs — human diagnostic AND machine discriminant, since cli_run decides degradation by scanning it for "memory.high"/"memory.max". The comment beside that scan already named this fix and the rule it breaks. Degraded is now a total match; rendering is one function; BudgetSourceUnavailable carries the kernel and is the arm the macOS path had nowhere to put. WITNESSES. Nine rows, SubstrateInputsOnly so they give the same verdict on every platform — deliberate, because a check that only ran on the affected platform could never run on the fleet's Linux CI, which is how the fabricated label survived. The discriminating pair is RED_procfs_sources_are_inadmissible_on_kernels_without_procfs plus its positive control: neither alone proves anything (one is satisfied by a predicate refusing everything, the other by the unconditional true that ships today), and together they pin the boundary at exactly "reads procfs AND kernel lacks procfs". Verified by perturbation — reverting the predicate to `true` reds that row and only that row. PEAK RESIDENT. peak_resident_measured_holds cannot pass without procfs and nothing said so; diagnosing it during this PR meant stashing the tree and re-running against main to prove the failure was the platform and not the diff. It now declares a typed ProcSelfStatus precondition. It does NOT branch on platform to return true — a witness that greens where it cannot observe reports coverage the fleet does not have, and CI runs on Linux where the skip would hide nothing while lying everywhere else. The deficit stays visible; dissolution is a Mach task_info realization behind the same builtin. HONEST RESIDUAL: v1 still hand-realizes this model (the seed cannot read .dag values at the point enforce_typed_cache_entry_cap needs the cap — it bounds the memory used to resolve the corpus), so host_budget_source carries a declared seed-mirror scaffold rather than pretending it is wired. That is the same unchecked-mirror class that let DECLARED_RUNNER_SLOT_MEMORY_HIGH_BYTES drift in this PR; one lens reading the seed's constants against their cited rows would cover all three. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…sctl, and a refusal
Operator ruling 2026-08-05: "we can't do fallbacks". The previous commit
modeled the macOS gap honestly and left the mechanism intact, which was
the wrong half of the job — an accurate label on an absorbing fallback is
still an absorbing fallback.
THE STRATEGY CHANGED. macOS is not a platform without memory facts; its
memory facts were never asked for. Reading VmHWM through /proc was a
TRANSPORT choice (section 3: one of N, never a fact about the observation),
and mistaking a transport limit for a capability limit is how "peak RSS is
unavailable on macOS" came to be believed. It is not:
peak RSS -> getrusage(RUSAGE_SELF).ru_maxrss, POSIX, ONE call for both
platforms rather than two transports selected by platform.
libc was already a stage0 dependency.
total RAM -> sysctl hw.memsize on Darwin (verified live: 17179869184).
POSIX deliberately leaves ru_maxrss's unit unspecified, so implementations
diverge permanently. Linux reports kibibytes, Darwin bytes — confirmed by
execution, not from the manual: a bare python3 reported 15417344, which is
14.7 MiB as bytes and an impossible 14.7 GiB as kibibytes on a 16 GiB
machine. Reading a Linux value as bytes understates peak residency 1024x,
in the direction that looks survivable. extdeps.posix.rusage owns the
interface and refuses to answer the unit; extdeps.linux.rusage and
extdeps.darwin.rusage each answer for their own implementation.
A THIRD COPY, found while wiring it. The interpreter's
observed_peak_resident_bytes arm carried its OWN inline procfs parse,
separate from cli_run's — two implementations of one observation, and the
copy that actually executes for witnesses. Fixing only cli_run's would
have left the witness Linux-only and looked like it worked. Both now route
through one reader.
THE REFUSAL. typed_module_cache_cap_derivation ended in
.unwrap_or(TYPED_MODULE_CACHE_MAX_ENTRIES_CEIL): an uncomputable budget
became the most permissive cap available. That is not hypothetical — it
OOM-killed the full witness corpus twice on the operator's Mac (exit 137,
at ~6800 and ~3300 witnesses). Nothing readable, cap defaults to ceiling,
nothing bounds the resolve, kernel ends the process; the deficit's
frequency was zero by construction so it never ranked for fixing. It now
panics with a typed diagnostic naming the modeled authority. Every platform
we run on has a real source, so reaching that arm means an unmodeled host —
exactly when an invented bound is least defensible.
MEASURED LIMIT, stated because the refusal does NOT fix the OOM: a 16 GiB
Mac derives 17179869184 / 3 MiB = 5461 entries, clamped to the 4000
ceiling — the same cap it had before. What changed is that the cap now
descends from a real host fact instead of from ignorance. Resolving the
whole corpus still needs more than this machine has; that is a genuine
capacity fact about a 16 GiB laptop versus a 125 GiB runner, not something
a budget source can repair.
RETIRED BY ITS OWN TRIGGER: the ProcSelfStatus precondition added one
commit ago. It declared this witness could not pass without procfs — true
of the code, false of the world — and peak_resident_measured_holds now
passes on macOS. Writing the wrong declaration down is what made it
checkable; left implicit it would have hardened into a platform the corpus
had quietly agreed not to cover.
Witnesses: 14 rows, SubstrateInputsOnly so they hold on every platform —
a check that only ran on the affected platform could never run on the
fleet's Linux CI, which is how the fabricated label survived. Two
discriminating pairs, both verified by perturbation:
RED_procfs_sources_are_inadmissible_on_kernels_without_procfs (reverting
the predicate to `true` reds that row and only that row) and
RED_unreadable_budget_yields_no_number_at_all, which any fallback
returning ANY number would red.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…nt lane srv1's CI build jobs run a median of 607000ms against a peer median of 238000ms — 2.55x — while its job failure rate is 26.2%, the SECOND LOWEST of the four hosts. Counting conclusion=failure finds nothing here, and counting cancellations finds nothing either. The harm is pure latency: ~6.2 minutes excess per build, 44 builds in the window, roughly 4.5 hours of wall-clock per day on the job that gates everything downstream through release-bins. THE MECHANISM IS VISIBLE IN THE DISTRIBUTION. Sorted, srv1's 44 samples split into two clusters with an EMPTY GAP between 112000ms and 505000ms — ten fast, thirty-four slow, nothing in a four-minute void. There is no partially-warm state because a compile is either served from cache or it is not, which is the one-server-per-host topology gunbc.fleet_host_budget gunbc_compile_pool_doc already describes. A CORRECTION THE FULL DISTRIBUTION FORCED, and it sharpens the diagnosis. srv1's fast cluster was first read as "faster than peers" by comparing its 78000ms floor to the peer MEDIAN. Wrong comparison: peer minima are 74000-81000ms, indistinguishable. Every host gets full cache hits at the same speed. The difference is entirely at the top — peers cap at 342000-372000ms, which is what a MISS costs on a healthy host, while srv1's misses run 505000-1640000ms, 1.4x to 4.4x a peer's worst. srv1 is not merely cold; its misses are individually more expensive, consistent with the server being memory-starved while compiling (229780 memory.max breaches, 12 oom_kills). Relocating that server fixes placement and leaves it unbudgeted; the durable repair is the managed unit plus the declared compile-pool slice. WHAT THIS MODULE IS: typed populations, a linear median selection after sort (this substrate exposes only first/last/length, so an index needs an explicit fold — and a quadratic rank-count would be the cost-shape defect DESIGN section 6 always fixes), an operator divergence policy, and a verdict. The 2x ratio is a policy budget grounded in all four hosts being the same board with the same caps — identical hardware cannot sustain a 2x median divergence for a hardware reason — not a threshold fitted to srv1, which sits at 2.55x and would still be caught at 2.5x. WITNESSES TEST THE DERIVATION, NOT THE FLEET. A row asserting "srv1 is slow" would compare a live population to a literal read off that same population, and would go RED when the defect is FIXED. So the fixtures are controlled, with the policy boundary straddled by one millisecond in both directions, and an empty population asserted to REFUSE rather than pass — the arm that would otherwise let a quarantined or wholly-failing host read as healthy. The one row touching recorded data checks internal consistency only: the stored verdict must equal what its stored samples re-derive. THAT WITNESS EARNED ITS KEEP IMMEDIATELY. It failed on first run: the derivation returns 607000ms (lower median, the declared convention) while a sibling note quoted 609000ms, which is the mean of the two middle samples — a duration no build on srv1 ever took. median_selection_note had declared the convention two declarations earlier and the prose violated it anyway. Corrected, with the receipt kept in the note. NO LIVE PRODUCER, and the module says so rather than implying one: the population was hand-collected and is a 2026-08-05 snapshot. The producer needs only the Actions jobs API, which already returns started_at, completed_at, conclusion and runner_name — no host access, no ssh, and nothing through the A1 secret-materialization gap, which is the argument for building it before the placement lane rather than after. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…oster ci_runner_placement decided whether a host owes a 20GiB sessions reservation by asking whether build_cache_desired_instances listed an InteractiveSessionCompiles instance for it. That CORRELATED with session residency and was nothing more than a correlation. It came within one cleanup of causing the bug the charge exists to prevent. On 2026-08-06 ctrl-sccache.service was removed from srv1 and srv2 as provably dead — 29MB accumulated in 45 days, zero socket connections, zero cache writes in the preceding week, because session containers set SCCACHE_DIR to their own in-container path and never used it. The obvious follow-up, dropping the now-meaningless session rows from the desired roster, would have silently stopped charging both hosts. The conservation wall would then have admitted 7 slots on each and overcommitted them by ~17GiB while returning true — the exact defect this PR opened by closing, reintroduced by a tidy-up two files away, with no test able to see the connection. Sessions consume host RAM whether or not a shared build cache exists for them. Measured the same day the cache was found dead: srv1 and srv2 were each running NINETEEN containers under sessions.slice. gunbc.session_residency is now the single authority. Positive rows are observed (the 19-container counts, plus deploy_dashboard_srv1's host pinning); negative rows are operator-declared and say so — srv3 refused a key login (the B2 gap) and srv4 failed host-key verification, so neither could be counted. That asymmetry matters in one direction specifically: the NEGATIVE rows are the ones that grant capacity, so they carry the dissolve-on and are first to re-check when those hosts become reachable. The unknown-host arm CHARGES rather than exempts, deliberately inverting the refuse-by-default convention this lane uses elsewhere. Refusing is not available — the consumer needs a Bool to size a budget — so the choice is between two wrong answers. Charging a session-free host wastes slots on it: visible, recoverable. Exempting a session-bearing host removes the largest non-runner claim from the conservation sum: the srv4 OOM shape, not recoverable inside CI. Plan output is unchanged (5/5/7/7, 24 concurrent runners) — this replaces the derivation, not the verdict. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…dmission
jobserver_config was JobserverAbsent, which made CompilePoolSliceDeclared
refuse with CompilePoolUnresolved and would have made the whole
runner_deployment_plan PlanUnsound the moment anyone flipped the compile
pool placement. That refusal was correct: the model carried the
installer's derivation and lacked its inputs.
It was never a modeling gap — it was a REACH gap, and it closed the moment
srv1 became readable. /usr/local/sbin/ctrl-jobserver documents
tokens = max(1, min(cores - MARGIN, floor(usable_mib / MIB_PER_JOB)))
with usable_mib = (MemTotal_gib - MEM_RESERVE_GIB) * 1024, which is
extdeps.jobserver.derive_jobserver_tokens term for term. So this is a
citation, not an approximation: margin 8 cores, mem_reserve 16GiB,
mib_per_job 1792MiB, read from the script's own defaults on srv1 (same
unit on srv2).
Citing moves no current number — gunbc_compile_pool_placement is still
CompilePoolInRunnerSlots, so compile_pool derives zero and the plan stays
5/5/7/7 at 24 concurrent runners. What it unblocks is the flip.
THE FINDING THAT CAME WITH IT. Both hosts set CTRL_JOBSERVER_TOKENS=128 in
/etc/default/ctrl-jobserver, and the script short-circuits on that
variable — the guard wraps the ENTIRE derivation, so an explicit setting
skips the memory bound rather than being clamped by it. Derived on these
hosts (nproc 128, MemTotal 125.09GiB) is min(120, 62) = 62, with the
MEMORY bound binding well below the core bound. The fleet runs 128. That
is 224GiB of admissible concurrent compile memory on a 125GiB host, about
2.06x what the jobserver's own inputs allow.
Not fixed here, deliberately: it is operator configuration on a ctrl-era
unit, gunbc has no realized knob for it (JobserverTokens is
KnobUnimplemented, and its presence is what makes interpret_host_converge
refuse the whole host), and changing build parallelism on a live fleet is
not a budget module's call. What matters here is that the compile pool
must be sized from DERIVED tokens when the placement flips — the gap
between 62 and 128 is over-admission that flip would EXPOSE, not create.
Corroboration from the same reads: srv1 held 85GiB of swap in use against
srv2's 1.3GiB, on identical hardware with identical provisioning (248GiB
across two files), consistent with srv1's compile server thrashing under
the starved cgroup gunbc_compile_pool_doc describes.
The brace escape in the quoted shell guard uses \{ per the substrate's
documented form, not a respelling around it — DESIGN records respelling as
the wrong fix for exactly this parse error.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Three review findings, all of them cases where a fact and the prose about it disagreed and the prose was load-bearing. srv4 published 7 slots while every other authority said 5. The disk cap was declared on runner_host_deploy, the "slots 06/07 must not be provisioned" caveat was a paragraph, and the roster shipped the memory verdict under a name that read as a commitment. host_memory_admitted_width and host_disk_admitted_width are now separate answers and the committed width is their minimum, so srv4 commits 5 by derivation. Fleet commits 22, not 24. The +1 conservation control moves to the memory axis, where it belongs — asserting srv4's committed width plus one fails RAM would assert something false. Session residency answered a two-valued verdict, so a counted observation and an unreachable host produced identical rows. SessionResidencyEvidence splits them into observed-present, observed-absent, operator-declared-absent and unobserved, and the verdict is projected from it rather than authored beside it. The two rows that GRANT capacity are the declared ones, and a witness now pins that they are declared rather than observed — so upgrading them without an observation reds. The width ruling note still cited the build-cache roster this PR retires (review 49415), and the residency scaffold bound to a declaration that exists, which v2.lens.disposition_redundancy reads as debt already payable. It now binds forward to the observation producer that would close it. Also carries the ci.yml / falsifier.yml regen the 14GiB per-slot cap implies: CARGO_BUILD_JOBS 4 -> 3.
gunbai-bot
Bot
changed the title
added 3 commits
August 6, 2026 08:09
The floor's extdeps scope placement gate refused this branch: five new dag/extdeps files landed enrolled in neither scope_carrier_paths nor the machinery exemption, and the frozen legacy manifest is not a landing state for anything added after the freeze. Each now declares extdeps_model_scope pointing at the upstream-defined symbol it actually models — getrusage's RUSAGE_* selector for POSIX, each implementation's own ru_maxrss unit row for Linux and Darwin, the read MIB set for Darwin sysctl, the read path set for procfs — and cites the authority anchor already present. All five join scope_carrier_paths. The subject choice is the point of the gate rather than paperwork: these five exist precisely because one Linux-only transport was standing in for a portable observation, so each has to name whose specification it speaks for. POSIX declines to fix ru_maxrss's unit and the two implementations answer differently by 1024x, which is why the unit rows are the subjects and not a shared constant. carriers_declare_scope_on_disk, frontier_rosters_are_disjoint, roster_paths_resolve_on_disk and the eight host_budget_source witnesses green by execution.
# Conflicts: # dag/gunbc/extdeps_scope_frontier.dag
The merge text-combined two generated workflows; regeneration is the only authority for them. Carries main's build-job changes (release test compile gate, feature flags, raised step caps) together with this branch's CARGO_BUILD_JOBS 3, which derives from the 14GiB per-slot cap.
Contributor
|
On the hand-authored per-host widths (review 49461) — agreed, and the finding adds something the PR body did not say. I had this listed under Not delivered as "width is validated, not solved," but I described only the over-admission direction: correcting an input turns the plan unsound. The review is right that the under-admission direction is silent. If the operator allowance shrinks, the session reservation is measured down, or the oomd floor moves, Not fixing it in this PR, deliberately. Deriving the width means The shape the follow-up wants, which the review and the earlier structural review agree on: with an unresolved load-bearing constraint producing a located refusal rather than dropping out of the minimum. One correction to my own PR body while I am here: it says affected witnesses were "green locally" at a point when that was not established — a scan directory I built ran a different witness set entirely. The 16 changed witnesses were subsequently run by name and all pass, including — sent from deep-badger-594 |
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 7, 2026
The floor's extdeps scope placement gate refused PR C: dag/extdeps/github/ actions_runner.dag landed as a new extdeps module enrolled in neither scope_carrier_paths nor the machinery exemption, and the frozen legacy manifest is not a landing state for anything added after the freeze. Subject is actions_runner_release_2_334_0 — the cited upstream release row, which is what GitHub actually publishes and what this module exists to pin. Appended to the carrier roster rather than re-sorted; re-sorting that list produced a pointless merge conflict on #7891 earlier today. carriers_declare_scope_on_disk, frontier_rosters_are_disjoint, roster_paths_resolve_on_disk and preflight_rows_counted green by execution. The other diagnostics in that run were the floor refusing to spend budget once batch 1 went red, not separate defects.
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 7, 2026
…ered residue
The floor reported three reds. Two roots, one of them not mine.
NON-FOLD RESIDUE. Three wildcard arms landed with the exact evaluator.
Two were avoidable and are now gone rather than declared: combine_evaluation
and evaluate_summation match over CostEvaluation, which has exactly two
variants, so `_ =>` became `ExactCost { value: .. } =>`. DESIGN section 5
puts construction above declaring a residue, and it buys what a roster row
cannot -- a third CostEvaluation variant would now make both matches
non-exhaustive and compile-clean would refuse, instead of the new variant
being swept into a wildcard silently.
multiply_evaluations is rostered, not "fixed". Its arms discriminate a
nested VALUE (an ExactCost carrying Zero) rather than a variant, so
enumerating would write the residual combine_evaluation call twice,
underneath the arm order that multiply_evaluations_zero_note declares
load-bearing. Duplicating that expression to satisfy a counter would make
the function more fragile. Its reason says so, rather than reusing the
generic nfr_reason_mint_era its neighbours carry.
INERT CARRIER. Not from this change. Probing inert_carrier_names_live
returned eleven live names against twelve rostered; the extra is
ProcMeminfo, whose consumer landed in #7891 -- already an ancestor of this
branch -- while the roster row stayed. origin/main carries both files
byte-identically, so this witness is red on main too. The row is deleted
here because it blocks merge and deletion is exactly what its own dissolve
trigger prescribes; reported upstream so another lane does not duplicate it.
Also records, in symbolic_product_zero_absorption_note, that the symmetry
the annihilator fix established is CLASSIFICATION and not provenance:
unknown times unknown still returns the left operand's diagnostic. That is
pre-existing and module-wide (symbolic_sequential drops the same way), and
closing it means widening UnknownCost to carry several diagnostics, which
is its own change with its own witnesses.
Green by execution: non_fold_residue_clean_holds,
non_fold_residue_no_unrostered_or_stale, inert_carrier_no_unrostered_or_stale,
and every_valuation_witness_holds over all 23 leaf witnesses -- the last
because the exhaustive-arm edits rewrote live evaluation paths, not just
roster data. Seed receipt reports unrostered=0 stale=0 live=149.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 8, 2026
…ogy authority. OPERATOR DIAGNOSIS, and it corrects mine. I had read the double count as a property of the current topology and concluded the arithmetic had merely drifted under a stable defect. Wrong on the load-bearing point: main ALREADY carries the correct rule, and #7931 reintroduced the defect locally. THE DEFECT IS A DUAL REPRESENTATION OF ONE SEMANTIC FACT — where compile RSS lives in the host's resource topology. Representation 1, the authority (gunbc.fleet_host_budget): CompilePoolInRunnerSlots => CompilePoolDerived { bytes: byte_size(0) } CompilePoolSliceDeclared => resolve_compile_pool(...) Compile memory is CONTAINED in runner-slot accounting under the current topology, so it is not a second claim on host RAM. Representation 2, the parked solver (gunbc.host_capacity_solve): per_slot_runner_pool_charge(CompilePoolInRunnerSlots) = full MemoryMax compile_pool = jobserver_build_pool_bytes_for_tokens(...) [EVERY placement] host_allocation_conserves(runner_pool: .., compile_pool: .., ..) Two additive SIBLING charges. The placement argument steers the runner-side charge but never gates whether the compile charge is added at all. A containment relation (compile RSS subset-of runner-slot RSS) flattened into a partition of disjoint siblings. The solver imports the placement and then reimplements its accounting meaning, which makes the solver a second authority over a fact fleet_host_budget already owns. WHY THE WITNESS FAILED NOW. joint_solve_double_counted_topology_refuses_seven_slots_at_derived_tokens asserts best.runner_slots < 7 — a NUMERIC CONSEQUENCE, not the invariant its name claims. At 16GiB slots, 7 x 16 = 112GiB against 125GiB usable, so the doubled charge pushed 7 over and the witness passed. At 14GiB (#7891's measured ruling, already on main) 7 x 14 = 98GiB leaves ~27GiB, so the same broken model now fits. The modeling error is unchanged; only its numerical shadow moved. Flipping the assertion to >= 7 would have been a tree-copied measurement — a change detector, which DESIGN section 5 forbids as an oracle. WHY REMOVAL RATHER THAN REPAIR. #7931 is parked, non-delivery content, and main's capacity authority already carries the correct placement-dependent decomposition, so deleting the fork restores single authority with no capability lost. Repairing in place would mean routing candidate accounting through one placement-aware charge and replacing the numeric witness with structural placement/charge controls — real work that belongs to the capacity lane, not to a consolidation. REVERTED TO MAIN, all four paths #7931's merge touched: D dag/gunbc/host_capacity_solve.dag (absent on main) D dag/test/claim/host_capacity_solve_witness_test.dag (absent on main) M dag/extdeps/jobserver.dag -> main (the _for_tokens split served only the solver) M dag/gunbc/host_layout.dag -> main (gunbc_managed_compile_pool_slice_unit had exactly one consumer, the solver; keeping it would strand an unconsumed carrier) Checked: zero dangling references to host_capacity_solve, jobserver_build_pool_bytes_for_tokens, or gunbc_managed_compile_pool_slice_unit remain in the corpus, and per_slot_runner_pool_charge is gone entirely. NOT CONFLATED WITH THIS: the live jobserver admits 128 tokens where the declared formula derives 62. That is an over-admission pointing the opposite way (too permissive) from the double count (too conservative). Untouched here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 8, 2026
* MemberChanged{from,to}: declaration-owned occurrence identity and typed replacement classification
Split MemberAction's collapsed upsert into four arms per operator ruling:
MemberAdded{to} | MemberChanged{from,to} | MemberRemoved{from} |
MemberRemovalRefused{from, cause}.
The discarded `from` was the load-bearing loss. Every safe realization of a
change consumes the prior value: an SCM ref update is a compare-and-swap that
names the expected prior (git update-ref <ref> <new> <old>), and a host resource
whose address moved needs the prior endpoint to retire. With only `to` in hand
the sole reachable realization is the unconditional write. MemberEffect splits
the same way (EffectAdd/EffectReplace{from,to}/EffectRemove) so the apply grain
can retire a prior realization instead of overwriting it blind.
gunbc.host_resource: identity is allocator-minted at declaration, never derived
from unit/path/content. HostResourceIdentity{host, occurrence} +
HostResource<R,V>{identity, role, value}, role a type parameter so a new role is
an instantiation rather than a widened central enum. This is the closed-system
answer to renames: git does not track them, it INFERS them from content
similarity, and DESIGN 4 rules a heuristic never necessary in a closed system --
a content-derived key_of is that inference wearing a bundle. Distinct carrier
from std.occurrence_identity (source-occurrence specific; one shared Int space
would let occurrence_id_eq answer true on a numeric coincidence -- the
cross-family comparison the ContentHash grounding closed). The subject-
parameterized extraction is registered as a trigger, not built under a
load-bearing module with stage0 work in flight.
gunbc.change_realization: the classification table. SCM ref -> atomic CAS;
source declaration move -> atomic SCM tree transformation; same runtime address
-> in-place update; changed host address -> staged replacement with declared
intermediates. Kills a live conflation: a .dag module re-home is an SCM tree
transformation, NOT a host migration. StagedIntermediates is head+tail so an
empty intermediate plan has no constructor, and an undeclared one refuses
(typed, located) rather than degrading to an overwrite -- the srv4 lesson (its
build-cache server died with its cgroup, never unlinked its socket, ran uncached
for weeks) made unwritable rather than warned about in prose.
A change-refusal arm was built during this work and WITHDRAWN: gunbc.ownership
defines Ensured as "requires present but does NOT own (never torn down)", a
constraint on removal, not update. It broke tool_readiness and
repo_local_git_config (whose job is re-installing drifted pins/bindings) and was
unreachable elsewhere. Per DESIGN 4c a carrier note is not evidence, so the
withdrawal is enrolled as w_ensured_member_converges_but_refuses_removal.
All three new guards verified DISCRIMINATING by planting their exact
regressions: reintroducing the change-refusal arm reds the Ensured control
alone; reintroducing the collapse reds the both-sides rows; turning the
staged-replacement refusal into an InPlaceUpdate fallback reds the srv4 row.
Caught during migration: repo_local_git_config's apply fold has a `_ => acc`
wildcard for its construction-unreachable removal arms, and MemberChanged would
have fallen into it -- silently dropping the drift that module exists to
converge. Both write arms are now explicit. live_deploy's EffectReplace is
structurally unreachable at both degenerate poles and emits a loud typed poison
per that module's discipline; its 44 byte-identity goldens pass unchanged.
Witnesses green by execution: membership_reconcile 10/10, change_realization
8/8, live_deploy 44/44, plus tool_readiness, repo_local_git_config,
workflow_reconcile, srv3, host_phase_status, roadmap_belt, host_axis_caps.
Corpus compile carries the same 10 pre-existing diagnostics as main, none mine.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Model runner connectivity recovery controller (PR B replace/repair slice).
Introduce typed RunnerConnectivityAction with incarnation replace, canary-first
fleet breaker, verified postcondition, and per-host reach refusal so wedged
acquire-job slots plan repair without watchdog fanout.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Trigger CI synchronize: #7938 opened with zero check runs (GitHub Actions webhook incident)
The PR opened during the Actions backend incident and no workflow runs were
created at all -- absent, not queued. ci.yml triggers on pull_request
[opened, synchronize, reopened, ready_for_review], so this empty commit fires
a synchronize to get the affected-set run executed against the branch.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Add repair effect choreography over shared HostEffect arms.
Project RunnerIncarnationReplace into a four-step observe-replace-observe
sequence with scaffold binds to still-ram-738's HostEffect variants; witnesses
green for replace and noop paths.
Co-authored-by: Cursor <cursoragent@cursor.com>
* PR B (add): gunbc-owned runner slot lifecycle — materialize, cap, activate, verify
Split from parked #7931 joint-solver PR per operator ruling (deep-badger-594):
this lane owns HostEffect arms, runner_lifecycle ADD sequence, slot
provision, disk observation, srv4 width-7 at allocation with apply-time
disk preflight, and fleet observation producer scaffolding.
Not included here: host_capacity_solve joint enumeration (stays on #7931).
Judgement calls in this PR body:
- runner_host_deploy / runner_slot_allocation: provisioning materialization
target (runner_count=7, disk gate at apply).
- fleet_shell_transport_observation, build_cache_endpoint_observation,
host_swap_backing, session_residency shell gate: interim observation
producers gated on transport; unsure → delivery PR.
- host_converge_slice1: under-count is postcondition for provision ADD,
not pre-refuse (count equality after RunnerSlotProvision).
Local verification: claim_batch on runner_lifecycle, runner_slot_provision,
runner_slot_allocation, host_allocation_conservation, runner_host_deploy
witnesses (pull_request checks absent repo-wide since 2026-08-06T19:36:59Z).
Co-authored-by: Cursor <cursoragent@cursor.com>
* Joint runner_slots × build_tokens capacity solve (srv3 compile-pool flip)
Parked off capacity-delivery critical path per operator ruling — NOT
presented as progress toward gunbc apply / seven runners. Lifecycle,
HostEffect arms, and provisioning live on session/still-ram-738-pr-b.
This PR contains only host_capacity_solve + witness and the jobserver
helper split needed for per-token pool sizing in the enumeration.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Fix shell transport fallback and slot ownership grounding (review 49707)
Keep producer-Unobserved as Unobserved with dated receipts as provenance
only, not authoritative ReachRefused. Refuse fabricated Owned on observed
slot dirs until systemd drop-in provenance lands (ownership_of Absent).
Co-authored-by: Cursor <cursoragent@cursor.com>
* PR C: wire mode=apply to runner_capacity_realize (last mile)
Connects gunbc.apply mode=apply to runner_capacity_plan + disk
preflight + ADD dispatch seam (depends on #7939 plan, #7946 effects).
Witnesses: two additions not count-refusal, disk unobservable refuses
(not width-5 fallback), replay no-op when observed satisfies request.
Local claim_batch: 3/3 PASS on runner_capacity_realize_witness_test.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Fix review 49712: resolvable witness imports and citation targets.
Import hardware_thread_count_value so the tokens-cap refusal witness resolves;
author srv3_non_compile_residency_observed as a scaffold producer so the dissolve
DeclarationRef cites a live symbol; ground slice_unit via host_layout.gunbc_managed_compile_pool_slice_unit.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Fix session-present fail-open on live capacity admission (review 49722)
Only SessionsObservedAbsent maps to CapacityEvidenceObserved; observed
session presence caps at candidate-only with an explicit reason. Add
srv1_session_present_live_capacity_is_candidate_only witness.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Port incident broker-progress watchdog into gunbc recovery model.
Models the conjunction predicate (remote offline + broker silence + no worker + grace elapsed), evidence grades, re-read refusal, and derived 10-minute bound with discriminating witnesses wired into runner_connectivity_recovery.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Enroll extdeps.github.actions_runner as a scope carrier
The floor's extdeps scope placement gate refused PR C: dag/extdeps/github/
actions_runner.dag landed as a new extdeps module enrolled in neither
scope_carrier_paths nor the machinery exemption, and the frozen legacy
manifest is not a landing state for anything added after the freeze.
Subject is actions_runner_release_2_334_0 — the cited upstream release row,
which is what GitHub actually publishes and what this module exists to pin.
Appended to the carrier roster rather than re-sorted; re-sorting that list
produced a pointless merge conflict on #7891 earlier today.
carriers_declare_scope_on_disk, frontier_rosters_are_disjoint,
roster_paths_resolve_on_disk and preflight_rows_counted green by execution.
The other diagnostics in that run were the floor refusing to spend budget
once batch 1 went red, not separate defects.
* Fix PR C compile-clean failures and land converged-seven replay no-op.
Add missing HostEffect match arms in fleet_converge_cli, fix lifecycle
witness construction (no bare _ values), and model post-convergence width
via converged-seven roster fixture so a second apply plans zero additions
and succeeds without disk preflight when nothing remains to materialize.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Close PR B fanout and re-read gaps against operator watchdog ruling.
Add fleet plan builder with per-host replacement cap, five-step repair choreography (observe before mutate), SIGPIPE diagnostic-read refusal, and reobservation witnesses.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Fix reserved-keyword binder and delete a tautological witness
'release' is a reserved word; using it as a match binder made
runner_lifecycle_witness_test.dag unparseable, which killed regen and
heal before they did any work and left ci reporting FloorUpstreamAlreadyRed.
All three red jobs had this one cause.
Underneath it, witness_runner_lifecycle_host_effects_declared constructed
each HostEffect variant and matched it straight back. That establishes only
that the constructor typechecks -- already the typechecker's guarantee -- and
cannot go red on any behavioral defect. The compiler refused each single-arm
match as non-exhaustive over the 31-variant coproduct; answering that with
thirty '=> false' arms would make the tautology compile without making it a
check. Deleted, with its now-dead imports. fleet_converge_cli already carries
the claim by execution: it matches HostEffect exhaustively and fails to
compile if an arm goes missing.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Ground ReplaceRunnerIncarnation on from/cause and fix witness parse.
ReplaceRunnerIncarnation now carries LocalRunnerSlotIncarnation plus
RunnerReplacementCause so repair plans can refuse stale incarnations and
name why replacement fired; witness binding renamed from release to cited
to avoid the reserved keyword that broke regen.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Name lifecycle realizer scaffold dissolution and retitle PR C honestly.
Add runner_lifecycle_realize_wet_transport_dissolve_on (srv3/srv4 SSH
reach + HostEffectTransport) and cite it from every NotConverged arm;
update runner_capacity_realize authority note to state apply does not
provision until the scaffold retires.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Land Step A: incarnation type-home, in-band admission, seam witnesses.
Move LocalRunnerSlotIncarnation to gunbc.runner_incarnation, add ReplaceRunnerIncarnation seam witnesses, and model in-band ADD admission (LocalShell + derived execution target; Step E void). Capture operator constraints: workflow-only application, srv1 row-6 control, unit/process width authority, imperative caps, and ctrl installer read-before-realize.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Model SlotMaterializedNotActivated and retire residue framing.
srv1 probe shows complete dormant install trees without .runner until JIT start. Add three-state installation carrier and witnesses; correct width notes. srv3/srv4 slot-06/07 state still unobserved from this session.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Refine slot state: stale .runner is history, ADD needs no replace.
Collapse materialized-never-activated and materialized-previously-activated into SlotMaterializedNotActive; unit_active drives readiness. Record srv3 06/07/08 probe, srv3 reach via srv2 jump, and width-8 vs intent-7 ceiling.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Add installation observation wrapper; pin vivid-eagle srv3 data.
RunnerSlotInstallationObservation separates observed states from Unobserved/ReachRefused so srv4 never defaults to SlotAbsent. Pin srv3 01-08 mapping from sibling probe; witnesses enforce srv4 blocks add without extract routing.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Fix PR #7947 CI witnesses: roster wiring, pinned incident width, nfr rows.
Restore srv3 shell transport session receipt for producer-unobserved authority, pin incident desired_width at 22, pass roster into connectivity repair planning, and enroll connectivity verdict predicates in the non-fold-residue roster.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Align CI fixes with deep-badger guidance: observe srv3, derive incident width.
Wire vivid-eagle srv3 shell transport as producer-observed success while srv4 stays unobserved with dated receipt provenance; derive incident desired_width=22 from srv4's five-slot outage pin instead of a naked literal.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Add owned CI control plane v0: poll-first queue, executor, Checks projection.
Introduces medium-neutral CiExecutionPlan carriers from ci_spec (not ci.yml), a poll-first ci_control_plane daemon with durable queue and lease reclaim, GitHub Checks create/update, and /ci serve routes for run receipts.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Address review 49764: authority projection, reconcile ordering, scaffold marker.
Load repo/stages/floor plan from gunbc.owned_ci_seed via eval; persist ledger before check create; mark CheckPublicationPending on API failure without duplicate enqueue; document seed REST transport as dissolve-on scaffold.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Address review 49792: typed durations, seed authority, publication honesty.
Ground lease duration on std.measure.Second and queue expiry on NumericDate;
load state root and lease seconds from gunbc.owned_ci_seed in the Rust bin;
fix unpublished-completed conclusion mapping and UpdateRun wire encoding;
dissolve ci_subject_is_fork_refused Bool predicate into direct coproduct match.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Clean up ci_control_plane per review 49812 non-blocking notes.
Drop dead failed/completed ternary on queue move (always completed dir);
remove tautological Rust unit tests — decision procedure stays in .dag witnesses.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Address review 49829: fail-closed clock and fork refusal receipts.
Propagate system-clock errors from now_unix instead of fabricating 0;
persist fork PR refusals to index/run ledger so the /ci UI can observe them.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Address review 49838: refuse fractional queue lease clocks.
Replace Bool lease expiry with typed reclaim/validity decisions that
carry LeaseClockRefused for fractional NumericDate arms; witness the refusal.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Address review 49852: remove poll bypass, enroll token refusal witness.
Delete undocumented OWNED_CI_POLL_MAIN_ONLY escape hatch; model PR poll
GitHub-read admission in owned_ci.dag with witness_poll_without_github_read_refuses;
route Rust refusal strings through owned_ci_seed.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Address review 49866: optional head SHA for refused subjects.
ci_subject_head_sha returns CommitSha? with Absent for ForkPullRequestRefused
instead of empty-string sentinel; witness enrolled in bundle.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Address review 49870: dry-run leaves queue pending, dedupe checks.
Skip claim/lease in --dry-run (peek-only log); route publication success
through check_conclusion_is_success; delete unused CiRunStage* types.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Register ci_control_plane in self-host frontier for regen parity.
Seed-retained intrinsic was missing from frontier and stage0 crate layout,
so regen_verify stripped pub mod ci_control_plane from lib.rs and CI regen failed.
Alphabetical ci_control_plane before cli_run matches rustfmt and frontier order.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Address review 49929: paginate open PR discovery, honest publication causes.
Follow GitHub Link rel=next with per_page=100 and refuse when pagination
cannot complete; pass through actual check-update errors at completion instead
of a canned API-unavailable string.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Address review 49931: PR-only token admission, refuse malformed PR payloads.
Missing or empty GITHUB_TOKEN refuses PR discovery only; main mirror subjects
still reconcile. Malformed open-PR API rows fail closed with a typed cause
recorded in the subject ledger instead of silent continue.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Address review 49950: refuse unsafe run_id before filesystem read.
Model owned_ci_run_id_admits in .dag (path_segment_is_safe plus {unix}-{8hex}
grammar), gate serve_ci_run_detail_response, mirror validation in the seed
reader, and harden write_json_atomic with pid-scoped tmp files plus parent fsync.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Fix CI compile-clean: break owned_ci_serve import cycle.
Remove dead page_render_refusal_body import from roadmap_static_site and
stop importing gunbc.roadmap_serve (cycle through roadmap_serve_witness).
Inline owned_ci_serve_text/page_response helpers locally instead.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Filter open PR discovery to merge-target branch (v0 scope).
Poll path compares GitHub base.ref to gunbc_default_branch_name from seed authority; non-main same-repo PRs are ledger-recorded refusals (not enqueued). Adds ci_pull_request_targets_merge_branch, witness, and Rust unit tests.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Route merge-target branch through repo_identity everywhere.
ci_subject_identity_key, mirror fetch, and push-subject discovery use gunbc_default_branch_name via seed authority instead of hardcoded "main".
Co-authored-by: Cursor <cursoragent@cursor.com>
* Retry CI after sccache EAGAIN on build job (infra flake).
Prior run 31155607568: v1-compiler compiled; v1-compiler-tests failed spawning rustc via sccache (os error 11). No code change.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Honor dry-run GitHub boundary and add operator-rerun enqueue.
dry_run skips GitHub REST PR poll (mirror-only discovery); --enqueue-rerun-sha realizes v0 OperatorRerun with rerun:<sha> keys. Witnesses and design doc updated.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Split owned-ci serve file reads into Present/Empty/Missing.
owned_ci_classify_filesystem_text uses Filesystem.Read success vs empty content instead of conflating missing and empty into Optional Absent.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Fix owned-ci .dag strings that parsed as template variables.
Replace curly-brace grammar placeholders in prose with angle brackets so compile-clean does not treat run_id/unix_seconds as undefined bindings.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Fail-closed on missing head.repo.full_name in PR poll.
Malformed pull payloads refuse at poll boundary instead of defaulting to empty and mislabeling as fork refusal; unit test added.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Refuse silent no-ops on index and queue state drift.
update_index_row and move_queue_file return typed errors when the expected row or queue file is absent instead of succeeding unchanged.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Document state-carrier dissolve-on in owned-ci seed scaffold.
Extend owned_ci_control_plane_seed_note to name JSON↔.dag coproduct unification and key-grammar eval alongside the REST bridge; register poll_interval Rust-only debt.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Align queue refused state and per-run summary receipts.
Add QueueRefused to CiRunQueueState with witness; key target summary receipts by run_id under target/owned-ci-run-receipts/.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Register owned-ci-control-plane design doc in doc graph.
The v0 design note was added on this branch without a HandAuthoredDocBind,
so doc_reachability flagged it as an orphan on the discovery-corpus floor.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Fix review 50233: wire watchdog inputs and reobservation into plan path.
RunnerSlotConnectivitySnapshot now carries broker/worker/grace; plan and decide_for_snapshot read them instead of fabricating wedged inputs. reobservation_refuses_mutation gates replace before actuation; two new witnesses cover offline-alone refusal and stale decision receipt.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Address review 50232: Terminal disposition on total-match predicate families.
NFR rows would stale the roster — these helpers are exhaustive matches without top-level wildcard arms (unlike connectivity_verdict_is_*). Document predicate-dissolution at authoring via explicit Terminal disposition rows.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Import RunnerSlotIdentity in runner_incarnation (review 50320).
The type is referenced twice in this module and was resolving only by pool
coincidence — the Class B binding failure the corpus already tracks. Picked up
from session/still-ram-738-pr-c commit 5df7f02, which fixed the same review
finding on the now-superseded branch.
That commit's other half — a stray brace in non_fold_residue_frontier — does
not apply here: it came from that branch's own conflict resolution, and this
branch's roster resolution did not produce one (checked, the list closes clean).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Re-vocabulary runner_slot_provision onto the MemberChanged{from,to} surface.
CI ci job red: 'Refused' not found in module 'gunbc.membership_reconcile'
(imported by 'gunbc.runner_slot_provision'), 3 occurrences. A genuine fold
defect, not a flake and not memory (floor peak 9.85 GB against memory.max
17179869184 = 57%, so the cap was not reached).
CAUSE: runner_slot_provision came from #7947 and was written against the
pre-rework membership_reconcile surface (MemberUpsert / MemberTeardown /
MemberTeardownRefused / membership_upsert_count). The fold also brought in
#7938's MemberChanged{from,to} rework of that module, which splits the old
fused upsert into distinct MemberAdded and MemberChanged arms. Neither PR
was wrong alone; consolidating them created the mismatch.
NOT A MECHANICAL RENAME. The old MemberUpsert fused add and change, and the
operator's Decision 1 split them deliberately, so each site is a decision:
- MemberAdded -> emit the slot extract script. This is the add path.
- MemberChanged -> []. Decision 2 says apply may execute RunnerSlotAdd only
and must refuse Change/Remove/IncarnationReplace; emitting an extract
script for a changed member would materialize a change the apply path is
required to refuse.
- MemberRemoved / MemberRemovalRefused -> [], unchanged in meaning.
- membership_upsert_count -> membership_added_count, NOT the derived
membership_write_count (= adds + changes). The consumer is
runner_slot_provision_has_width_increase: a width INCREASE is adds; counting
changes would overcount. membership_write_count exists for consumers that
want both, and this is not one.
The witness carried the same stale vocabulary and is migrated with it; its
assertion is preserved exactly (7 desired - 2 observed = 5, and the 2 observed
match desired so they are Unchanged, not Changed).
VERIFICATION, stated at its real strength. A local single-entry run does NOT
verify this: a stashed-fix control returns the IDENTICAL 2000 errors and zero
'Refused' reports on the pre-fix tree, so that instrument never surfaces this
defect class -- it dies at parse before resolution, and 2000 is a truncation
cap rather than a count. Verified instead at symbol grain: all 7 symbols
imported from membership_reconcile resolve to declarations, with a positive
control confirming the query reports the two removed names as MISSING. CI's ci
job is the instrument that found this and is the one that settles it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Add the check-publication predicate-family disposition (review 50389).
REQUEST_CHANGES verified against current code rather than taken on trust, and
the finding is correct: gunbc.owned_ci check_publication_reports_github_success
and check_publication_is_pending_honest are coproduct is_*/reports_* predicates
carrying no disposition, while this same diff already dispositions two sibling
families — extdeps.github.ci_runner github_runner_registration_predicate_family_disposition
(review 50232) and gunbc.runner_incarnation runner_slot_installation_predicate_family_disposition.
Inconsistent within one PR is the reviewer's point and it stands.
Adds check_publication_predicate_family_disposition = Terminal, matching the
runner_incarnation precedent's shape and reason.
TOTALITY CHECKED, NOT ASSERTED. The row claims both matches are total, so that
claim is measured: CheckPublicationState has six variants (NotStarted, Queued,
InProgress, Completed, Pending, Failed) and both fns carry an explicit arm for
all six with zero top-level wildcard arms. Positive control: the same query
reports a fictitious variant as missing, so an all-present result is a real
negative rather than a blind read. (First pass counted the type name itself as
a seventh variant and reported a false miss — the query was wrong, the code was
not.)
Terminal rather than NFR enrollment is the right arm for the same reason the
precedent gives: these dissolve at authoring, so an NFR row would stale the
roster. fleet_runner_connectivity connectivity_verdict_is_* is the contrasting
case — wildcard false arms, correctly enrolled in non_fold_residue_frontier.
Scope checked: exactly two Bool fns in gunbc.owned_ci match over a coproduct,
and both are fixed. owned_ci_run_id_char_is_digit / _is_hex take String, not a
coproduct. check_conclusion_is_success lives in extdeps.github.checks, outside
this diff.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Drop #7931's parked capacity solver: it forked the compile-pool topology authority.
OPERATOR DIAGNOSIS, and it corrects mine. I had read the double count as a
property of the current topology and concluded the arithmetic had merely drifted
under a stable defect. Wrong on the load-bearing point: main ALREADY carries the
correct rule, and #7931 reintroduced the defect locally.
THE DEFECT IS A DUAL REPRESENTATION OF ONE SEMANTIC FACT — where compile RSS
lives in the host's resource topology.
Representation 1, the authority (gunbc.fleet_host_budget):
CompilePoolInRunnerSlots => CompilePoolDerived { bytes: byte_size(0) }
CompilePoolSliceDeclared => resolve_compile_pool(...)
Compile memory is CONTAINED in runner-slot accounting under the current
topology, so it is not a second claim on host RAM.
Representation 2, the parked solver (gunbc.host_capacity_solve):
per_slot_runner_pool_charge(CompilePoolInRunnerSlots) = full MemoryMax
compile_pool = jobserver_build_pool_bytes_for_tokens(...) [EVERY placement]
host_allocation_conserves(runner_pool: .., compile_pool: .., ..)
Two additive SIBLING charges. The placement argument steers the runner-side
charge but never gates whether the compile charge is added at all.
A containment relation (compile RSS subset-of runner-slot RSS) flattened into a
partition of disjoint siblings. The solver imports the placement and then
reimplements its accounting meaning, which makes the solver a second authority
over a fact fleet_host_budget already owns.
WHY THE WITNESS FAILED NOW. joint_solve_double_counted_topology_refuses_seven_slots_at_derived_tokens
asserts best.runner_slots < 7 — a NUMERIC CONSEQUENCE, not the invariant its name
claims. At 16GiB slots, 7 x 16 = 112GiB against 125GiB usable, so the doubled
charge pushed 7 over and the witness passed. At 14GiB (#7891's measured ruling,
already on main) 7 x 14 = 98GiB leaves ~27GiB, so the same broken model now fits.
The modeling error is unchanged; only its numerical shadow moved. Flipping the
assertion to >= 7 would have been a tree-copied measurement — a change detector,
which DESIGN section 5 forbids as an oracle.
WHY REMOVAL RATHER THAN REPAIR. #7931 is parked, non-delivery content, and main's
capacity authority already carries the correct placement-dependent decomposition,
so deleting the fork restores single authority with no capability lost. Repairing
in place would mean routing candidate accounting through one placement-aware
charge and replacing the numeric witness with structural placement/charge
controls — real work that belongs to the capacity lane, not to a consolidation.
REVERTED TO MAIN, all four paths #7931's merge touched:
D dag/gunbc/host_capacity_solve.dag (absent on main)
D dag/test/claim/host_capacity_solve_witness_test.dag (absent on main)
M dag/extdeps/jobserver.dag -> main (the _for_tokens split served only the solver)
M dag/gunbc/host_layout.dag -> main (gunbc_managed_compile_pool_slice_unit had
exactly one consumer, the solver; keeping it would
strand an unconsumed carrier)
Checked: zero dangling references to host_capacity_solve,
jobserver_build_pool_bytes_for_tokens, or gunbc_managed_compile_pool_slice_unit
remain in the corpus, and per_slot_runner_pool_charge is gone entirely.
NOT CONFLATED WITH THIS: the live jobserver admits 128 tokens where the declared
formula derives 62. That is an over-admission pointing the opposite way (too
permissive) from the double count (too conservative). Untouched here.
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>
Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 8, 2026
…ries #8010's witness retirement) (#8027) * WIP: cost analysis * Execute the name-key precondition C0(b2)'s join was assuming classification_matches_fact joins a roster row to a DeclFact on BARE NAME, while DeclFact carries qualified_name and kind and could key exactly. That is sound only while every top-level declaration of v1.compiler.complexity has a distinct name, and nothing in the carrier makes that true -- it is a property of the subject module, not a wall this carrier erects. Measured over src/v1/complexity.dag: 201 top-level declarations (171 fn, 26 type, 4 data, 0 let), zero duplicate names. So the join is correct today. But a measurement of the current tree is not an oracle (DESIGN section 5), so the precondition is now EXECUTED rather than assumed. The gap this closes is real and none of the four existing totality witnesses covers it: a duplicate name in the DERIVED population still classifies, still matches a roster row, and leaves no stale row, so one roster row can silently answer for two declarations while every count agrees. roster_names_distinct does not cover it either -- it constrains the AUTHORED side only, and the duplicate here would be on the derived side. Added population_names_distinct beside the existing roster_names_distinct, reusing name_already_seen rather than minting a second distinctness fold. Green by execution, all three run through claim_batch against the real tree: PASS w_population_decl_names_are_distinct (live population) PASS w_distinctness_fold_reds_on_a_planted_duplicate (discriminating RED) PASS w_distinctness_fold_accepts_a_distinct_control (positive control) The RED matters: a distinctness fold that cannot fail proves nothing, so a planted same-name pair must come back false or the live green is empty. Dissolve-on is named on the carrier: the roster carrying exact DeclFact identity (qualified_name, or name plus kind) makes the join exact by construction and retires the precondition. That is a 201-row re-authoring and is deliberately not bundled here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Sweep the stale-status class across the whole plan, not the one line I fixed (review 49289) Review 49289 caught three more instances of exactly the defect this PR exists to remove, and it was right: I corrected one occurrence and did not sweep for the class -- the same shortcut I would send back on someone else's diff. Fixed, all verified against main rather than recalled: section 7 C0(c) bullet still called the split "the next implementation slice" while the C0 summary said DELIVERED section 9 operator ruling same, so a reader of section 9 could still treat C0(c) as open section 2 table still listed a single lens_contract_complexity row carrying RatchetForever. That row does not exist on main. Replaced with the two rows that do -- derived_kernel (WallAfterGrounding) and optimality (RatchetForever, the genuinely undecidable residue) Two the review did not name, found by sweeping for the class instead of the reported lines: section 4 asserted in the present tense that lens_contract_complexity carries RatchetForever. Marked RESOLVED by #7841 and kept as the argument the split rests on, rather than deleted -- the reasoning is why the split has the shape it has section 8 a discriminating control named the deleted contract. Re-pointed at both split rows, where the mode/consumer disagreement is actually checkable status blockquote said one carrier "currently" declares it permanent Remaining bare mentions at lines 119, 143 and 147 are deliberate historical references ("the mixed row", "as written then") describing the pre-split state in explicitly past tense, not live claims about the tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix the dissolution trigger: it named a deleted row and set an unsatisfiable condition (review 49307) Third catch of the same class, and this one was more than a stale name -- the retirement criteria were unsatisfiable as written. Clause 1 required that "lens_contract_complexity's boundary class distinguishes the genuinely undecidable residue from the decidable capability". That is precisely what #7841 delivered, so the clause is SATISFIED and now says so, naming the two rows that replaced the mixed one. Clause 2 required that "lens_contract_complexity has a live consumer witness and has flipped off AuditOnly". Read onto the split, that can never be true. lens_contract_complexity_optimality is RatchetForever and stays permanently AuditOnly by the plan's own section 7 C0(c) ruling -- so a retirement condition demanding it flip would make this doc unretirable BY CONSTRUCTION. Re-scoped to lens_contract_complexity_derived_kernel, which is the half that can legitimately flip, and the clause now states explicitly why optimality is excluded so nobody re-adds it later. That second half is the part worth noticing: a dissolution trigger that cannot fire is a scaffold with no exit, which is the failure DESIGN section 6 asks a named trigger to prevent. The stale name would have been cosmetic; the unsatisfiable condition was not. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: cost analysis * Remove merge-event status prose from the plan; cite carrier symbols instead Reviews caught this plan stale in four separate places, each claim true when written and false a day later. The common shape was a merge-event assertion -- "DELIVERED ON MERGE of #7841", "both rows are on main" -- which rots without anyone touching it, because nothing in the tree can decide it. Replace the class, not the four lines. Every delivery claim now names the carrier SYMBOL a reader can resolve (DESIGN section 3, cite-the-symbol), so it is decidable by grep rather than by remembering which PR merged when. Verified: all seven cited symbols resolve; zero PR numbers and zero merge-event phrases remain in the carrier. Also fixes a real dangling reference the C0(c) split created: the census note in gunbc.v1_complexity_capability_census cited lens_contract_complexity, a row that no longer exists. Re-pointed at lens_contract_complexity_derived_kernel, which is the one a consumer surface would actually move -- optimality is AuditOnly permanently. * chore: regenerate drifted generated artifacts (ci auto-heal) * WIP: cost analysis * Stop the witness-admission row scan slicing UTF-8 prose mid-character The floor worker died exit 101 with no terminal receipt on witness_admission_entry_function_keys_from_source: WINDOW is a 400-BYTE budget applied to UTF-8 prose via after.len().min(WINDOW), so whenever byte 400 lands inside a multi-byte char the slice panics and takes the whole run down. The row that exposed it simply happened to put an em dash across that offset. Every other slice in that function takes its offset from find/split_once, which return char boundaries; this fixed offset was the only unguarded one. It now walks down to the nearest boundary, so an over-long row is truncated rather than fatal. Note the comment directly above already recorded an earlier panic in this same function, so the failure mode has form. Fixing the string instead of the scanner was the tempting move and it is the unmarked workaround DESIGN section 5 forbids: it would leave the defect armed for the next author who writes prose with an em dash in it. So the em dash stays in the row, and the scanner is what changed. PROVEN DISCRIMINATING BY EXECUTION, both directions: - unfixed: panics "byte index 400 is not a char boundary; it is inside em dash (bytes 398..401)" -- the production failure reproduced exactly - fixed: passes The fixture puts entry: and function: FIRST, mirroring real rows, because the scanner deliberately panics when entry: falls outside the window and that refusal is correct behaviour rather than the bug under test -- an earlier draft of this fixture tripped that arm and would have tested the wrong thing. The prose is a run of em dashes shifted by 0/1/2 ASCII bytes, covering every residue class mod 3, so at least one iteration is GUARANTEED to put the window edge strictly inside a character. The test deliberately does not model where the scanner sets search_from; pinning that offset would make the fixture fail for the wrong reason the moment the scanner moves. * Lane A C1: evaluate CostExpr at concrete SizeVariable bindings, with the CostSum binder lexically scoped The subject is semantic work, not hardware time: a CostExpr plus concrete bindings yields exact, unresolved, or refused modelled work. No duration, rate, or calibration constant enters this module. The load-bearing part is binder handling. v2.lens.cost.expr normalize_cost_expr_to_symbolic matches CostSum with the binder discarded, so a binder-dependent body projects a SymbolicCost naming a variable that is bound inside the sum - the magnitude may survive, the variable identity does not. This evaluator does not inherit that: env_bind prepends and lookup_bindings answers the head-most match, so a binder shadows an outer binding of the same identity for the extent of its body and only for that extent, with removal on exit structural rather than an unbind step. Proven by execution against a binder-discarding mutation: pinning the binder to Zero reds binder_dependent_body_is_summed_not_treated_as_invariant and binder_shadowing_is_scoped_and_removed_on_exit while leaving the invariant-body and zero-iteration witnesses green - which is the exact signature of the defect, and is why the existing C1 fixture (same variable for binder and bound) cannot see it. A second mutation answering zero for an unbound variable reds both missing-binding witnesses while zero_iterations_produce_exact_zero stays green: that pairing is what keeps a zero in a cost report unambiguous between nothing to do and nothing modelled. Carriers: v2.lens.cost.valuation CostEvaluation, CostValuationBinding, evaluate_cost_expr, evaluate_cost_expr_partially; std.algebra FreeSemigroup with v2.std.algebra non_empty_singleton / non_empty_append. The nonempty arms are carried by std.algebra FreeSemigroup - the free semigroup over T exactly as FreeMonoid is the free monoid over T, one algebraic axis at two identities. Its head field is the construction wall: an UnresolvedCost naming no free variable and a refusal carrying no cause have no representation, rather than being validated against. It is deliberately not the Refined<List<T>> spelling of the manual fixture, whose refinement predicate concedes the empty state is writable, and the NonEmptyList alias is withheld until that fixture retires so one name never resolves to two declarations. NonEmptyDiagnostics, FiniteSet, NonEmptySymbolChain and NonEmptyGrammarChoiceAmbiguityRows are the same shape monomorphised and dissolve onto it at their own already-declared triggers; that corpus-wide de-fork is not carried here. Stated gaps rather than silent ones: BoundedCost is declared-not-produced because its seed is a ceiling-valued binding, which is the sibling discrete-cost note's envelope scope; CostLog refuses its magnitude through the expression authority's own vocabulary until a cited integer-logarithm authority exists on std.nat. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address review 49620 and the parent lane review: interval arithmetic, claim totality, quadratic accumulation, and a false citation Bounded-upper CostSum answered an EXACT value. combine_evaluation of ExactCost 3 and ExactCost 7 under nat_max reaches combine_known with both endpoints at 3, so bounded_or_exact collapses to ExactCost 7 — an exactness claim manufactured from an inexact input, sitting exactly where the envelope lane plugs its seed in. Replaced with evaluation_interval, which pairs the LOWER of one evaluation with the UPPER of a different one; an inverted interval refuses with InvertedCostInterval rather than being normalised by swapping the endpoints. Witnessed at its own seam because the arm has no producer yet; restoring the max spelling reds three of the four new witnesses. The PR body claim that the envelope lane adds a seed and no arithmetic was therefore false and is retracted. The Tier1 claim conjunction ran three of thirteen witnesses while its label asserted the refusal and scoping behaviour the other ten established, so CI could go green with the label false. every_valuation_witness_holds now enumerates every test fn in the file. Refusal accumulation was quadratic and reachable today: non_empty_append is linear in its left argument, so a body refusing under upper = u built u causes left-nested — and CostEffect refuses unconditionally in this slice. The causes were also IDENTICAL, because the body expression is fixed and only the binder value changes, so this amplified one deficit u times rather than counting u deficits. evaluate_summation now stops evaluating the body once the accumulator has settled; the soundness argument (a refusal here is a property of the body expression, not the binder's value) and its dissolve-on are on the carrier, and the new one-cause witness reds when the skip is removed. The FreeSemigroup grounding note carried a false citation, in the note arguing for single authority. Of the four carriers it named as each already carrying a migrate_when_nonempty_list_refinement_promoted trigger, grep says only two do, and a fifth instance was omitted. Corrected to five carriers, two triggered. Both surviving triggers are RETARGETED onto FreeSemigroup: they named the event as promoting the manual refinement to std, and this change decided that promotion is not the mechanism, so they would have been left waiting on an event that cannot occur as spelled. Also: the partial evaluation mode is stated as not being an escape from a refusal (swapping entry points to silence one is the author-side absorbing fallback); the order note now says causes accumulate WITHIN an arm and the dominated side's payload is dropped ACROSS arms; and the projection-path binder discard in normalize_cost_expr_to_symbolic is named as tracked debt with its trigger and the reason the existing fixture cannot see it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Trigger the pull_request ci workflow, which never fired for this branch Zero GitHub Actions runs were created for either pushed SHA over roughly an hour, while sibling branches got ci runs throughout that window; the run was not awaiting approval either. main protection requires the ci check, so an empty synchronize is the only way to get one. Two approvals on the previous head are re-earned rather than assumed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Recut to the exact core; fix the log arm reporting the wrong cause Operator ruling: scope to complete exact valuation. Kept — exact valuation at a complete binding set, CostSum binder scoping and shadowing, duplicate refusal, effect refusal, log refusal, and the earned-zero versus fabricated-zero distinction. Held on session/deep-owl-215-partial-bounded-hold — partial evaluation and bounded evaluation, sequenced rather than rejected, with both constraints that ride with them recorded on the carrier so they cannot be quietly undone: complete and partial stay TWO ENTRY POINTS over one fold, and the unresolved state must carry the residual CostExpr, not just free-variable names. CostEvaluation is two states here because at the exact core there are exactly two honest answers: the work is this number, or here is why it cannot be. Declaring an arm with no producer is rung inflation — and the bounded arm in particular was carried through an earlier revision while its arithmetic silently collapsed a two-endpoint envelope to its own ceiling. The log arm reported the wrong cause. It matched CostLog { base: _, .. }, ignored the base entirely, and answered UngroundedLogArgument for every non-refusing case — so base 0 read as an ARGUMENT problem, and a fully grounded argument was called UNGROUNDED, while v2.lens.cost.expr's normalizer right beside it already checked the base against its own InvalidLogBase. Two paths disagreeing about one fact. Now three distinct causes for three unrelated failures: an invalid base refuses through the expression authority's InvalidLogBase (cited, not re-minted), an unbound argument refuses as MissingSizeBinding like any other unbound size, and a valid base with an exact argument refuses as IntegerLogarithmUnavailable, which names the real gap and is countable against it. Restoring the base-ignoring arm reds both invalid-base witnesses; the base-zero and grounded-argument pair is the discriminating one, since the old arm gave both the same cause. All 16 witnesses green by execution, all 16 enrolled in the claim conjunction. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Enroll the claim conjunction as a test fn: it was the one orphan the naming-hygiene gate found The enroll-or-refuse pre-plan walk refused v2.test.lens_cost.valuation every_valuation_witness_holds as a plain fn unreachable from every test fn and test data — silent de-enrollment. It is the single root of the run: the ci job's failure was FloorUpstreamAlreadyRed with build=success and heal=success, which adds no verdict of its own. Note the remedy that does NOT work, since it is the obvious one: the claim data already referenced the helper by name — that is what it exists for — and a plain `data` does not count as reachability for this gate. Promotion to `test fn` is what satisfies it. Worth naming the shape rather than just fixing it: the conjunction was factored out to close review 49620's finding that the claim enumerated three of thirteen witnesses, and the helper that fixed a specification-without-execution defect was itself not executed by anything the gate recognises. Same class, one level out. The totality note now says so, so the next reader sees why the enrollment is deliberate rather than incidental. 17 witnesses green by execution; the local pre-plan walk that produced the CI refusal now completes clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Regenerate the stage0 seed: adding FreeSemigroup to a std authority drifted the self-host fixed-point regen_verify_gate_passes returned false because src/v1/stage0/src/std_algebra.rs did not contain the FreeSemigroup the emitter now produces from dag/std/algebra.dag. Adding a type to a std authority without regenerating the committed emitter output is exactly what the fixed-point gate exists to catch. Regenerated with regen_stage0 rather than hand-edited — the file is emitter output, and a hand-added struct would pass the diff while making the seed diverge from its authority. The diff is 7 lines, additive, only the struct. Order mattered: regenerate, rebuild the seed binaries from the regenerated sources, then verify with those binaries — regen_divergence_count=0, and 17 witnesses green against the rebuilt seed. The ci job's failure was again FloorUpstreamAlreadyRed with build and heal green, so regen was the only real signal. Note on the emitted shape, since it is visible in the diff: FreeSemigroup carries a _phantom: PhantomData<T> beside an already-inhabited T. That is the emitter's established convention for generic structs here, not something this type triggered — 25 of 39 structs in this one file carry it, including Magma<T> and the FieldOfFractions<R> pair DESIGN names as correctly grounded. There are zero construction sites for it in emitted Rust, so it imposes nothing on call sites. Whether the convention is a defect is a corpus-wide emitter question, not this PR's. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Zero is a two-sided annihilator: fix CostMul and symbolic_product together CostMul routed both sides through the generic refusal-dominates combiner, so CostMul of zero and CostEffect refused while the symbolic authority answered zero for the same expression — two paths disagreeing about one CostExpr, and the exact evaluator was the wrong one: a zero multiplicity means the body is never executed, so refusing because an unexecuted factor lacks an effect model is the did-no-work versus could-not-model conflation the earned-zero controls exist to prevent. Fixing only that would have traded one divergence for a narrower one, because the reference was itself ASYMMETRIC: symbolic_product matched a's arms first, including UnknownCost, and only then inspected b — so zero times unknown absorbed while unknown times ZERO returned unknown. Multiplication is commutative, so an operand order that changes the answer is a defect, not a style. Both paths are fixed in one motion and now agree in both orders. The annihilator lives in a multiplication-specific function and beats refusal-dominance, which governs every other combination here. That ordering is load-bearing and the carrier says so: checking refusals first reads like tightening a fail-closed path and would silently restore the defect, with only the two zero-times-effect witnesses reding. Controls, both directions on both properties, because an asymmetry defect cannot be caught by an asymmetric test: zero times unknown and unknown times zero both absorb; one times unknown and unknown times one both stay unknown; zero times CostEffect and CostEffect times zero are both ExactCost zero; one times CostEffect still refuses. Mutations discriminate — reverting multiply_evaluations reds both zero-order witnesses while one-times-effect still refuses; restoring the old arm order reds only the right-operand case. 24 witnesses green. The Blocking cost-wall baseline was re-run because this touches an authority feeding it: loop_iteration_floor (incl. its independent linear-times-zero control), disj_alternative_floor, bounded_summation (incl. existing_cost_lens_kernel_unchanged), atom_zero, expr_refusal and copied_port_derivation — 19 witnesses, all green. Witness accounting corrected: the claim label and note now say every LEAF witness, which the aggregating conjunction obviously cannot include itself in. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Qualify the one bare nat_max the second Nat authority made ambiguous Adding v2.std.nat.nat_max (the Peano Nat, needed by evaluate_size_expr's SizeMax and evaluate_cost_expr_in_env's CostMax) gave the name two declarations. test.claim.realization_schedule_critical_path is the single module whose import closure carries both authorities, so its bare call site stopped resolving and reddened the compile-clean gate. Qualified as std.nat.nat_max, matching the std.nat.nat_compare already qualified on the line above it inside the same witness. The four other bare nat_max call sites were checked by scoped compile rather than assumed safe -- dag/std/realization_width, dag/std/realization_measurement, dag/gunbc/econ/free_tier_serving and dag/gunbc/econ/scm_serving_model each compile with zero errors, so their closures do not carry both authorities and they need no qualification. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close the two hygiene gates: exhaustive arms where possible, one rostered residue The floor reported three reds. Two roots, one of them not mine. NON-FOLD RESIDUE. Three wildcard arms landed with the exact evaluator. Two were avoidable and are now gone rather than declared: combine_evaluation and evaluate_summation match over CostEvaluation, which has exactly two variants, so `_ =>` became `ExactCost { value: .. } =>`. DESIGN section 5 puts construction above declaring a residue, and it buys what a roster row cannot -- a third CostEvaluation variant would now make both matches non-exhaustive and compile-clean would refuse, instead of the new variant being swept into a wildcard silently. multiply_evaluations is rostered, not "fixed". Its arms discriminate a nested VALUE (an ExactCost carrying Zero) rather than a variant, so enumerating would write the residual combine_evaluation call twice, underneath the arm order that multiply_evaluations_zero_note declares load-bearing. Duplicating that expression to satisfy a counter would make the function more fragile. Its reason says so, rather than reusing the generic nfr_reason_mint_era its neighbours carry. INERT CARRIER. Not from this change. Probing inert_carrier_names_live returned eleven live names against twelve rostered; the extra is ProcMeminfo, whose consumer landed in #7891 -- already an ancestor of this branch -- while the roster row stayed. origin/main carries both files byte-identically, so this witness is red on main too. The row is deleted here because it blocks merge and deletion is exactly what its own dissolve trigger prescribes; reported upstream so another lane does not duplicate it. Also records, in symbolic_product_zero_absorption_note, that the symmetry the annihilator fix established is CLASSIFICATION and not provenance: unknown times unknown still returns the left operand's diagnostic. That is pre-existing and module-wide (symbolic_sequential drops the same way), and closing it means widening UnknownCost to carry several diagnostics, which is its own change with its own witnesses. Green by execution: non_fold_residue_clean_holds, non_fold_residue_no_unrostered_or_stale, inert_carrier_no_unrostered_or_stale, and every_valuation_witness_holds over all 23 leaf witnesses -- the last because the exhaustive-arm edits rewrote live evaluation paths, not just roster data. Seed receipt reports unrostered=0 stale=0 live=149. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Roster #7965's two carriers and handle #7909's two git mock cases Both failing witnesses on this PR are MAIN-SIDE DEBT landed today, not this branch's. Neither constituent introduced them and neither of main's own runs executed the witnesses that catch them. inert_carrier_no_unrostered_or_stale. TerminatingOneShotFrontier and WitnessPurpose (dag/std/witness_purpose.dag, #7965) are a taxonomy landed ahead of its consumer: nothing outside their own module and their own test file references them, which is precisely the seed's inert predicate (declared once, referenced by a test, zero non-test references outside the declaration block). They get roster rows in the established shape, carrying the shared dissolve trigger -- a live consumer reads the carrier and the stale-roster check then forces the row's deletion. git_mock_consumer_is_total_holds. #7909 added git.Inspect.WorkingTreeStatus and git.Inspect.IgnoredFiles to git_published_mock_corpus without arms in materialize_git_mock, so both fell to mock_unhandled_rejection and totality failed. main publishes 20 cases against 18 arms; this adds the two arms. HOW THE OWNER WAS ESTABLISHED, because my first attribution was wrong. I found seven type carriers new versus main and inferred they were the inert ones -- true premise, unsupported conclusion, since none of the seven can satisfy the predicate (five are referenced by no test file at all; the other two are consumed in non-test fn signatures). The primitive is not directly invocable (no unique runtime declaration identity) and a second-worktree run is invalid because the corpus scan anchors to the compile-time-baked workspace root. So the rule was read out of the seed and reimplemented, and THE REPLICA IS VALIDATED AGAINST THE EXECUTED ORACLE: on this head it reproduces 13 inert against 11 rostered, exactly the unrostered=2 stale=0 the real run measured. Run over three trees it gives main 2 unrostered + 1 stale, pr-7932 clean, this branch main's 2 with main's stale already fixed -- so this branch was strictly better than main before this commit. GREEN BY EXECUTION, with the discriminating red on the real consumer: inert_carrier_no_unrostered_or_stale FAILED on this head before this commit and PASSES after; git_mock_consumer_is_total_holds likewise, alongside both omission RED controls (git_mock_omitted_member_is_red_holds, git_mock_omitted_show_tree_is_red_holds) still passing, so the added arms did not disarm the controls. No regen: neither module projects to a stage0 seed file and no seed .rs references the roster units, verified against a positive control (dag/std/algebra.dag does project, to std_algebra.rs). 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> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.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.
Per-host runner allocation. This is a capacity-decision change: it corrects how much each host is admitted to run and closes three fail-opens in the wall that decides it. It actuates nothing — no slot is created, activated or drained by this PR.
Result
Committed fleet width is 22, not 24, and observed live width is 20. The delta — srv3 5→7 — requires provisioning and activation that this PR does not perform and cannot perform (see Not delivered).
srv4's 7 was a memory verdict published as a commitment.
gunbc.runner_host_deployhas pinned it at 5 on a declared disk cap since 2026-07-22, and an earlier revision of this PR carried "slots 06/07 must not be provisioned on srv4" as prose beside a roster that said 7. Width is now the minimum over resolved axes, so the disk cap binds by derivation and the caveat is gone.Why 14 GiB
186 floor-job cgroup peaks from 2026-08-05 plus five sampled days back to 07-16, read from the
[calibration] floor_peak_postreceipts thecijob already emits:No run reached the 16 GiB MemoryMax. The four at exactly 15.0 GiB are throttle pins — censored lower bounds, and the reason the cap does not fall further. MemoryHigh at 13 GiB sits 1 GiB above the already-measured 12 GiB
gunbc_floor_minimum_viable_armed_budget.Three fail-opens closed
gunbc.session_residency— residency, not the build-cache roster that merely correlated with it. That proxy came within one cleanup of causing the bug it prevented:ctrl-sccache.servicewas found provably dead on srv1/srv2 (29 MB in 45 days, zero connections) and deleting its roster rows would have zeroed the charge and admitted 7 slots each.Evidence grades are typed, not narrated
SessionResidencyEvidencedistinguishes a counted observation from an operator declaration from an unobserved host. This matters because the rows that grant capacity are the negative ones: srv3 and srv4 are classified session-free, which is what admits them the larger width, and neither was reachable when it was written (srv3 refused a key login — the B2 gap infleet_subsumption_manual_gaps; srv4 failed host-key verification). A witness pins that those two areSessionsOperatorDeclaredAbsent, so upgrading them to observed without an observation reds.The unknown-host arm deliberately charges rather than exempts, inverting the refuse-by-default convention used elsewhere in this lane. Refusing isn't available — the consumer needs a Bool to size a budget — so it's a choice between two wrong answers: charging a session-free host wastes slots, visibly and recoverably; exempting a session-bearing host is the srv4 OOM shape.
Jobserver citation, and the over-admission it exposed
jobserver_configwasJobserverAbsent— a reach gap, not a modeling gap, and it closed when srv1 became readable. The installed script's derivation isderive_jobserver_tokensterm for term, so this is a citation: margin 8, reserve 16 GiB, 1792 MiB/job.The script guards its whole derivation behind
if [[ -z "${CTRL_JOBSERVER_TOKENS:-}" ]], so an explicit setting skips the memory bound rather than being clamped by it — 128 × 1792 MiB = 224 GiB of admissible concurrent compile memory on a 125 GiB host, ~2.06× what the jobserver's own inputs allow. Recorded, not changed: it is operator config on a ctrl-era unit and gunbc has no realized knob for it. It matters for the compile-pool flip, which would expose this gap rather than create it.Not delivered — deliberately, and none of it is disguised as delivered
host_converge_realizeimplementsPerSlotMemoryCaponly;RunnerWidthandJobserverTokensreturnKnobUnimplemented. Nothing here creates slot directories, units, or drop-ins.runner_activate_commandrequires a grounded managed-cache receipt and a bound compile-pool receipt, andhost_compile_poolreturns not-ready for every host underCompilePoolInRunnerSlots. The 7-slot arithmetic uses a zero compile-pool sibling; flipping to a managed pool will change the answer and conservation must be rerun then.host_memory_admitted_widthis an authored table the wall then checks. Correcting an input turns the plan unsound rather than selecting a new width. A real solve (desired = min(resolved limits, requested)) is follow-up work.gunbc convergewill refuse srv3 until 7 units exist — the count cross-check compares live to declared. Count equality belongs at the end as a postcondition, not at the front as a prerequisite; that reordering is follow-up work.host_swap_backingrefuses rather than accepting a hand-entered probe result, which is correct; srv1 and srv2 were separately measured at 248 GiB configured (85 GiB and 1.3 GiB in use — corroborating srv1's known server thrashing).Follow-ups this PR deliberately does not attempt
membership_reconcilediscardsfromonModified, so role-keyed identity alone does not make retirement unforgettable.MemberModified { from, to }plus a staged hostReplace(install inert → verify → switch consumers → verify owner → retire → verify absent) is the shape, and it is shared with the SCM lane.{srv3-01..07}diffed against observed directories and units, with width as the cardinality of the desired set.Verification
Affected witnesses green locally.
.github/workflows/{ci,falsifier}.ymlcarry the regen the 14 GiB cap implies (CARGO_BUILD_JOBS4→3); they are author-commit-required, which is what theheal_generated_artifactsfailure was reporting.🤖 Generated with Claude Code