LAProof.accuracy_proofs.dot_acc_lemmas

Forward and Mixed Error Bounds for Floating-Point Dot Products

This file establishes accuracy lemmas for both FMA-based and non-FMA-based floating-point dot product computations. These results are foundational building blocks used in dot_acc.v and fma_dot_acc.v to prove the main accuracy theorems.

The proofs are structured around two inductive relations:

dot_prod_rel : relates a list of floating-point pairs to their computed (non-FMA) floating-point dot product.
fma_dot_prod_rel : relates a list of floating-point pairs to their computed FMA-based floating-point dot product.
R_dot_prod_rel : the analogous real-arithmetic dot product relation, used to state the ideal (exact) result.

The error bounds are expressed using the standard relative and absolute error model parameters: default_rel and default_abs.

Summary of Main Results

Forward Error Bounds

dotprod_forward_error_rel: Bounds the absolute error of a non-FMA floating-point dot product relative to the exact real dot product.
fma_dotprod_forward_error_rel: The analogous forward error bound for FMA-based dot products.

Sparse Forward Error Bounds

sparse_dotprod_forward_error_rel: A tighter forward error bound for non-FMA dot products that exploits zero entries in one of the input vectors, replacing the vector length with the number of nonzeros.
sparse_fma_dotprod_forward_error: The analogous sparse bound for FMA-based dot products.

Mixed Error Bounds

dotprod_mixed_error_rel: Shows that the computed non-FMA dot product can be expressed as an exact dot product of slightly perturbed inputs plus a small absolute error term.
fma_dotprod_mixed_error_rel: The analogous mixed error representation for FMA-based dot products, with a slightly tighter absolute error term.

From LAProof.accuracy_proofs Require Import
  preamble
  common
  dotprod_model
  float_acc_lems.

Section 1: Forward Error Bound — Non-FMA Dot Product

Section ForwardErrorRel1.

Forward error bound for the non-FMA dot product, using the inductive relation dot_prod_rel.

Context {NAN : FPCore.Nans} {t : type}.

Notation g := (@g t).
Notation g1 := (@g1 t).
Notation D := (@default_rel t).
Notation E := (@default_abs t).

dotprod_forward_error_rel establishes the standard forward error bound for the non-FMA floating-point dot product.

Given:

vF : a list of floating-point input pairs,
fp : the computed (finite) floating-point dot product satisfying dot_prod_rel vF fp,
rp : the exact real dot product satisfying R_dot_prod_rel (map FR2 vF) rp,
rp_abs : the dot product of absolute values satisfying R_dot_prod_rel (map Rabsp (map FR2 vF)) rp_abs,

the absolute error satisfies: |FT2R fp - rp| <= g(|vF|) * rp_abs + g1(|vF|, |vF| - 1)

Lemma dotprod_forward_error_rel :
  ∀ (vF : seq (ftype t × ftype t))
         (fp : ftype t)
         (Hfp : dot_prod_rel vF fp)
         (Hfin : Binary.is_finite fp = true)
         (rp rp_abs : R)
         (Hrp : R_dot_prod_rel (map FR2 vF) rp)
         (Hra : R_dot_prod_rel (map Rabsp (map FR2 vF)) rp_abs),
    Rabs (FT2R fp - rp) ≤ g (size vF) × rp_abs + g1 (size vF) (size vF - 1).

End ForwardErrorRel1.

Section 2: Forward Error Bound — FMA Dot Product

Section ForwardErrorRel2.

Forward error bound for the FMA-based dot product, using the inductive relation fma_dot_prod_rel. The bound takes the same form as the non-FMA case but uses FMA accuracy lemmas internally.

Context {NAN : FPCore.Nans} {t : type}.

Variable (vF : list (ftype t × ftype t)).
Notation vR := (map FR2 vF).
Notation vR' := (map Rabsp (map FR2 vF)).

Variable (fp : ftype t).
Hypothesis Hfp : fma_dot_prod_rel vF fp.
Hypothesis Hfin : Binary.is_finite fp = true.

Variable (rp rp_abs : R).
Hypothesis Hrp : R_dot_prod_rel vR rp.
Hypothesis Hra : R_dot_prod_rel vR' rp_abs.

Notation g := (@g t).
Notation g1 := (@g1 t).
Notation D := (@default_rel t).
Notation E := (@default_abs t).

fma_dotprod_forward_error_rel establishes the standard forward error bound for the FMA-based floating-point dot product.

The absolute error satisfies:

|FT2R fp - rp| <= g(|vF|) * rp_abs + g1(|vF|, |vF| - 1)

where rp is the exact real dot product and rp_abs is the dot product of absolute values.

Lemma fma_dotprod_forward_error_rel :
Rabs (FT2R fp - rp) ≤ g (size vF) × rp_abs + g1 (size vF) (size vF - 1).

End ForwardErrorRel2.

Section 3: Mixed Error Bound — Non-FMA Dot Product

Section MixedErrorRel1.

Mixed (componentwise relative + global absolute) error bound for the non-FMA dot product.

This section establishes that the computed dot product can be expressed as an exact dot product of perturbed inputs, up to a small absolute error.

Context {NAN : FPCore.Nans} {t : type}.

Notation g := (@g t).
Notation g1 := (@g1 t).
Notation D := (@default_rel t).
Notation E := (@default_abs t).

Variables (v1 v2 : list (ftype t)).
Hypothesis Hlen : size v1 = size v2.
Notation vF := (zip v1 v2).

