LAProof.C.cblas.asum_model: functional model of GSL's [cblas_dasum].

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

This file provides asum_model, the partial accumulation that the cblas_dasum loop invariant tracks, with the *step* lemma (how one loop iteration extends the accumulation) and the *end* lemma (the result of the accumulation once the loop finishes). GSL's kernel (source_asum_r.h) is

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

i.e., it adds |X[i]| left to right into the accumulator (BPLUS acc |x|), starting from +0.0. The C fabs computes BABS (the result of VSTlib's fabs_spec, whose ff_func is BABS), so the model uses BABS. The matching LAProof accuracy model is sum_model.sumF applied to map BABS X (the absolute values); over it sum_acc.fSUM proves the forward-error bound. The C's operand order (BPLUS acc x vs sumF's BPLUS x acc) and initial accumulator (+0.0 = Zconst Tdouble 0 vs sumF's neg_zero) differ, so the end/bridge lemma relates the two by feq (IEEE-equality identifying ±0/NaN).

asum_model X is the value the C loop *literally* computes: a left fold with the accumulator as the first BPLUS operand, separate abs-then-add, starting from +0.0. This mirrors the Clight AST in dasum.v exactly.

Model lemmas (the partial_row_× triple, specialised to a dense asum).

*step*: extending the length-k prefix X[0..k-1] with the element X[k] adds one BABS term, with the accumulator as the first BPLUS operand -- exactly the Clight statement r = r + fabs(X[k]).

*end*/bridge: the finished accumulation equals LAProof's summation model sumF (map BABS X) up to feq. Generalized-accumulator induction using common.BPLUS_comm and BPLUS_mor, with the feq (+0.0) (-0.0) base case (sumF starts at neg_zero).