Add initial IntegrationTestMontgomeryP256.v

1 files changed, 114 insertions, 0 deletions

diff --git a/src/Specific/IntegrationTestMontgomeryP256.v b/src/Specific/IntegrationTestMontgomeryP256.v
new file mode 100644
index 000000000..631ea3209
--- /dev/null
+++ b/src/Specific/IntegrationTestMontgomeryP256.v
@@ -0,0 +1,114 @@
+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.
+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:=4) 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.*)
+    Ltac reify_debug_level ::= constr:(3%nat).
+    Typeclasses eauto := debug.
+    Time admit; refine_reflectively. (* Finished transaction in 19.348 secs (19.284u,0.036s) (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 Admitted. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
+
+End BoundedField25p5.