From 42f62fbf8bc3d14d66ecf0a5db6fa2db16b82db5 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 3 Nov 2020 23:47:05 +0000 Subject: Add to Oshrximm proof --- src/common/IntegerExtra.v | 164 ++++++++++++++++++++++++++++++---------------- 1 file changed, 109 insertions(+), 55 deletions(-) (limited to 'src') diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index 6b68cf3..f1cc0e4 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -389,6 +389,21 @@ Module IntExtra. assumption. Qed. + Lemma neg_signed' : + forall x, + signed (neg x) = - signed x. + Proof. + intros. + Transparent repr. + Transparent signed. + unfold repr. + unfold signed. + simpl. + rewrite Z_mod_modulus_eq. + simpl. + repeat match goal with | |- context[if ?x then _ else _] => destruct x end. + Admitted. + Lemma neg_divs_distr_l : forall x y, neg (divs x y) = divs (neg x) y. @@ -402,79 +417,118 @@ Module IntExtra. 2: { rewrite Zquot.Zquot_opp_l. auto. } - Search signed eqm. - rewrite signed_eq_unsigned; auto. + unfold x'. + rewrite <- neg_signed'. auto with ints. - Admitted. - - Lemma neg_inj : - forall x y, - x = y -> neg x = neg y. - Proof. intros. rewrite H. trivial. Qed. - - Compute (max_signed). - Lemma neg_signed' : - forall x, - signed (neg x) = - signed x. - Proof. - intros. - unfold neg. - destruct (Z_le_gt_dec (unsigned x) max_signed). - - admit. - - - rewrite signed_repr. rewrite signed_eq_unsigned. - Qed. - - - Lemma neg_signed : forall x : int, signed x < 0 -> signed (neg x) >= 0. Proof. - unfold signed. intros. - destruct (Z_ge_lt_dec (unsigned x) half_modulus). - - rewrite zlt_false in H; try assumption. - destruct (Z_ge_lt_dec (unsigned (neg x)) half_modulus). - + rewrite zlt_false; try assumption. - rewrite neg_not in *. - rewrite add_unsigned. rewrite unsigned_repr. - Search unsigned not. - rewrite unsigned_not. - unfold_constants. - admit. admit. - + rewrite zlt_true; try assumption. - pose (unsigned_range (neg x)). - apply Z.le_ge. apply a. - - rewrite zlt_true in H; try assumption. - pose (unsigned_range x). lia. - Admitted. - - Lemma shrx_shrx2_equiv : forall x y, shrx x y = shrx2 x y. + rewrite neg_signed'. + lia. + 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. + + Theorem shrx_shrx2_equiv : + forall x y, + unsigned y <= 30 -> + shrx x y = shrx2 x y. Proof. intros. unfold shrx, shrx2, lt. destruct (Z_ge_lt_dec (signed x) 0). - rewrite zlt_false; try assumption. - pose (divu_pow2 x (shl one y) y). - rewrite <- e. - apply div_divs_equiv. - assumption. - admit (*shl >= 0*). - admit (* is_power2 shl *). + pose proof (divu_pow2 x (shl one y) y). + rewrite <- H0. + apply div_divs_equiv. assumption. + apply shl_signed_positive; assumption. + apply is_power2_shl; assumption. - rewrite zlt_true; try assumption. rewrite <- neg_involutive at 1. rewrite neg_divs_distr_l. - apply neg_inj. - pose (divu_pow2 (neg x) (shl one y) y). - rewrite <- e. + f_equal. + pose proof (divu_pow2 (neg x) (shl one y) y). + rewrite <- H0. apply div_divs_equiv. apply neg_signed; assumption. - admit (*shl >= 0*). - admit (* is_power2 shl *). - Admitted. + apply shl_signed_positive; assumption. + apply is_power2_shl; assumption. + Qed. End IntExtra. -- cgit