Skip to content

Replace the boot-start window with a relational origin, correct the wire it lied through, derive a fleet standing - #8852

Merged
briansrls merged 3 commits into
mainfrom
session/fierce-lynx-647-boot-standing
Aug 22, 2026
Merged

briansrls merged 3 commits into
mainfrom
session/fierce-lynx-647-boot-standing

Conversation

@gunbai-bot

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

Copy link
Copy Markdown
Contributor

Three changes, one subject: what boot-provenance means, how it reports, and what the fleet-level answer is. They ship together because splitting them puts a wire that explains a window in one PR and the window's deletion in the next — and under squash-merge no CI run ever compiles a PR against its unlanded siblings.

1. The window compared against the wrong origin

spark_serving_boot_start_window() is deleted, not widened. It asked whether the unit entered active within 10,000,000µs of kernel boot. Measured on both converged hosts:

host user manager (init.scope) gunbc-spark-serving.service delta
srv5 10,631,084 µs 10,670,729 µs 39.6 ms
srv6 10,571,698 µs 10,627,595 µs 55.9 ms

The user manager doesn't reach active until ~10.6s into kernel boot, because lingering brings the session up first. So a user unit that comes up perfectly with its manager is guaranteed to fall outside a kernel-boot window: the check had no true-positive path for the thing it existed to detect, and reported both durable hosts as not durable for two days.

This is a defect of reference, not of value — and that distinction is the finding. Widening to 11s would have greened both hosts by accident and left the defect intact until a host with a 12s session setup hit it. A constant wrong by reference cannot be repaired by adjusting it, and no amount of green would ever say so. The deleted carrier warned against "fitting a constant to a host until the check means nothing" — correct, and under-scoped: it didn't anticipate that the constant could be unsatisfiable.

The relation: the unit came up with the startup transaction exactly when it entered active no later than default.target did. The unit is WantedBy=default.target on both hosts, so one that came up with the transaction necessarily precedes the target, and one hand-started hours later doesn't. Both sides observed; nothing authored.

srv5  unit 10,670,729   default.target 10,675,297    inside by 4,568 µs
srv6  unit 10,627,595   default.target 10,632,705    inside by 5,110 µs

Not entered >= manager_start, which is trivially true of a unit hand-started 28 hours later — that would trade a false negative for silent false positives, strictly worse, since a wrong "durable" is harder to notice than a wrong "not durable".

2. The wire asserted a conclusion its instrument couldn't reach

UnitStartedAfterBoot printed "the unit is running but did NOT come up with this boot". That clause is an assertion of fact, it was false on the live fleet, and it propagated — "durability measured negative for the current boot" reached the operator on the strength of this string. A diagnostic stating a conclusion its own carrier says it cannot reach is fabricated plausible output at the wire layer (§5). Both arms now report the measured ordering.

3. Fleet standing, derived and rendered

Three states at fleet grain. Deliberately not the per-host four-state coproduct originally sketched: its states map 1:1 onto SparkServingBootProvenance, a second name for one concept (§3), and everything derived would fork too. The aggregate over N hosts is the part that didn't exist.

It also gives spark_serving_boot_provenance_establishes_durability its first production consumer — it had none, only its own witness. A predicate nothing asks can be correct forever and change nothing, and can't rot loudly because nothing depends on it.

The fork I didn't close the first time

An earlier change on this seam extracted spark_serving_host_observation_lines to kill a duplicated per-host render. That left the report-level assembly still forked in two — so the fleet standing, a report-level fact, was derived correctly, rendered by one assembler, and silently absent from the receipt the CI entry writes. Found by running it, exactly as the first instance was.

A fork is closed at the grain of the fact being added. Unifying the inner join does not unify the outer one.

Wet receipt (2026-08-22, both hosts, computed by the pipeline)

boot-provenance=started-by-manager-at-boot active_enter_us=10670729   (srv5)
boot-provenance=started-by-manager-at-boot active_enter_us=10627595   (srv6)
current-boot-durability=exhibited observed_hosts=2
account host=srv5/srv6 authorized_keys_mode=-rw------- owner=gunbc-automation

