diff options
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystem.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 08545bdb4..856cb1e81 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -8,6 +8,7 @@ Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.Notations. +Require Import Crypto.ModularArithmetic.Pow2Base. Local Open Scope Z_scope. Section PseudoMersenneBase. @@ -19,7 +20,8 @@ Section PseudoMersenneBase. Local Notation "u ~= x" := (rep u x). Local Hint Unfold rep. - Definition encode (x : F modulus) := encode x ++ BaseSystem.zeros (length base - 1)%nat. + (* max must be greater than input; this is used to truncate last digit *) + Definition encode (x : F modulus) := encodeZ limb_widths x. (* Converts from length of extended base to length of base by reduction modulo M.*) Definition reduce (us : digits) : digits := @@ -101,15 +103,6 @@ Section Canonicalization. (* compute at compile time *) Definition modulus_digits := modulus_digits' (length base - 1). - Fixpoint map2 {A B C} (f : A -> B -> C) (la : list A) (lb : list B) : list C := - match la with - | nil => nil - | a :: la' => match lb with - | nil => nil - | b :: lb' => f a b :: map2 f la' lb' - end - end. - Definition and_term us := if isFull us then max_ones else 0. Definition freeze us := |