diff --git a/crates/rocm-core/Cargo.toml b/crates/rocm-core/Cargo.toml index bfc8b391c..9b4b22d7e 100644 --- a/crates/rocm-core/Cargo.toml +++ b/crates/rocm-core/Cargo.toml @@ -34,6 +34,10 @@ ureq = { version = "2.12", features = ["native-certs"] } # spelling of that path, which is exactly the shape an example test misses: the # pre-existing example used `/etc/rocm-cli-test-runtime`, the one shape that # happened to work, while `/etc/` and `$HOME/../../etc` sailed through. +# +# Also used by `disk_space`, for the same reason: its unit formatting, margin +# arithmetic and mount selection are small total functions whose contracts are +# easy to state over ALL inputs and awkward to cover with examples. # Test-only, so it adds nothing to any shipped binary. proptest = { version = "1", default-features = false, features = ["std"] } diff --git a/crates/rocm-core/proptest-regressions/disk_space.txt b/crates/rocm-core/proptest-regressions/disk_space.txt new file mode 100644 index 000000000..f163805b7 --- /dev/null +++ b/crates/rocm-core/proptest-regressions/disk_space.txt @@ -0,0 +1,7 @@ +# Seeds for failure cases proptest has generated in the past. It is +# automatically read and these particular cases re-run before any +# novel cases are generated. +# +# It is recommended to check this file in to source control so that +# everyone who runs the test benefits from these saved cases. +cc 34d870941d50bdb12476decbb70a4e6630d4f741faaae77e30d6293a98fdac9a # shrinks to bytes = 1048525 diff --git a/crates/rocm-core/src/disk_space.rs b/crates/rocm-core/src/disk_space.rs index da5dc36fc..5f43b1bbc 100644 --- a/crates/rocm-core/src/disk_space.rs +++ b/crates/rocm-core/src/disk_space.rs @@ -286,7 +286,12 @@ pub fn format_bytes(bytes: u64) -> String { const UNITS: [&str; 5] = ["B", "KiB", "MiB", "GiB", "TiB"]; let mut value = bytes as f64; let mut unit = 0; - while value >= 1024.0 && unit + 1 < UNITS.len() { + // Promote while the value AS PRINTED would reach 1024, not merely while the + // raw value does. 1_048_525 divides to 1023.95…, which stops a `>= 1024.0` + // loop one unit early and then renders as "1024.0 KiB" once `:.1` rounds it + // — a size shown in a unit it has outgrown, in the user-facing out-of-space + // message. Comparing the rounded tenths closes that gap at every boundary. + while unit + 1 < UNITS.len() && (value * 10.0).round() >= 10_240.0 { value /= 1024.0; unit += 1; } @@ -423,6 +428,23 @@ mod tests { assert_eq!(format_bytes(3 * 1024 * 1024 * 1024), "3.0 GiB"); } + /// Just below a unit boundary the value rounds up to a full 1024 of the + /// SMALLER unit, which has to be reported as 1.0 of the larger one. These + /// are the minimal failing inputs + /// [`format_bytes_renders_a_size_in_its_own_unit`] shrank to; they are + /// pinned as examples too so the specific defect stays named even if the + /// generator is retuned. The last one names the property's lower edge. + #[test] + fn format_bytes_promotes_a_value_that_rounds_up_to_a_full_unit() { + assert_eq!(format_bytes(1_048_525), "1.0 MiB"); + assert_eq!(format_bytes(1_048_575), "1.0 MiB"); + assert_eq!(format_bytes(1_073_741_823), "1.0 GiB"); + assert_eq!(format_bytes(1_099_511_627_775), "1.0 TiB"); + // The value just below the rounding band still belongs to the smaller + // unit — promotion must not reach down and swallow it. + assert_eq!(format_bytes(1_048_524), "1023.9 KiB"); + } + #[test] fn extracted_size_uses_conservative_multiplier() { assert_eq!(estimated_extracted_size(1_000), 4_000); @@ -489,6 +511,320 @@ mod tests { assert_ne!(cache, other); } + // ── Properties ───────────────────────────────────────────────── + // + // The examples above pin the values somebody thought to write down. These + // state the contracts that must hold for EVERY input, and let proptest look + // for the inputs that break them. All pure and in-process: no subprocess, + // no filesystem, no GPU — the whole module runs in milliseconds as part of + // the ordinary unit-test lane. + + /// Split a rendered size into its numeric part and its unit. + fn split_rendered(rendered: &str) -> (f64, String) { + let mut parts = rendered.split_whitespace(); + let value = parts + .next() + .expect("rendered size has a numeric part") + .parse() + .expect("numeric part parses"); + let unit = parts.next().expect("rendered size has a unit").to_owned(); + (value, unit) + } + + proptest::proptest! { + /// A size is rendered in the unit it belongs to, which has two edges. + /// + /// Upper: never a unit it has outgrown. `1024.0 KiB` means the scaling + /// loop stopped one unit too early: it exits while the value is below + /// 1024, but the `:.1` rounding can then push the printed mantissa back + /// up to 1024.0. Only the largest unit may carry a mantissa that big, + /// because there is nothing to promote it to. + /// + /// Lower: never a unit it has not reached. A loop that promotes too + /// eagerly renders `0.6 KiB` for 600 bytes; every unit above `B` is + /// only entered by promotion, so its printed mantissa is at least 1.0. + /// That alone still lets a loop promote slightly early — `1023.9 KiB` + /// as `1.0 MiB` — so the lower edge is stated exactly: the next + /// smaller unit would have printed 1024.0 or more. + /// + /// Every edge compares the mantissa as printed, in tenths, which is the + /// same quantity the scaling loop decides on. + #[test] + fn format_bytes_renders_a_size_in_its_own_unit(bytes in byte_count_strategy()) { + const UNITS: [&str; 5] = ["B", "KiB", "MiB", "GiB", "TiB"]; + let rendered = format_bytes(bytes); + let (value, unit) = split_rendered(&rendered); + let tenths = (value * 10.0).round(); + let exponent = UNITS + .iter() + .position(|name| *name == unit) + .expect("rendered unit is one of the known units"); + if exponent + 1 < UNITS.len() { + proptest::prop_assert!( + tenths < 10_240.0, + "{bytes} rendered as {rendered}, which should have been \ + promoted to the next unit", + ); + } + if exponent > 0 { + proptest::prop_assert!( + tenths >= 10.0, + "{bytes} rendered as {rendered}, which was promoted before \ + it reached a whole unit", + ); + // Dividing by a power of two is exact, so this is the value the + // smaller unit would have printed, not an approximation of it. + let smaller = (1..exponent).fold(bytes as f64, |value, _| value / 1024.0); + proptest::prop_assert!( + (smaller * 10.0).round() >= 10_240.0, + "{bytes} rendered as {rendered}, but still fits the smaller \ + unit as {smaller:.1} {}", + UNITS[exponent - 1], + ); + } + } + + /// The margin is the larger of the floor and the proportional part — + /// no less, or a nearly-full disk lets an install start that cannot + /// finish; and no more, or a small download is refused on a disk with + /// ample room for it. Inputs stay below the point where the addition + /// saturates, which `with_margin_saturates` covers. + #[test] + fn with_margin_adds_the_floor_or_the_proportional_part( + bytes in margin_input_strategy(), + ) { + let margin = with_margin(bytes) - bytes; + let proportional = bytes / SPACE_MARGIN_DIVISOR; + proptest::prop_assert!( + margin >= SPACE_MARGIN_MIN_BYTES, + "{bytes} got a margin of {margin}, below the floor", + ); + proptest::prop_assert!( + margin >= proportional, + "{bytes} got a margin of {margin}, below its proportional part \ + {proportional}", + ); + proptest::prop_assert!( + margin <= SPACE_MARGIN_MIN_BYTES.max(proportional), + "{bytes} got a margin of {margin}, more than the larger of the \ + floor and {proportional}", + ); + } + + /// The extracted-size estimate is deliberately conservative: it + /// inflates every non-empty archive by the full multiplier, so it can + /// never collapse to the archive size itself. Inputs stay below the + /// point where the multiplication saturates, which + /// `extracted_size_uses_conservative_multiplier` covers. + #[test] + fn extracted_size_inflates_every_archive( + archive in 1..=u64::MAX / EXTRACTED_SIZE_MULTIPLIER, + ) { + let estimate = estimated_extracted_size(archive); + proptest::prop_assert!( + estimate > archive, + "{archive} was estimated at {estimate}, no larger than itself", + ); + proptest::prop_assert_eq!(estimate, archive * EXTRACTED_SIZE_MULTIPLIER); + } + + /// `classify_space` is a total decision with no third reading: with a + /// known figure it says Sufficient exactly when the space is there. + #[test] + fn classify_space_agrees_with_the_comparison(required: u64, available: u64) { + let check = classify_space(required, Some(available)); + proptest::prop_assert_eq!( + matches!(check, SpaceCheck::Sufficient { .. }), + available >= required, + ); + proptest::prop_assert_eq!(check.is_insufficient(), available < required); + } + + /// Soundness: a mount is only ever selected for a path it actually + /// contains. Picking a mount that is not a prefix would report an + /// unrelated filesystem's free space. + #[test] + fn selected_mount_is_always_a_prefix_of_the_path( + (path, mounts) in path_and_mounts_strategy(), + ) { + if let Some((selected, _)) = select_mount(&path, &mounts) { + proptest::prop_assert!( + path_starts_with( + &strip_verbatim_prefix(&path), + &strip_verbatim_prefix(&selected), + ), + "selected {} for {}", selected.display(), path.display(), + ); + } + } + + /// Maximality: the documented rule is longest-prefix-wins, so the + /// selected entry is the one for the deepest of the path's own + /// ancestors that is listed. A shallower pick would quote the + /// enclosing filesystem instead of the real one. + /// + /// Two distinct mount points of equal depth cannot both contain the + /// same path, so the only tie is one mount point listed twice. Then the + /// later entry wins: the platform lists mounts in mount order + /// (`/proc/mounts` on Linux), and a later mount on the same point + /// shadows the earlier one. + /// + /// The reference is built differently from `select_mount` — walking + /// the path's ancestors and looking each one up — so it does not just + /// restate the implementation, and it compares the whole selected + /// entry rather than only its depth. + #[test] + fn selected_mount_is_the_deepest_listed_ancestor( + (path, mounts) in path_and_mounts_strategy(), + ) { + let expected = path.ancestors().find_map(|ancestor| { + mounts + .iter() + .rev() + .find(|(mount, _)| mount.as_path() == ancestor) + .cloned() + }); + proptest::prop_assert_eq!(select_mount(&path, &mounts), expected); + } + + /// Irrelevance: a mount that does not contain the path must not change + /// the answer. This is what keeps an unrelated entry appearing in the + /// platform's mount list from perturbing the result. + /// + /// A drawn mount that does contain the path is pushed one component + /// below it instead of being discarded, which turns it into a near + /// miss — a child of one of the path's ancestors (or of the path + /// itself) that the path does not pass through — rather than + /// rejecting roughly a quarter of all cases. + #[test] + fn a_non_matching_mount_does_not_change_the_result( + (path, mounts) in path_and_mounts_strategy(), + extra in mount_point_strategy(), + extra_bytes: u64, + ) { + let contains = |mount: &Path| { + path_starts_with(&strip_verbatim_prefix(&path), &strip_verbatim_prefix(mount)) + }; + // `elsewhere` is outside the path alphabet, so this never matches. + let extra = if contains(&extra) { extra.join("elsewhere") } else { extra }; + proptest::prop_assert!(!contains(&extra), "{} contains the path", extra.display()); + let before = select_mount(&path, &mounts); + let mut widened = mounts; + widened.push((extra, extra_bytes)); + proptest::prop_assert_eq!(select_mount(&path, &widened), before); + } + } + + /// Byte counts that actually visit the interesting regions. + /// + /// A uniform `u64` is useless on its own: almost every value drawn sits in + /// the exabyte range, so the unit-boundary behaviour — the only place the + /// scaling loop can go wrong — is never sampled. The naive version of this + /// generator passed against a defect that was definitely present. + /// + /// So two more arms aim at the two edges of the contract: + /// + /// * 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 this arm's draws, + /// which is within a handful of draws across the whole strategy. + /// * A window just below each `1024^k` boundary. The window has to SCALE + /// with the boundary, because the band where `:.1` rounding pushes the + /// mantissa up to 1024.0 is itself proportional: it spans the top + /// `boundary / 20480` or so. A fixed-width window finds the defect at + /// the MiB boundary and misses it at TiB. `/ 16384` keeps that band + /// around three quarters of each window. The windows start at the MiB + /// boundary: at the KiB boundary `format_bytes` still prints a whole + /// number of bytes and never reaches `:.1`, so there is no band to find, + /// and the window there would hold only two values anyway. + /// + /// The generator is part of the specification; a careless one buys nothing + /// but false confidence. + fn byte_count_strategy() -> impl proptest::strategy::Strategy { + use proptest::prelude::*; + prop_oneof![ + any::(), + (0u32..=4).prop_flat_map(|exponent| { + let low = if exponent == 0 { + 0 + } else { + 1024u64.pow(exponent) + }; + low..1024u64.pow(exponent + 1) + }), + (2u32..=4).prop_flat_map(|exponent| { + let boundary = 1024u64.pow(exponent); + (boundary - boundary / 16384)..=(boundary + 1) + }), + ] + } + + /// Payload sizes for the margin property. The first arm straddles the + /// point where the proportional part overtakes the floor + /// (`SPACE_MARGIN_MIN_BYTES * SPACE_MARGIN_DIVISOR`), which a uniform draw + /// essentially never reaches; the second covers the rest of the range up + /// to `u64::MAX / 2`, where even a 5% margin cannot saturate. + fn margin_input_strategy() -> impl proptest::strategy::Strategy { + use proptest::prelude::*; + prop_oneof![ + 0..=SPACE_MARGIN_MIN_BYTES * SPACE_MARGIN_DIVISOR * 2, + 0..=u64::MAX / 2, + ] + } + + /// Absolute paths built from a small component alphabet, so independently + /// drawn paths still collide now and then. `database` sits beside `data` + /// so a text-prefix comparison would be caught. + fn path_strategy() -> impl proptest::strategy::Strategy { + use proptest::prelude::*; + proptest::collection::vec( + proptest::sample::select(vec!["home", "user", "data", "mnt", "var", "database"]), + 0..5, + ) + .prop_map(|components| { + let mut path = PathBuf::from(std::path::MAIN_SEPARATOR_STR); + for component in components { + path.push(component); + } + path + }) + .boxed() + } + + fn mount_point_strategy() -> impl proptest::strategy::Strategy { + path_strategy() + } + + /// A path together with a mount table to select it from. + /// + /// Independently drawn mounts rarely compete for the same path: most + /// tables would hold no match, or only the bare root. So most entries are + /// drawn from the path's own ancestors — with repeats, so candidates of + /// different depth compete and one mount point can be listed twice — and + /// the rest are independent paths that mostly do not match. The table is + /// shuffled so a match can sit anywhere in it. + fn path_and_mounts_strategy() + -> impl proptest::strategy::Strategy)> { + use proptest::prelude::*; + path_strategy().prop_flat_map(|path| { + let ancestors: Vec = path.ancestors().map(Path::to_path_buf).collect(); + let ancestor_mounts = proptest::collection::vec( + (proptest::sample::select(ancestors), any::()), + 0..4, + ); + let other_mounts = + proptest::collection::vec((mount_point_strategy(), any::()), 0..3); + let table = (ancestor_mounts, other_mounts) + .prop_map(|(mut mounts, others)| { + mounts.extend(others); + mounts + }) + .prop_shuffle(); + (Just(path), table) + }) + } + #[test] fn nearest_existing_ancestor_walks_up_missing_components() { let temp = std::env::temp_dir();