Skip to content

srvN build-cache: de-fork the sccache install authority on the P1b provisioning path - #7170

Merged
briansrls merged 37 commits into
mainfrom
session/vivid-wolf-453
Jul 25, 2026
Merged

briansrls merged 37 commits into
mainfrom
session/vivid-wolf-453

Conversation

@briansrls

@briansrls briansrls commented Jul 24, 2026 •

Copy link
Copy Markdown
Contributor

Follows up #7159 (doc-only) with the code for the sccache defect its census named. Goal per operator: get srvN subsumption working; the sccache issue exposed anemic modeling, and that rework lands here. The scope grew beyond the sccache install fork as the subsumption spine was walked end-to-end — the sections below describe each piece. All of it is one lane (srvN subsumption), reviewed head-verified at 5d910837e.


1. sccache install de-fork (the origin)

The subsumption spine had two ways to install sccache on a fleet host, firing on the same host in sequence:

phase authority source verified lands at
P1:runner-deploy-slot extdeps.cache.sccache.sccache_install_script pinned v0.15.0 release tarball per-arch sha256 /usr/local/bin/sccache
P1b:build-cache-provision hand-rolled sudo -n apt-get install -y sccache none /usr/bin/sccache

P1b then wrote a systemd user unit with ExecStart=/usr/bin/sccache --start-server — a path the modeled install never creates. The daemon could not start and the read-back refused. The fail-closed wall was refusing a state the emitter created by forking the concept — exactly #7159's "the emitter names no concept."

  • One install-path authority. sccache_installed_binary_path is read by both sccache_install_script and the unit ExecStart, so the two phases cannot disagree. The apt fork is deleted; the ensure arm calls the cited script.
  • Arch is derived, not constant. From the effect target's own ComputeHost CpuFacts.architecture. sccache_release_arch_token / sccache_release_digest are partial over the Architecture coproduct → an unpublished arch yields typed NotConverged. No default arch (the fabricated-plausible-output §5 forbids).
  • The classifier is a fold over the cited roster sccache_misconfigured_log_fragments, not three unrolled if/elif branches, plus a shell-quoting totality check (build_cache_fragment_words_are_shell_safe).
  • New PATH-authority wall. CI consumes the cache as bare sccache (RUSTC_WRAPPER=sccache); a healthy sccache earlier in PATH is the two-authority state, invisible to an absolute-path read-back. The judgement (DaemonPathShadowed/RefusalPathShadowed + verdict fold) lives in the model; its live observation is staged on the typed-argv dissolve-on (General orchestration intent to Bash emit fold over grammar rows #5828), not emitted as hand-shell (the A5 census scaffold must not grow its shell surface).
  • loginctl enable-linger. A systemd --user manager dies with the provisioning ssh session, so the read-back would green on a daemon already gone. (Acknowledged as new-but-bounded shell in the census note; does not settle user-vs-system scope — open.)
  • Located refusal. Build-cache failures reported as OsInstallActuatorToolchainEnsure because they reused a fold hardcoding the effect name; the header is now a parameter.
  • Census §4.I absorbing fallback is counted. ci_sccache_provider_shell_injection's bare if gained an else emitting CiSccacheProviderReceipt: provider=SKIPPED … host=$(hostname) — deliberately loud, not refusing; STEP 2's fail-closed flip is operator-sequenced after a live T4 read-back.
  • ci.yml + falsifier.yml regenerated from the model (main_wet), +3/+3.

2. HostToolchainReach — the target/access pairing (a §5 fail-open, fixed by construction)

Access used to be looked up from the requested host while the target was resolved kind-aware, so a BuildCache request for srv3 targeted srv3 but authenticated to srv1 — the effect would land on the wrong machine and report success. host_toolchain_ensure_access is replaced by HostToolchainReach { target, access } where access is derived from the resolved target, making the mis-pair unwritable rather than checkable-after. Witnessed by reach_access_host_is_the_target_host (compares the two sides) with the negative control reach_wrong_machine_pairing_is_unwritable (reconstructs the old shape by hand and shows it violates the predicate). Side effect: this stops consuming ci_deploy_srv1_operator_access (construction-identical to host_identity_srv1_access — a §3 nickname whose corpus-wide dissolution is a separate lane).

3. host_authorized_keys_reconcile — a faithful membership_reconcile instantiation

The root modeling gap the sccache issue rhymed with: a host's authorized_keys is materialized once and never reconciled against fleet_ssh_access.fleet_authorized_keys. This instantiates the membership_reconcile spine (member = SshPublicKey, key_of = material, ownership derived from fleet_authorized_keys — never hand-copied) with zero spine change. Material-keyed identity means a foreign key structurally cannot take the Modified arm. R5 (teardown-owned-only) holds: an out-of-band key → OwnershipUnknown → refused, never torn down. The rotation extension is a declared trigger, not built silently. The module produces the plan grain only, consciously reserving the apply policy (see §7).

4. Network grounding (dissolving anemic brands; extdeps.network.*)

New cited leaves, RFC-anchored, consumed (no floating islands):

  • extdeps.network.ipv4 — Ipv4Address = four Octets (Int where range(0,255), the bounded-Int idiom Port already uses), wire-parse refuses with a typed located Ipv4ParseError (wrong-count / out-of-range / non-numeric), round-trip witnessed. Dissolves the dissolve_on_ipv4_address_anemic_brand trigger; the dag/extdeps/dhcp/v4.dag Ipv4Address = NonEmptyStr where brand is gone and its 9 consumers migrated to the constructor. network_identity_subsumption.dag bare IPv4 literals migrated too.
  • extdeps.network.{ipv6,address,endpoint,reach} — IpAddress = V4|V6 (v6 render staged, render_ip_address returns Absent not a fabricated string), NetworkHost, SocketAddress (reuses Port), and Reach = DirectLan | ProxyJump | FabricTunnel cited to OpenSSH ssh_config, with FabricTunnel refusing realization (typed, not a silent fall-through).
  • gunbc.fleet_reach.srv3_reach — the concrete ProxyJump{via: srv2} interim (operator-sanctioned stand-in for the not-yet-working fabric), grounded on the ipv4 leaf, with srv3_reach_fabric_intended making the dissolution target a real value that honestly refuses today (not prose).

5. srv3 witnesses + live receipts

test.claim.srv3_subsumption (real observed fixtures — operator macbook reads of srv3/srv4, dated): srv3 yields exactly one named upsert (fleet-automation) + two named refusals (the out-of-band keys, OwnershipUnknown); srv4 is the empty-plan negative control; the R5 RED (reconcile_would_teardown_only_if_ownership_claimed_it) reconstructs the hinge — a lying ownership fn would emit teardowns, proving the refusal is caused by ownership_of, not incapacity. Reach + pairing witnesses alongside.

Grounded live (read-only, and one operator-authorized write): srv3 is reachable session→srv2→ubuntu@srv3 (node-orch@srv2 key; the reach realizes as nested-exec since srv2 forbids -J), aarch64/128c; the reconcile's srv3 plan was applied live (fleet-automation appended, R5-safe, 3 pre-existing keys untouched); the P1b sccache unit was provisioned and read back active/enabled.

6. Witness consolidation (floor cost-shape)

The six new witness files each paid a full whole-tree closure resolve in the floor and pushed batch 3 over its wall budget. Consolidated by shared closure into two entries — test.claim.srv3_subsumption (gunbc closure) and test.claim.network_grounding (extdeps.network closure) — a §6 cost-shape fix (fewer entry resolves, zero coverage lost; all 36 witnesses green). The wet witness roster (bin_witness_wet_entries pattern + rows) is re-pointed — no orphans from the 6→2 move.


Not decided here (surfaced, not smuggled)

  • Apply-grain policy for everything-on-host observed scopes — wholesale-refuse vs siblings-continue (membership_effects_wholesale_refuse_policy_note). authorized_keys is an EVERYTHING-ON-HOST scope where foreign keys are normal, so the spine's wholesale-refuse would wrongly block the owned upsert. The module refuses to decide this and produces the plan grain only; it gates the live srv3 apply alongside the operator write go-ahead and the account-reconcile follow-on's Modified-arm ownership semantics.
  • Follow-on lane (backed by observed fleet data): user/sudo reconcile (gated on Modified-arm consulting ownership_of → MemberAdoptRequired + visudo -c validate-before-install), grounding the sccache model against the real host-wide shared-UDS ctrl-sccache.service (production is a system service), fleet-wide key homogenization (srv1/srv2 miss fleet-automation), stale-key cleanup, srv4 recovery (host offline), static-lease automation on the modeled CR1000A, and step-(b) transport decomposition (SshShell carries a Reach).

Green by execution

host_build_cache_provision_design_witnesses PASS (run before/after the architecture_diagnostic_name switch); the wet provision_read_back_failure_not_converged_by_real_execution PASS (real fake-sccache on disk, off-PATH, exercises the read-back arm); all 36 consolidated witnesses PASS; whole-tree compile-clean under --dependency-pool-index primary-precedence; regen drift-free. Merge is squash (WIP commit subjects flatten).

Brian Searls and others added 4 commits July 24, 2026 15:22
…ovisioning path

The srvN subsumption spine had TWO authorities for "install sccache on a fleet
host", firing on the same host in sequence:

  P1:runner-deploy-slot   -> extdeps.cache.sccache.sccache_install_script
                             pinned v0.15.0 tarball, per-arch sha256 verified,
                             lands at /usr/local/bin/sccache
  P1b:build-cache-provision -> hand-rolled `sudo -n apt-get install -y sccache`
                             unpinned, unverified, plus a systemd user unit whose
                             ExecStart=/usr/bin/sccache

So the unit pointed at a path the modeled install never creates: the daemon could
not start, the read-back refused, and the fail-closed wall was correctly refusing
a state the EMITTER had created by forking the concept (the "emitter names no
concept" shape recorded in the shell->dag census 4.I / #7159).

- sccache_installed_binary_path is now the single authority for where the cited
  release lands; both the install script and the unit ExecStart read it.
- The ensure arm calls sccache_install_script; the apt fork is deleted.
- Arch is DERIVED from the effect target's own ComputeHost CpuFacts.architecture.
  sccache_release_arch_token / sccache_release_digest are partial over the
  Architecture coproduct, so an arch the cited release does not publish yields a
  typed NotConverged. No default arch (5: never fabricate a plausible binary).
- The misconfigured-fragment classifier is a FOLD over the cited roster
  sccache_misconfigured_log_fragments instead of three unrolled if/elif branches,
  so citing a fourth fragment costs zero emitter edits.
- NEW path-authority guard: CI consumes the cache as bare `sccache` on PATH
  (RUSTC_WRAPPER=sccache), so provisioning the modeled binary is not sufficient —
  a healthy sccache earlier in PATH is the two-authority state itself and is
  invisible to an absolute-path read-back. It now REFUSES, typed and located.
- loginctl enable-linger: a systemd --user manager dies with the provisioning ssh
  session, so the read-back would green on a daemon already gone. Does NOT settle
  open question 1 (user vs system scope) — that stays operator-open.
- The refusal is LOCATED: build-cache failures reported themselves as
  OsInstallActuatorToolchainEnsure because they reused a fold that hardcoded the
  effect name in its header. The header is now a parameter.
- ci_sccache_provider_shell_injection's bare `if` gained an else emitting a
  counted CiSccacheProviderReceipt naming the host. Deliberately LOUD, NOT a
  refusal: STEP 2's fail-closed flip is operator-sequenced after a live T4
  read-back, and refusing first would red the fleet.
- ci.yml + falsifier.yml regenerated from the model (main_wet), 3 lines each.

Green by execution:
  PASS host_build_cache_provision_design_witnesses (claim_batch, 396 modules /
  7232 items in closure) — 8 new assertions incl. the emitted script contains the
  cited release URL and NEITHER apt-get NOR /usr/bin/sccache; ExecStart equals the
  install-path authority; the classifier covers every cited fragment AND contains
  no elif (re-unrolling reds); arch token/digest Absent for Riscv64/Wasm32; a host
  with no readable CPU refuses realization; srv1's real row still resolves aarch64
  so the refusal path is not trivially always-on.
  Direct bash execution: emitted script syntax-valid; classifier fold classifies
  all three cited fragments and falls through on a fourth input; path guard
  refuses a shadowing binary (exit 1) and passes when nothing is on PATH.

The two new wet witnesses are enrolled in bin_witness_wet_entries — that roster is
keyed per test fn, so they would otherwise have been orphans (enrolled, zero
executions).

NOT done here, and not claimed: the live leg. This container reaches srv1/srv2/srv4
on :22 but holds no fleet ssh key and no ADC, so P1b has NOT been run against a
real host — that is gap A2 (reach-secrets) in fleet_subsumption_manual_gaps. This
lands at T1/T2; T3/T4 receipts need an operator-supplied credential.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review July 24, 2026 15:52
@gunbai-bot gunbai-bot Bot changed the title srvN subsumption srvN build-cache: de-fork the sccache install authority on the P1b provisioning path Jul 24, 2026
@cursor

cursor Bot commented Jul 24, 2026

Copy link
Copy Markdown

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

Brian Searls and others added 5 commits July 24, 2026 16:37
…back to 6 builders

Operator review: this module is a DECLARED SCAFFOLD whose dissolution trigger says
it should be going away, and the shell->dag census keys it as an A5 `decompose` row
(host_effect_realize.ProvisionBuildCache), deferred 2026-07-22 — real debt, NOT
done. The previous commit added a 7th `build_cache_*_body` to it. That is exactly
the failure the census predicts in prose:

  "while a raw-shell builder exists in the tree, LLMs copy it — one anemic
   concat(\"sudo -n \", …) becomes ten ... assume anything left behind is
   duplicated/triplicated"

The finding (a healthy sccache earlier in PATH is the two-authority state, and no
absolute-path read-back can see it) is real and kept. Only its LOCATION was wrong.

Model now owns the judgement (gunbc.host_build_cache_provision):
  - DaemonPathShadowed { resolved, expected } on BuildCacheDaemonObservation —
    carries BOTH paths so the refusal is located, not merely typed.
  - RefusalPathShadowed on BuildCacheProvisionRefusal.
  - verdict fold refuses fail-closed; the gate accepts only that refusal.
  - the widen sketch fabricates Converged on shadow, so the RED control has a real
    forbidden behaviour to reject rather than asserting a tautology.

Script only OBSERVES, and SHRANK:
  - build_cache_path_authority_guard_body DELETED.
  - the observation became build_cache_path_authority_lines() -> List<String>,
    appended into the two bodies that already existed (observe + read_back), so
    both checkpoints survive with no new builder.
  - builder count 7 -> 6, matching the census row exactly.

Routing (why shell was the wrong home at all): this site is RUNTIME-PRESENT — it
realizes through host_effect_apply_gated on LocalShell/SshShell — so per the census
routing decision its end state is a typed effect-plan with NO bash emitted. The
deploy-preflight precedent is the target shape: a typed predicate over captured
values (Not{StrEq}, never a minted StrNeq). There is no `command -v` typed op in
extdeps/os today; that is a §5.A new-op row, and §5.E's TransportScript
construction wall — the thing that would have made my 7th builder a type error —
is still awaiting the operator's wall-first-vs-migrate-now decision.

Census standing recorded ON THE CARRIER (host_build_cache_provision_script_census_
row_note), not in a PR description that evaporates: A5 decompose, deferred,
runtime-present, and the standing constraint that this module may SHRINK but must
not GROW — a new *_body here is a census regression even when the behaviour it
adds is correct.

Green by execution (claim_batch):
  PASS host_build_cache_provision_design_witnesses — adds path-shadow fail-closed
    refusal (reason names both paths), the widen-rejected RED control, and a check
    that the path-authority observation lives in the two existing bodies rather
    than a separate builder.
  PASS provision_read_back_failure_not_converged_by_real_execution
  PASS provision_path_authority_refuses_healthy_shadowing_sccache
  PASS provision_path_authority_passes_when_no_sccache_on_path
    (--wet; the read-back witness's fake binary moved OFF PATH so it exercises the
     read-back arm rather than short-circuiting on the shadow check, and asserts
     path_authority=SHADOWED is ABSENT.)

No ci.yml impact — the provisioning script is not part of the emitted workflow.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

Post-approval delta — please re-read this part

The five approvals above landed on the sccache de-fork scope. Two commits since then added srv3 to the model at the operator's request, and doing so surfaced a wrong-machine fail-open that the same lane would have hit. Flagging it explicitly so the approval tally isn't read as covering it.

What was wrong. host_toolchain_ensure_target_host was kind-aware — srv3 + OsInstallActuator resolves to the selected actuator host — but host_toolchain_ensure_access keyed on the requested host alone and pinned srv3 to ci_deploy_srv1_operator_access. Target and access were two independent decisions, so they could disagree:

  1. host_toolchain_ensure(host: srv3, kind: BuildCache) targeted srv3 and authenticated to srv1 — the provisioning effect lands on the wrong machine and reports ExitSuccess. That is the exact kind this PR adds (P1b).
  2. The srv1 pin is only correct in the actuator selector's ActuatorUnsatisfiable fallback arm. Whenever ActuatorSelected names a different host, access still pointed at srv1.
  3. host_runner_memory_provision.provision_runner_memory_caps consumed the same lookup and inherited defect (1).

Fix — construction, not validation (§5). Access is now derived from the resolved target, returned as one HostToolchainReach { target, access }, so a disagreement is unwritable rather than checkable after the fact. The two Absent arms became a typed HostToolchainReachOutcome coproduct so the diagnostics stay distinct and located; ReachAccessAbsent now names the target identity (the useful fact) alongside the requested one.

Proven by execution, dag/test/claim/host_toolchain_reach_pairing_witness_test.dag (6/6 PASS):

  • reach_wrong_machine_pairing_is_unwritable — reconstructs the old shape by hand and shows it violates the pairing predicate, so the predicate is proven to discriminate, not assumed to.
  • reach_build_cache_on_srv3_targets_srv3_not_the_actuator / reach_os_install_actuator_on_srv3_runs_from_the_actuator_host — the two kinds resolve to different machines, both self-consistent.
  • host_toolchain_srv1_access_rows_are_one_concept — ci_deploy_srv1_operator_access and host_identity_srv1_access are construction-identical (principal, host, transport, privileged commands). This is what makes the change behavior-preserving on the existing actuator path, and it records a §3 nickname whose corpus-wide dissolution is a separate lane, deliberately not smuggled in here (7 other consumers).

Also: fleet_intent_network_topology_endpoint_count_holds reds on any topology edit but says nothing about which endpoint appeared, so srv3 landed with a discriminating companion (fleet_intent_network_srv3_addresses_holds) asserting both addresses and the host/BMC role split. RED control run by hand: collapsing the host endpoint's role to BmcOutOfBand → FAIL, restore → PASS.

Regression set green: srv3_runner_memory_converge, host_build_cache_provision_design, srv3_os_install_reconcile (15), host_converge_slice1, fleet_intent_network (5). Generated-artifact regen: no drift.

Not claimed: srv3 is modeled and compiles, not reachable. The fleet key is authorized for no user probed on .221 (briansrls/ubuntu/root/installserver all refuse publickey), so the first live use fails closed — tracked as fleet_subsumption_manual_gaps A1/B2, not papered over.

— sent from vivid-wolf-453

Brian Searls and others added 15 commits July 24, 2026 19:48
The new host_authorized_keys_reconcile witness constructed a bare `Owned`
value in its RED-control helper. `Owned` is defined in TWO modules
(gunbc.ownership and extdeps.languages.rust.types), so it resolves under
scoped claim_batch (small pool) but is undefined/ambiguous under the
whole-tree compile-clean gate (--dependency-pool-index primary-precedence),
which the PR triggered by touching ci.yml (outside the selectable universe
-> whole-tree baseline).

Derive the "always Owned" lie from authorized_key_ownership(macbook) instead
of naming the ambiguous variant. Both symbols are unique. Verified: the exact
gate compile now has zero hard diagnostics; all 6 witnesses still PASS
including the lying-ownership RED control.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Continues the transport decomposition's leaf-grounding, toward reach.dag.

- extdeps/network/ipv6.dag: structured Ipv6Address (eight Int-where-range(0,65535)
  groups, the Port bound idiom; RFC 4291/5952 cited). Type + constructor grounded;
  the RFC 5952 string codec is STAGED with a dissolution trigger (reuses base16,
  zero fleet v6 consumers — §6, don't build for a host that doesn't diverge).
- extdeps/network/address.dag: IpAddress = IpV4 | IpV6, the honestly-closed
  coproduct. render_ip_address is fail-closed on v6 (returns Absent, never a
  fabricated v6 string, §5).
- extdeps/network/endpoint.dag: NetworkHost = HostByName | HostByAddress (reuses
  the already-grounded HostName + IpAddress — this is the leaf ssh_host grounds
  onto), SocketAddress reusing std.types.Port verbatim.
- network_address_host_witness_test: 7 witnesses green, incl. the v6-render-refuses
  fail-closed control. All new names unique; whole-tree compile-clean.

Next: reach.dag (OpenSSH ProxyJump cited; srv3 = ProxyJump via srv2 interim).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jul 25, 2026

Copy link
Copy Markdown
Contributor

Disposition of review 42343's four findings (all on the current head fb590ab):

1. Medium-string growth on the "must not grow" A5 scaffold [BLOCKER] — FIXED. The command -v sccache PATH-observation was unwound out of host_build_cache_provision_script.dag: build_cache_path_authority_lines and both splices into build_cache_observe_stats_body / build_cache_read_back_body are removed, so the emitted shell surface no longer grows. The PATH-shadow judgement stays in the model (DaemonPathShadowed / RefusalPathShadowed + the verdict fold, proven by design_witness_path_shadow_refuses_fail_closed against a synthetic observation); its live observation is staged on this module's own dissolve-on (typed argv, #5828). The census note and build_cache_path_authority_note now state this explicitly, and design_witness_path_authority_observation_not_emitted_as_shell reds if the shell surface regrows. Your census point was right — the earlier "count stayed at six" defense counted *_body builders, not the emitted surface.

2. octet_value_at returns 0 on parse failure (absorbing fallback) — FIXED. Replaced the parse_octet_at(Optional)+octet_value_at(0-widen) pair with a single-parse OctetResult = OctetOk{value} | OctetErr{error}; parse_ipv4_address nests on it and the first OctetErr yields Ipv4ParseFailed. No value is fabricated on failure — the error is typed and located.

3. Loopback ==127.0.0.1 should be the /8 — FIXED. is_loopback now tests a.octet1 == 127 (RFC 1122 127.0.0.0/8), with the discriminating control ipv4_loopback_is_the_whole_slash8 (127.5.5.5 is loopback, 128.0.0.1 is not).

4. Shell-safety build_cache_fragment_words_are_shell_safe is validation-after-fact, not construction — REPLY, not fixed. Agreed it is validation. The construction alternative — a ShellSingleQuotedWord smart constructor that makes an unescaped quote unwritable — is machinery for a surface this module is committed to delete: the typed-argv realization (#5828, this file's declared dissolve-on) removes shell quoting entirely, so the quoting concern does not survive the scaffold. Building the constructor now is work for a deleted surface (the §6 purity trap). The check is meanwhile fail-closed, not a widen: a cited fragment containing ' folds to false, which reds design_witness_fragment_words_are_shell_safe — the line stops on a bad fragment rather than emitting a broken word. So it is an interim guard on the scaffold, dissolving with the scaffold, not a permanent post-hoc check standing where construction was available.

— sent from vivid-wolf-453

@gunbai-bot

gunbai-bot Bot commented Jul 25, 2026

Copy link
Copy Markdown
Contributor

Thanks — both APPROVEs' non-blocking notes handled in 1241f9b386:

  • Endpoint addresses still bare strings (§3 half-consumed) — added a 🟡 dissolve-on note (network_endpoint_address_grounding_residual_note) recording that NetworkEndpoint.address / NetworkSegment literals stay strings until product.network_topology re-types the field onto extdeps.network.address.IpAddress. That's a product-layer field change + consumer migration, deliberately deferred rather than half-done, now visible instead of silently forked.
  • as String == over NonEmptyStr in the new reconcile file — dropped; compares at NonEmptyStr directly now. (NonEmptyStr is a Value::Str at runtime so it was behaviorally identical, but you're right not to codify the straddle-looking idiom in a new file.) All 5 reconcile witnesses stay green.

Leaving two as-is:

  • type HostToolchainReach = HostToolchainReach { ... } reads as a coproduct — this is the idiomatic .dag single-constructor record declaration (same shape as SocketAddress, Ipv4Address, etc. in this PR); no change.
  • A5 census "may SHRINK, must not GROW" is roughly net-flat — confirming the trade explicitly: apt-get install + ExecStart=/usr/bin/sccache unit lines went out, the cited-tarball install + loginctl enable-linger came in. The pledge forbids GROW, and flat satisfies it; the reason the swap is correct (not just neutral) is that it de-forks the install authority onto one sccache_installed_binary_path row — the whole point of the P1b fix — so the net-flat line count buys a removed §3 fork. The census note locates that judgment in the model; this is the explicit confirmation you asked for rather than leaving it to inference.

— sent from vivid-wolf-453

Brian Searls and others added 3 commits July 25, 2026 02:11
…census-note honesty

srv3 is a fabric-only target; the operator-sanctioned interim is a ProxyJump
through srv2 (reachable) standing in for the not-yet-working fabric. New
gunbc.fleet_reach models this on the extdeps.network.reach model built earlier
in this lane:
- srv3_reach = ProxyJump{jumps:[srv2], target:srv3}, grounded on
  extdeps.network.ipv4 (grounded srv2/srv3 Ipv4Address rows — the convergence
  target the fleet_intent_network bare-string endpoint residual dissolves onto,
  cross-linked both ways so the transitional dual representation is marked debt
  toward one authority, not a fork).
- srv3_reach_fabric_intended = FabricTunnel{srv3} — the dissolution target made
  a real value that HONESTLY refuses realization today (the §5 control).
- GROUNDED LIVE 2026-07-25: from srv2, an ssh handshake to srv3:22 returns
  Permission-denied for every probed user — a refused AUTH, not a network
  failure, which PROVES the network reach via srv2 is realizable while the
  shell/auth transport is fail-closed (srv2's key trusted by no srv3 user — the
  A1/B2 credential gap). That is exactly the operator's reach-independent-of-
  shell split, proven by execution: reach realizable, shell gated, held separate.
- host_identity_srv3_access note wires the split: SshShell realizes OVER
  srv3_reach; encoding the jump INTO the transport (SshShell carries a Reach) is
  step b, coordinated with the shell->dag transport-wall lane.

Witness (fleet_reach_witness_test): single-hop proxy, network realizable, target
is srv3's grounded .221, jump is srv2, fabric-intended refuses (RED control).

Also addresses review 42401's census-note finding: the "must not GROW the shell
surface" pledge is restated precisely — new shell must be a deduction or a cited
de-fork swap; the sccache de-fork's apt->cited-install swap and the genuinely-new
`loginctl enable-linger` leaf (bounded, required for the user-scope handler) are
both acknowledged rather than hidden behind a blanket no-growth claim.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jul 25, 2026

Copy link
Copy Markdown
Contributor

Thanks — census-note finding handled in c44ea4e2a4. The pledge is now stated precisely: new emitted shell must be a deduction or a cited de-fork swap, never an uncited unbounded addition. The two exact deltas are accounted rather than hidden behind a blanket "no growth":

  • the sccache de-fork swap (apt-get install + /usr/bin/sccache unit out, cited-tarball sccache_install_script in) — the §3 fork removal this PR exists for;
  • loginctl enable-linger acknowledged as genuinely new shell — bounded (one fixed leaf, not a corpus-denominated fold), required to make the already-selected user-scope systemd handler viable, justified in build_cache_user_service_linger_note.

What must-not-grow is scoped to the PATH-shadow observation (which is what the note actually argues, and is staged on #5828). Your ci_materialization #2 needs no change — it's the operator-sequenced STEP-2 interim (loud + host-attributable, flip-to-refuse after live T4 read-back), agreed.

Separately, this push also lands the srv3 network-reach model (gunbc.fleet_reach.srv3_reach = the ProxyJump-through-srv2 interim), grounded live: a Permission-denied handshake from srv2 proves the network reach is realizable while the shell/auth transport stays fail-closed — the operator's reach-independent-of-shell split, proven by execution.

— sent from vivid-wolf-453

Brian Searls and others added 5 commits July 25, 2026 03:07
The floor's batch-3 discovery corpus went over its 28-min wall budget (twice,
by 21s then 59s) because this PR added 6 new witness files and the floor pays a
full whole-tree closure resolve (~80s) per entry. Three of the six pull the
large gunbc closure. Per §6 (bare-minimum cost; a proven cost-shape defect is
always fixed) and the batch-wall-budget rule (a refusal, never a widen — do NOT
raise the budget), consolidate into 2 entries by shared closure:
- test.claim.srv3_subsumption = fleet_reach + host_authorized_keys_reconcile
  + host_toolchain_reach_pairing (gunbc closure) — 17 witnesses.
- test.claim.network_grounding = ipv4_address + network_address_host
  + network_reach (extdeps.network closure) — 19 witnesses.
All 36 witnesses preserved and green by execution; removes 4 whole-tree closure
resolves from the batch. No coverage lost — the merges are by shared closure and
lane, not unrelated concerns; original witness notes preserved verbatim.

Also folds in two live-run grounding corrections to srv3_reach_note:
- realization is nested exec (ssh srv2 'ssh srv3'), not a -J tunnel: srv2 sets
  AllowTcpForwarding no, so -J returns 'administratively prohibited'; the reach
  realizes via the ProxyCommand-family handler (reach abstraction is agnostic).
- fleet-automation was ADDED to ubuntu@srv3 live 2026-07-25 (the reconcile srv3
  upsert executed over the hop, R5-safe, backup taken) — srv3 now trusts the
  fleet identity; the "not yet on srv3" claim is corrected.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Copy link
Copy Markdown
Contributor Author

Management review at 5d910837e — verified by reading the head, not the body. Approve-shaped, two mechanical items before merge, one operator decision surfaced.

All eight body claims verify at head: sccache_installed_binary_path is written by the cited install script and read by both the P1b unit ExecStart and the PATH-shadow check (one answer to "which sccache is the modeled one"); sccache_release_arch_token/digest are genuinely partial (none for every unpublished arch — no default arm anywhere); the classifier is a fold over the cited fragment roster plus a shell-quoting totality check (build_cache_fragment_words_are_shell_safe) — a §5 catch beyond the claim; enable-linger present; the §4.I fallback now emits the counted provider=SKIPPED receipt, correctly loud-not-refusing pending the T4-gated STEP-2 flip; ci.yml/falsifier.yml +3/+3 from the model; the consolidated wet witness file is properly re-rostered (pattern + bin_wet rows both re-pointed — no orphans from the 6→2 consolidation).

The grown scope is strong work, not scope creep — but it must be described:

  • host_authorized_keys_reconcile is a faithful spine instantiation: material-keyed identity means a foreign key structurally cannot take the Modified arm (the hazard I flagged for name-keyed member types doesn't exist here); ownership is derived from fleet_authorized_keys, never hand-copied; the rotation extension is a declared trigger, not built silently; and the module consciously produces the plan grain only, reserving the apply policy.
  • The srv3 witnesses are exemplary: real observed fixtures (macbook reads, dated), srv3 yields exactly one named upsert + two named refusals, srv4 is the empty-plan negative control, and the R5 RED reconstructs the hinge — a lying ownership fn would emit teardowns, proving the refusal is caused by ownership_of, not incapacity. srv3_fabric_intended_refuses making the dissolution target a real value that honestly refuses today is the right way to keep a trigger from being prose.
  • extdeps.network.ipv4 is the model dissolution of an anemic brand done right: RFC-cited, octet as the bounded-Int idiom Port already uses, wire-parse refuses with a typed located error, round-trip witnessed.

Before merge: (1) the PR body is materially stale — it describes the sccache scope only; under the atomic bar it must describe the keys-reconcile, fleet-reach + ipv4 grounding, and srv3 witnesses too. Draft it and I'll apply it to the description, or say the word and I'll draft from the verified diff. (2) The three "WIP: srvN subsumption" commit subjects are fine only if this squash-merges; otherwise reword. CI green required (state currently blocked on checks).

Operator decision sitting inside this PR, surfaced: the apply-grain policy for everything-on-host observed scopes — wholesale-refuse vs siblings-continue (membership_effects_wholesale_refuse_policy_note). The module correctly refuses to decide it. It gates the live srv3 apply, alongside the already-adjudicated write go-ahead and the account-reconcile follow-on's Modified-arm ownership semantics.


Generated by Claude Code

@briansrls
briansrls merged commit 051d06a into main Jul 25, 2026
5 checks passed
@briansrls
briansrls deleted the session/vivid-wolf-453 branch July 25, 2026 06:15
gunbai-bot Bot pushed a commit that referenced this pull request Jul 25, 2026
…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>
briansrls added a commit that referenced this pull request Jul 25, 2026
…--start-server was a runtime no-op) (#7206)

* WIP: srvN subsumption

* sccache unit: foreground-supervise the daemon (Type=simple + --start-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>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jul 25, 2026
…x + DaemonUnsupervised refusal (follow-up to #7206) (#7213)

* WIP: srvN subsumption

* sccache unit: foreground-supervise the daemon (Type=simple + --start-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>

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* srvN build-cache: design-doc receipts for the idle-timeout finding

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jul 25, 2026
…-closed on absent producers (#7226)

* WIP: srvN subsumption

* sccache unit: foreground-supervise the daemon (Type=simple + --start-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>

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* srvN build-cache: design-doc receipts for the idle-timeout finding

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jul 25, 2026
…ependence criterion (#7235)

* WIP: srvN subsumption

* sccache unit: foreground-supervise the daemon (Type=simple + --start-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>

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* srvN build-cache: design-doc receipts for the idle-timeout finding

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* srvN quality sweep: enrollment wall, swap-backing axis, read-back independence 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>

* WIP: srvN subsumption

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jul 25, 2026
…s opening slice (#7248)

* WIP: srvN subsumption

* sccache unit: foreground-supervise the daemon (Type=simple + --start-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>

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* srvN build-cache: design-doc receipts for the idle-timeout finding

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* srvN quality sweep: enrollment wall, swap-backing axis, read-back independence 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>

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jul 25, 2026
…ll keyed on the RESOLVED toolchain (#7249)

* WIP: srvN subsumption

* sccache unit: foreground-supervise the daemon (Type=simple + --start-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>

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* srvN build-cache: design-doc receipts for the idle-timeout finding

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

* srvN quality sweep: enrollment wall, swap-backing axis, read-back independence 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>

* WIP: srvN subsumption

* WIP: srvN subsumption

* WIP: srvN subsumption

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (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.

1 participant