Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Redesign intuition, speeding up overall compilation by 20% #37

Merged
merged 2 commits into from
Jul 22, 2016
Merged

Redesign intuition, speeding up overall compilation by 20% #37

merged 2 commits into from
Jul 22, 2016

Commits on Jul 22, 2016

  1. Revert "Add more ZUtil automation" 

    This reverts commit 29bb3dd.

[intuition] is stupid and terrible.  Fix upcoming.
    @JasonGross
    JasonGross committed Jul 22, 2016
    Configuration menu
    Copy the full SHA
    5d7b2bc View commit details
    Browse the repository at this point in the history

  2. Make the library 20% faster: [auto with *] is evil 

    I do hereby revoke the privilege of [intuition] to grab random hints
from random databases.  This privilege is reserved for
[debug_intuition], which comes with a warning about not being used in
production code.  This tactic is useful in conjunction with `Print Hint
*`, to discover what hint databases the hints were grabbed from.

(Suggestions for renaming [debug_intuition] welcome.)

Any file using [intuition] must [Require Export
Crypto.Util.FixCoqMistakes.].  It's possible we could lift this
restriction by compiling [FixCoqMistakes] separately, and passing along
`-require FixCoqMistakes` to Coq.  Should we do this?

After    | File Name                                         | Before   || Change
------------------------------------------------------------------------------------
3m29.54s | Total                                             | 4m33.13s || -1m03.59s
------------------------------------------------------------------------------------
0m03.75s | BaseSystemProofs                                  | 0m43.84s || -0m40.09s
0m42.57s | CompleteEdwardsCurve/ExtendedCoordinates          | 0m34.48s || +0m08.09s
0m03.04s | Util/ListUtil                                     | 0m11.18s || -0m08.14s
0m01.62s | ModularArithmetic/PrimeFieldTheorems              | 0m09.53s || -0m07.90s
0m00.87s | Util/NumTheoryUtil                                | 0m07.61s || -0m06.74s
0m01.61s | Encoding/PointEncodingPre                         | 0m06.93s || -0m05.31s
0m51.95s | Specific/GF25519                                  | 0m47.52s || +0m04.42s
0m12.30s | Experiments/SpecEd25519                           | 0m11.29s || +0m01.01s
0m09.22s | Specific/GF1305                                   | 0m08.17s || +0m01.05s
0m03.48s | CompleteEdwardsCurve/Pre                          | 0m04.77s || -0m01.28s
0m02.70s | Assembly/State                                    | 0m04.09s || -0m01.38s
0m01.55s | ModularArithmetic/ModularArithmeticTheorems       | 0m02.93s || -0m01.38s
0m01.16s | Assembly/Pseudize                                 | 0m02.34s || -0m01.17s
0m15.67s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m16.37s || -0m00.70s
0m06.02s | Algebra                                           | 0m06.67s || -0m00.65s
0m05.90s | Experiments/GenericFieldPow                       | 0m06.68s || -0m00.77s
0m04.65s | WeierstrassCurve/Pre                              | 0m05.27s || -0m00.61s
0m03.93s | ModularArithmetic/Pow2BaseProofs                  | 0m03.94s || -0m00.00s
0m03.70s | ModularArithmetic/Tutorial                        | 0m03.85s || -0m00.14s
0m02.83s | ModularArithmetic/ModularBaseSystemOpt            | 0m02.84s || -0m00.00s
0m02.74s | Experiments/EdDSARefinement                       | 0m01.80s || +0m00.94s
0m02.35s | Util/ZUtil                                        | 0m02.51s || -0m00.15s
0m01.86s | Assembly/Wordize                                  | 0m02.32s || -0m00.45s
0m01.23s | ModularArithmetic/ExtendedBaseVector              | 0m01.20s || +0m00.03s
0m01.21s | BaseSystem                                        | 0m01.63s || -0m00.41s
0m01.03s | Experiments/SpecificCurve25519                    | 0m00.98s || +0m00.05s
0m01.01s | ModularArithmetic/ModularBaseSystemProofs         | 0m01.11s || -0m00.10s
0m00.95s | ModularArithmetic/BarrettReduction/Z              | 0m01.38s || -0m00.42s
0m00.92s | Experiments/DerivationsOptionRectLetInEncoding    | 0m01.81s || -0m00.89s
0m00.85s | ModularArithmetic/ModularBaseSystemField          | 0m00.86s || -0m00.01s
0m00.82s | ModularArithmetic/ModularBaseSystemListProofs     | 0m00.79s || +0m00.02s
0m00.80s | Assembly/QhasmEvalCommon                          | 0m00.93s || -0m00.13s
0m00.73s | Spec/EdDSA                                        | 0m00.59s || +0m00.14s
0m00.72s | Util/Tuple                                        | 0m00.71s || +0m00.01s
0m00.70s | Util/IterAssocOp                                  | 0m00.72s || -0m00.02s
0m00.67s | Encoding/ModularWordEncodingTheorems              | 0m00.71s || -0m00.03s
0m00.66s | Assembly/Pipeline                                 | 0m00.64s || +0m00.02s
0m00.65s | Testbit                                           | 0m00.65s || +0m00.00s
0m00.65s | Assembly/PseudoConversion                         | 0m00.65s || +0m00.00s
0m00.64s | Util/AdditionChainExponentiation                  | 0m00.63s || +0m00.01s
0m00.63s | ModularArithmetic/ExtPow2BaseMulProofs            | 0m00.64s || -0m00.01s
0m00.63s | Assembly/Pseudo                                   | 0m00.65s || -0m00.02s
0m00.62s | ModularArithmetic/ModularBaseSystem               | 0m00.57s || +0m00.05s
0m00.61s | ModularArithmetic/ModularBaseSystemList           | 0m00.57s || +0m00.04s
0m00.60s | Encoding/ModularWordEncodingPre                   | 0m00.69s || -0m00.08s
0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs   | 0m00.59s || +0m00.01s
0m00.56s | Assembly/StringConversion                         | 0m00.56s || +0m00.00s
0m00.54s | Spec/ModularWordEncoding                          | 0m00.61s || -0m00.06s
0m00.54s | Assembly/QhasmUtil                                | 0m00.46s || +0m00.08s
0m00.52s | Assembly/Qhasm                                    | 0m00.53s || -0m00.01s
0m00.48s | Assembly/AlmostQhasm                              | 0m00.52s || -0m00.04s
0m00.48s | ModularArithmetic/Pre                             | 0m00.48s || +0m00.00s
0m00.46s | Assembly/Vectorize                                | 0m00.72s || -0m00.25s
0m00.45s | Spec/WeierstrassCurve                             | 0m00.44s || +0m00.01s
0m00.44s | Assembly/AlmostConversion                         | 0m00.44s || +0m00.00s
0m00.43s | ModularArithmetic/Pow2Base                        | 0m00.51s || -0m00.08s
0m00.42s | ModularArithmetic/PseudoMersenneBaseParams        | 0m00.38s || +0m00.03s
0m00.41s | Spec/CompleteEdwardsCurve                         | 0m00.43s || -0m00.02s
0m00.34s | Spec/ModularArithmetic                            | 0m00.36s || -0m00.01s
0m00.03s | Util/FixCoqMistakes                               |   N/A    || +0m00.03s
0m00.02s | Util/Notations                                    | 0m00.04s || -0m00.02s
0m00.02s | Util/Tactics                                      | 0m00.02s || +0m00.00s
    @JasonGross
    JasonGross committed Jul 22, 2016
    Configuration menu
    Copy the full SHA
    4519b11 View commit details
    Browse the repository at this point in the history