Skip to content

refactor(invariants): simplify finite proof wrappers #134

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
acgetchell merged 1 commit into from
Jun 3, 2026
Merged

refactor(invariants): simplify finite proof wrappers #134

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
48 changes: 48 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,15 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0

- Feat!(matrix): enforce fallible matrix invariants [`e26c283`](https://github.com/acgetchell/la-stack/commit/e26c28358b2358100353b2895441b68892e92cd7)
- Feat!(api): enforce fallible numeric invariants [`adfc33b`](https://github.com/acgetchell/la-stack/commit/adfc33b945b259721bd1067e797ed2e7d4ec0e6e)
- Feat!(matrix): make determinant API tolerance-free [`11a355c`](https://github.com/acgetchell/la-stack/commit/11a355c099eaf366daec8c95af61b6934f914960)
- Feat!(api): hide finite and symmetry proofs behind matrix APIs
[`7219336`](https://github.com/acgetchell/la-stack/commit/721933671c28eb71953f1386a201622d6171caf7)
- Guard public Rust examples against unwrap [`df1130a`](https://github.com/acgetchell/la-stack/commit/df1130a7ad0ba69a1072ef231e14f3efb7e4b8de)

- Add repository-owned Semgrep rules for unwrap and expect usage in public doctests, examples, and benchmarks.
- Add fixture-based Semgrep rule tests and include them in the lint workflow.
- Update examples and benchmarks to model typed fallible flow or operation-labeled benchmark failures.
- Feat!(api): enforce finite Matrix and Vector construction [`92ba403`](https://github.com/acgetchell/la-stack/commit/92ba4034b194875c62a27f24dfbf6d43f380f54e)

### Changed

Expand All @@ -26,6 +35,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
- Reapply "ci: modernize tooling checks and example execution"
[`758321a`](https://github.com/acgetchell/la-stack/commit/758321acf872b1f17286ff3bb7bee6a807e4b440)

- Encode nonzero mantissas in exact decomposition [`7a664ed`](https://github.com/acgetchell/la-stack/commit/7a664ede2f4add168c5813f8d24e16732fa03b30)

- Replace the exact-arithmetic zero mantissa sentinel with `Option<NonZeroU64>`.
- Carry nonzero mantissa proof through matrix/vector decomposition and BigInt scaling.
- Clarify determinant documentation around uncertified `det()` bounds.
- Keep SPD determinant proptests on the tolerance-aware LU path.

### Dependencies

- Bump taiki-e/install-action from 2.75.18 to 2.75.22 [`d6c944b`](https://github.com/acgetchell/la-stack/commit/d6c944bb7dd30bb00dfe820bc355c4351cb1f242)
Expand All @@ -47,6 +63,38 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
- Clarify that la-stack intentionally supports f64 floating-point APIs plus optional exact rationals, not alternate scalar families.
- Add a roadmap covering the v0.4.x stable-Rust issue sequence and the v0.5.0 generic_const_exprs anchor.
- Refresh generated changelog entries and archived changelog grouping.
- Document finite RHS solve validation [`075aed7`](https://github.com/acgetchell/la-stack/commit/075aed78cf8264fc920258f1f1d977ddd589ffd7)

- Document that LU and LDLT solve_vec reject non-finite RHS entries with LaError::NonFinite metadata.
- Cite the Bareiss reference in the exact solve helper docs and describe exact-arithmetic growth and complexity.
- Cover finite proof defaults and non-finite RHS solve boundaries in unit tests.

### Fixed

- Reject overflowed symmetry tolerance scaling [`a7b052a`](https://github.com/acgetchell/la-stack/commit/a7b052af5dc6361198bbfe1e17d6b1f0ba225ed7)

- Enforce the tolerance contract around symmetry checks by surfacing scaled
tolerance overflow as a typed non-finite intermediate error.

- Document finite, non-negative tolerance requirements across tolerance-taking
matrix APIs.

- Add regression coverage for invalid tolerance construction and symmetry
tolerance overflow.

- Update exact examples to propagate typed crate errors instead of unwrapping.
- Harden Semgrep fixture parsing [`ac44c07`](https://github.com/acgetchell/la-stack/commit/ac44c078cc4435d5beca27f1890fbb4046cf5952)

- Ignore non-canonical todoruleid annotations when counting expected rule hits.
- Reject malformed Semgrep JSON results with clear stderr diagnostics instead of propagating KeyError.
- Revalidate finite proof conversions [`419a90f`](https://github.com/acgetchell/la-stack/commit/419a90f7267608051736498154ac5e6faf0909c5)

Ensure internal finite proof conversions cannot accept raw Matrix or Vector storage without checking the invariant.

- Revalidate TryFrom<Matrix<D>> and TryFrom<Vector<D>> before constructing finite wrappers.
- Measure exact random percentile benchmarks over repeated corpus timings and cumulative input sets.
- Tighten Codecov status thresholds and extend benchmark workflow timeout.
- Keep Semgrep constructor fixtures aligned with public API guardrails.

### Maintenance

Expand Down
78 changes: 1 addition & 77 deletions src/exact.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -536,7 +536,7 @@ impl<const D: usize> FiniteMatrix<D> {
}
result[i] = f;
}
Ok(FiniteVector::new_unchecked(Vector::new_unchecked(result)))
Ok(FiniteVector::new(Vector::new_unchecked(result)))
}

/// Exact determinant sign for an already finite matrix.
Expand Down Expand Up @@ -870,18 +870,6 @@ mod tests {
let det = Matrix::<$d>::identity().det_exact().unwrap();
assert_eq!(det, BigRational::from_integer(BigInt::from(1)));
}

#[test]
fn [<det_exact_err_on_nan_ $d d>]() {
let mut m = Matrix::<$d>::identity();
assert_eq!(m.set(0, 0, f64::NAN), Err(LaError::NonFinite { row: Some(0), col: 0 }));
}

#[test]
fn [<det_exact_err_on_inf_ $d d>]() {
let mut m = Matrix::<$d>::identity();
assert_eq!(m.set(0, 0, f64::INFINITY), Err(LaError::NonFinite { row: Some(0), col: 0 }));
}
}
};
}
Expand All @@ -899,12 +887,6 @@ mod tests {
let det = Matrix::<$d>::identity().det_exact_f64().unwrap();
assert!((det - 1.0).abs() <= f64::EPSILON);
}

#[test]
fn [<det_exact_f64_err_on_nan_ $d d>]() {
let mut m = Matrix::<$d>::identity();
assert_eq!(m.set(0, 0, f64::NAN), Err(LaError::NonFinite { row: Some(0), col: 0 }));
}
}
};
}
Expand Down Expand Up @@ -1391,32 +1373,6 @@ mod tests {
assert_eq!(det, BigRational::from_integer(BigInt::from(-1)));
}

/// Non-finite matrix entries surface as `LaError::NonFinite` with the
/// row/col of the first offending entry.
#[test]
fn bareiss_det_int_errs_on_nan() {
let mut m = Matrix::<3>::identity();
assert_eq!(
m.set(1, 2, f64::NAN),
Err(LaError::NonFinite {
row: Some(1),
col: 2
})
);
}

#[test]
fn bareiss_det_int_errs_on_inf() {
let mut m = Matrix::<2>::identity();
assert_eq!(
m.set(0, 0, f64::INFINITY),
Err(LaError::NonFinite {
row: Some(0),
col: 0
})
);
}

/// Per AGENTS.md: dimension-generic tests must cover D=2–5.
macro_rules! gen_bareiss_det_int_identity_tests {
($d:literal) => {
Expand Down Expand Up @@ -1639,32 +1595,6 @@ mod tests {
}
}

#[test]
fn [<solve_exact_err_on_nan_matrix_ $d d>]() {
let mut a = Matrix::<$d>::identity();
assert_eq!(a.set(0, 0, f64::NAN), Err(LaError::NonFinite { row: Some(0), col: 0 }));
}

#[test]
fn [<solve_exact_err_on_inf_matrix_ $d d>]() {
let mut a = Matrix::<$d>::identity();
assert_eq!(a.set(0, 0, f64::INFINITY), Err(LaError::NonFinite { row: Some(0), col: 0 }));
}

#[test]
fn [<solve_exact_err_on_nan_vector_ $d d>]() {
let mut b_arr = [1.0f64; $d];
b_arr[0] = f64::NAN;
assert_eq!(Vector::<$d>::try_new(b_arr), Err(LaError::NonFinite { row: None, col: 0 }));
}

#[test]
fn [<solve_exact_err_on_inf_vector_ $d d>]() {
let mut b_arr = [1.0f64; $d];
b_arr[$d - 1] = f64::INFINITY;
assert_eq!(Vector::<$d>::try_new(b_arr), Err(LaError::NonFinite { row: None, col: $d - 1 }));
}

#[test]
fn [<solve_exact_singular_ $d d>]() {
// Zero matrix is singular.
Expand Down Expand Up @@ -1693,12 +1623,6 @@ mod tests {
assert!((x[i] - b.data[i]).abs() <= f64::EPSILON);
}
}

#[test]
fn [<solve_exact_f64_err_on_nan_ $d d>]() {
let mut a = Matrix::<$d>::identity();
assert_eq!(a.set(0, 0, f64::NAN), Err(LaError::NonFinite { row: Some(0), col: 0 }));
}
}
};
}
Expand Down
2 changes: 1 addition & 1 deletion src/ldlt.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -264,7 +264,7 @@ impl<const D: usize> Ldlt<D> {
ii += 1;
}

Ok(FiniteVector::new_unchecked(Vector::new_unchecked(x)))
Ok(FiniteVector::new(Vector::new_unchecked(x)))
}
}

Expand Down
2 changes: 1 addition & 1 deletion src/lu.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -217,7 +217,7 @@ impl<const D: usize> Lu<D> {
ii += 1;
}

Ok(FiniteVector::new_unchecked(Vector::new_unchecked(x)))
Ok(FiniteVector::new(Vector::new_unchecked(x)))
}

