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/ModularBaseSystemOpt.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/ModularBaseSystemOpt.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 116fe10e5..4f918e147 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -71,9 +71,10 @@ Ltac construct_params prime_modulus len k := cbv in lw; eapply Build_PseudoMersenneBaseParams with (limb_widths := lw); [ abstract (apply fold_right_and_True_forall_In_iff; simpl; repeat (split; [omega |]); auto) - | abstract (unfold limb_widths; cbv; congruence) + | abstract (cbv; congruence) | abstract brute_force_indices lw | abstract apply prime_modulus + | abstract (cbv; congruence) | abstract brute_force_indices lw]. Definition construct_mul2modulus {m} (prm : PseudoMersenneBaseParams m) : digits := |