fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	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