Skip to content

feat(vector): add certified dot and affine error bounds - #232

Merged
acgetchell merged 2 commits into
mainfrom
feat/220-certified-linear-forms
Sep 4, 2026
Merged

feat(vector): add certified dot and affine error bounds#232
acgetchell merged 2 commits into
mainfrom
feat/220-certified-linear-forms

Conversation

@acgetchell

@acgetchell acgetchell commented Sep 4, 2026

Copy link
Copy Markdown
Owner
  • Add proof-bearing scalar certificates for dot products and unrounded axis · (left - right) reductions.
  • Expose outward bounds for sign and threshold filtering, with inconclusive results when proof conditions fail.
  • Document and benchmark the deterministic FMA error model.

Closes #220

Summary by CodeRabbit

  • New Features

    • Added certified vector dot products and affine differences with estimates, absolute error bounds, and enclosing intervals.
    • Added public access to ScalarWithErrorBound through the main library interface and prelude.
    • Added clear arithmetic error reporting for vector dot-difference operations.
  • Documentation

    • Expanded guidance on certified reductions, rounding behavior, failure conditions, and usage examples.
  • Benchmarks

    • Added focused benchmarks for dot products and affine differences, including conclusive and inconclusive cases.

- Add proof-bearing scalar certificates for dot products and unrounded axis · (left - right) reductions.
- Expose outward bounds for sign and threshold filtering, with inconclusive results when proof conditions fail.
- Document and benchmark the deterministic FMA error model.

Closes #220
@acgetchell acgetchell self-assigned this Sep 4, 2026
@acgetchell
acgetchell enabled auto-merge September 4, 2026 16:08
@coderabbitai

coderabbitai Bot commented Sep 4, 2026

Copy link
Copy Markdown
Contributor

Review Change Stack

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info
⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: CHILL

Plan: Essentials

Run ID: e9c627bf-9fcd-4ebd-8777-85d373656e16

📥 Commits

Reviewing files that changed from the base of the PR and between 973e662 and d8d21db.

📒 Files selected for processing (2)
  • src/error.rs
  • src/vector.rs
🚧 Files skipped from review as they are similar to previous changes (1)
  • src/error.rs

Included review availability: 2 reviews are currently available. Your included PR review attempts over the past 7 days set your current allowance at 3 reviews per hour.


📝 Walkthrough

Walkthrough

Changes

Certified linear-form evaluation

Layer / File(s) Summary
Certificate construction and reductions
src/vector.rs, src/interval.rs, src/error.rs
Adds ScalarWithErrorBound, outward-rounded endpoints, FMA-based reductions, certified dot products, affine differences, and typed operation reporting.
Public API and usage contract
src/lib.rs, README.md, REFERENCES.md, docs/mathematical_basis.md
Re-exports the certificate type and documents reduction semantics, bounds, threshold checks, and inconclusive results.
Certificate and edge-case validation
src/vector.rs, src/error.rs, tests/prelude_exports.rs, tests/proptest_exact.rs
Tests certificates against exact rational results and covers overflow, underflow, cancellation, signed zero, mixed magnitudes, and zero-dimensional vectors.
Linear-form benchmark workflow
Cargo.toml, benches/linear_form.rs, justfile, docs/BENCHMARKING.md, README.md
Adds the linear_form Criterion suite and the bench-linear-form command for plain, conclusive, and inconclusive reductions.

Estimated code review effort: 4 (Complex) | ~45 minutes

Merge Risk: ⚪ Minimal · up to d8d21

This change adds certified dot-product and affine-reduction bounds with defined inconclusive and typed-error behavior. No current merge-blocking risk remains.

Sequence Diagram(s)

sequenceDiagram
  participant Caller
  participant Vector
  participant FMA_Reduction
  participant ScalarWithErrorBound
  Caller->>Vector: request certified dot or dot difference
  Vector->>FMA_Reduction: evaluate left-to-right FMA tree
  FMA_Reduction->>ScalarWithErrorBound: construct estimate and bounds
  ScalarWithErrorBound-->>Caller: return certificate or inconclusive result
Loading
🚥 Pre-merge checks | ✅ 4
✅ Passed checks (4 passed)
Check name Status Explanation
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title clearly summarizes the main change: certified dot-product and affine error bounds for vectors.
Linked Issues check ✅ Passed The pull request implements the linked issue objectives [#220]. It adds certified dot-product and affine-form APIs, matching error bounds and interval endpoints, direct affine reduction, typed failure…
Out of Scope Changes check ✅ Passed The changes remain within the linked issue scope [#220]. Source changes, tests, documentation, benchmarks, and workflow updates directly support certified vector reductions and their validation.
✨ Finishing Touches
📝 Generate docstrings
  • Create stacked PR
  • Commit on current branch
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch feat/220-certified-linear-forms

Comment @coderabbitai help to get the list of available commands.

@codecov

codecov Bot commented Sep 4, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 97.84946% with 8 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.87%. Comparing base (c0c2a78) to head (d8d21db).
✅ All tests successful. No failed tests found.

Files with missing lines Patch % Lines
src/vector.rs 97.82% 8 Missing ⚠️
Additional details and impacted files
@@            Coverage Diff             @@
##             main     #232      +/-   ##
==========================================
- Coverage   97.87%   97.87%   -0.01%     
==========================================
  Files          10       10              
  Lines        6069     6440     +371     
==========================================
+ Hits         5940     6303     +363     
- Misses        129      137       +8     
Flag Coverage Δ
unittests 97.87% <97.84%> (-0.01%) ⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

Comment thread src/vector.rs Fixed
Comment thread src/vector.rs Fixed
Comment thread src/vector.rs Fixed
Comment thread src/vector.rs Fixed
Comment thread src/vector.rs Fixed
Comment thread src/vector.rs Fixed
Comment thread src/vector.rs Fixed
Comment thread src/vector.rs Fixed
- Rename numerical-bound locals so CodeQL does not mistake them for sensitive certificate data.
- Document finite bound invariants, the affine error formula, and typed failure contexts.
- Make proof-range and second-FMA overflow expectations explicit.
@acgetchell
acgetchell merged commit 0d947ac into main Sep 4, 2026
21 checks passed
@acgetchell
acgetchell deleted the feat/220-certified-linear-forms branch September 4, 2026 17:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

feat: Add certified dot-product and linear-form bounds

2 participants