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
26 changes: 24 additions & 2 deletions dag/gunbc/instrument_targets.dag
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,18 @@ fn primitive_egress_census_seed_label() -> Label {
Label { package: instruments_package() target: TargetName { name: "primitive-egress-census-seed" } }
}

// THE REQUIRED-LANE RESOLUTION CENSUS: for every module under the source roots, does at least
// one required lane RESOLVE it -- hand its source to compile_to_resolved under the Strict gate?
// The unreached population, by identity, is the printed product; the exit says whether it is
// empty. This is DESIGN section 3's "a product-layer dependent can stop resolving, stay broken,
// and let every required lane report SUCCESS" measured rather than warned about, after
// gunbc.site_pxe_edge_converge did exactly that on 2026-09-20 (gunbc#11607). The lane roster it
// classifies is read from gunbc.compiler_gate_workflow, the authority that emits witnesses.yml.
// `gunbc test //gunbc/instruments:required-lane-resolution-census`.
fn required_lane_resolution_census_label() -> Label {
Label { package: instruments_package() target: TargetName { name: "required-lane-resolution-census" } }
}

// THE INSTRUMENT IS A `TestRule` WITH NO DEPENDENCIES, and both halves are measurements rather
// than placeholders. It answers a test question — does the heads reading read the same grammar as
// the full reading — so it is not a `BuildRule`; and it depends on no other target in this graph,
Expand Down Expand Up @@ -261,6 +273,10 @@ fn primitive_egress_census_seed_target() -> BuildTarget {
instrument_test_target(label: primitive_egress_census_seed_label())
}

fn required_lane_resolution_census_target() -> BuildTarget {
instrument_test_target(label: required_lane_resolution_census_label())
}

fn v2_native_cli_binding() -> TargetBinding {
TargetBinding { target: v2_native_cli_label() producer: V2NativeCliProducer {} }
}
Expand Down Expand Up @@ -319,6 +335,10 @@ fn primitive_egress_census_seed_binding() -> TargetBinding {
TargetBinding { target: primitive_egress_census_seed_label() producer: PrimitiveEgressCensusSeedProducer {} }
}

fn required_lane_resolution_census_binding() -> TargetBinding {
TargetBinding { target: required_lane_resolution_census_label() producer: RequiredLaneResolutionCensusProducer {} }
}

// THE SUBJECT IS THE INSTRUMENT'S OWN FACT, NOT AN ARGUMENT THE CALLER SUPPLIES.
//
// `gunbc test //gunbc/instruments:heads-reading-differential` takes no source-root option, and
Expand Down Expand Up @@ -382,7 +402,8 @@ fn instrument_targets() -> List<Label> {
compile_clean_diagnostic_census_label(), self_host_label(), v2_native_cli_label(),
evaluation_store_address_exact_head_label(), primitive_egress_census_label(),
primitive_egress_census_v2_label(), primitive_egress_census_dag_label(),
primitive_egress_census_seed_label(), floor_memory_qualification_label()
primitive_egress_census_seed_label(), floor_memory_qualification_label(),
required_lane_resolution_census_label()
]
}

Expand All @@ -393,7 +414,8 @@ fn instrument_bindings() -> List<TargetBinding> {
compile_clean_diagnostic_census_binding(), self_host_binding(), v2_native_cli_binding(),
evaluation_store_address_exact_head_binding(), primitive_egress_census_binding(),
primitive_egress_census_v2_binding(), primitive_egress_census_dag_binding(),
primitive_egress_census_seed_binding(), floor_memory_qualification_binding()
primitive_egress_census_seed_binding(), floor_memory_qualification_binding(),
required_lane_resolution_census_binding()
]
}

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
module gunbc.recurring_failure_mode.a_planted_red_control_positioned_where_it_cannot_fire

