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

[rominf]

Stacked on #491 — draft until that merges. The diff shown against main includes #491's commits; the change proper is the last commit, fix(disk-space): promote a size that rounds up to a full unit. Both PRs add the same proptest dev-dependency to rocm-core, which is why this one is stacked rather than parallel.

• 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 the other byte formatter, 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 twin.

So the guard here is a property, not another example: no rendered size may carry a mantissa of 1024 unless it is already in the largest unit. 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 (with_margin never shrinks a requirement; the extracted-size estimate never underestimates), classify_space totality, and mount selection (soundness, maximality, and irrelevance of a non-matching mount).

• cargo test -p rocm-core --lib disk_space — 28 passed, 0 failed, ~0.03s: 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.