aboutsummaryrefslogtreecommitdiffstats
path: root/src/common/IntegerExtra.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/common/IntegerExtra.v')
-rw-r--r--src/common/IntegerExtra.v287
1 files changed, 287 insertions, 0 deletions
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index c9b5dbd..f44cac2 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -362,4 +362,291 @@ Module IntExtra.
rewrite testbit_repr; auto.
Abort.
+ 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 (pow2_nonneg (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 pow2_nonneg.
+ 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 pow2_nonneg.
+ 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 pow2_nonneg.
+ 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.
generated by cgit (git 2.34.1) at 2024-07-07 20:52:35 +0000