def oneE5M10 : PackedFloat 5 10

Equations

• oneE5M10 = PackedFloat.ofBits 5 10 15360#16

def twoE5M10 : PackedFloat 5 10

Equations

• twoE5M10 = PackedFloat.ofBits 5 10 16384#16

theorem FP16_e_lt_of_lt (a b : PackedFloat 5 10) : lt a b = true ↔ e_lt (a.toEFixed ⋯) (b.toEFixed ⋯) = true

theorem FP16_le_of_e_le (m : RoundingMode) (a b : EFixedPoint 43 24) : e_le a b = true → le (round 5 10 m a) (round 5 10 m b) = true

theorem FP16_e_le_of_le (a b : PackedFloat 5 10) : le a b = true → e_le (a.toEFixed ⋯) (b.toEFixed ⋯) = true

theorem FP16_toEFixed_isExactFloat (a : PackedFloat 5 10) : isExactFloat 5 10 (a.toEFixed ⋯) = true

Every floating point number converted to fixed point form, is an exact floating point number.

theorem FP16_isExactFloat_round_toEFixed (a : EFixedPoint 42 24) (m : RoundingMode) (ha : isExactFloat 5 10 a = true) : a.equal_denotation ((round 5 10 m a).toEFixed ⋯) = true

If a fixed point number is an exact floating point number, then converting to floating point and back should not change the denotation.

theorem FP16_round_leftinv_toEFixed (x : PackedFloat 5 10) (mode : RoundingMode) (hx : ¬x.isNaN = true) : round 5 10 mode (x.toEFixed ⋯) = x

Fixed -> Float rounding is left inverse to Float -> Fixed conversion

theorem FP16_f_add_comm (m : RoundingMode) (a b : FixedPoint 42 24) : f_add m a b = f_add m b a

theorem FP16_e_add_comm (m : RoundingMode) (a b : EFixedPoint 42 24) : e_add m a b = e_add m b a

theorem FP16_add_comm (m : RoundingMode) (a b : PackedFloat 5 10) : add ⋯ a b m = add ⋯ b a m

theorem FP16_add_neg_self_isZero_or_isNaN (a : PackedFloat 5 10) (m : RoundingMode) : (add ⋯ a (neg a) m).isZero = true ∨ (add ⋯ a (neg a) m).isNaN = true

theorem FP16_add_zero_is_id (a : PackedFloat 5 10) (m : RoundingMode) (ha : ¬a.isNaN = true ∧ ¬a.isZero = true) : add ⋯ a (PackedFloat.getZero 5 10) m = a

theorem FP16_e_add_monotone (m : RoundingMode) (a b c : EFixedPoint 42 24) (hc : c.state = State.Number) : e_le a b = true → e_le (e_add m a c) (e_add m b c) = true

theorem FP16_add_monotone (a b c : PackedFloat 5 10) (m : RoundingMode) (hc : c.isNormOrSubnorm = true) : le a b = true → le (add ⋯ a c m) (add ⋯ b c m) = true

theorem FP16_sterbenz (a b : PackedFloat 5 10) (h : le a (doubleRNE b) = true ∧ le b (doubleRNE a) = true) : isExactFloat 5 10 (e_add RoundingMode.RTZ (a.toEFixed ⋯) ((neg b).toEFixed ⋯)) = true

A floating-point subtraction is computed exactly iff the operands are within a factor of two of each other.

• https://en.wikipedia.org/wiki/Sterbenz_lemma

theorem FP16_mul_comm (a b : PackedFloat 5 10) (m : RoundingMode) : mul a b m = mul b a m

NOTE: bv_decide SAT solver times out on this theorem.

theorem FP16_mul_one_is_id (a : PackedFloat 5 10) (m : RoundingMode) (ha : ¬a.isNaN = true) : mul a oneE5M10 m = a

theorem FP16_add_eq_mul_two (a : PackedFloat 5 10) (m : RoundingMode) : add ⋯ a a m = mul twoE5M10 a m

theorem FP16_doubleRNE_eq_mul_two (a : PackedFloat 5 10) : doubleRNE a = mul twoE5M10 a RoundingMode.RNE

theorem FP16_f_mul_comm (a b : FixedPoint 42 24) : f_mul a b = f_mul b a

theorem FP16_e_mul_comm (a b : EFixedPoint 42 24) : e_mul a b = e_mul b a

theorem FP16_mulfixed_comm (a b : PackedFloat 5 10) (m : RoundingMode) : mulfixed ⋯ a b m = mulfixed ⋯ b a m

theorem FP16_div_one_is_id (a : PackedFloat 5 10) (h : ¬a.isNaN = true) : div a oneE5M10 RoundingMode.RTZ = a

theorem FP16_div_self_is_one (a : PackedFloat 5 10) (h : ¬a.isNaN = true ∧ ¬a.isInfinite = true ∧ ¬a.isZero = true) : div a a RoundingMode.RTZ = oneE5M10

theorem FP16_sterbenzFP16 (a b : PackedFloat 5 10) (h : le a (doubleRNE b) = true ∧ le b (doubleRNE a) = true) : isExactFloat 5 10 (e_add RoundingMode.RTZ (a.toEFixed ⋯) ((neg b).toEFixed ⋯)) = true