aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-10-02 13:43:58 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2017-10-07 00:05:30 -0400
commit76965f85cf742fb2fe9f75d7187da135fbd0eb57 (patch)
treece70e889b85c16ca3e00cb9311bb0fbab72117cf /_CoqProject
parentd7bc99e533f12c11e9e83ea9cec9300bf420caeb (diff)
Factor out parameter-specific code
After | File Name | Before || Change ------------------------------------------------------------------------------ 6m08.27s | Total | 6m25.95s || -0m17.68s ------------------------------------------------------------------------------ N/A | Specific/ArithmeticSynthesisTest32 | 0m39.62s || -0m39.61s 0m38.34s | Specific/X25519/C32/ArithmeticSynthesisTest | N/A || +0m38.34s 0m20.46s | Specific/X25519/C32/ReificationTypes | N/A || +0m20.46s 2m31.97s | Specific/X25519/C64/ladderstep | 2m51.10s || -0m19.12s N/A | Specific/ArithmeticSynthesisTest | 0m09.54s || -0m09.53s 0m09.50s | Specific/X25519/C64/ArithmeticSynthesisTest | N/A || +0m09.50s 1m03.72s | Specific/X25519/C32/femul | 1m11.22s || -0m07.50s 0m10.44s | Specific/IntegrationTestFreeze | 0m17.29s || -0m06.84s 0m34.55s | Specific/X25519/C32/fesquare | 0m40.47s || -0m05.92s 0m05.50s | Specific/X25519/C64/ReificationTypes | N/A || +0m05.50s 0m12.47s | Specific/X25519/C64/femul | 0m13.98s || -0m01.50s 0m08.93s | Specific/X25519/C64/fesquare | 0m10.67s || -0m01.74s 0m11.14s | Specific/IntegrationTestSub | 0m12.06s || -0m00.92s 0m00.50s | Specific/X25519/C32/CurveParameters | N/A || +0m00.50s 0m00.38s | Specific/CurveParameters | N/A || +0m00.38s 0m00.37s | Specific/X25519/C64/CurveParameters | N/A || +0m00.37s
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject9
1 files changed, 7 insertions, 2 deletions
diff --git a/_CoqProject b/_CoqProject
index 0adfec1b9..56eeb51ff 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -222,9 +222,8 @@ src/Spec/MontgomeryCurve.v
src/Spec/MxDH.v
src/Spec/WeierstrassCurve.v
src/Spec/Test/X25519.v
-src/Specific/ArithmeticSynthesisTest.v
src/Specific/ArithmeticSynthesisTest130.v
-src/Specific/ArithmeticSynthesisTest32.v
+src/Specific/CurveParameters.v
src/Specific/IntegrationTestDisplayCommon.v
src/Specific/IntegrationTestDisplayCommonTactics.v
src/Specific/IntegrationTestFreeze.v
@@ -262,10 +261,16 @@ src/Specific/NISTP256/AMD64/fesubDisplay.v
src/Specific/NISTP256/FancyMachine256/Barrett.v
src/Specific/NISTP256/FancyMachine256/Core.v
src/Specific/NISTP256/FancyMachine256/Montgomery.v
+src/Specific/X25519/C32/ArithmeticSynthesisTest.v
+src/Specific/X25519/C32/CurveParameters.v
+src/Specific/X25519/C32/ReificationTypes.v
src/Specific/X25519/C32/femul.v
src/Specific/X25519/C32/femulDisplay.v
src/Specific/X25519/C32/fesquare.v
src/Specific/X25519/C32/fesquareDisplay.v
+src/Specific/X25519/C64/ArithmeticSynthesisTest.v
+src/Specific/X25519/C64/CurveParameters.v
+src/Specific/X25519/C64/ReificationTypes.v
src/Specific/X25519/C64/femul.v
src/Specific/X25519/C64/femulDisplay.v
src/Specific/X25519/C64/fesquare.v