fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Make the library 20% faster: [auto with *] is evil	Jason Gross	2016-07-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
*	Add a TODO comment	Jason Gross	2016-07-06
\| \| \| \|	For jadep, or for me, after the 8.5 build is fixed.
*	Merged changes, including new ZUtil conventions.	jadep	2016-07-06
\|\
\| *	Make ZUtil more uniform	Jason Gross	2016-07-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The standard library uses Z., and Z and Z_* are compatibility notations. We follow suit. Also, eliminate a few lemmas that are duplicates of ones in the standard library.
\| *	Simplify a proof that no longer needs more hints	Jason Gross	2016-07-01
\| \| \| \| \| \| \| \|	[intuition] is overpowered and does [auto with *] or something
* \|	BaseSystem encode function is no longer naive; it does a mod/div loop rather ↵	jadep	2016-06-28
\|/ \| \| \|	than sticking the value of the Z input in the first digit. The condition that c is positive has been added to PseudoMersenneBaseParams--it is necessary for this encode and for canonicalization, for which it was previously a section variable.
*	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
\| \| \| \| \|	This prevents notation conflicts (see comment in Notations.v for more explanation).
*	8.5 fixes	Jason Gross	2016-06-10
\|
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-03-30
\|\
* \|	made BaseVector instance global	Jade Philipoom	2016-03-20
\| \|
* \|	refactor of Basesystem and ModularBaseSystem; includes general code ↵	Jade Philipoom	2016-03-20
\| \| \| \| \| \| \| \|	organization and changes to pseudomersenne base parameters that require bases to be expressed as powers of 2, which reduces the burden of proof on the caller and allows carry functions to use bitwise operations rather than mod and division
* \|	Refactored BaseSystem and ModularBaseSystem.	Jade Philipoom	2016-03-11
\| \|
\| *	Finish absolutizing imports	Jason Gross	2016-03-10
\|/ \| \| \| \| \| \| \| \| \| \| \|	The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" \| xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
*	Finish seperating our specs: remove old non-specified code	Andres Erbsen	2016-02-15