Add 128-bit version of montgomery for testing

4 files changed, 212 insertions, 5 deletions

diff --git a/src/Specific/IntegrationTestMontgomeryP256.v b/src/Specific/IntegrationTestMontgomeryP256.v
index 90aae7723..2fb08fb40 100644
--- a/src/Specific/IntegrationTestMontgomeryP256.v
+++ b/src/Specific/IntegrationTestMontgomeryP256.v
@@ -36,7 +36,7 @@ Section BoundedField25p5.
   Definition mulmod_256 : { f:feBW -> feBW -> feBW
                           | forall A B,
                               BoundedWordToZ _ _ _ (f A B) =
-                              Saturated.drop_high (redc (r:=r)(R_numlimbs:=4) p256 (BoundedWordToZ _ _ _ A) (BoundedWordToZ _ _ _ B) 1)
+                              Saturated.drop_high (redc (r:=r)(R_numlimbs:=sz) p256 (BoundedWordToZ _ _ _ A) (BoundedWordToZ _ _ _ B) 1)
                           }.
   Proof.
     (*Definition mulmod :
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128.v b/src/Specific/IntegrationTestMontgomeryP256_128.v
new file mode 100644
index 000000000..556bf42c4
--- /dev/null
+++ b/src/Specific/IntegrationTestMontgomeryP256_128.v
@@ -0,0 +1,112 @@
+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 Import Crypto.Specific.MontgomeryP256_128.
+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.
+Import ListNotations.
+
+Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
+
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.
+
+Section BoundedField25p5.
+  Local Coercion Z.of_nat : nat >-> Z.
+
+  Let bounds : Tuple.tuple zrange sz
+    := Eval compute in
+        Tuple.repeat {| lower := 0 ; upper := r-1 |} 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 phi : feBW -> F m :=
+    fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
+
+  (* TODO : change this to field once field isomorphism happens *)
+  Definition mulmod_256 : { f:feBW -> feBW -> feBW
+                          | forall A B,
+                              BoundedWordToZ _ _ _ (f A B) =
+                              Saturated.drop_high (redc (r:=r)(R_numlimbs:=sz) p256 (BoundedWordToZ _ _ _ A) (BoundedWordToZ _ _ _ B) 1)
+                          }.
+  Proof.
+    (*Definition mulmod :
+    { mulmod : feBW -> feBW -> feBW
+    | forall a b, phi (mulmod a b) = F.mul (phi a) (phi b) }.
+  Proof.*)
+    lazymatch goal with
+    | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ]
+      => apply lift2_sig with (P:=fun a b f => phi f = rhs a b)
+    end.
+    intros a b.
+    eexists_sig_etransitivity. all:cbv [phi].
+    rewrite <- (proj2_sig mulmod_256).
+    (*symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
+    set (carry_mulZ := fun a b => proj1_sig carry_sig (proj1_sig mul_sig a b)).
+    change (proj1_sig carry_sig (proj1_sig mul_sig ?a ?b)) with (carry_mulZ a b).*)
+    set (drop_high_mulmodZ := fun a b => dlet v := proj1_sig mulmod_256 a b in Saturated.drop_high v).
+    change (Saturated.drop_high (proj1_sig mulmod_256 ?a ?b)) with (drop_high_mulmodZ a b).
+    context_to_dlet_in_rhs drop_high_mulmodZ; cbv [drop_high_mulmodZ].
+    cbv [Saturated.drop_high Saturated.T fst snd Saturated.drop_high_cps CPSUtil.Tuple.left_tl_cps id append CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps].
+    cbv beta iota delta [mulmod_256 proj1_sig Saturated.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz].
+    reflexivity.
+    sig_dlet_in_rhs_to_context.
+    (*apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).*)
+    (* jgross start here! *)
+    Set Ltac Profiling.
+    Time refine_reflectively_with_bool_with default. (* Finished transaction in 212.693 secs (212.576u,0.184s) (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 21.291 secs (21.231u,0.032s) (successful) *)
+
+Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *)
diff --git a/src/Specific/MontgomeryP256.v b/src/Specific/MontgomeryP256.v
index 09e93ef81..4c2fdcf17 100644
--- a/src/Specific/MontgomeryP256.v
+++ b/src/Specific/MontgomeryP256.v
@@ -13,13 +13,13 @@ Definition p256 :=
   Eval vm_compute in
     ((Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (Z.pos m))).
 