Variable (fp : ftype t).
Hypothesis Hfp : dot_prod_rel vF fp.
Hypothesis Hfin : Binary.is_finite fp = true.

Notation neg_zero := (@common.neg_zero t).

dotprod_mixed_error_rel establishes the mixed error representation for the non-FMA floating-point dot product.

Lemma dotprod_mixed_error_rel :
  ∃ (u : list R) (eta : R),
    size u = size v2 ∧
    R_dot_prod_rel (zip u (map FT2R v2)) (FT2R fp - eta) ∧
    (∀ n, (n < size v2)%nat →
      ∃ delta ,
        nth 0 u n = FT2R (nth neg_zero v1 n) × (1 + delta) ∧
        Rabs delta ≤ g (size v2)) ∧
    Rabs eta ≤ g1 (size v2) (size v2).

End MixedErrorRel1.

Section 4: Mixed Error Bound — FMA Dot Product

Section MixedErrorRel2.

Mixed (componentwise relative + global absolute) error bound for the FMA-based dot product.

The structure mirrors MixedErrorRel1 but uses fma_dot_prod_rel and FMA accuracy lemmas, yielding the tighter absolute error bound due one fewer rounding step.

Context {NAN : FPCore.Nans} {t : type}.

Notation g := (@g t).
Notation g1 := (@g1 t).
Notation D := (@default_rel t).
Notation E := (@default_abs t).

Variables (v1 v2 : list (ftype t)).
Hypothesis Hlen : size v1 = size v2.
Notation vF := (zip v1 v2).

Variable (fp : ftype t).
Hypothesis Hfp : fma_dot_prod_rel vF fp.
Hypothesis Hfin : Binary.is_finite fp = true.

Notation neg_zero := (@common.neg_zero t).

fma_dotprod_mixed_error_rel establishes the mixed error representation for the FMA-based floating-point dot product.

The bound on the absolute error is one step tighter than the non-FMA case because each FMA step introduces only one rounding error.

Lemma fma_dotprod_mixed_error_rel :
  ∃ (u : list R) (eta : R),
    size u = size v1 ∧
    R_dot_prod_rel (zip u (map FT2R v2)) (FT2R fp - eta) ∧
    (∀ n, (n < size v2)%nat →
      ∃ delta ,
        nth 0 u n = FT2R (nth neg_zero v1 n) × (1 + delta) ∧
        Rabs delta ≤ g (size v2)) ∧
    Rabs eta ≤ g1 (size v2) (size v2 - 1).

End MixedErrorRel2.

Section 5: Sparse Forward Error Bound — Non-FMA Dot Product

Section SparseErrorRel1.

Sparse forward error bound for the non-FMA dot product.

When a vector in the product contains many zeros, the error bound can be sharpened by replacing the vector length with the number of nonzero entries. This follows from the observation that multiplying by zero contributes no rounding error, and thus such terms can be excluded from the error accumulation.

Context {NAN : FPCore.Nans} {t : type}.

Variables (v1 v2 : list (ftype t)).
Hypothesis (Hlen : size v1 = size v2).

Variable (fp : ftype t).
Hypothesis Hfp : dot_prod_rel (zip v1 v2) fp.
Hypothesis Hfin : Binary.is_finite fp = true.

Notation v1R := (map FT2R v1).
Notation nnzR := (nnzR v1R).

Variable (rp rp_abs : R).
Hypothesis Hrp : R_dot_prod_rel (map FR2 (zip v1 v2)) rp.
Hypothesis Hra : R_dot_prod_rel (map Rabsp (map FR2 (zip v1 v2))) rp_abs.

Notation g := (@common.g t).
Notation g1 := (@common.g1 t).

sparse_dotprod_forward_error_rel establishes the sparse forward error bound for the non-FMA dot product.This is tighter than the dense bound.

Lemma sparse_dotprod_forward_error_rel :
Rabs (FT2R fp - rp) ≤ g nnzR × rp_abs + g1 nnzR (nnzR - 1).

End SparseErrorRel1.

Section 6: Sparse Forward Error Bound — FMA Dot Product

Section SparseErrorRel2.

Sparse forward error bound for the FMA-based dot product.

As in SparseErrorRel1, zero entries in do not contribute to rounding error accumulation.

Context {NAN : FPCore.Nans} {t : type}.

Variables (v1 v2 : list (ftype t)).
Hypothesis (Hlen : size v1 = size v2).

Variable (fp : ftype t).
Hypothesis Hfp : fma_dot_prod_rel (zip v1 v2) fp.
Hypothesis Hfin : Binary.is_finite fp = true.

Notation v1R := (map FT2R v1).
Notation vR := (map FR2 (zip v1 v2)).
Notation vR' := (map Rabsp (map FR2 (zip v1 v2))).
Notation nnzR := (nnzR v1R).

Variable (rp rp_abs : R).
Hypothesis Hrp : R_dot_prod_rel vR rp.
Hypothesis Hra : R_dot_prod_rel vR' rp_abs.

Notation g := (@common.g t).
Notation g1 := (@common.g1 t).
Notation D := (@default_rel t).
Notation E := (@default_abs t).

sparse_fma_dotprod_forward_error establishes the sparse forward error bound for the FMA dot product.

Lemma sparse_fma_dotprod_forward_error :
Rabs (FT2R fp - rp) ≤ g nnzR × rp_abs + g1 nnzR (nnzR - 1).

End SparseErrorRel2.