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

1 files changed, 20 insertions, 69 deletions

diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v
index 18cee5114..ebfab0c69 100644
--- a/src/Specific/IntegrationTestFreeze.v
+++ b/src/Specific/IntegrationTestFreeze.v
@@ -1,74 +1,27 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
+Require Import Crypto.Specific.X25519.C64.ReificationTypes.
+Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Specific.ArithmeticSynthesisTest.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Tactics.MoveLetIn.
-Require Import Crypto.Util.Tactics.DestructHead.
-Import ListNotations.
-
+Require Import Crypto.Util.BoundedWord.
 Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
-
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
 
-Section BoundedField25p5.
-  Local Coercion Z.of_nat : nat >-> Z.
-
-  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
-  Let length_lw := Eval compute in List.length limb_widths.
+Local Definition phi : feBW -> F m :=
+  fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
 
-  Local Notation b_of exp := {| lower := 0 ; upper := 2^exp + 2^(exp-3) |}%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
-  (* The definition [bounds_exp] is a tuple-version of the
-     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
-     the approximate base-2 exponent of the bounds on the limb in that
-     position. *)
-  Let bounds_exp : Tuple.tuple Z length_lw
-    := Eval compute in
-        Tuple.from_list length_lw limb_widths eq_refl.
-  Let bounds : Tuple.tuple zrange length_lw
-    := Eval compute in
-        Tuple.map (fun e => b_of e) bounds_exp.
-
-  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
-  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
-  Let feZ : Type := tuple Z sz.
-  Let feW : Type := tuple (wordT lgbitwidth) sz.
-  Let feBW : Type := BoundedWord sz bitwidth bounds.
-  Let phi : feBW -> F m :=
-    fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
-  Lemma feBW_bounded (a : feBW)
-    : 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m.
-  Proof.
-    destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
-    revert H.
-    cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt]; cbn [fst snd].
-    repeat match goal with
-           | [ |- context[wt ?n] ]
-             => let v := (eval compute in (wt n)) in change (wt n) with v
-           end.
-    intro; destruct_head'_and.
-    omega.
-  Qed.
-
-  (* TODO : change this to field once field isomorphism happens *)
-  Definition freeze :
-    { freeze : feBW -> feBW
-    | forall a, phi (freeze a) = phi a }.
-  Proof.
-    start_preglue.
-    do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime.
-    all:fin_preglue.
-    (* jgross start here! *)
-    (*Set Ltac Profiling.*)
-    Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *)
-    (*Show Ltac Profile.*)
-    (* total time:      5.680s
+(* TODO : change this to field once field isomorphism happens *)
+Definition freeze :
+  { freeze : feBW -> feBW
+  | forall a, phi (freeze a) = phi a }.
+Proof.
+  start_preglue.
+  do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime.
+  all:fin_preglue.
+  (* jgross start here! *)
+  (*Set Ltac Profiling.*)
+  Time refine_reflectively_gen P.freeze_allowable_bit_widths anf. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *)
+  (*Show Ltac Profile.*)
+  (* total time:      5.680s
 
  tactic                                   local  total   calls       max
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
@@ -108,7 +61,5 @@ Section BoundedField25p5.
   └Glue.zrange_to_reflective -----------   0.1%   3.3%       1    0.188s
   └Glue.zrange_to_reflective_goal ------   2.0%   2.4%       1    0.136s
 
-*)
-  Time Defined. (* Finished transaction in 3.607 secs (3.607u,0.s) (successful) *)
-
-End BoundedField25p5.
+   *)
+Time Defined. (* Finished transaction in 3.607 secs (3.607u,0.s) (successful) *)