Repository navigation
srv1 daily workspace still doesn't work at all - #8729
Closed
gunbai-bot[bot] wants to merge 13 commits into
Closed
gunbai-bot[bot] wants to merge 13 commits into
gunbai-bot[bot] wants to merge 13 commits into
Conversation
…hecking
gunbc.fleet_main_revision requires the fleet's desired revision to derive from
merged, FLOOR-GREEN main -- "never from a CLI argument, a session's checkout, or
raw HEAD" -- and models the gate as admit_fleet_desired_advance, whose refusal
names the prevented class: raw-HEAD simultaneous fleet-bricking.
That gate's only caller was its own witness test. The emitted deploy.yml stamped
$GITHUB_SHA onto refs/fleet/desired on every push to main, consulting nothing.
Specification-without-execution (DESIGN section 5) with the unproven path live.
The blast radius is not the ref's name. gunbc.roadmap_belt_actuate gates worker
DISPATCH on revision standing, and its own note calls a dispatch from an
unadmitted tree "a worker spawned from code the fleet never admitted, reported as
an ordinary spawn". A desired ref equal to whatever last landed makes that
comparison agree unconditionally, so an existing safety gate passed in silence.
WHY THE ADMISSION MOVED OUT OF THE DEPLOY JOB. The required floor takes ~30
minutes, so at push time no conclusion exists for the candidate. A push-triggered
advance can only fabricate floor-green or refuse forever. The conclusion becomes
observable exactly once -- when the floor run completes -- so the admission is a
workflow_run-keyed workflow reading the conclusion GitHub delivers.
gunbc.fleet_desired_admission trust-walls the payload on identity the trigger
filter also claims (activity, workflow, branch, fork), derives floor_green from
the delivered conclusion (only Success), and calls the modeled gate. It renders
the authorized push ITSELF, so the surrounding shell carries no ref name, no
candidate and no expected prior: a shell that cannot name a revision cannot push
an unadmitted one.
An unobservable prior REFUSES rather than being read as an absent one.
fleet_desired_observe collapses "ls-remote refused" and "ref not advertised" into
one state with different causes, and those demand opposite actuations -- treating
the first as the second would create the ref from scratch and overwrite an
admitted revision nobody could read (the empty-observation narrow).
The ungated script is deleted at the root rather than kept beside the
replacement, and the two deploy claims that asserted the old behaviour are
rewritten -- one was NAMED for a ref this job no longer advances.
This is a scope narrowing, not a full climb: the actuation is still shell.
git.PublicationTransport PushRefUpdate is shadow-only and models no
--force-with-lease, so full construction is not reachable. The DECISION is
modeled; the residual debt is declared where the remaining shell lives.
EVIDENCE BY EXECUTION, not by green claims alone.
Wet, against the real remote, reading the actual admitted prior via ls-remote:
git push --force-with-lease=refs/fleet/desired:517fdac4dd... \
origin 5a10ca7e018f...:refs/fleet/desired
Six discriminating wet probes, each a distinct located cause, none writing an
authorization file:
floor conclusion failure -> rc=1, "raw-HEAD simultaneous fleet-bricking"
conclusion from "deploy" -> rc=1, wrong workflow
branch session/x -> rc=1, not the default branch
fork head repository -> rc=1, a fork's run never admits
activity "requested" -> rc=1, not completed
floor success on main -> rc=0, authorization written
Witnesses: 12/12 new, 5/5 rewritten deploy claims, both with the
[resolve-summary] footer (complete runs, not partial kills).
A DEFECT THE WET PATH CAUGHT AND THE MODEL DID NOT. GitObjectId as String
renders the debug form, so the first authorized push read
--force-with-lease=refs/fleet/desired:GitSha1ObjectId { digest: ... }. It
compiled, typechecked, and would have failed at the remote. Routed through
git_object_id_wire_hex.
STILL OPEN, and deliberately not decided here: whether DEPLOYMENT should also
block on floor-green, or only admission. This gates admission only, so a red
floor leaves srv1 deployed while the fleet holds last-known-good and the belt
refuses to dispatch -- loud, and the declared anti-entropy behaviour.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…53998) The admission workflow's annotation claimed "queued, never cancelled ... two floor runs completing close together must admit in order". The chosen variant does not provide that. Per extdeps.languages.yaml.gha_workflow concurrency_queue_max_emission_note, ConcurrencyMappingQueueNotMax is the default group -- at most one running and one PENDING entry, with a newly-arriving entry CANCELLING the pending one. Multi-entry in-order queueing is what ConcurrencyMappingQueueMax was minted for. The claim was a state-space conflation of "in-order queue" with the platform's pending-replacement default. The variant STAYS, with a narrower and true reason. What this workflow needs is that a RUNNING admission is never interrupted -- a cancellation between the compare-and-swap decision and the push would leave the advance half-observed -- and the default group gives exactly that, since cancel-in-progress defaults false and only the pending entry is replaceable. Losing a superseded pending admission is preferable, not a defect: the desired ref should track the newest floor-green revision. QueueMax would buy the in-order queue and then owe an explanation of why the fleet wants to walk through revisions it has already passed. ALSO DECLARED, found while checking the above rather than reported by it: neither variant prevents an OLDER floor run from admitting after a newer one. A manually re-run floor for an earlier commit completes later, observes the current prior, and its CAS succeeds -- moving the desired ref BACKWARD. The gate models floor-greenness, not ancestry. Class sits at mitigatable: it needs a deliberate re-run of an old floor run, and the result is a valid earlier revision rather than an unproven one. NEXT-RUNG TRIGGER: an ancestry operand on the admission, which needs a git ancestry read git.Core does not yet model. Annotation-only: the emitted .github/workflows/fleet-desired.yml is byte-identical. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The annotation claimed the fleet-desired admission "cannot run until the required floor has completed, which is strictly after this workflow has finished or failed". There is no such dependency. deploy.yml and witnesses.yml BOTH trigger on push to the default branch and run in parallel; nothing sequences them. The floor takes ~30 minutes against ~10 here, so the admission does land later in practice -- but deploy's concurrency group is a queue, so a deploy waiting behind another deploy can still be running when the floor completes. Typical is not guaranteed. An annotation saying "strictly" about a race is the prose half of the fail-open class this module's own history is made of, and it was load-bearing: it was the justification offered for moving the advance out. WHAT THE ANNOTATION NOW CLAIMS INSTEAD, which is the argument that actually needed making: the lost ordering is acceptable because refs/fleet/desired is a TARGET, not an observation of what is deployed. gunbc.fleet_main_revision defines it as the revision hosts converge TOWARD, and the anti-entropy property is precisely that a host which has not applied it yet keeps serving last-known-good while saying so. A host behind an advanced ref reads RevisionDrifted and refuses dispatch loudly, carrying both revisions. The original ordering argument was defending against a SILENT window; there is none, because the failure it feared is a typed refusal either way. Annotation-only: the emitted .github/workflows/deploy.yml is byte-identical. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…admission judge
Two findings from independent review, both verified against the emitted workflows
rather than accepted, and both correcting claims this PR itself made.
1. THE BACKWARD ADVANCE IS ORDINARY, NOT AN OPERATOR EDGE CASE. The annotation said
reaching it "requires deliberately re-running an old floor run". That was wrong
and it made a live race read as a curiosity. The floor's concurrency group is
witness-floor-${{ github.event.pull_request.number || github.run_id }}; on a
default-branch push there is no PR number, so the group is unique per run and the
floor imposes NO ordering between main pushes:
floor(C1) starts; floor(C2) starts
floor(C2) finishes first -> desired advances D -> C2
floor(C1) finishes later -> observes C2 -> CAS SUCCEEDS -> C2 -> C1, backward
--force-with-lease does not prevent this. The lease refuses an UNOBSERVED
concurrent write; the older admission observes the newer prior correctly and
overwrites it on purpose.
Rung is unchanged at mitigatable -- the ref lands on a revision that IS
floor-green, and a host behind it refuses dispatch loudly. What changes is
reachability: ordinary merge traffic, not operator action.
NEXT-RUNG TRIGGER, now stated as blocked on modelling rather than effort: a
forward-only operand needs an ancestry read git.Core does not model. RevList
cannot express it -- its argv is hardcoded to `{since}..HEAD`, so it answers only
HEAD-relative questions, while the discriminating test needs both endpoints named.
2. THE IDENTITY OF THE CODE MAKING THE ADMISSION DECISION IS NOT MODELLED. On a
workflow_run event GitHub checks out the DEFAULT BRANCH HEAD, not the triggering
run's head_sha, and the checkout step names no ref. So the binary adjudicating
candidate C is built from whatever the default branch is when the admission runs.
The decision is correct about WHICH revision it admits -- the candidate comes from
the event payload, not the checkout -- but the judge's provenance is an accident
of timing, and today that default branch can itself be red.
The naive repair (check out the event's head_sha) is not automatically safe:
workflow_run is privileged and carries write credentials, and the in-model trust
wall runs after checkout and compilation, so it cannot protect a step that already
executed candidate code. Two honest constructions are named in the annotation;
both are larger than this change.
Annotation-only: the emitted workflows are byte-identical. Neither gap is introduced
here -- the advance this PR replaces was an ungated raw-HEAD stamp on every push,
which is strictly worse on both axes -- but shipping them undeclared would be the
rung inflation this PR exists to remove.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…t typed rows The two residual classes were declared in prose with no stable identifier, so a future migration would have to find them by memory. They now carry greppable keys: FleetDesiredAdvanceForwardOnly the backward-advance race FleetDesiredAdmissionJudgeIdentity the timing-dependent judge provenance WHY THEY ARE NOT TYPED CARRIERS, recorded beside them because section 4c says a machine-consumed fact belongs in one and these are not: The intended owner exists as a PLAN and not as a MODULE. gunbc.roadmap_authority specifies GuaranteeRequirement (class identity, domain, harm, ceiling with typed reason, next_rung_trigger) with GuaranteePath and GuaranteeMeasurement beside it and the disposition DERIVED rather than stored, as Stage 1b. Grepping the tree finds that vocabulary only in that roadmap prose; no module declares it. So the only way to give these typed owners today is a bespoke registry in this module, refused on three of this repository's own grounds: it would be a second authority for facts Stage 1b exists to own (section 3); its whole future is migration-then-deletion, failing section 6's survival test; and section 6 forbids a scaffold authorized by its own author. A private registry would make this module look more modeled while trading visible incompleteness for false completion. The annotation is untyped debt that is honest about being debt. When the real carrier lands these two classes move straight into GuaranteeRequirement rows with no interim registry to dissolve first. Annotation-only: the emitted .github/workflows/fleet-desired.yml is byte-identical, verified by re-running the emitter. The block attaches to expected_fleet_desired_yml rather than sitting at end-of-file -- a section 4c annotation needs a following declaration, and an earlier revision of this PR reddened the floor by forgetting that. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…re cargo fleet-desired.yml runs `cargo build --release -p v1-compiler` on the same srv1 self-hosted runner that deploy.yml has been dying on. It had no toolchain step, so it would have exited 127 exactly as deploy.yml has on all 14 of its runs: the admission job would die before deciding anything and the fleet ref would silently never advance. This PR is the ordering gate that makes the deploy path safe, and it was about to merge a workflow that could not run — reproducing, inside the fix, the defect the fix exists to stay ahead of. The step is imported from witness_floor_workflow rather than copied. It is one fact — what a self-hosted runner needs before cargo — with several consumers (DESIGN §3). It keeps its current name here; #8663 renames it to self_hosted_rust_toolchain_step and updates both consumers, and lands after this. Two claims, each observed RED against a model with the step removed: the_admission_workflow_installs_a_toolchain_before_its_first_cargo_invocation the_admission_toolchain_step_disables_the_shared_home_cache Found by asking what the agreed merge sequence assumed. Its step 5 was "observe its first real floor-completion admission", which is only reachable if the admission job can start — an assumption nothing checked and no review of this diff alone would have questioned. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
main deleted .github/workflows/deploy.yml (#8676, operator co-authored, "delete rather than repair -- the workflow's origin/ownership is unclear"). This branch had modified that file, so the merge is a modify/delete conflict. Resolved in favour of the deletion. THE PART THAT NEEDED A DECISION, recorded because the resolution is not mechanical: the deletion cut the emitted file but not its authority. live_deploy_workflow.dag and the LiveDeployYamlArtifact registry row (CommitRequired, path .github/workflows/deploy.yml) are still on main, so running the ordinary generated-artifact actuator RE-CREATES the file. Measured on this branch: [file] write .github/workflows/deploy.yml (1062 bytes). This branch's version of that file would be the SAFE one -- 0 pushes, 0 ref mutations, because this branch removes the advance step from the model -- but it is still toolchain-less and therefore still permanently red, and the operator deleted it. So re-adding it here would quietly reverse a decision I was not part of, on the strength of my regen output. Deleted it again after regen. This branch therefore matches main exactly: no deploy.yml in the tree, authority still declaring one. That inconsistency is pre-existing and owned by the deletion decision; this change neither resolves nor worsens it. Completing the root cut -- removing the registry row and the workflow projection so regen stops emitting -- is an open operator question, deliberately not taken here. Also included: two docs/plans regen one-liners. main's committed copies are stale against their authority (a NanosecondDuration -> std.measure Nanosecond rename that never regenerated). They are unrelated to this change and are carried rather than dropped, because silently discarding regen output is knowingly leaving drift in a generated artifact. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… two annotations #8683 landed the deploy-workflow root cut. Six conflicts, and two were the dangerous kind: modify/delete on live_deploy_workflow.dag and its witness file, where resolving the habitual way — keep my branch's version — would have restored the deleted module and undone the cut. Both take the deletion. RESOLUTIONS live_deploy_workflow.dag deleted (root cut wins) live_deploy_workflow_witness_test deleted (its subject is gone) generated_artifact{,_emit}.dag both intents: LiveDeployYamlArtifact removed, FleetDesiredAdmissionYamlArtifact kept ci_spec.dag two annotations merged into one .gitattributes regenerated, never hand-resolved BOTH SIDES DELETED THE SAME SCRIPT and each wrote its own account of why. Two annotations for one deletion is the duplication §3 forbids, so they are merged rather than stacked — the merged text keeps the admission-gate reasoning, the belt-dispatch consequence, the no-lease create branch, and the two-consumer census. The `data ..._deleted_note: String` row is dropped: a String declaration whose sole purpose is commentary is the misplaced data §4c names, and the annotation already carries it. THE FIFTH INTERVAL DEFECT, and the one that justifies the checklist: this branch's own witness file imported gunbc.live_deploy_workflow and had NO merge conflict, so git reported nothing. It surfaced as an unresolved import at witness time. the_deploy_workflow_no_longer_advances_the_fleet_revision is deleted rather than repointed — its subject no longer exists, and a claim whose subject is gone cannot be kept alive by aiming it elsewhere. The property is subsumed: a workflow that does not exist cannot advance the ref, and the retirement witness asserts the retired path is absent from the roster, which is what stops it being regenerated. VERIFIED ON THE MERGED TREE deploy.yml NOT written by main_wet — the cut holds workflows fleet-converge, fleet-desired, witnesses .gitattributes no deploy line, fleet-desired line present retirement witness (from main) 2/2 PASS against this tree admission witnesses 13/13 PASS dangling references to deleted symbols 0 in code (2 in historical prose) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Their names asserted more than the predicate proves. They are textual projection sentinels over emitted yaml, not proofs that a Cargo consumer is dominated by a Cargo provider: the_admission_workflow_installs_a_toolchain_before_its_first_cargo_invocation -> the_emitted_admission_yaml_places_a_setup_action_before_its_literal_cargo_build the_admission_toolchain_step_disables_the_shared_home_cache -> the_emitted_admission_yaml_disables_the_shared_home_cache_on_its_setup_action The predicate splits on the literal "cargo build", which has two unequal failure modes. A changed spelling — for example `"$CARGO_BIN" build`, which is exactly how fleet-converge.yml already invokes cargo — makes the first conjunct false and the claim RED: a false alarm, but fail-closed. A second non-literal invocation placed BEFORE the provider, with a later literal one still present, makes `.first()` span both and the claim PASSES: a false green, fail-open. Adding "$CARGO_BIN" to the match would enlarge the recognised spellings and move the hole one substitution along. A text search over emitted bytes cannot see what a step executes; that is the ceiling, not a gap in effort. §4b rung declared in the annotation: mitigatable, with the next-rung trigger named — workflow capability closure, a typed step operation deriving CargoCapability (that derivation already exists for validations in gunbc.roadmap_execution_contract) plus a projection that refuses to emit a job whose derived capabilities are unclosed. The structural control is then invariant under every spelling because it inspects none of them, and these two claims are deleted or demoted to a byte fixture rather than kept beside it as though both were safety mechanisms. The claims still execute and still hold; only the names and the recorded rung change. 13/13 pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The replacement advance renders a script and executes it through `sh`, and the annotations said so — but neither module carried a `Disposition = Scaffold` or a `DissolutionCondition`, while the surviving ci_spec annotation claimed the debt was "re-declared where the remaining shell actually lives". It was explained there and not actually re-declared. One obligation covers the renderer and its executor: they are one independently removable unit, the renderer exists solely to feed the executor, both dissolve into the same typed git CAS realization, and neither has a useful life without the other. This authorizes nothing. `std.disposition.Scaffold` records the construction and its dissolution binding and says nothing about permission; the operator verdict is an external fact bound to the current head. Leaving the debt unmarked was not the conservative choice — under the doctrine it is marked debt's violation plus concealment, and declaring the population is what makes the verdict decidable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two annotations described the same deleted deploy workflow with different numbers -- the workflow annotation said 14 runs, the witness annotation said 30. A count measured once and then restated is a snapshot that decays; two of them are a §3 fork over one fact. Measured from the run history rather than picking a side: 30 runs between 2026-08-20T03:55:43Z and 2026-08-20T17:14:32Z, 29 failure and 1 cancelled, zero successes ever. So 14 was wrong, and "exited 127 on all 30" was also wrong -- one run was cancelled and never reached the shell at all. Both annotations now carry the dated receipt with its window, so the claim is falsifiable against a stated observation instead of asserting a timeless count. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Superseded by a clean re-cut. This branch was pushed after #8643 squash-merged, so its merge base predates the landed content and GitHub renders the whole of #8643 again (+957/-14) when the actual delta is a two-annotation prose fix. Re-cut from current main as a 5-line change; closing this rather than leaving a PR whose diff misrepresents its own scope. — sent from nimble-fox-671 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Auto-opened by session-dashboard for session
nimble-fox-671.Pushing to
session/nimble-fox-671-fleetadmitadvances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan