Theory: lift_machine

Theorems

fp16_float_add_relative

⊢ ∀a b.
    fp16_isFinite a ∧ fp16_isFinite b ∧
    abs (fp16_to_real a + fp16_to_real b) ∈
    ⦋1 / 2 pow 14 ⬝ 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)⟯ ⇒
    fp16_isFinite (fp16_add roundTiesToEven a b) ∧
    ∃e. abs e ≤ 1 / 2 pow 11 ∧
        fp16_to_real (fp16_add roundTiesToEven a b) =
        (fp16_to_real a + fp16_to_real b) * (1 + e)

fp16_float_div_relative

⊢ ∀a b.
    fp16_isFinite a ∧ fp16_isFinite b ∧ ¬fp16_isZero b ∧
    abs (fp16_to_real a / fp16_to_real b) ∈
    ⦋1 / 2 pow 14 ⬝ 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)⟯ ⇒
    fp16_isFinite (fp16_div roundTiesToEven a b) ∧
    ∃e. abs e ≤ 1 / 2 pow 11 ∧
        fp16_to_real (fp16_div roundTiesToEven a b) =
        fp16_to_real a / fp16_to_real b * (1 + e)

fp16_float_mul_add_relative

⊢ ∀a b c.
    fp16_isFinite a ∧ fp16_isFinite b ∧ fp16_isFinite c ∧
    abs (fp16_to_real a * fp16_to_real b + fp16_to_real c) ∈
    ⦋1 / 2 pow 14 ⬝ 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)⟯ ⇒
    fp16_isFinite (fp16_mul_add roundTiesToEven a b c) ∧
    ∃e. abs e ≤ 1 / 2 pow 11 ∧
        fp16_to_real (fp16_mul_add roundTiesToEven a b c) =
        (fp16_to_real a * fp16_to_real b + fp16_to_real c) * (1 + e)

fp16_float_mul_relative

⊢ ∀a b.
    fp16_isFinite a ∧ fp16_isFinite b ∧
    abs (fp16_to_real a * fp16_to_real b) ∈
    ⦋1 / 2 pow 14 ⬝ 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)⟯ ⇒
    fp16_isFinite (fp16_mul roundTiesToEven a b) ∧
    ∃e. abs e ≤ 1 / 2 pow 11 ∧
        fp16_to_real (fp16_mul roundTiesToEven a b) =
        fp16_to_real a * fp16_to_real b * (1 + e)

fp16_float_mul_sub_relative

⊢ ∀a b c.
    fp16_isFinite a ∧ fp16_isFinite b ∧ fp16_isFinite c ∧
    abs (fp16_to_real a * fp16_to_real b − fp16_to_real c) ∈
    ⦋1 / 2 pow 14 ⬝ 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)⟯ ⇒
    fp16_isFinite (fp16_mul_sub roundTiesToEven a b c) ∧
    ∃e. abs e ≤ 1 / 2 pow 11 ∧
        fp16_to_real (fp16_mul_sub roundTiesToEven a b c) =
        (fp16_to_real a * fp16_to_real b − fp16_to_real c) * (1 + e)

fp16_float_sqrt_relative

⊢ ∀a. fp16_isFinite a ∧ (¬word_msb a ∨ a = 32768w) ∧
      abs (sqrt (fp16_to_real a)) ∈
      ⦋1 / 2 pow 14 ⬝ 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)⟯ ⇒
      fp16_isFinite (fp16_sqrt roundTiesToEven a) ∧
      ∃e. abs e ≤ 1 / 2 pow 11 ∧
          fp16_to_real (fp16_sqrt roundTiesToEven a) =
          sqrt (fp16_to_real a) * (1 + e)

fp16_float_sub_relative

⊢ ∀a b.
    fp16_isFinite a ∧ fp16_isFinite b ∧
    abs (fp16_to_real a − fp16_to_real b) ∈
    ⦋1 / 2 pow 14 ⬝ 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)⟯ ⇒
    fp16_isFinite (fp16_sub roundTiesToEven a b) ∧
    ∃e. abs e ≤ 1 / 2 pow 11 ∧
        fp16_to_real (fp16_sub roundTiesToEven a b) =
        (fp16_to_real a − fp16_to_real b) * (1 + e)

