diff options
| -rw-r--r-- | _CoqProject | 4 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 126 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemField.v | 71 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemInterface.v | 150 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemList.v | 69 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListProofs.v | 95 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 142 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 507 | ||||
| -rw-r--r-- | src/ModularArithmetic/Pow2Base.v | 1 | ||||
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 22 | ||||
| -rw-r--r-- | src/Specific/GF1305.v | 60 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 59 |
12 files changed, 622 insertions, 684 deletions
diff --git a/_CoqProject b/_CoqProject index 404178d8a..187ea6541 100644 --- a/_CoqProject +++ b/_CoqProject @@ -38,7 +38,9 @@ src/ModularArithmetic/ExtPow2BaseMulProofs.v src/ModularArithmetic/ExtendedBaseVector.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v -src/ModularArithmetic/ModularBaseSystemInterface.v +src/ModularArithmetic/ModularBaseSystemField.v +src/ModularArithmetic/ModularBaseSystemList.v +src/ModularArithmetic/ModularBaseSystemListProofs.v src/ModularArithmetic/ModularBaseSystemOpt.v src/ModularArithmetic/ModularBaseSystemProofs.v src/ModularArithmetic/Pow2Base.v diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 8c850c941..70c8138da 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -1,103 +1,79 @@ 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). +Section ModularBaseSystem. + Context `{prm :PseudoMersenneBaseParams}. Local Notation base := (base_from_limb_widths limb_widths). + 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 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 limb_widths) us vs). + Definition decode (us : digits) : F modulus := decode [[us]]. - (* 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. + Definition encode (x : F modulus) : digits := from_list (encode x) length_encode. -End PseudoMersenneBase. - -Section CarryBasePow2. - Context `{prm :PseudoMersenneBaseParams}. - Local Notation base := (base_from_limb_widths limb_widths). - Local Notation log_cap i := (nth_default 0 limb_widths i). + Definition add (us vs : digits) : digits := from_list (add [[us]] [[vs]]) + (add_same_length _ _ _ length_to_list length_to_list). - (* - 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 mul (us vs : digits) : digits := from_list (mul [[us]] [[vs]]) + (length_mul length_to_list length_to_list). - 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 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). - Definition carry_sequence is us := fold_right carry us is. + Definition zero : digits := encode (ZToField 0). - Definition carry_full := carry_sequence (full_carry_chain limb_widths). + Definition one : digits := encode (ZToField 1). - Definition carry_mul us vs := carry_full (mul us vs). + (* Placeholder *) + Definition opp (x : digits) : digits := encode (ModularArithmetic.opp (decode x)). -End CarryBasePow2. + (* Placeholder *) + Definition inv (x : digits) : digits := encode (ModularArithmetic.inv (decode x)). -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). + (* Placeholder *) + Definition div (x y : digits) : digits := encode (ModularArithmetic.div (decode x) (decode y)). - (* compute at compile time *) - Definition max_ones := Z.ones (fold_right Z.max 0 limb_widths). + Definition carry i (us : digits) : digits := from_list (carry i [[us]]) + (length_carry length_to_list). - Definition max_bound i := Z.ones (log_cap i). + Definition rep (us : digits) (x : F modulus) := decode us = x. + Local Notation "u ~= x" := (rep u x). + Local Hint Unfold rep. - 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 carry_sequence is (us : digits) : digits := fold_right carry us is. - Definition isFull us := isFull' us true (length base - 1)%nat. + Definition carry_full : digits -> digits := carry_sequence (full_carry_chain limb_widths). - 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_mul (us vs : digits) : digits := carry_full (mul us vs). - (* compute at compile time *) - Definition modulus_digits := modulus_digits' (length base - 1). + Definition freeze (us : digits) : digits := + let us' := carry_full (carry_full (carry_full us)) in + from_list (conditional_subtract_modulus [[us']] (ge_modulus [[us']])) + (length_conditional_subtract_modulus length_to_list). - Definition and_term us := if isFull us then max_ones else 0. + Definition eq (x y : digits) : Prop := decode x = decode y. - Definition freeze us := - 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). + Import Morphisms. + Global Instance eq_Equivalence : Equivalence eq. + Proof. + split; cbv [eq]; repeat intro; congruence. + Qed. -End Canonicalization. +End ModularBaseSystem.
\ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemField.v b/src/ModularArithmetic/ModularBaseSystemField.v new file mode 100644 index 000000000..f5bedd644 --- /dev/null +++ b/src/ModularArithmetic/ModularBaseSystemField.v @@ -0,0 +1,71 @@ +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Algebra. Import Field. +Require Import Crypto.Util.Tuple Crypto.Util.Notations. +Local Open Scope Z_scope. + +Section ModularBaseSystemField. + Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm} + (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_). + Local Notation base := (Pow2Base.base_from_limb_widths limb_widths). + Local Notation digits := (tuple Z (length limb_widths)). + + Lemma add_decode : forall a b : digits, + decode (add_opt a b) = (decode a + decode b)%F. + Proof. + intros; rewrite add_opt_correct by assumption. + apply add_rep; apply decode_rep. + Qed. + + Lemma sub_decode : forall a b : digits, + decode (sub_opt a b) = (decode a - decode b)%F. + Proof. + intros; rewrite sub_opt_correct by assumption. + apply sub_rep; auto using coeff_mod, decode_rep. + Qed. + + Lemma mul_decode : forall a b : digits, + decode (carry_mul_opt k_ c_ a b) = (decode a * decode b)%F. + Proof. + intros; rewrite carry_mul_opt_correct by assumption. + apply carry_mul_rep; apply decode_rep. + Qed. + + Lemma zero_neq_one : eq zero one -> False. + Proof. + cbv [eq zero one]. erewrite !encode_rep. intro A. + eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). + congruence. + Qed. + + Lemma modular_base_system_field : + @field digits eq zero one opp add_opt sub_opt (carry_mul_opt k_ c_) inv div. + Proof. + eapply (Field.isomorphism_to_subfield_field (phi := decode) (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))). + Grab Existential Variables. + + intros; eapply encode_rep. + + intros; eapply encode_rep. + + intros; eapply encode_rep. + + intros; eapply encode_rep. + + intros; eapply mul_decode. + + intros; eapply sub_decode. + + intros; eapply add_decode. + + intros; eapply encode_rep. + + cbv [eq zero one]. erewrite !encode_rep. intro A. + eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). + congruence. + + trivial. + + repeat intro. cbv [div]. congruence. + + repeat intro. cbv [inv]. congruence. + + repeat intro. cbv [eq]. erewrite !mul_decode. congruence. + + repeat intro. cbv [eq]. erewrite !sub_decode. congruence. + + repeat intro. cbv [eq]. erewrite !add_decode. congruence. + + repeat intro. cbv [opp]. congruence. + + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec. + Qed. + +End ModularBaseSystemField.
\ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemInterface.v b/src/ModularArithmetic/ModularBaseSystemInterface.v deleted file mode 100644 index c79dce1d3..000000000 --- a/src/ModularArithmetic/ModularBaseSystemInterface.v +++ /dev/null @@ -1,150 +0,0 @@ -Require Import Crypto.BaseSystem. -Require Import Crypto.ModularArithmetic.ModularBaseSystem. -Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. -Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. -Require Import Crypto.BaseSystemProofs. -Require Import Crypto.Util.Tuple Crypto.Util.CaseUtil. -Require Import ZArith. -Require Import Crypto.Algebra. -Import Group. -Import PseudoMersenneBaseParams PseudoMersenneBaseParamProofs. - -Generalizable All Variables. -Section s. - Context `{prm:PseudoMersenneBaseParams m} {sc : SubtractionCoefficient m prm}. - Context {k_ c_} (pfk : k = k_) (pfc:c = c_). - Local Notation base := (Pow2Base.base_from_limb_widths limb_widths). - - Definition fe := tuple Z (length base). - - Arguments to_list {_ _} _. - - Definition mul (x y:fe) : fe := - carry_mul_opt_cps k_ c_ (from_list_default 0%Z (length base)) - (to_list x) (to_list y). - - Definition add (x y : fe) : fe := - from_list_default 0%Z (length base) (add_opt (to_list x) (to_list y)). - - Definition sub : fe -> fe -> fe. - refine (on_tuple2 sub_opt _). - abstract (intros; rewrite sub_opt_correct; apply length_sub; rewrite ?coeff_length; auto). - Defined. - - Definition phi (a : fe) : ModularArithmetic.F m := decode (to_list a). - Definition phi_inv (a : ModularArithmetic.F m) : fe := - from_list_default 0%Z _ (encode a). - - Lemma phi_inv_spec : forall a, phi (phi_inv a) = a. - Proof. - intros; cbv [phi_inv phi]. - erewrite from_list_default_eq. - rewrite to_list_from_list. - apply ModularBaseSystemProofs.encode_rep. - Grab Existential Variables. - apply ModularBaseSystemProofs.encode_rep. - Qed. - - Definition eq (x y : fe) : Prop := phi x = phi y. - - Import Morphisms. - Global Instance eq_Equivalence : Equivalence eq. - Proof. - split; cbv [eq]; repeat intro; congruence. - Qed. - - Lemma phi_inv_spec_reverse : forall a, eq (phi_inv (phi a)) a. - Proof. - intros. unfold eq. rewrite phi_inv_spec; reflexivity. - Qed. - - Definition zero : fe := phi_inv (ModularArithmetic.ZToField 0). - - Definition opp (x : fe) : fe := phi_inv (ModularArithmetic.opp (phi x)). - - Definition one : fe := phi_inv (ModularArithmetic.ZToField 1). - - Definition inv (x : fe) : fe := phi_inv (ModularArithmetic.inv (phi x)). - - Definition div (x y : fe) : fe := phi_inv (ModularArithmetic.div (phi x) (phi y)). - - Lemma add_correct : forall a b, - to_list (add a b) = BaseSystem.add (to_list a) (to_list b). - Proof. - intros; cbv [add]. - rewrite add_opt_correct. - erewrite from_list_default_eq. - apply to_list_from_list. - Grab Existential Variables. - apply add_same_length; auto using length_to_list. - Qed. - - Lemma add_phi : forall a b : fe, - phi (add a b) = ModularArithmetic.add (phi a) (phi b). - Proof. - intros; cbv [phi]. - rewrite add_correct. - apply ModularBaseSystemProofs.add_rep; auto using decode_rep, length_to_list. - Qed. - - Lemma sub_correct : forall a b, - to_list (sub a b) = ModularBaseSystem.sub coeff (to_list a) (to_list b). - Proof. - intros; cbv [sub on_tuple2]. - rewrite to_list_from_list. - apply sub_opt_correct. - Qed. - - Lemma sub_phi : forall a b : fe, - phi (sub a b) = ModularArithmetic.sub (phi a) (phi b). - Proof. - intros; cbv [phi]. - rewrite sub_correct. - apply ModularBaseSystemProofs.sub_rep; auto using decode_rep, length_to_list, - coeff_length, coeff_mod. - Qed. - - Lemma mul_correct : forall a b, - to_list (mul a b) = carry_mul (to_list a) (to_list b). - Proof. - intros; cbv [mul]. - rewrite carry_mul_opt_cps_correct by assumption. - erewrite from_list_default_eq. - apply to_list_from_list. - Grab Existential Variables. - apply carry_mul_length; apply length_to_list. - Qed. - - Lemma mul_phi : forall a b : fe, - phi (mul a b) = ModularArithmetic.mul (phi a) (phi b). - Proof. - intros; cbv beta delta [phi]. - rewrite mul_correct. - apply carry_mul_rep; auto using decode_rep, length_to_list. - Qed. - - Lemma modular_base_system_field : @field fe eq zero one opp add sub mul inv div. - Proof. - eapply (Field.isomorphism_to_subfield_field (phi := phi) (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))). - Grab Existential Variables. - + intros; eapply phi_inv_spec. - + intros; eapply phi_inv_spec. - + intros; eapply phi_inv_spec. - + intros; eapply phi_inv_spec. - + intros; eapply mul_phi. - + intros; eapply sub_phi. - + intros; eapply add_phi. - + intros; eapply phi_inv_spec. - + cbv [eq zero one]. erewrite !phi_inv_spec. intro A. - eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). congruence. - + trivial. - + repeat intro. cbv [div]. congruence. - + repeat intro. cbv [inv]. congruence. - + repeat intro. cbv [eq]. erewrite !mul_phi. congruence. - + repeat intro. cbv [eq]. erewrite !sub_phi. congruence. - + repeat intro. cbv [eq]. erewrite !add_phi. congruence. - + repeat intro. cbv [opp]. congruence. - + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec. - Qed. - -End s.
\ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v new file mode 100644 index 000000000..07b2c2bac --- /dev/null +++ b/src/ModularArithmetic/ModularBaseSystemList.v @@ -0,0 +1,69 @@ +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.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.Notations. +Require Import Crypto.ModularArithmetic.Pow2Base. +Local Open Scope Z_scope. + +Section Defs. + Context `{prm :PseudoMersenneBaseParams} (modulus_multiple : digits). + Local Notation base := (base_from_limb_widths limb_widths). + Local Notation "u [ i ]" := (nth_default 0 u i) (at level 40). + + Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us). + + 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 limb_widths) us in + let low := firstn (length limb_widths) us in + let wrap := map (Z.mul c) high in + BaseSystem.add low wrap. + + Definition mul (us vs : digits) := reduce (BaseSystem.mul (ext_base limb_widths) 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. + + (* + Definition carry_and_reduce := + carry_gen limb_widths (fun ci => c * ci). + *) + Definition carry_and_reduce i := fun us => + let di := us [i] in + let us' := set_nth i (Z.pow2_mod di (limb_widths [i])) us in + add_to_nth 0 (c * (Z.shiftr di (limb_widths [i]))) 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 modulus_digits := encodeZ limb_widths modulus. + + (* compute at compile time *) + Definition max_ones := Z.ones (fold_right Z.max 0 limb_widths). + + (* Constant-time comparison with modulus; only works if all digits of [us] + are less than 2 ^ their respective limb width. *) + Fixpoint ge_modulus' us acc i := + match i with + | O => andb (Z.ltb (modulus_digits [0]) (us [0])) acc + | S i' => ge_modulus' us (andb (Z.eqb (modulus_digits [i]) (us [i])) acc) i' + end. + + Definition ge_modulus us := ge_modulus' us true (length base - 1)%nat. + + Definition conditional_subtract_modulus (us : digits) (cond : bool) := + let and_term := if cond then max_ones else 0 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). + +End Defs.
\ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v new file mode 100644 index 000000000..35de02cde --- /dev/null +++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v @@ -0,0 +1,95 @@ +Require Import Zpower ZArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import List. +Require Import VerdiTactics. +Require Import Crypto.BaseSystemProofs. +Require Import Crypto.ModularArithmetic.Pow2Base. +Require Import Crypto.ModularArithmetic.Pow2BaseProofs. +Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.Notations. + +Require Import Crypto.ModularArithmetic.ModularBaseSystemList. +Local Open Scope Z_scope. + +Section LengthProofs. + Context `{prm :PseudoMersenneBaseParams}. + Local Notation base := (base_from_limb_widths limb_widths). + + Lemma length_encode {x} : length (encode x) = length limb_widths. + Proof. + cbv [encode encodeZ]; intros. + rewrite encode'_spec; + auto using encode'_length, limb_widths_nonneg, Nat.eq_le_incl, base_from_limb_widths_length. + Qed. + + Lemma length_reduce : forall us, + (length limb_widths <= length us <= length (ext_base limb_widths))%nat -> + (length (reduce us) = length limb_widths)%nat. + Proof. + rewrite extended_base_length. + unfold reduce; intros. + rewrite add_length_exact. + pose proof (@base_from_limb_widths_length limb_widths). + rewrite map_length, firstn_length, skipn_length, Min.min_l, Max.max_l; + omega. + Qed. + + Lemma length_mul {u v} : + length u = length limb_widths + -> length v = length limb_widths + -> length (mul u v) = length limb_widths. + Proof. + cbv [mul]; intros. + apply length_reduce. + destruct u; try congruence. + + rewrite @nil_length0 in *; omega. + + rewrite mul_length_exact, extended_base_length, base_from_limb_widths_length; try omega. + congruence. + Qed. + + Section Sub. + Context {mm : list Z} (mm_length : length mm = length limb_widths). + + Lemma length_sub {u v} : + length u = length limb_widths + -> length v = length limb_widths + -> length (sub mm u v) = length limb_widths. + Proof. + cbv [sub]; intros. + rewrite sub_length, add_length_exact. + repeat rewrite Max.max_r; omega. + Qed. + End Sub. + + Lemma length_carry_and_reduce {us}: forall i, 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 {u i} : + length u = length limb_widths + -> length (carry i u) = length limb_widths. + Proof. intros; unfold carry; break_if; autorewrite with distr_length; omega. Qed. + Hint Rewrite @length_carry : distr_length. + + Lemma length_modulus_digits : length modulus_digits = length limb_widths. + Proof. + intros; unfold modulus_digits, encodeZ. + rewrite encode'_spec, encode'_length; + auto using encode'_length, limb_widths_nonneg, Nat.eq_le_incl, base_from_limb_widths_length. + Qed. + + Lemma length_conditional_subtract_modulus {u cond} : + length u = length limb_widths + -> length (conditional_subtract_modulus u cond) = length limb_widths. + Proof. + intros; unfold conditional_subtract_modulus. + rewrite map2_length, map_length, length_modulus_digits. + apply Min.min_case; omega. + Qed. + +End LengthProofs.
\ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 1e748892d..ed8f80659 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -4,8 +4,12 @@ Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. Require Import Crypto.ModularArithmetic.Pow2BaseProofs. -Require Import Crypto.BaseSystem Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemList. +Require Import Crypto.ModularArithmetic.ModularBaseSystemListProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. Require Import Coq.Lists.List. +Require Import Crypto.Util.Tuple. Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil Crypto.Util.CaseUtil. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. @@ -14,8 +18,7 @@ Require Import Crypto.Tactics.VerdiTactics. Local Open Scope Z. Class SubtractionCoefficient (m : Z) (prm : PseudoMersenneBaseParams m) := { - coeff : BaseSystem.digits; - coeff_length : (length coeff = length (Pow2Base.base_from_limb_widths limb_widths))%nat; + coeff : tuple Z (length limb_widths); coeff_mod: decode coeff = 0%F }. @@ -37,9 +40,9 @@ Definition map_opt {A B} := Eval compute in @map A B. Definition full_carry_chain_opt := Eval compute in @Pow2Base.full_carry_chain. Definition length_opt := Eval compute in length. Definition base_from_limb_widths_opt := Eval compute in @Pow2Base.base_from_limb_widths. -Definition max_ones_opt := Eval compute in @max_ones. -Definition max_bound_opt := Eval compute in @max_bound. Definition minus_opt := Eval compute in minus. +Definition max_ones_opt := Eval compute in @max_ones. +Definition from_list_default_opt {A} := Eval compute in (@from_list_default A). Definition Let_In {A P} (x : A) (f : forall y : A, P y) := let y := x in f y. @@ -110,14 +113,16 @@ Section Carries. (* allows caller to precompute k and c *) (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_). Local Notation base := (Pow2Base.base_from_limb_widths limb_widths). + Local Notation digits := (tuple Z (length limb_widths)). Definition carry_opt_sig (i : nat) (b : digits) : { d : digits | (i < length limb_widths)%nat -> d = carry i b }. Proof. eexists ; intros. - cbv [carry]. - rewrite <- pull_app_if_sumbool. + cbv [carry ModularBaseSystemList.carry]. + rewrite <-from_list_default_eq with (d := 0%Z). + rewrite <-pull_app_if_sumbool. cbv beta delta [carry carry_and_reduce Pow2Base.carry_gen Pow2Base.carry_and_reduce_single Pow2Base.carry_simple Z.pow2_mod Z.ones Z.pred @@ -127,12 +132,13 @@ Section Carries. change @nth_default with @nth_default_opt in *. change @set_nth with @set_nth_opt in *. lazymatch goal with - | [ |- _ = (if ?br then ?c else ?d) ] + | [ |- _ = _ (if ?br then ?c else ?d) ] => let x := fresh "x" in let y := fresh "y" in evar (x:digits); evar (y:digits); transitivity (if br then x else y); subst x; subst y end. 2:cbv zeta. 2:break_if; reflexivity. + change @from_list_default with @from_list_default_opt. change @nth_default with @nth_default_opt. rewrite c_subst. change @set_nth with @set_nth_opt. @@ -141,10 +147,12 @@ Section Carries. reflexivity. Defined. - Definition carry_opt i b - := Eval cbv beta iota delta [proj1_sig carry_opt_sig] in proj1_sig (carry_opt_sig i b). + Definition carry_opt is us := Eval cbv [proj1_sig carry_opt_sig] in + proj1_sig (carry_opt_sig is us). - Definition carry_opt_correct i b : (i < length limb_widths)%nat -> carry_opt i b = carry i b := proj2_sig (carry_opt_sig i b). + Definition carry_opt_correct i us + : (i < length limb_widths)%nat -> carry_opt i us = carry i us + := proj2_sig (carry_opt_sig i us). Definition carry_sequence_opt_sig (is : list nat) (us : digits) : { b : digits | (forall i, In i is -> i < length base)%nat -> b = carry_sequence is us }. @@ -183,11 +191,10 @@ Section Carries. cbv beta iota delta [carry_opt]. let LHS := match goal with |- ?LHS = ?RHS => LHS end in let RHS := match goal with |- ?LHS = ?RHS => RHS end in - let RHSf := match (eval pattern (nth_default_opt 0%Z b i) in RHS) with ?RHSf _ => RHSf end in - change (LHS = Let_In (nth_default_opt 0%Z b i) RHSf). + let RHSf := match (eval pattern (nth_default_opt 0%Z (to_list _ b) i) in RHS) with ?RHSf _ => RHSf end in + change (LHS = Let_In (nth_default_opt 0%Z (to_list _ b) i) RHSf). change Z.shiftl with Z_shiftl_opt. - change (-1) with (Z_opp_opt 1). - change Z.add with Z_add_opt at 5 9 17 21. + match goal with |- appcontext[ ?x + -1] => change (x + -1) with (Z_add_opt x (Z_opp_opt 1)) end. reflexivity. Defined. @@ -265,13 +272,13 @@ Section Carries. Lemma carry_sequence_opt_cps_rep - : forall (is : list nat) (us : list Z) (x : F modulus), + : forall (is : list nat) (us : digits) (x : F modulus), (forall i : nat, In i is -> i < length base)%nat -> rep us x -> rep (carry_sequence_opt_cps is us) x. Proof. intros. rewrite carry_sequence_opt_cps_correct by assumption. - apply carry_sequence_rep; eauto using rep_length. + auto using carry_sequence_rep. Qed. Lemma full_carry_chain_bounds : forall i, In i (Pow2Base.full_carry_chain limb_widths) -> (i < length base)%nat. @@ -320,6 +327,7 @@ End Carries. Section Addition. Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}. + Local Notation digits := (tuple Z (length limb_widths)). Definition add_opt_sig (us vs : digits) : { b : digits | b = add us vs }. Proof. @@ -338,6 +346,7 @@ End Addition. Section Subtraction. Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}. + Local Notation digits := (tuple Z (length limb_widths)). Definition sub_opt_sig (us vs : digits) : { b : digits | b = sub coeff us vs }. Proof. @@ -358,9 +367,11 @@ Section Multiplication. Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm} (* allows caller to precompute k and c *) (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_). + Local Notation digits := (tuple Z (length limb_widths)). + Definition mul_bi'_step - (mul_bi' : nat -> digits -> list Z -> list Z) - (i : nat) (vsr : digits) (bs : list Z) + (mul_bi' : nat -> list Z -> list Z -> list Z) + (i : nat) (vsr : list Z) (bs : list Z) : list Z := match vsr with | [] => [] @@ -368,8 +379,8 @@ Section Multiplication. end. Definition mul_bi'_opt_step_sig - (mul_bi' : nat -> digits -> list Z -> list Z) - (i : nat) (vsr : digits) (bs : list Z) + (mul_bi' : nat -> list Z -> list Z -> list Z) + (i : nat) (vsr : list Z) (bs : list Z) : { l : list Z | l = mul_bi'_step mul_bi' i vsr bs }. Proof. eexists. @@ -384,19 +395,19 @@ Section Multiplication. Defined. Definition mul_bi'_opt_step - (mul_bi' : nat -> digits -> list Z -> list Z) - (i : nat) (vsr : digits) (bs : list Z) + (mul_bi' : nat -> list Z -> list Z -> list Z) + (i : nat) (vsr : list Z) (bs : list Z) : list Z := Eval cbv [proj1_sig mul_bi'_opt_step_sig] in proj1_sig (mul_bi'_opt_step_sig mul_bi' i vsr bs). Fixpoint mul_bi'_opt - (i : nat) (vsr : digits) (bs : list Z) {struct vsr} + (i : nat) (vsr : list Z) (bs : list Z) {struct vsr} : list Z := mul_bi'_opt_step mul_bi'_opt i vsr bs. Definition mul_bi'_opt_correct - (i : nat) (vsr : digits) (bs : list Z) + (i : nat) (vsr : list Z) (bs : list Z) : mul_bi'_opt i vsr bs = mul_bi' bs i vsr. Proof. revert i; induction vsr as [|vsr vsrs IHvsr]; intros. @@ -413,12 +424,12 @@ Section Multiplication. Qed. Definition mul'_step - (mul' : digits -> digits -> list Z -> digits) - (usr vs : digits) (bs : list Z) - : digits + (mul' : list Z -> list Z -> list Z -> list Z) + (usr vs : list Z) (bs : list Z) + : list Z := match usr with | [] => [] - | u :: usr' => add (mul_each u (mul_bi bs (length usr') vs)) (mul' usr' vs bs) + | u :: usr' => BaseSystem.add (mul_each u (mul_bi bs (length usr') vs)) (mul' usr' vs bs) end. Lemma map_zeros : forall a n l, @@ -428,9 +439,9 @@ Section Multiplication. Qed. Definition mul'_opt_step_sig - (mul' : digits -> digits -> list Z -> digits) - (usr vs : digits) (bs : list Z) - : { d : digits | d = mul'_step mul' usr vs bs }. + (mul' : list Z -> list Z -> list Z -> list Z) + (usr vs : list Z) (bs : list Z) + : { d : list Z | d = mul'_step mul' usr vs bs }. Proof. eexists. cbv [mul'_step]. @@ -449,18 +460,18 @@ Section Multiplication. Defined. Definition mul'_opt_step - (mul' : digits -> digits -> list Z -> digits) - (usr vs : digits) (bs : list Z) - : digits + (mul' : list Z -> list Z -> list Z -> list Z) + (usr vs : list Z) (bs : list Z) + : list Z := Eval cbv [proj1_sig mul'_opt_step_sig] in proj1_sig (mul'_opt_step_sig mul' usr vs bs). Fixpoint mul'_opt - (usr vs : digits) (bs : list Z) - : digits + (usr vs : list Z) (bs : list Z) + : list Z := mul'_opt_step mul'_opt usr vs bs. Definition mul'_opt_correct - (usr vs : digits) (bs : list Z) + (usr vs : list Z) (bs : list Z) : mul'_opt usr vs bs = mul' bs usr vs. Proof. revert vs; induction usr as [|usr usrs IHusr]; intros. @@ -471,13 +482,17 @@ Section Multiplication. cbv [mul_each mul_bi]. rewrite map_zeros. rewrite <- mul_bi'_opt_correct. + cbv [zeros]. reflexivity. } Qed. Definition mul_opt_sig (us vs : digits) : { b : digits | b = mul us vs }. Proof. eexists. - cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros reduce]. + cbv [mul ModularBaseSystemList.mul BaseSystem.mul mul_each mul_bi mul_bi' zeros reduce]. + rewrite <- from_list_default_eq with (d := 0%Z). + change (@from_list_default Z) with (@from_list_default_opt Z). + apply f_equal. rewrite ext_base_alt by auto using limb_widths_pos with zarith. rewrite <- mul'_opt_correct. change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt. @@ -512,6 +527,13 @@ Section Multiplication. Definition carry_mul_opt_cps_correct {T} (f:digits -> T) (us vs : digits) : carry_mul_opt_cps f us vs = f (carry_mul us vs) := proj2_sig (carry_mul_opt_sig f us vs). + + Definition carry_mul_opt := carry_mul_opt_cps id. + + Definition carry_mul_opt_correct (us vs : digits) + : carry_mul_opt us vs = carry_mul us vs := + carry_mul_opt_cps_correct id us vs. + End Multiplication. Section with_base. @@ -525,8 +547,8 @@ Section with_base. int_width_pos : 0 < int_width; int_width_compat : forall w, In w limb_widths -> w <= int_width; c_pos : 0 < c; - c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < max_bound 0 + 1; - c_reduce2 : c <= max_bound 0 - c; + c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < 2 ^ log_cap 0; + c_reduce2 : c < 2 ^ log_cap 0 - c; two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus }. End with_base. @@ -538,30 +560,26 @@ Section Canonicalization. (* allows caller to precompute k and c *) (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_) {int_width} (preconditions : freezePreconditions prm int_width). + Local Notation digits := (tuple Z (length limb_widths)). + + Definition encodeZ_opt := Eval compute in Pow2Base.encodeZ. Definition modulus_digits_opt_sig : - { b : digits | b = modulus_digits }. + { b : list Z | b = modulus_digits }. Proof. eexists. - cbv beta iota delta [modulus_digits modulus_digits' app]. - change @max_bound with max_bound_opt. - rewrite c_subst. - change length with length_opt. - change minus with minus_opt. - change Z.add with Z_add_opt. - change Z.sub with Z_sub_opt. - change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt. + cbv beta iota delta [modulus_digits]. + change Pow2Base.encodeZ with encodeZ_opt. reflexivity. Defined. - Definition modulus_digits_opt : digits + Definition modulus_digits_opt : list Z := Eval cbv [proj1_sig modulus_digits_opt_sig] in proj1_sig (modulus_digits_opt_sig). Definition modulus_digits_opt_correct : modulus_digits_opt = modulus_digits := proj2_sig (modulus_digits_opt_sig). - Definition carry_full_3_opt_cps_sig {T} (f : digits -> T) (us : digits) @@ -587,20 +605,20 @@ Section Canonicalization. { b : digits | b = freeze us }. Proof. eexists. - cbv [freeze]. - cbv [and_term]. + cbv [freeze conditional_subtract_modulus]. + rewrite <-from_list_default_eq with (d := 0%Z). + change (@from_list_default Z) with (@from_list_default_opt Z). let LHS := match goal with |- ?LHS = ?RHS => LHS end in let RHS := match goal with |- ?LHS = ?RHS => RHS end in - let RHSf := match (eval pattern (isFull (carry_full (carry_full (carry_full us)))) in RHS) with ?RHSf _ => RHSf end in - change (LHS = Let_In (isFull(carry_full (carry_full (carry_full us)))) RHSf). + let RHSf := match (eval pattern (to_list (length limb_widths) (carry_full (carry_full (carry_full us)))) in RHS) with ?RHSf _ => RHSf end in + change (LHS = Let_In (to_list (length limb_widths) (carry_full (carry_full (carry_full us)))) RHSf). let LHS := match goal with |- ?LHS = ?RHS => LHS end in let RHS := match goal with |- ?LHS = ?RHS => RHS end in let RHSf := match (eval pattern (carry_full (carry_full (carry_full us))) in RHS) with ?RHSf _ => RHSf end in rewrite <-carry_full_3_opt_cps_correct with (f := RHSf). - cbv beta iota delta [and_term isFull isFull']. + cbv beta iota delta [ge_modulus ge_modulus']. change length with length_opt. - change @max_bound with max_bound_opt. - rewrite c_subst. + change (nth_default 0 modulus_digits) with (nth_default_opt 0 modulus_digits_opt). change @max_ones with max_ones_opt. change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt. change minus with minus_opt. @@ -616,7 +634,7 @@ Section Canonicalization. Definition freeze_opt_correct us : freeze_opt us = freeze us := proj2_sig (freeze_opt_sig us). - +(* Lemma freeze_opt_canonical: forall us vs x, @pre_carry_bounds _ _ int_width us -> rep us x -> @pre_carry_bounds _ _ int_width vs -> rep vs x -> @@ -643,5 +661,5 @@ Section Canonicalization. split; eauto using freeze_opt_canonical. auto using freeze_opt_preserves_rep. Qed. - -End Canonicalization. +*) +End Canonicalization.
\ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index b815167e2..e6351dc17 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 auto. - 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 auto. + 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. @@ -73,75 +75,32 @@ Section PseudoMersenneProofs. destruct limb_widths; simpl in *; congruence. Qed. - 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, two_sum_firstn_limb_widths_nonzero; auto using bv. - * 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 auto. { - 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. Local Hint Resolve firstn_us_base_ext_base bv ExtBaseVector limb_widths_match_modulus. @@ -156,13 +115,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. @@ -189,53 +146,24 @@ Section PseudoMersenneProofs. BaseSystem.decode base (reduce us) mod modulus = BaseSystem.decode (ext_base limb_widths) 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 limb_widths))%nat -> - (length (reduce us) = length base)%nat. + Lemma mul_rep : forall u v x y, u ~= x -> v ~= y -> mul u v ~= (x*y)%F. 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. - 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. - pose proof limb_widths_nonnil. - autorewrite with distr_length in *. - destruct limb_widths; simpl in *; congruence. - 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 (auto using ExtBaseVector || rewrite extended_base_length; omega). - rewrite 2decode_short by auto with omega. - apply ZToField_mul. } + autounfold in *; unfold ModularBaseSystem.mul in *. + intuition idtac; subst. + rewrite to_list_from_list. + cbv [ModularBaseSystemList.mul ModularBaseSystemList.decode]. + rewrite ZToField_mod, reduce_rep, <-ZToField_mod. + pose proof (@base_from_limb_widths_length limb_widths). + rewrite mul_rep by (auto using ExtBaseVector || rewrite extended_base_length, !length_to_list; omega). + rewrite 2decode_short by (rewrite ?base_from_limb_widths_length; + auto using Nat.eq_le_incl, length_to_list with omega). + apply ZToField_mul. Qed. Lemma nth_default_base_positive : forall i, (i < length base)%nat -> @@ -259,11 +187,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. @@ -276,7 +204,7 @@ Section PseudoMersenneProofs. 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 auto | ]. + 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 | ]. @@ -284,7 +212,7 @@ Section PseudoMersenneProofs. - rewrite nth_default_out_of_bounds by omega. split; zero_bounds. + specialize (Hbounds i). - split; [ intuition auto | ]. + 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]. @@ -292,31 +220,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}. @@ -332,111 +252,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; try solve [ distr_length ]. - unfold rep, decode, carry in *. - intuition auto; break_if; subst; eauto; apply F_eq; simpl; intuition auto with zarith. + 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; distr_length. 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; distr_length. 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. @@ -448,36 +326,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}. @@ -486,13 +337,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. @@ -502,20 +353,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). @@ -528,13 +379,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. @@ -542,35 +393,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 auto; 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. @@ -589,16 +440,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. @@ -608,7 +459,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; @@ -640,7 +491,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. @@ -707,7 +558,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. @@ -717,7 +568,7 @@ Section CanonicalizationProofs. || omega). Qed. - Hint Rewrite pow2_mod_log_cap_small using (intuition auto; auto using shiftr_eq_0_max_bound) : core. + Hint Rewrite pow2_mod_log_cap_small using (intuition; auto using shiftr_eq_0_max_bound) : core. Lemma carry_carry_done_done : forall i us, (length us = length base)%nat -> @@ -730,13 +581,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; 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) @@ -753,7 +604,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. @@ -761,7 +612,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 | ]. @@ -840,7 +691,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)); @@ -878,13 +729,13 @@ Section CanonicalizationProofs. intros ? ? PCB ?. induction i. + simpl. specialize (PCB 0%nat). - intuition auto. + intuition. + simpl. destruct (lt_eq_lt_dec i (pred (length base))) as [[? | ? ] | ? ]. - apply carry_simple_no_overflow; carry_length_conditions; carry_seq_lower_bound. rewrite carry_sequence_unaffected; try omega. specialize (PCB (S i)); rewrite Nat.pred_succ in PCB. - break_if; intuition auto with zarith. + break_if; intuition. - unfold carry; break_if; try omega. rewrite nth_default_out_of_bounds; [ apply Z.pow_pos_nonneg; omega | ]. subst; unfold carry_and_reduce. @@ -895,7 +746,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. @@ -945,7 +796,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. @@ -953,7 +804,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. @@ -963,7 +814,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. @@ -1005,7 +856,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. @@ -1031,20 +882,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 @@ -1055,7 +906,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. @@ -1077,7 +928,7 @@ Section CanonicalizationProofs. apply pow2_mod_log_cap_bounds_lower. + rewrite carry_unaffected_low by carry_length_conditions. assert (0 < S i < length base)%nat by omega. - intuition auto. + intuition. Qed. Lemma carry_full_2_bounds_lower :forall us i, pre_carry_bounds us -> @@ -1096,20 +947,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; @@ -1117,21 +968,21 @@ 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. assert (0 < S i < length base)%nat by omega. - intuition auto; right. + intuition; right. apply carry_carry_done_done; try solve [carry_length_conditions]. assumption. Qed. @@ -1143,7 +994,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; @@ -1162,8 +1013,8 @@ Section CanonicalizationProofs. - eapply carry_carry_full_2_bounds_0_lower; eauto; omega. + pose proof (carry_carry_full_2_bounds_0_upper us (pred (length base))). assert (0 < pred (length base) < length base)%nat by omega. - intuition auto. - - replace (max_bound 0) with (c + (max_bound 0 - c)) by ring. + intuition. + - 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. @@ -1175,7 +1026,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. @@ -1189,7 +1040,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. @@ -1202,7 +1053,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 @@ -1213,7 +1064,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; @@ -1223,7 +1074,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. @@ -1266,23 +1117,23 @@ 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. + cbv [isFull']; apply Bool.andb_true_iff. - rewrite Z.ltb_lt; intuition auto. - + intuition auto. + rewrite Z.ltb_lt; intuition. + + intuition. simpl. match goal with H : forall j, _ -> ?b j = ?a j |- appcontext[?a ?i =? ?b ?i] => replace (a i =? b i) with true by (symmetry; apply Z.eqb_eq; symmetry; apply H; omega) end. - apply IHj; auto; intuition auto. + apply IHj; auto; intuition. 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. @@ -1295,7 +1146,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. @@ -1382,7 +1233,7 @@ Section CanonicalizationProofs. replace 1 with (Z.succ 0) by reflexivity. rewrite Z.le_succ_l, Z.lt_0_sub. match goal with H : carry_done us |- _ => rewrite carry_done_bounds in H by auto; specialize (H n) end. - replace x with (log_cap n); try intuition auto. + replace x with (log_cap n); try intuition. apply nth_error_value_eq_nth_default; auto. + repeat erewrite firstn_all_strong by omega. rewrite sum_firstn_all_succ by (rewrite <-base_length; omega). @@ -1411,7 +1262,7 @@ Section CanonicalizationProofs. - rewrite nth_default_base by (omega || eauto). apply Z.pow_nonneg; omega. - match goal with H : carry_done us |- _ => rewrite carry_done_bounds in H by auto; specialize (H n) end. - intuition auto. + intuition. + eapply Z.le_trans; [ apply IHn; eauto | ]. repeat rewrite firstn_all_strong by omega. omega. @@ -1430,7 +1281,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]). @@ -1448,7 +1299,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. @@ -1463,7 +1314,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. @@ -1507,8 +1358,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. @@ -1519,7 +1370,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. @@ -1546,14 +1397,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. @@ -1580,7 +1431,7 @@ Section CanonicalizationProofs. Lemma freeze_preserves_rep : forall us x, rep us x -> rep (freeze us) x. Proof. unfold rep; intros. - intuition auto; rewrite ?freeze_length; auto. + intuition; rewrite ?freeze_length; auto. unfold freeze, and_term. break_if. + apply decode_mod with (us := carry_full (carry_full (carry_full us))). @@ -1589,7 +1440,7 @@ Section CanonicalizationProofs. apply Min.min_r. simpl_lengths; omega. - repeat apply carry_full_preserves_rep; repeat rewrite carry_full_length; auto. - unfold rep; intuition auto. + unfold rep; intuition. - rewrite decode_map2_sub by (simpl_lengths; omega). rewrite map_land_max_ones_modulus_digits. rewrite decode_modulus_digits. @@ -1608,8 +1459,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. @@ -1882,8 +1733,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. @@ -1895,8 +1746,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 -> @@ -1966,7 +1817,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. @@ -2008,7 +1859,7 @@ Section CanonicalizationProofs. (BaseSystem.decode base us) mod modulus = (BaseSystem.decode base vs) mod modulus. Proof. unfold rep, decode; intros. - intuition auto. + intuition. repeat rewrite <-FieldToZ_ZToField. congruence. Qed. @@ -2024,7 +1875,7 @@ Section CanonicalizationProofs. repeat match goal with Hmin : minimal_rep ?us |- _ => unfold minimal_rep in Hmin; rewrite <- Hmin in eqmod; clear Hmin end. apply Z.compare_eq_iff in eqmod. - rewrite decode_compare in eqmod; unfold rep in *; auto; intuition auto; try congruence. + rewrite decode_compare in eqmod; unfold rep in *; auto; intuition; try congruence. apply compare_Eq; auto. congruence. Qed. @@ -2035,9 +1886,9 @@ Section CanonicalizationProofs. freeze us = freeze vs. Proof. intros. - assert (length us = length base) by (unfold rep in *; intuition auto). - assert (length vs = length base) by (unfold rep in *; intuition auto). + assert (length us = length base) by (unfold rep in *; intuition). + 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/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v index acc96ad73..c23cf8f40 100644 --- a/src/ModularArithmetic/Pow2Base.v +++ b/src/ModularArithmetic/Pow2Base.v @@ -39,7 +39,6 @@ Section Pow2Base. encode' z i' ++ (Z.shiftr (Z.land z (Z.ones (lw i))) (lw i')) :: nil end. - (* max must be greater than input; this is used to truncate last digit *) Definition encodeZ x:= encode' x (length limb_widths). (** ** Carrying *) diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index d95de5bd1..78c6bba0f 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -230,10 +230,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. @@ -245,7 +245,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. @@ -255,7 +255,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; @@ -265,7 +265,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 @@ -278,12 +278,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. @@ -416,14 +416,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/Specific/GF1305.v b/src/Specific/GF1305.v index 077c98954..fba77a4a8 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -1,13 +1,15 @@ -Require Import Crypto.ModularArithmetic.ModularBaseSystem. -Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Import Crypto.ModularArithmetic.ModularBaseSystemField. Require Import Coq.Lists.List Crypto.Util.ListUtil. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface. Require Import Crypto.Tactics.VerdiTactics. -Require Import Crypto.BaseSystem. Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Notations. Require Import Crypto.Algebra. Import ListNotations. @@ -26,12 +28,13 @@ Instance params1305 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 5%nat 130. Defined. -Definition mul2modulus := Eval compute in (construct_mul2modulus params1305). +Definition fe1305 := Eval compute in (tuple Z (length limb_widths)). + +Definition mul2modulus : fe1305 := + Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params1305)). Instance subCoeff : SubtractionCoefficient modulus params1305. apply Build_SubtractionCoefficient with (coeff := mul2modulus). - cbv; auto. - cbv [ModularBaseSystem.decode]. apply ZToField_eqmod. cbv; reflexivity. Defined. @@ -49,9 +52,7 @@ Definition c_ := Eval compute in c. Definition k_subst : k = k_ := eq_refl k_. Definition c_subst : c = c_ := eq_refl c_. -Definition fe1305 : Type := Eval cbv in fe. - -Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In phi. +Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In. Definition app_5 (f : fe1305) (P : fe1305 -> fe1305) : fe1305. Proof. @@ -80,25 +81,25 @@ Proof. Qed. Definition add_sig (f g : fe1305) : - { fg : fe1305 | fg = ModularBaseSystemInterface.add f g}. + { fg : fe1305 | fg = add_opt f g}. Proof. eexists. - rewrite <-appify2_correct. (* Coq 8.4 : 6s *) + rewrite <-appify2_correct. cbv. reflexivity. -Defined. (* Coq 8.4 : 7s *) +Defined. Definition add (f g : fe1305) : fe1305 := Eval cbv beta iota delta [proj1_sig add_sig] in proj1_sig (add_sig f g). Definition add_correct (f g : fe1305) - : add f g = ModularBaseSystemInterface.add f g := + : add f g = add_opt f g := Eval cbv beta iota delta [proj1_sig add_sig] in - proj2_sig (add_sig f g). (* Coq 8.4 : 10s *) + proj2_sig (add_sig f g). Definition sub_sig (f g : fe1305) : - { fg : fe1305 | fg = ModularBaseSystemInterface.sub f g}. + { fg : fe1305 | fg = sub_opt f g}. Proof. eexists. rewrite <-appify2_correct. @@ -111,12 +112,14 @@ Definition sub (f g : fe1305) : fe1305 := proj1_sig (sub_sig f g). Definition sub_correct (f g : fe1305) - : sub f g = ModularBaseSystemInterface.sub f g := + : sub f g = sub_opt f g := Eval cbv beta iota delta [proj1_sig sub_sig] in - proj2_sig (sub_sig f g). (* Coq 8.4 : 10s *) + proj2_sig (sub_sig f g). +(* For multiplication, we add another layer of definition so that we can + rewrite under the [let] binders. *) Definition mul_simpl_sig (f g : fe1305) : - { fg : fe1305 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}. + { fg : fe1305 | fg = carry_mul_opt k_ c_ f g}. Proof. cbv [fe1305] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -131,41 +134,40 @@ Definition mul_simpl (f g : fe1305) : fe1305 := proj1_sig (mul_simpl_sig f g). Definition mul_simpl_correct (f g : fe1305) - : mul_simpl f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g := + : mul_simpl f g = carry_mul_opt k_ c_ f g := Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in proj2_sig (mul_simpl_sig f g). Definition mul_sig (f g : fe1305) : - { fg : fe1305 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}. + { fg : fe1305 | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. rewrite <-mul_simpl_correct. rewrite <-appify2_correct. cbv. - autorewrite with zsimplify. reflexivity. -Defined. (* Coq 8.4 : 14s *) +Defined. Definition mul (f g : fe1305) : fe1305 := Eval cbv beta iota delta [proj1_sig mul_sig] in proj1_sig (mul_sig f g). Definition mul_correct (f g : fe1305) - : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g := + : mul f g = carry_mul_opt k_ c_ f g := Eval cbv beta iota delta [proj1_sig add_sig] in - proj2_sig (mul_sig f g). (* Coq 8.4 : 5s *) + proj2_sig (mul_sig f g). Import Morphisms. -Lemma field1305 : @field fe eq zero one opp add sub mul inv div. +Lemma field1305 : @field fe1305 eq zero one opp add sub mul inv div. Proof. pose proof (Equivalence_Reflexive : Reflexive eq). - eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_subst c_subst)). + eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_ c_ k_subst c_subst)). Grab Existential Variables. + reflexivity. + reflexivity. + reflexivity. - + intros; rewrite mul_correct; reflexivity. + + intros; rewrite mul_correct. reflexivity. + intros; rewrite sub_correct; reflexivity. + intros; rewrite add_correct; reflexivity. + reflexivity. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 6298941db..7ece3a5da 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -1,16 +1,19 @@ -Require Import Crypto.ModularArithmetic.ModularBaseSystem. -Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Import Crypto.ModularArithmetic.ModularBaseSystemField. Require Import Coq.Lists.List Crypto.Util.ListUtil. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface. Require Import Crypto.Tactics.VerdiTactics. -Require Import Crypto.BaseSystem. -Require Import Algebra. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Notations. +Require Import Crypto.Algebra. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Require Import Crypto.Util.Notations. Local Open Scope Z. (* BEGIN PseudoMersenneBaseParams instance construction. *) @@ -23,12 +26,13 @@ Instance params25519 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 10%nat 255. Defined. -Definition mul2modulus := Eval compute in (construct_mul2modulus params25519). +Definition fe25519 := Eval compute in (tuple Z (length limb_widths)). + +Definition mul2modulus : fe25519 := + Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params25519)). Instance subCoeff : SubtractionCoefficient modulus params25519. apply Build_SubtractionCoefficient with (coeff := mul2modulus). - cbv; auto. - cbv [ModularBaseSystem.decode]. apply ZToField_eqmod. cbv; reflexivity. Defined. @@ -45,11 +49,10 @@ Definition k_ := Eval compute in k. Definition c_ := Eval compute in c. Definition k_subst : k = k_ := eq_refl k_. Definition c_subst : c = c_ := eq_refl c_. -Definition fe25519 : Type := Eval cbv in fe. Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In. -Definition app_10 (f : fe25519) (P : fe25519 -> fe25519) : fe25519. +Definition app_5 (f : fe25519) (P : fe25519 -> fe25519) : fe25519. Proof. cbv [fe25519] in *. set (f0 := f). @@ -58,7 +61,7 @@ Proof. apply f0. Defined. -Lemma app_10_correct : forall f P, app_10 f P = P f. +Definition app_5_correct f (P : fe25519 -> fe25519) : app_5 f P = P f. Proof. intros. cbv [fe25519] in *. @@ -67,16 +70,16 @@ Proof. Qed. Definition appify2 (op : fe25519 -> fe25519 -> fe25519) (f g : fe25519):= - app_10 f (fun f0 => (app_10 g (fun g0 => op f0 g0))). + app_5 f (fun f0 => (app_5 g (fun g0 => op f0 g0))). Lemma appify2_correct : forall op f g, appify2 op f g = op f g. Proof. intros. cbv [appify2]. - etransitivity; apply app_10_correct. + etransitivity; apply app_5_correct. Qed. Definition add_sig (f g : fe25519) : - { fg : fe25519 | fg = ModularBaseSystemInterface.add f g}. + { fg : fe25519 | fg = add_opt f g}. Proof. eexists. rewrite <-appify2_correct. @@ -89,12 +92,12 @@ Definition add (f g : fe25519) : fe25519 := proj1_sig (add_sig f g). Definition add_correct (f g : fe25519) - : add f g = ModularBaseSystemInterface.add f g := + : add f g = add_opt f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (add_sig f g). Definition sub_sig (f g : fe25519) : - { fg : fe25519 | fg = ModularBaseSystemInterface.sub f g}. + { fg : fe25519 | fg = sub_opt f g}. Proof. eexists. rewrite <-appify2_correct. @@ -107,12 +110,14 @@ Definition sub (f g : fe25519) : fe25519 := proj1_sig (sub_sig f g). Definition sub_correct (f g : fe25519) - : sub f g = ModularBaseSystemInterface.sub f g := + : sub f g = sub_opt f g := Eval cbv beta iota delta [proj1_sig sub_sig] in proj2_sig (sub_sig f g). +(* For multiplication, we add another layer of definition so that we can + rewrite under the [let] binders. *) Definition mul_simpl_sig (f g : fe25519) : - { fg : fe25519 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}. + { fg : fe25519 | fg = carry_mul_opt k_ c_ f g}. Proof. cbv [fe25519] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -127,15 +132,15 @@ Definition mul_simpl (f g : fe25519) : fe25519 := proj1_sig (mul_simpl_sig f g). Definition mul_simpl_correct (f g : fe25519) - : mul_simpl f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g := + : mul_simpl f g = carry_mul_opt k_ c_ f g := Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in proj2_sig (mul_simpl_sig f g). Definition mul_sig (f g : fe25519) : - { fg : fe25519 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}. + { fg : fe25519 | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. - rewrite <- mul_simpl_correct. + rewrite <-mul_simpl_correct. rewrite <-appify2_correct. cbv. reflexivity. @@ -146,8 +151,8 @@ Definition mul (f g : fe25519) : fe25519 := proj1_sig (mul_sig f g). Definition mul_correct (f g : fe25519) - : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g := - Eval cbv beta iota delta [proj1_sig mul_sig] in + : mul f g = carry_mul_opt k_ c_ f g := + Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (mul_sig f g). Import Morphisms. @@ -155,12 +160,12 @@ Import Morphisms. Lemma field25519 : @field fe25519 eq zero one opp add sub mul inv div. Proof. pose proof (Equivalence_Reflexive : Reflexive eq). - eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_subst c_subst)). + eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_ c_ k_subst c_subst)). Grab Existential Variables. + reflexivity. + reflexivity. + reflexivity. - + intros; rewrite mul_correct; reflexivity. + + intros; rewrite mul_correct. reflexivity. + intros; rewrite sub_correct; reflexivity. + intros; rewrite add_correct; reflexivity. + reflexivity. |