fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
*	Variosu 8.5 fixes	Jason Gross	2016-06-20
*	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\|\
\| *	tuple tooling	Andres Erbsen	2016-06-20
\| *	port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...	Andres Erbsen	2016-06-18
* \|	Merge	jadep	2016-06-14
\|\ \
* \| \|	Finished admits for canonicalization proofs.	jadep	2016-06-14
* \| \|	progress on second stage (conditional constant-time subtraction) of canonical...	jadep	2016-06-13
\| * \|	Fix for Coq 8.4pl2	Jason Gross	2016-06-11
* \| \|	starting rewrite using different definition of map	jadep	2016-06-11
\| \|/ \|/\|
\| *	8.5 fixes	Jason Gross	2016-06-10
\|/
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-05-25
\|\
\| *	Remove unfolding, rewrite -> setoid_rewrite	Jason Gross	2016-05-24
* \|	First stage of canonicalization proofs complete; proved 3 carry loops reduce ...	jadep	2016-05-20
\|/
*	Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to	jadep	2016-04-29
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...	jadep	2016-04-28
*	Cleanup of GF25519	jadep	2016-04-20
*	moved lemmas from ModularBaseSystemProofs to various Util files	jadep	2016-04-20
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-04-19
\|\
* \|	Added lemmas to Util/ that are needed for testbit.	jadep	2016-04-19
\| *	Add a tactic for field inequalities	Jason Gross	2016-04-19
\|/
*	Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinate...	jadep	2016-04-14
*	Reverting Util/IterAssocOp to an earlier version for compatibility with Compl...	jadep	2016-04-12
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-03-30
\|\
\| *	Finish absolutizing imports	Jason Gross	2016-03-10
* \|	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
*	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
*	a few lemmas in util about powers of 2 in Bedrock's various rewritten forms	Jade Philipoom	2016-02-15
*	tweaks to util files, including automation for proving positivity/nonnegativi...	Jade Philipoom	2016-02-15
*	GaloisTheory: added lemmas useful for proving Euler's Criterion with GF. NumT...	Jade Philipoom	2016-02-02
*	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 pri...	Jade Philipoom	2016-01-13
\| *	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, move...	Jade Philipoom	2015-11-09
*	ModularBaseSystem: prove some admits in mase system extension	Andres Erbsen	2015-11-07