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

[gunbai-bot]

rust_crate_partition_dissolve_on already states that stage0_module_dag's edges are authored rather than derived, "so a policy over them would balance an incomplete graph". That was true and unquantified. This makes the size of the gap derivable — not transcribed.

The two authorities

Crate dependency is answered twice in stage0: by reexport_packages on each crate row, and by stage0_cross_unit_import_edges projected through the assignment. They already disagree for one unit, and nothing gated the disagreement — stage0_partition_row_lookups_resolved checks only that each named package resolves to some row, never that it matches an edge.

v1-stage0-v1-artifact authors four package dependencies and has zero derived cross-unit out-edges. The reexports are the correct side, established off this graph: src/v1/stage0_v1_artifact/src/lib.rs names all four packages and its Cargo.toml declares all four. So the authored edge list is what is missing them.

The producer, not the numbers

An earlier revision of this PR put the measurement in a String — "78 edges", "five of six units agree". DESIGN §6: "Name the instrument, never transcribe its output… a transcribed number is unreachable from the thing that owns it, so it rots without anyone touching either end." Those figures would have gone stale the moment anyone appended an edge row.

stage0_reexport_derivation_disagreements is now the producer. It folds the authored edges through the assignment into CompilationUnit.deps, closes them transitively, maps them back to package names, and returns the packages whose derived dependency set differs from their authored reexport_packages. The debt row names it.

Its refusal arms are typed. The first draft answered [] when the partition refused to resolve or fold — which reads as "no unit disagrees" from a run that established nothing. That is the §5 absorbing fallback, and it is the same class this lane deleted from compilation_unit in #12028, so it would have been the symptom arriving inside its own repair. Refusal is a constructor now.

The bound is a subset at identity grain

Not an equality, and not a count. Equality would red the floor over debt this row already declares, stopping every lane to repeat what the row says. Subset reds on a new divergence — the thing nothing would otherwise notice — stays green when the edge list is finally derived and the set empties, and becomes the §4b(4) regression control at that point rather than retiring with the climb.

A count equality would stay green if one unit were repaired while another began to diverge, which is why §5 requires membership at identity grain for a monotone debt contract.

The known-bad population is a named data row, not an inline literal: a subset assertion notices nothing when the set shrinks, so an inline literal would let the debt evaporate with no record it was ever paid. As a row, removing a package is an edit someone must justify — where the typed disposition lives.

The vacuous-green guard

Subset-of-known-bad is green when the set is empty and equally green when the detector is broken — 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 mask goes with it. So the detector also runs over supplied units and rows carrying a planted divergence.

Controls

Each mutation run on one build:

                                subset      planted-divergence guard
  unmutated                     PASS        PASS
  known-bad row emptied         FAIL        PASS
  detector comparison removed   PASS        FAIL

Superseded, and corrected here rather than left standing. That matrix was measured against the earlier one-way subset claim. The contract is now equality against the ledger, and re-measuring changes one row: breaking the detector now reds both the contract and the guard, because a detector that finds nothing leaves the ledger's entries missing from the derived set — exactly what no_stale_ledger_entry catches.

So the guard's justification is narrower than I first claimed, and is now stated at its real scope. While the ledger is non-empty, the contract already catches a broken detector. The hole is the future state: once the divergence is repaired the ledger empties, a broken detector yields [] against [], equality holds, the contract goes green and nothing else is looking. The guard is built now because that is when a live example still exists to build it from.

Current controls, one build:

	contract	planted	no-row
unmutated	PASS	PASS	PASS
phantom ledger entry added	FAIL	PASS	PASS
collapsing Absent => acc restored	PASS	PASS	FAIL
detector comparison removed	FAIL	FAIL	PASS

Full witness file: 23 PASS, 0 FAIL.

This matrix was re-run on the post-repair code, not carried over from before it. The cost repair changed what the detector consumes (unit dep edges rather than CompilationUnits), so the earlier controls no longer described it. The first mutation is the one that matters after a cost change: it proves the cheap route still finds the real v1-stage0-v1-artifact divergence, so the 7× did not come from quietly seeing less. The full witness file also runs green (22 PASS, 0 FAIL), which covers the R4 path that the unit-edge consolidation touches.

The cost repair, and why the obvious fix was the wrong one

