diff --git a/.github/workflows/fleet-desired.yml b/.github/workflows/fleet-desired.yml index 56b3838d755..1d9fed02feb 100644 --- a/.github/workflows/fleet-desired.yml +++ b/.github/workflows/fleet-desired.yml @@ -2,9 +2,12 @@ name: fleet-desired on: workflow_run: workflows: [witnesses] + branches: [main] types: [completed] concurrency: + queue: max group: gunbc-fleet-desired-admission + cancel-in-progress: false jobs: admit: runs-on: [self-hosted, linux, arm64, srv1] @@ -29,7 +32,7 @@ jobs: set -eu ROOT=$(git rev-parse --show-toplevel 2>/dev/null || pwd) mkdir -p "$ROOT/target" - rm -f "$ROOT/target/fleet-desired-authorized-push.sh" + rm -f "$ROOT/target/fleet-desired-authorized-action.sh" cp "$GITHUB_EVENT_PATH" "$ROOT/target/fleet-desired-admission-event.json" - name: Decide whether the floor admits this revision run: | @@ -39,5 +42,5 @@ jobs: run: | set -eu ROOT=$(git rev-parse --show-toplevel 2>/dev/null || pwd) - test -s "$ROOT/target/fleet-desired-authorized-push.sh" - sh "$ROOT/target/fleet-desired-authorized-push.sh" + test -s "$ROOT/target/fleet-desired-authorized-action.sh" + sh "$ROOT/target/fleet-desired-authorized-action.sh" diff --git a/dag/extdeps/git/inspect.dag b/dag/extdeps/git/inspect.dag index 0f577a42412..7a7d5f47916 100644 --- a/dag/extdeps/git/inspect.dag +++ b/dag/extdeps/git/inspect.dag @@ -1,6 +1,7 @@ module extdeps.git.inspect -import std.types { Bool, CommitSha, FilePath, GitRef, String } +import std.types { Bool, CommitSha, FilePath, GitRef, Int, String } +import std.algebra { trim } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } @@ -64,6 +65,43 @@ data git_inspect_service_note: String = "Read-only repository-root, revision, an // `--exclude-standard` is pinned because without it the command applies no ignore rules at all and would // return every untracked path — the opposite of the question. The output is a bare NUL-separated path list, // so unlike porcelain v1 it carries no status codes and no rename-source continuation to track. +// MergeBase NAMES THE REPOSITORY IT INSPECTS, AND THE OPERAND IS REQUIRED. +// An ambient operation answers about whichever checkout the process happens to occupy, so the +// same call means different things depending on where it was invoked from -- and a wrong answer +// is INDISTINGUISHABLE from a right one, because two repositories can hold refs that look +// identical. An OPTIONAL operand would keep the ambient form writable, so it is required: the +// state this replaces has no spelling. +// +// THIS IS THE REPOSITORY'S OWN ESTABLISHED ANSWER, NOT A NEW CONVENTION. extdeps.git RemoteUrlIn +// already takes `repository_path` and renders `git -C {repository_path}`, for exactly this reason +// -- it could otherwise confirm the remote of the wrong checkout. This operation is brought into +// line with that authority rather than inventing a second way to say the same thing. +// +// WHY THE OPERAND SITS ON THE OPERATION AND NOT ON THE INVOCATION. "Which repository does this +// inspect" is a fact about the git operation's SUBJECT; "what directory did the OS start this +// process in" is a transport fact. Modeling the first as the second would push repository +// selection into every handler that runs a command -- the N x M adapter shape. One +// repository-addressed operation with one shell realization is not that. +// +// THE SIBLING POPULATION IS DECLARED RATHER THAN SILENTLY LEFT. Five operations in this service +// are still repository-ambient by the same mechanism: HeadCommit, WorkingTreeStatus, +// IgnoredFiles, ListTreePathsAtRevision and ShowTree. They are NOT ported here because each +// carries its own consumer census and this cut is scoped to the operation whose ambient +// repository blocked a wet observation. Toplevel is deliberately NOT in that list: its purpose IS +// to discover the ambient repository, so naming one would be circular. RUNG for the five: +// mitigatable, and the mitigation is only that production happens to run from the repository +// root. NEXT TRIGGER: the first consumer that must inspect a repository other than its own +// process position -- which is what forced this one. + +// MergeBase CARRIES ITS EXIT CODE BECAUSE THE Bool COLLAPSES AN ANSWER WITH AN ABSENCE OF ONE. +// `git merge-base` exits 1 when the two commits genuinely share NO merge base -- unrelated +// histories, which is a FACT about the pair -- and 128 when the ref is invalid or this is not a +// repository, which is a failure to look. Both render `exit_success = false`, so a consumer +// holding only the Bool must either refuse both (losing a real answer) or admit both (treating an +// unreadable repository as proof that two revisions are unrelated). That operation's `exit` block +// has always DECLARED the distinction; its output simply never surfaced it, so the declaration was +// unreachable by any caller. + // ResolveRefCommit is a SEPARATE operation from ShowTree rather than a format flag on it, and the // separation is the point: `%T` and `%H` answer different questions about the same ref. The tree is // the CONTENT at that ref; the commit is its identity INCLUDING ancestry, which the tree does not @@ -137,14 +175,15 @@ service git.Inspect { } operation MergeBase { - input { left: GitRef, right: GitRef } + input { repository_path: String, left: GitRef, right: GitRef } output { sha: CommitSha from "stdout" success: Bool from "exit_success" + exit_code: Int from "exit_code" stderr: String from "stderr" } readonly - transport shell { argv: ["git", "merge-base", "{left}", "{right}"] } + transport shell { argv: ["git", "-C", "{repository_path}", "merge-base", "{left}", "{right}"] } exit { 0 => Unit 1 => String "No merge base" @@ -197,3 +236,62 @@ service git.Inspect { } } } + +// MERGE-BASE EXIT SEMANTICS ARE A FACT OF GIT, SO THEY ARE MODELED HERE BESIDE THE EXIT TABLE THAT +// DECLARES THEM, and not re-derived by each consumer as bare integers compared with `==`. The +// operation above already states the contract -- 0, 1, 128 with distinct meanings -- and a consumer +// that mints its own `merge_base_exit_ok: Int = 0` beside it is holding a second representation of +// this module's fact: the §2/§3 undeclared sum, free to drift from the exit table the day a fourth +// code is declared, and free to be compared against the wrong operation's codes with no complaint +// from anything. +// +// THE THREE OUTCOMES ARE NOT A RANKING AND THE MIDDLE ONE IS NOT AN ERROR. Exit 1 is a legitimate +// ANSWER -- git looked and there is no common ancestor -- which is precisely what lets a consumer +// distinguish "these histories never met" from "I could not find out", the distinction §5 forbids +// collapsing. Exit 128 is the refusal: a bad object or a path that is not a repository, where +// nothing about the two revisions has been established. Rendering 128 as NoCommonAncestor would +// read an unreadable repository as proof that two revisions are unrelated. +// +// THE FIELD IS `base_hex`, NOT `stdout`, AND THAT RENAME IS THE ACTUAL FIX. It never held raw +// stdout: the operation's output binding delivers `sha` already stripped of git's line terminator, +// so a field named for the transport was describing something the transport does not hand over. +// +// THE NEWLINE CLAIM THIS PARAGRAPH ORIGINALLY MADE WAS FALSE AND IS CORRECTED BY MEASUREMENT. +// Review 54424 reported that a future caller passing raw stdout would get an "undecodable" refusal +// on a trailing newline, and I wrote a paragraph here asserting exactly that mechanism -- citing +// `git merge-base` emitting a newline after the fortieth hex digit, which it does. What I had not +// checked was whether that byte survives to this fold. It does not. Receipt: a recorded fixture's +// stored `sha` is 40 characters with no terminator, and REMOVING the trim below leaves the whole +// wet matrix green -- a mutation that changes nothing is the proof the guard was inert. The +// caller's trim, which this change deleted, was equally inert for the same reason. +// +// So the trim stays as idempotent normalization at the boundary that owns the wire format, and it +// is described as what it is: a total function over any string a caller hands this fold, NOT a +// live defect being closed. Calling it the latter would have been a fabricated mechanism sitting +// in a paragraph justifying its own code -- the same class as an inflated rung, and the reason the +// measurement is recorded here rather than the conclusion alone. +// +// Decoding that hex into an object id still belongs to the consumer that owns the id type; this +// module owns what git SAID and what its exit code MEANS, not how the caller names commits. +type MergeBaseOutcome + = MergeBaseReported { base_hex: String } + | NoCommonAncestor + | MergeBaseRefused { exit_code: Int, stderr: String } + +data merge_base_exit_reported: Int = 0 + +data merge_base_exit_no_common_ancestor: Int = 1 + +// Total over every integer, deliberately: an undeclared exit code is a REFUSAL carrying the code +// that produced it, never a fourth silent arm and never a default that resolves to an answer. +fn merge_base_outcome(exit_code: Int, stdout: String, stderr: String) -> MergeBaseOutcome { + if exit_code == merge_base_exit_reported { + MergeBaseReported { base_hex: trim(s: stdout) } + } else { + if exit_code == merge_base_exit_no_common_ancestor { + NoCommonAncestor + } else { + MergeBaseRefused { exit_code: exit_code, stderr: stderr } + } + } +} diff --git a/dag/extdeps/github/actions.dag b/dag/extdeps/github/actions.dag index b60caf82424..fd7e3ce6fc7 100644 --- a/dag/extdeps/github/actions.dag +++ b/dag/extdeps/github/actions.dag @@ -83,7 +83,7 @@ type WorkflowTrigger | Schedule { cron: CronSchedule } | WorkflowDispatch { inputs: List } | WorkflowCall { inputs: List } - | WorkflowRunCompleted { workflows: List } + | WorkflowRunCompleted { workflows: List, branches: List } | MergeGroup type PullRequestActivity @@ -144,6 +144,25 @@ type CancelInProgressWhenQueueMax = QueueMaxCancelInProgressFalse | QueueMaxCancelInProgressExpression { expression: String } +// THE `queue` KEY IS NOT IN GITHUB'S PUBLISHED WORKFLOW SYNTAX, AND ITS BEHAVIOUR HERE IS +// GROUNDED BY OBSERVATION RATHER THAN BY CITATION. That is the honest position and it is stated on +// the type rather than left for a reader to assume a doc link exists: raised in review 54384, which +// asked whether GitHub silently ignores the key -- in which case the queueing guarantee reduces to +// `cancel-in-progress: false` and the emitted yaml promises something the platform never consumes. +// +// Established by execution, not by reading: two workflows differing ONLY in this key, three rapid +// pushes each, same repository and runner pool. With `queue: max` all four runs completed and none +// was cancelled; without it, two of four were CANCELLED while pending. So the key is consumed and +// it changes behaviour in exactly the direction the variant names. The measured receipt lives in +// the observing layer, per the external-upstream rule that an observation this repository produces +// is a receipt of ours and not a fact authored inside the upstream module: gunbc.fleet_desired_admission_workflow +// `fleet_desired_queue_max_measured_receipt`. +// +// WHAT IS STILL UNGROUNDED, named so it is not mistaken for settled: an undocumented key can change +// or be withdrawn without a deprecation, and the 100-pending ceiling is read from GitHub's prose +// about full queues rather than from a specification of this key. Next-rung trigger: GitHub +// publishing `queue` in the workflow-syntax authority, at which point this note becomes an ordinary +// citation row and the receipt becomes a regression control rather than the grounding itself. type ConcurrencySpec = ConcurrencyScalar { group: String } | ConcurrencyMappingQueueMax { diff --git a/dag/extdeps/languages/yaml/gha_workflow.dag b/dag/extdeps/languages/yaml/gha_workflow.dag index c917deb88a3..65da484c21e 100644 --- a/dag/extdeps/languages/yaml/gha_workflow.dag +++ b/dag/extdeps/languages/yaml/gha_workflow.dag @@ -167,9 +167,10 @@ fn workflow_trigger_entry(trigger: WorkflowTrigger) -> YamlKeyValue { ])) WorkflowCall { inputs: _ } => kv(key: "workflow_call", value: YamlNull) - WorkflowRunCompleted { workflows: ws } => + WorkflowRunCompleted { workflows: ws, branches: bs } => kv(key: "workflow_run", value: yaml_mapping(entries: [ kv(key: "workflows", value: string_list_flow(items: ws)), + kv(key: "branches", value: string_list_flow(items: bs)), kv(key: "types", value: string_list_flow(items: [workflow_run_activity_completed])) ])) MergeGroup => @@ -195,6 +196,8 @@ fn cancel_in_progress_when_queue_max_yaml(spec: CancelInProgressWhenQueueMax) -> } } +data workflow_run_branches_emission_note: String = "GitHub filters workflow_run by the branch of the TRIGGERING run, documented as `You can use the branches or branches-ignore filter to specify what branches the triggering workflow must run on in order to trigger your workflow` (docs.github.com Events that trigger workflows, workflow_run, read 2026-08-21). That is the same fact a job-level `head_branch ==` condition tests, one grain earlier: the condition skips the job AFTER the run has been created and has entered its concurrency group, while the filter stops the event creating a run at all. The distinction is load-bearing rather than cosmetic -- a created-then-skipped run still occupies a concurrency slot, and in the default group an arriving entry evicts the pending one, so an irrelevant branch could cancel a real pending admission and then do nothing. The member is REQUIRED and emitted unconditionally, matching the Push and PullRequest siblings: a caller declaring this trigger must decide which branches it answers to, and an omitted filter meaning `every branch` is exactly the state that produced the eviction." + data concurrency_queue_max_emission_note: String = "ConcurrencyMappingQueueMax exists to express GitHub's `queue: max`, and until this row it emitted NO queue key — so it serialized byte-identically to ConcurrencyMappingQueueNotMax and the modeled distinction had no realization difference at all (srv1-deploy-serialization-and-false-greens.md §4, second drop). That matters because the two variants mean DIFFERENT THINGS on the platform: the default (QueueNotMax) holds at most one running and one pending entry, and a newly-arriving entry CANCELS the existing pending one, whereas `queue: max` permits multiple pending up to a documented cap of 100 with cancel-in-progress forced false. A caller reaching for QueueMax is asking for the no-cancel queue and was silently getting pending-replacement. `queue` is emitted FIRST so the mapping reads queue-then-group-then-cancel; CancelInProgressWhenQueueMax already models the platform's constraint that cancel-in-progress cannot be true here, so that arm needs no extra guard. Witness: gha_job_projection_witness_test asserts the emitted mapping CONTAINS the queue key and that the two variants no longer serialize identically." fn concurrency_mapping_queue_max(group: String, cip: CancelInProgressWhenQueueMax?) -> YamlValue { diff --git a/dag/gunbc/ci_layer_roots.dag b/dag/gunbc/ci_layer_roots.dag index f68a116af81..7a8653485ac 100644 --- a/dag/gunbc/ci_layer_roots.dag +++ b/dag/gunbc/ci_layer_roots.dag @@ -161,6 +161,12 @@ data witness_exclusion_frontier: List = [ reason: "wet-integration class (wet_integration_offline_note posture), substantiated per-row: direct_rust_door_emit_write_compile_holds runs tools.direct_rust_door_transport.run_direct_rust_door_emit_write_compile_smoke, which performs live shell.Mktemp.Dir, Filesystem.Write, and cargo.Build.BuildManifest effects with no hermetic mock_response coverage. Hermetic discovery REFUSES rather than fabricating Unit, so per-PR discovery cannot exercise the write-to-disk + compile receipt. Ingest-path provenance and closing-contract witnesses live in src/v2/test/claim/long/ (5s budget rule); fast closure witnesses stay per-PR in src/v2/test/claim/self_host/.", dissolution: unbound_dissolution(description: "the wet lane un-darkens and admits live cargo compile smokes under its own budget; this witness enrolls there as a declared execution row and this exclusion deletes. Local recipe until then: claim_batch --wet --source-root dag --source-root src/v2 --entry dag/test/claim/direct_rust_door_write_compile_witness_test.dag --function direct_rust_door_emit_write_compile_holds") }, + WitnessExclusionRow { + pattern: "fleet_revision_relation_wet_matrix_test.dag", + classification: OfflineLocalRecipe, + reason: "wet/replay class (wet_integration_offline_note posture), substantiated by reading the carrier rather than by a floor red: every dispatching row reaches git.Inspect.MergeBase, which publishes no mock_response, so hermetic discovery REFUSES by construction rather than skipping. WHAT MAKES THIS ROW DIFFERENT FROM ITS SIBLINGS ABOVE, and the reason it is not merely 'another live-effects file': the recorded observations that WOULD make it hermetic already exist and are committed — the seven cases were recorded wet against a deterministic fixture repository and replay green from dag/test/fixtures/fleet-revision-relation. The blocker is that there is no way to hand them to a floor run. v2.std.witness_evaluation WitnessEvaluationFrame carries `rest_fixtures: List` and nothing else; its own note states that filesystem and environment replay bindings are intended to extend that carrier later, and no shell/service arm exists yet. The external store this file's recipe uses is a claim_batch flag (--fixture-store) and claim_executor has no equivalent, so neither route reaches the required floor. So the honest state is: the composition is PROVEN, and its proof executes nowhere the floor can see. THE PURE HALF IS NOT EXCLUDED — the merge-base fold's exit-code and relation controls stay discovery-enrolled in fleet_main_revision_witness_test.dag per-PR (exit_one_is_an_answer_and_exit_one_two_eight_is_an_absence_of_one, one_merge_base_decides_both_directions, a_successful_probe_with_undecodable_output_refuses); only the effectful composition runs here.", + dissolution: unbound_dissolution(description: "A SHELL/SERVICE FIXTURE ARM ON v2.std.witness_evaluation WitnessEvaluationFrame, beside rest_fixtures, so a recorded shell-transport observation can be installed for the dynamic extent of a witness the way a REST one already is. That is the carrier the frame's own note anticipates. When it lands these nine rows enroll unchanged — they are already written against a replay store — and this exclusion deletes; no second trigger is needed and the wet lane un-darkening is NOT one, because these rows do not need live git, they need their recorded answers to reach a hermetic run. Local recipe until then, and it carries its own discriminating controls: RECORD claim_batch --wet --record --fixture-store dag/test/fixtures/fleet-revision-relation --source-root dag --source-root src/v2 --entry dag/test/claim/fleet_revision_relation_wet_matrix_test.dag --functions identical_revisions_are_converged_without_dispatching_a_probe,identical_revisions_converge_even_when_the_path_is_not_a_repository,an_ancestor_current_is_a_forward_advance,an_ancestor_accepted_is_superseded,siblings_sharing_an_ancestor_are_neither_ancestor_of_the_other,an_orphan_root_has_no_common_ancestor,an_absent_object_is_unverifiable_not_unrelated,a_non_repository_path_is_unverifiable_rather_than_answering,no_merge_base_and_could_not_look_stay_distinguishable ; REPLAY the same command with --hermetic in place of --wet --record ; CONTROL replay again with --fixture-store pointing at an EMPTY directory — the two short-circuit rows must still PASS and the other seven must FAIL with `missing recorded fixture`, which is what proves the passing replay consumed recorded observations rather than reaching live git. The fixture repository is rebuilt by docs/plans/fleet-revision-relation-fixture.md") + }, WitnessExclusionRow { pattern: "external_model_scope_live_cover_witness_test.dag", classification: OfflineLocalRecipe, diff --git a/dag/gunbc/ci_spec.dag b/dag/gunbc/ci_spec.dag index 3672a6d9d7d..b18f5be4a07 100644 --- a/dag/gunbc/ci_spec.dag +++ b/dag/gunbc/ci_spec.dag @@ -461,7 +461,7 @@ data gunbc_ci_srv1_tasks_observation_function: String = "observe_srv1_tasks_prea // on a floor-green main push (needs: [ci] IS the floor-green admission — this job exists // only downstream of the required check succeeding in the same run), advance // refs/fleet/desired to the merged revision by CAS: --force-with-lease names the exact -// observed prior (gunbc.fleet_main_revision admit_fleet_desired_advance's from side), so +// observed prior (gunbc.fleet_main_revision decide_fleet_desired_advance's from side), so // a race with a concurrent advance refuses rather than overwriting; ref creation is the // from=none arm. Hosts follow the ref; no host is contacted here. @@ -915,7 +915,7 @@ fn gunbc_ci_authorized_key_enroll_invoke() -> String { // // The CAS half was correct. The ADMISSION half did not exist: gunbc.fleet_main_revision requires the // desired revision to derive from merged, FLOOR-GREEN main and models that gate as -// admit_fleet_desired_advance, and this script never called it -- so the gate's only caller was its +// decide_fleet_desired_advance, and this script never called it -- so the gate's only caller was its // own witness test while the unproven path ran on every push to main. That is exactly the raw-HEAD // advance the authority names as its prevented class, and it reached further than the ref: // gunbc.roadmap_belt_actuate gates worker dispatch on revision standing, so a desired ref equal to diff --git a/dag/gunbc/fleet_desired_admission.dag b/dag/gunbc/fleet_desired_admission.dag index 9eec1af5546..609477ebd54 100644 --- a/dag/gunbc/fleet_desired_admission.dag +++ b/dag/gunbc/fleet_desired_admission.dag @@ -1,9 +1,11 @@ module gunbc.fleet_desired_admission -import std.types { String, Bool, FilePath } +import std.types { String, Bool, FilePath, NonEmptyStr } import std.process { ProcessExit, ExitSuccess, exit_failure } import extdeps.filesystem.filesystem_io { Filesystem } -import extdeps.git.object_store { GitObjectId, git_object_id_from_untagged_hex, git_object_id_wire_hex } +import extdeps.git.object_store { + GitObjectId, GitRefName, git_object_id_from_untagged_hex, git_object_id_wire_hex, +} import extdeps.git.publication_transport { GitRemoteRefExpectation, RemoteRefMustBeAbsent, @@ -26,25 +28,45 @@ import extdeps.github.workflow_run_event { WorkflowRunEventPayloadReadRefused, workflow_run_event_from_event_path, } -import gunbc.witness_floor_workflow { witness_floor_workflow_name } -import gunbc.repo_identity { gunbc_default_branch_name } +import gunbc.fleet_revision_acceptance { + AcceptedFleetRevision, + RequiredCiSucceeded, + DefaultBranchRevisionObserved, + RequiredCiAdmitted, + RequiredCiRefused, + DefaultBranchAdmitted, + DefaultBranchRefused, + FleetRevisionAccepted, + RequiredCiAndDefaultBranchRevisionMismatch, + accept_required_ci_workflow_run, + observe_default_branch_revision, + admit_fleet_revision, + required_ci_refusal_message, + default_branch_refusal_message, +} +import gunbc.fleet_desired_observe { observe_fleet_revision_relation, observe_fleet_desired_revision } import gunbc.fleet_main_revision { - fleet_desired_ref_name, - FleetDesiredRevision, - FleetDesiredExpectationDecision, + FleetDesiredAdvanceInput, + FleetDesiredExpectationRefusedInput, + FleetDesiredRefAbsentInput, + FleetDesiredObservedCurrentInput, + FleetDesiredAdvanceDecision, + FleetDesiredAdvanceAdmitted, + FleetDesiredAlreadyConverged, + FleetDesiredSupersededNoOp, + FleetDesiredAdvanceRefused, + fleet_desired_advance_expectation, + fleet_desired_advance_refusal_message, + decide_fleet_desired_advance, FleetDesiredExpectationReady, FleetDesiredExpectationRefused, - FleetDesiredExpectationRefusal, - FleetDesiredRefUndecodable, - FleetDesiredRefUnobserved, - FleetDesiredAdvance, - AdvanceAdmitted, - AdvanceRefused, - admit_fleet_desired_advance, - fleet_desired_advance_expectation, - fleet_desired_revision_target, + FleetDesiredAbsent, + FleetDesiredUndecodable, + fleet_desired_ref_name, + FleetDesiredRevision, + FleetDesiredAdmitted, + FleetDesiredUnobserved, } -import gunbc.fleet_desired_observe { observe_fleet_desired_revision } import std.disposition { Disposition, Scaffold, SingleAuthority } import std.dissolution { DissolutionCondition, unbound_dissolution } import std.decl_ref { DeclarationRef, WholeDeclaration } @@ -52,7 +74,7 @@ import std.decl_ref { DeclarationRef, WholeDeclaration } // THIS MODULE IS THE LIVE HALF OF THE ADMISSION GATE, AND IT EXISTS BECAUSE THE GATE HAD // NO PRODUCTION CONSUMER. gunbc.fleet_main_revision states the rule in its own header — // the desired revision derives from MERGED, FLOOR-GREEN main, never from raw HEAD — and -// models it as admit_fleet_desired_advance, whose refusal names the prevented class +// models it as decide_fleet_desired_advance, whose refusal names the prevented class // ("raw-HEAD simultaneous fleet-bricking"). Until this module landed that function's ONLY // caller was its witness test, while the shell step emitted by gunbc.ci_spec // (gunbc_ci_advance_fleet_desired_script) stamped $GITHUB_SHA on every push to main @@ -72,7 +94,7 @@ import std.decl_ref { DeclarationRef, WholeDeclaration } // ordinary spawn". Advancing desired to whatever last landed makes that comparison agree // unconditionally, so the gate passes silently. Gating the advance is what gives the // dispatch gate something real to compare against. -data fleet_desired_admission_note: String = "The live consumer of gunbc.fleet_main_revision admit_fleet_desired_advance. See the annotation above it." +data fleet_desired_admission_note: String = "The live consumer of gunbc.fleet_main_revision decide_fleet_desired_advance. See the annotation above it." // The floor run's event payload, copied to a modeled path by the workflow step so the // decision reads a path this module names rather than an environment variable it cannot @@ -88,166 +110,117 @@ data fleet_desired_admission_event_payload_path: String = "target/fleet-desired- // yet — extdeps.git.publication_transport PushRefUpdate is shadow-only and models no // --force-with-lease — so the actuation stays shell; what changed is that the DECISION no // longer does. -data fleet_desired_admission_authorized_push_path: String = "target/fleet-desired-authorized-push.sh" +data fleet_desired_admission_authorized_action_path: String = "target/fleet-desired-authorized-action.sh" // The repository root the observation reads. The admission runs in the checkout the // workflow prepared, so the desired ref is observed through that checkout's origin. data fleet_desired_admission_repo_root: FilePath = "." as FilePath -// THE AUTHORIZED ADVANCE CARRIES AN EXPECTATION, NOT A PRIOR OID, and that is the shape the -// four-observation split forced. `from: GitObjectId` could only ever be spelled for the one -// observation that yields an oid, so it made ref CREATION — the case gunbc.fleet_main_revision -// says is the only other write it admits — unrepresentable in this outcome. The expectation is -// the closed sum extdeps.git.publication_transport already owns for exactly this: an oid the -// remote must still hold, or a claim that the remote holds nothing. +// THREE POSITIVE ACTIONS, AND TWO OF THEM MUTATE NOTHING. +// +// The workflow executes `test -s ; sh `, and that guard is not a convenience -- +// IT IS THE WALL SEPARATING "AUTHORIZATION PRODUCED NOTHING" FROM "AUTHORIZATION SAID DO NOTHING". +// Before this port those were the same state on disk (no file) and the guard refused both, which +// was correct while every authorized outcome was a push. It is no longer correct, because a +// converged or superseded decision is a SUCCESS that writes no git mutation. +// +// So the absent file keeps exactly one meaning: the decision never ran, crashed, or could not +// write. It is the transport-failure signal and nothing else. The tempting repair, one line away, +// is to see `test -s` fail on a legitimate no-op and relax it to "no file means nothing to do" -- +// at which point a crashed decider, a failed write, or a mis-set $ROOT all render as a successful +// no-op, permanently and silently. That is why the no-op arms are POSITIVE actions. +// +// AND EMPTY IS UNREACHABLE BY SHAPE, not by remembering to echo: every arm of the renderer below +// begins with a literal, so no decision can produce an empty script. The return type says +// NonEmptyStr and the fold makes it true. HONEST RUNG: the compiler does not today establish the +// NonEmptyStr refinement -- it is a declared carrier, not a proof -- so this is construction at +// the fold rather than a structural guarantee. What it does buy is that adding a fourth action +// cannot silently produce an empty script without deleting a literal on purpose. +type FleetDesiredAuthorizedAction + = FleetDesiredRemoteAdvance { accepted: GitObjectId, expected_prior: GitObjectId } + | FleetDesiredAlreadyConvergedAction { revision: GitObjectId } + | FleetDesiredSupersededAction { accepted: GitObjectId, current: GitObjectId } + type FleetDesiredAdmissionOutcome - = AdmissionAdvanceAuthorized { expected: GitRemoteRefExpectation, to: GitObjectId } + = AdmissionActionAuthorized { action: FleetDesiredAuthorizedAction } | AdmissionRefused { cause: String } -// THE TRUST WALL RE-CHECKS WHAT THE TRIGGER FILTER ALREADY CLAIMS, and that is deliberate -// rather than redundant. The workflow_run trigger names the floor workflow, but a trigger -// widened later — a second workflow added to the list, a branch filter dropped, the file -// edited on another branch — would silently route a foreign run's conclusion into an -// admission. The reader refuses on identity it can see in the payload, so a widened -// trigger is caught here instead of admitted. Each arm names the member that disagreed and -// both sides of the comparison; none of them widens to a default. -fn fleet_desired_admission_event_trusted(event: WorkflowRunEvent) -> String? { - if event.activity != "completed" { - Present { value: concat("fleet_desired_admission: workflow_run activity is not completed: ", event.activity) } - } else { - if event.workflow_name != witness_floor_workflow_name { - Present { - value: join([ - "fleet_desired_admission: conclusion belongs to workflow ", - event.workflow_name, - ", not the required floor (", - witness_floor_workflow_name, - ")", - ], ""), +// THE TRUST WALL IS GONE FROM THIS MODULE, AND THAT IS THE POINT OF THE PORT. +// +// fleet_desired_admission_event_trusted and fleet_desired_floor_green are DELETED, not wrapped. +// They answered "is this event a trustworthy floor result" and "was the floor green" with a String +// option and a Bool, and gunbc.fleet_revision_acceptance now answers both as two typed +// propositions over one decoded revision. Keeping the old pair as helpers would have left two +// authorities for one question -- the fork this lane spends its time removing -- and the Bool in +// particular bound greenness to no revision at all. +// +// WHAT THE PORT MUST NOT LOSE, checked arm by arm rather than assumed: the old wall refused a +// non-completed activity, a run of another workflow, a non-default branch, and a fork's head +// repository. The new producers refuse all four, and two of them more strictly -- the workflow is +// matched by PATH rather than name, and the repository is matched against the repository authority +// rather than only against itself, so a fork whose head and base agree with each other no longer +// passes. The new producers also refuse a non-push originating event, which the old wall did not +// check at all. +type FleetDesiredAcceptedRevision + = FleetDesiredRevisionAccepted { accepted: AcceptedFleetRevision } + | FleetDesiredRevisionRefused { cause: String } + +// The evidence both propositions carry is the run id: both facts are read from ONE delivered +// event, so claiming two independent provenances would be a lie about where they came from. +fn fleet_desired_accepted_from_event(event: WorkflowRunEvent) -> FleetDesiredAcceptedRevision { + match accept_required_ci_workflow_run(event: event, evidence: event.run_id) { + RequiredCiRefused { cause: why } => + FleetDesiredRevisionRefused { + cause: concat("fleet_desired_admission: ", required_ci_refusal_message(cause: why)), } - } else { - if event.head_branch != gunbc_default_branch_name { - Present { - value: join([ - "fleet_desired_admission: floor run is on branch ", - event.head_branch, - ", not ", - gunbc_default_branch_name, - " — only the default branch admits a fleet revision", - ], ""), - } - } else { - if event.head_repository_full_name != event.repository_full_name { - Present { - value: join([ - "fleet_desired_admission: floor run head repository ", - event.head_repository_full_name, - " is not this repository ", - event.repository_full_name, - " — a fork's run never admits a fleet revision", - ], ""), + RequiredCiAdmitted { succeeded: ci } => + match observe_default_branch_revision(event: event, evidence: event.run_id) { + DefaultBranchRefused { cause: why } => + FleetDesiredRevisionRefused { + cause: concat("fleet_desired_admission: ", default_branch_refusal_message(cause: why)), + } + DefaultBranchAdmitted { observed: br } => + match admit_fleet_revision(required_ci: ci, default_branch: br) { + FleetRevisionAccepted { accepted: a } => FleetDesiredRevisionAccepted { accepted: a } + RequiredCiAndDefaultBranchRevisionMismatch { + required_ci_revision: ci_rev, + default_branch_revision: br_rev, + } => + FleetDesiredRevisionRefused { + cause: join([ + "fleet_desired_admission: the floor proved ", + git_object_id_wire_hex(oid: ci_rev) as String, + " while the default branch carries ", + git_object_id_wire_hex(oid: br_rev) as String, + " -- both facts are true of different revisions, and only their conjunction would license an advance", + ], ""), + } } - } else { - none - } } - } - } -} - -// floor_green is DERIVED FROM THE DELIVERED CONCLUSION AND NOWHERE ELSE. Only Success is -// green; every other conclusion — including Cancelled, Skipped and StartupFailure — leaves -// it false and the modeled gate refuses with its own cause. There is no arm here that -// decides a non-Success conclusion is close enough, which is the point: the argument this -// function feeds is the one the authority says the ref advances on. -fn fleet_desired_floor_green(conclusion: WorkflowRunConclusion) -> Bool { - match conclusion { - Success => true - Failure => false - Cancelled => false - Neutral => false - Skipped => false - TimedOut => false - ActionRequired => false - StartupFailure => false } } -// THE OBSERVATION IS DECIDED BY gunbc.fleet_main_revision AND NOWHERE ELSE. This function used -// to match FleetDesiredRevision itself, over the two variants that type had when it was written. -// When the authority split into four (#8701, "FOUR OBSERVATIONS, FOUR REMEDIES") the match here -// went non-exhaustive and refused main's floor for eleven commits — the fail-closed substrate -// doing exactly what it should, naming the second decision site the authority's own header had -// already warned about ("A consumer holding only `none` cannot choose, so it would have to -// rematch the original observation, putting a second decision site beside this one"). -// -// So the repair is not two more arms here. It is to consume `fleet_desired_advance_expectation`, -// the seam that module publishes for this question, so a fifth observation is a change in one -// place. What survives locally is only the rendering of each typed refusal into this gate's -// cause string, which is a fact about THIS consumer's diagnostics, not about the observation. -// -// AN UNOBSERVED PRIOR STILL REFUSES; IT IS NEVER READ AS "no prior, so this is the first -// admission". That distinction is now the authority's — FleetDesiredAbsent is a claim about the -// remote and authorizes a creation, FleetDesiredUnobserved is the absence of any claim and -// authorizes nothing — where before this arm had to refuse both because it could not tell them -// apart. Collapsing them would make an ls-remote failure create the ref from scratch and -// overwrite an admitted revision it simply could not read, which is the empty-observation narrow -// with the fleet as the blast radius. -// -// AdvanceAdmitted's `from` is discarded at the admitting arm below, and that is deliberate: the -// CAS operand this gate publishes is the EXPECTATION, and both it and `current` are derived from -// the same observation by the same authority — re-deriving the prior from the admission's echo -// would be a second spelling of one fact. The prior is still passed IN, so the authority is asked -// the question it models rather than a narrowed one. -fn fleet_desired_admission_expectation_refusal_cause(refusal: FleetDesiredExpectationRefusal) -> String { - match refusal { - FleetDesiredRefUnobserved { cause: why } => - join([ - "fleet_desired_admission: the admitted prior could not be observed, so no advance is authorized (an unobserved prior is never read as an absent one): ", - why, - ], "") - FleetDesiredRefUndecodable { advertised: line } => - join([ - "fleet_desired_admission: the desired ref exists holding an advertisement that cannot be decoded, so no advance is authorized (a retry will not fix it and a write would destroy it): ", - line, - ], "") - } -} - -fn fleet_desired_admission_decide(event: WorkflowRunEvent, observed: FleetDesiredRevision) -> FleetDesiredAdmissionOutcome { - match fleet_desired_admission_event_trusted(event: event) { - Present { value: refusal } => AdmissionRefused { cause: refusal } - Absent => - match fleet_desired_advance_expectation(observed: observed) { - FleetDesiredExpectationRefused { cause: why } => - AdmissionRefused { cause: fleet_desired_admission_expectation_refusal_cause(refusal: why) } - FleetDesiredExpectationReady { expectation: expected } => - match git_object_id_from_untagged_hex(hex: event.head_sha as String) { - Absent => - AdmissionRefused { - cause: concat("fleet_desired_admission: floor run head_sha is not a decodable object id: ", event.head_sha as String), - } - Present { value: candidate } => - match admit_fleet_desired_advance( - candidate: candidate, - floor_green: fleet_desired_floor_green(conclusion: event.conclusion), - current: fleet_desired_revision_target(d: observed), - ) { - AdvanceRefused { cause: why } => - AdmissionRefused { - cause: join([ - why, - " [floor conclusion: ", - workflow_run_conclusion_wire_label(conclusion: event.conclusion), - "; candidate: ", - event.head_sha as String, - "]", - ], ""), - } - AdvanceAdmitted { from: _, to: admitted } => - AdmissionAdvanceAuthorized { expected: expected, to: admitted } - } - } +// Decision to action. Every admitted decision becomes exactly one positive action; every refusal +// becomes a cause and NO action, so the absent file continues to mean only that. +fn fleet_desired_action_from_decision( + decision: FleetDesiredAdvanceDecision, +) -> FleetDesiredAdmissionOutcome { + match decision { + FleetDesiredAdvanceAdmitted { accepted: a, expected_prior: prior } => + AdmissionActionAuthorized { + action: FleetDesiredRemoteAdvance { accepted: a.revision, expected_prior: prior }, + } + FleetDesiredAlreadyConverged { accepted: a } => + AdmissionActionAuthorized { + action: FleetDesiredAlreadyConvergedAction { revision: a.revision }, + } + FleetDesiredSupersededNoOp { accepted: a, current: cur } => + AdmissionActionAuthorized { + action: FleetDesiredSupersededAction { accepted: a.revision, current: cur }, + } + FleetDesiredAdvanceRefused { cause: why } => + AdmissionRefused { + cause: concat("fleet_desired_admission: ", fleet_desired_advance_refusal_message(cause: why)), } } } @@ -262,94 +235,151 @@ fn fleet_desired_admission_decide(event: WorkflowRunEvent, observed: FleetDesire // its dissolution binding and says nothing about permission — the operator verdict is an external // fact bound to the current head, and unmarked debt is not a way to defer it (it is marked debt's // violation plus concealment). Declaring the population is what makes the verdict decidable. -data fleet_desired_authorized_push_shell_scaffold: Disposition = Scaffold { +data fleet_desired_authorized_action_shell_scaffold: Disposition = Scaffold { dissolves_to: SingleAuthority, bind: DeclarationRef { module_path: "gunbc.fleet_desired_admission", - decl_name: "fleet_desired_authorized_push_script", + decl_name: "fleet_desired_authorized_action_script", field: WholeDeclaration } } -data fleet_desired_authorized_push_shell_dissolution_trigger: DissolutionCondition = unbound_dissolution(description: "🟡 dissolve-on: fleet_desired_authorized_push_script + gunbc.fleet_desired_admission_workflow fleet_desired_admission_push_step — the admitted advance is a model-rendered script executed by `sh`, because extdeps.git.publication_transport PushRefUpdate is shadow-only and models no --force-with-lease, so the compare-and-swap the authority requires has no typed carrier; DISSOLVES WHEN the SCM ref-update realization lands as a typed git CAS service op carrying the expected-prior operand (membership-diff spine classify_change SCM-ref arm) invoked via host_effect_apply, at which point the renderer and the sh step are deleted together") +data fleet_desired_authorized_action_shell_dissolution_trigger: DissolutionCondition = unbound_dissolution(description: "🟡 dissolve-on: fleet_desired_authorized_action_script + gunbc.fleet_desired_admission_workflow fleet_desired_admission_action_step — the admitted advance is a model-rendered shell script executed by `sh`. THE PREMISE THIS ROW CARRIED UNTIL 2026-08-21 WAS THAT NO TYPED COMPARE-AND-SWAP CARRIER EXISTED; that is now false and the honest remaining debt is narrower. extdeps.git.publication_transport PushRefUpdateWithLease IS the typed leased-push wire capability, and its own annotation states its rung: it takes `lease` and `refspec` as three independent NonEmptyStr, so nothing at that boundary requires them to have been derived from one GitRemoteRefCasRequest, and it collapses a REFUSED LEASE (an answer — the remote moved, re-observe and retry) into the same nonzero-plus-String as a TRANSPORT FAILURE (no answer at all). It has zero consumers. So what is missing is not the capability but the three things that would make it safe to be its first consumer: the sole request-to-wire binder push_remote_ref_compare_and_swap, a cited decoder for git's push-rejection output that separates a stale lease from a failed push, and an independent remote readback confirming the ref landed where the decision said. DISSOLVES WHEN those three land and this module reaches the remote through the binder instead of through rendered argv, at which point the renderer and the sh step are deleted together — not before, because moving to the typed row today would trade a shell that is honestly untyped for a typed call whose refusal semantics this gate cannot yet read.") -// The authorized push, rendered from the decision's own operands. The lease and the refspec are -// BOTH derived from one GitRemoteRefCasRequest through the authority that owns their spelling -// (extdeps.git.publication_transport), which is the pairing that row's own next-trigger note asks -// its first production consumer to hold: this gate never spells a lease or a refspec of its own, -// so it cannot pair a lease naming one ref with a refspec moving another. +// THE WIRE WORDS COME FROM THE CAS-REQUEST CARRIER, NOT FROM A STRING BUILT HERE. An earlier +// revision of this renderer hand-spelled `--force-with-lease=:`, which was a SECOND +// rendering of the lease beside extdeps.git.publication_transport, the module that owns it. That +// survives the creation retraction because it is orthogonal to it: the expectation is constructed +// here as RemoteRefMustEqual because an admitted advance is the only thing this gate authorizes, +// and the carrier still renders the words. +// +// A RECEIPT-ONLY PHRASE FUNCTION WAS DELETED WITH THE CREATION ARM rather than kept for one live +// case. It existed to render absence as a positive word, because git spells "must be absent" as +// an EMPTY expect value and an empty string in a receipt cannot be told from an operand nobody +// printed. With creation unauthorized here that arm is unreachable, and an unreachable arm is the +// dead-state problem in miniature. The reasoning is preserved upstream in nimble-fox-671's #8768, +// where creation IS authorized and the distinction is live. +// +// The authorized action, rendered from the decision's own operands. On the advancing arm +// --force-with-lease names the observed prior as the expected value, so a concurrent admission +// refuses at the remote instead of silently overwriting -- the compare-and-swap the authority +// requires, with the `from` side supplied by the gate rather than re-read by the shell. // -// An absent expectation renders as git's documented empty ``, so ref CREATION is the same -// compare-and-swap rather than an unconditional push — a concurrent admission that got there -// first refuses at the remote instead of being silently overwritten, in both directions. -fn fleet_desired_authorized_push_cas_request(expected: GitRemoteRefExpectation, to: GitObjectId) -> GitRemoteRefCasRequest { - GitRemoteRefCasRequest { - remote: "origin", - ref_name: fleet_desired_ref_name, - new_oid: to, - expected: expected, +// THE TWO NO-OP ARMS ARE NONEMPTY BY SHAPE, NOT BY REMEMBERING TO ECHO. Every arm opens with +// `set -eu` and the return type is NonEmptyStr, so an authorized no-op can never render as an +// empty file. That matters because the executing step's `test -s` is the wall distinguishing +// "authorization produced nothing" -- a transport or writer failure -- from "authorization said +// do nothing". If a no-op could render empty, those two states would collide at the only place +// that can still tell them apart, and a dropped authorization would read as a converged fleet. +fn fleet_desired_authorized_action_script(action: FleetDesiredAuthorizedAction) -> NonEmptyStr { + match action { + FleetDesiredRemoteAdvance { accepted: to, expected_prior: prior } => { + let request = GitRemoteRefCasRequest { + remote: "origin" as NonEmptyStr, + ref_name: fleet_desired_ref_name as GitRefName, + new_oid: to, + expected: RemoteRefMustEqual { oid: prior }, + } + join([ + "set -eu\n", + "git push ", git_remote_ref_lease_word(request: request) as String, + " ", request.remote as String, + " ", git_remote_ref_cas_refspec(request: request) as String, "\n", + "echo \"[fleet-desired] admitted ", git_object_id_wire_hex(oid: to) as String, + " expected-prior ", git_object_id_wire_hex(oid: prior) as String, "\"\n", + ], "") as NonEmptyStr + } + FleetDesiredAlreadyConvergedAction { revision: rev } => + join([ + "set -eu\n", + "echo \"[fleet-desired] already converged at ", + git_object_id_wire_hex(oid: rev) as String, + "; no ref mutation\"\n", + ], "") as NonEmptyStr + FleetDesiredSupersededAction { accepted: acc, current: cur } => + join([ + "set -eu\n", + "echo \"[fleet-desired] superseded: accepted ", + git_object_id_wire_hex(oid: acc) as String, + " is an ancestor of the current ", git_object_id_wire_hex(oid: cur) as String, + "; no ref mutation\"\n", + ], "") as NonEmptyStr } } -// The expectation as the RECEIPT says it, which is a different rendering from the one the LEASE -// needs: git spells "must be absent" as an empty , and an empty string in a receipt is -// indistinguishable from a prior that was never printed. So this renders the absent arm as a -// positive word rather than as nothing, and it matches over the closed sum instead of over the -// lease's hex-or-empty text — the two renderings answer to the same authority but not to the -// same reader. -fn fleet_desired_receipt_expected_phrase(expected: GitRemoteRefExpectation) -> String { - match expected { - RemoteRefMustBeAbsent => "absent" - RemoteRefMustEqual { oid: prior } => git_object_id_wire_hex(oid: prior) as String +// THE ONLY EFFECTFUL STEP BETWEEN THE ACCEPTED REVISION AND THE DECISION. +// +// The three-way classification of the observed ref is NOT repeated here: it is +// fleet_desired_advance_expectation's, and re-deriving "absent vs unreadable vs unobserved" beside +// it would be a second authority for the question that seam exists to answer. This function only +// routes each already-classified outcome into the input variant that carries the evidence that +// outcome has -- and only the observed-current branch reaches git at all, because it is the only +// one with two revisions to relate. +// +// THE RemoteRefMustBeAbsent ARM BELOW IS THE CREATION RETRACTION WORKING, NOT A LEFTOVER OF IT, +// and it is called out here because the correct action and the tidy-looking action are opposites. +// Creation is unauthorized, so a reader finishing the retraction by deleting the last mention of +// the absent expectation would delete that arm -- and an observed-absent remote would then have +// nowhere to land. Absence remains a real, observable STATE and must be CLASSIFIED in order to +// REACH its refusal. What the retraction removed is the authorized ACTION downstream; it never +// removed the ability to say what was seen. Same family as the absent-arm witness: a red or a +// stray symbol is not evidence of which repair is wanted, and only the policy separates them. +// (Pinned by nimble-fox-671 while independently verifying the retraction at fa2290eb6c5.) +fn fleet_desired_advance_input_wet( + accepted: AcceptedFleetRevision, +) -> FleetDesiredAdvanceInput { + match fleet_desired_advance_expectation( + observed: observe_fleet_desired_revision(repo: fleet_desired_admission_repo_root), + ) { + FleetDesiredExpectationRefused { cause: why } => + FleetDesiredExpectationRefusedInput { accepted: accepted, cause: why } + FleetDesiredExpectationReady { expectation: e } => + match e { + RemoteRefMustBeAbsent => FleetDesiredRefAbsentInput { accepted: accepted } + RemoteRefMustEqual { oid: current } => + FleetDesiredObservedCurrentInput { + accepted: accepted, + current: current, + relation: observe_fleet_revision_relation( + current: current, + accepted: accepted.revision, + ), + } + } } } -// The receipt names BOTH operands of the compare-and-swap. Naming only the target leaves a run -// that cannot evidence which prior the push required, and the run holds no other copy of it: the -// script executes under `set -eu` with no trace, so the lease word is never echoed, and git's own -// range line reports the transition that HAPPENED rather than the one that was DEMANDED. Those -// coincide exactly when the CAS held, which is the thing a receipt is supposed to let a reader -// check rather than assume. Measured before this row: eleven successful admissions whose expected -// prior appears nowhere in their logs. -fn fleet_desired_authorized_push_script(expected: GitRemoteRefExpectation, to: GitObjectId) -> String { - let request = fleet_desired_authorized_push_cas_request(expected: expected, to: to) - let to_hex = git_object_id_wire_hex(oid: to) as String - let expected_phrase = fleet_desired_receipt_expected_phrase(expected: expected) - join([ - "set -eu\n", - "git push ", git_remote_ref_lease_word(request: request) as String, - " ", request.remote as String, - " ", git_remote_ref_cas_refspec(request: request) as String, "\n", - "echo \"[fleet-desired] admitted ", to_hex, " expected-prior ", expected_phrase, "\"\n", - ], "") -} - func admit_fleet_desired_from_floor_event_wet() -> ProcessExit { match workflow_run_event_from_event_path(path: fleet_desired_admission_event_payload_path) { WorkflowRunEventObserved { event: event } => - match fleet_desired_admission_decide( - event: event, - observed: observe_fleet_desired_revision(repo: fleet_desired_admission_repo_root), - ) { - AdmissionRefused { cause: why } => exit_failure(reason: why) - AdmissionAdvanceAuthorized { expected: expected, to: to_oid } => { - let wrote = Filesystem.Write( - path: fleet_desired_admission_authorized_push_path, - content: fleet_desired_authorized_push_script(expected: expected, to: to_oid), - ) - if wrote.success { - ExitSuccess - } else { - exit_failure( - reason: join([ - "fleet_desired_admission: the advance was admitted but the authorized push could not be written to ", - fleet_desired_admission_authorized_push_path, - ": ", - wrote.error, - ], ""), - ) + match fleet_desired_accepted_from_event(event: event) { + FleetDesiredRevisionRefused { cause: why } => exit_failure(reason: why) + FleetDesiredRevisionAccepted { accepted: accepted } => + match fleet_desired_action_from_decision( + decision: decide_fleet_desired_advance( + input: fleet_desired_advance_input_wet(accepted: accepted), + ), + ) { + AdmissionRefused { cause: why } => exit_failure(reason: why) + AdmissionActionAuthorized { action: action } => { + let wrote = Filesystem.Write( + path: fleet_desired_admission_authorized_action_path, + content: fleet_desired_authorized_action_script(action: action) as String, + ) + if wrote.success { + ExitSuccess + } else { + exit_failure( + reason: join([ + "fleet_desired_admission: the action was authorized but could not be written to ", + fleet_desired_admission_authorized_action_path, + " -- the absent file is the transport-failure signal and must never be read as a no-op: ", + wrote.error, + ], ""), + ) + } + } } - } } WorkflowRunEventMemberAbsent { member: m } => exit_failure(reason: concat("fleet_desired_admission: floor run event payload is missing a required member: ", m)) diff --git a/dag/gunbc/fleet_desired_admission_workflow.dag b/dag/gunbc/fleet_desired_admission_workflow.dag index bbc9b809a5b..07e64cf89cc 100644 --- a/dag/gunbc/fleet_desired_admission_workflow.dag +++ b/dag/gunbc/fleet_desired_admission_workflow.dag @@ -7,7 +7,7 @@ import extdeps.github.actions { Workflow, Job, Step, RunStep, UsesStep, WorkflowTrigger, WorkflowRunCompleted, WorkflowPermissions, PermWrite, - ConcurrencySpec, ConcurrencyMappingQueueNotMax, + ConcurrencySpec, ConcurrencyMappingQueueMax, QueueMaxCancelInProgressFalse, checkout_action, github_event_path_env } @@ -17,7 +17,7 @@ import gunbc.merge_admission_produce { ci_repo_root_shell } import gunbc.witness_floor_workflow { witness_floor_workflow_name, witness_floor_toolchain_step } import gunbc.fleet_desired_admission { fleet_desired_admission_event_payload_path, - fleet_desired_admission_authorized_push_path, + fleet_desired_admission_authorized_action_path, } import v2.std.optional { Present } import std.types { String } @@ -34,7 +34,8 @@ import std.types { String } // // WHAT THIS REPLACES. deploy.yml previously ended with a step that stamped $GITHUB_SHA onto // refs/fleet/desired on every push to main, consulting nothing. The modeled gate -// (admit_fleet_desired_advance) existed the whole time with its witness test as its only caller. +// (gunbc.fleet_main_revision decide_fleet_desired_advance) existed the whole time with its witness +// test as its only caller. // That is not a missing feature, it is a wall standing beside an actuator that walked around it, // and the blast radius reaches further than the ref: gunbc.roadmap_belt_actuate gates worker // dispatch on revision standing, so a desired ref that always equals whatever last landed makes @@ -104,7 +105,7 @@ fn fleet_desired_admission_stage_payload_step() -> Step { "set -eu\n", "ROOT=", ci_repo_root_shell(), "\n", "mkdir -p \"$ROOT/target\"\n", - "rm -f \"$ROOT/", fleet_desired_admission_authorized_push_path, "\"\n", + "rm -f \"$ROOT/", fleet_desired_admission_authorized_action_path, "\"\n", "cp \"$", github_event_path_env, "\" \"$ROOT/", fleet_desired_admission_event_payload_path, "\"\n", ], ""), shell: none, @@ -137,22 +138,24 @@ fn fleet_desired_admission_decide_step() -> Step { } } -// THE ACTUATION CARRIES NO DECISION. It executes the push the model authorized and nothing +// THE ACTUATION CARRIES NO DECISION. It executes the action the model authorized and nothing // else -- no ref name, no candidate revision, no expected prior appears in this shell, because // all three are operands of the admission and are rendered into the authorized script by the // decision that produced them. A shell that cannot name a revision cannot push an unadmitted // one. The test -s is not a second gate but a refusal to run an absent or empty authorization: // if the previous step somehow exited zero without writing one, this stops rather than -// treating a missing authorization as permission. -fn fleet_desired_admission_push_step() -> Step { +// treating a missing authorization as permission. Two of the three authorized actions mutate no +// ref at all -- already-converged and superseded -- and they still render a nonempty script, so +// `test -s` continues to separate "nothing was written" from "nothing was to be done". +fn fleet_desired_admission_action_step() -> Step { RunStep { name: Present { value: "Execute the authorized fleet-desired advance" }, id: none, run: join([ "set -eu\n", "ROOT=", ci_repo_root_shell(), "\n", - "test -s \"$ROOT/", fleet_desired_admission_authorized_push_path, "\"\n", - "sh \"$ROOT/", fleet_desired_admission_authorized_push_path, "\"\n", + "test -s \"$ROOT/", fleet_desired_admission_authorized_action_path, "\"\n", + "sh \"$ROOT/", fleet_desired_admission_authorized_action_path, "\"\n", ], ""), shell: none, env: none, @@ -176,7 +179,7 @@ fn fleet_desired_admission_job() -> Job { fleet_desired_admission_build_step(), fleet_desired_admission_stage_payload_step(), fleet_desired_admission_decide_step(), - fleet_desired_admission_push_step() + fleet_desired_admission_action_step() ], needs: [], env: none, @@ -201,26 +204,99 @@ fn fleet_desired_admission_job() -> Job { } } -// CONCURRENCY, STATED AS WHAT THE PLATFORM ACTUALLY PROVIDES. An earlier revision of this -// annotation claimed "queued, never cancelled ... must admit in order", and review 53998 caught -// that the chosen variant does not provide it. Per the authority -// (extdeps.languages.yaml.gha_workflow concurrency_queue_max_emission_note), the default group -// modeled by ConcurrencyMappingQueueNotMax holds at most one running and one PENDING entry, and a -// newly-arriving entry CANCELS the pending one; multi-entry in-order queueing is what -// ConcurrencyMappingQueueMax was minted for. Asserting the queue property here was a state-space -// conflation of "in-order queue" with the platform's pending-replacement default -- a prose claim -// the emitted bytes do not support. +// CONCURRENCY, AND THE VARIANT CHANGED BECAUSE THIS CHANGE CHANGED WHAT IS SAFE. // -// The variant is nonetheless the RIGHT one, and the corrected reason is narrower than the claim it -// replaces. What this workflow needs is that a RUNNING admission is never interrupted, because a -// cancellation between the compare-and-swap decision and the push would leave the advance -// half-observed; 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 not a defect but -// the preferable outcome: the desired ref should track the newest floor-green revision, and -// admitting each intermediate one in turn would be slower convergence for no gain. Reaching for -// QueueMax would buy the in-order queue this comment used to claim and then have to justify why the -// fleet wants to walk through revisions it has already passed. +// THAT THE QUEUE IS REAL IS MEASURED, NOT ASSUMED, and the measurement is recorded here because +// review 54384 asked the question that would have made everything below fiction: `queue: max` is +// not in GitHub's published workflow syntax, so does the platform CONSUME it or accept and ignore +// it? Ignored, the guarantee reduces to `cancel-in-progress: false` and this file promises a +// property nothing enforces -- worse than no guarantee, because it is planned against. // +// THE EXPERIMENT (2026-08-21, throwaway branch, deleted after reading): two workflows identical +// but for this one key, each fired by the same three rapid pushes, each job sleeping 70s so the +// pushes genuinely contend. With `queue: max`: four runs, four success, ZERO cancelled -- and one +// completed, one in_progress and one PENDING were observed coexisting, a state that cannot exist +// under a depth-one queue. The CONTROL, identical minus the key: TWO OF FOUR CANCELLED while +// pending. The control is what makes this a measurement rather than an anecdote -- it proves the +// probe can detect the difference at all, and it independently reproduces the very defect this +// workflow exists to close (main's own fleet-desired.yml carries bare `group`, and 9 of its runs +// are cancelled). +// +// WHAT IS PROVEN: the key is read, and it moves behaviour in the direction the variant names. +// WHAT IS NOT, stated so the receipt is not over-read: the 100-pending ceiling, which comes from +// GitHub's prose about full queues rather than any specification of this key; and the key's +// stability, since an undocumented field can be withdrawn without deprecation. Next-rung trigger +// is GitHub publishing `queue` in the workflow-syntax authority, at which point this becomes an +// ordinary citation and the probe becomes a regression control rather than the grounding itself. +// +// Per the authority (extdeps.languages.yaml.gha_workflow concurrency_queue_max_emission_note) the +// DEFAULT group -- ConcurrencyMappingQueueNotMax -- holds at most one running and one PENDING +// entry, and a newly-arriving entry CANCELS the pending one. ConcurrencyMappingQueueMax is the +// multi-entry queue, up to a documented cap of 100 pending, with cancel-in-progress forced false. +// +// THIS WORKFLOW USED THE DEFAULT, AND THE ARGUMENT FOR IT WAS THAT LOSING A SUPERSEDED PENDING +// ADMISSION IS PREFERABLE TO WALKING THE FLEET THROUGH REVISIONS IT HAS ALREADY PASSED. That +// argument was sound, and its premise -- that every entry in the group is an admission which +// subsumes the pending one -- was false in three separate ways: +// +// A PULL REQUEST'S FLOOR (nimble-fox-671, against origin/main). The trigger named no branches, +// so every branch's floor completion created a run that entered this one constant group and +// only then skipped on the job-level condition. Observed tally over 131 runs: 77 skipped, +// 45 cancelled, 6 failure, 3 success -- consistent with routine silent drops. +// A RED MAIN FLOOR (nimble-fox-671, against the branch-filter fix). A red floor does not +// supersede a green admission; it cancels one and refuses in its place. +// A MANUAL DISPATCH OR AN OLDER SUCCESSFUL RERUN ON MAIN (side-chat review). Both carry +// head_branch main, both pass the branch filter, neither can advance -- and arrival order is +// not revision order. +// +// TWO FIXES, AND THEY ARE NOT ALTERNATIVES: THE BRANCH FILTER AND THE QUEUE ANSWER DIFFERENT +// HALVES. The population splits by whether admissibility is DECIDABLE AT THE TRIGGER GRAIN. +// A pull request's floor is decidable there -- the platform knows the branch -- so the right move +// is to REFUSE THE ENTRY, and the trigger now carries `branches`. Widening the queue to hold +// those instead would have been the absorbing fallback: it cannot compute which entries matter, +// so it holds them all, the deficit's frequency goes to zero by construction, and the cost is +// denominated in the corpus of branches rather than in the change. +// +// The remaining population -- every main-floor completion -- is NOT decidable at the trigger +// grain. Whether a run can advance depends on its conclusion, its originating event and its +// ancestry, and all three are facts this repository reads IN-MODEL, after the run exists. So +// GitHub's workflow-level concurrency is structurally too early to know whether an arriving entry +// subsumes a pending one. Queueing there is not a widened container standing in for a decision; +// it is the honest handling of a question that layer cannot answer, deferred to the layer that +// can. That is why QueueMax is right for this half and was wrong for the other. +// +// WHAT MAKES THE QUEUE SAFE IS THIS CHANGE, WHICH IS WHY THE VARIANT MOVES NOW AND NOT EARLIER. +// Before forward-only landed, queueing every main completion would have walked the desired ref +// BACKWARD -- an older admission arriving later observes the newer prior correctly, and +// --force-with-lease does not refuse a correctly-observed overwrite. Under that model the default +// group's drop was accidentally protective, and the sound-sounding argument above was collecting +// the benefit of a defect. decide_fleet_desired_advance now classifies a superseded candidate as +// a no-op, so every queued entry is harmless by construction: it advances, converges, no-ops, or +// refuses. The drop was buying safety that is now carried properly, and keeping it is pure loss. +// +// CANCEL-IN-PROGRESS IS FORCED FALSE ON THIS VARIANT, which preserves the one property the +// default group was genuinely providing: a RUNNING admission is never interrupted, so no +// cancellation can land between the compare-and-swap decision and the push. +// +// WHAT THE QUEUE BUYS, STATED AT ITS CEILING RATHER THAN AT ITS INTENT. GitHub: "Up to 100 jobs +// or workflow runs can be `pending` in the concurrency group. When the queue is full, any +// additional jobs or workflow runs are canceled." So this buys RETENTION INSTEAD OF +// PENDING-REPLACEMENT WHILE THE GROUP SITS BELOW 100 PENDING -- not losslessness. And it buys no +// ordering: pending entries are processed by when they began waiting, which is neither dispatch +// order nor commit order, and GitHub does not guarantee order at all. +// +// Both limits are stated because the alternative was already tried in prose one revision ago: +// the witness for this mapping was named `..._queues_every_admissible_completion_...`, and +// "every" is not a property the emitted bytes can witness -- at 100 pending the mechanism cancels +// and a witness reading the mapping still greens. A name outlives the reasoning that produced it. +// +// IF LOSSLESSNESS BECOMES REQUIRED, THE NEXT RUNG IS NOT A BIGGER QUEUE. It is durable +// reconciliation over (eligible floor-green revisions MINUS recorded admission decisions), which +// is an event ledger rather than a transport cap. Related but distinct: a NARROWER TERMINAL +// DESIGN puts concurrency AFTER classification, so only a positive AcceptedFleetRevision enters +// serialized actuation -- a classification job feeding a serialized actuation job, or the fabric +// queue. The queue here is the correct interim for both, and a stand-in for neither. + // DECLARED GAP -- SEARCH KEY: FleetDesiredAdvanceForwardOnly // WHAT ORDERING DOES NOT COVER: THE DESIRED REF CAN MOVE BACKWARD, AND THIS IS ORDINARY RATHER // THAN AN EDGE CASE. An earlier revision of this annotation said reaching it "requires deliberately @@ -271,13 +347,15 @@ fn fleet_desired_admission_job() -> Job { data fleet_desired_admission_workflow: Workflow = Workflow { name: "fleet-desired", on: [ - WorkflowRunCompleted { workflows: [witness_floor_workflow_name] } + WorkflowRunCompleted { + workflows: [witness_floor_workflow_name], + branches: [gunbc_default_branch_name], + } ], concurrency: Present { - value: ConcurrencyMappingQueueNotMax { + value: ConcurrencyMappingQueueMax { group: fleet_desired_admission_workflow_concurrency_group, - cancel_in_progress: none, - explicit_single: none + cancel_in_progress: Present { value: QueueMaxCancelInProgressFalse } } }, env: none, diff --git a/dag/gunbc/fleet_desired_observe.dag b/dag/gunbc/fleet_desired_observe.dag index 568ad9a231e..35def67f7ec 100644 --- a/dag/gunbc/fleet_desired_observe.dag +++ b/dag/gunbc/fleet_desired_observe.dag @@ -3,12 +3,18 @@ module gunbc.fleet_desired_observe import std.types { String, Bool, FilePath, GitRef } import std.algebra { trim } import extdeps.git +import extdeps.git.inspect import extdeps.git.object_store { GitObjectId, git_object_id_from_untagged_hex, git_object_id_eq, + git_object_id_wire_hex, } +import gunbc.live_deploy.revision { SameRevision } +import gunbc.output_policy { OutcomeIsData } import gunbc.fleet_main_revision { + FleetRevisionRelationObservation, + fleet_revision_relation_from_merge_base, fleet_desired_ref_name, FleetDesiredRevision, FleetDesiredAdmitted, @@ -55,6 +61,97 @@ fn observe_fleet_desired_revision(repo: FilePath) -> FleetDesiredRevision { } } +data fleet_desired_observe_repository_path: String = "." + +data fleet_desired_observe_repository_path_note: String = "The repository whose ancestry this observer inspects. It is `.` in production because the admission workflow runs in the checkout, and it is a DECLARED `.` rather than an ambient one so that a witness can point the same observation at a fixture repository without relocating the process." + + +// THE EFFECTFUL HALF OF THE ANCESTRY OBSERVATION, AND THE SOLE PRODUCTION CONSTRUCTOR OF A +// MERGE-BASE-DERIVED RELATION. +// +// The decidable half is a pure fold in gunbc.fleet_main_revision, and only this function may feed +// it observed facts. Product code must not author an exit_code, a base hex and a stderr and call +// that fold as though those had been observed -- the fold stays public because the POLICY has to +// be witnessable hermetically (git.Inspect.MergeBase carries no mock_response, so any witness +// reaching it refuses under the hermetic envelope), but authoring its inputs outside an actual +// probe is fabricating an observation. +// +// THE REPOSITORY IS NAMED, NOT INHERITED. An earlier revision of this annotation said the +// repository was "STATED RATHER THAN PARAMETERIZED" -- that git.Inspect.MergeBase took no +// repository, so this function's precondition was that the process already sits in the right +// checkout. That is no longer true and the sentence would now describe a shape the operation +// refuses: MergeBase requires `repository_path`, so the fact is supplied rather than assumed. +// +// Why it mattered enough to change the operation: an ambient repository makes a WRONG answer +// indistinguishable from a right one, because two checkouts can hold refs that look identical. +// It also made the observation unwitnessable against a controlled fixture, since a witness cannot +// relocate its own process. + +// THE REPOSITORY IS A PARAMETER HERE AND BOUND ONE FUNCTION BELOW, and the split exists because +// the annotation above made a promise the signature could not keep: it said a witness could point +// this observation at a fixture repository without relocating its process, while the repository was +// reachable only as a module-scope constant. Naming the repository on the OPERATION removed the +// ambient checkout; it did not give a caller any way to say WHICH repository, so the observation +// remained exactly as unwitnessable as before, now with a note claiming otherwise. +// +// This is not a second policy authority and the asymmetry is the point: `_in` owns the whole +// observation composition and the wrapper owns exactly one fact, which repository production reads. +// Both reach the same pure fold, so a matrix run against a fixture repository exercises the real +// observer rather than the merge-base operation alone -- the gap that let git.Inspect.MergeBase be +// proven by record/replay while the composition above it stayed unproven. +// +// The alternative -- record against `.` while launching the recorder from another directory -- is +// specifically rejected: it makes one identical operation input mean different repositories +// depending on ambient process state, which is the ambiguity naming the repository removed. +// THE CALLER NO LONGER TRIMS, and the reason is narrower than it looks: the trim here was INERT. +// The operation's output binding already delivers `sha` without git's line terminator -- measured, +// not assumed (a recorded fixture's stored sha is 40 characters, and removing the trim left the +// whole wet matrix green). So this was a guard against a byte that never arrives, and normalization +// now happens once inside extdeps.git.inspect merge_base_outcome, at the boundary that owns the +// wire format. Deleting it removes a second site for one invariant; it does not close a defect, +// and saying otherwise would credit this change with a repair it did not make. +fn observe_fleet_revision_relation_in( + repository_path: String, + current: GitObjectId, + accepted: GitObjectId, +) -> FleetRevisionRelationObservation { + if git_object_id_eq(left: current, right: accepted) { + FleetRevisionRelationObservation { + current: current, + accepted: accepted, + relation: SameRevision, + } + } else { + let probe = git.Inspect.MergeBase( + repository_path: repository_path, + left: git_object_id_wire_hex(oid: current) as String as GitRef, + right: git_object_id_wire_hex(oid: accepted) as String as GitRef, + expect: OutcomeIsData, + ) + fleet_revision_relation_from_merge_base( + current: current, + accepted: accepted, + exit_code: probe.exit_code, + base_hex: probe.sha as String, + stderr: probe.stderr, + ) + } +} + +// The production binding, and the ONLY place the production repository is named. Note what it does +// NOT do: it does not re-check equality, re-decode, or re-classify. A wrapper that repeated any of +// that would be the second authority this split was written to avoid. +fn observe_fleet_revision_relation( + current: GitObjectId, + accepted: GitObjectId, +) -> FleetRevisionRelationObservation { + observe_fleet_revision_relation_in( + repository_path: fleet_desired_observe_repository_path, + current: current, + accepted: accepted, + ) +} + // The local half of the comparison: what revision THIS host's deployed tree is at. // Absent (typed, located in the cause the caller renders) when the repo path is not a // git repository or HEAD does not decode — never a fabricated revision. diff --git a/dag/gunbc/fleet_main_revision.dag b/dag/gunbc/fleet_main_revision.dag index f6959b9f884..31aed8f5319 100644 --- a/dag/gunbc/fleet_main_revision.dag +++ b/dag/gunbc/fleet_main_revision.dag @@ -1,12 +1,29 @@ module gunbc.fleet_main_revision -import std.types { String, NonEmptyStr, Bool } -import extdeps.git.object_store { GitObjectId } +import std.types { String, NonEmptyStr, Bool, Int } +import extdeps.git.object_store { GitObjectId, git_object_id_eq, git_object_id_from_untagged_hex, git_object_id_wire_hex } +import extdeps.git.inspect { + MergeBaseOutcome, + MergeBaseReported, + NoCommonAncestor, + MergeBaseRefused, + merge_base_outcome, +} import extdeps.git.publication_transport { GitRemoteRefExpectation, RemoteRefMustBeAbsent, RemoteRefMustEqual, } +import gunbc.live_deploy.revision { + DeployRevisionRelation, + revision_relation_from_ancestry_facts, + SameRevision, + DeployedIsAncestor, + CandidateIsAncestor, + UnrelatedHistories, + RelationUnverifiable, +} +import gunbc.fleet_revision_acceptance { AcceptedFleetRevision } // fleet-main-revision-authority (arc item 3, operator directive 2026-08-08): the fleet's // desired revision derives from MERGED, FLOOR-GREEN main — never from a CLI argument, a @@ -96,26 +113,437 @@ fn fleet_desired_advance_expectation(observed: FleetDesiredRevision) -> FleetDes } } -// The admission gate: the ref advances ONLY when the candidate revision's floor is -// green. The advance is a compare-and-swap naming the expected prior (git update-ref -// — the MemberChanged `from` side, per the reconcile spine's CAS -// ruling), so a concurrent admission refuses instead of silently overwriting. A prior -// of none is the first admission (ref creation). -type FleetDesiredAdvance - = AdvanceAdmitted { from: GitObjectId?, to: GitObjectId } - | AdvanceRefused { cause: String } - -fn admit_fleet_desired_advance( - candidate: GitObjectId, - floor_green: Bool, - current: GitObjectId?, -) -> FleetDesiredAdvance { - if floor_green { - AdvanceAdmitted { from: current, to: candidate } +// THE ADMISSION GATE. A LEASE MAKES THE WRITE ATOMIC; IT DOES NOT MAKE IT MONOTONE. +// +// This is the correction that shapes the whole decision below, because it is the thing most +// easily assumed. A compare-and-swap naming the observed prior refuses a CONCURRENT modification +// -- someone else moved the ref while we were deciding -- and it says NOTHING about direction. A +// perfectly valid lease against a correctly observed prior will move the ref BACKWARDS to an +// older revision without complaint, and every check upstream of it will have passed: the +// revision was proven, the floor was green, the observation was real, the lease matched. Nothing +// in the CAS is capable of noticing. Forward-only motion is a SEPARATE property and it needs its +// own evidence, which is what the relation observation supplies. +// +// WHAT THE INPUTS USED TO BE, AND WHY NONE OF THEM SURVIVES: +// +// candidate: GitObjectId -- a target nameable independently of any evidence about it, so a +// caller could present proof about revision A and advance onto B. +// floor_green: Bool -- unfalsifiable at the call site. It asserts that SOME floor was +// green and binds that greenness to no revision at all. +// current: GitObjectId? -- `none` meant both "no such ref, create it" and "could not observe +// it", and the arm took the SAME action for both, so a transport +// failure actuated a ref CREATION. +// +// All three are replaced by carriers that cannot express the bad state rather than by checks +// that detect it. AcceptedFleetRevision is constructible only from two exact positive facts +// about ONE revision, so there is no candidate left beside it to substitute and no Bool standing +// in for "which revision was proven". FleetDesiredExpectationDecision has already refused the +// observations that license nothing. +// +// THE RELATION IS SUBJECT-BOUND, AND THE BINDING IS CHECKED RATHER THAN TRUSTED. A bare +// `DeployedIsAncestor` is not evidence: it does not say WHICH TWO revisions were compared, so a +// relation computed for some other pair would satisfy a decision about this one. The observation +// therefore carries both endpoints, and this function refuses when they are not the exact pair +// under decision. Without that check the subject-binding would be a naming convention rather +// than a wall -- which is the same distinction between a carrier that says a thing and a carrier +// that enforces it that the rest of this file exists to make. + +// ONE SUBJECT-BOUND RECORD, AND EXACTLY ONE WAY TO SAY "UNVERIFIABLE". +// +// This was a two-variant coproduct -- Observed carrying a DeployRevisionRelation, and Refused +// carrying a cause -- and that was a duplicate representation of one fact, because +// DeployRevisionRelation ALREADY has RelationUnverifiable { cause }. The proof that no distinction +// existed is that the decision mapped both to the same refusal: an Observed-carrying-Unverifiable +// and a Refused were indistinguishable downstream, so the outer variant was carrying nothing. +// +// A record removes the choice. Every observation names exactly one pair and exactly one relation +// result, every failure to establish direction is RelationUnverifiable, and the subject-binding +// check has one shape to inspect rather than two. Remedies that later need separating belong +// inside a typed cause for RelationUnverifiable -- one authority, refined -- not in a second outer +// refusal path beside it. +type FleetRevisionRelationObservation { + current: GitObjectId + accepted: GitObjectId + relation: DeployRevisionRelation +} + +// THE ANCESTRY OBSERVATION, SPLIT SO THE DECIDABLE HALF IS ACTUALLY TESTABLE. +// +// This fold is PURE: it takes the wire facts a merge-base probe returns and produces the +// subject-bound relation. The effect that obtains those facts lives at the workflow edge, and the +// split is not tidiness -- git.Inspect.MergeBase carries no mock_response, so ANY witness that +// reaches it refuses under the hermetic floor envelope rather than running. Folding the decision +// into the effect would therefore make the entire ancestry policy unwitnessable, and the tree has +// already paid for that lesson once (stage0_rust_host_observation_live_witness_test records a +// single unmocked operation taking down a 105-row batch). Here the policy is hermetic and total, +// and only the reading of two commits is not. +// +// EXIT 1 AND EXIT 128 ARE THE WHOLE REASON THIS TAKES AN EXIT CODE. `git merge-base` exits 1 when +// the pair genuinely shares no merge base -- unrelated histories, a FACT about the pair -- and 128 +// when a ref is invalid or this is not a repository, which is a failure to look. Both are +// `exit_success = false`. A consumer holding only that Bool must either refuse both, discarding a +// real answer, or admit both, which reads an unreadable repository as proof that two revisions are +// unrelated and then refuses an advance that should have been admitted. The distinction was always +// declared on the operation and was simply never surfaced. +// +// A MERGE BASE THAT IS NEITHER ENDPOINT MEANS THE HISTORIES DIVERGED, and it folds to +// UnrelatedHistories to match the semantics the existing probe fold already assigns that variant +// (gunbc.live_deploy.revision deploy_revision_relation_from_probes: neither-is-ancestor yields +// UnrelatedHistories). Reusing that vocabulary rather than minting a Diverged variant keeps one +// authority for "how do these two revisions relate"; the name is the deploy lane's, and it means +// neither-is-an-ancestor rather than share-no-history. +fn fleet_revision_relation_from_merge_base( + current: GitObjectId, + accepted: GitObjectId, + exit_code: Int, + base_hex: String, + stderr: String, +) -> FleetRevisionRelationObservation { + FleetRevisionRelationObservation { + current: current, + accepted: accepted, + relation: merge_base_relation( + current: current, + accepted: accepted, + exit_code: exit_code, + base_hex: base_hex, + stderr: stderr, + ), + } +} + +// THE EXIT CODES ARE NOT MATCHED HERE. They are git's fact and extdeps.git.inspect owns them +// beside the exit table that declares them; this module receives an already-classified +// MergeBaseOutcome and decides only what that outcome means for a fleet advance. The two local +// `merge_base_exit_*: Int` rows that used to sit here were an undeclared sum -- a second +// representation of the operation's own exit table, comparable against any other operation's codes +// without complaint from anything (raised in review 54373). +// +// A DECLARED CONFLATION SURVIVES THIS CHANGE, AND IT IS NOW VISIBLE AT ONE LINE INSTEAD OF NONE. +// NoCommonAncestor (git looked; these histories never met) and a reported base that is neither +// endpoint (they diverged from a shared past) both fold to UnrelatedHistories, because that is the +// vocabulary gunbc.live_deploy.revision owns and its variant means neither-is-an-ancestor. The two +// states are genuinely different and have opposite remedies: a divergence is a force-push or a +// rebase and the shared base is the thing an operator reasons from, while no common ancestor at all +// means the configured revision came from somewhere else entirely -- a wrong remote, a wrong +// repository -- which no amount of history reading will reconcile. The refusal message on that +// variant currently asserts "share no ancestry", which is FALSE for the divergent case and that is +// the overwhelmingly common one. +// +// It is left folded rather than split unilaterally because DeployRevisionRelation is the deploy +// lane's type and a split changes every consumer of it. The distinction is DECIDABLE and the +// evidence is now in hand rather than discarded upstream -- NoCommonAncestor arrives as its own +// variant. Next-rung trigger: the deploy lane splitting UnrelatedHistories into a diverged arm +// carrying the shared base and an unrelated arm carrying none; this call site consumes the split +// the day it lands, with no new evidence required. Raised to that owner separately. +fn merge_base_relation( + current: GitObjectId, + accepted: GitObjectId, + exit_code: Int, + base_hex: String, + stderr: String, +) -> DeployRevisionRelation { + if git_object_id_eq(left: current, right: accepted) { + SameRevision } else { - AdvanceRefused { - cause: "fleet_main_revision: candidate revision's floor is not green; the desired ref never advances onto an unproven revision (raw-HEAD simultaneous fleet-bricking is the prevented class)", + match merge_base_outcome(exit_code: exit_code, stdout: base_hex, stderr: stderr) { + NoCommonAncestor => UnrelatedHistories + MergeBaseReported { base_hex: hex } => + match git_object_id_from_untagged_hex(hex: hex) { + Present { value: base } => + relation_from_merge_base_oid(current: current, accepted: accepted, base: base) + none => + RelationUnverifiable { + cause: concat("git merge-base succeeded but its output is not a decodable object id: ", hex), + } + } + MergeBaseRefused { exit_code: _, stderr: why } => + RelationUnverifiable { + cause: concat("git merge-base could not answer for this pair: ", why), + } + } + } +} + +// One merge base decides both directions -- a commit is an ancestor of another exactly when it IS +// their merge base -- so no second probe is needed. The three-way ANSWER is not decided here: the +// merge-base facts are projected into the shared classification in gunbc.live_deploy.revision, so +// this module owns an evidence shape and not a policy. Reusing only the five variant names would +// have left two places computing one decision, agreeing today and free to drift apart tomorrow. +fn relation_from_merge_base_oid( + current: GitObjectId, + accepted: GitObjectId, + base: GitObjectId, +) -> DeployRevisionRelation { + revision_relation_from_ancestry_facts( + same: git_object_id_eq(left: current, right: accepted), + deployed_is_ancestor_of_candidate: git_object_id_eq(left: base, right: current), + candidate_is_ancestor_of_deployed: git_object_id_eq(left: base, right: accepted), + ) +} + +type FleetDesiredAdvanceRefusal + = AdvanceExpectationUnavailable { cause: FleetDesiredExpectationRefusal } + | AdvanceHistoriesUnrelated { current: GitObjectId, accepted: GitObjectId } + | AdvanceRelationUnobservable { current: GitObjectId, accepted: GitObjectId, cause: NonEmptyStr } + | InitialFleetDesiredCreationNotAuthorized { accepted: GitObjectId } + | AdvanceRelationIsAboutAnotherPair { + relation_current: GitObjectId, + relation_accepted: GitObjectId, + actual_current: GitObjectId, + actual_accepted: GitObjectId, + } + +// THE INPUT IS A SUM SO THAT IRRELEVANT EVIDENCE CANNOT BE SUPPLIED, LET ALONE FABRICATED. +// +// The decision took (accepted, expectation, relation) unconditionally, and only ONE of the three +// expectation outcomes raises an ancestry question at all: a refused expectation has no current +// revision to compare, and an absent ref has none either. The tell that this was wrong came from +// the fixtures -- the create witness had to construct a same-revision relation purely to satisfy a +// parameter the create arm ignores, and so did both refusal-remedy rows. A fixture that must +// invent a fact to call a function is reporting that the signature admits states the domain does +// not have, and a production caller would have had to invent the same one. +// +// This is the same construction move that removed GitObjectId? from the prior: the impossible +// pairing is ABSENT FROM THE INPUT SPACE rather than rejected after construction. +type FleetDesiredAdvanceInput + = FleetDesiredExpectationRefusedInput { + accepted: AcceptedFleetRevision, + cause: FleetDesiredExpectationRefusal, + } + | FleetDesiredRefAbsentInput { accepted: AcceptedFleetRevision } + | FleetDesiredObservedCurrentInput { + accepted: AcceptedFleetRevision, + current: GitObjectId, + relation: FleetRevisionRelationObservation, } + +// FOUR TERMINAL STATES, AND TWO OF THEM ARE SUCCESSES THAT WRITE NOTHING. +// +// AlreadyConverged and SupersededNoOp are not failures and must not be rendered as operational +// red. A late result for an older revision arriving after a newer one has already been admitted is +// the NORMAL consequence of runs finishing out of order; the desired state is already correct and +// more advanced, so the work is done. Reporting it as a failure trains an operator to ignore the +// channel, which is how a real refusal later goes unread. +// +// THERE IS NO CREATE-ADMITTED ARM, AND ITS ABSENCE IS DELIBERATE RATHER THAN AN OVERSIGHT. An +// earlier revision of this type had one, reached whenever the ref was observed absent. That +// conflated two different propositions: RemoteRefMustBeAbsent is a COMPARE-AND-SWAP PRECONDITION +// -- it proves the ref is not there -- and it says nothing about whether THIS path is authorized +// to bring the fleet's root authority into existence. Absence is a state; creation is a +// capability. Inferring the second from the first is how a workflow that was only ever authorized +// to ADVANCE an existing ref silently acquires the power to mint one. +// +// The live path (gunbc.fleet_desired_admission) refuses first creation today, deliberately, so +// admitting a create here would also have widened live policy under the label "consumer port". +// When first creation is authorized it arrives as its own positive carrier and only the +// CONJUNCTION -- ref observed absent AND creation authorized -- may admit; the arm returns then, +// with a producer, rather than sitting here now with none. +// +// NO `to:` FIELD SITS BESIDE accepted.revision. A second writable name for the target would +// immediately recreate the substitution this cut removed. +type FleetDesiredAdvanceDecision + = FleetDesiredAdvanceAdmitted { + accepted: AcceptedFleetRevision, + expected_prior: GitObjectId, + } + | FleetDesiredAlreadyConverged { accepted: AcceptedFleetRevision } + | FleetDesiredSupersededNoOp { + accepted: AcceptedFleetRevision, + current: GitObjectId, + } + | FleetDesiredAdvanceRefused { cause: FleetDesiredAdvanceRefusal } + +// The lease an admitted advance implies. Derived rather than stored, so the arm and its lease +// cannot drift apart: there is exactly one way to get an expectation out of a decision, and only +// the advance arm has one. +fn fleet_desired_admitted_expectation( + decision: FleetDesiredAdvanceDecision, +) -> GitRemoteRefExpectation? { + match decision { + FleetDesiredAdvanceAdmitted { accepted: _, expected_prior: prior } => + Present { value: RemoteRefMustEqual { oid: prior } } + FleetDesiredAlreadyConverged { accepted: _ } => none + FleetDesiredSupersededNoOp { accepted: _, current: _ } => none + FleetDesiredAdvanceRefused { cause: _ } => none + } +} + +// The typed refusal rendered for a human-facing receipt. Rendering lives beside the cause set so a +// new arm cannot be added without this fold refusing to compile. Consumers that ROUTE still match +// the variants; this is the line an operator reads, never a substitute for the typed cause. +// +// THE UNRELATED ARM SAYS ONLY WHAT ITS CARRIER ESTABLISHES. It used to read "sideways onto a +// DISJOINT history", which is false for the case that actually produces it most of the time: two +// revisions that diverged from a shared ancestor are not disjoint, they have a common past and a +// merge base an operator can name. The carrier behind this arm is the quotient "neither is an +// ancestor of the other", and that is now exactly what the sentence claims. A receipt asserting +// more topology than the observation carries is the same fabrication as a fabricated value; it is +// worse here than in a field, because a human reads THIS line and reaches for the wrong remedy -- +// disjoint says wrong repository, divergent says force-push. When the deploy lane splits the +// variant this arm can say which, and until then it does not guess. +fn fleet_desired_advance_refusal_message(cause: FleetDesiredAdvanceRefusal) -> String { + match cause { + AdvanceExpectationUnavailable { cause: why } => + match why { + FleetDesiredRefUndecodable { advertised: line } => + concat("the desired ref exists but its advertisement is not a decodable object id, so it must not be written over: ", line) + FleetDesiredRefUnobserved { cause: c } => + concat("the desired ref could not be observed, so no expectation licenses a write: ", c) + } + AdvanceHistoriesUnrelated { current: cur, accepted: acc } => + join([ + "neither revision is an ancestor of the other (current ", + git_object_id_wire_hex(oid: cur) as String, + ", accepted ", git_object_id_wire_hex(oid: acc) as String, + ") -- advancing would move the ref sideways", + ], "") + AdvanceRelationUnobservable { current: cur, accepted: acc, cause: c } => + join([ + "the ancestry of ", git_object_id_wire_hex(oid: cur) as String, + " and ", git_object_id_wire_hex(oid: acc) as String, + " could not be established, and an unknown direction is never read as forward: ", c, + ], "") + InitialFleetDesiredCreationNotAuthorized { accepted: acc } => + join([ + "origin advertises no such ref. An absent ref is a STATE and creation is a CAPABILITY: this path is authorized to ADVANCE an existing ref, not to mint the fleet root. Creating it at ", + git_object_id_wire_hex(oid: acc) as String, + " needs a positive mint authority, which no observation of absence can supply", + ], "") + AdvanceRelationIsAboutAnotherPair { + relation_current: rc, + relation_accepted: ra, + actual_current: ac, + actual_accepted: aa, + } => + join([ + "the ancestry evidence compares ", git_object_id_wire_hex(oid: rc) as String, + " with ", git_object_id_wire_hex(oid: ra) as String, + " but the decision is about ", git_object_id_wire_hex(oid: ac) as String, + " and ", git_object_id_wire_hex(oid: aa) as String, + ], "") + } +} + +// AN ABSENT REF DOES NOT AUTHORIZE CREATION, AND THIS GATE RETRACTS gunbc#8746's AUTHORIZATION +// RATHER THAN FAILING TO PORT IT. Declared, because retracting a landed capability silently is +// exactly what §4b(3) forbids. +// +// THE POLICY: absence is a STATE; creation is a CAPABILITY. Observing that origin advertises no +// refs/fleet/desired establishes that nothing is there -- it establishes nothing about who may +// mint the fleet root. Authorizing creation from "absence was observed AND this revision is +// floor-green" makes the ref self-healing in the one case where it must not be: DELETE the ref, +// and the next green main push silently recreates it at whatever happened to land, with no human +// decision anywhere in the loop. That erases the distinction between "the fleet has never been +// initialized" and "someone removed the baseline", which have opposite remedies. +// +// So the admitted decision carries `expected_prior: GitObjectId` and NOT a +// GitRemoteRefExpectation. That is deliberate and is the stronger form: with the narrower +// carrier, an authorized creation has no spelling in this module at all, rather than being a +// representable state some later arm must remember to refuse. +// +// THE HISTORY, because I got this wrong in both directions within one day and the record should +// not read as though the current shape was obvious. This refusal was authored at 07:47 as one of +// three deliberate structural corrections, under the title "creation is not implied by absence". +// gunbc#8746 landed the opposite policy on main at 12:14 -- four and a half hours LATER -- so +// merging main into this branch was a genuine POLICY DIVERGENCE, not a lost port. At 14:00 I +// then "restored" creation here, describing my own considered position as an accidental +// capability regression that a clean merge had silently reverted. That was wrong on the facts: +// nothing was silently reverted, a policy was reversed, and calling a reversal a repair is how a +// decision gets unmade without anyone deciding. +// +// WHAT WOULD MAKE CREATION ADMISSIBLE, stated so this is a bounded retraction and not a +// permanent no: a positive MINT-AUTHORITY carrier -- some fact that says THIS revision may +// establish the fleet root, authored by whoever is entitled to say so, rather than inferred from +// the ref's absence. When that carrier exists, the absent arm consumes it and this refusal +// dissolves. Until then the refusal is the honest answer, and a red witness demanding creation +// is answered by deleting the demand, never by re-adding the authorization. +// +// Raised by nimble-fox-671 relaying side-chat adjudication of both heads, who named the trap +// precisely: a red witness whose correct fix is DELETION looks exactly like one whose correct fix +// is RESTORATION, and only the policy tells them apart. +fn decide_fleet_desired_advance( + input: FleetDesiredAdvanceInput, +) -> FleetDesiredAdvanceDecision { + match input { + FleetDesiredExpectationRefusedInput { accepted: _, cause: c } => + FleetDesiredAdvanceRefused { cause: AdvanceExpectationUnavailable { cause: c } } + FleetDesiredRefAbsentInput { accepted: a } => + FleetDesiredAdvanceRefused { + cause: InitialFleetDesiredCreationNotAuthorized { accepted: a.revision }, + } + FleetDesiredObservedCurrentInput { accepted: a, current: cur, relation: rel } => + decide_against_observed_current(accepted: a, current: cur, relation: rel) + } +} + +// The subject-binding check reads as the precondition it is. A bare relation is not evidence: it +// does not say WHICH TWO revisions were compared, so a relation computed for another pair would +// satisfy a decision about this one. The observation carries both endpoints and this refuses when +// they are not the exact pair under decision -- without that check the binding would be a naming +// convention rather than a wall. +fn decide_against_observed_current( + accepted: AcceptedFleetRevision, + current: GitObjectId, + relation: FleetRevisionRelationObservation, +) -> FleetDesiredAdvanceDecision { + if relation_is_about( + relation_current: relation.current, + relation_accepted: relation.accepted, + actual_current: current, + actual_accepted: accepted.revision, + ) { + classify_admitted_relation(accepted: accepted, current: current, rel: relation.relation) + } else { + FleetDesiredAdvanceRefused { + cause: AdvanceRelationIsAboutAnotherPair { + relation_current: relation.current, + relation_accepted: relation.accepted, + actual_current: current, + actual_accepted: accepted.revision, + }, + } + } +} + +fn relation_is_about( + relation_current: GitObjectId, + relation_accepted: GitObjectId, + actual_current: GitObjectId, + actual_accepted: GitObjectId, +) -> Bool { + git_object_id_eq(left: relation_current, right: actual_current) + && git_object_id_eq(left: relation_accepted, right: actual_accepted) +} + +// The relation vocabulary is reused from gunbc.live_deploy.revision rather than re-coined: the +// question "how do these two revisions relate" is one concept, and a second five-variant enum +// beside it would be the nickname. Its variant names carry the deploy lane's roles, so the mapping +// is stated once here: `deployed` is the CURRENT desired ref, `candidate` is the newly ACCEPTED +// revision. +fn classify_admitted_relation( + accepted: AcceptedFleetRevision, + current: GitObjectId, + rel: DeployRevisionRelation, +) -> FleetDesiredAdvanceDecision { + match rel { + SameRevision => FleetDesiredAlreadyConverged { accepted: accepted } + DeployedIsAncestor => + FleetDesiredAdvanceAdmitted { accepted: accepted, expected_prior: current } + CandidateIsAncestor => + FleetDesiredSupersededNoOp { accepted: accepted, current: current } + UnrelatedHistories => + FleetDesiredAdvanceRefused { + cause: AdvanceHistoriesUnrelated { current: current, accepted: accepted.revision }, + } + RelationUnverifiable { cause: c } => + FleetDesiredAdvanceRefused { + cause: AdvanceRelationUnobservable { + current: current, + accepted: accepted.revision, + cause: c, + }, + } } } diff --git a/dag/gunbc/fleet_revision_acceptance.dag b/dag/gunbc/fleet_revision_acceptance.dag new file mode 100644 index 00000000000..80bafcc000e --- /dev/null +++ b/dag/gunbc/fleet_revision_acceptance.dag @@ -0,0 +1,370 @@ +module gunbc.fleet_revision_acceptance + +import std.types { String, NonEmptyStr, Bool } +import extdeps.git.object_store { GitObjectId, git_object_id_from_untagged_hex, git_object_id_eq, git_object_id_wire_hex } +import extdeps.github.workflow_runs { WorkflowRunConclusion, Success } +import extdeps.github.workflow_run_event { WorkflowRunEvent } +import gunbc.generated_artifact { GeneratedArtifact, WitnessFloorYamlArtifact, artifact_path } +import gunbc.repository { gunbc_repository } +import gunbc.repo_identity { gunbc_default_branch_name } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// WHAT MAKES A REVISION ELIGIBLE TO BECOME THE FLEET'S DESIRED STATE. +// +// The desired ref must never move onto a revision whose floor did not run, and the failure that +// matters is not a red floor -- a red floor is loud and refuses. It is a GREEN floor belonging to +// SOMETHING ELSE: a PR's merge-subject run, a fork's branch, a different workflow in the same +// repository, a run that was cancelled rather than concluded. Each produces a perfectly truthful +// "a workflow run succeeded", and none proves the thing the fleet needs proved. +// +// TWO PROPOSITIONS, TWO PRODUCERS, AND THE SPLIT IS THE POINT. +// +// RequiredCiSucceeded the Required CI contract completed successfully for revision R +// DefaultBranchRevisionObserved revision R entered the default branch +// +// Neither implies the other and they are proved by different facts, so folding them into one +// predicate would let either stand in for the pair. A PR's merge-subject run CAN produce the first +// -- the floor genuinely ran and genuinely passed on that tree, and saying otherwise would be a +// lie about a real result -- and it CANNOT produce the second. That asymmetry is what stops the +// fleet following a revision main never had, and it is only expressible because the two are apart. +// +// THE SCM FACT IS NAMED FOR WHAT THE EVENT CAN ACTUALLY PROVE. A workflow_run envelope carries the +// head branch and the originating event; it does not distinguish a PR merge from a direct +// fast-forward push, an authorized emergency push, or any other mechanism that moved the branch. +// So the carrier is DefaultBranchRevisionObserved and not MergedMainRevisionObserved: naming it +// for merges because merges are the ordinary producer would assert provenance nothing observed. A +// policy that genuinely requires merge origin needs a separate merge authority, and would find +// this carrier honestly insufficient rather than quietly sufficient-looking. +// +// EVERY IDENTITY FACT REFUSES WITH ITS OWN CAUSE. These arms have genuinely different remedies -- +// wrong workflow path means the fleet is reading the wrong producer, wrong repository means +// another repo entirely, a fork's head means an untrusted tree, a non-push event means a PR run +// reached a wall meant for branch history. Collapsing them answers the question nobody asks and +// discards the one an operator acts on. The precedent is deliberate: the floor receipt binds a +// receipt to its run through three distinct mismatch arms and refuses to project a Bool over them +// (gunbc.floor_component_receipt_document, its no-Bool-projection row). + +// The Required CI contract's IDENTITY -- which contract completed, not what it did internally. +// The fleet policy asks whether the exact contract succeeded for the exact revision; it does not +// own the contract's phase roster, and must not encode one. A `phases_run == 6` field would make +// every phase added to the floor a breaking change to fleet admission, which is backwards: the +// roster is the contract's own business and its evidence, not the fleet's precondition. +type RequiredCiContractIdentity { + workflow_path: String + repository_full_name: String +} + +fn required_ci_contract() -> RequiredCiContractIdentity { + RequiredCiContractIdentity { + workflow_path: artifact_path(a: WitnessFloorYamlArtifact), + repository_full_name: fleet_repository_full_name(), + } +} + +// NEITHER OF THESE IS THIS MODULE'S FACT, AND BOTH WERE SPELLED HERE AS LITERALS. +// +// `fleet_repository_full_name = "gunb-ai/gunbc"` and `fleet_default_branch = "main"` were the +// sixth and seventh nicknames for facts that already have authorities. gunbc.repository exists +// precisely because five spellings of this repository's identity had accumulated across the tree, +// and its own note says the answer to five nicknames is not a sixth. gunbc.repo_identity owns the +// default-branch name and has a perturbation oracle that moves every consumer when it changes -- +// a literal here is invisible to that oracle, which is what makes this class stay hidden: every +// individual literal looks obviously correct. +// +// OBSERVED WHILE DOING THIS, and flagged rather than silently resolved: `gunbc_repository` also +// carries a `default_branch` field, so the default branch appears to have two homes. They agree +// today. The branch name is read from gunbc.repo_identity here because that module's note claims +// the authority for branch facts explicitly and carries the perturbation oracle, while +// Repository.default_branch is part of the upstream API shape this project instantiates. Whether +// those should be one row is a real question and not this cut's to settle. +fn fleet_repository_full_name() -> String { + gunbc_repository.full_name +} + +fn fleet_default_branch() -> String { + gunbc_default_branch_name +} + +// THESE TWO ARE AN UNDECLARED SUM AND THE CLASS IS THE ONE THIS BRANCH CLOSED ONE LAYER DOWN, +// so it is named here rather than left for the next reader to notice the inconsistency. Comparing +// a wire string with `==` against a local `data` row is exactly what `merge_base_exit_ok: Int = 0` +// was doing to git's exit table before extdeps.git.inspect grew MergeBaseOutcome (raised in +// review 54424, which spotted the parallel). +// +// THE TWO HALVES ARE NOT THE SAME PROBLEM, though, and that distinction is why neither is fixed by +// reflex here. `activity` is a CLOSED vocabulary upstream documents exhaustively -- requested, +// in_progress, completed -- so it is genuinely a coproduct waiting to be written, and it belongs in +// extdeps.github.workflow_run_event beside the envelope that decodes it, not in this consumer. +// `originating_event` is NOT closed: it is the whole GitHub event namespace, open-ended and +// extended by upstream without notice, so a closed sum over it would be re-coining an open +// vocabulary -- the §3 nickname wearing a coproduct. Its honest shape is the documented members +// this repository actually discriminates plus an explicit unrecognized arm carrying the wire text, +// which is a different modeling decision than the first and should be made as one. +// +// NEXT-RUNG TRIGGER: a WorkflowRunActivity coproduct on extdeps.github.workflow_run_event, decoded +// where the envelope is already parsed, at which point these two rows and both `!=` comparisons +// below dissolve into exhaustive matches. RUNG until then: mitigatable -- a wire-value drift is +// caught, because both comparisons FAIL CLOSED into a typed refusal naming the observed string +// (CiActivityNotCompleted, BranchEventIsNotAPush) rather than admitting. What is unprotected is the +// opposite direction: a typo in these rows refuses everything forever, and nothing here would say +// which of the two it was. +// +// NOT AN ADMISSION. Recording a trigger does not authorize the shape; it is deferred because typing +// the envelope changes an extdeps carrier and its decoder, which is a different change from this +// branch's, and the deferral is stated so a reader can hold me to it rather than discover it. +data required_ci_completed_activity: String = "completed" + +data default_branch_originating_event: String = "push" + +// EVIDENCE IS A TYPE PARAMETER, NOT A VARIANT. GitHub is the first provider of both propositions +// and will not be the last -- an accepted fabric receipt proves the same Required CI proposition +// through a different channel. Putting `GitHub | Fabric` inside the positive carrier would make +// every consumer match on a provenance it has no business branching on, and would make adding a +// provider an edit to the admission carrier. Two provider bindings constructing the SAME type is +// the §2 move: one concept, N realizations, dispatch at the periphery. +type RequiredCiSucceeded { + revision: GitObjectId + contract: RequiredCiContractIdentity + evidence: E +} + +type DefaultBranchRevisionObserved { + revision: GitObjectId + branch: String + evidence: M +} + +type RequiredCiRefusal + = CiWorkflowNotTheRequiredFloor { observed_path: String, required_path: String } + | CiRepositoryNotThisRepository { observed: String, required: String } + | CiHeadRepositoryNotThisRepository { observed: String, required: String } + | CiActivityNotCompleted { observed: String } + | CiConclusionNotSuccess { observed: WorkflowRunConclusion } + | CiHeadShaUndecodable { observed: String } + +type RequiredCiAdmission + = RequiredCiAdmitted { succeeded: RequiredCiSucceeded } + | RequiredCiRefused { cause: RequiredCiRefusal } + +type DefaultBranchRefusal + = BranchIsNotTheDefaultBranch { observed: String, required: String } + | BranchEventIsNotAPush { observed: String } + | BranchRepositoryNotThisRepository { observed: String, required: String } + | BranchHeadRepositoryNotThisRepository { observed: String, required: String } + | BranchHeadShaUndecodable { observed: String } + +type DefaultBranchAdmission + = DefaultBranchAdmitted { observed: DefaultBranchRevisionObserved } + | DefaultBranchRefused { cause: DefaultBranchRefusal } + +// THE REVISION IS DECODED ONCE, HERE, AND CARRIED AS ONE CANONICAL IDENTITY. The event's head_sha +// is a non-empty string that GitHub says is a SHA; nothing on the wire establishes it as a Git +// object id. Decoding at the binding boundary means an undecodable value refuses BEFORE any +// positive carrier exists, so no downstream consumer can be handed a revision that is not one. +// Carrying both an authored CommitSha and a decoded GitObjectId downstream would be two writable +// names for one fact -- the §3 fork -- and the two could then disagree. +type RevisionDecode + = RevisionDecoded { revision: GitObjectId } + | RevisionUndecodable { observed: String } + +fn decode_event_revision(event: WorkflowRunEvent) -> RevisionDecode { + match git_object_id_from_untagged_hex(hex: event.head_sha as String) { + Present { value: oid } => RevisionDecoded { revision: oid } + none => RevisionUndecodable { observed: event.head_sha as String } + } +} + +// ORDERING: identity before outcome. A successful run of the WRONG workflow refuses as the wrong +// workflow, and so does a FAILED run of the wrong workflow. Checking the conclusion first would +// report "the floor was not green" about a run that was never the floor, sending a reader to +// investigate a failure that does not exist. The order asserts what the run IS before how it WENT. +// +// NOTE WHAT IS NOT CHECKED HERE: the branch and the originating event. This producer answers only +// "did the Required CI contract succeed for this revision", which is true of a PR's merge-subject +// run. The branch facts belong to the other proposition and are checked by its own producer. +fn accept_required_ci_workflow_run(event: WorkflowRunEvent, evidence: E) -> RequiredCiAdmission { + if event.workflow_path != artifact_path(a: WitnessFloorYamlArtifact) { + RequiredCiRefused { + cause: CiWorkflowNotTheRequiredFloor { + observed_path: event.workflow_path, + required_path: artifact_path(a: WitnessFloorYamlArtifact), + }, + } + } else { + if event.repository_full_name != fleet_repository_full_name() { + RequiredCiRefused { + cause: CiRepositoryNotThisRepository { + observed: event.repository_full_name, + required: fleet_repository_full_name(), + }, + } + } else { + if event.head_repository_full_name != fleet_repository_full_name() { + RequiredCiRefused { + cause: CiHeadRepositoryNotThisRepository { + observed: event.head_repository_full_name, + required: fleet_repository_full_name(), + }, + } + } else { + if event.activity != required_ci_completed_activity { + RequiredCiRefused { cause: CiActivityNotCompleted { observed: event.activity } } + } else { + match event.conclusion { + Success => + match decode_event_revision(event: event) { + RevisionDecoded { revision: oid } => + RequiredCiAdmitted { + succeeded: RequiredCiSucceeded { + revision: oid, + contract: required_ci_contract(), + evidence: evidence, + }, + } + RevisionUndecodable { observed: raw } => + RequiredCiRefused { cause: CiHeadShaUndecodable { observed: raw } } + } + other => RequiredCiRefused { cause: CiConclusionNotSuccess { observed: other } } + } + } + } + } + } +} + +// The SCM proposition: this revision entered the default branch. Repository identity is re-checked +// here rather than inherited from the CI producer, because the two propositions are independent by +// construction and a producer that trusted its sibling's checks would silently couple them -- the +// pair would then be as strong as whichever was called first, which is not a property anyone +// declared. +fn observe_default_branch_revision(event: WorkflowRunEvent, evidence: M) -> DefaultBranchAdmission { + if event.repository_full_name != fleet_repository_full_name() { + DefaultBranchRefused { + cause: BranchRepositoryNotThisRepository { + observed: event.repository_full_name, + required: fleet_repository_full_name(), + }, + } + } else { + if event.head_repository_full_name != fleet_repository_full_name() { + DefaultBranchRefused { + cause: BranchHeadRepositoryNotThisRepository { + observed: event.head_repository_full_name, + required: fleet_repository_full_name(), + }, + } + } else { + if event.originating_event != default_branch_originating_event { + DefaultBranchRefused { cause: BranchEventIsNotAPush { observed: event.originating_event } } + } else { + if event.head_branch != fleet_default_branch() { + DefaultBranchRefused { + cause: BranchIsNotTheDefaultBranch { + observed: event.head_branch, + required: fleet_default_branch(), + }, + } + } else { + match decode_event_revision(event: event) { + RevisionDecoded { revision: oid } => + DefaultBranchAdmitted { + observed: DefaultBranchRevisionObserved { + revision: oid, + branch: event.head_branch, + evidence: evidence, + }, + } + RevisionUndecodable { observed: raw } => + DefaultBranchRefused { cause: BranchHeadShaUndecodable { observed: raw } } + } + } + } + } + } +} + +// THE TYPED REFUSALS RENDERED FOR A HUMAN-FACING RECEIPT. Rendering lives beside each cause set so +// a new refusal arm cannot be added without these folds refusing to compile -- the message set and +// the cause set stay one authority. Consumers that ROUTE still match the variants; these are for +// the line an operator reads, never a substitute for the typed cause. +fn required_ci_refusal_message(cause: RequiredCiRefusal) -> String { + match cause { + CiWorkflowNotTheRequiredFloor { observed_path: p, required_path: q } => + join(["the run belongs to workflow ", p, ", not the required floor (", q, ")"], "") + CiRepositoryNotThisRepository { observed: o, required: r } => + join(["the run belongs to repository ", o, ", not ", r], "") + CiHeadRepositoryNotThisRepository { observed: o, required: r } => + join(["the run's head repository is ", o, ", not ", r, " -- a fork's run never admits a fleet revision"], "") + CiActivityNotCompleted { observed: o } => + concat("the workflow_run activity is not completed: ", o) + CiConclusionNotSuccess { observed: _ } => + "the required floor did not conclude Success, so the revision is unproven and the desired ref never advances onto it" + CiHeadShaUndecodable { observed: raw } => + concat("the run's head_sha is not a decodable object id: ", raw) + } +} + +fn default_branch_refusal_message(cause: DefaultBranchRefusal) -> String { + match cause { + BranchIsNotTheDefaultBranch { observed: o, required: r } => + join(["the run is on branch ", o, ", not ", r, " -- only the default branch admits a fleet revision"], "") + BranchEventIsNotAPush { observed: o } => + join([ + "the run originated from ", o, + ", not a push -- a pull-request run proves the floor passed on its tree and proves nothing about the default branch", + ], "") + BranchRepositoryNotThisRepository { observed: o, required: r } => + join(["the run belongs to repository ", o, ", not ", r], "") + BranchHeadRepositoryNotThisRepository { observed: o, required: r } => + join(["the run's head repository is ", o, ", not ", r], "") + BranchHeadShaUndecodable { observed: raw } => + concat("the run's head_sha is not a decodable object id: ", raw) + } +} + +// THE SOLE JOIN. Downstream, only AcceptedFleetRevision.revision exists -- there is no candidate +// left beside it to compare against or accidentally substitute. The join takes the two POSITIVE +// carriers, not the two admissions, so a refused producer cannot reach it at all: the caller must +// have matched out a success on both sides before it can even ask. +// +// THE MISMATCH ARM IS LOAD-BEARING. Required CI proving revision A and the default branch carrying +// revision B is not a contradiction in the data -- both facts can be perfectly true, about +// different revisions, and arrive together whenever a push lands while a run is in flight. What is +// false is the CONJUNCTION anyone would infer from holding both. It refuses, carrying both +// revisions, because "which two" is the entire content of the finding. +type AcceptedFleetRevision { + revision: GitObjectId + required_ci_contract: RequiredCiContractIdentity + required_ci_evidence: E + default_branch_evidence: M +} + +type FleetRevisionAdmission + = FleetRevisionAccepted { accepted: AcceptedFleetRevision } + | RequiredCiAndDefaultBranchRevisionMismatch { + required_ci_revision: GitObjectId, + default_branch_revision: GitObjectId, + } + +fn admit_fleet_revision( + required_ci: RequiredCiSucceeded, + default_branch: DefaultBranchRevisionObserved, +) -> FleetRevisionAdmission { + if git_object_id_eq(left: required_ci.revision, right: default_branch.revision) { + FleetRevisionAccepted { + accepted: AcceptedFleetRevision { + revision: required_ci.revision, + required_ci_contract: required_ci.contract, + required_ci_evidence: required_ci.evidence, + default_branch_evidence: default_branch.evidence, + }, + } + } else { + RequiredCiAndDefaultBranchRevisionMismatch { + required_ci_revision: required_ci.revision, + default_branch_revision: default_branch.revision, + } + } +} diff --git a/dag/gunbc/live_deploy/revision.dag b/dag/gunbc/live_deploy/revision.dag index 4207520c8ad..cb8b2b882a4 100644 --- a/dag/gunbc/live_deploy/revision.dag +++ b/dag/gunbc/live_deploy/revision.dag @@ -81,13 +81,24 @@ fn deploy_revision_refuses(verdict: DeployRevisionVerdict) -> Bool { data deploy_revision_probe_relation_note: String = "The (deployed→candidate, candidate→deployed) probe pair folded into a relation. SHA equality is checked first and short-circuits both probes. Note that (true,true) is reachable ONLY when the SHAs are equal — a commit is its own ancestor and ancestry is antisymmetric — so this arm is defensive rather than expected, and it agrees with the equality short-circuit instead of contradicting it." -fn deploy_revision_relation_from_probes( - deployed: CommitSha, - candidate: CommitSha, +// THE CLASSIFICATION IS ONE AUTHORITY WITH TWO EVIDENCE REALIZATIONS. +// +// This body was reachable only through the probe-pair projection below, which meant a second +// evidence shape -- a single merge-base object, which decides both directions at once -- had to +// re-derive the same three-way answer to use it. That is the §3 fork in its quietest form: not two +// names for one concept, but two places computing one decision, agreeing today and free to drift +// apart tomorrow. A later correction to either would leave two different meanings of +// CandidateIsAncestor with nothing to notice. +// +// So the decision takes ANCESTRY FACTS and the evidence shapes project into it: two directional +// probes here, one merge-base object in gunbc.fleet_main_revision. Reusing the five variant names +// was never enough -- the vocabulary was shared while the policy was copied. +fn revision_relation_from_ancestry_facts( + same: Bool, deployed_is_ancestor_of_candidate: Bool, candidate_is_ancestor_of_deployed: Bool, ) -> DeployRevisionRelation { - if deployed == candidate { + if same { SameRevision } else { if deployed_is_ancestor_of_candidate { @@ -98,6 +109,19 @@ fn deploy_revision_relation_from_probes( } } +fn deploy_revision_relation_from_probes( + deployed: CommitSha, + candidate: CommitSha, + deployed_is_ancestor_of_candidate: Bool, + candidate_is_ancestor_of_deployed: Bool, +) -> DeployRevisionRelation { + revision_relation_from_ancestry_facts( + same: deployed == candidate, + deployed_is_ancestor_of_candidate: deployed_is_ancestor_of_candidate, + candidate_is_ancestor_of_deployed: candidate_is_ancestor_of_deployed, + ) +} + data deploy_revision_persisted_outside_tree_note: String = "The deployed-revision record lives OUTSIDE the directory the deploy rsyncs into, and that placement is load-bearing rather than tidy. A marker inside the deployed tree is destroyed or overwritten by the very rsync whose outcome it is supposed to describe, so after a partial or interrupted deploy the record would describe a tree that was never fully written — the state the guard exists to detect becomes the state it cannot see. Keeping it beside the destination instead means the record is written ONLY after the service has restarted and the deployed surface has been read back, so a crash mid-deploy leaves the previous revision recorded and the next run correctly classifies the incomplete tree as still-at-the-old-revision rather than trusting a marker the failed run had already advanced." fn deploy_revision_state_path(target: DeployTargetId) -> FilePath { diff --git a/dag/gunbc/roadmap_acceptance_history_observation.dag b/dag/gunbc/roadmap_acceptance_history_observation.dag index 98fc01b7e95..ea0087b4c98 100644 --- a/dag/gunbc/roadmap_acceptance_history_observation.dag +++ b/dag/gunbc/roadmap_acceptance_history_observation.dag @@ -31,6 +31,10 @@ import std.content_hash { content_hash_atom, content_hash_eq_structural, Fnv1a64 import std.types { CommitSha, GitRef, Int, String } import v2.std.collection { List } +data roadmap_acceptance_history_repository_path: String = "." + +data roadmap_acceptance_history_repository_path_note: String = "The repository this observation inspects. Declared rather than ambient, for the reason git.Inspect.MergeBase now requires it: an ambient repository makes a right answer and a wrong one indistinguishable, because two checkouts can hold refs that look identical." + data roadmap_acceptance_history_authority_repo_path: String = "dag/gunbc/roadmap_authority.dag" data roadmap_acceptance_history_prior_history_next_rung_trigger: String = "DISSOLVED: merge-base prior_history parses dag/gunbc/roadmap_acceptance_event_history.jsonl via gunbc.roadmap_acceptance_history_carrier when the carrier exists at merge-base; when absent (carrier introduction on main) the typed bootstrap projects inline authority history via gunbc.roadmap_acceptance_history_projection. A changed carrier without a valid merge-base observation refuses AcceptanceHistoryIntegrityRefusedPriorHistoryObservation — never prior_history = []. git_show_path_absent_at_ref substring-matches both git stderr shapes for path absent at ref (tree miss: does not exist in; worktree-present-but-not-in-commit: exists on disk, but not in) until extdeps.git carries a typed path-absent-at-ref disposition. Remaining dissolve-on: delete both seed bridges when a modeled revision-addressed carrier ingest lands." @@ -112,6 +116,7 @@ fn observe_roadmap_acceptance_history_prior( } else { let revision = head.sha as String let baseline = git.Inspect.MergeBase( + repository_path: roadmap_acceptance_history_repository_path, left: revision as GitRef, right: base_ref as GitRef, expect: ExpectSuccess, diff --git a/dag/gunbc/stage0_rust_host_observation.dag b/dag/gunbc/stage0_rust_host_observation.dag index fcb3bce278d..f481f69ac92 100644 --- a/dag/gunbc/stage0_rust_host_observation.dag +++ b/dag/gunbc/stage0_rust_host_observation.dag @@ -27,6 +27,10 @@ import std.types { CommitSha, GitRef, String } import v2.std.algebra { fold_list, length, list_map, list_snoc_item } import v2.std.collection { List } +data stage0_rust_observation_repository_path: String = "." + +data stage0_rust_observation_repository_path_note: String = "The repository this observation inspects. Declared rather than ambient: git.Inspect.MergeBase names its repository (see that operation), so this fact is authored and visible even though production runs from the root. A `.` that is written down can be reviewed and changed; a `.` that is merely where the process happened to start cannot." + data stage0_rust_host_observation_note: String = "Rust-source OBSERVATION prerequisite only; lifecycle totality remains downstream in gunbc.stage0_rust_source_lifecycle_scaffold / v1-honest-frontier. extdeps.git owns the Git operation shapes. This module supplies repository policy (HEAD versus gunbc_merge_target_ref), filters the exact revision-addressed path population, normalizes authored Cargo target paths, hashes the exact manifest text through std.content_hash, and joins those facts. The temporary Rust seed owns only TOML decoding into CargoManifestBinParse plus its interpreter projection. CargoBin is a source role and cannot satisfy a maintenance disposition." // WHAT THE EMITTER DECLARED IT PRODUCED, AS AN OBSERVED FACT RATHER THAN A RECONSTRUCTION. @@ -230,6 +234,7 @@ fn observe_stage0_rust_sources( } else { let revision = head.sha as String let baseline = git.Inspect.MergeBase( + repository_path: stage0_rust_observation_repository_path, left: revision as GitRef, right: base_ref as GitRef, expect: ExpectSuccess diff --git a/dag/test/claim/fleet_desired_admission_witness_test.dag b/dag/test/claim/fleet_desired_admission_witness_test.dag index 2d9637b1ad3..c6c527b8215 100644 --- a/dag/test/claim/fleet_desired_admission_witness_test.dag +++ b/dag/test/claim/fleet_desired_admission_witness_test.dag @@ -8,19 +8,25 @@ import extdeps.github.workflow_runs { import extdeps.github.workflow_run_event { WorkflowRunEvent } import gunbc.witness_floor_workflow { witness_floor_workflow_name } import gunbc.repo_identity { gunbc_default_branch_name } -import extdeps.git.publication_transport { - GitRemoteRefExpectation, RemoteRefMustBeAbsent, RemoteRefMustEqual, -} +import gunbc.fleet_revision_acceptance { AcceptedFleetRevision } import gunbc.fleet_main_revision { - FleetDesiredRevision, FleetDesiredAdmitted, FleetDesiredAbsent, - FleetDesiredUndecodable, FleetDesiredUnobserved, + DeployRevisionRelation, SameRevision, DeployedIsAncestor, CandidateIsAncestor, + FleetRevisionRelationObservation, + FleetDesiredAdvanceInput, + FleetDesiredExpectationRefusedInput, FleetDesiredRefAbsentInput, FleetDesiredObservedCurrentInput, + FleetDesiredRefUnobserved, + FleetDesiredRefUndecodable, + decide_fleet_desired_advance, } import gunbc.fleet_desired_admission { - FleetDesiredAdmissionOutcome, AdmissionAdvanceAuthorized, AdmissionRefused, - fleet_desired_admission_decide, - fleet_desired_floor_green, - fleet_desired_authorized_push_script, - fleet_desired_admission_authorized_push_path, + FleetDesiredAdmissionOutcome, AdmissionActionAuthorized, AdmissionRefused, + FleetDesiredAuthorizedAction, + FleetDesiredRemoteAdvance, FleetDesiredAlreadyConvergedAction, FleetDesiredSupersededAction, + FleetDesiredAcceptedRevision, FleetDesiredRevisionAccepted, FleetDesiredRevisionRefused, + fleet_desired_accepted_from_event, + fleet_desired_action_from_decision, + fleet_desired_authorized_action_script, + fleet_desired_admission_authorized_action_path, } import gunbc.fleet_desired_admission_workflow { expected_fleet_desired_yml } @@ -35,24 +41,20 @@ fn fixture_oid(hex: String) -> GitObjectId { } } -fn fixture_prior() -> FleetDesiredRevision { - FleetDesiredAdmitted { revision: fixture_oid(hex: fixture_prior_hex) } -} - -fn fixture_event(workflow_name: String, conclusion: WorkflowRunConclusion, branch: String, head_repo: String, activity: String) -> WorkflowRunEvent { +fn fixture_event(workflow_name: String, conclusion: WorkflowRunConclusion, branch: String, head_repo: String, activity: String, workflow_path: String, originating: String) -> WorkflowRunEvent { WorkflowRunEvent { activity: activity, run_id: "1" as NonEmptyStr, workflow_name: workflow_name, workflow_id: "2" as NonEmptyStr, - workflow_path: ".github/workflows/witnesses.yml", + workflow_path: workflow_path, conclusion: conclusion, html_url: "https://example.invalid/run" as NonEmptyStr, run_started_at: "2026-08-20T00:00:00Z" as NonEmptyStr, head_sha: fixture_candidate_hex as CommitSha, head_branch: branch, head_repository_full_name: head_repo, - originating_event: "push", + originating_event: originating, repository_full_name: fixture_repo, } } @@ -64,222 +66,338 @@ fn admitting_event() -> WorkflowRunEvent { branch: gunbc_default_branch_name, head_repo: fixture_repo, activity: "completed", + workflow_path: ".github/workflows/witnesses.yml", + originating: "push", ) } -fn decided(event: WorkflowRunEvent, observed: FleetDesiredRevision) -> FleetDesiredAdmissionOutcome { - fleet_desired_admission_decide(event: event, observed: observed) -} - -fn is_refused(o: FleetDesiredAdmissionOutcome) -> Bool { +fn is_event_refused(o: FleetDesiredAcceptedRevision) -> Bool { match o { - AdmissionRefused { cause: _ } => true - AdmissionAdvanceAuthorized { expected: _, to: _ } => false - } -} - -fn expectation_is_prior(expected: GitRemoteRefExpectation, hex: String) -> Bool { - match expected { - RemoteRefMustEqual { oid: prior } => git_object_id_wire_hex(oid: prior) as String == hex - RemoteRefMustBeAbsent => false - } -} - -fn expectation_is_absent(expected: GitRemoteRefExpectation) -> Bool { - match expected { - RemoteRefMustBeAbsent => true - RemoteRefMustEqual { oid: _ } => false + FleetDesiredRevisionRefused { cause: _ } => true + FleetDesiredRevisionAccepted { accepted: _ } => false } } // THE POSITIVE CONTROL. Every refusal claim below removes exactly one fact from THIS event, so a -// refusal that fired for an unrelated reason would show up here as a failure to admit at all. -test fn a_floor_green_default_branch_run_admits_the_candidate() -> Bool { - match decided(event: admitting_event(), observed: fixture_prior()) { - AdmissionRefused { cause: _ } => false - AdmissionAdvanceAuthorized { expected: e, to: t } => - expectation_is_prior(expected: e, hex: fixture_prior_hex) - && (git_object_id_wire_hex(oid: t) as String == fixture_candidate_hex) +// refusal that fired for an unrelated reason would show up here as a failure to accept at all. +// It also pins the revision, because an acceptance naming the wrong one would advance the fleet +// to something the floor never proved. +test fn a_floor_green_default_branch_run_accepts_the_candidate_revision() -> Bool { + match fleet_desired_accepted_from_event(event: admitting_event()) { + FleetDesiredRevisionRefused { cause: _ } => false + FleetDesiredRevisionAccepted { accepted: a } => + git_object_id_wire_hex(oid: a.revision) as String == fixture_candidate_hex } } -// THE OTHER WRITE THE AUTHORITY ADMITS, and the one this gate could not express at all until the -// outcome stopped carrying a bare prior oid. An origin that advertises no such ref is an ANSWER -// about the remote, so first creation is authorized — and it is authorized as a compare-and-swap -// expecting absence, never as an unconditional push. -test fn an_absent_desired_ref_authorizes_a_creation_expecting_absence() -> Bool { - match decided(event: admitting_event(), observed: FleetDesiredAbsent) { - AdmissionRefused { cause: _ } => false - AdmissionAdvanceAuthorized { expected: e, to: t } => - expectation_is_absent(expected: e) - && (git_object_id_wire_hex(oid: t) as String == fixture_candidate_hex) - } -} - -// THE DISCRIMINATING RED FOR THE ARM THAT DID NOT EXIST. An undecodable advertisement means the -// ref EXISTS holding something unreadable; a write would destroy it and a retry will not fix it. -// The claim pins the remedy-bearing wording so this cannot be satisfied by the unobserved arm's -// cause — the two refusals must stay distinguishable, which is why the authority kept them apart. +// AN UNDECODABLE ADVERTISEMENT REFUSES WITHOUT WRITING OVER THE REF, and this row is PORTED from +// main rather than dropped with the vocabulary it was written against. It arrived here through a +// clean auto-merge -- no conflict marker -- still spelled in main's deleted `decided` / +// AdmissionAdvanceAuthorized terms, so it would not have compiled; the tempting resolution was to +// delete it with its siblings. But the CLAIM is real and this branch had no equivalent, and a +// replacement that quietly drops a refusal has erased a correctness distinction rather than +// completed a migration. +// +// The claim: the ref EXISTS holding something unreadable, so a write would destroy it and a retry +// will not fix it. The assertion pins the remedy-bearing wording AND denies the unobserved arm's, +// because the two refusals must stay distinguishable -- an operator repairs a corrupt ref and +// retries an unreachable one. Wording follows THIS branch's authority +// (gunbc.fleet_main_revision fleet_desired_advance_refusal_message), not main's, since porting a +// claim means re-asserting it against the live message rather than copying a string that no +// longer exists. test fn an_undecodable_desired_ref_refuses_without_writing_over_it() -> Bool { - match decided( - event: admitting_event(), - observed: FleetDesiredUndecodable { advertised: "not-a-sha refs/fleet/desired" }, - ) { - AdmissionAdvanceAuthorized { expected: _, to: _ } => false + match action_for(input: FleetDesiredExpectationRefusedInput { + accepted: accepted_fixture(), + cause: FleetDesiredRefUndecodable { advertised: "not-a-sha refs/fleet/desired" }, + }) { + AdmissionActionAuthorized { action: _ } => false AdmissionRefused { cause: c } => - string_contains(s: c, pattern: "a write would destroy it") + string_contains(s: c, pattern: "must not be written over") && string_contains(s: c, pattern: "not-a-sha refs/fleet/desired") - && !string_contains(s: c, pattern: "never read as an absent one") + && !string_contains(s: c, pattern: "could not be observed") } } // THE KEYSTONE. This is the defect the emitted deploy.yml carried: a candidate whose floor is not -// green was advanced anyway. The refusal must come from the modeled authority, so the claim pins -// the authority's own prevented-class wording rather than merely observing that something refused. -test fn a_floor_red_candidate_is_refused_by_the_modeled_authority() -> Bool { - match decided( - event: fixture_event( - workflow_name: witness_floor_workflow_name, - conclusion: Failure, - branch: gunbc_default_branch_name, - head_repo: fixture_repo, - activity: "completed", - ), - observed: fixture_prior(), - ) { - AdmissionAdvanceAuthorized { expected: _, to: _ } => false - AdmissionRefused { cause: c } => - string_contains(s: c, pattern: "raw-HEAD simultaneous fleet-bricking") - && string_contains(s: c, pattern: "failure") - } +// green was advanced anyway. Every non-Success conclusion is red -- Cancelled and Skipped are the +// two that most invite a "close enough" arm, since a cancelled floor proves nothing and a skipped +// one ran nothing. Enumerated rather than sampled, because the arm that admits one of these is +// exactly the arm that never fires in testing. +fn accepted_with_conclusion(conclusion: WorkflowRunConclusion) -> Bool { + !is_event_refused(o: fleet_desired_accepted_from_event(event: fixture_event( + workflow_name: witness_floor_workflow_name, + conclusion: conclusion, + branch: gunbc_default_branch_name, + head_repo: fixture_repo, + activity: "completed", + workflow_path: ".github/workflows/witnesses.yml", + originating: "push", + ))) } -// Every non-Success conclusion is red. Cancelled and Skipped are the two that most invite a -// "close enough" arm — a cancelled floor proves nothing and a skipped one ran nothing. -test fn only_success_is_floor_green() -> Bool { - fleet_desired_floor_green(conclusion: Success) - && !fleet_desired_floor_green(conclusion: Failure) - && !fleet_desired_floor_green(conclusion: Cancelled) - && !fleet_desired_floor_green(conclusion: Skipped) - && !fleet_desired_floor_green(conclusion: TimedOut) - && !fleet_desired_floor_green(conclusion: Neutral) - && !fleet_desired_floor_green(conclusion: ActionRequired) - && !fleet_desired_floor_green(conclusion: StartupFailure) -} - -test fn a_conclusion_from_another_workflow_is_refused() -> Bool { - is_refused(o: decided( - event: fixture_event( - workflow_name: "deploy", - conclusion: Success, - branch: gunbc_default_branch_name, - head_repo: fixture_repo, - activity: "completed", - ), - observed: fixture_prior(), - )) +test fn only_a_success_conclusion_is_accepted() -> Bool { + accepted_with_conclusion(conclusion: Success) + && !accepted_with_conclusion(conclusion: Failure) + && !accepted_with_conclusion(conclusion: Cancelled) + && !accepted_with_conclusion(conclusion: Skipped) + && !accepted_with_conclusion(conclusion: TimedOut) + && !accepted_with_conclusion(conclusion: Neutral) + && !accepted_with_conclusion(conclusion: ActionRequired) + && !accepted_with_conclusion(conclusion: StartupFailure) +} + +// The floor is identified by PATH, not by name. A workflow that renames itself "witnesses" does +// not become the floor, and the old wall -- which matched on the name -- would have admitted it. +test fn a_run_of_another_workflow_path_is_refused() -> Bool { + is_event_refused(o: fleet_desired_accepted_from_event(event: fixture_event( + workflow_name: witness_floor_workflow_name, + conclusion: Success, + branch: gunbc_default_branch_name, + head_repo: fixture_repo, + activity: "completed", + workflow_path: ".github/workflows/deploy.yml", + originating: "push", + ))) } test fn a_non_default_branch_run_is_refused() -> Bool { - is_refused(o: decided( - event: fixture_event( - workflow_name: witness_floor_workflow_name, - conclusion: Success, - branch: "session/nimble-fox-671", - head_repo: fixture_repo, - activity: "completed", - ), - observed: fixture_prior(), - )) + is_event_refused(o: fleet_desired_accepted_from_event(event: fixture_event( + workflow_name: witness_floor_workflow_name, + conclusion: Success, + branch: "session/nimble-fox-671", + head_repo: fixture_repo, + activity: "completed", + workflow_path: ".github/workflows/witnesses.yml", + originating: "push", + ))) } test fn a_fork_head_repository_is_refused() -> Bool { - is_refused(o: decided( - event: fixture_event( - workflow_name: witness_floor_workflow_name, - conclusion: Success, - branch: gunbc_default_branch_name, - head_repo: "someone-else/gunbc", - activity: "completed", - ), - observed: fixture_prior(), - )) + is_event_refused(o: fleet_desired_accepted_from_event(event: fixture_event( + workflow_name: witness_floor_workflow_name, + conclusion: Success, + branch: gunbc_default_branch_name, + head_repo: "someone-else/gunbc", + activity: "completed", + workflow_path: ".github/workflows/witnesses.yml", + originating: "push", + ))) } test fn an_incomplete_activity_is_refused() -> Bool { - is_refused(o: decided( - event: fixture_event( - workflow_name: witness_floor_workflow_name, - conclusion: Success, - branch: gunbc_default_branch_name, - head_repo: fixture_repo, - activity: "requested", - ), - observed: fixture_prior(), - )) + is_event_refused(o: fleet_desired_accepted_from_event(event: fixture_event( + workflow_name: witness_floor_workflow_name, + conclusion: Success, + branch: gunbc_default_branch_name, + head_repo: fixture_repo, + activity: "requested", + workflow_path: ".github/workflows/witnesses.yml", + originating: "push", + ))) +} + +// A refusal the OLD wall did not make at all. A floor run triggered by anything but a push to the +// default branch -- a manual dispatch, a schedule -- proves the floor green for a tree that was +// never merged, so its head_sha is not a landed revision. +test fn a_non_push_originating_event_is_refused() -> Bool { + is_event_refused(o: fleet_desired_accepted_from_event(event: fixture_event( + workflow_name: witness_floor_workflow_name, + conclusion: Success, + branch: gunbc_default_branch_name, + head_repo: fixture_repo, + activity: "completed", + workflow_path: ".github/workflows/witnesses.yml", + originating: "workflow_dispatch", + ))) +} + +// --------------------------------------------------------------------------------------------- +// THE JOIN. The rows above prove the event is classified; gunbc.fleet_main_revision's own witness +// proves the advance decision. These prove the seam BETWEEN them -- that each decision becomes +// exactly one action, and that a refusal becomes no action at all. + +// The refusing arm is unreachable while the positive control above holds -- it recurses rather +// than fabricating an accepted revision, because a fabricated one would let every row below pass +// against a fixture the producers never admitted. +fn accepted_fixture() -> AcceptedFleetRevision { + match fleet_desired_accepted_from_event(event: admitting_event()) { + FleetDesiredRevisionAccepted { accepted: a } => a + FleetDesiredRevisionRefused { cause: _ } => accepted_fixture() + } +} + +fn action_for(input: FleetDesiredAdvanceInput) -> FleetDesiredAdmissionOutcome { + fleet_desired_action_from_decision(decision: decide_fleet_desired_advance(input: input)) +} + +// The relation is carried as an OBSERVATION -- which two revisions were compared -- rather than as +// a bare verdict, so these fixtures name both endpoints. Building it any other way would let a +// relation computed for one pair be applied to another, which is the refusal the last row here +// pins down. +fn observed_input(current_hex: String, relation: DeployRevisionRelation) -> FleetDesiredAdvanceInput { + FleetDesiredObservedCurrentInput { + accepted: accepted_fixture(), + current: fixture_oid(hex: current_hex), + relation: FleetRevisionRelationObservation { + current: fixture_oid(hex: current_hex), + accepted: fixture_oid(hex: fixture_candidate_hex), + relation: relation, + }, + } +} + +// A candidate descending from the current ref is the advancing case, and the authorized action must carry BOTH +// operands: the revision to publish and the prior it expects. An action naming only the target is +// a blind overwrite wearing a compare-and-swap's name. +test fn a_descendant_candidate_authorizes_an_advance_carrying_the_observed_prior() -> Bool { + match action_for(input: observed_input(current_hex: fixture_prior_hex, relation: DeployedIsAncestor)) { + AdmissionRefused { cause: _ } => false + AdmissionActionAuthorized { action: a } => + match a { + FleetDesiredRemoteAdvance { accepted: to, expected_prior: prior } => + (git_object_id_wire_hex(oid: to) as String == fixture_candidate_hex) + && (git_object_id_wire_hex(oid: prior) as String == fixture_prior_hex) + FleetDesiredAlreadyConvergedAction { revision: _ } => false + FleetDesiredSupersededAction { accepted: _, current: _ } => false + } + } +} + +// THE TWO NO-OP ARMS ARE AUTHORIZED, NOT REFUSED, and the distinction is the whole point of the +// action type: "the fleet is already where it should be" is a successful admission that mutates +// nothing, while a refusal means the gate could not decide. Collapsing them would make a healthy +// converged fleet report as a broken one on every floor run. +test fn an_already_converged_fleet_authorizes_a_no_op_rather_than_refusing() -> Bool { + match action_for(input: observed_input(current_hex: fixture_candidate_hex, relation: SameRevision)) { + AdmissionRefused { cause: _ } => false + AdmissionActionAuthorized { action: a } => + match a { + FleetDesiredAlreadyConvergedAction { revision: r } => + git_object_id_wire_hex(oid: r) as String == fixture_candidate_hex + FleetDesiredRemoteAdvance { accepted: _, expected_prior: _ } => false + FleetDesiredSupersededAction { accepted: _, current: _ } => false + } + } +} + +// A superseded candidate must never roll the fleet backwards. The relation says the accepted +// revision is an ancestor of what the fleet already runs, so publishing it would be a rewind +// dressed as an advance. +test fn a_superseded_candidate_authorizes_a_no_op_and_never_an_advance() -> Bool { + match action_for(input: observed_input(current_hex: fixture_candidate_hex, relation: CandidateIsAncestor)) { + AdmissionRefused { cause: _ } => false + AdmissionActionAuthorized { action: a } => + match a { + FleetDesiredSupersededAction { accepted: _, current: _ } => true + FleetDesiredRemoteAdvance { accepted: _, expected_prior: _ } => false + FleetDesiredAlreadyConvergedAction { revision: _ } => false + } + } } // THE EMPTY-OBSERVATION NARROW, AS A CLAIM. An unreadable prior must refuse, not be treated as an -// absent one — the arm that would create the ref from scratch and overwrite an admitted revision -// nobody could read. This is the discriminating input: the event is otherwise fully admitting. -test fn an_unobservable_prior_refuses_rather_than_creating_the_ref() -> Bool { - match decided( - event: admitting_event(), - observed: FleetDesiredUnobserved { cause: "ls-remote refused: network unreachable" }, - ) { - AdmissionAdvanceAuthorized { expected: _, to: _ } => false - AdmissionRefused { cause: c } => - string_contains(s: c, pattern: "never read as an absent one") +// absent one -- the arm that would create the ref from scratch and overwrite an admitted revision +// nobody could read. The event is otherwise fully admitting, so this is discriminating. +test fn an_unobservable_prior_refuses_rather_than_authorizing_a_creation() -> Bool { + match action_for(input: FleetDesiredExpectationRefusedInput { + accepted: accepted_fixture(), + cause: FleetDesiredRefUnobserved { cause: "ls-remote refused: network unreachable" }, + }) { + AdmissionActionAuthorized { action: _ } => false + AdmissionRefused { cause: c } => string_contains(s: c, pattern: "fleet_desired_admission: ") } } -// The authorized push names the observed prior as the compare-and-swap expectation, so a +// AN ABSENT REF REFUSES, AND THIS ROW WAS INVERTED AND THEN INVERTED BACK WITHIN ONE DAY. +// +// The policy it asserts -- absence is a STATE, creation is a CAPABILITY, and no observation of +// absence can supply a mint authority -- is gunbc.fleet_main_revision's, authored deliberately +// under the title "creation is not implied by absence". gunbc#8746 landed the opposite policy on +// main four and a half hours later, so merging main here was a policy DIVERGENCE. I then flipped +// this row to assert creation, calling my own position an accidental regression. It was not, and +// the flip is reverted with the reasoning recorded rather than quietly undone. +// +// WHY THIS PARTICULAR ROW IS DANGEROUS IN BOTH DIRECTIONS, which is the reusable part: a witness +// about a capability that SHOULD NOT EXIST and a witness about one that WAS LOST look identical +// when red. Restoring the action greens either. Only the policy says which repair is correct -- +// so this annotation states the policy, and a future red here is answered by reading it, not by +// making the row pass. +test fn an_absent_ref_refuses_because_creation_needs_a_mint_authority() -> Bool { + match action_for(input: FleetDesiredRefAbsentInput { accepted: accepted_fixture() }) { + AdmissionActionAuthorized { action: _ } => false + AdmissionRefused { cause: c } => string_contains(s: c, pattern: "mint the fleet root") + } +} + +// --------------------------------------------------------------------------------------------- +// THE RENDERED ACTION. + +// The authorized advance names the observed prior as the compare-and-swap expectation, so a // concurrent admission refuses at the remote instead of overwriting. -test fn the_authorized_push_carries_the_observed_prior_as_the_cas_expectation() -> Bool { - let script = fleet_desired_authorized_push_script( - expected: RemoteRefMustEqual { oid: fixture_oid(hex: fixture_prior_hex) }, - to: fixture_oid(hex: fixture_candidate_hex), - ) +test fn the_authorized_advance_carries_the_observed_prior_as_the_cas_expectation() -> Bool { + let script = fleet_desired_authorized_action_script( + action: FleetDesiredRemoteAdvance { + accepted: fixture_oid(hex: fixture_candidate_hex), + expected_prior: fixture_oid(hex: fixture_prior_hex), + }, + ) as String string_contains(s: script, pattern: concat("--force-with-lease=refs/fleet/desired:", fixture_prior_hex)) && string_contains(s: script, pattern: concat(fixture_candidate_hex, ":refs/fleet/desired")) } -// The creation push is still a compare-and-swap: git's empty `` is "the ref must not -// already exist". The claim pins the space after the colon so an expectation that silently -// rendered the prior-oid form — or dropped the lease entirely — cannot satisfy it. -test fn the_creation_push_leases_on_the_ref_being_absent() -> Bool { - let script = fleet_desired_authorized_push_script( - expected: RemoteRefMustBeAbsent, - to: fixture_oid(hex: fixture_candidate_hex), - ) - string_contains(s: script, pattern: "--force-with-lease=refs/fleet/desired: ") - && string_contains(s: script, pattern: concat(fixture_candidate_hex, ":refs/fleet/desired")) - && !string_contains(s: script, pattern: fixture_prior_hex) -} - -// THE RECEIPT HALF, WHICH THE TWO CLAIMS ABOVE DO NOT COVER. They assert what the push DEMANDS; -// this asserts what the run RECORDS. The two came apart once already: #8746 replaced the `from` -// operand with the expectation sum and the echo silently lost its prior, leaving eleven successful -// admissions whose demanded prior appears nowhere in their logs — the lease is real but unechoed -// (`set -eu`, no trace), and git's range line reports what happened, not what was required. -test fn the_receipt_names_both_operands_of_the_compare_and_swap() -> Bool { - let script = fleet_desired_authorized_push_script( - expected: RemoteRefMustEqual { oid: fixture_oid(hex: fixture_prior_hex) }, - to: fixture_oid(hex: fixture_candidate_hex), - ) - string_contains(s: script, pattern: concat("[fleet-desired] admitted ", concat(fixture_candidate_hex, concat(" expected-prior ", fixture_prior_hex)))) +// THE RECEIPT MUST NAME THE EXPECTED PRIOR, NOT ONLY THE TARGET. The regression this guards +// shipped upstream as collateral of a correct change: when main's admitted decision widened from +// a prior oid to an expectation, the echo could no longer print `from` on the absent arm, and +// dropping it for BOTH arms was the path of least resistance. What actually happened stays +// recoverable from git's range line; what was EXPECTED then appeared nowhere in the run. +// +// This gate has one authorized action, so there is one arm to check -- and the check is the +// contiguous pattern rather than the two hexes separately, because a script naming both revisions +// in unrelated positions would satisfy a looser assertion while telling the reader nothing about +// which was expected. Found by nimble-fox-671. +test fn the_receipt_names_the_expected_prior_beside_the_target() -> Bool { + let script = fleet_desired_authorized_action_script( + action: FleetDesiredRemoteAdvance { + accepted: fixture_oid(hex: fixture_candidate_hex), + expected_prior: fixture_oid(hex: fixture_prior_hex), + }, + ) as String + string_contains(s: script, pattern: concat(concat("admitted ", fixture_candidate_hex), concat(" expected-prior ", fixture_prior_hex))) } -// The creation arm has no prior to name, and the receipt must say so POSITIVELY. git spells the -// absent expectation as an empty , and an empty string in a receipt is indistinguishable -// from an operand that was never printed — which is the state this whole pair exists to refuse. -test fn the_creation_receipt_names_absence_rather_than_nothing() -> Bool { - let script = fleet_desired_authorized_push_script( - expected: RemoteRefMustBeAbsent, - to: fixture_oid(hex: fixture_candidate_hex), - ) - string_contains(s: script, pattern: "expected-prior absent") - && !string_contains(s: script, pattern: "expected-prior \"") +// THE WALL THE EXECUTING STEP DEPENDS ON. `test -s` distinguishes "authorization produced +// nothing" -- a writer or transport failure -- from "authorization said do nothing". That +// distinction survives only while a no-op action renders a NONEMPTY script, and it must hold by +// the renderer's shape rather than by an author remembering to echo. These two rows are the +// discriminating half: if either no-op arm is ever simplified to an empty string, the executing +// step reads a dropped authorization as a converged fleet. +test fn a_no_op_action_still_renders_a_nonempty_script() -> Bool { + let converged = fleet_desired_authorized_action_script( + action: FleetDesiredAlreadyConvergedAction { revision: fixture_oid(hex: fixture_candidate_hex) }, + ) as String + let superseded = fleet_desired_authorized_action_script( + action: FleetDesiredSupersededAction { + accepted: fixture_oid(hex: fixture_prior_hex), + current: fixture_oid(hex: fixture_candidate_hex), + }, + ) as String + (string_length(s: converged) > 0) && (string_length(s: superseded) > 0) +} + +// A no-op must mutate no ref. The renderer is the last place a stray push could be introduced, +// and the executing step runs whatever it produces without inspecting it. +test fn a_no_op_action_renders_no_ref_mutation() -> Bool { + let converged = fleet_desired_authorized_action_script( + action: FleetDesiredAlreadyConvergedAction { revision: fixture_oid(hex: fixture_candidate_hex) }, + ) as String + let superseded = fleet_desired_authorized_action_script( + action: FleetDesiredSupersededAction { + accepted: fixture_oid(hex: fixture_prior_hex), + current: fixture_oid(hex: fixture_candidate_hex), + }, + ) as String + !string_contains(s: converged, pattern: "git push") + && !string_contains(s: superseded, pattern: "git push") } // THE EMISSION HALF. The pure decision above proves the gate decides correctly; it proves nothing @@ -291,11 +409,63 @@ test fn the_admission_workflow_triggers_on_the_floor_workflow_completing() -> Bo && string_contains(s: yml, pattern: "admit_fleet_desired_from_floor_event_wet") } -// THE ACTUATION CARRIES NO DECISION. If the push step ever names the ref or a revision expression -// of its own, it has re-acquired the ability to push something the gate did not admit. -test fn the_admission_workflow_push_step_names_no_revision_of_its_own() -> Bool { +// THE TRIGGER MUST FILTER ON THE BRANCH, NOT ONLY THE JOB. A workflow_run trigger naming no +// branches creates a run for EVERY branch's floor completion; each one enters the single constant +// concurrency group before the job-level condition can skip it, and in the default group an +// arriving entry evicts the pending one. So an unfiltered trigger lets an irrelevant branch cancel +// a pending admission for a green main revision and then do nothing -- the drop this row exists to +// keep closed. It reads the emitted bytes because the defect was in the emission, not the model: +// the branch was checked in two places that both ran too late. +test fn the_admission_workflow_filters_the_trigger_to_the_default_branch() -> Bool { + let yml = expected_fleet_desired_yml() + let workflow_run_block = split(s: yml, delimiter: "workflow_run:").last() + let trigger = split(s: workflow_run_block, delimiter: "jobs:").first() + string_contains(s: trigger, pattern: "branches:") + && string_contains(s: trigger, pattern: gunbc_default_branch_name) +} + +// MAIN-FLOOR COMPLETIONS ARE RETAINED FOR ADJUDICATION RATHER THAN PENDING-REPLACED, AND THE +// CLAIM IS BOUNDED BY THE PLATFORM'S QUEUE CAPACITY. +// +// The default concurrency group holds one running and one PENDING entry, and an arriving entry +// CANCELS the pending one -- so under it a green admission could be dropped by a later run that +// cannot advance (a red floor, a manual dispatch, an older rerun). The trigger filter cannot close +// that half: those all carry head_branch main, and whether they can advance is decided in-model, +// after the run exists. So the emitted mapping must carry `queue: max`. +// +// THIS ROW WAS NAMED `..._queues_every_admissible_completion_...` AND THAT WAS AN OVERCLAIM. +// GitHub documents the ceiling explicitly: "Up to 100 jobs or workflow runs can be `pending` in +// the concurrency group. When the queue is full, any additional jobs or workflow runs are +// canceled." (docs.github.com, workflow syntax, concurrency; read 2026-08-21.) So the honest claim +// is retention-instead-of-replacement WHILE THE GROUP SITS BELOW 100 PENDING -- not "every". +// +// The overclaim was not observable from the bytes this row reads, which is exactly why the NAME +// mattered: at 100 pending the mechanism cancels and this row still greens, because a queue depth +// is not a fact about an emitted mapping. A name is the claim the next reader inherits, and this +// one promised something the witness cannot witness. +// +// IF ABSOLUTE LOSSLESSNESS EVER BECOMES REQUIRED, THE NEXT RUNG IS NOT A BIGGER QUEUE. It is +// durable reconciliation over (eligible floor-green revisions MINUS recorded admission decisions). +// `queue: max` is a strong bounded transport, not an unbounded event ledger -- and it cannot buy +// ordering either, since GitHub processes pending entries by when they began waiting and does not +// guarantee order. Found by side-chat review, relayed by nimble-fox-671; the 100-entry cap and the +// cancel-when-full half were both verified against the documentation rather than taken on report. +// +// cancel-in-progress must ALSO be false, and it is a separate assertion rather than an implied +// one: it is what keeps a RUNNING admission from being interrupted between the compare-and-swap +// decision and the push, which is the one property the default group was genuinely providing. +test fn the_admission_workflow_uses_the_maximum_pending_queue_instead_of_pending_replacement() -> Bool { + let yml = expected_fleet_desired_yml() + let concurrency = split(s: split(s: yml, delimiter: "concurrency:").last(), delimiter: "jobs:").first() + string_contains(s: concurrency, pattern: "queue: max") + && string_contains(s: concurrency, pattern: "cancel-in-progress: false") +} + +// THE ACTUATION CARRIES NO DECISION. If the action step ever names the ref or a revision +// expression of its own, it has re-acquired the ability to push something the gate did not admit. +test fn the_admission_workflow_action_step_names_no_revision_of_its_own() -> Bool { let yml = expected_fleet_desired_yml() - string_contains(s: yml, pattern: fleet_desired_admission_authorized_push_path) + string_contains(s: yml, pattern: fleet_desired_admission_authorized_action_path) && !string_contains(s: yml, pattern: "GITHUB_SHA") && !string_contains(s: yml, pattern: "force-with-lease") && !string_contains(s: yml, pattern: "ls-remote") diff --git a/dag/test/claim/fleet_main_revision_witness_test.dag b/dag/test/claim/fleet_main_revision_witness_test.dag index ca045417096..312d654aa6e 100644 --- a/dag/test/claim/fleet_main_revision_witness_test.dag +++ b/dag/test/claim/fleet_main_revision_witness_test.dag @@ -1,17 +1,60 @@ module test.claim.fleet_main_revision_witness -import std.types { Bool, String } -import extdeps.git.object_store { GitObjectId, git_sha1_object_id } +import std.types { Bool, String, NonEmptyStr, Int } +import extdeps.git.object_store { + GitObjectId, + git_sha1_object_id, + git_object_id_eq, + git_object_id_wire_hex, +} +import extdeps.git.publication_transport { + GitRemoteRefExpectation, + RemoteRefMustBeAbsent, + RemoteRefMustEqual, +} +import gunbc.live_deploy.revision { + DeployRevisionRelation, + SameRevision, + DeployedIsAncestor, + CandidateIsAncestor, + UnrelatedHistories, + RelationUnverifiable, +} +import gunbc.fleet_revision_acceptance { + AcceptedFleetRevision, + RequiredCiContractIdentity, + required_ci_contract, +} import gunbc.fleet_main_revision { fleet_desired_ref_name, FleetDesiredRevision, FleetDesiredAdmitted, + FleetDesiredAbsent, + FleetDesiredUndecodable, FleetDesiredUnobserved, fleet_desired_revision_target, - FleetDesiredAdvance, - AdvanceAdmitted, - AdvanceRefused, - admit_fleet_desired_advance, + fleet_desired_advance_expectation, + FleetRevisionRelationObservation, + FleetDesiredAdvanceRefusal, + AdvanceExpectationUnavailable, + AdvanceHistoriesUnrelated, + AdvanceRelationUnobservable, + AdvanceRelationIsAboutAnotherPair, + InitialFleetDesiredCreationNotAuthorized, + FleetDesiredAdvanceInput, + FleetDesiredExpectationRefusedInput, + FleetDesiredRefAbsentInput, + FleetDesiredObservedCurrentInput, + FleetDesiredAdvanceDecision, + FleetDesiredAdvanceAdmitted, + FleetDesiredAlreadyConverged, + FleetDesiredSupersededNoOp, + FleetDesiredAdvanceRefused, + fleet_desired_admitted_expectation, + decide_fleet_desired_advance, + fleet_revision_relation_from_merge_base, + relation_from_merge_base_oid, + merge_base_relation, converge_target_revision, } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -22,52 +65,385 @@ fn fixture_rev(hex_char: String) -> GitObjectId? { git_sha1_object_id(hex: join([hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char,hex_char], "")) } -// RED — the load-bearing admission law: a revision whose floor is not green NEVER -// advances the desired ref, whatever the current ref state. -test fn advance_refused_without_floor_green() -> Bool { +fn accepted_at(revision: GitObjectId) -> AcceptedFleetRevision { + AcceptedFleetRevision { + revision: revision, + required_ci_contract: required_ci_contract(), + required_ci_evidence: "required-ci evidence", + default_branch_evidence: "default-branch evidence", + } +} + +fn observed_at(current: GitObjectId) -> FleetDesiredRevision { + FleetDesiredAdmitted { revision: current } +} + +fn relation_between( + current: GitObjectId, + accepted: GitObjectId, + relation: DeployRevisionRelation, +) -> FleetRevisionRelationObservation { + FleetRevisionRelationObservation { current: current, accepted: accepted, relation: relation } +} + +// Every row below decides ONE pair through the real seam. Note what the helper no longer needs: a +// relation for cases that have no current revision. The input sum means the create and refusal +// rows cannot supply one, so no fixture here invents a fact to satisfy a parameter. +fn decide_observed( + current: GitObjectId, + accepted: GitObjectId, + relation: DeployRevisionRelation, +) -> FleetDesiredAdvanceDecision { + decide_fleet_desired_advance( + input: FleetDesiredObservedCurrentInput { + accepted: accepted_at(revision: accepted), + current: current, + relation: relation_between(current: current, accepted: accepted, relation: relation), + }, + ) +} + +// ABSENCE IS A STATE; CREATION IS A CAPABILITY. RemoteRefMustBeAbsent is a compare-and-swap +// PRECONDITION -- it proves the ref is not there -- and it establishes nothing about whether this +// path may bring the fleet's root authority into existence. An earlier revision of this decision +// admitted a create on exactly that inference, which would also have silently widened live policy: +// gunbc.fleet_desired_admission refuses first creation today, deliberately, so a "consumer port" +// would have handed a workflow authorized only to ADVANCE the power to MINT. +// +// The refusal names the accepted revision, so the receipt says which creation was declined rather +// than merely that one was. +test fn an_absent_ref_is_a_precondition_not_an_authorization_to_create() -> Bool { match fixture_rev(hex_char: "a") { - Present { value: cand } => - match admit_fleet_desired_advance(candidate: cand, floor_green: false, current: none) { - AdvanceRefused { cause: _ } => true + Present { value: acc } => + match decide_fleet_desired_advance( + input: FleetDesiredRefAbsentInput { accepted: accepted_at(revision: acc) }, + ) { + FleetDesiredAdvanceRefused { + cause: InitialFleetDesiredCreationNotAuthorized { accepted: named }, + } => git_object_id_eq(left: named, right: acc) + _ => false + } + _ => false + } +} + +// FORWARD MOTION, AND THE LEASE NAMES THE EXACT PRIOR VERIFIED. A lease naming the wrong prior +// refuses forever; a lease claiming absent-when-present CLOBBERS. Asserting only the variant +// leaves both silent, so the prior's identity is asserted here. +test fn a_current_ancestor_admits_a_forward_advance_leasing_that_exact_prior() -> Bool { + match fixture_rev(hex_char: "b") { + Present { value: cur } => + match fixture_rev(hex_char: "c") { + Present { value: acc } => + match decide_observed(current: cur, accepted: acc, relation: DeployedIsAncestor) { + FleetDesiredAdvanceAdmitted { accepted: a, expected_prior: prior } => + git_object_id_eq(left: a.revision, right: acc) + && git_object_id_eq(left: prior, right: cur) + && match fleet_desired_admitted_expectation( + decision: decide_observed(current: cur, accepted: acc, relation: DeployedIsAncestor), + ) { + Present { value: RemoteRefMustEqual { oid: leased } } => + git_object_id_eq(left: leased, right: cur) + _ => false + } + _ => false + } _ => false } - && match fixture_rev(hex_char: "b") { - Present { value: cur } => - match admit_fleet_desired_advance(candidate: cand, floor_green: false, current: Present { value: cur }) { - AdvanceRefused { cause: _ } => true + _ => false + } +} + +// TWO TERMINAL SUCCESSES THAT WRITE NOTHING, and neither may be rendered as operational red. +// Superseded is a late result for an OLDER revision arriving after a newer one was admitted -- the +// normal consequence of runs finishing out of order. Both are asserted to be non-refusals AND to +// yield no lease, which is the property that would break if either were folded into the refusal +// arm for tidiness or given an expectation it must not have. +test fn already_converged_and_superseded_are_successes_that_write_nothing() -> Bool { + match fixture_rev(hex_char: "d") { + Present { value: rev } => + match decide_observed(current: rev, accepted: rev, relation: SameRevision) { + FleetDesiredAlreadyConverged { accepted: a } => git_object_id_eq(left: a.revision, right: rev) + _ => false + } + && match fleet_desired_admitted_expectation( + decision: decide_observed(current: rev, accepted: rev, relation: SameRevision), + ) { + Present { value: _ } => false + _ => true + } + _ => false + } + && match fixture_rev(hex_char: "e") { + Present { value: cur } => + match fixture_rev(hex_char: "f") { + Present { value: acc } => + match decide_observed(current: cur, accepted: acc, relation: CandidateIsAncestor) { + FleetDesiredSupersededNoOp { accepted: a, current: c } => + git_object_id_eq(left: a.revision, right: acc) + && git_object_id_eq(left: c, right: cur) _ => false } + && match fleet_desired_admitted_expectation( + decision: decide_observed(current: cur, accepted: acc, relation: CandidateIsAncestor), + ) { + Present { value: _ } => false + _ => true + } _ => false } + _ => false + } +} + +// THE ROW A CAS CANNOT SUPPLY. Unrelated histories means neither revision is an ancestor of the +// other, so the ref would move sideways. Every upstream check passes: the revision was proven, the +// observation was real, the lease would match. Only the relation refuses it, which is the whole +// argument for the relation existing. Unverifiable is asserted beside it because unknown-as-forward +// is the empty-observation narrow pointed at the one property the CAS cannot check. +test fn unrelated_and_unverifiable_both_refuse_though_the_lease_would_have_matched() -> Bool { + match fixture_rev(hex_char: "1") { + Present { value: cur } => + match fixture_rev(hex_char: "2") { + Present { value: acc } => + match decide_observed(current: cur, accepted: acc, relation: UnrelatedHistories) { + FleetDesiredAdvanceRefused { + cause: AdvanceHistoriesUnrelated { current: c, accepted: a }, + } => git_object_id_eq(left: c, right: cur) && git_object_id_eq(left: a, right: acc) + _ => false + } + && match decide_observed( + current: cur, + accepted: acc, + relation: RelationUnverifiable { cause: "shallow clone: merge base unreachable" }, + ) { + FleetDesiredAdvanceRefused { + cause: AdvanceRelationUnobservable { current: _, accepted: _, cause: _ }, + } => true + _ => false + } + _ => false + } _ => false } } -// The admitted advance is a CAS carrying the expected prior — first admission carries -// from=none (ref creation), a subsequent one carries the exact prior revision. -test fn admitted_advance_is_cas_carrying_expected_prior() -> Bool { - match fixture_rev(hex_char: "a") { - Present { value: cand } => - match admit_fleet_desired_advance(candidate: cand, floor_green: true, current: none) { - AdvanceAdmitted { from: f, to: _ } => - match f { - Present { value: _ } => false - _ => true +// THE SUBJECT-BINDING WALL. A bare relation is not evidence: it does not say WHICH TWO revisions +// were compared, so a genuine DeployedIsAncestor computed for some OTHER pair would license an +// advance here. Note the supplied relation is entirely TRUTHFUL about its own pair; what makes it +// inadmissible is that its pair is not the one under decision. +test fn a_relation_about_another_pair_is_refused_however_true_it_is() -> Bool { + match fixture_rev(hex_char: "5") { + Present { value: cur } => + match fixture_rev(hex_char: "6") { + Present { value: acc } => + match fixture_rev(hex_char: "7") { + Present { value: stranger } => + match decide_fleet_desired_advance( + input: FleetDesiredObservedCurrentInput { + accepted: accepted_at(revision: acc), + current: cur, + relation: relation_between( + current: stranger, + accepted: acc, + relation: DeployedIsAncestor, + ), + }, + ) { + FleetDesiredAdvanceRefused { + cause: AdvanceRelationIsAboutAnotherPair { + relation_current: rc, + relation_accepted: _, + actual_current: ac, + actual_accepted: _, + }, + } => + git_object_id_eq(left: rc, right: stranger) + && git_object_id_eq(left: ac, right: cur) + _ => false + } + _ => false } _ => false } - && match fixture_rev(hex_char: "b") { - Present { value: cur } => - match admit_fleet_desired_advance(candidate: cand, floor_green: true, current: Present { value: cur }) { - AdvanceAdmitted { from: f2, to: _ } => - match f2 { - Present { value: _ } => true + _ => false + } +} + +// The remedy-preserving refusals survive to the final decision. An unobservable ref and a corrupt +// one both refuse, and they refuse DISTINGUISHABLY -- the property the whole seam was rebuilt to +// hold, asserted at its last consumer rather than only at its source. Neither supplies a relation, +// because neither has a current revision to relate to. +test fn the_refusal_remedy_survives_to_the_final_decision() -> Bool { + match fixture_rev(hex_char: "8") { + Present { value: acc } => + match decide_fleet_desired_advance( + input: FleetDesiredExpectationRefusedInput { + accepted: accepted_at(revision: acc), + cause: FleetDesiredRefUnobserved { cause: "ls-remote refused" }, + }, + ) { + FleetDesiredAdvanceRefused { + cause: AdvanceExpectationUnavailable { cause: FleetDesiredRefUnobserved { cause: _ } }, + } => true + _ => false + } + && match decide_fleet_desired_advance( + input: FleetDesiredExpectationRefusedInput { + accepted: accepted_at(revision: acc), + cause: FleetDesiredRefUndecodable { advertised: "not-a-sha" }, + }, + ) { + FleetDesiredAdvanceRefused { + cause: AdvanceExpectationUnavailable { + cause: FleetDesiredRefUndecodable { advertised: line }, + }, + } => line == "not-a-sha" + _ => false + } + _ => false + } +} + +// THE PAIR THE EXIT CODE EXISTS FOR, AND IT IS THE ONLY ROW THAT JUSTIFIES CARRYING ONE. +// +// `git merge-base` exits 1 for "these two share no merge base" -- an ANSWER about the pair -- and +// 128 for "invalid ref, or this is not a repository" -- a failure to look. Both are +// exit_success = false. Reading the Bool alone forces one of two wrong moves: refuse both, which +// discards a real answer and blocks an advance that unrelated-histories should have decided; or +// admit both, which reads an unreadable repository as PROOF that two revisions are unrelated. +// +// These two rows are asserted together deliberately. Either alone is satisfiable by a fold that +// ignores the exit code entirely -- one by always observing, the other by always refusing -- so it +// is the DIVERGENCE between them that carries the claim, not either verdict on its own. +test fn exit_one_is_an_answer_and_exit_one_two_eight_is_an_absence_of_one() -> Bool { + match fixture_rev(hex_char: "1") { + Present { value: cur } => + match fixture_rev(hex_char: "2") { + Present { value: acc } => + match fleet_revision_relation_from_merge_base( + current: cur, + accepted: acc, + exit_code: 1, + base_hex: "", + stderr: "", + ) { + FleetRevisionRelationObservation { current: c, accepted: a, relation: rel } => + git_object_id_eq(left: c, right: cur) + && git_object_id_eq(left: a, right: acc) + && match rel { + UnrelatedHistories => true _ => false } + } + && match merge_base_relation( + current: cur, + accepted: acc, + exit_code: 128, + base_hex: "", + stderr: "fatal: not a git repository", + ) { + RelationUnverifiable { cause: _ } => true _ => false } - _ => false - } + _ => false + } + _ => false + } +} + +// One merge base decides BOTH directions -- a commit is an ancestor of another exactly when it IS +// their merge base -- so no second probe is needed. All three exit-0 shapes are exercised: the base +// is the current revision (forward), the accepted one (superseded), or neither (diverged). +test fn one_merge_base_decides_both_directions() -> Bool { + match fixture_rev(hex_char: "3") { + Present { value: cur } => + match fixture_rev(hex_char: "4") { + Present { value: acc } => + match fixture_rev(hex_char: "5") { + Present { value: third } => + relation_from_merge_base_oid(current: cur, accepted: acc, base: cur) == DeployedIsAncestor + && relation_from_merge_base_oid(current: cur, accepted: acc, base: acc) == CandidateIsAncestor + && relation_from_merge_base_oid(current: cur, accepted: acc, base: third) == UnrelatedHistories + _ => false + } + _ => false + } + _ => false + } +} + +// Equality short-circuits before any probe result is consulted, so a converged pair is decided +// without trusting the transport at all. Asserted against a REFUSING exit code: if the fold read +// the exit first, this would refuse instead of reporting convergence. +test fn an_equal_pair_is_converged_without_consulting_the_probe() -> Bool { + match fixture_rev(hex_char: "6") { + Present { value: rev } => + match merge_base_relation( + current: rev, + accepted: rev, + exit_code: 128, + base_hex: "", + stderr: "fatal: not a git repository", + ) { + SameRevision => true + _ => false + } + _ => false + } +} + +// A successful probe whose stdout is not an object id REFUSES rather than folding a garbage value +// into a relation. The success exit says the command ran; it does not say the output is a commit. +test fn a_successful_probe_with_undecodable_output_refuses() -> Bool { + match fixture_rev(hex_char: "7") { + Present { value: cur } => + match fixture_rev(hex_char: "8") { + Present { value: acc } => + match merge_base_relation( + current: cur, + accepted: acc, + exit_code: 0, + base_hex: "not-a-sha", + stderr: "", + ) { + RelationUnverifiable { cause: _ } => true + _ => false + } + _ => false + } + _ => false + } +} + +// The fold feeds the decision end to end: a merge base equal to the current revision is forward +// motion, and the advance leases exactly that prior. This is the row that proves the observer and +// the decision agree on which endpoint is which -- swapping them would still typecheck. +test fn the_folded_relation_drives_the_decision_and_leases_the_right_prior() -> Bool { + match fixture_rev(hex_char: "9") { + Present { value: cur } => + match fixture_rev(hex_char: "a") { + Present { value: acc } => + match decide_fleet_desired_advance( + input: FleetDesiredObservedCurrentInput { + accepted: accepted_at(revision: acc), + current: cur, + relation: fleet_revision_relation_from_merge_base( + current: cur, + accepted: acc, + exit_code: 0, + base_hex: git_object_id_wire_hex(oid: cur) as String, + stderr: "", + ), + }, + ) { + FleetDesiredAdvanceAdmitted { accepted: a, expected_prior: prior } => + git_object_id_eq(left: a.revision, right: acc) + && git_object_id_eq(left: prior, right: cur) + _ => false + } + _ => false + } _ => false } } diff --git a/dag/test/claim/fleet_revision_acceptance_witness_test.dag b/dag/test/claim/fleet_revision_acceptance_witness_test.dag new file mode 100644 index 00000000000..3f6fdca913c --- /dev/null +++ b/dag/test/claim/fleet_revision_acceptance_witness_test.dag @@ -0,0 +1,393 @@ +module test.claim.fleet_revision_acceptance_witness + +import std.types { String, NonEmptyStr, Bool } +import extdeps.git.object_store { GitObjectId, git_object_id_from_untagged_hex, git_object_id_eq } +import extdeps.github.workflow_runs { WorkflowRunConclusion, Success, Failure, Cancelled } +import extdeps.github.workflow_run_event { WorkflowRunEvent } +import gunbc.generated_artifact { WitnessFloorYamlArtifact, artifact_path } +import gunbc.fleet_revision_acceptance { + RequiredCiContractIdentity, + required_ci_contract, + RequiredCiSucceeded, + DefaultBranchRevisionObserved, + RequiredCiRefusal, + CiWorkflowNotTheRequiredFloor, + CiRepositoryNotThisRepository, + CiHeadRepositoryNotThisRepository, + CiActivityNotCompleted, + CiConclusionNotSuccess, + CiHeadShaUndecodable, + RequiredCiAdmission, + RequiredCiAdmitted, + RequiredCiRefused, + DefaultBranchRefusal, + BranchIsNotTheDefaultBranch, + BranchEventIsNotAPush, + BranchHeadShaUndecodable, + DefaultBranchAdmission, + DefaultBranchAdmitted, + DefaultBranchRefused, + AcceptedFleetRevision, + FleetRevisionAdmission, + FleetRevisionAccepted, + RequiredCiAndDefaultBranchRevisionMismatch, + accept_required_ci_workflow_run, + observe_default_branch_revision, + admit_fleet_revision, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data sha_a: String = "a1a1a1a1a1a1a1a1a1a1a1a1a1a1a1a1a1a1a1a1" + +data sha_b: String = "b2b2b2b2b2b2b2b2b2b2b2b2b2b2b2b2b2b2b2b2" + +data github_evidence: String = "workflow_run event, run 17000000001" + +// ONE BUILDER, AND EVERY WITNESS BREAKS EXACTLY ONE FACT, so a red row names the fact it broke +// rather than the shape of a hand-copied record. The workflow path defaults through the real +// artifact authority rather than a literal: a fixture hardcoding it would keep passing after a +// rename while production refused every genuine run -- and that failure is SILENT, because a +// too-strict wall simply stops the fleet advancing with nothing red anywhere. +fn ev( + activity: String, + workflow_path: String, + conclusion: WorkflowRunConclusion, + head_sha: String, + head_branch: String, + head_repository_full_name: String, + originating_event: String, + repository_full_name: String, +) -> WorkflowRunEvent { + WorkflowRunEvent { + activity: activity, + run_id: "17000000001", + workflow_name: "witnesses", + workflow_id: "900001", + workflow_path: workflow_path, + conclusion: conclusion, + html_url: "https://github.com/gunb-ai/gunbc/actions/runs/17000000001", + run_started_at: "2026-08-21T00:00:00Z", + head_sha: head_sha, + head_branch: head_branch, + head_repository_full_name: head_repository_full_name, + originating_event: originating_event, + repository_full_name: repository_full_name, + } +} + +fn trunk_push(head_sha: String) -> WorkflowRunEvent { + ev( + activity: "completed", + workflow_path: artifact_path(a: WitnessFloorYamlArtifact), + conclusion: Success, + head_sha: head_sha, + head_branch: "main", + head_repository_full_name: "gunb-ai/gunbc", + originating_event: "push", + repository_full_name: "gunb-ai/gunbc", + ) +} + +fn pull_request_run(head_sha: String) -> WorkflowRunEvent { + ev( + activity: "completed", + workflow_path: artifact_path(a: WitnessFloorYamlArtifact), + conclusion: Success, + head_sha: head_sha, + head_branch: "topic/experiment", + head_repository_full_name: "gunb-ai/gunbc", + originating_event: "pull_request", + repository_full_name: "gunb-ai/gunbc", + ) +} + +fn ci_admits(e: WorkflowRunEvent) -> Bool { + match accept_required_ci_workflow_run(event: e, evidence: github_evidence) { + RequiredCiAdmitted { succeeded: _ } => true + RequiredCiRefused { cause: _ } => false + } +} + +fn branch_admits(e: WorkflowRunEvent) -> Bool { + match observe_default_branch_revision(event: e, evidence: github_evidence) { + DefaultBranchAdmitted { observed: _ } => true + DefaultBranchRefused { cause: _ } => false + } +} + +fn oid(hex: String) -> GitObjectId? { git_object_id_from_untagged_hex(hex: hex) } + +// POSITIVE CONTROL, load-bearing rather than ceremonial. Almost every other row asserts a REFUSAL, +// and a pair of producers that refused unconditionally would satisfy all of them. This is the row +// that fails when a wall is TOO STRICT -- the failure mode a wall-shaped change actually has, and +// the one that is invisible in production. +test fn an_eligible_trunk_push_satisfies_both_propositions_and_the_join_accepts() -> Bool { + match accept_required_ci_workflow_run(event: trunk_push(head_sha: sha_a), evidence: github_evidence) { + RequiredCiAdmitted { succeeded: ci } => + match observe_default_branch_revision(event: trunk_push(head_sha: sha_a), evidence: github_evidence) { + DefaultBranchAdmitted { observed: br } => + match admit_fleet_revision(required_ci: ci, default_branch: br) { + FleetRevisionAccepted { accepted: a } => + match oid(hex: sha_a) { + Present { value: expected } => git_object_id_eq(left: a.revision, right: expected) + none => false + } + _ => false + } + DefaultBranchRefused { cause: _ } => false + } + RequiredCiRefused { cause: _ } => false + } +} + +// THE ASYMMETRY, AND IT IS THE WHOLE REASON THE TWO PROPOSITIONS ARE SEPARATE CARRIERS. +// +// A PR's merge-subject run genuinely ran the Required CI contract and genuinely passed on that +// tree. Refusing it as a CI failure would be a lie about a real result -- so this producer ADMITS +// it, and that admission is correct. What the run cannot prove is that the revision entered the +// default branch, and that is exactly where it is refused. +// +// Had the two been folded into one predicate, either fact could stand in for the pair, and the +// fleet would follow a revision main never had. This row is the executable form of that argument: +// the SAME event, admitted by one producer and refused by the other. +test fn a_pull_request_run_proves_required_ci_but_not_the_default_branch() -> Bool { + ci_admits(e: pull_request_run(head_sha: sha_a)) + && match observe_default_branch_revision( + event: pull_request_run(head_sha: sha_a), + evidence: github_evidence, + ) { + DefaultBranchRefused { cause: BranchEventIsNotAPush { observed: o } } => o == "pull_request" + _ => false + } +} + +// A push to a topic branch is the other half of the same asymmetry: the event IS a push, so the +// event-kind arm passes and the BRANCH arm must be the one that refuses. Without this row a +// producer checking only the originating event would pass every branch row above. +test fn a_push_to_a_topic_branch_is_refused_by_the_branch_fact() -> Bool { + match observe_default_branch_revision( + event: ev( + activity: "completed", + workflow_path: artifact_path(a: WitnessFloorYamlArtifact), + conclusion: Success, + head_sha: sha_a, + head_branch: "topic/experiment", + head_repository_full_name: "gunb-ai/gunbc", + originating_event: "push", + repository_full_name: "gunb-ai/gunbc", + ), + evidence: github_evidence, + ) { + DefaultBranchRefused { cause: BranchIsNotTheDefaultBranch { observed: o, required: r } } => + o == "topic/experiment" && r == "main" + _ => false + } +} + +// THE MISMATCH ARM. Required CI proving revision A and the default branch carrying revision B is +// not a contradiction in the data -- both facts can be perfectly true, about different revisions, +// and they arrive together whenever a push lands while a run is in flight. What is false is the +// CONJUNCTION anyone would infer from holding both, and the refusal carries BOTH revisions because +// "which two" is the entire content of the finding. +test fn required_ci_for_one_revision_and_a_branch_at_another_refuses_naming_both() -> Bool { + match accept_required_ci_workflow_run(event: trunk_push(head_sha: sha_a), evidence: github_evidence) { + RequiredCiAdmitted { succeeded: ci } => + match observe_default_branch_revision(event: trunk_push(head_sha: sha_b), evidence: github_evidence) { + DefaultBranchAdmitted { observed: br } => + match admit_fleet_revision(required_ci: ci, default_branch: br) { + RequiredCiAndDefaultBranchRevisionMismatch { + required_ci_revision: got_ci, + default_branch_revision: got_br, + } => + match oid(hex: sha_a) { + Present { value: a } => + match oid(hex: sha_b) { + Present { value: b } => + git_object_id_eq(left: got_ci, right: a) + && git_object_id_eq(left: got_br, right: b) + none => false + } + none => false + } + _ => false + } + DefaultBranchRefused { cause: _ } => false + } + RequiredCiRefused { cause: _ } => false + } +} + +// THE REVISION IS DECODED BEFORE ANY POSITIVE CARRIER EXISTS. GitHub says head_sha is a SHA; +// nothing on the wire establishes it. Both producers refuse an undecodable value rather than +// constructing a carrier around it, so no consumer can be handed a revision that is not one. +test fn an_undecodable_head_sha_refuses_on_both_producers() -> Bool { + match accept_required_ci_workflow_run( + event: trunk_push(head_sha: "not-a-sha"), + evidence: github_evidence, + ) { + RequiredCiRefused { cause: CiHeadShaUndecodable { observed: o } } => o == "not-a-sha" + _ => false + } + && match observe_default_branch_revision( + event: trunk_push(head_sha: "not-a-sha"), + evidence: github_evidence, + ) { + DefaultBranchRefused { cause: BranchHeadShaUndecodable { observed: o } } => o == "not-a-sha" + _ => false + } +} + +// Each CI identity fact refuses with ITS OWN cause. Asserting only "refused" would let every arm +// collapse into one and still pass -- and the collapse is what makes a refusal undebuggable, since +// the remedies differ: wrong producer, wrong repo, an untrusted fork's head, not finished. +test fn each_required_ci_identity_fact_refuses_with_its_own_cause() -> Bool { + match accept_required_ci_workflow_run( + event: ev( + activity: "completed", + workflow_path: ".github/workflows/fleet-converge.yml", + conclusion: Success, + head_sha: sha_a, + head_branch: "main", + head_repository_full_name: "gunb-ai/gunbc", + originating_event: "push", + repository_full_name: "gunb-ai/gunbc", + ), + evidence: github_evidence, + ) { + RequiredCiRefused { cause: CiWorkflowNotTheRequiredFloor { observed_path: p, required_path: q } } => + p == ".github/workflows/fleet-converge.yml" && q == artifact_path(a: WitnessFloorYamlArtifact) + _ => false + } + && match accept_required_ci_workflow_run( + event: ev( + activity: "completed", + workflow_path: artifact_path(a: WitnessFloorYamlArtifact), + conclusion: Success, + head_sha: sha_a, + head_branch: "main", + head_repository_full_name: "gunb-ai/gunbc", + originating_event: "push", + repository_full_name: "other/fork", + ), + evidence: github_evidence, + ) { + RequiredCiRefused { cause: CiRepositoryNotThisRepository { observed: o, required: _ } } => + o == "other/fork" + _ => false + } + && match accept_required_ci_workflow_run( + event: ev( + activity: "completed", + workflow_path: artifact_path(a: WitnessFloorYamlArtifact), + conclusion: Success, + head_sha: sha_a, + head_branch: "main", + head_repository_full_name: "someone/fork", + originating_event: "push", + repository_full_name: "gunb-ai/gunbc", + ), + evidence: github_evidence, + ) { + RequiredCiRefused { cause: CiHeadRepositoryNotThisRepository { observed: o, required: _ } } => + o == "someone/fork" + _ => false + } + && match accept_required_ci_workflow_run( + event: ev( + activity: "requested", + workflow_path: artifact_path(a: WitnessFloorYamlArtifact), + conclusion: Success, + head_sha: sha_a, + head_branch: "main", + head_repository_full_name: "gunb-ai/gunbc", + originating_event: "push", + repository_full_name: "gunb-ai/gunbc", + ), + evidence: github_evidence, + ) { + RequiredCiRefused { cause: CiActivityNotCompleted { observed: o } } => o == "requested" + _ => false + } +} + +// A run that did not conclude Success is refused and the OBSERVED conclusion is carried. Cancelled +// is exercised beside Failure deliberately: a cancelled run produces no failure to investigate, so +// it is the state most likely to be read as "nothing happened" -- and it is exactly the state that +// must not be mistaken for a floor that ran. +test fn only_a_successful_conclusion_admits_and_the_others_are_named() -> Bool { + match accept_required_ci_workflow_run( + event: ev( + activity: "completed", + workflow_path: artifact_path(a: WitnessFloorYamlArtifact), + conclusion: Failure, + head_sha: sha_a, + head_branch: "main", + head_repository_full_name: "gunb-ai/gunbc", + originating_event: "push", + repository_full_name: "gunb-ai/gunbc", + ), + evidence: github_evidence, + ) { + RequiredCiRefused { cause: CiConclusionNotSuccess { observed: c } } => + match c { + Failure => true + _ => false + } + _ => false + } + && match accept_required_ci_workflow_run( + event: ev( + activity: "completed", + workflow_path: artifact_path(a: WitnessFloorYamlArtifact), + conclusion: Cancelled, + head_sha: sha_a, + head_branch: "main", + head_repository_full_name: "gunb-ai/gunbc", + originating_event: "push", + repository_full_name: "gunb-ai/gunbc", + ), + evidence: github_evidence, + ) { + RequiredCiRefused { cause: CiConclusionNotSuccess { observed: c2 } } => + match c2 { + Cancelled => true + _ => false + } + _ => false + } +} + +// IDENTITY BEFORE OUTCOME, as a claim under test rather than an accident of how the ifs nest. A +// FAILED run of the WRONG workflow must refuse as the wrong workflow: reporting "the floor was not +// green" about a run that was never the floor sends a reader to investigate a failure that does +// not exist, and that investigation terminates in confusion rather than in a fix. +test fn a_failed_run_of_the_wrong_workflow_refuses_as_the_wrong_workflow() -> Bool { + match accept_required_ci_workflow_run( + event: ev( + activity: "completed", + workflow_path: ".github/workflows/fleet-converge.yml", + conclusion: Failure, + head_sha: sha_a, + head_branch: "main", + head_repository_full_name: "gunb-ai/gunbc", + originating_event: "push", + repository_full_name: "gunb-ai/gunbc", + ), + evidence: github_evidence, + ) { + RequiredCiRefused { cause: CiWorkflowNotTheRequiredFloor { observed_path: _, required_path: _ } } => true + _ => false + } +} + +// The contract identity is DERIVED from the artifact authority that emits the workflow, never +// re-typed. If this row and the emitter disagree, the fixture is lying rather than the wall. It +// carries no phase roster: the fleet asks whether the exact contract succeeded for the exact +// revision, and adding a phase to the floor must not be a breaking change to fleet admission. +test fn the_contract_identity_is_the_emitted_workflow_not_a_phase_roster() -> Bool { + required_ci_contract().workflow_path == artifact_path(a: WitnessFloorYamlArtifact) + && required_ci_contract().workflow_path == ".github/workflows/witnesses.yml" + && required_ci_contract().repository_full_name == "gunb-ai/gunbc" +} diff --git a/dag/test/claim/fleet_revision_relation_wet_matrix_test.dag b/dag/test/claim/fleet_revision_relation_wet_matrix_test.dag new file mode 100644 index 00000000000..bad91be89cd --- /dev/null +++ b/dag/test/claim/fleet_revision_relation_wet_matrix_test.dag @@ -0,0 +1,193 @@ +module test.claim.fleet_revision_relation_wet_matrix + +import std.types { Bool, String } +import extdeps.git.object_store { GitObjectId, git_sha1_object_id, git_object_id_eq } +import gunbc.live_deploy.revision { + DeployRevisionRelation, + SameRevision, + DeployedIsAncestor, + CandidateIsAncestor, + UnrelatedHistories, + RelationUnverifiable, +} +import gunbc.fleet_main_revision { FleetRevisionRelationObservation } +import gunbc.fleet_desired_observe { observe_fleet_revision_relation_in } +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// THIS FILE DOES NOT RUN IN THE REQUIRED FLOOR TODAY, AND THAT IS STATED FIRST BECAUSE THE +// OPPOSITE IS THE NATURAL ASSUMPTION FOR A GREEN WITNESS FILE. It is a wet/replay class: every +// dispatching row reaches git.Inspect.MergeBase, which publishes no mock_response, so under the +// hermetic envelope the run REFUSES by construction rather than skipping. Its exclusion row and +// substantiated reason live in gunbc.ci_layer_roots; the local recipe is beside them. +// +// WHY IT CANNOT SIMPLY BE ENROLLED, established by reading the carrier rather than assumed: the +// replay binding that WOULD carry recorded observations into a hermetic run is +// v2.std.witness_evaluation `WitnessEvaluationFrame`, and its fixture list is `rest_fixtures: +// List` -- REST-shaped. Its own note says filesystem and environment replay +// bindings are meant to extend that carrier later. There is no shell-transport fixture carrier, so +// a recorded git observation has no way into a floor run; the external `--fixture-store` that this +// file's recipe uses is a claim_batch flag and claim_executor has no equivalent. NEXT-RUNG +// TRIGGER: a shell/service fixture arm on WitnessEvaluationFrame, at which point these rows enroll +// unchanged and the exclusion row deletes. Until then the coverage question for this composition +// answers NO, and the receipt is local. +// +// THE EFFECTFUL OBSERVER, EXERCISED END TO END AGAINST A CONTROLLED REPOSITORY. +// +// What was already proven before this file: the pure fold, by authored exit codes; and +// git.Inspect.MergeBase itself, by record/replay. What was NOT proven is the composition between +// them -- observe_fleet_revision_relation_in -> MergeBase -> fleet_revision_relation_from_merge_base +// -- which is where a wrong operand order, a dropped trim, or a mis-decoded stdout would live. A +// fold fed authored inputs cannot catch any of those, because authoring the inputs is precisely the +// step under test. +// +// THE FIXTURE GRAPH, built by docs recipe with fixed identities and timestamps so the object ids +// are reproducible (they participate in the operation input hash, so a machine-dependent id would +// make the recorded fixtures unportable): +// +// B main +// / +// A ──┤ base-a +// \ +// C sibling +// +// D orphan -- an independent root, no common ancestor with anything above +// +// EVERY COMMIT CARRIES A REF ON PURPOSE. C was originally created on a detached HEAD, which left it +// unreachable; merge-base still answered because the object had not been collected yet. A fixture +// whose correctness depends on gc not having run is not a fixture, so each of the four commits is +// named by a branch. +// +// THE SEVEN CASES COVER EVERY EXIT THE OPERATION DECLARES AND EVERY RELATION THE FOLD PRODUCES. +// Three exit-0 shapes (base is current / base is accepted / base is neither), the exit-1 answer, +// and two distinct routes to exit 128 -- a valid-looking object that is absent, and a path that is +// not a repository. The last one matters because it is the case that would silently become +// "unrelated" if a consumer read a Bool instead of the exit code. + +data fixture_repository_path: String = "target/test-fixtures/fleet-revision-relation" + +data non_repository_path: String = "target/test-fixtures/not-a-repository" + +data revision_a_hex: String = "3728e5635c811256194971bcaed367914a6040e6" + +data revision_b_hex: String = "3ad80d79bd1f64a7f75e121d7323aed053a81f0b" + +data revision_c_hex: String = "d0d3a7f6e323428bd771a32b1a19554481e1ae7c" + +data revision_d_hex: String = "8286843fce4511d0157573ba33b48ba46e48958a" + +// A well-formed object id that the fixture repository does not contain. It must be DECODABLE, or +// the probe would never be dispatched and the case would prove nothing about exit 128. +data revision_absent_hex: String = "1111111111111111111111111111111111111111" + +fn rev(hex: String) -> GitObjectId? { git_sha1_object_id(hex: hex) } + +fn relation_in(repository_path: String, current_hex: String, accepted_hex: String) -> DeployRevisionRelation? { + match rev(hex: current_hex) { + Present { value: cur } => + match rev(hex: accepted_hex) { + Present { value: acc } => + match observe_fleet_revision_relation_in( + repository_path: repository_path, + current: cur, + accepted: acc, + ) { + FleetRevisionRelationObservation { current: c, accepted: a, relation: rel } => + if git_object_id_eq(left: c, right: cur) && git_object_id_eq(left: a, right: acc) { + Present { value: rel } + } else { + none + } + } + none => none + } + none => none + } +} + +fn is_same(r: DeployRevisionRelation?) -> Bool { + match r { Present { value: SameRevision } => true _ => false } +} + +fn is_deployed_ancestor(r: DeployRevisionRelation?) -> Bool { + match r { Present { value: DeployedIsAncestor } => true _ => false } +} + +fn is_candidate_ancestor(r: DeployRevisionRelation?) -> Bool { + match r { Present { value: CandidateIsAncestor } => true _ => false } +} + +fn is_unrelated(r: DeployRevisionRelation?) -> Bool { + match r { Present { value: UnrelatedHistories } => true _ => false } +} + +fn is_unverifiable(r: DeployRevisionRelation?) -> Bool { + match r { + Present { value: RelationUnverifiable { cause: _ } } => true + _ => false + } +} + +// CASE 1 -- IDENTICAL REVISIONS SHORT-CIRCUIT BEFORE ANY DISPATCH. This is also the fixture-store +// control that must pass with an EMPTY store: if it ever needs a recorded fixture, the equality +// check has stopped happening before the probe and every no-op admission has started paying a +// subprocess. +test fn identical_revisions_are_converged_without_dispatching_a_probe() -> Bool { + is_same(r: relation_in(repository_path: fixture_repository_path, current_hex: revision_b_hex, accepted_hex: revision_b_hex)) +} + +// CASE 1b -- THE SHORT-CIRCUIT DOES NOT DEPEND ON THE REPOSITORY EXISTING. Same inputs, a path that +// is not a repository. Still converged, because git was never asked. +test fn identical_revisions_converge_even_when_the_path_is_not_a_repository() -> Bool { + is_same(r: relation_in(repository_path: non_repository_path, current_hex: revision_b_hex, accepted_hex: revision_b_hex)) +} + +// CASE 2 -- THE ORDINARY FORWARD ADVANCE. A is an ancestor of B, so the merge base IS the current +// revision. +test fn an_ancestor_current_is_a_forward_advance() -> Bool { + is_deployed_ancestor(r: relation_in(repository_path: fixture_repository_path, current_hex: revision_a_hex, accepted_hex: revision_b_hex)) +} + +// CASE 3 -- SUPERSEDED. The merge base IS the accepted revision, so the fleet already carries +// something newer and this run must do nothing and exit zero. +test fn an_ancestor_accepted_is_superseded() -> Bool { + is_candidate_ancestor(r: relation_in(repository_path: fixture_repository_path, current_hex: revision_b_hex, accepted_hex: revision_a_hex)) +} + +// CASE 4 -- DIVERGED, WITH A SHARED ANCESTOR. Exit 0 and a real merge base (A), which is NEITHER +// endpoint. This is the case whose receipt used to claim a disjoint history. +test fn siblings_sharing_an_ancestor_are_neither_ancestor_of_the_other() -> Bool { + is_unrelated(r: relation_in(repository_path: fixture_repository_path, current_hex: revision_b_hex, accepted_hex: revision_c_hex)) +} + +// CASE 5 -- NO COMMON ANCESTOR AT ALL. Exit 1, which is an ANSWER: git looked and there is none. +// It folds to the same refusal as case 4 today, and the two are deliberately distinguishable +// upstream at MergeBaseOutcome. +test fn an_orphan_root_has_no_common_ancestor() -> Bool { + is_unrelated(r: relation_in(repository_path: fixture_repository_path, current_hex: revision_b_hex, accepted_hex: revision_d_hex)) +} + +// CASE 6 -- A DECODABLE OBJECT ID THE REPOSITORY DOES NOT HOLD. Exit 128. The distinction from +// case 5 is the whole point: "there is no merge base" and "I could not look" must not collapse, +// because one refuses a real divergence and the other refuses an unreadable repository. +test fn an_absent_object_is_unverifiable_not_unrelated() -> Bool { + is_unverifiable(r: relation_in(repository_path: fixture_repository_path, current_hex: revision_b_hex, accepted_hex: revision_absent_hex)) +} + +// CASE 7 -- A PATH THAT IS NOT A REPOSITORY, with two revisions that ARE genuinely related in the +// real fixture. Exit 128 again, by a different route. If this ever answered a relation, the +// observation would be reading some other repository -- exactly the ambiguity that naming the +// repository on the operation removed. +test fn a_non_repository_path_is_unverifiable_rather_than_answering() -> Bool { + is_unverifiable(r: relation_in(repository_path: non_repository_path, current_hex: revision_b_hex, accepted_hex: revision_c_hex)) +} + +// THE DISCRIMINATING PAIR ACROSS CASES 5 AND 6, asserted as one row so it cannot be half-satisfied. +// Both refuse; they must refuse DIFFERENTLY. A consumer reading the operation's `success: Bool` +// instead of its exit code cannot tell these apart at all, which is the live residual recorded on +// MergeBaseOutcome. +test fn no_merge_base_and_could_not_look_stay_distinguishable() -> Bool { + is_unrelated(r: relation_in(repository_path: fixture_repository_path, current_hex: revision_b_hex, accepted_hex: revision_d_hex)) + && is_unverifiable(r: relation_in(repository_path: fixture_repository_path, current_hex: revision_b_hex, accepted_hex: revision_absent_hex)) +} diff --git a/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/605c5419d7d5b517.json b/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/605c5419d7d5b517.json new file mode 100644 index 00000000000..349795f7d8e --- /dev/null +++ b/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/605c5419d7d5b517.json @@ -0,0 +1,50 @@ +{ + "operation": "git.Inspect.MergeBase", + "input_hash": "605c5419d7d5b517", + "inputs": [ + { + "name": "repository_path", + "value": { + "__tag": "Str", + "value": "target/test-fixtures/fleet-revision-relation" + } + }, + { + "name": "left", + "value": { + "__tag": "Str", + "value": "3ad80d79bd1f64a7f75e121d7323aed053a81f0b" + } + }, + { + "name": "right", + "value": { + "__tag": "Str", + "value": "1111111111111111111111111111111111111111" + } + } + ], + "response": { + "__tag": "Record", + "__type": "MergeBase", + "fields": { + "exit_code": { + "__tag": "Int", + "value": 128 + }, + "sha": { + "__tag": "Str", + "value": "" + }, + "stderr": { + "__tag": "Str", + "value": "fatal: Not a valid commit name 1111111111111111111111111111111111111111" + }, + "success": { + "__tag": "Bool", + "value": false + } + } + }, + "recorded_at": 1787332539 +} \ No newline at end of file diff --git a/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/69a63cdcf2f7e5ed.json b/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/69a63cdcf2f7e5ed.json new file mode 100644 index 00000000000..82a58bfa7a5 --- /dev/null +++ b/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/69a63cdcf2f7e5ed.json @@ -0,0 +1,50 @@ +{ + "operation": "git.Inspect.MergeBase", + "input_hash": "69a63cdcf2f7e5ed", + "inputs": [ + { + "name": "repository_path", + "value": { + "__tag": "Str", + "value": "target/test-fixtures/fleet-revision-relation" + } + }, + { + "name": "left", + "value": { + "__tag": "Str", + "value": "3ad80d79bd1f64a7f75e121d7323aed053a81f0b" + } + }, + { + "name": "right", + "value": { + "__tag": "Str", + "value": "8286843fce4511d0157573ba33b48ba46e48958a" + } + } + ], + "response": { + "__tag": "Record", + "__type": "MergeBase", + "fields": { + "exit_code": { + "__tag": "Int", + "value": 1 + }, + "sha": { + "__tag": "Str", + "value": "" + }, + "stderr": { + "__tag": "Str", + "value": "" + }, + "success": { + "__tag": "Bool", + "value": false + } + } + }, + "recorded_at": 1787332539 +} \ No newline at end of file diff --git a/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/7be9704682d60499.json b/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/7be9704682d60499.json new file mode 100644 index 00000000000..5f8620b03e5 --- /dev/null +++ b/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/7be9704682d60499.json @@ -0,0 +1,50 @@ +{ + "operation": "git.Inspect.MergeBase", + "input_hash": "7be9704682d60499", + "inputs": [ + { + "name": "repository_path", + "value": { + "__tag": "Str", + "value": "target/test-fixtures/not-a-repository" + } + }, + { + "name": "left", + "value": { + "__tag": "Str", + "value": "3ad80d79bd1f64a7f75e121d7323aed053a81f0b" + } + }, + { + "name": "right", + "value": { + "__tag": "Str", + "value": "d0d3a7f6e323428bd771a32b1a19554481e1ae7c" + } + } + ], + "response": { + "__tag": "Record", + "__type": "MergeBase", + "fields": { + "exit_code": { + "__tag": "Int", + "value": 128 + }, + "sha": { + "__tag": "Str", + "value": "" + }, + "stderr": { + "__tag": "Str", + "value": "fatal: Not a valid commit name 3ad80d79bd1f64a7f75e121d7323aed053a81f0b" + }, + "success": { + "__tag": "Bool", + "value": false + } + } + }, + "recorded_at": 1787332539 +} \ No newline at end of file diff --git a/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/b264da0c183bb7fd.json b/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/b264da0c183bb7fd.json new file mode 100644 index 00000000000..561ddf9c3b5 --- /dev/null +++ b/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/b264da0c183bb7fd.json @@ -0,0 +1,50 @@ +{ + "operation": "git.Inspect.MergeBase", + "input_hash": "b264da0c183bb7fd", + "inputs": [ + { + "name": "repository_path", + "value": { + "__tag": "Str", + "value": "target/test-fixtures/fleet-revision-relation" + } + }, + { + "name": "left", + "value": { + "__tag": "Str", + "value": "3ad80d79bd1f64a7f75e121d7323aed053a81f0b" + } + }, + { + "name": "right", + "value": { + "__tag": "Str", + "value": "3728e5635c811256194971bcaed367914a6040e6" + } + } + ], + "response": { + "__tag": "Record", + "__type": "MergeBase", + "fields": { + "exit_code": { + "__tag": "Int", + "value": 0 + }, + "sha": { + "__tag": "Str", + "value": "3728e5635c811256194971bcaed367914a6040e6" + }, + "stderr": { + "__tag": "Str", + "value": "" + }, + "success": { + "__tag": "Bool", + "value": true + } + } + }, + "recorded_at": 1787332539 +} \ No newline at end of file diff --git a/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/c42cbc47c934d7ae.json b/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/c42cbc47c934d7ae.json new file mode 100644 index 00000000000..3ae8bb62899 --- /dev/null +++ b/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/c42cbc47c934d7ae.json @@ -0,0 +1,50 @@ +{ + "operation": "git.Inspect.MergeBase", + "input_hash": "c42cbc47c934d7ae", + "inputs": [ + { + "name": "repository_path", + "value": { + "__tag": "Str", + "value": "target/test-fixtures/fleet-revision-relation" + } + }, + { + "name": "left", + "value": { + "__tag": "Str", + "value": "3728e5635c811256194971bcaed367914a6040e6" + } + }, + { + "name": "right", + "value": { + "__tag": "Str", + "value": "3ad80d79bd1f64a7f75e121d7323aed053a81f0b" + } + } + ], + "response": { + "__tag": "Record", + "__type": "MergeBase", + "fields": { + "exit_code": { + "__tag": "Int", + "value": 0 + }, + "sha": { + "__tag": "Str", + "value": "3728e5635c811256194971bcaed367914a6040e6" + }, + "stderr": { + "__tag": "Str", + "value": "" + }, + "success": { + "__tag": "Bool", + "value": true + } + } + }, + "recorded_at": 1787332539 +} \ No newline at end of file diff --git a/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/c42f940ae04b9e50.json b/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/c42f940ae04b9e50.json new file mode 100644 index 00000000000..e107aca1a35 --- /dev/null +++ b/dag/test/fixtures/fleet-revision-relation/git__Inspect__MergeBase/c42f940ae04b9e50.json @@ -0,0 +1,50 @@ +{ + "operation": "git.Inspect.MergeBase", + "input_hash": "c42f940ae04b9e50", + "inputs": [ + { + "name": "repository_path", + "value": { + "__tag": "Str", + "value": "target/test-fixtures/fleet-revision-relation" + } + }, + { + "name": "left", + "value": { + "__tag": "Str", + "value": "3ad80d79bd1f64a7f75e121d7323aed053a81f0b" + } + }, + { + "name": "right", + "value": { + "__tag": "Str", + "value": "d0d3a7f6e323428bd771a32b1a19554481e1ae7c" + } + } + ], + "response": { + "__tag": "Record", + "__type": "MergeBase", + "fields": { + "exit_code": { + "__tag": "Int", + "value": 0 + }, + "sha": { + "__tag": "Str", + "value": "3728e5635c811256194971bcaed367914a6040e6" + }, + "stderr": { + "__tag": "Str", + "value": "" + }, + "success": { + "__tag": "Bool", + "value": true + } + } + }, + "recorded_at": 1787332539 +} \ No newline at end of file diff --git a/docs/plans/fleet-revision-relation-fixture.md b/docs/plans/fleet-revision-relation-fixture.md new file mode 100644 index 00000000000..1bae70ca890 --- /dev/null +++ b/docs/plans/fleet-revision-relation-fixture.md @@ -0,0 +1,119 @@ +# The fleet-revision-relation fixture repository + +Rebuild recipe for the controlled git repository behind +`dag/test/claim/fleet_revision_relation_wet_matrix_test.dag`. + +## Why a fixture repository at all + +The pure merge-base fold is already witnessed by authored exit codes, and +`git.Inspect.MergeBase` itself is witnessed by record/replay. Neither covers the +*composition* — `observe_fleet_revision_relation_in` → `MergeBase` → +`fleet_revision_relation_from_merge_base` — which is where a swapped operand, a dropped +`trim`, or a mis-decoded stdout would live. A fold fed authored inputs cannot catch any of +those, because authoring the inputs is the step under test. + +## The graph + +``` + B main + / + A ──┤ base-a + \ + C sibling + + D orphan an independent root, no common ancestor with anything above +``` + +Every commit carries a branch **on purpose**. `C` was originally created on a detached +HEAD, which left it unreachable; `merge-base` still answered because the object had not +been collected yet. A fixture whose correctness depends on gc not having run is not a +fixture. + +## Recipe + +Identities and timestamps are fixed because the object ids participate in the operation +input hash: a machine-dependent id makes the recorded fixtures unportable. + +```sh +FX=target/test-fixtures/fleet-revision-relation +rm -rf "$FX"; mkdir -p "$FX" +export GIT_AUTHOR_NAME=fixture GIT_AUTHOR_EMAIL=fixture@invalid +export GIT_COMMITTER_NAME=fixture GIT_COMMITTER_EMAIL=fixture@invalid +export GIT_AUTHOR_DATE="2020-01-01T00:00:00+0000" +export GIT_COMMITTER_DATE="2020-01-01T00:00:00+0000" +git -C "$FX" init -q -b main +echo a > "$FX/f"; git -C "$FX" add -A; git -C "$FX" commit -q -m A +git -C "$FX" branch base-a +echo b > "$FX/f"; git -C "$FX" add -A; git -C "$FX" commit -q -m B +git -C "$FX" checkout -q -b sibling base-a +echo c > "$FX/f"; git -C "$FX" add -A; git -C "$FX" commit -q -m C +git -C "$FX" checkout -q --orphan orphan +echo d > "$FX/f"; git -C "$FX" add -A; git -C "$FX" commit -q -m D +git -C "$FX" checkout -q main + +mkdir -p target/test-fixtures/not-a-repository # case 7 needs a real non-repository path +``` + +Verified reproducible: two independent builds produced identical `show-ref` output. + +## Object roster + +| ref | commit | oid | +|---|---|---| +| `base-a` | A | `3728e5635c811256194971bcaed367914a6040e6` | +| `main` | B | `3ad80d79bd1f64a7f75e121d7323aed053a81f0b` | +| `sibling` | C | `d0d3a7f6e323428bd771a32b1a19554481e1ae7c` | +| `orphan` | D | `8286843fce4511d0157573ba33b48ba46e48958a` | +| — | absent, decodable | `1111111111111111111111111111111111111111` | + +The absent id must be **decodable**, or the probe is never dispatched and the case proves +nothing about exit 128. + +## The seven cases, and what each one is for + +| # | current, accepted | exit | relation | why it is in the matrix | +|---|---|---|---|---| +| 1 | B, B | — | `SameRevision` | short-circuits before any dispatch | +| 1b | B, B (non-repository path) | — | `SameRevision` | the short-circuit does not depend on the repository existing | +| 2 | A, B | 0, base = A | `DeployedIsAncestor` | ordinary forward advance; base **is** current | +| 3 | B, A | 0, base = A | `CandidateIsAncestor` | superseded; base **is** accepted | +| 4 | B, C | 0, base = A | `UnrelatedHistories` | diverged **with a shared ancestor** — the case whose receipt used to claim a disjoint history | +| 5 | B, D | 1 | `UnrelatedHistories` | no common ancestor; exit 1 is an **answer** | +| 6 | B, absent | 128 | `RelationUnverifiable` | could not look — must not collapse into 5 | +| 7 | B, C (non-repository path) | 128 | `RelationUnverifiable` | a second route to 128; if it ever answered a relation, the observation is reading some other repository | + +Cases 5 and 6 are additionally asserted as one row +(`no_merge_base_and_could_not_look_stay_distinguishable`) so the distinction cannot be +half-satisfied. A consumer reading the operation's `success: Bool` instead of its exit code +cannot tell them apart at all — the live residual recorded on `MergeBaseOutcome`. + +## Record, replay, and the controls + +Commands are in the exclusion row's dissolution description +(`gunbc.ci_layer_roots`, pattern `fleet_revision_relation_wet_matrix_test.dag`) so that the +recipe and the reason a reader is looking it up sit together. + +Measured results: + +- **record (wet)** — 9/9 PASS, 6 distinct fixtures written for `git.Inspect.MergeBase` + (six, not seven, because case 5 and case 6 each appear twice across the nine rows). +- **replay (hermetic, exact store)** — 9/9 PASS. +- **control: empty store** — the two short-circuit rows still PASS; the other seven FAIL + with `missing recorded fixture`, each naming a **distinct** input hash. This is what + proves the passing replay consumed recorded observations rather than reaching live git, + and separately proves the short-circuit is real. +- **control: wrong input hash** — one fixture renamed to a bogus hash, the rest left in + place. Its case refuses with its own exact hash while a sibling case still passes from + the same store. The store is an exact observation map, not a nearest-match catalog. + +The recorded `inputs` array includes `repository_path`, which is the direct evidence that +the repository participates in the key rather than being ambient. + +## What this does not cover + +The file does not run in the required floor. `git.Inspect.MergeBase` publishes no +`mock_response`, and there is no way to hand recorded shell observations to a floor run: +`WitnessEvaluationFrame` carries only `rest_fixtures`, and `--fixture-store` is a +`claim_batch` flag with no `claim_executor` equivalent. The exclusion row carries the +substantiated reason and the dissolution trigger — a shell/service fixture arm on +`WitnessEvaluationFrame`, after which these rows enroll unchanged.