fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	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
\| \| \| \| \| \| \| \|	the commit looks huge)
* \|	added generic encoding spec	Jade Philipoom	2016-02-15
\| \|
* \|	moved two non-primality-dependent lemmas to ModularArithmeticTheorems from ↵	Jade Philipoom	2016-02-15
\| \| \| \| \| \| \| \|	PrimeFieldTheorems
* \|	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
\| \|
* \|	added square roots and an assortment of lemmas about prime fields/rings	Jade Philipoom	2016-02-15
\| \|
* \|	changed the name of the ring to ring, not field	Jade Philipoom	2016-02-15
\| \|
* \|	tweaks to util files, including automation for proving ↵	Jade Philipoom	2016-02-15
\| \| \| \| \| \| \| \|	positivity/nonnegativity in Z
\| *	port bounded iter_op and Edwards doubleAndAdd	Andres Erbsen	2016-02-15
\| \|
\| *	CompleteEdwardsCurve: unifiedAddM1: Closed Under Global Context	Andres Erbsen	2016-02-15
\|/
*	update F Coercions and tutorial	Andres Erbsen	2016-02-14
\|
*	port ModularBaseSystem.v and GF25519.v to F m	Andres Erbsen	2016-02-14
\|
*	Spec/EdDSA: comments, remove prehashing	Andres Erbsen	2016-02-13
\|
*	Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v	Andres Erbsen	2016-02-13
\|
*	prove existance of F inv, implement pow -- CompleteEdwardsCurve.unifiedAdd ↵	Andres Erbsen	2016-02-13
\| \| \| \|	Closed Under Global Context
*	Merge branch 'master' into spec	Jade Philipoom	2016-02-13
\|\
\| *	EdDSA spec ported over to new field implementation	Jade Philipoom	2016-02-13
\| \|
* \|	implement F_opp	Andres Erbsen	2016-02-12
\| \|
\| *	Merge branch 'spec' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2016-02-12
\| \|\ \| \|/ \|/\|
\| *	EdDSA25519: progress on proving PointEncoding admits; code still unorganized	Jade Philipoom	2016-02-12
\| \|
* \|	workaround field with typeclass modulus	Andres Erbsen	2016-02-12
\| \|
* \|	fix imports	Andres Erbsen	2016-02-12
\| \|
* \|	document field issue re-appearing	Andres Erbsen	2016-02-12
\| \|
* \|	port some edwards curve theorems	Andres Erbsen	2016-02-12
\| \|
* \|	make field on F automatically clean up the constant-vomit it expands	Andres Erbsen	2016-02-11
\| \|
* \|	port some Edwards curve stuff from GF to F	Andres Erbsen	2016-02-11
\| \|
* \|	port several theorems from GF to F	Andres Erbsen	2016-02-11
\| \|
* \|	Define F m, a replacement for GF with several benefits.	Andres Erbsen	2016-02-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- F has a human readable complete specification - F is a parametric type, not a parametric module - Different F instances can be disambiguated by type inference, which is more conventient that notation scopes. - F has significant support for non-prime moduli - It should be relatively easy to port existing GF code to F. Since the repository currently contains code referencing both F and GF, it makes sense to keep the names different for now. Later, F may or may not be renamed to GF.
* \|	fresh take at specifications using implicit arguments instead of module ↵	Andres Erbsen	2016-02-07
\| \| \| \| \| \| \| \|	parameters
* \|	remove a dangling About	Andres Erbsen	2016-02-07
\|/
*	removed lingering Check/SearchAbout statements	Jade Philipoom	2016-02-07
\|
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2016-02-07
\|\
* \|	EdDSA25519 : wrote and proved optimized PointEncoding, which encodes y and ↵	Jade Philipoom	2016-02-07
\| \| \| \| \| \| \| \|	the sign bit of x, then solves the curve equation for x ^ 2. Required adding several lemmas to GaloisField (and moving others there from PointFormats).
\| *	PointFormats: prove dangling admit	Andres Erbsen	2016-02-07
\| \|
\| *	Specific/GF25519: factor out lemmas	Andres Erbsen	2016-02-07
\| \|
\| *	Do some work pair-programming with Andres on opts	Jason Gross	2016-02-05
\| \| \| \| \| \| \| \|	Partially pre-compile various optimizations in GF25519.
\| *	Update build process to use COQPATH & _CoqProject	Jason Gross	2016-02-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Removed all of the files not built by default; they can be resurrected from git history. _CoqProject is the standard way to list the files in a project and to give information to coq_makefile. COQPATH is the standard way to make use of not-yet-installed libraries that are not part of your project (i.e., you don't want to remove them when you `make clean`, etc.).
* \|	GaloisTheory: added lemmas useful for proving Euler's Criterion with GF. ↵	Jade Philipoom	2016-02-02
\| \| \| \| \| \| \| \|	NumTheoryUtil: cleanup.
* \|	ModualrBaseSystem: proved lingering admit in subtraction proof.	Jade Philipoom	2016-01-25
\|/
*	NumTheoryUtil: proved Fermat's Little Theorem.	Jade Philipoom	2016-01-23
\|
*	NumTheoryUtil : code cleanup; moved some lemmas to ZUtil.	Jade Philipoom	2016-01-23
\|
*	Import coqprime; use it to prove Euler's criterion.	Jade Philipoom	2016-01-20
\|