From 6fb3a24a3600a588f63ef57850c5468e446b9fb5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 31 Oct 2016 02:41:14 -0400 Subject: 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 --- Bedrock/Word.v | 10 ++++++---- src/Assembly/WordizeUtil.v | 32 ++++++++++++++------------------ 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. - -- cgit v1.2.3