fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Weaker UniformBase assumptions	Jason Gross	2016-08-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 0m59.51s \| Total \| 0m59.14s \|\| +0m00.37s ---------------------------------------------------------------------------------- 0m16.46s \| ModularArithmetic/ModularBaseSystemProofs \| 0m16.45s \|\| +0m00.01s 0m14.41s \| Specific/GF25519 \| 0m14.36s \|\| +0m00.05s 0m08.35s \| ModularArithmetic/Pow2BaseProofs \| 0m08.58s \|\| -0m00.23s 0m04.71s \| Testbit \| 0m04.33s \|\| +0m00.37s 0m03.41s \| Experiments/SpecificCurve25519 \| 0m03.31s \|\| +0m00.10s 0m02.09s \| Specific/GF1305 \| 0m02.05s \|\| +0m00.04s 0m02.02s \| ModularArithmetic/ModularBaseSystemOpt \| 0m02.09s \|\| -0m00.06s 0m01.71s \| ModularArithmetic/BarrettReduction/ZBounded \| 0m01.70s \|\| +0m00.01s 0m01.15s \| ModularArithmetic/ExtendedBaseVector \| 0m01.16s \|\| -0m00.01s 0m00.91s \| ModularArithmetic/Montgomery/ZBounded \| 0m00.84s \|\| +0m00.07s 0m00.90s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.92s \|\| -0m00.02s 0m00.86s \| ModularArithmetic/ModularBaseSystemField \| 0m00.90s \|\| -0m00.04s 0m00.69s \| ModularArithmetic/ModularBaseSystemList \| 0m00.61s \|\| +0m00.07s 0m00.65s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.66s \|\| -0m00.01s 0m00.61s \| ModularArithmetic/ModularBaseSystem \| 0m00.57s \|\| +0m00.04s 0m00.59s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.62s \|\| -0m00.03s
*	Tweaks for 8.4 compatibility	jadep	2016-08-11
\|
*	Removed old conversion cruft and fixed Testbit to fit new decode_bitwise proofs	jadep	2016-08-11
\|
*	{base} -> base	Jason Gross	2016-07-19
\|
*	rewrote Testbit and factored out some necessary lemmas about 'uniform' bases ↵	jadep	2016-07-18
\| \| \| \|	(bases that are repeats of the same power of 2) into Pow2Base
*	Merged changes, including new ZUtil conventions.	jadep	2016-07-06
\|\
\| *	Make ZUtil more uniform	Jason Gross	2016-07-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The standard library uses Z., and Z and Z_* are compatibility notations. We follow suit. Also, eliminate a few lemmas that are duplicates of ones in the standard library.
* \|	added and proved shift/or decode operation 'decode_bitwise'	jadep	2016-06-30
\|/
*	8.5 fixes	Jason Gross	2016-06-10
\|
*	Defined a testbit variant for BaseSystem vectors and proved equivalence to ↵	jadep	2016-04-19
	Z.testbit.