diff options
author | Jason Gross <jgross@mit.edu> | 2017-07-08 20:31:22 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-07-08 20:46:01 -0400 |
commit | dcca63da237b255442aa7260b8d5001d94bf90df (patch) | |
tree | 98f73a81dd16a15d167a708c2cec2b7b42192148 /src/Specific/X25519/C64/fesquare.v | |
parent | e63299d7b76e6fb2416cfca00b29f992501cf76d (diff) |
Factor out some of the preglue synthesis code
This makes it a bit more uniform, and hopefully more automatable and
packageable. Unfortunately, there's still no spec for this part of the
pipeline, so the tactics simply aggregate common patterns.
Alas, this also makes things a bit slower; I suspect that [Defined] is
the place where things are slower.
After | File Name | Before || Change
---------------------------------------------------------------------------------------
13m51.14s | Total | 12m59.29s || +0m51.84s
---------------------------------------------------------------------------------------
1m54.18s | Specific/IntegrationTestKaratsubaMul | 1m43.12s || +0m11.06s
1m38.97s | Specific/IntegrationTestLadderstep130 | 1m30.26s || +0m08.70s
2m19.75s | Specific/NISTP256/AMD64/femul | 2m14.08s || +0m05.66s
0m39.90s | Specific/IntegrationTestMontgomeryP256_128 | 0m34.21s || +0m05.68s
0m21.95s | Specific/NISTP256/AMD64/fesub | 0m19.23s || +0m02.71s
0m21.37s | Specific/NISTP256/AMD64/feadd | 0m18.82s || +0m02.55s
0m21.02s | Specific/X25519/C64/femul | 0m18.32s || +0m02.69s
0m20.53s | Specific/IntegrationTestFreeze | 0m23.26s || -0m02.73s
0m18.28s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m15.32s || +0m02.96s
0m18.20s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m15.52s || +0m02.67s
0m16.35s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m13.52s || +0m02.83s
0m13.92s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m11.84s || +0m02.08s
0m18.23s | Specific/NISTP256/AMD64/MontgomeryP256 | 0m16.62s || +0m01.60s
0m15.54s | Specific/IntegrationTestSub | 0m14.53s || +0m01.00s
0m14.78s | Specific/X25519/C64/fesquare | 0m13.13s || +0m01.64s
0m13.71s | Specific/NISTP256/AMD64/fenz | 0m12.69s || +0m01.02s
3m14.34s | Specific/X25519/C64/ladderstep | 3m14.32s || +0m00.02s
0m16.54s | Specific/NISTP256/AMD64/feopp | 0m16.48s || +0m00.05s
0m12.21s | Specific/MontgomeryP256_128 | 0m12.70s || -0m00.48s
0m00.73s | Specific/IntegrationTestTemporaryMiscCommon | 0m00.72s || +0m00.01s
0m00.64s | Specific/IntegrationTestDisplayCommon | 0m00.60s || +0m00.04s
Diffstat (limited to 'src/Specific/X25519/C64/fesquare.v')
-rw-r--r-- | src/Specific/X25519/C64/fesquare.v | 18 |
1 files changed, 3 insertions, 15 deletions
diff --git a/src/Specific/X25519/C64/fesquare.v b/src/Specific/X25519/C64/fesquare.v index d7d717c61..0bba90c68 100644 --- a/src/Specific/X25519/C64/fesquare.v +++ b/src/Specific/X25519/C64/fesquare.v @@ -46,21 +46,9 @@ Section BoundedField25p5. { square : feBW -> feBW | forall a, phi (square a) = F.mul (phi a) (phi a) }. Proof. - lazymatch goal with - | [ |- { f | forall a, ?phi (f a) = @?rhs a } ] - => apply lift1_sig with (P:=fun a f => phi f = rhs a) - end. - intros a. - eexists_sig_etransitivity. all:cbv [phi]. - rewrite <- (proj2_sig square_sig). - symmetry; rewrite <- (proj2_sig carry_sig); symmetry. - set (carry_squareZ := fun a => proj1_sig carry_sig (proj1_sig square_sig a)). - change (proj1_sig carry_sig (proj1_sig square_sig ?a)) with (carry_squareZ a). - context_to_dlet_in_rhs carry_squareZ. - cbv beta iota delta [carry_squareZ proj1_sig square_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)). + start_preglue. + do_rewrite_with_1sig_add_carry square_sig carry_sig; cbv_runtime. + all:fin_preglue. (* jgross start here! *) (*Set Ltac Profiling.*) Time refine_reflectively. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *) |