LAProof: accuracy and correctness of linear algebra programs
LAProof is a modular, portable proof layer between the verification of application software and the verification of programs implementing operations defined by the basic linear algebra subprograms (BLAS) specification.
See also:
- GitHub repo
- Our paper in 30th IEEE International Symposium on Computer Arithmetic (ARITH '23) or non-paywall version
LAProof provides formal machine-checked proofs of the accuracy of basic linear algebra operations: inner product using conventional multiply and add, inner product using fused multiply-add (each with independent error bound proofs), scaled matrix-vector and matrix-matrix multiplication, and scaled vector and matrix addition. LAProof error bounds are backward error bounds and mixed backward-forward error bounds that account for underflow, proved subject to no assumptions except a low- level formal model of IEEE-754 arithmetic. We treat low-order error terms concretely, not approximating as O(u2).
The LAProof repository contains a machine-checked correctness proof of a C function implementing compressed sparse row matrix-vector multiplication as an example of connecting LAProof to concrete programs.
LAProof 2.0beta1 is based more directly on MathComp (compared to LAProof 1.0 which used a list-of-list representation for matrices). That is, matrix and vector operations use definitions in mathcomp.algebra.matrix.
Documentation
C programs
- alloc.[c,h]: Memory allocation utilities
- densemat.[c,h]: Dense matrix operations
- bandmat.[c,h]: Symmetric band matrix operations
- sparse.[c,h]: CSR (Compressed Sparse Row) matrix operations
Algorithm Accuracy Proofs
See also the specs-and-proofs table of contents.
Most of the definitions and lemmas listed here are parameterized by a floating-point format not shown in this summary: that is, implicit parameters {_: FPCore.Nans}{t: FPStdLib.type}.
Floating-point operation definitions (mv_mathcomp)
- F.sum
[n] ('I_n -> ftype t) : ftype t - F.dotprod
[n] (x: 'rV[ftype t]_n) (y: 'cV[ftype t]_n) : ftype t - F.mulmx
[m n p] (A: 'M[ftype t]_(m,n)) (B: 'M[ftype t]_(n,p)) : 'M[ftype t]_(m,p) - F.scalemx
[m n] (a: ftype t) (M: 'M[ftype t]_(m,n)) : 'M[ftype t]_(m,n) - F.addmx
[m n] (A B: 'M[ftype t]_(m,n)) : 'M[ftype t]_(m,n)
Summation (sum_acc)
- Fsum_backward_error
[n] (x: 'I_n -> ftype t) ... - Fsum_forward_error
[n] (x: 'I_n -> ftype t) ...
Dot product, non-FMA (dot_acc)
Dot product, FMA (fma_dot_acc)
Vector norms (vecnorm_acc)
Scalar and componentwise matrix operations (vec_op_acc)
- Fscalemx_mixed_error
[m n] (a: ftype t) (v: 'M[ftype t]_(m,n)) ... - Faddmx_mixed_error
[m n] (A B: 'M[ftype t]_(m,n)) ...
Matrix-vector multiplication, GEMV (gemv_acc)
- mat_vec_mul_mixed_error
[m n] (A: 'M[ftype t]_(m,n)) (B: 'cV[ftype t]_n) ... - mat_vec_mul_forward_error
[m n] (A: 'M[ftype t]_(m,n)) (B: 'cV[ftype t]_n) ...
Matrix-matrix multiplication, GEMM (gemm_acc)
- mat_axpby_error
[m n] (A B: 'M[ftype t]_(m,n)) (x y: ftype t) ... - GEMM_error
[m n p] (A: 'M[ftype t]_(m,n)) (B: 'M[ftype t]_(n,p)) (Y: 'M[ftype t]_(m,p)) (s1 s2: ftype t) ...
Cholesky solve (libvalidsdp)
- LVDSP_cholesky_success: accuracy of solving a linear system using Cholesky decomposition followed by forward and back substitution (see also Cholesky/triangular-solve functional model)
C Program Correctness Proofs
See also the specs-and-proofs table of contents.
Generally these prove that the C programs correctly implement the algorithms. These theorems may be composed with the algorithm accuracy proofs.
Functional models: matrix model definitions and lemmas.
- Dense Matrices: densemat.c
- Band Matrices: bandmat.c
- Sparse Matrices: sparse.c (CSR matrix-vector multiply)
- Specification
- Correctness proofs: standard, row-by-row variant
- Verified Software Unit