fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Move side lemmas to appropriate files	jadep	2016-09-17
\|
*	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
*	Move more proofs earlier	Jason Gross	2016-07-18
\|
*	Add more distr_length proofs in BaseSystemProofs	Jason Gross	2016-07-18
\|
*	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.
* \|	BaseSystem encode function is no longer naive; it does a mod/div loop rather ↵	jadep	2016-06-28
\|/ \| \| \|	than sticking the value of the Z input in the first digit. The condition that c is positive has been added to PseudoMersenneBaseParams--it is necessary for this encode and for canonicalization, for which it was previously a section variable.
*	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
\| \| \| \| \|	This prevents notation conflicts (see comment in Notations.v for more explanation).
*	changed representation definition to require digits vector to be the exact ↵	jadep	2016-06-15
\| \| \| \|	length of the base vector
*	Merge	jadep	2016-06-14
\|\
* \|	Finished admits for canonicalization proofs.	jadep	2016-06-14
\| \|
\| *	8.5 fixes	Jason Gross	2016-06-10
\|/
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵	jadep	2016-04-28
\| \| \| \|	general contexts.
*	refactor of Basesystem and ModularBaseSystem; includes general code ↵	Jade Philipoom	2016-03-20
	organization and changes to pseudomersenne base parameters that require bases to be expressed as powers of 2, which reduces the burden of proof on the caller and allows carry functions to use bitwise operations rather than mod and division