LAProof.accuracy_proofs.fma_is_finite

Finite Sum from Bounded Inputs

This file establishes key lemmas for proving finiteness of floating-point dot products computed via fused multiply-add (FMA) operations. The central result, finite_sum_from_bounded, shows that if all input vector elements are bounded in absolute value, then the accumulated floating-point dot product remains finite.
The proof strategy relies on:
  • A bound function fun_bnd t n that decreases monotonically in n, ensuring that element-wise bounds suffice to prevent overflow at each FMA step.
  • Forward error analysis for FMA-based dot products, connecting floating-point accumulation to real-valued dot products.

Key Definitions

  • fun_bnd t n : A per-element magnitude bound such that dot products of vectors of length n whose entries satisfy this bound do not overflow.

Key Lemmas


From LAProof.accuracy_proofs Require Import
  preamble
  real_lemmas
  common
  dotprod_model
  sum_model
  float_acc_lems
  dot_acc_lemmas
  sum_acc.

Import Zorder.

Section NAN.

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

Notation fmax := (@fmax t).

Bound Function

fun_bnd t n is used to construct a bound that will not cause overflow during FMA-based dot product of vectors of length n.

Definition fun_bnd (t : type) (n : nat) :=
  let x := (fmax - @default_abs t) / (1 + @default_rel t) - @g1 t n (n - 1) in
  let y := 1 / (1 + INR n × (@g t (n - 1) + 1)) in
  x × y.

Positivity of fun_bnd Components

The numerator of fun_bnd is non-negative when the g1 bound holds.

Lemma fun_bnd_pos_1 :
  ∀ (n : nat)
    (Hn : @g1 t (n + 1) n ≤ fmax),
    0 ≤ (fmax - @default_abs t) / (1 + @default_rel t) - @g1 t n (n - 1).

Monotonicity of fun_bnd

fun_bnd t n is non-increasing.

Lemma fun_bnd_le (n : nat) :
  ∀ (Hn : @g1 t (S n + 1) (S n) ≤ fmax),
    fun_bnd t (S n) ≤ fun_bnd t n.

List Splitting Lemmas

The two halves of l have equal length.

Lemma length_split {A : Type} (l : list (A × A)) :
  length (fst (List.split l)) = length (snd (List.split l)).

fun_bnd t n is non-negative.

Lemma fun_bound_pos (n : nat) :
  ∀ (Hn : @g1 t (n + 1) n ≤ fmax),
    0 ≤ fun_bnd t n.

Splitting and recombining a list of pairs is the identity.

Lemma combine_split {A : Type} (l : list (A × A)) :
  combine (fst (List.split l)) (snd (List.split l)) = l.

Main Result: Finiteness from Bounded Inputs

If every pair (x, y) in the combined input list satisfies:
  • both x and y are finite,
  • |FT2R x| and |FT2R y| are strictly bounded,
and the g1 overflow condition holds for the list length, then the FMA dot product accumulation fp is finite.
The proof proceeds by induction on the input list, applying the single-step is_finite_fma_no_overflow' lemma and the forward error bound fma_dotprod_forward_error_rel at each step.

Lemma finite_sum_from_bounded :
  ∀ (v1 v2 : list (ftype t))
    (fp : ftype t)
    (Hfp : fma_dot_prod_rel (List.combine v1 v2) fp)
    (Hn : @g1 t (S (length (List.combine v1 v2)) + 1)
                  (S (length (List.combine v1 v2))) ≤ fmax),
    (∀ x, In x (List.combine v1 v2) →
        Binary.is_finite (fst x) = true ∧
        Binary.is_finite (snd x) = true ∧
        Rabs (FT2R (fst x)) < sqrt (fun_bnd t (length (List.combine v1 v2))) ∧
        Rabs (FT2R (snd x)) < sqrt (fun_bnd t (length (List.combine v1 v2)))) →
    Binary.is_finite fp = true.
End NAN.