fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add reverse_nondep and ring_simplify_subterms_in_all tactics	Jason Gross	2016-07-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 2m50.48s \| Total \| 3m00.71s \|\| -0m10.23s ------------------------------------------------------------------------------------ 0m15.26s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m18.84s \|\| -0m03.58s 0m48.47s \| Specific/GF25519 \| 0m51.03s \|\| -0m02.56s 0m35.42s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m34.27s \|\| +0m01.14s 0m09.92s \| Specific/GF1305 \| 0m08.66s \|\| +0m01.25s 0m05.73s \| Experiments/GenericFieldPow \| 0m07.03s \|\| -0m01.29s 0m03.67s \| ModularArithmetic/Pow2BaseProofs \| 0m04.78s \|\| -0m01.11s 0m11.26s \| Experiments/SpecEd25519 \| 0m11.21s \|\| +0m00.04s 0m05.81s \| Algebra \| 0m06.09s \|\| -0m00.28s 0m04.54s \| WeierstrassCurve/Pre \| 0m05.08s \|\| -0m00.54s 0m03.62s \| ModularArithmetic/Tutorial \| 0m04.38s \|\| -0m00.75s 0m03.34s \| CompleteEdwardsCurve/Pre \| 0m03.56s \|\| -0m00.22s 0m02.83s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.37s \|\| -0m00.54s 0m01.76s \| Experiments/EdDSARefinement \| 0m01.81s \|\| -0m00.05s 0m01.54s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.67s \|\| -0m00.12s 0m01.52s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.62s \|\| -0m00.10s 0m01.47s \| Encoding/PointEncodingPre \| 0m01.63s \|\| -0m00.15s 0m01.21s \| ModularArithmetic/ExtendedBaseVector \| 0m01.33s \|\| -0m00.12s 0m00.99s \| Experiments/SpecificCurve25519 \| 0m00.95s \|\| +0m00.04s 0m00.98s \| ModularArithmetic/ModularBaseSystemProofs \| 0m01.08s \|\| -0m00.10s 0m00.90s \| ModularArithmetic/BarrettReduction/Z \| 0m00.96s \|\| -0m00.05s 0m00.87s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.88s \|\| -0m00.01s 0m00.86s \| ModularArithmetic/ModularBaseSystemField \| 0m00.99s \|\| -0m00.13s 0m00.81s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.94s \|\| -0m00.12s 0m00.71s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.69s \|\| +0m00.02s 0m00.67s \| Util/IterAssocOp \| 0m00.74s \|\| -0m00.06s 0m00.65s \| Encoding/ModularWordEncodingTheorems \| 0m00.68s \|\| -0m00.03s 0m00.64s \| Testbit \| 0m00.63s \|\| +0m00.01s 0m00.61s \| Util/AdditionChainExponentiation \| 0m00.68s \|\| -0m00.07s 0m00.61s \| ModularArithmetic/ModularBaseSystem \| 0m00.72s \|\| -0m00.10s 0m00.61s \| Encoding/ModularWordEncodingPre \| 0m00.82s \|\| -0m00.20s 0m00.60s \| Spec/EdDSA \| 0m00.60s \|\| +0m00.00s 0m00.59s \| ModularArithmetic/ModularBaseSystemList \| 0m00.87s \|\| -0m00.28s 0m00.57s \| Spec/ModularWordEncoding \| 0m00.62s \|\| -0m00.05s 0m00.57s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.61s \|\| -0m00.04s 0m00.43s \| Spec/WeierstrassCurve \| 0m00.43s \|\| +0m00.00s 0m00.40s \| Spec/CompleteEdwardsCurve \| 0m00.44s \|\| -0m00.03s 0m00.04s \| Util/Tactics \| 0m00.03s \|\| +0m00.01s
*	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 ring_simplify_subterms	Jason Gross	2016-07-22
\|
*	Merge of fixedlength and master	jadep	2016-07-11
\|\
\| *	wrap nsatz in Algebra	Andres Erbsen	2016-07-11
\| \|
\| *	Add useful tactics and util lemmas	Jason Gross	2016-07-08
\| \|
* \|	stuck trying to figure out dependently typed continuation passing style	Andres Erbsen	2016-07-06
\|/
*	Add [specialize_by] tactic	Jason Gross	2016-07-01
\|
*	Fix field_algebra in 8.4	Jason Gross	2016-06-28
\|
*	Fix super_nsatz tactic to be better about ordering	Jason Gross	2016-06-28
\| \| \| \|	See also #13.
*	Add [destruct_head] tactics	Jason Gross	2016-06-27
\|
*	Add [break_match] for hypotheses	Jason Gross	2016-06-27
\|
*	Various nsatz and field tactic improvements	Jason Gross	2016-06-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 2m29.81s \| Total \| 2m34.05s \|\| -0m04.23s ------------------------------------------------------------------------------------ 0m11.98s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m15.22s \|\| -0m03.24s 0m29.71s \| ModularArithmetic/ModularBaseSystemProofs \| 0m30.05s \|\| -0m00.33s 0m29.12s \| Specific/GF25519 \| 0m29.12s \|\| +0m00.00s 0m21.50s \| Experiments/SpecEd25519 \| 0m21.43s \|\| +0m00.07s 0m18.20s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m18.24s \|\| -0m00.03s 0m07.36s \| Specific/GF1305 \| 0m07.33s \|\| +0m00.03s 0m06.66s \| Experiments/GenericFieldPow \| 0m06.89s \|\| -0m00.22s 0m03.84s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.84s \|\| +0m00.00s 0m03.82s \| ModularArithmetic/Tutorial \| 0m03.88s \|\| -0m00.06s 0m03.74s \| CompleteEdwardsCurve/Pre \| 0m03.81s \|\| -0m00.06s 0m02.30s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.27s \|\| +0m00.02s 0m02.11s \| ModularArithmetic/PrimeFieldTheorems \| 0m02.05s \|\| +0m00.06s 0m01.93s \| Algebra \| 0m02.06s \|\| -0m00.13s 0m01.17s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.19s \|\| -0m00.02s 0m01.13s \| ModularArithmetic/ExtendedBaseVector \| 0m01.18s \|\| -0m00.05s 0m01.01s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m01.07s \|\| -0m00.06s 0m00.61s \| Encoding/ModularWordEncodingTheorems \| 0m00.64s \|\| -0m00.03s 0m00.61s \| Spec/EdDSA \| 0m00.62s \|\| -0m00.01s 0m00.57s \| Encoding/ModularWordEncodingPre \| 0m00.62s \|\| -0m00.05s 0m00.56s \| Spec/ModularWordEncoding \| 0m00.59s \|\| -0m00.02s 0m00.55s \| ModularArithmetic/ModularBaseSystem \| 0m00.59s \|\| -0m00.03s 0m00.52s \| ModularArithmetic/PseudoMersenneBaseRep \| 0m00.52s \|\| +0m00.00s 0m00.41s \| Tactics/Nsatz \| 0m00.41s \|\| +0m00.00s 0m00.38s \| Spec/CompleteEdwardsCurve \| 0m00.40s \|\| -0m00.02s 0m00.03s \| Util/Tactics \| 0m00.03s \|\| +0m00.00s
*	Improve some tactics and lemmas	Jason Gross	2016-06-23
\|
*	[break_match] should not be local	Jason Gross	2016-06-23
\|
*	Add tactics to Tactics, at most 2 sq-roots to Algebra	Jason Gross	2016-06-23
\|
*	Add a tactic for field inequalities	Jason Gross	2016-04-19
	Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc.