fix(disk-space): promote a size that rounds up to a full unit

[rominf]

• If this PR fixes a bug, searched tests/e2e-cucumber/expectations.toml for the fixed ticket ID and removed/narrowed any now-stale xfail rows. — no rows reference this area.
• If this PR adds a new subcommand or subsystem, its domain implementation lives in its own file per docs/architecture.md. — N/A.
• Every new or changed user-facing message was read against the code path that runs after it, and its test asserts the resulting state — not only the wording, per AGENTS.md §3. — see "On the Gherkin requirement".

Fixes #502

Summary

format_bytes scaled while the raw value was >= 1024.0, then printed it to one decimal place. A value like 1023.95 KiB stops the loop and is then rounded up by the formatting, so 1_048_525 bytes rendered as "1024.0 KiB" instead of "1.0 MiB" — a size shown in a unit it has outgrown. The same happened at every boundary.

That string reaches users: this formatter renders the out-of-space refusal and its "Free up …" shortfall figure, so an install blocked on a nearly-full disk could quote 1024.0 KiB.

Risk: low. One pure function, no API or schema change. The loop condition now compares the value as printed rather than the raw value.

The part worth a reviewer's attention

This defect was already known and already fixed in one other byte formatter, format_bytes in apps/rocm/src/main.rs, whose test is named format_bytes_steps_up_instead_of_printing_1024_of_the_smaller_unit and whose comment reads "One byte short of the next unit used to round to 1024.0 KiB". The rocm-core copy kept the bug, because an example test sits next to one implementation and cannot see its twins. And there are more than two: format_bytes_for_user in apps/rocm has the same defect at ordinary sizes, and it is user-visible in the download: approved up to … line. mib/mib_pair in the dashboard TUI have it too, though only near a pebibyte of VRAM. Those are left to a follow-up PR that points the same two-edge property at each. This PR's own fix also reaches download progress (cli_progress.rs), not only the out-of-space message.

So the guard here is a property, not another example: a rendered size must print in its own unit — below 1024.0 unless it is already in the largest unit, and at least 1.0 once promoted (the next smaller unit having reached 1024.0). A property is attached to the contract rather than to a call site, so it holds wherever it is pointed.

The two formatters still disagree in output shape ("1023 bytes" vs "1023 B") and in their largest unit (GiB vs TiB). Unifying them touches user-facing strings on two surfaces and is deliberately not attempted here.

Test plan

Red-before/green-after verified by reverting only the loop condition: the property fails and shrinks to bytes = 1048525, the same minimal input each run. That value and the other boundaries are also pinned as explicit examples, so the specific defect stays named if the generator is ever retuned — including 1_048_524 -> "1023.9 KiB", so the promotion cannot reach down and swallow a value that genuinely belongs to the smaller unit.

Four further properties come with it, covering margin arithmetic (the margin is the larger of the floor and 5% of the size; the extracted-size estimate is the full multiplier), classify_space totality, and mount selection (soundness, irrelevance of a non-matching mount, and maximality, which compares the whole selected entry and pins that a later-listed duplicate mount wins). Each was mutation-checked against an implementation the earlier version of the property let through.

• cargo test -p rocm-core --lib disk_space — 28 passed, 0 failed, ~0.15s: no subprocess, no filesystem, no GPU
• cargo clippy --locked --workspace --all-targets -- -D warnings, cargo fmt --all --check, cargo xtask manifest --check, cargo xtask tpn --check — all exit 0

A caveat recorded in the code, because it is easy to get wrong

The first version of the central property passed against a defect that was definitely present. A uniform u64 generator essentially never lands near a unit boundary — almost every draw is in the exabyte range — so it never sampled the only region where the scaling loop can go wrong. The sampling window has to scale with the boundary, because the band where rounding bites is itself proportional. That reasoning is in the generator's doc comment rather than only in this description, since the next person to touch it needs it.

The reference the properties measure against is also kept derived from the contract rather than restated from the implementation, for the same reason.

On the Gherkin requirement

