fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add a lemma about hprop and eq	Jason Gross	2016-07-29
\|
*	Make IsIso a class	Jason Gross	2016-07-29
\|
*	Add HProp, Isomorphism	Jason Gross	2016-07-29
\|
*	Add inversion helper tactics to Sigma.v	Jason Gross	2016-07-29
\|
*	Rename path_sig{,T}{ => _uncurried}_iff	Jason Gross	2016-07-29
\|
*	Add path_sig{,T}_iff	Jason Gross	2016-07-29
\|
*	Add some lemmas to Util.Sigma	Jason Gross	2016-07-29
\|
*	Set Asymmetric Patterns, add util lemmas about sig	Jason Gross	2016-07-29
\|
*	Get rid of unparsable unicode notation	Jason Gross	2016-07-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 3m22.68s \| Total \| 3m13.21s \|\| +0m09.46s ------------------------------------------------------------------------------------ 0m38.91s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m35.64s \|\| +0m03.26s 0m36.93s \| Specific/GF25519 \| 0m33.09s \|\| +0m03.83s 0m08.87s \| Specific/GF1305 \| 0m07.33s \|\| +0m01.53s 0m06.74s \| Algebra \| 0m08.08s \|\| -0m01.33s 0m04.96s \| WeierstrassCurve/Pre \| 0m06.12s \|\| -0m01.16s 0m02.58s \| Util/ZUtil \| 0m03.71s \|\| -0m01.12s 0m15.89s \| ModularArithmetic/ModularBaseSystemProofs \| 0m15.59s \|\| +0m00.30s 0m15.41s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m15.74s \|\| -0m00.33s 0m12.20s \| Experiments/SpecEd25519 \| 0m11.29s \|\| +0m00.91s 0m04.56s \| ModularArithmetic/Tutorial \| 0m03.89s \|\| +0m00.66s 0m04.41s \| BaseSystemProofs \| 0m05.04s \|\| -0m00.62s 0m04.40s \| ModularArithmetic/Pow2BaseProofs \| 0m04.21s \|\| +0m00.19s 0m04.16s \| CompleteEdwardsCurve/Pre \| 0m03.55s \|\| +0m00.61s 0m03.30s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.31s \|\| -0m00.01s 0m02.66s \| Assembly/State \| 0m02.69s \|\| -0m00.02s 0m02.29s \| Encoding/PointEncodingPre \| 0m01.57s \|\| +0m00.72s 0m02.14s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.63s \|\| +0m00.51s 0m02.00s \| Assembly/Wordize \| 0m01.90s \|\| +0m00.10s 0m01.84s \| Experiments/EdDSARefinement \| 0m01.82s \|\| +0m00.02s 0m01.77s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.66s \|\| +0m00.11s 0m01.42s \| ModularArithmetic/BarrettReduction/Z \| 0m00.97s \|\| +0m00.44s 0m01.22s \| BaseSystem \| 0m01.81s \|\| -0m00.59s 0m01.12s \| ModularArithmetic/ExtendedBaseVector \| 0m01.13s \|\| -0m00.00s 0m01.12s \| Assembly/Pseudize \| 0m01.14s \|\| -0m00.01s 0m00.97s \| Util/AdditionChainExponentiation \| 0m00.61s \|\| +0m00.36s 0m00.97s \| Assembly/Pipeline \| 0m00.62s \|\| +0m00.35s 0m00.95s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.94s \|\| +0m00.01s 0m00.94s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.57s \|\| +0m00.37s 0m00.91s \| ModularArithmetic/ModularBaseSystemField \| 0m00.92s \|\| -0m00.01s 0m00.87s \| Spec/EdDSA \| 0m00.63s \|\| +0m00.24s 0m00.85s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.84s \|\| +0m00.01s 0m00.85s \| Util/NumTheoryUtil \| 0m00.91s \|\| -0m00.06s 0m00.79s \| Assembly/QhasmEvalCommon \| 0m00.79s \|\| +0m00.00s 0m00.78s \| Spec/ModularWordEncoding \| 0m00.63s \|\| +0m00.15s 0m00.77s \| Util/IterAssocOp \| 0m00.73s \|\| +0m00.04s 0m00.70s \| Assembly/Vectorize \| 0m00.62s \|\| +0m00.07s 0m00.70s \| Experiments/SpecificCurve25519 \| 0m00.69s \|\| +0m00.01s 0m00.69s \| Assembly/PseudoConversion \| 0m00.79s \|\| -0m00.10s 0m00.67s \| Spec/WeierstrassCurve \| 0m00.44s \|\| +0m00.23s 0m00.66s \| Encoding/ModularWordEncodingTheorems \| 0m00.64s \|\| +0m00.02s 0m00.65s \| Encoding/ModularWordEncodingPre \| 0m00.67s \|\| -0m00.02s 0m00.65s \| Testbit \| 0m00.69s \|\| -0m00.03s 0m00.62s \| ModularArithmetic/Pow2Base \| 0m00.41s \|\| +0m00.21s 0m00.62s \| Assembly/StringConversion \| 0m00.74s \|\| -0m00.12s 0m00.62s \| Assembly/Pseudo \| 0m00.83s \|\| -0m00.20s 0m00.62s \| ModularArithmetic/ModularBaseSystem \| 0m00.60s \|\| +0m00.02s 0m00.61s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.63s \|\| -0m00.02s 0m00.60s \| ModularArithmetic/ModularBaseSystemList \| 0m00.59s \|\| +0m00.01s 0m00.55s \| Assembly/Qhasm \| 0m00.55s \|\| +0m00.00s 0m00.54s \| Assembly/AlmostQhasm \| 0m00.48s \|\| +0m00.06s 0m00.49s \| ModularArithmetic/Pre \| 0m00.49s \|\| +0m00.00s 0m00.48s \| Assembly/QhasmUtil \| 0m00.48s \|\| +0m00.00s 0m00.46s \| Assembly/AlmostConversion \| 0m00.47s \|\| -0m00.00s 0m00.42s \| Spec/CompleteEdwardsCurve \| 0m00.43s \|\| -0m00.01s 0m00.40s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.40s \|\| +0m00.00s 0m00.35s \| Spec/ModularArithmetic \| 0m00.45s \|\| -0m00.10s 0m00.03s \| Util/Notations \| 0m00.03s \|\| +0m00.00s
*	Add more reserved notations	Jason Gross	2016-07-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 3m14.96s \| Total \| 3m18.23s \|\| -0m03.26s ------------------------------------------------------------------------------------ 0m11.32s \| Experiments/SpecEd25519 \| 0m13.08s \|\| -0m01.75s 0m03.38s \| ModularArithmetic/ModularBaseSystemOpt \| 0m05.18s \|\| -0m01.79s 0m37.46s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m36.70s \|\| +0m00.75s 0m33.52s \| Specific/GF25519 \| 0m34.26s \|\| -0m00.73s 0m16.05s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m15.79s \|\| +0m00.26s 0m15.57s \| ModularArithmetic/ModularBaseSystemProofs \| 0m15.57s \|\| +0m00.00s 0m07.56s \| Specific/GF1305 \| 0m07.69s \|\| -0m00.13s 0m06.05s \| Algebra \| 0m06.11s \|\| -0m00.06s 0m04.81s \| WeierstrassCurve/Pre \| 0m04.99s \|\| -0m00.18s 0m04.64s \| ModularArithmetic/Pow2BaseProofs \| 0m04.51s \|\| +0m00.12s 0m04.17s \| CompleteEdwardsCurve/Pre \| 0m03.83s \|\| +0m00.33s 0m03.97s \| BaseSystemProofs \| 0m04.48s \|\| -0m00.51s 0m03.75s \| ModularArithmetic/Tutorial \| 0m03.75s \|\| +0m00.00s 0m03.24s \| Assembly/State \| 0m02.65s \|\| +0m00.59s 0m02.74s \| Experiments/EdDSARefinement \| 0m02.60s \|\| +0m00.14s 0m02.70s \| Assembly/Wordize \| 0m01.86s \|\| +0m00.84s 0m02.44s \| Util/ZUtil \| 0m02.42s \|\| +0m00.02s 0m01.74s \| ModularArithmetic/ExtendedBaseVector \| 0m01.22s \|\| +0m00.52s 0m01.62s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.70s \|\| -0m00.07s 0m01.58s \| Encoding/PointEncodingPre \| 0m02.29s \|\| -0m00.71s 0m01.55s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.68s \|\| -0m00.12s 0m01.30s \| Util/NumTheoryUtil \| 0m00.95s \|\| +0m00.35s 0m01.18s \| BaseSystem \| 0m01.19s \|\| -0m00.01s 0m01.18s \| Assembly/Pseudize \| 0m01.36s \|\| -0m00.18s 0m01.01s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.82s \|\| +0m00.19s 0m00.95s \| ModularArithmetic/BarrettReduction/Z \| 0m00.95s \|\| +0m00.00s 0m00.94s \| ModularArithmetic/ModularBaseSystemList \| 0m00.96s \|\| -0m00.02s 0m00.94s \| Assembly/PseudoConversion \| 0m00.85s \|\| +0m00.08s 0m00.93s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.01s \|\| -0m00.07s 0m00.93s \| ModularArithmetic/ModularBaseSystemField \| 0m01.34s \|\| -0m00.41s 0m00.93s \| Spec/EdDSA \| 0m00.63s \|\| +0m00.30s 0m00.84s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m01.30s \|\| -0m00.46s 0m00.83s \| Assembly/QhasmEvalCommon \| 0m00.87s \|\| -0m00.04s 0m00.71s \| Util/IterAssocOp \| 0m01.03s \|\| -0m00.32s 0m00.71s \| Assembly/QhasmUtil \| 0m00.50s \|\| +0m00.20s 0m00.69s \| Assembly/Vectorize \| 0m00.46s \|\| +0m00.22s 0m00.69s \| Experiments/SpecificCurve25519 \| 0m00.68s \|\| +0m00.00s 0m00.67s \| Assembly/Pipeline \| 0m00.66s \|\| +0m00.01s 0m00.67s \| Assembly/AlmostConversion \| 0m00.43s \|\| +0m00.24s 0m00.66s \| Encoding/ModularWordEncodingTheorems \| 0m00.64s \|\| +0m00.02s 0m00.64s \| Util/AdditionChainExponentiation \| 0m00.93s \|\| -0m00.29s 0m00.62s \| Assembly/Pseudo \| 0m00.65s \|\| -0m00.03s 0m00.62s \| Testbit \| 0m00.64s \|\| -0m00.02s 0m00.61s \| ModularArithmetic/ModularBaseSystem \| 0m00.61s \|\| +0m00.00s 0m00.60s \| Encoding/ModularWordEncodingPre \| 0m00.63s \|\| -0m00.03s 0m00.60s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.53s \|\| +0m00.06s 0m00.56s \| Spec/ModularWordEncoding \| 0m00.62s \|\| -0m00.05s 0m00.56s \| Assembly/StringConversion \| 0m00.63s \|\| -0m00.06s 0m00.48s \| Spec/WeierstrassCurve \| 0m00.44s \|\| +0m00.03s 0m00.48s \| Assembly/AlmostQhasm \| 0m00.58s \|\| -0m00.09s 0m00.48s \| Assembly/Qhasm \| 0m00.58s \|\| -0m00.09s 0m00.45s \| ModularArithmetic/Pre \| 0m00.52s \|\| -0m00.07s 0m00.42s \| Spec/CompleteEdwardsCurve \| 0m00.43s \|\| -0m00.01s 0m00.41s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.38s \|\| +0m00.02s 0m00.40s \| ModularArithmetic/Pow2Base \| 0m00.46s \|\| -0m00.06s 0m00.38s \| Spec/ModularArithmetic \| 0m00.58s \|\| -0m00.19s 0m00.03s \| Util/Notations \| 0m00.03s \|\| +0m00.00s
*	Add instances about congruence modulo	Jason Gross	2016-07-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 1m44.65s \| Total \| 1m56.10s \|\| -0m11.44s ---------------------------------------------------------------------------------- 0m32.68s \| Specific/GF25519 \| 0m34.42s \|\| -0m01.74s 0m07.28s \| Specific/GF1305 \| 0m08.30s \|\| -0m01.02s 0m03.89s \| BaseSystemProofs \| 0m04.91s \|\| -0m01.02s 0m03.80s \| ModularArithmetic/Tutorial \| 0m05.65s \|\| -0m01.85s 0m15.65s \| ModularArithmetic/ModularBaseSystemProofs \| 0m16.40s \|\| -0m00.74s 0m11.87s \| Experiments/SpecEd25519 \| 0m12.04s \|\| -0m00.16s 0m04.08s \| ModularArithmetic/Pow2BaseProofs \| 0m04.81s \|\| -0m00.72s 0m03.22s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.37s \|\| -0m00.14s 0m02.44s \| Util/ZUtil \| 0m02.46s \|\| -0m00.02s 0m02.31s \| Encoding/PointEncodingPre \| 0m02.32s \|\| -0m00.00s 0m01.56s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.88s \|\| -0m00.31s 0m01.55s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.30s \|\| -0m00.74s 0m01.20s \| BaseSystem \| 0m01.86s \|\| -0m00.66s 0m01.15s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.07s \|\| +0m00.07s 0m01.08s \| ModularArithmetic/ExtendedBaseVector \| 0m01.23s \|\| -0m00.14s 0m00.95s \| ModularArithmetic/BarrettReduction/Z \| 0m01.03s \|\| -0m00.08s 0m00.90s \| Util/NumTheoryUtil \| 0m01.29s \|\| -0m00.39s 0m00.89s \| ModularArithmetic/ModularBaseSystemField \| 0m00.93s \|\| -0m00.04s 0m00.80s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.84s \|\| -0m00.03s 0m00.70s \| Experiments/SpecificCurve25519 \| 0m00.72s \|\| -0m00.02s 0m00.69s \| Encoding/ModularWordEncodingTheorems \| 0m00.98s \|\| -0m00.29s 0m00.66s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.68s \|\| -0m00.02s 0m00.63s \| Testbit \| 0m00.71s \|\| -0m00.07s 0m00.62s \| Encoding/ModularWordEncodingPre \| 0m00.95s \|\| -0m00.32s 0m00.61s \| ModularArithmetic/ModularBaseSystemList \| 0m00.63s \|\| -0m00.02s 0m00.60s \| Spec/ModularWordEncoding \| 0m00.63s \|\| -0m00.03s 0m00.59s \| ModularArithmetic/ModularBaseSystem \| 0m00.57s \|\| +0m00.02s 0m00.57s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.81s \|\| -0m00.24s 0m00.49s \| ModularArithmetic/Pre \| 0m00.71s \|\| -0m00.21s 0m00.42s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.58s \|\| -0m00.15s 0m00.40s \| ModularArithmetic/Pow2Base \| 0m00.46s \|\| -0m00.06s 0m00.38s \| Spec/ModularArithmetic \| 0m00.56s \|\| -0m00.18s
*	Add unicode reserved notations	Jason Gross	2016-07-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 3m17.30s \| Total \| 3m15.15s \|\| +0m02.15s ------------------------------------------------------------------------------------ 0m05.13s \| WeierstrassCurve/Pre \| 0m06.46s \|\| -0m01.33s 0m04.64s \| CompleteEdwardsCurve/Pre \| 0m03.48s \|\| +0m01.15s 0m04.39s \| ModularArithmetic/Pow2BaseProofs \| 0m05.95s \|\| -0m01.56s 0m36.30s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m35.39s \|\| +0m00.90s 0m33.32s \| Specific/GF25519 \| 0m33.98s \|\| -0m00.65s 0m16.42s \| ModularArithmetic/ModularBaseSystemProofs \| 0m16.07s \|\| +0m00.35s 0m16.08s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m16.77s \|\| -0m00.69s 0m11.33s \| Experiments/SpecEd25519 \| 0m11.31s \|\| +0m00.01s 0m07.29s \| Specific/GF1305 \| 0m07.25s \|\| +0m00.04s 0m07.17s \| Algebra \| 0m06.25s \|\| +0m00.92s 0m04.22s \| ModularArithmetic/Tutorial \| 0m04.27s \|\| -0m00.04s 0m03.99s \| BaseSystemProofs \| 0m03.84s \|\| +0m00.15s 0m03.36s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.35s \|\| +0m00.00s 0m02.83s \| Assembly/State \| 0m02.73s \|\| +0m00.10s 0m02.51s \| Util/ZUtil \| 0m02.42s \|\| +0m00.08s 0m02.30s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.63s \|\| +0m00.67s 0m01.92s \| Experiments/EdDSARefinement \| 0m01.87s \|\| +0m00.04s 0m01.89s \| BaseSystem \| 0m01.20s \|\| +0m00.69s 0m01.87s \| Assembly/Wordize \| 0m01.89s \|\| -0m00.01s 0m01.64s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.61s \|\| +0m00.02s 0m01.61s \| Assembly/Pseudize \| 0m01.77s \|\| -0m00.15s 0m01.56s \| Encoding/PointEncodingPre \| 0m01.80s \|\| -0m00.24s 0m01.38s \| ModularArithmetic/ModularBaseSystemField \| 0m00.90s \|\| +0m00.47s 0m01.15s \| ModularArithmetic/ExtendedBaseVector \| 0m01.44s \|\| -0m00.29s 0m01.02s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.95s \|\| +0m00.07s 0m00.99s \| ModularArithmetic/BarrettReduction/Z \| 0m01.00s \|\| -0m00.01s 0m00.99s \| Encoding/ModularWordEncodingPre \| 0m00.62s \|\| +0m00.37s 0m00.98s \| ModularArithmetic/ModularBaseSystemList \| 0m00.90s \|\| +0m00.07s 0m00.96s \| Assembly/Pipeline \| 0m00.65s \|\| +0m00.30s 0m00.93s \| Util/AdditionChainExponentiation \| 0m00.62s \|\| +0m00.31s 0m00.92s \| Spec/EdDSA \| 0m00.61s \|\| +0m00.31s 0m00.91s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.92s \|\| -0m00.01s 0m00.90s \| Util/NumTheoryUtil \| 0m00.89s \|\| +0m00.01s 0m00.89s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.94s \|\| -0m00.04s 0m00.88s \| Assembly/Pseudo \| 0m00.63s \|\| +0m00.25s 0m00.87s \| Assembly/QhasmEvalCommon \| 0m00.83s \|\| +0m00.04s 0m00.78s \| Assembly/StringConversion \| 0m00.54s \|\| +0m00.24s 0m00.71s \| Experiments/SpecificCurve25519 \| 0m00.73s \|\| -0m00.02s 0m00.69s \| Util/IterAssocOp \| 0m00.73s \|\| -0m00.04s 0m00.68s \| Assembly/AlmostQhasm \| 0m00.55s \|\| +0m00.13s 0m00.68s \| Assembly/PseudoConversion \| 0m00.73s \|\| -0m00.04s 0m00.67s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.63s \|\| +0m00.04s 0m00.67s \| ModularArithmetic/Pre \| 0m00.45s \|\| +0m00.22s 0m00.64s \| Testbit \| 0m00.90s \|\| -0m00.26s 0m00.64s \| Encoding/ModularWordEncodingTheorems \| 0m00.67s \|\| -0m00.03s 0m00.63s \| Spec/ModularWordEncoding \| 0m00.83s \|\| -0m00.19s 0m00.59s \| ModularArithmetic/ModularBaseSystem \| 0m00.56s \|\| +0m00.02s 0m00.53s \| Spec/ModularArithmetic \| 0m00.47s \|\| +0m00.06s 0m00.53s \| Assembly/Qhasm \| 0m00.55s \|\| -0m00.02s 0m00.52s \| ModularArithmetic/Pow2Base \| 0m00.41s \|\| +0m00.11s 0m00.51s \| Assembly/QhasmUtil \| 0m00.45s \|\| +0m00.06s 0m00.49s \| Assembly/AlmostConversion \| 0m00.49s \|\| +0m00.00s 0m00.48s \| Assembly/Vectorize \| 0m00.70s \|\| -0m00.21s 0m00.46s \| Spec/WeierstrassCurve \| 0m00.70s \|\| -0m00.23s 0m00.43s \| Spec/CompleteEdwardsCurve \| 0m00.43s \|\| +0m00.00s 0m00.40s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.40s \|\| +0m00.00s 0m00.03s \| Util/Notations \| 0m00.04s \|\| -0m00.01s
*	Add Z.mod_mod to zsimplify	Jason Gross	2016-07-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 1m46.76s \| Total \| 1m47.10s \|\| -0m00.33s ---------------------------------------------------------------------------------- 0m05.21s \| ModularArithmetic/Tutorial \| 0m03.82s \|\| +0m01.39s 0m04.09s \| ModularArithmetic/Pow2BaseProofs \| 0m05.39s \|\| -0m01.29s 0m33.15s \| Specific/GF25519 \| 0m33.13s \|\| +0m00.01s 0m15.42s \| ModularArithmetic/ModularBaseSystemProofs \| 0m15.68s \|\| -0m00.25s 0m12.24s \| Experiments/SpecEd25519 \| 0m11.94s \|\| +0m00.30s 0m07.30s \| Specific/GF1305 \| 0m07.36s \|\| -0m00.06s 0m03.96s \| BaseSystemProofs \| 0m03.93s \|\| +0m00.02s 0m03.26s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.26s \|\| +0m00.00s 0m02.38s \| Util/ZUtil \| 0m02.47s \|\| -0m00.09s 0m01.64s \| Encoding/PointEncodingPre \| 0m01.55s \|\| +0m00.08s 0m01.58s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.64s \|\| -0m00.05s 0m01.55s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.59s \|\| -0m00.04s 0m01.19s \| BaseSystem \| 0m01.18s \|\| +0m00.01s 0m01.18s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.43s \|\| -0m00.25s 0m01.14s \| ModularArithmetic/ExtendedBaseVector \| 0m01.18s \|\| -0m00.04s 0m00.95s \| ModularArithmetic/BarrettReduction/Z \| 0m01.08s \|\| -0m00.13s 0m00.93s \| ModularArithmetic/ModularBaseSystemField \| 0m01.10s \|\| -0m00.17s 0m00.89s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.64s \|\| +0m00.25s 0m00.87s \| Util/NumTheoryUtil \| 0m00.91s \|\| -0m00.04s 0m00.85s \| Encoding/ModularWordEncodingTheorems \| 0m00.69s \|\| +0m00.16s 0m00.82s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.85s \|\| -0m00.03s 0m00.72s \| Experiments/SpecificCurve25519 \| 0m00.72s \|\| +0m00.00s 0m00.66s \| Testbit \| 0m00.66s \|\| +0m00.00s 0m00.61s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.59s \|\| +0m00.02s 0m00.61s \| ModularArithmetic/ModularBaseSystem \| 0m00.69s \|\| -0m00.07s 0m00.60s \| ModularArithmetic/ModularBaseSystemList \| 0m00.60s \|\| +0m00.00s 0m00.59s \| Spec/ModularWordEncoding \| 0m00.59s \|\| +0m00.00s 0m00.59s \| Encoding/ModularWordEncodingPre \| 0m00.62s \|\| -0m00.03s 0m00.58s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.58s \|\| +0m00.00s 0m00.46s \| ModularArithmetic/Pre \| 0m00.47s \|\| -0m00.00s 0m00.40s \| ModularArithmetic/Pow2Base \| 0m00.42s \|\| -0m00.01s 0m00.35s \| Spec/ModularArithmetic \| 0m00.35s \|\| +0m00.00s
*	Move most notation level declarations into Util	Jason Gross	2016-07-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reveals and prevents notation clashes. Notable breakage: - `x {{ y }}` breaks `Context {forall x, {P x} + {~P x}}.` (@jadephilipoom) - `x [[ y ]]` breaks `destruct x as [[a]\|[b]].` (@jadephilipoom) - `O :( A , B ): :?: L ::: R` breaks `((1):nat)` and `constr:(nat)` (@varomodt) After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 3m16.07s \| Total \| 3m23.63s \|\| -0m07.55s ------------------------------------------------------------------------------------ 0m16.90s \| ModularArithmetic/ModularBaseSystemProofs \| 0m19.02s \|\| -0m02.12s 0m03.29s \| ModularArithmetic/ModularBaseSystemOpt \| 0m05.30s \|\| -0m02.00s 0m12.04s \| Experiments/SpecEd25519 \| 0m13.89s \|\| -0m01.85s 0m36.02s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m36.12s \|\| -0m00.09s 0m34.48s \| Specific/GF25519 \| 0m34.27s \|\| +0m00.20s 0m15.62s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m15.76s \|\| -0m00.14s 0m07.36s \| Specific/GF1305 \| 0m07.34s \|\| +0m00.02s 0m06.64s \| Algebra \| 0m06.14s \|\| +0m00.50s 0m05.12s \| WeierstrassCurve/Pre \| 0m05.09s \|\| +0m00.03s 0m04.58s \| ModularArithmetic/Tutorial \| 0m03.83s \|\| +0m00.75s 0m04.46s \| BaseSystemProofs \| 0m04.33s \|\| +0m00.12s 0m04.26s \| ModularArithmetic/Pow2BaseProofs \| 0m05.16s \|\| -0m00.90s 0m03.91s \| CompleteEdwardsCurve/Pre \| 0m04.62s \|\| -0m00.71s 0m02.75s \| Assembly/State \| 0m03.12s \|\| -0m00.37s 0m02.55s \| Experiments/EdDSARefinement \| 0m01.85s \|\| +0m00.69s 0m02.46s \| Util/ZUtil \| 0m02.45s \|\| +0m00.00s 0m01.86s \| Assembly/Wordize \| 0m02.02s \|\| -0m00.15s 0m01.68s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.68s \|\| +0m00.00s 0m01.67s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.96s \|\| -0m00.29s 0m01.50s \| Encoding/PointEncodingPre \| 0m02.20s \|\| -0m00.70s 0m01.46s \| ModularArithmetic/BarrettReduction/Z \| 0m01.02s \|\| +0m00.43s 0m01.26s \| BaseSystem \| 0m01.21s \|\| +0m00.05s 0m01.24s \| Assembly/Pseudize \| 0m01.22s \|\| +0m00.02s 0m01.20s \| ModularArithmetic/ExtendedBaseVector \| 0m01.86s \|\| -0m00.66s 0m01.04s \| Util/IterAssocOp \| 0m00.74s \|\| +0m00.30s 0m00.96s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.67s \|\| +0m00.28s 0m00.96s \| Assembly/Pipeline \| 0m00.65s \|\| +0m00.30s 0m00.93s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.98s \|\| -0m00.04s 0m00.93s \| ModularArithmetic/ModularBaseSystemField \| 0m00.95s \|\| -0m00.01s 0m00.92s \| Util/NumTheoryUtil \| 0m01.19s \|\| -0m00.26s 0m00.90s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.89s \|\| +0m00.01s 0m00.82s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.95s \|\| -0m00.13s 0m00.81s \| Assembly/QhasmEvalCommon \| 0m00.86s \|\| -0m00.04s 0m00.80s \| Assembly/StringConversion \| 0m00.60s \|\| +0m00.20s 0m00.79s \| Assembly/Qhasm \| 0m00.54s \|\| +0m00.25s 0m00.73s \| Assembly/Pseudo \| 0m00.98s \|\| -0m00.25s 0m00.72s \| Util/AdditionChainExponentiation \| 0m00.92s \|\| -0m00.20s 0m00.69s \| Experiments/SpecificCurve25519 \| 0m00.72s \|\| -0m00.03s 0m00.65s \| Spec/ModularWordEncoding \| 0m00.85s \|\| -0m00.19s 0m00.65s \| ModularArithmetic/ModularBaseSystemList \| 0m00.68s \|\| -0m00.03s 0m00.65s \| Assembly/PseudoConversion \| 0m00.67s \|\| -0m00.02s 0m00.64s \| Encoding/ModularWordEncodingPre \| 0m00.62s \|\| +0m00.02s 0m00.64s \| Spec/EdDSA \| 0m00.93s \|\| -0m00.29s 0m00.64s \| Testbit \| 0m00.94s \|\| -0m00.29s 0m00.63s \| Encoding/ModularWordEncodingTheorems \| 0m00.66s \|\| -0m00.03s 0m00.62s \| Assembly/AlmostQhasm \| 0m00.49s \|\| +0m00.13s 0m00.59s \| ModularArithmetic/ModularBaseSystem \| 0m00.61s \|\| -0m00.02s 0m00.49s \| Spec/WeierstrassCurve \| 0m00.43s \|\| +0m00.06s 0m00.49s \| Assembly/QhasmUtil \| 0m00.51s \|\| -0m00.02s 0m00.49s \| ModularArithmetic/Pre \| 0m00.47s \|\| +0m00.02s 0m00.47s \| Assembly/Vectorize \| 0m00.51s \|\| -0m00.04s 0m00.46s \| Assembly/AlmostConversion \| 0m00.44s \|\| +0m00.02s 0m00.42s \| ModularArithmetic/Pow2Base \| 0m00.42s \|\| +0m00.00s 0m00.41s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.45s \|\| -0m00.04s 0m00.41s \| Spec/ModularArithmetic \| 0m00.41s \|\| +0m00.00s 0m00.39s \| Spec/CompleteEdwardsCurve \| 0m00.41s \|\| -0m00.01s 0m00.03s \| Util/Notations \| 0m00.03s \|\| +0m00.00s
*	Restore functionality of Z.simplify_fractions_le	Jason Gross	2016-07-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 1m47.80s \| Total \| 1m48.25s \|\| -0m00.45s ---------------------------------------------------------------------------------- 0m34.29s \| Specific/GF25519 \| 0m34.05s \|\| +0m00.24s 0m15.82s \| ModularArithmetic/ModularBaseSystemProofs \| 0m15.44s \|\| +0m00.38s 0m11.45s \| Experiments/SpecEd25519 \| 0m11.70s \|\| -0m00.25s 0m07.79s \| Specific/GF1305 \| 0m07.10s \|\| +0m00.69s 0m04.18s \| ModularArithmetic/Tutorial \| 0m04.69s \|\| -0m00.51s 0m04.07s \| ModularArithmetic/Pow2BaseProofs \| 0m04.62s \|\| -0m00.54s 0m03.75s \| BaseSystemProofs \| 0m03.95s \|\| -0m00.20s 0m03.23s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.22s \|\| +0m00.00s 0m02.40s \| Util/ZUtil \| 0m02.37s \|\| +0m00.02s 0m01.66s \| BaseSystem \| 0m01.23s \|\| +0m00.42s 0m01.65s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.61s \|\| +0m00.03s 0m01.65s \| Encoding/PointEncodingPre \| 0m01.54s \|\| +0m00.10s 0m01.59s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.56s \|\| +0m00.03s 0m01.40s \| Util/NumTheoryUtil \| 0m01.34s \|\| +0m00.05s 0m01.12s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.49s \|\| -0m00.36s 0m01.12s \| ModularArithmetic/ExtendedBaseVector \| 0m01.12s \|\| +0m00.00s 0m00.96s \| ModularArithmetic/BarrettReduction/Z \| 0m01.41s \|\| -0m00.44s 0m00.91s \| ModularArithmetic/ModularBaseSystemField \| 0m00.89s \|\| +0m00.02s 0m00.81s \| Testbit \| 0m00.67s \|\| +0m00.14s 0m00.80s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.85s \|\| -0m00.04s 0m00.77s \| Experiments/SpecificCurve25519 \| 0m00.77s \|\| +0m00.00s 0m00.74s \| Encoding/ModularWordEncodingTheorems \| 0m00.71s \|\| +0m00.03s 0m00.65s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.63s \|\| +0m00.02s 0m00.64s \| ModularArithmetic/ModularBaseSystemList \| 0m00.59s \|\| +0m00.05s 0m00.63s \| Encoding/ModularWordEncodingPre \| 0m00.92s \|\| -0m00.29s 0m00.61s \| Spec/ModularWordEncoding \| 0m00.60s \|\| +0m00.01s 0m00.61s \| ModularArithmetic/Pre \| 0m00.52s \|\| +0m00.08s 0m00.60s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.58s \|\| +0m00.02s 0m00.58s \| ModularArithmetic/ModularBaseSystem \| 0m00.55s \|\| +0m00.02s 0m00.53s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.53s \|\| +0m00.00s 0m00.43s \| ModularArithmetic/Pow2Base \| 0m00.64s \|\| -0m00.21s 0m00.36s \| Spec/ModularArithmetic \| 0m00.36s \|\| +0m00.00s
*	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.6 build	Jason Gross	2016-07-26
\| \| \| \| \|	Terrible, horrible, no good, very bad bugs in Coq. https://coq.inria.fr/bugs/show_bug.cgi?id=4966
*	Fix 8.4 build.	jadep	2016-07-25
\|
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-25
\|\
* \|	Put ModularBaseSystem carries in terms of [carry_gen], and pushed this ↵	jadep	2016-07-25
\| \| \| \| \| \| \| \|	change through the pipeline. Also began the process of redoing canonicalization proofs, attempting to put the messy case analysis in theorem statements rather than separate lemmas.
* \|	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 databases for ring_simplify	Jason Gross	2016-07-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 2m39.49s \| Total \| 2m36.24s \|\| +0m03.25s ------------------------------------------------------------------------------------ 0m48.49s \| Specific/GF25519 \| 0m48.53s \|\| -0m00.03s 0m34.52s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m34.24s \|\| +0m00.28s 0m15.71s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m15.24s \|\| +0m00.47s 0m11.41s \| Experiments/SpecEd25519 \| 0m11.34s \|\| +0m00.07s 0m08.23s \| Specific/GF1305 \| 0m08.30s \|\| -0m00.07s 0m05.64s \| Algebra \| 0m05.55s \|\| +0m00.08s 0m05.03s \| WeierstrassCurve/Pre \| 0m04.51s \|\| +0m00.52s 0m04.23s \| ModularArithmetic/Tutorial \| 0m03.63s \|\| +0m00.60s 0m03.33s \| CompleteEdwardsCurve/Pre \| 0m03.34s \|\| -0m00.00s 0m02.87s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.80s \|\| +0m00.07s 0m01.80s \| Experiments/EdDSARefinement \| 0m01.77s \|\| +0m00.03s 0m01.54s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.55s \|\| -0m00.01s 0m01.52s \| Encoding/PointEncodingPre \| 0m01.54s \|\| -0m00.02s 0m01.51s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.51s \|\| +0m00.00s 0m01.19s \| ModularArithmetic/ExtendedBaseVector \| 0m01.18s \|\| +0m00.01s 0m01.16s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.80s \|\| +0m00.35s 0m01.03s \| ModularArithmetic/ModularBaseSystemProofs \| 0m00.96s \|\| +0m00.07s 0m00.95s \| Experiments/SpecificCurve25519 \| 0m00.95s \|\| +0m00.00s 0m00.92s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.85s \|\| +0m00.07s 0m00.91s \| ModularArithmetic/ModularBaseSystemField \| 0m00.86s \|\| +0m00.05s 0m00.76s \| Encoding/ModularWordEncodingPre \| 0m00.60s \|\| +0m00.16s 0m00.69s \| Util/IterAssocOp \| 0m00.67s \|\| +0m00.01s 0m00.69s \| ModularArithmetic/ModularBaseSystemList \| 0m00.57s \|\| +0m00.12s 0m00.68s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.63s \|\| +0m00.05s 0m00.68s \| Spec/EdDSA \| 0m00.61s \|\| +0m00.07s 0m00.67s \| Encoding/ModularWordEncodingTheorems \| 0m00.64s \|\| +0m00.03s 0m00.66s \| Spec/ModularWordEncoding \| 0m00.56s \|\| +0m00.09s 0m00.62s \| Util/AdditionChainExponentiation \| 0m00.59s \|\| +0m00.03s 0m00.58s \| ModularArithmetic/ModularBaseSystem \| 0m00.57s \|\| +0m00.01s 0m00.55s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.54s \|\| +0m00.01s 0m00.51s \| Spec/WeierstrassCurve \| 0m00.43s \|\| +0m00.08s 0m00.41s \| Spec/CompleteEdwardsCurve \| 0m00.38s \|\| +0m00.02s
\| *	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
\|/
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-21
\|\
* \|	Fix 8.4{pl1,pl2} builds	jadep	2016-07-21
\| \|
\| *	Add another lemma to zarith	Jason Gross	2016-07-21
\| \|
* \|	Changed name of [carry_and_reduce_single] to [carry_single], since it does ↵	jadep	2016-07-21
\| \| \| \| \| \| \| \|	not perform reduction
\| *	Split up proof in BarrettReduction.Z	Jason Gross	2016-07-21
\| \| \| \| \| \| \| \| \| \| \| \|	In particular, we do equality reasoning in one place and inequality reasoning in another. This makes it very clear how the inequality reasoning follows from the equality reasoning.
\| *	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
\|/
*	Removed lingering print statement.	jadep	2016-07-21
\|
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-21
\|\
* \|	Fixes #29	jadep	2016-07-21
\| \|
* \|	re-introduced extra field isomorphism layer for 8.4 compatibility and better ↵	jadep	2016-07-21
\| \| \| \| \| \| \| \|	organization of reasoning.
\| *	ed25519 spec: small cleanup	Andres Erbsen	2016-07-21
\| \|