fp32_float_add_relative

⊢ ∀a b.
    fp32_isFinite a ∧ fp32_isFinite b ∧
    abs (fp32_to_real a + fp32_to_real b) ∈
    ⦋1 / 2 pow 126 ⬝ 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)⟯ ⇒
    fp32_isFinite (fp32_add roundTiesToEven a b) ∧
    ∃e. abs e ≤ 1 / 2 pow 24 ∧
        fp32_to_real (fp32_add roundTiesToEven a b) =
        (fp32_to_real a + fp32_to_real b) * (1 + e)

fp32_float_div_relative

⊢ ∀a b.
    fp32_isFinite a ∧ fp32_isFinite b ∧ ¬fp32_isZero b ∧
    abs (fp32_to_real a / fp32_to_real b) ∈
    ⦋1 / 2 pow 126 ⬝ 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)⟯ ⇒
    fp32_isFinite (fp32_div roundTiesToEven a b) ∧
    ∃e. abs e ≤ 1 / 2 pow 24 ∧
        fp32_to_real (fp32_div roundTiesToEven a b) =
        fp32_to_real a / fp32_to_real b * (1 + e)

fp32_float_mul_add_relative

⊢ ∀a b c.
    fp32_isFinite a ∧ fp32_isFinite b ∧ fp32_isFinite c ∧
    abs (fp32_to_real a * fp32_to_real b + fp32_to_real c) ∈
    ⦋1 / 2 pow 126 ⬝ 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)⟯ ⇒
    fp32_isFinite (fp32_mul_add roundTiesToEven a b c) ∧
    ∃e. abs e ≤ 1 / 2 pow 24 ∧
        fp32_to_real (fp32_mul_add roundTiesToEven a b c) =
        (fp32_to_real a * fp32_to_real b + fp32_to_real c) * (1 + e)

fp32_float_mul_relative

⊢ ∀a b.
    fp32_isFinite a ∧ fp32_isFinite b ∧
    abs (fp32_to_real a * fp32_to_real b) ∈
    ⦋1 / 2 pow 126 ⬝ 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)⟯ ⇒
    fp32_isFinite (fp32_mul roundTiesToEven a b) ∧
    ∃e. abs e ≤ 1 / 2 pow 24 ∧
        fp32_to_real (fp32_mul roundTiesToEven a b) =
        fp32_to_real a * fp32_to_real b * (1 + e)

fp32_float_mul_sub_relative

⊢ ∀a b c.
    fp32_isFinite a ∧ fp32_isFinite b ∧ fp32_isFinite c ∧
    abs (fp32_to_real a * fp32_to_real b − fp32_to_real c) ∈
    ⦋1 / 2 pow 126 ⬝ 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)⟯ ⇒
    fp32_isFinite (fp32_mul_sub roundTiesToEven a b c) ∧
    ∃e. abs e ≤ 1 / 2 pow 24 ∧
        fp32_to_real (fp32_mul_sub roundTiesToEven a b c) =
        (fp32_to_real a * fp32_to_real b − fp32_to_real c) * (1 + e)

fp32_float_sqrt_relative

⊢ ∀a. fp32_isFinite a ∧ (¬word_msb a ∨ a = 0x80000000w) ∧
      abs (sqrt (fp32_to_real a)) ∈
      ⦋1 / 2 pow 126 ⬝ 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)⟯ ⇒
      fp32_isFinite (fp32_sqrt roundTiesToEven a) ∧
      ∃e. abs e ≤ 1 / 2 pow 24 ∧
          fp32_to_real (fp32_sqrt roundTiesToEven a) =
          sqrt (fp32_to_real a) * (1 + e)

fp32_float_sub_relative

⊢ ∀a b.
    fp32_isFinite a ∧ fp32_isFinite b ∧
    abs (fp32_to_real a − fp32_to_real b) ∈
    ⦋1 / 2 pow 126 ⬝ 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)⟯ ⇒
    fp32_isFinite (fp32_sub roundTiesToEven a b) ∧
    ∃e. abs e ≤ 1 / 2 pow 24 ∧
        fp32_to_real (fp32_sub roundTiesToEven a b) =
        (fp32_to_real a − fp32_to_real b) * (1 + e)

fp64_float_add_relative

