diff --git a/dag/gunbc/required_lanes_gate.dag b/dag/gunbc/required_lanes_gate.dag index 0c3c26c647f..dd03f8e233d 100644 --- a/dag/gunbc/required_lanes_gate.dag +++ b/dag/gunbc/required_lanes_gate.dag @@ -12,7 +12,7 @@ import v2.extdeps.languages.bash_build { bash_build_word_lit, bash_build_word_var } -import v2.std.algebra { list_append } +import v2.std.algebra { FreeSemigroup, fold_list, list_append, list_flat_map } import gunbc.floor_attempt_standing { floor_attempt_receipt_prefix, floor_attempt_receipt_measured_head_label, @@ -193,6 +193,88 @@ fn required_lanes_head_standing_stmts( ] } +// THE REQUIRED LANE, AS ONE CONCEPT WITH N INSTANCES RATHER THAN N NAMED PARAMETERS. +// +// This axis was a HARDCODED PAIR -- `build_var` beside `floor_var`, threaded through four +// functions and spelled 28 times -- which is one concept given one name per instance, the fork +// DESIGN section 2 horizontal exists to delete. The tell was mechanical: promoting a third job +// into the aggregate was described by `gunbc.witness_floor_workflow` as a one-row edit, and was +// in fact a signature change in four places plus a step-name rewrite, because the gate could not +// say "a lane" at all -- only "the build one" and "the floor one". +// +// A LANE IS THREE FACTS AND NOT ONE, and each is read by a different surface: the JOB ID is what +// the workflow's `needs..result` expression names, the VARIABLE is what the emitted shell +// reads, and the LABEL is what the receipt prints. They are genuinely distinct strings -- the job +// id is `required-witnesses-build`, the variable `BUILD`, the label `build` -- so collapsing any +// two would force one surface to derive its spelling from another's, which is a nickname for a +// fact the caller already holds. Carrying all three is what lets the gate AND the step's `env` +// block be projections of one roster instead of two hand-kept lists whose agreement nothing +// checks. +// +// NON-EMPTY BY CONSTRUCTION, and that is the whole safety argument for the shape. The verdict is +// an OR-fold over the lanes, and an or-fold over nothing is FALSE -- so an empty lane list would +// publish the required context GREEN over a gate that read no lane at all, which is section 5's +// fail-open in its purest form. `FreeSemigroup` has no empty representation, so that state is +// UNWRITABLE rather than validated: the structurally-impossible rung of section 4b rather than +// the mechanically-preventable one, and no refusal arm is owed because there is no arm to write. +// +// THE BOUNDARY THAT GUARANTEE HOLDS AT, stated because section 4b says unwritable in the ACCEPTED +// CORPUS and unwritable as SOURCE HANDED TO THE COMPILER are different claims and only the second +// decides whether a RED is authorable. MEASURED, not reasoned: a fixture module authoring +// `FreeSemigroup { tail: [] }` was handed to the compiler on 2026-09-02 and refused with +// `error: missing required field 'head' in literal of type 'FreeSemigroup'`, located at the +// literal -- one blocking error. So the empty roster is authorable as fixture source and is +// refused there, which is the stronger of the two boundaries. +// +// WHAT THAT DOES NOT ESTABLISH, AND THE TRIGGER IS OWNED ELSEWHERE. The refusal is the compiler's +// GENERAL record-completeness wall, not anything this roster authored, and the roadmap node +// `floor-record-construction-wall` (rn_ILWLG34LVL5SAS6QPN5GZDPMFY) records that wall's own +// evidence as NOT YET ENROLLED -- in its words, a construction wall "currently rests on +// record-completeness enforcement that is itself unmeasured" -- the refusal measured here is +// recorded as that node's executed RED specimen rather than restated. So this roster's rung is section +// 4b(4) CONDITIONAL ON that wall, and its next-rung trigger is that node's probe-pairing rather +// than anything in this file. A per-consumer fixture asserting the same refusal is deliberately +// NOT added here: it would be one more monomorphised copy of a corpus-wide property, the same +// duplication declining a sixth NonEmpty carrier avoids. +// It is deliberately not a fresh NonEmptyRequiredLanes carrier -- `free_semigroup_grounding_note` +// already names five monomorphised copies of that shape as convergence debt, and a sixth would be +// the re-invention that section 2's own test forbids. +type RequiredLane { + job_id: String, + label: String, + var_name: String +} + +// THE OR-FOLD OVER THE LANES, left-associated so that the two-lane case is the exact node the +// hardcoded pair built: `or_else(left: test(first), right: test(second))`. +fn required_lanes_any_test(lanes: FreeSemigroup, mk: fn(String) -> Node) -> Node { + fold_list( + xs: lanes.tail, + empty: mk(lanes.head.var_name), + cons: fn(acc, lane) { bash_build_or_else(left: acc, right: mk(lane.var_name)) } + ) +} + +// THE RECEIPT'S LANE SEGMENT, one `label=$VAR` pair per lane. +// +// The head's literal carries the caller's leading text so it stays ONE literal word part rather +// than two adjacent ones -- the serializer is handed the same node shape it was handed before, +// not a shape that merely renders the same today. +fn required_lanes_receipt_parts(lanes: FreeSemigroup, head_prefix: String) -> List { + list_append( + left: [ + bash_build_word_lit(text: concat(head_prefix, lanes.head.label, "=")), + bash_build_word_var(name: lanes.head.var_name) + ], + right: list_flat_map(xs: lanes.tail, f: fn(lane) { + [ + bash_build_word_lit(text: concat(" ", lane.label, "=")), + bash_build_word_var(name: lane.var_name) + ] + }) + ) +} + fn required_lane_is_failure_test(var_name: String) -> Node { required_lane_var_equals_lit_test(var_name: var_name, text: floor_lane_result_failure) } @@ -210,26 +292,23 @@ fn required_lane_is_failure_test(var_name: String) -> Node { // unknown spelling therefore lands in unestablished and blocks; it can never land in green. // Reversing these two would make the enumeration load-bearing and reopen exactly that hole. fn required_lanes_verdict_stmts( - build_var: String, - floor_var: String, + lanes: FreeSemigroup, verdict_var: String ) -> List { [ bash_build_assign_lit(name: verdict_var, text: floor_rendered_verdict_green_name), bash_build_if_from_stmts( - cond: bash_build_or_else( - left: required_lane_not_success_test(var_name: build_var), - right: required_lane_not_success_test(var_name: floor_var) - ), + cond: required_lanes_any_test(lanes: lanes, mk: fn(v) { + required_lane_not_success_test(var_name: v) + }), then_stmts: [ bash_build_assign_lit(name: verdict_var, text: floor_rendered_verdict_unestablished_name) ] ), bash_build_if_from_stmts( - cond: bash_build_or_else( - left: required_lane_is_failure_test(var_name: build_var), - right: required_lane_is_failure_test(var_name: floor_var) - ), + cond: required_lanes_any_test(lanes: lanes, mk: fn(v) { + required_lane_is_failure_test(var_name: v) + }), then_stmts: [ bash_build_assign_lit(name: verdict_var, text: floor_rendered_verdict_red_name) ] @@ -267,8 +346,7 @@ fn required_lanes_interruption_stmts( } fn required_lanes_verdict_receipt_stmt( - build_var: String, - floor_var: String, + lanes: FreeSemigroup, verdict_var: String, mechanism_var: String, attribution_var: String @@ -277,18 +355,17 @@ fn required_lanes_verdict_receipt_stmt( words: [ bash_build_word_lit(text: "echo"), bash_build_word_concat_parts( - parts: [ - bash_build_word_lit(text: "required lanes: build="), - bash_build_word_var(name: build_var), - bash_build_word_lit(text: " floor="), - bash_build_word_var(name: floor_var), + parts: list_append( + left: required_lanes_receipt_parts(lanes: lanes, head_prefix: "required lanes: "), + right: [ bash_build_word_lit(text: " verdict="), bash_build_word_var(name: verdict_var), bash_build_word_lit(text: " mechanism="), bash_build_word_var(name: mechanism_var), bash_build_word_lit(text: " attribution="), bash_build_word_var(name: attribution_var) - ] + ] + ) ) ] ) @@ -296,8 +373,7 @@ fn required_lanes_verdict_receipt_stmt( fn required_lanes_error_stmt( text: String, - build_var: String, - floor_var: String, + lanes: FreeSemigroup, mechanism_var: String, attribution_var: String ) -> Node { @@ -306,17 +382,16 @@ fn required_lanes_error_stmt( words: [ bash_build_word_lit(text: "echo"), bash_build_word_concat_parts( - parts: [ - bash_build_word_lit(text: text), - bash_build_word_var(name: build_var), - bash_build_word_lit(text: " floor="), - bash_build_word_var(name: floor_var), + parts: list_append( + left: required_lanes_receipt_parts(lanes: lanes, head_prefix: text), + right: [ bash_build_word_lit(text: " mechanism="), bash_build_word_var(name: mechanism_var), bash_build_word_lit(text: " attribution="), bash_build_word_var(name: attribution_var), bash_build_word_lit(text: ") - open that job's log") - ] + ] + ) ) ] ), @@ -341,8 +416,7 @@ fn required_lanes_error_stmt( // reader to different places, and each carries the mechanism and attribution the aggregator can // actually establish, which today is one case and none respectively. fn required_lanes_refusal_stmts( - build_var: String, - floor_var: String, + lanes: FreeSemigroup, verdict_var: String, mechanism_var: String, attribution_var: String @@ -355,9 +429,8 @@ fn required_lanes_refusal_stmts( ), then_stmts: [ required_lanes_error_stmt( - text: "::error::a required lane concluded failure; that alone does not establish whether its subject was evaluated, so read the log before assuming a defect in the diff (build=", - build_var: build_var, - floor_var: floor_var, + text: "::error::a required lane concluded failure; that alone does not establish whether its subject was evaluated, so read the log before assuming a defect in the diff (", + lanes: lanes, mechanism_var: mechanism_var, attribution_var: attribution_var ), @@ -371,9 +444,8 @@ fn required_lanes_refusal_stmts( ), then_stmts: [ required_lanes_error_stmt( - text: "::error::a required lane produced no conclusion of its own, so this head's floor verdict is unobservable rather than failed; rerun it (build=", - build_var: build_var, - floor_var: floor_var, + text: "::error::a required lane produced no conclusion of its own, so this head's floor verdict is unobservable rather than failed; rerun it (", + lanes: lanes, mechanism_var: mechanism_var, attribution_var: attribution_var ), @@ -417,8 +489,7 @@ fn required_lanes_refusal_stmts( // function no longer has a parameter through which an expression could be handed to a shell // literal (DESIGN 5, construction over validation). fn required_lanes_gate_stmts( - build_var: String, - floor_var: String, + lanes: FreeSemigroup, pull_request_var: String, event_name_var: String, measured_head_var: String, @@ -449,8 +520,7 @@ fn required_lanes_gate_stmts( let through_lane_axis = list_append( left: through_subject_receipt, right: required_lanes_verdict_stmts( - build_var: build_var, - floor_var: floor_var, + lanes: lanes, verdict_var: verdict_var ) ) @@ -465,8 +535,7 @@ fn required_lanes_gate_stmts( left: through_interruption_axes, right: [ required_lanes_verdict_receipt_stmt( - build_var: build_var, - floor_var: floor_var, + lanes: lanes, verdict_var: verdict_var, mechanism_var: mechanism_var, attribution_var: attribution_var @@ -476,8 +545,7 @@ fn required_lanes_gate_stmts( list_append( left: through_verdict_receipt, right: required_lanes_refusal_stmts( - build_var: build_var, - floor_var: floor_var, + lanes: lanes, verdict_var: verdict_var, mechanism_var: mechanism_var, attribution_var: attribution_var diff --git a/dag/gunbc/roadmap/roadmap_authority.dag b/dag/gunbc/roadmap/roadmap_authority.dag index bc0b61606e9..427a3e87602 100644 --- a/dag/gunbc/roadmap/roadmap_authority.dag +++ b/dag/gunbc/roadmap/roadmap_authority.dag @@ -4156,7 +4156,7 @@ fn guarantee_ladder_nodes() -> List { boundary: "A record literal missing a required field refuses at compile with the field named; defaults apply only where declared; a literal claiming a nominal type it does not ground refuses. Owns the census's record-completeness class — the declared-conformance chain owns return, data, and generic instantiation, not this. Probe-paired via the corpus's record-completeness pair. Motivating specimen: HandAuthoredDocBind's primary_work construction wall currently rests on record-completeness enforcement that is itself unmeasured.", displaced_cost: "A construction wall anywhere in the corpus is only as strong as required-field enforcement; this node is what makes primary_work-style walls load-bearing rather than declared.", first_slice: "Missing-required-field refusal, probe-paired.", - red_control: "A record literal minus one required field refuses naming it; every corpus record literal compiles.", + red_control: "A record literal minus one required field refuses naming it; every corpus record literal compiles. RED ARM HAS AN EXECUTED SPECIMEN (2026-09-02, gunbc.required_lanes_gate lane roster): a fixture authoring FreeSemigroup { tail: [] } handed to the compiler refuses `missing required field 'head' in literal of type 'FreeSemigroup'`, located at the literal, 1 blocking error. That establishes the RED is authorable as source, not merely absent from the corpus; the every-corpus-literal-compiles arm and the probe pairing remain unmeasured, so this node is still the trigger for anything resting on this wall.", out_of_scope: "Row polymorphism; invocation default semantics (call-shape owns those).", handback: "The judgment site, probe flip, corpus receipt." ) diff --git a/dag/gunbc/witness/witness_floor_workflow.dag b/dag/gunbc/witness/witness_floor_workflow.dag index 6dfd118c0c6..0d2926aa015 100644 --- a/dag/gunbc/witness/witness_floor_workflow.dag +++ b/dag/gunbc/witness/witness_floor_workflow.dag @@ -15,7 +15,7 @@ import gunbc.workflow_capability_closure { workflow_job_capability_closure, capability_closure_is_closed, } -import v2.std.algebra { list_map } +import v2.std.algebra { FreeSemigroup, list_append, list_map, non_empty_to_list } import extdeps.languages.yaml.emit { serialize_yaml } import extdeps.languages.yaml.gha_workflow { project_workflow_to_yaml } import v2.workflow.ci_workflow_run_emit { ci_toolchain_homes_isolated_or_refuse_command } @@ -49,7 +49,7 @@ import gunbc.merge_admission_produce { ci_repo_root_shell } import gunbc.ci_layer_roots { witness_layer_roots } import gunbc.fabric_witness_run { witnesses_lane_run_command, build_lane_run_command } import extdeps.exec.command { ArgvCommand, shell_command_render } -import gunbc.required_lanes_gate { required_lanes_gate_stmts } +import gunbc.required_lanes_gate { RequiredLane, required_lanes_gate_stmts } import extdeps.github.expressions { ContextAccess, Github, Needs, interpolate } import v2.workflow.bash_command_fold_serialize { bash_fold_serialize_program } import v2.std.diagnostic { Outcome } @@ -1370,9 +1370,26 @@ fn witness_floor_job() -> Job { // THE RUST UNIT TESTS, IN THEIR OWN JOB AND NOT IN EITHER REQUIRED LANE (operator ruling // 2026-08-29: "add the rust unit tests but keep them in a separate job for now"). The 774 // `#[test]`s under src/v1/stage0 ran on no CI path before this job existed. It is not a `needs` of -// the aggregate, so it does not gate a merge yet; it is a third context beside the two lanes, and -// promoting it is a one-row edit to `required_lanes_aggregate_job` once its wall clock is measured -// on the fleet runner. +// the aggregate, so it does not gate a merge yet; it is a third context beside the two lanes. +// +// PROMOTING IT IS NOW ACTUALLY ONE ROW, WHICH IT WAS NOT WHEN THIS SENTENCE WAS FIRST WRITTEN. +// The claim was true of the aggregate's shape then and had gone stale: the lane axis was a +// hardcoded pair spelled 28 times across four functions in `gunbc.required_lanes_gate`, so +// promotion was a signature change in four places, and -- worse -- a `needs`-only edit would have +// added the wait while granting no authority to block, because the gate reads named variables and +// a lane whose result it does not read cannot fail it. The axis is now one `RequiredLane` roster +// from which the gate's verdict, the receipt, both refusal messages, the step's `env` block and +// the job's `needs` edge are all derived, so adding this job is one row in +// `required_lanes_roster` and nothing else. +// +// WHAT STILL GATES THE PROMOTION IS NOT THE EDIT SIZE. Two conditions, and neither is discharged +// by this file: main must be green, and the fleet's toolchain-install fault must be fixed. The +// second is the load-bearing one -- measured over 120 witnesses runs on 2026-09-02, this job's +// wall clock is BELOW `required-witnesses-floor` at every quantile (p50 21.9 vs 25.9 minutes, p90 +// 32.1 vs 36.2, max 41.5 vs 47.0), so promotion costs nothing on the critical path, but a host +// fault that evicts the toolchain would become a merge block on every pull request in the +// repository the moment this lane gates. Re-derive that measurement from +// `actions/runs//jobs` rather than trusting these numbers. data rust_unit_tests_job_id: String = "rust-unit-tests" fn rust_unit_tests_step() -> Step { @@ -1866,6 +1883,34 @@ fn required_lanes_run_id_expression() -> String { // all. A `Rejected` fold can therefore never reach a published step. data required_lanes_gate_build_var: String = "BUILD" data required_lanes_gate_floor_var: String = "FLOOR" + +// THE REQUIRED LANE ROSTER, AND IT IS ONE ROSTER READ TWICE RATHER THAN TWO LISTS THAT AGREE. +// +// The gate's verdict and the step's `env` block are the same fact asked in two directions -- which +// jobs decide the merge -- and they were previously two hand-kept lists whose agreement nothing +// checked. A lane present here but absent from `needs` reads an unset variable; a lane in `needs` +// but absent here is a job that runs and cannot block. Both are silent. Deriving both surfaces +// from this row makes the second state unwritable and leaves only the `needs` edge to keep in +// step, which is the one edge GitHub owns rather than us. +// +// NON-EMPTY BY CONSTRUCTION -- see `RequiredLane` in `gunbc.required_lanes_gate` for why an empty +// roster is a fail-open rather than a degenerate case. +fn required_lanes_roster() -> FreeSemigroup { + FreeSemigroup { + head: RequiredLane { + job_id: build_lane_job_id, + label: "build", + var_name: required_lanes_gate_build_var + }, + tail: [ + RequiredLane { + job_id: floor_lane_job_id, + label: "floor", + var_name: required_lanes_gate_floor_var + } + ] + } +} data required_lanes_gate_pull_request_var: String = "PULL_REQUEST" data required_lanes_gate_event_name_var: String = "EVENT_NAME" data required_lanes_gate_measured_head_var: String = "MEASURED_HEAD" @@ -1878,8 +1923,7 @@ data required_lanes_gate_attribution_var: String = "ATTRIBUTION" fn required_lanes_aggregate_script_outcome() -> String? { match bash_fold_serialize_program( stmts: required_lanes_gate_stmts( - build_var: required_lanes_gate_build_var, - floor_var: required_lanes_gate_floor_var, + lanes: required_lanes_roster(), pull_request_var: required_lanes_gate_pull_request_var, event_name_var: required_lanes_gate_event_name_var, measured_head_var: required_lanes_gate_measured_head_var, @@ -1931,14 +1975,20 @@ fn required_lanes_aggregate_script() -> String { // takes variable NAMES only and reads them as shell variables; the expressions live here, one row // per variable, joined to the gate by the same declarations the gate is handed. fn required_lanes_aggregate_step_env() -> List { - [ - kv(key: required_lanes_gate_build_var, value: yaml_string(s: required_lane_result_expression(job_id: build_lane_job_id))), - kv(key: required_lanes_gate_floor_var, value: yaml_string(s: required_lane_result_expression(job_id: floor_lane_job_id))), + list_append( + left: list_map(xs: non_empty_to_list(xs: required_lanes_roster()), f: fn(lane) { + kv( + key: lane.var_name, + value: yaml_string(s: required_lane_result_expression(job_id: lane.job_id)) + ) + }), + right: [ kv(key: required_lanes_gate_pull_request_var, value: yaml_string(s: required_lanes_pull_request_expression())), kv(key: required_lanes_gate_event_name_var, value: yaml_string(s: required_lanes_event_name_expression())), kv(key: required_lanes_gate_measured_head_var, value: yaml_string(s: required_lanes_measured_head_expression())), kv(key: required_lanes_gate_run_id_var, value: yaml_string(s: required_lanes_run_id_expression())) - ] + ] + ) } fn required_lanes_aggregate_step() -> Step { @@ -1973,7 +2023,7 @@ fn required_lanes_aggregate_job() -> Job { name: none, runner: gunbc_ci_selected_runner_spec(), steps: [required_lanes_aggregate_step()], - needs: [build_lane_job_id, floor_lane_job_id], + needs: list_map(xs: non_empty_to_list(xs: required_lanes_roster()), f: fn(lane) { lane.job_id }), env: none, outputs: none, if_condition: Present { value: required_lanes_aggregate_job_condition() },