competitive/algorithm/
dyadic_ranges.rs

1/// Maximal aligned power-of-two intervals.
2pub fn dyadic_ranges(range: std::ops::Range<u64>) -> impl Iterator<Item = std::ops::Range<u64>> {
3    let mut left = range.start;
4    let right = range.end;
5    std::iter::from_fn(move || {
6        if left >= right {
7            return None;
8        }
9        let remaining = right - left;
10        let exponent = left.trailing_zeros().min(remaining.ilog2());
11        let end = left + (1u64 << exponent);
12        let result = left..end;
13        left = end;
14        Some(result)
15    })
16}
17
18#[cfg(kani)]
19mod verification {
20    use super::*;
21
22    #[kani::proof]
23    fn proof_dyadic_step() {
24        let left: u64 = kani::any();
25        let right: u64 = kani::any();
26        let mut iter = dyadic_ranges(left..right);
27        match iter.next() {
28            Some(range) => {
29                let length = range.end - range.start;
30                kani::assert(
31                    range.start == left
32                        && range.end <= right
33                        && length.is_power_of_two()
34                        && range.start & (length - 1) == 0,
35                    "For all nonempty u64 intervals, the first dyadic range starts at the left endpoint, is aligned, has power-of-two length and fits within the interval",
36                );
37                let doubled = 2 * length as u128;
38                kani::assert(
39                    left as u128 & (doubled - 1) != 0 || left as u128 + doubled > right as u128,
40                    "For all u64 intervals, the emitted dyadic range has the largest aligned power-of-two length that fits at the current left endpoint",
41                );
42                kani::assert(
43                    match iter.next() {
44                        Some(next) => next.start == range.end && next.end <= right,
45                        None => range.end == right,
46                    },
47                    "For all u64 intervals, dyadic iteration advances without gaps and stops only at the right endpoint",
48                );
49            }
50            None => kani::assert(
51                left >= right && iter.next().is_none(),
52                "Empty and reversed u64 intervals produce no dyadic ranges and stay exhausted",
53            ),
54        }
55        kani::cover!(left == 0 && right == u64::MAX);
56        kani::cover!(left == u64::MAX - 1 && right == u64::MAX);
57    }
58}
59
60#[cfg(test)]
61mod tests {
62    use super::*;
63    use crate::tools::Xorshift;
64
65    #[test]
66    fn test_dyadic_ranges() {
67        let mut rng = Xorshift::default();
68        let ranges = (0..=256)
69            .flat_map(|left| (0..=256).map(move |right| (left, right)))
70            .chain([
71                (0, u64::MAX),
72                (u64::MAX - 1000, u64::MAX),
73                (1 << 63, u64::MAX),
74                (u64::MAX, u64::MAX),
75                (u64::MAX, 0),
76            ])
77            .chain(rng.random_iter((0..=u64::MAX, 0..=u64::MAX)).take(1000));
78        for (left, right) in ranges {
79            if left > right {
80                assert!(dyadic_ranges(left..right).next().is_none());
81                continue;
82            }
83            let mut expected_start = left;
84            for range in dyadic_ranges(left..right) {
85                let length = range.end - range.start;
86                assert!(length.is_power_of_two());
87                assert_eq!(range.start % length, 0);
88                assert_eq!(range.start, expected_start);
89                assert!(range.end <= right);
90                let parent_length = 2 * length as u128;
91                let parent_start = range.start as u128 & !(parent_length - 1);
92                assert!(
93                    parent_start < left as u128 || parent_start + parent_length > right as u128
94                );
95                expected_start = range.end;
96            }
97            assert_eq!(expected_start, right);
98        }
99    }
100}
competitive/algorithm/dyadic_ranges.rs

competitive/algorithm/
dyadic_ranges.rs
