fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	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
\|
*	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 ↵	Jade Philipoom	2016-01-13
\| \| \| \| \| \| \| \|	primitive roots.
\| *	Merge branch 'specific-rewrite'	Andres Erbsen	2016-01-06
\|/\|
\| *	fix letify to only insert a term once	Andres Erbsen	2016-01-06
\| \|
* \|	Util: added util lemmas needed to instantiate EdDSA25519.	Jade Philipoom	2016-01-05
\|/
*	reorganized lemmas; moved several to ListUtil and ZUtil.	Jade Philipoom	2015-11-24
\|
*	Added base_succ precondition to BaseSystem to help prove carrying.	Jade Philipoom	2015-11-19
\|
*	ModularBaseSystem: carry_rep has boring modular arithmetic proofs	Andres Erbsen	2015-11-17
\|
*	ModularBaseSystem.carry: implement, state lemmas, some progress on proofs	Andres Erbsen	2015-11-17
\|
*	BaseSystem: more boring	Andres Erbsen	2015-11-10
\|
*	ModularBaseSystem: finished most admits for addition and multiplication, ↵	Jade Philipoom	2015-11-09
\| \| \| \|	moved some lemmas to ListUtil.
*	ModularBaseSystem: prove some admits in mase system extension	Andres Erbsen	2015-11-07
\|
*	ModularBaseSystem: continuing to prove base_good.	Jade Philipoom	2015-11-07
\|
*	Merge remote-tracking branch 'jadep/master'	Andres Erbsen	2015-11-06
\|\
* \|	instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19)	Andres Erbsen	2015-11-06
\| \|
\| *	Added lemmas to ListUtil and BaseSystem to help in ModularBaseSystem.	Jade Philipoom	2015-11-05
\| \|
\| *	Relocated boring tactic to ListUtil and added combine_truncate lemma.	Jade Philipoom	2015-11-04
\|/
*	set_nth_splice case coverage	Andres Erbsen	2015-11-03
\|
*	more set_nth	Andres Erbsen	2015-11-03
\|
*	set_nth	Andres Erbsen	2015-11-01
\|
*	BaseSystem to Util.ListUtil: separate out generic list lemmas	Andres Erbsen	2015-10-29