We will need the following; but the file names here are just provisional, and I may be missing parts of the picture, so this is just a first stab at it:
floatlib.v (from iterative_methods repo), supporting definitions for float functional models
floatmodel.v (list-of-list functional models of matrices, vectors, fma- and ordinary dot-product and matrix-vector multiply etc)
MCfloatmodel.v (mathcomp functional models of float matrices, vectors, fma- and ordinary operations on them)
Lemmas to relate floatmodel.v to MCfloatmodel.v
definitions/lemmas to relate MCfloatmodel.v to mathcomp real-valued matrix and vector models; perhaps these are, in fact, the main accuracy theorems
src/ directory containing C programs that implement the various operations; for now these will be just sparse.c from iterative_methods, but eventually it may be components from PETSc or something.
include/ directory containing C header files importable by clients (and also imported by the .c progams in src/ )
I've made an initial commit with the following correspondences to this issue.
float_acc_lems.v contains basic Flocq/VCFloat theorems used in accuracy proofs. I used this file in the stationary_methods directory of the iterative methods repo.
mv_mathcomp.v relates list-of-list functional models to MathComp matrices. An MCfloatmodel.v seems unnecessary; we already have injections for float lists to real lists and real lists to MathComp matrices.
We will need the following; but the file names here are just provisional, and I may be missing parts of the picture, so this is just a first stab at it: