LAProof.C.cblas.spec_ddot: VST specification of GSL's [cblas_ddot].

Corresponds to C program C/cblas/src/ddot.c (ported from GSL cblas).

This file connects a real-world BLAS implementation -- GSL's double-precision dot product cblas_ddot -- to LAProof's functional dot-product model. GSL's loop (after macro expansion of source_dot_r.h) is

      double r = 0.0;
      for (i = 0; i < N; i++) { r += X[ix] * Y[iy]; ix += incX; iy += incY; }
      return r;

i.e. a forward, left-to-right accumulation using *separate* multiply-then-add (not fused multiply-add), starting from +0.0. That is exactly the dotprodF model of LAProof.accuracy_proofs.dotprod_model (dotprodF = dotprod BMULT BPLUS pos_zero), over which the forward-error theorem dot_acc.dotprod_forward_error is proved -- *not* the FMA-based floatlib.dotprod. Note on operand order: the C statement r += X×Y computes BPLUS acc prod (accumulator first), whereas dotprodF's fold step is BPLUS prod acc (product first). IEEE addition is commutative *up to feq*, so we state the postcondition with feq -- the same convention used by LAProof.C.spec_sparse for csr_row_vector_multiply_spec.

The partial-accumulation model ddot_model and its start/step/end lemmas live in LAProof.C.cblas.ddot_model (mirroring the sparse_model / spec_sparse split). This file states only the VST funspec. A stride is valid when GSL's initial OFFSET calculation, every selected array index, and every signed-int index update are safe. The strict lower bound in the nonpositive case makes the C expression -inc defined when inc is negative.

Funspec for cblas_ddot at general stride.