fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	finished last cases of nonzero proofs for associativity	jadep	2016-04-21
*	added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ...	jadep	2016-04-21
*	automated most of the code in GF25519	jadep	2016-04-21
*	Cleanup of GF25519	jadep	2016-04-20
*	Pulled generalized code out of GF25519 so that it can be used for other moduli	jadep	2016-04-20
*	moved lemmas from ModularBaseSystemProofs to various Util files	jadep	2016-04-20
*	GF25519 addition	jadep	2016-04-20
*	GF25519: boring stuff -- fixed indentation and removed commented-out code	jadep	2016-04-20
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-04-19
\|\
* \|	Defined a testbit variant for BaseSystem vectors and proved equivalence to Z....	jadep	2016-04-19
* \|	Added lemmas to Util/ that are needed for testbit.	jadep	2016-04-19
\| *	Add a tactic for field inequalities	Jason Gross	2016-04-19
\| *	ed25519 derivation: down to final encoding	Andres Erbsen	2016-04-17
\| *	ed25519 derivation: use representation of F	Andres Erbsen	2016-04-17
\| *	ed25519 derivation: wrangle non-unique representations	Andres Erbsen	2016-04-16
\| *	ed25519 derivation: stuck at main loop	Andres Erbsen	2016-04-16
\| *	ed25519 derivation down to word until main equation	Andres Erbsen	2016-04-16
* \|	Cleaned up and revised DoubleAndAdd.	jadep	2016-04-15
* \|	Removed old iter_op version and its last dependency.	jadep	2016-04-15
\|/
*	Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinate...	jadep	2016-04-14
*	Fixed syntax error (missing bracket) in Ed25519 to make merge build	jadep	2016-04-12
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-04-12
\|\
* \|	Finished refactor of GF25519 (partial evaluation); code builds but needs to b...	jadep	2016-04-12
* \|	Reverting Util/IterAssocOp to an earlier version for compatibility with Compl...	jadep	2016-04-12
* \|	Merge and refactor of GF25519	jadep	2016-04-11
\| *	ed25519: continue derivation	Andres Erbsen	2016-04-08
* \|	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-03-30
\|\\|
\| *	Drop second projections in Ed25519	Jason Gross	2016-03-29
\| *	ed25519 derivation: pair programming with jgross... slow progress	Andres Erbsen	2016-03-24
\| *	nicer verify() derivation starter	Andres Erbsen	2016-03-21
\| *	state top-level derivation for Ed25519.verify	Andres Erbsen	2016-03-20
\| *	instantiate ed25519 sign in spec	Andres Erbsen	2016-03-20
\| *	Ed25519: d is nonsquare	Andres Erbsen	2016-03-20
* \|	fix of GF25519 in progress; created instantiation of PseudoMersenneBaseParams	Jade Philipoom	2016-03-20
* \|	made BaseVector instance global	Jade Philipoom	2016-03-20
* \|	refactor of Basesystem and ModularBaseSystem; includes general code organizat...	Jade Philipoom	2016-03-20
\| *	extended coordinates setoid boilerplate	Andres Erbsen	2016-03-20
* \|	Refactored BaseSystem and ModularBaseSystem.	Jade Philipoom	2016-03-11
\| *	Finish absolutizing imports	Jason Gross	2016-03-10
\| *	Remove [Admitted]; [Qed] is now under a second	Jason Gross	2016-03-08
\| *	Use [rewrite] rather than [change] to speed up Qed	Jason Gross	2016-03-08
* \|	IterAssocOp: now uses arbitrary representation of scalar that implements testbit	Jade Philipoom	2016-03-08
* \|	IterAssocOp : now takes a bound argument instead of just using size of exponent	Jade Philipoom	2016-03-07
\|/
*	IterAssocOp : proved iter_op with function exponential	Jade Philipoom	2016-03-03
*	tweak to NumTheoryUtil so it builds on older Coq versions	Jade Philipoom	2016-03-03
*	CompleteEdwardsCurveTheorems: associativity proof that times out on Qed	Andres Erbsen	2016-03-03
*	Instance Fq_Integral_domain : @Integral_domain (F q) ...	Andres Erbsen	2016-02-28
*	ModularArithmetic: [field] tactic that respects opacity, prettify ExtendedCoo...	Andres Erbsen	2016-02-28
*	Makefile: single-quotes for shell globbing	Andres Erbsen	2016-02-28
*	generic binary exponentiation correctness proof in 3 one-liners	Andres Erbsen	2016-02-26