fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Various nsatz and field tactic improvements	Jason Gross	2016-06-24
*	Use Decidable machinery for is_eq_dec	Jason Gross	2016-06-24
*	Add Unit.v	Jason Gross	2016-06-23
*	Add equality on sum types	Jason Gross	2016-06-23
*	Improve some tactics and lemmas	Jason Gross	2016-06-23
*	[break_match] should not be local	Jason Gross	2016-06-23
*	Add tactics to Tactics, at most 2 sq-roots to Algebra	Jason Gross	2016-06-23
*	Fix broken notations (hopefully)	Jason Gross	2016-06-22
*	Fix missing notations	Jason Gross	2016-06-22
*	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
*	Fix for broken abstract	Jason Gross	2016-06-22
*	Add decidability util file	Jason Gross	2016-06-22
*	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