Binary reductions and their error bounds

Exact-accumulation reduction kernels are exported together with their correctness proofs. Reduction.Tree bounds the accumulated error when each addition rounds separately. Runtime-only consumers of exact accumulation should import Reduction.Runtime.