Module ExtFloats

  unfold fast_isfinitef1. intros.
  rewrite Float32.to_of_bits.
  Local Transparent Float32.of_bits.
  unfold Float32.of_bits.
  Local Opaque Float32.of_bits.
  unfold Bits.b32_of_bits.
  unfold Bits.binary_float_of_bits, Bits.binary_float_of_bits_aux.
  pose proof (Int.eq_spec (Int.and x (Int.repr isfinitef1_mask)) (Int.repr isfinitef1_mask)) as SPEC.
  symmetry.
  rewrite is_finite_FF2B.
  destruct (Bits.split_bits 23 8 (Int.unsigned x)) as [[s m] e] eqn:BITS.
  unfold Bits.split_bits in BITS.
  injection BITS. intros EXP MANTISSA SIGN. clear BITS.
  change (Z.pow_pos 2 23) with (two_p 23) in EXP.
  rewrite <- Zbits.Zshiftr_div_two_p in EXP by lia.
  change (Z.pow_pos 2 8) with (two_p 8) in EXP.
  rewrite <- Zbits.Zzero_ext_mod in EXP by lia.
  destruct Int.eq.
  {
    replace e with (2^ 8 - 1).
    { simpl. destruct m; reflexivity. }
    subst e.
    apply Zbits.equal_same_bits.
    intros.
    rewrite Zbits.Zzero_ext_spec by assumption.
    change (2 ^ 8) with (two_p 8).
    rewrite Zbits.Ztestbit_two_p_m1 by lia.
    destruct Coqlib.zlt. 2: reflexivity.
    rewrite Z.shiftr_spec by lia.
    fold (Int.testbit x (i+23)).
    assert(BIT : Int.testbit (Int.and x (Int.repr isfinitef1_mask)) (i+23) =
             (Int.testbit (Int.repr isfinitef1_mask)) (i+23))
      by(f_equal; assumption).
    rewrite Int.bits_and in BIT by (change Int.zwordsize with 32; lia).
    rewrite Int.testbit_repr in BIT by (change Int.zwordsize with 32; lia).
    unfold isfinitef1_mask in *.
    rewrite Z.shiftl_spec in BIT by lia.
    replace (i +23-23) with i in BIT by ring.
    rewrite Zbits.Ztestbit_two_p_m1 in BIT by lia.
    destruct (Coqlib.zlt i 8). 2: lia.
    rewrite andb_true_r in BIT.
    symmetry. assumption.
  }
  assert (NEQ: e <> 255).
  { change 255 with (two_p 8 - 1).
    intro. subst e.
    apply SPEC. clear SPEC.
    apply Int.same_bits_eq.
    intros.
    rewrite Int.bits_and by assumption.
    unfold isfinitef1_mask.
    rewrite Int.testbit_repr by assumption.
    rewrite Z.shiftl_spec by lia.
    destruct (Z_lt_le_dec i 23).
    { rewrite Z.testbit_neg_r by lia.
      apply andb_false_r. }
    assert(BIT : Z.testbit (Zbits.Zzero_ext 8 (Z.shiftr (Int.unsigned x) 23)) ( i - 23) = Z.testbit (two_p 8 - 1) (i - 23)) by (f_equal; assumption).
    rewrite Zbits.Zzero_ext_spec in BIT by lia.
    rewrite Z.shiftr_spec in BIT by lia.
    rewrite Zbits.Ztestbit_two_p_m1 in * by lia.
    replace (i - 23 +23) with i in BIT by ring.
    fold (Int.testbit x i) in BIT.
    destruct Coqlib.zlt.
    { rewrite andb_true_r. assumption. }
    apply andb_false_r.
  }
  pose proof (Zeq_bool_if e (2^8 - 1)) as BLAH.
  destruct Zeq_bool.
  { simpl in BLAH. lia. }
  clear BLAH.
  assert (0 <= m) as m_NONNEG.
  { rewrite <- MANTISSA.
    apply Z_mod_nonneg_nonneg.
    pose proof (Int.unsigned_range x). lia.
    change (Z.pow_pos 2 23) with (2^23). lia.
  }
  pose proof (Zeq_bool_if e 0) as BLAH.
  destruct Zeq_bool.
  { destruct m; trivial. lia.
  }
  assert (0 < m + 2^23) by lia.
  destruct (m + 2^23); trivial; lia.
Qed.

  intro.
  rewrite <- (Float32.of_to_bits x).
  apply fast_isfinitef1_correct_bits.
