fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	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
*	PointFOrmats,EdDSA: remove redundant axioms	Andres Erbsen	2016-01-16
*	remove duplicate axiom	Andres Erbsen	2016-01-16
*	PointFormats: extended coordinates equivalence proofs	Andres Erbsen	2016-01-16
*	fix merge conflicts + PointFormats proofs	Robert Sloan	2016-01-14
\|\
\| *	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2016-01-13
\| \|\
\| * \|	euler's criterion reduced to fermat's little theorem and two lemmas about pri...	Jade Philipoom	2016-01-13
* \| \|	simple tactic rule	Rob Sloan	2016-01-11
* \| \|	assumption lemmas in PointFormats	Rob Sloan	2016-01-11
* \| \|	simple refactor of makefile; comments	varomodt	2016-01-09
\| \| *	cleanup	Andres Erbsen	2016-01-08
\| \|/ \|/\|
* \|	PointFormats: factor out admits	Andres Erbsen	2016-01-08
* \|	PointFormats: no zero denominators in Edwards addition	Andres Erbsen	2016-01-08
* \|	PointFormats: addition produces points on curve	Andres Erbsen	2016-01-07
* \|	fix field for division by constant (by dmz@mit.edu)	Andres Erbsen	2016-01-07
* \|	fix unverified typo in fermat proof	Andres Erbsen	2016-01-07
* \|	Start writing PointFormats field proofs	Andres Erbsen	2016-01-07
* \|	Merge branch 'specific-rewrite'	Andres Erbsen	2016-01-06
\|\ \ \| \|/ \|/\|
\| *	fix letify to only insert a term once	Andres Erbsen	2016-01-06
* \|	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2016-01-05
\|\ \
* \| \|	Specific/EdDSA25519: created most of specific instantiation of EdDSA; still m...	Jade Philipoom	2016-01-05
* \| \|	PointFormats/EdDSA: scoping tweaks in PointFormats, small changes of phrasing...	Jade Philipoom	2016-01-05
* \| \|	Util: added util lemmas needed to instantiate EdDSA25519.	Jade Philipoom	2016-01-05
\| * \|	remove comment	Andres Erbsen	2016-01-04
\| \| *	prettier GF25519 derivation that runs out of memory	Andres Erbsen	2016-01-04
\| \| *	UNTESTED simplification of specific GF25519 derivation	Andres Erbsen	2016-01-02
\| \|/
\| *	draft of Fermat's Little Theorem	Andres Erbsen	2015-12-31
\|/
*	Code-reviewing EdDSA	Adam Chlipala	2015-12-29
*	PointFormats : removed reliance on Pos.size_nat; doubleAndAdd now takes an ar...	Jade Philipoom	2015-12-28
*	PointFormats : changed iter_op to allow overestimating bitlength of argument.	Jade Philipoom	2015-12-26
*	Removed OpWithZero typeclass in favor of explicit arguments.	Jade Philipoom	2015-12-25
*	PointFormats: completed remaining admits for non-destruction doubleAndAdd.	Jade Philipoom	2015-12-24
*	PointFormats: implemented doubleAndAdd without destructing scalar and proved ...	Jade Philipoom	2015-12-24
*	PointFormats: wrote and proved equivalent a double-and-add implementation of ...	Jade Philipoom	2015-12-20
*	EdDSA: prettification of proofs; parameter l is now a nat instead of a Prime.	Jade Philipoom	2015-12-17
*	EdDSA: Proved verify_valid_passes and rewrote spec in terms of encoding typec...	Jade Philipoom	2015-12-17
*	rename fields for encodings	Andres Erbsen	2015-12-15
*	EdDSA: point encoding is a parameter	Andres Erbsen	2015-12-15
*	PointFormats: all Edwards25519 points are onCurve	Andres Erbsen	2015-12-15
*	another pass over the eddsa spec	Andres Erbsen	2015-12-15
*	EdDSA: mostly-complete spec and preliminary structure.	Jade Philipoom	2015-12-12
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2015-12-10
\|\
* \|	More improved structure for EdDSA and PointFormats.	Jade Philipoom	2015-12-10
* \|	More refacoring PointFormats.	Jade Philipoom	2015-12-09
* \|	Rewrote PointFormats to be parameterized by modulus; reformatting of EdDSA.	Jade Philipoom	2015-12-09
\| *	Remove redundancy in lemma statement	Adam Chlipala	2015-12-09
\|/
*	EdDSA: Added PointFormatsSpec module type (possibly temporary). Transcribed p...	Jade Philipoom	2015-12-07
*	Transcribed EdDSA parameters from [https://eprint.iacr.org/2015/677.pdf].	Jade Philipoom	2015-12-07