LAProof.C.cblas.verif_ddot: VST proof for GSL's [cblas_ddot].

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

body_cblas_ddot proves the accumulation over the logical vectors selected by arbitrary signed strides, including zero. The reduction models ddot_model and dotprodF are unchanged.

Require Import VST.floyd.proofauto.
From vcfloat Require Import FPStdCompCert FPStdLib.
From LAProof.C Require Import floatlib.
From LAProof.C.cblas Require Import ddot stride_model ddot_model spec_ddot.
Require Import LAProof.accuracy_proofs.dotprod_model.

Lemma body_cblas_ddot: semax_body Vprog Gprog f_cblas_ddot cblas_ddot_spec.

Conditional accuracy payoff: the result is feq-equal to dotprodF applied to the two logical strided vectors. After additionally establishing that this model result is finite, one can transfer LAProof.accuracy_proofs.dot_acc.dotprod_forward_error to the value computed by the compiled C cblas_ddot. That composition is not stated as a checked theorem here.