No scenario is added. Reaching this string end-to-end requires a genuinely nearly-full filesystem; a scenario would have to fake one, which tests the fake rather than the behaviour. The formatter is covered at the unit level, where it is a pure function.

[rominf]

#491 has merged, so this is now rebased onto main (ce7d0269) and contains only its own change: one commit, 2967156b. The earlier stray const on the non-unix mount_owns_path stub, and the commit reverting it, are folded away, so the stub is untouched. Verified locally: disk_space tests (28), xtask (255), e2e-cucumber --lib (130), feature_naming, and clippy -D warnings for both --all-targets and --test e2e.

[volen-silo]

I went through this one carefully, since the production change is a single line and the tests are the rest of the diff.

The fix itself is right. I reproduced the old and new format_bytes and scanned roughly 180 million inputs - every integer around each 1024^k boundary, the whole band below 2^40 where the GiB mantissa exceeds 1023.9, plus the extremes - and found no input that still renders a 1024.0 mantissa in a non-final unit. Two traps I went looking for specifically are not there: the (value * 10.0).round() promotion test never disagrees with what {:.1} actually prints (I compared them at every loop step, not just the final one), and the repeated /= 1024.0 accumulates nothing, because dividing by a power of two is exact and the loop never approaches subnormals. Four of the five new pinned examples genuinely fail against the old code. 1_048_524 -> "1023.9 KiB" passes either way, which is fine - it is a guard rather than a regression test. It is also the only thing in the PR holding the lower edge, which brings me to the main point.

What I would want changed is in the tests, which is where most of this PR lives.

The central property is one-sided. It says a non-TiB mantissa must be below 1024.0, and says nothing about the other direction, so an implementation that promotes far too early satisfies it completely. I checked with a deliberately broken version that promotes at half a unit: it renders 0.6 KiB, 0.7 MiB, 0.9 GiB, and the property raises nothing across every input I threw at it. The contract being described has two edges and only one of them is written down - the other is held by a single example, which is precisely the arrangement this PR argues against.

Two of the four supporting properties cannot fail. with_margin ends in saturating_add of a u64, so >= bytes is true by construction, including if the margin formula were deleted and the margin were always zero. estimated_extracted_size is saturating_mul, so >= archive is true for any multiplier of 1 or more, including a regression to 1 that removes the inflation the function exists for. Both already have example tests that pin more than the properties do. As written they read as contracts on the margin arithmetic but do not constrain it.

The generator's exponent-1 arm is dead. 1024 / 16384 floors to zero, so that window is exactly {1024, 1025}, and neither value can exhibit the defect anyway: at unit 0 the function prints the raw integer and never reaches {:.1}, so there is no rounding band at the B/KiB transition at all. That is around an eighth of the case budget spent on two values that were never at risk, and the doc comment's claim that the scaling keeps the band a large fraction of every window is not true for that one. It holds well for exponents 2 through 4, which is where the work actually happens.

Last, a correction to the framing rather than to the code. The description says the defect was already fixed in "the other" byte formatter, treating this as a two-way duplication. It is wider. format_bytes_for_user in apps/rocm has the identical defect at ordinary sizes and its output reaches users; mib/mib_pair in the dashboard TUI have it too, though only near a pebibyte of VRAM, so that one is theoretical. Declining to fix them here is reasonable and the scoping argument is fine. But the stated premise is that a property beats an example because it attaches to the contract and holds wherever it is pointed - and it is currently pointed at one implementation, while the one with live user-visible breakage is untouched and unmentioned.

A few concerns that did not hold up, for completeness: u64::MAX renders as 16777216.0 TiB and the top of the ladder behaves sensibly with nothing left to promote to; committing the proptest regression file matches what this crate already does for runtime.txt; proptest really is in [dev-dependencies], so the Cargo.toml comment is accurate; and no test, snapshot or e2e expectation anywhere pins a rendered size string, so the behaviour change breaks nothing downstream. The suite runs in 0.03s as claimed.

[volen-silo]

