path: root/src/common/IntegerExtra.v

(*
 * Vericert: Verified high-level synthesis.
 * Copyright (C) 2020-2021 Yann Herklotz <yann@yannherklotz.com>
 *               2020 James Pollard <j@mes.dev>
 *
 * This program is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program.  If not, see <https://www.gnu.org/licenses/>.
 *)

Require Import Coq.ZArith.BinInt.
Require Import Coq.micromega.Lia.
Require Import Coq.Numbers.Integer.Binary.ZBinary.

Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.

Require Import vericert.common.Vericertlib.

Local Open Scope Z_scope.

Module PtrofsExtra.

  Ltac ptrofs_mod_match m :=
    match goal with
    | [ H : ?x = 0 |- context[?x] ] => rewrite H
    | [ _ : _ |- context[_ - 0] ] => rewrite Z.sub_0_r
    | [ _ : _ |- context[0 + _] ] => rewrite Z.add_0_l
    | [ _ : _ |- context[_ + 0] ] => rewrite Z.add_0_r
    | [ _ : _ |- context[0 * _] ] => rewrite Z.mul_0_l
    | [ _ : _ |- context[_ * 0] ] => rewrite Z.mul_0_r
    | [ _ : _ |- context[?m mod ?m] ] =>
      rewrite Z_mod_same_full with (a := m)
    | [ _ : _ |- context[0 mod _] ] =>
      rewrite Z.mod_0_l
    | [ _ : _ |- context[(_ mod ?m) mod ?m] ] =>
      rewrite Zmod_mod
    | [ _ : _ |- context[(_ mod Ptrofs.modulus) mod m ] ] =>
      rewrite <- Zmod_div_mod;
      try (crush; lia || assumption)

    | [ _ : _ |- context[Ptrofs.modulus mod m] ] =>
      rewrite Zdivide_mod with (a := Ptrofs.modulus);
      try (lia || assumption)

    | [ _ : _ |- context[Ptrofs.signed ?a mod Ptrofs.modulus] ] =>
      rewrite Z.mod_small with (a := Ptrofs.signed a) (b := Ptrofs.modulus)

    | [ _ : _ |- context[(?x - ?y) mod ?m] ] =>
      rewrite Zminus_mod with (a := x) (b := y) (n := m)

    | [ _ : _ |- context[((?x + ?y) mod ?m) + _] ] =>
      rewrite Zplus_mod with (a := x) (b := y) (n := m)
    | [ _ : _ |- context[(?x + ?y) mod ?m] ] =>
      rewrite Zplus_mod with (a := x) (b := y) (n := m)

    | [ _ : _ |- context[(?x * ?y) mod ?m] ] =>
      rewrite Zmult_mod with (a := x) (b := y) (n := m)
    end.

  Ltac ptrofs_mod_tac m :=
    repeat (ptrofs_mod_match m); lia.

  Lemma signed_mod_unsigned_mod :
    forall x m,
      0 < m ->
      Ptrofs.modulus mod m = 0 ->
      Ptrofs.signed x mod m = 0 ->
      Ptrofs.unsigned x mod m = 0.
  Proof.
    intros.

    repeat match goal with
           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
           | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
             rewrite <- Zmod_div_mod; try lia; try assumption
           | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed
           end; try crush; ptrofs_mod_tac m.
  Qed.

  Lemma of_int_mod :
    forall x m,
      Int.unsigned x mod m = 0 ->
      Ptrofs.unsigned (Ptrofs.of_int x) mod m = 0.
  Proof.
    intros.
    unfold Ptrofs.of_int.
    rewrite Ptrofs.unsigned_repr; crush;
      apply Int.unsigned_range_2.
  Qed.

  Lemma mul_mod :
    forall x y m,
      0 < m ->
      (m | Ptrofs.modulus) ->
      Ptrofs.unsigned x mod m = 0 ->
      Ptrofs.unsigned y mod m = 0 ->
      (Ptrofs.signed (Ptrofs.mul x y)) mod m = 0.
  Proof.
    intros. unfold Ptrofs.mul.
    rewrite Ptrofs.signed_repr_eq.

    repeat match goal with
           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
           | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
             rewrite <- Zmod_div_mod; try lia; try assumption
           end; try(crush; lia); ptrofs_mod_tac m.
  Qed.

  Lemma add_mod :
    forall x y m,
      0 < m ->
      (m | Ptrofs.modulus) ->
      Ptrofs.unsigned x mod m = 0 ->
      Ptrofs.unsigned y mod m = 0 ->
      (Ptrofs.unsigned (Ptrofs.add x y)) mod m = 0.
  Proof.
    intros. unfold Ptrofs.add.
    rewrite Ptrofs.unsigned_repr_eq.

    repeat match goal with
           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
           | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
             rewrite <- Zmod_div_mod; try lia; try assumption
           end; try (crush; lia); ptrofs_mod_tac m.
  Qed.

  Lemma mul_divu :
    forall x y,
      0 < Ptrofs.unsigned x ->
      Ptrofs.unsigned y mod Ptrofs.unsigned x = 0 ->
      (Integers.Ptrofs.mul x (Integers.Ptrofs.divu y x)) = y.
  Proof.
    intros.

    assert (x <> Ptrofs.zero).
    { intro.
      rewrite H1 in H.
      replace (Ptrofs.unsigned Ptrofs.zero) with 0 in H by reflexivity.
      lia. }

    exploit (Ptrofs.modu_divu_Euclid y x); auto; intros.
    unfold Ptrofs.modu in H2. rewrite H0 in H2.
    replace (Ptrofs.repr 0) with Ptrofs.zero in H2 by reflexivity.
    rewrite Ptrofs.add_zero in H2.
    rewrite Ptrofs.mul_commut.
    congruence.
  Qed.

  Lemma divu_unsigned :
    forall x y,
      0 < Ptrofs.unsigned y ->
      Ptrofs.unsigned x <= Ptrofs.max_unsigned ->
      Ptrofs.unsigned (Ptrofs.divu x y) = Ptrofs.unsigned x / Ptrofs.unsigned y.
  Proof.
    intros.
    unfold Ptrofs.divu.
    rewrite Ptrofs.unsigned_repr; auto.
    split.
    apply Z.div_pos; auto.
    apply Ptrofs.unsigned_range.
    apply Z.div_le_upper_bound; auto.
    eapply Z.le_trans.
    exact H0.
    rewrite Z.mul_comm.
    apply Z.le_mul_diag_r; crush.
  Qed.

  Lemma mul_unsigned :
    forall x y,
      Ptrofs.mul x y =
      Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y).
  Proof.
    intros; unfold Ptrofs.mul.
    apply Ptrofs.eqm_samerepr.
    apply Ptrofs.eqm_mult; exists 0; lia.
  Qed.

  Lemma pos_signed_unsigned :
    forall x,
      0 <= Ptrofs.signed x ->
      Ptrofs.signed x = Ptrofs.unsigned x.
  Proof.
    intros.
    rewrite Ptrofs.unsigned_signed.
    destruct (Ptrofs.lt x Ptrofs.zero) eqn:EQ.
    unfold Ptrofs.lt in EQ.
    destruct (zlt (Ptrofs.signed x) (Ptrofs.signed Ptrofs.zero)); try discriminate.
    replace (Ptrofs.signed (Ptrofs.zero)) with 0 in l by reflexivity. lia.
    reflexivity.
  Qed.
