strided_view/injectivity.rs
1//! Output-layout injectivity validation.
2//!
3//! Kernel families that write through a strided destination must prove that
4//! distinct logical positions map to distinct memory offsets. This is the one
5//! owner of that analysis: `strided-basic` re-exports it for its kernel
6//! families and `strided-perm` calls it before its unsafe permutation loops.
7//!
8//! The common case is validated without allocating: axes are reduced in
9//! ascending `|stride|` order and only the interleaved block of small-stride
10//! axes is compared pairwise. A two-axis block is settled exactly by a gcd
11//! argument regardless of size. A block of three or more axes is settled
12//! exactly by searching for a colliding difference vector over all but its two
13//! largest axes, which is cheap whenever the other axes are short, regardless
14//! of the block's element count. A block whose difference search exceeds its
15//! budget falls back to pairwise comparison, then to the exact (allocating)
16//! enumeration. All paths conservatively reject metadata whose spans do not
17//! fit the analysis, which keeps the entry points panic-free.
18
19/// Decide whether distinct logical positions map to distinct offsets.
20///
21/// Runs the allocation-free proof first (separated axes, the two-axis gcd
22/// argument, the difference search, then the pairwise budget) and falls back
23/// to the exact enumeration only when all of those are out of budget. This
24/// accepts the interleaved `[3, 1500]` / `[2000, 3]` and
25/// `[2, 2, 5_000_000]` / `[4, 5, 6]` cases without allocating.
26///
27/// `true` always means injective. `false` means the layout aliases, except
28/// for one documented residual: an interleaved block of three or more axes
29/// whose difference search (half the product of `2 * extent - 1` over all but
30/// its two longest axes) exceeds 2^22 vectors *and* whose element count
31/// exceeds 2^24 is not decided and is reported as `false`. Such a block needs
32/// at least three interleaved axes with long extents.
33///
34/// # Examples
35///
36/// ```
37/// use strided_view::is_injective_layout;
38/// assert!(is_injective_layout(&[2, 3], &[1, 2]));
39/// assert!(!is_injective_layout(&[2, 3], &[0, 1]));
40/// // Interleaved but injective: 2000 = 2 (mod 3) keeps the rows apart.
41/// assert!(is_injective_layout(&[3, 1500], &[2000, 3]));
42/// ```
43pub fn is_injective_layout(dims: &[usize], strides: &[isize]) -> bool {
44 is_injective_layout_without_alloc(dims, strides) || is_injective_layout_exact(dims, strides)
45}
46
47/// Allocation-free injectivity check.
48///
49/// Exact for a two-axis interleaved block (any size), for a block whose
50/// difference search fits `DIFFERENCE_SEARCH_BUDGET`, and for interleaved
51/// blocks of at most `PAIRWISE_BLOCK_BUDGET` logical elements; other blocks
52/// are conservatively rejected (callers that must keep
53/// every injective layout use [`is_injective_layout`] instead, which spills to
54/// the exact enumeration). Exposed for the kernel adapters that validate a
55/// destination on a per-call path.
56#[doc(hidden)]
57pub fn is_injective_layout_without_alloc(dims: &[usize], strides: &[isize]) -> bool {
58 let Some(total) = validate_injective_layout_inputs(dims, strides) else {
59 return false;
60 };
61 if total <= 1 {
62 return true;
63 }
64 match interleaved_block(dims, strides) {
65 None => false,
66 Some(None) => true,
67 Some(Some(block)) => {
68 if !block.may_be_injective() {
69 // Pigeonhole: more elements than reachable offsets always alias.
70 return false;
71 }
72 if let Some(injective) = two_axis_block_is_injective(dims, strides, &block) {
73 return injective;
74 }
75 if let Some(injective) = block_differences_avoid_zero(dims, strides, &block) {
76 return injective;
77 }
78 block.total <= PAIRWISE_BLOCK_BUDGET as u128
79 && block_offsets_unique_pairwise(dims, strides, &block)
80 }
81 }
82}
83
84/// Exact injectivity check used when the pairwise budget is exceeded.
85fn is_injective_layout_exact(dims: &[usize], strides: &[isize]) -> bool {
86 let Some(total) = validate_injective_layout_inputs(dims, strides) else {
87 return false;
88 };
89 if total <= 1 {
90 return true;
91 }
92 match interleaved_block(dims, strides) {
93 None => false,
94 Some(None) => true,
95 Some(Some(block)) => {
96 if !block.may_be_injective() {
97 // Pigeonhole: more elements than reachable offsets always alias.
98 return false;
99 }
100 if let Some(injective) = two_axis_block_is_injective(dims, strides, &block) {
101 return injective;
102 }
103 // The difference search already ran in the allocation-free path
104 // and was out of budget.
105 block.total <= EXACT_BLOCK_BUDGET as u128 && block_offsets_unique(dims, strides, &block)
106 }
107 }
108}
109
110/// Largest interleaved block enumerated exactly by the spill path.
111///
112/// INVARIANT: bounds the auxiliary memory of the exact check. The block is
113/// visited once in O(block) time; its seen-set is a bitmap over the block's
114/// offset span when that span is at most 64 offsets per element, otherwise a
115/// sorted offset list, so it never exceeds 8 bytes per block element
116/// (128 MiB at this bound). Separated axes never count toward the budget.
117const EXACT_BLOCK_BUDGET: usize = 1 << 24;
118
119/// Largest interleaved block compared pairwise by the allocation-free check.
120///
121/// INVARIANT: keeps the O(block^2) pairwise comparison bounded; larger blocks
122/// use the exact spill path. Separated axes never count toward the budget.
123const PAIRWISE_BLOCK_BUDGET: usize = 4096;
124
125/// Largest number of difference vectors visited by the difference search.
126///
127/// INVARIANT: bounds the time of the allocation-free difference search in
128/// [`block_differences_avoid_zero`]. Each visit is O(1) integer arithmetic
129/// after an O(rank) setup, and the count is half the product of
130/// `2 * extent - 1` over every block axis except the two largest, so the
131/// bound is independent of the block's element count.
132const DIFFERENCE_SEARCH_BUDGET: u128 = 1 << 22;
133
134/// The smallest-stride axes that must be checked by enumeration.
135struct InterleavedBlock {
136 last_key: (u128, usize),
137 /// Product of the block's extents.
138 total: u128,
139 /// Largest offset reachable inside the block after normalising strides to
140 /// their absolute values (the smallest is zero).
141 span: u128,
142}
143
144impl InterleavedBlock {
145 fn contains(&self, axis: usize, dim: usize, stride: isize) -> bool {
146 dim > 1 && (stride.unsigned_abs() as u128, axis) <= self.last_key
147 }
148
149 /// Pigeonhole: more elements than reachable offsets always alias.
150 fn may_be_injective(&self) -> bool {
151 self.total <= self.span + 1
152 }
153}
154
155/// Exact, allocation-free injectivity decision for a two-axis interleaved
156/// block.
157///
158/// For strides `s1 <= s2` and extents `d1`, `d2`, the sums `i*s1 + j*s2` are
159/// all distinct iff `s2/g >= d1` or `s1/g >= d2`, where `g = gcd(s1, s2)`: a
160/// non-zero `a*s1 + b*s2 = 0` must have `|a| >= s2/g` and `|b| >= s1/g`, so a
161/// collision exists exactly when both bounds fit inside the extents. The
162/// result is exact, so it is decidable without enumeration even for a block
163/// far above the enumeration budget. Returns `None` when the block does not
164/// hold exactly two axes.
165fn two_axis_block_is_injective(
166 dims: &[usize],
167 strides: &[isize],
168 block: &InterleavedBlock,
169) -> Option<bool> {
170 let mut axes = [(0usize, 0usize); 2]; // (extent, |stride|)
171 let mut count = 0;
172 for (axis, (&dim, &stride)) in dims.iter().zip(strides.iter()).enumerate() {
173 if !block.contains(axis, dim, stride) {
174 continue;
175 }
176 if count == 2 {
177 return None;
178 }
179 axes[count] = (dim, stride.unsigned_abs());
180 count += 1;
181 }
182 if count != 2 {
183 return None;
184 }
185 // Order by stride so the pairing of the gcd bounds matches the proof.
186 let (extent_lo, stride_lo, extent_hi, stride_hi) = if axes[0].1 <= axes[1].1 {
187 (
188 axes[0].0 as u128,
189 axes[0].1 as u128,
190 axes[1].0 as u128,
191 axes[1].1 as u128,
192 )
193 } else {
194 (
195 axes[1].0 as u128,
196 axes[1].1 as u128,
197 axes[0].0 as u128,
198 axes[0].1 as u128,
199 )
200 };
201 let g = gcd(stride_lo, stride_hi);
202 debug_assert!(g > 0, "stride zero on a non-singleton axis was rejected");
203 Some(stride_hi / g >= extent_lo || stride_lo / g >= extent_hi)
204}
205
206/// Exact, allocation-free injectivity decision for a block of three or more
207/// axes, by searching for a colliding difference vector.
208///
209/// Two positions collide iff a non-zero `delta` with `|delta[k]| < dims[k]`
210/// solves `sum(delta[k] * strides[k]) == 0`. The two block axes with the
211/// largest extents are solved in closed form: for a fixed difference `r` of
212/// the other axes, `x * a + y * b == -r` with `|x| <= X`, `|y| <= Y` is a
213/// bounded two-variable linear Diophantine equation, settled by its gcd and
214/// one modular inverse. Only the other axes are enumerated, and `delta` and
215/// `-delta` are the same collision, so half of their box is visited. The
216/// search is therefore independent of the two largest extents, which is
217/// what lets a large block with small cross axes be decided exactly
218/// (tensor4all/strided-rs#342). Returns `None` when the block has fewer than
219/// three axes or the search exceeds `DIFFERENCE_SEARCH_BUDGET`.
220fn block_differences_avoid_zero(
221 dims: &[usize],
222 strides: &[isize],
223 block: &InterleavedBlock,
224) -> Option<bool> {
225 let in_block = |axis: usize| block.contains(axis, dims[axis], strides[axis]);
226 // The two block axes with the largest extents.
227 let (mut first, mut second) = (None::<usize>, None::<usize>);
228 let mut count = 0usize;
229 for axis in (0..dims.len()).filter(|&axis| in_block(axis)) {
230 count += 1;
231 if first.is_none_or(|f| dims[axis] > dims[f]) {
232 second = first;
233 first = Some(axis);
234 } else if second.is_none_or(|s| dims[axis] > dims[s]) {
235 second = Some(axis);
236 }
237 }
238 if count < 3 {
239 return None;
240 }
241 let (first, second) = (first?, second?);
242 let enumerated = |axis: usize| axis != first && axis != second && in_block(axis);
243
244 // The difference box of the enumerated axes holds `boxed` vectors, an
245 // odd number with the zero vector in the middle.
246 let mut boxed = 1u128;
247 for axis in (0..dims.len()).filter(|&axis| enumerated(axis)) {
248 boxed = boxed.checked_mul(2 * dims[axis] as u128 - 1)?;
249 if boxed / 2 > DIFFERENCE_SEARCH_BUDGET {
250 return None;
251 }
252 }
253
254 // The block span fits `isize` (checked by the caller's input
255 // validation), so every partial sum below fits `i128` comfortably.
256 let a = strides[first].unsigned_abs() as i128;
257 let b = strides[second].unsigned_abs() as i128;
258 let (x_bound, y_bound) = ((dims[first] - 1) as i128, (dims[second] - 1) as i128);
259 let (g, inverse) = gcd_and_inverse(a, b);
260 let (a, b) = (a / g, b / g);
261 // `x * a + y * b == c` (after dividing by `g`) has a solution in the box.
262 let solvable = |c: i128| -> bool {
263 // All solutions: x = x0 + t * b, y = (c - x * a) / b.
264 let x0 = (c.rem_euclid(b) * inverse).rem_euclid(b);
265 // |y| <= Y <=> c - Y b <= x a <= c + Y b.
266 let lo = (c - y_bound * b).div_euclid(a) + i128::from((c - y_bound * b).rem_euclid(a) != 0);
267 let hi = (c + y_bound * b).div_euclid(a);
268 let (lo, hi) = (lo.max(-x_bound), hi.min(x_bound));
269 lo <= hi && lo + (x0 - lo).rem_euclid(b) <= hi
270 };
271
272 // Collisions with the enumerated axes all zero: the two-axis gcd bound.
273 if b <= x_bound && a <= y_bound {
274 return Some(false);
275 }
276
277 // Walk the upper half of the box in mixed radix, starting just past the
278 // zero vector. Each axis is (delta, extent - 1, |stride|) and `r` is the
279 // running `sum(delta * stride)`; negating every enumerated stride is a
280 // bijection on the box, so `|stride|` is used throughout.
281 let mut axes: tinyvec::TinyVec<[(i128, i128, i128); crate::INLINE_RANK]> = (0..dims.len())
282 .filter(|&axis| enumerated(axis))
283 .map(|axis| {
284 (
285 0,
286 (dims[axis] - 1) as i128,
287 strides[axis].unsigned_abs() as i128,
288 )
289 })
290 .collect();
291 let mut r = 0i128;
292 for _ in 0..boxed / 2 {
293 for (delta, bound, stride) in axes.iter_mut() {
294 if *delta < *bound {
295 *delta += 1;
296 r += *stride;
297 break;
298 }
299 r -= *stride * (*delta + *bound);
300 *delta = -*bound;
301 }
302 if r % g == 0 && solvable(-r / g) {
303 return Some(false);
304 }
305 }
306 Some(true)
307}
308
309/// `gcd(a, b)` and the inverse of `a / g` modulo `b / g` (`0` when
310/// `b / g == 1`), for positive `a` and `b`.
311fn gcd_and_inverse(a: i128, b: i128) -> (i128, i128) {
312 // Extended Euclid: invariant `old_r == old_s * a (mod b)`.
313 let (mut old_r, mut r) = (a, b);
314 let (mut old_s, mut s) = (1i128, 0i128);
315 while r != 0 {
316 let q = old_r / r;
317 (old_r, r) = (r, old_r - q * r);
318 (old_s, s) = (s, old_s - q * s);
319 }
320 let modulus = b / old_r;
321 (old_r, old_s.rem_euclid(modulus))
322}
323
324/// Greatest common divisor of two non-negative integers.
325fn gcd(mut a: u128, mut b: u128) -> u128 {
326 while b != 0 {
327 let remainder = a % b;
328 a = b;
329 b = remainder;
330 }
331 a
332}
333
334/// Find the interleaved block of a layout.
335///
336/// Returns `None` when a stride or span cannot be represented, `Some(None)`
337/// when every axis is separated (so the layout is injective), and the block
338/// otherwise. Negating a stride only reflects the coordinate along that axis
339/// and shifts all offsets by a constant, so the analysis uses `|stride|`.
340fn interleaved_block(dims: &[usize], strides: &[isize]) -> Option<Option<InterleavedBlock>> {
341 let mut covered_span = 0u128;
342 let mut covered_total = 1u128;
343 let mut previous_key = None;
344 let mut block = None;
345 let active_axes = dims.iter().filter(|&&dim| dim > 1).count();
346 for _ in 0..active_axes {
347 let mut next = None;
348 for (axis, (&dim, &stride)) in dims.iter().zip(strides.iter()).enumerate() {
349 if dim <= 1 {
350 continue;
351 }
352 let key = (stride.checked_abs()? as u128, axis);
353 if previous_key.is_some_and(|previous| key <= previous) {
354 continue;
355 }
356 if next.is_none_or(|(best, _)| key < best) {
357 next = Some((key, dim as u128));
358 }
359 }
360 let ((stride, axis), dim) = next?;
361 let separated = stride > covered_span;
362 covered_span = stride
363 .checked_mul(dim - 1)
364 .and_then(|span| covered_span.checked_add(span))?;
365 covered_total = covered_total.checked_mul(dim)?;
366 if !separated {
367 block = Some(InterleavedBlock {
368 last_key: (stride, axis),
369 total: covered_total,
370 span: covered_span,
371 });
372 }
373 previous_key = Some((stride, axis));
374 }
375 Some(block)
376}
377
378/// Enumerate the block's offsets once and report whether they are distinct.
379fn block_offsets_unique(dims: &[usize], strides: &[isize], block: &InterleavedBlock) -> bool {
380 let axes: Vec<(usize, usize)> = dims
381 .iter()
382 .zip(strides.iter())
383 .enumerate()
384 .filter(|&(axis, (&dim, &stride))| block.contains(axis, dim, stride))
385 .map(|(_, (&dim, &stride))| (dim, stride.unsigned_abs()))
386 .collect();
387 let (Ok(total), Ok(span)) = (usize::try_from(block.total), usize::try_from(block.span)) else {
388 return false;
389 };
390
391 // Every visited offset and every partial axis span lies within
392 // [0, span], which fits `usize` (checked above), so the incremental
393 // updates below cannot overflow.
394 let mut indices = vec![0usize; axes.len()];
395 let mut offset = 0usize;
396 let mut advance = |offset: &mut usize| {
397 for (index, &(dim, stride)) in indices.iter_mut().zip(axes.iter()) {
398 if *index + 1 < dim {
399 *index += 1;
400 *offset += stride;
401 return;
402 }
403 *offset -= stride * (dim - 1);
404 *index = 0;
405 }
406 };
407
408 if block.span / 64 <= block.total {
409 let mut seen = vec![0u64; span / 64 + 1];
410 for _ in 0..total {
411 let (word, bit) = (offset / 64, 1u64 << (offset % 64));
412 if seen[word] & bit != 0 {
413 return false;
414 }
415 seen[word] |= bit;
416 advance(&mut offset);
417 }
418 true
419 } else {
420 let mut offsets = Vec::with_capacity(total);
421 for _ in 0..total {
422 offsets.push(offset);
423 advance(&mut offset);
424 }
425 offsets.sort_unstable();
426 offsets.windows(2).all(|pair| pair[0] != pair[1])
427 }
428}
429
430fn block_offset_for_linear_index(
431 dims: &[usize],
432 strides: &[isize],
433 block: &InterleavedBlock,
434 mut linear: usize,
435) -> u128 {
436 let mut offset = 0u128;
437 for (axis, (&dim, &stride)) in dims.iter().zip(strides.iter()).enumerate() {
438 if !block.contains(axis, dim, stride) {
439 continue;
440 }
441 offset += stride.unsigned_abs() as u128 * (linear % dim) as u128;
442 linear /= dim;
443 }
444 offset
445}
446
447fn block_offsets_unique_pairwise(
448 dims: &[usize],
449 strides: &[isize],
450 block: &InterleavedBlock,
451) -> bool {
452 let Ok(total) = usize::try_from(block.total) else {
453 return false;
454 };
455 for lhs in 0..total {
456 let lhs_offset = block_offset_for_linear_index(dims, strides, block, lhs);
457 for rhs in (lhs + 1)..total {
458 if block_offset_for_linear_index(dims, strides, block, rhs) == lhs_offset {
459 return false;
460 }
461 }
462 }
463 true
464}
465
466fn validate_injective_layout_inputs(dims: &[usize], strides: &[isize]) -> Option<usize> {
467 if dims.len() != strides.len() {
468 return None;
469 }
470
471 // A zero-sized layout is trivially injective even when the product of its
472 // other extents would overflow.
473 let total = total_len(dims)?;
474 if total <= 1 {
475 return Some(total);
476 }
477 if dims
478 .iter()
479 .zip(strides.iter())
480 .any(|(&dim, &stride)| dim > 1 && stride == 0)
481 {
482 return None;
483 }
484
485 let mut min_offset = 0isize;
486 let mut max_offset = 0isize;
487 for (&dim, &stride) in dims.iter().zip(strides.iter()) {
488 if dim <= 1 {
489 continue;
490 }
491 let extent = isize::try_from(dim - 1).ok()?;
492 let span = stride.checked_mul(extent)?;
493 if span >= 0 {
494 max_offset = max_offset.checked_add(span)?;
495 } else {
496 min_offset = min_offset.checked_add(span)?;
497 }
498 }
499 Some(total)
500}
501
502/// Checked product of extents; `None` on overflow.
503fn total_len(dims: &[usize]) -> Option<usize> {
504 // A zero extent wins before the product, matching the kernel helper: a
505 // zero-sized layout is trivially injective even when its other extents
506 // would overflow.
507 if dims.contains(&0) {
508 return Some(0);
509 }
510 dims.iter()
511 .try_fold(1usize, |acc, &dim| acc.checked_mul(dim))
512}
513
514#[cfg(test)]
515mod tests;