Hi everyone, I released covstream, a Rust library for fixed-dimension streaming covariance and Ledoit-Wolf shrinkage, with a Lean-backed specification in the same repository.

What covstream does:

• maintains a fixed-dimension streaming covariance state in memory
• updates covariance one aligned sample at a time without rebuilding from scratch
• ingests flat row-major batches for research, backtests, or offline jobs
• supports checked ingest paths that reject malformed input and non-finite values
• supports faster trusted ingest paths when validation already happens upstream
• extracts covariance in either dense row-major form or packed upper-triangle form
• applies Ledoit-Wolf style shrinkage toward the scaled-identity target
• includes a parallel batch ingest path for larger workloads

That makes it useful for tasks like:

• online covariance estimation for return streams or telemetry vectors
• research pipelines that need repeated covariance snapshots
• downstream numerical code that prefers packed symmetric output
• systems where you want the mathematical contract kept close to the implementation

I started this project because to learn both Rust and Lean/mathlib on a small problem because both seem interesting to me, formalizing the something mathematically before you code it seems like it can be useful for a multitude of applications where making a backed up claim about the code can be critical

And rust feels like it's the natural extension of that paradigm with strong typing and memory correctness guarantees.

I’d be interested in feedback on the API shape, the docs, and whether the Rust/Lean boundary is explained clearly enough.

Here are some benchmark notes of the app:

• Ryzen 5 5600 Linux desktop: observe/2 about 48.2 ns, observe/8 about 98.3 ns, observe/32 about 348 ns
• Ryzen 5 5600 Linux desktop: observe_hot/trusted/256 about 8.25 µs
• Apple M2 MacBook Air: observe_hot/trusted/256 about 11.4 µs
• Ryzen 5 5600 Linux desktop: 1024x256 trusted batch ingest about 8.41 ms serial vs 1.82 ms parallel

Repo: GitHub - gratus00/Covstream: Covariance matrix estimator, with formalized welford's algorithm on Lean · GitHub
Crate: crates.io: Rust Package Registry
API notes: Covstream/docs/RUST_API.md at main · gratus00/Covstream · GitHub

1 post - 1 participant

Read full topic