Factored out some proofs that rely only on base being powers of two, and defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.

1 files changed, 1 insertions, 2 deletions

diff --git a/src/ModularArithmetic/PseudoMersenneBaseParams.v b/src/ModularArithmetic/PseudoMersenneBaseParams.v
index 02d409b68..1f9a0f2f6 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParams.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParams.v
@@ -1,10 +1,9 @@
 Require Import ZArith.
 Require Import List.
+Require Import Crypto.Util.ListUtil.
 Require Crypto.BaseSystem.
 Local Open Scope Z_scope.
 
-Definition sum_firstn l n := fold_right Z.add 0 (firstn n l).
-
 Class PseudoMersenneBaseParams (modulus : Z) := {
   limb_widths : list Z;
   limb_widths_pos : forall w, In w limb_widths -> 0 < w;