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
8 changes: 8 additions & 0 deletions .github/workflows/witnesses.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
136 changes: 136 additions & 0 deletions dag/gunbc/gate_closure_decline_census.dag
Original file line number Diff line number Diff line change
@@ -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<String> = 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<String> = ["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<String> }
| 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<String> }
| 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<String>) -> 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<String>) -> List<ModuleDeclineCount> {
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<String>) -> List<String> {
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)
)
)
}
38 changes: 38 additions & 0 deletions dag/gunbc/instruments/gate_closure_decline_census_instrument.dag
Original file line number Diff line number Diff line change
@@ -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 <run-id> -n required-floor-disposition -D <root>/<run-id>
// 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=<root> --arg run=<run-id>
// 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 }
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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 },
],
}
Loading