Skip to content

Pkg4: resource-admitted execution on one host - #11962

Merged
gunbai-bot[bot] merged 19 commits into
mainfrom
session/bold-lynx-559
Sep 22, 2026
Merged

gunbai-bot[bot] merged 19 commits into
mainfrom
session/bold-lynx-559

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 21, 2026 •

Copy link
Copy Markdown
Contributor

This PR is admission + pool. Lifecycle/recovery is PR 2 (split approved by the manager, 2026-09-21). The reason is safety, not workload: without a recovery route every lifecycle defect degrades to the seat stays charged — the host under-admits and nothing is over-promised. With a half-built one, the same defects free seats that should not be freed. The gap is declared as a rostered failure mode with a capability trigger, not left implied. Head: 5ee0cceea8922117e09a0e86670527e20864c9e2.

Subject

Admission of a compute work request on ONE host against observed memory capacity, through an atomic reservation. Home domain: fabric/compute + the leasing rows of DESIGN §3b.

What was wrong

gunbc.compute.work_provider_local admitted work by listing its lease directory, comparing the count against compute_cold_build_cap = 2, then creating a lease for this identity.

  1. It was not atomic. The list and the create are two operations on different names, and the create's O_EXCL excludes a second producer of the same identity. Two requests with different identities both read one lease in flight, both compared 1 < 2, and both created their own lease — the cap admitted three. No exclusive create of any path excludes a quantity.
  2. 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 differing fourfold, and a class needing a gibibyte was charged the same as a release build.

Implementation boundary

New gunbc.compute.host_capacity — and it coins no capacity vocabulary. The homes DESIGN §3b already names for this domain do the work:

  • product.capacity.pool — appropriation, encumbrance, term, release law
  • product.capacity.pool_events — SeatRequest, PoolAcquired, PoolReleased
  • gunbc.fabric_event_log — one compare-and-set per append against the partition head. That is what makes the reservation atomic across competing requests rather than merely checked.

