fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Make Z.pre_reorder_fractions / Z.simplify_fractions_le not loop	Jason Gross	2016-07-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 1m50.76s \| Total \| 1m52.98s \|\| -0m02.22s ---------------------------------------------------------------------------------- 0m33.56s \| Specific/GF25519 \| 0m34.00s \|\| -0m00.43s 0m15.81s \| ModularArithmetic/ModularBaseSystemProofs \| 0m15.78s \|\| +0m00.03s 0m11.88s \| Experiments/SpecEd25519 \| 0m11.77s \|\| +0m00.11s 0m07.21s \| Specific/GF1305 \| 0m07.49s \|\| -0m00.28s 0m04.84s \| ModularArithmetic/Tutorial \| 0m05.31s \|\| -0m00.46s 0m04.67s \| ModularArithmetic/Pow2BaseProofs \| 0m05.34s \|\| -0m00.67s 0m04.65s \| BaseSystemProofs \| 0m04.13s \|\| +0m00.52s 0m03.26s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.33s \|\| -0m00.07s 0m02.39s \| Util/ZUtil \| 0m02.40s \|\| -0m00.00s 0m02.39s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.62s \|\| +0m00.77s 0m02.28s \| Encoding/PointEncodingPre \| 0m02.27s \|\| +0m00.00s 0m01.72s \| BaseSystem \| 0m01.23s \|\| +0m00.49s 0m01.64s \| ModularArithmetic/PrimeFieldTheorems \| 0m02.06s \|\| -0m00.42s 0m01.44s \| ModularArithmetic/BarrettReduction/Z \| 0m01.45s \|\| -0m00.01s 0m01.34s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.49s \|\| -0m00.14s 0m01.13s \| ModularArithmetic/ExtendedBaseVector \| 0m01.13s \|\| +0m00.00s 0m00.92s \| ModularArithmetic/ModularBaseSystemField \| 0m00.95s \|\| -0m00.02s 0m00.91s \| Util/NumTheoryUtil \| 0m01.38s \|\| -0m00.46s 0m00.85s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.96s \|\| -0m00.10s 0m00.77s \| Encoding/ModularWordEncodingTheorems \| 0m00.93s \|\| -0m00.16s 0m00.76s \| Experiments/SpecificCurve25519 \| 0m00.75s \|\| +0m00.01s 0m00.67s \| Testbit \| 0m00.62s \|\| +0m00.05s 0m00.65s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.62s \|\| +0m00.03s 0m00.62s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.95s \|\| -0m00.32s 0m00.60s \| ModularArithmetic/ModularBaseSystem \| 0m00.62s \|\| -0m00.02s 0m00.60s \| Spec/ModularWordEncoding \| 0m00.88s \|\| -0m00.28s 0m00.60s \| Encoding/ModularWordEncodingPre \| 0m00.71s \|\| -0m00.10s 0m00.59s \| ModularArithmetic/ModularBaseSystemList \| 0m00.90s \|\| -0m00.31s 0m00.54s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.40s \|\| +0m00.14s 0m00.51s \| ModularArithmetic/Pre \| 0m00.70s \|\| -0m00.18s 0m00.50s \| Spec/ModularArithmetic \| 0m00.36s \|\| +0m00.14s 0m00.46s \| ModularArithmetic/Pow2Base \| 0m00.46s \|\| +0m00.00s
*	Add another ZUtil lemma	Jason Gross	2016-07-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 1m39.75s \| Total \| 1m39.99s \|\| -0m00.24s ---------------------------------------------------------------------------------- 0m31.61s \| Specific/GF25519 \| 0m31.72s \|\| -0m00.10s 0m14.64s \| ModularArithmetic/ModularBaseSystemProofs \| 0m14.65s \|\| -0m00.00s 0m11.16s \| Experiments/SpecEd25519 \| 0m11.19s \|\| -0m00.02s 0m07.06s \| Specific/GF1305 \| 0m06.94s \|\| +0m00.11s 0m03.95s \| ModularArithmetic/Tutorial \| 0m03.68s \|\| +0m00.27s 0m03.91s \| ModularArithmetic/Pow2BaseProofs \| 0m03.94s \|\| -0m00.02s 0m03.59s \| BaseSystemProofs \| 0m03.72s \|\| -0m00.13s 0m03.11s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.10s \|\| +0m00.00s 0m02.40s \| Util/ZUtil \| 0m02.30s \|\| +0m00.10s 0m01.53s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.52s \|\| +0m00.01s 0m01.52s \| Encoding/PointEncodingPre \| 0m01.49s \|\| +0m00.03s 0m01.48s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.53s \|\| -0m00.05s 0m01.12s \| BaseSystem \| 0m01.40s \|\| -0m00.27s 0m01.10s \| ModularArithmetic/ExtendedBaseVector \| 0m01.07s \|\| +0m00.03s 0m00.98s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.95s \|\| +0m00.03s 0m00.93s \| ModularArithmetic/BarrettReduction/Z \| 0m00.89s \|\| +0m00.04s 0m00.89s \| Encoding/ModularWordEncodingPre \| 0m00.80s \|\| +0m00.08s 0m00.84s \| Util/NumTheoryUtil \| 0m00.81s \|\| +0m00.02s 0m00.84s \| ModularArithmetic/ModularBaseSystemField \| 0m00.86s \|\| -0m00.02s 0m00.74s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.79s \|\| -0m00.05s 0m00.67s \| Experiments/SpecificCurve25519 \| 0m00.65s \|\| +0m00.02s 0m00.66s \| Encoding/ModularWordEncodingTheorems \| 0m00.64s \|\| +0m00.02s 0m00.62s \| Testbit \| 0m00.59s \|\| +0m00.03s 0m00.58s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.57s \|\| +0m00.01s 0m00.57s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.59s \|\| -0m00.02s 0m00.57s \| Spec/ModularWordEncoding \| 0m00.58s \|\| -0m00.01s 0m00.54s \| ModularArithmetic/ModularBaseSystem \| 0m00.54s \|\| +0m00.00s 0m00.54s \| ModularArithmetic/ModularBaseSystemList \| 0m00.55s \|\| -0m00.01s 0m00.45s \| ModularArithmetic/Pre \| 0m00.43s \|\| +0m00.02s 0m00.40s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.57s \|\| -0m00.16s 0m00.40s \| ModularArithmetic/Pow2Base \| 0m00.59s \|\| -0m00.18s 0m00.35s \| Spec/ModularArithmetic \| 0m00.35s \|\| +0m00.00s
*	Fix 8.4 build.	jadep	2016-07-25
\|
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-25
\|\
* \|	A couple new util lemmas	jadep	2016-07-25
\| \|
\| *	More Zpow in ZUtil	Jason Gross	2016-07-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 1m43.01s \| Total \| 1m43.85s \|\| -0m00.83s ---------------------------------------------------------------------------------- 0m47.97s \| Specific/GF25519 \| 0m47.51s \|\| +0m00.46s 0m11.39s \| Experiments/SpecEd25519 \| 0m11.22s \|\| +0m00.16s 0m08.26s \| Specific/GF1305 \| 0m08.22s \|\| +0m00.03s 0m03.77s \| ModularArithmetic/Pow2BaseProofs \| 0m04.47s \|\| -0m00.69s 0m03.68s \| ModularArithmetic/Tutorial \| 0m03.91s \|\| -0m00.23s 0m03.62s \| BaseSystemProofs \| 0m03.67s \|\| -0m00.04s 0m02.84s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.74s \|\| +0m00.09s 0m02.18s \| Util/ZUtil \| 0m02.18s \|\| +0m00.00s 0m01.50s \| Encoding/PointEncodingPre \| 0m02.09s \|\| -0m00.58s 0m01.44s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.52s \|\| -0m00.08s 0m01.43s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.62s \|\| -0m00.19s 0m01.22s \| ModularArithmetic/ExtendedBaseVector \| 0m01.14s \|\| +0m00.08s 0m01.14s \| BaseSystem \| 0m01.12s \|\| +0m00.01s 0m00.94s \| Experiments/SpecificCurve25519 \| 0m00.96s \|\| -0m00.02s 0m00.93s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.98s \|\| -0m00.04s 0m00.91s \| ModularArithmetic/ModularBaseSystemProofs \| 0m00.91s \|\| +0m00.00s 0m00.90s \| ModularArithmetic/BarrettReduction/Z \| 0m00.88s \|\| +0m00.02s 0m00.85s \| Util/NumTheoryUtil \| 0m00.82s \|\| +0m00.03s 0m00.82s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.57s \|\| +0m00.25s 0m00.82s \| ModularArithmetic/ModularBaseSystemField \| 0m00.90s \|\| -0m00.08s 0m00.77s \| ModularArithmetic/ModularBaseSystemList \| 0m00.51s \|\| +0m00.26s 0m00.72s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.72s \|\| +0m00.00s 0m00.63s \| Encoding/ModularWordEncodingTheorems \| 0m00.68s \|\| -0m00.05s 0m00.60s \| Testbit \| 0m00.58s \|\| +0m00.02s 0m00.58s \| Spec/ModularWordEncoding \| 0m00.58s \|\| +0m00.00s 0m00.55s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.55s \|\| +0m00.00s 0m00.55s \| Encoding/ModularWordEncodingPre \| 0m00.60s \|\| -0m00.04s 0m00.52s \| ModularArithmetic/ModularBaseSystem \| 0m00.53s \|\| -0m00.01s 0m00.44s \| ModularArithmetic/Pre \| 0m00.47s \|\| -0m00.02s 0m00.38s \| ModularArithmetic/Pow2Base \| 0m00.44s \|\| -0m00.06s 0m00.36s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.39s \|\| -0m00.03s 0m00.31s \| Spec/ModularArithmetic \| 0m00.38s \|\| -0m00.07s
\| *	More ZUtil	Jason Gross	2016-07-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 1m42.25s \| Total \| 1m43.34s \|\| -0m01.09s ---------------------------------------------------------------------------------- 0m47.63s \| Specific/GF25519 \| 0m47.32s \|\| +0m00.31s 0m11.34s \| Experiments/SpecEd25519 \| 0m11.30s \|\| +0m00.03s 0m08.26s \| Specific/GF1305 \| 0m08.34s \|\| -0m00.08s 0m03.78s \| ModularArithmetic/Pow2BaseProofs \| 0m03.81s \|\| -0m00.03s 0m03.65s \| ModularArithmetic/Tutorial \| 0m03.80s \|\| -0m00.14s 0m03.58s \| BaseSystemProofs \| 0m03.73s \|\| -0m00.14s 0m02.77s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.89s \|\| -0m00.12s 0m02.28s \| Util/ZUtil \| 0m02.27s \|\| +0m00.00s 0m01.52s \| Encoding/PointEncodingPre \| 0m01.55s \|\| -0m00.03s 0m01.47s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.55s \|\| -0m00.08s 0m01.45s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.54s \|\| -0m00.09s 0m01.15s \| ModularArithmetic/ExtendedBaseVector \| 0m01.21s \|\| -0m00.06s 0m01.13s \| BaseSystem \| 0m01.17s \|\| -0m00.04s 0m00.97s \| ModularArithmetic/ModularBaseSystemProofs \| 0m00.98s \|\| -0m00.01s 0m00.96s \| Experiments/SpecificCurve25519 \| 0m01.00s \|\| -0m00.04s 0m00.93s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.99s \|\| -0m00.05s 0m00.92s \| ModularArithmetic/BarrettReduction/Z \| 0m00.95s \|\| -0m00.02s 0m00.84s \| ModularArithmetic/ModularBaseSystemField \| 0m00.89s \|\| -0m00.05s 0m00.83s \| Util/NumTheoryUtil \| 0m00.84s \|\| -0m00.01s 0m00.73s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.74s \|\| -0m00.01s 0m00.65s \| Encoding/ModularWordEncodingTheorems \| 0m00.70s \|\| -0m00.04s 0m00.62s \| Testbit \| 0m00.63s \|\| -0m00.01s 0m00.56s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.61s \|\| -0m00.04s 0m00.56s \| Encoding/ModularWordEncodingPre \| 0m00.58s \|\| -0m00.01s 0m00.55s \| Spec/ModularWordEncoding \| 0m00.59s \|\| -0m00.03s 0m00.53s \| ModularArithmetic/ModularBaseSystemList \| 0m00.59s \|\| -0m00.05s 0m00.52s \| ModularArithmetic/ModularBaseSystem \| 0m00.54s \|\| -0m00.02s 0m00.50s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.59s \|\| -0m00.08s 0m00.46s \| ModularArithmetic/Pre \| 0m00.46s \|\| +0m00.00s 0m00.39s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.40s \|\| -0m00.01s 0m00.38s \| ModularArithmetic/Pow2Base \| 0m00.43s \|\| -0m00.04s 0m00.34s \| Spec/ModularArithmetic \| 0m00.36s \|\| -0m00.01s
\| *	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
\| *	More ZUtil lemmas	Jason Gross	2016-07-22
\| \|
\| *	Revert "Revert "Add more ZUtil automation""	Jason Gross	2016-07-22
\| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit 5d7b2bc9a4e902d3c3aa7a3625ffda6eb127011f. Now it should work fine
\| *	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
\| *	Revert "Add more ZUtil automation"	Jason Gross	2016-07-22
\| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit 29bb3dd531be45ba7960b34ef759b44436e48905. [intuition] is stupid and terrible. Fix upcoming.
\| *	Add more ZUtil automation	Jason Gross	2016-07-22
\| \|
\| *	Add ring_simplify_subterms	Jason Gross	2016-07-22
\| \|
\| *	Generalize div_sub_small a bit	Jason Gross	2016-07-22
\|/
*	Add another lemma to zarith	Jason Gross	2016-07-21
\|
*	Add another ZUtil lemma	Jason Gross	2016-07-21
\|
*	Another ZUtil lemma	Jason Gross	2016-07-21
\|
*	Fix broken proofs	Jason Gross	2016-07-21
\|
*	Add more ZUtil	Jason Gross	2016-07-21
\|
*	More ZUtil helper lemmas	Jason Gross	2016-07-21
\|
*	Add more ZUtil lemmas	Jason Gross	2016-07-21
\| \| \| \|	We really want rewrite mod AC here...
*	Add ZUtil lemmas	Jason Gross	2016-07-21
\|
*	Add Z.lt_le_incl to zarith	Jason Gross	2016-07-20
\|
*	Add another lemma about +, <= to arith	Jason Gross	2016-07-20
\|
*	Add a distr_length database	Jason Gross	2016-07-19
\|
*	Remove stuff from PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
\|
*	Add a lemma about sum_firstn	Jason Gross	2016-07-18
\|
*	Add a ListUtil lemma	Jason Gross	2016-07-18
\|
*	Fix for Coq 8.4 (missing lemmas)	Jason Gross	2016-07-18
\|
*	Fix for Coq 8.4 (omega used to be weaker)	Jason Gross	2016-07-18
\|
*	Add more natsimplify le_dec lemmas	Jason Gross	2016-07-18
\|
*	Add more NatUtil lemmas	Jason Gross	2016-07-18
\|
*	Add natsimplify lemmas about eq_nat_dec	Jason Gross	2016-07-18
\|
*	Fix some typos in the previous commit	Jason Gross	2016-07-18
\|
*	Add some lemmas about nth_default in bounds	Jason Gross	2016-07-18
\|
*	Move some definitions to Pow2Base (#24)	Jason Gross	2016-07-18
\| \| \| \| \| \| \| \| \|	* Move some definitions to Pow2Base These definitions don't depend on PseudoMersenneBaseParams, only on limb_widths, and we'll want them for BarrettReduction / P256. * Fix for Coq 8.4
*	ported IterAssocOp to use monoid rather than a billion context variables ↵	jadep	2016-07-18
\| \| \| \|	that add up to a monoid
*	Added lemmas to ZUtil and NatUtil (for Testbit)	jadep	2016-07-18
\|
*	tuple: applying functions to tuples of arbitrary length	Andres Erbsen	2016-07-12
\|
*	Merge of fixedlength and master	jadep	2016-07-11
\|\
\| *	wrap nsatz in Algebra	Andres Erbsen	2016-07-11
\| \|
\| *	[congruence] is more powerful in 8.5 than in 8.4	Andres Erbsen	2016-07-11
\| \|
\| *	merge	jadep	2016-07-10
\| \|\
\| * \|	added proofs about addition chain exponentiation for later use in ↵	jadep	2016-07-10
\| \| \| \| \| \| \| \| \| \| \| \|	ModularBaseSystem [pow], which we need for sqrt and inversion.
\| \| *	Fix ListUtil for Coq 8.4	Jason Gross	2016-07-10
\| \| \|
\| \| *	Update ListUtil	Jason Gross	2016-07-08
\| \| \|
\| \| *	Fix NatUtil for 8.4	Jason Gross	2016-07-08
\| \| \|
\| \| *	Add useful tactics and util lemmas	Jason Gross	2016-07-08
\| \| \|
\| \| *	Add a NatUtil lemma and db	Jason Gross	2016-07-08
\| \| \|