The first version of this claim was refused by the floor at 191,613 eval steps against the new-witness budget of 72,300. The claim passed — the refusal was about cost, not about the answer — and as a post-cut witness it faces the strict tier.

Measured before changing anything:

	eval steps
stage0_partition_receipt_outcome alone	190,226
the comparison built on top of it	1,640
the planted-divergence guard	361

My fold was 0.9% of the cost. The per-row closure and the repeated row scan — the moves a "make it faster" target sends you at, because they sit at the link where the number was read — could not have reached the budget between them.

The earliest unjustified boundary was one link up: the claim asked partition_fold_outcome for whole CompilationUnits, and that producer saturates interface closures the claim never inspects, to answer a question purely about dependencies. DESIGN §3 names the shape — a claim dominated by one call whose result shape is all it looks at, whose cost does not move when its assertions change. The budget refusal was the tell, not the rule that was broken.

So unit dep edges are now projected from stage0_module_dag.edges through the assignment: the route assignment_unit_graph_has_cycle already used, and which its own note already described as reading that fact "without asking for interfaces". 27,821 eval steps, cpu 32ms — from 191,613 and 234ms.

On which number to compare. The same claim measures 4,589 steps in a full-file run, because earlier witnesses have already evaluated stage0_resolve_partition_outcome and it is memoised. That figure is real and it reads better. It is not the comparable one: the floor's original refusal matched the isolated measurement, so the isolated universe is what the budget adjudicates. 27,821 is the number this PR should be judged on.

A note on the import list, for the next reader

CompilationUnit was initially used in the new fixture without being imported, and the claims still ran — verified by execution, not inference: on the pre-fix head the planted-divergence guard passed and red-ed under the detector mutation, both of which require evaluating probe_unit.

That is a known property, not a defect this PR introduces: a .dag import list is not a binding — resolution falls through to a global spelling search over the corpus. It is rostered twice under gunbc.recurring_failure_mode — shadowing_body_local_bypassed_by_global_call_fallback (the sharp form, where a body-local shadowing a module-scope declaration is bypassed and the call is typed against the global) and resolution_scope_conflated_with_ownership_scope (which names func_sig_from_global_bare directly) — and #12009 deletes the global spelling search, after which an unimported name refuses.

The consequence worth stating: until then, every module's import list is documentation rather than a declaration, so a §3 citation defect of the form "this module depends on that one" is undetectable by the mechanism most readers assume catches it. The import here is added for legibility, not because anything enforced it.

Scope

Deriving the edge list — which dissolves the second authority and makes the equality true by construction — is a stage0 replacement migration with its own root and is deliberately not folded in here.

🤖 Generated with Claude Code

[gunbai-bot]

review 69889 — both findings taken, and the fix reconciles them rather than choosing between them. Pushed in e307014.

Finding 1 (§6, transcribed measurement). Accepted without reservation. Worse than you knew: I had just removed transcribed figures from rust_crate_partition.dag in #12030 on this same rule, then committed the identical violation one PR later.

stage0_reexport_derivation_disagreements is now the producer — it folds the authored edges through the assignment into CompilationUnit.deps, closes them transitively, maps back to package names, and returns the packages whose derived set differs from their authored reexport_packages. The row names it; the numbers are gone.

One thing the first draft of that fold got wrong, recorded because it is the class this lane exists to remove: its refusal arms answered [], which reads as "no unit disagrees" from a run that established nothing — the §5 absorbing fallback arriving inside its own repair. Refusal is a constructor now.

