Repository navigation
A mirror pair cannot leave the published population unnoticed - #2392
Merged
matrixarkai merged 1 commit intoOct 30, 2026
Merged
matrixarkai merged 1 commit into
matrixarkai merged 1 commit into
Conversation
`every_page_named_shard_stat_agrees_with_its_block_twin` built its groups with `groups.retain(|_, members| members.len() >= 2)` and then asserted the group COUNT. Retiring one spelling of a pair drops the group below two members, the count stops matching, and the obvious repair is to lower the number -- at which point nothing compares that pair's two spellings any more and every assertion in the file is green. The count moved and the coverage went with it. It also could not tell the two halves of a retirement apart: dropping `block_reads` and keeping `page_reads` lowers the count by exactly as much as dropping `page_reads` does. The filter is gone, so a one-member group is still a group, and the population is declared by TWINNED_ON_SHARD_STATS and SINGLE_ON_SHARD_STATS. Retiring a spelling means moving a name between those two lists, and five clauses refuse every other way of shrinking the population: the rosters are well formed and a retired name's survivor is the block spelling; the set of names published under two or more spellings IS the twinned roster, in both directions; each declared pair carries exactly its two spellings; each retired name carries exactly its survivor; and the pair agrees and is non-zero. The published contract test had the same defect -- it counted its two page-spelled keys -- so the count becomes the named set PAGE_SPELLED_CONTRACT_KEYS. Three facts the module header used to carry as prose are now scanned for instead: no type declared with a name beginning `Page`, no `page_id` or `page_ordinal` FIELD, and no `const`/`static PAGE_SIZE`. Each matcher requires the line to BE a declaration, so a doc line, a serde alias and a JSON key inside a fixture string cannot match and no path needs excluding by hand. Five non-vacuity clauses: the walk reaches a file floor and recurses, each matcher is exercised in both directions, and the walk is required to find the Block spelling of two of the three shapes. No published key, no stored key, no format stamp and no value moves. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
matrixarkai
deleted the
guard/a-mirror-pair-cannot-leave-the-published-population-unnoticed
branch
October 30, 2026 06:07
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
pageandblockname one storage tier in this crate,blockis the canonicalspelling, and the published
page_*statistics are a mirror of theblock_*ones.every_page_named_shard_stat_agrees_with_its_block_twinis what holds that mirrortogether. It could be switched off by shrinking the population it checks.
The defect
The test built its groups like this:
and then asserted the group COUNT:
Retire one spelling of a pair and the group falls below two members, so it is dropped
from the map entirely. The count then no longer matches, and the obvious repair is to
lower the number. The moment the number is lowered, nothing in the file compares the two
spellings of that pair any more, and every assertion is green. The count moved and the
coverage went with it — and no failing test anywhere says so.
It also could not tell the two halves of a retirement apart. Dropping
block_readsandkeeping
page_readslowers the count by exactly as much as droppingpage_readsdoes,and leaves the tier published only under the word this crate does not use.
What replaces it
The filter is gone, so a one-member group is still a group, and the population is
DECLARED rather than measured:
TWINNED_ON_SHARD_STATS— the canonical names published under both spellings, withthe exact pair each one must carry.
SINGLE_ON_SHARD_STATS— the canonical names that are down to one spelling, with thespelling that survived. Empty today, and every clause runs over it, so the first
retirement adds one line and writes no new machinery.
Retiring a spelling means moving a name between those two lists. That move is the
reviewable artefact, and five clauses refuse every other way of shrinking the
population:
listed under, no name sits on both lists, and a retired name's survivor is the block
spelling;
roster, in both directions, so a pair that leaves without a roster move fails, and a
pair that arrives unnoticed fails too;
every spelling.
The same defect sat on the published contract test, which asserted that two
page-spelled keys exist by counting them. The count becomes a named set,
PAGE_SPELLED_CONTRACT_KEYS, for the same reason: a 2 can be written as a 1 withoutsaying which key left.
Three facts that were prose are now scanned for
The module header used to rest on five type-level facts, and three of its citations named
things that had already stopped existing:
PageIndexNamedByandPageEntryAthad beenrenamed to
BlockIndexNamedByandBlockEntryAt, andPAGE_SIZEandpage_ordinalwereonly ever named in order to be denied. Each of those four tokens occurred exactly ONCE in
this crate, and the occurrence was the header itself. #2386 removed that prose, which
leaves the facts unstated rather than untrue.
no_page_named_identity_type_field_or_size_constant_exists_in_this_cratescans thecrate's
srcfor the three shapes instead: a type declared with a name beginningPage,a
page_idorpage_ordinalFIELD, and aconst/static PAGE_SIZE. Each matcherrequires the line to BE a declaration, so a doc line, a serde alias and a JSON key inside
a fixture string cannot match and no path has to be excluded by hand — including this
file, which names all three shapes in its own comments.
Five non-vacuity clauses, because a scan that finds nothing looks the same as a clean
tree: the walk reaches a floor of files and recurses, each matcher is exercised on a line
it must report and on a line it must not, and the walk is required to find the Block
spelling of two of the three shapes, so a clean page-named result is a fact about the
spelling rather than about the scan. It reports 461 files scanned, 60 Block-named type
declarations and 53
block_idfields.StoragePageAddressSampleandStoragePageIndexEntrySampledo not begin withPageandare deliberately untouched: they are report projections, not identities.
What does not move
No published key, no stored key, no format stamp and no value. The three mirror pairs on
ShardCanonicalStorageStatsare exactly the three that were there before:block_index_entries/page_index_entriesat 20,block_reads/page_readsat 10 andblock_writes/page_writesat 10.The plants
Six, each against one clause, run in release and reverted:
page_readswith#[serde(skip)]block_readsas the pair that leftblock_writesfrom the twinned rosterblock_writesas the pair that arrivedblock_readsas retired while it is also twinnedpub struct PageOrdinalIdentity { page_id: u64 }andconst PAGE_SIZEinengine/lifecycle.rsAnd a positive arm:
page_readsretired ANDblock_readsmoved toSINGLE_ON_SHARD_STATSPASSES, printing
mirror block_reads: block_reads=10— a one-member group still named andstill checked. So the designed repair is a repair, and it is the only one.
Validation
🤖 Generated with Claude Code