LAProof.accuracy_proofs.dotprod_model
Dot Product Definitions and Properties
Overview of contents
- dotprod: a generic, parameterised dot-product computed via
foldl over a zipped pair of lists. Specialised to
- dotprodF - IEEE floating-point (BMULT / BPLUS),
- fma_dotprod - IEEE floating-point with fused multiply-add (BFMA), and
- dotprodR - real arithmetic (Rmult / Rplus).
- Inductive relations that characterize the value produced by each
variant:
- dot_prod_rel for dotprodF,
- fma_dot_prod_rel for fma_dotprod,
- dotprod_any / dotprod_any' for arbitrary reassociation / reordering of a floating-point dot product,
- R_dot_prod_rel for dotprodR.
- Key lemmas connecting implementations to their relations:
- dotprodF_rel_fold_right - dot_prod_rel holds for dotprodF.
- fma_dot_prod_rel_fold_right - fma_dot_prod_rel holds for fma_dotprod.
- dotprodR_rel - R_dot_prod_rel holds for dotprodR.
- dotprod_rel_dotprod_any - every result of dot_prod_rel
can be witnessed by dotprod_any.
- Bound lemmas for the real dot product:
- dotprodR_rel_bound' - |⟨u,v⟩| ≤ n·a when each component has absolute value at most √a.
- dotprodR_rel_bound'' - same bound but for the dot product of absolute values ⟨|u|,|v|⟩.
- dot_prod_sum_rel_R_Rabs - |⟨u,v⟩| ≤ ⟨|u|,|v|⟩.
- Non-zero-detection lemmas (Section NonZeroDP): when every entry of a vector has real value 0 the floating-point (and real) dot products are 0.
From LAProof.accuracy_proofs Require Import preamble common float_acc_lems.
Require Import FunctionalExtensionality.
Require Import Permutation.
Generic dot product
Definition dotprod {A} (mult plus : A → A → A) (zero : A)
(v1 v2 : list A) : A :=
foldl (Basics.flip plus) zero (map (uncurry mult) (zip v1 v2)).
If the left argument is nil the result is zero, regardless of
the right argument.
Lemma dotprod_nil_l :
∀ A (l : list A) (mult plus : A → A → A) (zero : A),
dotprod mult plus zero nil l = zero.
If the right argument is nil the result is zero, regardless of
the left argument.
Lemma dotprod_nil_r :
∀ A (l : list A) (mult plus : A → A → A) (zero : A),
dotprod mult plus zero l nil = zero.
When the right list is a singleton, the dot product reduces
to a single multiplication.
Lemma dotprod_single :
∀ A (l : list A)
(mult plus : A → A → A) (zero a2 : A)
(Hpz : ∀ y, plus y zero = y)
(Hmz : ∀ y, mult zero y = zero),
let a1 := nth zero l 0 in
dotprod mult plus zero l [a2] = mult a1 a2.
dotprodF v1 v2 is the standard left-to-right floating-point dot
product using IEEE multiplication BMULT and addition BPLUS,
starting from the positive zero.
dot_prod_rel l s is the inductive relation that characterizes the
value s obtained by computing the dot product of the list of
pairs l in left-to-right order using IEEE arithmetic.
Inductive dot_prod_rel :
list (ftype t × ftype t) → ftype t → Prop :=
| dot_prod_rel_nil :
dot_prod_rel nil pos_zero
| dot_prod_rel_cons :
∀ l (xy : ftype t × ftype t) s,
dot_prod_rel l s →
dot_prod_rel (xy :: l)
(BPLUS (BMULT (fst xy) (snd xy)) s).
dotprod_any' h v s witnesses that s can be obtained as the
floating-point dot product of the pairs in v by any
parenthesisation of depth at most h, including arbitrary
permutations of the summands (via Dotprod_Any_perm). This
relation supports accuracy analyses that do not depend on a
particular evaluation order.
Inductive dotprod_any' :
∀ (h : nat) (v : list (ftype t × ftype t))
(s : ftype t), Prop :=
| Dotprod_Any_1 :
∀ x,
dotprod_any' O [x] (BMULT (fst x) (snd x))
| Dotprod_Any_split :
∀ n1 n2 al bl a b,
dotprod_any' n1 al a →
dotprod_any' n2 bl b →
dotprod_any' (S (Nat.max n1 n2)) (al ++ bl) (BPLUS a b)
| Dotprod_Any_perm :
∀ n al bl s,
Permutation al bl →
dotprod_any' n al s →
dotprod_any' n bl s.
dotprod_any h v s extends dotprod_any' to handle the empty
list, where the dot product is positive zero.
Inductive dotprod_any :
∀ (h : nat) (v : list (ftype t × ftype t))
(s : ftype t), Prop :=
| Dotprod_Any_None :
dotprod_any O nil pos_zero
| Dotprod_Any_Some :
∀ n v s,
dotprod_any' n v s →
dotprod_any n v s.
Every value related to a list by dot_prod_rel is (up to feq)
also witnessed by dotprod_any, provided all pairwise products
are finite. This is the key lemma that bridges the sequential
IEEE relation and the order-independent dotprod_any relation.
Lemma dotprod_rel_dotprod_any :
∀ (z : ftype t) (v : list (ftype t × ftype t)) s
(Hz : iszero z)
(Hfin : Forall (fun xy ⇒
Binary.is_finite (BMULT (fst xy) (snd xy))) v),
dot_prod_rel v s →
∃ s', feq s s' ∧ dotprod_any (Nat.pred (size v)) v s'.
dot_prod_rel characterizes dotprodF: the relation holds for
the reversed zip of the two input lists.
Lemma dotprodF_rel_fold_right :
∀ (v1 v2 : list (ftype t)),
dot_prod_rel (rev (zip v1 v2)) (dotprodF v1 v2).
End DotProdFloat.
Definition fma_dotprod (v1 v2 : list (ftype t)) : ftype t :=
foldl (fun s x12 ⇒ BFMA (fst x12) (snd x12) s)
pos_zero (zip v1 v2).
fma_dot_prod_rel l s is the FMA analogue of dot_prod_rel:
s is the value obtained by accumulating BFMA from the left
over the pair list l.
Inductive fma_dot_prod_rel :
list (ftype t × ftype t) → ftype t → Prop :=
| fma_dot_prod_rel_nil :
fma_dot_prod_rel nil (Zconst t 0)
| fma_dot_prod_rel_cons :
∀ l (xy : ftype t × ftype t) s,
fma_dot_prod_rel l s →
fma_dot_prod_rel (xy :: l)
(BFMA (fst xy) (snd xy) s).
Note: there is no fma_dotprod_any analogue of dotprod_any,
because the FMA model is inherently sequential - it accumulates
products one at a time into a single running sum and does not
naturally support arbitrary reassociation.
fma_dot_prod_rel characterizes fma_dotprod: the relation holds
for the reversed zip of the two input lists.
Lemma fma_dot_prod_rel_fold_right :
∀ (v1 v2 : list (ftype t)),
fma_dot_prod_rel (rev (zip v1 v2)) (fma_dotprod v1 v2).
End DotProdFMA.
dotprodR l1 l2 is the exact real dot product of l1 and l2,
defined as an instance of the generic dotprod over ℝ.
R_dot_prod_rel l s is the real analogue of dot_prod_rel:
s is the value of the dot product of the pair list l in ℝ.
Inductive R_dot_prod_rel : list (R × R) → R → Prop :=
| R_dot_prod_rel_nil :
R_dot_prod_rel nil 0%R
| R_dot_prod_rel_cons :
∀ l xy s,
R_dot_prod_rel l s →
R_dot_prod_rel (xy :: l) (fst xy × snd xy + s).
The value witnessed by R_dot_prod_rel is unique.
Rabsp p replaces each component of the pair p by its absolute
value. It is used to build the absolute-value dot product that bounds
|⟨u, v⟩|.
Convenience rewriting rule: (FT2R a, FT2R a0) = FR2 (a, a0).
Basics.flip Rplus is propositionally equal to Rplus because
real addition is commutative.
R_dot_prod_rel characterizes dotprodR: for any v1 and v2,
R_dot_prod_rel (zip v1 v2) (dotprodR v1 v2).
The value of the real dot product relation is injective in s.
Reversing the second argument is equivalent to reversing the
first, when both lists have the same length.
Lemma dotprodR_rev :
∀ (v1 v2 : list R),
size v1 = size v2 →
dotprodR v1 (rev v2) = dotprodR (rev v1) v2.
Zipping then mapping FR2 is the same as mapping FT2R
componentwise before zipping.
Lemma map_FR2_zip :
∀ {t} (v1 v2 : seq (ftype t)),
map FR2 (zip v1 v2) = zip (map FT2R v1) (map FT2R v2).
Zipping then mapping Rabsp is the same as mapping Rabs
componentwise before zipping.
The real dot product of the real images of v1 and v2 satisfies
R_dot_prod_rel on the reversed FR2-mapped zip, and equals the
sum_fold of the pointwise products.
Lemma R_dot_prod_rel_fold_right t :
∀ (v1 v2 : list (ftype t)),
size v1 = size v2 →
let prods :=
map (uncurry Rmult) (map FR2 (zip v1 v2)) in
R_dot_prod_rel (rev (map FR2 (zip v1 v2))) (sum_fold prods).
Lemma R_dot_prod_rel_fold_right' t :
∀ (v1 v2 : list (ftype t)),
size v1 = size v2 →
let prods :=
map (uncurry Rmult) (map FR2 (zip v1 v2)) in
R_dot_prod_rel (rev (map FR2 (zip v1 v2)))
(dotprodR (map FT2R v1) (map FT2R v2)).
R_dot_prod_rel for the absolute-value dot product: the reversed zip
of Rabsp ∘ FR2 satisfies the relation with value sum_fold prods.
Lemma R_dot_prod_rel_fold_right_Rabs t :
∀ (v1 v2 : list (ftype t)),
size v1 = size v2 →
let prods :=
map (uncurry Rmult) (map Rabsp (map FR2 (zip v1 v2))) in
R_dot_prod_rel (rev (map Rabsp (map FR2 (zip v1 v2))))
(sum_fold prods).
Variant of R_dot_prod_rel_fold_right_Rabs expressing the sum as
dotprodR (map Rabs (map FT2R v1)) (map Rabs (map FT2R v2)).
Lemma R_dot_prod_rel_fold_right_Rabs' t :
∀ (v1 v2 : list (ftype t)),
size v1 = size v2 →
let prods :=
map (uncurry Rmult) (map Rabsp (map FR2 (zip v1 v2))) in
R_dot_prod_rel (rev (map Rabsp (map FR2 (zip v1 v2))))
(dotprodR (map Rabs (map FT2R v1))
(map Rabs (map FT2R v2))).
When all pairs in l have been replaced by their absolute values
(via Rabsp), the resulting sum is non-negative, so Rabs s = s.
The absolute value of the exact dot product is bounded by the
absolute-value dot product: |⟨u, v⟩| ≤ ⟨|u|, |v|⟩.
Lemma dot_prod_sum_rel_R_Rabs :
∀ l s1 s2,
R_dot_prod_rel l s1 →
R_dot_prod_rel (map Rabsp l) s2 →
Rabs s1 ≤ Rabs s2.
Scaling the left factor of every pair by a scalar
a scales the
dot product by a. Formally, if R_dot_prod_rel (zip u v) r
then R_dot_prod_rel (zip (map (Rmult a) u) v) (a × r).
Lemma dot_prod_zip_map_Rmult a u v r :
size u = size v →
R_dot_prod_rel (zip u v) r →
R_dot_prod_rel (zip (map (Rmult a) u) v) (a × r).
Given a floating-point dot-product computation witnessed by
dot_prod_rel, there exists a real value rp related to the
real-image list by R_dot_prod_rel.
Lemma dotprod_rel_R_exists {NAN : FPCore.Nans} {t : type} :
∀ (l : list (ftype t × ftype t)) (fp : ftype t),
dot_prod_rel l fp →
∃ rp, R_dot_prod_rel (map FR2 l) rp.
FMA analogue of dotprod_rel_R_exists: given a computation
witnessed by fma_dot_prod_rel, there exists a real value related
to the real-image list.
Lemma dotprod_rel_R_exists_fma {NAN : FPCore.Nans} {t : type} :
∀ (l : list (ftype t × ftype t)) (fp : ftype t),
fma_dot_prod_rel l fp →
∃ rp, R_dot_prod_rel (map FR2 l) rp.
FMA analogue for the absolute-value dot product: given
fma_dot_prod_rel l fp, there exists a real value related to
map Rabsp (map FR2 l).
Lemma sum_rel_R_abs_exists_fma {NAN : FPCore.Nans} {t : type} :
∀ (l : list (ftype t × ftype t)) (fp : ftype t),
fma_dot_prod_rel l fp →
∃ rp, R_dot_prod_rel (map Rabsp (map FR2 l)) rp.
Component-wise bound on the real dot product:
if every component of the pairs in l has absolute value at most
√a, then |⟨u, v⟩| ≤ n · a, where n = length l.
This is a standard building block for rounding error bounds.
Lemma dotprodR_rel_bound' :
∀ (t : type) (l : list (ftype t × ftype t)) (rp a : R)
(Ha : 0 ≤ a)
(Hrp : R_dot_prod_rel (map FR2 l) rp)
(Hin : ∀ x, In x l →
Rabs (FT2R (fst x)) ≤ sqrt a ∧
Rabs (FT2R (snd x)) ≤ sqrt a),
Rabs rp ≤ INR (length l) × a.
Variant of dotprodR_rel_bound' for the absolute-value
relation: if R_dot_prod_rel (map Rabsp (map FR2 l)) rs_abs and
every component has absolute value at most √a, then
rs_abs ≤ n · a.
Lemma dotprodR_rel_bound'' :
∀ (t : type) (l : list (ftype t × ftype t)) (rs_abs a : R)
(Ha : 0 ≤ a)
(Hrp : R_dot_prod_rel (map Rabsp (map FR2 l)) rs_abs)
(Hin : ∀ x, In x l →
Rabs (FT2R (fst x)) ≤ sqrt a ∧
Rabs (FT2R (snd x)) ≤ sqrt a),
rs_abs ≤ INR (length l) × a.
End RealDotProd.
Section NonZeroDP.
Context {NAN : FPCore.Nans} {t : type}.
Variables (v1 v2 : list (ftype t)).
Hypothesis (Hlen : size v1 = size v2).
Notation v1R := (map FT2R v1).
Req_bool and the boolean equality eq_op coincide on ℝ.
If every component of v1 has real value 0 (i.e. nnzR v1R = 0),
and the IEEE dot product fp is finite, then FT2R fp = 0.
This justifies early exit when the first operand is the zero
vector.
Lemma dot_prod_rel_nnzR :
∀ (fp : ftype t)
(Hfp : dot_prod_rel (zip v1 v2) fp)
(Hfin : Binary.is_finite fp = true),
nnzR v1R == 0%nat → FT2R fp = 0.
Print nnzR.
Qed.
FMA analogue of dot_prod_rel_nnzR: when nnzR v1R = 0 and the
FMA dot product is finite, FT2R fp = 0.
Lemma fma_dot_prod_rel_nnzR :
∀ (fp : ftype t)
(Hfp : fma_dot_prod_rel (zip v1 v2) fp)
(Hfin : Binary.is_finite fp = true),
nnzR v1R == 0%nat → FT2R fp = 0.
Real analogue: when nnzR v1R = 0, the real dot product rp
obtained via R_dot_prod_rel (map FR2 (zip v1 v2)) rp is 0.
Lemma R_dot_prod_rel_nnzR :
∀ (rp : R)
(Hrp : R_dot_prod_rel (map FR2 (zip v1 v2)) rp),
nnzR v1R == 0%nat → rp = 0.
Absolute-value dot product analogue of R_dot_prod_rel_nnzR:
when nnzR v1R = 0, the absolute-value sum rp_abs is 0.