Floating point multiplication

For floating point, multiplication is easier than addition, as the exponent adds. If z = x * y, we have

z.n * 2^(z.s - 2^63) = x.n * y.n * 2^(x.s + y.s - 2^63 - 2^63)

Auxiliary lemmas

def Floating.mul_n_max : ℕ

The limit for our 64 bit → 128 bit multiplication

Equations

• Floating.mul_n_max = (2 ^ 63 - 1) ^ 2

theorem Floating.mul_n_le {x y : Floating} (x0 : 0 ≤ x.val) (y0 : 0 ≤ y.val) : (mul128 x.n.toUInt64 y.n.toUInt64).toNat ≤ mul_n_max

Our 64 → 128 bit integer multiplication doesn't get too big

Normalization of the inner integer multiplication

@[irreducible, inline]

def Floating.mul_norm (n : UInt128) (up : Bool) : UInt64 × UInt64

Normalize a 128-bit n into a 64-bit one, rounding and shifting as necessary. We also return how much we shifted left by.

Equations

• One or more equations did not get rendered due to their size.

theorem Floating.mul_norm_correct (n : UInt128) (up : Bool) (n0 : n ≠ 0) (lo : n.toNat ≤ mul_n_max) : (mul_norm n up).1.toNat ∈ Set.Ico (2 ^ 62) (2 ^ 63) ∧ Rounds (↑(mul_norm n up).1.toNat * 2 ^ (64 - ↑(mul_norm n up).2.toNat)) (↑n.toNat) up

mul_norm returns a normalized, correctly rounded value.

I think writing a bunch of separate lemmas in Add.lean made the result super long. Part of that is that the situation was very non-modular, as the component routine semantics were very coupled. Here in Mul.lean things are hopefully better factored, and ideally that means only mul_norm needs to know the internals of the mul_norm proof.

The definition of multiplication

theorem Floating.valid_mul_finish (n : UInt64) (s : Int128) (norm : n.toNat ∈ Set.Ico (2 ^ 62) (2 ^ 63)) : Valid n.toInt64 s.n.lo

mul_finish is valid

@[irreducible, inline]

def Floating.mul_finish (n : UInt64) (s : Int128) (up : Bool) (norm : n.toNat ∈ Set.Ico (2 ^ 62) (2 ^ 63)) : Floating

Build a Floating with value n * 2^s, rounding if necessary

Equations

• Floating.mul_finish n s up norm = bif s.n.hi == 0 then { n := n.toInt64, s := s.n.lo, v := ⋯ } else bif s.isNeg then bif up then Floating.min_norm else 0 else nan

@[irreducible, inline]

def Floating.mul_exponent (xs ys t : UInt64) : Int128

Twos complement, 128-bit exponent e = xs + ys + t + 64 - 2^63

Equations

• Floating.mul_exponent xs ys t = ↑xs + ↑ys - ↑t - Int128.ofNat (2 ^ 63 - 64)

@[irreducible, inline]

def Floating.mul_of_nonneg (x y : Floating) (up : Bool) (x0 : 0 ≤ x.val) (y0 : 0 ≤ y.val) : Floating

Multiply two nonnegative, non-nan Floatings

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Floating.mul (x y : Floating) (up : Bool) : Floating

Floating point multiply

Equations

• x.mul y up = if n : x = nan ∨ y = nan then nan else have p := x.n.isNeg != y.n.isNeg; have z := x.abs.mul_of_nonneg y.abs (up != p) ⋯ ⋯; bif p then -z else z

Multiplication is correct

theorem Floating.mul_finish_correct (n : UInt64) (s : Int128) (up : Bool) (norm : n.toNat ∈ Set.Ico (2 ^ 62) (2 ^ 63)) : Rounds (mul_finish n s up norm) (↑n.toNat * 2 ^ (↑s - 2 ^ 63)) up

mul_finish is correct

theorem Floating.mul_exponent_eq (xs ys t : UInt64) : ↑(mul_exponent xs ys t) = ↑xs.toNat + ↑ys.toNat + 64 - ↑t.toNat - 2 ^ 63

mul_exponent is correct

theorem Floating.approx_mul_of_nonneg {x' y' : ℝ} {x y : Floating} {up : Bool} {x0 : 0 ≤ x.val} {y0 : 0 ≤ y.val} (ax : approx x x') (ay : approx y y') : Rounds (x.mul_of_nonneg y up x0 y0) (x' * y') up

mul_of_nonneg rounds in the correct direction

theorem Floating.approx_mul {x' y' : ℝ} (x y : Floating) (up : Bool) (ax : approx x x') (ay : approx y y') : Rounds (x.mul y up) (x' * y') up

mul rounds in the correct direction

Additional multiplication lemmas

@[simp]

theorem Floating.mul_nan {x : Floating} {up : Bool} : x.mul nan up = nan

mul propagates nan

@[simp]

theorem Floating.nan_mul {x : Floating} {up : Bool} : nan.mul x up = nan

mul propagates nan

theorem Floating.ne_nan_of_mul {x y : Floating} {up : Bool} (n : x.mul y up ≠ nan) : x ≠ nan ∧ y ≠ nan

mul propagates nan

theorem Floating.mul_le {x y : Floating} (n : x.mul y false ≠ nan) : (x.mul y false).val ≤ x.val * y.val

mul _ _ false rounds down

theorem Floating.le_mul {x y : Floating} (n : x.mul y true ≠ nan) : x.val * y.val ≤ (x.mul y true).val

mul _ _ true rounds up