The default.target probe was verified through the modeled ssh path, not only by hand — deleting the window on the strength of a probe the pipeline couldn't perform would have left the module with no classifier at all.

The rung, and it moved by exactly one notch

Before this, auto-start was measured positive by a hand probe and not established by the instrument, because no .dag consumer asked the question. What this buys is that the instrument can answer. The answer above is a receipt from a run and stays one, rather than becoming a property of the fleet.

Still not reboot durability. Coming up with the manager on this boot is evidence for auto-start. Full durability needs a boot_id compared across an actual reboot, which nothing here does.

Tests

The window's boundary test is replaced by a relational one (equal-to-target inside, one microsecond past outside), plus a permanent regression control carrying the real srv5 numbers — if it reds, someone reintroduced an origin the user manager cannot satisfy — plus a hand-start false-positive guard, plus an unreached-target arm that refuses rather than deciding.

Not mine

Two pre-existing diagnostics in dag/gunbc/host_effect_realize.dag (no field 'Cli', method 'Run' unresolved) are whole-tree strict residue on main, untouched by this change.

🤖 Generated with Claude Code

gunbc-ci-auto-heal and others added 2 commits August 22, 2026 01:54
…ire it lied through, derive a fleet standing

Three changes, one subject: what boot-provenance MEANS, how it REPORTS, and what the
fleet-level answer is. They ship together because splitting them puts a wire that
explains a window in one PR and the window's deletion in the next -- and under
squash-merge no CI run ever compiles a PR against its unlanded siblings.

═══ 1. THE WINDOW COMPARED AGAINST THE WRONG ORIGIN ═══
spark_serving_boot_start_window() is DELETED, not widened. It asked whether the unit
entered active within 10,000,000us of KERNEL boot. Measured on both converged hosts:

  srv5  user manager (init.scope) active-enter  10,631,084us
        gunbc-spark-serving.service              10,670,729us   delta 39.6ms
  srv6  user manager                            10,571,698us
        gunbc-spark-serving.service              10,627,595us   delta 55.9ms

The user manager does not itself reach active until ~10.6s into kernel boot, because
lingering brings the user session up first. So a user unit that comes up PERFECTLY with
its manager is GUARANTEED to fall outside a kernel-boot window: the check had NO
TRUE-POSITIVE PATH for the thing it existed to detect, and duly reported both durable
hosts as not durable for two days.

This is a defect of REFERENCE, not of VALUE, and that distinction is the finding.
Widening to 11s would have greened both hosts by accident and left the defect intact
until a host with a 12s session setup hit it. A constant wrong by reference cannot be
repaired by adjusting it, and no amount of green would ever have said so. The deleted
carrier warned against "fitting a constant to a host until the check means nothing" --
correct, and under-scoped: it did not anticipate that the constant could be unsatisfiable.

THE RELATION: the unit came up with the startup transaction exactly when it entered
active NO LATER than default.target did. gunbc-spark-serving.service is
WantedBy=default.target (verified on both hosts), so a unit that came up with the
transaction necessarily precedes the target, and one started by hand hours later does
not. Both sides are observed on the host; nothing is authored.

  srv5  unit 10,670,729  default.target 10,675,297   inside by 4,568us
  srv6  unit 10,627,595  default.target 10,632,705   inside by 5,110us

NOT `entered >= manager_start`, which is trivially true of a unit hand-started 28 hours
later and would have traded a false negative for silent false positives -- strictly
worse, because a wrong "durable" is harder to notice than a wrong "not durable".

═══ 2. THE WIRE ASSERTED A CONCLUSION ITS INSTRUMENT COULD NOT REACH ═══
UnitStartedAfterBoot printed "the unit is running but did NOT come up with this boot".
That clause is an assertion of fact, it was FALSE on the live fleet, and it propagated:
the sparks lane reported "durability measured negative for the current boot" to the
operator on the strength of this string. A diagnostic stating a conclusion its own
carrier says it cannot reach is fabricated plausible output at the wire layer (DESIGN
section 5). Both arms now report the measured ordering against default.target.

