Repository navigation
Pkg4 lifecycle: the attempt slot on the real route, and a door out for a wedged seat - #12040
Merged
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>
…n and the
recovery trigger
Not the finished package -- this is the spine that criteria 1, 2, 3, 4 and 6
rest on, with its controls. The provider is not wired to it yet (5 and 7 are
next), so nothing in PR 1's behaviour changes.
THE ATTEMPT SLOT. One durable CAS slot per attempt, keyed by the reservation
reference, on gunbc.durable_cas_file_store. Its value is the attempt record:
identity, reference, UNIT NAME, granted amount, launch deadline, state.
(3) THE LAUNCH IS CAS-GATED AND THAT IS ONE STEP. The producer advances
Reserved -> Launching expecting the generation it read; recovery advances
Reserved -> Terminal expecting the SAME generation. The store admits exactly
one, and the losing PRODUCER has not spawned yet -- the refusal arrives
before the launch, which is the difference between a gate and a regret. Both
interleavings are driven on a real store: terminate-then-launch (producer
refused, slot stays terminal) and launch-then-terminate (recovery refused,
slot stays launching).
(2) The unit name is READ from the record the attempt wrote, never derived from
the identity or a path spelling -- a derived name is a second authority for
the binding, and a wrong derivation stops somebody else's unit.
(1) FIVE ARMS, NOT FOUR, and the count is a consequence rather than a target
(ruling, loyal-swift-608). Folding authoritative absence into a failure arm
would have spent a distinction PR 1 landed: "the manager has no record of
this unit" and "the attempt failed" are different facts with different
evidence, and only the first is safe to free a seat on WITHOUT an attempt
record to consult. So TerminatedCauseUnknown carries it under a name that
says what it is. Each arm's refusal is asserted individually.
(4) Unreadable is never absent, at the slot and at the record: an undecodable
record is AttemptSlotUnreadable, and a state word this fold does not know is
unreadable rather than defaulted -- a future state must not read as Reserved,
which is the one state a launch may proceed from.
(6) Settling carries the verdict AND why, and the generation-suffixed store
keeps what it settled: the reserved and launching generations are still
readable after the terminal one lands.
THE GAP THE GATE DOES NOT CLOSE, AND THE TRIGGER THAT DOES. A compare-and-set
decides who WINS a race; it says nothing about whether recovery should have
entered one. A live producer that has not yet reached its CAS sits in Reserved --
exactly what an impatient recovery would terminate -- and the CAS then makes that
outcome look CORRECT: the producer refuses, releases, and the system appears to
work while a legitimate attempt was killed by a bystander.
So the trigger splits on the state, structurally rather than by policy. In
Reserved there is NO UNIT TO OBSERVE, so observation cannot distinguish a
pre-launch producer from a dead one -- both present the same absence -- and the
trigger is TEMPORAL, bounded by the deadline the producer itself declared when it
opened. In Launching the unit exists, so the trigger is the five-arm observation
with criterion 4 in full: only the three ended arms may terminate.
Eight wet controls pass against a real generation-file store.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…s named Both gaps closed before the provider is wired to the trigger rather than after, because both are about the thing that is about to become load-bearing. THE DEADLINE IS DECLARED BY THE PARTY IT PROTECTS. A producer says what it needs for checkout and argv assembly, and that same declaration is what stops anyone reclaiming its seat -- so nothing stopped it declaring an hour. The cost does not land on the producer: it lands on every other contender on the host as a seat nobody may reclaim, which is DESIGN 5's externalization exactly -- an accepted risk re-exported to another principal while the contract keeps its name. Ceiling: 300 seconds, and it is an AUTHORED POLICY BUDGET, not a measurement. What the window covers is one `git worktree add` of this repository plus argv assembly; the srv1 receipts show whole attempts including checkout at about four minutes, so five minutes for the checkout alone is generous by a wide margin and still bounded. When a measured checkout distribution exists this row is re-derived from it rather than defended. IT REFUSES, IT DOES NOT CLAMP. Clamping would admit the attempt under a bound it did not ask for and then reclaim its seat mid-checkout -- a widen wearing a safety limit's clothes. The refusal names both numbers so the author learns the ceiling instead of meeting it as a mysterious reclaim. A deadline that precedes the opening instant refuses too: a window already closed is reclaimable the moment it is written. WHICH CLOCK, AND WHY IT IS SAFE HERE. The host's own epoch clock, and for two reasons rather than convenience: the compute pool is host-local by construction -- PR 1 placed its ledger on the host precisely because a host's memory is not a fleet fact -- so both principals read one clock; and the pool's lease terms are already denominated in these same epoch seconds, so a second source here would be a second time authority for one quantity. The store offers no ordering to prefer: its generations order TRANSITIONS, not elapsed time. BOTH STEP DIRECTIONS NAMED, AND THE DANGEROUS-SOUNDING ONE IS BOUNDED BY THE GATE RATHER THAN THE CLOCK. Forward makes recovery fire late: the seat stays charged, the fail-closed direction, costing throughput. Backward makes it fire early against a live pre-launch producer -- and that does NOT produce an unbacked launch, because the producer's gate CAS then expects a generation recovery has moved and it is refused before it spawns. The loss is the attempt, not the invariant: a retry, not a seat handed to two holders. The deadline decides who may ENTER the race; the compare-and-set decides who wins it, and only the second is load-bearing for safety. Nine wet controls pass, including the ceiling refusing at one second over and admitting at exactly the ceiling. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…d grep
that missed them
review 69769. Generalizing SeatRequest to SeatRequest<Q, S> left
gunbc.instruments.fabric_seat_probe (3 sites) and
gunbc.instruments.fabric_event_log_probe (3 sites) passing a bare `amount: 1`.
Both are operator-invoked entry points, so nothing in the required gate compiles
them and the breakage would have stayed silent until somebody ran the probe --
which is exactly the case DESIGN 3 legislates for: "for a root outside the gate,
enumerate the consumers by name before you delete".
THE CAUSE IS THE ENUMERATION, NOT THE EDIT. I did enumerate the consumers, and
then piped the enumeration through `head -12` and acted on what survived the
truncation. A capped list is not a population; it is a list that has already
agreed with whatever I was about to do. The re-run is unfiltered and uncapped:
six construction sites, all six now carrying Measure { count: 1 }, and zero bare
ones left anywhere in dag or src/v2.
The PoolAcquired wire record in fabric_event_log_probe deliberately keeps its
bare Nat, for the reason already recorded on that field: its dimension is the
partition's and is restored at both ends from the pool's parameters.
Verified: both instrument closures compile with 0 blocking errors, which is the
check that did not exist for them before -- nothing routinely compiles these, so
the compile is the enumeration's receipt rather than a formality.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…the probes Asked for by the owning manager after review 69769, and filed for the SHAPE rather than the instance: the invalid state is a census whose denominator was silently reduced by the reading tool and then used to justify a deletion or a re-signature. THE SHARP EDGE IS THAT IT DOES NOT FAIL RANDOMLY. A cap fails toward the consumers nothing else would catch: a module with few mentions sorts to the bottom and is cut first, and having few mentions is exactly what makes it unlikely to be caught by any other route. The arms the cap hides are POSITIVELY CORRELATED with the arms that matter. WHY IT SURVIVES REVIEW: incompleteness is a property of the READING, not of the diff. Every migrated site is correct, the typechecker is silent because the missed consumers are outside the gate's closure, and the enumeration itself is not an artifact anybody reviews -- it happened in a shell and left no trace. Re-running it uncapped is the only thing that finds it. DISCRIMINATOR, phrased as a question about the enumeration rather than the diff: was the enumeration that justified this change itself UNBOUNDED? Not "did you check the consumers" -- the author of the specimen did check them. WHY IT IS NOT truncated_local_diagnostics_indistinguishable_from_the_complete_set, stated because the two look alike and the manager asked me to grow a row rather than split a class: there an ORACLE DIED mid-measure and nobody chose the truncation, so the discriminators are out of band -- an abort line, a missing receipt, a stack limit. Here the truncation is CHOSEN, by the reader, as a display convenience, on a population the reader is about to act on; there is no abort to notice and no receipt to be missing. Same silence, different cause, different discriminator, different remedy. TRIGGER NAMES THE CAPABILITY: a change that alters or removes a declaration is checked against the declaration's full consumer set derived from the namespace tree, consumers outside the required gate included by construction. Deliberately not "do not use head" -- a habit is not a wall, and the class would stay exactly as alive under a different paging tool. Filed on the lifecycle branch rather than PR 1, to keep PR 1's head still. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
review 69784. meminfo_line_metric took token 0 as the key and token 1 as the count and DISCARDED token 2 -- the `kB` the module's own annotation leans on. /proc/meminfo is not uniformly kB: four lines on every Linux host (HugePages_Total, HugePages_Free, HugePages_Rsvd, HugePages_Surp) carry NO unit because they are counts of PAGES, verified on this machine -- 54 lines, 4 without a unit, exactly the four named. Minting those as Kibibyte is wrong by the huge page size, 2048x at 2 MiB, and nothing in the type says so: a MemoryMetric carrying 0 pages and one carrying 0 KiB are indistinguishable. The seven named fields are all genuinely kB, so the admission arithmetic was never affected. What was wrong is the surface all_metrics and meminfo_metric_named expose to the next consumer. AND THE WITNESS LOCKED IT IN: count(all_metrics) == 8 against a fixture whose eighth line is `HugePages_Total: 0` -- it asserted the non-kB line WAS admitted. That is the second control in this change to pin the behaviour it existed to refuse, after the one that asserted completed+unknown frees a seat. Both were mine and both were written the same way: state what the code does, then assert it. THE UNIT IS NOW REQUIRED AND COMPARED, not discarded, and all_metrics is named for what it is -- the kB-denominated metrics, not every line. A page count is a different quantity and would need its own carrier; that is a row to add when a consumer exists, not a field to fake now. TWO FIXTURES BECAUSE TWO DIFFERENT PARTS OF THE FOLD EXCLUDE THEM, and finding the second is the reason the mutation was worth running. A UNITLESS line is excluded by the arity requirement. A line with the WRONG unit is excluded only by the comparison -- and nothing in /proc/meminfo authors that shape, so without a fixture the comparison was a permanently green decoration. Mutating the comparison away left the cell GREEN; with `SomeFutureField: 64 MB` added it goes FAIL. Restored and green again. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…iblings Side-chat verdict on #11962: one cited-module-absent, reported by the floor's declaration phase. a_held_compute_seat_has_no_in_corpus_discharge cited "test.claim.compute.work_request_witness"; the module declares itself "test.claim.compute.work_request_witness_test". The declaration it names is real and is in that module, so this is the string and nothing else. THE TRAP IS A NAMING INCONSISTENCY AMONG SIBLINGS, worth recording because the next citation will meet it too: host_capacity_wet_witness_test.dag declares `module test.claim.compute.host_capacity_wet_witness` and os_proc_meminfo_witness_test.dag declares `module test.claim.os_proc_meminfo_witness` -- both DROP the _test -- while work_request_witness_test.dag KEEPS it. A citation written from the pattern rather than from the file is wrong for exactly one file in the directory. So I audited rather than fixed the one: every module_path and decl_name in both rows this change adds, resolved against the real `module` lines and declarations. All resolve. It predates the approved baseline bf58075 -- no delta commit introduced it -- but it is a live declaration refusal inside this package, so it is fixed here rather than deferred. The census-image wet refusal is disposed nonblocking by the owning manager and is not touched. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two findings arrived at independently by two sessions within an hour, which is what makes the class worth a row rather than two apologies. a_control_that_shares_its_derivation_with_its_subject: a control whose content is DERIVED FROM the thing it is meant to discriminate cannot disagree with it. Two routes, and neither author recognised the other's until they were compared -- DESCRIBING (read what the code does, assert that) and COPYING (inline the production body with one input swapped). Copying is just the most literal way of writing a control from the implementation. Specimen one is mine, twice in one change: a meminfo witness that asserted the non-kB line WAS admitted, and a termination control that asserted completed-plus-unknown frees a seat. Specimen two is loyal-swift-608's on gunbc#12017: a RED carrying the production door's body inlined, so it evaluated its own copy of the test it existed to guard, with an annotation above it asserting the opposite in as many words. THE SMELL THAT NEEDS NO RUN, which is their contribution and is cheaper than the mutation: ASK WHAT THE CONTROL SHARES WITH ITS SUBJECT. If it re-derives, re-implements or re-describes the thing under test it is suspect before any mutation is attempted. The mutation is the proof; the shared-derivation question is what says to go looking. AND THE REPAIR HAS ITS OWN FAILURE MODE, which is the more transferable half: the first fix of specimen one added the missing unit comparison, and mutating that comparison away left the control STILL GREEN, because a unitless line is excluded by the ARITY requirement and /proc/meminfo publishes no wrong-unit line at all. THE FIXTURE POPULATION HAS TO CONTAIN THE CASE THE CHECK EXISTS FOR -- and a real-world corpus is exactly where that case tends not to occur, which is why the fixture is where it must be authored. Boundary against predicate_vacuously_true_on_an_empty_domain stated in the row: there the domain is empty, here it is populated and healthy-looking and merely lacks the one case. Also into an_enumeration_capped_by_its_reading_tool, a statement of the rule sharper than either the manager's or mine (reviewer on gunbc#11962): PRESERVE THE COMPLETE CONSUMER SET AS THE MIGRATION INPUT, AND CHECK EVERY AFFECTED OUT-OF-GATE ROOT FROM THAT SET; TRUNCATE ONLY ITS DISPLAY. That splits the legitimate cap from the illegitimate one, which neither "never truncate" nor "do not use head" manages: a cap on what you LOOK AT is how anyone reads a long list; a cap on what you ACT FROM is the defect. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
lease-drop contracts become one
(5) RE-CHECK UNDER THE LEASE, and the instance is concrete rather than
ceremonial. The stored-outcome attach was read BEFORE the producer lease
existed, which makes it evidence about a past world: between reading "no
stored outcome" and winning the lease, another producer can finish and
publish one. The first caller then re-produces work already done AND takes a
second reservation for an identity already satisfied -- the dedup the
contract promises, lost to a window nobody held anything across.
The observation is now re-taken while holding the lease and THAT one is the
decision. The early read is kept as an optimisation, so the common case --
an identity already built -- still answers without touching the lease at
all, and the annotation says which of the two decides.
(7) ONE LEASE-UNDROPPED CONTRACT, because there were THREE and they already
disagreed. compute_refused_unreserved turned a failed drop into a verdict
about the work (StoreUnavailable); compute_run_and_settle folded it into the
consumption note and did not; and the attach path added by (5) would have
needed a third. Three places deciding one fact is the DESIGN 3 fork, and the
thing to delete rather than to keep consistent by hand.
The contract, stated once and applied at every site: a lease that could not
be dropped NEVER changes what the work did. It is a host-operational fact, it
rides as a HostRecordLost so the caller hears it without the stored record
being contradicted, and the remedy is an operator removing the name.
compute_drop_producer_lease is now the only caller of Filesystem.Delete on
the lease path.
Also carried here, on the owning manager's instruction not to push it to PR 1:
the duplicated annotation fragment review 69814 noted at work_provider_local
line 783. Pushing a comment typo to PR 1 would restart CI and invalidate an
APPROVE that already sits on its head -- the whole tally for one character class
of edit.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…-pkg4-lifecycle # Conflicts: # dag/gunbc/compute/work_provider_local.dag
…or out The gate is now ON the real route: reserve, open the attempt, check out, ASK, spawn. The ask sits last because the window the launch deadline protects IS the checkout -- with it immediately after the open, the two compare-and-sets are microseconds apart and the interleaving the gate exists to refuse cannot occur on the real route, so the wall would have been permanently green by construction. compute_recover_cli is the discharge the seat had no route to. It reads the attempt slot, observes the unit through the manager and its cgroup, evaluates the recovery trigger, and commits the terminal generation EXPECTING the generation it read -- so a producer that advanced meanwhile wins and the recovery is refused by the store rather than by noticing afterwards. unit_population is narrowed to the two readings it uses. Recovery previously had to construct the producer's whole observation record, which carries attempt_completed -- a first-hand fact recovery cannot have. Recovery now has no carrier for first-hand completion anywhere on its route, so the distinction is unwritable rather than unwritten. RecoverySettledButHeld separates the terminal transition landing from the seat coming back. A recovery whose release the ledger refuses closes the attempt and leaves the memory charged, and says so with a nonzero exit. a_held_compute_seat_has_no_in_corpus_discharge records its trigger as fired and its rung as climbed rather than being deleted, and the refusal text that pointed at an unbuilt capability now names the door. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…dropped contract gets a control The consumption receipt's new "attempt:" line was rendered with host_record_wire, which returns the empty string on success because it is built to be appended to a sentence. The first real srv1 run at the wired head printed "attempt: " with nothing after it. A line that says nothing on the good path cannot be read as evidence the good path happened, which is why the line exists. work_request_witness_test was still calling compute_with_lost_host_record with the pre-refactor dropped_ok/dropped_error pair, so the file did not typecheck on this branch at all. It now takes the LeaseDrop carrier, and criterion 7 gets the control it was missing: an undropped producer lease is recorded, never becomes the work's verdict, and its note does not tell the operator something the contract contradicts. The AttemptState annotation now names what ENFORCES the entailment the temporal trigger rests on: compute_spawn_and_collect is reachable from exactly one place, so a slot reading "reserved" means nothing was ever spawned. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…he record, bare numbers only at the JSON boundary, and one host clock Review 69915 on gunbc#12040 found two sites; the sweep found the population. granted_kib: Int stripped the carrier the producer held (work_request's own note names the defect); compute_now_seconds reproduced gunbc.fabric_event_log_host now_epoch_seconds body-for-body while the annotation beside it named that authority. Both were annotations written from the right model with the code going the other way. The record now holds granted: Kibibyte and EpochSecs instants; RecoveryTooEarly and recovery_trigger take EpochSecs; the decode re-admits an instant and a grant (negative is unreadable, not cast); the Int? clock fork is deleted and both callers consume now_epoch_seconds, as host_capacity already did. granted was never read for a decision -- only serialized and re-decoded -- so this was a DESIGN 3 fork, not a live miscalculation. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… that can reach it Two items, both from review 69915's population rather than its two sites. THE SWEEP'S THIRD INSTANCE. compute_pre_launch_ceiling_seconds and compute_launch_window_seconds carried the unit in the field NAME on a bare Int, which is the same defect finding 1 named: modeled twice, in the name and in the rendered text, and nowhere the compiler can see. std.types Seconds is the carrier and is consumed corpus-wide -- gunbc.auth.access_request holds the identical ceiling/requested shape -- so both constants take it. THE ROUTE GAP, which is not a code defect and is answered by the contract home its own package already used. The hermetic route has no arm for shell.Mktemp.DirWithTemplate, so the floor plans this witness and it reaches no subject. gunbc#11962's host_capacity_wet_witness_test.dag admits exactly this effect and is disposed of by a pair: a gunbc.ci.ci_layer_roots WitnessExclusionRow under excl_local_repo_wet_tempdir_write_reason, and every one of its functions on v2.workflow.local_repo_wet_terminal local_repo_wet_schedule. This file takes the same pair. Not a floor_route_gap enrolment: the exclusion keeps the identities out of the hermetic discovery corpus rather than recording a gap as held debt, which is what the neighbour does and what the effect warrants. ALL NINE FUNCTIONS ARE ENROLLED, NOT THE GAPPED SUBSET, and the two measurements are the argument. The #12040 CI run named five identities; a hermetic claim_batch over this tree ends six that way and reaches three verdicts. Which claims get a verdict hermetically is a property of the evaluation order, not of the claim, so a subset roster would be right today and wrong after an edit nobody connects to it. Measured wet over this tree before enrollment, which is the receipt the roster's own idiom requires: attempt_lifecycle_wet_witness 9/9 and work_request_witness 10/10 PASS, 19/19, no FAIL. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
Review 69915 answered, plus the CI route gap — head
|
…ause is printed and the token still says FAIL The checkable question was whether the six route-gap lines carried their cause. THEY DID, verbatim: "FAIL <fn> (hermetic route has no arm for DirWithTemplate: operation declares no mock_response -- the claim never reached its subject, so this is a route gap and not a verdict)". So this is not the reporting layer distinguishing a gap on one path and conflating it on another; claim_batch says in words that the line is not a verdict. It says so AFTER the verdict token, which is the part worth filing: grep -c ^FAIL counts six reds, ^PASS reports three of nine, and the same nine are 9/9 with --wet over the same tree. FILED AS A RECEIPT ON AN EXISTING ROW RATHER THAN AS A NEW CLASS. gunbc.recurring_failure_mode an_unreached_measurement_renders_as_a_failed_one already owns this invalid state -- an unreached subject presented where adjudicated-and-lost is meant -- and a second row would be the section 3 fork the ledger exists to avoid. Only the grain moves, from a required lane at the merge surface to one identity inside a batch run. The two specimens bracket the remedy, which is why the second is worth keeping beside the first. The original has the distinction TYPED in a standing field the deciding surface never reads. This one has it RENDERED where every reader sees it and no reader can act on it mechanically. Neither is fixed by emitting more, which is what that row's trigger already says: the surface has to consume it. For a per-identity line the surface IS the token, so the remedy here is a token of its own, not a better parenthetical. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… terminal Per the parent's point on 9d9f074. The row said the cause was printed and left a reader to infer what follows from that. It now says it outright: this is NOT the harness conflating a route gap with a verdict -- the cause is computed, correct and rendered -- and what fails is that it is carried under a token that reads as a verdict. The remedy is therefore a distinct terminal, not more annotation, and an instruction to read the parenthetical is a mitigation carrying exactly the dependency on a human knowing to look that the row's own RUNG note names. Held out of the push that is currently building: a push cancels the in-flight floor run, and this is prose on a data row. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e roster Raised on the #12040/#12044 merge. Append-against-append resolves as a union, which is right when the two appended rows are independent and silently wrong when both sides appended the SAME identity -- git cannot see that, because both sides did the same legal thing, so the merge produces a green tree carrying a duplicate. The read that cleared that merge was an eye over 220 rows. NEITHER SIBLING CLAIM CAN SEE ONE, and the second is the interesting half. every_roster_row_spells_its_function_the_same_way_twice reads WITHIN a row. And the_local_roster_is_not_empty compares length(identities) == length(schedule), which is a map -- a map never changes a list's length, so that equality holds over a roster with a duplicate in it. It reads like a completeness check and is structurally incapable of being one. MEASURED RATHER THAN ARGUED. Duplicating one row in the real schedule: no_two_roster_rows_name_the_same_identity FAIL, the_local_roster_is_not_empty PASS, every_roster_row_spells_its_function_the_same_way_twice PASS. Restored tree: all three PASS. So the claim is wired to the roster and the reading above is the run's, not mine. the_duplicate_identity_predicate_discriminates is the second control and covers what the mutation cannot: the roster claim is a filter returning zero, and a filter over a predicate that never fires returns zero too. Two supplied lists differing only in whether one name repeats separate those. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 69967, and it is fabricated plausible output on a reachable path rather than a modeling point. compute_run_leased returns AttemptGateRefused when the launch CAS loses, compute_run_under_grant writes compute_attempt_settlement_wire into the consumption receipt, and the refusal mapped to HostRecordWritten -- so the operator-facing record of a LOST launch race asserted this producer settled the attempt slot, having settled nothing and observed nothing about the slot's final state. DESIGN section 5. THE CAUSE IS A THREE-VALUED FACT ON A TWO-ARMED CARRIER, so the third case had nowhere to go but the success arm. The fix is the third arm, and the argument is about WHOSE TYPE it belongs to. It is not on HostRecordStatus: that answers one question -- did this host record its own side facts, or is there a loss an operator must chase -- for five producers, and `nothing was owed here` is not an answer to it for any of the others. The arm would be uninhabitable everywhere but this call and would owe host_record_join and host_record_was_written a rule with no meaning to carry. So settlement gets AttemptSettlement (Settled / NotSettled / Unsettleable) and a total projection into the shared carrier. UNSETTLEABLE PROJECTS TO HostRecordWritten DELIBERATELY. A loss means this host owed a record and failed to write it, which is an operator action. A refused gate owed nothing: it never held the slot. Mapping it to HostRecordLost would manufacture an incident -- the same fabrication as the success arm, pointed the other way. CONTROL, driving the REAL race rather than describing it: two producers open against one store, the winner advances the generation, so the loser's begin_launch is refused BY THE STORE. PASS. Mutation restoring `AttemptGateRefused => AttemptSettled`: FAIL, on a clean run. An earlier mutation attempt was killed and is reported nowhere, because the tree was restored while it executed -- a run whose input changed under it has no verdict. ROUTE-GAP ENROLMENT, which is the other half of the CI red at 9d9f074. The exclusion row keeps this file off the floor on every run that does not touch it; a CHANGED witness is selected regardless of discovery exclusion, so the PR that edits it plans the identities anyway. floor_route_gap_expectation_chunk_21 enrols exactly the six that gapped, and the row names what re-observes it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
Round three + the CI red — head
|
# Conflicts: # src/v2/workflow/floor_route_gap.dag
Round four on gunbc#12040, verified at head d2be498 before acting on it. compute_recover_attempt occurs exactly twice in the tree: its definition, and one call from compute_recover_cli. The only test-side touch is a string_contains over the remedy TEXT, and DESIGN section 5 rules in those words that a typecheck and a .contains() grep are not consumers. The wet witnesses reach attempt_open, attempt_begin_launch and attempt_terminate; none reach this door. So the row's own trigger -- the capability CONSUMED BY A REAL CALLER -- was marked discharged while its own words went unmet. CURRENT RUNG GOES BACK TO MITIGATABLE, stated as a correction rather than left implied by the absence of a climb. Nothing regressed: the door is as good as it was and the evidence for it never existed. Section 4b(1) is the governing sentence, and rung inflation is worse than sitting low because an inflated class never ranks for climbing -- here the class that would stop being asked about is a compute seat nobody can reclaim. THE TRIGGER IS A CAPABILITY AND NOT A CHORE, because the control cannot be written today at any price. compute_recover_attempt takes a HostDashboardInstance and derives its attempts root from it, so no fixture can point the door anywhere but a real instance's real compute root -- a wet control over it would drive production, not the tempdir the harness already builds for every other attempt-lifecycle claim. The trigger is therefore a door whose STORE IS A PARAMETER, sufficient for an executing control to drive a held seat through discharge against a temporary store. Naming `write a test` would have been a trigger nobody could satisfy. The annotation at the door said the same thing in the second place and is corrected too. Leaving it is how the row got re-inflated once already. Also merges origin/main. The route-gap roster conflicted in the shape that is worth recording: main landed the SAME fix for host_capacity_wet_witness -- its header says gunbc#11962 shipped two of the three rows and the five identities blocked the merge queue for gunbc#11829 -- and both sides named the new function floor_route_gap_expectation_chunk_21. The two `chunks()` lines were textually identical, so git merged that line clean and left TWO definitions with ONE call site. Mine is renamed chunk_22 and both are registered; the enrolled identities were checked for duplicates separately. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…hould have said so was a count Review 70036 and the floor at 3a60e2c agree, which is as confirmed as a finding gets: the wet witness file holds TEN test fns and nine were enrolled. The tenth, the_loser_of_a_launch_race_never_reports_that_it_settled_the_slot, appeared only at its own definition -- and git grep AttemptUnsettleable returns exactly two files, so it is the SOLE EXECUTING CONTROL for the arm added in d2be498. The fabricated-settlement finding had been answered with a control that does not run, which is 4b(1)'s inert-lens case with the sting that it LOOKS like evidence in the diff. CI reported it as route_gap AND changed_witness_planned_without_terminal_verdict. ENROLLED IN BOTH ROSTERS, and the route-gap row is a PREDICTION rather than an observation -- a departure from that roster's own rule, said in the row. The claim's first statement is fresh_root(), which is DirWithTemplate unconditionally, so it cannot reach its subject hermetically under any order. THE CENSUS IS NOW A RULE, NOT A COUNT. It said NINE ATTEMPT-LIFECYCLE MEMBERS over a file that had grown to ten, and that is how the gap stayed invisible. Changing NINE to TEN would reproduce it on the next addition, so membership is stated as every test fn in the file, with the admitting property being the EFFECT. Same class as the route-gap roster's six-against-nine, in the other direction: there the honest form is an observation, here it is a policy. THE ROSTER-UNIQUENESS CLAIM IS LIFTED OUT, and the reasoning stays behind in the module so nobody pays for the wall twice. It costs 346735 eval steps against a 72300 new-witness budget, the overage is the pairwise comparison itself, and no construction here makes it linear -- the substrate has no set and no sort over String. A declared ceiling or a reduced subject are both decisions about a shared budget and belong to their own change, not to a compute-lifecycle PR four rounds deep. What it guards is real and unguarded: a duplicated schedule row survives a union merge silently, wet_forward_causes walks SCHEDULED so it finds the same terminal twice with n == 1 and raises nothing, and both sibling claims are structurally blind to it. AND THE MEASUREMENT FALSIFIED MY OWN REPAIR, which is the part worth keeping. I read the first version as rebuilding the roster projection inside the inner predicate and hoisted it. The figure moved 343406 -> 346735, the difference being one row the roster gained. The rebuilt projection was never the expense, and the structural story I told about it was wrong. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…mes nothing CI on 9eb96c4: 20 parse errors, one block, all 'source annotation names no subject: no module item follows it'. The REQUIRED-FLOOR refusal ArmSetConsumerPlanningUnavailable in the same run is downstream of the parse failure rather than a second defect -- no parse-phase declaration index reaches the floor when the module will not parse. The block is the reasoning about the roster-uniqueness claim this change lifted out. It went at the end of the file, and annotations are module-item grain: a block at EOF has no subject. It now sits above the roster claims it is about, which is also where a reader looking for the missing check would start. The indented-annotation grep that has been circulating passes this cleanly, because the block is at column 1. Both shapes need checking: grep -Hn '^[[:space:]]\+//' <file> awk '/^[[:space:]]*\/\//{c=NR;next} /^[[:space:]]*$/{next} {c=0} END{if(c) print FILENAME": trailing annotation at "c}' <file> Both now run clean over every file in this diff. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
compute_release_on folded SeatNotHeld into ComputeReleaseRefused through a catch-all arm, so a double release (recovery then producer) wrote outcome.json as STILL CHARGED with the stuck-reservation remedy. ComputeNothingToRelease is now its own arm, the three pre-grant arms use it, and every SeatRelease arm is named. The new wet claim releases one real seat twice and is enrolled in local_repo_wet_schedule; it holds, and goes red when SeatNotHeld is routed back to the refusal arm. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… no annotation is admitted Moved to the fn it explains (DESIGN §4c: // attaches only at module-item grain); emit-build refused it as 'source annotation sits inside a declaration body'. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…state words accepted it
Review 70244. AttemptTerminal.verdict is now AttemptVerdict = AttemptWorkEnded
{ ending: WorkEnding } | AttemptRecovered -- the two writers the slot has. WorkEnding
types the ending words work_outcome_ending already spelled (it now projects through
work_ending_wire, so there is one spelling). attempt_state_decode refuses a verdict
outside the set; RecoveryStateNotRecoverable carries the AttemptState. The witness's
'released' was never a word any producer wrote; it now uses real verdicts.
Control a_terminal_verdict_outside_the_closed_set_is_unreadable (enrolled in the wet
schedule) round-trips all six verdicts through the real record wire and decodes
'recoverd', 'released' and '' as unreadable. All 11 lifecycle claims hold; widening
an unknown verdict to Recovered turns the new claim false.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Review 70244 addressed at a2a19f9. The terminal verdict is now a typed |
…ted settlement (#12044) * A manager that cannot be asked is a property not queried: ShowUserProperty opts into ShellOutcome, and the two unit readings fold it before the fold decides Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The check that replaced a decoration was a decoration too, and only the mutation said so Review 69970, both findings, plus one the review did not name and one my own first repair introduced. FINDING 1, the borrowed exclusion reason. The row reused excl_shell_spawn_refused_reason, which substantiates a DIFFERENT subject in its own words -- whether the host can spawn argv[0], one effect, a local program. This witness's subject is a systemd user manager, four unit properties and a cgroup read. DESIGN 3b: a home that resolves but owns only part of the scope a row claims is a scope mismatch on the row. It now has excl_manager_unaskable_reason and its own dissolution, which also states what a PARTIAL mock does not discharge. Returning the borrowed row repaired its own sentence: `this row and its four schedule rows delete together` is true again. FINDING 2, the decoration. On the one lane this cell runs (srv1, systemctl present) the claim was `if present { true }` and the pre-change behaviour was identical, so nothing on the executing path could turn it red. The subject was FUSED TO THE EFFECT -- observable only where systemd is absent. unit_property_ from_shell is now its own fold, so both ShellOutcome arms are authorable anywhere, and the wet claim keeps the inhabitance half with something real to assert on the present-manager branch. THE THIRD PROBLEM, WHICH IS FINDING 2 ONE MOVE ALONG. The new hermetic claim was sitting in a DISCOVERY-EXCLUDED file, so it would have executed on the change that wrote it and never again. Exclusion silently converts `always runs` into `runs when this file changes`, which is invisible at the call site and reads as coverage. The fold's claim moved to work_request_witness, discovered every run; the wet file keeps only what needs a host, and says why the split is where it is. THE FOURTH, AND IT IS MINE. The relocated claim PASSED against a fold mutated to `ShellSpawnRefused => { queried: success, value: value }` -- the wrong arm that reads the flag instead of the outcome. I had supplied that arm with success: false and an empty value, so the correct fold and the wrong one produced the SAME reading and the claim carried no information. Right interface, right layer, right assertions, zero discrimination. The separating input is a refusal with a FLATTERING FLAG -- success: true, value: "active" -- because the contract is that the OUTCOME decides: a spawn that produced no process is not a reading whatever the transport's other fields say. CONTROLS at this head: mutation FAIL, restored PASS, and the wet inhabitance cell PASS. The reasoning about the inputs is in the claim rather than here, because the next person to edit them is the one who needs it. Also merges the current gunbc#12040 head. Chunk names did not collide this time (21/22 against 23) and all four checks ran: no duplicate name, 24 definitions against 24 registered members, no duplicate identity, module resolves. 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>
…otation is admitted Hoisted above the test fn (DESIGN 4c). Swept every .dag file in the PR's diff for an indented // line; this was the only one. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
6 tasks
…enrolled DirWithTemplate route gap releasing_one_seat_twice_is_not_a_ledger_failure_and_charges_nothing landed with its WetScheduledClaim row but no floor_route_gap row; floor job 106999407163 read route_gap_unenrolled=1 while the local-repo wet lane passed it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ough the attempt gate The retry opens its own slot under compute_ceiling_retry_reference and asks before spawning; the first attempt is settled in its slot before the retry opens. ComputeAttempt carries the gate (LeasedRun folded into it). Imports are the union. Adds a wet witness that a held retry slot refuses the retry before spawn. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…mplate route-gap row The floor at bf63e3c reported it as an unenrolled route gap (fresh_root is DirWithTemplate); the file's LocalRepoWetLane exclusion already covers it by pattern. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
6 tasks
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
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.
Pkg4 lifecycle: the attempt slot on the real route, and a door out for a wedged seat
Subject. One compute attempt on one qualified host: the state it is in between reserving
memory and releasing it, who may act on it, and how a seat comes back when the run that took it
cannot give it back.
Implementation boundary.
gunbc.compute.attempt_lifecycle(the attempt slot, its transitionsand the recovery trigger) and
gunbc.compute.work_provider_local(the provider route that nowopens, gates and settles the slot, plus the recovery door). No new task format, no parallel
framework, no seed or V1 fallback.
product.capacity's pool andgunbc.durable_cas_file_store'scompare-and-set are consumed as they stand; nothing here redeclares either.
What it replaces. Nothing is deleted. gunbc#11962 landed admission and release and DECLARED
what it could not do --
gunbc.recurring_failure_mode a_held_compute_seat_has_no_in_corpus_discharge,whose trigger named a lifecycle capability with four properties. This is that capability. The row
is updated rather than deleted: the class still exists, its rung climbed, and the trigger is
recorded as fired. The refusal text that pointed at an unbuilt capability now names the door.
The route, and where the gate sits in it
The ask is last, and that placement is the whole reason a control exists. It was first written
immediately after the open, which reads correctly and is wrong: the window the launch deadline
protects IS the checkout, so with the ask adjacent to the open the two compare-and-sets are
microseconds apart and the interleaving the gate exists to refuse cannot occur on the real route.
The wall would have been permanently green by construction -- DESIGN §4b's question, is the RED
authorable, answered by trying to build the control rather than by reasoning about semantics.
Measured on srv1 at this head, the window is about one second of
git worktree add(generation 1at 02:44:38.843, checkout complete at 02:44:39.808, generation 2 at 02:44:39.873, unit after
that). It is short and it is real, and it is reported as measured rather than described as large.
One honest limit: an attempt whose checkout is already present has a near-zero window. That is
harmless -- recovery declines inside the declared deadline regardless -- but it means the race is
only reachable on a fresh checkout, which is how the control below is staged.
The seven criteria, each with the mutation that makes a control go red
Every row's mutation was RUN, not described. The mutation edits are one anchored replacement each
and are listed with the finding so a reviewer can re-apply them.
the_lifecycle_verdict_has_four_states_and_unknown_carries_whythe_unit_binding_is_read_back_from_the_record_the_attempt_wrotean_undecodable_slot_is_unreadable_and_never_absenta_launch_that_won_refuses_a_recovery_arriving_behind_itsettling_records_why_and_does_not_erase_what_it_settledan_undropped_lease_is_recorded_and_never_becomes_the_works_verdictWhat the recovery door is, and why it has arms that look pessimistic
compute_recover_cli repo_root reference receipt_path. It reads the attempt slot, observes theunit through the manager and its cgroup, evaluates the trigger, and commits the terminal generation
expecting the generation it read. Four things it will not do, each because the opposite frees a
seat that should stay held:
opposite facts with opposite remedies. Collapsing them is §5's absorbing fallback exactly.
producer wrote, never from the identity, a path spelling or a listing. A recovery acting on a
name it invented can stop a unit belonging to a different attempt.
deadline it asked for is not dead, and the refusal says so with both numbers.
UnitLifecyclehas no first-handcompletion arm, and since this change
unit_populationtakes the two readings it uses ratherthan the producer's whole observation record -- so recovery has no carrier for
attempt_completedanywhere on its route. That was true by convention before and is true by construction now.
RecoverySettledButHeldis the arm that keeps the door honest. The terminal transition landingand the seat coming back are two facts. A recovery whose release the ledger refuses closes the
attempt and leaves the memory charged; it exits nonzero and says the host under-admits by that
grant until a release is taken for that reference. Reporting that as success would re-create the
class this change exists to close, under a name that reads as fixed.
Exact-head handback
Head at handback:
17e06b6b2516e59c43563370382ee78837e8a683.Re-validated at this head in this session (local
claim_batch --wet, one dispatch per module):dag/test/claim/compute/attempt_lifecycle_wet_witness_test.dag— 9/9 PASS.dag/test/claim/compute/work_request_witness_test.dag— 10/10 PASS, after the lastcommit repaired one conjunct that was RED at the previous head.
What was red, and why the repair is on the claim rather than the note.
an_undropped_lease_is_recorded_and_never_becomes_the_works_verdictasserted that thestale-lease note contains no
ProducerInFlightanywhere. The note's repair earlier in thisbranch was to SCOPE that sentence, not remove the word: a caller reaching a published success
ATTACHES before the name is consulted, and the name still refuses a request that must PRODUCE
again. The claim therefore forbade more than the contract requires (DESIGN §4d,
over-prohibition) and went red against correct text. It now asserts the two clauses that carry
the scope, so an unconditional note is still red.
One control is owed and was NOT run. The mutation for that repaired conjunct — reverting the
note to the unconditional "the next request will refuse as ProducerInFlight" and confirming the
cell goes red — was started and interrupted by session closeout, so it has no verdict. Treat it
as outstanding: it is one anchored replacement in
gunbc.compute.work_provider_localcompute_stale_lease_note, and the working tree was restored. Every other row's mutation in thetable above was run.