diff options
author | Jason Gross <jasongross9@gmail.com> | 2016-07-18 19:09:46 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-07-18 19:09:46 +0200 |
commit | 07ca661557d86b96d1ee0a9b9013d0834158571f (patch) | |
tree | 78980ce7dbbf836f1d109159332600370ed224e6 /src/ModularArithmetic/ModularBaseSystem.v | |
parent | 0fd535b57b93bada6cc00c2e372f2f94d2768567 (diff) |
Move some definitions to Pow2Base (#24)
* Move some definitions to Pow2Base
These definitions don't depend on PseudoMersenneBaseParams, only on
limb_widths, and we'll want them for BarrettReduction / P256.
* Fix for Coq 8.4
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystem.v')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 24 |
1 files changed, 6 insertions, 18 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index b6138381e..23b0c2ef6 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -42,14 +42,10 @@ Section CarryBasePow2. Local Notation base := (base_from_limb_widths limb_widths). Local Notation log_cap i := (nth_default 0 limb_widths i). - Definition add_to_nth n (x:Z) xs := - set_nth n (x + nth_default 0 xs n) xs. - - Definition carry_simple 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 (S i) ( (Z.shiftr di (log_cap i))) us'. - + (* + 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 @@ -58,19 +54,11 @@ Section CarryBasePow2. Definition carry i : digits -> digits := if eq_nat_dec i (pred (length base)) then carry_and_reduce i - else carry_simple i. + else carry_simple limb_widths i. Definition carry_sequence is us := fold_right carry us is. - Fixpoint make_chain i := - match i with - | O => nil - | S i' => i' :: make_chain i' - end. - - Definition full_carry_chain := make_chain (length limb_widths). - - Definition carry_full := carry_sequence full_carry_chain. + Definition carry_full := carry_sequence (full_carry_chain limb_widths). Definition carry_mul us vs := carry_full (mul us vs). |