Replace curve-specific definitions with tactics

This requires Coq >= 8.7

After     | File Name                                          | Before    || Change
---------------------------------------------------------------------------------------
11m15.52s | Total                                              | 11m14.53s || +0m00.99s
---------------------------------------------------------------------------------------
0m31.11s  | Specific/X25519/C32/Synthesis                      |    N/A    || +0m31.10s
   N/A    | Specific/X25519/C32/ArithmeticSynthesisTest        | 0m30.80s  || -0m30.80s
0m09.61s  | Specific/X25519/C64/Synthesis                      |    N/A    || +0m09.60s
   N/A    | Specific/X25519/C64/ArithmeticSynthesisTest        | 0m08.56s  || -0m08.56s
1m54.56s  | Specific/X25519/C64/ladderstep                     | 1m56.56s  || -0m02.00s
1m21.50s  | Specific/IntegrationTestKaratsubaMul               | 1m22.98s  || -0m01.48s
1m15.96s  | Specific/IntegrationTestLadderstep130              | 1m14.08s  || +0m01.88s
0m51.80s  | Specific/X25519/C32/femul                          | 0m53.79s  || -0m01.99s
1m51.81s  | Specific/NISTP256/AMD64/femul                      | 1m51.27s  || +0m00.53s
0m28.68s  | Specific/X25519/C32/fesquare                       | 0m28.30s  || +0m00.37s
0m25.45s  | Specific/IntegrationTestMontgomeryP256_128         | 0m25.60s  || -0m00.15s
0m18.81s  | Specific/NISTP256/AMD64/fesub                      | 0m18.32s  || +0m00.48s
0m16.01s  | Specific/NISTP256/AMD64/feadd                      | 0m15.86s  || +0m00.15s
0m15.15s  | Specific/NISTP256/AMD64/feopp                      | 0m14.95s  || +0m00.20s
0m12.42s  | Specific/IntegrationTestMontgomeryP256_128_Sub     | 0m12.15s  || +0m00.26s
0m12.41s  | Specific/IntegrationTestMontgomeryP256_128_Add     | 0m12.31s  || +0m00.09s
0m11.10s  | Specific/IntegrationTestMontgomeryP256_128_Opp     | 0m11.31s  || -0m00.21s
0m10.70s  | Specific/X25519/C64/femul                          | 0m10.17s  || +0m00.52s
0m09.94s  | Specific/NISTP256/AMD64/fenz                       | 0m09.94s  || +0m00.00s
0m09.37s  | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.36s  || +0m00.00s
0m08.78s  | Specific/IntegrationTestSub                        | 0m08.84s  || -0m00.06s
0m07.98s  | Specific/IntegrationTestFreeze                     | 0m08.12s  || -0m00.13s
0m07.42s  | Specific/X25519/C64/fesquare                       | 0m07.22s  || +0m00.20s
0m00.99s  | Specific/SynthesisFramework                        |    N/A    || +0m00.99s
0m00.88s  | Specific/ReificationTypes                          | 0m00.91s  || -0m00.03s
0m00.85s  | Specific/ArithmeticSynthesisFramework              |    N/A    || +0m00.85s
   N/A    | Specific/X25519/C32/ReificationTypes               | 0m00.82s  || -0m00.82s
   N/A    | Specific/X25519/C64/ReificationTypes               | 0m00.77s  || -0m00.77s
0m00.77s  | Specific/IntegrationTestTemporaryMiscCommon        | 0m00.79s  || -0m00.02s
0m00.72s  | Specific/LadderstepSynthesisFramework              |    N/A    || +0m00.72s
0m00.38s  | Specific/IntegrationTestDisplayCommon              | 0m00.40s  || -0m00.02s
0m00.36s  | Specific/IntegrationTestDisplayCommonTactics       | 0m00.35s  || +0m00.01s

1 files changed, 5 insertions, 4 deletions

diff --git a/_CoqProject b/_CoqProject
index 3f2d895f5..afeab0c02 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -228,6 +228,7 @@ src/Spec/MontgomeryCurve.v
 src/Spec/MxDH.v
 src/Spec/WeierstrassCurve.v
 src/Spec/Test/X25519.v
+src/Specific/ArithmeticSynthesisFramework.v
 src/Specific/ArithmeticSynthesisTest130.v
 src/Specific/CurveParameters.v
 src/Specific/IntegrationTestDisplayCommon.v
@@ -252,8 +253,10 @@ src/Specific/IntegrationTestSub.v
 src/Specific/IntegrationTestSubDisplay.v
 src/Specific/IntegrationTestTemporaryMiscCommon.v
 src/Specific/Karatsuba.v
+src/Specific/LadderstepSynthesisFramework.v
 src/Specific/MontgomeryP256_128.v
 src/Specific/ReificationTypes.v
+src/Specific/SynthesisFramework.v
 src/Specific/NISTP256/AMD64/MontgomeryP256.v
 src/Specific/NISTP256/AMD64/feadd.v
 src/Specific/NISTP256/AMD64/feaddDisplay.v
@@ -268,16 +271,14 @@ 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/Synthesis.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/Synthesis.v
 src/Specific/X25519/C64/femul.v
 src/Specific/X25519/C64/femulDisplay.v
 src/Specific/X25519/C64/fesquare.v