fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Reorganization and revision of Encoding code and redefinition of sign_bit ↵	jadep	2016-04-25
\| \| \| \|	function.
*	point_eq_dec	Andres Erbsen	2016-04-22
\|
*	ed25519: continue derivation	Andres Erbsen	2016-04-08
\|
*	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
\|
*	instantiate ed25519 sign in spec	Andres Erbsen	2016-03-20
\|
*	Ed25519: d is nonsquare	Andres Erbsen	2016-03-20
\|
*	Finish absolutizing imports	Jason Gross	2016-03-10
\| \| \| \| \| \| \| \| \| \| \| \|	The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" \| xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
*	Factor out some bedrock dependencies into WordUtil	Jason Gross	2016-02-25
\| \| \| \|	Also move a definition about words, with a TODO about location, into WordUtil.
*	efficient powmod	Andres Erbsen	2016-02-17
\|
*	removed Print Assumptions	Jade Philipoom	2016-02-16
\|
*	moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ↵	Jade Philipoom	2016-02-16
\| \| \| \|	CompleteEdwardsCurve, where the precondition is not in scope.
*	proved most of point encoding admits, fixed some build system issues (dead ↵	Jade Philipoom	2016-02-16
\| \| \| \|	imports of PointFormats and Galois things)
*	added point encodings; some admits remain	Jade Philipoom	2016-02-16
\|
*	EdDSA: tweaked l_bound	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
\| \|
\| *	Finish seperating our specs: remove old non-specified code	Andres Erbsen	2016-02-15
\|/
*	ported some of EdDSA25519 to new field framework	Jade Philipoom	2016-02-15
\|
*	update F Coercions and tutorial	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
\|/
*	document field issue re-appearing	Andres Erbsen	2016-02-12
\|
*	port some edwards curve theorems	Andres Erbsen	2016-02-12
\|
*	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