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
44 changes: 34 additions & 10 deletions dag/gunbc/discovery_census.dag
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ import gunbc.build_target {
import v2.workflow.required_floor {
RequiredFloorDisposition,
Planned, PlannedAsChangedWitness, DeclinedLongModule, DeclinedFixtureMember, DeclinedCostDebt,
DeclinedOutsideRequiredGate, DeclinedOutsideGateClosure, DeclinedDiscoveryExcluded,
DeclinedOutsideRequiredGate, DeclinedOutsideGateClosure, DeclinedDiscoveryExcluded, DeclinedNoCiWetLane,
required_floor_site_disposition,
}
import v2.std.live_tree { LiveTreeDisposition }
Expand Down Expand Up @@ -265,6 +265,8 @@ fn census_partition_step(acc: CensusPartition, row: CensusRow) -> CensusPartitio
CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) }
DeclinedDiscoveryExcluded { matched_substring: _ } =>
CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) }
DeclinedNoCiWetLane { pattern: _ } =>
CensusPartition { planned: acc.planned, declined: concat([row], acc.declined) }
}
}

Expand Down Expand Up @@ -338,6 +340,7 @@ type CensusCounts {
declined_outside_required_gate: Int
declined_outside_gate_closure: Int
declined_discovery_excluded: Int
declined_no_ci_wet_lane: Int
}

fn census_counts_zero() -> CensusCounts {
Expand All @@ -349,7 +352,8 @@ fn census_counts_zero() -> CensusCounts {
declined_cost_debt: 0,
declined_outside_required_gate: 0,
declined_outside_gate_closure: 0,
declined_discovery_excluded: 0
declined_discovery_excluded: 0,
declined_no_ci_wet_lane: 0
}
}

Expand All @@ -364,7 +368,8 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu
declined_cost_debt: counts.declined_cost_debt,
declined_outside_required_gate: counts.declined_outside_required_gate,
declined_outside_gate_closure: counts.declined_outside_gate_closure,
declined_discovery_excluded: counts.declined_discovery_excluded
declined_discovery_excluded: counts.declined_discovery_excluded,
declined_no_ci_wet_lane: counts.declined_no_ci_wet_lane
}
PlannedAsChangedWitness =>
CensusCounts {
Expand All @@ -375,7 +380,8 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu
declined_cost_debt: counts.declined_cost_debt,
declined_outside_required_gate: counts.declined_outside_required_gate,
declined_outside_gate_closure: counts.declined_outside_gate_closure,
declined_discovery_excluded: counts.declined_discovery_excluded
declined_discovery_excluded: counts.declined_discovery_excluded,
declined_no_ci_wet_lane: counts.declined_no_ci_wet_lane
}
DeclinedLongModule { matched_prefix: _ } =>
CensusCounts {
Expand All @@ -386,7 +392,8 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu
declined_cost_debt: counts.declined_cost_debt,
declined_outside_required_gate: counts.declined_outside_required_gate,
declined_outside_gate_closure: counts.declined_outside_gate_closure,
declined_discovery_excluded: counts.declined_discovery_excluded
declined_discovery_excluded: counts.declined_discovery_excluded,
declined_no_ci_wet_lane: counts.declined_no_ci_wet_lane
}
DeclinedFixtureMember { matched_prefix: _ } =>
CensusCounts {
Expand All @@ -397,7 +404,8 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu
declined_cost_debt: counts.declined_cost_debt,
declined_outside_required_gate: counts.declined_outside_required_gate,
declined_outside_gate_closure: counts.declined_outside_gate_closure,
declined_discovery_excluded: counts.declined_discovery_excluded
declined_discovery_excluded: counts.declined_discovery_excluded,
declined_no_ci_wet_lane: counts.declined_no_ci_wet_lane
}
DeclinedCostDebt =>
CensusCounts {
Expand All @@ -408,7 +416,8 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu
declined_cost_debt: counts.declined_cost_debt + 1,
declined_outside_required_gate: counts.declined_outside_required_gate,
declined_outside_gate_closure: counts.declined_outside_gate_closure,
declined_discovery_excluded: counts.declined_discovery_excluded
declined_discovery_excluded: counts.declined_discovery_excluded,
declined_no_ci_wet_lane: counts.declined_no_ci_wet_lane
}
DeclinedOutsideRequiredGate =>
CensusCounts {
Expand All @@ -419,7 +428,8 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu
declined_cost_debt: counts.declined_cost_debt,
declined_outside_required_gate: counts.declined_outside_required_gate + 1,
declined_outside_gate_closure: counts.declined_outside_gate_closure,
declined_discovery_excluded: counts.declined_discovery_excluded
declined_discovery_excluded: counts.declined_discovery_excluded,
declined_no_ci_wet_lane: counts.declined_no_ci_wet_lane
}
DeclinedOutsideGateClosure =>
CensusCounts {
Expand All @@ -430,7 +440,8 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu
declined_cost_debt: counts.declined_cost_debt,
declined_outside_required_gate: counts.declined_outside_required_gate,
declined_outside_gate_closure: counts.declined_outside_gate_closure + 1,
declined_discovery_excluded: counts.declined_discovery_excluded
declined_discovery_excluded: counts.declined_discovery_excluded,
declined_no_ci_wet_lane: counts.declined_no_ci_wet_lane
}
DeclinedDiscoveryExcluded { matched_substring: _ } =>
CensusCounts {
Expand All @@ -441,7 +452,20 @@ fn census_counts_add(counts: CensusCounts, d: RequiredFloorDisposition) -> Censu
declined_cost_debt: counts.declined_cost_debt,
declined_outside_required_gate: counts.declined_outside_required_gate,
declined_outside_gate_closure: counts.declined_outside_gate_closure,
declined_discovery_excluded: counts.declined_discovery_excluded + 1
declined_discovery_excluded: counts.declined_discovery_excluded + 1,
declined_no_ci_wet_lane: counts.declined_no_ci_wet_lane
}
DeclinedNoCiWetLane { pattern: _ } =>
CensusCounts {
offered: counts.offered + 1,
planned: counts.planned,
declined_long_module: counts.declined_long_module,
declined_fixture_member: counts.declined_fixture_member,
declined_cost_debt: counts.declined_cost_debt,
declined_outside_required_gate: counts.declined_outside_required_gate,
declined_outside_gate_closure: counts.declined_outside_gate_closure,
declined_discovery_excluded: counts.declined_discovery_excluded,
declined_no_ci_wet_lane: counts.declined_no_ci_wet_lane + 1
}
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ data doctrine_safety_claim_stated_wider_than_the_census_that_delivers_it: Recurr

