fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
* \|	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
*	ModularArithmetic: reasonable-time FieldToZ inv implementation	Andres Erbsen	2016-02-26
*	Factor out some bedrock dependencies into WordUtil	Jason Gross	2016-02-25
*	cleanup of bounded iter_op	Jade Philipoom	2016-02-25
*	efficient powmod	Andres Erbsen	2016-02-17
*	update ModularArithmetic tutorial	Andres Erbsen	2016-02-17
*	removed Print Assumptions	Jade Philipoom	2016-02-16
*	proved sqrt_solutions, the last remaining admit for point encodings	Jade Philipoom	2016-02-16
*	moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ...	Jade Philipoom	2016-02-16
*	proved most of point encoding admits, fixed some build system issues (dead im...	Jade Philipoom	2016-02-16
*	added point encodings; some admits remain	Jade Philipoom	2016-02-16
*	cleaned up and ported definition to solve for x ^ 2 in the curve equation	Jade Philipoom	2016-02-16
*	EdDSA: tweaked l_bound	Jade Philipoom	2016-02-15
*	fixed renamed files and added imports for encodings	Jade Philipoom	2016-02-15
*	merge	Jade Philipoom	2016-02-15
\|\
* \|	instantiated FqEncoding and FlEncoding (also fixed indentation, which is why ...	Jade Philipoom	2016-02-15
* \|	added generic encoding spec	Jade Philipoom	2016-02-15
* \|	moved two non-primality-dependent lemmas to ModularArithmeticTheorems from Pr...	Jade Philipoom	2016-02-15
* \|	a few lemmas in util about powers of 2 in Bedrock's various rewritten forms	Jade Philipoom	2016-02-15
\| *	Finish seperating our specs: remove old non-specified code	Andres Erbsen	2016-02-15
\| *	remove Check	Andres Erbsen	2016-02-15
\|/
*	Merge branch 'spec' of github.mit.edu:plv/fiat-crypto into spec	Jade Philipoom	2016-02-15
\|\
* \|	ported some of EdDSA25519 to new field framework	Jade Philipoom	2016-02-15