import std.types { NonEmptyStr }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data a_planted_red_control_positioned_where_it_cannot_fire: RecurringFailureMode = RecurringFailureMode {
identity: "a_planted_red_control_positioned_where_it_cannot_fire" as NonEmptyStr,

receipts: [
"**a planted red control positioned where it cannot fire** (an instrument folds a verdict into an accumulator -- `failures=0; for ...; failures=$((failures+1))` -- and the author splices the planted red control ABOVE the line that resets the accumulator, or before the fold's first read, so the control's contribution is discarded before the verdict is taken. The instrument then reports green on the control and on the subject alike, and the control is cited as proof the instrument can go red.",

"INVALID STATE: a control whose effect on the verdict is unreachable from the position it was planted at -- reset after it, scoped outside the fold, written to a variable the verdict does not read. HARM: the control is the only thing that distinguishes an instrument that measures from one that prints green, so a control that cannot fire converts every later green from that instrument into a decoration cited as coverage (DESIGN section 4b: ask whether the check's RED is authorable before writing the check -- and here it was authored, but could not reach the verdict).",

"DISCRIMINATOR: trace the data path from the control's plant site to the verdict's read site and find an assignment, reset, `local`, subshell boundary or pipeline stage between them that the control's value does not survive. The positive control ON THE PLANT (the same session's memory carries this as its own rule -- a planted red needs a positive control on the plant): run the instrument with ONLY the control planted and confirm the verdict is red; a control that returns green when it is the only input is not a control.",

"RECEIPT (2026-09-20, dashboard node adhoc-3bc1b8e0-982): the second of two session evidence instruments that reported green over gunbc.site_pxe_edge_converge not resolving carried a red control spliced above its accumulator reset, so it could only return green; both instruments failed toward green on one defect and the head carried four approvals on that evidence. The drivers were session-authored shell and are not in-tree; no in-tree driver of this shape was found, and the in-tree walls against the sibling shape (a control asserted rather than produced; coverage read per call site rather than per argument) are rostered as their own rows.",

"REPAIR SHAPE: the control is planted at the subject's own input, downstream of every reset and inside every scope the verdict reads, and the receipt records the red it produced BESIDE the green the subject produced -- two runs, two statuses, or the receipt is one run and one status and establishes nothing about the instrument.",

"Rung: mitigatable -- the positive control on the plant exposes it when run. Ceiling: mechanically preventable, not structural: a verdict fold whose accumulator is a value threaded through the fold rather than a mutable shell variable has no reset to splice above, and an instrument rendered from a typed fold (gunbc.cli_wire, the claim executor's per-claim outcome rows) cannot be authored in this shape; a session's ad-hoc shell can, and is outside the modeled guarantee.",

"Next-rung trigger: the manual receipt `gunbc.rung_drop` `required_gate_bankruptcy` obliges every PR to carry while that drop stands names an rc-red control as a required part, and the control is required to be shown red in the same receipt -- a receipt whose control did not print red is refused as a receipt by review, which is the executing consumer of this row until the receipt itself is a typed carrier.",
],

evidence: [],
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
module gunbc.recurring_failure_mode.exit_status_read_through_a_pipe_reports_the_last_stage

import std.types { NonEmptyStr }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data exit_status_read_through_a_pipe_reports_the_last_stage: RecurringFailureMode = RecurringFailureMode {
identity: "exit_status_read_through_a_pipe_reports_the_last_stage" as NonEmptyStr,

receipts: [
"**exit status read through a pipe reports the last stage** (an instrument runs its subject as `subject ... | tail -n 40` or `| grep ...` and then reads `$?`, or lets the pipeline's status be the step's; without `set -o pipefail` a POSIX pipeline's status is the LAST stage's, so a subject that refused with exit 1 or 2 is reported as exit 0 whenever `tail` or `grep` exits 0 -- the instrument fails toward green on the one defect it was run to detect.",

"INVALID STATE: a shell driver whose verdict is a pipeline status while its subject is not the last stage. HARM: a refusal is read as a pass, so a session posts an exact-head APPROVE, a PR body cites a green receipt, or a lane reports SUCCESS over a subject that refused -- the silent-wrongness column DESIGN section 5 forbids, produced by the evidence instrument itself.",

"DISCRIMINATOR: the driver's status read (`$?`, `if cmd | filter; then`, a step whose last command is a pipeline) sits AFTER a `|` whose left side is the subject, and no `set -o pipefail` or `PIPESTATUS` read is in scope. The control that must be run before citing such a driver: replace the subject with `false` (or `sh -c 'exit 2'`) and confirm the driver goes red; a driver that stays green over `false | tail` is reading tail's status.",

"RECEIPT (2026-09-20, dashboard node adhoc-3bc1b8e0-982): one of two session evidence instruments that reported green over gunbc.site_pxe_edge_converge not resolving read its `claim_batch` exit status through `| tail`; the head carried four approvals and reached position 1 in the merge queue on that evidence. The drivers were session-authored shell, not in-tree: a grep of `.githooks`, `tools`, `.github/workflows` and every emitted `run:` line found no in-tree driver reading a subject's status through a filter -- the emitted floor steps set `set -o pipefail` before `| tee` (gunbc.ci_failure_class wrap_command_with_floor_attempt_receipt), and gunbc.live_deploy.intent live_deploy_unit_status_tail_command, the one in-tree `| tail` over a diagnostic subject, is already a marked scaffold whose dissolution trigger names exactly this class (exit code recorded as data, never masked by `| tail`).",

"REPAIR SHAPE: the subject's status is data, not a side effect of the pipeline -- `set -o pipefail` at minimum; better, run the subject to a file and read its status directly, as the floor wrapper does. A rendered filter that is kept for readability (`tail -40`) is applied to the captured output afterwards, never between the subject and the status read.",

"Rung: mitigatable -- the class is caught by the red control above when someone runs it. Ceiling: structurally impossible for drivers this repository EMITS, once every emitted step script is rendered from a typed carrier that records the subject's status as data (gunbc.systemctl_status_read is the shape; the floor wrapper is the executing instance). Session-authored shell is outside the modeled guarantee and stays at the red-control rung: the obligation on a manual receipt is that its driver was run against `false` once.",

"Next-rung trigger: the manual-receipt obligation on `gunbc.rung_drop` `required_gate_bankruptcy` names the rc-red control as a required part of the receipt, so a receipt without it is not a receipt; and the emitted-step carrier gunbc.live_deploy.intent live_deploy_unit_diagnosis_dissolution_trigger names retires the last in-tree instance.",
],

evidence: [],
}
135 changes: 135 additions & 0 deletions dag/gunbc/required_lane_resolution_census.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,135 @@
module gunbc.required_lane_resolution_census

import std.types { String, Bool, List, Int }
import v2.std.optional { Optional, Present, Absent }

// FOR EVERY MODULE UNDER THE SOURCE ROOTS, DOES AT LEAST ONE REQUIRED LANE RESOLVE IT?
//
// DESIGN section 3 states the hazard as a warning: outside the required gate the substrate still
// refuses and nothing asks it to, so a product-layer dependent can stop resolving, stay broken,
// and let every required lane report SUCCESS. On 2026-09-20 it was the live state --
// gunbc.site_pxe_edge_converge did not resolve on main while all four required lanes were green,
// with four approvals and a place in the merge queue (gunbc#11607) -- and the question "which
// modules can do that" had no instrument, only the warning. This module is the instrument's fold:
// pure, over supplied populations, so its claims discriminate at one interface and its live
// entry (gunbc.required_lane_resolution_census_live) supplies the populations from the lanes'
// own producers.
//
// "RESOLVE" MEANS ONE THING: the module's source is in the source set the lane's compile
// transaction hands to compile_to_resolved under the Strict gate. A module named only in a
// `run:` line's argv is not resolved by that step unless the entry's closure reaches it.
//
// NOMINAL, NOT DIFF-SCOPED. The floor also seeds its subject from a run's diff, so a module a PR
// touches is resolved on THAT run. The population this census reports is the complement of what
// the lanes resolve when the diff seeds nothing -- exactly the modules a rename elsewhere can
// break without any lane noticing, which is the incident's shape.
//
// IDENTITIES ARE THE PRODUCT. The unreached population is printed by identity and every count in
// the receipt is rendered from a list the receipt also prints; nothing here is a number to be
// transcribed into prose (DESIGN section 6: name the instrument).

// One population of module identities as a compiler query answers it, or the typed reason the
// population could not be established. The live entry's three queries
// (source_root_ingest_module_identities, required_floor_nominal_subject_module_identities,
// entry_closure_module_identities) return this; the census refuses on the second arm rather than
// treating an unestablished population as empty.
type ModuleIdentityPopulation
= ModuleIdentityPopulationObserved { modules: List<String> }
| ModuleIdentityPopulationRefused { cause: String }

// WHAT ONE REQUIRED JOB RESOLVES, as a subject kind naming the producer that decides it.
// FloorNominalPreparedSubject -- `claim_executor --required-ci --required-lane witnesses`: the
// prepared subject over the gate's nominal seeds (v1_compiler.cli_run
// required_floor_nominal_subject_seeds, assemble_prepared_subject_closure).
// RunEntryClosure -- `gunbc run --entry <path>`: the entry's loader closure
// (v1_compiler.cli_run load_sources_for_entry_with_pool, the call resolve_entry_graph makes).
// ResolvesNoDagModule -- a job that compiles Rust or aggregates lane results and hands no .dag
// source to the compiler; the reason names what it does instead.
type LaneResolutionSubject
= FloorNominalPreparedSubject
| RunEntryClosure { entry_path: String }
| ResolvesNoDagModule { reason: String }

// One required job and the subjects its steps resolve. A job may carry several (the floor job
// runs the witness fold AND the drift gate); a job with none is unclassified, which the live
// entry refuses rather than reading as "resolves nothing".
type LaneResolutionRow {
job_id: String
subjects: List<LaneResolutionSubject>
}

// The resolved population one (job, subject) pair contributed, supplied to the fold.
type LaneResolvedPopulation {
job_id: String
subject: LaneResolutionSubject
modules: List<String>
}

type ResolutionCensusInputs {
admitted: List<String>
resolved: List<LaneResolvedPopulation>
}

type ResolutionCensus {
admitted: List<String>
reached: List<String>
unreached: List<String>
lanes: List<LaneResolvedPopulation>
}

type ResolutionCensusStanding
= ResolutionCensusHeld
| ResolutionCensusDidNotHold { unreached: List<String> }

// THE JOIN IS AT IDENTITY GRAIN. Reached is every admitted identity some lane resolved; unreached
// is the rest, in the admitted order. A resolved identity the ingestion does not admit is not an
// admitted module and is neither reached nor unreached: the denominator is the ingestion's, not
// the union's.
fn resolution_census(inputs: ResolutionCensusInputs) -> ResolutionCensus {
let reached_by_any = inputs.resolved |> fold(init: empty_map(), f: fn(acc, lane) {
lane.modules |> fold(init: acc, f: fn(m, x) { map_insert(m, x, true) })
})
let reached = inputs.admitted |> filter(x => map_contains_key(reached_by_any, x))
let unreached = inputs.admitted |> filter(x => !map_contains_key(reached_by_any, x))
ResolutionCensus { admitted: inputs.admitted, reached: reached, unreached: unreached, lanes: inputs.resolved }
}

fn resolution_census_standing(c: ResolutionCensus) -> ResolutionCensusStanding {
if (c.unreached |> count) == 0 { ResolutionCensusHeld {} } else { ResolutionCensusDidNotHold { unreached: c.unreached } }
}

fn subject_rendered(s: LaneResolutionSubject) -> String {
match s {
FloorNominalPreparedSubject => "floor-nominal-prepared-subject"
RunEntryClosure { entry_path: p } => concat("run-entry-closure:", p)
ResolvesNoDagModule { reason: _ } => "resolves-no-dag-module"
}
}

fn json_string(s: String) -> String {
concat(concat("\"", s), "\"")
}

fn json_string_list(xs: List<String>) -> String {
concat(concat("[", xs |> map(x => json_string(s: x)) |> join(separator: ",")), "]")
}

// THE RECEIPT: one JSON object per line. A summary line whose counts are the lengths of lists
// printed beneath it; one `lane` line per (job, subject) with the identities it resolved; and one
// `unreached` line per unreached identity, so the population is greppable by identity and a
// consumer never has to re-derive it from a count.
fn census_receipt_lines(c: ResolutionCensus) -> List<String> {
let summary = concat(concat(concat(concat(
"{\"kind\":\"summary\",\"instrument\":\"required-lane-resolution-census\",\"admitted\":", to_string(c.admitted |> count)),
concat(",\"reached\":", to_string(c.reached |> count))),
concat(",\"unreached\":", to_string(c.unreached |> count))),
concat(",\"lanes\":", concat(to_string(c.lanes |> count), "}")))
let lane_lines = c.lanes |> map(l =>
concat(concat(concat(concat(concat(concat(
"{\"kind\":\"lane\",\"job_id\":", json_string(s: l.job_id)),
",\"subject\":"), json_string(s: subject_rendered(s: l.subject))),
",\"resolved\":"), to_string(l.modules |> count)),
concat(",\"modules\":", concat(json_string_list(xs: l.modules), "}"))))
let unreached_lines = c.unreached |> map(m => concat(concat("{\"kind\":\"unreached\",\"module\":", json_string(s: m)), "}"))
concat(concat([summary], lane_lines), unreached_lines)
}
Loading