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, 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(u²).

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}.

• 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))
• Fsum_backward_error [n] (x: 'I_n -> ftype t) ...
• Fsum_forward_error [n] (x: 'I_n -> ftype t) ...
• Faddmx_mixed_error [m n] (A B: 'M[ftype t]_(m,n)) ...
• Fscalemx_mixed_error [m n] (a: ftype t) (v: 'M[ftype t]_(m,n)) ...
• vec_vec_mul_mixed_error [n] (A: 'rV[ftype t]_n) (B: 'cV[ftype t]_n) ...
• 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) ...
• mat_sum_error [m n] (A B: 'M[ftype t]_(m,n)) ...
• mat_axpby_error [m n] (A B: 'M[ftype t]_(m,n)) (x y: ftype t) ... (xA+yB)
• 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) ... (s1*A*B+s2*Y)

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

Specifications, Supporting lemmas, Correctness proofs of basic operations, matrix multiply, Cholesky factoring and solve, and packaging the Verified Software Unit.

Band Matrices: bandmat.c

(not yet proved correct).

Sparse Matrices: sparse.c

Specification, Verification. Correctness of CSR matrix-vector multiply.