═══ 3. FLEET STANDING, DERIVED AND RENDERED ═══
Three states at FLEET grain. Deliberately NOT the per-host four-state coproduct that was
sketched for this: its states map 1:1 onto SparkServingBootProvenance, which is a second
name for one concept (section 3), and everything derived from it would fork too. The
aggregate over N hosts is the part that did not exist.

It also gives spark_serving_boot_provenance_establishes_durability its FIRST production
consumer -- it had none, only its own witness. A predicate nothing asks can be correct
forever and change nothing, and cannot rot loudly because nothing depends on it.

═══ THE FORK I DID NOT CLOSE THE FIRST TIME ═══
An earlier change on this seam extracted spark_serving_host_observation_lines to kill a
duplicated PER-HOST render. That left the REPORT-LEVEL assembly still forked in two, so
the fleet standing -- a report-level fact -- was derived correctly, rendered by
spark_serving_observation_report_text, and SILENTLY ABSENT from the receipt the CI entry
writes. Found by running it, exactly as the first instance was.
A FORK IS CLOSED AT THE GRAIN OF THE FACT BEING ADDED: unifying the inner join does not
unify the outer one. spark_serving_report_body_lines now owns the body; both callers
prepend their own genuinely-different headers.

═══ WET RECEIPT (2026-08-22, both converged hosts, computed by the pipeline) ═══
  boot-provenance=started-by-manager-at-boot active_enter_us=10670729   (srv5)
  boot-provenance=started-by-manager-at-boot active_enter_us=10627595   (srv6)
  current-boot-durability=exhibited observed_hosts=2
  account host=srv5/srv6 authorized_keys_mode=-rw------- owner=gunbc-automation

THE RUNG, and it moved by exactly one notch. Before this, auto-start was measured
positive by a HAND probe and not established by the instrument, because no .dag consumer
asked the question. What this change buys is that the instrument CAN answer; the answer
above is a receipt from a run, and it stays a receipt from a run rather than becoming a
property of the fleet. AND IT IS STILL NOT REBOOT DURABILITY: coming up with the manager
on THIS boot is evidence for auto-start. Full durability needs a boot_id compared across
an actual reboot, which nothing here does.

TESTS: the window's boundary test is replaced by a relational one (equal-to-target is
inside, one microsecond past is outside), plus a permanent regression control carrying
the real srv5 numbers -- if it reds, someone reintroduced an origin the user manager
cannot satisfy -- plus a hand-start false-positive guard, plus an unreached-target arm
that refuses rather than deciding.

