Significantly faster wordToN, I hope

After    | File Name                                           | Before   || Change
--------------------------------------------------------------------------------------
3m22.43s | Total                                               | 3m22.13s || +0m00.30s
--------------------------------------------------------------------------------------
0m34.51s | Spec/Ed25519                                        | 0m34.56s || -0m00.05s
0m28.83s | Experiments/Ed25519                                 | 0m28.60s || +0m00.22s
0m17.28s | EdDSARepChange                                      | 0m17.25s || +0m00.03s
0m08.66s | [require-in-module,deprecated]
src/Assembly/GF25519 | 0m08.66s || +0m00.00s
0m08.46s | Encoding/PointEncoding                              | 0m08.47s || -0m00.00s
0m08.35s | Specific/GF25519BoundedCommonWord                   | 0m08.44s || -0m00.08s
0m07.74s | Specific/GF25519Reflective                          | 0m07.69s || +0m00.04s
0m07.59s | Specific/GF25519Reflective/Reified/Mul              | 0m07.65s || -0m00.06s
0m07.35s | Specific/GF25519BoundedCommon                       | 0m07.39s || -0m00.04s
0m06.88s | Specific/GF25519Reflective/Reified/Freeze           | 0m06.86s || +0m00.01s
0m05.80s | Bedrock/Word                                        | 0m05.74s || +0m00.05s
0m05.43s | Specific/SC25519                                    | 0m05.32s || +0m00.10s
0m04.76s | Reflection/Z/Interpretations                        | 0m04.65s || +0m00.10s
0m04.27s | Encoding/PointEncodingPre                           | 0m04.31s || -0m00.04s
0m03.72s | Assembly/GF25519BoundedInstantiation                | 0m03.68s || +0m00.04s
0m03.21s | Specific/GF25519Reflective/Reified/CarrySub         | 0m03.34s || -0m00.12s
0m02.91s | Specific/GF25519Reflective/Reified/CarryOpp         | 0m02.86s || +0m00.05s
0m02.84s | Specific/GF25519Reflective/Reified/CarryAdd         | 0m02.87s || -0m00.03s
0m02.70s | Assembly/State                                      | 0m02.67s || +0m00.03s
0m02.00s | Specific/GF25519Reflective/Reified/Unpack           | 0m01.96s || +0m00.04s
0m01.97s | Specific/GF25519Reflective/Reified/Sub              | 0m01.95s || +0m00.02s
0m01.95s | Specific/GF25519Reflective/Reified/Pack             | 0m02.03s || -0m00.07s
0m01.81s | Assembly/Evaluables                                 | 0m01.88s || -0m00.06s
0m01.78s | Specific/GF25519Bounded                             | 0m01.77s || +0m00.01s
0m01.71s | Specific/GF25519Reflective/Reified/Opp              | 0m01.68s || +0m00.03s
0m01.66s | Specific/GF25519Reflective/Reified/Add              | 0m01.66s || +0m00.00s
0m01.52s | Assembly/Compile                                    | 0m01.48s || +0m00.04s
0m01.49s | Specific/GF25519Reflective/Reified/GeModulus        | 0m01.48s || +0m00.01s
0m01.44s | Assembly/WordizeUtil                                | 0m01.51s || -0m00.07s
0m01.33s | Assembly/Bounds                                     | 0m01.34s || -0m00.01s
0m01.22s | Assembly/Conversions                                | 0m01.23s || -0m00.01s
0m01.05s | Util/WordUtil                                       | 0m01.03s || +0m00.02s
0m00.94s | Assembly/LL                                         | 0m00.94s || +0m00.00s
0m00.94s | Assembly/Pipeline                                   | 0m00.90s || +0m00.03s
0m00.87s | Assembly/HL                                         | 0m00.89s || -0m00.02s
0m00.81s | Assembly/PhoasCommon                                | 0m00.77s || +0m00.04s
0m00.79s | Assembly/QhasmEvalCommon                            | 0m00.83s || -0m00.03s
0m00.75s | Specific/GF25519Reflective/Reified                  | 0m00.80s || -0m00.05s
0m00.72s | Specific/GF25519Reflective/Common                   | 0m00.71s || +0m00.01s
0m00.70s | Encoding/ModularWordEncodingTheorems                | 0m00.65s || +0m00.04s
0m00.66s | Spec/EdDSA                                          | 0m00.66s || +0m00.00s
0m00.61s | Spec/ModularWordEncoding                            | 0m00.58s || +0m00.03s
0m00.61s | Encoding/ModularWordEncodingPre                     | 0m00.67s || -0m00.06s
0m00.51s | Assembly/Qhasm                                      | 0m00.51s || +0m00.00s
0m00.48s | Assembly/StringConversion                           | 0m00.50s || -0m00.02s
0m00.47s | Assembly/QhasmUtil                                  | 0m00.40s || +0m00.06s
0m00.36s | Assembly/QhasmCommon                                | 0m00.31s || +0m00.04s

