From 3bf84fc8bd82bf90af9059611f77403ffaa83ef5 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 20 Sep 2026 07:31:45 +0000 Subject: [PATCH 1/2] Two witnesses drifted from legitimate changes: the deploy-order oracle pinned tree,binary; the seat oracle copied group B's ceiling Both reds reproduce from source on main and both are oracle drift, not production defects (DESIGN 6b: the earliest unjustified boundary is the transcription in the witness, every upstream contract holds). - test.claim.deployed_tree_remote_witness the_remote_converges_after_its_inputs_and_before_the_belt pinned the sequence tree,binary,... while gunbc.live_deploy.spec deployment_steps_apply_order states binary-then-tree with its reason (the tree is published by a oneshot that RUNS the admitted binary, review on #10696). The claim's own annotation never made the order of those two its subject. The literal now follows the authority, and the stale prose on deployment_tree_remote_unit_name is corrected to match. - test.claim.harness_seat_witness the_tolerant_pool_is_a_separate_pool_whose_ceiling_is_not_the_engines_sequence_limit transcribed group B's tolerant ceiling as 1 after #11617 superseded gunbc.serving.serving_enrollment serving_group_b_route_turn_ceiling to 4 (and updated serving_routing_witness but not this one). The copy is removed rather than re-copied: the claim now asserts the harness pool ceiling equals serving_route_turn_ceiling_count(serving_route_ceiling) for each group -- the ROUTE of the number is the subject -- and keeps != quality ceiling and != engine max_num_seqs as the discriminators. The two serve-unit oracle claims reported red at 43643bad4f were already repaired by #11484 (after that base): at the base the oracle pinned --host 0.0.0.0 / --eval-budget-wall-ms 30000 while production rendered 127.0.0.1 / 120000. #11723 is a descendant of that base and did not cause them. No change to those claims here. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/live_deploy/spec.dag | 16 +++++++------- .../deployed_tree_remote_witness_test.dag | 9 +++++++- dag/test/claim/harness_seat_witness_test.dag | 21 +++++++++++++++++-- 3 files changed, 36 insertions(+), 10 deletions(-) diff --git a/dag/gunbc/live_deploy/spec.dag b/dag/gunbc/live_deploy/spec.dag index ef7fb1ab855..dd41e64bcb5 100644 --- a/dag/gunbc/live_deploy/spec.dag +++ b/dag/gunbc/live_deploy/spec.dag @@ -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 @@ -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 } diff --git a/dag/test/claim/deployed_tree_remote_witness_test.dag b/dag/test/claim/deployed_tree_remote_witness_test.dag index 5196710a357..27806c280a6 100644 --- a/dag/test/claim/deployed_tree_remote_witness_test.dag +++ b/dag/test/claim/deployed_tree_remote_witness_test.dag @@ -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. // @@ -255,5 +262,5 @@ fn ordered_tags() -> List { } 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" } diff --git a/dag/test/claim/harness_seat_witness_test.dag b/dag/test/claim/harness_seat_witness_test.dag index 89321f86c98..c8cd88bd3b4 100644 --- a/dag/test/claim/harness_seat_witness_test.dag +++ b/dag/test/claim/harness_seat_witness_test.dag @@ -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, } @@ -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 { @@ -120,9 +127,19 @@ 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 +// second; 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) From afd7ae9671859634a37caa77d3f5c6949ee551ab Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 20 Sep 2026 08:01:20 +0000 Subject: [PATCH 2/2] harness_seat_witness: name the conjunct a class fusion fails (review nit) Co-Authored-By: Claude Opus 5 (1M context) --- dag/test/claim/harness_seat_witness_test.dag | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/dag/test/claim/harness_seat_witness_test.dag b/dag/test/claim/harness_seat_witness_test.dag index c8cd88bd3b4..9e9de9cd756 100644 --- a/dag/test/claim/harness_seat_witness_test.dag +++ b/dag/test/claim/harness_seat_witness_test.dag @@ -135,7 +135,8 @@ test fn the_quality_ceiling_is_one_and_is_not_a_capacity_claim() -> Bool { // 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 -// second; the row moving no longer fails anything, which is the point of not copying it. +// 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) == w_route_ceiling(group: FabricGroupA) && w_tolerant_ceiling(group: FabricGroupB) == w_route_ceiling(group: FabricGroupB)