diff options
author | jadep <jade.philipoom@gmail.com> | 2016-06-30 15:16:50 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-06-30 15:16:50 -0400 |
commit | e215871febb7d1294aa5aa13b0c70b2207e745e2 (patch) | |
tree | 618c2782b13fe99d07db7cfcf63db968052fe6fc | |
parent | a12c5e7bd5df69138bcb0c890594a0daacf0cc70 (diff) |
added and proved shift/or decode operation 'decode_bitwise'
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 209 | ||||
-rw-r--r-- | src/Testbit.v | 7 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 58 |
3 files changed, 227 insertions, 47 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 0bf1f8c34..544670f9b 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -316,6 +316,187 @@ Section PseudoMersenneProofs. apply FieldToZ_ZToField. Qed. + Lemma log_cap_nonneg : forall i, 0 <= log_cap i. + Proof. + unfold log_cap, nth_default; intros. + case_eq (nth_error limb_widths i); intros; try omega. + apply limb_widths_nonneg. + eapply nth_error_value_In; eauto. + Qed. Local Hint Resolve log_cap_nonneg. + + Definition carry_done us := forall i, (i < length base)%nat -> + 0 <= nth_default 0 us i /\ Z.shiftr (nth_default 0 us i) (log_cap i) = 0. + + Lemma carry_done_bounds : forall us, (length us = length base) -> + (carry_done us <-> forall i, 0 <= nth_default 0 us i < 2 ^ log_cap i). + Proof. + intros ? ?; unfold carry_done; split; [ intros Hcarry_done i | intros Hbounds i i_lt ]. + + destruct (lt_dec i (length base)) as [i_lt | i_nlt]. + - specialize (Hcarry_done i i_lt). + split; [ intuition | ]. + destruct Hcarry_done as [Hnth_nonneg Hshiftr_0]. + apply Z.shiftr_eq_0_iff in Hshiftr_0. + destruct Hshiftr_0 as [nth_0 | []]; [ rewrite nth_0; zero_bounds | ]. + apply Z.log2_lt_pow2; auto. + - rewrite nth_default_out_of_bounds by omega. + split; zero_bounds. + + specialize (Hbounds i). + split; [ intuition | ]. + destruct Hbounds as [nth_nonneg nth_lt_pow2]. + apply Z.shiftr_eq_0_iff. + apply Z.le_lteq in nth_nonneg; destruct nth_nonneg; try solve [left; auto]. + right; split; auto. + apply Z.log2_lt_pow2; auto. + Qed. + + Fixpoint decode_bitwise' us i acc := + match i with + | O => acc + | S i' => decode_bitwise' us i' (Z.lor (nth_default 0 us i') (Z.shiftl acc (log_cap i'))) + end. + + Definition decode_bitwise us := decode_bitwise' us (length us) 0. + + + (* TODO : move to ZUtil *) + Lemma Z_lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n -> + Z.lor a (Z.shiftl b n) = a + (Z.shiftl b n). + Proof. + intros. + apply Z.bits_inj'; intros t ?. + rewrite Z.lor_spec, Z.shiftl_spec by assumption. + destruct (Z_lt_dec t n). + + rewrite Z_testbit_add_shiftl_low by omega. + rewrite Z.testbit_neg_r with (n := t - n) by omega. + apply Bool.orb_false_r. + + rewrite Z_testbit_add_shiftl_high by omega. + replace (Z.testbit a t) with false; [ apply Bool.orb_false_l | ]. + symmetry. + apply Z.testbit_false; try omega. + rewrite Z.div_small; try reflexivity. + split; try eapply Z.lt_le_trans with (m := 2 ^ n); try omega. + apply Z.pow_le_mono_r; omega. + Qed. + + Lemma decode_bitwise'_succ : forall us i acc, carry_done us -> length us = length base -> + decode_bitwise' us (S i) acc = decode_bitwise' us i (acc * (2 ^ log_cap i) + nth_default 0 us i). + Proof. + intros. + simpl; f_equal. + rewrite Z_lor_shiftl by (auto; rewrite carry_done_bounds in H by assumption; + specialize (H i); assumption). + rewrite Z.shiftl_mul_pow2 by auto. + ring. + Qed. + + (* c is a counter, allows i to count up rather than down *) + Fixpoint partial_decode us i c := + match c with + | O => 0 + | S c' => (partial_decode us (S i) c' * 2 ^ log_cap i) + nth_default 0 us i + end. + + Lemma base_shift_log_cap : forall us, BaseSystem.decode' (skipn 1 base) us = + BaseSystem.decode' base us * 2 ^ log_cap 0. + Admitted. + + Lemma decode_cons_log_cap : forall us u0, + BaseSystem.decode' base (u0 :: us) = u0 + BaseSystem.decode' base us * 2 ^ log_cap 0. + Proof. + intros. + rewrite decode_cons by apply bv. + f_equal. + replace (0 :: us) with (BaseSystem.zeros 1%nat ++ us) by reflexivity. + rewrite decode'_splice, zeros_rep, length_zeros. + apply base_shift_log_cap. + Qed. + + Lemma partial_decode_counter_over : forall c us i, (c >= length us - i)%nat -> + partial_decode us i c = partial_decode us i (length us - i). + Proof. + induction c; intros. + + f_equal. omega. + + simpl. rewrite IHc by omega. + case_eq (length us - i)%nat; intros. + - rewrite nth_default_out_of_bounds by omega. + replace (length us - S i)%nat with 0%nat by omega. + reflexivity. + - simpl. repeat f_equal. omega. + Qed. + + Lemma partial_decode_counter_subst : forall c c' us i, + (c >= length us - i)%nat -> (c' >= length us - i)%nat -> + partial_decode us i c = partial_decode us i c'. + Proof. + intros. + rewrite partial_decode_counter_over by assumption. + symmetry. + auto using partial_decode_counter_over. + Qed. + + Lemma partial_decode_succ : forall c us i, (c >= length us - i)%nat -> + partial_decode us (S i) c * 2 ^ log_cap i + nth_default 0 us i = + partial_decode us i c. + Proof. + intros. + rewrite partial_decode_counter_subst with (i := i) (c' := S c) by omega. + reflexivity. + Qed. + + Lemma partial_decode_intermediate : forall c us i, length us = length base -> + (c >= length us - i)%nat -> + partial_decode us i c = BaseSystem.decode' (base_from_limb_widths (skipn i limb_widths)) (skipn i us). + Proof. + induction c; intros. + + simpl. rewrite skipn_all by (rewrite <-base_length; omega). + symmetry; apply decode_base_nil. + + simpl. + destruct (lt_dec i (length base)). + - rewrite IHc by omega. + do 2 (rewrite skipn_nth_default with (n := i) (d := 0) by (rewrite <-?base_length; omega)). + unfold base_from_limb_widths; fold base_from_limb_widths. + rewrite peel_decode. + fold (BaseSystem.mul_each (two_p (nth_default 0 limb_widths i))). + rewrite <-mul_each_base, mul_each_rep, two_p_correct. + ring_simplify. + f_equal; ring. + - rewrite <- IHc by omega. + apply partial_decode_succ; omega. + Qed. + + + Lemma decode_bitwise'_succ_partial_decode : forall us i c, + carry_done us -> length us = length base -> + decode_bitwise' us (S i) (partial_decode us (S i) c) = + decode_bitwise' us i (partial_decode us i (S c)). + Proof. + intros. + rewrite decode_bitwise'_succ by auto. + f_equal. + Qed. + + Lemma decode_bitwise'_spec : forall us i, (i <= length base)%nat -> + carry_done us -> length us = length base -> + decode_bitwise' us i (partial_decode us i (length us - i)) = + BaseSystem.decode base us. + Proof. + induction i; intros. + + rewrite partial_decode_intermediate by auto. + reflexivity. + + rewrite decode_bitwise'_succ_partial_decode by auto. + replace (S (length us - S i)) with (length us - i)%nat by omega. + apply IHi; auto; omega. + Qed. + + Lemma decode_bitwise_spec : forall us, carry_done us -> length us = length base -> + decode_bitwise us = BaseSystem.decode base us. + Proof. + unfold decode, decode_bitwise; intros. + replace 0 with (partial_decode us (length us) (length us - length us)) by + (rewrite Nat.sub_diag; reflexivity). + apply decode_bitwise'_spec; auto; omega. + Qed. + End PseudoMersenneProofs. Section CarryProofs. @@ -329,14 +510,6 @@ Section CarryProofs. Qed. Hint Resolve base_length_lt_pred. - Lemma log_cap_nonneg : forall i, 0 <= log_cap i. - Proof. - unfold log_cap, nth_default; intros. - case_eq (nth_error limb_widths i); intros; try omega. - apply limb_widths_nonneg. - eapply nth_error_value_In; eauto. - Qed. - Lemma nth_default_base_succ : forall i, (S i < length base)%nat -> nth_default 0 base (S i) = 2 ^ log_cap i * nth_default 0 base i. Proof. @@ -641,9 +814,6 @@ Section CanonicalizationProofs. Qed. Local Hint Resolve pre_carry_bounds_nonzero. - Definition carry_done us := forall i, (i < length base)%nat -> - 0 <= nth_default 0 us i /\ Z.shiftr (nth_default 0 us i) (log_cap i) = 0. - (* END defs *) (* BEGIN proofs about first carry loop *) @@ -734,23 +904,6 @@ Section CanonicalizationProofs. | subst; apply pow2_mod_log_cap_small; assumption ]). Qed. - Lemma carry_done_bounds : forall us, (length us = length base) -> - (carry_done us <-> forall i, 0 <= nth_default 0 us i < 2 ^ log_cap i). - Proof. - intros ? ?; unfold carry_done; split; [ intros Hcarry_done i | intros Hbounds i i_lt ]. - + destruct (lt_dec i (length base)) as [i_lt | i_nlt]. - - specialize (Hcarry_done i i_lt). - split; [ intuition | ]. - rewrite <- max_bound_log_cap. - apply Z.lt_succ_r. - apply shiftr_eq_0_max_bound; intuition. - - rewrite nth_default_out_of_bounds; try split; try omega; auto. - + specialize (Hbounds i). - split; intuition. - apply max_bound_shiftr_eq_0; auto. - rewrite <-max_bound_log_cap in *; omega. - Qed. - Lemma carry_carry_done_done : forall i us, (length us = length base)%nat -> (i < length base)%nat -> diff --git a/src/Testbit.v b/src/Testbit.v index 2bfcc3df6..545c3cbce 100644 --- a/src/Testbit.v +++ b/src/Testbit.v @@ -179,9 +179,10 @@ Proof. - rewrite nth_default_cons_S. erewrite IHus; eauto using no_overflow_tail. remember (i * limb_width)%nat as k. - rewrite Z_shiftr_add_land by omega. - replace (limb_width + k - limb_width)%nat with k by omega. - reflexivity. + rewrite Z_shiftr_add_shiftl_high; rewrite ?Nat2Z.inj_add; + repeat f_equal; try omega. + rewrite Z.land_ones by apply Nat2Z.is_nonneg. + apply Z.mod_pos_bound. zero_bounds. Qed. Lemma unfold_bits_testbit : forall limb_width us n, (0 < limb_width)%nat -> diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index a5716fca4..1ebadeada 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -181,17 +181,18 @@ Proof. omega. Qed. - -Lemma Z_testbit_shiftl : forall i, (0 <= i) -> forall a b n, (i < n) -> +Lemma Z_testbit_add_shiftl_low : forall i a b n, (0 <= i < n) -> Z.testbit (a + Z.shiftl b n) i = Z.testbit a i. Proof. intros. erewrite Z_testbit_low; eauto. rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega. rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega). - auto using Z.mod_pow2_bits_low. + apply Z.mod_pow2_bits_low. + omega. Qed. + Lemma Z_mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0. Proof. intros. @@ -199,21 +200,46 @@ Proof. auto using Z.mod_pos_bound. Qed. -Lemma Z_shiftr_add_land : forall n m a b, (n <= m)%nat -> - Z.shiftr ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.of_nat m) = Z.shiftr b (Z.of_nat (m - n)). +Lemma Z_shiftr_add_shiftl_high : forall n m a b, 0 <= n <= m -> 0 <= a < 2 ^ n -> + Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr b (m - n). Proof. intros. - rewrite Z.land_ones by apply Nat2Z.is_nonneg. - rewrite !Z.shiftr_div_pow2 by apply Nat2Z.is_nonneg. - rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg. - rewrite (le_plus_minus n m) at 1 by assumption. - rewrite Nat2Z.inj_add. - rewrite Z.pow_add_r by apply Nat2Z.is_nonneg. - rewrite <- Z.div_div by first - [ pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega - | apply Z.pow_pos_nonneg; omega ]. - rewrite Z.div_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega). - rewrite Z_mod_div_eq0 by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega); auto. + rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2 by omega. + replace (2 ^ m) with (2 ^ n * 2 ^ (m - n)) by + (rewrite <-Z.pow_add_r by omega; f_equal; ring). + rewrite <-Z.div_div, Z.div_add, (Z.div_small a) ; try solve + [assumption || apply Z.pow_nonzero || apply Z.pow_pos_nonneg; omega]. + f_equal; ring. +Qed. + +Lemma Z_shiftr_add_shiftl_low : forall n m a b, 0 <= m <= n -> 0 <= a < 2 ^ n -> + Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr a m + Z.shiftr b (m - n). +Proof. + intros. + rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2, Z.shiftr_mul_pow2 by omega. + replace (2 ^ n) with (2 ^ (n - m) * 2 ^ m) by + (rewrite <-Z.pow_add_r by omega; f_equal; ring). + rewrite Z.mul_assoc, Z.div_add by (apply Z.pow_nonzero; omega). + repeat f_equal; ring. +Qed. + +Lemma Z_testbit_add_shiftl_high : forall i, (0 <= i) -> forall a b n, (0 <= n <= i) -> + 0 <= a < 2 ^ n -> + Z.testbit (a + Z.shiftl b n) i = Z.testbit b (i - n). +Proof. + intros ? ?. + apply natlike_ind with (x := i); intros; try assumption; + (destruct (Z_eq_dec 0 n); [ subst; rewrite Z.pow_0_r in *; + replace a with 0 by omega; f_equal; ring | ]); try omega. + rewrite <-Z.add_1_r at 1. rewrite <-Z.shiftr_spec by assumption. + replace (Z.succ x - n) with (x - (n - 1)) by ring. + rewrite Z_shiftr_add_shiftl_low, <-Z.shiftl_opp_r with (a := b) by omega. + rewrite <-H1 with (a := Z.shiftr a 1); try omega; [ repeat f_equal; ring | ]. + rewrite Z.shiftr_div_pow2 by omega. + split; apply Z.div_pos || apply Z.div_lt_upper_bound; + try solve [rewrite ?Z.pow_1_r; omega]. + rewrite <-Z.pow_add_r by omega. + replace (1 + (n - 1)) with n by ring; omega. Qed. Lemma Z_land_add_land : forall n m a b, (m <= n)%nat -> |