Factor out cmov{l,ne} and neg

This way we will have a faster build of reification things

4 files changed, 30 insertions, 23 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v
index 847df592b..8cce5481c 100644
--- a/src/ModularArithmetic/ModularBaseSystemList.v
+++ b/src/ModularArithmetic/ModularBaseSystemList.v
@@ -7,6 +7,7 @@ Require Import Crypto.BaseSystem.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
 Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Notations.
@@ -52,9 +53,6 @@ Section Defs.
 
   Definition modulus_digits := encodeZ limb_widths modulus.
 
-  Definition cmovl (x y r1 r2 : Z) := if Z.leb x y then r1 else r2.
-  Definition cmovne (x y r1 r2 : Z) := if Z.eqb x y then r1 else r2.
-
   (* Constant-time comparison with modulus; only works if all digits of [us]
     are less than 2 ^ their respective limb width. *)
   Fixpoint ge_modulus' {A} (f : Z -> A) us (result : Z) i :=
@@ -68,11 +66,6 @@ Section Defs.
 
   Definition ge_modulus us := ge_modulus' id us 1 (length limb_widths - 1)%nat.
 
-  (* analagous to NEG assembly instruction on an integer that is 0 or 1:
-       neg 1 = 2^64 - 1 (on 64-bit; 2^32-1 on 32-bit, etc.) 
-       neg 0 = 0 *)
-  Definition neg (int_width : Z) (b : Z) := if b =? 1 then Z.ones int_width else 0.
-
   Definition conditional_subtract_modulus int_width (us : digits) (cond : Z) :=
     (* [and_term] is all ones if us' is full, so the subtractions subtract q overall.
        Otherwise, it's all zeroes, and the subtractions do nothing. *)
@@ -85,7 +78,7 @@ Section Defs.
   Context {target_widths} (target_widths_nonneg : forall x, In x target_widths -> 0 <= x)
           (bits_eq : sum_firstn limb_widths   (length limb_widths) =
                      sum_firstn target_widths (length target_widths)).
-  
+
   Definition pack := @convert limb_widths limb_widths_nonneg
                               target_widths target_widths_nonneg
                               (Z.eq_le_incl _ _ bits_eq).
@@ -93,5 +86,5 @@ Section Defs.
   Definition unpack := @convert target_widths target_widths_nonneg
                                 limb_widths limb_widths_nonneg
                                 (Z.eq_le_incl _ _ (Z.eq_sym bits_eq)).
-  
-End Defs.
\ No newline at end of file
+
+End Defs.
diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v
index 3a6ffbeac..9cb65bd19 100644
--- a/src/ModularArithmetic/ModularBaseSystemListProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v
@@ -16,6 +16,7 @@ Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Notations.
 
+Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemList.
 Local Open Scope Z_scope.
 
@@ -189,7 +190,7 @@ Section ModulusDigitsProofs.
            | |- _ => unique pose proof modulus_pos
            | |- _ => unique assert (modulus = 2 ^ k - c) by (cbv [c]; ring)
            | |- _ => break_if
-           | |- _ => rewrite decode_modulus_digits 
+           | |- _ => rewrite decode_modulus_digits
            | |- _ => rewrite Z.testbit_pow2_mod
                        by eauto using nth_default_limb_widths_nonneg
            | |- _ => rewrite Z.ones_spec by eauto using nth_default_limb_widths_nonneg
@@ -204,7 +205,7 @@ Section ModulusDigitsProofs.
            | |- Z.testbit modulus ?i = true => transitivity (Z.testbit (2 ^ k - c) i)
            | |- _ => congruence
            end.
-    
+
     replace (c - 1) with ((c - 1) mod 2 ^ nth_default 0 limb_widths 0) by (apply Z.mod_small; omega).
     rewrite Z.mod_pow2_bits_high; auto.
     pose proof (sum_firstn_prefix_le limb_widths 1 i).
@@ -244,7 +245,7 @@ Section ModulusComparisonProofs.
   (* Lexicographically compare two vectors of equal length, starting from the END of the list
      (in our context, this is the most significant end). NOT constant time. *)
   Definition compare us vs := compare' us vs (length us).
-  
+
   Lemma decode_firstn_compare' : forall us vs i,
     (i <= length limb_widths)%nat ->
     length us = length limb_widths -> bounded limb_widths us ->
@@ -258,8 +259,8 @@ Section ModulusComparisonProofs.
              | |- _ => progress (simpl compare')
              | |- _ => progress specialize_by (assumption || omega)
              | |- _ => rewrite sum_firstn_0
-             | |- _ => rewrite set_higher 
-             | |- _ => rewrite nth_default_base by eauto 
+             | |- _ => rewrite set_higher
+             | |- _ => rewrite nth_default_base by eauto
              | |- _ => rewrite firstn_length, Min.min_l by omega
              | |- _ => rewrite firstn_O
              | |- _ => rewrite firstn_succ with (d := 0) by omega
@@ -270,7 +271,7 @@ Section ModulusComparisonProofs.
                (rewrite (Z.mul_comm (2 ^ x)); apply Z.shiftl_mul_pow2; eauto)
              | |- _ => tauto
              | |- _ => split
-             | |- _ => break_if 
+             | |- _ => break_if
              end.
   Qed.
 
@@ -321,7 +322,7 @@ Section ModulusComparisonProofs.
              | |- _ =>erewrite (ge_modulus'_0 (@id Z)) in *
              | H : (?x <= 0)%nat |- _ => progress replace x with 0%nat in * by omega
              | |- _ => break_if
-             | |- _ => discriminate 
+             | |- _ => discriminate
              | |- _ => solve [rewrite ?Z.leb_le, ?Z.eqb_eq in *; omega]
              end.
     destruct (le_dec j i).
@@ -440,7 +441,7 @@ Section ConditionalSubtractModulusProofs.
   Proof.
     induction us; boring.
   Qed.
-  
+
   Hint Rewrite @length_modulus_digits @length_zeros : distr_length.
   Lemma conditional_subtract_modulus_spec : forall u cond
     (cond_01 : cond = 0 \/ cond = 1),
@@ -456,10 +457,10 @@ Section ConditionalSubtractModulusProofs.
            | |- _ => rewrite map_land_zero
            | |- _ => rewrite map2_sub_eq by distr_length
            | |- _ => rewrite sub_rep by auto
-           | |- _ => rewrite zeros_rep 
+           | |- _ => rewrite zeros_rep
            | |- _ => rewrite decode_modulus_digits by auto
            | |- _ => f_equal; ring
-           | |- _ => discriminate 
+           | |- _ => discriminate
            end.
   Qed.
 
@@ -475,7 +476,7 @@ Section ConditionalSubtractModulusProofs.
            | |- _ => rewrite map_land_zero
            | |- _ => rewrite length_modulus_digits in *
            | |- _ => rewrite length_zeros in *
-           | |- _ => rewrite Min.min_l in * by omega 
+           | |- _ => rewrite Min.min_l in * by omega
            | |- _ => rewrite nth_default_zeros
            | |- _ => rewrite nth_default_map2 with (d1 := 0) (d2 := 0)
            | |- _ => break_if
@@ -540,4 +541,4 @@ Section ConditionalSubtractModulusProofs.
     + pose proof (bounded_mul2_modulus u); specialize_by auto.
       omega.
   Qed.
-End ConditionalSubtractModulusProofs.
\ No newline at end of file
+End ConditionalSubtractModulusProofs.
diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperations.v b/src/ModularArithmetic/ModularBaseSystemListZOperations.v
new file mode 100644
index 000000000..1d863abbd
--- /dev/null
+++ b/src/ModularArithmetic/ModularBaseSystemListZOperations.v
@@ -0,0 +1,12 @@
+(** * Definitions of some basic operations on ℤ used in ModularBaseSystemList *)
+(** We separate these out so that we can depend on them in other files
+    without waiting for ModularBaseSystemList to build. *)
+Require Import Coq.ZArith.ZArith.
+
+Definition cmovl (x y r1 r2 : Z) := if Z.leb x y then r1 else r2.
+Definition cmovne (x y r1 r2 : Z) := if Z.eqb x y then r1 else r2.
+
+(* analagous to NEG assembly instruction on an integer that is 0 or 1:
+   neg 1 = 2^64 - 1 (on 64-bit; 2^32-1 on 32-bit, etc.)
+   neg 0 = 0 *)
+Definition neg (int_width : Z) (b : Z) := if Z.eqb b 1 then Z.ones int_width else 0%Z.
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index d2c73b57a..f7f6efad7 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -6,6 +6,7 @@ Require Import Crypto.ModularArithmetic.Conversion.
 Require Import Crypto.ModularArithmetic.Pow2Base.
 Require Import Crypto.ModularArithmetic.Pow2BaseProofs.
 Require Import Crypto.BaseSystem.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemList.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemListProofs.
 Require Import Crypto.ModularArithmetic.ModularBaseSystem.