Dot Product Accuracy Proofs (Non-FMA)

This file establishes floating-point accuracy bounds for the non-fused multiply-add (non-FMA) dot product computation over lists of floating-point numbers. It provides both mixed-error and forward-error analyses, as well as a refined bound for sparse vectors.

Error Factors

Throughout, the accumulated relative error factor is \(g(n) = (1 + \mathbf{u})^n - 1\) and the mixed absolute error factor is \(g_1(n_1, n_2) = n_1 \cdot \eta \cdot (1 + g(n_2))\), where \(\mathbf{u}\) is the unit roundoff and \(\eta\) is the underflow threshold for the given floating-point type. Both are defined in common.

Main Results

• dotprod_mixed_error: Shows that the computed dot product can be expressed as an exact dot product of slightly perturbed inputs plus a small absolute error term. Each input component is perturbed by a relative factor bounded by \(g(n)\), and the absolute residual is bounded by \(g_1(n,n)\), where \(n\) is the vector length.
• dotprod_forward_error: Bounds the absolute forward error \(|\mathtt{fl}(v_1 \cdot v_2) - v_1 \cdot v_2|\) by \(g(n)\,(|v_1| \cdot |v_2|) + g_1(n,\,n-1)\), where \(|v|\) denotes componentwise absolute value.
• sparse_dotprod_forward_error: Refines dotprod_forward_error for sparse inputs by replacing the full vector length \(n\) with the number of nonzero entries \(n_{\mathrm{nz}}\), giving a tighter bound when the input vectors are sparse.

Dependencies

This file relies on the following modules from LAProof.accuracy_proofs:

• preamble: basic setup and notation,
• common: shared definitions including nnzR and neg_zero ,
• dotprod_model: the floating-point model dotprodF and its relational characterization dotprodF_rel_fold_right,
• sum_model: summation model infrastructure,
• float_acc_lems: generic floating-point accuracy lemmas,
• dot_acc_lemmas: the core relational accuracy lemmas dotprod_mixed_error_rel, dotprod_forward_error_rel, and sparse_dotprod_forward_error_rel that drive the proofs here.

Structure

The file is organised into two Sections:

• MixedError: proves dotprod_mixed_error.
• ForwardError: proves dotprod_forward_error and sparse_dotprod_forward_error.

dotprod_mixed_error expresses the computed dot product as an exact inner product of component-wise perturbed inputs plus a small absolute offset. The relative perturbation on each input component is bounded by \(g(n)\) and the absolute residual by \(g_1(n,n)\).

dotprod_forward_error bounds the absolute forward error of the computed dot product by \(g(n)\,(|v_1| \cdot |v_2|) + g_1(n,\,n-1)\), where \(|v|\) denotes the componentwise absolute-value vector.

sparse_dotprod_forward_error refines dotprod_forward_error for sparse inputs: the vector length \(n\) is replaced by the number of nonzero entries \(n_{\mathrm{nz}}\), yielding \(g(n_{\mathrm{nz}})\,(|v_1| \cdot |v_2|) + g_1(n_{\mathrm{nz}},\,n_{\mathrm{nz}}-1)\).