fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Put ModularBaseSystem carries in terms of [carry_gen], and pushed this ↵	jadep	2016-07-25
\| \| \| \|	change through the pipeline. Also began the process of redoing canonicalization proofs, attempting to put the messy case analysis in theorem statements rather than separate lemmas.
*	Absolutize some imports	Jason Gross	2016-07-20
\|
*	Remove dependency of ext_base on pseudomersenne	Jason Gross	2016-07-20
\|
*	Use a proof that doesn't require as many assumptions in extended_base_length	Jason Gross	2016-07-20
\|
*	Remove stuff from PseudoMersenneBaseParamProofs.v	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
*	ext_base: now defined in terms of ext_limb_widths	Jason Gross	2016-07-18
\|
*	Move more proofs earlier	Jason Gross	2016-07-18
\|
*	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.
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\|
*	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