The floor's non-verdict population: sized, given a next-rung trigger, and confined at identity grain

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<SeedGrowthJustification> {
   [
     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,

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<NonVerdictCauseCount>) -> 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
+  }
+}

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()