NOT MINE: two pre-existing diagnostics in dag/gunbc/host_effect_realize.dag ('no field
Cli', method 'Run' unresolved) are whole-tree strict residue on main and are untouched
by this change.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ix had to change

CI red on this PR: the_wire_separates_came_up_with_this_boot_from_started_later
returned false. The witness is mine and the red is genuine, but the defect is
in the witness rather than in the wire.

It pinned two literal phrases: "came up WITH this boot" and "did NOT come up
with this boot". The second was REMOVED DELIBERATELY in this same PR, because
UnitStartedAfterBoot does not mean durability failed -- only that the unit was
not part of the manager startup transaction. The first went stale too: that arm
now says "came up WITH the manager startup transaction".

So a witness was holding the explanatory half of a wire line hostage, which
makes correcting a wrong sentence indistinguishable from breaking a contract.

It now joins on the WIRE TAG -- boot-provenance=started-by-manager-at-boot vs
boot-provenance=started-after-boot -- which is what a consumer actually parses;
the prose after the dashes is explanation and must stay free to be corrected.

The final clause is what keeps it discriminating rather than two independent
containments: the after-boot wire must NOT also carry the at-boot tag, so
collapsing both arms onto one tag reds this test.

Verified by execution: returns true on this tree.

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 witness fix is confirmed in CI; the remaining red is main's

Run 32547228709 @ bc74efe16ab:

required-regen: first_generation_equal=true planned=132 executed=132 declared_divergent=1 [main.rs]
required-floor: planned=10433 executed=10433 terminal=10433 passed=10110
                known_red_held=206 failed=16 interrupted_before_verdict=0 stale_quarantine=0

Against the pre-fix run 32544808292 @ 97799b86f4f (failed=17 passed=10109), diffed by identity rather than by count:

disappeared:  test.claim.spark_serving_boot_provenance_witness.
              the_wire_separates_came_up_with_this_boot_from_started_later
appeared:     (none)
unique to this PR vs main:  (none)

So the count going 17 → 16 is not the evidence — the evidence is that the identity which left is exactly the witness this commit rewrote, and nothing else moved. passed rising 10109 → 10110 on an unchanged planned=10433 says the same thing from the other side: one witness changed verdict, no roster churn.

The remaining 16 are v2.test.claim.fold_lowering.* (12) and body_lowering.statement_let_bind.* (4), red on main since 67437fcbe90 (#8833) — not touched by this PR.

On the fix itself

The witness pinned two literal sentences from the wire, one of which — "did NOT come up with this boot" — this PR deliberately removed, because UnitStartedAfterBoot does not mean durability FAILED, only that the unit was not part of the manager startup transaction. The other had gone stale too.

A witness holding the explanatory half of a wire line hostage makes correcting a false sentence indistinguishable from breaking an interface. It now joins on the wire tag — boot-provenance=started-by-manager-at-boot vs =started-after-boot — which is what a consumer parses; the prose after the dashes must stay free to be corrected.

The last clause is what keeps it from being vacuous: the after-boot wire must not also carry the at-boot tag, so collapsing both arms onto one tag reds it. Two independent string_contains checks would pass a wire emitting both tags at once.

— sent from fierce-lynx-647

@gunbai-bot

gunbai-bot Bot commented Aug 22, 2026

Copy link
Copy Markdown
Contributor Author

Narrowing one line of evidence in my earlier comment

I wrote that passed rising 10109 → 10110 "on an unchanged planned=10433" says the same thing from the other side — "one witness changed verdict, no roster churn."

Drop the second half. planned= has since been shown to be a confounded measure: discovery is deterministic per commit (verified on this repo's own attempt pair — same sha on srv2-03 and srv4-01 gives byte-identical figures), but a single unrelated line has been measured moving offered by fourteen. Those two runs are different commits, so an unchanged planned does not establish an unchanged roster; it is consistent with no churn and with compensating changes I did not cause.

The primary evidence is unaffected and is what this rests on: diffed by identity, the set that disappeared between the two runs is exactly

test.claim.spark_serving_boot_provenance_witness.the_wire_separates_came_up_with_this_boot_from_started_later

with nothing appearing, and nothing unique to this PR versus main. That is a set comparison, not a count, and it holds regardless of what planned does.

The count was corroboration that reached further than it could support. The identity diff was always the check.

— sent from fierce-lynx-647

gunbai-bot Bot pushed a commit that referenced this pull request Aug 22, 2026
MEASURED, read-only `sudo -n -l` on both units 2026-08-22:

  192.168.1.222  spark-a3ee   (root) NOPASSWD: /usr/bin/loginctl enable-linger gunbc-automation
                              (root) NOPASSWD: /usr/bin/systemctl reboot
  192.168.1.223  spark-3bd5   (same two)

ONE COMMAND PER LINE, no comma list -- each grant is its own drop-in and so its
own Cmnd_Spec. The comma shape does not occur on srv5 or srv6 today.

THE JOIN SPLITS ON COMMAS ANYWAY, because sudo renders a multi-command Cmnd_Spec
comma-separated on one line, and reading that line as ONE command would match
neither grant it names. That is a LIVENESS hole rather than a safety one --
convergence would never complete on a host that plainly holds both, and the
diagnostic would report grants missing that are visibly present. One line of
parsing, so it is taken rather than declared as a limit. And the split cannot
make a wrong answer right-looking: a comma inside a command's own ARGUMENT makes
fragments that match nothing, the grant reads not-held, the installer reinstalls
-- the same safe direction as not splitting, over a strictly larger set of
listings read correctly.

`NOPASSWD: ALL` READS NOT HELD, now named in the carrier before someone files it.
That is correct and fail-closed: teaching the join that ALL subsumes everything
would let a blanket grant answer for every specific one, which is the
host-grained "is provisioned" Bool this module exists to avoid.

THE COMMA TEST'S FIRST DRAFT WAS WRONG AND THE RUN CAUGHT IT. I hand-spelled the
fixture with the post-#8860 linger command, and it returned FALSE -- reporting a
comma-splitting defect when what it had measured was the subject's absence from
today's modeled command. Two ordering-dependent tests where one was intended, and
the second one lying about which axis it failed on. The fixture is now RENDERED
from spark_managed_grant_sudoers_command over the population, so it agrees with
the model on spelling by construction -- right here precisely because spelling is
the ordering witness's subject, not this test's.

BOTH NEW TESTS RE-VERIFIED AGAINST THEIR CONTROLS after this change, since a fix
can quietly turn a discriminator vacuous:

  two_commands_on_one_entry_line_are_two_grants
    comma split present            returned `true`
    comma split removed (control)  returned `false`
  an_entry_that_merely_starts_with_the_desired_command_is_not_that_grant
    still returned `true` after the comma change -- the split did not erode it

THE LIVE READ ALSO CONFIRMS #8860 FROM THE HOST SIDE: the installed linger
command carries the subject, byte-identical to the constant the ordering witness
pins. The witness therefore measures against a line read off a host, not against
a fixture that agrees with the model by construction.

srv5/srv6 stand 2/2 by live host reading. The INSTRUMENT does not compute that
verdict until #8860 and #8852 land.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@briansrls
briansrls merged commit 9b58df0 into main Aug 22, 2026
1 check passed
@briansrls
briansrls deleted the session/fierce-lynx-647-boot-standing branch August 22, 2026 17:32
briansrls pushed a commit that referenced this pull request Aug 23, 2026
…raint instead of noting it (#8882)

* Join the grant listing entry-by-entry, and execute the ordering constraint instead of noting it

THE SUBSTRING JOIN WAS PREFIX-BLIND. `spark_managed_grant_standing_from_outcome`
asked `string_contains(listing, command)` over the whole `sudo -n -l` blob, which
answers HELD for any installed command the desired one is a prefix of. So a host
authorizing MORE than the population desires read as converged, with nothing
naming the excess -- and the grain at which sudo's answer is meaningful is one
ENTRY, so a substring test over the concatenation is a test at no grain at all.

The join is now entry-grained, parsed at sudo's own seam: each authorization
renders as `    (root) NOPASSWD: <command>`, so the command is what follows the
last `NOPASSWD: ` on its line, trimmed. Splitting on the marker rather than on
whitespace keeps a command containing spaces one command. A line with no marker
yields NO command rather than a false one, so banners and blank separators
contribute nothing to the join instead of contributing a negative vote.

THE DISCRIMINATING RED, AND THE FACT THAT MY FIRST ONE WAS VACUOUS. The new test
feeds a listing whose entry ends in a subject the desired command does not name
-- a wider grant, of which the desired command is a proper prefix. Measured, same
test, two trees:

  entry-grained join (this branch)   returned `true`
  substring join restored (control)  returned `false`

The first draft of that test asserted `!converged` and stayed GREEN under the
mutation. It was measuring the reboot grant's absence from the fixture -- unheld
under either join -- and nothing about the change it was written for. Counting
the install set isolates the one grant the two joins disagree about: 2 under the
entry-grained join, 1 under the substring join. The control is what caught it,
which is the only reason the surviving test can be trusted.

THE ORDERING WITNESS IS RED ON THIS BRANCH BY CONSTRUCTION. This fix and the
grant-spelling correction in gunbc#8860 are two defects that CANCEL: the modeled
linger command currently omits the subject the hosts hold, and the substring join
is the only reason that mismatch does not surface. Tighten the join first and the
linger grant reads NOT-HELD on two converged live hosts, and the reconcile
reports a remedy to install a grant that is already there.

A note in a PR body cannot enforce a merge order -- it depends on a human merging
two PRs in one direction. So the constraint executes instead:
`the_modeled_linger_command_is_byte_equal_to_the_line_the_hosts_hold` asserts the
modeled command equals the line measured on srv5 and srv6. It returns `false`
today and `true` once #8860 lands, so merging this branch first cannot go green.
It reads only rendered command strings, never #8860's variant shape, so it
compiles identically before and after that PR.

DO NOT MERGE THIS BEFORE gunbc#8860. The witness says so by failing, not by
asking.

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

* Split multi-command entry lines, measured against both live hosts

MEASURED, read-only `sudo -n -l` on both units 2026-08-22:

  192.168.1.222  spark-a3ee   (root) NOPASSWD: /usr/bin/loginctl enable-linger gunbc-automation
                              (root) NOPASSWD: /usr/bin/systemctl reboot
  192.168.1.223  spark-3bd5   (same two)

ONE COMMAND PER LINE, no comma list -- each grant is its own drop-in and so its
own Cmnd_Spec. The comma shape does not occur on srv5 or srv6 today.

THE JOIN SPLITS ON COMMAS ANYWAY, because sudo renders a multi-command Cmnd_Spec
comma-separated on one line, and reading that line as ONE command would match
neither grant it names. That is a LIVENESS hole rather than a safety one --
convergence would never complete on a host that plainly holds both, and the
diagnostic would report grants missing that are visibly present. One line of
parsing, so it is taken rather than declared as a limit. And the split cannot
make a wrong answer right-looking: a comma inside a command's own ARGUMENT makes
fragments that match nothing, the grant reads not-held, the installer reinstalls
-- the same safe direction as not splitting, over a strictly larger set of
listings read correctly.

`NOPASSWD: ALL` READS NOT HELD, now named in the carrier before someone files it.
That is correct and fail-closed: teaching the join that ALL subsumes everything
would let a blanket grant answer for every specific one, which is the
host-grained "is provisioned" Bool this module exists to avoid.

THE COMMA TEST'S FIRST DRAFT WAS WRONG AND THE RUN CAUGHT IT. I hand-spelled the
fixture with the post-#8860 linger command, and it returned FALSE -- reporting a
comma-splitting defect when what it had measured was the subject's absence from
today's modeled command. Two ordering-dependent tests where one was intended, and
the second one lying about which axis it failed on. The fixture is now RENDERED
from spark_managed_grant_sudoers_command over the population, so it agrees with
the model on spelling by construction -- right here precisely because spelling is
the ordering witness's subject, not this test's.

BOTH NEW TESTS RE-VERIFIED AGAINST THEIR CONTROLS after this change, since a fix
can quietly turn a discriminator vacuous:

  two_commands_on_one_entry_line_are_two_grants
    comma split present            returned `true`
    comma split removed (control)  returned `false`
  an_entry_that_merely_starts_with_the_desired_command_is_not_that_grant
    still returned `true` after the comma change -- the split did not erode it

THE LIVE READ ALSO CONFIRMS #8860 FROM THE HOST SIDE: the installed linger
command carries the subject, byte-identical to the constant the ordering witness
pins. The witness therefore measures against a line read off a host, not against
a fixture that agrees with the model by construction.

srv5/srv6 stand 2/2 by live host reading. The INSTRUMENT does not compute that
verdict until #8860 and #8852 land.

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

* Name the test that owns the spelling axis, so the rendered fixture is not "fixed" back

The carrier already said the fixture renders from the model deliberately. It did
not NAME the test that owns the axis it is deferring to, so a reader had the
justification without the referent -- and the §3 rule is to cite the symbol.

It now names `the_modeled_linger_command_is_byte_equal_to_the_line_the_hosts_hold`
as the owner of the spelling axis, says why agreeing-by-construction is normally
disqualifying, and says plainly not to convert this back to a hand-spelled
literal -- which would silently restore the two-axis failure and make a parse
test fail for a spelling reason.

Re-verified after the edit: two_commands_on_one_entry_line_are_two_grants still
returns `true`.

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>
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