"BOUNDARY AGAINST [[check_subject_narrower_than_its_declared_claim]], which is the same asymmetry one layer down. There a CHECK is cited for a population wider than the one its implementation ranges over, and the repair is to widen the check or narrow its citation. Here there is no defective check to widen: the substrate's refusal is total and correct at every site it reaches, and the floor's selection is a priced ruling rather than an accident of first implementation -- which is precisely the distinction that row makes load-bearing when it says the narrowing `is never a decision`. Here it WAS a decision. The narrowness lives only in the JOIN between a doctrine's stated subject and a mechanism's signed subject, which is why the population is prose in `gunbc.design_document` rather than any executing declaration.",

"THE POPULATION IS NAMED BY ITS PRODUCER AND NOT TRANSCRIBED, because a count of unqualified safety sentences copied here would rot beside the document it describes. The candidates are the sentences of `gunbc.design_document` that assert a guarantee in the present tense over a substrate-grain subject; the mechanisms they could rest on are the required lanes rostered at `gunbc.witness_floor_workflow` `required_lanes_roster` and the prefix roster at `v2.workflow.required_floor` `required_gate_prefixes`, read beside the standing drops at `gunbc.rung_drop`. `the deletion is the census` is the one adjudicated. No number is recorded here and none may be quoted from this row.",
"THE POPULATION IS NAMED BY ITS PRODUCER AND NOT TRANSCRIBED, because a count of unqualified safety sentences copied here would rot beside the document it describes. The candidates are the sentences of `gunbc.design_document` that assert a guarantee in the present tense over a substrate-grain subject; the mechanisms they could rest on are the required lanes rostered at `gunbc.witness_floor_lanes` `required_lanes_roster` and the prefix roster at `v2.workflow.required_floor` `required_gate_prefixes`, read beside the standing drops at `gunbc.rung_drop`. `the deletion is the census` is the one adjudicated. No number is recorded here and none may be quoted from this row.",

"RUNG FOUND AT: 1, mitigatable, and the mitigation is that a reader happened to read a review. Nothing holds this class today: the doctrine is prose, no `Accepted` program can read it (DESIGN section 4c), and the one instrument that could have contradicted it -- the required floor -- reported SUCCESS on the named runs while the modules where the doctrine failed sat outside that run's prepared closure. CEILING: 2, mechanically preventable, and the ceiling is honestly 2 and not higher because the subject is an authored English sentence whose intended scope is not derivable from any modeled fact; what IS derivable is the gate's admitted subject, so a doctrine sentence can be REQUIRED to cite the mechanism it rests on and that citation can be joined against the mechanism's actual subject. Making the unqualified sentence unwritable would need the doctrine itself modeled as a claim with a declared subject, which is not a capability this repo has or has planned.",

