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, 0 insertions, 438 deletions

diff --git a/src/Specific/NISTP256/AMD64/MontgomeryP256.v b/src/Specific/NISTP256/AMD64/MontgomeryP256.v
deleted file mode 100644
index e8b25a781..000000000
--- a/src/Specific/NISTP256/AMD64/MontgomeryP256.v
+++ /dev/null
@@ -1,438 +0,0 @@
-Require Import Coq.micromega.Lia.
-Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
-Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Proofs.
-Require Import Crypto.Arithmetic.Core. Import B.
-Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
-Require Import Crypto.Arithmetic.Saturated.UniformWeight.
-Require Import Crypto.Util.Sigma.Lift.
-Require Import Coq.ZArith.BinInt.
-Require Import Coq.PArith.BinPos.
-Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.ZUtil.ModInv.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.Tactics.DestructHead.
-Require Import Crypto.Util.Tactics.BreakMatch.
-
-Definition wt (i:nat) : Z := Z.shiftl 1 (64*Z.of_nat i).
-Definition r := Eval compute in (2^64)%positive.
-Definition sz := 4%nat.
-Definition m : positive := 2^256-2^224+2^192+2^96-1.
-Definition p256 :=
-  Eval vm_compute in
-    ((Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (Z.pos m))).
-Definition r' := Eval vm_compute in Zpow_facts.Zpow_mod (Z.pos r) (Z.pos m - 2) (Z.pos m).
-Definition r'_correct := eq_refl : ((Z.pos r * r') mod (Z.pos m) = 1)%Z.
-Definition m' : Z := Eval vm_compute in Option.invert_Some (Z.modinv_fueled 10 (-Z.pos m) (Z.pos r)).
-Definition m'_correct := eq_refl : ((Z.pos m * m') mod (Z.pos r) = (-1) mod Z.pos r)%Z.
-Definition m_p256 := eq_refl (Z.pos m) <: Z.pos m = MontgomeryAPI.eval (n:=sz) (Z.pos r) p256.
-
-Lemma r'_pow_correct : ((r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 = 1)%Z.
-Proof. vm_compute; reflexivity. Qed.
-
-Definition mulmod_256' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                        | forall (A B : Tuple.tuple Z sz),
-                               f A B =
-                               (redc (r:=r)(R_numlimbs:=sz) p256 A B m')
-                            }.
-Proof.
-  eapply (lift2_sig (fun A B c => c = _)); eexists.
-  cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In].
-  (*
-  cbv [
-      r wt sz p256
-        CPSUtil.Tuple.tl_cps CPSUtil.Tuple.hd_cps
-       CPSUtil.to_list_cps CPSUtil.to_list'_cps CPSUtil.to_list_cps' CPSUtil.flat_map_cps CPSUtil.fold_right_cps
-       CPSUtil.map_cps CPSUtil.Tuple.left_append_cps CPSUtil.firstn_cps CPSUtil.combine_cps CPSUtil.on_tuple_cps CPSUtil.update_nth_cps CPSUtil.from_list_default_cps CPSUtil.from_list_default'_cps
-       fst snd length List.seq List.hd List.app
-       redc redc_cps redc_loop_cps redc_body_cps
-       Positional.to_associational_cps
-       MontgomeryAPI.divmod_cps
-       MontgomeryAPI.scmul_cps
-       uweight
-       MontgomeryAPI.Columns.mul_cps
-       MontgomeryAPI.Associational.mul_cps
-       (*Z.of_nat Pos.of_succ_nat  Nat.pred
-       Z.pow Z.pow_pos Z.mul Pos.iter Pos.mul Pos.succ*)
-       Tuple.hd Tuple.append Tuple.tl Tuple.hd' Tuple.tl' CPSUtil.Tuple.left_tl_cps CPSUtil.Tuple.left_hd_cps CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps
-       MontgomeryAPI.Columns.from_associational_cps
-       MontgomeryAPI.Associational.multerm_cps
-       MontgomeryAPI.Columns.compact_cps
-       MontgomeryAPI.Columns.compact_step_cps
-       MontgomeryAPI.Columns.compact_digit_cps
-       MontgomeryAPI.drop_high_cps
-       MontgomeryAPI.add_cps
-       MontgomeryAPI.Columns.add_cps
-       MontgomeryAPI.Columns.cons_to_nth_cps
-       Nat.pred
-       MontgomeryAPI.join0
-       MontgomeryAPI.join0_cps CPSUtil.Tuple.left_append_cps
-       CPSUtil.Tuple.mapi_with_cps
-       id
-       Positional.zeros MontgomeryAPI.zero MontgomeryAPI.Columns.nils Tuple.repeat Tuple.append
-       Positional.place_cps
-       CPSUtil.Tuple.mapi_with'_cps Tuple.hd Tuple.hd' Tuple.tl Tuple.tl' CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps fst snd
-       Z.of_nat fst snd Z.pow Z.pow_pos Pos.of_succ_nat Z.div Z.mul Pos.mul Z.modulo Z.div_eucl Z.pos_div_eucl Z.leb Z.compare Pos.compare_cont Pos.compare Z.pow_pos Pos.iter Z.mul Pos.succ Z.ltb Z.gtb Z.geb Z.div Z.sub Z.pos_sub Z.add Z.opp Z.double
-       Decidable.dec Decidable.dec_eq_Z Z.eq_dec Z_rec Z_rec Z_rect
-       Positional.zeros MontgomeryAPI.zero MontgomeryAPI.Columns.nils Tuple.repeat Tuple.append
-       (*
-       MontgomeryAPI.Associational.multerm_cps
-       MontgomeryAPI.Columns.from_associational_cps Positional.place_cps MontgomeryAPI.Columns.cons_to_nth_cps MontgomeryAPI.Columns.nils
-Tuple.append
-Tuple.from_list Tuple.from_list'
-Tuple.from_list_default Tuple.from_list_default'
-Tuple.hd
-Tuple.repeat
-Tuple.tl
-Tuple.tuple *)
-       (* MontgomeryAPI.add_cps MontgomeryAPI.divmod_cps MontgomeryAPI.drop_high_cps MontgomeryAPI.scmul_cps MontgomeryAPI.zero MontgomeryAPI.Columns.mul_cps MontgomeryAPI.Columns.add_cps uweight MontgomeryAPI.T *)
-            (*
-            CPSUtil.to_list_cps CPSUtil.to_list'_cps CPSUtil.to_list_cps'
-Positional.zeros
-Tuple.to_list
-Tuple.to_list'
-List.hd
-List.tl
-Nat.max
-Positional.to_associational_cps
-Z.of_nat *)
-    ].
-  Unset Printing Notations.
-
-  (* cbv -[runtime_add runtime_mul LetIn.Let_In Definitions.Z.add_get_carry_full Definitions.Z.mul_split]. *)
-
-  (* basesystem_partial_evaluation_RHS. *)
-   *)
-  reflexivity.
-Defined.
-
-
-Definition mulmod_256'' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                        | forall (A B : Tuple.tuple Z sz),
-                            small (Z.pos r) A -> small (Z.pos r) B ->
-                            let eval := MontgomeryAPI.eval (Z.pos r) in
-                            (small (Z.pos r) (f A B)
-                             /\ (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)
-                             /\ (eval (f A B) mod Z.pos m
-                                 = (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z
-                            }.
-Proof.
-  exists (proj1_sig mulmod_256').
-  abstract (
-      intros; rewrite (proj2_sig mulmod_256');
-      split; [ | split ];
-      [ apply small_redc with (ri:=r') | apply redc_bound_N with (ri:=r') | apply redc_mod_N ];
-      try match goal with
-          | _ => assumption
-          | [ |- _ = _ :> Z ] => vm_compute; reflexivity
-          | _ => reflexivity
-          | [ |- small (Z.pos r) p256 ]
-            => hnf; cbv [Tuple.to_list sz p256 r Tuple.to_list' List.In]; intros; destruct_head'_or;
-               subst; try lia
-          | [ |- MontgomeryAPI.eval (Z.pos r) p256 <> 0%Z ]
-            => vm_compute; lia
-          end
-    ).
-Defined.
-
-Definition add' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | forall (A B : Tuple.tuple Z sz),
-                     f A B =
-                     (add (r:=r)(R_numlimbs:=sz) p256 A B)
-                 }.
-Proof.
-  eapply (lift2_sig (fun A B c => c = _)); eexists.
-  cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In].
-  reflexivity.
-Defined.
-
-Definition sub' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | forall (A B : Tuple.tuple Z sz),
-                     f A B =
-                     (sub (r:=r) (R_numlimbs:=sz) p256 A B)
-                 }.
-Proof.
-  eapply (lift2_sig (fun A B c => c = _)); eexists.
-  cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In].
-  reflexivity.
-Defined.
-
-Definition opp' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | forall (A : Tuple.tuple Z sz),
-                     f A =
-                     (opp (r:=r) (R_numlimbs:=sz) p256 A)
-                 }.
-Proof.
-  eapply (lift1_sig (fun A c => c = _)); eexists.
-  cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In].
-  reflexivity.
-Defined.
-
-Definition nonzero' : { f:Tuple.tuple Z sz -> Z
-                      | forall (A : Tuple.tuple Z sz),
-                          f A =
-                          (nonzero (R_numlimbs:=sz) A)
-                      }.
-Proof.
-  eapply (lift1_sig (fun A c => c = _)); eexists.
-  cbv -[runtime_lor Let_In].
-  reflexivity.
-Defined.
-
-Import ModularArithmetic.
-
-(*Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                        | forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                                 (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                            small (Z.pos r) (f A B)
-                            /\ (let eval := MontgomeryAPI.eval (Z.pos r) in
-                                0 <= eval (f A B) < Z.pos r^Z.of_nat sz
-                                /\ (eval (f A B) mod Z.pos m
-                                    = (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z
-                        }.
-Proof.*)
-
-(** TODO: MOVE ME *)
-Definition montgomery_to_F (v : Z) : F m
-  := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F.
-
-
-Definition mulmod_256_ext
-  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-    | let eval := MontgomeryAPI.eval (Z.pos r) in
-      (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-              (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-          montgomery_to_F (eval (f A B))
-          = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F)
-      /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                 (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-             (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }.
-Proof.
-  exists (proj1_sig mulmod_256'').
-  abstract (
-      split; intros A Asm B Bsm;
-      pose proof (proj2_sig mulmod_256'' A B Asm Bsm) as H;
-      cbv zeta in *;
-      try solve [ destruct_head'_and; assumption ];
-      rewrite ModularArithmeticTheorems.F.eq_of_Z_iff in H;
-      unfold montgomery_to_F;
-      destruct H as [H1 [H2 H3]];
-      rewrite H3;
-      rewrite <- !ModularArithmeticTheorems.F.of_Z_mul;
-      f_equal; nia
-    ).
-Defined.
-
-Definition mulmod_256
-  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-    | let eval := MontgomeryAPI.eval (Z.pos r) in
-      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-             (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-        montgomery_to_F (eval (f A B))
-        = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F }.
-Proof.
-  let v := (eval cbv [proj1_sig mulmod_256_ext mulmod_256'' mulmod_256' lift2_sig] in (proj1_sig mulmod_256_ext)) in
-  (exists v).
-  abstract apply (proj2_sig mulmod_256_ext).
-Defined.
-
-Lemma mulmod_256_bounded
-  : let eval := MontgomeryAPI.eval (Z.pos r) in
-    forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-           (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-      (eval B < eval p256 -> 0 <= eval (proj1_sig mulmod_256 A B) < eval p256)%Z.
-Proof. apply (proj2_sig mulmod_256_ext). Qed.
-
-Local Ltac t_fin :=
-  [ > reflexivity
-  | repeat match goal with
-           | _ => assumption
-           | [ |- _ = _ :> Z ] => vm_compute; reflexivity
-           | _ => reflexivity
-           | [ |- small (Z.pos r) p256 ]
-             => hnf; cbv [Tuple.to_list sz p256 r Tuple.to_list' List.In]; intros; destruct_head'_or;
-                subst; try lia
-           | [ |- MontgomeryAPI.eval (Z.pos r) p256 <> 0%Z ]
-             => vm_compute; lia
-           | [ |- and _ _ ] => split
-           | [ |- (0 <= MontgomeryAPI.eval (Z.pos r) _)%Z ] => apply MontgomeryAPI.eval_small
-           end.. ].
-
-Definition add_ext
-  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-    | let eval := MontgomeryAPI.eval (Z.pos r) in
-      ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-           (eval A < eval p256
-            -> eval B < eval p256
-            -> montgomery_to_F (eval (f A B))
-               = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F))
-       /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-              (eval A < eval p256
-               -> eval B < eval p256
-               -> 0 <= eval (f A B) < eval p256)))%Z }.
-Proof.
-  exists (proj1_sig add').
-  abstract (
-      split; intros; rewrite (proj2_sig add');
-      unfold montgomery_to_F; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?ModularArithmeticTheorems.F.of_Z_add;
-      rewrite <- ?Z.mul_add_distr_r;
-      [ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; push_Zmod; rewrite eval_add_mod_N; pull_Zmod
-      | apply add_bound ];
-      t_fin
-    ).
-Defined.
-
-Definition sub_ext
-  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-    | let eval := MontgomeryAPI.eval (Z.pos r) in
-      ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-           (eval A < eval p256
-            -> eval B < eval p256
-            -> montgomery_to_F (eval (f A B))
-               = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F))
-       /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-              (eval A < eval p256
-               -> eval B < eval p256
-               -> 0 <= eval (f A B) < eval p256)))%Z }.
-Proof.
-  exists (proj1_sig sub').
-  abstract (
-      split; intros; rewrite (proj2_sig sub');
-      unfold montgomery_to_F; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?ModularArithmeticTheorems.F.of_Z_sub;
-      rewrite <- ?Z.mul_sub_distr_r;
-      [ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; push_Zmod; rewrite eval_sub_mod_N; pull_Zmod
-      | apply sub_bound ];
-      t_fin
-    ).
-Defined.
-
-Definition opp_ext
-  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
-    | let eval := MontgomeryAPI.eval (Z.pos r) in
-      ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-           (eval A < eval p256
-            -> montgomery_to_F (eval (f A))
-               = (F.opp (montgomery_to_F (eval A)))%F))
-       /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-              (eval A < eval p256
-               -> 0 <= eval (f A) < eval p256)))%Z }.
-Proof.
-  exists (proj1_sig opp').
-  abstract (
-      split; intros; rewrite (proj2_sig opp');
-      unfold montgomery_to_F; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?F_of_Z_opp;
-      rewrite <- ?Z.mul_opp_l;
-      [ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; push_Zmod; rewrite eval_opp_mod_N; pull_Zmod
-      | apply opp_bound ];
-      t_fin
-    ).
-Defined.
-
-Definition nonzero_ext
-  : { f:Tuple.tuple Z sz -> Z
-    | let eval := MontgomeryAPI.eval (Z.pos r) in
-      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-        (eval A < eval p256
-         -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
-Proof.
-  exists (proj1_sig nonzero').
-  abstract (
-      intros eval A H **; rewrite (proj2_sig nonzero'), (@eval_nonzero r) by (eassumption || reflexivity);
-      subst eval;
-      unfold montgomery_to_F, uweight in *; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul;
-      rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256;
-      let H := fresh in
-      split; intro H;
-      [ rewrite H; autorewrite with zsimplify_const; reflexivity
-      | cut ((MontgomeryAPI.eval (Z.pos r) A * (r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz)) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 = 0)%Z;
-        [ rewrite Z.mul_mod, r'_pow_correct; autorewrite with zsimplify_const; pull_Zmod; [ | vm_compute; congruence ];
-          rewrite Z.mod_small; [ trivial | split; try assumption; apply MontgomeryAPI.eval_small; try assumption; lia ]
-        | rewrite Z.mul_assoc, Z.mul_mod, H by (vm_compute; congruence); autorewrite with zsimplify_const; reflexivity ] ]
-    ).
-Defined.
-
-Definition add
-  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-    | let eval := MontgomeryAPI.eval (Z.pos r) in
-      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-             (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-        (eval A < eval p256
-         -> eval B < eval p256
-         -> montgomery_to_F (eval (f A B))
-            = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)%Z }.
-Proof.
-  let v := (eval cbv [proj1_sig add_ext add' lift2_sig] in (proj1_sig add_ext)) in
-  (exists v).
-  abstract apply (proj2_sig add_ext).
-Defined.
-
-Lemma add_bounded
-  : let eval := MontgomeryAPI.eval (Z.pos r) in
-    (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-        (eval A < eval p256
-         -> eval B < eval p256
-         -> 0 <= eval (proj1_sig add A B) < eval p256))%Z.
-Proof. apply (proj2_sig add_ext). Qed.
-
-Definition sub
-  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-    | let eval := MontgomeryAPI.eval (Z.pos r) in
-      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-             (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-        (eval A < eval p256
-         -> eval B < eval p256
-         -> montgomery_to_F (eval (f A B))
-            = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)%Z }.
-Proof.
-  let v := (eval cbv [proj1_sig sub_ext sub' lift2_sig] in (proj1_sig sub_ext)) in
-  (exists v).
-  abstract apply (proj2_sig sub_ext).
-Defined.
-
-Lemma sub_bounded
-  : let eval := MontgomeryAPI.eval (Z.pos r) in
-    (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-        (eval A < eval p256
-         -> eval B < eval p256
-         -> 0 <= eval (proj1_sig sub A B) < eval p256))%Z.
-Proof. apply (proj2_sig sub_ext). Qed.
-
-Definition opp
-  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
-    | let eval := MontgomeryAPI.eval (Z.pos r) in
-      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-        (eval A < eval p256
-         -> montgomery_to_F (eval (f A))
-            = (F.opp (montgomery_to_F (eval A)))%F)%Z }.
-Proof.
-  let v := (eval cbv [proj1_sig opp_ext opp' lift1_sig] in (proj1_sig opp_ext)) in
-  (exists v).
-  abstract apply (proj2_sig opp_ext).
-Defined.
-
-Lemma opp_bounded
-  : let eval := MontgomeryAPI.eval (Z.pos r) in
-    (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-        (eval A < eval p256
-         -> 0 <= eval (proj1_sig opp A) < eval p256))%Z.
-Proof. apply (proj2_sig opp_ext). Qed.
-
-Definition nonzero
-  : { f:Tuple.tuple Z sz -> Z
-    | let eval := MontgomeryAPI.eval (Z.pos r) in
-      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-        (eval A < eval p256
-         -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
-Proof.
-  let v := (eval cbv [proj1_sig nonzero_ext nonzero' lift1_sig] in (proj1_sig nonzero_ext)) in
-  (exists v).
-  abstract apply (proj2_sig nonzero_ext).
-Defined.
-
-Local Definition for_assumptions := (mulmod_256, add, sub, opp, nonzero).
-Print Assumptions for_assumptions.