diff --git a/dag/gunbc/floor_non_verdict_enrollment.dag b/dag/gunbc/floor_non_verdict_enrollment.dag new file mode 100644 index 00000000000..3f2cd04c667 --- /dev/null +++ b/dag/gunbc/floor_non_verdict_enrollment.dag @@ -0,0 +1,247 @@ +module gunbc.floor_non_verdict_enrollment + +import std.types { List, String, Int } +import std.decl_ref { DeclarationRef, decl_ref, WholeDeclaration } +import std.dissolution { DissolutionCondition, unbound_dissolution } +import gunbc.seed_growth { SeedGrowthJustification } +import gunbc.roadmap_authority { RoadmapNodeId } + +// AN EXPECTED-RED ENROLLMENT DISCHARGED BY AN OUTCOME THAT IS NOT A VERDICT, REPORTED AND NOT +// GATING. +// +// v1_compiler.cli_run run_required_floor routes an enrolled identity that THREW to +// known_red_runtime_errored and one that answered a non-Bool to known_red_observation_unreadable, +// and its own message says why: "Enrollment asserts an expected verdict; a claim that threw +// produced none." Both collections are printed by claim_executor report_required_floor_outcome and +// NEITHER is read by required_floor_outcome_is_clean, whose comment records the choice: they "are +// REPORTED and deliberately NOT gating", because making them block "reds lanes with no connection +// to the defect, which needs an approved design and a shadow phase rather than an author's +// judgement". +// +// THAT CHOICE IS NOT RESTATED HERE AND IS NOT DISPUTED BY THIS MODULE. What is missing is the +// DESIGN section 4b(2) obligation that comes with it: a class below its ceiling must name its +// next-rung trigger and its population, or the stall is untracked. This module carries those two +// facts and nothing else -- no gate, no roster, no second copy of the arms. +// +// WHAT THE HEADLINE LOOKS LIKE WHILE THE CLASS IS OPEN, because that is the harm and it is exactly +// the shape the same receipt line already repaired once for route gaps: the run prints failed=0, +// and a reader takes failed=0 as "nothing is broken". The correcting counters are on the same line +// (known_red_runtime_errored, known_red_observation_unreadable) -- which is why this is a stall +// rather than a silence -- but the population they count has never been sized, classified, or +// bound. + +// WHAT AN ENROLLED IDENTITY ACTUALLY DID INSTEAD OF ANSWERING. One variant per cause the census +// below observed, and no variant for a cause it did not: an arm nothing measured would be +// vocabulary claiming coverage. These are causes of the THROW, not a taxonomy of witness defects -- +// a name that does not resolve in the run's loaded index and a call whose contract does not match +// have different owners and different repairs, which is the whole reason the census splits them. +type NonVerdictCause + = NameNotInLoadedIndex + | TypeError + | UndefinedVariable + | CallContractMismatch + +type NonVerdictCauseCount { + cause: NonVerdictCause + identities: Int +} + +// THE POPULATION IS MEASURED, AND THE MEASUREMENT IS A SNAPSHOT OF ONE RUN -- NOT A BOUND. +// +// DESIGN section 4b(3) requires a bounded population and section 5 rules that a count copied from +// the current tree is not an oracle. Both apply here and neither is satisfied by a number: nothing +// counts a witness that starts throwing after this row was written, and nothing refuses one. So the +// basis is carried as an arm rather than implied by the presence of a figure, and the figure below +// is what the named run measured at the moment it ran. +type PopulationBasis + = MeasuredOnOneRun { run: String, head_commit: String } + | BoundedByRefusal { refusal: String } + +// A REPAIR IS ALREADY IN FLIGHT AGAINST THIS POPULATION, AND THE ROW IS DELIBERATELY NOT +// PRE-ADJUSTED FOR IT. gunbc#9020 resolves 99 of the 142 -- measured, not projected: its branch +// head c767f4c962 runs 43 where the base runs 142, over an identical planned population of 10791. +// The figure below is what MAIN reports, which is the only population any floor run today +// measures, and writing 43 here would be a count copied from a branch that has not landed -- +// exactly the fix-carrying baseline that produced the false regression this carrier was dispatched +// under. The row is re-measured when that PR merges, and the basis arm is what says it must be. +// +// THE FALSE REGRESSION THE LINE ABOVE NAMES, stated once so the reference resolves: the brief was +// that 99 witnesses went PASSED -> RUNTIME-ERRORED across 330f63c514..5482863b4e while the floor +// reported failed=0. An identity-set diff shows no such transition -- the 99 were baselined +// against a branch head already carrying the fix, so they were compared to a tree they never ran +// in. The brief was wrong about the cause and right about the smell, and the smell is this module. +// +// THE MEASUREMENT IS NOT TRANSCRIBED IN PROSE ANYWHERE, per the 2026-08-24 bankruptcy ruling +// (#9132: name the instrument, never transcribe its output). It lives below as typed rows whose +// PopulationBasis names the run and head each was measured on, so a reader can tell a figure from +// a receipt -- the distinction a markdown board cannot carry. A probe document holding these same +// counts was deleted from this change for that reason, rather than left as the one file +// re-establishing a corpus main had just emptied. +data floor_non_verdict_population_basis: PopulationBasis = MeasuredOnOneRun { + run: "github actions witnesses.yml run 32681700364", + head_commit: "5482863b4e8c01c91bb0261481acfd727cea552b", +} + +// THE CAUSE CENSUS AS MEASURED ON THAT RUN. The sum is the run's known_red_runtime_errored figure; +// known_red_observation_unreadable was 0 on the same run, so every non-verdict identity in this +// population threw. +data floor_non_verdict_cause_census: List = [ + { cause: NameNotInLoadedIndex, identities: 119 }, + { cause: TypeError, identities: 13 }, + { cause: UndefinedVariable, identities: 9 }, + { cause: CallContractMismatch, identities: 1 }, +] + +data floor_non_verdict_measured_total: Int = 142 + +// THE DOMINANT CAUSE IS AN AUTHORED WITNESS DEFECT, NOT A FLOOR SCOPE DEFECT, and the distinction +// is stated because it decides who owns the repair. Four of the unresolved names were checked +// against the corpus by hand: every one IS declared (gunbc.design_argument design_argument, +// gunbc.srv3_os_install_diagnostic srv3_install_hang_no_router_lease_ms, +// v2.std.algebra_laws.nat_semiring nat_add_left_identity_input, +// v2.lens.extdeps_shape_transport_policy.module_refs extdeps_cargo_build_module) and the witness +// referencing it declares no import that would bring it into the run's loaded index. The refusal is +// correct; the witness is unimportable. That is why the next-rung trigger below is not "widen the +// scope". +// +// THE SAMPLE WAS FOUR AND THE POPULATION HAS A SECOND SHAPE, recorded because four names all +// lacking imports leaves the impression that the whole class does. It does not. An independent +// census of the erroring modules (valiant-lynx-227, run 32743601436) partitions them 53 declaring +// NO import against 8 that DECLARE imports and error anyway, and cross-joining that against the +// cause census here puts SIX of those 8 inside this same no-declaration-named bucket -- so the +// bucket is not homogeneous and a repairer working from the four names above would be surprised +// by the sixth file they opened. +// +// ONE OF THE SIX READ IN FULL, so the second shape is named from evidence rather than inferred: +// `v2.lens.vacuity_test` fails on `nat_add_left_identity_input` while declaring ten imports -- +// including `v2.test.nat_semiring.rung_5`, a module that REFERENCES that name but is not the +// module that DECLARES it (`v2.std.algebra_laws.nat_semiring`). Importing a module does not +// transitively supply the names ITS OWN declarations reach for. So the second shape is an +// INCOMPLETE import set rather than an absent one. +// +// THE CONCLUSION IS UNCHANGED AND SLIGHTLY STRENGTHENED: both shapes are authored defects and +// both are repaired by adding the import that declares the referenced name. Neither is a floor +// scope defect, so "widen the scope" is still the wrong trigger. What moves is the repairer's +// expectation, not the remedy. The remaining five of the six are established only as "declares +// imports AND lands in this bucket"; each one's specific missing import is unread. +data floor_non_verdict_dominant_cause_specimen: DeclarationRef = decl_ref(module_path: "test.claim.design_argument_witness", decl_name: "design_s1_argument_form_is_valid") + +// RUNG, PER SEAM, AND THE GOVERNING RUNG IS THE MINIMUM ACROSS THEM. +// +// An earlier revision of this row read "the class sits at MITIGATABLE: every identity is typed, +// located and counted on the receipt line, and the line does not stop", with the gating conjunct +// named as a next rung. That was too generous, and the correction is a ruling rather than a +// rewording: THE OBSERVATION ARM IS NOT THE DEFECT. `known_red_runtime_errored` and +// `known_red_observation_unreadable` say something TRUE -- this enrolled claim produced no +// Boolean verdict. What was wrong is the COMPOSITION that read them: +// +// routing a thrown claim into its arm ................ mitigatable +// printing the count on the receipt line ............. mitigatable +// printing `failed=0` without distinguishing +// verdict incompleteness ........................... misleading projection +// returning CLEAN while an enrolled claim +// produced no verdict .............................. BELOW FLOOR +// +// Below floor is not a rung. It is outside the ladder and forbidden outright, so it is not a +// stall to be tracked -- which is what the earlier revision made it -- and the remedy could not +// wait on the population being repaid. A diagnostic can describe the evidence truthfully while +// the gate draws a false conclusion from it, and that gap is where this class lived. +// +// WHAT CLOSED IT, and what deliberately did not. `v2.workflow.floor_non_verdict` freezes the +// population's GROWTH at identity grain: an enrolled identity that produces no verdict and is +// not on that roster stops the line. The two arms themselves are still not gating conjuncts, +// and making them so is still not this author's call -- the ruling did not change that half. +// So 142 -> 0 is admitted in any order, 142 -> 143 refuses, and a swap that leaves the count +// unmoved refuses too, which is the case that makes the identity-grain decision load-bearing +// rather than incidental. +// THE DECISION NOW HAS TWO IMPLEMENTATIONS, AND THE CLASS RUNG IS THE MINIMUM ACROSS THEM. +// +// `v2.workflow.floor_non_verdict_admission` models the admission -- added = observed - roster, +// admit iff added is empty -- and `v1_compiler.cli_run` `non_verdict_admission` recomputes it +// over two HashSets. That is a second representation of one rule, and it is recorded here rather +// than left for a reader to notice, on exactly the footing the corpus already uses for the same +// shape: `v1_compiler.required_regen_host` `run_required_regen` mirrors its carrier's ordering BY +// HAND and is therefore only MITIGATABLE, with its next-rung trigger declared as the host being +// derived from the carrier rather than written beside it. +// +// So: the modeled half may reach a higher rung; THE SEED HALF IS MITIGATABLE UNTIL DERIVED, and +// the class rung is the minimum, which is mitigatable. What keeps that honest rather than +// nominal is that the seed half carries its OWN discriminating red -- `non_verdict_admission` is +// a pure function of two identity sets precisely so it can be refuted without a floor run, and +// `floor_non_verdict_admission_seed_path` drives growth, the equal-count swap, and the empty +// roster through the code that actually gates. What that test does NOT reach is the wiring from +// a real thrown witness into the observed set; that is the residual gap and it is named here +// rather than papered over. + +// THE WALL HAS TWO AXES AND ONLY ONE OF THEM EXECUTES. +// +// OBSERVED-VS-ROSTER is walled by execution every run: the two sets must be equal, growth and +// stale exemptions both refuse. ROSTER-VS-BASE-ROSTER is not walled at all. Nothing compares the +// roster authored at HEAD against the one admitted at the MERGE BASE, so a change that makes a +// new identity stop producing a verdict may add its row in the same change, satisfy both +// executing arms, and be admitted -- the roster legalising the regression it exists to bound. +// +// That is the same shape review 55361 caught for stale rows (the row becomes the permission), +// reached through authorship instead of through survival, and it is recorded here rather than +// left for a reader to infer from the wall's name. It is also the honest price of the +// single-run design: the admission was specified against a BASE OBSERVATION, and substituting +// the roster for it is what makes the wall runnable in one pass -- sound exactly to the degree +// the roster cannot be grown freely. +// +// RUNG ON THIS AXIS: MITIGATABLE -- confined by review diligence, which is strictly weaker than +// execution. The class rung stays the minimum across axes and paths, which is mitigatable. + +// THE FUTURE AUTHORITY IS THE TARGET-BASE TIP, NOT THE MERGE BASE, and an earlier revision of +// this trigger named the merge base. That is not a wording preference: EXEMPTION RESURRECTION. +// Let M be the roster at the historical merge base, B the roster at the current base tip, H the +// roster in the composed result, O the observed population. +// +// M = {a}. Main later repairs `a` and deletes its row, so B = {}. A stale branch reintroduces +// `a` and it throws: H = {a}, O = {a}. Then O = H passes, and H subset-of M PASSES -- readmitting +// an exemption main has already paid off. H subset-of B fails, which is the law actually wanted. +// +// The mirror is a FALSE RED: a row main legitimately adds after the fork is in B and in the +// composed result, but not in M, so a subset-of-M rule refuses a branch that did nothing wrong. +// +// CONSEQUENCE FOR THE CUT'S SHAPE, worth knowing before it is scoped: a BRANCH-HEAD-ONLY RUN +// CANNOT ESTABLISH THIS LAW. It needs the composed result AND that result's base parent, which +// is strictly stronger than "read the roster at another commit". + +data floor_non_verdict_roster_growth_next_rung_trigger: DissolutionCondition = unbound_dissolution(description: "dissolve-on: the required floor establishes H subset-of B -- the roster in the COMPOSED RESULT is a subset of the roster at that result's CURRENT TARGET-BASE PARENT -- refusing when it is not, established by execution against a discriminating red: one composed result carrying a row for an identity the base roster does not carry, refused. NOT the merge base: a merge-base baseline admits exemption resurrection, where main repairs an identity and deletes its row while a stale branch reintroduces it, and it also false-reds a row main legitimately added after the fork. Identity grain, for the same reason the observed-vs-roster admission is: an addition and a deletion in one change leave every count unmoved. RECEIPT THE CUT PINS: target_base_sha, composed_result_sha, base_roster_identity_set, result_roster_identity_set, added_exemptions = result - base; and it refuses when the base subject or its roster cannot be evaluated, the same read-failure polarity the executing arms already carry.") + +data floor_non_verdict_seed_mirror_next_rung_trigger: DissolutionCondition = unbound_dissolution(description: "dissolve-on: v1_compiler.cli_run non_verdict_admission is DERIVED from v2.workflow.floor_non_verdict_admission rather than written beside it -- the same trigger v1_compiler.required_regen_host carries for its hand-mirrored ordering -- at which point the two implementations become one and the minimum-across-paths rung stops being pinned by the seed. Not satisfied by the seed's unit test alone: a discriminating red proves the mirror is correct TODAY, which is what mitigatable means, and does not make a divergence unwritable.") + +data floor_non_verdict_next_rung_trigger: DissolutionCondition = unbound_dissolution(description: "dissolve-on: known_red_runtime_errored and known_red_observation_unreadable are conjuncts of v1_compiler.claim_executor required_floor_outcome_is_clean, established by execution against a discriminating red -- one enrolled identity made to throw, the run refusing. Precondition, not a follow-up: the measured population is repaid to zero first (the unresolved-name majority by giving each witness the import its subject needs, or by deleting the witness), so the conjunct lands over an empty collection rather than converting a counted silence into an uncounted red.") + +// WHERE THE ARMS AND THE GATE ACTUALLY LIVE. Cited rather than copied: this module must not become +// a second account of the seed's routing, which is the fork DESIGN section 3 forbids. +data floor_non_verdict_routing_authority: DeclarationRef = decl_ref(module_path: "v1_compiler.cli_run", decl_name: "run_required_floor") + +data floor_non_verdict_gate_authority: DeclarationRef = decl_ref(module_path: "v1_compiler.claim_executor", decl_name: "required_floor_outcome_is_clean") + +// THE FORWARD-FREEZE ENUMERATION FOR THIS CHANGE'S HAND-AUTHORED RUST. +// +// `gunbc.seed_growth_admission` `seed_growth_forward_freeze_policy_note` requires every PR that +// adds hand-written src/v1 Rust to enumerate exact item identity, .dag authority, why Rust is +// still needed, owning lane, deletion trigger, current boundary, hand-item delta and hand-LOC +// delta -- and rules that unenumerated hand growth is a stop-line, with no netting of deletions +// against additions. This change added hand Rust and shipped without the row; review 55361 +// caught it. The row is authored here, beside the obligation it declares, and joined into the +// closed roster in that module. +data floor_non_verdict_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification { + hand_authored_declarations: [ + DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "NonVerdictAdmission", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "non_verdict_admission", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "non_verdict_admits", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.tests.floor_non_verdict_admission_seed_path", decl_name: "unchanged_population_is_admitted", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.tests.floor_non_verdict_admission_seed_path", decl_name: "repayment_that_leaves_the_row_behind_refuses", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.tests.floor_non_verdict_admission_seed_path", decl_name: "repayment_with_the_row_deleted_is_admitted", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.tests.floor_non_verdict_admission_seed_path", decl_name: "growth_stops_the_line", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.tests.floor_non_verdict_admission_seed_path", decl_name: "a_swap_that_leaves_the_count_unmoved_still_stops_the_line", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.tests.floor_non_verdict_admission_seed_path", decl_name: "an_empty_roster_refuses_every_observed_non_verdict", field: WholeDeclaration } + ], + reason: "WHY RUST IS STILL NEEDED: the required floor executes in the seed. `claim_executor` is the only witness-executing consumer in the tree, so a wall that must stop THAT line has to be readable by it; a modeled admission alone would be a specification with no consumer at the point the run is admitted or refused. The rule itself is modeled in v2.workflow.floor_non_verdict_admission and this Rust is its mirror, not a second authority -- the carrier records the mirror as MITIGATABLE with derivation as its next rung, on the footing v1_compiler.required_regen_host already carries for its hand-mirrored ordering.\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits a change by PURPOSE -- it serves the v2 self-host program. The required floor is the instrument that guards that program, and the defect repaired here is below floor: the composition returned CLEAN while an enrolled expected-red assertion had ceased to assert anything. This is defect repair on the self-host path, not growth of the seed for its own sake, and the roster-plumbing seam it uses is the one floor_route_gap already established.\n\nHAND-ITEM DELTA: +8, enumerated above rather than counted from what was touched. Three are production -- the admission record, the pure function over two identity sets, and the admission predicate -- and five are the unit tests that discriminate it, including the equal-count swap that a count-based implementation passes in silence.\n\nHAND-LOC DELTA: +210/-1 in cli_run.rs, +60/-5 in claim_executor.rs and +102/-0 in the new test file, measured as git diff --numstat against origin/main at the head this row ships on, a large share of it doc comments carrying the receipts and the refusal strings. CORRECTED 2026-08-24 (review 55577): an earlier revision read +195 and +65 and omitted claim_executor's deletions entirely, which is the stale-transcription failure this policy exists to refuse -- a receipt measured once and then not re-measured as the change grew is a figure, not a receipt, and it must be re-measured on every push that touches these files.\n\nWHAT IS NOT GROWTH AND IS NOT LISTED: the two new fields on RequiredFloorOutcome (non_verdict_unenrolled, stale_non_verdict), the new conjuncts inside required_floor_outcome_is_clean, the roster read, and the report lines. None of them adds a declaration -- each modifies an existing item -- so their disposition is ExistingSeedItemModified, and listing them would net modifications into an addition census.", + owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, + trigger: "Delete all eight declarations when the self-emitted claim executor drives the floor's execution, at which point v2.workflow.floor_non_verdict_admission is the sole authority and the seed's copy goes with the rest of the mirror. This is the same trigger the terminal ledger's seam carries and it is joined here rather than restated.", + current_boundary: "v2.workflow.floor_non_verdict_admission non_verdict_admits -> v1_compiler.cli_run non_verdict_admission -> v1_compiler.claim_executor required_floor_outcome_is_clean" +} diff --git a/dag/gunbc/seed_growth_admission.dag b/dag/gunbc/seed_growth_admission.dag index 643a7d8d318..3a944ce5586 100644 --- a/dag/gunbc/seed_growth_admission.dag +++ b/dag/gunbc/seed_growth_admission.dag @@ -6,6 +6,7 @@ import gunbc.roadmap_authority { observation_scoped_run_seed_growth_justificatio import gunbc.witness_runtime_cause_seed_growth { witness_runtime_cause_seed_growth_justification } import gunbc.seed_growth { SeedGrowthJustification } import gunbc.stage0_rust_host_observation { stage0_rust_observation_seed_growth_justification } +import gunbc.floor_non_verdict_enrollment { floor_non_verdict_seed_growth_justification } import gunbc.whole_corpus_compile_admission { whole_corpus_compile_seed_growth_justification } import std.decl_ref { DeclarationRef, WholeDeclaration } import std.disposition { Disposition, RealizationDispatch, Scaffold, SingleAuthority } @@ -41,7 +42,7 @@ type SeedGrowthChangeDisposition data seed_growth_forward_freeze_policy_note: String = "FORWARD-FREEZE POLICY (enforceable now). Every PR that adds hand-written src/v1 Rust MUST enumerate: exact item identity, .dag authority, why Rust is still needed, owning lane, deletion trigger, current boundary, hand-item delta, and hand-LOC delta. Unenumerated hand growth is a stop-line — no netting deletions against additions. Generated Rust is exempt only with generation-authority proof (gunbc.stage0_rust_source_lifecycle_scaffold derived_generated_stage0_repo_paths or gunbc.generated_artifact). This module's G1 join is the mechanical backstop once rust_item_host_observation supplies diff populations; until then the closed roster + witness tests enforce roster honesty." -data seed_growth_justification_roster_note: String = "CLOSED ROSTER of every SeedGrowthJustification row in the corpus. G1 joins new/modified hand items against this list. Rows are authored beside the obligation they declare; the roster is derived by enumeration, never by grep. Today: anonymous_record_resolution_seed_growth_justification (gunbc.anonymous_record_resolution_seed_growth), stage0_rust_observation_seed_growth_justification (gunbc.stage0_rust_host_observation), observation_scoped_run_seed_growth_justification (gunbc.roadmap_authority), whole_corpus_compile_seed_growth_justification (gunbc.whole_corpus_compile_admission), bare_reference_scanner_seed_growth_justification (gunbc.bare_reference_scanner_admission) and witness_runtime_cause_seed_growth_justification (gunbc.witness_runtime_cause_seed_growth). Each new justification adds one row here AND one data row in its owning module. BOTH SIDES OF A ROSTER MERGE ARE KEPT: this is a closed roster, so taking either side whole silently deletes the other authority obligation rather than conflicting -- the last two rows above arrived that way, from two branches that each added one. THIS PROSE LISTING IS ALSO A SECOND REPRESENTATION of seed_growth_justification_roster() and decays independently of it: gunbc#9089 added its import and its roster entry without naming its row here, so the note listed three while the roster carried four, and the omission surfaced only as a merge conflict against a branch that had edited the same sentence. Note that the both-sides rule does not protect against THAT failure -- a row missing from the prose but present in the function conflicts with nothing, so nobody is asked to keep both. The standing fix is to derive the listing from the roster function rather than re-author it; until that lands, every change adding a row must edit this sentence too, which is exactly the maintenance burden that argues for the derivation." +data seed_growth_justification_roster_note: String = "CLOSED ROSTER of every SeedGrowthJustification row in the corpus. G1 joins new/modified hand items against this list. Rows are authored beside the obligation they declare; the roster is derived by enumeration, never by grep. Today: anonymous_record_resolution_seed_growth_justification (gunbc.anonymous_record_resolution_seed_growth), floor_non_verdict_seed_growth_justification (gunbc.floor_non_verdict_enrollment), stage0_rust_observation_seed_growth_justification (gunbc.stage0_rust_host_observation), observation_scoped_run_seed_growth_justification (gunbc.roadmap_authority), whole_corpus_compile_seed_growth_justification (gunbc.whole_corpus_compile_admission), bare_reference_scanner_seed_growth_justification (gunbc.bare_reference_scanner_admission) and witness_runtime_cause_seed_growth_justification (gunbc.witness_runtime_cause_seed_growth). Each new justification adds one row here AND one data row in its owning module. BOTH SIDES OF A ROSTER MERGE ARE KEPT: this is a closed roster, so taking either side whole silently deletes the other authority obligation rather than conflicting -- the last two rows above arrived that way, from two branches that each added one. THIS PROSE LISTING IS ALSO A SECOND REPRESENTATION of seed_growth_justification_roster() and decays independently of it: gunbc#9089 added its import and its roster entry without naming its row here, so the note listed three while the roster carried four, and the omission surfaced only as a merge conflict against a branch that had edited the same sentence. Note that the both-sides rule does not protect against THAT failure -- a row missing from the prose but present in the function conflicts with nothing, so nobody is asked to keep both. The standing fix is to derive the listing from the roster function rather than re-author it; until that lands, every change adding a row must edit this sentence too, which is exactly the maintenance burden that argues for the derivation." // UNCITABLE ITEMS (prose-only until std.decl_ref gains ImplMethod). stage0_rust_observation_seed_growth_justification documents one: impl std::fmt::Display for Stage0CargoBinManifestParseRefusal in v1_compiler.cli_run — seven hand items, six citable DeclarationRef rows. G1 reports uncitable_items separately; they do NOT satisfy the forward-freeze enumeration via DeclarationRef alone. data seed_growth_admission_join_scaffold: Disposition = Scaffold { @@ -71,6 +72,7 @@ data seed_growth_admission_g0_population_note: String = "G0 CENSUS HOST (scripts fn seed_growth_justification_roster() -> List { [ anonymous_record_resolution_seed_growth_justification, + floor_non_verdict_seed_growth_justification, stage0_rust_observation_seed_growth_justification, observation_scoped_run_seed_growth_justification(), whole_corpus_compile_seed_growth_justification, diff --git a/dag/test/claim/floor_non_verdict_enrollment_witness_test.dag b/dag/test/claim/floor_non_verdict_enrollment_witness_test.dag new file mode 100644 index 00000000000..a987a49f713 --- /dev/null +++ b/dag/test/claim/floor_non_verdict_enrollment_witness_test.dag @@ -0,0 +1,40 @@ +module test.claim.floor_non_verdict_enrollment_witness_test + +import std.types { List, Int, Bool } +import v2.std.algebra { fold_list } +import gunbc.floor_non_verdict_enrollment { + NonVerdictCauseCount, PopulationBasis, MeasuredOnOneRun, BoundedByRefusal, + floor_non_verdict_cause_census, floor_non_verdict_measured_total, + floor_non_verdict_population_basis, +} + +data live_tree_disposition: v2.std.live_tree.LiveTreeDisposition = v2.std.live_tree.SubstrateInputsOnly + +fn census_total(rows: List) -> Int { + fold_list(xs: rows, empty: 0, cons: fn(acc, r) { acc + r.identities }) +} + +// THE CENSUS AND THE TOTAL ARE ONE MEASUREMENT WRITTEN TWICE, so they must agree. This is the +// discriminating assertion the module needs: an editor who revises one cause's count from a later +// run and leaves the total alone -- the ordinary way a two-place figure rots -- reds here rather +// than shipping a census that sums to something the receipt never printed. +test fn non_verdict_cause_census_sums_to_the_measured_total() -> Bool { + census_total(rows: floor_non_verdict_cause_census) == floor_non_verdict_measured_total +} + +// EVERY CAUSE CARRIES A POSITIVE COUNT. A zero row is a cause nothing measured, and DESIGN's rule +// against speculative vocabulary applies to the row as much as to the variant: an arm kept at zero +// claims coverage of a cause this population does not exhibit. +test fn every_declared_cause_was_actually_measured() -> Bool { + fold_list(xs: floor_non_verdict_cause_census, empty: true, cons: fn(acc, r) { acc && r.identities > 0 }) +} + +// THE POPULATION IS DECLARED AS A SNAPSHOT AND NOT AS A BOUND. This reds the day someone rewrites +// the basis to BoundedByRefusal without a refusal existing -- which is exactly the next-rung +// transition, and it should not be assertable by editing this row alone. +test fn population_basis_is_a_measured_snapshot_not_a_bound() -> Bool { + match floor_non_verdict_population_basis { + MeasuredOnOneRun { run: _, head_commit: _ } => true + BoundedByRefusal { refusal: _ } => false + } +} diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 02bb1bf9df0..81ae58b30fd 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -12034,27 +12034,82 @@ fn report_required_floor_outcome(outcome: &v1_compiler::cli_run::RequiredFloorOu for unreadable in &outcome.known_red_observation_unreadable { eprintln!("required-floor: KNOWN-RED-OBSERVATION-UNREADABLE {unreadable}"); } + for unenrolled in &outcome.non_verdict_unenrolled { + eprintln!("required-floor: NON-VERDICT-UNENROLLED {unenrolled}"); + } + for stale in &outcome.stale_non_verdict { + eprintln!("required-floor: STALE-NON-VERDICT {stale}"); + } for gap in &outcome.route_gap { eprintln!("required-floor: ROUTE-GAP {gap}"); } for stale in &outcome.stale_route_gap { eprintln!("required-floor: STALE-ROUTE-GAP {stale}"); } + // THE VERDICT LINE, AND WHY A ZERO NEEDED A SENTENCE BESIDE IT. + // + // `failed=0` is a sentence a reader can finish alone, and finishes wrongly: it says nothing + // about whether the population that was supposed to answer actually answered. This exact + // misreading dispatched a session against a regression that did not exist — a run was + // compared to a baseline carrying a fix, `planned` matched on both sides, and `failed=0` + // supplied the confidence that the rest was equivalent. Separating the two questions removes + // the ability to finish that sentence: `unexpected_failures` is how many claims answered + // WRONG, `verdict_incomplete` is how many never answered AT ALL, and a run can be admitted + // while the second is large. + // + // ADMITTED IS NOT CLEAN, and the word carries that. `FloorAdmittedWithNonVerdictDebt` gates + // nothing by itself — the conjunct that gates is growth in the non-verdict population — but + // it refuses to let a run with 142 unanswered assertions render identically to one with + // none. + let verdict_incomplete = + outcome.known_red_runtime_errored.len() + outcome.known_red_observation_unreadable.len(); + let verdict = if !required_floor_outcome_is_clean(outcome) { + "FloorRefused" + } else if verdict_incomplete > 0 { + "FloorAdmittedWithNonVerdictDebt" + } else { + "FloorClean" + }; + eprintln!( + "required-floor: verdict={verdict} unexpected_failures={} verdict_incomplete={} \ + non_verdict_unenrolled={} stale_non_verdict={}", + outcome.failures.len(), + verdict_incomplete, + outcome.non_verdict_unenrolled.len(), + outcome.stale_non_verdict.len() + ); } /// Whether the floor outcome permits a green run. /// -/// SEVEN CAUSES, ONE STOPPED LINE — and the conjunction is written once here rather than at each +/// NINE CAUSES, ONE STOPPED LINE — and the conjunction is written once here rather than at each /// caller, because a mode that forgot one of them would green a run the other refused. (The /// count is stated because a reader checks it; it was five before main added `route_gap` and /// `stale_route_gap`, and the sentence went on saying five through the merge that added them. /// It briefly said nine while `known_red_runtime_errored` and `known_red_observation_unreadable` -/// were wired in here; they are REPORTED and deliberately NOT gating, so the count is seven -/// again. Making them block reds lanes with no connection to the defect, which needs an -/// approved design and a shadow phase rather than an author's judgement — and the honest -/// reporting half does not have to wait for that decision.) +/// were wired in here directly; that was reverted and the count returned to seven.) +/// +/// THE EIGHTH IS `non_verdict_unenrolled`, AND IT IS NOT THOSE TWO ARMS MADE GATING. The +/// distinction is the whole design. Those arms are HONEST OBSERVATIONS — they say correctly that +/// an enrolled claim produced no verdict — and gating on them directly would red every lane +/// holding a row of a population nobody has repaired. What was below floor is the COMPOSITION: +/// this function returned CLEAN while an enrolled expected-red assertion had ceased to assert +/// anything, so a true diagnostic sat beside a false conclusion drawn from it. The conjunct +/// therefore gates on GROWTH at identity grain — an identity producing no verdict that +/// `v2.workflow.floor_non_verdict` does not carry — which admits 142 → 0 in any order and +/// refuses 142 → 143, and refuses a swap that leaves the count untouched. +/// +/// THE NINTH IS `stale_non_verdict`, AND IT GATES FOR THE REASON THE EIGHTH DOES. A row whose +/// identity has been repaired is a LIVE EXEMPTION until it is deleted: the witness is fixed +/// today and, should it stop producing a verdict again, it is already rostered and the eighth +/// conjunct admits it. Repayment and deletion are therefore one act, which is what +/// `stale_route_gap` and the expected-red staleness join already require. This shipped as +/// report-only for one commit under the argument that refusing "punishes the fix"; it does not +/// — it requires the fix to be complete, and the diagnostic names every row to delete. fn required_floor_outcome_is_clean(outcome: &v1_compiler::cli_run::RequiredFloorOutcome) -> bool { outcome.failures.is_empty() + && outcome.non_verdict_unenrolled.is_empty() + && outcome.stale_non_verdict.is_empty() && outcome.stale_quarantine.is_empty() && outcome.interrupted_before_verdict.is_empty() && outcome.completed_over_cost_requirement.is_empty() diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 5a3b34b37cf..d823511f48d 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -43096,6 +43096,24 @@ pub struct RequiredFloorOutcome { /// either lets an enrollment cover a witness that has not actually run since the day it was /// enrolled. pub known_red_runtime_errored: Vec, + /// BLOCKING. An enrolled expected-red identity that produced no verdict and is not enrolled + /// in `v2.workflow.floor_non_verdict`. This is the conjunct that makes the composition + /// honest: the arms above are true observations, and returning CLEAN over them while an + /// enrolled assertion has stopped asserting is what was below floor. + pub non_verdict_unenrolled: Vec, + /// BLOCKING, and an earlier revision of this field had it reported-only on the argument that + /// refusing a repaid row "punishes the fix". That argument was wrong, and review 55361 found + /// why: a stale row is a LIVE EXEMPTION. The identity is repaired, the row stays, and if the + /// witness later stops producing a verdict again it is ALREADY ROSTERED — so the regression + /// this wall exists to refuse is admitted in silence. Repayment without deletion converts a + /// bounded debt row into a permanent licence, which is the absorbing fallback wearing the + /// word "diagnostic". + /// + /// Refusing does not punish a repair; it requires the repair to be COMPLETE. The diagnostic + /// names every row to delete, deletion is mechanical, and this is exactly the discipline + /// `stale_route_gap` and the expected-red staleness join already enforce. Consistency with + /// them turned out to be the correct answer rather than the lazy one. + pub stale_non_verdict: Vec, /// See `known_red_runtime_errored`. pub known_red_observation_unreadable: Vec, /// Host tool could not be resolved — infra undecided, not budget-refused. @@ -43775,6 +43793,61 @@ fn floor_cgroup_envelope(when: &str) { } } +/// The non-verdict admission, as a PURE FUNCTION OF TWO IDENTITY SETS. +/// +/// It is written this way so it can be exercised without a floor run, a fixture, or a witness +/// that actually throws — the thing that decides admission should be a pure function of two +/// sets, and the seed's discriminating red lives in `tests` below rather than only in the +/// modeled admission it mirrors. +/// +/// `added` is what the run observed and the roster does not carry: the growth this wall exists +/// to refuse. `repaid` is what the roster carries and the run did not observe: a debt paid, +/// REPORTED and never refused, because refusing it makes the merge that repairs the population +/// the merge that reds the floor. +/// +/// SETS, NEVER COUNTS. The case that decides the shape is a swap — one identity repaired while a +/// different identity begins producing no verdict — where `added` and `repaid` are both nonempty +/// and every count in the run is unchanged. A length comparison admits exactly that trade, which +/// is a repaired witness buying permission for an unrelated witness to lose its verdict. +#[derive(Debug, Default, PartialEq, Eq)] +pub struct NonVerdictAdmission { + pub added: Vec, + pub repaid: Vec, +} + +pub fn non_verdict_admission( + observed: &HashSet, + roster: &HashSet, +) -> NonVerdictAdmission { + let mut added: Vec = observed + .iter() + .filter(|q| !roster.contains(q.as_str())) + .cloned() + .collect(); + let mut repaid: Vec = roster + .iter() + .filter(|q| !observed.contains(q.as_str())) + .cloned() + .collect(); + added.sort(); + repaid.sort(); + NonVerdictAdmission { added, repaid } +} + +/// The admission itself: `added` AND `repaid` are both empty. Kept separate from the sets so a +/// caller reads the rule rather than reconstructing it. Both arms refuse for different reasons: a +/// row in `added` is an unenrolled non-verdict, and a row in `repaid` is a STALE ROW — the +/// identity answers again while the roster still names it, which is a live exemption if it later +/// regresses. Repaying and deleting the row are one act, so the repaired population is admitted +/// only once the roster row goes with it. +/// +/// CORRECTED 2026-08-24 (review 55577): this docstring and the body both described an asymmetry in +/// which `repaid` was admitted, while the executing gate already refused it via +/// `stale_non_verdict`. +pub fn non_verdict_admits(admission: &NonVerdictAdmission) -> bool { + admission.added.is_empty() && admission.repaid.is_empty() +} + pub fn run_required_floor( source_roots: &[String], commit: &str, @@ -44508,6 +44581,88 @@ pub fn run_required_floor( } } + // THE NON-VERDICT ROSTER. See `v2.workflow.floor_non_verdict` for the contract; the short + // form is that an enrolled expected-red identity which produces NO VERDICT — it throws, or + // answers a non-Bool — must be enrolled here, and an unenrolled one STOPS THE LINE. + // + // THE POLARITY IS THE CONSTRUCTION. An identity that is not enrolled BLOCKS, so an EMPTY + // roster is the STRICTEST state rather than the most permissive one, and a read failure + // here cannot flatter a run — it can only red one that would otherwise be green. The + // opposite polarity (a roster of things to gate ON) would have made losing the roster + // produce a greener answer, which is the absorbing-fallback shape rebuilt inside the + // mechanism written to close an absorbing fallback. + let non_verdict_roster: HashSet = { + let value = v1_interpreter::run_in_context( + &hermetic, + "v2.workflow.floor_non_verdict.floor_non_verdict_roster", + false, + ) + .map_err(|e| format!("floor_non_verdict_roster: {e}"))?; + let items = floor_decode_list(&hermetic, Some(&value)) + .map_err(|e| format!("floor_non_verdict_roster: {e}"))?; + let mut out = HashSet::new(); + for item in items { + match item { + v1_interpreter::Value::Str(s) => { + if !out.insert(s.to_string()) { + return Err(format!( + "floor_non_verdict_roster: duplicate enrolled identity: {s}" + )); + } + } + other => { + return Err(format!( + "floor_non_verdict_roster: expected a qualified name, got {}", + floor_value_shape(Some(other)) + )); + } + } + } + out + }; + eprintln!( + "[floor-non-verdict] roster carries {} enrolled identity(ies)", + non_verdict_roster.len() + ); + + // AND THIS ROSTER NEEDS NO SEPARATE FREEZE-DISJOINTNESS CHECK, which is worth saying because + // the wall below now covers three rosters and this is a fourth. The refusal immediately + // beneath enforces non-verdict SUBSET-OF expected-red, and expected-red is already + // cross-referenced against `frozen_path_deferrals` there — so an identity claiming both + // "produced no verdict while executing" and "never executes" is already refused, transitively + // and by construction. A fourth arm would be a second representation of a fact the subset + // relation already carries. + + // A NON-VERDICT ROW THAT IS NOT ALSO EXPECTED-RED CAN NEVER FIRE, so it is refused rather + // than left in the tree. Only an ENROLLED identity reaches the arms this roster classifies; + // an unenrolled one that throws goes through the ordinary failure path. So such a row is not + // a guard sitting quiet — the mechanism cannot produce the state it names — and DESIGN's + // reachability rule is explicit that unreachable is not empty: a check whose red cannot be + // authored is a decoration, worse than absent, because it is cited as coverage. + { + let mut orphans: Vec<&String> = non_verdict_roster + .iter() + .filter(|q| !expected_red_roster.contains(q.as_str())) + .collect(); + orphans.sort(); + if !orphans.is_empty() { + return Err(format!( + "REQUIRED-FLOOR REFUSAL cause=NonVerdictRowUnreachable count={} — these \ + identities are enrolled in v2.workflow.floor_non_verdict but NOT in \ + v2.workflow.floor_expected_red. Only an enrolled identity can reach the \ + non-verdict arms, so these rows can never classify anything: they read as debt \ + while being incapable of being debt. Enroll the identity as expected-red, or \ + delete the row: {}", + orphans.len(), + orphans + .iter() + .map(|q| q.as_str()) + .collect::>() + .join(", ") + )); + } + } + // CONTRADICTORY-INTERSECTION WALL: both executing-roster classifications and // `witness_deferral_freeze`'s // `frozen_path_deferrals` (`LegacyFrozenPathDeferral` — admitted as NEVER EXECUTED) make @@ -44644,6 +44799,8 @@ pub fn run_required_floor( interrupted_before_verdict: Vec::new(), completed_over_cost_requirement: Vec::new(), known_red_runtime_errored: Vec::new(), + non_verdict_unenrolled: Vec::new(), + stale_non_verdict: Vec::new(), known_red_observation_unreadable: Vec::new(), host_tool_unresolved: Vec::new(), route_gap: Vec::new(), @@ -44731,6 +44888,10 @@ pub fn run_required_floor( // "is this enrollment still real", which is exactly how a skip list rots. let mut route_gap_seen: HashSet = HashSet::new(); let mut route_gap_held: usize = 0; + // IDENTITY GRAIN, NEVER COUNTS. The whole point of the roster is the case where one + // identity is repaired while a different one begins throwing and the COUNT DOES NOT MOVE. + let mut non_verdict_seen: HashSet = HashSet::new(); + let mut non_verdict_detail: BTreeMap = BTreeMap::new(); let mut expected_red_seen: HashSet = HashSet::new(); let mut claim_rss_kb_max: u64 = 0; let mut claim_rss_kb_max_row = String::new(); @@ -45118,6 +45279,8 @@ pub fn run_required_floor( format!("{other:?}") } }; + non_verdict_seen.insert(claim.qualified.clone()); + non_verdict_detail.insert(claim.qualified.clone(), detail.clone()); outcome.known_red_runtime_errored.push(format!( "{} is enrolled as expected-red but RUNTIME-ERRORED, not failed: {}. \ Enrollment asserts an expected verdict; a claim that threw \ @@ -45130,6 +45293,11 @@ pub fn run_required_floor( } ExpectedRedArm::ObservationUnreadable => { known_red_observation_unreadable_count += 1; + non_verdict_seen.insert(claim.qualified.clone()); + non_verdict_detail.insert( + claim.qualified.clone(), + format!("returned {result:?}, which is not a Bool"), + ); outcome.known_red_observation_unreadable.push(format!( "{} is enrolled as expected-red but returned something that is NOT A \ VERDICT ({:?}), so it is neither the enrolled failure nor a \ @@ -45409,6 +45577,48 @@ pub fn run_required_floor( // row — and separating them would ask the reader to learn two names for it. An identity // that executed and did not gap, and an identity that did not execute at all (renamed, // deleted, or declined), are distinguished in the message rather than in the mechanism. + // ONE DECISION POINT, TAKEN AFTER THE FOLD, over the two identity sets. The arms above only + // RECORD what they observed; nothing there decides admission, so there is no second place + // where the rule could drift from the one written in + // `v2.workflow.floor_non_verdict_admission`. + { + let admission = non_verdict_admission(&non_verdict_seen, &non_verdict_roster); + for identity in &admission.added { + let detail = non_verdict_detail + .get(identity) + .map(|d| d.as_str()) + .unwrap_or("no verdict"); + outcome.non_verdict_unenrolled.push(format!( + "{identity} is enrolled as expected-red and produced NO VERDICT ({detail}), and \ + it is NOT enrolled in v2.workflow.floor_non_verdict. Enrollment as expected-red \ + admits a known SEMANTIC VERDICT -- this witness reaches its subject and answers \ + false -- and is not permission for the subject to stop evaluating. Repair the \ + witness or its subject. Enrolling the identity records the debt; it does not \ + make the missing verdict acceptable, and the roster is frozen against growth." + )); + } + // REFUSED, NOT MERELY REPORTED. A repaid row left standing is a live exemption: the + // identity is fixed today, and if it regresses tomorrow it is already rostered and the + // wall admits it. So repayment and roster deletion are one act. + for identity in &admission.repaid { + let ran = receipted.contains(identity.as_str()); + outcome.stale_non_verdict.push(if ran { + format!( + "{identity} is enrolled in v2.workflow.floor_non_verdict but PRODUCED A \ + VERDICT this run -- it reaches its subject again. Delete the row; the debt \ + is repaid." + ) + } else { + format!( + "{identity} is enrolled in v2.workflow.floor_non_verdict but did not \ + execute at all, so no non-verdict could be observed. It was renamed, \ + deleted, or declined. Delete the row or restore the identity to the routed \ + roster." + ) + }); + } + } + { let mut stale: Vec<&String> = route_gap_roster .iter() diff --git a/src/v1/stage0/tests/floor_non_verdict_admission_seed_path.rs b/src/v1/stage0/tests/floor_non_verdict_admission_seed_path.rs new file mode 100644 index 00000000000..29656644d0b --- /dev/null +++ b/src/v1/stage0/tests/floor_non_verdict_admission_seed_path.rs @@ -0,0 +1,102 @@ +//! THE DISCRIMINATING RED ON THE SEED PATH, not on the model it mirrors. +//! +//! `v2.workflow.floor_non_verdict_admission` carries the modeled admission and its own witnesses +//! establish that the RULE discriminates. Those witnesses say nothing about the Rust that +//! actually stops the line: the seed recomputes the same two sets, and a mirror can be wrong in +//! ways its carrier cannot see. This file exercises the seed's own decision function directly, +//! with synthetic identity sets, so the wall has a red that goes through the code that gates. +//! +//! WHAT THIS DOES NOT ESTABLISH, stated so it is not read as more than it is: it does not prove +//! the wiring from a real thrown witness into `observed`. That path remains unexercised, and it +//! is the honest residual gap — narrower than "the seed wall is untested", and not zero. + +use std::collections::HashSet; +use v1_compiler::cli_run::{non_verdict_admission, non_verdict_admits}; + +fn ids(xs: &[&str]) -> HashSet { + xs.iter().map(|s| s.to_string()).collect() +} + +fn roster() -> HashSet { + ids(&["m.a", "m.b", "m.c"]) +} + +#[test] +fn unchanged_population_is_admitted() { + let a = non_verdict_admission(&ids(&["m.a", "m.b", "m.c"]), &roster()); + assert!(a.added.is_empty(), "added: {:?}", a.added); + assert!(a.repaid.is_empty(), "repaid: {:?}", a.repaid); + assert!(non_verdict_admits(&a)); +} + +/// A REPAID IDENTITY WHOSE ROW STILL STANDS IS A STALE ROW, AND STALE ROWS REFUSE. An earlier +/// revision of this test asserted the opposite, reasoning that refusing repayment would red the +/// merge that repairs the population (gunbc#9020 repays 99 in one landing). That reasoning was +/// right about the goal and wrong about the subject: what refuses is not the repayment, it is the +/// roster row left behind asserting a debt that no longer exists. The executing gate already +/// refuses it — `stale_non_verdict` is a conjunct of `required_floor_outcome_is_clean` — so +/// admitting it here made this mirror disagree with its own consumer (review 55577). +#[test] +fn repayment_that_leaves_the_row_behind_refuses() { + let a = non_verdict_admission(&ids(&["m.b"]), &roster()); + assert!(a.added.is_empty(), "added: {:?}", a.added); + assert_eq!(a.repaid, vec!["m.a".to_string(), "m.c".to_string()]); + assert!(!non_verdict_admits(&a)); +} + +/// THE CONTROL THAT KEEPS THE ROW ABOVE FROM READING AS A PENALTY ON REPAYMENT. Repaying and +/// deleting the row are one act: delete the two repaid identities from the roster in the same +/// change and both collections are empty, so the same function that refuses the stale form admits +/// this one. Without this pair the suite would not discriminate "stale rows refuse" from +/// "repayment refuses", which are opposite rules. +#[test] +fn repayment_with_the_row_deleted_is_admitted() { + let a = non_verdict_admission(&ids(&["m.b"]), &ids(&["m.b"])); + assert!(a.added.is_empty(), "added: {:?}", a.added); + assert!(a.repaid.is_empty(), "repaid: {:?}", a.repaid); + assert!(non_verdict_admits(&a)); +} + +#[test] +fn growth_stops_the_line() { + let a = non_verdict_admission(&ids(&["m.a", "m.b", "m.c", "m.d"]), &roster()); + assert_eq!(a.added, vec!["m.d".to_string()]); + assert!(!non_verdict_admits(&a)); +} + +/// THE CASE THE WHOLE MECHANISM EXISTS FOR, and the one a count-based implementation passes in +/// silence: `m.c` was repaired and `m.d` began producing no verdict in the same change. The +/// population is still three identities, so every count in the run is identical to the unchanged +/// case above — and a repaired witness has bought permission for an unrelated witness to lose its +/// verdict. The length equality is asserted here so the refusal cannot be read as an artifact of +/// the two sets being different sizes. +#[test] +fn a_swap_that_leaves_the_count_unmoved_still_stops_the_line() { + let observed = ids(&["m.a", "m.b", "m.d"]); + let roster = roster(); + assert_eq!( + observed.len(), + roster.len(), + "the discriminating property of this case is that the counts agree" + ); + let a = non_verdict_admission(&observed, &roster); + assert_eq!(a.added, vec!["m.d".to_string()]); + assert_eq!(a.repaid, vec!["m.c".to_string()]); + assert!(!non_verdict_admits(&a)); +} + +/// AN EMPTY ROSTER IS THE STRICTEST STATE, NOT THE MOST PERMISSIVE. This is the polarity that +/// makes a roster read failure unable to flatter a run: with nothing enrolled, every observed +/// non-verdict identity is growth and the line stops. The opposite polarity would rebuild the +/// absorbing-fallback shape inside the mechanism written to close one. +#[test] +fn an_empty_roster_refuses_every_observed_non_verdict() { + let a = non_verdict_admission(&ids(&["m.a"]), &HashSet::new()); + assert_eq!(a.added, vec!["m.a".to_string()]); + assert!(!non_verdict_admits(&a)); + + // ...and an empty observation over an empty roster is clean, so the strictness above is a + // property of what was observed rather than a function stuck at refuse. + let b = non_verdict_admission(&HashSet::new(), &HashSet::new()); + assert!(non_verdict_admits(&b)); +} diff --git a/src/v2/test/claim/floor_non_verdict_admission_test.dag b/src/v2/test/claim/floor_non_verdict_admission_test.dag new file mode 100644 index 00000000000..b2a7f471f87 --- /dev/null +++ b/src/v2/test/claim/floor_non_verdict_admission_test.dag @@ -0,0 +1,70 @@ +module v2.test.claim.floor_non_verdict_admission_test + +import v2.std.algebra { Cons, Empty, length } +import v2.std.collection { List } +import v2.std.text { String } +import v2.std.logic { Bool } +import v2.workflow.floor_non_verdict_admission { + non_verdict_added, non_verdict_repaid, non_verdict_admits, +} + +data live_tree_disposition: v2.std.live_tree.LiveTreeDisposition = v2.std.live_tree.SubstrateInputsOnly + +data roster_fixture: List = Cons { head: "m.a", tail: Cons { head: "m.b", tail: Cons { head: "m.c", tail: Empty {} } } } + +// UNCHANGED: the population is exactly the roster. +data observed_unchanged: List = Cons { head: "m.a", tail: Cons { head: "m.b", tail: Cons { head: "m.c", tail: Empty {} } } } + +// REPAID: two identities now answer while their roster rows still stand. Must REFUSE -- not +// because repayment is penalised, but because a row the run no longer observes is a stale row +// asserting a debt that no longer exists, and the executing gate refuses exactly that +// (stale_non_verdict is a conjunct of required_floor_outcome_is_clean). Repaying and deleting the +// row are one act; the fixture below drives the deleted-row form and is admitted. +data observed_repaid: List = Cons { head: "m.b", tail: Empty {} } + +// GROWN: a fourth identity begins producing no verdict. Must refuse. +data observed_grown: List = Cons { head: "m.a", tail: Cons { head: "m.b", tail: Cons { head: "m.c", tail: Cons { head: "m.d", tail: Empty {} } } } } + +// THE DISCRIMINATING CASE, AND THE REASON THE ADMISSION IS NOT A COUNT. `m.c` was repaired and +// `m.d` began throwing in the same change. The population is STILL THREE IDENTITIES, so every +// count in the run is identical to the unchanged case -- and a repaired witness has bought +// permission for an unrelated witness to lose its verdict. This is the mutation a count-based +// implementation passes silently. +data observed_swapped: List = Cons { head: "m.a", tail: Cons { head: "m.b", tail: Cons { head: "m.d", tail: Empty {} } } } + +test fn unchanged_population_is_admitted() -> Bool { + non_verdict_admits(observed: observed_unchanged, roster: roster_fixture) +} + +test fn repayment_that_leaves_the_row_behind_refuses_and_is_reported_per_identity() -> Bool { + !non_verdict_admits(observed: observed_repaid, roster: roster_fixture) + && length(xs: non_verdict_repaid(observed: observed_repaid, roster: roster_fixture)) == 2 + && length(xs: non_verdict_added(observed: observed_repaid, roster: roster_fixture)) == 0 +} + +// AND THE REPAIR ITSELF IS ADMITTED, which is the control that keeps the row above from reading as +// a penalty on repayment. Deleting the two repaid identities from the roster in the same change +// leaves both collections empty, and the same function that refuses the stale form admits this +// one. Without this control the pair would not discriminate between "stale rows refuse" and +// "repayment refuses", which are opposite rules. +test fn repayment_with_the_row_deleted_is_admitted() -> Bool { + non_verdict_admits(observed: observed_repaid, roster: observed_repaid) + && length(xs: non_verdict_repaid(observed: observed_repaid, roster: observed_repaid)) == 0 + && length(xs: non_verdict_added(observed: observed_repaid, roster: observed_repaid)) == 0 +} + +test fn growth_refuses() -> Bool { + !non_verdict_admits(observed: observed_grown, roster: roster_fixture) + && length(xs: non_verdict_added(observed: observed_grown, roster: roster_fixture)) == 1 +} + +// THE EVIDENCE THAT THE IDENTITY-GRAIN DECISION WAS REAL, not the plumbing test. The swapped +// population has the SAME LENGTH as the roster, so this assertion is the one a count-based +// admission fails -- and the length equality is asserted here beside the refusal, so the +// discrimination cannot be read as an artifact of the sizes differing. +test fn a_swap_that_leaves_the_count_unmoved_still_refuses() -> Bool { + length(xs: observed_swapped) == length(xs: roster_fixture) + && !non_verdict_admits(observed: observed_swapped, roster: roster_fixture) + && length(xs: non_verdict_added(observed: observed_swapped, roster: roster_fixture)) == 1 + && length(xs: non_verdict_repaid(observed: observed_swapped, roster: roster_fixture)) == 1 +} diff --git a/src/v2/workflow/floor_non_verdict.dag b/src/v2/workflow/floor_non_verdict.dag new file mode 100644 index 00000000000..2fc0ec13e76 --- /dev/null +++ b/src/v2/workflow/floor_non_verdict.dag @@ -0,0 +1,565 @@ +module v2.workflow.floor_non_verdict + +import v2.std.algebra { Cons, Empty, list_flat_map } +import v2.std.collection { List } +import v2.std.text { String } + +// THE NON-VERDICT ROSTER: identities enrolled as expected-red that the required floor EXECUTES +// and that produce NO BOOLEAN VERDICT -- they throw, or they answer with something that is not a +// Bool -- enrolled by exact qualified name. +// +// WHY IT EXISTS, and the fact it exists to make gating rather than merely visible. `cli_run` +// `run_required_floor` routes such a claim to `known_red_runtime_errored` or +// `known_red_observation_unreadable`, and those arms are HONEST: they say correctly that this +// enrolled claim produced no verdict. The defect was never in the arm. It was in the +// COMPOSITION -- `claim_executor` `required_floor_outcome_is_clean` consulted neither, so the +// floor returned CLEAN while an enrolled expected-red assertion had ceased to assert anything. +// A diagnostic can describe the evidence truthfully while the gate draws a false conclusion +// from it, and that is what happened here on every run for a day. +// +// THE RUNG, PER SEAM, because the governing rung is the minimum across them and stating only +// the strongest seam is the inflation DESIGN section 4b(1) forbids: routing a thrown claim into +// its arm is MITIGATABLE; printing the count is MITIGATABLE; printing `failed=0` without +// distinguishing verdict incompleteness is a MISLEADING PROJECTION; and returning CLEAN while +// an enrolled claim produced no verdict is BELOW FLOOR. Below floor is not a rung -- it is +// outside the ladder and forbidden outright -- which is why this roster gates rather than +// waiting for the population to be repaid first. +// +// WHAT ENROLMENT ADMITS, AND WHAT IT CANNOT. Enrolment in `floor_expected_red` is an admission +// about a known SEMANTIC VERDICT: this witness reaches its subject and answers false. It is not +// permission for the subject to stop evaluating. Without this roster the expected-red arm +// absorbs an arbitrary regression INSIDE the enrolled population -- yesterday the witness +// executed and returned false, today it throws before reaching its assertion, no verdict +// exists, and the floor stays clean. (Strictly inside it: an UNENROLLED witness that throws +// goes through the ordinary failure path and already gates. The absorption was never repo-wide, +// and saying otherwise would overstate the defect this closes.) +// +// WHAT THIS WALL CONFINES, AND WHAT IT DOES NOT. Stated first because the short name for this +// module -- a growth freeze -- claims more than the mechanism delivers, and a reader who takes +// the name literally will conclude that growth is REFUSED. It is not, in one direction. +// +// CONFINED, by execution, every run: the OBSERVED population must equal the ROSTER exactly. An +// observed identity the roster does not carry refuses (unrostered debt); a rostered identity the +// run did not observe refuses (stale exemption). Together those pin O = R. +// +// NOT CONFINED: the roster itself. Nothing here compares the roster authored at HEAD against the +// roster admitted at the MERGE BASE, so an author whose change makes a NEW identity stop +// producing a verdict may add its row IN THE SAME CHANGE. Observed then equals roster, both +// arms pass, and the regression is admitted -- LEGALISED BY THE ROSTER THAT EXISTS TO BOUND IT. +// The row becomes the permission, which is exactly the defect review 55361 identified for stale +// rows, arriving through authorship rather than through survival. +// +// THIS IS A CONSEQUENCE OF THE SINGLE-RUN DESIGN AND NOT AN OVERSIGHT IN IT. The admission was +// specified as `added = head_observed - base_observed`, which needs a SECOND floor run over the +// base. Substituting the roster for base-observation is what makes the wall implementable in one +// run -- and that substitution is sound exactly to the degree the roster cannot be grown freely. +// So `R subset-of B` is the condition that makes the simplification safe, not an extra nicety on +// top of it, and its absence is the honest cost of the cheap design. +// +// RUNG ON THAT AXIS: MITIGATABLE. Roster growth is confined by review diligence alone, which is +// strictly weaker than execution, and this paragraph is the declaration rather than a reader's +// inference. +// +// NEXT-RUNG TRIGGER: the floor establishes `H subset-of B` -- the roster in the COMPOSED RESULT is a +// subset of the roster at that result's CURRENT TARGET-BASE PARENT. NOT the merge base, and the +// difference is a real admission rather than a spelling: with M = {a} at the merge base, main +// repairing `a` and deleting its row (B = {}), and a stale branch reintroducing it (H = O = {a}), +// a subset-of-M rule PASSES and readmits an exemption main already retired. The mirror is a false +// red on a row main legitimately added after the fork. The cut therefore needs the composed result +// and its base parent, which a branch-head-only run cannot supply. + +// THE ADMISSION AS IMPLEMENTED: the ADDED set is empty. +// +// added = head_non_verdict_identities - roster +// repaid = roster - head_non_verdict_identities +// admit <=> added is empty +// +// So 142 -> 43 -> 42 -> 0 is admitted and 142 -> 143 refuses. So does one old identity repaired +// while a different identity begins throwing, with the count still reading 142 -- and THAT is +// why both sides are compared as IDENTITY SETS and never as counts. A repaired witness must not +// buy permission for an unrelated witness to lose its verdict, and a count-based implementation +// admits exactly that trade in silence. The corpus has already paid for this lesson once in the +// other direction: the false regression that produced this module was a comparison whose +// `planned` counts matched on both sides while the trees did not. +// +// REPAYMENT AND ROSTER DELETION ARE ONE ACT, and an earlier revision of this header said the +// opposite. It argued that refusing a stale row "punishes the fix", because gunbc#9020 repairs +// 99 of these in one landing and would go red for it. That argument is wrong, and review 55361 +// found why: A STALE ROW IS A LIVE EXEMPTION. The identity is repaired, the row stays, and if +// that witness later stops producing a verdict again it is ALREADY ROSTERED -- so the exact +// regression this wall exists to refuse is admitted in silence. Repayment without deletion turns +// a bounded debt row into a permanent licence, which is the absorbing fallback wearing the word +// "diagnostic". +// +// Refusing does not punish a repair; it requires the repair to be COMPLETE. The run names every +// row to delete, the deletion is mechanical, and this is the discipline `floor_route_gap` and +// the expected-red staleness join already enforce. The asymmetry was the error and consistency +// with them is the repair -- which is worth recording, because the asymmetry had an argument +// behind it and was endorsed before a reviewer found the hole in it. +// +// EMPTY IS THE INTENDED TERMINAL STATE. When every enrolled identity reaches its subject and +// answers, this module deletes, and the two collections become ordinary conjuncts over nothing. +// +// THE POPULATION, MEASURED RATHER THAN ESTIMATED (floor run 32694337921, sha 1239cace120): 142 +// identities, all of them `known_red_runtime_errored` -- `known_red_observation_unreadable` was +// 0 on that run, so every member of this population threw rather than answering a non-Bool. The +// causes: +// 119 no declaration named X in this execution's loaded index +// 13 type error +// 9 undefined variable +// 1 call contract mismatch +// +// THE DOMINANT CAUSE IS AN AUTHORED DEFECT, NOT A FLOOR SCOPE DEFECT, and it was checked rather +// than assumed: four of the unresolved names were looked up and every one IS declared in the +// corpus, while the witness referencing it declares no import that would bring it into the run's +// loaded index. The refusal is correct and the witness is unimportable, so the repair is a per +// witness import and never a widening of the floor's scope. +fn floor_non_verdict_chunk_00() -> List { + Cons { + head: "test.claim.accelerator_demo_execution_witness.accelerator_demo_execution_lane_witnesses", + tail: Cons { + head: "test.claim.accelerator_demo_model_witness.accelerator_demo_modeling_lane_witnesses", + tail: Cons { + head: "test.claim.ci_deploy_target_host_witness.witness_deploy_job_not_on_ubicloud_runner", + tail: Cons { + head: "test.claim.ci_deploy_target_host_witness.witness_deploy_stage_pins_srv1_runner_label", + tail: Cons { + head: "test.claim.config_record_emit_witness.witness_manifest_knobs_space_separated", + tail: Cons { + head: "test.claim.config_record_emit_witness.witness_same_fields_differ_across_knobs", + tail: Cons { + head: "test.claim.design_argument_witness.cycle_is_detected", + tail: Cons { + head: "test.claim.design_argument_witness.design_full_argument_axiom_set_is_closed", + tail: Cons { + head: "test.claim.design_argument_witness.design_full_argument_form_is_valid", + tail: Cons { + head: "test.claim.design_argument_witness.design_full_argument_has_no_orphan", + tail: Cons { + head: "test.claim.design_argument_witness.design_full_argument_is_acyclic", + tail: Cons { + head: "test.claim.design_argument_witness.design_s1_argument_form_is_valid", + tail: Cons { + head: "test.claim.design_argument_witness.design_s1_argument_is_non_vacuous", + tail: Cons { + head: "test.claim.design_argument_witness.orphan_is_detected", + tail: Cons { + head: "test.claim.design_argument_witness.smuggled_axiom_is_detected", + tail: Cons { + head: "test.claim.ebay_listing_witness.witness_default_listing_policy_targets_us_marketplace", + tail: Cons { + head: "test.claim.emit_host_gate_witness.w_byte_count_is_five", + tail: Cons { + head: "test.claim.emit_host_gate_witness.w_go_fixture_nonempty", + tail: Cons { + head: "test.claim.emit_host_gate_witness.w_python_fixture_nonempty", + tail: Cons { + head: "test.claim.emit_host_gate_witness.w_rust_fixture_nonempty", + tail: Cons { + head: "test.claim.emit_host_gate_witness.w_ts_byte_count_is_four", + tail: Cons { + head: "test.claim.emit_host_gate_witness.w_ts_fixture_nonempty", + tail: Cons { + head: "test.claim.fleet_convergence_verdict_witness.knob_receipts_alone_cannot_converge_the_fleet", + tail: Cons { + head: "test.claim.fleet_convergence_verdict_witness.live_fleet_is_not_converged_and_unobserved_cells_are_counted", + tail: Cons { + head: "test.claim.fleet_receipt_collector_witness.witness_partial_collection_never_yields_fleet_converged", + tail: Cons { + head: "test.claim.go_module_versioning_witness.w_go_manifest_file", + tail: Cons { + head: "test.claim.hand_lens_host_bridge_scaffold_watchdog.hand_lens_host_bridge_scaffold_roster_tracks_5364_dissolution", + tail: Cons { + head: "test.claim.hetzner_cost_quote_witness.hetzner_cax41_cost_class_is_per_second_billed", + tail: Cons { + head: "test.claim.hetzner_cost_quote_witness.hetzner_cax41_currency_is_eur", + tail: Cons { + head: "test.claim.hetzner_cost_quote_witness.hetzner_cax41_unit_price_matches_catalog", + tail: Cons { + head: "test.claim.host_phase_status.witness_enrolled_spark_cells_are_all_unobserved", + tail: Cons { + head: "test.claim.host_phase_status.witness_enrolled_sparks_carry_exactly_the_shared_obligations", + tail: Cons { + head: "test.claim.host_phase_status.witness_every_covered_cell_today_is_the_authored_one", + tail: Cons { + head: "test.claim.host_phase_status.witness_fleet_matrix_has_no_duplicated_cells", + tail: Cons { + head: "test.claim.host_phase_status.witness_live_observation_frontier_is_one_cell", + tail: Cons { + head: "test.claim.host_phase_status.witness_matrix_hosts_are_exactly_the_enrolled_roster", + tail: Cons { + head: "test.claim.host_phase_status.witness_matrix_is_exact_join_over_participation_programs", + tail: Cons { + head: "test.claim.host_phase_status.witness_program_scoping_preserves_the_runner_fleet_matrix", + tail: Cons { + head: "test.claim.host_phase_status.witness_reconcile_covers_upsert_teardown_and_noop", + tail: Cons { + head: "test.claim.host_phase_status.witness_remaining_work_counts_every_unfinished_cell", + tail: Empty {} + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } +} + +fn floor_non_verdict_chunk_01() -> List { + Cons { + head: "test.claim.host_phase_status.witness_runner_only_obligations_exist_on_runner_hosts", + tail: Cons { + head: "test.claim.host_phase_status.witness_unmodeled_cells_track_spine_gaps", + tail: Cons { + head: "test.claim.host_reach_identity_probe_witness.committed_probe_receipts_feed_producers_and_grow_coverage", + tail: Cons { + head: "test.claim.host_reach_identity_probe_witness.observe_host_phase_routes_by_label_and_stays_fail_closed", + tail: Cons { + head: "test.claim.host_standup_assimilation_deduction.no_lease_past_budget_is_drifted_not_fabricated_success", + tail: Cons { + head: "test.claim.host_standup_assimilation_deduction.post_install_lease_row_deduces_converged_noop", + tail: Cons { + head: "test.claim.host_standup_assimilation_deduction.pre_install_within_budget_is_absent_not_converged", + tail: Cons { + head: "test.claim.host_standup_assimilation_deduction.unreadable_lease_is_unknown_refused_not_pending", + tail: Cons { + head: "test.claim.host_standup_assimilation_deduction.upsert_pending_applies_assert_pending_plan", + tail: Cons { + head: "test.claim.host_standup_spine.post_install_dhcp_subsumption_reduces_gap_count_by_one", + tail: Cons { + head: "test.claim.realization_reconcile_witness.witness_different_keysource_does_not_collapse", + tail: Cons { + head: "test.claim.realization_reconcile_witness.witness_post_always_never_collapses", + tail: Cons { + head: "test.claim.realization_reconcile_witness.witness_same_keysource_collapses_to_share", + tail: Cons { + head: "test.claim.samsung_dram_module.four_rank_by_four_is_realizable_on_ddr4", + tail: Cons { + head: "test.claim.samsung_dram_module.generation_mismatch_fails_closed", + tail: Cons { + head: "test.claim.samsung_dram_module.same_capacity_at_one_rank_by_eight_is_not_realizable", + tail: Cons { + head: "test.claim.srv3_subsumption.comment_only_drift_is_one_change_not_remove_add", + tail: Cons { + head: "test.claim.srv3_subsumption.reconcile_would_teardown_only_if_ownership_claimed_it", + tail: Cons { + head: "test.claim.srv3_subsumption.srv3_and_srv4_disagree_on_convergence", + tail: Cons { + head: "test.claim.srv3_subsumption.srv3_reconcile_adds_exactly_the_missing_fleet_key", + tail: Cons { + head: "test.claim.srv3_subsumption.srv3_reconcile_refuses_both_unowned_keys_never_teardown", + tail: Cons { + head: "test.claim.srv3_subsumption.srv4_reconcile_is_converged_empty_plan", + tail: Cons { + head: "v2.test.claim.compiler_materialization_witness.compile_stage_carrier_inhabits_realization", + tail: Cons { + head: "v2.test.claim.compiler_materialization_witness.parse_table_carrier_inhabits_realization", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_coproduct_exhaustiveness_anchor_holds", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_coproduct_exhaustiveness_covers_every_coproduct", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_coproduct_exhaustiveness_is_diagnostic", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_coproduct_exhaustiveness_roster_covers_testclaim", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_cross_representation_equality_anchor_holds", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_cross_representation_equality_covers_bool", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_cross_representation_equality_covers_optional_null", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_cross_representation_equality_is_equals", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_lbe_conj_snapshot_passes", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_lbe_dag_surface_language_identity", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_lbe_disj_snapshot_passes", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_lbe_schedules_three_generators", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_lbe_transform_snapshot_passes", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_refinement_claim_emits", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_refinement_preserves_nonempty_list_base", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_refinement_scheduler_emits_one_generator", + tail: Empty {} + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } +} + +fn floor_non_verdict_chunk_02() -> List { + Cons { + head: "v2.test.claim.generated_conformance_floor.generated_refinement_subject_anchor_holds", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_witness_validity_constraint_satisfaction_emits", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_witness_validity_evidence_node_mismatch_emits", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_witness_validity_property_symbol_mismatch_emits", + tail: Cons { + head: "v2.test.claim.generated_conformance_floor.generated_witness_validity_rule_not_realized_emits", + tail: Cons { + head: "v2.test.claim.gha_workflow_yaml_fold_structural.gha_fold_structural_tier_holds", + tail: Cons { + head: "v2.test.claim.source_root_tagging.source_root_tag_carried_and_folded_to_grounded_set", + tail: Cons { + head: "v2.test.claim.staging.cached_stage_hit_skips_stage", + tail: Cons { + head: "v2.test.claim.staging.cached_stage_miss_runs_stage", + tail: Cons { + head: "v2.test.emit.produced_decl_support_preserved.produced_decl_support_survives_augmentation", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.corpus.cargo_build_policy_leak.corpus_cargo_build_defused_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.corpus.cargo_clippy_dead_param.corpus_cargo_clippy_dead_param_defused_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.corpus.cargo_doc_dead_param.corpus_cargo_doc_dead_param_defused_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.corpus.cargo_doc_policy_leak.corpus_cargo_doc_defused_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.corpus.cargo_fmt_dead_param.corpus_cargo_fmt_dead_param_defused_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.corpus.cargo_fmt_policy_leak.corpus_cargo_fmt_defused_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.corpus.cargo_run_dead_param.corpus_cargo_run_dead_param_defused_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.corpus.gcp_login_dead_param.corpus_gcp_login_dead_param_defused_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.corpus.gcp_oauth_fusion_fork.corpus_gcp_oauth_defused_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.corpus.gist_create_policy_leak.corpus_gist_create_defused_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.corpus.git_policy_leak.corpus_git_policy_leak_defused_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.corpus.runtime_local_embedded_policy.corpus_runtime_local_embedded_policy_defused_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.coverage_domain_equivalence_test.extdeps_shape_transport_policy_coverage_domain_equivalence_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.clean_gist_create.clean_gist_create_is_green_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.clean_git_diff.clean_git_diff_is_green_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.dead_param_cargo_build.dead_param_cargo_build_is_red_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.dead_param_cargo_clippy.dead_param_cargo_clippy_is_red_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.dead_param_gcp_login.dead_param_gcp_login_is_red_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.embedded_policy_literal_local.embedded_policy_literal_local_is_red_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.module_path_rename.module_path_rename_resolves_by_qn_not_filepath_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.module_path_rename.module_path_rename_unknown_qn_does_not_resolve_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.module_source_nickname_literal_coverage_domain_green.module_source_nickname_literal_coverage_domain_is_green_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.module_source_nickname_literal_green.module_source_nickname_literal_exempt_literals_is_green_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.module_source_nickname_literal_local_red.module_source_nickname_literal_local_red_is_red_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.policy_leak_cargo_build.policy_leak_cargo_build_is_red_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.policy_leak_cargo_doc.policy_leak_cargo_doc_is_red_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.policy_leak_cargo_fmt.policy_leak_cargo_fmt_is_red_holds", + tail: Cons { + head: "v2.test.extdeps_shape_transport_policy.lens_unit.transport_fusion_gcp_oauth.transport_fusion_gcp_oauth_is_red_holds", + tail: Cons { + head: "v2.test.extdeps.spice_rc_passive_deck_claims.spice_rc_passive_deck_authority_holds", + tail: Cons { + head: "v2.test.fact_cardinality.lens_unit.synthetic_fork_red.synthetic_fork_red_holds", + tail: Empty {} + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } +} + +fn floor_non_verdict_chunk_03() -> List { + Cons { + head: "v2.test.intent_linearity.lens_unit.runtime_axis.flat_loop_cost_not_lowerable", + tail: Cons { + head: "v2.test.intent_linearity.lens_unit.runtime_axis.flat_loop_is_linear", + tail: Cons { + head: "v2.test.intent_linearity.lens_unit.runtime_axis.flat_loop_not_runtime_candidate", + tail: Cons { + head: "v2.test.intent_linearity.lens_unit.runtime_axis.nested_loop_cost_is_lowerable", + tail: Cons { + head: "v2.test.intent_linearity.lens_unit.runtime_axis.nested_loop_is_runtime_candidate", + tail: Cons { + head: "v2.test.intent_linearity.lens_unit.runtime_axis.nested_loop_not_changetime_redundant", + tail: Cons { + head: "v2.test.lens_mutation_adequacy.mutation_adequacy_test.adequate_when_every_mutation_has_a_discriminating_witness", + tail: Cons { + head: "v2.test.lens_mutation_adequacy.mutation_adequacy_test.surviving_mutation_is_inadequate", + tail: Cons { + head: "v2.test.lens_vacuity.vacuity_test.vacuity_advisory_census_partitions_falsification_suite", + tail: Cons { + head: "v2.test.lens_vacuity.vacuity_test.vacuity_falsification_cases_each_match_expected_evidence", + tail: Cons { + head: "v2.test.lens_vacuity.vacuity_test.vacuity_falsification_suite_nonempty", + tail: Cons { + head: "v2.test.lens_vacuity.vacuity_test.vacuity_rung5_emit_vs_eval_classifies_proven_independent", + tail: Cons { + head: "v2.test.lens_vacuity.vacuity_test.vacuity_unified_node_corpus_matches_transport_classifier", + tail: Cons { + head: "v2.test.manual.bootstrap_footprint_anchor.bootstrap_footprint_bad_content_hash_violates", + tail: Cons { + head: "v2.test.manual.bootstrap_footprint_anchor.bootstrap_footprint_bad_runtime_same_identity_violates", + tail: Cons { + head: "v2.test.manual.bootstrap_footprint_anchor.bootstrap_footprint_canonical_holds", + tail: Cons { + head: "v2.test.manual.bootstrap_footprint_anchor.bootstrap_footprint_non_canonical_violates", + tail: Cons { + head: "v2.test.manual.medium_node_instantiation.medium_node_carried_is_expected", + tail: Cons { + head: "v2.test.manual.medium_node_instantiation.medium_node_fidelity_is_lossless", + tail: Cons { + head: "v2.test.manual.medium_node_instantiation.medium_node_lossy_tag_not_lossless", + tail: Cons { + head: "v2.test.manual.medium_source_text_instantiation.witness_source_field_is_medium", + tail: Cons { + head: "v2.test.manual.value_null_split_witness.optional_null_straddle_rostered_until_phase_e", + tail: Empty {} + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } + } +} + +fn floor_non_verdict_chunks() -> List> { + Cons { head: floor_non_verdict_chunk_00(), tail: Cons { head: floor_non_verdict_chunk_01(), tail: Cons { head: floor_non_verdict_chunk_02(), tail: Cons { head: floor_non_verdict_chunk_03(), tail: Empty {} } } } } +} + +fn floor_non_verdict_roster() -> List { + list_flat_map(xs: floor_non_verdict_chunks(), f: fn(chunk) { chunk }) +} diff --git a/src/v2/workflow/floor_non_verdict_admission.dag b/src/v2/workflow/floor_non_verdict_admission.dag new file mode 100644 index 00000000000..84db436fbdb --- /dev/null +++ b/src/v2/workflow/floor_non_verdict_admission.dag @@ -0,0 +1,74 @@ +module v2.workflow.floor_non_verdict_admission + +import v2.std.algebra { Cons, Empty, fold_list, length } +import v2.std.collection { List } +import v2.std.text { String } +import v2.std.logic { Bool } + +// THE ADMISSION, MODELED WHERE THE ROSTER LIVES rather than only in the seed that reads it. +// +// The seed computes the same two sets inline over `HashSet`s; this module is the authority for +// WHAT THE ADMISSION IS, and its witness is what establishes that the rule discriminates. The +// duplication is the ordinary seed-mirrors-carrier seam and dissolves with the self-emitted +// claim executor, exactly as the terminal ledger's does. + +fn identity_in(xs: List, q: String) -> Bool { + fold_list(xs: xs, empty: false, cons: fn(acc, x) { acc || x == q }) +} + +// ADDED = observed - roster. The set the admission is about. +fn non_verdict_added(observed: List, roster: List) -> List { + fold_list( + xs: observed, + empty: Empty {}, + cons: fn(acc, q) { if identity_in(xs: roster, q: q) { acc } else { Cons { head: q, tail: acc } } }, + ) +} + +// REPAID = roster - observed: rows whose identity produced a verdict this run, so the debt is +// paid and the row must come out. IT REFUSES, and an earlier revision of this line said the +// opposite -- "reported, never gating: a repaid row must not red the run that repaid it". That +// was the original design and review 55361 refuted it: a stale row is a LIVE EXEMPTION, so +// leaving it standing lets the identity regress later and be admitted by the roster that exists +// to bound it. Repayment and deletion are ONE ACT. +// +// The line is called out here rather than quietly overwritten because of WHERE it survived. The +// reversal updated the roster header, the seed's field doc and the gate conjunct, and missed the +// docstring on this function -- leaving two authorities stating opposite rules about one +// admission, inside the module whose whole subject is single authority (review 55515). The +// mechanism was never wrong; only this sentence was, which is exactly why it lasted. +fn non_verdict_repaid(observed: List, roster: List) -> List { + fold_list( + xs: roster, + empty: Empty {}, + cons: fn(acc, q) { if identity_in(xs: observed, q: q) { acc } else { Cons { head: q, tail: acc } } }, + ) +} + +// THE ADMISSION IS "ADDED IS EMPTY AND REPAID IS EMPTY", AND IT IS NOT A COUNT COMPARISON. +// +// `list_length(observed) <= list_length(roster)` would admit every case this refuses except one, +// and the one it wrongly admits is the case the whole mechanism exists for: one identity +// repaired while a different identity begins throwing, with the total unmoved. A count cannot +// see a swap, so the admission is written over identities and the witness beside it drives +// exactly that mutation. +// +// WHY REPAID IS A REFUSAL AND NOT AN ADMISSION, corrected 2026-08-24 (review 55577). An earlier +// revision admitted repayment outright, reasoning that refusing it would red the merge that +// repairs the population. That reasoning was right about the goal and wrong about the subject: a +// repaid identity is one the roster still names and the run no longer observes, which is a STALE +// ROW, and the executing gate refuses exactly that -- `stale_non_verdict` is a conjunct of +// v1_compiler.claim_executor required_floor_outcome_is_clean. So this function said ADMIT where +// its only consumer said REFUSE, which is the DESIGN section 3 divergence a modeled authority +// exists to prevent rather than to demonstrate. +// +// REPAYMENT IS STILL NOT PENALISED, because repaying and deleting the row are ONE ACT: the change +// that repairs an identity deletes its roster row in the same diff, after which the identity is +// in neither collection and both are empty. What refuses is repayment that leaves the row behind, +// which is a roster asserting a debt that no longer exists -- the same monotone-shrink discipline +// the route-gap roster states as "enrolled, and the route did NOT gap: reds the build as a stale +// row". +fn non_verdict_admits(observed: List, roster: List) -> Bool { + length(xs: non_verdict_added(observed: observed, roster: roster)) == 0 + && length(xs: non_verdict_repaid(observed: observed, roster: roster)) == 0 +} diff --git a/src/v2/workflow/required_floor.dag b/src/v2/workflow/required_floor.dag index cab54670c1e..97568655b4e 100644 --- a/src/v2/workflow/required_floor.dag +++ b/src/v2/workflow/required_floor.dag @@ -6,6 +6,7 @@ import v2.std.logic { Bool, True, False } import v2.std.text { String } import v2.std.integer { Int, int_gt } import v2.workflow.floor_expected_red { floor_expected_red_roster } +import v2.workflow.floor_non_verdict { floor_non_verdict_roster } import v2.workflow.floor_route_gap { floor_route_gap_roster } import std.dissolution { DissolutionCondition, unbound_dissolution } import std.nat { Nat } @@ -129,6 +130,22 @@ fn long_home_storage_agreement(path_is_long: Bool, module_is_long: Bool) -> Long // edge the module is not in the world that frame was built from and the call fails with `no // such function` — the failure this comment was written to record the first time. The import is // reachability, not re-export. +// +// `v2.workflow.floor_non_verdict.floor_non_verdict_roster` is the THIRD, and it arrived by +// making the same mistake a third time — with these two paragraphs already sitting here saying +// exactly what would happen. CI refused with `no declaration named +// 'v2.workflow.floor_non_verdict.floor_non_verdict_roster' in this execution's loaded index`, +// which is the same diagnostic, in the same place, for the same missing edge. +// +// THAT IS WORTH RECORDING AS A DEFECT IN THE MECHANISM RATHER THAN IN THREE AUTHORS. A prose +// note is not a wall: this list is a hand-maintained reachability closure that nothing derives +// and nothing checks, so every new roster the host evaluates in this frame must be remembered +// here by whoever adds it, and the failure surfaces only from a full CI run. The refusal is at +// least loud and located — the roster read fails closed, so the floor stops rather than +// proceeding with an empty roster — and that polarity is what keeps this a build failure +// instead of a silently permissive one. The structural repair is for the host's roster +// evaluations to derive their own reachability from the qualified names they call, at which +// point this import list and these three paragraphs delete together. // // THREE PREFIXES, NOT ONE, and the count is what found that. A single `test.claim.long.` test