From a4eb4c85816fb525f69640564fa588341b7bfe71 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 5 Oct 2026 13:37:36 +0000 Subject: [PATCH 1/4] RFM: witness_outside_gate_closure_falsified_by_other_file gains the population-grain receipt (below mitigatable for the declined set) Co-Authored-By: Claude Opus 5.5 (1M context) --- .../witness_outside_gate_closure_falsified_by_other_file.dag | 1 + 1 file changed, 1 insertion(+) diff --git a/dag/gunbc/recurring_failure_mode/witness_outside_gate_closure_falsified_by_other_file.dag b/dag/gunbc/recurring_failure_mode/witness_outside_gate_closure_falsified_by_other_file.dag index 2b7902d4630..2cd37800661 100644 --- a/dag/gunbc/recurring_failure_mode/witness_outside_gate_closure_falsified_by_other_file.dag +++ b/dag/gunbc/recurring_failure_mode/witness_outside_gate_closure_falsified_by_other_file.dag @@ -47,6 +47,7 @@ data witness_outside_gate_closure_falsified_by_other_file: RecurringFailureMode "THE TWO CLAIM REDS THE REPAIR ABOVE EXPOSED, RE-DERIVED (swift-bat-688, 2026-10-04), AND NEITHER IS A PRODUCT DEFECT. fleet_intent_network_topology_membership_is_an_identity_join: the fold is right and the witness did what it was built to do. gunbc.fleet_intent_network gained srv12_host_lan_endpoint in its topology on 2026-09-05 (76ee135bd3) and the roster the witness authors by name was not told, so the join reported a topology member no named row declares. The earliest unjustified link is the authored roster, repaired by naming the row; the claim is its own discriminating control, FAIL without the row and 10 of 10 PASS with it, both executed. It was red about a month and could not be seen because the entry did not resolve. witness_srv1_width_drifts_from_declared_count_after_recarve: NOT repaired, and named here so it is owned. The claim compares the 2026-07-03 fixture row (ten active units) with gunbc.runner_slot_allocation gunbc_runner_committed_width for srv1 and asserts Drifted. That was true while the derived width was five; the derivation has since moved (memory envelope from the host, per-host CPU offer) and now yields exactly ten, read by twelve temporary probes of which only the equals-ten probe passed. So the verdict function is correct and returns converged, and the claim is falsified by a model change in a module it does not own. It is also the fusion its own annotation warns against, a parse fixture joined to a live-derived count: ten equal to ten is a three-month-old observation agreeing with a new model by coincidence, which establishes neither convergence nor drift. Flipping the assertion to converged would mint that coincidence as a readback. Its stated dissolution is a post-re-carve width readback replacing the fixture row, which is a live observation of srv1 and is the trigger that owns this red.", "PROPOSED WALL, SHAPE ONLY, NOT BUILT (swift-bat-688, 2026-10-04): AN ActiveDebt ROW IN A CLAIM-ROOT FILE CARRIES A WITNESS-RUN RECEIPT OR THE FLOOR REFUSES. SUBJECT: a row of v2.workflow.floor_unimported_bare_provider_debt_roster whose file is a claim root, decided by the same discovery the floor already runs (the file declares at least one test fn), never by a path prefix. A file with imports that is not a claim root is out of scope, because the predicate file-has-imports is true of every row and refuses the whole roster. CARRIER: standing gains an arm beside ActiveDebt for those rows, carrying the entry it was run as, the tree it was run on as a GitRef, and the claims run; one receipt per FILE joined to its rows, not one per row, since resolution is a fact about the entry. JUDGMENTS, each a located refusal in v2.workflow.floor_unimported_bare_provider_debt beside the existing three: a claim-root row with bare ActiveDebt refuses as unwitnessed; a receipt with zero claims run refuses, because an entry that resolved and ran nothing is the state this class hides in; a receipt whose tree is not an ancestor of the head, or whose file changed since that tree, refuses as stale. The host supplies only the facts it alone can read (is the file a claim root, did it change since the receipt tree). WHAT IT DOES NOT REACH, STATED SO THE RUNG IS NOT INFLATED: the receipt is authored, so it is a transcription and not an execution, and every specimen on this row was falsified by a change to a DIFFERENT file, which leaves the receipt tree an ancestor and the file unchanged. The wall therefore closes one face only, debt enrolled in a claim root that was never run at all, which is how gunbc#12205 seeded these rows. It is rung 2 for that face and leaves the class where it was. The capability stays the one already named: plan the enrolled population, that is, the floor resolves every claim-root file and refuses one that does not, at which point this receipt arm is redundant and dissolves.", "THE THREE RESIDUAL REDS, CLASSIFIED (swift-bat-688, 2026-10-04, claim_batch on BuildBuddy, GUNBC_MEMORY_BUDGET_BYTES forwarded). (1) `v2.test.claim.body_lowering.single_arm_match` 4 of 6 is a v2 REGRESSION from gunbc#13056, bisected; receipt on `match_arms_after_the_second_are_dropped_at_v2_body_lowering`. (2) `v2.test.long.cwc_resolution_probe` 7 of 9: `cwc_malformed_nary_coproduct_normalize_rejects` and `cwc_malformed_nary_coproduct_fail_open_control` are each other's negation, so exactly one is red by construction; that pair is a STALE EXPECTATION SHAPE (a declared fail-open written as a permanent red, not a finding), and today normalize accepts the malformed coproduct. `cwc_cwc_module_resolve_accepts` is a REGRESSION CANDIDATE, not bisected: resolve refuses with `lve_anonymous_record_expected_type_not_record` on `data review_event_wire_contract: CoproductWireContract = { ... }`, where CoproductWireContract is the one-line comma record form used in 73 corpus files; rostered as `anonymous_record_literal_refused_against_a_declared_record_type`. (3) `v2.test.long.accumulator_copy_fold_analysis` 5 of 24: the lowered Loop is still found (`quadratic_ingest_has_lowered_loop` passes) but `report_counters_state_the_domain` fails and no suspect is reported on any planted copy, so the lens no longer binds the fold carrier; REGRESSION, not bisected, rostered as `accumulator_copy_lens_binds_no_carrier`. THE COST ROW QUESTION: `v2.workflow.floor_cost_debt` separates PROVEN (passed, over cost) from CENSORED (interrupted before verdict), and a censored row asserts no semantic verdict. single_arm_match sits in a CENSORED chunk. The proposed narrowing: an OBSERVED semantic FAIL must not stay represented only as a cost or censored disposition; it is a semantic red and is rostered as one. An interrupted run still establishes nothing, and nothing here promotes unknown to passing. One unbudgeted run at admission and at restoration supplies evidence at those two revisions only. It is snapshot-limited and cannot catch a regression that lands while the row stands, which is exactly how single_arm_match went red under #13056. So it supplements the existing execution and restoration obligation and does not replace it. No gate is implemented in this change.", + "RECEIPT, 2026-10-05 (snappy-stag-806, from calm-boar-904's bisection and calm-crab-469's grammar census), AND IT STATES THE RUNG AT POPULATION GRAIN. Seven claims of v2.test.claim.value_position_whole_read were falsified by gunbc#12923 (2026-10-01); on that PR's own floor run (36893078130, FloorClean) the module's disposition was declined_outside_gate_closure, so the floor that admitted the falsifier was green because it never asked the witness. One claim of v2.test.claim.function_value_body_route was falsified by gunbc#12506 by the same route. Separately, every v2.test.parse.* module lay outside the floor's prepared universe, with seven of their claims false on main (calm-crab-469, gunbc#13372, closed; phase-1 gating is gunbc#13374). RUNG, STATED HONESTLY (DESIGN 4b(1)): for the declined population the class sits BELOW MITIGATABLE. No mechanism on the merge path executes those claims, so a falsifying change lands with no typed outcome anywhere, and that is silent wrongness rather than a rung. The decline is discovered and counted, but a count of unasked witnesses is not evidence that any of them holds. The current rung of the class is the minimum over its in-scope paths, and this path is the minimum. The per-identity population is the floor's own required_floor_disposition.tsv rows whose disposition is declined_outside_gate_closure. That file is written by the floor and not published by any CI step, so the population is not readable from a run today, and publishing it is the census's first obligation. NEXT TRIGGER, UNCHANGED IN SUBSTANCE: the capability is that every claim-root witness has a disposition that EXECUTES it on the merge path or a declared rung_drop or stall naming it. A per-change selector cannot discharge it, for the reason the compiler-wall face of witness_that_fails_to_compile_is_absent_rather_than_red gives.", ], evidence: [], From 63137ceff868d9c79e2467cff90069e4a3434a31 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 5 Oct 2026 14:15:31 +0000 Subject: [PATCH 2/4] Publish the floor's admission roster and read it: the gate-closure decline census required_floor_disposition.tsv was written on every floor run and published by none since the job move (instrument_artifact_stopped_existing_while_cited). It is now uploaded as required-floor-disposition through one named bound step in both step lists, and read by tools.gate_closure_decline_census_instrument gate_closure_decline_census, the population census of witness_outside_gate_closure_falsified_by_other_file. Co-Authored-By: Claude Opus 5.5 (1M context) --- .github/workflows/witnesses.yml | 8 ++ dag/gunbc/gate_closure_decline_census.dag | 84 +++++++++++++++++++ ...gate_closure_decline_census_instrument.dag | 31 +++++++ ..._artifact_stopped_existing_while_cited.dag | 3 + dag/gunbc/witness/compiler_gate_workflow.dag | 3 +- dag/gunbc/witness/witness_floor_workflow.dag | 29 ++++--- 6 files changed, 147 insertions(+), 11 deletions(-) create mode 100644 dag/gunbc/gate_closure_decline_census.dag create mode 100644 dag/gunbc/instruments/gate_closure_decline_census_instrument.dag diff --git a/.github/workflows/witnesses.yml b/.github/workflows/witnesses.yml index 554a9a54c69..c3dd7af8367 100644 --- a/.github/workflows/witnesses.yml +++ b/.github/workflows/witnesses.yml @@ -410,6 +410,14 @@ jobs: if-no-files-found: error retention-days: 14 if: "!cancelled() && steps.build_witness_fold.outcome == 'success'" + - name: Upload the floor's admission roster + uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f + with: + name: required-floor-disposition + path: required_floor_disposition.tsv + if-no-files-found: error + retention-days: 14 + if: "!cancelled() && steps.build_witness_fold.outcome == 'success'" env: MALLOC_ARENA_MAX: "2" GUNBC_EXPECTED_RED_ROSTER_JOIN: expected_red_roster_join.tsv diff --git a/dag/gunbc/gate_closure_decline_census.dag b/dag/gunbc/gate_closure_decline_census.dag new file mode 100644 index 00000000000..8c8e1f4222a --- /dev/null +++ b/dag/gunbc/gate_closure_decline_census.dag @@ -0,0 +1,84 @@ +module gunbc.gate_closure_decline_census + +import std.types { Bool, Int, String } +import v2.std.optional { Present, Absent } +import v2.workflow.required_floor { changed_selection_identity_module_path } + +// THE POPULATION OF gunbc.recurring_failure_mode witness_outside_gate_closure_falsified_by_other_file, +// READ FROM THE FLOOR'S OWN RECORD RATHER THAN RECOMPUTED. The floor decides, per qualified witness +// identity, whether its module is in the prepared gate closure; an identity whose module is not is +// written to required_floor_disposition.tsv with the disposition declined_outside_gate_closure +// (gunbc.witness_floor_workflow required_floor_disposition_upload_bound_step publishes it as the +// `required-floor-disposition` artifact). Recomputing the closure here would be a second authority +// for one fact, so this module only folds rows the floor wrote. +// +// EVERY FUNCTION HERE IS PURE AND TAKES ITS LINES AS AN ARGUMENT. Reading the artifact off disk is +// the instrument's fact (tools.gate_closure_decline_census_instrument). + +data gate_closure_decline_disposition: String = "declined_outside_gate_closure" + +// The grammar lane owns this population (gunbc#13374), so the census leaves it out by module +// prefix rather than double-counting it. +data gate_closure_decline_census_excluded_prefixes: List = ["v2.test.parse."] + +type DispositionRow { + identity: String + disposition: String +} + +type ModuleDeclineCount { + module: String + claims: Int +} + +// A data line is decided before it is split: the artifact carries a `#` summary line, a header and +// possibly a trailing blank, none of which is a row. +fn is_disposition_data_line(line: String) -> Bool { + line != "" + && !starts_with(s: line, prefix: "#") + && !starts_with(s: line, prefix: "identity\t") +} + +fn parse_disposition_line(line: String) -> DispositionRow { + let fields = split(s: line, delimiter: "\t") + if count(fields) < 2 { + DispositionRow { identity: line, disposition: "" } + } else { + DispositionRow { identity: fields[0], disposition: fields[1] } + } +} + +fn census_excludes_module(module: String) -> Bool { + fold(gate_closure_decline_census_excluded_prefixes, init: false, f: fn(acc, p) { acc || starts_with(s: module, prefix: p) }) +} + +// The declined identities, in artifact order, after the exclusion. +fn gate_closure_declined_identities(lines: List) -> List { + lines + |> filter(l => is_disposition_data_line(line: l)) + |> map(l => parse_disposition_line(line: l)) + |> filter(r => r.disposition == gate_closure_decline_disposition + && !census_excludes_module(module: changed_selection_identity_module_path(identity: r.identity))) + |> map(r => r.identity) +} + +// One count per declining module, keyed once per identity (a map, so the tally is linear in rows). +fn gate_closure_decline_by_module(identities: List) -> List { + let counts = fold(identities, init: empty_map(), f: fn(m, identity) { + let module = changed_selection_identity_module_path(identity: identity) + map_insert(m, module, 1 + match map_get(m, module) { Present { value: n } => n Absent => 0 }) + }) + map(map_keys(counts), k => ModuleDeclineCount { module: k, claims: match map_get(counts, k) { Present { value: n } => n Absent => 0 } }) +} + +fn gate_closure_decline_census_lines(lines: List) -> List { + let identities = gate_closure_declined_identities(lines) + let modules = gate_closure_decline_by_module(identities) + concat( + ["summary declined_identities=" + to_string(length(identities)) + " modules=" + to_string(length(modules))], + concat( + map(modules, c => "module " + c.module + " claims=" + to_string(c.claims)), + map(identities, i => "identity " + i) + ) + ) +} diff --git a/dag/gunbc/instruments/gate_closure_decline_census_instrument.dag b/dag/gunbc/instruments/gate_closure_decline_census_instrument.dag new file mode 100644 index 00000000000..ab7d3533b5b --- /dev/null +++ b/dag/gunbc/instruments/gate_closure_decline_census_instrument.dag @@ -0,0 +1,31 @@ +module tools.gate_closure_decline_census_instrument + +import extdeps.filesystem.filesystem_io +import std.process { ProcessExit, ExitSuccess, exit_failure } +import std.types { String } +import gunbc.cli_wire { CliWireResponse, CliWirePrintable } +import gunbc.gate_closure_decline_census { gate_closure_decline_census_lines } + +// THE CENSUS OF WITNESSES THE REQUIRED FLOOR NEVER ASKS, re-derived from one floor run's own +// admission roster. The recipe: +// gh run download -n required-floor-disposition -D / +// gunbc run --source-root dag --source-root src/v2 \ +// --entry dag/gunbc/instruments/gate_closure_decline_census_instrument.dag \ +// --function gate_closure_decline_census --arg root= --arg run= +// The counts are the run's, never this file's: a citation names the run, and this entry re-derives. +data gate_closure_decline_census_file: String = "required_floor_disposition.tsv" + +// AN UNREADABLE ROSTER REFUSES rather than printing an empty census: an empty declined set and a +// missing roster are different facts, and only the first is good news. +fn gate_closure_decline_census(root: String, run: String) -> CliWireResponse { + let path = root + "/" + run + "/" + gate_closure_decline_census_file + let read = Filesystem.Read(path: path) + if !read.success { + CliWirePrintable { bytes: "", exit: exit_failure(reason: "gate closure decline census: unreadable " + path) } + } else { + CliWirePrintable { + bytes: join(gate_closure_decline_census_lines(lines: split(s: read.content, delimiter: "\n")), "\n") + "\n", + exit: ExitSuccess, + } + } +} diff --git a/dag/gunbc/recurring_failure_mode/instrument_artifact_stopped_existing_while_cited.dag b/dag/gunbc/recurring_failure_mode/instrument_artifact_stopped_existing_while_cited.dag index 2a91c6f292a..8694873c34a 100644 --- a/dag/gunbc/recurring_failure_mode/instrument_artifact_stopped_existing_while_cited.dag +++ b/dag/gunbc/recurring_failure_mode/instrument_artifact_stopped_existing_while_cited.dag @@ -20,11 +20,14 @@ data instrument_artifact_stopped_existing_while_cited: RecurringFailureMode = Re "CEILING: mechanically preventable. The published-output set of the required workflow is derivable from its emitter, and the artifact names its consumers cite are declarations (gunbc.witness_floor_workflow required_floor_claim_cost_artifact_name), so the join between cited artifacts and emitted upload steps is decidable at emission.", "NEXT-RUNG TRIGGER, A CAPABILITY: an emission-time join that refuses when an artifact-name declaration consumed by a production fold or rostered as an instrument has no upload step in the emitted required workflow -- sufficient that removing an upload, or replacing the job that carried it, reds the generated-artifact phase. One shared bound-step function (required_floor_claim_cost_upload_bound_step) keeps this one artifact's two step lists from parting again; it does not discover the next one.", + "RECEIPT, 2026-10-05 (snappy-stag-806): THE ADMISSION ROSTER IS RESTORED, AND IT IS RESTORED WITH A READER. required_floor_disposition.tsv is again published as `required-floor-disposition`, bound by name in both step lists through gunbc.witness_floor_workflow required_floor_disposition_upload_bound_step, the way the claim-cost upload already is. Its executing consumer is tools.gate_closure_decline_census_instrument gate_closure_decline_census, the population census of witness_outside_gate_closure_falsified_by_other_file. The expected-red roster join, long-home storage agreement and cross-claim demand uploads remain unrepaired members of this class.", ], evidence: [ DeclarationRef { module_path: "gunbc.witness_floor_workflow", decl_name: "required_floor_claim_cost_upload_bound_step", field: WholeDeclaration }, DeclarationRef { module_path: "gunbc.witness_floor_workflow", decl_name: "required_floor_claim_cost_artifact_name", field: WholeDeclaration }, DeclarationRef { module_path: "gunbc.compiler_gate_workflow", decl_name: "compiler_gate_floor_measurement_bound_steps", field: WholeDeclaration }, DeclarationRef { module_path: "gunbc.floor_cost_distribution", decl_name: "parse_claim_cost_tsv", field: WholeDeclaration }, + DeclarationRef { module_path: "gunbc.witness_floor_workflow", decl_name: "required_floor_disposition_upload_bound_step", field: WholeDeclaration }, + DeclarationRef { module_path: "gunbc.gate_closure_decline_census", decl_name: "gate_closure_declined_identities", field: WholeDeclaration }, ], } diff --git a/dag/gunbc/witness/compiler_gate_workflow.dag b/dag/gunbc/witness/compiler_gate_workflow.dag index 08ee9998508..48185a44527 100644 --- a/dag/gunbc/witness/compiler_gate_workflow.dag +++ b/dag/gunbc/witness/compiler_gate_workflow.dag @@ -123,6 +123,7 @@ import gunbc.witness_floor_workflow { required_floor_cross_claim_demand_path, required_ci_measurement_bound_steps, required_floor_claim_cost_upload_bound_step, + required_floor_disposition_upload_bound_step, required_ci_measurement_scripts_are_renderable, WitnessFloorGenerationOutcome, WitnessFloorGenerated, WitnessFloorGenerationRefused } @@ -739,7 +740,7 @@ fn compiler_gate_generated_bound_steps() -> List { // the cost of what it executed. fn compiler_gate_floor_measurement_bound_steps() -> List { list_map( - xs: concat(required_ci_measurement_bound_steps(), [required_floor_claim_cost_upload_bound_step()]), + xs: concat(required_ci_measurement_bound_steps(), [required_floor_claim_cost_upload_bound_step(), required_floor_disposition_upload_bound_step()]), f: fn(b) { CompilerGateBoundStep { step: b.step, role: b.role, step_name: b.step_name } }, ) } diff --git a/dag/gunbc/witness/witness_floor_workflow.dag b/dag/gunbc/witness/witness_floor_workflow.dag index c57db8a007a..55d4cbd3a83 100644 --- a/dag/gunbc/witness/witness_floor_workflow.dag +++ b/dag/gunbc/witness/witness_floor_workflow.dag @@ -1674,6 +1674,24 @@ fn required_floor_claim_cost_upload_bound_step() -> WitnessFloorBoundStep { } } +// THE ADMISSION ROSTER (required_floor_disposition.tsv) IS BOUND THE SAME WAY, for the same reason: +// it was one of the four uploads instrument_artifact_stopped_existing_while_cited named as lost with +// the job move, and it is the only per-identity record of which witnesses the floor declined +// (declined_outside_gate_closure among them). Its reader is gunbc.instruments +// gate_closure_decline_census, the census of witness_outside_gate_closure_falsified_by_other_file. +fn required_floor_disposition_upload_bound_step() -> WitnessFloorBoundStep { + WitnessFloorBoundStep { + step: witness_floor_tsv_upload_step( + step_name: "Upload the floor's admission roster", + artifact_name: required_floor_disposition_artifact_name, + path: required_floor_disposition_path, + condition: witness_floor_precondition() + ), + role: capability_neutral, + step_name: "Upload the floor's admission roster", + } +} + fn required_ci_measurement_bound_steps() -> List { [ WitnessFloorBoundStep { @@ -1712,16 +1730,7 @@ fn witness_floor_bound_steps() -> List { step_name: "All witnesses (one prepared subject, one fold)", }, ], concat(required_ci_measurement_bound_steps(), concat([ - WitnessFloorBoundStep { - step: witness_floor_tsv_upload_step( - step_name: "Upload the floor's admission roster", - artifact_name: required_floor_disposition_artifact_name, - path: required_floor_disposition_path, - condition: witness_floor_precondition() - ), - role: capability_neutral, - step_name: "Upload the floor's admission roster", - }, + required_floor_disposition_upload_bound_step(), WitnessFloorBoundStep { step: witness_floor_tsv_upload_step( step_name: "Upload the expected-red roster join", From 3d7087a976f1cd530d494b21b650d823e9cc1b62 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 5 Oct 2026 14:29:03 +0000 Subject: [PATCH 3/4] Gate-closure census refuses a malformed roster line; witness the fold Review 76577: a short line or a disposition outside the floor's vocabulary now refuses, located by line, instead of being dropped. The vocabulary is derived from v2.workflow.required_floor required_floor_disposition_name. test.claim.gate_closure_decline_census_witness executes every clause, including an empty-census control that keeps the refusal arms honest. Co-Authored-By: Claude Opus 5.5 (1M context) --- dag/gunbc/gate_closure_decline_census.dag | 104 +++++++++++++----- ...gate_closure_decline_census_instrument.dag | 16 ++- ...te_closure_decline_census_witness_test.dag | 66 +++++++++++ 3 files changed, 152 insertions(+), 34 deletions(-) create mode 100644 dag/test/claim/gate_closure_decline_census_witness_test.dag diff --git a/dag/gunbc/gate_closure_decline_census.dag b/dag/gunbc/gate_closure_decline_census.dag index 8c8e1f4222a..ea009ff855b 100644 --- a/dag/gunbc/gate_closure_decline_census.dag +++ b/dag/gunbc/gate_closure_decline_census.dag @@ -2,7 +2,14 @@ module gunbc.gate_closure_decline_census import std.types { Bool, Int, String } import v2.std.optional { Present, Absent } -import v2.workflow.required_floor { changed_selection_identity_module_path } +import v2.workflow.required_floor { + changed_selection_identity_module_path, + required_floor_disposition_name, + RequiredFloorDisposition, + Planned, PlannedAsChangedWitness, DeclinedLongModule, DeclinedFixtureMember, + DeclinedOutsideRequiredGate, DeclinedOutsideGateClosure, DeclinedDiscoveryExcluded, + DeclinedCostDebt, DeclinedNoCiWetLane, DeclinedChangedWitnessOutsideDiscovery +} // THE POPULATION OF gunbc.recurring_failure_mode witness_outside_gate_closure_falsified_by_other_file, // READ FROM THE FLOOR'S OWN RECORD RATHER THAN RECOMPUTED. The floor decides, per qualified witness @@ -15,36 +22,53 @@ import v2.workflow.required_floor { changed_selection_identity_module_path } // EVERY FUNCTION HERE IS PURE AND TAKES ITS LINES AS AN ARGUMENT. Reading the artifact off disk is // the instrument's fact (tools.gate_closure_decline_census_instrument). -data gate_closure_decline_disposition: String = "declined_outside_gate_closure" +data gate_closure_decline_disposition: String = required_floor_disposition_name(d: DeclinedOutsideGateClosure) + +// THE WIRE VOCABULARY, DERIVED FROM THE ARMS' OWN NAMER rather than respelled. Payloads are blank +// because the name does not read them. An arm added to RequiredFloorDisposition and not listed here +// makes its rows REFUSE below rather than vanish, which is the direction a stale list must fail. +data required_floor_disposition_names: List = map([ + Planned, PlannedAsChangedWitness, DeclinedLongModule { matched_prefix: "" }, + DeclinedFixtureMember { matched_prefix: "" }, DeclinedOutsideRequiredGate, + DeclinedOutsideGateClosure, DeclinedDiscoveryExcluded { matched_substring: "" }, + DeclinedCostDebt, DeclinedNoCiWetLane { pattern: "" }, + DeclinedChangedWitnessOutsideDiscovery { module_path: "" } +], d => required_floor_disposition_name(d: d)) // The grammar lane owns this population (gunbc#13374), so the census leaves it out by module // prefix rather than double-counting it. data gate_closure_decline_census_excluded_prefixes: List = ["v2.test.parse."] -type DispositionRow { - identity: String - disposition: String -} - type ModuleDeclineCount { module: String claims: Int } -// A data line is decided before it is split: the artifact carries a `#` summary line, a header and -// possibly a trailing blank, none of which is a row. -fn is_disposition_data_line(line: String) -> Bool { - line != "" - && !starts_with(s: line, prefix: "#") - && !starts_with(s: line, prefix: "identity\t") -} +// A ROSTER IS READ WHOLE OR REFUSED, NEVER NARROWED. A data line with fewer than two columns, or a +// disposition outside the floor's vocabulary, is an artifact defect located by its 1-based line; +// dropping it would let a drifted roster print declined_identities=0, the one answer an unreadable +// roster must never produce (DESIGN section 5, a failure arm refuses). +type DispositionRosterRead + = DispositionRosterRows { identities: List } + | DispositionRosterRefused { line_number: Int, line: String, cause: String } -fn parse_disposition_line(line: String) -> DispositionRow { - let fields = split(s: line, delimiter: "\t") - if count(fields) < 2 { - DispositionRow { identity: line, disposition: "" } +type DispositionLineRead + = DispositionLineSkipped + | DispositionLineRow { identity: String, disposition: String } + | DispositionLineRefused { cause: String } + +fn read_disposition_line(line: String) -> DispositionLineRead { + if line == "" || starts_with(s: line, prefix: "#") || starts_with(s: line, prefix: "identity\t") { + DispositionLineSkipped } else { - DispositionRow { identity: fields[0], disposition: fields[1] } + let fields = split(s: line, delimiter: "\t") + if count(fields) < 2 { + DispositionLineRefused { cause: "fewer than two tab-separated columns" } + } else if !contains(required_floor_disposition_names, fields[1]) { + DispositionLineRefused { cause: "disposition outside the floor's vocabulary: " + fields[1] } + } else { + DispositionLineRow { identity: fields[0], disposition: fields[1] } + } } } @@ -52,14 +76,35 @@ fn census_excludes_module(module: String) -> Bool { fold(gate_closure_decline_census_excluded_prefixes, init: false, f: fn(acc, p) { acc || starts_with(s: module, prefix: p) }) } -// The declined identities, in artifact order, after the exclusion. -fn gate_closure_declined_identities(lines: List) -> List { - lines - |> filter(l => is_disposition_data_line(line: l)) - |> map(l => parse_disposition_line(line: l)) - |> filter(r => r.disposition == gate_closure_decline_disposition - && !census_excludes_module(module: changed_selection_identity_module_path(identity: r.identity))) - |> map(r => r.identity) +type RosterFold { + line_number: Int + refused: Bool + refusal: DispositionRosterRead + identities: List +} + +// The declined identities, after the exclusion, or the FIRST refused line. The accumulator is +// built in reverse and reversed once, so the fold is linear in lines. +fn gate_closure_declined_identities(lines: List) -> DispositionRosterRead { + let done = fold(lines, init: RosterFold { line_number: 0, refused: false, refusal: DispositionRosterRows { identities: [] }, identities: [] }, f: fn(acc, line) { + let n = acc.line_number + 1 + if acc.refused { + acc + } else { + match read_disposition_line(line: line) { + DispositionLineSkipped => RosterFold { line_number: n, refused: false, refusal: acc.refusal, identities: acc.identities } + DispositionLineRefused { cause } => RosterFold { line_number: n, refused: true, refusal: DispositionRosterRefused { line_number: n, line: line, cause: cause }, identities: acc.identities } + DispositionLineRow { identity, disposition } => + if disposition == gate_closure_decline_disposition + && !census_excludes_module(module: changed_selection_identity_module_path(identity: identity)) { + RosterFold { line_number: n, refused: false, refusal: acc.refusal, identities: concat([identity], acc.identities) } + } else { + RosterFold { line_number: n, refused: false, refusal: acc.refusal, identities: acc.identities } + } + } + } + }) + if done.refused { done.refusal } else { DispositionRosterRows { identities: reverse(done.identities) } } } // One count per declining module, keyed once per identity (a map, so the tally is linear in rows). @@ -71,9 +116,8 @@ fn gate_closure_decline_by_module(identities: List) -> List ModuleDeclineCount { module: k, claims: match map_get(counts, k) { Present { value: n } => n Absent => 0 } }) } -fn gate_closure_decline_census_lines(lines: List) -> List { - let identities = gate_closure_declined_identities(lines) - let modules = gate_closure_decline_by_module(identities) +fn gate_closure_decline_census_lines(identities: List) -> List { + let modules = gate_closure_decline_by_module(identities: identities) concat( ["summary declined_identities=" + to_string(length(identities)) + " modules=" + to_string(length(modules))], concat( diff --git a/dag/gunbc/instruments/gate_closure_decline_census_instrument.dag b/dag/gunbc/instruments/gate_closure_decline_census_instrument.dag index ab7d3533b5b..71375cfdfef 100644 --- a/dag/gunbc/instruments/gate_closure_decline_census_instrument.dag +++ b/dag/gunbc/instruments/gate_closure_decline_census_instrument.dag @@ -4,7 +4,13 @@ import extdeps.filesystem.filesystem_io import std.process { ProcessExit, ExitSuccess, exit_failure } import std.types { String } import gunbc.cli_wire { CliWireResponse, CliWirePrintable } -import gunbc.gate_closure_decline_census { gate_closure_decline_census_lines } +import gunbc.gate_closure_decline_census { + gate_closure_decline_census_lines, + gate_closure_declined_identities, + DispositionRosterRead, + DispositionRosterRows, + DispositionRosterRefused +} // THE CENSUS OF WITNESSES THE REQUIRED FLOOR NEVER ASKS, re-derived from one floor run's own // admission roster. The recipe: @@ -23,9 +29,11 @@ fn gate_closure_decline_census(root: String, run: String) -> CliWireResponse { if !read.success { CliWirePrintable { bytes: "", exit: exit_failure(reason: "gate closure decline census: unreadable " + path) } } else { - CliWirePrintable { - bytes: join(gate_closure_decline_census_lines(lines: split(s: read.content, delimiter: "\n")), "\n") + "\n", - exit: ExitSuccess, + match gate_closure_declined_identities(lines: split(s: read.content, delimiter: "\n")) { + DispositionRosterRefused { line_number, line, cause } => + CliWirePrintable { bytes: "", exit: exit_failure(reason: "gate closure decline census: " + path + " line " + to_string(line_number) + " refused (" + cause + "): " + line) } + DispositionRosterRows { identities } => + CliWirePrintable { bytes: join(gate_closure_decline_census_lines(identities: identities), "\n") + "\n", exit: ExitSuccess } } } } diff --git a/dag/test/claim/gate_closure_decline_census_witness_test.dag b/dag/test/claim/gate_closure_decline_census_witness_test.dag new file mode 100644 index 00000000000..9595b4e603d --- /dev/null +++ b/dag/test/claim/gate_closure_decline_census_witness_test.dag @@ -0,0 +1,66 @@ +module test.claim.gate_closure_decline_census_witness + +import std.types { Bool, Int, String } +import v2.std.optional { Present, Absent } +import gunbc.gate_closure_decline_census { + DispositionRosterRead, + DispositionRosterRows, + DispositionRosterRefused, + ModuleDeclineCount, + gate_closure_declined_identities, + gate_closure_decline_by_module +} + +// THE FLOOR'S ROSTER SHAPE, SUPPLIED (DESIGN section 3, a witness discriminates at one interface): +// a `#` summary line, the header, then identity/disposition/matched_prefix/outcome rows. The rows +// cover every clause the selection has: two declined identities in one module, one in another, a +// declined v2.test.parse.* identity the census must exclude, and a planned row it must not count. +data census_fixture_lines: List = [ + "# summary\ttotal=5", + "identity\tdisposition\tmatched_prefix\toutcome", + "a.b.f1\tdeclined_outside_gate_closure\t\t", + "a.b.f2\tdeclined_outside_gate_closure\t\t", + "v2.test.parse.x.g\tdeclined_outside_gate_closure\t\t", + "c.d.h\tplanned\t\tpass", + "e.f.k\tdeclined_outside_gate_closure\t\t", + "" +] + +test fn the_census_selects_declined_identities_and_excludes_the_grammar_lane_and_planned_rows() -> Bool { + match gate_closure_declined_identities(lines: census_fixture_lines) { + DispositionRosterRows { identities } => identities == ["a.b.f1", "a.b.f2", "e.f.k"] + DispositionRosterRefused { line_number: _, line: _, cause: _ } => false + } +} + +fn module_claims(counts: List, module: String) -> Int { + fold(counts, init: 0, f: fn(acc, c) { if c.module == module { acc + c.claims } else { acc } }) +} + +test fn the_census_tallies_claims_per_declaring_module() -> Bool { + let counts = gate_closure_decline_by_module(identities: ["a.b.f1", "a.b.f2", "e.f.k"]) + length(counts) == 2 && module_claims(counts: counts, module: "a.b") == 2 && module_claims(counts: counts, module: "e.f") == 1 +} + +test fn a_row_with_one_column_refuses_at_its_line_rather_than_being_dropped() -> Bool { + match gate_closure_declined_identities(lines: ["identity\tdisposition\tmatched_prefix\toutcome", "a.b.f1\tdeclined_outside_gate_closure", "a.b.f2"]) { + DispositionRosterRows { identities: _ } => false + DispositionRosterRefused { line_number, line, cause: _ } => line_number == 3 && line == "a.b.f2" + } +} + +test fn a_disposition_outside_the_floors_vocabulary_refuses_rather_than_being_dropped() -> Bool { + match gate_closure_declined_identities(lines: ["a.b.f1\tdeclined_outside_the_gate\t\t"]) { + DispositionRosterRows { identities: _ } => false + DispositionRosterRefused { line_number, line: _, cause: _ } => line_number == 1 + } +} + +// THE CONTROL THAT KEEPS THE TWO ABOVE HONEST: a roster with no declined row is a valid, empty +// census, not a refusal, so the refusal arms cannot be satisfied by refusing everything. +test fn a_roster_with_no_declined_row_reads_as_an_empty_census_not_a_refusal() -> Bool { + match gate_closure_declined_identities(lines: ["# summary\ttotal=1", "identity\tdisposition\tmatched_prefix\toutcome", "c.d.h\tplanned\t\tpass"]) { + DispositionRosterRows { identities } => length(identities) == 0 + DispositionRosterRefused { line_number: _, line: _, cause: _ } => false + } +} From 9bb74408bdfb4ad702627f9907070aade45a425e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 5 Oct 2026 14:49:41 +0000 Subject: [PATCH 4/4] Census reads the roster path from its one home; the fold's accumulator is a sum Review 76598: import gunbc.witness_floor_workflow required_floor_disposition_path instead of a second literal, and replace the flag-plus-payload accumulator with RosterReading | RosterStopped so a refused fold cannot carry a success arm. Co-Authored-By: Claude Opus 5.5 (1M context) --- dag/gunbc/gate_closure_decline_census.dag | 47 ++++++++++--------- ...gate_closure_decline_census_instrument.dag | 5 +- 2 files changed, 27 insertions(+), 25 deletions(-) diff --git a/dag/gunbc/gate_closure_decline_census.dag b/dag/gunbc/gate_closure_decline_census.dag index ea009ff855b..aae559abca5 100644 --- a/dag/gunbc/gate_closure_decline_census.dag +++ b/dag/gunbc/gate_closure_decline_census.dag @@ -76,35 +76,38 @@ fn census_excludes_module(module: String) -> Bool { fold(gate_closure_decline_census_excluded_prefixes, init: false, f: fn(acc, p) { acc || starts_with(s: module, prefix: p) }) } -type RosterFold { - line_number: Int - refused: Bool - refusal: DispositionRosterRead - identities: List -} +// THE ACCUMULATOR IS A SUM, so a stopped fold cannot also hold a success arm (review 76598): the +// only way to carry a refusal is the arm that carries nothing else. +type RosterFold + = RosterReading { line_number: Int, identities_reversed: List } + | RosterStopped { refusal: DispositionRosterRead } // The declined identities, after the exclusion, or the FIRST refused line. The accumulator is // built in reverse and reversed once, so the fold is linear in lines. fn gate_closure_declined_identities(lines: List) -> DispositionRosterRead { - let done = fold(lines, init: RosterFold { line_number: 0, refused: false, refusal: DispositionRosterRows { identities: [] }, identities: [] }, f: fn(acc, line) { - let n = acc.line_number + 1 - if acc.refused { - acc - } else { - match read_disposition_line(line: line) { - DispositionLineSkipped => RosterFold { line_number: n, refused: false, refusal: acc.refusal, identities: acc.identities } - DispositionLineRefused { cause } => RosterFold { line_number: n, refused: true, refusal: DispositionRosterRefused { line_number: n, line: line, cause: cause }, identities: acc.identities } - DispositionLineRow { identity, disposition } => - if disposition == gate_closure_decline_disposition - && !census_excludes_module(module: changed_selection_identity_module_path(identity: identity)) { - RosterFold { line_number: n, refused: false, refusal: acc.refusal, identities: concat([identity], acc.identities) } - } else { - RosterFold { line_number: n, refused: false, refusal: acc.refusal, identities: acc.identities } - } + let done = fold(lines, init: RosterReading { line_number: 0, identities_reversed: [] }, f: fn(acc, line) { + match acc { + RosterStopped { refusal } => acc + RosterReading { line_number, identities_reversed } => { + let n = line_number + 1 + match read_disposition_line(line: line) { + DispositionLineSkipped => RosterReading { line_number: n, identities_reversed: identities_reversed } + DispositionLineRefused { cause } => RosterStopped { refusal: DispositionRosterRefused { line_number: n, line: line, cause: cause } } + DispositionLineRow { identity, disposition } => + if disposition == gate_closure_decline_disposition + && !census_excludes_module(module: changed_selection_identity_module_path(identity: identity)) { + RosterReading { line_number: n, identities_reversed: concat([identity], identities_reversed) } + } else { + RosterReading { line_number: n, identities_reversed: identities_reversed } + } + } } } }) - if done.refused { done.refusal } else { DispositionRosterRows { identities: reverse(done.identities) } } + match done { + RosterStopped { refusal } => refusal + RosterReading { line_number: _, identities_reversed } => DispositionRosterRows { identities: reverse(identities_reversed) } + } } // One count per declining module, keyed once per identity (a map, so the tally is linear in rows). diff --git a/dag/gunbc/instruments/gate_closure_decline_census_instrument.dag b/dag/gunbc/instruments/gate_closure_decline_census_instrument.dag index 71375cfdfef..1d6c28e035c 100644 --- a/dag/gunbc/instruments/gate_closure_decline_census_instrument.dag +++ b/dag/gunbc/instruments/gate_closure_decline_census_instrument.dag @@ -3,6 +3,7 @@ module tools.gate_closure_decline_census_instrument import extdeps.filesystem.filesystem_io import std.process { ProcessExit, ExitSuccess, exit_failure } import std.types { String } +import gunbc.witness_floor_workflow { required_floor_disposition_path } import gunbc.cli_wire { CliWireResponse, CliWirePrintable } import gunbc.gate_closure_decline_census { gate_closure_decline_census_lines, @@ -19,12 +20,10 @@ import gunbc.gate_closure_decline_census { // --entry dag/gunbc/instruments/gate_closure_decline_census_instrument.dag \ // --function gate_closure_decline_census --arg root= --arg run= // The counts are the run's, never this file's: a citation names the run, and this entry re-derives. -data gate_closure_decline_census_file: String = "required_floor_disposition.tsv" - // AN UNREADABLE ROSTER REFUSES rather than printing an empty census: an empty declined set and a // missing roster are different facts, and only the first is good news. fn gate_closure_decline_census(root: String, run: String) -> CliWireResponse { - let path = root + "/" + run + "/" + gate_closure_decline_census_file + let path = root + "/" + run + "/" + required_floor_disposition_path let read = Filesystem.Read(path: path) if !read.success { CliWirePrintable { bytes: "", exit: exit_failure(reason: "gate closure decline census: unreadable " + path) }