This module declares which pool (the host's compute appropriation), where it linearizes, and joins it to the observation.

Linearized on this host, not the fleet DB. gunbc.fabric_storage_placement places the fabric DB on srv1 because an upstream rate limit is metered on a credential that every host contends for. A host's own memory is not such a fact — every contender is local — so routing it through another machine would refuse a local build when that machine was unreachable, a refusal that is not about capacity at all. Same realization (gunbc.fabric_storage_file_store, whose exclusive create supplies the linearization), rooted under this host's own compute root; the partition names the instance.

Two readings, joined in one comparison — not two checks. MemTotal is installed memory and does not move; MemAvailable is what is free right now, including everything outside this pool. They are not independent tests, and making them independent was the first design defect: the ceiling an attempt is adjudicated against is min(appropriation, observed available), evaluated inside the same CAS'd fold that computes the pool's committed total. So "everything this pool has promised, plus what I am asking for, must fit in what the machine actually has" is one predicate in one linearized step. Read through a new linux.Procfs.ReadMeminfo operation (one op per file, as the service already requires) and a parse that lives with the fields' owner, extdeps.linux.proc_meminfo.

The bound 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 of outstanding grants — observable, since each runs in a named transient unit with its own cgroup — and that is a declared frontier with its trigger, not a silent approximation.

The pool is a host's, and is keyed by the host. srv1 declares two dashboard instances (srv1-live, srv1-lab) with different ids and different roots, spending one machine's memory. Both the partition and the ledger root are keyed by host identity, resolved through dashboard_instance_for_host — the same host-to-instance authority the fabric event log already uses, rather than a new host-scoped path. A host that authority cannot resolve reserves nothing.

The grant is the enforcement. The transient unit's MemoryMax is now the amount the pool reserved, not a ceiling read independently from the instance. A reservation of X that caps the unit at Y is arithmetic about a number nothing enforces.

Release law is QuiescenceRequired, deliberately. A running cargo honours no fence, so an expired term frees nothing and the seat returns only by explicit release. A worker that dies wedges its own share rather than silently handing it to the next arrival — the only direction that cannot oversubscribe a machine. Completion and cancellation are the same transition with different reasons, and every ending of compute_run_leased reaches it.

Release is gated on evidence about the unit, not on the launcher's exit. systemd-run --wait is a launcher, not the unit's parent, so a launcher killed or timed out returns failure while the unit keeps running — and releasing on that would hand a live build's memory to the next arrival. The decision is four-valued over evidence the repo already models: authoritative absence (LoadState=not-found, the wire value this corpus reads positively), observed termination (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 — a lost launcher, an unreadable manager and a missing cgroup all look like it.

The discharge gap is declared, not implied. A release that cannot be proven safe leaves the seat charged, and this PR ships no route to give it back. That is filed as gunbc.recurring_failure_mode a_held_compute_seat_has_no_in_corpus_discharge — a new class, not a §4b(3) rung drop, because no discharge existed on main either (admission was a count of lease files; there were no reservations at all). Its trigger names PR 2's capability, and its remedy sentence reaches the caller through compute_stuck_reservation_remedy.

Positive control — real execution

test.claim.compute.host_capacity_wet_witness (five cells), enrolled on the local-repo wet lane (ci_layer_roots exclusion row and v2.workflow.local_repo_wet_terminal local_repo_wet_schedule, which joins both directions). Real appends to a real event log on a real temp directory, decided against a real reading of this machine's /proc/meminfo.

claim_batch --wet --source-root dag --source-root src/v2 \
  --entry dag/test/claim/compute/host_capacity_wet_witness_test.dag --functions <all five>
PASS competing_reservations_cannot_over_reserve_and_a_release_returns_the_capacity
PASS a_request_the_machine_cannot_back_refuses_below_the_live_floor
PASS an_appropriation_larger_than_the_machine_refuses_rather_than_admitting
PASS the_deployment_join_roots_the_ledger_under_the_instance_compute_root
PASS a_reused_reference_is_a_ledger_refusal_and_never_reported_as_a_full_pool

A 2 GiB pool admits two 1 GiB reservations and refuses the third; the standing then reads 2 GiB committed; the release returns exactly what it held; the next request is admitted again. A request the machine cannot back is refused below the floor with the ledger untouched — a different fact from a full pool, with a different remedy. An appropriation larger than the machine refuses outright rather than presenting hours later as a kernel kill.

The subject is supplied (four values, rather than standing up a deployment record to add two numbers); the fourth cell is its inhabitance claim and asserts the route: the real producer compute_capacity_subject roots the ledger under that instance's own compute root and names it in the partition.

Failure / mutation control — goes red

Raise the appropriation from 2 × to 4 × the request and re-run the first cell:

FAIL competing_reservations_cannot_over_reserve_and_a_release_returns_the_capacity

The third reservation is admitted. Reverted in this branch. This is precisely the behaviour the deleted count-based admission had whenever the two lease files belonged to different identities.

Also test.claim.os_proc_meminfo_witness parsing_meminfo_reads_the_named_fields_and_refuses_a_missing_one (PASS): a field the kernel did not publish reads as MeminfoFieldAbsent, never as a zero — a host with no MemAvailable line would otherwise present as a host with no memory available and refuse forever for the wrong reason.

Disposition of what it replaces

  • compute_cold_build_cap — deleted. Its fact is HostComputeCapacityFull, measured in the bytes the count was implicitly worth: the appropriation is 2 × dispatch_worker_memory_max, exactly the memory two producers under the worker ceiling admitted. Nothing is widened; a class needing less than a ceiling now admits more requests than a count ever could.
  • HostAtColdBuildCap { in_flight, cap } — deleted, replaced by three arms, because one arm for three remedies is the conflation §5 forbids: a full pool (wait), the machine's live availability (find out who else is on the host), an unreadable ledger (repair the store).
  • compute_count_lines — deleted with its only caller.
  • gunbc.harness.harness_guidance's decl_ref to the deleted row is repaired to compute_reserve, the admission that now withholds the capability.
  • fabric_seat_acquire / fabric_seat_observe / seat_attempt generalize over the measure — memory is not a dimensionless count. Pure signature change; the folds beneath were already generic.
  • The observe/append/retry loop gunbc.fabric_quota held alone moves to the carrier that owns partition appends (fabric_pool_event_append), and quota settlement is migrated onto it rather than a second copy growing beside it, free to disagree about how a contended head is retried.
  • std.measure kibibyte_from_byte_size_floor — the flooring inverse of kibibyte_to_byte_size. Floor, because rounding a capacity up reports a ceiling the host does not have.

Stated divergences from the brief (DESIGN §3b's middle value)

  1. Memory-only is the correct choice, and the manager has confirmed it: the operator ruling of 2026-09-19 stands and TAKES PRECEDENCE OVER THE BRIEF'S "or CPU" (neat-boar-16, 2026-09-21). gunbc.runner_slot_allocation's terminal disposition records that ruling — "there is no CPU demand - the processes we run are single core - do NOT overthink it please" — under which cores_per_slot is an authored policy, the CPU axis stops binding on every host, and cpu_quota is deliberately SlotCpuQuotaUnbounded because a finite quota would throttle parallel link/codegen. Adding a CPU reservation pool would contradict that standing ruling. I built a /proc/stat hardware-thread reader for it and reverted it rather than land a declaration with no honest consumer (§3c). If the manager wants the CPU axis reserved, that ruling is what has to move first.
  2. The real workload under the grant has now run on srv1 — see the section above. This is no longer an open item. compute_run_unit refuses without systemd-run, and this session's container has no systemd and no route to a qualified host. What executed here is the admission, reservation, release and standing — the real path the provider calls — against real files and a real host reading. The remaining step is one run of gunbc run … compute_request_cli (or the worker-facing gunbc.compute.test_run test_pattern_cli) on srv1/srv2, which will write the aggregate consumption reading this change starts recording: the ledger's committed total beside the machine's own availability, read while the grant is still held. Their disagreement is the signal — committed far above the machine's shortfall means every class is over-reserving, which is the measurement that retires the declared frontier below.

The real run on srv1 — and the four defects it found

Run from this session over the fleet SSH route against the srv1 live instance (/opt/gunbc/gunbc, 502 GiB installed, ~400 GiB available). The gunbc run driver itself had to be placed in a cgroup-bound scope first, because gunbc.host_budget_source refuses to plan against a host-shared memory reading — a wall I respected rather than routed around.

The chain, both classes, each under its own grant:

Re-run in full at the final head 725d9c58620b, after the design changed, because a receipt from a superseded design is not a receipt for this one:

identity operation grant unit runtime unit peak ending
ab9e86ae4c6c0945 build:release:gunbc,claim_batch 27262976 KiB — — succeeded
e4b178f9785733a2 compile:dag/gunbc/compute/work_request.dag 27262976 KiB — — succeeded

Re-taken again at 5ee0cceea89 after the settlement gate changed, because a conservative gate that fails to release would wedge a seat on every run. It does not:

unit: absent (gunbc-compute-ab9e86ae4c6c0945 LoadState=not-found)
reservation: released ab9e86ae4c6c0945@2026-09-21T18:08:04Z (work succeeded, unit absent ...)
leases remaining: 0

The happy path releases on the strongest arm — the transient unit is collected by --wait, so the manager authoritatively reports it absent — and the evidence is carried into the durable record rather than assumed. An earlier run at 725d9c58 measured the peaks: build 4m13s peaking 4.0 G against a 26 GiB grant, compile 3m05s.

The compile attached to the build's stored success and ran the gunbc that build produced, which is the contract's "two callers, one build" executing on a real host.

The grant is the enforcement, byte-exact. Read off the live unit while it held the grant:

PoolAcquired  amount = 27262976 KiB   term_seconds = 7200
systemd       MemoryMax = 27917287424 bytes      (= 27262976 × 1024)
unit          gunbc-compute-<identity>.service
              /home/briansrls/.cargo/bin/cargo build --release -p v1-compiler --bin gunbc --bin claim_batch

The partition is host-keyed in production, which is fix (B) observed rather than asserted: compute-memory-srv1, not the instance id it used to carry.

Aggregate consumption, recorded beside each outcome while the grant was held:

committed 27262976 KiB of 54525952 KiB (headroom 27262976 KiB);
host reports 429358428 KiB available of 526641732 KiB installed

And the disagreement the design says to read: the build reserved 26 GiB and peaked at 4.0 GiB. That is the over-reservation signal, now measured rather than predicted, and it is exactly what retires the per-class frontier below.

The event chain, four generations, references per attempt:

acquired  82fbbb6139f7c955@2026-09-21T16:37:55Z  27262976
released  82fbbb6139f7c955@2026-09-21T16:37:55Z            reason="work succeeded"
acquired  f769cd349545ce08@2026-09-21T16:42:10Z  27262976
released  f769cd349545ce08@2026-09-21T16:42:10Z            reason="work succeeded"

Leases remaining afterwards: 0. srv1 cleaned up (compute root emptied, provider worktrees pruned, scratch checkout removed).

What the run found — the case for having insisted on it

(These four were found at 3e3b72c02fa / 047bb3eade1; the four design defects above them were found by review at dd240f0d171f. All eight are fixed at the head this receipt was taken on.)

Every one of these was invisible to the hermetic and wet evidence, because none of that evidence touches 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" was silently dead. Measured directly: the provider's own dependent compile refused with dependency … ended refused_by_infrastructure on a build that had in fact succeeded. The reading now has its own file beside the log; a realization's measurement does not get to 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 one 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 the caller as "capacity full" on a host with 400 GiB free. product.capacity.pool_events now names the marker it writes (pool_full_wire) so both sides read one authority, and anything else is carried through as a ledger refusal. 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.
  4. 14 blocking compile errors on a module every witness called green. DESIGN §4c admits annotation blocks at module-item grain only. The interpreter route the witnesses run on tolerates a block inside a function body; gunbc compile refuses it. work_provider_local had stopped compiling and nothing in the hermetic or wet evidence could see it. Prose moved above the declaration it describes; gunbc compile --entry dag/gunbc/compute/work_provider_local.dag now reports 0 blocking errors, against 14 before.

Declared gaps, each with its trigger

Two are rostered failure modes rather than frontiers, because they name states this change makes reachable rather than work it defers.

  • A held compute seat has no in-corpus discharge. A reservation whose release does not land stays charged, and this PR ships no route to give it back — the lifecycle capability is PR 2. Filed as gunbc.recurring_failure_mode a_held_compute_seat_has_no_in_corpus_discharge, a new class rather than a §4b(3) rung drop, because no discharge existed on main either: admission was a count of lease files and there were no reservations at all. Trigger names PR 2's capability in four parts. Its remedy sentence reaches the caller through compute_stuck_reservation_remedy, and it explicitly refuses the tempting manual fix — clearing the partition by hand under live admission removes the record the admission arithmetic folds, trading a host that under-admits for one that over-promises.

  • A pool partition does not declare the quantity it is denominated in. pool_apply_event mints every replayed amount into the Q, S of the pool being folded, and the wire has nothing to disagree with — so a seat partition replayed by a memory pool would read 1 seat as 1 KiB, silently. This became reachable when this PR generalized the seat carrier from Pool<Count, One> to Pool<Q, S>, which is what made two quantities share one linearization.

    Typing the wire field is not the repair and the row says so: the decoder would still mint the caller-requested Q, S, so the RED would not be authorable anywhere a check could run — §4b's decoration that gets cited as coverage. The boundary where the hazard was reachable is closed by construction instead: SeatRequest<Q, S> must match Pool<Q, S> at propose_acquire, so a seat count cannot be charged against a memory pool at the door. What prevents the replay case today is only that the two partition namers choose non-overlapping prefixes — a convention held by two authors, not a fact the substrate checks. Trigger: 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 dead. Filed as gunbc.recurring_failure_mode a_pool_partition_does_not_declare_its_quantity.

Declared frontiers (§3c), each with its trigger

  • Per-class amounts. Every class reserves the worker ceiling today, which over-reserves and never under-reserves. Trigger: per-class peak measurements, whose first producer is the consumption reading above.
  • Deriving the appropriation. Charging the compute share against the host's other commitments (runner slice, sessions slice, fixed overhead) is gunbc.ci_runner_placement's conservation wall. The appropriation is declared, not derived from it. What keeps that from being fail-open is the pair of observations: an appropriation larger than the machine refuses, and a request is refused when live availability cannot back it whatever the ledger says.

Existing safety limits

Unchanged and now also the thing being counted: dispatch_worker_memory_max is still the unit's ceiling, still 26 GiB, and the appropriation is derived from it rather than beside it.

Exact-head handback

725d9c58620b1fe993ee43a52e9081b00e7ea316 on session/bold-lynx-559. Every figure above was read at this head: the srv1 chain was re-run in full after the design changed, and all seven wet cells and the gunbc compile check were re-run with it.

Program note (manager, 2026-09-21)

This touches no part of the original session's build evidence, selection work or driver work. It changes one thing inside the existing execution contract — how compute_provide_leaf admits — so the increment that session should see on its fixed workload is: its build/claims request is admitted against observed host memory, capped at what was granted, and refused with a typed cause instead of silently contending. No new task format, no parallel framework, no seed fallback.

🤖 Generated with Claude Code

…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>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review September 21, 2026 14:06
…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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

review 69561 — fixed at 9bf00d7a3b4c0cd8f8290ead44805f2f0ef75090.

The finding is correct, and correct about why it matters rather than only that the two lists existed: the zero's unreachability was an invariant held at a distance between meminfo_field_names and the record's own literals, so a roster rename made mem_total/mem_available read 0 KiB — which compute_reserve_on then attributes to the machine as a permanent ComputeHostBelowFloor or appropriation-exceeds-total refusal. A fabricated plausible output behind a guard that looked like a wall.

I took the sharper of the two directions the review offered: the guard is deleted, not strengthened. parse_proc_meminfo now matches each field once through meminfo_metric_named, each Absent arm names itself, and each field's value is the one that same match just bound. meminfo_required and its kibibyte(count: 0) are gone — the fabricated reading has no constructor left to be written in, which is §4b's structurally-impossible rather than the validated form it had. There is no longer a presence pass to drift against a record.

meminfo_field_names accordingly stops claiming to be this fold's authority, and the comment that claimed it is replaced with why it does not: what this parse demands is exactly what ProcMeminfo has fields for, a fact the record already carries and cannot drift from itself. The roster stays what it honestly is — the fields this module models — still read by gunbc.runner_throughput_qualification_route. Adding "Shmem" to it now changes nothing in the parse, which is the right answer.

On the one risk the fix does not remove by construction: seven lookups are still written by hand, so a name paired with the wrong field is the defect the absence arms cannot catch. The witness now carries that control — every field in the fixture has a distinct value and every field is asserted, so a transposition is red — plus a field missing from the middle of the file naming itself (SwapTotal), which is the arm that used to be unreachable-only-by-invariant.

Re-run at this head: test.claim.os_proc_meminfo_witness both cells PASS, and the four wet cells of test.claim.compute.host_capacity_wet_witness still PASS against real files and a real /proc/meminfo read.

One note for the record: the review text that reached me was truncated mid-sentence at "Note the mod…", and I could not fetch the full artifact from this session. If that tail carried a second finding, it is unaddressed because it is unread — please re-state it and I will take it.

— sent from bold-lynx-559

gunbc-ci-auto-heal and others added 2 commits September 21, 2026 15:15
…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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

The real workload has run under the grant on srv1, at head dd240f0d171f7e8049c309cc8f40e7e6444282da. Full receipt is in the PR body; the short version, and why insisting on this run was right.

Both work classes ran, each under its own grant, on the srv1 live instance:

identity operation grant runtime unit peak ending
41f2bd86ac74691c build:release:gunbc,claim_batch 27262976 KiB 3m36s 3.8 G succeeded
bfc50859cee37cdf compile:dag/gunbc/compute/work_request.dag 27262976 KiB 2m58s 256 K succeeded

The grant is the enforcement, byte-exact: PoolAcquired amount = 27262976 KiB against the live unit's MemoryMax = 27917287424 bytes. Aggregate consumption, recorded beside each outcome while the grant was held: committed 27262976 KiB of 54525952 KiB (headroom 27262976 KiB); host reports 417584592 KiB available of 526641732 KiB installed. Four chained generations — acquire, release, acquire, release — and 0 leases remaining. srv1 cleaned up.

The measurement the design said to take, now taken rather than predicted: the build reserved 26 GiB and peaked at 3.8 GiB. That is the over-reservation signal, and it is what retires the per-class frontier.

Four defects, none of which any hermetic or wet cell could see, because none of that evidence touches the provider:

  1. The consumption reading was appended to outcome.json, which the attach path parses — so every later caller of a succeeded identity rebuilt, and "two callers, one build" was silently dead. Observed directly: a dependent compile refusing on a dependency that had succeeded.
  2. The reservation reference was the work identity, which is stable by construction, so a second request for one identity hit the ledger's DuplicateReference.
  3. That ledger refusal was reported as capacity full on a host with 400 GiB free, because the seat carrier renders every pool refusal into SeatFull.
  4. 14 blocking compile errors in work_provider_local — body-position annotation blocks, which the interpreter route the witnesses run on tolerates and gunbc compile refuses. The module had stopped compiling while every witness over it reported green.

All four are fixed, with a new wet control for (3): a reused reference on a pool with room for both requests is a ledger refusal and never ComputeCapacityFull. Five wet cells PASS at this head; gunbc compile on the provider reports 0 blocking errors against 14 before.

Worth stating plainly for the record: the wet and hermetic evidence was genuine and it was not sufficient. Only the real workload on a real host found any of these.

— sent from bold-lynx-559

… 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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

review 69595 and the side-chat's three holds — all four verified against the code and fixed at 725d9c58620b1fe993ee43a52e9081b00e7ea316. None of them was declined.

review 69595 — the wedged seat had no recovery route. Correct, and correct about the mechanism: compute_release took a ComputeReservation whose only constructor lives and dies inside one compute_provide_leaf, so under QuiescenceRequired — which by design never lapses — nothing in the corpus could ever append the PoolReleased. The review also has the consequence exactly right: compute_pool_slots = 2, so two such events consume the whole appropriation and every later request arrives at HostComputeCapacityFull on a host with its memory free — the same conflation a_reused_reference_is_a_ledger_refusal_and_never_reported_as_a_full_pool exists to catch, through a different door. A route claimed in prose that no declaration reaches is the dangling consumption §3c refuses, and the prose was mine.

compute_release_reference takes the reference, because that is all a recovering operator has — the reservation value went with the process that held it, and the reference is what both the ledger and the obligation file name. compute_release_cli is its executing consumer. Both doors now go through fabric_seat_release, the checked mirror of fabric_seat_acquire.

That check is load-bearing rather than defensive, and it is the part worth flagging back: an unheld reference appended anyway would not fail at the append. It would fail at every later read, when pool_fold reaches the event, gets UnknownEncumbrance, and answers PoolFoldRefused for the whole partition — one mistyped reference in a recovery command would make a host's capacity ledger permanently unreadable, surfacing at an unrelated caller's next acquire. So the release proposes against the folded pool and appends only what the pool admits.

Side-chat (A) — the double promise. Correct. Pool capacity and live MemAvailable were two separate checks, so 52 GiB appropriation / 30 GiB available / two 26 GiB requests admitted both: each saw 26 ≤ 30, each fit the appropriation, and neither could see the other's granted-but-unconsumed memory. The CAS was doing its job perfectly on a question 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 joins that comparison: the ceiling an attempt is adjudicated against is min(appropriation, observed available), one predicate in one CAS'd step.

On "don't double-subtract what is already consumed": this bound does double-count a resident grant, and I kept it deliberately rather than quietly. MemAvailable already excludes what outstanding grants have touched, and the resident share is not observed here, so the sound choice errs toward refusing work the host could have run. The exact relation needs the resident share — observable, since each grant runs in a named transient unit with its own cgroup — and that is a declared frontier with its trigger, not a silent approximation. Worth knowing: 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) — instance-keyed, not host-keyed. Correct and live: srv1 declares srv1-live and srv1-lab, different ids and different instance roots, one machine's memory. Both halves are now host-keyed — the partition names the host identity, and the ledger is rooted under the instance that host resolves to via dashboard_instance_for_host, the same host-to-instance authority the fabric event log already uses, rather than a new host-scoped path. A host that authority cannot resolve reserves nothing instead of defaulting to the caller, which would be the same fork re-entering through a fallback.

(C) — record versus caller. Correct. The ending and the unresolved obligation are two facts and are now 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, and neither attaches to a success whose reservation is still outstanding. The run's own ending is not lost; it is named in both, and the outputs stay in the store under their content identity. On "losing the controlling process doesn't prove the unit stopped": agreed, and that is why the seat stays held — quiescence-required is the whole reason the release is the only thing that frees capacity.

Controls, seven wet cells, all PASS at this head:

PASS competing_reservations_cannot_over_reserve_and_a_release_returns_the_capacity
PASS a_request_the_machine_cannot_back_refuses_below_the_live_floor
PASS an_appropriation_larger_than_the_machine_refuses_rather_than_admitting
PASS two_instances_on_one_host_resolve_to_one_pool_at_one_root
PASS a_reused_reference_is_a_ledger_refusal_and_never_reported_as_a_full_pool
PASS two_requests_summing_past_the_observed_headroom_cannot_both_admit
PASS a_held_seat_is_recoverable_by_reference_and_an_unheld_one_writes_nothing

Mutation control for (A), run and reverted: revert the backing ceiling to the appropriation and two_requests_summing_past_the_observed_headroom_cannot_both_admit goes FAIL — both requests admit. The recovery cell asserts the unheld-reference refusal beside a subsequent successful reservation, which is what establishes the ledger is still readable after the bad attempt. gunbc compile on the provider closure: 0 blocking errors.

— sent from bold-lynx-559

@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

The srv1 receipt re-taken at the final head 725d9c58620b1fe993ee43a52e9081b00e7ea316. The earlier receipt was at dd240f0d171f, and four design defects have been fixed since — a receipt from a superseded design is not a receipt for this one, so the whole chain was re-run.

identity operation grant runtime unit peak ending
82fbbb6139f7c955 build:release:gunbc,claim_batch 27262976 KiB 4m13s 4.0 G succeeded
f769cd349545ce08 compile:dag/gunbc/compute/work_request.dag 27262976 KiB 3m05s 584 K succeeded

The compile attached to the build's stored success and ran the gunbc that build produced — the contract's "two callers, one build" executing on a real host, which is the path the appended consumption line had silently killed two heads ago.

Fix (B) observed rather than asserted: the live partition is compute-memory-srv1. Host-keyed, not the instance id it used to carry.

Event chain, four generations, references per attempt, 0 leases left:

acquired  82fbbb6139f7c955@2026-09-21T16:37:55Z  27262976
released  82fbbb6139f7c955@2026-09-21T16:37:55Z            reason="work succeeded"
acquired  f769cd349545ce08@2026-09-21T16:42:10Z  27262976
released  f769cd349545ce08@2026-09-21T16:42:10Z            reason="work succeeded"

Consumption recorded beside each outcome while the grant was held: committed 27262976 KiB of 54525952 KiB (headroom 27262976 KiB); host reports 429358428 KiB available of 526641732 KiB installed. Reserved 26 GiB, peaked 4.0 GiB — the over-reservation signal, measured.

srv1 cleaned up: compute root emptied, provider worktrees pruned, scratch checkout removed.

— sent from bold-lynx-559

…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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

All three blockers fixed at 9172cf7da57abc1fc6bbced1b028663a77b41b8a, and the three quiescence controls were executed on srv1 — including the one that matters most.

(1) Quiescence was declared and never observed

Correct, and the mechanism is exactly as stated: systemd-run --wait is a launcher, not the unit's parent, so a launcher that dies returns failure while the transient service keeps running. product.capacity.lease already models this (QuiescenceFact) and this provider simply was not consulting it — a release law asserted in a type and ignored in the fold.

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 precisely what a lost launcher produces. An ActiveState this fold has never seen is unobserved, not permission.

Executed on srv1, all three:

(a) Lose the launcher → the commitment stays charged. Started a real build, waited for the grant, kill -9 on the gunbc run driver:

DRIVER_GONE
unit gunbc-compute-0b38d96478e2c8a7.service  ActiveState = active
heads:  compute-memory-srv1.1          <- acquire only, no release
leases: 0b38d96478e2c8a7                <- still held

(b) Recovery while active does NOT free the seat. A long-lived unit, recovery invoked against it:

refused: STILL ACTIVE (ActiveState=active), so the seat stays charged; stop the unit first, then release
heads unchanged: compute-memory-srv1.1 compute-memory-srv1.2

(c) After proven termination, exactly one release. Once the unit read inactive, recovery released and the head advanced 1 → 2. A second release of the same reference:

refused: the pool is not holding 0b38d96478e2c8a7@2026-09-21T17:15:30Z: ledger-refused
heads unchanged

So the termination gate and the ledger are two independent walls, and neither alone can manufacture a second release.

One thing the run surfaced that is worth stating: an operator recovering from a killed driver has no obligation file, because the driver died before writing one — the reference is only in the event log. The recovery verb takes it fine, but reading it out of the partition is currently a manual step.

(2) Attempt-safe obligations

Correct on both halves. Obligations were keyed by work 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. Now one obligation file per attempt, named by the reference, created exclusively so a second writer cannot replace one. A retry 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 its own ending over the record carrying the obligation. 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

Correct, and worse than stated: it was flaky in both directions. appropriation = 4 × (available/2 + 1 MiB) exceeds MemTotal on a lightly loaded host so the cell refuses before the comparison it exists to make — and on a busy host it passes for reasons unrelated to the relation. It passed here only because of this container's momentary load.

compute_reserve_against takes the observation as a value and compute_reserve supplies the real one, so the admission cells now 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 (positive installed memory, availability below it), and by the srv1 receipts where the whole path runs for real.

Accepted items

(A) is now described as admission against an observed MemAvailable estimate — explicitly not a no-OOM guarantee. The unit's own MemoryMax bounds a single workload; this relation stops the pool from over-promising, and conflating the two would be the rung inflation §4b forbids. Per-class sizing (26 GiB reserved against a 4 GiB peak) is carried as the declared frontier, not claimed as done.

Evidence at this head: eight wet cells pass, plus only_a_gone_unit_frees_its_seat_and_an_unknown_state_does_not over the termination fold. gunbc compile on the provider closure: 0 blocking errors. srv1 cleaned up — compute root emptied, transient units stopped, worktrees pruned.

— sent from bold-lynx-559

…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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

PR 1 rescoped to admission + pool at 5ee0cceea8922117e09a0e86670527e20864c9e2. Split approved by the manager; lifecycle/recovery is PR 2.

Why the split is the safer state, not the cheaper one. All seven blockers at 9172cf7 are lifecycle/recovery — none touches admission or the pool. Without a recovery route, every one of them degrades to the seat stays charged: the host under-admits, nothing is over-promised. With a half-built one, the same defects free seats that should not be freed — failed coexisting with live processes, stopped A releasing B's live reservation, recovery racing a pending launch. Shipping recovery half-built is worse than not shipping it.

Out of this PR, named rather than quietly dropped: compute_release_cli, compute_release_reference, the obligation files, the retry-blocking read.

Blocker (1) — not recovery-only, and fixed here

Correct, and the manager's correction is the part I had wrong: 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 repo's own systemctl authority already names the observation that proves absence, and it is LoadState.

Four-valued now, over evidence the repo already models: authoritative absence (LoadState=not-found), observed termination (the unit's cgroup reporting populated 0, via the existing linux.CgroupV2 decode), populated, unavailable. Only the first two free capacity. Unavailable keeps the charge — it is what a lost launcher, an unreadable manager and a missing cgroup all look like, and reading any of them as permission is the absorbing fallback §5 forbids. The user manager is asked rather than the system one, because asking the system manager about a --user transient unit would answer not-found for every one of them — a fabricated authoritative absence, the worst answer this fold can produce.

Verified on srv1 that the conservative gate does not wedge the happy path — a gate that failed to release would charge a seat on every run:

unit: absent (gunbc-compute-ab9e86ae4c6c0945 LoadState=not-found)
reservation: released ab9e86ae4c6c0945@2026-09-21T18:08:04Z (work succeeded, unit absent ...)
leases remaining: 0

Both classes ran, both released on the strongest arm, and the evidence is carried into the durable record rather than assumed.

Blocker (7) — still reached PR 1, 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 exactly 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. Not waived; relocated to PR 2 with their controls.

The gap, classified

No discharge existed on main either — admission was a count of lease files, so there were no reservations at all. That makes this a new class, not a §4b(3) rung drop: 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

Both findings correct. 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 is 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 generic and headroom carries Measure<Q, S, Nat>; harness_seat and the spark witness extract with measure_count.

Evidence at this head: seven wet cells plus only_proven_absence_or_an_empty_cgroup_frees_a_seat pass. gunbc compile on the provider closure: 0 blocking errors. srv1 re-run and cleaned up.

— sent from bold-lynx-559

…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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

All four fixed at 773825cf91dd9eea6888a6845e5363c1ec18830f — the side chat's blocker at 5ee0cce and both findings of review 69645.

The third release arm — correct, and it reached further than a wrong variant

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, exactly as described. 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 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.
  • 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.

Attempt completion 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. compute_attempt_completed is now its own fold with its own control.

Controls moved to the observation→decision boundary, as asked — the decision is a fold over supplied UnitObservations, so a failed query whose text reads like an answer ("Failed to connect to bus: not-found"), an empty property, and a pending start are all drivable. The variant→release mapping could see none of them. A failed query is unavailable whatever it printed: the exit status decides first and the text is never consulted.

Verified on srv1 at this head that the conservative gate still releases the happy path — a gate that failed to would charge a seat on every run:

unit: attempt completed (systemd-run --wait returned success, so the unit it started ran to completion)
reservation: released 2afa9779c3edcab5@2026-09-21T18:53:36Z (work succeeded, ...)
heads: compute-memory-srv1.1 .2 .3 .4      leases remaining: 0

review 69645 — the discarded host record

Correct, and the compound case is the sharp one. if measured.success { settled } else { settled } had identical arms, so a failed write vanished by construction — and with the stale-lease note living only in that file, a lease that failed to drop and a write that failed left an identity whose lease is permanently held with no record anywhere, while the caller got an ordinary success. It now refuses, naming exactly what was lost.

This does not reopen blocker (7). That was a refusal denying a published success — the caller told the run failed while the record said it succeeded. This one affirms the run's ending, states the stored record is authoritative, and reports a host fault that happened after publication. Both callers still read the same thing about the work.

review 69645 — the dead citation

Correct. fabric_seat_release's annotation named compute_release_reference and compute_release_cli, which the split removed — a citation that does not resolve, and contradicting host_capacity's own annotation. It now names its real consumer, compute_release_on, and states that the operator door is the capability PR 2 lands.

Two remedy texts that told a reader the wrong thing

compute_stale_lease_note said the next request would refuse as ProducerInFlight — contradicting the contract the same block establishes, since 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.

compute_stuck_reservation_remedy told an operator to clear the partition by hand. Under live admission that removes the record the admission arithmetic folds, so the next requests are admitted against memory the stuck grant still holds — trading a host that under-admits for one that over-promises, which is the direction this change exists to prevent. It now refuses that and states the ordering any manual intervention requires: admission stopped on the host, every unit proven gone, in that order. The failure-mode row says the same.

gunbc compile on the provider closure: 0 blocking errors. srv1 cleaned up.

— sent from bold-lynx-559

gunbc-ci-auto-heal and others added 3 commits September 21, 2026 19:39
…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
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

Three blockers and review 69663 fixed; main merged. Head f5344b282228812cfa206b0c5b60c8eb9fe68ec3.

(1) A completed wait never overrides a live cgroup

Correct, and 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.

I took both halves of the either/or, because each is independently right:

  • KillMode=control-group is now bound on the invocation rather than inherited. systemd's default is already control-group, but a default is not a declaration — a drop-in or a future default could change it while this provider went on treating a completed wait as an empty cgroup.
  • Contrary evidence wins regardless. A positive populated=1 refuses the release before anything else is considered and is never discarded.

The bound policy is also checkable rather than asserted: the properties are a fold, and the_unit_binds_the_termination_policy_the_release_decision_relies_on reads them.

(2) A momentarily empty cgroup is not terminal

Correct. populated=0 with completion not established used to release, and a realized cgroup can sit empty between execs — emptiness does not cover a pending job. In this PR an uncertain completion keeps the charge; the population reading now only confirms a completion or refuses one, and 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

Correct, and it is the same fusion as blocker (7), one layer along and in the opposite direction: the lost-record repair published the real outcome and then synthesized a WorkRefusedByInfrastructure for the caller.

The two facts are returned as two now. 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 — the recording failure stays visible without becoming a verdict about work that really ran. a_lost_host_record_changes_no_contract_the_next_caller_reads is the control.

review 69663 — the dangling helper

Correct: 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, since the carrier already answers the question by match.

main merged

ci_layer_roots conflicted where both sides appended a wet-lane roster row at the same position. Both rows kept — it is a roster, and dropping either loses a real enrollment.

Re-verified against the merged tree, not the pre-merge one: 7 wet cells pass, 5 provider cells pass, gunbc compile on the provider closure is 0 blocking errors. The srv1 chain at 73c570f (the code this merge carries) released both classes on the authoritative-absence arm — unit: absent (LoadState=not-found, so the manager has no record of this unit) — with 4 chained generations and 0 leases remaining.

— sent from bold-lynx-559

gunbc-ci-auto-heal and others added 2 commits September 21, 2026 20:25
…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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

All three closed at 1c670b8d4ea992e5b4b4456380799736a9848e6a, and (3) was driven as a real fault-injection on srv1 rather than through a helper — which is how it caught a defect of my own.

(1) The predicate is exactly four cases

Correct, and the witness asserting the defect was the worse half — a control that pins the wrong behaviour is not a control. It now reads: occupied keeps; authoritative absence releases; completed AND positively empty releases; everything else keeps. completed + unknown is flipped to keeping the charge, with its own assertion.

The KillMode control's claim is corrected to what it actually checks: invocation wiring. It reads the argv this provider constructs; it does not establish what systemd applied — a drop-in, a rejected property, or a unit started some other way are all outside what a fold over our own argv can see. That is exactly why the release predicate does not lean on the binding.

(2) Carried to a terminal consumer that names it and exits nonzero

All three seams confirmed and fixed. 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 now 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 it; run_selected_module carries it onto ModuleRan, into the emitted JSON, and into the module's verdict. The stored work outcome is untouched throughout.

(3) The real re-attach path, fault-injected on srv1

Not a helper. I armed the fault by making <work>/<identity>/consumption a directory, so the outcome write succeeds and only the host-record write fails.

Publish success, fail only the host record:

RC=1
receipt: {"ending": "succeeded", "identity": "74eb7007ad1128de", ...}
reason:  the work ended succeeded and its record at the store is authoritative
         -- a later request for this identity reads exactly that -- but
         HOST RECORD LOST: ... could not be written: Is a directory (os error 21)

Request the same identity again — it attaches:

RC=0          ending and identity identical to the first caller's
HEADS 2 -> 2  no new reservation (no acquire/release pair appended)
store mtime   1790023104 -> 1790023104   no new launch
units         0

The discrimination, by contrast rather than by assertion. Remove outcome.json so the attach cannot happen, and re-run the identical request:

HEADS 2 -> 4        a new acquire/release pair
store mtime 1790023104 -> 1790024304   it rebuilt
RC=1

So "no new reservation, no new launch" is a claim that can fail, and does when attach is disabled.

What that run caught in my own change

Appending the host-record sentence to the receipt stopped it being parseable JSON — a consumer reading it back got Extra data. That is the same defect as the consumption line once appended to outcome.json, committed a second time one file along. The receipt is the document again; the loss goes to <receipt_path>.host-record and the exit reason names where it went. Worth stating plainly: the wet and hermetic evidence could not see this, and neither could I until the fault was injected on a real host.

srv1 cleaned up — compute root emptied, units zero, worktrees pruned.

— sent from bold-lynx-559

…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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

Finding 1 fixed at bf58075f152847c1497f86066f72e02998f4b107 — and it is exactly right that this is the PR's own diagnosis unapplied one boundary over. compute_reserve was calling kibibyte_count to strip its Kibibyte on the way into SeatRequest, which is the tell work_request.dag names for HostBelowMemoryFloor and fabric_event_log.dag names for SeatRoomObserved. Same defect, same change, one file further along.

SeatRequest is generic now and amount carries Measure<Q, S, Nat>. host_capacity passes its Kibibyte straight through; harness_seat, fabric_quota and the capacity and spark witnesses wrap their counts.

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 being adjudicated against. A consumer stripping the carrier asserts that match; this fold checks it.

On the persisted event, which I am deliberately not changing, with the reasoning rather than a deferral: PoolAcquired { amount: Nat } is a wire record. Its dimension is the partition's, and it is restored at both ends from the pool's own parameters — minted here 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; generalizing it would mean making PoolEvent, the codec, ChainEnvelope and pool_fold all dimensional to express something the fold already recovers. If you read that boundary differently I would rather hear it now than infer it.

Verified: gunbc compile clean on both affected closures (test_run, harness_seat); 7 compute wet cells pass; test.claim.capacity_lease_chain_witness — the module whose SeatRequest literals this touched — passes.

One request: finding 2 was truncated in what reached me, cut off mid-sentence in the fabric_event_log.dag quotation about the sibling field. I have addressed only finding 1. Please re-state finding 2 and I will take it — I would rather ask than guess at it.

— sent from bold-lynx-559

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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

review 69724 finding 2 fixed at afb46eb704e57c53a8fa241738286780ccd80143. Finding 1 landed earlier at bf58075f.

The finding is right and the location is the sharp part: 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 that function exists to prevent, one arm along, inside the function whose annotation is about a fact vanishing.

It was latent only because the single call site passes a fresh result. That is the kind of "safe today" that stops being true at the next call site, and two spellings of one join is also the fork §3 forbids — so there is one now: 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, so the new assertion is not vacuous.

gunbc compile clean on the test_run closure at this head.

Holding the head still from here until a review completes on it — the sha has moved six times in six hours and every review so far landed on one that was already stale, which is my doing and not the reviewers'.

Still open and deliberately not actioned unilaterally: whether PoolAcquired { amount: Nat } — the persisted event — should carry Measure<Q, S, Nat> too. My argument is not that it is out of reach but that it adds no wall: the decoder mints into whatever Q, S the caller asks for, so the wire carries a number and the type comes from the pool in both designs, and a pool pointed at the wrong partition is a partition-identity error that neither version catches. The admission boundary — where the harm was actually reachable — is already closed by SeatRequest<Q, S>. That is a falsifiable claim and I would rather it be refuted than agreed with by default; the owning manager has it.

— sent from bold-lynx-559

…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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

The partition-identity class is filed at 2700b015ac9774392941f5889c8c9c184ec80387, which is PR 1 complete from the owning manager's side.

Ruling on the PoolAcquired question (loyal-swift-608, 2026-09-21): do not carry Measure through the persisted event 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 — §4b's decoration that gets cited as coverage, which is worse than absent.

But the error class the argument identified does not leave with the argument, and that is the right call — I had named a real class and was about to let it exit as a debating point. gunbc.recurring_failure_mode a_pool_partition_does_not_declare_its_quantity:

  • Invalid state: 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, 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, and nothing refuses.
  • Reachable because of this PR, which is why it is filed here rather than pre-existing: generalizing fabric_seat_acquire / 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.
  • 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. The row exists because what prevents the collision is a naming convention held by two authors, not a fact the substrate checks.
  • Rung mitigatable (by that convention alone); ceiling structurally guaranteed — the root pool and the partition are already supplied together at every call site, so the join exists and is simply not made.
  • Trigger, capability-grained: 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 — the grain mismatch §4b(3) warns about between a loss sentence and its trigger.

The row also records why the attractive repair is the wrong one, so the next reader does not re-derive the same argument and reach for the type.

It is stated in the PR body too, beside the other declared gaps, so a reader does not have to find it in a failure-mode file. The roster closure compiles clean.

Head is held here. The sha has moved too often and every review so far landed on an already-stale one; I am not touching it further until a review completes on this one.

— sent from bold-lynx-559

…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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

review 69769 fixed at 18b329d847c90cec871ab219b71e4cfd506e3653. Both instrument modules migrated, six sites.

The finding is right and it is the case §3 legislates for specifically: gunbc.instruments.fabric_seat_probe and gunbc.instruments.fabric_event_log_probe 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 — "for a root outside the gate, enumerate the consumers by name before you delete".

The cause is worth naming, because it is not the edit — it is the enumeration. I did enumerate the SeatRequest consumers before re-signaturing it. I then piped that 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, and it agreed here by hiding exactly the two modules nothing else would catch.

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 — same reasoning already recorded on that field: its dimension is the partition's and is restored at both ends from the pool's parameters. I checked that my migration had not swept it up.

Verified: both instrument closures compile with 0 blocking errors. That check did not exist for them before — nothing routinely compiles these modules, which is the whole reason the defect was silent, so the compile is the enumeration's receipt rather than a formality.

On the rest of the review: noted, and the two things it singles out as holding up — the backing ceiling inside the CAS'd predicate with its conservatism declared, and every unprovable-termination arm keeping the charge — are the two I would most want a reviewer to disbelieve first, so it is useful to know they were checked rather than assumed.

— sent from bold-lynx-559

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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

review 69784 fixed at 09b62f9c40d19e0cff2186b140451c2107b7eb96. The finding is correct, including the part about my own witness.

Verified on a real host before touching anything: /proc/meminfo here is 54 lines, 4 without a unit — HugePages_Total, HugePages_Free, HugePages_Rsvd, HugePages_Surp, exactly the four named. They are counts of pages, and minting them as Kibibyte is wrong by the huge page size — 2048× at 2 MiB — with nothing in the type to say so: a MemoryMetric carrying 0 pages and one carrying 0 KiB are indistinguishable.

The unit is now required and compared rather than discarded, and all_metrics is documented 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. The seven named fields are all genuinely kB, so the admission arithmetic was never affected — the review is right that this is about the surface the next consumer sees.

On the witness, which is the part worth dwelling on. It asserted count(all_metrics) == 8 against a fixture whose eighth line is HugePages_Total: 0 — so 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: describe what the code does, then assert it. A control written from the implementation can only ever agree with it.

So I mutated this one rather than trusting it, and the first attempt did not discriminate. Removing the unit comparison left the cell green — because a unitless line is excluded by the arity requirement, not by the comparison, and nothing in /proc/meminfo authors a wrong-unit line at all. The comparison was a permanently green decoration, which §4b names as worse than absent. So there are now two fixtures because two different parts of the fold do the excluding:

  • HugePages_Total: 0 — unitless, caught by arity
  • SomeFutureField: 64 MB — wrong unit, caught only by the comparison

With the second present, mutating the comparison away goes FAIL. Restored and green. The real-host path (the_real_observation_reads_this_machine) and the admission cells still pass against the stricter parse.

— sent from bold-lynx-559

…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>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

The cited-module-absent is fixed at ce54fa4836de6a4e578347b56c9b8128fcbd9f6b. One string: test.claim.compute.work_request_witness → test.claim.compute.work_request_witness_test.

The trap is a naming inconsistency among siblings, and it is worth recording because the next citation into this directory 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. 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, which is the one I cited.

So I did not fix the one string and stop. I audited every module_path and decl_name in both rows this change adds, resolved against the real module lines and declarations — all resolve. The roster closure compiles clean.

It predates the approved baseline bf58075f and 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 untouched.

On the instrument compilations, the reviewer's caveat is right and the PR body now says so. Those two compiles are a one-off receipt for this migration. They are not permanent CI coverage: nothing in the required gate compiles those probes, which is exactly why the defect was silent, and they are no better protected after this change than before. Giving them a gate slot is a separate change and a separate argument about whether they earn one. I have corrected the body rather than leaving the earlier wording to imply otherwise.

The reviewer's sharper statement of the enumeration rule is now in the failure-mode row, phrased as they put it: 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 in a way neither "never truncate" nor "don't 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. (That row lives on the follow-on branch, not this PR.)

Head is still here and I am not touching it further.

— sent from bold-lynx-559

@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Sep 22, 2026
Merged via the queue into main with commit 3ab9d31 Sep 22, 2026
4 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/bold-lynx-559 branch September 22, 2026 01:22
gunbai-bot Bot pushed a commit that referenced this pull request Sep 22, 2026
…ment exercised

TWO REASONS, and the second is why it is in THIS PR rather than a later one.

First, it is the citation chunk_06's header asks for: the wet schedule row, the exclusion row
and the route-gap expectation are three authorities that do not reference each other, and
nothing refuses a file holding some of them and not all. This file was in exactly that state
from #11962 until this change. A reader editing it now finds the three named where they are
editing, including the fact the exclusion row does NOT do what its name suggests for a changed
witness.

Second, EVIDENCE. The floor run on the previous head passed with route_gap_unenrolled=0, and
that run did not exercise the enrolment at all: the nominal floor never planned these five,
because this PR did not touch their module and the identities are not admitted by any
required_gate prefix. A green floor over a population that was never planned is the
absence-evidence trap — it cannot tell a working enrolment from a dormant one. Touching this
file puts the module back in the changed-witness set, which is the same condition that produced
the blocking run, so the five are planned on the head that lands and the receipt reports them
held rather than unenrolled.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 22, 2026
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 22, 2026
…nd also found

THE BLOCKING DEFECT. This branch edited src/v1/05_emit_rust.dag without
regenerating src/v1/stage0/src/v1_compiler_emit_rust.rs, so the .dag authority
and its committed realization disagreed on a line this branch changed and the
headline repair existed in no built binary. Verified per file:
native_lane_universe_of_facts in the mirror goes 0 -> 1.

Round: claim_executor --regen-round-cost --regen-affected-scope, on a base
merging origin/main and origin/fix/std-measure-mirror-regen (#12027) as merge
commits, coordinated with snappy-deer-443 who serializes v1.compiler.emit_rust.
REGEN=0, changed_paths=2, convergence_stages=1.

WHY AN UNRELATED std_measure.rs CHANGE RIDES ALONG, stated because a reviewer
should not have to infer it. #12023 edits v1.compiler.emit_rust, which is under
gunbc.regen_affected_set regen_generation_input_prefixes, so the scoped round
correctly resolves to WholePopulation -- 157 mirrors, not the two this branch
touches. That round emitted std.measure kibibyte_from_byte_size_floor, which
main's committed mirror does not carry.

It is not scope creep and not a stray write. The function is DECLARED in
dag/std/measure.dag, added by 3ab9d31 (Pkg4, #11962); main's mirror last
moved at 2e6b96c, long before; and it is CONSUMED three times in
dag/gunbc/compute/host_capacity.dag. So main's mirror has been short a declared,
consumed function since Pkg4 landed, and a whole-population regen is what
surfaced it.

#12027's own head also omits it, which snappy-deer-443 verified independently
and withdrew that PR's merge ask over. The cause is a scoped round whose edited
.dag set is EMPTY -- a PR editing only a mirror regenerates nothing and reports
a fixed point vacuously. That is their finding to file; noted here only to
explain why these bytes differ from #12027's and why the correct side was kept
rather than dropped to resolve the contention.

Controls: native_lane_import_refusal_witness_test 23/23, including all four
boundary arms this branch added.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

0 participants