Rocq modules
- matrix_model
- Functional models of matrix operations. We describe floating-point matrices using the
Mathematical Components library,
and present functional models of operations such as access to
matrix elements,
Cholesky decomposition (inner-product algorithm),
Cholesky solve by forward substitution and back substitution, etc.
These functional models are agnostic about whether the matrix representation is dense, banded, sparse, or otherwise; mapping the matrix values to their representations in C programs is done in (for example) spec_densemat, spec_bandmat, etc. Of course, there is no guarantee that you'd want to use exactly the same algorithm (e.g., for Cholesky) on band matrices that you'd use on dense matrices.
- spec_densemat
- VST specifications of functions on dense matrices, with some explanation of how to
specify the connection of C programs to MathComp functional models.
- verif_densemat
- VST proofs of functions on dense matrices.