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/IntegrationTestLadderstep130.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/IntegrationTestLadderstep130.v')
-rw-r--r-- | src/Specific/IntegrationTestLadderstep130.v | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v index 541dcaee8..4dd01d018 100644 --- a/src/Specific/IntegrationTestLadderstep130.v +++ b/src/Specific/IntegrationTestLadderstep130.v @@ -77,12 +77,7 @@ Section BoundedField25p5. /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz)))) /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }. Proof. - lazymatch goal with - | [ |- { op | forall (a:?A) (b:?B) (c:?C), - let v := op a b c in - @?P a b c v } ] - => refine (@lift3_sig A B C _ P _) - end. + apply_lift_sig. intros a b c; cbv beta iota zeta. lazymatch goal with | [ |- { e | ?A -> ?B -> ?C -> @?E e } ] @@ -102,11 +97,12 @@ Section BoundedField25p5. cbv [proj1_sig]; cbv [Mxzladderstep_sig]. context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _ _). cbv [M.xzladderstep a24_sig]. - do 4 lazymatch goal with - | [ |- context[@proj1_sig ?a ?b ?f_sig _] ] - => context_to_dlet_in_rhs (@proj1_sig a b f_sig) - end. - cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]; cbn [fst snd]. + repeat lazymatch goal with + | [ |- context[@proj1_sig ?a ?b ?f_sig _] ] + => context_to_dlet_in_rhs (@proj1_sig a b f_sig) + end. + cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig]. + cbv_runtime. refine (proj2 FINAL). } subst feW feW_bounded; cbv beta. (* jgross start here! *) |