Qed.

  unfold fast_isfinitef2. intros.
  rewrite Float32.to_of_bits.
  Local Transparent Float32.of_bits.
  unfold Float32.of_bits.
  Local Opaque Float32.of_bits.
  unfold Bits.b32_of_bits.
  unfold Bits.binary_float_of_bits, Bits.binary_float_of_bits_aux.
  pose proof (Int.eq_spec (Int.zero_ext 8 (Int.shru x (Int.repr 23)))
       (Int.repr isfinitef2_mask)) as SPEC.
  symmetry.
  rewrite is_finite_FF2B.
  destruct (Bits.split_bits 23 8 (Int.unsigned x)) as [[s m] e] eqn:BITS.
  unfold Bits.split_bits in BITS.
  injection BITS. intros EXP MANTISSA SIGN. clear BITS.
  change (Z.pow_pos 2 23) with (two_p 23) in EXP.
  rewrite <- Zbits.Zshiftr_div_two_p in EXP by lia.
  change (Z.pow_pos 2 8) with (two_p 8) in EXP.
  rewrite <- Zbits.Zzero_ext_mod in EXP by lia.
  destruct Int.eq.
  {
    replace e with (2^ 8 - 1).
    { destruct m; reflexivity. }
       
    subst e.
    apply Zbits.equal_same_bits.
    intros.
    rewrite Zbits.Zzero_ext_spec by assumption.
    change (2 ^ 8) with (two_p 8).
    rewrite Zbits.Ztestbit_two_p_m1 by lia.
    destruct Coqlib.zlt. 2: reflexivity.
    rewrite Z.shiftr_spec by lia.
    fold (Int.testbit x (i+23)).
    assert(BIT : Int.testbit (Int.zero_ext 8 (Int.shru x (Int.repr 23))) i =
             (Int.testbit (Int.repr isfinitef2_mask)) i)
      by(f_equal; assumption).
    rewrite Int.bits_zero_ext in BIT by (change Int.zwordsize with 32; lia).
    rewrite Int.testbit_repr in BIT by (change Int.zwordsize with 32; lia).
    unfold isfinitef2_mask in *.
    rewrite Int.bits_shru in BIT by (change Int.zwordsize with 32; lia).
    change (Int.unsigned (Int.repr 23)) with 23 in BIT.
    change Int.zwordsize with 32 in BIT.
    destruct Coqlib.zlt. 2: lia.
    rewrite Zbits.Ztestbit_two_p_m1 in BIT by lia.
    destruct (Coqlib.zlt i 8). 2: lia.
    destruct (Coqlib.zlt (i+23) 32). 2: lia.
    symmetry. assumption.
  }
  assert (NEQ: e <> 255).
  { change 255 with (two_p 8 - 1).
    intro. subst e.
    apply SPEC. clear SPEC.
    apply Int.same_bits_eq.
    intros.
    
    rewrite Int.bits_zero_ext by lia.
    unfold isfinitef2_mask.
    rewrite Int.testbit_repr by assumption.
    rewrite Int.bits_shru by lia.
    change (Int.unsigned (Int.repr 23)) with 23.
    change Int.zwordsize with 32.
    destruct (Z_lt_le_dec i 8).
    { destruct Coqlib.zlt. 2: lia.
      rewrite Zbits.Ztestbit_two_p_m1 by lia.
      destruct Coqlib.zlt. 2: lia.
      assert(BIT : Z.testbit (Zbits.Zzero_ext 8 (Z.shiftr (Int.unsigned x) 23)) i = Z.testbit (two_p 8 - 1) i) by (f_equal; assumption).
      rewrite Zbits.Zzero_ext_spec in BIT by lia.
      destruct Coqlib.zlt. 2: lia.
      rewrite Z.shiftr_spec in BIT by lia.
      rewrite Zbits.Ztestbit_two_p_m1 in * by lia.
      destruct Coqlib.zlt. 2: lia.
      assumption.
    }
    rewrite Zbits.Ztestbit_two_p_m1 by lia.
    destruct (Coqlib.zlt i 8). lia.
    reflexivity.
  }
  pose proof (Zeq_bool_if e (2^8 - 1)) as BLAH.
  destruct Zeq_bool.
  { simpl in BLAH. lia. }
  clear BLAH.
  assert (0 <= m) as m_NONNEG.
  { rewrite <- MANTISSA.
    apply Z_mod_nonneg_nonneg.
    pose proof (Int.unsigned_range x). lia.
    change (Z.pow_pos 2 23) with (2^23). lia.
  }
  pose proof (Zeq_bool_if e 0) as BLAH.
  destruct Zeq_bool.
  { destruct m; trivial. lia.
  }
  assert (0 < m + 2^23) by lia.
  destruct (m + 2^23); trivial; lia.
Qed.

  intro.
  rewrite <- (Float32.of_to_bits x).
  apply fast_isfinitef2_correct_bits.
