view: coordinate-rank bijection tests on extents (#737)

Summary:
coordinate–rank isomorphism tests

Pull Request resolved: #737

Reviewed By: mariusae

Differential Revision: D79495963

Pulled By: shayne-fletcher

fbshipit-source-id: 4b00f232ee3cff61825194199804a5b0333d3000

Author: shayne-fletcher

ndslice/src/slice.rs

@@ -401,21 +401,21 @@ impl Slice {
     /// multidimensional point in a row-major flattened array,
     /// assuming dense gapless storage with zero offset:
     ///
-    /// ```lang=text
+    /// ```plain
     ///     index := Σ(coordinate[i] × ∏(sizes[j] for j > i))
     /// ```
     ///
     /// For example, given a 3x2 row-major base array B:
     ///
-    /// ```lang=text
+    /// ```plain
     ///       0 1 2         1
     /// B =   3 4 5    V =  4
     ///       6 7 8         7
     /// ```
     ///
     /// Let V be the first column of B. Then,
     ///
-    /// ```lang=text
+    /// ```plain
     /// V      | loc   | index
     /// -------+-------+------
     /// (0, 0) |  1    | 0
@@ -428,17 +428,17 @@ impl Slice {
     /// The physical offset formula computes the memory location of a
     /// point `p` as:
     ///
-    /// ```lang=text
+    /// ```plain
     /// loc := offset + Σ(coordinate[i] × stride[i])
     /// ```
     ///
     /// Let the layout be dense row-major and offset = 0.
     /// Then,
-    /// ```lang=text
+    /// ```plain
     /// stride[i] := ∏(sizes[j] for j > i).
     /// ```
     /// and substituting into the physical offset formula:
-    /// ```lang=text
+    /// ```plain
     ///   loc = Σ(coordinate[i] × stride[i])
     ///       = Σ(coordinate[i] × ∏(sizes[j] for j > i))
     ///       = index.

ndslice/src/strategy.rs

@@ -41,6 +41,7 @@ use crate::selection::EvalOpts;
 use crate::selection::Selection;
 use crate::selection::dsl;
 use crate::shape::Range;
+use crate::view::Extent;
 
 /// Generates a random [`Slice`] with up to `max_dims` dimensions,
 /// where each dimension has a size between 1 and `max_len`
@@ -76,6 +77,25 @@ pub fn gen_slice(max_dims: usize, max_len: usize) -> impl Strategy<Value = Slice
     prop::collection::vec(1..=max_len, 1..=max_dims).prop_map(Slice::new_row_major)
 }
 
+/// Generate a random [`Extent`] with `dims` dimensions, where each
+/// size is in `1..=max_len`.
+///
+/// For example, `gen_extent(1..=4, 1..=8)` generates extents like:
+/// - x=3
+/// - x=2, y=4
+/// - x=2, y=4, z=1, w=5
+pub fn gen_extent(
+    dims: std::ops::RangeInclusive<usize>,
+    max_len: usize,
+) -> impl Strategy<Value = Extent> {
+    prop::collection::vec(1..=max_len, dims).prop_map(|sizes| {
+        let labels = (0..sizes.len())
+            .map(|i| format!("d/{}", i))
+            .collect::<Vec<_>>();
+        Extent::new(labels, sizes).unwrap()
+    })
+}
+
 /// Generates a pair `(base, subview)` where:
 /// - `base` is a randomly shaped row-major `Slice`,
 /// - `subview` is a valid rectangular region within `base`.
@@ -620,4 +640,91 @@ mod tests {
             }
         }
     }
+
+    // Coordinate–Rank Isomorphism for Extents
+
+    // Theorem 1: Rank is injective on valid points
+    //
+    // For a given Extent, every distinct coordinate (i.e. Point)
+    // maps to a unique rank.
+    //
+    // ∀ p ≠ q ∈ extent.iter(),  p.rank() ≠ q.rank()
+    proptest! {
+      #[test]
+      fn rank_is_injective(extent in gen_extent(1..=4, 8)) {
+        let mut seen = HashSet::new();
+        for point in extent.iter() {
+          let rank = point.rank();
+          prop_assert!(
+            seen.insert(rank),
+            "Duplicate rank {} for point {}",
+            rank,
+            point
+          );
+        }
+      }
+    }
+
+    // Theorem 2: Row-major monotonicity
+    //
+    // The rank function is monotonic in lexicographic (row-major)
+    // coordinate order.
+    //
+    // ∀ p, q ∈ ℕᵈ, p ≺ q ⇒ rank(p) < rank(q)
+    proptest! {
+      #[test]
+      fn rank_is_monotonic(extent in gen_extent(1..=4, 8)) {
+        let mut last_rank = None;
+        for point in extent.iter() {
+          let rank = point.rank();
+          if let Some(prev) = last_rank {
+            prop_assert!(prev < rank, "Rank not monotonic: {} >= {}", prev, rank);
+          }
+          last_rank = Some(rank);
+        }
+      }
+    }
+
+    // Theorem 3: Rank bounds
+    //
+    // For any point p in extent E, the rank of p is in the range:
+    //     0 ≤ rank(p) < E.len()
+    //
+    // ∀ p ∈ E, 0 ≤ rank(p) < |E|
+    proptest! {
+      #[test]
+      fn rank_bounds(extent in gen_extent(1..=4, 8)) {
+        let len = extent.len();
+        for point in extent.iter() {
+          let rank = point.rank();
+          prop_assert!(rank < len, "Rank {} out of bounds for extent of size {}", rank, len);
+        }
+      }
+    }
+
+    // Theorem 4: Isomorphism (Rank-point round-trip is identity on
+    // all ranks)
+    //
+    // For every valid rank ∈ [0, extent.len()), converting it to a
+    // point and back gives the same rank:
+    //
+    //     rank(point_of_rank(r)) = r
+    //
+    // In categorical terms: point_of_rank ∘ rank = 𝟙ₙ
+    proptest! {
+        #[test]
+        fn rank_point_trip(extent in gen_extent(1..=4, 8)) {
+            for r in 0..extent.len() {
+                let point = extent.point_of_rank(r).unwrap();
+                prop_assert_eq!(
+                    point.rank(),
+                    r,
+                    "point_of_rank({}) returned {}, which maps to rank {}",
+                    r,
+                    point,
+                    point.rank()
+                );
+            }
+        }
+    }
 }