fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
* \| \|	Add some proofs about Z.div and Z.mul	Jason Gross	2016-07-01
* \| \|	Add [specialize_by] tactic	Jason Gross	2016-07-01
* \| \|	Fix a typo in Zsplit_sums	Jason Gross	2016-07-01
* \| \|	Add tactic to split sums and differences in inequalities	Jason Gross	2016-07-01
* \| \|	Add fraction inequality reasoning tactics to ZUtil	Jason Gross	2016-07-01
* \| \|	Add a proof of 2 * x - x = x	Jason Gross	2016-06-30
* \| \|	Add a classification of n / m < 0	Jason Gross	2016-06-30
* \| \|	Add a tactic for making use of destructed <? in Z	Jason Gross	2016-06-30
* \| \|	Prove that a ^ k <> 0	Jason Gross	2016-06-30
\| * \|	added and proved shift/or decode operation 'decode_bitwise'	jadep	2016-06-30
* \| \|	Add pow_Zpow to Util.ZUtil	Jason Gross	2016-06-30
\| \|/ \|/\|
* \|	Fix field_algebra in 8.4	Jason Gross	2016-06-28
* \|	Fix super_nsatz tactic to be better about ordering	Jason Gross	2016-06-28
* \|	Tuple: from_list_to_list	Andres Erbsen	2016-06-28
\|/
*	Add [destruct_head] tactics	Jason Gross	2016-06-27
*	Add [break_match] for hypotheses	Jason Gross	2016-06-27
*	Add decidable instances for sumwise and fieldwise	Jason Gross	2016-06-27
*	Add a tactic for dealing with equalities of [sum]	Jason Gross	2016-06-27
*	EdDSA: prove things about spec	Andres Erbsen	2016-06-25
*	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
\|\