1use crate::zorder::{z_n::ZN, z_range::ZRange};
19use core::convert::TryInto;
20
21#[derive(Debug, PartialEq, Eq, Ord, PartialOrd)]
23pub struct Z2 {
24 z: u64,
25}
26
27impl Z2 {
28 #[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 #[must_use]
39 pub fn new_from_zorder(zorder: u64) -> Self {
40 Z2 { z: zorder }
41 }
42
43 #[must_use]
45 pub fn z(&self) -> u64 {
46 self.z
47 }
48
49 #[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 #[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 #[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 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 #[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 #[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 #[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 #[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); assert_eq!(Z2::longest_common_prefix(&[12, 15]).prefix, 12); }
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 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 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 #[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 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)); let max_ranges = max_ranges.map(|v| usize::from(v % 32) + 1); let ranges = Z2::zranges::<Z2>(&[zbound], 64, max_ranges, max_recurse);
428
429 let cell_count = u64::from(side) * u64::from(side);
430
431 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 for rg in &ranges {
443 if rg.contained() {
444 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}