LAProof.accuracy_proofs.preamble

LAProof.accuracy_proofs.common

LAProof.accuracy_proofs.float_acc_lems

LAProof.accuracy_proofs.dotprod_model

LAProof.accuracy_proofs.sum_model

LAProof.accuracy_proofs.sum_acc

LAProof.accuracy_proofs.dot_acc_lemmas

LAProof.accuracy_proofs.dot_acc

LAProof.accuracy_proofs.vecnorm_acc

LAProof.accuracy_proofs.fma_dot_acc

LAProof.accuracy_proofs.fma_is_finite

LAProof.accuracy_proofs.mv_mathcomp

LAProof.accuracy_proofs.gemv_acc

LAProof.accuracy_proofs.vec_op_acc

LAProof.accuracy_proofs.gemm_acc

LAProof.accuracy_proofs.export

LAProof.C.floatlib

LAProof.C.sparse_model

LAProof.C.sparse

LAProof.C.spec_sparse

LAProof.C.verif_sparse

LAProof.C.verif_sparse_byrows

LAProof.C.VSU_sparse

LAProof.C.cholesky

LAProof.C.verif_cholesky

LAProof.C.alloc

LAProof.C.spec_alloc

LAProof.C.verif_alloc

LAProof.C.densemat

LAProof.C.spec_densemat: VST specifications of functions on dense matrices.

• • Corresponds to C program densemat.h and densemat.c
  • Abstracting the floating-point precision
  • Conversions between floats, float-options, and val
  • Representation predicates for dense matrices
• Function specifications (funspecs)
• Not-yet-specified functions
• Building the "Abstract Specification Interface", the list of funspecs for this module

LAProof.C.densemat_lemmas: Supporting lemmas for VST proofs of functions on dense matrices.

• VSU definitions
• Many useful supporting lemmas about column_major, ordinal, ord_enum, etc.
• Tactics for ordinals
• Tactics for calling matrix subscripting functions

LAProof.C.verif_densemat: VST proofs of functions on dense matrices.

• • Corresponds to C program densemat.c
• Prologue.
• densemat_malloc verification
• densemat_free verification
• Unpacking dependently typed WITH components
• densemat_clear verification
• densemat_get verification
• densemat_set verification
• densemat_addto verification
• data_norm and densemat_norm verification

LAProof.C.verif_densemat_mult: VST proofs dense matrix multiply functions

• • Corresponds to C program densemat.c
• Prologue.

LAProof.C.verif_densemat_cholesky: VST proofs of Cholesky functions on dense matrices.

• • Corresponds to C program densemat.c
• Prologue.
• densemat_cfactor verification: Cholesky factorization
• densemat_csolve verification: Cholesky solve by forward substitution and back substitution

LAProof.C.VSU_densemat: Packaging the [densematVSU], the Verified Software Unit

• • Corresponds to C program densemat.c
• Prologue.

LAProof.C.matrix_model: Functional models of matrix operations

• Prologue: typical imports for MathComp floating-point matrix functional models
• MathComp matrices over a nonring
• Functional model of Cholesky decomposition (jik algorithm)
• Definitions for manipulating triangular matrices

LAProof.C.bandmat