This is only the upper edge of the contract. Nothing here says a promoted value must print as at least 1.0, so an implementation that promotes far too eagerly passes untouched - I tried one that promotes at half a unit and it renders 0.6 KiB, 0.7 MiB, 0.9 GiB without tripping this assertion on any input.

The lower edge is currently held only by the single 1_048_524 example above, which is the example-shaped guard this PR sets out to replace. Asserting (value * 10.0).round() >= 10.0 for any unit above B would close it, and would turn that example into a genuine duplicate rather than the only thing standing there.

[rominf]

Fixed in d6f65af1. The property, now format_bytes_renders_a_size_in_its_own_unit, asserts both edges. Above B, the printed tenths must be at least 10. Stricter than that, the next smaller unit must have printed at least 1024.0, because the at-least-1.0 bound alone still passes a loop that promotes at 1023.9. A new generator arm draws uniformly within each unit's range, so the early side actually gets sampled. Mutation-checked: your half-unit promoter fails it now, so does a 1023.9 promoter, and the old >= 1024.0 loop still fails the upper edge.

[volen-silo]

with_margin ends in bytes.saturating_add(margin) with margin: u64, so this assertion is true by construction. It would still pass if the proportional/floor selection were deleted and the margin were always zero - which is the part of the function the doc comment is describing.

The only regression it can catch is saturating_add becoming +, and with_margin_saturates already pins that. Something like with_margin(bytes) - bytes >= SPACE_MARGIN_MIN_BYTES for non-saturating inputs would actually constrain the formula.

[rominf]

Agreed, it was true by construction. Replaced in d6f65af1 with with_margin_adds_the_floor_or_the_proportional_part: for non-saturating inputs, the margin is at least the floor, at least bytes/20, and no more than the larger of the two. One generator arm straddles the crossover point. Saturation stays with with_margin_saturates. A zero margin, floor-only, and floor-plus-proportional each fail it.

[volen-silo]

Same shape: saturating_mul by a constant of 1 or more satisfies this for every input, so a regression that drops EXTRACTED_SIZE_MULTIPLIER to 1 - removing the conservatism this function exists for - sails straight through. Only a multiplier of 0 would fail it, and extracted_size_uses_conservative_multiplier is the only thing pinning the actual value.

archive > 0 implying estimated_extracted_size(archive) > archive would at least rule out the identity case.

[rominf]

Replaced in d6f65af1 with extracted_size_inflates_every_archive: over 1..=u64::MAX / EXTRACTED_SIZE_MULTIPLIER it asserts estimate > archive and estimate == archive * EXTRACTED_SIZE_MULTIPLIER. A multiplier of 1 now fails it, and so does saturating_add in place of saturating_mul.

[volen-silo]

1024 / 16384 floors to zero, so for exponent == 1 this window is exactly 1024..=1025. Two values, and neither can exhibit the defect: at unit 0 format_bytes prints {bytes} B and never reaches {:.1}, so there is no rounding band at the B/KiB transition to sample. With the arms equally weighted that is roughly an eighth of the default 256 cases spent on two values that were never at risk.

Starting the range at 2 recovers them. The other windows are good - I make them 66, 65538 and 67108866 values at exponents 2, 3 and 4, with 77 to 80 percent of each inside the band that actually rounds up. Worth tightening the doc comment above too, since it currently claims the scaling keeps the band a large fraction of every window.

[rominf]

Right, that window was {1024, 1025}, and the B unit never reaches {:.1}. In d6f65af1 the windows start at exponent 2, and the doc comment explains why there is no band at the KiB edge. It now claims about three quarters per window instead of every window.

[volen-silo]

The doc comment says the small alphabet makes prefixes collide often enough to exercise mount selection. Measured over the generated distribution that is only partly true: about a third of draws produce any match at all, and most of those match only because this strategy can emit the bare root, which prefixes everything. Draws with two competing mounts at depth two or more - the only case where maximality actually has to choose between candidates - come out at roughly two cases in a default 256-case run.

