rominf · Oct 6, 2026 · Oct 5, 2026 · Oct 5, 2026 · Oct 6, 2026 · volen-silo
@@ -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"] }
 

@@ -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
@@ -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<Value = u64> {
+        use proptest::prelude::*;
+        prop_oneof![
+            any::<u64>(),
+            (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<Value = u64> {
+        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<Value = PathBuf> {
+        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<Value = PathBuf> {
+        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<Value = (PathBuf, Vec<(PathBuf, u64)>)> {
+        use proptest::prelude::*;
+        path_strategy().prop_flat_map(|path| {
+            let ancestors: Vec<PathBuf> = path.ancestors().map(Path::to_path_buf).collect();
+            let ancestor_mounts = proptest::collection::vec(
+                (proptest::sample::select(ancestors), any::<u64>()),
+                0..4,
+            );
+            let other_mounts =
+                proptest::collection::vec((mount_point_strategy(), any::<u64>()), 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();