Qed.

  unfold fast_isfinite. intros.
  rewrite Float.to_of_bits.
  Local Transparent Float.of_bits.
  unfold Float.of_bits.
  Local Opaque Float.of_bits.
  unfold Bits.b64_of_bits.
  unfold Bits.binary_float_of_bits, Bits.binary_float_of_bits_aux.
  pose proof (Int.eq_spec (Int.zero_ext 11 (Int.shru (Int64.hiword x) (Int.repr 20)))
       (Int.repr isfinite_mask)) as SPEC.
  symmetry.
  rewrite is_finite_FF2B.
  destruct (Bits.split_bits 52 11 (Int64.unsigned x)) as [[s m] e] eqn:BITS.
  unfold Bits.split_bits in BITS.
  injection BITS. intros EXP MANTISSA SIGN. clear BITS.
  change (Z.pow_pos 2 52) with (two_p 52) in EXP.
  rewrite <- Zbits.Zshiftr_div_two_p in EXP by lia.
  change (Z.pow_pos 2 11) with (two_p 11) in EXP.
  rewrite <- Zbits.Zzero_ext_mod in EXP by lia.
  destruct Int.eq.
  {
    replace e with (2^ 11 - 1).
    { destruct m; reflexivity. }
       
    subst e.
    apply Zbits.equal_same_bits.
    intros.
    rewrite Zbits.Zzero_ext_spec by assumption.
    change (2 ^ 11) with (two_p 11).
    rewrite Zbits.Ztestbit_two_p_m1 by lia.
    destruct Coqlib.zlt. 2: reflexivity.
    rewrite Z.shiftr_spec by lia.
    fold (Int64.testbit x (i+52)).
    assert(BIT : Int.testbit (Int.zero_ext 11 (Int.shru (Int64.hiword x) (Int.repr 20))) i =
             (Int.testbit (Int.repr isfinite_mask)) i)
      by(f_equal; assumption).
    rewrite Int.bits_zero_ext in BIT by (change Int.zwordsize with 32; lia).
    rewrite Int.testbit_repr in BIT by (change Int.zwordsize with 32; lia).
    unfold isfinite_mask in *.
    rewrite Int.bits_shru in BIT by (change Int.zwordsize with 32; lia).
    change (Int.unsigned (Int.repr 20)) with 20 in BIT.
    rewrite Int64.bits_hiword in BIT by (change Int.zwordsize with 32; lia).
    change Int.zwordsize with 32 in BIT.
    destruct Coqlib.zlt. 2: lia.
    rewrite Zbits.Ztestbit_two_p_m1 in BIT by lia.
    destruct (Coqlib.zlt i 11). 2: lia.
    destruct (Coqlib.zlt (i+20) 32). 2: lia.
    replace (i + 20 + 32) with (i + 52) in BIT by lia.
    symmetry. assumption.
  }
  assert (NEQ: e <> 2047).
  { change 2047 with (two_p 11 - 1).
    intro. subst e.
    apply SPEC. clear SPEC.
    apply Int.same_bits_eq.
    intros.
    
    rewrite Int.bits_zero_ext by lia.
    unfold isfinite_mask.
    rewrite Int.testbit_repr by assumption.
    rewrite Int.bits_shru by lia.
    change (Int.unsigned (Int.repr 20)) with 20.
    change Int.zwordsize with 32.
    destruct (Z_lt_le_dec i 11).
    { rewrite Int64.bits_hiword by (change Int.zwordsize with 32; lia).
      destruct Coqlib.zlt. 2: lia.
      rewrite Zbits.Ztestbit_two_p_m1 by lia.
      destruct Coqlib.zlt. 2: lia.
      assert(BIT : Z.testbit (Zbits.Zzero_ext 11 (Z.shiftr (Int64.unsigned x) 52)) i = Z.testbit (two_p 11 - 1) i) by (f_equal; assumption).
      rewrite Zbits.Zzero_ext_spec in BIT by lia.
      destruct Coqlib.zlt. 2: lia.
      rewrite Z.shiftr_spec in BIT by lia.
      rewrite Zbits.Ztestbit_two_p_m1 in * by lia.
      destruct Coqlib.zlt. 2: lia.
      change Int.zwordsize with 32.
      replace (i+20+32) with (i+52) by lia.
      assumption.
    }
    rewrite Zbits.Ztestbit_two_p_m1 by lia.
    destruct (Coqlib.zlt i 11). lia.
    reflexivity.
  }
  pose proof (Zeq_bool_if e (2^11 - 1)) as BLAH.
  destruct Zeq_bool.
  { simpl in BLAH. lia. }
  clear BLAH.
  assert (0 <= m) as m_NONNEG.
  { rewrite <- MANTISSA.
    apply Z_mod_nonneg_nonneg.
    pose proof (Int64.unsigned_range x). lia.
    change (Z.pow_pos 2 52) with (2^52). lia.
  }
  pose proof (Zeq_bool_if e 0) as BLAH.
  destruct Zeq_bool.
  { destruct m; trivial. lia.
  }
  assert (0 < m + 2^52) by lia.
  destruct (m + 2^52); trivial; lia.
Qed.

  intro.
  rewrite <- (Float.of_to_bits x).
  apply fast_isfinite_correct_bits.
Qed.