From 4da0eff9d15fa54224faa2f78534ee51ccdf5c29 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 09:01:01 +0000 Subject: [PATCH 1/3] The required-lane axis was a hardcoded pair; make it a roster, with the emitted YAML byte-identical MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PR A of the two-part promotion item. Behaviour-identical §2 dedup, landing on its own so the promotion row (PR B) waits on the fleet condition without holding this. WHAT WAS FORKED. The aggregate's lane axis was `build_var` beside `floor_var`, threaded through four functions and spelled 28 times in gunbc.required_lanes_gate (`grep -c 'build_var\|floor_var'`). That is one concept -- a required lane -- given one name per instance, which is the fork §2 horizontal exists to delete. THE TELL WAS THAT A CLAIMED ONE-ROW EDIT WAS NOT ONE. gunbc.witness_floor_workflow at `rust_unit_tests_job_id` says promoting a third job into the aggregate is "a one-row edit to `required_lanes_aggregate_job`". That was true of the shape the aggregate had when it was written and had since gone stale: promotion was a signature change in four places plus a step-name rewrite. Worse, the obvious reading of it -- add the `needs` edge -- would have added the WAIT while granting NO AUTHORITY TO BLOCK, because the gate's verdict reads named shell variables and a lane whose result it does not read cannot fail it. A promotion that looks landed and gates nothing is worse than no promotion, because the roster would then cite it as coverage. WHAT THE ROSTER IS. `RequiredLane { job_id, label, var_name }` -- three genuinely distinct strings (`required-witnesses-build`, `build`, `BUILD`), each read by a different surface, so collapsing any two would make one surface derive its spelling from another's. FIVE surfaces now derive from the single `required_lanes_roster()`: the verdict's or-folds, the receipt line, both refusal messages, the step's `env` block, and the job's `needs` edge. Those last two were previously hand-kept lists whose agreement nothing checked -- a lane in the env but not in `needs` reads an unset variable, a lane in `needs` but not the env is a job that runs and cannot block, and both are silent. NON-EMPTY BY CONSTRUCTION, and this is the safety half rather than a shape preference. The verdict is an OR-fold over the lanes, and an or-fold over nothing is FALSE -- an empty roster would publish the required context GREEN over a gate that read no lane at all. `FreeSemigroup` has no empty representation, so that state is UNWRITABLE rather than validated: §4b(4) rather than §4b(2), and no refusal arm is owed because there is no arm to write. 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 §2's own test forbids. ACCEPTANCE TEST: THE EMITTED YAML IS BYTE-IDENTICAL. Producer, not transcription: gunbc run --source-root dag --source-root src/v2 \ --entry dag/gunbc/instruments/generated_artifact_gate.dag --function main_wet then diff .github/workflows/witnesses.yml against its pre-change bytes. No generated artifact in the tree changes; only the two authority files do. AND THE BYTE-IDENTITY IS SHOWN NOT TO BE A STALE ARTIFACT, because a diff of zero is readable only beside a nonzero. Two controls, both executed: - mutate ONE roster field (label "build" -> "REDCTL") and regenerate: the diff fires in THREE places -- the receipt line and both refusal messages -- proving the emission reads this roster rather than surviving bytes. - add ONE row to the roster (the rust-unit-tests lane) and regenerate: the verdict fold grows a third `|| [ "$UNIT" != success ]` conjunct AND a third `= failure` conjunct, the receipt grows ` unit=$UNIT`, both refusal messages grow it, and the env block grows `UNIT: ${{ needs['rust-unit-tests'].result }}`. That is the forward receipt that PR B really is one row, measured rather than promised. Both probes were reverted; neither is in this diff. The `rust_unit_tests_job_id` annotation is corrected to say what is now true, and to record the two conditions that actually gate the promotion -- main green AND the fleet toolchain fault fixed, the second because a host fault that evicts the toolchain becomes a merge block on every PR the moment this lane gates. NOT IN THIS PR, deliberately: the aggregate step is still named "Both required lanes must have succeeded". "Both" becomes wrong only when a third lane lands, and changing it now would break the byte-identity that is this PR's whole acceptance test. It belongs to PR B. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VSP89XiSm2YMnUvSwSR1ct --- dag/gunbc/required_lanes_gate.dag | 135 +++++++++++++------ dag/gunbc/witness/witness_floor_workflow.dag | 74 ++++++++-- 2 files changed, 154 insertions(+), 55 deletions(-) diff --git a/dag/gunbc/required_lanes_gate.dag b/dag/gunbc/required_lanes_gate.dag index 0c3c26c647f..68c51e83fc1 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,69 @@ 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. +// 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 +273,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 +327,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 +336,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 +354,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 +363,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 +397,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 +410,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 +425,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 +470,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 +501,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 +516,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 +526,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/witness/witness_floor_workflow.dag b/dag/gunbc/witness/witness_floor_workflow.dag index ad75c9f9906..42018d246cf 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 } @@ -1319,9 +1319,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 { @@ -1795,6 +1812,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" @@ -1807,8 +1852,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, @@ -1860,14 +1904,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 { @@ -1902,7 +1952,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() }, From c80c9d88db2ce21f292acb386e3b4a4b43281e21 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 09:10:40 +0000 Subject: [PATCH 2/3] State the boundary the non-empty guarantee holds at, measured rather than asserted Review caution: "unwritable in the ACCEPTED CORPUS" and "unwritable as SOURCE HANDED TO THE COMPILER" are different claims, and section 4b says only the second decides whether a RED is authorable. The previous note stated the guarantee without saying which boundary it held at, which reads as stronger than it is. MEASURED, NOT REASONED. A fixture module authoring `FreeSemigroup { tail: [] }` was handed to the compiler and refused: error[...empty_roster_probe.dag:9:3]: missing required field 'head' in literal of type 'FreeSemigroup' 1 blocking error(s) So the empty roster IS authorable as fixture source and IS refused there, located at the literal -- the stronger of the two boundaries, established by execution. The probe was deleted after the run and is not in this diff. WHAT THAT DOES NOT ESTABLISH, and this is the half the caution was really about. 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 -- a construction wall "currently rests on record-completeness enforcement that is itself unmeasured". So the rung is honestly 4b(4) CONDITIONAL ON that wall, and the next-rung trigger is that node's probe-pairing rather than anything in this file. That is a tracked stall, not a permanent ceiling. NO PER-CONSUMER FIXTURE ADDED, deliberately. Enrolling a local probe that asserts the same corpus-wide refusal would be one more monomorphised copy of a general property -- the same duplication that declining a sixth NonEmpty carrier avoids, and it would attribute to this roster evidence that belongs to record construction. Emitted YAML unchanged: annotation only, re-verified byte-identical against the same regeneration. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VSP89XiSm2YMnUvSwSR1ct --- dag/gunbc/required_lanes_gate.dag | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/dag/gunbc/required_lanes_gate.dag b/dag/gunbc/required_lanes_gate.dag index 68c51e83fc1..701dc9d7356 100644 --- a/dag/gunbc/required_lanes_gate.dag +++ b/dag/gunbc/required_lanes_gate.dag @@ -217,6 +217,24 @@ fn required_lanes_head_standing_stmts( // 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". 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. From ad388184accf2bd01a4726548978d6846a8d488b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 09:21:12 +0000 Subject: [PATCH 3/3] Give floor-record-construction-wall the executed RED specimen, and cite it rather than restate it Follow-up to the boundary statement. The manager's ruling: do not enroll a local probe -- it would assert a corpus-wide property from one consumer and attribute to the lane roster evidence that belongs to record construction -- but DO give the receipt to the node where the class lives, one line each way. roadmap_authority `floor-record-construction-wall` (rn_ILWLG34LVL5SAS6QPN5GZDPMFY) now records in `red_control` that its RED arm has an executed specimen: a fixture authoring `FreeSemigroup { tail: [] }`, refused with `missing required field 'head' in literal of type 'FreeSemigroup'`, located at the literal, 1 blocking error. Stated with what it does NOT establish -- the every-corpus-literal-compiles arm and the probe pairing remain unmeasured, so this node stays the trigger for anything resting on this wall. `red_control` is the right field and the budget does not reach it: the ~100-word page budget is on `brief`, and `roadmap_ticket_brief_violations` walks `declared_roadmap_nodes()` rather than the projection precisely so a long red_control cannot price a derived node's brief a second time. gunbc.required_lanes_gate's annotation now CITES that receipt instead of carrying it, so the measurement has one home. TWO THINGS VERIFIED RATHER THAN ASSUMED, both cheap and both nearly wrong: - red_control has a real consumer -- `disclosure_field(label: "red control", ...)` in roadmap_presentation -- so this is a receipt in a typed carrier, not prose in a String field. - the braces. `{ ... }` in a .dag string can interpolate, and neighbouring rows in this same file escape as `\{cause\}`. Measured with a two-arm probe before trusting it: `"FreeSemigroup { tail: [] } end"` and its escaped twin render IDENTICALLY, so interpolation needs a bare identifier immediately after the brace and escaping here would have emitted a literal backslash. witnesses.yml re-verified byte-identical; no generated artifact changes (the roadmap ticket fields are not projected into committed markdown). Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VSP89XiSm2YMnUvSwSR1ct --- dag/gunbc/required_lanes_gate.dag | 3 ++- dag/gunbc/roadmap/roadmap_authority.dag | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/dag/gunbc/required_lanes_gate.dag b/dag/gunbc/required_lanes_gate.dag index 701dc9d7356..dd03f8e233d 100644 --- a/dag/gunbc/required_lanes_gate.dag +++ b/dag/gunbc/required_lanes_gate.dag @@ -230,7 +230,8 @@ fn required_lanes_head_standing_stmts( // 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". So this roster's rung is section +// 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 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." )