Finding 2 (enrol the fold, don't describe it). You were right that prose was the wrong answer, and your closing line is what moved it — "what buys no new information today is the paragraph; the fold buys the information every time it runs."

I enrolled it as a subset bound at identity grain rather than an equality. Equality would red the floor over debt the row already declares, stopping every lane to repeat what the row says; subset reds on a new divergence, stays green when the edge list is derived and the set empties, and becomes the §4b(4) regression control at that point rather than retiring with the climb. §5's membership-not-count rule is why it is a set and not a count — a count would stay green if one unit were repaired while another began to diverge. The known-bad population is a named data row, not an inline literal, so shrinking it is an edit that carries a disposition.

You also implicitly flagged the trap in the subset form, so I guarded it: subset-of-known-bad is green when the set is empty and green when the detector is broken. The detector therefore also runs over supplied units/rows with a planted divergence.

	subset	planted-divergence guard
unmutated	PASS	PASS
known-bad row emptied	FAIL	PASS
detector comparison removed	PASS	FAIL

Each mutation reds exactly one claim. The third row is the point: with the detector broken the subset claim goes green with no evidence it can still see anything.

Not folded in: deriving the edge list. That is a stage0 replacement migration with its own root, and putting it here would give this change two subjects.

— sent from calm-koi-296

[gunbai-bot]

review 69939 — import added and the unused one dropped, in 2010f74. Re-ran the enrolment rather than adding it blind, as you asked: both claims PASS.

One correction to the reasoning, because the evidence is mine and it points the other way.

The finding infers that the unresolved name should refuse at the floor, and concludes that the vacuous-green guard "cannot be the claim that ran as described." It ran. On e307014 — the exact head you reviewed, without the import — the_disagreement_detector_finds_a_planted_divergence passed, and under the detector mutation it failed:

	subset	planted-divergence guard
unmutated	PASS	PASS
known-bad row emptied	FAIL	PASS
detector comparison removed	PASS	FAIL

Both the pass and the mutation-red require evaluating probe_unit, whose return type and constructor are the name in question. So it resolved.

That is a property of the substrate rather than luck: a .dag import list does not bind — a name absent from the braces still resolves corpus-wide. The consequence cuts both ways and is the useful part: a green run proves nothing about a module's imports, and equally a missing import does not establish that a claim never executed.

None of which makes the fix wrong. Explicit import is the corpus convention you correctly cite at all three call sites, and the dependency should be legible at the import list rather than inferred from the body. I have made it, and removed Stage0FoundationCrate.

The interesting residue, which is not this PR's: if DESIGN §4b names "names resolve" as the ordinary compiler floor, then an unimported name resolving means the import list is not load-bearing — which is a question about gunbc's floor rather than about this change. I am not widening the PR into it, but it seems worth someone's time, and your finding is what surfaced it.

— sent from calm-koi-296

[gunbai-bot]

review 69966 — approved, and neither note needs action before merge. Taking you at your word on that, but one of the two is worth refining rather than leaving as recorded, because someone could later cite it in the general form.

On derived_dep_packages's Absent arm returning [] "failing toward red". That holds for four of the five module-bearing rows, and not for the fifth. stage0_package_sets_agree(authored, []) is true exactly when authored is empty — it is a two-way subset check, so an empty derived set disagrees with any non-empty authored set (→ reported divergent → red), but agrees with an empty one.

v1-stage0-runtime is the foundation crate and carries reexport_packages: []. So for that one row a failed unit lookup produces [] == [] → agree → silent. It is the only row where the Absent arm is invisible rather than red.

That does not change your verdict and I am not fixing it under this PR — a missing unit for a row the fold is iterating would mean the partition receipt and the crate rows had diverged, which is a larger breakage than this arm — but "fails toward red" is true of the rows with reexports and not of the foundation row, and the honest form is worth having on the record. The typed-refusal treatment this arm deserves is the same one I gave the outer fold, and it is small enough to take with the follow-up already queued for partition_fold_deps_match_boundary_edges.

On unit_package_name taking the first matching row — agreed, and your reasoning is the part I would keep: a duplicate unit id surfaces as a divergence rather than silently, because the second row's authored reexports would be compared against the first row's derived set.

— sent from calm-koi-296

[gunbai-bot]

CI fix pushed in 72f8474. The floor red was real and was mine; here is the diagnosis rather than just the patch.

2 failing checks, 1 root cause. witnesses is the aggregating job — its only complaint is "a required lane concluded failure" — so it was downstream of floor, not a second defect.

The floor failure was an over-cost refusal on a passing claim. floor_class=structural, so a verdict about the diff rather than infra: stage0_reexport_derivation_disagreements_are_bounded_to_the_known_unit reached the right answer in 191,613 eval steps against the new-witness budget of 72,300. As a post-cut witness it faces the strict tier — the same mechanism #12028 established, now correctly biting my own work.

Where the cost was, measured before changing anything, because the obvious repair was the wrong one:

	eval steps
stage0_partition_receipt_outcome alone	190,226
the comparison built on top of it	1,640
the planted-divergence guard	361

My fold was 0.9% of the total. Optimizing it — the per-row closure and the repeated row scan, which is where a percentage target would have sent me — could not have reached the budget.

The earliest unjustified boundary was one link up. The claim asked partition_fold_outcome for whole CompilationUnits, and that producer saturates interface closures the claim never inspects, to answer a question purely about dependencies. DESIGN §3 names this shape exactly: a claim dominated by one call whose result shape is all it looks at, whose cost does not move when its assertions change. The budget refusal was the tell, not the rule that was broken.

So the derivation is re-taken rather than the symptom optimized. Unit dep edges are now projected straight from stage0_module_dag.edges through the assignment — the same projection assignment_unit_graph_has_cycle already performs, whose own note describes it as reading the fact "partition_fold_outcome derives as CompilationUnit.deps … without asking for interfaces". The claim consumes stage0_resolve_partition_outcome instead of the receipt; the refusal arm now carries ResolvePartitionOutcome and still refuses rather than answering [].

27,821 eval steps, cpu 32ms — from 191,613 and 234ms. 7×, under budget.

Controls re-run on the new code, not carried over, since the repair changed the detector's inputs:

	subset	planted-divergence guard
unmutated	PASS	PASS
known-bad row emptied	FAIL	PASS
detector comparison removed	PASS	FAIL

The first mutation is the one that matters here: it proves the cheap route still finds the real v1-stage0-v1-artifact divergence, so the 7× did not come from quietly seeing less.

— sent from calm-koi-296

[gunbai-bot]

review 69998 — both findings verified and fixed in 86b1f3d. Both were mine and both are worth naming plainly.

1. The refusal arm admitted the non-refusal. You are right, and the tell you pointed at is the part that stings: Stage0ReexportDisagreementsUnavailable carried a whole ResolvePartitionOutcome, so Unavailable { cause: ResolvePartitionOk { … } } — "unavailable because it succeeded" — was constructible, and the producer had to re-wrap as ResolvePartitionRefused { cause: cause } to fit it. I wrote the note above that type arguing at length that this refusal must not collapse into [], and then gave the refusal a type admitting the state it exists to exclude.

Now ResolvePartitionRefusalCause, exactly as Stage0PartitionReceiptResolveRefused already uses it. §4b rung 4 rather than a check.

2. Naming a duplication is not dissolving it. Also right, and the note I added is the evidence against me — it said outright "this is the same projection assignment_unit_graph_has_cycle already performs," which documents a §3 fork instead of removing one. assignment_unit_graph_has_cycle now consumes assignment_unit_dep_edges and maps to GraphEdge; one producer, and the note records why it is not repeated rather than that it is.

That second fix is on the production R4 path — validate_partition_r4 calls the cycle check — so I ran the whole witness file rather than the two claims this PR adds:

22 PASS, 0 FAIL

The drift candidates you named (self-loop filter, dedup rule) are exactly what a consolidation could have silently changed, and the R4 witnesses are where that would surface.

One number to read carefully. The subject claim measures 4,589 eval steps in a full-file run and 27,821 in isolation; the difference is memoisation of stage0_resolve_partition_outcome by earlier witnesses. The floor's original refusal matched the isolated measurement, so 27,821 is the figure to compare against the 72,300 budget — not the smaller one. I would rather state the conservative number than the flattering one.

— sent from calm-koi-296

[gunbai-bot]

Blocker fixed in 36a8976. The finding is right, and the part worth stating is that I found this defect myself and classified it non-blocking — that triage was wrong, and the reason it was wrong is the useful bit.

My reasoning was: the production route cannot reach it. Stage0 pairs all six unit IDs with six rows, so the Absent arm is unreachable today and the reported result is correct. That is the right test for a production path and the wrong one for this declaration. The detector is deliberately exposed over supplied inputs and is meant to survive as the permanent debt control once the edge list is derived. What decides it is what the signature permits, not what it currently reports — a permanent control that can be handed an input for which it lies is a different object from a code path that happens not to reach the case.

The shape it permitted was this PR's own stated defect arriving through a different arm: a foundation row authoring reexport_packages: [], plus a dropped edge, leaves derived [] against authored [] and certifies agreement from a projection it could not complete.

The repair is the one already queued twice in this lane — return the refusal rather than collapse it — carried all the way to the consumer. derived_dep_packages yields DerivedDepPackagesUnitHasNoRow, the scan yields ReexportDisagreementScanUnitHasNoRow, and the public outcome's cause becomes a coproduct so a lookup failure and a resolve refusal stay distinguishable instead of sharing one arm.

The discriminator you specified, which needed its own claim rather than a wider fixture — the planted-divergence fixture pairs every edge destination with a row, so it never reaches the arm:

	no-row	planted	subset
repaired	PASS	PASS	PASS
Absent => acc restored	FAIL	PASS	PASS

Only the new claim moves, which is the evidence that it discriminates the arm rather than restating what the other two already cover. Full witness file: 23 PASS, 0 FAIL.

I'll leave the merge ask withdrawn until this head is reviewed and its floor is green.

— sent from calm-koi-296

[gunbai-bot]

review 70179 — both findings verified and fixed in feed8d2.

1. A one-way subset never catches a stale ledger entry. Correct, and your rebuttal of my stated reason is the part that settles it. I argued equality would stop lanes over debt the row already declares. But this is equality against the ledger, not against the derived set — it cannot stop a lane over declared debt, and it reds in exactly one situation: the ledger disagreeing with reality, which is the situation nobody would otherwise notice.

The consequence you name is real and it would have falsified the row's own promise. Once v1-stage0-v1-artifact is repaired the derived set empties, the subset still holds, and the ledger goes on naming a unit that no longer diverges — silently re-admitting it to diverge again with the claim green, which is the §4b(3) regression. Nothing forced the edit the row said someone must make and justify.

Three arms now, 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. This is what forces the removal edit.
• no_repaired_divergence_returned — something recorded as repaired came back; the §4b(4) control.

And the removal carries a typed disposition (§5): a repaired divergence moves to stage0_reexport_derivation_repaired_divergences carrying what repaired it, rather than vanishing. That roster is empty today and is not decoration — the third arm asserts against it, so it becomes a live regression control the moment it has a row, and the edge-list derivation is what will put the first one there.

2. A measurement copied into prose. Also correct, and this is the third time in this lane I have transcribed figures into a String after being corrected on exactly this rule — this time inside the annotation explaining the cost repair. They are gone; the annotation names claim_batch's per-witness eval_steps as the producer that re-derives them.

Controls, one build:

	contract	planted	no-row
unmutated	PASS	PASS	PASS
phantom ledger entry added	FAIL	PASS	PASS

Only the contract moves — evidence the new arm discriminates a stale ledger rather than restating what the fixtures already cover. Full witness file: 23 PASS, 0 FAIL.

— sent from calm-koi-296

[gunbai-bot]

review 70187 — finding taken, fixed in 4f67ef1. And you found one instance of a pattern; sweeping for it found three, the third being in my evidence rather than a comment.

The named one. rust_crate_partition_dissolve_on still said the claim "asserts the disagreeing set is a SUBSET … so a NEW divergence reds, a repair stays green." The claim stopped doing that in the previous commit — no_stale_ledger_entry makes a repair red until the package moves to the repaired roster. One fact, two statements, in one change. This is the same class as this file's previous blocker, one PR later.

I took your better option rather than the minimal one: the sentence is removed, not corrected. The contract is the claim's to state; the row names the claim and the ledger. A restatement that has to be kept in step is the §3 fork rather than a convenience.

Two more the sweep found. A witness heading still read "WHY THE BOUND IS A SUBSET", and a note still called it "the subset claim". Both corrected.

And one that was not a comment. The note above the drivable detector asserted that a broken detector leaves the contract green — which was the entire argument for the fixture guard, and which I had repeated in a commit message, two PR comments and the PR body. Re-measured against the equality contract, it is false:

	contract	planted	no-row
unmutated	PASS	PASS	PASS
phantom ledger entry added	FAIL	PASS	PASS
collapsing Absent => acc restored	PASS	PASS	FAIL
detector comparison removed	FAIL	FAIL	PASS

Breaking the detector now reds both, because a detector that finds nothing leaves the ledger's entries missing from the derived set — exactly what no_stale_ledger_entry catches.

So the guard's justification is narrower and is now stated at its real scope. While the ledger is non-empty the contract already catches a broken detector. The hole is the future state: once the divergence is repaired the ledger empties, a broken detector yields [] against [], equality holds, the contract goes green and nothing else is looking. The guard is built now because that is when a live example still exists to build it from.

I carried a measured control result across a design change without re-measuring it — a stale trigger pointed at my own evidence, which is the defect this PR is about. The PR body is corrected rather than left standing; full witness file 23 PASS, 0 FAIL.

— sent from calm-koi-296