End PtrofsExtra.

Ltac ptrofs :=
  repeat match goal with
         | [ |- context[Ptrofs.add (Ptrofs.zero) _] ] => setoid_rewrite Ptrofs.add_zero_l
         | [ H : context[Ptrofs.add (Ptrofs.zero) _] |- _ ] => setoid_rewrite Ptrofs.add_zero_l in H

         | [ |- context[Ptrofs.repr 0] ] => replace (Ptrofs.repr 0) with Ptrofs.zero by reflexivity
         | [ H : context[Ptrofs.repr 0] |- _ ] =>
           replace (Ptrofs.repr 0) with Ptrofs.zero in H by reflexivity

         | [ H: context[Ptrofs.unsigned (Ptrofs.repr (Ptrofs.unsigned _))] |- _ ] =>
           setoid_rewrite Ptrofs.unsigned_repr in H; [>| apply Ptrofs.unsigned_range_2]
         | [ |- context[Ptrofs.unsigned (Ptrofs.repr (Ptrofs.unsigned _))] ] =>
           rewrite Ptrofs.unsigned_repr; [>| apply Ptrofs.unsigned_range_2]

         | [ |- context[0 <= Ptrofs.unsigned _] ] => apply Ptrofs.unsigned_range_2
         end.

Module IntExtra.
  Import Int.
  Ltac int_mod_match m :=
    match goal with
    | [ H : ?x = 0 |- context[?x] ] => rewrite H
    | [ _ : _ |- context[_ - 0] ] => rewrite Z.sub_0_r
    | [ _ : _ |- context[0 + _] ] => rewrite Z.add_0_l
    | [ _ : _ |- context[_ + 0] ] => rewrite Z.add_0_r
    | [ _ : _ |- context[0 * _] ] => rewrite Z.mul_0_l
    | [ _ : _ |- context[_ * 0] ] => rewrite Z.mul_0_r
    | [ _ : _ |- context[?m mod ?m] ] =>
      rewrite Z_mod_same_full with (a := m)
    | [ _ : _ |- context[0 mod _] ] =>
      rewrite Z.mod_0_l
    | [ _ : _ |- context[(_ mod ?m) mod ?m] ] =>
      rewrite Zmod_mod
    | [ _ : _ |- context[(_ mod Int.modulus) mod m ] ] =>
      rewrite <- Zmod_div_mod;
      try (crush; lia || assumption)

    | [ _ : _ |- context[Int.modulus mod m] ] =>
      rewrite Zdivide_mod with (a := Int.modulus);
      try (lia || assumption)

    | [ _ : _ |- context[Int.signed ?a mod Int.modulus] ] =>
      rewrite Z.mod_small with (a := Int.signed a) (b := Int.modulus)

    | [ _ : _ |- context[(?x - ?y) mod ?m] ] =>
      rewrite Zminus_mod with (a := x) (b := y) (n := m)

    | [ _ : _ |- context[((?x + ?y) mod ?m) + _] ] =>
      rewrite Zplus_mod with (a := x) (b := y) (n := m)
    | [ _ : _ |- context[(?x + ?y) mod ?m] ] =>
      rewrite Zplus_mod with (a := x) (b := y) (n := m)

    | [ _ : _ |- context[(?x * ?y) mod ?m] ] =>
      rewrite Zmult_mod with (a := x) (b := y) (n := m)
    end.

  Ltac int_mod_tac m :=
    repeat (int_mod_match m); lia.

  Lemma mul_mod1 :
    forall x y m,
      0 < m ->
      (m | Int.modulus) ->
      Int.unsigned x mod m = 0 ->
      (Int.unsigned (Int.mul x y)) mod m = 0.
  Proof.
    intros. unfold Int.mul.
    rewrite Int.unsigned_repr_eq.

    repeat match goal with
           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
           | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
             rewrite <- Zmod_div_mod; try lia; try assumption
           end; try (crush; lia); int_mod_tac m.
  Qed.

  Lemma mul_mod2 :
    forall x y m,
      0 < m ->
      (m | Int.modulus) ->
      Int.unsigned y mod m = 0 ->
      (Int.unsigned (Int.mul x y)) mod m = 0.
  Proof.
    intros. unfold Int.mul.
    rewrite Int.unsigned_repr_eq.

    repeat match goal with
           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
           | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
             rewrite <- Zmod_div_mod; try lia; try assumption
           end; try (crush; lia); int_mod_tac m.
  Qed.

  Lemma add_mod :
    forall x y m,
      0 < m ->
      (m | Int.modulus) ->
      Int.unsigned x mod m = 0 ->
      Int.unsigned y mod m = 0 ->
      (Int.unsigned (Int.add x y)) mod m = 0.
  Proof.
    intros. unfold Int.add.
    rewrite Int.unsigned_repr_eq.

    repeat match goal with
           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
           | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
             rewrite <- Zmod_div_mod; try lia; try assumption
           end; try (crush; lia); int_mod_tac m.
  Qed.

  Definition ofbytes (a b c d : byte) : int :=
    or (shl (repr (Byte.unsigned a)) (repr (3 * Byte.zwordsize)))
       (or (shl (repr (Byte.unsigned b)) (repr (2 * Byte.zwordsize)))
           (or (shl (repr (Byte.unsigned c)) (repr Byte.zwordsize))
               (repr (Byte.unsigned d)))).

  Definition byte1 (n: int) : byte := Byte.repr (unsigned n).

  Definition byte2 (n: int) : byte := Byte.repr (unsigned (shru n (repr Byte.zwordsize))).

  Definition byte3 (n: int) : byte := Byte.repr (unsigned (shru n (repr (2 * Byte.zwordsize)))).

  Definition byte4 (n: int) : byte := Byte.repr (unsigned (shru n (repr (3 * Byte.zwordsize)))).

  Lemma bits_byte1:
    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n i.
  Proof.
    intros. unfold byte1. rewrite Byte.testbit_repr; auto.
  Qed.

  Lemma bits_byte2:
    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + Byte.zwordsize).
  Proof.
    intros. unfold byte2. rewrite Byte.testbit_repr; auto.
    assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
    fold (testbit (shru n (repr Byte.zwordsize)) i). rewrite bits_shru.
    change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize.
    apply zlt_true. lia. lia.
  Qed.

  Lemma bits_byte3:
    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (2 * Byte.zwordsize)).
  Proof.
    intros. unfold byte3. rewrite Byte.testbit_repr; auto.
    assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
    fold (testbit (shru n (repr (2 * Byte.zwordsize))) i). rewrite bits_shru.
    change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize).
    apply zlt_true. lia. lia.
  Qed.

  Lemma bits_byte4:
    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte4 n) i = testbit n (i + (3 * Byte.zwordsize)).
  Proof.
    intros. unfold byte4. rewrite Byte.testbit_repr; auto.
    assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
    fold (testbit (shru n (repr (3 * Byte.zwordsize))) i). rewrite bits_shru.
    change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize).
    apply zlt_true. lia. lia.
  Qed.

  Lemma div_divs_equiv :
    forall x y,
      signed x >= 0 ->
      signed y >= 0 ->
      divs x y = divu x y.
  Proof.
    unfold divs, divu.
    intros.
    rewrite !signed_eq_unsigned;
    try rewrite Zquot.Zquot_Zdiv_pos; try reflexivity;
    lazymatch goal with
    | |- unsigned _ <= max_signed =>
      solve [rewrite <- signed_positive; assumption]
    | |- 0 <= unsigned _ => solve [apply unsigned_range_2]
    end.
  Qed.

  Lemma neg_signed' :
    forall x : int,
      unsigned x <> 2147483648 ->
      signed (neg x) = - signed x.
  Proof.
    intros x Hhalf.
    Transparent repr.
    unfold signed.
    simpl.
    rewrite Z_mod_modulus_eq.
    replace modulus with 4294967296; auto.
    replace half_modulus with 2147483648; auto.
    repeat match goal with | |- context[if ?x then _ else _] => destruct x end.
    - destruct (Z.eq_dec (unsigned x) 0).
      + rewrite e. auto.
      + pose proof (Z.mod_opp_l_nz (unsigned x) 4294967296).
        assert (4294967296 <> 0) by lia.
        apply H in H0.
        rewrite H0 in l.
        pose proof (Z.mod_small (unsigned x) 4294967296).
        assert (0 <= unsigned x < 4294967296).
        pose proof (unsigned_range_2 x). lia.
        apply H1 in H2. rewrite H2 in l. lia.
        rewrite Z.mod_small. assumption.
        pose proof (unsigned_range_2 x). lia.
    - destruct (Z.eq_dec (unsigned x) 0).
      + lia.
      + rewrite Z.mod_opp_l_nz; try lia.
        rewrite Z.opp_sub_distr.
        rewrite Z.mod_small. lia.
        pose proof (unsigned_range_2 x).
        simplify; lia.
        rewrite Z.mod_small. assumption.
        pose proof (unsigned_range_2 x).
        simplify; lia.
    - destruct (Z.eq_dec (unsigned x) 0).
      + rewrite e in *. rewrite Z.opp_0 in *. rewrite Zmod_0_l in g. lia.
      + rewrite Z.mod_opp_l_nz; try lia.
        rewrite Z.mod_small. lia.
        pose proof (unsigned_range_2 x). lia.
        rewrite Z.mod_small. assumption.
        pose proof (unsigned_range_2 x). lia.
    - destruct (Z.eq_dec (unsigned x) 0).
      + lia.
      + rewrite Z.mod_opp_l_nz in g; try lia.
        rewrite Z.mod_small in g.
        assert (unsigned x < 2147483648) by lia. lia.
        pose proof (unsigned_range_2 x).
        replace max_unsigned with 4294967295 in * by auto. lia.
        rewrite Z.mod_small. assumption.
        pose proof (unsigned_range_2 x).
        replace max_unsigned with 4294967295 in * by auto. lia.
  Qed.

  Lemma neg_divs_distr_l :
    forall x y,
      unsigned x <> 2147483648 ->
      neg (divs x y) = divs (neg x) y.
  Proof.
    intros x y Hhalf. unfold divs, neg.
    set (x' := signed x). set (y' := signed y).
    apply eqm_samerepr.
    apply eqm_trans with (- (Z.quot x' y')).
    auto with ints.
    replace (- (Z.quot x' y')) with (Z.quot (- x') y')
      by (rewrite Zquot.Zquot_opp_l; auto).
    unfold x'.
    rewrite <- neg_signed'.
    auto with ints.
    assumption.
  Qed.

  Lemma neg_signed :
    forall x : int,
      unsigned x <> 2147483648 ->
      signed x < 0 ->
      signed (neg x) >= 0.
  Proof.
    intros.
    rewrite neg_signed'. lia.
    assumption.
  Qed.

  Lemma shl_signed_positive :
    forall y,
      unsigned y <= 30 ->
      signed (shl one y) >= 0.
  Proof.
    intros.
    unfold signed, shl.
    destruct (zlt (unsigned (repr (Z.shiftl (unsigned one) (unsigned y)))) half_modulus).
    - rewrite unsigned_repr.
      + rewrite Z.shiftl_1_l.
        apply Z.le_ge. apply Z.pow_nonneg. lia.
      + rewrite Z.shiftl_1_l. split.
        apply Z.pow_nonneg. lia.
        simplify.
        replace (4294967295) with (2 ^ 32 - 1); try lia.
        transitivity (2 ^ 31); try lia.
        apply Z.pow_le_mono_r; lia.
    - simplify. rewrite Z.shiftl_1_l in g.
      unfold half_modulus, modulus, wordsize,
      Wordsize_32.wordsize in *. unfold two_power_nat in *. simplify.
      unfold Z_mod_modulus in *.
      destruct (2 ^ unsigned y) eqn:?.
      apply Z.ge_le in g. exfalso.
      replace (4294967296 / 2) with (2147483648) in g; auto.
      rewrite Z.shiftl_1_l. rewrite Heqz.
      unfold wordsize in *. unfold Wordsize_32.wordsize in *.
      rewrite Zbits.P_mod_two_p_eq in *.
      replace (4294967296 / 2) with (2147483648) in g; auto.
      rewrite <- Heqz in g.
      rewrite Z.mod_small in g.
      replace (2147483648) with (2 ^ 31) in g.
      pose proof (Z.pow_le_mono_r 2 (unsigned y) 30).
      apply Z.ge_le in g.
      assert (0 < 2) by lia. apply H0 in H1. lia. assumption. lia.
      split. lia. rewrite two_power_nat_equiv.
      apply Z.pow_lt_mono_r; lia.

      pose proof (Zlt_neg_0 p).
      pose proof (Z.pow_nonneg 2 (unsigned y)). rewrite <- Heqz in H0.
      lia.
  Qed.

  Lemma is_power2_shl :
    forall y,
      unsigned y <= 30 ->
      is_power2 (shl one y) = Some y.
  Proof.
    intros.
    unfold is_power2, shl.
    destruct (Zbits.Z_is_power2 (unsigned (repr (Z.shiftl (unsigned one) (unsigned y))))) eqn:?.
    - simplify.
      rewrite Z_mod_modulus_eq in Heqo.
      rewrite Z.mod_small in Heqo. rewrite Z.shiftl_1_l in Heqo.
      rewrite <- two_p_correct in Heqo.
      rewrite Zbits.Z_is_power2_complete in Heqo. inv Heqo.
      rewrite repr_unsigned. auto.
      pose proof (unsigned_range_2 y). lia.
      rewrite Z.shiftl_1_l. unfold modulus, wordsize, Wordsize_32.wordsize.
      rewrite two_power_nat_equiv.
      split. apply Z.pow_nonneg. lia.
      apply Z.pow_lt_mono_r; lia.
    - simplify.
      rewrite Z_mod_modulus_eq in Heqo.
      rewrite Z.mod_small in Heqo. rewrite Z.shiftl_1_l in Heqo.
      rewrite <- two_p_correct in Heqo.
      rewrite Zbits.Z_is_power2_complete in Heqo. discriminate.
      pose proof (unsigned_range_2 y). lia.
      rewrite Z.shiftl_1_l. unfold modulus, wordsize, Wordsize_32.wordsize.
      rewrite two_power_nat_equiv.
      split. apply Z.pow_nonneg. lia.
      apply Z.pow_lt_mono_r; lia.
  Qed.

  Definition shrx_alt (x y : int) : int :=
    if zlt (signed x) 0
    then neg (shru (neg x) y)
    else shru x y.

  Lemma shrx_shrx_alt_equiv_ne :
    forall x y,
      unsigned x <> 2147483648 ->
      unsigned y <= 30 ->
      shrx x y = shrx_alt x y.
  Proof.
    intros x y Hhalf H.
    unfold shrx, shrx_alt, lt.
    destruct (Z_ge_lt_dec (signed x) 0);
      [rewrite zlt_false | rewrite zlt_true];

      repeat lazymatch goal with
             | |- is_power2 _ = Some _ => apply is_power2_shl
             | |- signed (shl one _) >= 0 => apply shl_signed_positive
             | |- signed (neg _) >= 0 => apply neg_signed
             | |- divs _ _ = divu _ _ => apply div_divs_equiv
             | |- divs ?x (shl one ?y) = neg (shru (neg ?x) ?y) =>
               rewrite <- neg_involutive at 1; rewrite neg_divs_distr_l;
                 try assumption; f_equal
             | |- divs ?x (shl one ?y) = shru ?x ?y =>
               let H := fresh "H" in
               pose proof (divu_pow2 x (shl one y) y) as H;
                 rewrite <- H
             end; try assumption.
  Qed.

  Lemma shrx_shrx_alt_equiv_eq :
    forall x y,
      unsigned x = 2147483648 ->
      unsigned y <= 30 ->
      shrx x y = shrx_alt x y.
  Proof.
    intros.
    repeat unfold shrx, shrx_alt, signed, divs, neg.
    replace half_modulus with 2147483648 by auto.
    replace modulus with 4294967296 by auto.
    simplify.
    rewrite !Z_mod_modulus_eq.
    rewrite !H.
    simplify.
    assert (Hshl: Z.shiftl 1 (unsigned y) mod 4294967296 = Z.shiftl 1 (unsigned y)).
    { apply Z.mod_small.
      rewrite Z.shiftl_1_l.
      split.
      apply Z.pow_nonneg. lia.
      replace 4294967296 with (2^32) by auto.
      apply Z.le_lt_trans with (m := 2 ^ 31); try lia.
      apply Z.pow_le_mono_r; lia.
    }
    rewrite !Hshl.
    f_equal.
    assert ((Z.shiftl 1 (unsigned y)) < 2147483648).
    rewrite Z.shiftl_1_l.
    replace 2147483648 with (2^31) by auto.
    apply Z.le_lt_trans with (m := 2 ^ 30); try lia.
    apply Z.pow_le_mono_r; lia.
    destruct (zlt (Z.shiftl 1 (unsigned y)) 2147483648); try lia.
    replace (-2147483648 mod 4294967296) with 2147483648 by auto.
    assert (Hmodeq : Z.shiftr 2147483648 (unsigned y) mod 4294967296
                     = Z.shiftr 2147483648 (unsigned y)).
    { apply Z.mod_small. split.
      apply Z.shiftr_nonneg. lia.
      rewrite Z.shiftr_div_pow2.
      replace 4294967296 with (Z.succ 4294967295); auto.
      apply Zle_lt_succ.
      replace 4294967295 with (4294967295 * (2 ^ unsigned y) / (2 ^ unsigned y)).
      2: {
          apply Z.div_mul.
          pose proof (Z.pow_pos_nonneg 2 (unsigned y)).
          apply not_eq_sym.
          apply Z.le_neq. apply H2; try lia.
          apply unsigned_range_2.
      }

      apply Z.div_le_mono.
      apply Z.pow_pos_nonneg. lia.
      apply unsigned_range_2.
      transitivity 4294967295; try lia.
      apply Z.le_mul_diag_r; try lia.
      replace 1 with (Z.succ 0) by auto.
      apply Z.le_succ_l.
      apply Z.pow_pos_nonneg; try lia.
      apply unsigned_range_2. apply unsigned_range_2.
    }
    rewrite !Hmodeq.
    replace (-2147483648) with (Z.opp 2147483648) by auto.
    rewrite Zquot.Zquot_opp_l.
    f_equal.
    rewrite Zquot.Zquot_Zdiv_pos.
    rewrite Z.shiftr_div_pow2.
    rewrite Z.shiftl_1_l. auto.
    apply unsigned_range_2.
    lia.
    rewrite Z.shiftl_1_l.
    apply Z.lt_le_incl.
    apply Z.pow_pos_nonneg; try lia.
    apply unsigned_range_2.
  Qed.

  Theorem shrx_shrx_alt_equiv :
    forall x y,
      unsigned y <= 30 ->
      shrx x y = shrx_alt x y.
  Proof.
    intros.
    destruct (Z.eq_dec (unsigned x) 2147483648);
    [ apply shrx_shrx_alt_equiv_eq | apply shrx_shrx_alt_equiv_ne]; auto.
  Qed.

End IntExtra.