2 files changed, 20 insertions, 22 deletions

diff --git a/Bedrock/Word.v b/Bedrock/Word.v
index 036b3198a..2c518807d 100644
--- a/Bedrock/Word.v
+++ b/Bedrock/Word.v
@@ -48,8 +48,8 @@ Fixpoint natToWord (sz n : nat) : word sz :=
 Fixpoint wordToN sz (w : word sz) : N :=
   match w with
     | WO => 0
-    | WS false _ w' => 2 * wordToN w'
-    | WS true _ w' => Nsucc (2 * wordToN w')
+    | WS false _ w' => N.double (wordToN w')
+    | WS true _ w' => N.succ_double (wordToN w')
   end%N.
 
 Definition Nmod2 (n : N) : bool :=
@@ -506,6 +506,8 @@ Theorem wordToN_nat : forall sz (w : word sz), wordToN w = N_of_nat (wordToNat w
   rewrite N_of_mult.
   rewrite <- IHw.
   rewrite Nmult_comm.
+  rewrite N.succ_double_spec.
+  rewrite N.add_1_r.
   reflexivity.
 
   rewrite N_of_mult.
@@ -1038,12 +1040,12 @@ Proof.
   induction a; intro b0; rewrite (shatter_word b0); intuition.
   simpl in H.
   destruct b; destruct (whd b0); intros.
-  f_equal. eapply IHa. eapply Nsucc_inj in H.
+  f_equal. eapply IHa. eapply N.succ_double_inj in H.
   destruct (wordToN a); destruct (wordToN (wtl b0)); try congruence.
   destruct (wordToN (wtl b0)); destruct (wordToN a); inversion H.
   destruct (wordToN (wtl b0)); destruct (wordToN a); inversion H.
   f_equal. eapply IHa.
-  destruct (wordToN a); destruct (wordToN (wtl b0)); try congruence.
+  destruct (wordToN a); destruct (wordToN (wtl b0)); simpl in *; try congruence.
 Qed.
 Lemma unique_inverse : forall sz (a b1 b2 : word sz),
   a ^+ b1 = wzero _ ->
diff --git a/src/Assembly/WordizeUtil.v b/src/Assembly/WordizeUtil.v
index 6526c94ac..2727bac07 100644
--- a/src/Assembly/WordizeUtil.v
+++ b/src/Assembly/WordizeUtil.v
@@ -162,7 +162,7 @@ Section Misc.
       intros x H.
 
     replace (& wones (S n)) with (2 * & (wones n) + N.b2n true)%N
-      by (simpl; nomega).
+      by (simpl; rewrite ?N.succ_double_spec; simpl; nomega).
 
     rewrite N.testbit_succ_r; reflexivity.
   Qed.
@@ -181,7 +181,7 @@ Section Misc.
 
       + replace (& (wones (S (S n))))
            with (2 * (& (wones (S n))) + N.b2n true)%N
-          by (simpl; nomega).
+          by (simpl; rewrite ?N.succ_double_spec; simpl; nomega).
         rewrite Nat2N.inj_succ.
         rewrite N.testbit_succ_r.
         assumption.
@@ -189,7 +189,7 @@ Section Misc.
     - induction k.
 
       + replace (& (wones (S n))) with (2 * (& (wones n)) + N.b2n true)%N
-          by (simpl; nomega).
+          by (simpl; rewrite ?N.succ_double_spec; simpl; nomega).
         rewrite N.testbit_0_r.
         reflexivity.
 
@@ -203,12 +203,12 @@ Section Misc.
           try rewrite Pos.succ_pred_double;
           intuition).
         replace (& (wones (S n))) with (2 * (& (wones n)) + N.b2n true)%N