/// Determinant of the original matrix.
Expand Down
16 changes: 3 additions & 13 deletions src/matrix.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,21 +26,11 @@ pub(crate) struct FiniteMatrix<const D: usize> {
}

impl<const D: usize> FiniteMatrix<D> {
/// Construct a finite matrix without checking the invariant.
///
/// This is crate-internal so raw storage still goes through
/// [`Matrix::try_from_rows`], which preserves diagnostics for rejected
/// entries.
#[inline]
pub(crate) const fn new_unchecked(matrix: Matrix<D>) -> Self {
Self { matrix }
}

/// Wrap an already-finite matrix for algorithms that carry the invariant
/// explicitly.
#[inline]
pub const fn new(matrix: Matrix<D>) -> Self {
Self::new_unchecked(matrix)
Self { matrix }
Comment on lines 32 to +33
Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai Bot Jun 3, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major | 🏗️ Heavy lift

FiniteMatrix::new no longer distinguishes checked from unchecked construction.

Matrix::from_rows_unchecked(...) still exists, but FiniteMatrix::new(...) now just wraps the raw matrix. So the proof wrapper can still be built from unchecked storage, and the public algorithm helpers below (inf_norm, lu, ldlt, det*) are not actually entering through a validated boundary.

Suggested direction 
- pub const fn new(matrix: Matrix<D>) -> Self {
-     Self { matrix }
+ pub const fn new(matrix: Matrix<D>) -> Result<Self, LaError> {
+     if let Some((row, col)) = Matrix::<D>::first_non_finite_cell_in(&matrix.rows) {
+         return Err(LaError::non_finite_cell(row, col));
+     }
+     Ok(Self { matrix })
  }

If some internal paths genuinely have a local finiteness proof, keep an explicitly named private unchecked constructor for those sites rather than making new(...) silently unchecked.

As per coding guidelines, "Non-finite values (NaN, ±∞) always surface as LaError::NonFinite { row, col } with source-location metadata. No silent NaN propagation, no unwrap_or(f64::NAN)."

🤖 Prompt for AI Agents 
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@src/matrix.rs` around lines 32 - 33, FiniteMatrix::new currently accepts a
raw Matrix and thus silently allows unchecked (possibly non-finite) storage;
change the API so new is a checked constructor (validate finiteness) and restore
an explicit private unchecked constructor for internal use. Specifically: make
FiniteMatrix::new(Matrix<D>) perform the finiteness check and return a
Result<FiniteMatrix, LaError> that emits LaError::NonFinite { row, col } (with
source-location metadata) on NaN/±∞, and add a clearly named private fn
new_unchecked(matrix: Matrix<D>) -> Self for internal callers that already prove
finiteness; update call sites that relied on the old unchecked behavior to call
new_unchecked only when a local proof exists and call new(...) everywhere else.

}

/// Validate raw row-major storage and construct a finite matrix.
Expand All @@ -50,15 +40,15 @@ impl<const D: usize> FiniteMatrix<D> {
#[inline]
pub const fn from_rows(rows: [[f64; D]; D]) -> Result<Self, LaError> {
match Matrix::try_from_rows(rows) {
Ok(matrix) => Ok(Self::new_unchecked(matrix)),
Ok(matrix) => Ok(Self::new(matrix)),
Err(err) => Err(err),
}
}

/// All-zeros finite matrix.
#[inline]
pub const fn zero() -> Self {
Self::new_unchecked(Matrix::zero())
Self::new(Matrix::zero())
}

/// Consume the wrapper and return the underlying raw matrix.
Expand Down
15 changes: 3 additions & 12 deletions src/vector.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,20 +22,11 @@ pub(crate) struct FiniteVector<const D: usize> {
}

impl<const D: usize> FiniteVector<D> {
/// Construct a finite vector without checking the invariant.
///
/// This is crate-internal so raw storage still goes through
/// [`Vector::try_new`], which preserves diagnostics for rejected entries.
#[inline]
pub(crate) const fn new_unchecked(vector: Vector<D>) -> Self {
Self { vector }
}

/// Wrap an already-finite vector for algorithms that carry the invariant
/// explicitly.
#[inline]
pub const fn new(vector: Vector<D>) -> Self {
Self::new_unchecked(vector)
Self { vector }
Comment on lines 28 to +29
Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai Bot Jun 3, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major | 🏗️ Heavy lift

FiniteVector::new is still an unchecked proof constructor.

This now just rewraps Vector<D>, so every call site switched from new_unchecked(...) to new(...) still accepts Vector::new_unchecked(...) without surfacing LaError::NonFinite. That means the validated-construction invariant is not actually enforced in the updated LU/LDLT/exact solve paths.

Suggested direction 
- pub const fn new(vector: Vector<D>) -> Self {
-     Self { vector }
+ pub const fn new(vector: Vector<D>) -> Result<Self, LaError> {
+     let mut i = 0;
+     while i < D {
+         if !vector.data[i].is_finite() {
+             return Err(LaError::non_finite_at(i));
+         }
+         i += 1;
+     }
+     Ok(Self { vector })
  }

If you still need a bypass for locally-proven outputs, keep a clearly named private new_unchecked(...) alongside the checked constructor instead of collapsing them into one infallible new(...).

As per coding guidelines, "Non-finite values (NaN, ±∞) always surface as LaError::NonFinite { row, col } with source-location metadata. No silent NaN propagation, no unwrap_or(f64::NAN)."

🤖 Prompt for AI Agents 
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@src/vector.rs` around lines 28 - 29, FiniteVector::new currently just wraps
Vector<D> and removes the finiteness check, allowing Vector::new_unchecked(...)
to silently pass non-finite values; restore a checked public constructor that
validates all entries and returns LaError::NonFinite with source-location
metadata on failure, and keep a clearly named private bypass (e.g.,
FiniteVector::new_unchecked) for internal use where you have a local proof.
Update call sites in LU/LDLT/exact solve paths to use the public checked
constructor (or explicitly call the private unchecked where justified) and
ensure any creation that can fail surfaces LaError::NonFinite { row, col }
rather than panicking or producing NaN.

}

/// Validate raw vector storage and construct a finite vector.
Expand All @@ -45,15 +36,15 @@ impl<const D: usize> FiniteVector<D> {
#[inline]
pub const fn from_array(data: [f64; D]) -> Result<Self, LaError> {
match Vector::try_new(data) {
Ok(vector) => Ok(Self::new_unchecked(vector)),
Ok(vector) => Ok(Self::new(vector)),
Err(err) => Err(err),
}
}

/// All-zeros finite vector.
#[inline]
pub const fn zero() -> Self {
Self::new_unchecked(Vector::zero())
Self::new(Vector::zero())
}

/// Consume the wrapper and return the underlying raw vector.
Expand Down
Loading