The properties are sound, they just rarely get to do any work. Deriving mounts as prefixes of the drawn path, rather than drawing them independently from the same alphabet, would give them something to discriminate. Related: selected_mount_is_the_deepest_match compares components().count() rather than the selected mount itself, so when two generated mounts tie on depth (which happens often with this alphabet) a change in tie-breaking would not be caught.

[rominf]

Reworked in d6f65af1. Mounts are now drawn mostly from the path's own ancestors, with repeats so that depths compete and a mount point can be listed twice, plus a few independent ones, shuffled. selected_mount_is_the_deepest_listed_ancestor compares the whole selected (mount, bytes) entry against a reference built differently: walk the path's ancestors and look each one up. Two distinct mount points of equal depth can't both contain one path, so the only possible tie is a duplicate listing. The property pins that the later entry wins, which is what the code already did and matches mount semantics, where a later mount hides an earlier one. A first-listed-wins mutant now fails; the old suite let it through. The irrelevance property also stopped rejecting a quarter of its cases, which had exhausted proptest's reject budget at 20000 cases.

[volen-silo]

Not about this line - anchoring here because the files involved are outside the diff.

The description treats this as a two-way duplication with apps/rocm's format_bytes, but the same defect is live in at least two more places:

• format_bytes_for_user at apps/rocm/src/main.rs:19013 renders 1_048_575 as "1024.0 KB" and 1_073_741_823 as "1024.0 MB", and its output reaches users in the download: approved up to ... line at apps/rocm/src/main.rs:18878. Those are ordinary download-limit sizes, not exotic ones.
• mib and mib_pair at crates/rocm-dash-tui/src/ui/format.rs:49 and :61 have the same pattern, but it only bites around a pebibyte of VRAM, so that one is theoretical.

Fixing them here is a fair thing to decline. But the argument for a property over an example is that it attaches to the contract and holds wherever it is pointed, and right now it is pointed at one implementation while the one with live user-visible breakage is untouched and unmentioned.

[rominf]

Confirmed. format_bytes_for_user renders 1048525 to 1048575 as 1024.0 KB and 1073741772 to 1073741823 as 1024.0 MB, and that reaches the download: approved up to … line. mib/mib_pair hit the same band only near 1 PiB of VRAM. There's also one more reach of this fix itself: rocm_core::format_bytes renders download progress too (cli_progress.rs). I'll fix the other formatters in a follow-up PR, pointing the same two-edge property at each, and I've corrected the description here.

[rominf]

Follow-up is #556. Two corrections to my reply above, found while fixing it:

• The MB band of format_bytes_for_user starts at 1,073,689,396 bytes, not 1,073,741,772. Everything from there to 1,073,741,823 printed "1024.0 MB", so the band was wider than I said.
• mib takes MiB, so its affected band is just under 1 TiB of VRAM, not 1 PiB. Still theoretical for today's hardware, but closer than I stated.

Dismissed as stale: this review is of 2967156. All six findings are addressed in d6f65af, with a reply in each thread: two-sided format property, margin and extraction properties that pin the formulas, the dead KiB window removed, and mount selection drawing competing ancestors and comparing the selected entry. Each new property is mutation-checked against an implementation the old one let through. The other formatters are a planned follow-up PR. Please re-review the current head.

[volen-silo]

I re-reviewed this on d6f65af1. Rather than read the new assertions, I built each mutant the last round named and ran it. All five substantive points are closed.

The two-edge format property. The half-unit promoter I described now fails it, and so does a 1023.9 promoter. The plain "at least 1.0" bound on its own would not have caught the second one, so stating the lower edge exactly was the right call. The original >= 1024.0 loop still fails the upper edge. I also checked that the exact lower bound is true of the implementation and not merely of the values drawn: scanning about 41 million inputs (every integer below 2^22, wide windows either side of each 1024^k, the rounding bands, several million uniform u64 draws, and the extremes) produced no failure. Reverting only the loop condition still shrinks to bytes = 1048525, the same input on all eight runs I tried, so the retuned generator did not cost the red-before.

