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
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 @@ -1644,13 +1644,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 @@ -2039,13 +2041,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 @@ -2520,12 +2524,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,32 @@ 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.
//
// PERMANENT AFTER OBSERVED RED (DESIGN 4b(4)). Run 33924210916 supplied `fabric-evidence` and
// observed this exact identity return Bool(false). This probe is therefore a regression control,
// not scaffolding: keep it enrolled for as long as any of the three citing rung drops stands.
// 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