Support p256 / montgomery in json format

Extra time comes from adding AMD128 to NISTP256, mostly.

After     | File Name                                                | Before    || Change
---------------------------------------------------------------------------------------------
13m25.13s | Total                                                    | 13m30.82s || -0m05.69s
---------------------------------------------------------------------------------------------
   N/A    | Specific/IntegrationTestMontgomeryP256_128               | 0m25.42s  || -0m25.42s
0m22.75s  | Specific/NISTP256/AMD128/femul                           |    N/A    || +0m22.75s
1m31.64s  | Specific/NISTP256/AMD64/femul                            | 1m52.42s  || -0m20.78s
0m14.46s  | Specific/NISTP256/AMD128/fesub                           |    N/A    || +0m14.46s
0m14.25s  | Specific/NISTP256/AMD128/feadd                           |    N/A    || +0m14.25s
0m14.12s  | Specific/NISTP256/AMD128/fenz                            |    N/A    || +0m14.11s
   N/A    | Specific/NISTP256/AMD64/MontgomeryP256                   | 0m13.00s  || -0m13.00s
   N/A    | Specific/IntegrationTestMontgomeryP256_128_Sub           | 0m12.40s  || -0m12.40s
   N/A    | Specific/IntegrationTestMontgomeryP256_128_Add           | 0m11.99s  || -0m11.99s
0m11.74s  | Specific/NISTP256/AMD128/feopp                           |    N/A    || +0m11.74s
   N/A    | Specific/IntegrationTestMontgomeryP256_128_Opp           | 0m11.22s  || -0m11.22s
   N/A    | Specific/IntegrationTestMontgomeryP256_128_Nonzero       | 0m09.27s  || -0m09.26s
   N/A    | Specific/MontgomeryP256_128                              | 0m09.26s  || -0m09.25s
0m08.42s  | Specific/NISTP256/AMD64/Synthesis                        |    N/A    || +0m08.41s
0m14.67s  | Specific/NISTP256/AMD64/fenz                             | 0m09.98s  || +0m04.68s
0m04.12s  | Specific/Framework/ArithmeticSynthesis/Montgomery        |    N/A    || +0m04.12s
0m03.58s  | Specific/NISTP256/AMD128/Synthesis                       |    N/A    || +0m03.58s
1m10.78s  | Specific/X2555/C128/ladderstep                           | 1m08.36s  || +0m02.42s
1m02.10s  | Specific/X25519/C32/femul                                | 1m00.59s  || +0m01.50s
0m43.59s  | Specific/X2448/Karatsuba/C64/Synthesis                   | 0m44.86s  || -0m01.26s
0m34.97s  | Specific/X25519/C32/fesquare                             | 0m35.98s  || -0m01.00s
0m20.10s  | Specific/NISTP256/AMD64/fesub                            | 0m18.37s  || +0m01.73s
0m17.61s  | Specific/NISTP256/AMD64/feadd                            | 0m15.94s  || +0m01.67s
2m09.77s  | Specific/X25519/C64/ladderstep                           | 2m09.79s  || -0m00.01s
1m11.70s  | Specific/X2448/Karatsuba/C64/femul                       | 1m11.60s  || +0m00.10s
0m32.14s  | Specific/X25519/C32/Synthesis                            | 0m31.70s  || +0m00.44s
0m27.94s  | Specific/X25519/C32/freeze                               | 0m28.06s  || -0m00.11s
0m17.62s  | Specific/X25519/C64/femul                                | 0m17.41s  || +0m00.21s
0m15.21s  | Specific/X25519/C64/freeze                               | 0m14.74s  || +0m00.47s
0m14.86s  | Specific/NISTP256/AMD64/feopp                            | 0m14.96s  || -0m00.10s
0m14.58s  | Specific/X25519/C64/fesquare                             | 0m14.06s  || +0m00.51s
0m10.10s  | Specific/X25519/C64/Synthesis                            | 0m09.78s  || +0m00.32s
0m06.22s  | Specific/X2555/C128/Synthesis                            | 0m06.17s  || +0m00.04s
0m01.01s  | Specific/X25519/C32/CurveParameters                      | 0m01.05s  || -0m00.04s
0m00.99s  | Specific/Framework/SynthesisFramework                    | 0m01.08s  || -0m00.09s
0m00.79s  | Specific/Framework/MontgomeryReificationTypes            |    N/A    || +0m00.79s
0m00.78s  | Specific/Framework/ArithmeticSynthesis/SquareFromMul     | 0m00.70s  || +0m00.08s
0m00.78s  | Specific/Framework/ArithmeticSynthesis/Karatsuba         | 0m00.75s  || +0m00.03s
0m00.76s  | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage |    N/A    || +0m00.76s
0m00.75s  | Specific/Framework/IntegrationTestTemporaryMiscCommon    | 0m00.80s  || -0m00.05s
0m00.75s  | Specific/Framework/MontgomeryReificationTypesPackage     |    N/A    || +0m00.75s
0m00.73s  | Specific/Framework/ArithmeticSynthesis/Defaults          | 0m00.75s  || -0m00.02s
0m00.72s  | Specific/Framework/ReificationTypesPackage               | 0m00.70s  || +0m00.02s
0m00.72s  | Specific/Framework/ArithmeticSynthesis/Base              | 0m00.73s  || -0m00.01s
0m00.72s  | Specific/Framework/ArithmeticSynthesis/BasePackage       | 0m00.69s  || +0m00.03s
0m00.72s  | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.76s  || -0m00.04s
0m00.70s  | Specific/Framework/ArithmeticSynthesis/Freeze            | 0m00.75s  || -0m00.05s
0m00.70s  | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage  | 0m00.77s  || -0m00.07s
0m00.69s  | Specific/Framework/ArithmeticSynthesis/DefaultsPackage   | 0m00.71s  || -0m00.02s
0m00.67s  | Specific/Framework/ArithmeticSynthesis/FreezePackage     | 0m00.74s  || -0m00.06s
0m00.43s  | Specific/X25519/C64/CurveParameters                      | 0m00.43s  || +0m00.00s
0m00.38s  | Specific/Framework/IntegrationTestDisplayCommon          | 0m00.40s  || -0m00.02s
0m00.38s  | Specific/Framework/IntegrationTestDisplayCommonTactics   | 0m00.37s  || +0m00.01s
0m00.34s  | Specific/Framework/CurveParameters                       | 0m00.32s  || +0m00.02s
0m00.33s  | Specific/X2555/C128/CurveParameters                      | 0m00.33s  || +0m00.00s
0m00.32s  | Specific/NISTP256/AMD128/CurveParameters                 |    N/A    || +0m00.32s
0m00.32s  | Specific/X2448/Karatsuba/C64/CurveParameters             | 0m00.33s  || -0m00.01s
0m00.31s  | Specific/Framework/CurveParametersPackage                | 0m00.33s  || -0m00.02s
0m00.30s  | Specific/NISTP256/AMD64/CurveParameters                  |    N/A    || +0m00.30s

