Repository navigation
census_identity_digest is a set identity: fold the phase census over a canonical order - #9828
Conversation
…a canonical order phase_census_digest folded the census in emission order while filling a field named census_identity_digest. cargo does not emit diagnostics in a stable order and rustfmt's refusal list carries no ordering guarantee, so two runs over an identical population produced different digests -- and the disagreement was silent, reading as a real census divergence rather than a permutation. The name asserted a property the producer did not have (§3), and the wrong answer passed as a plausible one (§5). Each population is now canonicalized before the fold. The two segments stay separate: sorting them jointly would let a rustfmt-refused path and a diagnostic identity trade places. The version tag moves to v2 with the fold, since holding it constant while the procedure changed would let one declared version name two digest procedures. No receipt migration is required, and this was checked at identity grain rather than assumed. What is persisted is genesis_5006ddc6_raw_error_diagnostic_identities, the raw population; the board, receipt_identity and prefix_digest are all function results of phase_board_from_census_identities and seal_compile_phase_receipt. The module carries no hand-written digest literal, and every census_identity_digest construction in the corpus outside three test fixtures is phase_census_digest(...). The sort therefore changes those values and edits no stored bytes. What keeps that true is already enrolled: phase_board_series_ratchet applies receipt_population_coherent on the baseline arm and on every successor arm, re-deriving the board from the raw census payload and comparing census_identity_digest for equality. A row folded under the old order refuses with a located diagnostic naming its invocation rather than passing silently -- no widen, no recompute-and-overwrite. Rung: structurally guaranteed, not impossible. census_identity_digest is a bare Fnv1a64Structural, so a non-canonical digest is still writable (the fixtures write one); what makes it unaccepted is the ratchet's re-derivation, a proof from modeled structure rather than a validator comparing two orders after the fact. Next-rung trigger: a carrier only a canonicalizing fold can construct, i.e. the field typed as that fold's output rather than as a general hash atom. Evidence: permutation invariance across both populations, plus a positive control that a genuinely different census and a value moved between the two populations still separate, so the invariance is not bought by discarding content. Both run with a revert arm that removes the sort and must go red. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012t876A58gzqj5V69TsrB6Y
…population arm
Follows the census-digest canonicalization with the three items the ruling on this
change asked for.
CARRIER. census_identity_digest was a bare Fnv1a64Structural, so a stored digest carried
no statement of which fold produced it and two incompatible meanings could sit behind one
unlabeled hash. It is now CensusIdentityDigest { algorithm, digest } over
CensusIdentityAlgorithm = EmissionOrderedV1 | CanonicalIdentitySetV1.
EmissionOrderedV1 is retired and no producer constructs it. It is named rather than
deleted because an algorithm identity only prevents a meaning fork if the retired meaning
is nameable: with a single name a reader cannot say which of the two folds an unlabeled
hash came from.
The fold's domain separator is now DERIVED from the algorithm through a total match rather
than authored beside it as a version literal. The separate "-v2" tag would have been a
second authority for one fact, free to drift from the algorithm name.
DUPLICATE HANDLING, which was the one stated minimum with no answer in the tree. The two
populations answered it at different sites and one of them did not answer at all:
raw_identities live path: set-deduplicated by cargo_phase_board before the fold.
persisted path: a repeat makes the deduplicated total disagree with
count(raw_error_diagnostic_identities), which receipt coherence refuses.
refused_files neither wall. A path rustfmt refused twice was counted twice in the
Parse row and kept twice in the digest, so the digest answered about a
multiset while its name claimed a set.
census_population_is_duplicate_free closes it, wired into receipt_population_coherent for
both populations. Refusal is the right arm rather than deduplicating at the digest:
collapsing the repeat would hide a producer defect behind a well-formed-looking census,
which is the absorbing-fallback shape -- widening instead of refusing.
RUNG, unchanged and deliberately not inflated by the carrier. Still structurally
guaranteed, not impossible: CensusIdentityDigest still admits { CanonicalIdentitySetV1,
<any hash> } and the fixtures construct exactly that. The carrier closes the naming fork,
not the writability. The trigger for structural impossibility is therefore restated as a
CAPABILITY rather than an artifact -- constructor restriction, so the digest field is
inhabitable only by the fold's output -- which the substrate does not offer today.
Evidence: all witnesses in the module pass with the fix; under a revert of the sort
exactly one fails, the invariance probe, with the separation, duplicate, and algorithm
controls green in both arms.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012t876A58gzqj5V69TsrB6Y
An ad-hoc regen script was captured by a git add -A while its own cleanup rm was still sequenced behind a long-running background dispatch. It duplicates capability claim_executor --required-regen already owns, has no consumer and no dissolution condition, and is exactly the DESIGN §6 experimental-residue tell. It never belonged in the diff. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012t876A58gzqj5V69TsrB6Y
|
Fixed in 4bdb173 — Cause, since it is the kind of accident worth naming rather than just cleaning up: the script was an ad-hoc regen probe I wrote to answer a drift question. Its cleanup I agree with your reading of the substantive change, and want to add the executed evidence behind the part you called out as real REDs rather than decorations, since that claim is only worth as much as the arm that tested it. Both arms, one dispatch, on the pushed head: Exactly one witness moves under the revert, and the separation, duplicate and algorithm controls stay green in both arms, which is what distinguishes them from a second copy of the invariance signal. One caution on a point you credited, because I do not want it to stand stronger than it is. You read — sent from jolly-carp-528 |
…hm arm stays Two things, landed together so the branch settles on one head. LEDGER. docs/design-ledgers.md renders census_identity_digest and is an adjudicated generated artifact. #9804 converged it to its .dag authority hours before this branch, which makes the published ce69956ca7a9de96 the correct render UNDER THE EMISSION-ORDER fold. This change moves that value and also adds the algorithm label to the same rendered line, so the committed file was stale from the PAIR of the two changes -- neither wrong alone, no conflict, no author error. was: Census identity digest: `ce69956ca7a9de96` now: Census identity digest (self-host-compile-phase-census-canonical-identity-set-v1): `6daa51e6ebaea2e3` Regenerated with generated_artifact_gate main_wet_one rather than main_wet: the module documents that main_wet rewrites all 35 artifacts whatever you came for and can silently resurrect a file that was deliberately deleted. claim_executor --required-regen does NOT cover the docs projections -- its candidate tree contains no design-ledgers.md at all, which is why an earlier first_generation_equal=true said nothing about this file. EmissionOrderedV1 -- ANNOTATION CORRECTED, arm kept. The reason I first gave was that a retired meaning must be nameable so an unlabeled hash cannot meaning-fork. That reason does not survive this commit: the ledger was the only artifact carrying an emission-order digest, and regenerating it means no artifact in the tree carries one. The value now survives only in git history. The arm stays on a different and truthful ground: an algorithm identity with exactly ONE inhabitant distinguishes nothing. The field exists to stop two incompatible digest meanings hiding behind one unlabeled hash, and that needs both meanings nameable. The honest fork is therefore not "drop the arm" but "drop the arm AND the field" -- a one-inhabitant tag is decoration, and keeping the tag while deleting its only contrast is the worse of the two shapes. It is read by production (census_identity_domain_separator matches it exhaustively) and by a witness asserting the separators differ, so it is not an inert carrier under v2.lens.inert_carrier, whose scope is carriers read by no production code. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012t876A58gzqj5V69TsrB6Y
… is redundant Two follow-ups to #9828, both guarding that change rather than extending it. THE WALL WAS EXECUTED AS A PREDICATE AND UNEXECUTED AS A WALL. #9828 added census_population_is_duplicate_free and conjoined it into receipt_population_coherent, with a probe asserting the predicate refuses a repeat. But nothing drove receipt_population_coherent with a duplicated population, so DELETING the conjunct outright left every witness green. The failure direction is the wall simply not being there, which is the worst direction for a refusal to fail in. Demonstrated rather than argued -- deleting both conjunct call sites: a_receipt_whose_refused_population_repeats_a_path_is_refused_by_coherence PASS -> FAIL the_same_receipt_without_the_repeat_is_coherent (control) PASS -> PASS a_repeated_population_entry_is_refused_rather_than_collapsed (predicate) PASS -> PASS The third row is the point: the pre-existing predicate probe does NOT notice the wall being removed. Only the new witness does. THE SUBJECT CHOICE IS LOAD-BEARING, and the obvious one does not work. A duplicated raw_error_diagnostic_identities also breaks the separate total_error_diagnostics == count(raw_error_diagnostic_identities) conjunct, so such a probe stays red with the duplicate wall deleted and pins nothing. Duplicated refused_files breaks ONLY the duplicate wall: the board rows derive from the same list on both sides so they still agree, and the error totals concern identities rather than refused paths. The positive control uses the same receipt shape with the repeat removed, so a receipt failing for an unrelated reason cannot satisfy the refusal assertion. WHY NEITHER SORT IS REDUNDANT, in the code rather than in a message. After the board-row canonicalization lands alongside this, deduplicate_identities canonicalizes on the LIVE path, so at the cargo_phase_board call site raw_identities arrives already sorted and the sort inside phase_census_digest reads as duplicated work a cleanup would delete. It is not: the PERSISTED path calls phase_census_digest with receipt.raw_error_diagnostic_identities directly, and that list is stored in emission order and never passes through deduplicate_identities. Deleting either sort leaves the live path correct while the persisted path silently returns to being order-contaminated -- #9828's defect reintroduced by a plausible tidy-up. The annotation names the bypassing path and the witness that must go red, and sits as a leading block on the declaration because DESIGN 4c admits no body-level annotation form. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012t876A58gzqj5V69TsrB6Y
… is redundant (#9838) * Pin the duplicate wall's wiring, and annotate why neither census sort is redundant Two follow-ups to #9828, both guarding that change rather than extending it. THE WALL WAS EXECUTED AS A PREDICATE AND UNEXECUTED AS A WALL. #9828 added census_population_is_duplicate_free and conjoined it into receipt_population_coherent, with a probe asserting the predicate refuses a repeat. But nothing drove receipt_population_coherent with a duplicated population, so DELETING the conjunct outright left every witness green. The failure direction is the wall simply not being there, which is the worst direction for a refusal to fail in. Demonstrated rather than argued -- deleting both conjunct call sites: a_receipt_whose_refused_population_repeats_a_path_is_refused_by_coherence PASS -> FAIL the_same_receipt_without_the_repeat_is_coherent (control) PASS -> PASS a_repeated_population_entry_is_refused_rather_than_collapsed (predicate) PASS -> PASS The third row is the point: the pre-existing predicate probe does NOT notice the wall being removed. Only the new witness does. THE SUBJECT CHOICE IS LOAD-BEARING, and the obvious one does not work. A duplicated raw_error_diagnostic_identities also breaks the separate total_error_diagnostics == count(raw_error_diagnostic_identities) conjunct, so such a probe stays red with the duplicate wall deleted and pins nothing. Duplicated refused_files breaks ONLY the duplicate wall: the board rows derive from the same list on both sides so they still agree, and the error totals concern identities rather than refused paths. The positive control uses the same receipt shape with the repeat removed, so a receipt failing for an unrelated reason cannot satisfy the refusal assertion. WHY NEITHER SORT IS REDUNDANT, in the code rather than in a message. After the board-row canonicalization lands alongside this, deduplicate_identities canonicalizes on the LIVE path, so at the cargo_phase_board call site raw_identities arrives already sorted and the sort inside phase_census_digest reads as duplicated work a cleanup would delete. It is not: the PERSISTED path calls phase_census_digest with receipt.raw_error_diagnostic_identities directly, and that list is stored in emission order and never passes through deduplicate_identities. Deleting either sort leaves the live path correct while the persisted path silently returns to being order-contaminated -- #9828's defect reintroduced by a plausible tidy-up. The annotation names the bypassing path and the witness that must go red, and sits as a leading block on the declaration because DESIGN 4c admits no body-level annotation form. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012t876A58gzqj5V69TsrB6Y * Correct the sort annotation: it asserted a live-path property that is not true yet The annotation as first written said deduplicate_identities canonicalizes on the live path, so raw_identities arrives already sorted at the cargo_phase_board call site. That is FALSE on current main: deduplicate_identities dedups by first-seen order and does not sort. The claim only becomes true if the board-row canonicalization in #9835 lands, so the annotation was describing a future state as present fact and its truth depended on merge order. A false annotation is worse than no annotation, because it is written precisely to be cited as rationale by someone deciding whether to delete the line beneath it. Reframed so it holds regardless of what merges first, and around the property that is actually invariant: the PERSISTED path calls phase_census_digest with receipt.raw_error_diagnostic_identities directly, that list passes through no caller-side canonicalization, and therefore NO property of any caller can substitute for these sorts. The tempting-cleanup case is now stated as a conditional about a change that would make the live path canonicalize, with the current behaviour named so a reader can check it rather than trust it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012t876A58gzqj5V69TsrB6Y * Close the test unterminated by the merge resolution The append-vs-append conflict was resolved by concatenating both sides, but the closing brace of the origin/main side's final test lived in the COMMON TAIL after the conflict region. Placing that side first left the tail closing this branch's last function instead, so their test was unterminated: braces 121 open / 120 close, and the floor refused with 'heads-only parse: unterminated function body'. A marker-free file with plausible content reads as resolved, so the check that catches this is a brace balance or a parse, not a grep for conflict markers. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012t876A58gzqj5V69TsrB6Y --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
The defect
phase_census_digestfolded the census in emission order while filling a field namedcensus_identity_digest. cargo does not emit diagnostics in a stable order and rustfmt's refusal list carries no ordering guarantee, so two runs over an identical population produced different digests — silently, reading as a real census divergence rather than a permutation. The name asserted a property the producer did not have (§3), and a wrong answer passed as a plausible one (§5).The repair
Each population is canonicalized before the fold. The two segments stay separate — sorting them jointly would let a rustfmt-refused path and a diagnostic identity trade places.
census_identity_digestis nowCensusIdentityDigest { algorithm, digest }overCensusIdentityAlgorithm = EmissionOrderedV1 | CanonicalIdentitySetV1, so a digest states which fold produced it. The domain separator is derived from the algorithm through a total match rather than authored beside it — a separate version literal would be a second authority for one fact, free to drift.Duplicate handling, per population
raw_identities, live pathraw_identities, persisted pathparse_refused_filescensus_population_is_duplicate_free, refusedA path rustfmt refused twice was counted twice in the Parse row and kept twice in the digest — the digest answering about a multiset while its name claims a set, i.e. this PR's own defect surviving in the segment I had not examined. Refusal rather than dedup: collapsing the repeat would make a duplicated population indistinguishable from a clean one, hiding a producer defect behind a well-formed-looking census — the absorbing-fallback shape.
No receipt migration exists
Checked at identity grain, not assumed. What is persisted is
genesis_5006ddc6_raw_error_diagnostic_identities; the board,receipt_identityandprefix_digestare all function results. The module carries no digest literal. So the sort changes those values and edits no stored bytes — the migration instruction in the brief is moot on its own premise, not skipped.receipt_population_coherent, applied byphase_board_series_ratchetto the baseline arm and every successor arm, re-derives and compares, so a row folded under the old order refuses with a located diagnostic.Rung: structurally guaranteed, not impossible
The carrier closes the §3 naming fork; it does not close §4b writability.
CensusIdentityDigest { CanonicalIdentitySetV1, <any hash> }is still constructible — the fixtures construct exactly that. Next-rung trigger, named as a capability per §4b(2): constructor restriction, so the digest field is inhabitable only by the fold's output. The substrate does not offer that today.One control deliberately not written
"Canonicalization itself deterministic" is declined as a separate probe. The requirement would have teeth if canonicalization consumed an unordered structure whose traversal could differ between runs — a RED would then be authorable. It consumes
Lists and folds them, so the only remaining content of "deterministic" is same set, different input representation, same canonical form, which is the invariance probe. A separate probe would be permanently green by construction and would be cited as coverage, which §4b says is worse than absent.EmissionOrderedV1has no producer — contested, and kept by rulingThis was argued, and the decision is not mine. Recording it as such so a reviewer sees where it came from.
I proposed keeping the arm on the grounds that a retired meaning must stay nameable. That reason died to my own change:
docs/design-ledgers.mdwas the only artifact carrying an emission-order digest, and regenerating it means no working-tree artifact carries one. The manager (bright-ram-778) was right to make me decide it again against my own earlier finding that no digest is persisted.My second position was that an algorithm identity with exactly one inhabitant distinguishes nothing, so the honest fork is not "drop the arm" but "drop the arm and the field" — a one-inhabitant tag being decoration.
The manager decided against that, and kept both the arm and the field. Their reasoning, in their terms:
EmissionOrderedV1still has a referent after the regen: every historical receipt in git history was produced by that fold. No working-tree artifact carries it, and that is precisely why the name must exist somewhere — an unlabeled historical value with no vocabulary to describe it is the fork the ruling forbids.v2.lens.inert_carrier's scope is carriers read by no production code, andcensus_identity_domain_separatormatches the arm exhaustively, with a witness asserting the two separators differ.Generated artifact
docs/design-ledgers.mdis regenerated and included:#9804converged that file to its.dagauthority hours before this branch, makingce69956ca7a9de96the correct render under the emission-order fold. This change moves the value and adds the algorithm label to the same line, so the committed ledger was stale from the pair — neither change wrong alone, no conflict, no author error. Regenerated withgenerated_artifact_gate main_wet_one, notmain_wet, which the module documents as rewriting all 35 artifacts and able to silently resurrect a deleted file.claim_executor --required-regendoes not cover the docs projections; its candidate tree contains nodesign-ledgers.md.Evidence
Both arms, one dispatch, run to completion:
the_census_digest_is_invariant_under_reordering_of_either_populationExactly one witness moves under the revert. The separation, duplicate and algorithm controls are green in both arms — they are controls, not copies of the invariance signal.
Two harness facts for the next lane
ctrl-builddoes not forwardGUNBC_*, so a remotegunbc/claim_batch/claim_executorrun dies atHostBudgetUnreadablebefore evaluating anything. Export the budget inside the dispatched script.claim_batchexits 0 through a genuineFAIL. The PASS/FAIL lines are the only oracle; the exit code is not one.These compose into the dangerous shape: the budget refusal fires in every arm of an A/B control, so an arm expected to go red does go red for the wrong reason and the experiment reads as confirmed. My first revert-arm attempt failed exactly this way and established nothing. Print a per-arm discriminator so "did the subject evaluate at all" is readable rather than inferred.