Correctness of IEEE binary arithmetic

The executable operations in Model first decode finite operands to exact dyadics, perform integer arithmetic, and round once in the destination format. This module proves the corresponding real-number statements uniformly in the exponent and fraction widths for descriptors satisfying fmt.isIEEE = true.

The result-finiteness hypotheses exclude IEEE overflow to infinity. NaNs and infinities are covered by the executable special-value rules, but they do not have values in this real-number semantics.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_add_of_abs_toReal_add_le_posMaxFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hbound : |x.toReal + y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.add y).isFinite = true

Finite operands whose exact real sum is within the destination's largest finite magnitude cannot overflow under nearest-even addition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_add_of_abs_add_le_posMaxFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hbound : |x.toReal| + |y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.add y).isFinite = true

The triangle bound |x| + |y| ≤ maxFinite is a symbolic sufficient condition for finite nearest-even addition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_add_eq_roundAt {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hfin : (x.add y).isFinite = true) : (x.add y).toReal = roundAt fmt (x.toReal + y.toReal)

Finite addition is exact real addition followed by one nearest-even format rounding.

The hypothesis hfin excludes overflow: it asks that the executable sum itself be finite, which is decidable on the result. toReal_add_eq_roundAt_of_abs_add_le_posMaxFinite replaces that observation by a symbolic bound on the operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_add_eq_roundAt_of_abs_add_le_posMaxFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hbound : |x.toReal| + |y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.add y).toReal = roundAt fmt (x.toReal + y.toReal)

Finite addition under a symbolic triangle bound is exact real addition followed by one nearest-even format rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_mul_of_abs_mul_le_posMaxFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hbound : |x.toReal| * |y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.mul y).isFinite = true

Finite operands whose exact real product is within the destination's largest finite magnitude cannot overflow under nearest-even multiplication.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_mul_eq_roundAt {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hfin : (x.mul y).isFinite = true) : (x.mul y).toReal = roundAt fmt (x.toReal * y.toReal)

Finite multiplication is exact real multiplication followed by one nearest-even rounding.

The hypothesis hfin excludes overflow by asking that the executable product be finite; toReal_mul_eq_roundAt_of_abs_mul_le_posMaxFinite supplies it from a bound on the operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_mul_eq_roundAt_of_abs_mul_le_posMaxFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hbound : |x.toReal| * |y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.mul y).toReal = roundAt fmt (x.toReal * y.toReal)

Finite multiplication under a symbolic magnitude-product bound is exact real multiplication followed by one nearest-even format rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_fma_of_abs_toReal_fma_le_posMaxFinite {fmt : FloatFormat} (x y z : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hz : z.isFinite = true) (hbound : |x.toReal * y.toReal + z.toReal| ≤ (posMaxFinite fmt).toReal) : (x.fma y z).isFinite = true

Finite operands whose exact fused result is within the destination's largest finite magnitude cannot overflow under nearest-even fused multiply-add.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_fma_of_abs_mul_add_le_posMaxFinite {fmt : FloatFormat} (x y z : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hz : z.isFinite = true) (hbound : |x.toReal| * |y.toReal| + |z.toReal| ≤ (posMaxFinite fmt).toReal) : (x.fma y z).isFinite = true

The triangle bound |x| * |y| + |z| ≤ maxFinite is a symbolic sufficient condition for finite nearest-even fused multiply-add.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_fma_eq_roundAt {fmt : FloatFormat} (x y z : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hz : z.isFinite = true) (hfin : (x.fma y z).isFinite = true) : (x.fma y z).toReal = roundAt fmt (x.toReal * y.toReal + z.toReal)

Finite fused multiply-add is exact real multiplication and addition followed by one rounding.

The hypothesis hfin excludes overflow by asking that the executable result be finite; toReal_fma_eq_roundAt_of_abs_mul_add_le_posMaxFinite supplies it from a bound on the operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_fma_eq_roundAt_of_abs_mul_add_le_posMaxFinite {fmt : FloatFormat} (x y z : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hz : z.isFinite = true) (hbound : |x.toReal| * |y.toReal| + |z.toReal| ≤ (posMaxFinite fmt).toReal) : (x.fma y z).toReal = roundAt fmt (x.toReal * y.toReal + z.toReal)

Finite fused multiply-add under a symbolic triangle bound is exact real FMA followed by one nearest-even format rounding.