fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add path_prod_eta	Jason Gross	2016-09-03
\|
*	Make [inversion_option] work on Prop options	Jason Gross	2016-09-03
\|
*	Reserve λ notation	Jason Gross	2016-09-02
\|
*	Add reserved syntax-let notation	Jason Gross	2016-09-02
\|
*	Don't zeta-reduce in [simplify_projections]	Jason Gross	2016-09-02
\|
*	Add prod_beq	Jason Gross	2016-09-02
\|
*	Strip <infomsg>; it messes things up in Coq 8.6 display	Jason Gross	2016-09-02
\|
*	Slightly better cfail	Jason Gross	2016-09-02
\|
*	Add cfail{2,3}	Jason Gross	2016-09-02
\|
*	Add [idtac_goal]	Jason Gross	2016-09-02
\|
*	Add constr-based idtac tactics	Jason Gross	2016-09-02
\|
*	Add another reserved notation	Jason Gross	2016-09-01
\|
*	Add more reserved infixes	Jason Gross	2016-08-31
\|
*	Rename congrunce_option to inversion_option, add [inversion_prod]	Jason Gross	2016-08-31
\|
*	Add congruence_option tactic	Jason Gross	2016-08-31
\|
*	Removed lingering SearchAbout.	jadep	2016-08-31
\|
*	Defined an equality comparison for tuples that uses bool instead of Prop ↵	jadep	2016-08-31
\| \| \| \|	(like Z.eqb). This is necessary for the runtime equality comparison on tuples that will appear in square root calculations during point-decoding.
*	Integrate suggestions from Andres	Jason Gross	2016-08-25
\|
*	More zarith	Jason Gross	2016-08-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 2m59.90s \| Total \| 2m45.43s \|\| +0m14.46s ---------------------------------------------------------------------------------- 0m47.27s \| ModularArithmetic/Pow2BaseProofs \| 0m37.78s \|\| +0m09.49s 0m11.27s \| ModularArithmetic/Montgomery/ZProofs \| 0m09.44s \|\| +0m01.83s 0m17.72s \| ModularArithmetic/ModularBaseSystemProofs \| 0m17.72s \|\| +0m00.00s 0m13.74s \| Experiments/SpecEd25519 \| 0m13.85s \|\| -0m00.10s 0m12.31s \| Specific/GF25519 \| 0m12.16s \|\| +0m00.15s 0m11.55s \| Util/ZUtil \| 0m11.60s \|\| -0m00.04s 0m09.67s \| Testbit \| 0m08.91s \|\| +0m00.75s 0m07.47s \| Specific/GF1305 \| 0m07.60s \|\| -0m00.12s 0m05.37s \| BaseSystemProofs \| 0m04.60s \|\| +0m00.77s 0m04.17s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m03.98s \|\| +0m00.18s 0m03.70s \| ModularArithmetic/Tutorial \| 0m03.70s \|\| +0m00.00s 0m03.48s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m04.13s \|\| -0m00.64s 0m03.32s \| Experiments/SpecificCurve25519 \| 0m03.34s \|\| -0m00.02s 0m03.12s \| ModularArithmetic/ModularArithmeticTheorems \| 0m03.00s \|\| +0m00.12s 0m02.55s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.37s \|\| +0m00.17s 0m02.41s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.36s \|\| +0m00.05s 0m02.08s \| ModularArithmetic/BarrettReduction/Z \| 0m02.06s \|\| +0m00.02s 0m01.97s \| Encoding/PointEncodingPre \| 0m01.68s \|\| +0m00.29s 0m01.66s \| BaseSystem \| 0m01.26s \|\| +0m00.39s 0m01.55s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.17s \|\| +0m00.38s 0m01.40s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.25s \|\| +0m00.14s 0m01.28s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.83s \|\| +0m00.45s 0m01.21s \| ModularArithmetic/ExtendedBaseVector \| 0m01.15s \|\| +0m00.06s 0m01.00s \| Util/NumTheoryUtil \| 0m00.88s \|\| +0m00.12s 0m00.98s \| ModularArithmetic/Montgomery/ZBounded \| 0m00.97s \|\| +0m00.01s 0m00.75s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.71s \|\| +0m00.04s 0m00.70s \| Encoding/ModularWordEncodingPre \| 0m00.65s \|\| +0m00.04s 0m00.69s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.78s \|\| -0m00.09s 0m00.68s \| Encoding/ModularWordEncodingTheorems \| 0m01.00s \|\| -0m00.31s 0m00.66s \| ModularArithmetic/ModularBaseSystemList \| 0m00.67s \|\| -0m00.01s 0m00.64s \| ModularArithmetic/ModularBaseSystem \| 0m00.61s \|\| +0m00.03s 0m00.63s \| ModularArithmetic/ZBounded \| 0m00.44s \|\| +0m00.19s 0m00.60s \| ModularArithmetic/Montgomery/Z \| 0m00.50s \|\| +0m00.09s 0m00.57s \| Spec/ModularWordEncoding \| 0m00.57s \|\| +0m00.00s 0m00.50s \| ModularArithmetic/Pre \| 0m00.52s \|\| -0m00.02s 0m00.46s \| ModularArithmetic/Pow2Base \| 0m00.43s \|\| +0m00.03s 0m00.40s \| Spec/ModularArithmetic \| 0m00.36s \|\| +0m00.04s 0m00.38s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.41s \|\| -0m00.02s
*	Add more reserved notations	Jason Gross	2016-08-24
\|
*	Fewer side-conditions on zsimplify	Jason Gross	2016-08-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 3m23.91s \| Total \| 3m03.61s \|\| +0m20.30s ---------------------------------------------------------------------------------- 0m52.44s \| ModularArithmetic/Pow2BaseProofs \| 0m38.87s \|\| +0m13.57s 0m18.83s \| ModularArithmetic/ModularBaseSystemProofs \| 0m27.00s \|\| -0m08.17s 0m13.77s \| ModularArithmetic/Montgomery/ZProofs \| 0m09.31s \|\| +0m04.45s 0m16.91s \| Experiments/SpecEd25519 \| 0m14.02s \|\| +0m02.89s 0m05.95s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m03.94s \|\| +0m02.01s 0m15.10s \| Specific/GF25519 \| 0m16.29s \|\| -0m01.18s 0m09.03s \| Specific/GF1305 \| 0m10.27s \|\| -0m01.24s 0m05.09s \| ModularArithmetic/Tutorial \| 0m03.68s \|\| +0m01.40s 0m03.78s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.61s \|\| +0m01.16s 0m12.20s \| Util/ZUtil \| 0m11.39s \|\| +0m00.80s 0m10.50s \| Testbit \| 0m10.45s \|\| +0m00.05s 0m04.99s \| BaseSystemProofs \| 0m04.22s \|\| +0m00.77s 0m04.01s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m03.05s \|\| +0m00.96s 0m03.42s \| Experiments/SpecificCurve25519 \| 0m03.52s \|\| -0m00.10s 0m02.87s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.38s \|\| +0m00.49s 0m02.55s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.43s \|\| -0m00.88s 0m02.14s \| ModularArithmetic/BarrettReduction/Z \| 0m01.55s \|\| +0m00.59s 0m01.77s \| Encoding/PointEncodingPre \| 0m01.57s \|\| +0m00.19s 0m01.68s \| BaseSystem \| 0m01.65s \|\| +0m00.03s 0m01.51s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.09s \|\| +0m00.41s 0m01.37s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.86s \|\| +0m00.51s 0m01.31s \| ModularArithmetic/ExtendedBaseVector \| 0m01.17s \|\| +0m00.14s 0m01.16s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.30s \|\| -0m00.14s 0m01.15s \| Util/NumTheoryUtil \| 0m01.33s \|\| -0m00.18s 0m01.07s \| Encoding/ModularWordEncodingTheorems \| 0m01.02s \|\| +0m00.05s 0m00.98s \| Encoding/ModularWordEncodingPre \| 0m00.92s \|\| +0m00.05s 0m00.97s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.64s \|\| +0m00.32s 0m00.85s \| ModularArithmetic/Montgomery/ZBounded \| 0m00.97s \|\| -0m00.12s 0m00.79s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.69s \|\| +0m00.10s 0m00.76s \| ModularArithmetic/Pre \| 0m00.48s \|\| +0m00.28s 0m00.73s \| ModularArithmetic/ModularBaseSystemList \| 0m00.66s \|\| +0m00.06s 0m00.71s \| Spec/ModularWordEncoding \| 0m00.58s \|\| +0m00.13s 0m00.68s \| ModularArithmetic/Pow2Base \| 0m00.41s \|\| +0m00.27s 0m00.67s \| ModularArithmetic/ZBounded \| 0m00.48s \|\| +0m00.19s 0m00.66s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.43s \|\| +0m00.23s 0m00.66s \| ModularArithmetic/ModularBaseSystem \| 0m00.62s \|\| +0m00.04s 0m00.45s \| ModularArithmetic/Montgomery/Z \| 0m00.40s \|\| +0m00.04s 0m00.41s \| Spec/ModularArithmetic \| 0m00.36s \|\| +0m00.04s
*	Added rewrite hints for two ListUtil lemmas	jadep	2016-08-24
\|
*	Moved a tactic to Util/Tactics.v	jadep	2016-08-24
\|
*	Fix a typo	Jason Gross	2016-08-24
\|
*	Add map_cons from Coq 8.6	Jason Gross	2016-08-24
\|
*	Merge branch 'fast-inverse'	jadep	2016-08-24
\|\
* \|	Fix a Hint Resolve typo	Jason Gross	2016-08-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 3m27.80s \| Total \| 3m20.02s \|\| +0m07.77s ---------------------------------------------------------------------------------- 0m54.16s \| ModularArithmetic/Pow2BaseProofs \| 0m48.95s \|\| +0m05.20s 0m14.95s \| Util/ZUtil \| 0m12.98s \|\| +0m01.96s 0m13.35s \| ModularArithmetic/Montgomery/ZProofs \| 0m11.51s \|\| +0m01.83s 0m04.58s \| BaseSystemProofs \| 0m06.07s \|\| -0m01.49s 0m20.73s \| ModularArithmetic/ModularBaseSystemProofs \| 0m20.21s \|\| +0m00.51s 0m15.71s \| Experiments/SpecEd25519 \| 0m14.99s \|\| +0m00.72s 0m13.21s \| Testbit \| 0m12.23s \|\| +0m00.98s 0m10.51s \| Specific/GF25519 \| 0m11.33s \|\| -0m00.82s 0m07.18s \| Specific/GF1305 \| 0m07.50s \|\| -0m00.32s 0m05.75s \| ModularArithmetic/Tutorial \| 0m05.51s \|\| +0m00.24s 0m05.71s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m05.86s \|\| -0m00.15s 0m04.88s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m04.95s \|\| -0m00.07s 0m03.37s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m03.59s \|\| -0m00.21s 0m03.31s \| Experiments/SpecificCurve25519 \| 0m03.58s \|\| -0m00.27s 0m03.22s \| ModularArithmetic/ModularArithmeticTheorems \| 0m03.99s \|\| -0m00.77s 0m02.29s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.55s \|\| -0m00.25s 0m02.28s \| ModularArithmetic/BarrettReduction/Z \| 0m02.38s \|\| -0m00.10s 0m01.82s \| BaseSystem \| 0m01.87s \|\| -0m00.05s 0m01.67s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.57s \|\| +0m00.09s 0m01.58s \| Encoding/PointEncodingPre \| 0m01.67s \|\| -0m00.08s 0m01.40s \| ModularArithmetic/ExtendedBaseVector \| 0m01.53s \|\| -0m00.13s 0m01.39s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.97s \|\| +0m00.41s 0m01.32s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m01.33s \|\| -0m00.01s 0m01.29s \| ModularArithmetic/Montgomery/ZBounded \| 0m01.25s \|\| +0m00.04s 0m01.25s \| Util/NumTheoryUtil \| 0m01.07s \|\| +0m00.17s 0m01.00s \| ModularArithmetic/ModularBaseSystem \| 0m00.91s \|\| +0m00.08s 0m00.97s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.88s \|\| +0m00.08s 0m00.96s \| ModularArithmetic/ModularBaseSystemField \| 0m01.08s \|\| -0m00.12s 0m00.91s \| Spec/ModularWordEncoding \| 0m00.59s \|\| +0m00.32s 0m00.90s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.83s \|\| +0m00.07s 0m00.89s \| ModularArithmetic/ModularBaseSystemList \| 0m00.96s \|\| -0m00.06s 0m00.75s \| Encoding/ModularWordEncodingPre \| 0m00.74s \|\| +0m00.01s 0m00.74s \| ModularArithmetic/Pre \| 0m00.76s \|\| -0m00.02s 0m00.71s \| Encoding/ModularWordEncodingTheorems \| 0m00.71s \|\| +0m00.00s 0m00.68s \| ModularArithmetic/ZBounded \| 0m00.68s \|\| +0m00.00s 0m00.67s \| ModularArithmetic/Pow2Base \| 0m00.66s \|\| +0m00.01s 0m00.61s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.61s \|\| +0m00.00s 0m00.57s \| ModularArithmetic/Montgomery/Z \| 0m00.59s \|\| -0m00.02s 0m00.53s \| Spec/ModularArithmetic \| 0m00.58s \|\| -0m00.04s
* \|	More ZUtil	Jason Gross	2016-08-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 3m12.82s \| Total \| 3m41.60s \|\| -0m28.77s ---------------------------------------------------------------------------------- 0m45.19s \| ModularArithmetic/Pow2BaseProofs \| 0m56.43s \|\| -0m11.24s 0m11.84s \| Util/ZUtil \| 0m14.96s \|\| -0m03.12s 0m18.96s \| ModularArithmetic/ModularBaseSystemProofs \| 0m20.98s \|\| -0m02.01s 0m13.99s \| Experiments/SpecEd25519 \| 0m16.65s \|\| -0m02.65s 0m11.97s \| ModularArithmetic/Montgomery/ZProofs \| 0m13.49s \|\| -0m01.51s 0m05.06s \| ModularArithmetic/Tutorial \| 0m06.06s \|\| -0m01.00s 0m13.89s \| Specific/GF25519 \| 0m14.28s \|\| -0m00.38s 0m10.57s \| Testbit \| 0m10.65s \|\| -0m00.08s 0m10.11s \| Specific/GF1305 \| 0m10.76s \|\| -0m00.65s 0m05.77s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m06.03s \|\| -0m00.26s 0m05.58s \| BaseSystemProofs \| 0m06.05s \|\| -0m00.46s 0m04.54s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m05.03s \|\| -0m00.49s 0m04.28s \| ModularArithmetic/ModularArithmeticTheorems \| 0m04.36s \|\| -0m00.08s 0m03.70s \| Experiments/SpecificCurve25519 \| 0m03.37s \|\| +0m00.33s 0m03.17s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.80s \|\| +0m00.37s 0m02.35s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.61s \|\| -0m00.25s 0m01.82s \| BaseSystem \| 0m01.93s \|\| -0m00.10s 0m01.67s \| Encoding/PointEncodingPre \| 0m02.45s \|\| -0m00.78s 0m01.64s \| ModularArithmetic/BarrettReduction/Z \| 0m02.41s \|\| -0m00.77s 0m01.47s \| ModularArithmetic/ExtendedBaseVector \| 0m01.85s \|\| -0m00.38s 0m01.28s \| Util/NumTheoryUtil \| 0m01.43s \|\| -0m00.14s 0m01.26s \| ModularArithmetic/Montgomery/ZBounded \| 0m01.37s \|\| -0m00.11s 0m01.19s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m01.18s \|\| +0m00.01s 0m01.17s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.35s \|\| -0m00.18s 0m01.05s \| ModularArithmetic/ModularBaseSystemField \| 0m01.38s \|\| -0m00.32s 0m00.99s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.27s \|\| -0m00.28s 0m00.82s \| ModularArithmetic/ModularBaseSystem \| 0m00.79s \|\| +0m00.02s 0m00.80s \| ModularArithmetic/ModularBaseSystemList \| 0m00.99s \|\| -0m00.18s 0m00.79s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.84s \|\| -0m00.04s 0m00.74s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.78s \|\| -0m00.04s 0m00.71s \| Encoding/ModularWordEncodingTheorems \| 0m01.11s \|\| -0m00.40s 0m00.71s \| ModularArithmetic/Pre \| 0m00.80s \|\| -0m00.09s 0m00.68s \| Encoding/ModularWordEncodingPre \| 0m00.94s \|\| -0m00.25s 0m00.62s \| Spec/ModularWordEncoding \| 0m00.90s \|\| -0m00.28s 0m00.55s \| Spec/ModularArithmetic \| 0m00.60s \|\| -0m00.04s 0m00.51s \| ModularArithmetic/ZBounded \| 0m00.74s \|\| -0m00.23s 0m00.51s \| ModularArithmetic/Pow2Base \| 0m00.70s \|\| -0m00.18s 0m00.46s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.65s \|\| -0m00.19s 0m00.42s \| ModularArithmetic/Montgomery/Z \| 0m00.63s \|\| -0m00.21s
* \|	More ZUtil	Jason Gross	2016-08-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 3m15.25s \| Total \| 3m13.26s \|\| +0m01.99s ---------------------------------------------------------------------------------- 0m45.71s \| ModularArithmetic/Pow2BaseProofs \| 0m48.18s \|\| -0m02.46s 0m21.84s \| ModularArithmetic/ModularBaseSystemProofs \| 0m18.97s \|\| +0m02.87s 0m12.08s \| Util/ZUtil \| 0m14.07s \|\| -0m01.99s 0m04.13s \| ModularArithmetic/ModularArithmeticTheorems \| 0m03.13s \|\| +0m01.00s 0m15.10s \| Experiments/SpecEd25519 \| 0m15.56s \|\| -0m00.46s 0m12.15s \| ModularArithmetic/Montgomery/ZProofs \| 0m11.29s \|\| +0m00.86s 0m11.83s \| Specific/GF25519 \| 0m12.41s \|\| -0m00.58s 0m10.60s \| Testbit \| 0m09.79s \|\| +0m00.81s 0m07.90s \| Specific/GF1305 \| 0m08.12s \|\| -0m00.21s 0m05.50s \| BaseSystemProofs \| 0m05.78s \|\| -0m00.28s 0m05.19s \| ModularArithmetic/Tutorial \| 0m05.39s \|\| -0m00.19s 0m05.17s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m04.98s \|\| +0m00.18s 0m04.61s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m03.80s \|\| +0m00.81s 0m03.36s \| Experiments/SpecificCurve25519 \| 0m03.44s \|\| -0m00.08s 0m03.13s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.70s \|\| +0m00.42s 0m02.32s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.38s \|\| -0m00.06s 0m02.32s \| Encoding/PointEncodingPre \| 0m01.97s \|\| +0m00.34s 0m01.98s \| ModularArithmetic/BarrettReduction/Z \| 0m01.72s \|\| +0m00.26s 0m01.85s \| BaseSystem \| 0m01.44s \|\| +0m00.41s 0m01.61s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.58s \|\| +0m00.03s 0m01.33s \| ModularArithmetic/ExtendedBaseVector \| 0m01.73s \|\| -0m00.39s 0m01.28s \| ModularArithmetic/Montgomery/ZBounded \| 0m01.33s \|\| -0m00.05s 0m01.19s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m01.13s \|\| +0m00.06s 0m01.13s \| Util/NumTheoryUtil \| 0m01.23s \|\| -0m00.10s 0m01.06s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.03s \|\| +0m00.03s 0m01.04s \| ModularArithmetic/ModularBaseSystemField \| 0m00.99s \|\| +0m00.05s 0m01.00s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.98s \|\| +0m00.02s 0m00.98s \| Encoding/ModularWordEncodingTheorems \| 0m00.78s \|\| +0m00.19s 0m00.96s \| Encoding/ModularWordEncodingPre \| 0m00.81s \|\| +0m00.14s 0m00.93s \| ModularArithmetic/ModularBaseSystemList \| 0m00.96s \|\| -0m00.02s 0m00.89s \| ModularArithmetic/ModularBaseSystem \| 0m00.93s \|\| -0m00.04s 0m00.80s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.94s \|\| -0m00.13s 0m00.70s \| Spec/ModularWordEncoding \| 0m00.70s \|\| +0m00.00s 0m00.67s \| ModularArithmetic/ZBounded \| 0m00.53s \|\| +0m00.14s 0m00.66s \| ModularArithmetic/Pre \| 0m00.63s \|\| +0m00.03s 0m00.60s \| ModularArithmetic/Pow2Base \| 0m00.53s \|\| +0m00.06s 0m00.59s \| ModularArithmetic/Montgomery/Z \| 0m00.44s \|\| +0m00.14s 0m00.54s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.52s \|\| +0m00.02s 0m00.53s \| Spec/ModularArithmetic \| 0m00.38s \|\| +0m00.15s
\| *	Updated AdditionChainExponentiation.v such that the exponentiation ↵	jadep	2016-08-23
\|/ \| \| \|	correctness is in terms of N rather than nat; this allows us to compute the correctness proof for large exponents.
*	Merge.	jadep	2016-08-21
\|\
* \|	ListUtil.v : new proofs about sum_firstn for lists with nonnegative elements	jadep	2016-08-21
\| \|
\| *	Add Z.rewrite_mod_small	Jason Gross	2016-08-19
\| \|
\| *	More powerful Z.div_mod_to_quot_rem	Jason Gross	2016-08-19
\| \|
\| *	More ZUtil	Jason Gross	2016-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 2m37.84s \| Total \| 2m32.22s \|\| +0m05.61s ---------------------------------------------------------------------------------- 0m10.58s \| Specific/GF25519 \| 0m16.17s \|\| -0m05.59s 0m05.58s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m03.76s \|\| +0m01.82s 0m04.68s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m03.29s \|\| +0m01.38s 0m23.88s \| ModularArithmetic/Pow2BaseProofs \| 0m22.97s \|\| +0m00.91s 0m17.87s \| ModularArithmetic/ModularBaseSystemProofs \| 0m17.58s \|\| +0m00.29s 0m14.61s \| Experiments/SpecEd25519 \| 0m13.99s \|\| +0m00.61s 0m11.12s \| Util/ZUtil \| 0m11.49s \|\| -0m00.37s 0m09.76s \| Testbit \| 0m08.96s \|\| +0m00.79s 0m09.42s \| ModularArithmetic/Montgomery/ZProofs \| 0m08.66s \|\| +0m00.75s 0m08.04s \| Specific/GF1305 \| 0m07.48s \|\| +0m00.55s 0m05.09s \| ModularArithmetic/Tutorial \| 0m04.41s \|\| +0m00.67s 0m04.41s \| BaseSystemProofs \| 0m03.91s \|\| +0m00.50s 0m03.60s \| Experiments/SpecificCurve25519 \| 0m03.31s \|\| +0m00.29s 0m03.31s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.70s \|\| +0m00.60s 0m03.29s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.40s \|\| +0m00.89s 0m02.28s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.31s \|\| -0m00.03s 0m02.28s \| Encoding/PointEncodingPre \| 0m01.81s \|\| +0m00.46s 0m01.70s \| ModularArithmetic/BarrettReduction/Z \| 0m01.48s \|\| +0m00.21s 0m01.51s \| ModularArithmetic/ExtendedBaseVector \| 0m01.16s \|\| +0m00.35s 0m01.48s \| BaseSystem \| 0m01.18s \|\| +0m00.30s 0m01.34s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.39s \|\| -0m00.04s 0m01.10s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.09s \|\| +0m00.01s 0m00.88s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.87s \|\| +0m00.01s 0m00.87s \| Util/NumTheoryUtil \| 0m00.87s \|\| +0m00.00s 0m00.87s \| ModularArithmetic/ModularBaseSystemField \| 0m00.88s \|\| -0m00.01s 0m00.83s \| ModularArithmetic/Montgomery/ZBounded \| 0m00.85s \|\| -0m00.02s 0m00.78s \| Encoding/ModularWordEncodingTheorems \| 0m00.76s \|\| +0m00.02s 0m00.69s \| Encoding/ModularWordEncodingPre \| 0m00.80s \|\| -0m00.11s 0m00.67s \| ModularArithmetic/ZBounded \| 0m00.42s \|\| +0m00.25s 0m00.64s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.63s \|\| +0m00.01s 0m00.63s \| ModularArithmetic/ModularBaseSystem \| 0m00.63s \|\| +0m00.00s 0m00.63s \| Spec/ModularWordEncoding \| 0m00.64s \|\| -0m00.01s 0m00.59s \| ModularArithmetic/ModularBaseSystemList \| 0m00.66s \|\| -0m00.07s 0m00.58s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.60s \|\| -0m00.02s 0m00.54s \| ModularArithmetic/Pre \| 0m00.49s \|\| +0m00.05s 0m00.52s \| ModularArithmetic/Pow2Base \| 0m00.42s \|\| +0m00.10s 0m00.41s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.42s \|\| -0m00.01s 0m00.41s \| ModularArithmetic/Montgomery/Z \| 0m00.41s \|\| +0m00.00s 0m00.37s \| Spec/ModularArithmetic \| 0m00.38s \|\| -0m00.01s
\| *	Add ZUtil	Jason Gross	2016-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 2m37.39s \| Total \| 2m44.14s \|\| -0m06.75s ---------------------------------------------------------------------------------- 0m21.75s \| ModularArithmetic/Pow2BaseProofs \| 0m25.07s \|\| -0m03.32s 0m07.25s \| Specific/GF1305 \| 0m09.34s \|\| -0m02.08s 0m21.79s \| ModularArithmetic/ModularBaseSystemProofs \| 0m23.32s \|\| -0m01.53s 0m10.03s \| ModularArithmetic/Montgomery/ZProofs \| 0m11.15s \|\| -0m01.12s 0m04.01s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.80s \|\| +0m01.20s 0m13.95s \| Experiments/SpecEd25519 \| 0m14.48s \|\| -0m00.53s 0m11.59s \| Specific/GF25519 \| 0m12.20s \|\| -0m00.60s 0m11.23s \| Util/ZUtil \| 0m11.15s \|\| +0m00.08s 0m09.22s \| Testbit \| 0m08.89s \|\| +0m00.33s 0m04.88s \| BaseSystemProofs \| 0m04.24s \|\| +0m00.63s 0m04.37s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m03.74s \|\| +0m00.62s 0m04.04s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m04.58s \|\| -0m00.54s 0m04.01s \| ModularArithmetic/Tutorial \| 0m03.71s \|\| +0m00.29s 0m03.28s \| Experiments/SpecificCurve25519 \| 0m03.32s \|\| -0m00.04s 0m02.79s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.66s \|\| +0m00.12s 0m02.23s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.38s \|\| -0m00.14s 0m01.96s \| ModularArithmetic/BarrettReduction/Z \| 0m02.30s \|\| -0m00.33s 0m01.61s \| Encoding/PointEncodingPre \| 0m01.74s \|\| -0m00.12s 0m01.33s \| BaseSystem \| 0m01.79s \|\| -0m00.46s 0m01.33s \| ModularArithmetic/ExtendedBaseVector \| 0m01.21s \|\| +0m00.12s 0m01.31s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.39s \|\| -0m00.07s 0m01.24s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.87s \|\| +0m00.37s 0m01.21s \| Util/NumTheoryUtil \| 0m01.02s \|\| +0m00.18s 0m01.09s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.24s \|\| -0m00.14s 0m01.01s \| Encoding/ModularWordEncodingTheorems \| 0m00.65s \|\| +0m00.36s 0m00.93s \| ModularArithmetic/ModularBaseSystemField \| 0m00.93s \|\| +0m00.00s 0m00.90s \| ModularArithmetic/ModularBaseSystemList \| 0m00.61s \|\| +0m00.29s 0m00.88s \| ModularArithmetic/Montgomery/ZBounded \| 0m00.89s \|\| -0m00.01s 0m00.84s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.72s \|\| +0m00.12s 0m00.76s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.64s \|\| +0m00.12s 0m00.68s \| Encoding/ModularWordEncodingPre \| 0m00.61s \|\| +0m00.07s 0m00.62s \| ModularArithmetic/ModularBaseSystem \| 0m00.84s \|\| -0m00.21s 0m00.61s \| Spec/ModularWordEncoding \| 0m00.56s \|\| +0m00.04s 0m00.51s \| ModularArithmetic/Pre \| 0m00.54s \|\| -0m00.03s 0m00.47s \| ModularArithmetic/ZBounded \| 0m00.65s \|\| -0m00.18s 0m00.46s \| ModularArithmetic/Montgomery/Z \| 0m00.59s \|\| -0m00.12s 0m00.43s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.40s \|\| +0m00.02s 0m00.43s \| ModularArithmetic/Pow2Base \| 0m00.54s \|\| -0m00.11s 0m00.36s \| Spec/ModularArithmetic \| 0m00.38s \|\| -0m00.02s
\| *	Add a ZUtil hint	Jason Gross	2016-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 2m33.78s \| Total \| 2m34.23s \|\| -0m00.45s ---------------------------------------------------------------------------------- 0m22.98s \| ModularArithmetic/Pow2BaseProofs \| 0m24.08s \|\| -0m01.09s 0m10.80s \| ModularArithmetic/Montgomery/ZProofs \| 0m12.07s \|\| -0m01.26s 0m03.02s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m04.40s \|\| -0m01.38s 0m18.19s \| ModularArithmetic/ModularBaseSystemProofs \| 0m17.78s \|\| +0m00.41s 0m13.63s \| Experiments/SpecEd25519 \| 0m13.77s \|\| -0m00.13s 0m10.95s \| Util/ZUtil \| 0m10.96s \|\| -0m00.01s 0m10.46s \| Specific/GF25519 \| 0m10.30s \|\| +0m00.16s 0m09.89s \| Testbit \| 0m09.16s \|\| +0m00.73s 0m07.37s \| Specific/GF1305 \| 0m07.10s \|\| +0m00.27s 0m05.22s \| ModularArithmetic/Tutorial \| 0m05.05s \|\| +0m00.16s 0m04.79s \| BaseSystemProofs \| 0m04.22s \|\| +0m00.57s 0m04.78s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m05.13s \|\| -0m00.34s 0m03.34s \| Experiments/SpecificCurve25519 \| 0m03.48s \|\| -0m00.14s 0m03.08s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.68s \|\| +0m00.39s 0m02.30s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.27s \|\| +0m00.02s 0m02.24s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.31s \|\| -0m00.06s 0m01.59s \| Encoding/PointEncodingPre \| 0m01.64s \|\| -0m00.04s 0m01.55s \| ModularArithmetic/BarrettReduction/Z \| 0m01.59s \|\| -0m00.04s 0m01.47s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.07s \|\| +0m00.39s 0m01.31s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.93s \|\| +0m00.38s 0m01.24s \| BaseSystem \| 0m01.37s \|\| -0m00.13s 0m01.21s \| ModularArithmetic/ExtendedBaseVector \| 0m01.20s \|\| +0m00.01s 0m01.06s \| Encoding/ModularWordEncodingTheorems \| 0m00.73s \|\| +0m00.33s 0m01.01s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.43s \|\| -0m00.41s 0m00.96s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.66s \|\| +0m00.29s 0m00.92s \| ModularArithmetic/ModularBaseSystemList \| 0m00.64s \|\| +0m00.28s 0m00.92s \| ModularArithmetic/Montgomery/ZBounded \| 0m00.86s \|\| +0m00.06s 0m00.91s \| ModularArithmetic/ModularBaseSystemField \| 0m00.90s \|\| +0m00.01s 0m00.90s \| Util/NumTheoryUtil \| 0m00.90s \|\| +0m00.00s 0m00.82s \| Spec/ModularWordEncoding \| 0m00.88s \|\| -0m00.06s 0m00.72s \| ModularArithmetic/Pre \| 0m00.48s \|\| +0m00.24s 0m00.62s \| ModularArithmetic/ModularBaseSystem \| 0m00.59s \|\| +0m00.03s 0m00.62s \| Encoding/ModularWordEncodingPre \| 0m00.68s \|\| -0m00.06s 0m00.59s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.58s \|\| +0m00.01s 0m00.53s \| ModularArithmetic/ZBounded \| 0m00.68s \|\| -0m00.15s 0m00.53s \| ModularArithmetic/Pow2Base \| 0m00.46s \|\| +0m00.07s 0m00.48s \| ModularArithmetic/Montgomery/Z \| 0m00.39s \|\| +0m00.08s 0m00.41s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.41s \|\| +0m00.00s 0m00.37s \| Spec/ModularArithmetic \| 0m00.40s \|\| -0m00.03s
\| *	Add some ZUtil lemmas and hints	Jason Gross	2016-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 2m45.95s \| Total \| 2m39.20s \|\| +0m06.74s ---------------------------------------------------------------------------------- 0m17.76s \| ModularArithmetic/ModularBaseSystemProofs \| 0m20.55s \|\| -0m02.78s 0m14.41s \| Util/ZUtil \| 0m11.79s \|\| +0m02.62s 0m12.45s \| Specific/GF25519 \| 0m10.16s \|\| +0m02.28s 0m09.20s \| Specific/GF1305 \| 0m07.08s \|\| +0m02.11s 0m11.29s \| ModularArithmetic/Montgomery/ZProofs \| 0m10.07s \|\| +0m01.21s 0m05.36s \| ModularArithmetic/Tutorial \| 0m03.87s \|\| +0m01.49s 0m02.73s \| ModularArithmetic/ModularArithmeticTheorems \| 0m03.91s \|\| -0m01.18s 0m24.05s \| ModularArithmetic/Pow2BaseProofs \| 0m23.30s \|\| +0m00.75s 0m15.10s \| Experiments/SpecEd25519 \| 0m14.69s \|\| +0m00.41s 0m10.42s \| Testbit \| 0m10.86s \|\| -0m00.43s 0m04.40s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m04.26s \|\| +0m00.14s 0m04.29s \| BaseSystemProofs \| 0m04.96s \|\| -0m00.67s 0m04.11s \| Experiments/SpecificCurve25519 \| 0m03.28s \|\| +0m00.83s 0m03.66s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m04.01s \|\| -0m00.34s 0m02.80s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m03.50s \|\| -0m00.70s 0m02.26s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.24s \|\| +0m00.01s 0m02.12s \| Encoding/PointEncodingPre \| 0m01.81s \|\| +0m00.31s 0m02.04s \| ModularArithmetic/BarrettReduction/Z \| 0m01.52s \|\| +0m00.52s 0m01.71s \| ModularArithmetic/ExtendedBaseVector \| 0m01.29s \|\| +0m00.41s 0m01.62s \| BaseSystem \| 0m01.22s \|\| +0m00.40s 0m01.28s \| ModularArithmetic/Montgomery/ZBounded \| 0m01.20s \|\| +0m00.08s 0m01.05s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.22s \|\| -0m00.16s 0m00.96s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.01s \|\| -0m00.05s 0m00.94s \| Util/NumTheoryUtil \| 0m00.93s \|\| +0m00.00s 0m00.93s \| ModularArithmetic/ModularBaseSystem \| 0m00.78s \|\| +0m00.15s 0m00.93s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m01.06s \|\| -0m00.13s 0m00.92s \| ModularArithmetic/ModularBaseSystemList \| 0m00.87s \|\| +0m00.05s 0m00.90s \| ModularArithmetic/ModularBaseSystemField \| 0m00.89s \|\| +0m00.01s 0m00.72s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.80s \|\| -0m00.08s 0m00.72s \| Encoding/ModularWordEncodingTheorems \| 0m00.79s \|\| -0m00.07s 0m00.72s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.88s \|\| -0m00.16s 0m00.65s \| Encoding/ModularWordEncodingPre \| 0m00.82s \|\| -0m00.16s 0m00.59s \| Spec/ModularWordEncoding \| 0m00.65s \|\| -0m00.06s 0m00.56s \| ModularArithmetic/Pre \| 0m00.53s \|\| +0m00.03s 0m00.53s \| Spec/ModularArithmetic \| 0m00.39s \|\| +0m00.14s 0m00.49s \| ModularArithmetic/ZBounded \| 0m00.59s \|\| -0m00.09s 0m00.44s \| ModularArithmetic/Pow2Base \| 0m00.50s \|\| -0m00.06s 0m00.43s \| ModularArithmetic/Montgomery/Z \| 0m00.42s \|\| +0m00.01s 0m00.41s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.51s \|\| -0m00.10s
\| *	Add versions of ZUtil lemmas without nonzero assumptions	Jason Gross	2016-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 2m38.91s \| Total \| 2m40.89s \|\| -0m01.97s ---------------------------------------------------------------------------------- 0m17.80s \| ModularArithmetic/ModularBaseSystemProofs \| 0m25.90s \|\| -0m08.09s 0m25.51s \| ModularArithmetic/Pow2BaseProofs \| 0m23.25s \|\| +0m02.26s 0m15.42s \| Experiments/SpecEd25519 \| 0m13.98s \|\| +0m01.43s 0m11.16s \| Util/ZUtil \| 0m12.18s \|\| -0m01.01s 0m10.54s \| ModularArithmetic/Montgomery/ZProofs \| 0m08.81s \|\| +0m01.72s 0m10.22s \| Specific/GF25519 \| 0m10.69s \|\| -0m00.46s 0m09.68s \| Testbit \| 0m09.06s \|\| +0m00.61s 0m06.84s \| Specific/GF1305 \| 0m06.97s \|\| -0m00.12s 0m05.08s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m04.74s \|\| +0m00.33s 0m04.91s \| BaseSystemProofs \| 0m04.90s \|\| +0m00.00s 0m04.57s \| ModularArithmetic/Tutorial \| 0m05.05s \|\| -0m00.47s 0m04.07s \| ModularArithmetic/ModularArithmeticTheorems \| 0m03.09s \|\| +0m00.98s 0m03.68s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m04.53s \|\| -0m00.85s 0m03.31s \| Experiments/SpecificCurve25519 \| 0m03.29s \|\| +0m00.02s 0m02.81s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.28s \|\| +0m00.53s 0m02.33s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.32s \|\| +0m00.01s 0m01.82s \| ModularArithmetic/BarrettReduction/Z \| 0m02.10s \|\| -0m00.28s 0m01.76s \| BaseSystem \| 0m01.28s \|\| +0m00.48s 0m01.66s \| Encoding/PointEncodingPre \| 0m01.70s \|\| -0m00.04s 0m01.60s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.10s \|\| +0m00.50s 0m01.34s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.02s \|\| +0m00.32s 0m01.30s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.89s \|\| +0m00.41s 0m01.21s \| ModularArithmetic/ExtendedBaseVector \| 0m01.16s \|\| +0m00.05s 0m00.99s \| Util/NumTheoryUtil \| 0m00.97s \|\| +0m00.02s 0m00.92s \| ModularArithmetic/Montgomery/ZBounded \| 0m00.85s \|\| +0m00.07s 0m00.86s \| ModularArithmetic/ModularBaseSystemField \| 0m00.91s \|\| -0m00.05s 0m00.76s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.65s \|\| +0m00.10s 0m00.75s \| Encoding/ModularWordEncodingPre \| 0m00.69s \|\| +0m00.06s 0m00.71s \| ModularArithmetic/ZBounded \| 0m00.66s \|\| +0m00.04s 0m00.68s \| Encoding/ModularWordEncodingTheorems \| 0m00.69s \|\| -0m00.00s 0m00.64s \| ModularArithmetic/ModularBaseSystem \| 0m00.89s \|\| -0m00.25s 0m00.63s \| Spec/ModularWordEncoding \| 0m00.63s \|\| +0m00.00s 0m00.60s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.59s \|\| +0m00.01s 0m00.59s \| ModularArithmetic/ModularBaseSystemList \| 0m00.65s \|\| -0m00.06s 0m00.49s \| ModularArithmetic/Pre \| 0m00.49s \|\| +0m00.00s 0m00.45s \| ModularArithmetic/Pow2Base \| 0m00.46s \|\| -0m00.01s 0m00.44s \| ModularArithmetic/Montgomery/Z \| 0m00.46s \|\| -0m00.02s 0m00.40s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.44s \|\| -0m00.03s 0m00.39s \| Spec/ModularArithmetic \| 0m00.57s \|\| -0m00.17s
\| *	Add Z.opp_involutive to Zshift_to_pow	Jason Gross	2016-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It makes for nicer powers that don't involve b^(--n) After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 2m36.09s \| Total \| 2m30.06s \|\| +0m06.02s ---------------------------------------------------------------------------------- 0m26.17s \| ModularArithmetic/Pow2BaseProofs \| 0m22.91s \|\| +0m03.26s 0m13.18s \| ModularArithmetic/Montgomery/ZProofs \| 0m10.26s \|\| +0m02.92s 0m17.22s \| ModularArithmetic/ModularBaseSystemProofs \| 0m17.44s \|\| -0m00.22s 0m14.06s \| Experiments/SpecEd25519 \| 0m13.17s \|\| +0m00.89s 0m10.89s \| Util/ZUtil \| 0m10.94s \|\| -0m00.04s 0m10.35s \| Specific/GF25519 \| 0m10.87s \|\| -0m00.51s 0m09.07s \| Testbit \| 0m09.24s \|\| -0m00.16s 0m07.14s \| Specific/GF1305 \| 0m07.01s \|\| +0m00.12s 0m05.09s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m05.23s \|\| -0m00.14s 0m04.32s \| BaseSystemProofs \| 0m04.06s \|\| +0m00.26s 0m04.26s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m03.88s \|\| +0m00.37s 0m03.78s \| ModularArithmetic/Tutorial \| 0m04.02s \|\| -0m00.23s 0m03.34s \| Experiments/SpecificCurve25519 \| 0m03.31s \|\| +0m00.02s 0m02.74s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.19s \|\| +0m00.55s 0m02.72s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.81s \|\| -0m00.08s 0m02.27s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.23s \|\| +0m00.04s 0m01.95s \| Encoding/PointEncodingPre \| 0m01.55s \|\| +0m00.39s 0m01.66s \| ModularArithmetic/BarrettReduction/Z \| 0m02.25s \|\| -0m00.59s 0m01.24s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m01.29s \|\| -0m00.05s 0m01.22s \| BaseSystem \| 0m01.56s \|\| -0m00.34s 0m01.18s \| ModularArithmetic/ExtendedBaseVector \| 0m01.17s \|\| +0m00.01s 0m01.08s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.59s \|\| -0m00.51s 0m00.96s \| ModularArithmetic/ModularBaseSystemField \| 0m00.90s \|\| +0m00.05s 0m00.92s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.93s \|\| -0m00.01s 0m00.90s \| Util/NumTheoryUtil \| 0m00.95s \|\| -0m00.04s 0m00.87s \| ModularArithmetic/Montgomery/ZBounded \| 0m00.82s \|\| +0m00.05s 0m00.71s \| Encoding/ModularWordEncodingTheorems \| 0m00.69s \|\| +0m00.02s 0m00.67s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.59s \|\| +0m00.08s 0m00.66s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.66s \|\| +0m00.00s 0m00.66s \| ModularArithmetic/ModularBaseSystemList \| 0m00.66s \|\| +0m00.00s 0m00.66s \| Encoding/ModularWordEncodingPre \| 0m00.62s \|\| +0m00.04s 0m00.62s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.41s \|\| +0m00.21s 0m00.62s \| ModularArithmetic/Pow2Base \| 0m00.48s \|\| +0m00.14s 0m00.61s \| ModularArithmetic/ModularBaseSystem \| 0m00.65s \|\| -0m00.04s 0m00.58s \| Spec/ModularWordEncoding \| 0m00.58s \|\| +0m00.00s 0m00.57s \| ModularArithmetic/Pre \| 0m00.52s \|\| +0m00.04s 0m00.44s \| ModularArithmetic/ZBounded \| 0m00.69s \|\| -0m00.24s 0m00.37s \| ModularArithmetic/Montgomery/Z \| 0m00.58s \|\| -0m00.20s 0m00.34s \| Spec/ModularArithmetic \| 0m00.36s \|\| -0m00.01s
\| *	Add a ZUtil hint	Jason Gross	2016-08-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 3m12.69s \| Total \| 3m16.43s \|\| -0m03.74s ---------------------------------------------------------------------------------- 0m11.44s \| Util/ZUtil \| 0m17.68s \|\| -0m06.24s 0m38.50s \| Specific/GF25519 \| 0m33.01s \|\| +0m05.49s 0m26.17s \| ModularArithmetic/Pow2BaseProofs \| 0m27.37s \|\| -0m01.19s 0m12.70s \| ModularArithmetic/Montgomery/ZProofs \| 0m10.86s \|\| +0m01.83s 0m08.87s \| Specific/GF1305 \| 0m07.04s \|\| +0m01.82s 0m04.01s \| ModularArithmetic/Tutorial \| 0m05.33s \|\| -0m01.32s 0m18.62s \| ModularArithmetic/ModularBaseSystemProofs \| 0m18.56s \|\| +0m00.06s 0m14.58s \| Experiments/SpecEd25519 \| 0m15.11s \|\| -0m00.52s 0m09.83s \| Testbit \| 0m10.73s \|\| -0m00.90s 0m05.35s \| BaseSystemProofs \| 0m05.65s \|\| -0m00.30s 0m04.55s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m05.22s \|\| -0m00.67s 0m04.11s \| Experiments/SpecificCurve25519 \| 0m03.39s \|\| +0m00.72s 0m03.98s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m03.87s \|\| +0m00.10s 0m03.41s \| ModularArithmetic/ModularArithmeticTheorems \| 0m04.06s \|\| -0m00.64s 0m02.68s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.37s \|\| +0m00.31s 0m02.50s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m03.34s \|\| -0m00.83s 0m02.25s \| Encoding/PointEncodingPre \| 0m01.85s \|\| +0m00.39s 0m01.76s \| ModularArithmetic/BarrettReduction/Z \| 0m02.00s \|\| -0m00.24s 0m01.72s \| ModularArithmetic/ExtendedBaseVector \| 0m01.35s \|\| +0m00.36s 0m01.28s \| BaseSystem \| 0m01.43s \|\| -0m00.14s 0m01.25s \| ModularArithmetic/ModularBaseSystemField \| 0m00.90s \|\| +0m00.35s 0m01.22s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.21s \|\| +0m00.01s 0m01.10s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.54s \|\| -0m00.43s 0m00.93s \| ModularArithmetic/Montgomery/ZBounded \| 0m01.28s \|\| -0m00.35s 0m00.93s \| Util/NumTheoryUtil \| 0m01.20s \|\| -0m00.26s 0m00.92s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m01.29s \|\| -0m00.37s 0m00.78s \| ModularArithmetic/ModularBaseSystem \| 0m00.76s \|\| +0m00.02s 0m00.77s \| ModularArithmetic/ModularBaseSystemList \| 0m00.94s \|\| -0m00.16s 0m00.76s \| Encoding/ModularWordEncodingTheorems \| 0m00.82s \|\| -0m00.05s 0m00.70s \| Spec/ModularWordEncoding \| 0m00.69s \|\| +0m00.01s 0m00.69s \| ModularArithmetic/Pre \| 0m00.59s \|\| +0m00.09s 0m00.68s \| Encoding/ModularWordEncodingPre \| 0m00.93s \|\| -0m00.25s 0m00.65s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.66s \|\| -0m00.01s 0m00.64s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.71s \|\| -0m00.06s 0m00.60s \| ModularArithmetic/Pow2Base \| 0m00.62s \|\| -0m00.02s 0m00.53s \| Spec/ModularArithmetic \| 0m00.46s \|\| +0m00.07s 0m00.46s \| ModularArithmetic/ZBounded \| 0m00.62s \|\| -0m00.15s 0m00.39s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.55s \|\| -0m00.16s 0m00.38s \| ModularArithmetic/Montgomery/Z \| 0m00.44s \|\| -0m00.06s
\| *	Add Z.div_mod_to_quot_rem	Jason Gross	2016-08-17
\| \| \| \| \| \| \| \|	Progress towards #55
\| *	Add simplify_projections to Util.Tactics	Jason Gross	2016-08-17
\| \|
\| *	Add [Z.linear_solve_for], [Z.linear_substitute]	Jason Gross	2016-08-17
\|/ \| \| \| \| \| \| \| \|	The first solves for a variable; the second does this, and then runs [subst]. By design, they only handle addition and subtraction. They should be easily generalizable to handle arbitrary rings (and should probably be generalized to do so at some point). (Also requested, if I recall correctly, by @andres-erbsen.)
*	More zsimplify	Jason Gross	2016-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 2m58.58s \| Total \| 3m01.39s \|\| -0m02.80s ---------------------------------------------------------------------------------- 0m17.56s \| ModularArithmetic/ModularBaseSystemProofs \| 0m27.13s \|\| -0m09.57s 0m40.47s \| Specific/GF25519 \| 0m33.17s \|\| +0m07.29s 0m22.10s \| ModularArithmetic/Pow2BaseProofs \| 0m23.84s \|\| -0m01.73s 0m06.88s \| Specific/GF1305 \| 0m08.00s \|\| -0m01.12s 0m13.87s \| Experiments/SpecEd25519 \| 0m14.51s \|\| -0m00.64s 0m10.89s \| Util/ZUtil \| 0m10.73s \|\| +0m00.16s 0m09.17s \| ModularArithmetic/Montgomery/ZProofs \| 0m08.95s \|\| +0m00.22s 0m08.83s \| Testbit \| 0m09.62s \|\| -0m00.78s 0m04.06s \| BaseSystemProofs \| 0m04.03s \|\| +0m00.02s 0m04.06s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m03.64s \|\| +0m00.41s 0m03.64s \| ModularArithmetic/Tutorial \| 0m03.85s \|\| -0m00.20s 0m03.45s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m03.15s \|\| +0m00.30s 0m03.32s \| Experiments/SpecificCurve25519 \| 0m03.39s \|\| -0m00.07s 0m03.16s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.69s \|\| +0m00.47s 0m02.66s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m03.03s \|\| -0m00.36s 0m02.30s \| Encoding/PointEncodingPre \| 0m01.69s \|\| +0m00.60s 0m02.24s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.46s \|\| -0m00.21s 0m02.10s \| ModularArithmetic/BarrettReduction/Z \| 0m01.50s \|\| +0m00.60s 0m01.87s \| BaseSystem \| 0m01.29s \|\| +0m00.58s 0m01.25s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.39s \|\| -0m00.13s 0m01.23s \| Util/NumTheoryUtil \| 0m00.88s \|\| +0m00.35s 0m01.19s \| ModularArithmetic/ExtendedBaseVector \| 0m01.17s \|\| +0m00.02s 0m01.18s \| ModularArithmetic/Montgomery/ZBounded \| 0m00.88s \|\| +0m00.29s 0m01.08s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.07s \|\| +0m00.01s 0m01.03s \| Encoding/ModularWordEncodingTheorems \| 0m00.73s \|\| +0m00.30s 0m00.96s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.68s \|\| +0m00.27s 0m00.93s \| ModularArithmetic/ModularBaseSystemList \| 0m00.64s \|\| +0m00.29s 0m00.91s \| ModularArithmetic/ModularBaseSystemField \| 0m00.99s \|\| -0m00.07s 0m00.86s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.83s \|\| +0m00.03s 0m00.68s \| Encoding/ModularWordEncodingPre \| 0m00.62s \|\| +0m00.06s 0m00.65s \| Spec/ModularWordEncoding \| 0m00.76s \|\| -0m00.10s 0m00.60s \| ModularArithmetic/ModularBaseSystem \| 0m00.60s \|\| +0m00.00s 0m00.59s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.57s \|\| +0m00.02s 0m00.58s \| ModularArithmetic/Montgomery/Z \| 0m00.43s \|\| +0m00.14s 0m00.57s \| ModularArithmetic/Pre \| 0m00.52s \|\| +0m00.04s 0m00.44s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.57s \|\| -0m00.12s 0m00.44s \| ModularArithmetic/ZBounded \| 0m00.50s \|\| -0m00.06s 0m00.42s \| ModularArithmetic/Pow2Base \| 0m00.48s \|\| -0m00.06s 0m00.37s \| Spec/ModularArithmetic \| 0m00.42s \|\| -0m00.04s
*	Add natutil	Jason Gross	2016-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 4m05.87s \| Total \| 3m55.03s \|\| +0m10.84s ------------------------------------------------------------------------------------ 0m29.03s \| ModularArithmetic/Pow2BaseProofs \| 0m22.86s \|\| +0m06.17s 0m42.14s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m37.78s \|\| +0m04.35s 0m33.70s \| Specific/GF25519 \| 0m36.48s \|\| -0m02.77s 0m18.10s \| ModularArithmetic/ModularBaseSystemProofs \| 0m16.95s \|\| +0m01.15s 0m09.83s \| ModularArithmetic/Montgomery/ZProofs \| 0m08.72s \|\| +0m01.10s 0m08.38s \| Specific/GF1305 \| 0m06.89s \|\| +0m01.49s 0m04.00s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.62s \|\| +0m01.37s 0m03.61s \| ModularArithmetic/Tutorial \| 0m05.40s \|\| -0m01.79s 0m16.27s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m16.14s \|\| +0m00.12s 0m13.68s \| Experiments/SpecEd25519 \| 0m13.66s \|\| +0m00.01s 0m10.18s \| Util/ZUtil \| 0m09.70s \|\| +0m00.48s 0m08.91s \| Testbit \| 0m09.14s \|\| -0m00.23s 0m03.99s \| BaseSystemProofs \| 0m03.85s \|\| +0m00.14s 0m03.96s \| Util/ListUtil \| 0m04.19s \|\| -0m00.23s 0m03.60s \| ModularArithmetic/BarrettReduction/ZHandbook \| 0m03.59s \|\| +0m00.01s 0m03.37s \| Experiments/SpecificCurve25519 \| 0m03.36s \|\| +0m00.01s 0m02.90s \| ModularArithmetic/BarrettReduction/ZGeneralized \| 0m02.90s \|\| +0m00.00s 0m02.51s \| Experiments/EdDSARefinement \| 0m01.78s \|\| +0m00.72s 0m02.28s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.35s \|\| -0m00.07s 0m02.25s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.27s \|\| -0m00.02s 0m01.58s \| Util/Tuple \| 0m01.63s \|\| -0m00.04s 0m01.53s \| Encoding/PointEncodingPre \| 0m02.33s \|\| -0m00.80s 0m01.47s \| ModularArithmetic/BarrettReduction/Z \| 0m01.54s \|\| -0m00.07s 0m01.27s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.93s \|\| +0m00.34s 0m01.19s \| Util/NatUtil \| 0m01.10s \|\| +0m00.08s 0m01.19s \| ModularArithmetic/ExtendedBaseVector \| 0m01.18s \|\| +0m00.01s 0m01.18s \| BaseSystem \| 0m01.20s \|\| -0m00.02s 0m01.17s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.04s \|\| +0m00.12s 0m00.97s \| Util/NumTheoryUtil \| 0m00.86s \|\| +0m00.10s 0m00.88s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.94s \|\| -0m00.05s 0m00.87s \| ModularArithmetic/ModularBaseSystemField \| 0m00.92s \|\| -0m00.05s 0m00.84s \| ModularArithmetic/Montgomery/ZBounded \| 0m00.88s \|\| -0m00.04s 0m00.78s \| Spec/ModularWordEncoding \| 0m00.68s \|\| +0m00.09s 0m00.68s \| Encoding/ModularWordEncodingTheorems \| 0m00.75s \|\| -0m00.06s 0m00.66s \| Encoding/ModularWordEncodingPre \| 0m00.79s \|\| -0m00.13s 0m00.65s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.78s \|\| -0m00.13s 0m00.65s \| Util/AdditionChainExponentiation \| 0m00.67s \|\| -0m00.02s 0m00.65s \| Spec/EdDSA \| 0m00.92s \|\| -0m00.27s 0m00.63s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.64s \|\| -0m00.01s 0m00.62s \| ModularArithmetic/ModularBaseSystemList \| 0m00.64s \|\| -0m00.02s 0m00.61s \| ModularArithmetic/ModularBaseSystem \| 0m00.60s \|\| +0m00.01s 0m00.52s \| ModularArithmetic/Pre \| 0m00.49s \|\| +0m00.03s 0m00.50s \| Util/WordUtil \| 0m00.62s \|\| -0m00.12s 0m00.45s \| ModularArithmetic/Pow2Base \| 0m00.47s \|\| -0m00.01s 0m00.44s \| ModularArithmetic/ZBounded \| 0m00.44s \|\| +0m00.00s 0m00.42s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.39s \|\| +0m00.02s 0m00.40s \| ModularArithmetic/Montgomery/Z \| 0m00.41s \|\| -0m00.00s 0m00.38s \| Spec/ModularArithmetic \| 0m00.56s \|\| -0m00.18s
*	Add a faster zsimplify database	Jason Gross	2016-08-16
\|
*	More 8.4 compat	Jason Gross	2016-08-16
\|
*	Add some list util, and decode'_map_mul	Jason Gross	2016-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 3m41.37s \| Total \| 3m29.78s \|\| +0m11.59s ------------------------------------------------------------------------------------ 0m49.73s \| Specific/GF25519 \| 0m31.66s \|\| +0m18.06s 0m23.64s \| ModularArithmetic/Pow2BaseProofs \| 0m31.36s \|\| -0m07.71s 0m42.29s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m44.80s \|\| -0m02.50s 0m08.88s \| Specific/GF1305 \| 0m07.07s \|\| +0m01.81s 0m19.09s \| ModularArithmetic/ModularBaseSystemProofs \| 0m19.86s \|\| -0m00.76s 0m16.62s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m16.74s \|\| -0m00.11s 0m15.31s \| Experiments/SpecEd25519 \| 0m14.40s \|\| +0m00.91s 0m10.10s \| Testbit \| 0m10.15s \|\| -0m00.05s 0m04.95s \| BaseSystemProofs \| 0m04.49s \|\| +0m00.46s 0m03.96s \| Util/ListUtil \| 0m03.16s \|\| +0m00.79s 0m03.40s \| Experiments/SpecificCurve25519 \| 0m03.31s \|\| +0m00.08s 0m02.36s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m02.69s \|\| -0m00.33s 0m02.23s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.24s \|\| -0m00.01s 0m02.14s \| Util/Tuple \| 0m01.87s \|\| +0m00.27s 0m01.92s \| Experiments/EdDSARefinement \| 0m01.85s \|\| +0m00.06s 0m01.71s \| Encoding/PointEncodingPre \| 0m01.67s \|\| +0m00.04s 0m01.71s \| BaseSystem \| 0m01.28s \|\| +0m00.42s 0m01.28s \| ModularArithmetic/Montgomery/ZBounded \| 0m00.85s \|\| +0m00.43s 0m01.16s \| ModularArithmetic/ExtendedBaseVector \| 0m01.65s \|\| -0m00.49s 0m01.04s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.94s \|\| +0m00.10s 0m00.95s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.96s \|\| -0m00.01s 0m00.89s \| ModularArithmetic/ModularBaseSystemField \| 0m00.90s \|\| -0m00.01s 0m00.87s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.77s \|\| +0m00.09s 0m00.78s \| Encoding/ModularWordEncodingTheorems \| 0m00.69s \|\| +0m00.09s 0m00.73s \| Spec/EdDSA \| 0m00.67s \|\| +0m00.05s 0m00.69s \| Util/AdditionChainExponentiation \| 0m00.74s \|\| -0m00.05s 0m00.68s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.73s \|\| -0m00.04s 0m00.67s \| ModularArithmetic/ModularBaseSystemList \| 0m00.71s \|\| -0m00.03s 0m00.61s \| ModularArithmetic/ModularBaseSystem \| 0m00.70s \|\| -0m00.08s 0m00.52s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.45s \|\| +0m00.07s 0m00.47s \| ModularArithmetic/Pow2Base \| 0m00.42s \|\| +0m00.04s
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-08-16
\|\