The two properties that were true by construction. Deleting the margin selection so the margin is always zero now fails with_margin_adds_the_floor_or_the_proportional_part, and so do floor-only and proportional-only variants. Regressing the multiplier to 1 now fails extracted_size_inflates_every_archive, as does saturating_add in place of saturating_mul. On the previous head all three of those mutants passed their own property: the margin one was caught only by with_margin_saturates, and the multiplier one by nothing at all. So this is a real change in what the suite detects, not a change of wording.

The generators. I measured the distributions instead of redoing the arithmetic. Over 200k draws the byte generator now puts nothing in the dead {1024, 1025} window, 26% of draws land in the band where the old and fixed loops disagree, and 40% of non-B draws carry a mantissa below half a unit, which is what gives the lower edge something to bite on. The mount generator went from matching about a third of the time to 80%. Draws with two or more distinct matching mounts at depth 2 or more went from roughly 2 per 256-case run to about 91, and the duplicate listing that the tie-break rule is about turns up in 28% of draws. A first-listed-wins tie-break now fails selected_mount_is_the_deepest_listed_ancestor; the previous suite passed it clean. Regressing path_starts_with to a text prefix also fails every run now, so the data/database pairing in the alphabet is doing the work its comment claims. The irrelevance property, which used to abort with "Too many global rejects" at 20k cases, runs 200k clean.

The description. It now names the other formatters, says where their output reaches users, and commits to the follow-up. That was the whole of the objection; declining to fix them here was always fair.

I also swept for anything this commit might have introduced. No flakiness: 30 runs on fresh seeds plus runs at 20k and 200k cases, all green. cargo fmt and cargo clippy -D warnings are clean. Both new input bounds are safe rather than merely lucky: u64::MAX / 2 leaves the margin addition far short of saturating, and u64::MAX / EXTRACTED_SIZE_MULTIPLIER is the exact largest value whose product still fits the assertion. The exact-equality reference in the maximality property cannot disagree with the prefix match for anything this generator produces, and comparing the whole entry instead of only the depth is a strict gain. Nothing in the repo still refers to the old property names.

One thing is left, and it is a wording fix in a comment rather than a defect in a test. I have put it inline. It is marked as changes requested because that is the honest shape of a review that still has something open, not because it should hold up the merge.

Separately, and not worth changing on its own: the byte generator's comment gives the uniform arm as [1024^k, 1024^(k+1)), but the k = 0 arm starts at 0 rather than 1. Including zero is better than the formula, so the code is right and the formula is just narrower than what it describes.

[volen-silo]

Measured over the generated distribution, this holds for about four fifths of the rewritten draws but not all of them. When the drawn extra happens to equal path exactly, extra.join("elsewhere") is a child of path itself, and path has no ancestor one component deeper for that to be a sibling of.

Over 200k draws, 23% get rewritten, so "roughly a quarter" is accurate. Of those, about 21% (close to 5% of all draws) land as a child of the path rather than as a sibling of an ancestor.

The assertion is unaffected either way: !contains(&extra) holds in both cases and the test does what its name says. It is the description of the shape that is slightly off. Since this PR argues that generator comments are part of the specification, something like "a child of one of the path's ancestors that the path itself does not pass through" would cover both cases.

[rominf]

Fixed in 56d96db. The doc now says the rewritten mount is "a child of one of the path's ancestors (or of the path itself) that the path does not pass through", which covers both cases you measured. The same commit fixes the byte generator's comment: the B range starts at 0 rather than at 1024^0, so zero is drawn too. Both are comment-only changes.

[volen-silo]

Re-reviewed at 56d96dbc. The one item left open from my last pass is closed, and I checked that this commit did not loosen anything while editing next to it.

The mount generator's doc comment. The new wording — "a child of one of the path's ancestors (or of the path itself) that the path does not pass through" — is exhaustively true, not merely less wrong. Over 200k draws of (path_and_mounts_strategy(), mount_point_strategy()): 23.0% of draws get rewritten, so "roughly a quarter" is right; of those, 79.0% land as a child of a strict ancestor and 21.0% as a child of the path itself (4.8% of all draws, matching what I measured before). Nothing fell outside those two shapes, and nothing rewritten still contained the path, so the prop_assert! guard never has to catch anything.

