Repository navigation
Compute units report their peak and an OOM kill is a typed, counted ending (no class resized yet: every class still reserves the ceiling) - #12021
Merged
Conversation
…nt of leases The local compute provider admitted work by listing its lease directory and comparing the count against a policy budget of two. That is not atomic -- the list and the create are two operations on different names, and O_EXCL excludes a NAME, never a QUANTITY, so two requests with different identities both read one lease in flight and both proceeded -- and a count is not a capacity: two producers on a 125 GiB host and two on a 502 GiB host are the same policy applied to machines that differ fourfold. Admission is now a seat in a memory pool. The homes are the ones DESIGN 3b names for fabric/compute: product.capacity.pool owns the appropriation, encumbrance, term and release law; product.capacity.pool_events owns the transitions; gunbc.fabric_event_log linearizes each append with one compare-and-set against the partition head. gunbc.compute.host_capacity declares which pool, where it is linearized (this host, not the fleet DB -- a host's own memory is not a fact the fleet contends on, and routing it through another machine would refuse local builds on a network fault), and joins it to a real reading of /proc/meminfo. The unit's MemoryMax is the amount the pool granted, so the ledger's arithmetic is the enforcement rather than a parallel description of it. Every ending -- succeeded, failed, mismatch, infrastructure refusal -- releases, and a release that did not land is reported rather than assumed. Disposition: compute_cold_build_cap is DELETED, and HostAtColdBuildCap with it. Its fact is now HostComputeCapacityFull, measured in bytes; the two arms beside it are facts a count could not express (the machine's live availability, and an unreadable ledger). The appropriation is two worker ceilings, exactly the memory the deleted count admitted. Also: fabric_seat_acquire/observe generalize over the measure (memory is not a dimensionless count), and the observe/append/retry loop gunbc.fabric_quota held alone moves to the carrier as fabric_pool_event_append, with quota settlement migrated onto it rather than a second copy growing beside it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…esent review 69561 on #11962. The presence pass walked meminfo_field_names and refused the first missing name; the record was then built from a SECOND spelling of those names, each falling back to kibibyte(count: 0) on an absence the presence pass had supposedly ruled out. Two lists for one concept is DESIGN 3's nicknaming, and the fork was load-bearing: the zero's unreachability was an invariant held AT A DISTANCE between roster and record, so renaming or dropping a roster entry made mem_total and mem_available read 0 KiB -- which compute_reserve_on turns into a permanent below-floor or appropriation-exceeds-total refusal ATTRIBUTED TO THE MACHINE rather than to the parse. A fabricated plausible output behind a guard that looked like a wall (DESIGN 5). The guard is deleted rather than strengthened. Each field is matched once, its absence names itself, and its value is the one that match just bound: meminfo_required and its zero are gone, so the fabricated reading has no constructor left (DESIGN 4b). meminfo_field_names no longer claims to be this fold's authority -- what the parse demands is exactly what ProcMeminfo has fields for, a fact the record carries and cannot drift from itself. The witness gains the control the absence arms cannot supply: every field carries a DISTINCT value and every field is asserted, so a name paired with the wrong field is red; and a field missing from the MIDDLE of the file names itself. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…them The workload ran under the grant on srv1: a real cargo release build of v1-compiler as gunbc-compute-1bf2556cc4b015f9.service, capped at the 26 GiB the pool granted, binaries returned by content. It also surfaced three defects that no wet cell could see, because none of them touched the provider. 1. THE CONSUMPTION READING BROKE THE ATTACH PATH. It was appended to outcome.json, which the attach path PARSES (stored_outcome_decode), so every later caller of a SUCCEEDED identity read StoredOutcomeUnreadable and rebuilt -- the contract's "two callers, one build" silently dead. Measured: the provider's own dependent compile request refused on a dependency that had in fact succeeded. The reading moves to its own file beside the log; a realization's measurement does not change the shape of the contract's document. 2. THE RESERVATION REFERENCE WAS THE WORK IDENTITY. The identity is stable by construction -- that is its job -- so a second request for the same identity hit the encumbrance ledger's DuplicateReference. The pool's reference names one HOLD, so it is now per attempt; the identity stays in the receipt. 3. A LEDGER REFUSAL WAS REPORTED AS A FULL POOL. The seat carrier renders every pool refusal into SeatFull, so DuplicateReference reached an operator as "capacity full" on a host with 400 GiB free. product.capacity.pool_events names the marker it writes (pool_full_wire) so both sides read one authority, and anything else is carried through as a ledger refusal. The typed-arm fix widens SeatAcquisition and every match on SeatFull, so it is a declared frontier with its trigger rather than a silent widen here. New wet control, red under the conflation: a reused reference on a pool with room for both requests is a ledger refusal and never ComputeCapacityFull. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…le grain The fourth thing the srv1 run found, and the one that makes the case for running it. DESIGN 4c admits standalone leading blocks attached to MODULE-SCOPE declarations only. The witness route this provider is covered by tolerates a block inside a function body; `gunbc compile` refuses it outright. So work_provider_local carried 14 blocking errors while every witness over it reported green, and the real compile request on srv1 is what said so -- the provider had stopped compiling and nothing in the wet or hermetic evidence could see it. The prose is not deleted: it moves above compute_provide_leaf, which is the declaration it was describing. Verified: `gunbc compile --entry dag/gunbc/compute/work_provider_local.dag` reports 0 blocking errors at this head, against 14 before. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… record that disagreed with its caller, and the recovery route that did not exist Side-chat review of #11962 at dd240f0, plus review 69595. All four are real and all four were verified against the code before anything was changed. A. THE DOUBLE PROMISE. Pool capacity and live MemAvailable were checked separately, so with a 52 GiB appropriation, 30 GiB available and two 26 GiB requests, each request saw 26 <= 30 and each fit the appropriation, and BOTH admitted -- neither could see the other's granted-but-not-yet-consumed memory. The compare-and-set was doing its job perfectly on a question that was missing a term. The fix is not a third check. The pool already computes the committed total inside the linearized fold, so the machine's reading belongs in the SAME comparison: the ceiling an attempt is adjudicated against is the smaller of the declared appropriation and what the host says is free. This is worst-case-sound and conservative, and says so: MemAvailable already excludes what outstanding grants have touched, so a resident grant is counted twice. The exact relation needs the resident share, which is observable per unit and is a declared frontier with its trigger. product.capacity.pool already ruled that replay never adjudicates the ceiling, so a moving ceiling cannot poison the fold -- it makes the pool over-committed, which refuses new acquires until it drains. B. THE POOL WAS KEYED BY THE INSTANCE, NOT THE HOST. srv1 declares two instances -- srv1-live and srv1-lab -- with different ids and roots, and the memory they spend is ONE machine's. Both halves are now host-keyed: the partition names the host identity, and the ledger is rooted under the instance that host resolves to through dashboard_instance_for_host, the same host-to-instance authority the fabric event log already uses. A host that authority cannot resolve reserves nothing rather than defaulting to the caller. C. THE RECORD DISAGREED WITH THE CALLER. A run whose work succeeded but whose release failed wrote WorkSucceeded to outcome.json and handed its caller a refusal -- and the next caller ATTACHED to that success, so the leaked seat had no consumer that would ever look for it. The ending and the unresolved obligation are two facts and are recorded as two: the obligation is its own durable file, and the outcome document carries the refusal the caller was given, so a later caller attaches to exactly what this caller was told. D. THE RECOVERY ROUTE DID NOT EXIST (review 69595). The module's prose said a wedged seat is recovered by an explicit release naming why; compute_release took a ComputeReservation whose only constructor lives and dies inside one compute_provide_leaf, so under QuiescenceRequired -- which never lapses -- nothing in the corpus could discharge it, and two such events would consume the whole appropriation and turn every later request into a capacity refusal on a host with its memory free. A claimed route no declaration reaches is the dangling consumption DESIGN 3c refuses. compute_release_reference takes the reference, which is all a recovering operator has, and compute_release_cli is its executing consumer. Both doors go through fabric_seat_release, the checked mirror of fabric_seat_acquire: read, fold, PROPOSE against the folded pool, append only what it admits. That check is load-bearing rather than defensive -- an unheld reference appended anyway would not fail at the append, it would fail at every later READ, when the fold hits UnknownEncumbrance and refuses the whole partition. Controls, all executing wet, seven cells: two requests summing past the observed headroom cannot both admit (RED when the backing ceiling is reverted to the appropriation); two instances on one host resolve to one pool at one root; a held seat is recoverable by reference and an unheld one writes nothing, asserted beside a later successful reservation so the ledger is shown still readable. gunbc compile on the provider closure: 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…n cells supply their own inputs Side-chat review of #11962 at 725d9c5. All three blockers verified against the code first; all three were real. 1. QUIESCENCE WAS DECLARED AND NEVER OBSERVED. compute_release ran unconditionally on what compute_run_leased returned, and that is the exit of `systemd-run --wait` -- a LAUNCHER, not the unit's parent. A launcher killed, timed out, or disconnected from the bus yields ComputeExecFailed WHILE THE UNIT KEEPS RUNNING, so the seat's memory would be handed to the next arrival on top of a live cargo. product.capacity.lease already models this exactly (QuiescenceFact) and this provider was not consulting it. Settlement and recovery now both consume a termination decision bound to the actual unit, read through the existing systemd.Systemctl.ShowUserProperty. Only two arms free capacity: the manager has no record of the unit (never started, or ran and was collected -- the same fact for this decision), or it reports it stopped. Running keeps the charge, and so does UNOBSERVED, which is the arm a fail-open would swallow and the one a lost launcher produces. An ActiveState this fold has never seen is unobserved, not permission. The recovery CLI observes it too: an operator releasing "because the worker looked dead" was asserting the one fact nothing checked. A running unit is refused by name with the state that refused it. 2. OBLIGATIONS WERE KEYED BY IDENTITY WHILE RESERVATIONS ARE KEYED BY ATTEMPT, so a retry overwrote the first obligation and the first seat became unrecoverable -- the reference that was the only way to release it was gone. One obligation file per attempt, named by the reference, created exclusively so a second writer cannot replace one. A retry now CONSUMES that lifecycle state: an identity with an outstanding obligation refuses by name and points at the release verb rather than reserving on top of a charged seat and publishing over the record carrying it. And the producer lease is dropped LAST -- it was deleted before the outcome was written, so the exclusion held for the name and not for the publication it exists to protect. 3. THE HEADROOM FIXTURE DERIVED ITSELF FROM THE THING UNDER TEST. appropriation = 4 x (available/2 + 1MiB) exceeds MemTotal on a lightly loaded host, so the cell refused before reaching the comparison it existed to make -- and on a busy host it passed for unrelated reasons. It was flaky in both directions. compute_reserve_against takes the observation as a value and compute_reserve supplies the real one, so the admission cells state the relation exactly: each request fits available, two exceed it, two fit the appropriation, and the appropriation fits MemTotal. Not a skip -- the pairing obligation is discharged by the_real_observation_reads_this_machine, which asserts the real producer reads THIS machine, and by the srv1 receipts. Also, per the accepted (A): the relation is described as admission against an observed MemAvailable ESTIMATE, and explicitly not a no-OOM guarantee. The unit's MemoryMax bounds one workload; this stops the POOL from over-promising, and conflating the two would be the rung inflation DESIGN 4b forbids. Eight wet cells and the termination fold all pass; gunbc compile on the provider closure: 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…arge gap, and the memory carriers the refusals were stripping Split approved by the manager. All seven of the side chat's blockers at 9172cf7 are lifecycle/recovery; none touches admission or the pool. The argument for splitting is safety, not workload: WITHOUT a recovery route every one of those defects degrades to "the seat stays charged" -- the host under-admits and nothing is over-promised. WITH a half-built one they FREE SEATS THAT SHOULD NOT BE FREED. Shipping recovery half-built is worse than not shipping it. OUT OF THIS PR, and named rather than quietly dropped: compute_release_cli, compute_release_reference, the obligation files and the retry-blocking read. BLOCKER (1) IS NOT RECOVERY-ONLY AND IS FIXED HERE, per the manager's correction: automatic settlement releases too. ActiveState alone is not the evidence -- `failed` can coexist with live processes while a unit's stop reaches its SIGKILL timeout, and an empty ActiveState is the manager declining to answer, not authoritative absence. The decision is now four-valued over evidence the repo already models: authoritative absence from LoadState=not-found (the wire value this corpus reads positively), observed termination from the unit's own cgroup reporting populated 0, populated, and unavailable. Only the first two free capacity; unavailable keeps the charge, and that is the arm that matters, because a lost launcher, an unreadable manager and a missing cgroup all look like it. BLOCKER (7) STILL REACHED PR 1 AND IS FIXED: the lease-undropped arm handed the caller a refusal while the outcome document already said the run SUCCEEDED, then claimed the next request would refuse as ProducerInFlight -- three claims that cannot all be true, since the stored record is what the next caller attaches to. One contract now: the stored record is the result, the caller is told what the next caller will read, and the stale lease is recorded as an operational fact rather than converted into a verdict about the work. Blockers (2)-(6) are no longer reached: each was about the recovery door or the obligation files, and both are out. THE GAP IS CLASSIFIED AS THE MANAGER ASKED. No discharge route existed on main -- admission was a count of lease files and there were no reservations at all -- so this is not a rung that fell and is not a 4b(3) drop. It is a new class: gunbc.recurring_failure_mode a_held_compute_seat_has_no_in_corpus_discharge, rostered, with a trigger naming PR 2's CAPABILITY (termination from absence or an empty cgroup; attempt-to-unit binding; coordination with a pending producer; a settled state a retry consumes) rather than an artifact. Its remedy sentence reaches the caller through compute_stuck_reservation_remedy. review 69624, unit modeling: HostBelowMemoryFloor carried Int fields NAMED _kib while its producer already had Kibibyte and the provider called kibibyte_count to strip the carrier on the way in -- the unit modeled twice and checked nowhere. It carries Kibibyte now. And SeatRoomObserved.headroom was the boundary THIS PR moved: a bare Nat was right while the pool was fixed at seats, and generalizing fabric_seat_observe to Pool<Q, S> made the same field mean KiB for one caller and seats for another. SeatStandingObservation is now generic and headroom carries Measure<Q, S, Nat>. Seven wet cells plus the termination fold pass; gunbc compile on the provider closure: 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…o remedy texts that told a reader the wrong thing Side-chat review at 5ee0cce plus review 69645. All four verified against the code first. THE THIRD RELEASE ARM. observe_unit_cgroup read an empty ControlGroup as UnitTerminatedObserved without reading any cgroup at all, and an empty or unrecognized successful LoadState could reach it. An empty ControlGroup does not mean finished: systemd realizes the cgroup AT SPAWN, so it equally describes a start that is still PENDING -- which makes a whole unbacked launch reachable. Reserve; the start is pending; the LAUNCHER is lost while this driver lives on; settlement sees the empty property, releases; the job then starts against memory nobody holds. The arm is deleted and an empty required property is never promoted to a conclusion -- it is UNAVAILABLE like every other absence of evidence. Capacity is now freed on two facts that establish the attempt ENDED, plus one that requires a realized cgroup: THE ATTEMPT COMPLETED -- `systemd-run --wait` returned success, which it does only after the unit ran to completion. A lost launcher does not return success and a pending job has not returned at all. This is a SEPARATE fact from the work's ending, and conflating them is what let a lost launcher free a live unit's memory: a WorkFailed says the unit exited nonzero OR that the launcher never got an answer. THE MANAGER HAS NO RECORD -- LoadState=not-found. A REALIZED CGROUP REPORTING populated 0 -- which cannot be a pending start, because the cgroup exists only from spawn onward. THE DECISION IS NOW A FOLD OVER SUPPLIED READINGS (UnitObservations), so the controls sit at the OBSERVATION-TO-DECISION boundary rather than at the variant-to-release mapping, which cannot see any of the defects that actually occurred: a failed query whose text reads like an answer, an empty property, a pending start. A failed query is unavailable whatever it printed -- the exit status decides first and the text is never consulted. review 69645, THE DISCARDED HOST RECORD: `if measured.success { settled } else { settled }` had identical arms, so a failed write vanished by construction. The compound case was the sharp one -- the producer lease failing to drop AND that write failing left an identity whose lease is permanently held with NO RECORD ANYWHERE that it is stale, while the caller got an ordinary success. It now refuses, naming what was lost. This does not reopen blocker (7): that was a refusal DENYING a published success; this one affirms the run's ending, says the stored record is authoritative, and reports a host fault that happened after publication. review 69645, THE DEAD CITATION: fabric_seat_release's annotation named compute_release_reference and compute_release_cli, which the split removed. It now names its real consumer and states that the operator door is the capability PR 2 lands. TWO REMEDY TEXTS THAT MISLED. compute_stale_lease_note said the next request would refuse as ProducerInFlight, contradicting the contract the same block establishes: a caller reaching a published SUCCESS attaches, and the attach is decided before the lease is consulted -- the stale name only blocks a request that must PRODUCE again. And compute_stuck_reservation_remedy told an operator to clear the partition by hand, which under live admission removes the record the admission arithmetic folds and trades a host that under-admits for one that over-promises; it now refuses that and states the ordering any manual intervention requires. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…on keeps the charge; the record and the caller stop disagreeing Side-chat review at 773825c, plus review 69663. All four verified first. (1) THE ORDER OF THE TESTS WAS THE DEFECT. attempt_completed was checked FIRST and returned immediately, so {completed, populated 1} RELEASED -- a launcher's success overriding the kernel saying processes are still there. `--wait` returns when the MAIN process exits, and under KillMode=process or none a forked child outlives it in the unit's cgroup. Both halves of the reviewer's either/or are taken, because each is independently right. KillMode=control-group is now BOUND on the invocation rather than inherited -- a default is not a declaration, and a drop-in could change it while this provider went on treating a completed wait as an empty cgroup. AND contrary evidence wins regardless: a positive populated=1 refuses the release before anything else is considered and is never discarded. (2) A MOMENTARILY EMPTY CGROUP IS NOT TERMINAL. populated=0 with completion NOT established used to release, and a realized cgroup can be empty between execs. In this PR an uncertain completion keeps the charge; the population reading now only CONFIRMS a completion or REFUSES one. UnitTerminatedObserved is gone as a releasing arm. Establishing termination without a completed attempt is the lifecycle capability's job. (3) THE RECORD AND THE CALLER DISAGREED AGAIN, one layer along: the lost-record repair published the real outcome and synthesized a WorkRefusedByInfrastructure for the caller, so the caller and the next attacher read different contracts -- the same fusion as before, in the opposite direction. The two facts are now returned as two. ProvideResult carries the stored outcome UNCHANGED plus a HostRecordStatus beside it, so re-requesting an identity yields exactly the ending the first caller was told. The CLI turns a lost record into a nonzero exit naming both halves, which is how the recording failure stays visible without becoming a verdict about work that really ran. review 69663: seat_release_landed had no consumer anywhere in the tree -- compute_release_on matches SeatRelease structurally and the provider uses its own compute_release_landed. Deleted rather than given a consumer, because the carrier already answers the question by match (DESIGN 3c). Controls, all at the observation-to-decision boundary: a completed wait with populated=1 keeps the charge; populated=0 without completion keeps the charge; a pending start establishes nothing; a failed query whose text reads like an answer is unavailable; and a lost host record changes no contract the next caller reads. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ence A completed wait may confirm a release only because KillMode=control-group means systemd tears the cgroup down with the unit. Spelled inline at the call, that was an assertion nothing checked; the properties are a fold now, and the_unit_binds_the_termination_policy_the_release_decision_relies_on is what makes "bound" a fact. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts: # dag/gunbc/ci/ci_layer_roots.dag
…terminal consumer; the KillMode control claims only what it checks Side-chat verdict at f5344b2. All three verified first. (1) THE PREDICATE READ "not occupied AND (absent OR completed)", so completed + UNKNOWN released -- and the witness ASSERTED that, which is the worse half: a control that pins the defect is not a control. It is now exactly: occupied keeps; authoritative absence releases; completed AND POSITIVELY EMPTY releases; everything else keeps. A bound KillMode says what systemd WILL do and is not a reading of what is true, so an unreadable cgroup establishes nothing beside a completed wait. The witness is flipped. The KillMode control now claims only what it checks: it reads the argv this provider CONSTRUCTS -- invocation wiring -- and does NOT establish what systemd applied. A drop-in, a rejected property, or a unit started by some other path are outside what any fold over our own argv can see, which is exactly why the release predicate does not lean on the binding. (2) HostRecordLost WAS ERASED BY THREE CONSUMERS and is carried through all of them now. compute_provide_dependent returned only the child's result, so a BUILD that lost its record followed by a successful dependent reported clean -- the status is joined onto the dependent's result, accumulating rather than letting the later arm win, because the two details name different identities. ProvideAttached carries the status too, so an attach cannot drop a carried loss. compile_entry_cli exits nonzero naming the loss, and run_selected_module carries it onto ModuleRan, into the emitted JSON, and into the module's verdict. None of this changes the stored work outcome: the ending and the document reported are exactly what was stored, and only whether the run is called clean moves. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…eside it Found by the srv1 fault-injection run for the re-attach control, and it is the same defect as the consumption line once appended to outcome.json -- committed a second time, one file along. Appending the host-record sentence to the receipt stopped it being parseable JSON, so a consumer reading it back got "Extra data" instead of an outcome. A document a consumer parses carries exactly what its contract says. The receipt is the document again; the loss is written to <receipt_path>.host-record and the exit reason names where it went. Both CLIs. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…proves it review 69724, and it is this change's own diagnosis unapplied one boundary over. gunbc.compute.host_capacity was calling kibibyte_count to STRIP its Kibibyte on the way into SeatRequest -- the exact tell work_request.dag names for HostBelowMemoryFloor and fabric_event_log.dag names for SeatRoomObserved. A bare Nat was right while every pool reachable through this fold was Pool<Count, One>: seats are dimensionless and the field meant seats. This PR generalized the carrier to Pool<Q, S>, which made the same field mean KiB for a memory pool and seats for a seat pool with nothing in the type to say which. So SeatRequest is generic and amount carries Measure<Q, S, Nat>. WHERE THE STRIP LEGITIMATELY HAPPENS IS ONE LAYER DOWN, and the difference is not cosmetic: propose_acquire holds the POOL, so the pool's own type parameters prove the request's dimension matches the appropriation it is adjudicated against. A consumer stripping the carrier ASSERTS that match; this fold CHECKS it. THE PERSISTED EVENT KEEPS A BARE Nat AND THAT IS NOT THE SAME DEFECT, stated rather than left to be re-found. PoolAcquired is a wire record: its dimension is the partition's, and it is restored at both ends from the pool's own parameters -- minted from a Measure the pool typed, and re-minted at replay by pool_apply_event into the Pool<Q, S> being folded. A JSON integer carrying a magnitude whose unit the surrounding type fixes is a serialization, not a second model of the unit. Call sites: harness_seat and fabric_quota wrap their counts, the capacity and spark witnesses likewise, and host_capacity passes its Kibibyte straight through. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
review 69724 finding 2. compute_with_lost_host_record matched the arms itself, and the ProvideAttached arm returned the status it was handed while THROWING AWAY the detail it had just built -- the exact vanish this function exists to prevent, one arm along, in the function whose annotation is about a fact vanishing. It was latent only because the single call site passes a fresh result, which is the kind of "safe today" that stops being true at the next call site. Two spellings of one join is also the fork DESIGN 3 forbids, so there is now one: provide_result_with_host_record, which already handled both arms and accumulates rather than letting either side win. The control drives BOTH arms. Mutation, run and reverted: restore the arm-matching discard and a_lost_host_record_changes_no_contract_the_next_caller_reads goes FAIL. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e buried Ruled 2026-09-21 (loyal-swift-608): do NOT carry Measure through PoolAcquired and the codec -- the decoder would still mint the caller-requested Q,S because the wire has nothing to disagree with, so the RED would not be authorable anywhere a check could run, which DESIGN 4b names as worse than absent. But the error class the argument identified is real and nothing in the corpus holds it, so it does not leave with the argument. gunbc.recurring_failure_mode a_pool_partition_does_not_declare_its_quantity: a persisted capacity partition carries magnitudes and does not declare the QUANTITY they are denominated in. pool_apply_event mints every replayed amount into the Q and S OF THE POOL BEING FOLDED, so a seat partition replayed by a memory pool reads 1 seat as 1 KiB and a memory partition replayed by a seat pool reads 27262976 KiB as 27262976 seats -- arithmetically consistent, semantically unrelated, nothing refuses. THE CLASS BECAME REACHABLE IN THIS PR, which is why it is filed here: generalizing fabric_seat_acquire and fabric_seat_observe from Pool<Count, One> to Pool<Q, S> is what made two quantities share one linearization. Before it, every partition reachable through that fold was seats and the question could not be asked. What is NOT claimed: that it has occurred. The two partition namers are disjoint by construction today -- `quota-` over a rate-limit key, `compute-memory-` over a host -- so the row is filed because the discipline preventing it is a naming convention held by two authors, not a fact the substrate checks. Trigger names the CAPABILITY -- partition identity binds the pool quantity, so a mismatched fold refuses -- deliberately not "carry Measure through the codec", which could land in full while the class stayed exactly as dead. Rostered, and stated in the PR body beside the other declared gaps so a reader does not have to find it in a failure-mode file. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… resolution (every class at ceiling) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ff, fail-closed arm linked Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…, typed peak sample at its upper bound Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
marked this pull request as ready for review
September 22, 2026 02:26
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
💡 Codex Reviewgunbc/dag/gunbc/compute/host_capacity.dag Line 270 in f054978  Add compaction before the compute ledger reaches its read bound
This fixed 4096-event budget gives the new host-wide compute partition a guaranteed finite lifetime: each completed job appends an acquire and a release, so after roughly 2048 jobs the next acquire can append event 4097, but settlement can no longer traverse the chain and therefore cannot append its release. That leaves the reservation charged and every subsequent gunbc/dag/gunbc/compute/work_provider_local.dag Lines 991 to 992 in f054978  Use a truly unique reservation reference
When the same work identity starts another reservation within the same second—most directly, an immediate ceiling retry after a fast OOM—this produces the identical ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
… who owes the truncated read
Two responses to loyal-swift-608 (2026-09-22).
THE --quiet TRAP IS NOW UNWRITABLE RATHER THAN MERELY UNUSED. systemd-run prints the result and
peak lines only under `if (arg_wait && !arg_quiet)` (run.c, v255), so anything routed through
systemd.SystemdRun RunTransientAndWait -- which carries --quiet -- reads MemoryPeakNotReported
forever: a dead producer indistinguishable from a healthy launcher whose manager is below v254,
reachable by a one-word difference between two operations in one file. The provider did not use it,
and that is exactly the protection that decays.
So systemd_run_wait_summary no longer takes a loose String. It takes a SystemdSummaryPrintingWait,
minted in exactly one place -- systemd_run_user_wait_arguments, the only wait builder here that
omits --quiet -- so a launcher that cannot print a peak cannot be handed to the thing whose contract
is to observe one. RunTransientAndWait keeps --quiet, with the reason stated: its callers want the
child's stdio unpolluted, which is a real and different need; the fix is that the two cannot be
confused, not that one loses its flag.
Two consequences, both improvements. The provider reads the summary inside compute_run_unit, where
the invocation is in scope (ComputeUnitRun { exec, summary }), so no site further out holds a bare
stderr String a peak could be read from. And every fixture claim now names the invocation it is
pretending came from.
WHO OWES THE TRUNCATED READ, since the parser may not guard it. A truncation under-reports -- "11G"
cut to "1G" parses cleanly as a tenth -- and under-reporting is the direction that OOMs. No parser
guard can catch it: gunbc.machine_intake_host_capture_envelope HostCaptureText settled that
line-wholeness is the CALLER's fact, never inferred from bytes, and this stderr is a completed
transcript the seed's shell observation trims. The reader is gunbc.WitnessBin.Run and it CAN return
a prefix: stderr_capture defaults to BoundedTail { bytes: 16384 }. What closes the hazard is the
direction of that policy -- a bounded TAIL discards the oldest bytes and the summary is the
youngest, so a cut can only slice the first retained line, which is the unit's own output. Stated as
a named dependency on that operation's contract, not as a check this module performs.
ABSENCE CLAIMS. NotReported is reachable by three absence shapes, all constructible without a host:
empty stderr, a failed unit whose stderr carries only its own output, and the pre-v254 omission.
None reads as a peak of zero, and an unterminated summary still READS -- pinned so no one adds the
termination guard that would drop every real run.
the_peak_is_unreported_by_absence_and_an_untrimmed_summary_still_reads returned true; whole closure
typechecked with no other error.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
marked this pull request as ready for review
September 22, 2026 02:59
…ass on one defect loyal-swift-608, 2026-09-22: assert the mechanism, not the outcome. A bare NotReported is an OUTCOME several causes produce -- a pre-v254 manager, a --quiet launcher, a unit never started, an empty capture, a dead parser -- so a defect that makes EVERYTHING unreported satisfied all three absence claims at once. That is DESIGN section 5's absorbing fallback in miniature: the failure arm answers where it should refuse precisely. SummaryAbsence types the cause (NoInvocation, SuppressedByQuietLauncher, CaptureEmpty, LineAbsent), shared by both readings because both go missing for the same reasons, and every claim now asserts its own arm. Also lands the demoted wall's regression control. The intent was that SystemdSummaryPrintingWait, minted only by the builder omitting --quiet, makes a quiet launcher unexpressible as the reader's argument. Measured otherwise: a record parameter accepted a List<String> on the evaluation path and read a peak out of stderr no quiet launcher could have printed -- rung 2, not rung 4, with the fold as the actual wall and parameter-type enforcement as the next-rung trigger. Evidence, nine claims in work_class_grant_witness_test: clean tree 9 PASS quiet check -> `if false` reds exactly a_quiet_launcher_reports_no_peak... absence collapsed to one reds exactly the two claims asserting LineAbsent Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
loyal-swift-608, 2026-09-22: run the other collapse arm. It falsified what I expected and the finding is worth more than the run. Typing the absence made three claims stop passing on ONE defect, but it did NOT pin each claim to one cause: both absence claims asserted CaptureEmpty AND LineAbsent, so collapsing every absence to EITHER cause reds THE SAME TWO CLAIMS. Pairwise discrimination held; per-claim separability did not, and the second is the property worth having -- a red that names which cause collapsed, not one that says some cause did. Each cause is now asserted in exactly one claim. No fixture was dropped: the failed-unit-without-a-peak-line case moved to the LineAbsent claim, and the empty capture got its own. Evidence, ten claims, four runs: clean 10 PASS collapse -> CaptureEmpty reds ONLY the_peak_is_unreported_by_absence... collapse -> LineAbsent reds ONLY an_empty_capture_is_reported_as_capture_empty... quiet fold deleted reds ONLY a_quiet_launcher_reports_no_peak... Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… the wall TWO THINGS, both rung honesty. FIRST, the class is rostered rather than left in a commit message: a_claim_asserting_several_causes_cannot_name_which_one_went. Its tell is greppable and needs no knowledge of the subject -- a conjunction, inside one claim, over two or more sibling arms of the same cause type. If a claim asserts N causes, its red cannot name which one went, however precisely the OUTCOME is typed. Verification is a matrix, not a mutation: collapse to each cause in turn, require each direction to red exactly one claim. Bounded against executed_conjunct_discriminates_nothing, which owns the red that never fires; this is its complement, where the red fires and the loss is attribution. SECOND, the correction neat-boar-16's scoping makes me owe. I demoted the reader's wall to rung 2 when I measured a List<String> accepted for a record formal, but TWO OTHER ANNOTATIONS still stated the mint as construction -- that a quiet launcher was "no longer expressible" and that a claim "cannot read a peak no launcher could have printed". Both false by the same measurement, both corrected to name the argv fold as the wall. The scope is narrow and is now recorded where the rung is: declared parameter types ARE enforced generally (Int<-String, Int<-List<Int>, Rec<-Other, Rec<-Optional all refuse); the hole is ONE relation, a collection handed to a nominal product and its dual, in v1.compiler.infer declared_type_inhabitance -- a third specimen of declared_type_wall_keyed_on_the_value_being_a_kernel, not a new class. The trigger now names that relation and names the PATH: the interpreter's evaluation path was measured, emission was not, and DESIGN 4b(1) takes the minimum across paths. Evidence: ten claims PASS; the derived roster regenerated with the new row and the closure typechecks with it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… owns it loyal-swift-608, 2026-09-22, generalizing this lane's own receipt. Appended to stale_claim_survives_its_own_correct_edit rather than forked into a new class: the specimens there have the falsifying edit made ELSEWHERE by someone else, which is what makes the join hard to demand. This variant removes that excuse -- the correcting edit was the AUTHOR'S OWN, minutes earlier -- and is still missed. The addition that is not a restatement: WHY THE SURVIVORS ARE WORSE THAN THE ORIGINAL OVERCLAIM. Before, N annotations agreed and all were wrong, so a reader got one consistent wrong story. After a site-local demotion, N-1 assert the wall and 1 denies it, each individually honest-looking, and the majority is the stale side -- the one place that tells the truth is outvoted. The sweep is free: grep the ASSERTION, and the count is the population the demotion owes. Also records the complement, because a roster with no green arm trains readers to ignore its red: a harness that says "route gap and not a verdict" IN THE VERDICT LINE. The failure it avoids -- a route gap reported as a red -- is the one that teaches people to triage reds as infrastructure. Evidence: ledger_row_coherence witness 3 PASS, so the appended receipt parses and the row still renders coherently. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ad of parsing loyal-swift-608, 2026-09-22: the version was an assumption sitting outside the type. It is now inside it -- systemd_run_wait_summary takes a SummaryFormatStanding, and only SummaryFormatGrounded reaches the parser. WHY A REFUSAL AND NOT A BEST-EFFORT PARSE. Everything this module knows about the summary was read at ONE major, and the load-bearing part is invisible in the output: FORMAT_BYTES passes USE_IEC, so the figures are 1024-based, while format_bytes_full DEFAULTS to SI 1000-based factors. A major that dropped the flag would print a well-formed line this module reads ~7% high and would size every grant BELOW the peak that produced it -- silent, unsafe, undetectable from the line, and it would have survived every mutation here because the fixtures and the parser would carry the same wrong base. The grounded set is a LIST, not a floor: a newer major is not safer, only unread. Deliberately NOT the same question as systemctl systemd_memory_peak_support, which asks whether a peak is reported at all (>= 254, open-ended). A manager can report a peak in a format nobody has read; that is the case that must refuse. The version is observed from systemd-run itself -- the binary whose output is parsed -- not from systemctl, which would answer about a different executable. Evidence, thirteen claims, four runs: clean 13 PASS grounded set widened to 257 reds ONLY an_unread_major_refuses... ungrounded major parsed reds ONLY an_unread_major_refuses... unreadable version parsed reds ONLY an_unreadable_version_line_refuses... One honest limit: the Grounded arm has no single-claim collapse, because negating it means emptying the grounded set, which disables every fixture and reds broadly by construction -- a capability removal, not a collapse to a sibling cause. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…onsumer loyal-swift-608, 2026-09-22. Every new systemd major refuses until someone reads it, which is correct and will happen -- so the diagnostic carries the procedure instead of making the next reader rediscover it: read run.c and format-util.h at that major, confirm the guard, the emit and its UINT64_MAX condition, that FORMAT_BYTES still passes USE_IEC | BELOW_POINT | TRAILING_B, and the line order, then add the major to grounded_summary_format_majors. Same discipline as a next-rung trigger naming the capability rather than an artifact. The third fact is named because it is the one that would be skipped: the flags are invisible in the output, and USE_IEC is the difference between 1024-based and 1000-based figures. A REMEDY NOTHING CARRIES IS PROSE NOBODY READS AT THE MOMENT THEY HIT THE WALL, so the claim asserts the JOIN: the refusal reaches work_class_peak_sample's reason with the remedy on it. Keyed to the DECLARATION, not to a literal -- rewording the remedy stays green because the wording is not the claim; dropping it from the consumer's path goes red because the join is. Evidence: 13 PASS; dropping the remedy from the ungrounded wire reds ONLY an_unread_major_refuses_instead_of_reading_its_figures. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
loyal-swift-608, 2026-09-22, and the rule rather than the preference: a claim's NAME is what the next reader uses to decide whether it may be retargeted, narrowed or deleted, so a name that understates what depends on a claim is a decay the annotation cannot repair -- the annotation is read AFTER the decision to touch it. an_unreadable_version_line_refuses_rather_than_assuming_the_grounded_major read as edge-case tidying. It is not: deciding whether the format may be parsed requires READING A VERSION LINE, so "parse the version to decide whether you may parse" is circular unless the version read can itself refuse. Ordinary edge-case cleanup would have deleted the base case and left the recursion open. Renamed to the_grounding_recursion_terminates_because_an_unreadable_version_refuses. The rule's exception did not apply: this claim is new on this branch, in no roster and behind no declared split, so the rename is cheap and the annotate-and-cite substitute was not needed. The two-way citation is there anyway because it was free -- each end of the grounding relation now names the other. Evidence: 13 PASS after the rename. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…y local loop cannot see CI floor red since 6a53f39, three annotation blocks of mine sitting INSIDE declaration bodies -- a fn body, an else branch, and a nested `operation` within a service. DESIGN 4c admits standalone leading `//` only above a MODULE-SCOPE declaration; body grain refuses until separately modeled. main carried none of these, so all three are mine. WHY THIRTEEN GREEN CLAIMS DID NOT CATCH IT, which is the part worth recording: claim_batch over a witness entry resolves the module closure and NEVER RUNS THE DAG PARSE SWEEP, so a grain defect in a touched module is invisible to it while every witness reports PASS. That is the rostered class annotation_inside_a_declaration_body_is_invisible_to_the_authoring_gate, and I walked into it by verifying with the only instrument I had running. Each block moved above its enclosing module-scope declaration AND REWORDED to name its subject, because it is no longer adjacent to what it describes -- an annotation that says "this operation" from a site two levels out is a citation by position. The service-level one states why it is authored at that grain. Evidence, and the green is falsified rather than trusted: v1_src_dag_parse 6591 files parse-clean, exit 0 planted body annotation LOCATED at work_provider_local.dag:373:3, exit 1 plant removed parse-clean again, exit 0 claim_batch 13 PASS (text moved across declaration boundaries) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
One precision owed in The row annotation currently reads: "a policy budget grounded in observations … what makes it admissible (DESIGN §5) is that it is FALSIFIABLE." That subtly conflates two different jobs, and a future reviewer will re-litigate it as a §5 defect rather than stopping at "which arm":
So the sentence to add names the arm, and keeps falsifiability as what upgrades the arm to a contract. This does not change behaviour and nothing in the diff is wrong — it is the annotation attributing admissibility to the wrong half of its own argument. It rides with the relief PR, which must touch Unchanged and worth restating at merge time: this PR gives no class a grant. Four classes, four ceilings, zero samples. It is the producer and the typed ending; the relief is the next change and is gated on a real sample from a host with systemd. — sent from lively-bat-737 |
…the retry reference is not re-minted Both found by side-chat review of #12021, both verified in the source before repair. BLOCKER 1 -- THE CEILING RETRY COULD REUSE A RELEASED REFERENCE. compute_reservation_reference is identity + "@" + a SECOND-granularity clock, and the retry re-minted it immediately after releasing the first hold. A unit oom-killed fast enough -- the common case for a grant sized below what the class needs -- releases and re-reserves inside one second, reproducing the released reference. DuplicateReference is a measured ledger fact: gunbc.product.capacity.pool_events records it rendered to an operator as a FULL POOL on a host with 400 GiB free (srv1, 2026-09-21). So the advertised retry would be refused as a capacity failure exactly where it exists to serve. Repaired by CONSTRUCTION rather than precision: compute_ceiling_retry_reference derives the retry's reference from the first one, so the collision is unexpressible and no clock is consulted. One discriminator suffices because exactly one ceiling retry is permitted per attempt. BLOCKER 2 -- AN UNCLASSIFIABLE ENDING BECAME WorkFailed. compute_summary_is_oom_kill answered false for an unrecognized result, an absent summary AND an ungrounded manager, and the consumer read false as "definitely not an oom-kill". So "the ending could not be classified" rendered as "definitely failed", suppressing UnitMemoryGrantExceeded and its counted retry precisely where the manager's result was unavailable -- the version-grounding refusal two files up, discarded one layer down. The predicate was not wrong; asking a yes/no question of a three-valued fact was. Typed UnitEnding plus a new UnitEndingUnclassifiable refusal arm carrying its cause. AND THE REVIEWER'S INSTRUCTION ABOUT CONTROL PLACEMENT CAUGHT A DEFECT IN MY OWN CONTROLS. My first draft asserted compute_unit_ending directly. Mutating the CALL SITES left all twenty green -- the controls established the decision function was correct while saying nothing about the decision being MADE, which is the failure the reviewer named, one level up. The mapping is now compute_failed_unit_outcome, a pure fold the effectful body calls, and the claims assert the OUTCOME. Stated in the module rather than implied: a claim cannot observe WHICH function an effectful call site calls, so bypassing the fold is not detectable here. The pairing obligation for that is the srv1 real-path run this PR declares unexecuted. Evidence, twenty claims: clean 20 PASS fold reverts to the Bool reds the three unclassifiable-ending claims, nothing else retry discriminator emptied reds the two retry-reference claims, nothing else v1_src_dag_parse 6591 files parse-clean, exit 0 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
added this pull request to the merge queue
Sep 23, 2026
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.
Base:
main. #11962 landed 2026-09-22 01:22 and is merged into this branch; this PR no longer stacks on it.What this is, and what it is not
This adds a unit peak producer and a typed, counted grant-exceeded ending for the compute pool. It does not size anything per class yet. It ships no grant rows, so every class still reserves the ceiling and no reserved amount moves. The relief comes in the next PR, from the samples this one starts recording.
Brief correction, found before any code was written: #12001 is the floor runner's memory-beat attribution, not a per-class peak producer for the compute provider's units. No such producer existed, so this PR builds it.
The chain
extdeps.systemd.systemd_runsystemd_run_wait_summary. Work runs undersystemd-run --wait --pipe --collect, so the unit and its cgroup are gone when the launcher returns. systemd-run readsResultandMemoryPeakover D-Bus before exiting and printsFinished with result:/Memory peak:. We read the last occurrence of each, because the unit's own stderr precedes the summary. The peak is carried as the upper bound of FORMAT_BYTES's truncated tenth,(10W+d+2)·F/10. An absent line never reads as 0.gunbc.compute.work_requestUnitMemoryGrantExceeded. An OOM-killed unit is the machine ending the work, so it no longer renders asWorkFailed { exit_code }.gunbc.compute.work_provider_localcompute_run_granted. A grant below the ceiling that is OOM-killed has this attempt retried once at the ceiling; the class is not downgraded permanently. The exceedance is recorded before the retry, and an unreadable record reads as unreadable, never 0. A grant already at the ceiling is not retried.gunbc.compute.work_class_grantwork_class_grant. Row = samples + headroom (operator policy budget, falsified by a non-zero exceedance count). Fewer than 2 samples, two rows for one class, or a sized figure at/above the ceiling all resolve to the ceiling.work_class_grant_rowsis empty.a_sampled_grant_is_discovered_below_worst_case, rung 1. Next-rung trigger is a structural peak bound, not "more samples".Two fail-closed properties added after the first review
An absence carries its cause. A bare
NotReportedis an outcome several causes produce — a pre-v254 manager, a--quietlauncher, no invocation, an empty capture, a dead parser — so one broken parser satisfied every absence claim at once.SummaryAbsencetypes the cause, and each cause is asserted in exactly one claim, so a red names which cause collapsed rather than saying some cause did. Filed asa_claim_asserting_several_causes_cannot_name_which_one_went.The summary format is version-keyed, so an unread major refuses. Everything here was read from systemd source at one major, and the load-bearing part is invisible in the output:
FORMAT_BYTESpassesUSE_IEC, so figures are 1024-based, whileformat_bytes_fulldefaults to SI 1000-based. A major that dropped the flag would print a well-formed line read ~7% high, sizing every grant below the peak that produced it — silent and unsafe. Sosystemd_run_wait_summarytakes aSummaryFormatStandingand onlySummaryFormatGroundedreaches the parser.>=would assert a property of versions nobody has read.systemctl, which can differ on a mixed install.A wall that was measured and demoted, not claimed
SystemdSummaryPrintingWaitis minted only by the builder that omits--quiet, which reads as making a quiet launcher unexpressible. It is not. AList<String>carrying--quietwas accepted for that record formal on the evaluation path and read a peak out of stderr no quiet launcher could have printed. So the honest rung is 2, not 4: the wall is the argv fold in the reader, with a regression control. Scoped since by neat-boar-16 to one relation — a collection handed to a nominal product and its dual, a third specimen ofdeclared_type_wall_keyed_on_the_value_being_a_kernel. The trigger names that relation and the path: the interpreter was measured, emission was not, and §4b(1) takes the minimum across paths.Two further annotations that still asserted the mint as construction were corrected in the same sweep — a demotion has a population, not a site.
Report (classes)
neat-boar-16's 9.7 GB
v2.compiler.compilepeak was not taken under a provider unit. Cited for the next PR; it sizes nothing here.Evidence
claim_batch --source-root dag --source-root src/v2 --entry dag/test/claim/compute/work_class_grant_witness_test.dag --functions <all 13>— 13 PASS at this head.Every control was mutated and shown to go red. The absence and format-standing mutations were run as a matrix, one collapse per cause, because a single direction looks like confirmation:
…summarys_last_lines…an_absent_peak_is_not_reported…a_grant_is_the_largest_sample…work_class_minimum_samples2 → 1a_grant_is_the_largest_sample…only_an_oom_kill_below_the_ceiling…with_the_shipped_rows_every_class_reserves_the_ceilingCaptureEmptythe_peak_is_unreported_by_absence…LineAbsentan_empty_capture_is_reported_as_capture_empty…--quietfolda_quiet_launcher_reports_no_peak…an_unread_major_refuses…an_unread_major_refuses…the_grounding_recursion_terminates…an_unread_major_refuses…One limit, stated rather than omitted: the
Groundedarm has no single-claim collapse. Negating it means emptying the grounded set, which disables every fixture and reds broadly — a capability removal, not a collapse to a sibling cause.Not executed, stated plainly
The real route — a provider unit on srv1 that emits the summary, is parsed, is OOM-killed under a sub-ceiling grant and retried — has not been run. No container here has systemd (PID 1 is tini) and I have no host access.
What that does and does not leave uncertain, at its real size: the format is grounded in a versioned external authority (
run.c,format-util.hat v255) and independently re-verified against upstream — guard, emit, formatter flags, truncation arithmetic and line order. What is unverified is that srv1's manager emits it: its version, and the real bytes. An escalation is open forsystemctl --versionplus two probe stderr blocks; the version is requested with the bytes because the citation is at v255 and does not transfer.Why this lands anyway, which is the obvious question: no class has a grant, every class reserves the ceiling, and the ceiling is the fail-closed arm and it is reachable. The producer refuses correctly with no sample — an absent peak is
NotReportedand never 0, an unread major refuses, an unrecordable exceedance refuses the retry. The first real sample therefore changes what this reports, not whether it is safe, and the sized-grant arm it unlocks is unreachable in production today becausework_class_grant_rowsis empty. That gap gates the next PR's first real sample, not this one's refusals.🤖 Generated with Claude Code