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.*) 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) *)