-          by (simpl; nomega).
+          by (simpl; rewrite ?N.succ_double_spec; simpl; nomega).
         rewrite N.testbit_succ_r.
         assumption.
   Qed.
 
-  
+
   Lemma plus_le: forall {n} (x y: word n),
     (& (x ^+ y) <= &x + &y)%N.
   Proof.
@@ -329,7 +329,7 @@ Section Exp.
       rewrite <- IHn.
       simpl; intuition.
   Qed.
- 
+
   Lemma Npow2_succ: forall n, (Npow2 (S n) = 2 * (Npow2 n))%N.
   Proof. intros; simpl; induction (Npow2 n); intuition. Qed.
 
@@ -454,12 +454,7 @@ Section SpecialFunctions.
        with (N.double (& (wtl x)))
          by (induction (& (wtl x)); simpl; intuition).
 
-    - rewrite N.double_spec.
-      replace (N.succ (2 * & wtl x))
-         with ((2 * (& wtl x)) + 1)%N
-           by nomega.
-      rewrite <- N.succ_double_spec.
-      rewrite N.div2_succ_double.
+    - rewrite N.div2_succ_double.
       reflexivity.
 
     - induction (& (wtl x)); simpl; intuition.
@@ -504,11 +499,13 @@ Section SpecialFunctions.
       induction k'.
 
       + clear IHn; induction x; simpl; intuition.
-        destruct (& x), b; simpl; intuition. 
+        destruct (& x), b; simpl; intuition.
 
       + clear IHk'.
         shatter x; simpl.
 
+        rewrite N.succ_double_spec; simpl.
+
         rewrite kill_match.
         replace (N.pos (Pos.of_succ_nat k'))
            with (N.succ (N.of_nat k'))
@@ -531,7 +528,7 @@ Section SpecialFunctions.
           rewrite Nat2N.id;
           reflexivity.
   Qed.
- 
+
   Lemma wordToN_split1: forall {n m} x,
     & (@split1 n m x) = N.land (& x) (& (wones n)).
   Proof.
@@ -620,7 +617,7 @@ Section SpecialFunctions.
       rewrite N.shiftr_spec; try apply N_ge_0.
       replace (k - N.of_nat n + N.of_nat n)%N with k by nomega.
       rewrite N.land_spec.
-      induction (N.testbit x k); 
+      induction (N.testbit x k);
         replace (N.testbit (& wones n) k) with false;
         simpl; intuition;
         try apply testbit_wones_false;
@@ -643,7 +640,7 @@ Section SpecialFunctions.
 
     - rewrite Nat2N.inj_succ.
       replace (& wones (S x)) with (2 * & (wones x) + N.b2n true)%N
-        by (simpl; nomega).
+        by (simpl; rewrite ?N.succ_double_spec; simpl; nomega).
       replace (N.ones (N.succ _))
          with (2 * N.ones (N.of_nat x) + N.b2n true)%N.
 
@@ -729,7 +726,7 @@ Section SpecialFunctions.
     - propagate_wordToN.
       rewrite N2Nat.id.
       reflexivity.
-    
+
     - rewrite N.land_ones.
       rewrite N.mod_small; try reflexivity.
       rewrite <- (N2Nat.id m).
@@ -977,4 +974,3 @@ Section TopLevel.
 
   Close Scope nword_scope.
 End TopLevel.
-