diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 115 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 466 | ||||
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 22 | ||||
| -rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 16 | ||||
| -rw-r--r-- | src/Testbit.v | 6 |
5 files changed, 216 insertions, 409 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 23b0c2ef6..dde021b4c 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -1,103 +1,58 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. Require Import Coq.Lists.List. -Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.BaseSystem. -Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.BaseSystemProofs. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. -Require Import Crypto.Tactics.VerdiTactics. -Require Import Crypto.Util.Notations. Require Import Crypto.ModularArithmetic.Pow2Base. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.ModularBaseSystemList. +Require Import Crypto.ModularArithmetic.ModularBaseSystemListProofs. +Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Notations. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope Z_scope. -Section PseudoMersenneBase. - Context `{prm :PseudoMersenneBaseParams} (modulus_multiple : digits). - Local Notation base := (base_from_limb_widths limb_widths). - - Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us). - - Definition rep (us : digits) (x : F modulus) := (length us = length base)%nat /\ decode us = x. - Local Notation "u ~= x" := (rep u x). - Local Hint Unfold rep. - - (* max must be greater than input; this is used to truncate last digit *) - Definition encode (x : F modulus) := encodeZ limb_widths x. - - (* Converts from length of extended base to length of base by reduction modulo M.*) - Definition reduce (us : digits) : digits := - let high := skipn (length base) us in - let low := firstn (length base) us in - let wrap := map (Z.mul c) high in - BaseSystem.add low wrap. - - Definition mul (us vs : digits) := reduce (BaseSystem.mul ext_base us vs). - - (* In order to subtract without underflowing, we add a multiple of the modulus first. *) - Definition sub (us vs : digits) := BaseSystem.sub (add modulus_multiple us) vs. - -End PseudoMersenneBase. - -Section CarryBasePow2. +Section ModularBaseSystem. Context `{prm :PseudoMersenneBaseParams}. Local Notation base := (base_from_limb_widths limb_widths). - Local Notation log_cap i := (nth_default 0 limb_widths i). + Local Notation digits := (tuple Z (length limb_widths)). + Local Arguments to_list {_ _} _. + Local Arguments from_list {_ _} _ _. + Local Arguments length_to_list {_ _ _}. + Local Notation "[[ u ]]" := (to_list u). - (* - Definition carry_and_reduce := - carry_gen limb_widths (fun ci => c * ci). - *) - Definition carry_and_reduce i := fun us => - let di := nth_default 0 us i in - let us' := set_nth i (Z.pow2_mod di (log_cap i)) us in - add_to_nth 0 (c * (Z.shiftr di (log_cap i))) us'. + Definition decode (us : digits) : F modulus := decode [[us]]. - Definition carry i : digits -> digits := - if eq_nat_dec i (pred (length base)) - then carry_and_reduce i - else carry_simple limb_widths i. + Definition encode (x : F modulus) : digits := from_list (encode x) length_encode. - Definition carry_sequence is us := fold_right carry us is. + Definition add (us vs : digits) : digits := from_list (add [[us]] [[vs]]) + (add_same_length _ _ _ length_to_list length_to_list). - Definition carry_full := carry_sequence (full_carry_chain limb_widths). + Definition mul (us vs : digits) : digits := from_list (mul [[us]] [[vs]]) + (length_mul length_to_list length_to_list). - Definition carry_mul us vs := carry_full (mul us vs). + Definition sub (modulus_multiple us vs : digits) : digits := + from_list (sub [[modulus_multiple]] [[us]] [[vs]]) + (length_sub length_to_list length_to_list length_to_list). -End CarryBasePow2. + Definition carry i (us : digits) : digits := from_list (carry i [[us]]) + (length_carry length_to_list). -Section Canonicalization. - Context `{prm :PseudoMersenneBaseParams}. - Local Notation base := (base_from_limb_widths limb_widths). - Local Notation log_cap i := (nth_default 0 limb_widths i). - - (* compute at compile time *) - Definition max_ones := Z.ones (fold_right Z.max 0 limb_widths). - - Definition max_bound i := Z.ones (log_cap i). - - Fixpoint isFull' us full i := - match i with - | O => andb (Z.ltb (max_bound 0 - c) (nth_default 0 us 0)) full - | S i' => isFull' us (andb (Z.eqb (max_bound i) (nth_default 0 us i)) full) i' - end. - - Definition isFull us := isFull' us true (length base - 1)%nat. + Definition rep (us : digits) (x : F modulus) := decode us = x. + Local Notation "u ~= x" := (rep u x). + Local Hint Unfold rep. - Fixpoint modulus_digits' i := - match i with - | O => max_bound i - c + 1 :: nil - | S i' => modulus_digits' i' ++ max_bound i :: nil - end. + Definition carry_sequence is (us : digits) : digits := fold_right carry us is. - (* compute at compile time *) - Definition modulus_digits := modulus_digits' (length base - 1). + Definition carry_full : digits -> digits := carry_sequence (full_carry_chain limb_widths). - Definition and_term us := if isFull us then max_ones else 0. + Definition carry_mul (us vs : digits) : digits := carry_full (mul us vs). - Definition freeze us := + Definition freeze (us : digits) : digits := let us' := carry_full (carry_full (carry_full us)) in - let and_term := and_term us' in - (* [and_term] is all ones if us' is full, so the subtractions subtract q overall. - Otherwise, it's all zeroes, and the subtractions do nothing. *) - map2 (fun x y => x - y) us' (map (Z.land and_term) modulus_digits). + from_list (conditional_subtract_modulus [[us]] (ge_modulus [[us]])) + (length_conditional_subtract_modulus length_to_list). -End Canonicalization. +End ModularBaseSystem.
\ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 5d1becc00..7d4f0107c 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -1,15 +1,20 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Coq.Lists.List. -Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil Crypto.Util.NatUtil. Require Import Crypto.Tactics.VerdiTactics. -Require Crypto.BaseSystem. -Require Import Crypto.ModularArithmetic.ModularBaseSystem Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.BaseSystemProofs Crypto.ModularArithmetic.Pow2Base. +Require Import Crypto.BaseSystem. +Require Import Crypto.BaseSystemProofs. +Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.ModularArithmetic.Pow2Base. Require Import Crypto.ModularArithmetic.Pow2BaseProofs. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. -Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.ModularArithmetic.ModularBaseSystemList. +Require Import Crypto.ModularArithmetic.ModularBaseSystemListProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil Crypto.Util.NatUtil. +Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. Local Open Scope Z_scope. @@ -19,29 +24,26 @@ Local Opaque add_to_nth carry_simple. Section PseudoMersenneProofs. Context `{prm :PseudoMersenneBaseParams}. + Local Arguments to_list {_ _} _. + Local Arguments from_list {_ _} _ _. + Local Hint Unfold decode. Local Notation "u ~= x" := (rep u x). - Local Notation "u .+ x" := (add u x). - Local Notation "u .* x" := (ModularBaseSystem.mul u x). - Local Hint Unfold rep. + Local Notation digits := (tuple Z (length limb_widths)). Local Hint Resolve (@limb_widths_nonneg _ prm) sum_firstn_limb_widths_nonneg. Local Hint Resolve log_cap_nonneg. Local Notation base := (base_from_limb_widths limb_widths). Local Notation log_cap i := (nth_default 0 limb_widths i). - Lemma rep_decode : forall us x, us ~= x -> decode us = x. - Proof. - autounfold; intuition. - Qed. + Local Hint Unfold rep decode ModularBaseSystemList.decode. - Lemma rep_length : forall us x, us ~= x -> length us = length base. + Lemma rep_decode : forall us x, us ~= x -> decode us = x. Proof. autounfold; intuition. Qed. - Lemma decode_rep : forall us, length us = length base -> - rep us (decode us). + Lemma decode_rep : forall us, rep us (decode us). Proof. cbv [rep]; auto. Qed. @@ -57,75 +59,32 @@ Section PseudoMersenneProofs. pose proof (NumTheoryUtil.lt_1_p _ prime_modulus); omega. Qed. Hint Resolve modulus_pos. - Lemma encode'_eq : forall (x : F modulus) i, (i <= length limb_widths)%nat -> - encode' limb_widths x i = BaseSystem.encode' base x (2 ^ k) i. + Lemma encode_eq : forall x : F modulus, + ModularBaseSystemList.encode x = BaseSystem.encode base x (2 ^ k). Proof. - rewrite <-base_length; induction i; intros. - + rewrite encode'_zero. reflexivity. - + rewrite encode'_succ, <-IHi by omega. - simpl; do 2 f_equal. - rewrite Z.land_ones, Z.shiftr_div_pow2 by eauto. - match goal with H : (S _ <= length base)%nat |- _ => - apply le_lt_or_eq in H; destruct H end. - - repeat f_equal; rewrite nth_default_base by (eauto || omega); reflexivity. - - repeat f_equal; try solve [rewrite nth_default_base by (eauto || omega); reflexivity]. - rewrite nth_default_out_of_bounds by omega. - unfold k. - rewrite <-base_length; congruence. + cbv [ModularBaseSystemList.encode BaseSystem.encode encodeZ]; intros. + rewrite base_length. + apply encode'_spec; auto using Nat.eq_le_incl, base_length. Qed. - Lemma encode_eq : forall x : F modulus, - encode x = BaseSystem.encode base x (2 ^ k). + Lemma encode_rep : forall x : F modulus, encode x ~= x. Proof. - unfold encode, BaseSystem.encode; intros. - rewrite base_length; apply encode'_eq; omega. + autounfold; cbv [encode]; intros. + rewrite to_list_from_list; autounfold. + rewrite encode_eq, encode_rep. + + apply ZToField_FieldToZ. + + apply bv. + + split; [ | etransitivity]; try (apply FieldToZ_range; auto using modulus_pos); auto. + + eauto using base_upper_bound_compatible, limb_widths_nonneg. Qed. - Lemma encode_rep : forall x : F modulus, encode x ~= x. + Lemma add_rep : forall u v x y, u ~= x -> v ~= y -> + add u v ~= (x+y)%F. Proof. - intros. - rewrite encode_eq. - unfold encode, rep. - split. { - unfold BaseSystem.encode. - auto using encode'_length. - } { - unfold decode. - rewrite encode_rep. - + apply ZToField_FieldToZ. - + apply bv. - + split; [ | etransitivity]; try (apply FieldToZ_range; auto using modulus_pos); auto. - + unfold base_max_succ_divide; intros. - match goal with H : (_ <= length base)%nat |- _ => - apply le_lt_or_eq in H; destruct H end. - - apply Z.mod_divide. - * apply nth_default_base_nonzero; auto using bv, two_k_nonzero. - * rewrite !nth_default_eq. - do 2 (erewrite nth_indep with (d := 2 ^ k) (d' := 0) by omega). - rewrite <-!nth_default_eq. - apply base_succ; eauto; omega. - - rewrite nth_default_out_of_bounds with (n := S i) by omega. - rewrite nth_default_base by (omega || eauto). - unfold k. - match goal with H : S _ = length base |- _ => - rewrite base_length in H; rewrite <-H end. - erewrite sum_firstn_succ by (apply nth_error_Some_nth_default with (x0 := 0); omega). - rewrite Z.pow_add_r by (eauto using sum_firstn_limb_widths_nonneg; - apply limb_widths_nonneg; rewrite nth_default_eq; apply nth_In; omega). - apply Z.divide_factor_r. - } - Qed. - - Lemma add_rep : forall u v x y, u ~= x -> v ~= y -> BaseSystem.add u v ~= (x+y)%F. - Proof. - autounfold; intuition. { - unfold add. - auto using add_same_length. - } - unfold decode in *; unfold decode in *. - rewrite add_rep. - rewrite ZToField_add. - subst; auto. + autounfold; cbv [add]; intros. + rewrite to_list_from_list; autounfold. + rewrite add_rep, ZToField_add. + f_equal; assumption. Qed. Lemma firstn_us_base_ext_base : forall (us : BaseSystem.digits), @@ -162,13 +121,11 @@ Section PseudoMersenneProofs. Proof. intros. replace (2^k) with ((2^k - c) + c) by ring. - rewrite Z.mul_add_distr_r. - rewrite Zplus_mod. + rewrite Z.mul_add_distr_r, Zplus_mod. unfold c. rewrite Z.sub_sub_distr, Z.sub_diag. simpl. - rewrite Z.mul_comm. - rewrite Z.mod_add_l; auto using modulus_nonzero. + rewrite Z.mul_comm, Z.mod_add_l; auto using modulus_nonzero. rewrite <- Zplus_mod; auto. Qed. @@ -194,52 +151,24 @@ Section PseudoMersenneProofs. BaseSystem.decode base (reduce us) mod modulus = BaseSystem.decode ext_base us mod modulus. Proof. - intros. - rewrite extended_shiftadd. - rewrite pseudomersenne_add. - unfold reduce. - remember (firstn (length base) us) as low. - remember (skipn (length base) us) as high. - unfold BaseSystem.decode. - rewrite BaseSystemProofs.add_rep. - replace (map (Z.mul c) high) with (BaseSystem.mul_each c high) by auto. + cbv [reduce]; intros. + rewrite extended_shiftadd, base_length, pseudomersenne_add, BaseSystemProofs.add_rep. + change (map (Z.mul c)) with (BaseSystem.mul_each c). rewrite mul_each_rep; auto. Qed. - Lemma reduce_length : forall us, - (length base <= length us <= length ext_base)%nat -> - (length (reduce us) = length base)%nat. - Proof. - rewrite extended_base_length. - unfold reduce; intros. - rewrite add_length_exact. - rewrite map_length, firstn_length, skipn_length. - rewrite Min.min_l by omega. - apply Max.max_l; omega. - Qed. - - Lemma length_mul : forall u v, - length u = length base - -> length v = length base - -> length (u .* v) = length base. + Lemma mul_rep : forall u v x y, u ~= x -> v ~= y -> mul u v ~= (x*y)%F. Proof. - autounfold in *; unfold ModularBaseSystem.mul in *; intuition eauto. - apply reduce_length. - rewrite mul_length_exact, extended_base_length; try omega. - destruct u; try congruence. - rewrite @nil_length0 in *. - pose proof base_length_nonzero; omega. - Qed. - - Lemma mul_rep : forall u v x y, u ~= x -> v ~= y -> u .* v ~= (x*y)%F. - Proof. - split; autounfold in *; unfold ModularBaseSystem.mul in *. - { apply length_mul; intuition auto. } - { intuition idtac; subst. - rewrite ZToField_mod, reduce_rep, <-ZToField_mod. - rewrite mul_rep by (apply ExtBaseVector || rewrite extended_base_length; omega). - rewrite 2decode_short by omega. - apply ZToField_mul. } + autounfold; cbv [mul]; intros. + rewrite to_list_from_list; autounfold. + cbv [ModularBaseSystemList.mul]. + rewrite ZToField_mod, reduce_rep. + rewrite mul_rep, <-ZToField_mod, ZToField_mul. + rewrite <-!decode_short; rewrite ?base_length; + auto using Nat.eq_le_incl, length_to_list. + + f_equal; assumption. + + apply ExtBaseVector. + + rewrite extended_base_length, base_length, !length_to_list. omega. Qed. Lemma nth_default_base_positive : forall i, (i < length base)%nat -> @@ -263,11 +192,11 @@ Section PseudoMersenneProofs. apply base_succ; eauto. Qed. - Lemma Fdecode_decode_mod : forall us x, (length us = length base) -> - decode us = x -> BaseSystem.decode base us mod modulus = x. + Lemma Fdecode_decode_mod : forall us x, + decode us = x -> BaseSystem.decode base (to_list us) mod modulus = x. Proof. - unfold decode; intros ? ? ? decode_us. - rewrite <-decode_us. + autounfold; intros. + rewrite <-H. apply FieldToZ_ZToField. Qed. @@ -296,31 +225,23 @@ Section PseudoMersenneProofs. apply Z.log2_lt_pow2; auto. Qed. - Context mm (mm_length : length mm = length base) (mm_spec : decode mm = 0%F). - - Lemma length_sub : forall u v, - length u = length base - -> length v = length base - -> length (ModularBaseSystem.sub mm u v) = length base. - Proof. - autounfold; unfold ModularBaseSystem.sub; intuition idtac. - rewrite sub_length, add_length_exact. - case_max; try rewrite Max.max_r; omega. - Qed. + Context (mm : digits) (mm_spec : decode mm = 0%F). Lemma sub_rep : forall u v x y, u ~= x -> v ~= y -> ModularBaseSystem.sub mm u v ~= (x-y)%F. Proof. - split; autounfold in *. - { apply length_sub; intuition (auto; omega). } - { unfold decode, ModularBaseSystem.sub, BaseSystem.decode in *; intuition idtac. - rewrite BaseSystemProofs.sub_rep, BaseSystemProofs.add_rep. - rewrite ZToField_sub, ZToField_add. - match goal with H : _ = 0%F |- _ => rewrite H end. - rewrite F_add_0_l. congruence. } + autounfold; cbv [sub]; intros. + rewrite to_list_from_list; autounfold. + cbv [ModularBaseSystemList.sub]. + rewrite BaseSystemProofs.sub_rep, BaseSystemProofs.add_rep. + rewrite ZToField_sub, ZToField_add, ZToField_mod. + apply Fdecode_decode_mod in mm_spec; cbv [BaseSystem.decode] in *. + rewrite mm_spec, F_add_0_l. + f_equal; assumption. Qed. End PseudoMersenneProofs. +Opaque encode add mul sub. Section CarryProofs. Context `{prm : PseudoMersenneBaseParams}. @@ -336,111 +257,69 @@ Section CarryProofs. Hint Resolve base_length_lt_pred. Lemma carry_decode_eq_reduce : forall us, - (length us = length base) -> + (length us = length limb_widths) -> BaseSystem.decode base (carry_and_reduce (pred (length base)) us) mod modulus = BaseSystem.decode base us mod modulus. Proof. unfold carry_and_reduce; intros ? length_eq. pose proof base_length_nonzero. - rewrite add_to_nth_sum by (rewrite length_set_nth; omega). - rewrite set_nth_sum by omega. + rewrite add_to_nth_sum by (rewrite length_set_nth, base_length; omega). + rewrite set_nth_sum by (rewrite base_length; omega). rewrite Zplus_comm, <- Z.mul_assoc, <- pseudomersenne_add, BaseSystem.b0_1. rewrite (Z.mul_comm (2 ^ k)), <- Zred_factor0. f_equal. rewrite <- (Z.add_comm (BaseSystem.decode base us)), <- Z.add_assoc, <- Z.add_0_r. f_equal. destruct (NPeano.Nat.eq_dec (length base) 0) as [length_zero | length_nonzero]. - + apply length0_nil in length_zero. - pose proof (base_length) as limbs_length. - rewrite length_zero in length_eq, limbs_length. - apply length0_nil in length_eq. - symmetry in limbs_length. - apply length0_nil in limbs_length. - subst; rewrite length_zero, limbs_length, nth_default_nil. - reflexivity. + + pose proof (base_length) as limbs_length. + destruct us; rewrite ?(@nil_length0 Z), ?(@length_cons Z) in *; + pose proof base_length_nonzero; omega. + rewrite nth_default_base by (omega || eauto). rewrite <- Z.add_opp_l, <- Z.opp_sub_distr. unfold Z.pow2_mod. rewrite Z.land_ones by eauto using log_cap_nonneg. rewrite <- Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.pow_pos_nonneg; omega || eauto using log_cap_nonneg). rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg. - rewrite Zopp_mult_distr_r. - rewrite Z.mul_comm. - rewrite Z.mul_assoc. - rewrite <- Z.pow_add_r by eauto using log_cap_nonneg. unfold k. replace (length limb_widths) with (S (pred (length base))) by (subst; rewrite <- base_length; apply NPeano.Nat.succ_pred; omega). rewrite sum_firstn_succ with (x:= log_cap (pred (length base))) by (apply nth_error_Some_nth_default; rewrite <- base_length; omega). - rewrite <- Zopp_mult_distr_r. - rewrite Z.mul_comm. - rewrite (Z.add_comm (log_cap (pred (length base)))). + rewrite Z.pow_add_r by eauto using log_cap_nonneg. ring. Qed. - Lemma length_carry_and_reduce : forall i us, length (carry_and_reduce i us) = length us. - Proof. intros; unfold carry_and_reduce; autorewrite with distr_length; reflexivity. Qed. - Hint Rewrite @length_carry_and_reduce : distr_length. - - Lemma length_carry : forall i us, length (carry i us) = length us. - Proof. intros; unfold carry; break_if; autorewrite with distr_length; reflexivity. Qed. - Hint Rewrite @length_carry : distr_length. - - Local Hint Extern 1 (length _ = _) => progress autorewrite with distr_length. - Lemma carry_rep : forall i us x, - (length us = length base) -> (i < length base)%nat -> us ~= x -> carry i us ~= x. Proof. - pose proof length_carry. pose proof carry_decode_eq_reduce. pose proof (@carry_simple_decode_eq limb_widths). + cbv [carry rep decode]; intros. + rewrite to_list_from_list. + pose proof carry_decode_eq_reduce. pose proof (@carry_simple_decode_eq limb_widths). + specialize_by eauto. - intros; split; auto. - unfold rep, decode, carry in *. - intuition; break_if; subst; eauto; apply F_eq; simpl; intuition. + cbv [ModularBaseSystemList.carry]. + break_if; subst; eauto. + apply F_eq; apply carry_decode_eq_reduce; apply length_to_list. + cbv [ModularBaseSystemList.decode]. + f_equal. + apply carry_simple_decode_eq; try omega; rewrite ?base_length; auto using length_to_list. Qed. Hint Resolve carry_rep. - Lemma length_carry_sequence: forall is us, - (length (carry_sequence is us) = length us)%nat. - Proof. - induction is; boring. - Qed. - Hint Rewrite length_carry_sequence : distr_length. - - Lemma carry_sequence_length: forall is us, - (length us = length base)%nat -> - (length (carry_sequence is us) = length base)%nat. - Proof. intros; autorewrite with distr_length; congruence. Qed. - Hint Resolve carry_sequence_length. - Lemma carry_sequence_rep : forall is us x, (forall i, In i is -> (i < length base)%nat) -> - (length us = length base) -> us ~= x -> carry_sequence is us ~= x. Proof. induction is; boring. Qed. - Lemma length_carry_full : forall us, - length (carry_full us) = length us. - Proof. - intros; cbv [carry_full]; auto using carry_sequence_length. - Qed. - Hint Rewrite length_carry_full : distr_length. - - Lemma carry_full_length : forall us, (length us = length base)%nat -> - length (carry_full us) = length base. - Proof. intros; autorewrite with distr_length; congruence. Qed. - Lemma carry_full_preserves_rep : forall us x, rep us x -> rep (carry_full us) x. Proof. unfold carry_full; intros. apply carry_sequence_rep; auto. unfold full_carry_chain; rewrite base_length; apply make_chain_lt. - eauto using rep_length. Qed. Opaque carry_full. @@ -452,36 +331,9 @@ Section CarryProofs. auto using mul_rep. Qed. - Local Arguments minus !_ !_. - - Lemma length_carry_mul : forall us vs, - length (carry_mul us vs) = (if eq_nat_dec (length us) 0 - then 0 - else if le_dec (length base) (pred (length us + length vs)) - then if lt_dec (length base + length base) (pred (length us + length vs)) - then pred (length us + length vs) - length base - else length base - else pred (length us + length vs))%nat. - Proof. - unfold carry_mul, ModularBaseSystem.mul, reduce; intros; autorewrite with distr_length natsimplify. - destruct us; simpl; autorewrite with natsimplify. - { reflexivity. } - { repeat break_if; omega *. } - Qed. - - Lemma carry_mul_length : forall us vs, - length us = length base -> length vs = length base -> - length (carry_mul us vs) = length base. - Proof. - intros; rewrite length_carry_mul. - rewrite_hyp !* in *. - edestruct eq_nat_dec; [ congruence | ]. - autorewrite with natsimplify; reflexivity. - Qed. - End CarryProofs. -Hint Rewrite @length_carry_and_reduce @length_carry @length_carry_sequence @length_carry_full @length_carry_mul : distr_length. +Hint Rewrite @length_carry_and_reduce @length_carry : distr_length. Section CanonicalizationProofs. Context `{prm : PseudoMersenneBaseParams}. @@ -490,13 +342,13 @@ Section CanonicalizationProofs. Context (lt_1_length_base : (1 < length base)%nat) {B} (B_pos : 0 < B) (B_compat : forall w, In w limb_widths -> w <= B) (* on the first reduce step, we add at most one bit of width to the first digit *) - (c_reduce1 : c * (Z.ones (B - log_cap (pred (length base)))) < max_bound 0 + 1) + (c_reduce1 : c * (Z.ones (B - log_cap (pred (length base)))) < 2 ^ log_cap 0) (* on the second reduce step, we add at most one bit of width to the first digit, and leave room to carry c one more time after the highest bit is carried *) - (c_reduce2 : c <= max_bound 0 - c) + (c_reduce2 : c <= nth_default 0 modulus_digits 0) (* this condition is probably implied by c_reduce2, but is more straighforward to compute than to prove *) (two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus). - +(* (* BEGIN groundwork proofs *) Local Hint Resolve (@log_cap_nonneg limb_widths) limb_widths_nonneg. @@ -506,20 +358,20 @@ Section CanonicalizationProofs. Qed. Local Hint Resolve pow_2_log_cap_pos. - Lemma max_bound_log_cap : forall i, Z.succ (max_bound i) = 2 ^ log_cap i. + Lemma max_value_log_cap : forall i, Z.succ (max_value i) = 2 ^ log_cap i. Proof. intros. - unfold max_bound, Z.ones. + unfold max_value, Z.ones. rewrite Z.shiftl_1_l. omega. Qed. - Lemma pow2_mod_log_cap_range : forall a i, 0 <= Z.pow2_mod a (log_cap i) <= max_bound i. + Lemma pow2_mod_log_cap_range : forall a i, 0 <= Z.pow2_mod a (log_cap i) <= max_value i. Proof. intros. unfold Z.pow2_mod. rewrite Z.land_ones by eauto using log_cap_nonneg. - unfold max_bound, Z.ones. + unfold max_value, Z.ones. rewrite Z.shiftl_1_l, <-Z.lt_le_pred. apply Z_mod_lt. pose proof (pow_2_log_cap_pos i). @@ -532,13 +384,13 @@ Section CanonicalizationProofs. pose proof (pow2_mod_log_cap_range a i); omega. Qed. - Lemma pow2_mod_log_cap_bounds_upper : forall a i, Z.pow2_mod a (log_cap i) <= max_bound i. + Lemma pow2_mod_log_cap_bounds_upper : forall a i, Z.pow2_mod a (log_cap i) <= max_value i. Proof. intros. pose proof (pow2_mod_log_cap_range a i); omega. Qed. - Lemma pow2_mod_log_cap_small : forall a i, 0 <= a <= max_bound i -> + Lemma pow2_mod_log_cap_small : forall a i, 0 <= a <= max_value i -> Z.pow2_mod a (log_cap i) = a. Proof. intros. @@ -546,35 +398,35 @@ Section CanonicalizationProofs. rewrite Z.land_ones by eauto using log_cap_nonneg. apply Z.mod_small. split; try omega. - rewrite <- max_bound_log_cap. + rewrite <- max_value_log_cap. omega. Qed. - Lemma max_bound_pos : forall i, (i < length base)%nat -> 0 < max_bound i. + Lemma max_value_pos : forall i, (i < length base)%nat -> 0 < max_value i. Proof. - unfold max_bound; intros; apply Z.ones_pos_pos. + unfold max_value; intros; apply Z.ones_pos_pos. apply limb_widths_pos. rewrite nth_default_eq. apply nth_In. rewrite <-base_length; assumption. Qed. - Local Hint Resolve max_bound_pos. + Local Hint Resolve max_value_pos. - Lemma max_bound_nonneg : forall i, 0 <= max_bound i. + Lemma max_value_nonneg : forall i, 0 <= max_value i. Proof. - unfold max_bound; intros; eauto using Z.ones_nonneg. + unfold max_value; intros; eauto using Z.ones_nonneg. Qed. - Local Hint Resolve max_bound_nonneg. + Local Hint Resolve max_value_nonneg. - Lemma shiftr_eq_0_max_bound : forall i a, Z.shiftr a (log_cap i) = 0 -> - a <= max_bound i. + Lemma shiftr_eq_0_max_value : forall i a, Z.shiftr a (log_cap i) = 0 -> + a <= max_value i. Proof. intros ? ? shiftr_0. apply Z.shiftr_eq_0_iff in shiftr_0. - intuition; subst; try apply max_bound_nonneg. + intuition; subst; try apply max_value_nonneg. match goal with H : Z.log2 _ < log_cap _ |- _ => apply Z.log2_lt_pow2 in H; - replace (2 ^ log_cap i) with (Z.succ (max_bound i)) in H by - (unfold max_bound, Z.ones; rewrite Z.shiftl_1_l; omega) + replace (2 ^ log_cap i) with (Z.succ (max_value i)) in H by + (unfold max_value, Z.ones; rewrite Z.shiftl_1_l; omega) end; auto. omega. Qed. @@ -593,16 +445,16 @@ Section CanonicalizationProofs. Qed. Local Hint Resolve B_compat_log_cap. - Lemma max_bound_shiftr_eq_0 : forall i a, 0 <= a -> a <= max_bound i -> + Lemma max_value_shiftr_eq_0 : forall i a, 0 <= a -> a <= max_value i -> Z.shiftr a (log_cap i) = 0. Proof. - intros ? ? ? le_max_bound. + intros ? ? ? le_max_value. apply Z.shiftr_eq_0_iff. destruct (Z_eq_dec a 0); auto. right. split; try omega. apply Z.log2_lt_pow2; try omega. - rewrite <-max_bound_log_cap. + rewrite <-max_value_log_cap. omega. Qed. @@ -612,7 +464,7 @@ Section CanonicalizationProofs. Qed. (* END groundwork proofs *) - Opaque Z.pow2_mod max_bound. + Opaque Z.pow2_mod max_value. (* automation *) Ltac carry_length_conditions' := unfold carry_full; @@ -644,7 +496,7 @@ Section CanonicalizationProofs. (* BEGIN proofs about first carry loop *) Lemma nth_default_carry_bound_upper : forall i us, (length us = length base) -> - nth_default 0 (carry i us) i <= max_bound i. + nth_default 0 (carry i us) i <= max_value i. Proof. unfold carry; intros. break_if. @@ -711,7 +563,7 @@ Section CanonicalizationProofs. Lemma carry_nothing : forall i j us, (i < length base)%nat -> (length us = length base)%nat -> - 0 <= nth_default 0 us j <= max_bound j -> + 0 <= nth_default 0 us j <= max_value j -> nth_default 0 (carry j us) i = nth_default 0 us i. Proof. unfold carry, carry_and_reduce; intros. @@ -734,13 +586,13 @@ Section CanonicalizationProofs. split. + rewrite carry_nothing; auto. split; [ apply Hcarry_done; auto | ]. - apply shiftr_eq_0_max_bound. + apply shiftr_eq_0_max_value. apply Hcarry_done; auto. + unfold carry, carry_and_reduce; break_if; subst. - add_set_nth; subst. * rewrite shiftr_0_i, Z.mul_0_r, Z.add_0_l. assumption. - * rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_bound). + * rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_value). assumption. - repeat (carry_length_conditions || (autorewrite with push_nth_default natsimplify core zsimplify) @@ -757,7 +609,7 @@ Section CanonicalizationProofs. Lemma carry_bounds_0_upper : forall us j, (length us = length base) -> (0 < j < length base)%nat -> - nth_default 0 (carry_sequence (make_chain j) us) 0 <= max_bound 0. + nth_default 0 (carry_sequence (make_chain j) us) 0 <= max_value 0. Proof. induction j as [ | [ | j ] IHj ]; [simpl; intros; omega | | ]; intros. + subst; simpl; auto. @@ -765,7 +617,7 @@ Section CanonicalizationProofs. Qed. Lemma carry_bounds_upper : forall i us j, (0 < i < j)%nat -> (length us = length base) -> - nth_default 0 (carry_sequence (make_chain j) us) i <= max_bound i. + nth_default 0 (carry_sequence (make_chain j) us) i <= max_value i. Proof. unfold carry_sequence; induction j; [simpl; intros; omega | ]. @@ -844,7 +696,7 @@ Section CanonicalizationProofs. Lemma carry_full_bounds : forall us i, (i <> 0)%nat -> (forall i, 0 <= nth_default 0 us i) -> (length us = length base)%nat -> - 0 <= nth_default 0 (carry_full us) i <= max_bound i. + 0 <= nth_default 0 (carry_full us) i <= max_value i. Proof. unfold carry_full, full_carry_chain; intros. split; (destruct (lt_dec i (length limb_widths)); @@ -899,7 +751,7 @@ Section CanonicalizationProofs. Lemma carry_full_bounds_0 : forall us, pre_carry_bounds us -> (length us = length base)%nat -> - 0 <= nth_default 0 (carry_full us) 0 <= max_bound 0 + c * (Z.ones (B - log_cap (pred (length base)))). + 0 <= nth_default 0 (carry_full us) 0 <= max_value 0 + c * (Z.ones (B - log_cap (pred (length base)))). Proof. unfold carry_full, full_carry_chain; intros. rewrite <- base_length. @@ -949,7 +801,7 @@ Section CanonicalizationProofs. - apply IHi; auto; omega. - rewrite carry_sequence_unaffected by carry_length_conditions. apply carry_full_bounds; auto; omega. - + rewrite <-max_bound_log_cap, <-Z.add_1_l. + + rewrite <-max_value_log_cap, <-Z.add_1_l. apply Z.add_le_mono. - rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg. apply Z.div_floor; auto. @@ -957,7 +809,7 @@ Section CanonicalizationProofs. * simpl. eapply Z.le_lt_trans; [ apply carry_full_bounds_0; auto | ]. replace (2 ^ log_cap 0 * 2) with (2 ^ log_cap 0 + 2 ^ log_cap 0) by ring. - rewrite <-max_bound_log_cap, <-Z.add_1_l. + rewrite <-max_value_log_cap, <-Z.add_1_l. apply Z.add_lt_le_mono; omega. * eapply Z.le_lt_trans; [ apply IHi; auto; omega | ]. apply Z.lt_mul_diag_r; auto; omega. @@ -967,7 +819,7 @@ Section CanonicalizationProofs. Lemma carry_full_2_bounds_0 : forall us, pre_carry_bounds us -> (length us = length base)%nat -> (1 < length base)%nat -> - 0 <= nth_default 0 (carry_full (carry_full us)) 0 <= max_bound 0 + c. + 0 <= nth_default 0 (carry_full (carry_full us)) 0 <= max_value 0 + c. Proof. intros. unfold carry_full at 1 3, full_carry_chain. @@ -1009,7 +861,7 @@ Section CanonicalizationProofs. rewrite carry_sequence_unaffected by carry_length_conditions. apply carry_full_bounds; carry_length_conditions. carry_seq_lower_bound. - + rewrite <-max_bound_log_cap, <-Z.add_1_l. + + rewrite <-max_value_log_cap, <-Z.add_1_l. rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg. apply Z.add_le_mono. - apply Z.div_le_upper_bound; auto. @@ -1035,20 +887,20 @@ Section CanonicalizationProofs. - eapply carry_full_2_bounds_0; eauto. - eapply carry_full_bounds; eauto; carry_length_conditions. carry_seq_lower_bound. - + rewrite <-max_bound_log_cap, <-Z.add_1_l. + + rewrite <-max_value_log_cap, <-Z.add_1_l. rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg. apply Z.add_le_mono. - apply Z.div_floor; auto. eapply Z.le_lt_trans; [ eapply carry_full_2_bounds_0; eauto | ]. replace (Z.succ 1) with (2 ^ 1) by ring. - rewrite <-max_bound_log_cap. + rewrite <-max_value_log_cap. ring_simplify. pose proof c_pos; omega. - apply carry_full_bounds; carry_length_conditions; carry_seq_lower_bound. Qed. Lemma carry_full_2_bounds' : forall us i j, pre_carry_bounds us -> (length us = length base)%nat -> (0 < i < length base)%nat -> (i + j < length base)%nat -> (j <> 0)%nat -> - 0 <= nth_default 0 (carry_sequence (make_chain (i + j)) (carry_full (carry_full us))) i <= max_bound i. + 0 <= nth_default 0 (carry_sequence (make_chain (i + j)) (carry_full (carry_full us))) i <= max_value i. Proof. induction j; intros; try omega. split; (destruct j; [ rewrite Nat.add_1_r; simpl @@ -1059,7 +911,7 @@ Section CanonicalizationProofs. Lemma carry_full_2_bounds : forall us i j, pre_carry_bounds us -> (length us = length base)%nat -> (0 < i < length base)%nat -> (i < j < length base)%nat -> - 0 <= nth_default 0 (carry_sequence (make_chain j) (carry_full (carry_full us))) i <= max_bound i. + 0 <= nth_default 0 (carry_sequence (make_chain j) (carry_full (carry_full us))) i <= max_value i. Proof. intros. replace j with (i + (j - i))%nat by omega. @@ -1100,20 +952,20 @@ Section CanonicalizationProofs. Lemma carry_carry_full_2_bounds_0_upper : forall us i, pre_carry_bounds us -> (length us = length base)%nat -> (0 < i < length base)%nat -> - (nth_default 0 (carry_sequence (make_chain i) (carry_full (carry_full us))) 0 <= max_bound 0 - c) + (nth_default 0 (carry_sequence (make_chain i) (carry_full (carry_full us))) 0 <= max_value 0 - c) \/ carry_done (carry_sequence (make_chain i) (carry_full (carry_full us))). Proof. induction i; try omega. intros ? length_eq ?; simpl. destruct i. - + destruct (Z_le_dec (nth_default 0 (carry_full (carry_full us)) 0) (max_bound 0)). + + destruct (Z_le_dec (nth_default 0 (carry_full (carry_full us)) 0) (max_value 0)). - right. apply carry_carry_done_done; try solve [carry_length_conditions]. apply carry_done_bounds; try solve [carry_length_conditions]. intros. simpl. split; [ auto using carry_full_2_bounds_lower | ]. - destruct i; rewrite <-max_bound_log_cap, Z.lt_succ_r; auto. + destruct i; rewrite <-max_value_log_cap, Z.lt_succ_r; auto. apply carry_full_bounds; auto using carry_full_bounds_lower. - left; unfold carry. break_if; @@ -1121,16 +973,16 @@ Section CanonicalizationProofs. autorewrite with push_nth_default natsimplify. simpl. remember ((nth_default 0 (carry_full (carry_full us)) 0)) as x. - apply Z.le_trans with (m := (max_bound 0 + c) - (1 + max_bound 0)); try omega. + apply Z.le_trans with (m := (max_value 0 + c) - (1 + max_value 0)); try omega. replace x with ((x - 2 ^ log_cap 0) + (1 * 2 ^ log_cap 0)) by ring. rewrite Z.pow2_mod_spec by eauto. cbv [make_chain carry_sequence fold_right]. rewrite Z.mod_add by (pose proof (pow_2_log_cap_pos 0); omega). - rewrite <-max_bound_log_cap, <-Z.add_1_l, Z.mod_small; + rewrite <-max_value_log_cap, <-Z.add_1_l, Z.mod_small; [ apply Z.sub_le_mono_r; subst; apply carry_full_2_bounds_0; auto | ]. split; try omega. pose proof carry_full_2_bounds_0. - apply Z.le_lt_trans with (m := (max_bound 0 + c) - (1 + max_bound 0)); + apply Z.le_lt_trans with (m := (max_value 0 + c) - (1 + max_value 0)); [ apply Z.sub_le_mono_r; subst x; apply carry_full_2_bounds_0; auto; ring_simplify | ]; pose proof c_pos; omega. + rewrite carry_unaffected_low by carry_length_conditions. @@ -1147,7 +999,7 @@ Section CanonicalizationProofs. Lemma carry_full_3_bounds : forall us i, pre_carry_bounds us -> (length us = length base)%nat ->(i < length base)%nat -> - 0 <= nth_default 0 (carry_full (carry_full (carry_full us))) i <= max_bound i. + 0 <= nth_default 0 (carry_full (carry_full (carry_full us))) i <= max_value i. Proof. intros. destruct i; [ | apply carry_full_bounds; carry_length_conditions; @@ -1167,7 +1019,7 @@ Section CanonicalizationProofs. + pose proof (carry_carry_full_2_bounds_0_upper us (pred (length base))). assert (0 < pred (length base) < length base)%nat by omega. intuition. - - replace (max_bound 0) with (c + (max_bound 0 - c)) by ring. + - replace (max_value 0) with (c + (max_value 0 - c)) by ring. apply Z.add_le_mono; try assumption. etransitivity; [ | replace c with (c * 1) by ring; reflexivity ]. apply Z.mul_le_mono_pos_l; try omega. @@ -1179,7 +1031,7 @@ Section CanonicalizationProofs. H : carry_done _ |- _ => destruct (H (pred (length base)) H0) as [Hcd1 Hcd2]; rewrite Hcd2 by omega end. ring_simplify. - apply shiftr_eq_0_max_bound; auto. + apply shiftr_eq_0_max_value; auto. assert (0 < length base)%nat as zero_lt_length by omega. match goal with H : carry_done _ |- _ => destruct (H 0%nat zero_lt_length) end. @@ -1193,7 +1045,7 @@ Section CanonicalizationProofs. intros. apply carry_done_bounds; [ carry_length_conditions | intros ]. destruct (lt_dec i (length base)). - + rewrite <-max_bound_log_cap, Z.lt_succ_r. + + rewrite <-max_value_log_cap, Z.lt_succ_r. auto using carry_full_3_bounds. + rewrite nth_default_out_of_bounds; carry_length_conditions. Qed. @@ -1206,7 +1058,7 @@ Section CanonicalizationProofs. Qed. Lemma isFull'_last : forall us b j, (j <> 0)%nat -> isFull' us b j = true -> - max_bound j = nth_default 0 us j. + max_value j = nth_default 0 us j. Proof. induction j; simpl; intros; try omega. match goal with @@ -1217,7 +1069,7 @@ Section CanonicalizationProofs. Qed. Lemma isFull'_lower_bound_0 : forall j us b, isFull' us b j = true -> - max_bound 0 - c < nth_default 0 us 0. + max_value 0 - c < nth_default 0 us 0. Proof. induction j; intros. + match goal with H : isFull' _ _ 0 = _ |- _ => cbv [isFull'] in H; @@ -1227,7 +1079,7 @@ Section CanonicalizationProofs. Qed. Lemma isFull'_true_full : forall us i j b, (i <> 0)%nat -> (i <= j)%nat -> isFull' us b j = true -> - max_bound i = nth_default 0 us i. + max_value i = nth_default 0 us i. Proof. induction j; intros; try omega. assert (i = S j \/ i <= j)%nat as cases by omega. @@ -1270,8 +1122,8 @@ Section CanonicalizationProofs. Qed. Lemma full_isFull'_true : forall j us, (length us = length base) -> - ( max_bound 0 - c < nth_default 0 us 0 - /\ (forall i, (0 < i <= j)%nat -> nth_default 0 us i = max_bound i)) -> + ( max_value 0 - c < nth_default 0 us 0 + /\ (forall i, (0 < i <= j)%nat -> nth_default 0 us i = max_value i)) -> isFull' us true j = true. Proof. induction j; intros. @@ -1285,8 +1137,8 @@ Section CanonicalizationProofs. Qed. Lemma isFull'_true_iff : forall j us, (length us = length base) -> (isFull' us true j = true <-> - max_bound 0 - c < nth_default 0 us 0 - /\ (forall i, (0 < i <= j)%nat -> nth_default 0 us i = max_bound i)). + max_value 0 - c < nth_default 0 us 0 + /\ (forall i, (0 < i <= j)%nat -> nth_default 0 us i = max_value i)). Proof. intros; split; intros; auto using full_isFull'_true. split; eauto using isFull'_lower_bound_0. @@ -1299,7 +1151,7 @@ Section CanonicalizationProofs. isFull' us true j = true. Proof. simpl; intros ? ? succ_true. - destruct (max_bound (S j) =? nth_default 0 us (S j)); auto. + destruct (max_value (S j) =? nth_default 0 us (S j)); auto. rewrite isFull'_false in succ_true. congruence. Qed. @@ -1434,7 +1286,7 @@ Section CanonicalizationProofs. Lemma nth_default_modulus_digits' : forall d j i, nth_default d (modulus_digits' j) i = if lt_dec i (S j) - then (if (eq_nat_dec i 0) then max_bound i - c + 1 else max_bound i) + then (if (eq_nat_dec i 0) then max_value i - c + 1 else max_value i) else d. Proof. induction j; intros; (break_if; [| apply nth_default_out_of_bounds; rewrite modulus_digits'_length; omega]). @@ -1452,7 +1304,7 @@ Section CanonicalizationProofs. Lemma nth_default_modulus_digits : forall d i, nth_default d modulus_digits i = if lt_dec i (length base) - then (if (eq_nat_dec i 0) then max_bound i - c + 1 else max_bound i) + then (if (eq_nat_dec i 0) then max_value i - c + 1 else max_value i) else d. Proof. unfold modulus_digits; intros. @@ -1467,7 +1319,7 @@ Section CanonicalizationProofs. intros. rewrite nth_default_modulus_digits. break_if; [ | split; auto; omega]. - break_if; subst; split; auto; try rewrite <- max_bound_log_cap; pose proof c_pos; omega. + break_if; subst; split; auto; try rewrite <- max_value_log_cap; pose proof c_pos; omega. Qed. Local Hint Resolve carry_done_modulus_digits. @@ -1511,8 +1363,8 @@ Section CanonicalizationProofs. rewrite decode'_cons, decode_nil, Z.add_0_r. replace z with (nth_default 0 base 0) by (rewrite base_eq; auto). rewrite nth_default_base by (omega || eauto). - replace (max_bound 0 - c + 1) with (Z.succ (max_bound 0) - c) by ring. - rewrite max_bound_log_cap. + replace (max_value 0 - c + 1) with (Z.succ (max_value 0) - c) by ring. + rewrite max_value_log_cap. rewrite sum_firstn_succ with (x := log_cap 0) by ( apply nth_error_Some_nth_default; rewrite <-base_length; omega). rewrite Z.pow_add_r by eauto. @@ -1523,7 +1375,7 @@ Section CanonicalizationProofs. - rewrite sum_firstn_succ with (x := log_cap (S i)) by (apply nth_error_Some_nth_default; rewrite <-base_length; omega). - rewrite Z.pow_add_r, <-max_bound_log_cap, set_higher by eauto. + rewrite Z.pow_add_r, <-max_value_log_cap, set_higher by eauto. rewrite IHi, modulus_digits'_length by omega. rewrite nth_default_base by (omega || eauto). ring. @@ -1550,14 +1402,14 @@ Section CanonicalizationProofs. + cbv [modulus_digits' map]. f_equal. apply land_max_ones_noop with (i := 0%nat). - rewrite <-max_bound_log_cap. + rewrite <-max_value_log_cap. pose proof c_pos; omega. + unfold modulus_digits'; fold modulus_digits'. rewrite map_app. f_equal; [ apply IHi; omega | ]. cbv [map]; f_equal. apply land_max_ones_noop with (i := S i). - rewrite <-max_bound_log_cap. + rewrite <-max_value_log_cap. split; auto; omega. Qed. @@ -1612,8 +1464,8 @@ Section CanonicalizationProofs. Hint Resolve freeze_preserves_rep. Lemma isFull_true_iff : forall us, (length us = length base) -> (isFull us = true <-> - max_bound 0 - c < nth_default 0 us 0 - /\ (forall i, (0 < i <= length base - 1)%nat -> nth_default 0 us i = max_bound i)). + max_value 0 - c < nth_default 0 us 0 + /\ (forall i, (0 < i <= length base - 1)%nat -> nth_default 0 us i = max_value i)). Proof. unfold isFull; intros; auto using isFull'_true_iff. Qed. @@ -1886,8 +1738,8 @@ Section CanonicalizationProofs. apply Z.compare_ge_iff. omega. * match goal with H : isFull' _ _ _ = true |- _ => - apply isFull'_true_iff in H; try assumption; destruct H as [? eq_max_bound] end. - specialize (eq_max_bound j). + apply isFull'_true_iff in H; try assumption; destruct H as [? eq_max_value] end. + specialize (eq_max_value j). omega. + apply isFull'_true_iff; try assumption. match goal with H : compare' _ _ _ <> Lt |- _ => apply compare'_not_Lt in H; [ destruct H as [Hdigit0 Hnonzero] | | ] end. @@ -1899,8 +1751,8 @@ Section CanonicalizationProofs. - intros. rewrite nth_default_modulus_digits. repeat (break_if; try omega). - rewrite <-Z.lt_succ_r with (m := max_bound i). - rewrite max_bound_log_cap; apply carry_done_bounds; assumption. + rewrite <-Z.lt_succ_r with (m := max_value i). + rewrite max_value_log_cap; apply carry_done_bounds; assumption. Qed. Lemma isFull_compare : forall us, (length us = length base) -> carry_done us -> @@ -1970,7 +1822,7 @@ Section CanonicalizationProofs. specialize (high_digits i i_range). clear first_digit i_range. rewrite high_digits. - rewrite <-max_bound_log_cap. + rewrite <-max_value_log_cap. rewrite nth_default_modulus_digits. repeat (break_if; try omega). * rewrite Z.sub_diag. @@ -2043,5 +1895,5 @@ Section CanonicalizationProofs. assert (length vs = length base) by (unfold rep in *; intuition). eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption. Qed. - +*) End CanonicalizationProofs. diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 6a8d4a8ff..db910ba93 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -170,10 +170,10 @@ Section BitwiseDecodeEncode. Local Hint Resolve limb_widths_nonneg. Local Notation "w[ i ]" := (nth_default 0 limb_widths i). Local Notation base := (base_from_limb_widths limb_widths). - Local Notation max := (upper_bound limb_widths). + Local Notation upper_bound := (upper_bound limb_widths). Lemma encode'_spec : forall x i, (i <= length base)%nat -> - encode' limb_widths x i = BaseSystem.encode' base x max i. + encode' limb_widths x i = BaseSystem.encode' base x upper_bound i. Proof. induction i; intros. + rewrite encode'_zero. reflexivity. @@ -185,7 +185,7 @@ Section BitwiseDecodeEncode. - repeat f_equal; rewrite nth_default_base by (omega || auto); reflexivity. - repeat f_equal; try solve [rewrite nth_default_base by (omega || auto); reflexivity]. rewrite nth_default_out_of_bounds by omega. - unfold upper_bound. + unfold Pow2Base.upper_bound. rewrite <-base_from_limb_widths_length by auto. congruence. Qed. @@ -195,7 +195,7 @@ Section BitwiseDecodeEncode. intros; apply nth_default_preserves_properties; auto; omega. Qed. Hint Resolve nth_default_limb_widths_nonneg. - Lemma base_upper_bound_compatible : @base_max_succ_divide base max. + Lemma base_upper_bound_compatible : @base_max_succ_divide base upper_bound. Proof. unfold base_max_succ_divide; intros i lt_Si_length. rewrite Nat.lt_eq_cases in lt_Si_length; destruct lt_Si_length; @@ -205,7 +205,7 @@ Section BitwiseDecodeEncode. rewrite Z.pow_add_r; auto using sum_firstn_limb_widths_nonneg. apply Z.divide_factor_r. + rewrite nth_default_out_of_bounds by omega. - unfold upper_bound. + unfold Pow2Base.upper_bound. replace (length limb_widths) with (S (pred (length limb_widths))) by (rewrite base_from_limb_widths_length in H by auto; omega). replace i with (pred (length limb_widths)) by @@ -218,12 +218,12 @@ Section BitwiseDecodeEncode. Hint Resolve base_upper_bound_compatible. Lemma encodeZ_spec : forall x, - BaseSystem.decode base (encodeZ limb_widths x) = x mod max. + BaseSystem.decode base (encodeZ limb_widths x) = x mod upper_bound. Proof. intros. assert (length base = length limb_widths) by auto using base_from_limb_widths_length. unfold encodeZ; rewrite encode'_spec by omega. - rewrite BaseSystemProofs.encode'_spec; unfold upper_bound; try zero_bounds; + rewrite BaseSystemProofs.encode'_spec; unfold Pow2Base.upper_bound; try zero_bounds; auto using sum_firstn_limb_widths_nonneg. rewrite nth_default_out_of_bounds by omega. reflexivity. @@ -356,14 +356,14 @@ End BitwiseDecodeEncode. Section Conversion. Context {limb_widthsA} (limb_widthsA_nonneg : forall w, In w limb_widthsA -> 0 <= w) {limb_widthsB} (limb_widthsB_nonneg : forall w, In w limb_widthsB -> 0 <= w). - Local Notation "{baseA}" := (base_from_limb_widths limb_widthsA). - Local Notation "{baseB}" := (base_from_limb_widths limb_widthsB). - Context (bvB : BaseSystem.BaseVector {baseB}). + Local Notation baseA := (base_from_limb_widths limb_widthsA). + Local Notation baseB := (base_from_limb_widths limb_widthsB). + Context (bvB : BaseSystem.BaseVector baseB). Definition convert xs := @encodeZ limb_widthsB (@decode_bitwise limb_widthsA xs). Lemma convert_spec : forall xs, @bounded limb_widthsA xs -> length xs = length limb_widthsA -> - BaseSystem.decode {baseA} xs mod (@upper_bound limb_widthsB) = BaseSystem.decode {baseB} (convert xs). + BaseSystem.decode baseA xs mod (@upper_bound limb_widthsB) = BaseSystem.decode baseB (convert xs). Proof. unfold convert; intros. rewrite encodeZ_spec, decode_bitwise_spec by auto. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index e0a194c3b..50ef9df00 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -11,7 +11,7 @@ Local Open Scope Z_scope. Section PseudoMersenneBaseParamProofs. Context `{prm : PseudoMersenneBaseParams}. - Local Notation "{base}" := (base_from_limb_widths limb_widths). + Local Notation base := (base_from_limb_widths limb_widths). Lemma limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. Proof. @@ -29,9 +29,9 @@ Section PseudoMersenneBaseParamProofs. (i < length limb_widths)%nat -> (j < length limb_widths)%nat -> (i+j >= length limb_widths)%nat-> - let b := nth_default 0 {base} in - let r := (b i * b j) / (2^k * b (i+j-length {base})%nat) in - b i * b j = r * (2^k * b (i+j-length {base})%nat). + let b := nth_default 0 base in + let r := (b i * b j) / (2^k * b (i+j-length base)%nat) in + b i * b j = r * (2^k * b (i+j-length base)%nat). Proof. intros. rewrite (Z.mul_comm r). @@ -53,8 +53,8 @@ Section PseudoMersenneBaseParamProofs. Qed. Lemma base_good : forall i j : nat, - (i + j < length {base})%nat -> - let b := nth_default 0 {base} in + (i + j < length base)%nat -> + let b := nth_default 0 base in let r := b i * b j / b (i + j)%nat in b i * b j = r * b (i + j)%nat. Proof. @@ -70,12 +70,12 @@ Section PseudoMersenneBaseParamProofs. rewrite <-base_from_limb_widths_length; auto using limb_widths_nonneg. Qed. - Lemma base_length : length {base} = length limb_widths. + Lemma base_length : length base = length limb_widths. Proof. auto using base_from_limb_widths_length. Qed. - Global Instance bv : BaseSystem.BaseVector {base} := { + Global Instance bv : BaseSystem.BaseVector base := { base_positive := base_positive limb_widths_nonneg; b0_1 := fun x => b0_1 x limb_widths_nonnil; base_good := base_good diff --git a/src/Testbit.v b/src/Testbit.v index 13d56f207..9a2f63751 100644 --- a/src/Testbit.v +++ b/src/Testbit.v @@ -13,7 +13,7 @@ Section Testbit. Context {width : Z} (limb_width_pos : 0 < width). Context (limb_widths : list Z) (limb_widths_nonnil : limb_widths <> nil) (limb_widths_uniform : forall w, In w limb_widths -> w = width). - Local Notation "{base}" := (base_from_limb_widths limb_widths). + Local Notation base := (base_from_limb_widths limb_widths). Definition testbit (us : list Z) (n : nat) := Z.testbit (nth_default 0 us (n / (Z.to_nat width))) (Z.of_nat (n mod Z.to_nat width)%nat). @@ -22,7 +22,7 @@ Section Testbit. Lemma testbit_spec' : forall a b us, (0 <= b < width) -> bounded limb_widths us -> (length us <= length limb_widths)%nat -> - Z.testbit (nth_default 0 us a) b = Z.testbit (decode {base} us) (Z.of_nat a * width + b). + Z.testbit (nth_default 0 us a) b = Z.testbit (decode base us) (Z.of_nat a * width + b). Proof. induction a; destruct us; intros; match goal with H : bounded _ _ |- _ => @@ -42,7 +42,7 @@ Section Testbit. Lemma testbit_spec : forall n us, (length us = length limb_widths)%nat -> bounded limb_widths us -> - testbit us n = Z.testbit (BaseSystem.decode {base} us) (Z.of_nat n). + testbit us n = Z.testbit (BaseSystem.decode base us) (Z.of_nat n). Proof. cbv [testbit]; intros. pose proof limb_width_pos as limb_width_pos_nat. |