Proposal for organization of this repo

[andrew-appel]

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/ )

[ak-2485]

I've made an initial commit with the following correspondences to this issue.

1. 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.
2. dotprod_model.v & gem_defs.v contain polymorphic list-of-list functional models.
3. 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.