LAProof.C.cblas.verif_dasum: VST proof for GSL's [cblas_dasum].

Corresponds to C program C/cblas/src/dasum.c.

body_cblas_dasum proves the positive-stride accumulation over strided incX N X and the kernel's early return for incX ≤ 0. The reduction models asum_model and sumF are unchanged.

Require Import VST.floyd.proofauto.
From vcfloat Require Import FPStdCompCert FPStdLib.
From VSTlib Require Import spec_math.
From LAProof.C Require Import floatlib.
From LAProof.C.cblas Require Import dasum scal_model asum_model spec_dasum.
Require Import LAProof.accuracy_proofs.sum_model.

Lemma body_cblas_dasum: semax_body Vprog Gprog f_cblas_dasum cblas_dasum_spec.

For incX > 0, the conditional accuracy payoff applies fSUM to map BABS (strided incX N X) after establishing that its sum is finite. The composition is not stated as a checked theorem here.