-Definition mulmod_256 : { f:Tuple.tuple Z 4 -> Tuple.tuple Z 4 -> Tuple.tuple Z 5
-                           | forall (A B : Tuple.tuple Z 4),
+Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z (S sz)
+                           | forall (A B : Tuple.tuple Z sz),
                                f A B =
-                               (redc (r:=r)(R_numlimbs:=4) p256 A B 1)
+                               (redc (r:=r)(R_numlimbs:=sz) p256 A B 1)
                             }.
 Proof.
-  eapply (lift2_sig (fun A B c => c = (redc (r:=r)(R_numlimbs:=4) p256 A B 1)
+  eapply (lift2_sig (fun A B c => c = (redc (r:=r)(R_numlimbs:=sz) p256 A B 1)
                            )); eexists.
   cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth runtime_add runtime_mul Let_In].
   (* TODO: is there a better way to do this?  Maybe make runtime_mul_split_at_bitwidth? *)
diff --git a/src/Specific/MontgomeryP256_128.v b/src/Specific/MontgomeryP256_128.v
new file mode 100644
index 000000000..85c0bcc7e
--- /dev/null
+++ b/src/Specific/MontgomeryP256_128.v
@@ -0,0 +1,95 @@
+Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
+Require Import Crypto.Arithmetic.Core. Import B.
+Require Import Crypto.Util.Sigma.Lift.
+Require Import Coq.ZArith.BinInt.
+Require Import Coq.PArith.BinPos.
+Require Import Crypto.Util.LetIn.
+
+Definition wt (i:nat) : Z := Z.shiftl 1 (64*Z.of_nat i).
+Definition r := Eval compute in (2^64)%positive.
+Definition sz := 2%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 mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z (S sz)
+                           | forall (A B : Tuple.tuple Z sz),
+                               f A B =
+                               (redc (r:=r)(R_numlimbs:=sz) p256 A B 1)
+                            }.
+Proof.
+  eapply (lift2_sig (fun A B c => c = (redc (r:=r)(R_numlimbs:=sz) p256 A B 1)
+                           )); eexists.
+  cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth runtime_add runtime_mul Let_In].
+  (* TODO: is there a better way to do this?  Maybe make runtime_mul_split_at_bitwidth? *)
+  cbv [Definitions.Z.mul_split_at_bitwidth].
+  change Z.mul with runtime_mul; change Z.shiftr with runtime_shr; change Z.land with runtime_and.
+  cbv -[Definitions.Z.add_get_carry runtime_add runtime_mul runtime_and runtime_shr Let_In]. (* unfold Z.ones *)
+  (*
+  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
+       Saturated.divmod_cps
+       Saturated.scmul_cps
+       Saturated.uweight
+       Saturated.Columns.mul_cps
+       Saturated.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
+       Saturated.Columns.from_associational_cps
+       Saturated.Associational.multerm_cps
+       Saturated.Columns.compact_cps
+       Saturated.Columns.compact_step_cps
+       Saturated.Columns.compact_digit_cps
+       Saturated.drop_high_cps
+       Saturated.add_cps
+       Saturated.Columns.add_cps
+       Saturated.Columns.cons_to_nth_cps
+       Nat.pred
+       Saturated.join0
+       Saturated.join0_cps CPSUtil.Tuple.left_append_cps
+       CPSUtil.Tuple.mapi_with_cps
+       id
+       Positional.zeros Saturated.zero Saturated.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 Saturated.zero Saturated.Columns.nils Tuple.repeat Tuple.append
+       (*
+       Saturated.Associational.multerm_cps
+       Saturated.Columns.from_associational_cps Positional.place_cps Saturated.Columns.cons_to_nth_cps Saturated.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 *)
+       (* Saturated.add_cps Saturated.divmod_cps Saturated.drop_high_cps Saturated.scmul_cps Saturated.zero Saturated.Columns.mul_cps Saturated.Columns.add_cps Saturated.uweight Saturated.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.