diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-07-08 20:13:14 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-07-08 20:46:01 -0400 |
| commit | e63299d7b76e6fb2416cfca00b29f992501cf76d (patch) | |
| tree | 48de6cf3ca8f75bc5179b817d7fc3b9a64a648cd /src/Compilers/Z | |
| parent | 699c7964f388e0ec232f4b71096294250cd6e4cd (diff) | |
Unfold tuple arguments in reflective pipeline
This closes #239
After | File Name | Before || Change
---------------------------------------------------------------------------------------
10m04.12s | Total | 10m05.68s || -0m01.55s
---------------------------------------------------------------------------------------
2m45.12s | Specific/X25519/C64/ladderstep | 2m48.45s || -0m03.32s
1m06.06s | Specific/IntegrationTestLadderstep130 | 1m04.76s || +0m01.29s
2m03.02s | Specific/NISTP256/AMD64/femul | 2m02.29s || +0m00.72s
1m20.35s | Specific/IntegrationTestKaratsubaMul | 1m20.10s || +0m00.25s
0m25.29s | Specific/IntegrationTestMontgomeryP256_128 | 0m25.17s || +0m00.11s
0m16.66s | Specific/IntegrationTestFreeze | 0m16.18s || +0m00.48s
0m14.81s | Specific/NISTP256/AMD64/feadd | 0m15.09s || -0m00.27s
0m14.58s | Specific/NISTP256/AMD64/fesub | 0m14.48s || +0m00.09s
0m13.23s | Specific/X25519/C64/femul | 0m13.54s || -0m00.30s
0m12.00s | Specific/NISTP256/AMD64/feopp | 0m12.07s || -0m00.07s
0m11.25s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m11.44s || -0m00.18s
0m11.23s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m11.19s || +0m00.04s
0m11.06s | Specific/IntegrationTestSub | 0m11.24s || -0m00.17s
0m10.39s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m10.41s || -0m00.01s
0m09.85s | Specific/X25519/C64/fesquare | 0m09.75s || +0m00.09s
0m09.19s | Specific/NISTP256/AMD64/fenz | 0m09.04s || +0m00.15s
0m08.76s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.11s || -0m00.34s
0m00.69s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.80s || -0m00.11s
0m00.59s | Compilers/Z/Bounds/Pipeline | 0m00.57s || +0m00.02s
Diffstat (limited to 'src/Compilers/Z')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v index f132eb92a..9194f49db 100644 --- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v +++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v @@ -27,6 +27,7 @@ Require Import Crypto.Compilers.Z.InterpSideConditions. Require Import Crypto.Compilers.Z.Bounds.Pipeline.Definition. Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Tactics.SubstLet. +Require Import Crypto.Util.Tactics.UnfoldArg. Require Import Crypto.Util.Tactics.UnifyAbstractReflexivity. Require Import Crypto.Util.FixedWordSizes. Require Import Crypto.Util.Option. @@ -58,6 +59,8 @@ forall x, Interp _ ?e x = F >> by reifying [F]. *) Ltac do_reify := + unfold_second_arg Tuple.tuple; + unfold_second_arg Tuple.tuple'; cbv beta iota delta [Tuple.tuple Tuple.tuple'] in *; cbv beta iota delta [Syntax.interp_flat_type Syntax.interp_base_type]; reify_context_variables; |