The byte generator's B arm. Also correct: low is 0 at exponent 0, and zero really is drawn — 21 times in 200k draws, about 1 in 10k.

Mutants re-run at the new head. I moved the checked-in proptest-regressions seed aside first, since it replays before any novel case and would otherwise do the catching on the generator's behalf. With it gone, each one is still caught by generation alone, three runs each on fresh seeds:

• promoting at half a unit → format_bytes_renders_a_size_in_its_own_unit fails on 512 -> 0.5 KiB
• margin selection deleted, margin always zero → with_margin_adds_the_floor_or_the_proportional_part fails on 0
• EXTRACTED_SIZE_MULTIPLIER back to 1 → extracted_size_inflates_every_archive fails on 1

The original defect too: the plain value >= 1024.0 loop fails on 1048525 within 0 to 11 draws across five runs with no stored seed. So the seed file is belt and braces rather than load bearing, which is the right way round.

Suite stability. Ten runs at PROPTEST_CASES=4096 on fresh seeds, with both the global and local reject budgets forced down to 1: 28 passed every time, zero rejections anywhere. The rejection pressure the earlier version had is gone, not just raised above the budget. cargo fmt --check and cargo clippy --all-targets are clean, and the full rocm-core lib suite is 469 passed.

One thing to take or leave, in the same bullet this commit edited: "so a loop that promotes too early is caught on most draws". Measured against the half-unit promoter over 15 runs, the median is 3 draws to catch and the worst was 24 — reliable, but that works out to roughly one draw in six across the whole strategy, and about half within that arm's own range. "within a handful of draws" would match what it does. Not worth a round on its own.

Good call sending the other formatters out separately in #556 rather than folding them in here.

Nothing blocking left from my side. This looks safe to approve after the usual final validation — a maintainer's own pass and green CI. This comment is not itself an approval, and reading the code and running the tests locally does not stand in for either.

[volen-silo]

Approving. The earlier comment on this PR already covered the detail; this is the formal sign-off.

Everything raised across the two previous rounds is closed. The three properties that could not fail under their own named mutants now do: a half-unit promoter fails the rendering property, deleting the margin selection fails the margin property, and resetting the multiplier to 1 fails the archive-size property. I confirmed those by running the mutants with the checked-in regression seeds moved aside, so the properties are caught by generation rather than by a stored seed. The generator gaps are gone too, and the suite holds across repeated fresh seeds with no reject-budget pressure.

One thing to be clear about: this reflects what reading the diff and running the tests locally can show. It is not a statement about CI. Three self-hosted lanes were still pending when I approved, and the usual caveat applies that a local run is not the same as the full matrix.

The one remaining remark is wording in a doc comment, noted earlier and not worth another round.

[rominf]

Force-pushed (now 0333b610). Two changes to 56d96dbc, which this replaces:

• the byte generator's comment now says an early promoter is caught on about half of that arm's draws, within a handful across the whole strategy, as you measured, instead of "on most draws"
• the commit message drops a co-author trailer that does not belong in this repo's history

Both are a comment and a message only; no test or code changed. This makes the approval on 56d96dbc stale, sorry for the churn.

[volen-silo]

I re-checked this after the force-push, since my earlier approval is anchored to 56d96dbc, which is no longer in the branch.

What actually changed. The delta from that commit is one hunk in crates/rocm-core/src/disk_space.rs, and every changed line is a doc comment. No code, test, or fixture line moved. The compare view shows more than that because it diffs against the shared parent; the net change from the commit I read last time is just the one sentence about the too-early promoter. The mount-generator rewording and the "B range starts at 0" clause were both already in the commit I read.

The reworded claims, measured rather than read, since the previous wording turned out to be measurably wrong.

