Skip to content

fleet_posix_accounts: drop the host-discarding automation-user function; scope the fleet-wide claims to the hosts that hold them - #8857

Merged
briansrls merged 2 commits into
mainfrom
session/fierce-lynx-647-fleet-account
Aug 22, 2026
Merged

briansrls merged 2 commits into
mainfrom
session/fierce-lynx-647-fleet-account

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 22, 2026

Copy link
Copy Markdown
Contributor

What

fleet_automation_user_on(host: HostIdentity) took a host and discarded it, returning one constant. Replaced with data fleet_automation_user: PosixUser; both call sites updated. Two fleet-wide prose claims scoped to the hosts that actually hold them, and one dissolve-on row gains evidence.

Why the signature was the defect

A signature promising a host-varying answer over a body that cannot give one is a false promise in the type. Every call site reads on(host:) and believes the answer was computed for that host. Both call sites passed srv1 and srv2 — which agree — so no test over the covered hosts could ever have exposed it.

Removed rather than made to branch: the fact is uniform across the hosts this principal covers, and a constant that says so is honest where a function pretending to a variation it does not have is not. If a covered host ever differs, this becomes a real per-host lookup and every call site is forced to be re-read — exactly what the old signature quietly prevented.

The scoping fixes

Measured against the live fleet on 2026-08-22:

claim as written measured
"Label gunbc-fleet, the same on every host" srv5/srv6 carry no gunbc-fleet account; they run gunbc-automation, a separately declared principal with disjoint permitted operations
automation_uid_coincidence_note: two accounts read uid 1001 three do — gunbc-automation is 1001:1001 on srv5 and srv6
fleet_posix_ci_runner_user carries contradicted uid/gid getent passwd ghrunner returns nothing on srv5 or srv6 — absent, not merely different

The unscoped sentence is the stale-citation mechanism from DESIGN.md §3: a reader looking for the automation account on srv5 finds nothing and concludes the host is unprovisioned, rather than that they read a claim whose scope narrowed underneath it.

What this deliberately does NOT do

fleet_account_contradiction_dissolve_on gains evidence only. The authored ghrunner values are left wrong. Hand-editing the observed numbers in would satisfy the letter of the dissolution condition while bypassing the ProcessReceipt grounding the condition exists to require — the precise failure mode it was written against. The new evidence also narrows what a corrected row must say: uid/gid alone cannot express an account that does not exist on a host, so grounding has to carry per-host presence rather than one fleet-wide pair.

Verification

  • 0 blocking error(s) on the module.
  • The removed symbol had zero references outside its own module (grepped .dag and .rs corpus-wide), so this is not a behavior change.
  • No host was touched: every measurement above is a read (getent, sudo -l).

…on; scope the fleet-wide claims to the hosts that hold them

fleet_automation_user_on(host) took a HostIdentity and discarded it, returning
one constant. A signature promising a host-varying answer over a body that
cannot give one is a false promise in the type: every call site reads
`on(host:)` and believes the answer was computed for that host. Both call
sites passed srv1 and srv2, which agree, so no test on the covered hosts
could have exposed it.

Removed rather than made to branch. The fact is genuinely uniform across the
hosts this principal covers, and a constant that says so is honest where a
function pretending to a variation it does not have is not. If a covered host
ever differs this becomes a real per-host lookup and every call site is forced
to be re-read -- which the old signature quietly prevented.

Two prose claims are scoped to what was actually measured rather than left
standing over a fleet that now contains counterexamples:

- "Label gunbc-fleet, the same on every host" is now scoped to srv1..srv4.
  Measured 2026-08-22, srv5 and srv6 carry NO gunbc-fleet account; they run
  gunbc-automation, a separately declared principal (operator declaration
  2026-08-12 in gunbc.spark.serving_desired) with disjoint permitted
  operations. The unscoped sentence is the stale-citation mechanism: a reader
  looking for the automation account on srv5 finds nothing and concludes the
  host is unprovisioned.

- automation_uid_coincidence_note recorded two accounts reading uid 1001.
  A third does: gunbc-automation on srv5 and srv6. The hazard it named got
  worse rather than different -- a reader treating uid as identity now fuses
  three principals, one with disjoint sudo grants from the other two.

fleet_account_contradiction_dissolve_on gains evidence only, and deliberately
does not correct the authored ghrunner values: `getent passwd ghrunner`
returns nothing on srv5 or srv6, so the row is wrong there in a second way.
Hand-editing observed numbers in would satisfy the letter of the condition
while bypassing the ProcessReceipt grounding the condition exists to require.
It also narrows what a corrected row must say: uid/gid alone cannot express an
account that does not exist on a host.

No behavior change. The symbol had zero references outside its own module.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 22, 2026

Copy link
Copy Markdown
Contributor Author

The failing check on this PR is inherited from main, not caused here

Run 32545830237 @ 5a65356:

required-floor: planned=10425 executed=10425 terminal=10425 passed=10102
                known_red_held=206 failed=16 stale_quarantine=0
                interrupted_before_verdict=0 budget_refused=0

I diffed the failure identities against main's own witnesses run at 90986d194 — not the counts, since two different failure sets can share a count and a count comparison would prove nothing:

comm -23 <(fails on this PR) <(fails on main)   ->  empty
comm -13 <(fails on this PR) <(fails on main)   ->  empty

The two sets are identical. All 16 are v2.test.claim.fold_lowering.* (12) and v2.test.claim.body_lowering.statement_let_bind.* (4) — modules this diff does not touch. This PR changes one file, dag/gunbc/fleet_posix_accounts.dag, and the symbol it removes had zero references outside its own module.

Main's history: last green 77ced016ef0 (00:49), red from 67437fcbe90 (00:51, #8833). That lane owns them; #8853, #8854 and #8856 are open against it.

interrupted_before_verdict=0 and stale_quarantine=0 rule out the instrument-artifact explanations, and only the floor step failed — parse and regen did not.

So there is nothing to fix here, and I am not pushing a commit. A change made to turn this check green would be a change with no defect behind it. This PR is unblocked the moment main is.

— sent from fierce-lynx-647

@briansrls
briansrls merged commit d0446e7 into main Aug 22, 2026
1 check passed
@briansrls
briansrls deleted the session/fierce-lynx-647-fleet-account branch August 22, 2026 17:32
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