diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-06-28 21:22:39 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-06-28 21:22:39 -0400 |
| commit | ce8862f3df1d7a9a961e8d0823fff2353e3ac7c2 (patch) | |
| tree | 458d3421e5e340a808387a250687790c778adbda /src/ModularArithmetic/PseudoMersenneBaseParams.v | |
| parent | b1b4493de3522c71ac3f40081eb95aeba5361dd0 (diff) | |
BaseSystem encode function is no longer naive; it does a mod/div loop rather than sticking the value of the Z input in the first digit. The condition that c is positive has been added to PseudoMersenneBaseParams--it is necessary for this encode and for canonicalization, for which it was previously a section variable.
Diffstat (limited to 'src/ModularArithmetic/PseudoMersenneBaseParams.v')
| -rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParams.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParams.v b/src/ModularArithmetic/PseudoMersenneBaseParams.v index e20a7ed09..02d409b68 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParams.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParams.v @@ -15,6 +15,7 @@ Class PseudoMersenneBaseParams (modulus : Z) := { prime_modulus : Znumtheory.prime modulus; k := sum_firstn limb_widths (length limb_widths); c := 2 ^ k - modulus; + c_pos : 0 < c; limb_widths_match_modulus : forall i j, (i < length limb_widths)%nat -> (j < length limb_widths)%nat -> |