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
154 changes: 111 additions & 43 deletions dag/gunbc/required_lanes_gate.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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.<id>.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<RequiredLane>, 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<RequiredLane>, head_prefix: String) -> List<Node> {
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)
}
Expand All @@ -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<RequiredLane>,
verdict_var: String
) -> List<Node> {
[
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)
]
Expand Down Expand Up @@ -267,8 +346,7 @@ fn required_lanes_interruption_stmts(
}

fn required_lanes_verdict_receipt_stmt(
build_var: String,
floor_var: String,
lanes: FreeSemigroup<RequiredLane>,
verdict_var: String,
mechanism_var: String,
attribution_var: String
Expand All @@ -277,27 +355,25 @@ 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)
]
]
)
)
]
)
}

fn required_lanes_error_stmt(
text: String,
build_var: String,
floor_var: String,
lanes: FreeSemigroup<RequiredLane>,
mechanism_var: String,
attribution_var: String
) -> Node {
Expand All @@ -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")
]
]
)
)
]
),
Expand All @@ -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<RequiredLane>,
verdict_var: String,
mechanism_var: String,
attribution_var: String
Expand All @@ -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
),
Expand All @@ -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
),
Expand Down Expand Up @@ -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<RequiredLane>,
pull_request_var: String,
event_name_var: String,
measured_head_var: String,
Expand Down Expand Up @@ -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
)
)
Expand All @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/roadmap/roadmap_authority.dag
Original file line number Diff line number Diff line change
Expand Up @@ -4156,7 +4156,7 @@ fn guarantee_ladder_nodes() -> List<RoadmapNode> {
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."
)
Expand Down
Loading
Loading