ferrolearn_sparse/
csc.rs

1//! Compressed Sparse Column (CSC) matrix format.
2//!
3//! [`CscMatrix<T>`] is a newtype wrapper around [`sprs::CsMat<T>`] in CSC
4//! storage. CSC matrices are efficient for column-wise operations and are the
5//! natural choice when algorithms need to iterate over columns.
6
7use std::ops::{Add, AddAssign, Mul, MulAssign};
8
9use ferrolearn_core::FerroError;
10use ndarray::{Array1, Array2, ArrayView2};
11use num_traits::Zero;
12use sprs::CsMat;
13
14use crate::coo::CooMatrix;
15use crate::csr::CsrMatrix;
16
17/// Compressed Sparse Column (CSC) sparse matrix.
18///
19/// Stores non-zero entries in column-major order using three arrays: `indptr`
20/// (column pointer array of length `n_cols + 1`), `indices` (row indices of
21/// each non-zero), and `data` (values of each non-zero).
22///
23/// # Type Parameter
24///
25/// `T` — the scalar element type.
26#[derive(Debug, Clone)]
27pub struct CscMatrix<T> {
28    inner: CsMat<T>,
29}
30
31impl<T> CscMatrix<T>
32where
33    T: Clone,
34{
35    /// Construct a CSC matrix from raw components.
36    ///
37    /// # Arguments
38    ///
39    /// * `n_rows` — number of rows.
40    /// * `n_cols` — number of columns.
41    /// * `indptr` — column pointer array of length `n_cols + 1`.
42    /// * `indices` — row index of each non-zero entry.
43    /// * `data` — value of each non-zero entry.
44    ///
45    /// # Errors
46    ///
47    /// Returns [`FerroError::InvalidParameter`] if the data is structurally
48    /// invalid (wrong lengths, out-of-bound indices, unsorted inner indices).
49    pub fn new(
50        n_rows: usize,
51        n_cols: usize,
52        indptr: Vec<usize>,
53        indices: Vec<usize>,
54        data: Vec<T>,
55    ) -> Result<Self, FerroError> {
56        CsMat::try_new_csc((n_rows, n_cols), indptr, indices, data)
57            .map(|inner| Self { inner })
58            .map_err(|(_, _, _, err)| FerroError::InvalidParameter {
59                name: "CscMatrix raw components".into(),
60                reason: err.to_string(),
61            })
62    }
63
64    /// Build a [`CscMatrix`] from a pre-validated [`sprs::CsMat<T>`] in CSC storage.
65    ///
66    /// This is used internally for format conversions.
67    pub(crate) fn from_inner(inner: CsMat<T>) -> Self {
68        debug_assert!(inner.is_csc(), "inner matrix must be in CSC storage");
69        Self { inner }
70    }
71
72    /// Returns the number of rows.
73    pub fn n_rows(&self) -> usize {
74        self.inner.rows()
75    }
76
77    /// Returns the number of columns.
78    pub fn n_cols(&self) -> usize {
79        self.inner.cols()
80    }
81
82    /// Returns the number of stored non-zero entries.
83    pub fn nnz(&self) -> usize {
84        self.inner.nnz()
85    }
86
87    /// Returns a reference to the underlying [`sprs::CsMat<T>`].
88    pub fn inner(&self) -> &CsMat<T> {
89        &self.inner
90    }
91
92    /// Consume this matrix and return the underlying [`sprs::CsMat<T>`].
93    pub fn into_inner(self) -> CsMat<T> {
94        self.inner
95    }
96
97    /// Construct a [`CscMatrix`] from a [`CooMatrix`] by converting to CSC.
98    ///
99    /// Duplicate entries at the same position are summed.
100    ///
101    /// # Errors
102    ///
103    /// This conversion is always successful for structurally valid inputs.
104    pub fn from_coo(coo: &CooMatrix<T>) -> Result<Self, FerroError>
105    where
106        T: Clone + Add<Output = T> + 'static,
107    {
108        let inner: CsMat<T> = coo.inner().to_csc();
109        Ok(Self { inner })
110    }
111
112    /// Construct a [`CscMatrix`] from a [`CsrMatrix`].
113    ///
114    /// # Errors
115    ///
116    /// This conversion is always successful.
117    pub fn from_csr(csr: &CsrMatrix<T>) -> Result<Self, FerroError>
118    where
119        T: Clone + Default + 'static,
120    {
121        Ok(csr.to_csc())
122    }
123
124    /// Convert to [`CsrMatrix`].
125    pub fn to_csr(&self) -> CsrMatrix<T>
126    where
127        T: Clone + Default + 'static,
128    {
129        // from_csc is infallible for a valid CscMatrix
130        CsrMatrix::from_csc(self).unwrap()
131    }
132
133    /// Convert to [`CooMatrix`].
134    pub fn to_coo(&self) -> CooMatrix<T> {
135        let mut coo = CooMatrix::with_capacity(self.n_rows(), self.n_cols(), self.nnz());
136        for (val, (r, c)) in self.inner.iter() {
137            // indices come from a valid matrix, so push is infallible here
138            let _ = coo.push(r, c, val.clone());
139        }
140        coo
141    }
142
143    /// Convert this sparse matrix to a dense [`Array2<T>`].
144    pub fn to_dense(&self) -> Array2<T>
145    where
146        T: Clone + Zero + 'static,
147    {
148        self.inner.to_dense()
149    }
150
151    /// Construct a [`CscMatrix`] from a dense [`Array2<T>`], dropping entries
152    /// whose absolute value is less than or equal to `epsilon`.
153    pub fn from_dense(dense: &ArrayView2<'_, T>, epsilon: T) -> Self
154    where
155        T: Copy + Zero + PartialOrd + num_traits::Signed + 'static,
156    {
157        let inner = CsMat::csc_from_dense(dense.view(), epsilon);
158        Self { inner }
159    }
160
161    /// Return a new CSC matrix containing only the columns in `start..end`.
162    ///
163    /// # Errors
164    ///
165    /// Returns [`FerroError::InvalidParameter`] if `start > end` or
166    /// `end > n_cols()`.
167    pub fn col_slice(&self, start: usize, end: usize) -> Result<CscMatrix<T>, FerroError>
168    where
169        T: Clone + Default + 'static,
170    {
171        if start > end {
172            return Err(FerroError::InvalidParameter {
173                name: "col_slice range".into(),
174                reason: format!("start ({start}) must be <= end ({end})"),
175            });
176        }
177        if end > self.n_cols() {
178            return Err(FerroError::InvalidParameter {
179                name: "col_slice range".into(),
180                reason: format!("end ({end}) exceeds n_cols ({})", self.n_cols()),
181            });
182        }
183        let view = self.inner.slice_outer(start..end);
184        Ok(Self {
185            inner: view.to_owned(),
186        })
187    }
188
189    /// Scalar multiplication in-place: multiplies every non-zero by `scalar`.
190    ///
191    /// Requires `T: for<'r> MulAssign<&'r T>`, which is satisfied by all
192    /// primitive numeric types.
193    pub fn scale(&mut self, scalar: T)
194    where
195        for<'r> T: MulAssign<&'r T>,
196    {
197        self.inner.scale(scalar);
198    }
199
200    /// Scalar multiplication returning a new matrix.
201    pub fn mul_scalar(&self, scalar: T) -> CscMatrix<T>
202    where
203        T: Copy + Mul<Output = T> + Zero + 'static,
204    {
205        let new_inner = self.inner.map(|&v| v * scalar);
206        Self { inner: new_inner }
207    }
208
209    /// Element-wise addition of two CSC matrices with the same shape.
210    ///
211    /// # Errors
212    ///
213    /// Returns [`FerroError::ShapeMismatch`] if the matrices have different shapes.
214    pub fn add(&self, rhs: &CscMatrix<T>) -> Result<CscMatrix<T>, FerroError>
215    where
216        T: Zero + Default + Clone + 'static,
217        for<'r> &'r T: Add<&'r T, Output = T>,
218    {
219        if self.n_rows() != rhs.n_rows() || self.n_cols() != rhs.n_cols() {
220            return Err(FerroError::ShapeMismatch {
221                expected: vec![self.n_rows(), self.n_cols()],
222                actual: vec![rhs.n_rows(), rhs.n_cols()],
223                context: "CscMatrix::add".into(),
224            });
225        }
226        let result = &self.inner + &rhs.inner;
227        Ok(Self { inner: result })
228    }
229
230    /// Sparse matrix-dense vector product: computes `self * rhs`.
231    ///
232    /// # Errors
233    ///
234    /// Returns [`FerroError::ShapeMismatch`] if `rhs.len() != n_cols()`.
235    pub fn mul_vec(&self, rhs: &Array1<T>) -> Result<Array1<T>, FerroError>
236    where
237        T: Clone + Zero + 'static,
238        for<'r> &'r T: Mul<Output = T>,
239        T: AddAssign,
240    {
241        if rhs.len() != self.n_cols() {
242            return Err(FerroError::ShapeMismatch {
243                expected: vec![self.n_cols()],
244                actual: vec![rhs.len()],
245                context: "CscMatrix::mul_vec".into(),
246            });
247        }
248        let result = &self.inner * rhs;
249        Ok(result)
250    }
251}
252
253#[cfg(test)]
254mod tests {
255    use super::*;
256    use approx::assert_abs_diff_eq;
257    use ndarray::array;
258
259    fn sample_csc() -> CscMatrix<f64> {
260        // 3x3 sparse matrix (same logical matrix as CsrMatrix tests):
261        // [1 0 2]
262        // [0 3 0]
263        // [4 0 5]
264        //
265        // CSC indptr is per-column:
266        //   col 0: rows 0, 2  → values 1, 4
267        //   col 1: row 1      → value 3
268        //   col 2: rows 0, 2  → values 2, 5
269        CscMatrix::new(
270            3,
271            3,
272            vec![0, 2, 3, 5],
273            vec![0, 2, 1, 0, 2],
274            vec![1.0, 4.0, 3.0, 2.0, 5.0],
275        )
276        .unwrap()
277    }
278
279    #[test]
280    fn test_new_valid() {
281        let m = sample_csc();
282        assert_eq!(m.n_rows(), 3);
283        assert_eq!(m.n_cols(), 3);
284        assert_eq!(m.nnz(), 5);
285    }
286
287    #[test]
288    fn test_to_dense() {
289        let m = sample_csc();
290        let d = m.to_dense();
291        assert_abs_diff_eq!(d[[0, 0]], 1.0);
292        assert_abs_diff_eq!(d[[0, 2]], 2.0);
293        assert_abs_diff_eq!(d[[1, 1]], 3.0);
294        assert_abs_diff_eq!(d[[2, 0]], 4.0);
295        assert_abs_diff_eq!(d[[2, 2]], 5.0);
296    }
297
298    #[test]
299    fn test_from_dense() {
300        let dense = array![[1.0_f64, 0.0], [0.0, 2.0]];
301        let m = CscMatrix::from_dense(&dense.view(), 0.0);
302        assert_eq!(m.nnz(), 2);
303        let back = m.to_dense();
304        assert_abs_diff_eq!(back[[0, 0]], 1.0);
305        assert_abs_diff_eq!(back[[1, 1]], 2.0);
306    }
307
308    #[test]
309    fn test_from_coo_roundtrip() {
310        let mut coo: CooMatrix<f64> = CooMatrix::new(3, 3);
311        coo.push(0, 0, 1.0).unwrap();
312        coo.push(1, 2, 4.0).unwrap();
313        coo.push(2, 1, 7.0).unwrap();
314        let csc = CscMatrix::from_coo(&coo).unwrap();
315        let dense = csc.to_dense();
316        assert_abs_diff_eq!(dense[[0, 0]], 1.0);
317        assert_abs_diff_eq!(dense[[1, 2]], 4.0);
318        assert_abs_diff_eq!(dense[[2, 1]], 7.0);
319    }
320
321    #[test]
322    fn test_csc_csr_roundtrip() {
323        let csc = sample_csc();
324        let csr = csc.to_csr();
325        let back = CscMatrix::from_csr(&csr).unwrap();
326        assert_eq!(back.to_dense(), csc.to_dense());
327    }
328
329    #[test]
330    fn test_col_slice() {
331        let m = sample_csc();
332        let sliced = m.col_slice(0, 2).unwrap();
333        assert_eq!(sliced.n_rows(), 3);
334        assert_eq!(sliced.n_cols(), 2);
335        let d = sliced.to_dense();
336        assert_abs_diff_eq!(d[[0, 0]], 1.0);
337        assert_abs_diff_eq!(d[[1, 1]], 3.0);
338    }
339
340    #[test]
341    fn test_col_slice_empty() {
342        let m = sample_csc();
343        let sliced = m.col_slice(1, 1).unwrap();
344        assert_eq!(sliced.n_cols(), 0);
345    }
346
347    #[test]
348    fn test_col_slice_invalid() {
349        let m = sample_csc();
350        assert!(m.col_slice(2, 1).is_err());
351        assert!(m.col_slice(0, 4).is_err());
352    }
353
354    #[test]
355    fn test_mul_scalar() {
356        let m = sample_csc();
357        let m2 = m.mul_scalar(2.0);
358        let d = m2.to_dense();
359        assert_abs_diff_eq!(d[[0, 0]], 2.0);
360        assert_abs_diff_eq!(d[[1, 1]], 6.0);
361    }
362
363    #[test]
364    fn test_scale_in_place() {
365        let mut m = sample_csc();
366        m.scale(3.0);
367        let d = m.to_dense();
368        assert_abs_diff_eq!(d[[0, 0]], 3.0);
369        assert_abs_diff_eq!(d[[2, 2]], 15.0);
370    }
371
372    #[test]
373    fn test_add() {
374        let m = sample_csc();
375        let sum = m.add(&m).unwrap();
376        let d = sum.to_dense();
377        assert_abs_diff_eq!(d[[0, 0]], 2.0);
378        assert_abs_diff_eq!(d[[1, 1]], 6.0);
379    }
380
381    #[test]
382    fn test_add_shape_mismatch() {
383        let m1 = sample_csc();
384        let m2 = CscMatrix::new(2, 3, vec![0, 0, 0, 0], vec![], vec![]).unwrap();
385        assert!(m1.add(&m2).is_err());
386    }
387
388    #[test]
389    fn test_mul_vec() {
390        let m = sample_csc();
391        let v = Array1::from(vec![1.0_f64, 2.0, 3.0]);
392        let result = m.mul_vec(&v).unwrap();
393        assert_abs_diff_eq!(result[0], 7.0);
394        assert_abs_diff_eq!(result[1], 6.0);
395        assert_abs_diff_eq!(result[2], 19.0);
396    }
397
398    #[test]
399    fn test_mul_vec_shape_mismatch() {
400        let m = sample_csc();
401        let v = Array1::from(vec![1.0_f64, 2.0]);
402        assert!(m.mul_vec(&v).is_err());
403    }
404}
405
406/// Kani proof harnesses for CscMatrix structural invariants.
407///
408/// These proofs verify that after construction via `new()`, `from_coo()`, and
409/// `add()`, the underlying CSC representation satisfies all structural
410/// invariants:
411///
412/// - `indptr.len() == n_cols + 1`
413/// - `indptr` is monotonically non-decreasing
414/// - All row indices are less than `n_rows`
415/// - `indices.len() == data.len()`
416///
417/// All proofs use small symbolic bounds (at most 3 rows/cols) because sparse
418/// matrix verification is computationally expensive for Kani.
419#[cfg(kani)]
420mod kani_proofs {
421    use super::*;
422    use crate::coo::CooMatrix;
423
424    /// Maximum dimension for symbolic exploration.
425    const MAX_DIM: usize = 3;
426
427    /// Helper: assert all CSC structural invariants on the inner `CsMat`.
428    fn assert_csc_invariants<T>(m: &CscMatrix<T>) {
429        let inner = m.inner();
430
431        // Invariant 1: indptr length == n_cols + 1
432        let indptr = inner.indptr();
433        let indptr_raw = indptr.raw_storage();
434        assert!(indptr_raw.len() == m.n_cols() + 1);
435
436        // Invariant 2: indptr is monotonically non-decreasing
437        for i in 0..m.n_cols() {
438            assert!(indptr_raw[i] <= indptr_raw[i + 1]);
439        }
440
441        // Invariant 3: all row indices < n_rows
442        let indices = inner.indices();
443        for &row_idx in indices {
444            assert!(row_idx < m.n_rows());
445        }
446
447        // Invariant 4: indices.len() == data.len()
448        assert!(inner.indices().len() == inner.data().len());
449    }
450
451    /// Verify `indptr.len() == n_cols + 1` after `new()` with a symbolic
452    /// empty matrix of arbitrary dimensions.
453    #[kani::proof]
454    #[kani::unwind(5)]
455    fn csc_new_indptr_length() {
456        let n_rows: usize = kani::any();
457        let n_cols: usize = kani::any();
458        kani::assume(n_rows > 0 && n_rows <= MAX_DIM);
459        kani::assume(n_cols > 0 && n_cols <= MAX_DIM);
460
461        // Build a valid empty CSC matrix
462        let indptr = vec![0usize; n_cols + 1];
463        let indices: Vec<usize> = vec![];
464        let data: Vec<i32> = vec![];
465
466        if let Ok(m) = CscMatrix::new(n_rows, n_cols, indptr, indices, data) {
467            let inner_indptr = m.inner().indptr();
468            assert!(inner_indptr.raw_storage().len() == n_cols + 1);
469        }
470    }
471
472    /// Verify indptr monotonicity after `new()` with a symbolic single-entry
473    /// matrix.
474    #[kani::proof]
475    #[kani::unwind(5)]
476    fn csc_new_indptr_monotonic() {
477        let n_rows: usize = kani::any();
478        let n_cols: usize = kani::any();
479        kani::assume(n_rows > 0 && n_rows <= MAX_DIM);
480        kani::assume(n_cols > 0 && n_cols <= MAX_DIM);
481
482        // Place a single non-zero at a symbolic valid position
483        let row: usize = kani::any();
484        let col: usize = kani::any();
485        kani::assume(row < n_rows);
486        kani::assume(col < n_cols);
487
488        // Build indptr for a single entry in column `col`
489        let mut indptr = vec![0usize; n_cols + 1];
490        for i in (col + 1)..=n_cols {
491            indptr[i] = 1;
492        }
493        let indices = vec![row];
494        let data = vec![42i32];
495
496        if let Ok(m) = CscMatrix::new(n_rows, n_cols, indptr, indices, data) {
497            let inner_indptr = m.inner().indptr().raw_storage().to_vec();
498            for i in 0..m.n_cols() {
499                assert!(inner_indptr[i] <= inner_indptr[i + 1]);
500            }
501        }
502    }
503
504    /// Verify all row indices < n_rows after `new()`.
505    #[kani::proof]
506    #[kani::unwind(5)]
507    fn csc_new_row_indices_in_bounds() {
508        let n_rows: usize = kani::any();
509        let n_cols: usize = kani::any();
510        kani::assume(n_rows > 0 && n_rows <= MAX_DIM);
511        kani::assume(n_cols > 0 && n_cols <= MAX_DIM);
512
513        let row: usize = kani::any();
514        let col: usize = kani::any();
515        kani::assume(row < n_rows);
516        kani::assume(col < n_cols);
517
518        let mut indptr = vec![0usize; n_cols + 1];
519        for i in (col + 1)..=n_cols {
520            indptr[i] = 1;
521        }
522        let indices = vec![row];
523        let data = vec![1i32];
524
525        if let Ok(m) = CscMatrix::new(n_rows, n_cols, indptr, indices, data) {
526            for &r in m.inner().indices() {
527                assert!(r < m.n_rows());
528            }
529        }
530    }
531
532    /// Verify `indices.len() == data.len()` after `new()`.
533    #[kani::proof]
534    #[kani::unwind(5)]
535    fn csc_new_indices_data_same_length() {
536        let n_rows: usize = kani::any();
537        let n_cols: usize = kani::any();
538        kani::assume(n_rows > 0 && n_rows <= MAX_DIM);
539        kani::assume(n_cols > 0 && n_cols <= MAX_DIM);
540
541        let indptr = vec![0usize; n_cols + 1];
542        let indices: Vec<usize> = vec![];
543        let data: Vec<i32> = vec![];
544
545        if let Ok(m) = CscMatrix::new(n_rows, n_cols, indptr, indices, data) {
546            assert!(m.inner().indices().len() == m.inner().data().len());
547        }
548    }
549
550    /// Verify that `new()` rejects inputs where indices and data have
551    /// mismatched lengths.
552    #[kani::proof]
553    #[kani::unwind(5)]
554    fn csc_new_rejects_mismatched_lengths() {
555        let n_rows: usize = kani::any();
556        let n_cols: usize = kani::any();
557        kani::assume(n_rows > 0 && n_rows <= MAX_DIM);
558        kani::assume(n_cols > 0 && n_cols <= MAX_DIM);
559
560        // indices has 1 element, data has 0 — must fail
561        let indptr = vec![0usize; n_cols + 1];
562        let indices = vec![0usize];
563        let data: Vec<i32> = vec![];
564
565        let result = CscMatrix::new(n_rows, n_cols, indptr, indices, data);
566        assert!(result.is_err());
567    }
568
569    /// Verify all structural invariants after `from_coo()` with symbolic
570    /// entries.
571    #[kani::proof]
572    #[kani::unwind(5)]
573    fn csc_from_coo_invariants() {
574        let n_rows: usize = kani::any();
575        let n_cols: usize = kani::any();
576        kani::assume(n_rows > 0 && n_rows <= MAX_DIM);
577        kani::assume(n_cols > 0 && n_cols <= MAX_DIM);
578
579        let mut coo = CooMatrix::<i32>::new(n_rows, n_cols);
580
581        // Insert a symbolic number of entries (0 or 1)
582        let do_insert: bool = kani::any();
583        if do_insert {
584            let row: usize = kani::any();
585            let col: usize = kani::any();
586            kani::assume(row < n_rows);
587            kani::assume(col < n_cols);
588            let _ = coo.push(row, col, 1i32);
589        }
590
591        if let Ok(csc) = CscMatrix::from_coo(&coo) {
592            assert_csc_invariants(&csc);
593            assert!(csc.n_rows() == n_rows);
594            assert!(csc.n_cols() == n_cols);
595        }
596    }
597
598    /// Verify that `add()` preserves shape and structural invariants.
599    #[kani::proof]
600    #[kani::unwind(5)]
601    fn csc_add_preserves_invariants() {
602        let n_rows: usize = kani::any();
603        let n_cols: usize = kani::any();
604        kani::assume(n_rows > 0 && n_rows <= MAX_DIM);
605        kani::assume(n_cols > 0 && n_cols <= MAX_DIM);
606
607        // Build two valid empty CSC matrices of the same shape
608        let indptr = vec![0usize; n_cols + 1];
609        let a = CscMatrix::<i32>::new(n_rows, n_cols, indptr.clone(), vec![], vec![]);
610        let b = CscMatrix::<i32>::new(n_rows, n_cols, indptr, vec![], vec![]);
611
612        if let (Ok(a), Ok(b)) = (a, b) {
613            if let Ok(sum) = a.add(&b) {
614                // Shape is preserved
615                assert!(sum.n_rows() == n_rows);
616                assert!(sum.n_cols() == n_cols);
617                // Structural invariants hold
618                assert_csc_invariants(&sum);
619            }
620        }
621    }
622
623    /// Verify that `add()` with non-empty matrices preserves invariants.
624    #[kani::proof]
625    #[kani::unwind(5)]
626    fn csc_add_nonempty_preserves_invariants() {
627        // Fixed 2x2 matrices with one entry each in different columns
628        let a = CscMatrix::<i32>::new(2, 2, vec![0, 1, 1], vec![0], vec![1]);
629        let b = CscMatrix::<i32>::new(2, 2, vec![0, 0, 1], vec![1], vec![2]);
630
631        if let (Ok(a), Ok(b)) = (a, b) {
632            if let Ok(sum) = a.add(&b) {
633                assert!(sum.n_rows() == 2);
634                assert!(sum.n_cols() == 2);
635                assert_csc_invariants(&sum);
636            }
637        }
638    }
639
640    /// Verify `mul_vec()` output has correct dimension and does not panic.
641    #[kani::proof]
642    #[kani::unwind(5)]
643    fn csc_mul_vec_output_dimension() {
644        let n_rows: usize = kani::any();
645        let n_cols: usize = kani::any();
646        kani::assume(n_rows > 0 && n_rows <= MAX_DIM);
647        kani::assume(n_cols > 0 && n_cols <= MAX_DIM);
648
649        // Empty matrix for tractable verification
650        let indptr = vec![0usize; n_cols + 1];
651        let m = CscMatrix::<f64>::new(n_rows, n_cols, indptr, vec![], vec![]);
652
653        if let Ok(m) = m {
654            let v = Array1::<f64>::zeros(n_cols);
655            if let Ok(result) = m.mul_vec(&v) {
656                assert!(result.len() == n_rows);
657            }
658        }
659    }
660
661    /// Verify `mul_vec()` rejects vectors of wrong dimension.
662    #[kani::proof]
663    #[kani::unwind(5)]
664    fn csc_mul_vec_rejects_wrong_dimension() {
665        let n_rows: usize = kani::any();
666        let n_cols: usize = kani::any();
667        kani::assume(n_rows > 0 && n_rows <= MAX_DIM);
668        kani::assume(n_cols > 0 && n_cols <= MAX_DIM);
669
670        let indptr = vec![0usize; n_cols + 1];
671        let m = CscMatrix::<f64>::new(n_rows, n_cols, indptr, vec![], vec![]);
672
673        if let Ok(m) = m {
674            let wrong_len: usize = kani::any();
675            kani::assume(wrong_len <= MAX_DIM);
676            kani::assume(wrong_len != n_cols);
677            let v = Array1::<f64>::zeros(wrong_len);
678            let result = m.mul_vec(&v);
679            assert!(result.is_err());
680        }
681    }
682
683    /// Verify `mul_vec()` with a non-empty matrix produces the correct
684    /// output dimension and does not trigger any out-of-bounds access.
685    #[kani::proof]
686    #[kani::unwind(5)]
687    fn csc_mul_vec_nonempty_no_oob() {
688        // 2x3 CSC matrix with entries at (0,1) and (1,2)
689        // Column 0: empty, Column 1: row 0, Column 2: row 1
690        let m = CscMatrix::<f64>::new(2, 3, vec![0, 0, 1, 2], vec![0, 1], vec![3.0, 4.0]);
691        if let Ok(m) = m {
692            let v = Array1::from(vec![1.0, 2.0, 3.0]);
693            if let Ok(result) = m.mul_vec(&v) {
694                assert!(result.len() == 2);
695            }
696        }
697    }
698}
ferrolearn_sparse/csc.rs

ferrolearn_sparse/
csc.rs
