Verify GSL CBLAS ddot, dasum, and dscal against LAProof models

[ak-2485]

Summary

Adds a new C/cblas/ directory connecting three GSL CBLAS routines (cblas_ddot, cblas_dasum, and cblas_dscal) to LAProof accuracy models. The GSL CBLAS source and headers in C/cblas/src and C/cblas/include are taken nearly verbatim; make generates the Clight AST with clightgen (the *.v build artifacts are .gitignored, like the other C programs). The verification for each routine is organized into:

• a functional model (*_model.v) capturing what the C loop literally computes, proved equal up tofeq to the corresponding LAProof accuracy model (dotprodF, map BABS ; sumF, and an elementwise BMULT map, respectively);
• a VST funspec relating the C result to that model (spec_*.v), and a proof verifying the C function against it (verif_*.v).

Documentation

• New "BLAS Level-1 (GSL CBLAS)" entry in index.html under C Program Correctness Proofs, linking the model / spec / verif coqdoc pages.
• CBLAS sources added to the top "C programs" list, with the.c names linking to cblas_ddot.html / cblas_dasum.html / cblas_dscal.html (generated from //ldoc on markers in the sources, matching the densemat/sparse convention).
• A C/cblas/ README.md with directory-level details on the CBLAS proofs.

Future work

The current proofs assume unit stride (incX = incY = 1), which lets the strided index variables coincide with the loop counter and makes the OFFSET/incX <= 0 guards dead code. Extending to general (non-unit, possibly negative) strides is the natural next step.