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.
*	Changed name of [carry_and_reduce_single] to [carry_single], since it does ↵	jadep	2016-07-21
\| \| \| \|	not perform reduction
*	re-introduced extra field isomorphism layer for 8.4 compatibility and better ↵	jadep	2016-07-21
\| \| \| \|	organization of reasoning.
*	Use update_nth in add_to_nth (#26)	Jason Gross	2016-07-19
\| \| \| \| \| \|	It leads to a slightly more transparent and clearer definition. If I got everything right, nothing should depend on the judgmental definition of [add_to_nth] anymore.
*	Express carry_simple in terms of carry_gen	Jason Gross	2016-07-18
\| \| \| \| \| \|	Also make much of the remaining code outside of Pow2BaseProofs independent of the precise definition of carry_simple. (We use [Local Opaque] to enforce this modularity.
*	Move some definitions to Pow2Base (#24)	Jason Gross	2016-07-18
\| \| \| \| \| \| \| \| \|	* Move some definitions to Pow2Base These definitions don't depend on PseudoMersenneBaseParams, only on limb_widths, and we'll want them for BarrettReduction / P256. * Fix for Coq 8.4
*	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.
*	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.