Runtime shell programs in live-deploy and converge: executable behavior still carried as String

[briansrls]

What this changes

gunbc.fleet_converge_plan carried the fleet-lease generation guard two ways, and they disagreed.

The modeled reader (fleet_converge_generation_from_store_content) mapped store absent to generation 0 — the deliberate first-run rule — and refused a present-but-unparseable store, naming zero as the exact wrong answer for it. The emitted guard it feeds then produced that wrong answer: the lease-wrapped body read the store as CURRENT=$(cat "PATH" 2>/dev/null || echo 0), so a present store that could not be read (permissions, truncated write, I/O error) became 0 — indistinguishable from a first run, and the staleness comparison then passed against a number nobody observed. The model stated the rule and the realization contradicted it.

The same body was assembled as text: an inner program joined from strings and spliced into sudo -n flock -x "PATH" bash -c ' … ', with the quoting hand-spelled around a value the model does not constrain.

What lands

• The observation splits. GenerationStoreObservation = GenerationObserved { generation } | GenerationStoreAbsent | GenerationUnobserved { reason }. GenerationUnobserved carries no numeric payload of any kind — that was the entire defect, a state with no number being given one. Admission is a separate, typed decision: fleet_converge_generation_admission maps GenerationStoreAbsent to fleet_converge_first_generation (the first-run rule, now stated once and in the open) and GenerationUnobserved to GenerationAdmissionRefused. The CLI (fleet_converge_plan_cli fleet_converge_plan_wet) refuses on that arm rather than planning against a fabricated prior.
• The emitted guard derives from that reader instead of restating it. The lease body is now a modeled bash program — bash_build_* nodes serialized through v2.workflow.bash_command_fold_serialize — and the inner program enters the outer flock … bash -c command as one word node, so its quoting is structural rather than hand-spelled. The store read is if [ -e PATH ]; then _gunbc_current=$(cat PATH); fi: absent leaves the modeled default in place, and there is no 2>/dev/null || echo 0 arm to coerce an unreadable store into a number.
• A shape the grammar cannot express refuses with a poison marker rather than a hand-spelled fallback — not valid shell, so the consuming step fails loudly (§5: refuse, never widen).

Exposure, stated honestly

This is not a live incident. The plan path reads the store itself before emitting, so the reachable window is the store becoming unreadable between plan and apply, or apply invoked without its plan. No occurrence is claimed or known. What is fixed is that the emitted realization no longer contradicts the reader that governs it.

Deviation from the two-variant spec, declared

The direction I was given named two observation states (observed / unobserved). I shipped three. A strict two-way split has no home for store legitimately absent, which is every host's first apply — the store is only written after the guard passes — so a two-variant reader would have to answer GenerationUnobserved there and refuse forever. The absent case is a real third state of the world, and the requirement it was protecting is honored exactly: the absent→first-generation mapping lives in fleet_converge_generation_admission, not in the read, and no not-observed state carries a number.

Residue

The staleness comparison is still spelled twice — once in .dag and once in the emitted guard the .dag builds. The emitted side is now derived from the same modeled prior generation rather than re-reading independently, which is what closes the divergence; collapsing the two spellings entirely needs the apply body to become a program the host runs from the model, which is a larger cut than this PR.

Verification (executed, remote runner, HEAD of this branch)

Eight witnesses in dag/test/claim/fleet_converge_plan_witness_test.dag, each returning true:

• generation_observation_separates_absent_from_unreadable
• generation_admission_admits_absent_as_first_and_refuses_unreadable
• locked_apply_script_serializes_generation_under_flock
• locked_apply_inner_program_is_quoted_not_spliced — RED control: fails if the inner program is spliced between literal '
• locked_apply_guard_does_not_coerce_an_unreadable_store_to_zero — RED control: fails on || echo 0 or 2>/dev/null
• locked_apply_guard_compares_the_modelled_prior_generation
• apply_shell_carries_dissolve_on_marker_not_host_gate
• parse_nonneg_generation_refuses_corrupt_and_negative

[gunbai-bot]

Fixed the diagnostic nit from review 54519: observed= and the shell variable are now one word (bash_build_word_concat_from_nodes), so the stale line reads observed=4 rather than observed= 4 — a rendering that would have read as an empty observation followed by a number, which is the exact confusion this PR removes from the guard itself. Pinned by a new witness, locked_apply_stale_diagnostic_keeps_observed_value_in_one_word, which refuses observed= and requires observed=; verified green by execution alongside the other four lease-guard witnesses on this head.

— sent from silent-otter-405

[gunbai-bot]

review 54526 is right and it is already fixed on this head: verify_lease2.sh was an ad-hoc probe I committed by accident and it was deleted in 1d89ad677d. No hand-authored script from this work remains in the tree — git ls-files matches nothing at the repo root for it. No obligation row was authored, because the file has no admitted role: the modeled route already answers the question it was asking.

— sent from silent-otter-405

[gunbai-bot]

Pushed one addition since the approval, in response to a question from the lane: what does the GenerationStoreAbsent arm actually do?

It proceeds, at the first generation — so removing the store on a host passes the staleness compare, and a deleted store is the same observation as a host that has never applied. That is a real bypass, and nothing modelled separates the two histories: Filesystem.Read yields success and content, so absence carries no history; the store's directory is created out of band and must already exist for any commit to have succeeded (the commit is a plain printf redirect, no mkdir), so its presence is evidence about provisioning rather than about a prior apply; and the lock file is created by the guard itself, so it exists on a first run too.

The commit names that plainly in the module rather than leaving a reader to assume the absent arm is as safe as the other two, and states the close as a construction: provision the store with the first generation, at which point absence stops being a legitimate state and GenerationStoreAbsent becomes a third refusal beside GenerationUnobserved. That is a provisioning change rather than a guard change, so it is not in this PR.

— sent from silent-otter-405

[gunbai-bot]

CI red here is not from this PR. The floor reports failed=16, and all sixteen are v2.test.claim.body_lowering.statement_let_bind.* and v2.test.claim.fold_lowering.* erroring with non-exhaustive pattern match on: OccurrenceId { value: N } — nothing in this diff is reachable from either module (this PR touches gunbc.fleet_converge_plan, its CLI, and its witness file).

The same sixteen identities fail on main at the same time: run for 90986d194 on main carries a byte-identical failure list. main was green through 77ced016e and red from 67437fcbe, the only commit in that range being #8833. So this is inherited, and it will clear here when main clears; I am not going to paper over it on a branch that did not cause it.

parse and regen phases both passed on this head (parse OK 50 file(s), regen first_generation_equal=true).

— sent from silent-otter-405