Repository navigation
Wire the build-cache realize path through both admission authorities, with the observation producer they were waiting on - #8825
Conversation
… with the observation producer they were waiting on `realize_provision_build_cache` had exactly one gate ahead of it -- the catalog gate, which is pure id validation in a third module and observes no host -- and then rendered the unit, installed it and restarted it on every pass. The two authorities that were supposed to decide whether that was safe, `build_cache_ensure.admit_ensure_build_cache_instance` and `host_build_cache_provision.provision_build_cache_verdict`, had zero production callers. Their witnesses were green, which established that the folds were correct, not that the class was guarded -- the rung inflation DESIGN 4b calls worse than sitting low. The shell-to-dag census C-note filed it as one wiring job; this is that job. What was missing was a producer. `build_cache_ci_endpoint_observed_producer` returned `ProcTableUnreadable` in every arm because it takes a `HostIdentity` and so has no transport to read through. The producer now lives in `gunbc.build_cache_endpoint_observe` as a pure decode of read text into `BuildCacheEndpointObservation` / `EndpointPathState` / `ObservationCurrency`, and `gunbc.host_effect_realize` performs the reads over the transport it already holds: four to seven single-argv, non-mutating reads per pass (boot id, `stat -c %F` on the endpoint path, `ss -H -l -p -x src <path>`, then the owner's cgroup, stat, principal and exe only when exactly one owner resolved). Local reads go through `command_runner.run_shell_command_capture`, remote through `run_typed_argv_transport`. No shell body was added -- the reads land on the typed-argv side of #5828 and the ensure step's concat-built script is untouched. The two authorities sit on opposite sides of the act and do not duplicate each other. The ensure admission is the precondition: `EnsureAlreadyConverged` converges with no unit written and no restart issued, removing a per-pass reinstall that re-colded every compile on the host; a runner-owned endpoint refuses with the owner located, which is the srv1 incident class. The provision verdict is the postcondition over a re-observed placement after the ensure ran, which catches an ensure that reports success while the endpoint ends up owned by something else. The verdict fold moved to `gunbc.build_cache_provision_verdict` because `host_build_cache_provision` imports `host_toolchain_ensure`, which imports `host_effect_realize` -- calling it from there would have closed an import cycle. Two bounds are declared rather than closed, both in carrier notes beside the code: `EndpointStaleSocket` is still never produced, because the fourth clause of its observer contract needs a glob over /proc that this census row may not emit, so srv4's stranded socket refuses with the unread clause named instead of being unlinked on partial evidence; and the post-ensure survey races the unit start, a false refusal on an idempotent operation rather than a silent misreport. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…two conflations it exposed The false capability claim is removed from all five artifacts that carried it. Resolving a socket inode to its holder does NOT require a shell: `find /proc -maxdepth 3 -path '*/fd/*' -lname 'socket:?N?'` is one argv. The first probe used the bracketed form, find read `[...]` as a glob character class, it matched nothing, and "found nothing" was accepted as proof the walk was impossible. A zero with no nonzero beside it in the same run is not a measurement. Consequences: `ss` is gone, gunbc.build_cache_instance endpoint_ownership_note is byte-identical with main again (it was right as written), all four stale-socket clauses are established, EndpointStaleSocket is produced, and the admitted-unlink arm is reachable rather than dead. Two defects the reworked witnesses caught, neither of which was the fixture: - endpoint_path_state answered EndpointListening from the fd-holder observation alone, so a socket HELD OPEN by a non-accepting process was reported as a healthy listening endpoint. Clause (2) (no LISTEN entry) and clause (3) (no fd holder) are separate reads and neither may answer for the other. Now routed through socket_owner_path_state, which requires the listen entry. - The witness module had no import block, so bare `ProcessIdentity` resolved corpus-wide and extdeps.posix's homonym won under the whole-corpus floor. A targeted compile of the entry never loaded posix and reported zero blocking diagnostics while CI refused. Imported explicitly, with the measurement recorded. Recorded but NOT repaired: a server that IS our unit, holding its socket open while not listening, short-circuits to EnsureAlreadyConverged on the placement axis without consulting the path. That predates this wiring and changing it is a change to what ALREADY-CONVERGED means. 22 witnesses green by execution; host_effect_realize typechecks to the same 2 pre-existing gunbc.Cli diagnostics main already carries. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…rename through it #8825 landed the admission wiring and the observation producer while this branch was open, and both lanes edit gunbc.host_effect_realize. The conflict was confined to that file's import block; everything else auto-merged. RESOLUTION: main's import block taken wholesale, with the single symbol this branch renamed swapped in (render_build_cache_unit -> build_cache_unit_text). Nothing of #8825's was dropped -- the new observe/verdict/ensure imports, the endpoint survey, and the stale-socket admission all arrive intact. THE FIELD RENAME REACHED FURTHER THAN THE PREDICTION. I told zesty-wolf-464 the collision was one token in one destructure. That was right about their realize-side binding and wrong about the blast radius: #8825's new claim module build_cache_endpoint_observe_test destructures the arm in EIGHT places, seven binding the field to `_` and one reading it. The seven are mechanical; the eighth asserted `lines.count() > 0` over a List<String> and now projects the modeled value through extdeps.systemd.unit_file systemd_unit_file_lines to make the same claim. Its intent is unchanged -- I migrated another lane's witness, I did not restate what it asserts. The projection is imported explicitly rather than resolved bare, following that module's own ambiguous_type_name_import_note: it exists because a bare name there resolved by last-import-wins under a reduced pool and refused under the whole-corpus one, which is exactly the failure a merge like this is positioned to reintroduce. VERIFIED ON THE MERGED TREE, not on either side of it: build_cache_ensure_test 14/14 and build_cache_endpoint_observe_test 22/22 pass. The annotation-grain proxy is clean (no indented // in the diff), which is the check whose absence red the floor last time. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Correcting a prediction I made about this PR, posted here because this is the diff a reader would be looking at when it matters, and the session I originally told is gone. While #8825 was open I told its author that my in-flight rename of the The actual collision, measured on the merged tree rather than predicted:
I have taken all of that in #8827's merge of main, preserving this PR's witness intent — I migrated the assertion's carrier, not what it asserts. Its 22 witnesses pass on the merged tree, alongside The generalizable lesson, which is why this is worth a comment rather than a silent fixup: I predicted the radius from the author's message describing the diff, not from the diff. The message said "my consumer does not read — sent from sunny-ant-215 |
…e new refusal arm at every elimination site CI red on 261c6ea was four non-exhaustive matches over EnsureRefusal in test.claim.build_cache_endpoint_observe: adding EnsureOwnedButNotServing to the coproduct is precisely the compile error a closed vocabulary is supposed to produce, and the sites are covered here rather than by widening any of them. The witness at the centre of it is #8825's pin. It asserted that our own unit holding an unlistened socket READS CONVERGED -- the behaviour that PR measured, pinned, and explicitly declined to endorse. It is inverted rather than deleted: same fixture, opposite arm, now the regression control for the contract it used to contradict, with a note in the file recording that it changed direction and why. Its same-run nonzero is witness_managed_unit_owner_is_already_converged, one field apart (listening vs no-listen /proc/net/unix text), so the refusal is readable as evidence rather than as an admission that refuses everything. transitional_states_note records what the tightened axis does with the states between present and serving, decoded rather than argued: the unit started with no socket yet, and a restart in flight over a leftover socket, both land on not-ours placements and keep their pre-existing write arms untouched; only the bind-before-listen / wedged-server state moves, and it moves from a silent converge to a refusal that writes nothing. No arm in this change turns a converge into a write, so it cannot reintroduce the restart thrash. Each of the three states is checked by a witness in the same file. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ild-cache ensure contract (#8844) * ALREADY-CONVERGED must mean serving, not merely placed: the build-cache ensure contract Placement answers WHO owns the endpoint; it cannot answer WHETHER the endpoint is served. admit_ensure_build_cache_instance short-circuited on placement alone, so a process in our own intended unit's cgroup holding its socket OPEN while nothing LISTENS on it converged: no unit written, no restart issued, a receipt reading already_converged, and a cache no client can reach. That state is produced by the live decoder, not hypothesised -- gunbc.build_cache_endpoint_observe socket_owner_path_state mints EndpointPathConflict for exactly it -- and the tree had already measured the consequence: test.claim.build_cache_endpoint_observe's held-without-listening fixture had to name a FOREIGN owner to reach the path-conflict arm at all, because our own unit's ownership swallowed it. Its note recorded the gap and named the decision this commit makes. The contract: EnsureAlreadyConverged is minted only when the endpoint owner is our intended managed unit AND the path is observed LISTENING. Every other path state under our own placement refuses with the unit named, rather than converging or restarting -- replacing a live owner of in-flight compiles is an eviction, a different operation, per the sibling occupied-endpoint rule. What this does not establish is named in the carrier rather than left to be discovered: serving here means a listener is bound, not that the daemon responds or that its storage/capacity/principal still match desired. Those are the postcondition axes gunbc.build_cache_provision_verdict folds after the acted path runs; the no-act path cannot read them without a probe this lane refuses (--show-stats prints a table whether or not a server exists), so the weakness is declared with its next-rung trigger. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Invert the pinning witness the new contract contradicts, and cover the new refusal arm at every elimination site CI red on 261c6ea was four non-exhaustive matches over EnsureRefusal in test.claim.build_cache_endpoint_observe: adding EnsureOwnedButNotServing to the coproduct is precisely the compile error a closed vocabulary is supposed to produce, and the sites are covered here rather than by widening any of them. The witness at the centre of it is #8825's pin. It asserted that our own unit holding an unlistened socket READS CONVERGED -- the behaviour that PR measured, pinned, and explicitly declined to endorse. It is inverted rather than deleted: same fixture, opposite arm, now the regression control for the contract it used to contradict, with a note in the file recording that it changed direction and why. Its same-run nonzero is witness_managed_unit_owner_is_already_converged, one field apart (listening vs no-listen /proc/net/unix text), so the refusal is readable as evidence rather than as an admission that refuses everything. transitional_states_note records what the tightened axis does with the states between present and serving, decoded rather than argued: the unit started with no socket yet, and a restart in flight over a leftover socket, both land on not-ours placements and keep their pre-existing write arms untouched; only the bind-before-listen / wedged-server state moves, and it moves from a silent converge to a refusal that writes nothing. No arm in this change turns a converge into a write, so it cannot reintroduce the restart thrash. Each of the three states is checked by a witness in the same file. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…on family (#8827) * Build-cache vertical: the systemd unit becomes a modeled value, not INI text gunbc spells itself gunbc.build_cache_unit hand-concatenated "[Unit]", "[Service]", "Environment=..." and "WantedBy=..." as string literals, which made gunbc a SECOND AUTHORITY for systemd's unit-file syntax beside extdeps.systemd.unit_file -- the §3 nicknaming that module's own header says it exists to prevent. Its systemd_medium_as_string_note declared the debt and named the wrong exit: the dissolve-on pointed at extdeps.languages, while the grammar had already landed at extdeps.systemd.unit_file. The trigger had effectively fired and nothing noticed. extdeps.systemd.unit_file grows the directives this consumer needs, each cited: Before=/Requires= in [Unit] (systemd.unit(5), already in scope) and Slice= plus a [Slice] section with MemoryMax=/MemoryHigh= (systemd.resource-control(5), a scope the module did not previously cite and now does). SliceUnitFile joins the unit-type coproduct, so a [Service] in a slice stays unwritable. Drop-ins get their own type rather than a unit file with empty sections: a fragment has no unit type, so SystemdDropIn is a LIST of known sections -- absence is absence from the list, and an empty [Service] stays distinct from no [Service] at all. The line view and the bytes are now one assembly read at two grains (systemd_unit_file_lines / serialize_systemd_unit_file), which is what let the build-cache render drop its own List<String> renderer instead of keeping one to serve consumers that want lines. The admissions stop carrying rendered text. EnsureBuildCacheAdmitted carried unit_lines: List<String> and EnsureCompilePoolAdmitted carried slice_lines -- a decision type holding a serialized artifact of one realization. Both now carry the modeled unit value, so bytes are produced by the single serializer at the moment of writing rather than frozen into the decision. NO HOST BYTES CHANGE, measured rather than reasoned. An earlier draft declared a one-byte behavioural change (a trailing newline); that was wrong -- the heredoc already supplied it. build_cache_ensure_daemon_body was rendered on this tree and on origin/main with one compiler, for the CI instance (absent capacity) and the session instance (present capacity), byte-identical both times, with a control confirming the two trees genuinely differ. The write site concatenates the heredoc terminator rather than joining it, which is what keeps that true. 95 witnesses across the six affected claim modules pass. Six new witnesses cover the added grammar, including exact bytes for a slice unit and the empty-vs-absent drop-in section. Three mutations were executed against the new walls -- a wrong MemoryHigh spelling, a line view that stops sharing the serializer's assembly, and a drop-in that always emits [Unit] -- each producing targeted reds. Does NOT wire realize_provision_build_cache onto the admission; that stays open and is zesty-wolf-464's lane on #8825. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Move the heredoc rationale to module-item grain: a body-level // refuses at the floor CI's floor phase refused this branch with four typed, located diagnostics -- "source annotation sits inside a declaration body. Only module-item grain is modeled" -- against the four-line comment I put inside build_cache_ensure_daemon_body's list literal. DESIGN section 4c says exactly this: the .dag realization admits only standalone leading // blocks attached to module-scope declarations, and body, trailing, unattached and block-comment forms refuse until separately modeled. The rationale is unchanged in substance and now sits above the declaration it describes, which is where section 4c puts it. WHY IT WAS NOT CAUGHT LOCALLY, recorded because the next person will reach for the same tool: `gunbc run` is eval-only and never applies the annotation-grain gate, so all 95 witnesses passed over source the floor refuses. `gunbc compile` is the strict path, but a whole-corpus compile does not finish inside a single local window (reconcile alone is 8-10 minutes, and the attempt timed out mid-emit), so the known-positive probe for the gate was INCONCLUSIVE rather than green -- stated that way rather than as a local check that passed. What was actually verified before pushing is narrower and is the decidable proxy for this class: the diff carries no indented // anywhere, checked mechanically across all seven changed files. That is a syntactic property, not a run of the gate, and CI remains the authority. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Merge origin/main: pick up #8818/#8828, whose witnesses were the 16 floor failures The floor red on 77c9121 was 16 FAILs, all in v2.test.claim.fold_lowering (12) and v2.test.claim.body_lowering.statement_let_bind (4), every one 'non-exhaustive pattern match on OccurrenceId'. None of it is reachable from this branch's subject -- the diff touches the systemd unit-file grammar and the build-cache renderers. Diagnosed rather than assumed: main was GREEN at the same head class, and the two failing families map exactly to two commits this branch did not contain -- #8818, which routed the fold-lowering witnesses out of long/ and into the executing floor, and #8828, which is the statement-form let lowering. This branch carried the test files at their pre-#8818 home while the merged main-side routing executed them, so it ran witnesses against a compiler half a lane behind them. The remedy is the merge, not an edit: no file of mine is implicated, and the merge is clean (#8818 deletes src/v2/test/claim/long/fold_lowering_test.dag outright). Re-verified after merging: build_cache_ensure witness green, my grammar and renderer changes intact, no body-level annotation in the diff. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Delete two _text projections that never gained a consumer runner_ordering_drop_in_text and compile_pool_slice_text were authored as the natural peers of their _lines projections and nothing ever called them -- not in this module, not in the tests, not in the realize path. Under DESIGN §6 that is "a new artifact with no final consumer", and the honest fix is a deletion rather than a note explaining why the surface exists. The _lines peers stay: render_compile_pool_slice reaches compile_pool_ensure's admission and runner_ordering_dropin_lines reaches the tests. build_cache_unit_text stays: host_effect_realize writes it into the heredoc. serialize_systemd_drop_in stays in the grammar module -- its byte-exact witnesses consume it -- and only this module's now-unused import of it is dropped. Found by review 54749 on #8827. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…e denominator to its head The banner asserted that absence of a name is not discharge because a rename looks identical. It now demonstrates it, with six names that already have verdicts on main and do not all point the same way: srv3_chown_directory_to_current_user discharged 61bf47b (#8590) host_build_cache_provision_script discharged 40f2fb6 (#8825) four host_hygiene_reap_*_body files deleted ffa16a5 (#8583) git_fetch_script RENAME, not gone (unadjudicated) Three causes, one grep signature. The host_hygiene row is the sharpest: the commit that discharges those four names does not mention them, so the evidence is not reachable from the symbol at all -- which is precisely why the per-row lane cannot be done by symbol search. All four commits are ancestors of main, so the table is head-safe independent of the SS1.C corrections landing separately in #10529. The denominator now says it was measured at 70925ee and is valid only there: any later edit that strikes a row through changes what the closed-marker grep counts, so the 180/41/~139 split moves and must be re-derived rather than quoted. The demonstration table sits inside the blockquote, so it does not itself perturb the row count -- re-derived at 180 after the edit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013GCBVTWARwTLkAfVWaGfKA
… flag the census's dead-ci.yml population (#10537) * Correct the stale ci_floor_peak rows and flag the census's dead-ci.yml population gunbc.plans.shell_emission_model's Phase 1 PARTIAL row still said While emit's one production consumer, ci_floor_peak_emit, has cond and body "still raw shell strings". That was true when written and is stale: ecbd086 (#7978, shell -> dag Phase 1 cgroup vertical, 2026-08-08, ancestor of origin/main) replaced both leaves, and the membership assign with them, with derived text from a typed NearestAncestorContaining (std.path_intent) plus extdeps.linux.proc_self_cgroup membership, lowered through bash_orch_if / bash_proc_self_cgroup, refusing with a located marker rather than widening. git log -S on both bash_nearest_ancestor_locate_cond_command and ci_floor_peak_nearest_ancestor_spec, scoped to that file, returns exactly that commit as first introduction. The correction carries the residue forward rather than reading as completion: the peak calibration leaves on the same pipeline and the runtime-scan transport in bash_membership_assign_from_source are still raw String Run.command values, declared Phase 2 typed filesystem observation by the module itself. Three census rows in docs/plans/shell-to-dag-residual-census-and-arc-completion.md carried the same stale claim -- the SS1.A "concat-built floor-peak/cgroup runners" row, the SS4.E already-on-emit row, and the SS4.J Phase-1 dispatch row that still listed the two leaves as unassigned open work. That last one is what dispatched a lane onto discharged work. Sweeping the class turned up a larger root cause, filed as a banner rather than silently truncated: .github/workflows/ci.yml was deleted by 611fd02 (#8283, FLOOR-Y cutover), CI is now the witnesses.yml emission from gunbc.witness_floor_workflow, and this census mentions none of that while still naming ci.yml drift+parse as its byte-oracle in four places. A symbol-existence check over the SS4.J dispatch roster found ~20 named production symbols with no declaration anywhere in the .dag corpus. The banner states the denominator (180 data rows, 41 already closed, ~139 asserting live state) and states explicitly what it does NOT establish: absence of a name is not discharge, since a rename looks identical -- git_fetch_script is gone while git_fetch_no_tags_shell and git_fetch_prune_shell exist. Per-row adjudication needs its own lane. Model-side prose only; no seed growth, no .rs. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013GCBVTWARwTLkAfVWaGfKA * Name the instrument behind the banner's counts, so the banner is not the next stale row The staleness banner cited bare counts (180 data rows / 41 closed / ~139 live) and a ~20-name absent-symbol list. Transcribed numbers under a dated claim are exactly the defect the banner is about, one layer up: nothing re-derives them, so they rot without anyone touching either end. The banner now carries the two checks that produce them, verified to reproduce their stated output as printed at 70925ee, and says to run them rather than read them. It also states the second check's raw output honestly -- 50 candidates, of which the ~20 production symbols are what survives discarding module names, the commit-sha and fn-fragment spellings the banner itself introduced, and already-struck rows -- so the gap between "50 out" and "20 listed" cannot be mistaken for a miscount. The ci.yml deletion is the one claim that is not count-shaped and its own one-line derivation is given. The dispatch prohibition is unchanged and deliberate: a banner that describes staleness while still permitting dispatch off the rows is a documented hazard with no refusal. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013GCBVTWARwTLkAfVWaGfKA * Turn the banner's absent-symbol list into a demonstration, and pin the denominator to its head The banner asserted that absence of a name is not discharge because a rename looks identical. It now demonstrates it, with six names that already have verdicts on main and do not all point the same way: srv3_chown_directory_to_current_user discharged 61bf47b (#8590) host_build_cache_provision_script discharged 40f2fb6 (#8825) four host_hygiene_reap_*_body files deleted ffa16a5 (#8583) git_fetch_script RENAME, not gone (unadjudicated) Three causes, one grep signature. The host_hygiene row is the sharpest: the commit that discharges those four names does not mention them, so the evidence is not reachable from the symbol at all -- which is precisely why the per-row lane cannot be done by symbol search. All four commits are ancestors of main, so the table is head-safe independent of the SS1.C corrections landing separately in #10529. The denominator now says it was measured at 70925ee and is valid only there: any later edit that strikes a row through changes what the closed-marker grep counts, so the 180/41/~139 split moves and must be re-derived rather than quoted. The demonstration table sits inside the blockquote, so it does not itself perturb the row count -- re-derived at 180 after the edit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013GCBVTWARwTLkAfVWaGfKA * Re-derive on the merged tree: correct a worked example reading found, repin the denominator Reading every row either PR touched on the merged tree -- rather than trusting the clean auto-merge -- turned up an error in my own worked-examples table. #10529's srv3 row names a live successor, srv3_ensure_directory_owned_by_current_user (gunbc.host_effect_realize), so srv3_chown_directory_to_current_user was not plain "discharged" as my table said: it was RENAMED AND CLIMBED at once. That is a fourth cause a two-way discharge/rename split cannot express, and calling it discharged loses the successor a reader needs to find. The table now carries all four causes: dissolution, file deletion upstream of the name, bare rename, and rename-plus-climb. The denominator moved exactly as predicted. Re-derived on the merged tree it is 180 rows / 43 closed / ~137 live, against 41/~139 one merge earlier; #10529 striking two more SS1.C rows through is the whole difference. The banner now says so, because a split that moves within one merge of being written is the argument for naming the recipe rather than a bookkeeping detail. Measurement is pinned to the merge of 70925ee with origin/main 16a702e. Controls re-run on the merged tree, not carried forward: the four bash_nearest_ancestor_locate_* call sites still stand and #7978 is an ancestor of the merged HEAD; ci.yml is still absent with witnesses.yml present and #8283 an ancestor; git_fetch_script is still absent while git_fetch_no_tags_shell and git_fetch_prune_shell exist, so the rename example still discriminates. Diff is still model-side prose only -- no .rs, no seed growth. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013GCBVTWARwTLkAfVWaGfKA --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
What this does
realize_provision_build_cachehad exactly one gate — a pure id validation — and then rendered, installed and restarted unconditionally. The semantic admission that should have gated it (gunbc.build_cache_ensureadmit_ensure_build_cache_instance, withgunbc.host_build_cache_provisionplacement_verdict) existed with zero production callers, because nothing in the tree produced its inputs.This PR builds the missing observation producer and wires realize onto the admission. It is one PR rather than the two the brief suggested, per the parent's ruling after the rework below.
gunbc.build_cache_endpoint_observeis a pure decode over read text — no transport of its own.gunbc.host_effect_realizeperforms the reads and threads them in. The chain is the onedocs/plans/build-cache-placement-receipt.mdexecuted by hand and the onegunbc.build_cache_instanceendpoint_ownership_notespecifies:/proc/net/unix(exact path,St==01) → listening inode →find /proc -maxdepth 3 -path '*/fd/*' -lname 'socket:?N?'→ owner pid →/proc/<pid>/{cgroup,stat,exe}, with/proc/sys/kernel/random/boot_idbounding the pass.Five to nine single-argv, non-mutating reads per pass. No
ss, nopgrep, nohead -1, nolsof, no shell — matching both authorities, which were right as written and are unamended.Realize now observes before it acts:
EnsureAlreadyConvergedwrites nothing and restarts nothing (this is the idempotency fix — a healthy unit was previously rewritten and restarted every pass, re-colding the host's build cache);EnsureBuildCacheRefusedreturnsNotConvergedcarrying the located reason; onlyEnsureBuildCacheAdmittedreaches the ensure shell, with an admitted unlink as its own prior command.provision_build_cache_verdictfolds the read-back on the far side. A live wrong owner is refused rather than evicted; a host whose placement could not be read is refused rather than mutated.The false capability claim, and its removal from all five artifacts
An earlier revision of this branch claimed — in three carrier notes, the census doc and this PR body — that clause (3) of the stale-socket contract needs a glob over
/procand therefore a shell this lane may not emit, and usedssinstead. That was false.findtakes the whole walk as one argv.The probe that produced the error used
socket:[N];findreads[...]as a glob character class; it matched nothing; and "found nothing" was accepted as confirmation the walk was impossible.socket:?N?andsocket:\[N\]both resolve, with an empty control on a bogus inode. Independently reproduced by the parent session.The claim is removed from all five, and in the census — the artifact a future reader consults for what is possible — the paragraph is not merely deleted: it states that the boundary was measured and refuted, and by what. A silently removed impossibility claim leaves the next person with no reason to try either.
Consequence:
EndpointStaleSocketis produced and the admitted-unlink arm is reachable rather than dead.Live host mutation this makes reachable
The first real unlink this authorizes would touch srv4, path
/var/lib/ctrl/sccache-ci/server.sock— the stranded socket with no listener that has left that host uncached for about a week, and which under the previous revision would have refused forever.Two defects the reworked witnesses caught
Neither was a fixture problem.
endpoint_path_stateconflated held-open with listening. It answeredEndpointListeningfrom the fd-holder observation alone, so a socket held open by a non-accepting process was reported as a healthy listening endpoint. Clause (2) (no LISTEN entry) and clause (3) (no fd holder) are separate reads and neither may answer for the other; a decoder that lets one answer for the other has collapsed a four-clause contract into a two-clause one. Both states refuse, so nothing was destroyed — but they refuse for different reasons and only one is true, andEnsureEndpointOccupied("a live server is serving here") is the wrong sentence for an operator whose cache is unreachable precisely because nothing is serving. Now routed throughsocket_owner_path_state.A
ProcessIdentityname collision — the §3 nicknaming class inside the subject being modeled. The witness module had no import block, so the bare name resolved corpus-wide. There are two:gunbc.build_cache_instance(record:boot_id,pid,start_time) andsrc/v2/extdeps/posix.dag(record:id,command,parent). Under the whole-corpus floor posix won, and CI refused withno field 'pid' on type 'ProcessIdentity'. A targeted compile of the same entry resolved a closure that never loaded posix and reported zero blocking diagnostics. Imported explicitly now, with the measurement recorded in the module — a green targeted compile is not evidence that a bare name is unambiguous.Recorded, not repaired
A server that is our unit, holding its socket open while not listening, short-circuits to
EnsureAlreadyConvergedon the placement axis without ever consulting the path — so ensure reports converged while the cache is unreachable. It predates this wiring (the fold is unchanged here), and closing it changes what ALREADY-CONVERGED means: the converged arm would have to require a LISTENING path, not merely our unit's ownership. That is a decision about the admission's contract, not its consumer. Named beside the witness that measures it (witness_our_own_unit_holding_an_unlistened_socket_reads_converged) so the next reader finds a measured boundary rather than re-deriving it from a failing fixture./proc/net/tcpownership is genuinely unmodeled. NoBuildCacheInstancein the tree carries a TCP endpoint; that arm is a positive typed refusal rather than an untested path that answers.The standing rule this lane adopts
Every probe that licenses an action on an empty result carries a same-run non-empty control. Load-bearing twice over here: the holder walk's EMPTY result is the evidence that licenses an unlink, so an unlink authorized by a probe that silently matches nothing is a data-loss defect, not a refusal defect. It is written into the witnesses (
empty_licensing_probe_rule_note) and enforced by the pairwitness_stale_socket_is_admitted_behind_an_unlink/witness_socket_held_open_without_listening_is_not_unlinked, which differ in exactly one input and must land on opposite arms.witness_holder_argv_cannot_regress_to_the_bracket_formpins the argv itself, since no fixture can see an argv regression.Evidence
claim_batch --hermetic), including both discriminating REDs above.dag/gunbc/host_effect_realize.dagand the witness entry each typecheck to the same 2 hard diagnosticsorigin/mainalready carries (gunbc.Cli) — none added.unit_linesis bound to_and never read. sunny-ant-215 has renamed and retyped it tounit_file: SystemdUnitFilewith arity unchanged; whoever merges second takes the one-token edit.— sent from zesty-wolf-464