Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 9 additions & 7 deletions dag/gunbc/live_deploy/spec.dag
Original file line number Diff line number Diff line change
Expand Up @@ -548,13 +548,15 @@ fn deployment_credential_env_path(names: DeploymentNames) -> NonEmptyStr {
// so a `git config` from the apply is EACCES on one side and outside the six sudo grants on the
// other. That argues for the tree-sync unit, which already has the right principal.
//
// It cannot be the tree-sync unit. That unit is installed and started inside the GunbcSourceTree
// step, which is FIRST in deployment_owned_steps, while ServeBinary is second -- so on a fresh
// instance the gunbc binary the convergence invokes does not exist yet, and the leg would red the
// first deploy of every new slot. Ordering the member AFTER ServeBinary is what makes the binary a
// precondition the membership itself establishes.
// It cannot be the tree-sync unit. That unit was installed and started inside the GunbcSourceTree
// step, and when this member was written that step came FIRST in deployment_owned_steps with
// ServeBinary second -- so on a fresh instance the gunbc binary the convergence invokes did not
// exist yet, and the leg would red the first deploy of every new slot. Ordering the member AFTER
// ServeBinary is what makes the binary a precondition the membership itself establishes. (The two
// have since swapped -- deployment_steps_apply_order says why binary now lands before the tree --
// and this member's position after BOTH is unchanged by that.)
//
// It sits THIRD -- immediately after GunbcSourceTree and ServeBinary, and before the belt timer.
// It sits THIRD -- immediately after ServeBinary and GunbcSourceTree, and before the belt timer.
// An earlier cut of this change said "last" and placed it last; that was an inversion of
// the rule deployment_steps_apply_order's annotation states, that dependencies precede their
// consumers, because the
Expand All @@ -563,7 +565,7 @@ fn deployment_credential_env_path(names: DeploymentNames) -> NonEmptyStr {
// position satisfying the fresh-instance constraint above, so it satisfies both; last satisfied
// only one. Witness: deployed_tree_remote_witness_test
// `the_remote_converges_after_its_inputs_and_before_the_belt` pins the sequence
// tree,binary,remote,belt,route.
// binary,tree,remote,publication,belt,route.
fn deployment_tree_remote_unit_name(names: DeploymentNames) -> NonEmptyStr {
join([deployment_belt_unit_stem(names: names), "-tree-remote.service"], "") as NonEmptyStr
}
Expand Down
9 changes: 8 additions & 1 deletion dag/test/claim/deployed_tree_remote_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -212,6 +212,13 @@ test fn only_an_exact_read_back_reports_success() -> Bool {
// concern that put it last to begin with — so this position satisfies both constraints, and the
// original placement satisfied only one.
//
// THE ORDER OF THOSE TWO IS NOT THIS CLAIM'S SUBJECT, and the expectation below no longer pins it
// the wrong way round. gunbc.live_deploy.spec deployment_steps_apply_order states binary-then-tree
// -- the tree is published by a service-user oneshot that RUNS the admitted binary (review on
// PR #10696) -- and this expectation kept the older tree-then-binary spelling, so it was red against
// its own authority with no production defect behind it. What the claim discriminates is unchanged:
// the remote after both of its inputs and before the publication helper and the belt.
//
// Asserted as a filtered SEQUENCE rather than absolute indices, so inserting an unrelated member
// leaves this green while a genuine reordering reds it.
//
Expand Down Expand Up @@ -255,5 +262,5 @@ fn ordered_tags() -> List<String> {
}

test fn the_remote_converges_after_its_inputs_and_before_the_belt() -> Bool {
join(ordered_tags(), ",") == "tree,binary,remote,publication,belt,route"
join(ordered_tags(), ",") == "binary,tree,remote,publication,belt,route"
}
22 changes: 20 additions & 2 deletions dag/test/claim/harness_seat_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ import gunbc.harness.harness_seat {
harness_seat_partition, SeatCeilingByDeclaredPolicy, AdmissionCeilingUnestablished,
harness_seat_capacity, harness_interactive_quality_seats, harness_seat_reference,
}
import gunbc.serving.serving_enrollment { serving_route_ceiling, serving_route_turn_ceiling_count }
import gunbc.harness.harness_cli {
harness_seat_policy, harness_request_deadline, harness_seat_release_allowance_seconds,
}
Expand All @@ -34,6 +35,12 @@ fn w_tolerant_ceiling(group: FabricGroup) -> Int {
}
}

// The route's own declared allocation, read from the row that owns it, so the claims below compare
// the harness's reading against its authority rather than against a copy of it.
fn w_route_ceiling(group: FabricGroup) -> Int {
serving_route_turn_ceiling_count(c: serving_route_ceiling(group: group))
}

// The engine's OWN scheduler count limit, read straight off the desired unit. This witness needs it
// only to prove the seat ceiling is NOT it.
fn w_engine_max_num_seqs(group: FabricGroup) -> Int {
Expand Down Expand Up @@ -120,9 +127,20 @@ test fn the_quality_ceiling_is_one_and_is_not_a_capacity_claim() -> Bool {
// halves are asserted, and the tolerant one is asserted DIFFERENT from the desired unit's
// max_num_seqs -- the stale launch-line reading this lane declined to inherit -- so a future edit
// that quietly re-derived it from that row goes red here.
//
// THE TOLERANT NUMBERS ARE READ FROM THE ROW THAT OWNS THEM, NOT TRANSCRIBED. This claim used to
// spell 4 and 1 for groups A and B; gunbc.serving.serving_enrollment serving_group_b_route_turn_ceiling
// was then superseded 1 -> 4 (#11617, 2026-09-18) and the copy here went red against a legitimate
// change while asserting nothing the copy was needed for. What the claim discriminates is the ROUTE
// of the number: the harness pool's ceiling is the route's declared allocation (serving_route_ceiling),
// not harness_interactive_quality_seats and not the engine's max_num_seqs. A build that re-read the
// ceiling off the desired unit fails the last conjunct; one that fused the two classes fails the
// tolerant-differs-from-quality conjunct; the row moving no longer fails anything, which is the
// point of not copying it.
test fn the_tolerant_pool_is_a_separate_pool_whose_ceiling_is_not_the_engines_sequence_limit() -> Bool {
w_tolerant_ceiling(group: FabricGroupA) == 4
&& w_tolerant_ceiling(group: FabricGroupB) == 1
w_tolerant_ceiling(group: FabricGroupA) == w_route_ceiling(group: FabricGroupA)
&& w_tolerant_ceiling(group: FabricGroupB) == w_route_ceiling(group: FabricGroupB)
&& w_tolerant_ceiling(group: FabricGroupA) != w_ceiling(group: FabricGroupA)
&& w_ceiling(group: FabricGroupA) == 1
&& w_ceiling(group: FabricGroupB) == 1
&& w_tolerant_ceiling(group: FabricGroupA) != w_engine_max_num_seqs(group: FabricGroupA)
Expand Down