diff options
-rw-r--r-- | src/Experiments/Ed25519.v | 48 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 47 |
2 files changed, 47 insertions, 48 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 98cf5064d..1e3611399 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -461,25 +461,6 @@ Proof. intuition assumption. Qed. -(* MOVE : ZUtil *) -Lemma lor_shiftl_bounds : forall x y n m, - (0 <= n)%Z -> (0 <= m)%Z -> - (0 <= x < 2 ^ m)%Z -> - (0 <= y < 2 ^ n)%Z -> - (0 <= Z.lor y (Z.shiftl x n) < 2 ^ (n + m))%Z. -Proof. - intros. - apply ZUtil.Z.lor_range. - { split; try omega. - apply Z.lt_le_trans with (m := (2 ^ n)%Z); try omega. - apply Z.pow_le_mono_r; omega. } - { rewrite Z.shiftl_mul_pow2 by omega. - rewrite Z.pow_add_r by omega. - split; ZUtil.Z.zero_bounds. - rewrite Z.mul_comm. - apply Z.mul_lt_mono_pos_l; omega. } -Qed. - (* TODO : automate (after moving feEnc) or consider moving this and feSign_correct pre-specific *) Lemma feEnc_correct : forall x, PointEncoding.Fencode x = feEnc (GF25519BoundedCommon.encode x). @@ -1067,35 +1048,6 @@ Proof. split; simpl; omega. Qed. -(* TODO : move to ZUtil *) -Lemma pow2_mod_range : forall a n m, - (0 <= n)%Z -> - (n <= m)%Z -> - (0 <= ZUtil.Z.pow2_mod a n < 2 ^ m)%Z. -Proof. - intros; unfold ZUtil.Z.pow2_mod. - rewrite Z.land_ones; [|assumption]. - split; [apply Z.mod_pos_bound, ZUtil.Z.pow2_gt_0; assumption|]. - eapply Z.lt_le_trans; [apply Z.mod_pos_bound, ZUtil.Z.pow2_gt_0; assumption|]. - apply Z.pow_le_mono; [|assumption]. - split; simpl; omega. -Qed. - -(* TODO : move to ZUtil *) -Lemma shiftr_range : forall a n m, - (0 <= n)%Z -> - (0 <= m)%Z -> - (0 <= a < 2 ^ (n + m))%Z -> - (0 <= Z.shiftr a n < 2 ^ m)%Z. -Proof. - intros a n m H0 H1 H2; destruct H2. - split; [apply Z.shiftr_nonneg; assumption|]. - rewrite Z.shiftr_div_pow2; [|assumption]. - apply Z.div_lt_upper_bound; [apply ZUtil.Z.pow2_gt_0; assumption|]. - eapply Z.lt_le_trans; [eassumption|apply Z.eq_le_incl]. - apply Z.pow_add_r; omega. -Qed. - (* MOVE : same place as feDec *) (* TODO : automate *) Lemma feDec_correct : forall w : Word.word (pred b), option_eq GF25519BoundedCommon.eq diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 4c6e2441d..581ced889 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1035,6 +1035,24 @@ Module Z. Qed. Hint Resolve lor_range : zarith. + Lemma lor_shiftl_bounds : forall x y n m, + (0 <= n)%Z -> (0 <= m)%Z -> + (0 <= x < 2 ^ m)%Z -> + (0 <= y < 2 ^ n)%Z -> + (0 <= Z.lor y (Z.shiftl x n) < 2 ^ (n + m))%Z. + Proof. + intros. + apply Z.lor_range. + { split; try omega. + apply Z.lt_le_trans with (m := (2 ^ n)%Z); try omega. + apply Z.pow_le_mono_r; omega. } + { rewrite Z.shiftl_mul_pow2 by omega. + rewrite Z.pow_add_r by omega. + split; zero_bounds. + rewrite Z.mul_comm. + apply Z.mul_lt_mono_pos_l; omega. } + Qed. + Lemma N_le_1_l : forall p, (1 <= N.pos p)%N. Proof. destruct p; cbv; congruence. @@ -2253,6 +2271,34 @@ Module Z. | [|- (_ < _)%Z] => omega end. + Lemma pow2_mod_range : forall a n m, + (0 <= n) -> + (n <= m) -> + (0 <= Z.pow2_mod a n < 2 ^ m). + Proof. + intros; unfold Z.pow2_mod. + rewrite Z.land_ones; [|assumption]. + split; [apply Z.mod_pos_bound, pow2_gt_0; assumption|]. + eapply Z.lt_le_trans; [apply Z.mod_pos_bound, pow2_gt_0; assumption|]. + apply Z.pow_le_mono; [|assumption]. + split; simpl; omega. + Qed. + + Lemma shiftr_range : forall a n m, + (0 <= n)%Z -> + (0 <= m)%Z -> + (0 <= a < 2 ^ (n + m))%Z -> + (0 <= Z.shiftr a n < 2 ^ m)%Z. + Proof. + intros a n m H0 H1 H2; destruct H2. + split; [apply Z.shiftr_nonneg; assumption|]. + rewrite Z.shiftr_div_pow2; [|assumption]. + apply Z.div_lt_upper_bound; [apply pow2_gt_0; assumption|]. + eapply Z.lt_le_trans; [eassumption|apply Z.eq_le_incl]. + apply Z.pow_add_r; omega. + Qed. + + Lemma shiftr_le_mono: forall a b c d, (0 <= a)%Z -> (0 <= d)%Z @@ -3284,3 +3330,4 @@ Ltac Zmod_to_equiv_modulo := | [ |- context T[?x mod ?M = ?y mod ?M] ] => let T' := context T[Z.equiv_modulo M x y] in change T' end. + |