Derive the stage0 edge-list disagreement, and enrol the fold that keeps it honest

src/v2/test/claim/rust_crate_partition_witness_test.dag

@@ -40,6 +40,17 @@ import v2.workflow.rust_crate_partition {
   rust_crate_partition_module_bearing_unit_target,
   stage0_interim_explicit_assignment,
   stage0_module_dag,
+  Stage0PartitionCrateRow,
+  Stage0LayeredCoreCrate,
+  UnitDepEdge,
+  ReexportDisagreementScanOk,
+  ReexportDisagreementScanUnitHasNoRow,
+  Stage0ReexportDisagreementsDerived,
+  Stage0ReexportDisagreementsUnavailable,
+  reexport_derivation_disagreements_over,
+  stage0_reexport_derivation_disagreements,
+  stage0_reexport_derivation_known_divergent_packages,
+  stage0_reexport_derivation_repaired_divergences,
   stage0_module_dag_interface_grounding,
   InterfaceGroundingCapability,
   Stage0ModuleDagInterfaceSourceGrounded,
@@ -384,6 +395,107 @@ test fn witness_stage0_module_dag_interface_grounding_debt_declared_holds() -> B
   stage0_module_dag_interface_grounding_is_debt()
 }
 
+// ── THE TWO AUTHORITIES FOR "WHAT DOES THIS CRATE DEPEND ON", AND WHY THE BOUND IS AN EQUALITY ──
+//
+// rust_crate_partition_dissolve_on declares stage0's edges authored rather than derived. The size
+// of that gap is DERIVED by stage0_reexport_derivation_disagreements rather than transcribed into
+// prose (DESIGN 6), and this pins its population at IDENTITY grain rather than by count: a count
+// equality would stay green if one unit were repaired while another began to diverge.
+//
+// EQUALITY AGAINST THE LEDGER, IN BOTH DIRECTIONS, plus the repaired roster. A one-way subset --
+// which this claim used to be -- catches a NEW divergence and nothing else: once
+// v1-stage0-v1-artifact is repaired the derived set empties, the subset still holds, and the ledger
+// keeps naming a unit that no longer diverges. A stale entry then silently re-admits that unit to
+// diverge again with this claim green, which is the regression DESIGN 4b(3) forbids.
+//
+// The objection to equality does not apply, because this is equality against the LEDGER rather than
+// against the derived set: it cannot stop a lane over debt the ledger already declares, and it reds
+// in exactly one situation -- the ledger disagreeing with reality.
+//
+// Three arms, each with its own red. no_new_divergence: a unit outside the ledger started
+// diverging. no_stale_ledger_entry: a ledger unit stopped diverging and nobody recorded it, which
+// is what forces the removal edit and its typed disposition (DESIGN section 5). And
+// no_repaired_divergence_returned: something recorded as repaired came back -- the 4b(4) regression
+// control, which keeps the climb real rather than retiring with it.
+test fn stage0_reexport_derivation_disagreements_are_bounded_to_the_known_unit() -> Bool {
+  match stage0_reexport_derivation_disagreements() {
+    Stage0ReexportDisagreementsUnavailable { cause: _ } => false
+    Stage0ReexportDisagreementsDerived { packages: packages } => {
+      let no_new_divergence = packages |> fold(init: true, f: fn(ok, pkg) {
+        ok && (stage0_reexport_derivation_known_divergent_packages |> any(known => known == pkg))
+      })
+      let no_stale_ledger_entry = stage0_reexport_derivation_known_divergent_packages
+        |> fold(init: true, f: fn(ok, known) {
+          ok && (packages |> any(pkg => pkg == known))
+        })
+      let no_repaired_divergence_returned = stage0_reexport_derivation_repaired_divergences
+        |> fold(init: true, f: fn(ok, repaired) {
+          ok && !(packages |> any(pkg => pkg == repaired.package_name))
+        })
+      no_new_divergence && no_stale_ledger_entry && no_repaired_divergence_returned
+    }
+  }
+}
+
+// THE VACUOUS-GREEN GUARD, and it is the claim that keeps the one above honest. Subset-of-known-bad
+// is green when the disagreement set is EMPTY and equally green when the detector is BROKEN and
+// finds nothing -- the same observation from two different worlds. Today v1-stage0-v1-artifact
+// inhabits the set and masks that; when the edge list is derived the set empties and the mask goes
+// with it, leaving a permanently green assertion with no evidence it can still see anything, which
+// is the inert lens DESIGN section 5 names. So the detector is run over SUPPLIED units and rows
+// carrying a PLANTED disagreement: "probe-diverging" authors a dependency the unit graph does not
+// give it, "probe-agreeing" authors exactly what it derives. Removing the comparison from
+// reexport_derivation_disagreements_over reds this and leaves the OTHER two claims untouched.
+fn probe_edge(from: String, to: String) -> UnitDepEdge {
+  UnitDepEdge { from: from as CompilationUnitId, to: to as CompilationUnitId }
+}
+
+fn probe_row(package: String, unit: String, reexports: List<String>) -> Stage0PartitionCrateRow {
+  Stage0PartitionCrateRow {
+    unit_id: unit as CompilationUnitId,
+    package_name: package,
+    crate_dir: "src/probe",
+    kind: Stage0LayeredCoreCrate,
+    modules: [],
+    reexport_packages: reexports,
+    carries_non_empty_wrappers: false,
+  }
+}
+
+test fn the_disagreement_detector_finds_a_planted_divergence() -> Bool {
+  let edges = [probe_edge(from: "u-agree", to: "u-base")]
+  let rows = [
+    probe_row(package: "probe-base", unit: "u-base", reexports: []),
+    probe_row(package: "probe-agreeing", unit: "u-agree", reexports: ["probe-base"]),
+    probe_row(package: "probe-diverging", unit: "u-diverge", reexports: ["probe-base"]),
+  ]
+  match reexport_derivation_disagreements_over(edges: edges, rows: rows) {
+    ReexportDisagreementScanUnitHasNoRow { unit_id: _ } => false
+    ReexportDisagreementScanOk { packages: found } =>
+      (found |> any(p => p == "probe-diverging"))
+        && !(found |> any(p => p == "probe-agreeing"))
+        && !(found |> any(p => p == "probe-base"))
+  }
+}
+
+// THE DISCRIMINATOR FOR THE FALSE GREEN, and it is the input the detector used to certify.
+// A FOUNDATION row authors reexport_packages: [] and has a derived edge to a unit that NO package
+// row covers. The old fold dropped that edge, leaving derived [] against authored [], and reported
+// AGREEMENT from a projection it could not complete -- the exact shape this declaration exists to
+// make impossible, reached through the arm rather than through the comparison.
+//
+// It must REFUSE. Restoring `Absent => acc` inside derived_dep_packages reds this claim and leaves
+// the planted-divergence guard above green, because that fixture pairs every edge destination with
+// a row and so never reaches the arm -- which is why this case needed its own claim rather than a
+// wider fixture.
+test fn a_dep_edge_to_a_unit_with_no_package_row_refuses() -> Bool {
+  let edges = [probe_edge(from: "u-foundation", to: "u-unrostered")]
+  let rows = [probe_row(package: "probe-foundation", unit: "u-foundation", reexports: [])]
+  match reexport_derivation_disagreements_over(edges: edges, rows: rows) {
+    ReexportDisagreementScanUnitHasNoRow { unit_id: unit_id } => (unit_id as String) == "u-unrostered"
+    ReexportDisagreementScanOk { packages: _ } => false
+  }
+}
 // The debt row's trigger has now been repointed twice, and BOTH previous targets named an
 // authority that could not carry the fact -- a roster row and then a module-to-location index.
 // This pins the third: the dissolve target must name the module-binding SUPPLY, whose contents