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, 56 deletions

diff --git a/src/Specific/X25519/C64/fesquare.v b/src/Specific/X25519/C64/fesquare.v
index 6be0713b6..cfad2d111 100644
--- a/src/Specific/X25519/C64/fesquare.v
+++ b/src/Specific/X25519/C64/fesquare.v
@@ -1,63 +1,12 @@
-Require Import Crypto.Specific.X25519.C64.ReificationTypes.
-Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest.
-Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.BoundedWord.
-Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
-Require Import Crypto.Compilers.Z.Bounds.Pipeline.
+Require Import Crypto.Specific.X25519.C64.Synthesis.
 
 (* TODO : change this to field once field isomorphism happens *)
 Definition square :
   { square : feBW -> feBW
   | forall a, phiBW (square a) = F.mul (phiBW a) (phiBW a) }.
 Proof.
-  start_preglue.
-  do_rewrite_with_1sig_add_carry square_sig carry_sig; cbv_runtime.
-  all:fin_preglue.
-  (* jgross start here! *)
-  (*Set Ltac Profiling.*)
-  Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
-  (*Show Ltac Profile.*)
-  (* total time:     19.632s
-
- tactic                                   local  total   calls       max
-────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─refine_reflectively -------------------   0.0%  98.4%       1   19.320s
-─ReflectiveTactics.do_reflective_pipelin  -0.0%  96.2%       1   18.884s
-─ReflectiveTactics.solve_side_conditions   1.2%  96.1%       1   18.860s
-─ReflectiveTactics.do_reify ------------  27.7%  44.0%       1    8.640s
-─ReflectiveTactics.abstract_vm_compute_r  12.3%  13.9%       2    2.024s
-─ReflectiveTactics.abstract_vm_compute_r   8.9%  12.2%       2    1.576s
-─Reify_rhs_gen -------------------------   0.8%  11.7%       1    2.300s
-─ReflectiveTactics.renamify_rhs --------  10.4%  11.5%       1    2.260s
-─ReflectiveTactics.abstract_rhs --------   4.6%   5.8%       1    1.148s
-─clear (var_list) ----------------------   5.2%   5.2%      57    0.184s
-─eexact --------------------------------   4.1%   4.1%      68    0.028s
-─prove_interp_compile_correct ----------   0.0%   3.4%       1    0.664s
-─ReflectiveTactics.abstract_cbv_interp_r   2.7%   3.3%       1    0.648s
-─unify (constr) (constr) ---------------   3.2%   3.2%       6    0.248s
-─rewrite ?EtaInterp.InterpExprEta ------   3.1%   3.1%       1    0.612s
-─ReflectiveTactics.abstract_cbv_rhs ----   2.0%   2.7%       1    0.532s
-─Glue.refine_to_reflective_glue --------   0.0%   2.2%       1    0.436s
-─rewrite H -----------------------------   2.1%   2.1%       1    0.420s
-
- tactic                                   local  total   calls       max
-────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─refine_reflectively -------------------   0.0%  98.4%       1   19.320s
- ├─ReflectiveTactics.do_reflective_pipel  -0.0%  96.2%       1   18.884s
- │└ReflectiveTactics.solve_side_conditio   1.2%  96.1%       1   18.860s
- │ ├─ReflectiveTactics.do_reify --------  27.7%  44.0%       1    8.640s
- │ │ ├─Reify_rhs_gen -------------------   0.8%  11.7%       1    2.300s
- │ │ │ ├─prove_interp_compile_correct --   0.0%   3.4%       1    0.664s
- │ │ │ │└rewrite ?EtaInterp.InterpExprEt   3.1%   3.1%       1    0.612s
- │ │ │ └─rewrite H ---------------------   2.1%   2.1%       1    0.420s
- │ │ └─eexact --------------------------   4.1%   4.1%      68    0.028s
- │ ├─ReflectiveTactics.abstract_vm_compu  12.3%  13.9%       2    2.024s
- │ ├─ReflectiveTactics.abstract_vm_compu   8.9%  12.2%       2    1.576s
- │ ├─ReflectiveTactics.renamify_rhs ----  10.4%  11.5%       1    2.260s
- │ ├─ReflectiveTactics.abstract_rhs ----   4.6%   5.8%       1    1.148s
- │ ├─ReflectiveTactics.abstract_cbv_inte   2.7%   3.3%       1    0.648s
- │ └─ReflectiveTactics.abstract_cbv_rhs    2.0%   2.7%       1    0.532s
- └─Glue.refine_to_reflective_glue ------   0.0%   2.2%       1    0.436s
-   *)
-Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
+  Set Ltac Profiling.
+  Time synthesize_square ().
+  Show Ltac Profile.
+Time Defined.