fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Remove stuff from PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
\|
*	{base} -> base	Jason Gross	2016-07-19
\|
*	Move two_k_nonzero to PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
\| \| \| \|	It has nothing to do with ext_base
*	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
*	Make [base] and [log_cap] notations	Jason Gross	2016-07-11
\| \| \| \| \| \| \| \|	Also use [ZUtil.Z.pow2_mod]. This lets us remove the dependency of ModularBaseSystem on ModularArithmetic.PseudoMersenneBaseParamProofs. This is a small part of reorganizing and factoring ModularBaseSystem for use with Barrett reduction.
*	Merged changes, including new ZUtil conventions.	jadep	2016-07-06
\|\
* \|	Factored out some proofs that rely only on base being powers of two, and ↵	jadep	2016-07-06
\| \| \| \| \| \| \| \|	defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.
\| *	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.
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\|
*	starting rewrite using different definition of map	jadep	2016-06-11
\|
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵	jadep	2016-04-28
\| \| \| \|	general contexts.
*	Merge and refactor of GF25519	jadep	2016-04-11
\|
*	made BaseVector instance global	Jade Philipoom	2016-03-20
\|
*	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