Shape functions
Thus far in the project, the main things verified are,- Dense matrix functions (in the LAProof library, see specifications in spec_densemat and verifications in verif_densemat, verif_densemat_mult, verif_densemat_cholesky.
- Shape functions.
Read the description here;
See the C program;
Then, to see how it works for, e.g., the 2dP1 shape function, visit these pages:
- Real-valued functional model
- 2dP1 instance of real-valued functional model
- Float-valued functional model
- 2dP1 instance of float-valued functional model
- General form of shape accuracy theorem
- 2dP1 instance of shape accuracy theorem
- General form of function specification for C shape functions
- 2dP1 C program correctness proof
- C program correctness proof for entire shapes API
Rocq modules
- matrix_util
- Utility lemmas and tactics for rewriting matrix expressions
- shapes
- Functional models of shape functions, including proofs that they are Lagrangian and continuously differentiable.
- shapefloat
- Functional models of float-valued shape functions
- shape_accuracy
- Roundoff-error bounds for float-valued shape functions
- C.spec_shapes
- VST function spec for shape functions
- C.verif_shapes_base
- Preamble for the VST verifications of shape functions
- C.verif_shapes1d, C.verif_shapes2d, C.verif_shapes2dP2
- VST verifications of 1-dimensional and 2-dimensional shape functions
- 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.
- LAProof.C.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.
- LAProof.C.verif_densemat
- VST proofs of basic functions on dense matrices.
- LAProof.C.verif_densemat_mult
- VST proofs of dense matrix multiply.
- LAProof.C.verif_densemat_cholesky
- VST proofs of dense matrix Cholesky factoring and Cholesky solve (back-subst, forward_subst).