diff options
Diffstat (limited to 'src/Specific/IntegrationTestSub.v')
| -rw-r--r-- | src/Specific/IntegrationTestSub.v | 86 |
1 files changed, 20 insertions, 66 deletions
diff --git a/src/Specific/IntegrationTestSub.v b/src/Specific/IntegrationTestSub.v index 7599c99e1..f88dc51d9 100644 --- a/src/Specific/IntegrationTestSub.v +++ b/src/Specific/IntegrationTestSub.v @@ -1,71 +1,27 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Local Open Scope Z_scope. - +Require Import Crypto.Specific.X25519.C64.ReificationTypes. +Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest. Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Specific.ArithmeticSynthesisTest. 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.Util.BoundedWord. Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. - Require Import Crypto.Compilers.Z.Bounds.Pipeline. -Section BoundedField25p5. - Local Coercion Z.of_nat : nat >-> Z. - - Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)). - Let length_lw := Eval compute in List.length limb_widths. +Local Definition phi : feBW -> F m := + fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x). - Local Notation b_of exp := {| lower := 0 ; upper := 2^exp + 2^(exp-3) |}%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *) - (* The definition [bounds_exp] is a tuple-version of the - limb-widths, which are the [exp] argument in [b_of] above, i.e., - the approximate base-2 exponent of the bounds on the limb in that - position. *) - Let bounds_exp : Tuple.tuple Z length_lw - := Eval compute in - Tuple.from_list length_lw limb_widths eq_refl. - Let bounds : Tuple.tuple zrange length_lw - := Eval compute in - Tuple.map (fun e => b_of e) bounds_exp. - - Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))). - 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 sub : - { sub : feBW -> feBW -> feBW - | forall a b, phi (sub a b) = F.sub (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 sub_sig). - symmetry; rewrite <- (proj2_sig carry_sig); symmetry. - set (carry_subZ := fun a b => proj1_sig carry_sig (proj1_sig sub_sig a b)). - change (proj1_sig carry_sig (proj1_sig sub_sig ?a ?b)) with (carry_subZ a b). - context_to_dlet_in_rhs carry_subZ. - cbv beta iota delta [carry_subZ proj1_sig sub_sig carry_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. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *) - (*Show Ltac Profile.*) - (* total time: 19.632s +(* TODO : change this to field once field isomorphism happens *) +Definition sub : + { sub : feBW -> feBW -> feBW + | forall a b, phi (sub a b) = F.sub (phi a) (phi b) }. +Proof. + start_preglue. + do_rewrite_with_2sig_add_carry sub_sig carry_sig; cbv_runtime. + all:fin_preglue. + (* jgross start here! *) + (*Set Ltac Profiling.*) + Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *) + (*Show Ltac Profile.*) + (* total time: 19.632s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ @@ -106,7 +62,5 @@ Section BoundedField25p5. │ ├─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 10.167 secs (10.123u,0.023s) (successful) *) - -End BoundedField25p5. + *) +Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *) |