refactor(invariants): simplify finite proof wrappers#134
Conversation
- Use the checked proof-wrapper constructors as the single internal path for finite matrices and vectors. - Remove exact-arithmetic tests that duplicated the matrix and vector non-finite boundary checks.
📝 WalkthroughWalkthroughThis PR enforces validated construction of finite-proof wrappers by removing internal unchecked constructors and routing all FiniteVector and FiniteMatrix instances through checked ChangesFinite-proof validation enforcement
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~20 minutes Possibly related PRs
Suggested labels
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #134 +/- ##
==========================================
- Coverage 99.31% 99.29% -0.02%
==========================================
Files 5 5
Lines 2757 2707 -50
==========================================
- Hits 2738 2688 -50
Misses 19 19
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
CHANGELOG.md (1)
14-97:⚠️ Potential issue | 🟠 Major | ⚡ Quick winDo not edit
CHANGELOG.mdmanually; regenerate it via project tooling.This block appears to be directly edited in
CHANGELOG.md, which violates the repo rule for changelog generation. Please revert manual edits and regenerate withjust changelog(orjust changelog-unreleased <version>for unreleased prepends).As per coding guidelines: "Never edit
CHANGELOG.mddirectly - it's auto-generated from git commits. Usejust changelogto regenerate orjust changelog-unreleased <version>to prepend unreleased changes."🤖 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 `@CHANGELOG.md` around lines 14 - 97, The PR contains a manual edit to CHANGELOG.md (don't edit changelogs by hand); revert the manual changes to CHANGELOG.md (undo the commit or remove the file modification from the branch) and regenerate the changelog using the project tooling: run just changelog to rebuild from commits or just changelog-unreleased <version> if you need to prepend an unreleased entry, then commit the generated file instead of the manual edits.
🤖 Prompt for all review comments with 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.
Inline comments:
In `@src/matrix.rs`:
- Around line 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.
In `@src/vector.rs`:
- Around line 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.
---
Outside diff comments:
In `@CHANGELOG.md`:
- Around line 14-97: The PR contains a manual edit to CHANGELOG.md (don't edit
changelogs by hand); revert the manual changes to CHANGELOG.md (undo the commit
or remove the file modification from the branch) and regenerate the changelog
using the project tooling: run just changelog to rebuild from commits or just
changelog-unreleased <version> if you need to prepend an unreleased entry, then
commit the generated file instead of the manual edits.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: 4913b7f8-21b0-4176-a587-4510d1faa97f
📒 Files selected for processing (6)
CHANGELOG.mdsrc/exact.rssrc/ldlt.rssrc/lu.rssrc/matrix.rssrc/vector.rs
| pub const fn new(matrix: Matrix<D>) -> Self { | ||
| Self::new_unchecked(matrix) | ||
| Self { matrix } |
There was a problem hiding this comment.
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.
| pub const fn new(vector: Vector<D>) -> Self { | ||
| Self::new_unchecked(vector) | ||
| Self { vector } |
There was a problem hiding this comment.
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.
1 participant
Summary by CodeRabbit
Bug Fixes
Refactor