1 files changed, 11 insertions, 109 deletions

diff --git a/src/Specific/NISTP256/AMD64/fenz.v b/src/Specific/NISTP256/AMD64/fenz.v
index 13dc4478f..8b61924a7 100644
--- a/src/Specific/NISTP256/AMD64/fenz.v
+++ b/src/Specific/NISTP256/AMD64/fenz.v
@@ -1,114 +1,16 @@
 Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
-Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
-Require Import Crypto.Arithmetic.Core. Import B.
-Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
-Require Import Crypto.Arithmetic.Saturated.UniformWeight.
-Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256.
 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.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Import ListNotations.
-
-Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon.
-
-Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-
-Section BoundedField25p5.
-  Local Coercion Z.of_nat : nat >-> Z.
-
-  Let bound1 : zrange
-    := Eval compute in
-        {| lower := 0 ; upper := r-1 |}.
-  Let bounds : Tuple.tuple zrange sz
-    := Eval compute in
-        Tuple.repeat bound1 sz.
-
-  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))).
-  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 eval : feBW -> Z :=
-    fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
-  Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
-  Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
-  Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
-  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.
-    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 _) ]
-      => cut (x <-> y);
-           [ destruct (Decidable.dec x), (Decidable.dec y); try reflexivity; intros [? ?];
-             generalize dependent x; generalize dependent y; solve [ intuition congruence ]
-           | ]
-    end.
-    etransitivity; [ | eapply (proj2_sig nonzero) ];
-      [ | 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) _).
-    { intros a' H'; rewrite H'.
-      let H := fresh in
-      lazymatch goal with |- context[Decidable.dec ?x] => destruct (Decidable.dec x) as [H|H]; try rewrite H end.
-      { reflexivity. }
-      { let H := fresh in
-        lazymatch goal with |- context[?x =? 0] => destruct (x =? 0) eqn:? end;
-          try reflexivity.
-        Z.ltb_to_lt; congruence. } }
-    eexists_sig_etransitivity.
-    do_set_sig nonzero.
-    cbv_runtime.
-    reflexivity.
-    sig_dlet_in_rhs_to_context.
-    cbv [proj1_sig].
-    match goal with
-    | [ H : feBW_small |- _ ] => destruct H as [? _]
-    end.
-    (* jgross start here! *)
-    Set Ltac Profiling.
-    (*     Set Ltac Profiling.
-    Print Ltac ReflectiveTactics.solve_side_conditions.
-    Ltac ReflectiveTactics.solve_side_conditions ::= idtac.
-    Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *)
-    { Time ReflectiveTactics.do_reify. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Require Import CNotations.
-      Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
-    { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. }
-  { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. }
-  { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. }
-  { Time SubstLet.subst_let; clear; vm_compute; reflexivity. }
-  { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. }
-  { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. }
-  { Time abstract ReflectiveTactics.handle_bounds_from_hyps. }
-  { Time ReflectiveTactics.handle_boundedness_side_condition. } *)
-    Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *)
-    Show Ltac Profile.
-  Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *)
+Require Import Crypto.Specific.NISTP256.AMD64.Synthesis.
+Local Open Scope Z_scope.
 
-Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *)
+(* TODO : change this to field once field isomorphism happens *)
+Definition nonzero :
+  { nonzero : feBW_small -> BoundedWord.BoundedWord 1 adjusted_bitwidth bound1
+  | forall a, (BoundedWord.BoundedWordToZ _ _ _ (nonzero a) =? 0) = (if Decidable.dec (phiM_small a = F.of_Z m 0) then true else false) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_nonzero ().
+  Show Ltac Profile.
+Time Defined.
 
 Print Assumptions nonzero.