diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-04-11 22:39:00 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-04-11 22:39:00 -0400 |
| commit | ef4a656933ce31144ad11f83b7f6a0758cd7e518 (patch) | |
| tree | cf412e453462843e4d02b5bf342bd50cb1620219 /src/ModularArithmetic/PseudoMersenneBaseParams.v | |
| parent | ce1a0e8508f53481138362f14581193b7394552b (diff) | |
Merge and refactor of GF25519
Diffstat (limited to 'src/ModularArithmetic/PseudoMersenneBaseParams.v')
| -rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParams.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParams.v b/src/ModularArithmetic/PseudoMersenneBaseParams.v index 09f4bc68e..3914d6219 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParams.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParams.v @@ -12,11 +12,9 @@ Class PseudoMersenneBaseParams (modulus : Z) := { limb_widths_good : forall i j, (i + j < length limb_widths)%nat -> sum_firstn limb_widths (i + j) <= sum_firstn limb_widths i + sum_firstn limb_widths j; - k : Z; - c : Z; - k_matches_limb_widths : sum_firstn limb_widths (length limb_widths) = k; - modulus_pseudomersenne : modulus = 2^k - c; prime_modulus : Znumtheory.prime modulus; + k := sum_firstn limb_widths (length limb_widths); + c := 2 ^ k - modulus; limb_widths_match_modulus : forall i j, (i < length limb_widths)%nat -> (j < length limb_widths)%nat -> |