⊢ ∀a b.
    fp64_isFinite a ∧ fp64_isFinite b ∧
    abs (fp64_to_real a + fp64_to_real b) ∈
    ⦋1 / 2 pow 1022 ⬝ 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)⟯ ⇒
    fp64_isFinite (fp64_add roundTiesToEven a b) ∧
    ∃e. abs e ≤ 1 / 2 pow 53 ∧
        fp64_to_real (fp64_add roundTiesToEven a b) =
        (fp64_to_real a + fp64_to_real b) * (1 + e)

fp64_float_div_relative

⊢ ∀a b.
    fp64_isFinite a ∧ fp64_isFinite b ∧ ¬fp64_isZero b ∧
    abs (fp64_to_real a / fp64_to_real b) ∈
    ⦋1 / 2 pow 1022 ⬝ 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)⟯ ⇒
    fp64_isFinite (fp64_div roundTiesToEven a b) ∧
    ∃e. abs e ≤ 1 / 2 pow 53 ∧
        fp64_to_real (fp64_div roundTiesToEven a b) =
        fp64_to_real a / fp64_to_real b * (1 + e)

fp64_float_mul_add_relative

⊢ ∀a b c.
    fp64_isFinite a ∧ fp64_isFinite b ∧ fp64_isFinite c ∧
    abs (fp64_to_real a * fp64_to_real b + fp64_to_real c) ∈
    ⦋1 / 2 pow 1022 ⬝ 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)⟯ ⇒
    fp64_isFinite (fp64_mul_add roundTiesToEven a b c) ∧
    ∃e. abs e ≤ 1 / 2 pow 53 ∧
        fp64_to_real (fp64_mul_add roundTiesToEven a b c) =
        (fp64_to_real a * fp64_to_real b + fp64_to_real c) * (1 + e)

fp64_float_mul_relative

⊢ ∀a b.
    fp64_isFinite a ∧ fp64_isFinite b ∧
    abs (fp64_to_real a * fp64_to_real b) ∈
    ⦋1 / 2 pow 1022 ⬝ 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)⟯ ⇒
    fp64_isFinite (fp64_mul roundTiesToEven a b) ∧
    ∃e. abs e ≤ 1 / 2 pow 53 ∧
        fp64_to_real (fp64_mul roundTiesToEven a b) =
        fp64_to_real a * fp64_to_real b * (1 + e)

fp64_float_mul_sub_relative

⊢ ∀a b c.
    fp64_isFinite a ∧ fp64_isFinite b ∧ fp64_isFinite c ∧
    abs (fp64_to_real a * fp64_to_real b − fp64_to_real c) ∈
    ⦋1 / 2 pow 1022 ⬝ 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)⟯ ⇒
    fp64_isFinite (fp64_mul_sub roundTiesToEven a b c) ∧
    ∃e. abs e ≤ 1 / 2 pow 53 ∧
        fp64_to_real (fp64_mul_sub roundTiesToEven a b c) =
        (fp64_to_real a * fp64_to_real b − fp64_to_real c) * (1 + e)

fp64_float_sqrt_relative

⊢ ∀a. fp64_isFinite a ∧ (¬word_msb a ∨ a = 0x8000000000000000w) ∧
      abs (sqrt (fp64_to_real a)) ∈
      ⦋1 / 2 pow 1022 ⬝ 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)⟯ ⇒
      fp64_isFinite (fp64_sqrt roundTiesToEven a) ∧
      ∃e. abs e ≤ 1 / 2 pow 53 ∧
          fp64_to_real (fp64_sqrt roundTiesToEven a) =
          sqrt (fp64_to_real a) * (1 + e)

fp64_float_sub_relative

⊢ ∀a b.
    fp64_isFinite a ∧ fp64_isFinite b ∧
    abs (fp64_to_real a − fp64_to_real b) ∈
    ⦋1 / 2 pow 1022 ⬝ 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)⟯ ⇒
    fp64_isFinite (fp64_sub roundTiesToEven a b) ∧
    ∃e. abs e ≤ 1 / 2 pow 53 ∧
        fp64_to_real (fp64_sub roundTiesToEven a b) =
        (fp64_to_real a − fp64_to_real b) * (1 + e)

Theory lift_machine_ieee

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems