Repository navigation
srvN quality sweep: enrollment wall, swap-backing axis, read-back independence criterion - #7235
Merged
Merged
Conversation
…server was a no-op) Follow-up to #7170. Live execution on srv3 caught what the string witnesses missed (§5 specification-without-execution): the modeled unit was Type=simple ExecStart=/usr/local/bin/sccache --start-server # daemonizes, exits 0 so systemd saw the ExecStart exit cleanly and marked the unit `inactive (dead)` the instant it started; the backgrounded server idle-timed-out unsupervised and Restart=on-failure never fired (success exit). The unit was a no-op — sccache survived only via its own per-invocation auto-start. The string witness "ExecStart equals the install path" was green the whole time. Fix (grounded by execution on srv3 first): foreground the server, matching the production ctrl-sccache.service invocation verified running month+ on srv1/srv2: Type=simple Environment=SCCACHE_START_SERVER=1 Environment=SCCACHE_NO_DAEMON=1 ExecStart=/usr/local/bin/sccache This reduces the §3 fork between the modeled unit and production rather than minting a third shape. Closes the execution gap two ways: build_cache_unit_is_foreground_supervised is a construction check that makes the defective combo (Type=simple paired with a backgrounding --start-server) UNWRITABLE (carries the CI grain, since systemd --user is not runnable in the hermetic container), and the live srv3 re-provision carries the runtime is-active grain. Census note accounts the +1-line delta as a correctness swap toward the cited production authority. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ependence criterion Three quality items over the "modeled" middle of the host-standup spine, each landing with a discriminating RED control run by execution. 1. Enrollment construction wall (runner_host_deploy). No function takes a bare RunnerHostDeploy and yields an ArgvCommand any more: both command builders consume a RunnerHostAdmission and return RunnerCommandOrRefusal whose refusal arm carries no command, so a host absent from fleet_intent cannot produce installer or enable argv at all. Honest residual named in-code: .dag has no visibility modifiers, so RunnerHostEnrolled can be hand-forged — an explicit lie rather than an accident; closes when node/subtree visibility grants land. 2. Swap backing as a modeled axis (host_swap_backing). The corpus already converges MemorySwapMax = 32 GiB per slot over a resource whose existence nothing models — systemd stores and reports a ceiling byte-for-byte on a host with zero swap devices, so the knob greens over nothing. The requirement is DERIVED from the declared cap rather than authored per host (no fleet reach from a session container, so a per-host swap table would be invention); backing states stay separable (no producer / zero / undersized / sufficient, four different pieces of work); and a cap verdict is qualified by its backing, asymmetrically — a presupposition check, pinned by witness against becoming a lattice meet. The observation frontier is a counted number (4 of 4 hosts UnknownRefused today), so a fabricated fixture reds the witness instead of greening the matrix. Effect realization is blocked on the argv materializer's hardcoded five-parameter vocabulary and is declared, not stubbed. 3. Read-back independence as a standing criterion (readback_independence). #7213 Finding 2 generalized off one host: a read-back is evidence only if performing the read could not have established the subject. Asymmetric correction (tainted negatives survive; only Converged is rewritten, to UnknownRefused so the deficit stays countable), unclassified probes treated as tainted, and inert probes keep their evidence so the criterion is non-vacuous in both directions. Live consumer: host_swap_backing routes every host verdict through it; the witness proves the routing is load-bearing by substitution, since /proc/swaps is inert today. Witnesses: 7 swap conjuncts, 7 read-back conjuncts, 4 wall conjuncts — all PASS. RED controls: perturbing swap_cap_verdict_qualified_by_backing to be backing-blind and readback_evidence_verdict to trust the probe FAILs both witnesses; perturbing admit_runner_host to admit everything reds 3 of 4 wall conjuncts with enrolled_host_still_admits correctly staying green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot
Bot
force-pushed
the
session/vivid-wolf-453
branch
from
July 25, 2026 20:53
a5d5487 to
736bc9e
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Item 3 of the operator's three-item direction: the quality sweep over the "modeled" middle of the host-standup spine. Three pieces, each with a discriminating RED control run by execution.
1. Enrollment construction wall —
gunbc.runner_host_deployRunner-host commands were built from a bare
RunnerHostDeploy, so nothing structurally prevented producing installer/enable argv for a host that is not afleet_intentrow. Now no function takes a bare deploy and yields anArgvCommand: both builders consume aRunnerHostAdmissionand returnRunnerCommandOrRefusalwhose refusal arm carries no command — the bad state is unwritable rather than checked after the fact (DESIGN §5 construction-over-validation).Honest residual, named in-code:
.daghas no visibility modifiers, soRunnerHostEnrolledcan still be hand-forged. That is an explicit lie rather than an accident, and it closes when node/subtree visibility grants land.2. Swap backing as a modeled axis —
gunbc.host_swap_backingThe finding this piece surfaced is the reason it is worth having: the corpus already converges a swap cap over a resource whose existence nothing models.
runner_slot_allocationdeclaresmemory_swap_max = 34359738368(32 GiB) per slot,host_convergedrives it asMemorySwapMax,runner_unit_live_readreads it back and reportsConvergedon a match. Every step is correct in isolation and the composition proves nothing, becauseMemorySwapMaxis a ceiling: systemd stores, reports, and matches it byte-for-byte on a host with zero swap devices. Corpus-wide there are zeromkswap/swapon/fallocate//proc/swapsoccurrences — swap exists only as prose infleet_acceptance_criteriaand as the floor-timeout mechanism inci_budget_tree.MemorySwapMaxis declaring that backing must exist, so the requirement falls out ofgunbc_runner_slot_desired().memory_swap_maxand moves when it moves. Declared limit:min_totalis the per-slot cap, not slots × cap — the aggregate question is unmeasured and multiplying would assert a worst case as fact.UnknownRefused(build one), zero →Absent(provision), undersized →Drifted(resize), sufficient →Converged. No "assume the distro default gave us swap" arm: srv1..srv4 were installed across at least two paths, so its error rate would be unmeasurable by construction.UnknownRefusedtoday; the count is pinned by witness, so a fabricated fixture reds rather than greening the matrix.Effect realization (
fallocate/mkswap/swapon/fstab,/proc/swapsread) is blocked on the argv materializer's hardcoded five-parameter vocabulary and is declared, not stubbed — declaring unreachable operations would add census rows no consumer can reach.3. Read-back independence as a standing criterion —
gunbc.readback_independence#7213 Finding 2 was recorded as a note beside one verdict fold. Generalized: a read-back is evidence about a subject only if performing the read could not have established the subject. The class is not rare — a client that auto-starts its daemon, a mount check that triggers an automount, a token read that refreshes the token, an ensure-shaped operation used as a query. The tell is about the transport, never the value: could running this have made the answer true?
Convergedis rewritten, and toUnknownRefusedrather thanAbsentorConflict, so the deficit stays countable.systemctl show/is-activeand a/proc/swapsread are classified inert and keep theirConverged; a criterion that refused every probe would be the absorbing fallback wearing a safety badge.Live consumer:
host_swap_backingroutes every host verdict through it. The routing is a no-op today, so the witness proves it load-bearing by substitution — the same verdict carried by the sccache probe is refused.Verification
swap_cap_verdict_qualified_by_backing→ backing-blind ⇒FAIL host_swap_backing_witnessesreadback_evidence_verdict→ trust the probe ⇒FAIL readback_independence_witnessesadmit_runner_host→ admit everything ⇒ 3 of 4 wall conjuncts red,enrolled_host_still_admitscorrectly stays green (non-vacuity control)Plan doc gains §5.5 (criterion) and §5.6 (swap presupposition). No merged module's behaviour changes.