Factor out some of the preglue synthesis code

This makes it a bit more uniform, and hopefully more automatable and
packageable.  Unfortunately, there's still no spec for this part of the
pipeline, so the tactics simply aggregate common patterns.

Alas, this also makes things a bit slower; I suspect that [Defined] is
the place where things are slower.

After     | File Name                                          | Before    || Change
---------------------------------------------------------------------------------------
13m51.14s | Total                                              | 12m59.29s || +0m51.84s
---------------------------------------------------------------------------------------
1m54.18s  | Specific/IntegrationTestKaratsubaMul               | 1m43.12s  || +0m11.06s
1m38.97s  | Specific/IntegrationTestLadderstep130              | 1m30.26s  || +0m08.70s
2m19.75s  | Specific/NISTP256/AMD64/femul                      | 2m14.08s  || +0m05.66s
0m39.90s  | Specific/IntegrationTestMontgomeryP256_128         | 0m34.21s  || +0m05.68s
0m21.95s  | Specific/NISTP256/AMD64/fesub                      | 0m19.23s  || +0m02.71s
0m21.37s  | Specific/NISTP256/AMD64/feadd                      | 0m18.82s  || +0m02.55s
0m21.02s  | Specific/X25519/C64/femul                          | 0m18.32s  || +0m02.69s
0m20.53s  | Specific/IntegrationTestFreeze                     | 0m23.26s  || -0m02.73s
0m18.28s  | Specific/IntegrationTestMontgomeryP256_128_Sub     | 0m15.32s  || +0m02.96s
0m18.20s  | Specific/IntegrationTestMontgomeryP256_128_Add     | 0m15.52s  || +0m02.67s
0m16.35s  | Specific/IntegrationTestMontgomeryP256_128_Opp     | 0m13.52s  || +0m02.83s
0m13.92s  | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m11.84s  || +0m02.08s
0m18.23s  | Specific/NISTP256/AMD64/MontgomeryP256             | 0m16.62s  || +0m01.60s
0m15.54s  | Specific/IntegrationTestSub                        | 0m14.53s  || +0m01.00s
0m14.78s  | Specific/X25519/C64/fesquare                       | 0m13.13s  || +0m01.64s
0m13.71s  | Specific/NISTP256/AMD64/fenz                       | 0m12.69s  || +0m01.02s
3m14.34s  | Specific/X25519/C64/ladderstep                     | 3m14.32s  || +0m00.02s
0m16.54s  | Specific/NISTP256/AMD64/feopp                      | 0m16.48s  || +0m00.05s
0m12.21s  | Specific/MontgomeryP256_128                        | 0m12.70s  || -0m00.48s
0m00.73s  | Specific/IntegrationTestTemporaryMiscCommon        | 0m00.72s  || +0m00.01s
0m00.64s  | Specific/IntegrationTestDisplayCommon              | 0m00.60s  || +0m00.04s

1 files changed, 8 insertions, 11 deletions

diff --git a/src/Specific/NISTP256/AMD64/fenz.v b/src/Specific/NISTP256/AMD64/fenz.v
index cfea6e957..b46460550 100644
--- a/src/Specific/NISTP256/AMD64/fenz.v
+++ b/src/Specific/NISTP256/AMD64/fenz.v
@@ -44,18 +44,16 @@ Section BoundedField25p5.
   Let phi : feBW -> F m :=
     fun x => montgomery_to_F (eval x).
 
+  Local Ltac op_sig_side_conditions_t _ :=
+    try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption.
+
   (* TODO : change this to field once field isomorphism happens *)
   Definition nonzero
     : { nonzero : feBW_small -> BoundedWord  1 bitwidth bound1
       | forall A, (BoundedWordToZ _ _ _ (nonzero A) =? 0) = (if Decidable.dec (phi A = F.of_Z m 0) then true else false) }.
   Proof.
-    lazymatch goal with
-    | [ |- { f | forall a, (?R (?phi (f a)) ?v) = @?rhs a } ]
-      => apply lift1_sig with (P:=fun a f => R (phi f) v = rhs a)
-    end.
-    intros a.
-    cbv [feBW_of_feBW_small].
-    eexists_sig_etransitivity. all:cbv [phi eval].
+    apply_lift_sig; intros; eexists_sig_etransitivity.
+    all:cbv [feBW_of_feBW_small phi eval].
     refine (_ : (if Decidable.dec (_ = 0) then true else false) = _).
     lazymatch goal with
     | [ |- (if Decidable.dec ?x then _ else _) = (if Decidable.dec ?y then _ else _) ]
@@ -65,7 +63,7 @@ Section BoundedField25p5.
            | ]
     end.
     etransitivity; [ | eapply (proj2_sig nonzero) ];
-      [ | solve [ try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption ].. ].
+      [ | solve [ op_sig_side_conditions_t () ].. ].
     reflexivity.
     let decP := lazymatch goal with |- { c | _ = if Decidable.dec (?decP = 0) then _ else _ } => decP end in
     apply (@proj2_sig_map _ (fun c => BoundedWordToZ 1 _ _ c = decP) _).
@@ -78,9 +76,8 @@ Section BoundedField25p5.
           try reflexivity.
         Z.ltb_to_lt; congruence. } }
     eexists_sig_etransitivity.
-    set (nonzeroZ := proj1_sig nonzero).
-    context_to_dlet_in_rhs nonzeroZ; cbv [nonzeroZ].
-    cbv beta iota delta [nonzero nonzero' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    do_set_sig nonzero.
+    cbv_runtime.
     reflexivity.
     sig_dlet_in_rhs_to_context.
     match goal with