Skip to content
9 changes: 9 additions & 0 deletions dag/gunbc/rung_drop/required_gate_bankruptcy.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,15 @@ module gunbc.rung_drop.required_gate_bankruptcy
import std.types { NonEmptyStr }
import gunbc.rung_drop { RungDrop, Standing, AuthoredProse, RequiredGateBankruptcy }

// WORKFLOW-COUNTABLE PARTIAL CLIMB (2026-09-04): the exact module
// `test.claim.witness_floor_workflow_consolidation_witness_test` joins the static roster because
// three standing drops cite one of its rows as their required-path countable. This restores
// recurring execution for four previously unheld identities in that one module. It follows the
// 2026-08-31 generated-artifact partial-climb precedent and DOES NOT RETIRE THIS DROP: it moves
// the static population, while the restoration trigger remains a required run deriving its
// population from the change over the whole corpus. The roster header records the measured
// import-closure, strict-preparation, and per-claim wall-clock price from run 33899564106.

data required_gate_bankruptcy: RungDrop = RungDrop {
identity: "required_gate_bankruptcy" as NonEmptyStr,

Expand Down
51 changes: 44 additions & 7 deletions dag/gunbc/witness/witness_floor_workflow.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1643,13 +1643,15 @@ fn witness_floor_capability_closure_holds() -> Bool {
// which have no automated consumer, so it is run deliberately or not at all. A declared scope
// narrowing, not a climb; naming it here keeps its absence from reading as coverage.

fn witness_floor_lane_needs() -> List<String> { [] }

fn witness_floor_job() -> Job {
Job {
id: floor_lane_job_id,
name: none,
runner: gunbc_ci_selected_runner_spec(),
steps: witness_floor_steps(),
needs: [],
needs: witness_floor_lane_needs(),
env: none,
outputs: none,
if_condition: none,
Expand Down Expand Up @@ -2014,13 +2016,15 @@ fn heal_generated_artifacts_job() -> Job {
}
}

fn build_lane_needs() -> List<String> { [] }

fn build_lane_job() -> Job {
Job {
id: build_lane_job_id,
name: none,
runner: gunbc_ci_selected_runner_spec(),
steps: build_lane_steps(),
needs: [],
needs: build_lane_needs(),
env: none,
outputs: none,
if_condition: none,
Expand Down Expand Up @@ -2495,12 +2499,45 @@ fn witness_floor_triggers() -> List<WorkflowTrigger> {
// THE AGGREGATE IS DELIBERATELY NOT A MEMBER. It checks out nothing and runs no witness: it reads
// the other lanes' results. Every consumer of this list is asking about lanes that carry a subject,
// and the aggregate joined that population only as something to filter back out.
type WitnessFloorLane = WitnessFloorBuildLane | WitnessFloorFloorLane | WitnessFloorHealLane

fn witness_floor_lane_roster() -> FreeSemigroup<WitnessFloorLane> {
FreeSemigroup {
head: WitnessFloorBuildLane,
tail: [WitnessFloorFloorLane, WitnessFloorHealLane]
}
}

fn witness_floor_lane_job(lane: WitnessFloorLane) -> Job {
match lane {
WitnessFloorBuildLane => build_lane_job()
WitnessFloorFloorLane => witness_floor_job()
WitnessFloorHealLane => heal_generated_artifacts_job()
}
}

fn witness_floor_lane_jobs() -> List<Job> {
[
build_lane_job(),
witness_floor_job(),
heal_generated_artifacts_job()
]
list_map(xs: non_empty_to_list(xs: witness_floor_lane_roster()), f: fn(lane) {
witness_floor_lane_job(lane: lane)
})
}

// THE IDENTITY PROJECTION IS NARROW ON PURPOSE. A witness deciding which jobs exist must not
// materialize every job's steps (and therefore the compiler-floor command) merely to read ids.
// Both this projection and the materialized jobs derive from `witness_floor_lane_roster`, so an
// added lane cannot enter one without entering the other.
fn witness_floor_lane_job_id(lane: WitnessFloorLane) -> String {
match lane {
WitnessFloorBuildLane => build_lane_job_id
WitnessFloorFloorLane => floor_lane_job_id
WitnessFloorHealLane => heal_generated_artifacts_job_id
}
}

fn witness_floor_lane_job_ids() -> List<String> {
list_map(xs: non_empty_to_list(xs: witness_floor_lane_roster()), f: fn(lane) {
witness_floor_lane_job_id(lane: lane)
})
}

data witness_floor_workflow: Workflow = {
Expand Down
20 changes: 20 additions & 0 deletions dag/test/claim/discovery_census_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -273,6 +273,26 @@ test fn w_site_is_planned_when_no_home_matched() -> Bool {
}
}

// The three deleted-lane rung drops cite this exact identity as their countable. A prefix-only
// control over `v2.test.` cannot establish that a `test.claim.` workflow witness is admitted,
// and the prior absence left it discovered but declined on every required run. Pin the cited
// row, rather than a synthetic neighbour, so removing its exact-module gate admission reds.
test fn w_deleted_lane_countable_is_planned_by_the_required_gate() -> Bool {
match required_floor_site_disposition(
module_path: "test.claim.witness_floor_workflow_consolidation_witness_test",
identity: "test.claim.witness_floor_workflow_consolidation_witness_test.w_RED_the_deleted_lanes_do_not_return"
) {
Planned => true
DeclinedLongModule { matched_prefix: _ } => false
DeclinedFixtureMember { matched_prefix: _ } => false
DeclinedOutsideRequiredGate => false
DeclinedCostDebt => false
DeclinedOutsideGateClosure => false
DeclinedDiscoveryExcluded { matched_substring: _ } => false
PlannedAsChangedWitness => false
}
}

// THE GATE DECLINES ON THE AUTHORED MODULE NAME, and a product witness that is neither long nor
// a fixture member lands here rather than in Planned. This is the RED for the 2026-08-29 static
// required gate: before the arm existed this site was planned.
Expand Down
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
module test.claim.witness_floor_workflow_consolidation_witness_test

import std.types { Bool, String }
import std.types { Bool, List, String }
import v2.std.algebra { count_where, length, non_empty_to_list }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
import gunbc.witness_floor_workflow { expected_witness_floor_yml, WitnessFloorGenerated, WitnessFloorGenerationRefused, build_lane_job_id, floor_lane_job_id, witness_floor_workflow_job_id, required_ci_measurement_publish_condition, required_ci_measurement_bound_steps, witness_floor_run_step }
import gunbc.witness_floor_workflow { expected_witness_floor_yml, WitnessFloorGenerated, WitnessFloorGenerationRefused, build_lane_job_id, floor_lane_job_id, witness_floor_workflow_job_id, required_ci_measurement_publish_condition, required_ci_measurement_bound_steps, witness_floor_run_step, required_lanes_roster, witness_floor_lane_job_ids, build_lane_needs, witness_floor_lane_needs }
import gunbc.fabric_witness_run { required_ci_lane_build, required_ci_lane_witnesses }
import gunbc.required_lanes_gate { required_lanes_gate_unrenderable_stmts }
import gunbc.fleet_converge_workflow { fleet_converge_workflow }
Expand Down Expand Up @@ -268,22 +269,27 @@ test fn w_RED_lane_contexts_collide_with_no_other_emitted_workflow() -> Bool {
// necessarily carries a `needs` edge, so a row forbidding the token outright would have made
// the fail-closed repair unrepresentable.
//
// The claim is therefore stated at the grain that actually matters. A lane waiting on the other
// renders as that lane's job carrying `needs: [<other lane>]`, so both single-lane forms are
// refused; the aggregator's two-lane edge is required to be present. That is a strictly sharper
// discriminator than the token count was, because it distinguishes the serialization being
// forbidden from the aggregation being demanded, which "no needs anywhere" could not.
// The claim is therefore stated at the grain that actually matters. The typed lane jobs must
// carry no `needs`, while the one roster from which the aggregate derives its `needs` must carry
// exactly both lane identities. Reading those narrow producers avoids serializing the aggregate's
// large gate program merely to recover fields that existed before serialization. This remains a
// strictly sharper discriminator than the old token count: it distinguishes the serialization
// being forbidden from the aggregation being demanded, which "no needs anywhere" could not.
//
// It is a RED that can be authored in both directions: giving either lane job a `needs` row
// fails the negatives, and dropping the aggregator's fails the positive.
test fn w_RED_neither_lane_waits_on_the_other() -> Bool {
match expected_witness_floor_yml() {
WitnessFloorGenerated { content: yml } =>
string_contains(s: yml, pattern: concat("needs: [", concat(build_lane_job_id, concat(", ", concat(floor_lane_job_id, "]")))))
&& !string_contains(s: yml, pattern: concat("needs: [", concat(build_lane_job_id, "]")))
&& !string_contains(s: yml, pattern: concat("needs: [", concat(floor_lane_job_id, "]")))
WitnessFloorGenerationRefused { reason: _ } => false
}
length(xs: build_lane_needs()) == 0
&& length(xs: witness_floor_lane_needs()) == 0
&& length(xs: non_empty_to_list(xs: required_lanes_roster())) == 2
&& count_where(
xs: non_empty_to_list(xs: required_lanes_roster()),
predicate: fn(lane) { lane.job_id == build_lane_job_id },
) == 1
&& count_where(
xs: non_empty_to_list(xs: required_lanes_roster()),
predicate: fn(lane) { lane.job_id == floor_lane_job_id },
) == 1
}

// THE FABRIC LANE STILL RUNS AND NO LONGER GATES, AND THIS ROW ASSERTS BOTH HALVES.
Expand All @@ -294,21 +300,28 @@ test fn w_RED_neither_lane_waits_on_the_other() -> Bool {
// deliberately no longer true. It is not retired as obsolete -- the lane's restoration is still
// the drop's trigger -- it is restated at the subject the drop now covers.
//
// SO THE CLAIM IS ABSENCE, AND ABSENCE OF ALL THREE SPELLINGS RATHER THAN ONE. A diff that
// re-adds the job authors RED here; so does one that restores only the `needs` edge or only the
// FABRIC_EVIDENCE binding, because a lane that gates without running is the fail-open a skipped
// required check produces. The row goes green again only together with the drop's retirement,
// which is a measured wall and not a pull request.
// SO THE CLAIM IS ABSENCE AT THE TYPED PRODUCERS rather than after whole-workflow serialization.
// A diff that re-adds any deleted job authors RED here; so does one that restores only the
// FABRIC_EVIDENCE roster binding, because a lane that gates without running is the fail-open a
// skipped required check produces. The row goes green again only together with the drop's
// retirement, which is a measured wall and not a pull request.
// POSITIVE-CONTROL SEAM: the countable must author RED when a deleted lane is supplied. Without
// this input boundary, a planned/pass receipt would not distinguish a live absence wall from a
// vacuous projection that always returned an empty list.
fn deleted_lane_job_ids_are_absent(job_ids: List<String>) -> Bool {
!any(xs: job_ids, predicate: fn(job_id) {
job_id == "fabric-evidence"
|| job_id == "rust-unit-tests"
|| job_id == "emit-copy-qualification-battery"
})
}

test fn w_RED_the_deleted_lanes_do_not_return() -> Bool {
match expected_witness_floor_yml() {
WitnessFloorGenerated { content: yml } =>
!string_contains(s: yml, pattern: "\n fabric-evidence:")
&& !string_contains(s: yml, pattern: "FABRIC_EVIDENCE")
&& !string_contains(s: yml, pattern: "bash tools/fabric_ci_evidence_calibration.sh")
&& !string_contains(s: yml, pattern: "\n rust-unit-tests:")
&& !string_contains(s: yml, pattern: "\n emit-copy-qualification-battery:")
WitnessFloorGenerationRefused { reason: _ } => false
}
deleted_lane_job_ids_are_absent(job_ids: witness_floor_lane_job_ids())
&& deleted_lane_job_ids_are_absent(job_ids: ["fabric-evidence"])
&& !any(xs: non_empty_to_list(xs: required_lanes_roster()), predicate: fn(lane) {
lane.var_name == "FABRIC_EVIDENCE"
})
}

// THE GATE RUNS FOR EVERY ATTEMPT, INCLUDING A CANCELLED ONE, AND THEN REFUSES A NON-SUCCESS
Expand Down
29 changes: 29 additions & 0 deletions src/v2/workflow/required_floor.dag
Original file line number Diff line number Diff line change
Expand Up @@ -550,13 +550,42 @@ fn required_gate_prefixes() -> List<String> {
"test.claim.legacy_binding_",
"test.claim.compiler_frontend_program_status_witness",
"test.claim.discovery_census_witness_test",
"test.claim.witness_floor_workflow_consolidation_witness_test",
"test.claim.host_budget_source_witness",
"test.claim.typed_module_cache_capacity_witness",
"test.claim.whole_corpus_compile_admission_witness",
"test.claim.memory_stall_refusal_witness",
]
}

// THE WORKFLOW-CONSOLIDATION MODULE IS ADMITTED AT EXACT MODULE GRAIN. Three declared rung
// drops cite its `w_RED_the_deleted_lanes_do_not_return` row as the countable refusal if a cut
// CI lane returns. Before this row, the required floor discovered all 12 witnesses in that
// module but dispositioned every one `DeclinedOutsideGateClosure`; eight happened also to be
// named by the cost-debt roster, while the other four had no executing recurring path at all.
// The run log's bounded presentation showed only the eight rostered identities, but run
// 33889629622's authoritative disposition artifact contains all 12, so the loss is module-wide
// preparation and the unheld population is four -- not a four-row discovery failure.
//
// This exact module belongs under the compiler-floor ruling because it judges the emitted
// required workflow and aggregate that execute the compiler floor. A broader `test.claim.witness_`
// prefix would also admit product and operational witnesses the ruling explicitly moved off the
// gate. The existing eight cost-debt identities remain withheld by their own authority; this
// admission makes the other four execute, including the rung drops' named countable.
//
// THIS IS A PARTIAL CLIMB UNDER `gunbc.rung_drop.required_gate_bankruptcy`, not its retirement.
// It follows that row's 2026-08-31 generated-artifact partial-climb precedent: one exact class is
// restored and the static population moves. The standing drop's trigger remains a required run
// deriving its population from the change with the whole corpus as universe; neither this exact
// widening, another static widening, nor a faster static gate fires it. PRICE, from this change's
// first required-floor receipts (run 33899564106): the admitted import closure resolved 2,339
// modules versus 2,209 in the adjacent predecessor run 33889629622 (+130); strict preparation was
// 635,645ms versus 630,511ms (+5,134ms, an adjacent-run observation rather than a causal claim).
// The four newly planned claims cost 1ms, 54ms, and at least 507ms and 510ms CPU respectively; the
// latter two were right-censored by the 500ms claim ceiling and are narrowed at their typed
// producers in the same change. The green receipt from run 33907907019 prices the resulting four
// executions at 1ms, 59ms, 457ms, and 451ms CPU; all four were planned and passed.

// test.claim.memory_stall_refusal_witness JOINS THE SAME FAMILY BY THE SAME TEST: it judges
// the arm that stops a resolve which is thrashing instead of computing (gunbc.
// memory_stall_refusal), which is the state the three modules below cannot see -- budget
Expand Down
Loading