The mount-generator sentence holds exactly. Over 200,000 draws the rewrite fired on 23.15% of them, so "roughly a quarter" is right, and in every one of those 46,295 cases the rewritten mount was a child of one of the path's ancestors and the path did not pass through it. The "(or of the path itself)" parenthetical earns its place: the drawn mount was the path itself in 20.9% of the rewrites, so without it the sentence would be wrong one time in five.

"Within a handful of draws across the whole strategy" holds too. The whole strategy catches a half-unit promoter on 20.0% of draws, a mean of 5.0 draws to a catch.

The one claim that does not quite hold is "about half of this arm's draws", which measures 40.07%. I left the detail inline. It is not a merge blocker and it does not touch behaviour; I am filing it as a change request only because that is how I file anything that survives a re-read, not because I think it should hold the PR.

Nothing loosened. I re-ran the three mutants with the checked-in regression seeds moved aside, so each had to be caught by generation rather than by a stored seed. The half-unit promoter fails the rendering property, deleting the margin selection fails the margin property, and resetting the extraction multiplier to 1 fails the archive-size property. Ten runs at 4096 cases on fresh seeds with the reject budget set to 1 all passed, with no rejections and no new seeds written. cargo fmt and clippy are clean.

[volen-silo]

Measured over 200,000 draws from this arm: the promoter is caught on 40.07% of them, not about half.

The premise is right. 49.93% of the draws land below half of the next unit. But the conclusion does not carry to the top of the arm. The exponent runs 0..=4, so one fifth of the draws land in [1024^4, 1024^5), and there the loop is already at TiB and unit + 1 < UNITS.len() stops it. A promoter that fires at half a unit produces byte-for-byte the same output as the real one for every value in that range, so the property has nothing to see. Measured: 0 catches in 39,558 draws at exponent 4, against 49.7% to 50.3% at exponents 0 through 3.

So the arm catches it on two fifths of its draws rather than a half. The second half of the sentence is unaffected: the whole strategy measures 20.0%, a mean of 5.0 draws to a catch, which is the handful you describe.

Something like:

    /// * Uniform within one unit's range, `[1024^k, 1024^(k+1))`, except
    ///   that the `B` range starts at 0 so zero is drawn too. About half
    ///   of each range lies below half of the next unit, so a loop that
    ///   promotes too early is caught on about half of the draws in every
    ///   range but the largest, where there is nothing left to promote to
    ///   — two fifths of this arm's draws, which is within a handful of
    ///   draws across the whole strategy.

[rominf]

Thanks for measuring it. You are right that the top range has nothing left to promote to, so the arm catches the early promoter on two fifths of its draws, not half. This PR is in the merge queue on your approval. I will land your wording in a small follow-up rather than reset the approval again.

[rominf]

Your wording is now in #574, as a follow-up since this PR merged.

Superseded by an approval at the same head. The inline note about the 'about half of this arm's draws' sentence stands as a suggestion, not a request for changes.

[volen-silo]

Re-approving at the current head, re-anchoring the approval I left on the pre-force-push commit.

I checked what the force-push actually changed rather than assuming: one hunk, one file, two lines, all inside a doc comment. No code, test, or fixture line moved, so everything the earlier approval rested on still holds. I re-confirmed it at this head anyway — with the checked-in regression seeds moved aside, a half-unit promoter still fails the rendering property, deleting the margin selection still fails the margin property, and resetting the multiplier to 1 still fails the archive-size property. Ten runs at 4096 cases on fresh seeds with the reject limits set to 1 passed with no rejections.

The one note I left inline stands as a suggestion rather than a request. The sentence says a too-early promoter is caught on about half of that arm's draws; measured over 200k draws it is 40%, and the gap is structural rather than noise. The arm's exponent runs 0 through 4, and draws in the top range land where the loop has already reached TiB and stops, so a half-unit promoter is identical to the real function there and the property cannot tell them apart. Worth tightening when you next touch that comment; not worth another round on its own.

As before: this reflects reading the diff and running the tests locally. It is not a statement about CI, and several self-hosted lanes were still pending when I approved.