Skip to main content

space_time/zorder/
z_2.rs

1//
2// Copyright 2020, Gobsmacked Labs, LLC.
3//
4// Licensed under the Apache License, Version 2.0 (the "License");
5// you may not use this file except in compliance with the License.
6// You may obtain a copy of the License at
7//
8//     http://www.apache.org/licenses/LICENSE-2.0
9//
10// Unless required by applicable law or agreed to in writing, software
11// distributed under the License is distributed on an "AS IS" BASIS,
12// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13// See the License for the specific language governing permissions and
14// limitations under the License.
15
16//! A two dimensional Z-Order curve.
17
18use crate::zorder::{z_n::ZN, z_range::ZRange};
19use core::convert::TryInto;
20
21/// A two dimensional Z-Order curve.
22#[derive(Debug, PartialEq, Eq, Ord, PartialOrd)]
23pub struct Z2 {
24    z: u64,
25}
26
27impl Z2 {
28    /// Constructor for `Z2` from values from dimension-1 and dimension-2.
29    #[must_use]
30    pub fn new(x: u32, y: u32) -> Self {
31        assert!(x <= Self::MAX_MASK as u32);
32        assert!(y <= Self::MAX_MASK as u32);
33
34        Self::new_from_zorder(Self::split(x) | Self::split(y) << 1)
35    }
36
37    /// Create a Z2 directly from the z value.
38    #[must_use]
39    pub fn new_from_zorder(zorder: u64) -> Self {
40        Z2 { z: zorder }
41    }
42
43    /// Index value.
44    #[must_use]
45    pub fn z(&self) -> u64 {
46        self.z
47    }
48
49    /// Return the user space (un-z-order indexed) values.
50    #[must_use]
51    pub fn decode(&self) -> (u32, u32) {
52        (self.dim(0), self.dim(1))
53    }
54
55    fn dim(&self, i: u64) -> u32 {
56        Z2::combine(self.z >> i)
57    }
58
59    fn d0(&self) -> u32 {
60        self.dim(0)
61    }
62
63    fn d1(&self) -> u32 {
64        self.dim(1)
65    }
66
67    fn partial_overlaps(a1: u32, a2: u32, b1: u32, b2: u32) -> bool {
68        a1.max(b1) <= a2.min(b2)
69    }
70}
71
72impl ZN for Z2 {
73    const DIMENSIONS: u64 = 2;
74
75    const BITS_PER_DIMENSION: u32 = 31;
76
77    const TOTAL_BITS: u64 = Self::DIMENSIONS * Self::BITS_PER_DIMENSION as u64;
78
79    const MAX_MASK: u64 = 0x7fff_ffff;
80
81    fn split(value: u32) -> u64 {
82        let mut x = value.into();
83        x &= Self::MAX_MASK;
84        x = (x | (x << 32)) & 0x0000_0000_ffff_ffff_u64;
85        x = (x | (x << 16)) & 0x0000_ffff_0000_ffff_u64;
86        x = (x | (x << 8)) & 0x00ff_00ff_00ff_00ff_u64;
87        x = (x | (x << 4)) & 0x0f0f_0f0f_0f0f_0f0f_u64;
88        x = (x | (x << 2)) & 0x3333_3333_3333_3333_u64;
89        x = (x | (x << 1)) & 0x5555_5555_5555_5555_u64;
90        x
91    }
92
93    fn combine(z: u64) -> u32 {
94        let mut x = z & 0x5555_5555_5555_5555;
95        x = (x ^ (x >> 1)) & 0x3333_3333_3333_3333;
96        x = (x ^ (x >> 2)) & 0x0f0f_0f0f_0f0f_0f0f;
97        x = (x ^ (x >> 4)) & 0x00ff_00ff_00ff_00ff;
98        x = (x ^ (x >> 8)) & 0x0000_ffff_0000_ffff;
99        x = (x ^ (x >> 16)) & 0x0000_0000_ffff_ffff;
100        x.try_into().expect("Value fits into a u32")
101    }
102
103    fn contains(range: ZRange, value: u64) -> bool {
104        let (x, y) = Z2 { z: value }.decode();
105        x >= Z2 { z: range.min }.d0()
106            && x <= Z2 { z: range.max }.d0()
107            && y >= Z2 { z: range.min }.d1()
108            && y <= Z2 { z: range.max }.d1()
109    }
110
111    fn overlaps(range: ZRange, value: ZRange) -> bool {
112        Self::partial_overlaps(
113            Z2 { z: range.min }.d0(),
114            Z2 { z: range.max }.d0(),
115            Z2 { z: value.min }.d0(),
116            Z2 { z: value.max }.d0(),
117        ) && Self::partial_overlaps(
118            Z2 { z: range.min }.d1(),
119            Z2 { z: range.max }.d1(),
120            Z2 { z: value.min }.d1(),
121            Z2 { z: value.max }.d1(),
122        )
123    }
124}
125
126#[cfg(kani)]
127mod kani_proofs {
128    use super::*;
129
130    /// Splitting then combining a value within `MAX_MASK` is the identity, for
131    /// every valid input. Also proves the `try_into().expect(..)` in `combine`
132    /// never panics.
133    #[kani::proof]
134    fn split_combine_roundtrip() {
135        let x: u32 = kani::any();
136        kani::assume(x <= Z2::MAX_MASK as u32);
137        assert_eq!(Z2::combine(Z2::split(x)), x);
138    }
139
140    /// Encoding two dimensions into a `Z2` and decoding recovers the original
141    /// pair, for every valid input.
142    #[kani::proof]
143    fn encode_decode_roundtrip() {
144        let x: u32 = kani::any();
145        let y: u32 = kani::any();
146        kani::assume(x <= Z2::MAX_MASK as u32);
147        kani::assume(y <= Z2::MAX_MASK as u32);
148        assert_eq!(Z2::new(x, y).decode(), (x, y));
149    }
150
151    /// Build a `ZRange` bounding box from two ordered user-space corners.
152    fn box_from(x0: u32, y0: u32, x1: u32, y1: u32) -> ZRange {
153        ZRange {
154            min: Z2::new(x0, y0).z(),
155            max: Z2::new(x1, y1).z(),
156        }
157    }
158
159    /// Any user-space point inside a bounding box (built from two ordered
160    /// corners) is reported as contained by `Z2::contains`. This proves the
161    /// user-space containment semantics of the index-space predicate.
162    #[kani::proof]
163    fn point_in_box_is_contained() {
164        let x0: u32 = kani::any();
165        let y0: u32 = kani::any();
166        let x1: u32 = kani::any();
167        let y1: u32 = kani::any();
168        kani::assume(x0 <= x1 && x1 <= Z2::MAX_MASK as u32);
169        kani::assume(y0 <= y1 && y1 <= Z2::MAX_MASK as u32);
170
171        let px: u32 = kani::any();
172        let py: u32 = kani::any();
173        kani::assume(x0 <= px && px <= x1);
174        kani::assume(y0 <= py && py <= y1);
175
176        let range = box_from(x0, y0, x1, y1);
177        assert!(Z2::contains(range, Z2::new(px, py).z()));
178    }
179
180    /// For bounding boxes built from ordered corners, if `range` contains both
181    /// corners of `value` then `range` and `value` overlap. A containing range
182    /// must overlap.
183    #[kani::proof]
184    fn contains_value_implies_overlaps() {
185        let rx0: u32 = kani::any();
186        let ry0: u32 = kani::any();
187        let rx1: u32 = kani::any();
188        let ry1: u32 = kani::any();
189        kani::assume(rx0 <= rx1 && rx1 <= Z2::MAX_MASK as u32);
190        kani::assume(ry0 <= ry1 && ry1 <= Z2::MAX_MASK as u32);
191
192        let vx0: u32 = kani::any();
193        let vy0: u32 = kani::any();
194        let vx1: u32 = kani::any();
195        let vy1: u32 = kani::any();
196        kani::assume(vx0 <= vx1 && vx1 <= Z2::MAX_MASK as u32);
197        kani::assume(vy0 <= vy1 && vy1 <= Z2::MAX_MASK as u32);
198
199        let range = box_from(rx0, ry0, rx1, ry1);
200        let value = box_from(vx0, vy0, vx1, vy1);
201
202        kani::assume(Z2::contains_value(range, value));
203        assert!(Z2::overlaps(range, value));
204    }
205
206    /// `Z2::overlaps` is symmetric for every pair of index-space rectangles.
207    #[kani::proof]
208    fn overlaps_is_symmetric() {
209        let a_min: u64 = kani::any();
210        let a_max: u64 = kani::any();
211        let b_min: u64 = kani::any();
212        let b_max: u64 = kani::any();
213        let a = ZRange {
214            min: a_min,
215            max: a_max,
216        };
217        let b = ZRange {
218            min: b_min,
219            max: b_max,
220        };
221        assert_eq!(Z2::overlaps(a, b), Z2::overlaps(b, a));
222    }
223
224    /// A point is contained by a bounding box exactly when the box overlaps the
225    /// degenerate range made of just that point. Ties `contains` and `overlaps`
226    /// together.
227    #[kani::proof]
228    fn contains_matches_degenerate_overlap() {
229        let x0: u32 = kani::any();
230        let y0: u32 = kani::any();
231        let x1: u32 = kani::any();
232        let y1: u32 = kani::any();
233        kani::assume(x0 <= x1 && x1 <= Z2::MAX_MASK as u32);
234        kani::assume(y0 <= y1 && y1 <= Z2::MAX_MASK as u32);
235
236        let px: u32 = kani::any();
237        let py: u32 = kani::any();
238        kani::assume(px <= Z2::MAX_MASK as u32);
239        kani::assume(py <= Z2::MAX_MASK as u32);
240
241        let range = box_from(x0, y0, x1, y1);
242        let point = Z2::new(px, py).z();
243        let degenerate = ZRange {
244            min: point,
245            max: point,
246        };
247
248        assert_eq!(Z2::contains(range, point), Z2::overlaps(range, degenerate));
249    }
250}
251
252#[cfg(test)]
253mod tests {
254    use super::*;
255
256    #[quickcheck]
257    fn test_userspace_to_z2_and_back(x: u32, y: u32) -> bool {
258        if x > Z2::MAX_MASK as u32 || y > Z2::MAX_MASK as u32 {
259            true
260        } else {
261            let (x_, y_) = Z2::new(x, y).decode();
262            x_ == x && y_ == y
263        }
264    }
265
266    #[quickcheck]
267    fn test_split_and_combine(x: u32) -> bool {
268        if x > Z2::MAX_MASK as u32 {
269            true
270        } else {
271            Z2::combine(Z2::split(x)) == x
272        }
273    }
274
275    #[test]
276    fn test_z2_encoding() {
277        assert_eq!(Z2::new(1, 0).z, 1);
278        assert_eq!(Z2::new(2, 0).z, 4);
279        assert_eq!(Z2::new(3, 0).z, 5);
280        assert_eq!(Z2::new(4, 0).z, 16);
281        assert_eq!(Z2::new(0, 1).z, 2);
282        assert_eq!(Z2::new(0, 2).z, 8);
283        assert_eq!(Z2::new(0, 3).z, 10);
284    }
285
286    #[test]
287    fn test_z2_decoding() {
288        assert_eq!(Z2::new(23, 13).decode(), (23, 13));
289        assert_eq!(
290            Z2::new(Z2::MAX_MASK as u32, 0).decode(),
291            (Z2::MAX_MASK as u32, 0)
292        );
293        assert_eq!(
294            Z2::new(0, Z2::MAX_MASK as u32).decode(),
295            (0, Z2::MAX_MASK as u32)
296        );
297        assert_eq!(
298            Z2::new(Z2::MAX_MASK as u32, Z2::MAX_MASK as u32).decode(),
299            (Z2::MAX_MASK as u32, Z2::MAX_MASK as u32)
300        );
301        assert_eq!(
302            Z2::new(Z2::MAX_MASK as u32 - 10, Z2::MAX_MASK as u32 - 10).decode(),
303            (Z2::MAX_MASK as u32 - 10, Z2::MAX_MASK as u32 - 10)
304        );
305    }
306
307    #[test]
308    fn test_longest_common_prefix() {
309        assert_eq!(
310            Z2::longest_common_prefix(&[u64::MAX, u64::MAX - 15]).prefix,
311            u64::MAX - 15
312        );
313        assert_eq!(Z2::longest_common_prefix(&[15, 13]).prefix, 12); // 1111, 1101 => 1100 => 12
314        assert_eq!(Z2::longest_common_prefix(&[12, 15]).prefix, 12); // 1100, 1111 => 1100
315        // => 12
316    }
317
318    #[test]
319    fn test_zrange() {
320        let ranges = Z2::zranges_default::<Z2>(&[ZRange { min: 12, max: 15 }]);
321
322        assert_eq!(ranges.len(), 1);
323        assert_eq!(ranges[0].lower(), 12);
324        assert_eq!(ranges[0].upper(), 15);
325
326        let ranges = Z2::zranges_default::<Z2>(&[ZRange { min: 0, max: 15 }]);
327        assert_eq!(ranges.len(), 1);
328        assert_eq!(ranges[0].lower(), 0);
329        assert_eq!(ranges[0].upper(), 15);
330
331        let ranges = Z2::zranges_default::<Z2>(&[ZRange { min: 0, max: 27 }]);
332        assert_eq!(ranges.len(), 2);
333        assert_eq!(ranges[0].lower(), 0);
334        assert_eq!(ranges[0].upper(), 19);
335        assert_eq!(ranges[1].lower(), 24);
336        assert_eq!(ranges[1].upper(), 27);
337    }
338
339    #[test]
340    fn test_contains() {
341        let z_range_1 = ZRange { min: 0, max: 3 };
342        let z_range_2 = ZRange { min: 2, max: 3 };
343        assert!(Z2::contains_value(z_range_1, z_range_2));
344
345        assert!(Z2::contains(ZRange { min: 2, max: 6 }, 3));
346    }
347
348    #[test]
349    fn test_overlaps() {
350        assert!(Z2::overlaps(
351            ZRange { min: 0, max: 1 },
352            ZRange { min: 1, max: 4 }
353        ));
354        // Smaller overlaps larger
355        assert!(Z2::overlaps(
356            ZRange {
357                min: Z2::new(1, 0).z(),
358                max: Z2::new(2, 0).z()
359            },
360            ZRange {
361                min: Z2::new(0, 0).z(),
362                max: Z2::new(4, 0).z()
363            }
364        ));
365        // larger overlaps smaller
366        assert!(Z2::overlaps(
367            ZRange {
368                min: Z2::new(0, 0).z(),
369                max: Z2::new(4, 0).z()
370            },
371            ZRange {
372                min: Z2::new(1, 0).z(),
373                max: Z2::new(2, 0).z()
374            }
375        ));
376    }
377}
378
379#[cfg(test)]
380mod range_query_tests {
381    use super::*;
382    use quickcheck_macros::quickcheck;
383
384    /// End-to-end property for the range engine over `Z2`: for any rectangular
385    /// query box on a small grid, and any bottom-out settings, `zranges` must be
386    ///
387    ///  * COMPLETE — every cell inside the box falls in some returned range, so a query
388    ///    never silently drops results, and
389    ///  * SOUND — every index inside a `CoveredRange` decodes back into the box
390    ///    (overlapping ranges are allowed to spill, covered ones are not).
391    ///
392    /// `max_recurse`/`max_ranges` are varied (including the aggressive values
393    /// that force early `bottom_out`) to confirm completeness survives the
394    /// coarsening.
395    #[quickcheck]
396    fn z2_zranges_complete_and_sound(
397        bits: u8,
398        a: u16,
399        b: u16,
400        c: u16,
401        d: u16,
402        max_recurse: Option<u8>,
403        max_ranges: Option<u8>,
404    ) -> bool {
405        // Grid side 2..=32 (powers of two so every z in `0..side*side` is a cell).
406        let n_bits: u32 = u32::from(bits % 5) + 1;
407        let side: u32 = 1 << n_bits;
408
409        let (col_min, col_max) = {
410            let (lo, hi) = (u32::from(a) % side, u32::from(c) % side);
411            (lo.min(hi), lo.max(hi))
412        };
413        let (row_min, row_max) = {
414            let (lo, hi) = (u32::from(b) % side, u32::from(d) % side);
415            (lo.min(hi), lo.max(hi))
416        };
417
418        let zbound = ZRange {
419            min: Z2::new(col_min, row_min).z(),
420            max: Z2::new(col_max, row_max).z(),
421        };
422
423        let max_recurse = max_recurse.map(|v| usize::from(v % 10)); // 0..=9
424        let max_ranges = max_ranges.map(|v| usize::from(v % 32) + 1); // 1..=32
425
426        // 64 is the precision the public `ranges()` entry points always pass.
427        let ranges = Z2::zranges::<Z2>(&[zbound], 64, max_ranges, max_recurse);
428
429        let cell_count = u64::from(side) * u64::from(side);
430
431        // Completeness.
432        for col in col_min..=col_max {
433            for row in row_min..=row_max {
434                let z = Z2::new(col, row).z();
435                if !ranges.iter().any(|rg| rg.lower() <= z && z <= rg.upper()) {
436                    return false;
437                }
438            }
439        }
440
441        // Soundness of covered ranges.
442        for rg in &ranges {
443            if rg.contained() {
444                // A sound covered range can hold at most `box_cells` (< grid
445                // cells) consecutive in-box indices; a larger span is unsound on
446                // its face and also guards against runaway enumeration on a bug.
447                if rg.upper().saturating_sub(rg.lower()) >= cell_count {
448                    return false;
449                }
450                for z in rg.lower()..=rg.upper() {
451                    let (col, row) = Z2::new_from_zorder(z).decode();
452                    if col < col_min || col > col_max || row < row_min || row > row_max {
453                        return false;
454                    }
455                }
456            }
457        }
458
459        true
460    }
461}