The dissolution census asserted over an empty population, so its headline green could not fail

dag/gunbc/dissolution_census.dag

@@ -2,43 +2,48 @@ module gunbc.dissolution_census
 
 import std.roster_frontier {
   FrontierRow,
-  FrontierExpiryReport,
-  fold_frontier_expiry,
   frontier_expiry_clean,
   frontier_rows_well_formed,
 }
 import std.dissolution { DissolutionCondition, dissolution_is_bound }
-import std.decl_ref { DeclarationRef }
+import std.decl_ref { declaration_ref_display_key }
 import gunbc.census_closure_frontier { census_closure_frontier_rows }
-
-fn dissolution_census_report() -> FrontierExpiryReport {
-  fold_frontier_expiry(rows: census_closure_frontier_rows(), present_decls: [])
-}
-
-fn dissolution_census_report_against(present_decls: List<DeclarationRef>) -> FrontierExpiryReport {
-  fold_frontier_expiry(rows: census_closure_frontier_rows(), present_decls: present_decls)
-}
-
-fn dissolution_census_unbound_count() -> Int {
-  dissolution_census_report().unbound_count
-}
-
-fn dissolution_census_pending_count() -> Int {
-  dissolution_census_report().pending_count
-}
-
-fn dissolution_census_fired_still_present_count() -> Int {
-  dissolution_census_report().fired_still_present_count
-}
-
-fn dissolution_census_total() -> Int {
-  let r = dissolution_census_report()
-  r.unbound_count + r.pending_count + r.fired_still_present_count
+import gunbc.dissolution_observation {
+  DissolutionCensusVerdict,
+  DissolutionCensusAnswered,
+  DissolutionCensusRefused,
+  dissolution_census_pool_roots,
+  dissolution_census_facts,
+  dissolution_census_modules,
+  dissolution_census_verdict_for,
+}
+
+// THE CENSUS IS THE ROSTER-BEARING HALF. The mechanism — resolving a trigger ref against
+// the live declaration index and refusing what it cannot decide — lives in
+// gunbc.dissolution_observation, which imports no roster, so a consumer that wants the
+// mechanism does not acquire this module's ~20-module extdeps fan-in to get it.
+fn dissolution_census_verdict() -> DissolutionCensusVerdict {
+  dissolution_census_verdict_for(
+    rows: census_closure_frontier_rows(),
+    facts: dissolution_census_facts(),
+    modules: dissolution_census_modules(),
+  )
+}
+
+fn dissolution_census_refused_keys(verdict: DissolutionCensusVerdict) -> List<String> {
+  match verdict {
+    DissolutionCensusAnswered { report: _ } => []
+    DissolutionCensusRefused { undecided: u } =>
+      u |> map(r => declaration_ref_display_key(ref: r))
+  }
 }
 
 fn dissolution_census_holds() -> Bool {
   frontier_rows_well_formed(rows: census_closure_frontier_rows())
-    && frontier_expiry_clean(report: dissolution_census_report())
+    && match dissolution_census_verdict() {
+      DissolutionCensusRefused { undecided: _ } => false
+      DissolutionCensusAnswered { report: r } => frontier_expiry_clean(report: r)
+    }
 }
 
 fn frontier_rows_bound_count(rows: List<FrontierRow>) -> Int {

dag/gunbc/dissolution_observation.dag

@@ -0,0 +1,184 @@
+module gunbc.dissolution_observation
+
+import std.roster_frontier {
+  FrontierRow,
+  FrontierExpiryReport,
+  fold_frontier_expiry,
+}
+import std.dissolution {
+  DissolutionCondition,
+  BoundDissolution,
+  UnboundDissolution,
+  dissolution_is_bound,
+  dissolution_trigger_ref,
+}
+import std.decl_ref { DeclarationRef, declaration_ref_display_key }
+import v2.std.decl_index { DeclFact, decl_facts }
+import v2.lens.module_graph { ModuleDeclarationFact, module_declaration_facts_live }
+import v2.std.decl_ref_resolution {
+  resolve_declaration_ref,
+  DeclarationRefResolved,
+  DeclarationRefModuleAbsent,
+  DeclarationRefDeclarationAbsent,
+  DeclarationRefFieldAbsent,
+  DeclarationRefAmbiguous,
+}
+
+// THE POPULATION THE FOLD IS ANSWERED AGAINST, AND WHY IT USED TO BE EMPTY.
+//
+// `dissolution_census_report` folded the roster against `present_decls: []`. Under an
+// empty population no `DeclarationAppears` trigger can ever be found, so every bound row
+// reports Pending, `fired_still_present_count` is 0 BY CONSTRUCTION, and
+// `frontier_expiry_clean` — the census's headline assertion — could not fail. That is
+// not a weak check; it is a predicate with one reachable answer, reporting green over a
+// roster nothing had read. `std.dissolution` was a correct model with no observer.
+//
+// The population is now the live tree, and the two trigger directions read it in
+// opposite ways: a forward trigger fires when its declaration is FOUND, a retirement
+// trigger when it is GONE. That symmetry is why a partial or wrong population is
+// dangerous rather than merely imprecise — it would mass-fire one direction while
+// mass-silencing the other — so nothing here answers a ref it could not resolve.
+data dissolution_census_pool_roots: List<String> = ["dag", "src/v2"]
+
+fn dissolution_census_facts() -> List<DeclFact> {
+  decl_facts(pool_roots: dissolution_census_pool_roots)
+}
+
+fn dissolution_census_modules() -> List<ModuleDeclarationFact> {
+  module_declaration_facts_live(pool_roots: dissolution_census_pool_roots)
+}
+
+fn frontier_row_trigger_refs(row: FrontierRow) -> List<DeclarationRef> {
+  match row.dissolution {
+    BoundDissolution { trigger: t } => [dissolution_trigger_ref(trigger: t)]
+    UnboundDissolution { description: _ } => []
+  }
+}
+
+fn census_trigger_refs(rows: List<FrontierRow>) -> List<DeclarationRef> {
+  flat_map(rows, row => frontier_row_trigger_refs(row: row))
+}
+
+// A MODULE THE DECLARATION INDEX DOES NOT COVER IS NOT A MODULE WHOSE DECLARATIONS ARE
+// GONE, and conflating the two is the whole hazard. `decl_facts` deliberately skips test
+// `.dag` files while `module_declaration_facts` still reports their modules, so a ref
+// into a witness module resolves as DeclarationAbsent for a reason that has nothing to
+// do with the tree. `std.decl_ref` already names this state
+// (`OutsideDeclIndexTestWitnessModule`); here it is DERIVED rather than pattern-matched
+// on a path convention — a module is outside the index exactly when the index carries no
+// declaration from its file at all.
+fn module_rel_path(module_path: String, modules: List<ModuleDeclarationFact>) -> String {
+  fold(modules, init: "", f: fn(acc, m) { if m.module == module_path { m.path } else { acc } })
+}
+
+fn index_covers_rel_path(rel_path: String, facts: List<DeclFact>) -> Bool {
+  fold(facts, init: false, f: fn(acc, f) { acc || f.rel_path == rel_path })
+}
+
+type CensusRefVerdict
+  = CensusRefPresent { ref: DeclarationRef }
+  | CensusRefAbsent { ref: DeclarationRef }
+  | CensusRefOutsideIndex { ref: DeclarationRef }
+  | CensusRefAmbiguous { ref: DeclarationRef }
+
+fn census_ref_verdict(
+  ref: DeclarationRef,
+  facts: List<DeclFact>,
+  modules: List<ModuleDeclarationFact>,
+) -> CensusRefVerdict {
+  match resolve_declaration_ref(ref: ref, facts: facts, modules: modules) {
+    DeclarationRefResolved { declaration_identity: _ } => CensusRefPresent { ref: ref }
+    DeclarationRefAmbiguous { reference: _, candidates: _ } => CensusRefAmbiguous { ref: ref }
+    DeclarationRefFieldAbsent { reference: _ } => CensusRefAbsent { ref: ref }
+    DeclarationRefModuleAbsent { reference: _ } => CensusRefAbsent { ref: ref }
+    DeclarationRefDeclarationAbsent { reference: _ } =>
+      if index_covers_rel_path(
+        rel_path: module_rel_path(module_path: ref.module_path as String, modules: modules),
+        facts: facts,
+      ) {
+        CensusRefAbsent { ref: ref }
+      } else {
+        CensusRefOutsideIndex { ref: ref }
+      }
+  }
+}
+
+fn census_ref_is_present(verdict: CensusRefVerdict) -> Bool {
+  match verdict {
+    CensusRefPresent { ref: _ } => true
+    CensusRefAbsent { ref: _ } => false
+    CensusRefOutsideIndex { ref: _ } => false
+    CensusRefAmbiguous { ref: _ } => false
+  }
+}
+
+fn census_ref_is_undecided(verdict: CensusRefVerdict) -> Bool {
+  match verdict {
+    CensusRefPresent { ref: _ } => false
+    CensusRefAbsent { ref: _ } => false
+    CensusRefOutsideIndex { ref: _ } => true
+    CensusRefAmbiguous { ref: _ } => true
+  }
+}
+
+fn census_ref_verdict_ref(verdict: CensusRefVerdict) -> DeclarationRef {
+  match verdict {
+    CensusRefPresent { ref: r } => r
+    CensusRefAbsent { ref: r } => r
+    CensusRefOutsideIndex { ref: r } => r
+    CensusRefAmbiguous { ref: r } => r
+  }
+}
+
+fn census_ref_verdicts(
+  rows: List<FrontierRow>,
+  facts: List<DeclFact>,
+  modules: List<ModuleDeclarationFact>,
+) -> List<CensusRefVerdict> {
+  census_trigger_refs(rows: rows)
+    |> map(ref => census_ref_verdict(ref: ref, facts: facts, modules: modules))
+}
+
+// The present population is the roster's OWN refs that resolved, so identity is exact —
+// no qualified-name reprojection stands between the resolver's answer and the fold's
+// `declaration_ref_eq`, and field grain is preserved because the resolver already
+// decided it.
+fn census_present_decls(verdicts: List<CensusRefVerdict>) -> List<DeclarationRef> {
+  verdicts
+    |> filter(v => census_ref_is_present(verdict: v))
+    |> map(v => census_ref_verdict_ref(verdict: v))
+}
+
+fn census_undecided_refs(verdicts: List<CensusRefVerdict>) -> List<DeclarationRef> {
+  verdicts
+    |> filter(v => census_ref_is_undecided(verdict: v))
+    |> map(v => census_ref_verdict_ref(verdict: v))
+}
+
+// THE FAILURE ARM REFUSES, IT DOES NOT WIDEN OR NARROW (DESIGN §5). A ref the resolver
+// could not decide is neither present nor absent, and answering it either way would
+// silently fire one trigger direction. The verdict carries the located refs so the
+// deficit is countable and prioritizable rather than absorbed.
+type DissolutionCensusVerdict
+  = DissolutionCensusAnswered { report: FrontierExpiryReport }
+  | DissolutionCensusRefused { undecided: List<DeclarationRef> }
+
+fn dissolution_census_verdict_for(
+  rows: List<FrontierRow>,
+  facts: List<DeclFact>,
+  modules: List<ModuleDeclarationFact>,
+) -> DissolutionCensusVerdict {
+  let verdicts = census_ref_verdicts(rows: rows, facts: facts, modules: modules)
+  let undecided = census_undecided_refs(verdicts: verdicts)
+  if length(xs: undecided) > 0 {
+    DissolutionCensusRefused { undecided: undecided }
+  } else {
+    DissolutionCensusAnswered {
+      report: fold_frontier_expiry(
+        rows: rows,
+        present_decls: census_present_decls(verdicts: verdicts),
+      ),
+    }
+  }
+}
+

dag/test/claim/dissolution_census_mechanism_witness_test.dag

@@ -11,6 +11,13 @@ import std.dissolution { bound_dissolution, unbound_dissolution, retires_dissolu
 import extdeps.bmc.serial_console { sol_console_send_bash_emit_dissolution_trigger }
 import extdeps.linux.usb_gadget { configfs_op_render_dissolution_trigger }
 import extdeps.storage.nbd { nbd_server_config_render_dissolution_trigger }
+import gunbc.dissolution_observation {
+  DissolutionCensusAnswered,
+  DissolutionCensusRefused,
+  dissolution_census_verdict_for,
+}
+import v2.std.decl_index { decl_facts }
+import v2.lens.module_graph { module_declaration_facts_live }
 import std.roster_frontier { FrontierRow, frontier_row_decl, fold_frontier_expiry, frontier_expiry_clean }
 
 fn planted_bound_ref() -> DeclarationRef {
@@ -99,6 +106,63 @@ test fn migrated_production_retirement_conditions_are_bound() -> Bool {
     && dissolution_is_bound(condition: nbd_server_config_render_dissolution_trigger)
 }
 
+// THE LIVE DISCRIMINATOR, AND IT IS DELIBERATELY NOT A COUNT.
+//
+// Once `present_decls` is real, the two trigger arms read the population in OPPOSITE
+// directions, so a wrong or partial population mass-fires one of them while
+// mass-silencing the other — and any assertion phrased as a total is satisfied by both
+// mistakes. The pair below is phrased at identity grain instead: one subject KNOWN to be
+// present and one KNOWN to be absent, asserted in opposite directions IN THE SAME RUN
+// against the same resolver answer. A population that lost the tree fails the first; a
+// population that fabricated it fails the second.
+//
+// The pool is the purpose-built fixture rather than a production directory: the subject
+// under test is the RESOLVER's behaviour, and scanning production to establish it prices
+// the mechanism at that directory's breadth — the cost-shape defect DESIGN §6 names.
+// Measured rather than assumed: pointed at `dag/std` this row was BUDGET-REFUSED at
+// 5510ms against the floor's 5000ms deadline and went undecided, which is a worse
+// outcome than a failure because nothing then claims it is broken.
+data live_discriminator_pool_roots: List<String> = ["dag/test/fixture/dissolution_live_discriminator"]
+
+fn live_discriminator_rows() -> List<FrontierRow> {
+  [
+    frontier_row_decl(
+      ref: decl_ref(module_path: "test.claim.dissolution_census_mechanism_witness_test", decl_name: "present_subject_row"),
+      reason: "live discriminator: subject known present, so its retirement is PENDING",
+      dissolution: retires_dissolution(
+        ref: decl_ref(
+          module_path: "test.fixture.dissolution_live_discriminator.subject",
+          decl_name: "present_subject_declaration",
+        ),
+      ),
+    ),
+    frontier_row_decl(
+      ref: decl_ref(module_path: "test.claim.dissolution_census_mechanism_witness_test", decl_name: "absent_subject_row"),
+      reason: "live discriminator: subject known absent, so its arrival is PENDING",
+      dissolution: bound_dissolution(
+        ref: decl_ref(
+          module_path: "test.fixture.dissolution_live_discriminator.subject",
+          decl_name: "absent_subject_declaration",
+        ),
+      ),
+    ),
+  ]
+}
+
+test fn opposite_trigger_directions_agree_on_one_live_population() -> Bool {
+  match dissolution_census_verdict_for(
+    rows: live_discriminator_rows(),
+    facts: decl_facts(pool_roots: live_discriminator_pool_roots),
+    modules: module_declaration_facts_live(pool_roots: live_discriminator_pool_roots),
+  ) {
+    DissolutionCensusRefused { undecided: _ } => false
+    DissolutionCensusAnswered { report: r } =>
+      r.pending_count == 2
+        && r.fired_still_present_count == 0
+        && r.unbound_count == 0
+  }
+}
+
 fn w_unbound_dissolution_empty_literal_red() -> Bool {
   compile_dag_rust_emit_check(
     "module dissolution_empty_literal_red\nimport std.dissolution { DissolutionCondition, unbound_dissolution }\ndata bad: DissolutionCondition = unbound_dissolution(description: \"\")\n",