Expand Down
3 changes: 2 additions & 1 deletion dag/gunbc/repo/repo_ruleset.dag
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,8 @@ import std.process { ProcessExit, ExitSuccess, exit_failure }
import std.types { HttpStatus, NonEmptyStr }
import std.dissolution { DissolutionCondition, unbound_dissolution }
import gunbc.repository { gunbc_repository }
import gunbc.witness_floor_workflow { witness_floor_workflow_job_id, witness_floor_lane_timeout, required_lanes_roster }
import gunbc.witness_floor_workflow { witness_floor_workflow_job_id, witness_floor_lane_timeout }
import gunbc.witness_floor_lanes { required_lanes_roster }
import std.measure { Minute, minute, minute_count, measure_add, MergeQueueEntryCount, merge_queue_entry_count, merge_queue_entry_count_value }
import gunbc.ensure {
EnsurePolicy,
Expand Down
53 changes: 1 addition & 52 deletions dag/gunbc/required_lanes_gate.dag
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ import gunbc.floor_attempt_standing {
import gunbc.ci_failure_class { floor_outcome_wire_infra, floor_outcome_wire_structural }
import v2.std.node { Node }
import std.types { String, List }
import gunbc.witness_floor_lanes { RequiredLane }

// THE REQUIRED AGGREGATOR'S REFUSAL, CONSTRUCTED AS NODES RATHER THAN SPELLED AS TEXT.
//
Expand Down Expand Up @@ -209,58 +210,6 @@ fn required_lanes_head_standing_stmts(
]
}

// THE REQUIRED LANE, AS ONE CONCEPT WITH N INSTANCES RATHER THAN N NAMED PARAMETERS.
//
// This axis was a HARDCODED PAIR -- `build_var` beside `floor_var`, threaded through four
// functions and spelled 28 times -- which is one concept given one name per instance, the fork
// DESIGN section 2 horizontal exists to delete. The tell was mechanical: promoting a third job
// into the aggregate was described by `gunbc.witness_floor_workflow` as a one-row edit, and was
// in fact a signature change in four places plus a step-name rewrite, because the gate could not
// say "a lane" at all -- only "the build one" and "the floor one".
//
// A LANE IS THREE FACTS AND NOT ONE, and each is read by a different surface: the JOB ID is what
// the workflow's `needs.<id>.result` expression names, the VARIABLE is what the emitted shell
// reads, and the LABEL is what the receipt prints. They are genuinely distinct strings -- the job
// id is `required-witnesses-build`, the variable `BUILD`, the label `build` -- so collapsing any
// two would force one surface to derive its spelling from another's, which is a nickname for a
// fact the caller already holds. Carrying all three is what lets the gate AND the step's `env`
// block be projections of one roster instead of two hand-kept lists whose agreement nothing
// checks.
//
// NON-EMPTY BY CONSTRUCTION, and that is the whole safety argument for the shape. The verdict is
// an OR-fold over the lanes, and an or-fold over nothing is FALSE -- so an empty lane list would
// publish the required context GREEN over a gate that read no lane at all, which is section 5's
// fail-open in its purest form. `FreeSemigroup` has no empty representation, so that state is
// UNWRITABLE rather than validated: the structurally-impossible rung of section 4b rather than
// the mechanically-preventable one, and no refusal arm is owed because there is no arm to write.
//
// THE BOUNDARY THAT GUARANTEE HOLDS AT, stated because section 4b says unwritable in the ACCEPTED
// CORPUS and unwritable as SOURCE HANDED TO THE COMPILER are different claims and only the second
// decides whether a RED is authorable. MEASURED, not reasoned: a fixture module authoring
// `FreeSemigroup { tail: [] }` was handed to the compiler on 2026-09-02 and refused with
// `error: missing required field 'head' in literal of type 'FreeSemigroup'`, located at the
// literal -- one blocking error. So the empty roster is authorable as fixture source and is
// refused there, which is the stronger of the two boundaries.
//
// WHAT THAT DOES NOT ESTABLISH, AND THE TRIGGER IS OWNED ELSEWHERE. The refusal is the compiler's
// GENERAL record-completeness wall, not anything this roster authored, and the roadmap node
// `floor-record-construction-wall` (rn_ILWLG34LVL5SAS6QPN5GZDPMFY) records that wall's own
// evidence as NOT YET ENROLLED -- in its words, a construction wall "currently rests on
// record-completeness enforcement that is itself unmeasured" -- the refusal measured here is
// recorded as that node's executed RED specimen rather than restated. So this roster's rung is section
// 4b(4) CONDITIONAL ON that wall, and its next-rung trigger is that node's probe-pairing rather
// than anything in this file. A per-consumer fixture asserting the same refusal is deliberately
// NOT added here: it would be one more monomorphised copy of a corpus-wide property, the same
// duplication declining a sixth NonEmpty carrier avoids.
// It is deliberately not a fresh NonEmptyRequiredLanes carrier — that would re-invent
// std.algebra FreeSemigroup.
type RequiredLane {
job_id: String,
label: String,
var_name: String,
class_var_name: String
}

// THE OR-FOLD OVER THE LANES, left-associated so that the two-lane case is the exact node the
// hardcoded pair built: `or_else(left: test(first), right: test(second))`.
fn required_lanes_any_test(lanes: FreeSemigroup<RequiredLane>, mk: fn(String) -> Node) -> Node {
Expand Down
Loading