fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Removed lingering print statement.	jadep	2016-07-21
\|
*	re-introduced extra field isomorphism layer for 8.4 compatibility and better ↵	jadep	2016-07-21
\| \| \| \|	organization of reasoning.
*	restructured ModularBaseSystem pipeline to put tuple conversion before ↵	jadep	2016-07-20
\| \| \| \|	ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt
*	Fixed unsimplified multiplication definitions in Specific by separating out ↵	jadep	2016-07-18
\| \| \| \|	the zsimplify step; after inserting clauses, we can't rewrite under the binders, but we can do the rewrite and insertions in different definitions.
*	more changes to Specific for 8.4 compatibility	jadep	2016-07-15
\|
*	re-cleaned operations in Specific and updated GF25519 to match GF1305	jadep	2016-07-12
\|
*	cleaned Specific operations so they produce code without proof terms, and ↵	jadep	2016-07-12
\| \| \| \|	proved that GF1305 is a field
*	pushing through a tweak to the arguments of [sub], and defining a field over ↵	jadep	2016-07-12
\| \| \| \|	ModularBaseSystemInterface using some placeholder operations.
*	ported Specific files to use ModularBaseSystemInterface	jadep	2016-07-11
\|
*	defined some group operations, stated group lemma for tuple-based [add] (in ↵	jadep	2016-07-08
\| \| \| \|	terms of isomorphism to ModularArithmetic.F), proved lemma about tuple-based [mul] based on the goals generated by the group constructor
*	stuck trying to figure out dependently typed continuation passing style	Andres Erbsen	2016-07-06
\|
*	Canonicalization is now automated in GF25519 and added to GF1305.	jadep	2016-06-17
\|
*	PseudoMersenneBaseRep.mul now carries by default (made possible by strictly ↵	jadep	2016-06-15
\| \| \| \|	base-length digit vectors)
*	Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ↵	jadep	2016-05-09
\| \| \| \|	unsigned integer underflow. Also changed rep in Specific proofs so that it is PseudoMersenneBaseRep.rep rather than ModularBaseSystem.rep; these are equivalent but the first is the abstraction level we want.
*	added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ↵	jadep	2016-04-21
	weight 2^26)