diff --git a/.github/workflows/witnesses.yml b/.github/workflows/witnesses.yml index c2d590b6b55..9c31ac32620 100644 --- a/.github/workflows/witnesses.yml +++ b/.github/workflows/witnesses.yml @@ -466,6 +466,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..2ac79151341 --- /dev/null +++ b/dag/gunbc/gate_closure_decline_census.dag @@ -0,0 +1,136 @@ +module gunbc.gate_closure_decline_census + +import std.types { Bool, Int, String } +import std.optional { Present, Absent } +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 +// 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 = 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 ModuleDeclineCount { + module: String + claims: Int +} + +// 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 } + +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 { + let fields = split(s: line, delimiter: "\t") + match fields[0] { + Absent => DispositionLineRefused { cause: "no identity column" } + Present { value: identity } => match fields[1] { + Absent => DispositionLineRefused { cause: "fewer than two tab-separated columns" } + Present { value: disposition } => + if !contains(required_floor_disposition_names, disposition) { + DispositionLineRefused { cause: "disposition outside the floor's vocabulary: " + disposition } + } else { + DispositionLineRow { identity: identity, disposition: disposition } + } + } + } + } +} + +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 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: 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 } + } + } + } + } + }) + 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). +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(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( + 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..1d6c28e035c --- /dev/null +++ b/dag/gunbc/instruments/gate_closure_decline_census_instrument.dag @@ -0,0 +1,38 @@ +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, + 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: +// 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. +// 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 + "/" + 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) } + } else { + 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/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/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 46b7a6eedb5..3ac831dd27e 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 @@ -48,6 +48,7 @@ data witness_outside_gate_closure_falsified_by_other_file: RecurringFailureMode "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-04 (swift-bat-688), THE CLAIM-ROOT DEBT CENSUSED BY EXECUTION, AND ONE UNROSTERED NAME WAS HIDING THE REST. Subject: the 86 claim-root files that hold 494 ActiveDebt rows of v2.workflow.floor_unimported_bare_provider_debt_roster. Instrument: claim_batch per file with every test fn named, built from the tree in the dispatch on BuildBuddy. NONE OF THE 86 IS IN THE GATE, read from v2.workflow.required_floor required_gate_admits, whose selectors are eleven family prefixes and sixteen named modules and nothing else; so this population is outside the gate, not inside it and masked, and each file runs only when its own file is touched. FIRST PASS: 76 files refused at the entry and ran nothing, 1 failed to resolve, 3 passed, 1 ran with failures, 5 declare no claim. Seventy of the 76 stopped on the same pair: the file declares data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly, has imports, imports neither name, and the roster carries no row for LiveTreeDisposition in any file. WHY THE SEED HAD NO ROW: gunbc#12205 seeded from a byte scanner (bare_identifier_candidates) that classed any identifier directly followed by = as an assignment binder, so the annotation type in data x: T = v was bound and never a reference, while the value on the same line was rostered. gunbc#12609 replaced the scanner with the parsed reference walk, which does derive the type, but the roster edit judgment refuses a gained identity, so the newly derived pairs became Unrostered and not debt, refused only where the file is an entry or is touched. The class is any simple type annotation directly before =; measured over all 2534 claim files with imports in one gate run it hid this one name at scale and five other pairs. SECOND PASS, WITH THE TWO NAMES IMPORTED: 34 files run and pass, 4 run with failing claims, 37 fail to resolve with effect-summary-incomplete and run nothing, 6 still refuse at the entry, none resolves to zero claims. So the first refusal was masking 37 files of the same class as the receipt above, which is the population the next repairs own. TWO THINGS THE REPAIR ITSELF TAUGHT. Importing only the type puts the declaring module in the import closure, the variant then resolves through it, and the variant rows turn RosterStale, so the import names both and the variant rows retire as ImportsFixed. And retiring any row in a file makes the gate re-derive that file on every run: dag/test/claim/budget_tree_witness_test.dag holds an ActiveDebt row for Evicted, which is now declared in two modules and so has no derivable provider, and one retirement in that file made its stale row refuse EVERY entry in the tree. A stale row is latent until its file gains a retirement. AND THE LANDING CONSTRAINT: touching a witness file enrols it as a changed witness and holds it to the unrostered rule, so a mechanical import over a hundred files is executed by the floor file by file and cannot land over files whose deeper debt does not resolve. The import therefore lands first on the files that pass when touched, and every other file receives it together with its own repair.", + "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: [], diff --git a/dag/gunbc/witness/compiler_gate_workflow.dag b/dag/gunbc/witness/compiler_gate_workflow.dag index 3d0913bf306..7d0cf0e9fea 100644 --- a/dag/gunbc/witness/compiler_gate_workflow.dag +++ b/dag/gunbc/witness/compiler_gate_workflow.dag @@ -122,6 +122,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 } @@ -866,7 +867,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", 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..e3ae623a9d4 --- /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 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 + } +}