fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	added and proved shift/or decode operation 'decode_bitwise'	jadep	2016-06-30
*	encode operation in ModularBaseSystem now uses bitwise operators, taking adva...	jadep	2016-06-29
*	BaseSystem encode function is no longer naive; it does a mod/div loop rather ...	jadep	2016-06-28
*	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-06-27
\|\
* \	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-06-27
\|\ \
\| \| *	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
\| \| *	Fix notation level	Jason Gross	2016-06-27
\| \| *	Add global notation for eq_dec	Jason Gross	2016-06-27
\| \|/
\| *	scalarmult support; EdDSA.sign produces valid signatures	Andres Erbsen	2016-06-27
\| *	first pass of scalarmult	Andres Erbsen	2016-06-27
\| *	Add a tactic to handle "at most two square roots"	Jason Gross	2016-06-27
\| *	Fix for Coq 8.4	Jason Gross	2016-06-25
\| *	EdDSA: prove things about spec	Andres Erbsen	2016-06-25
* \|	update new lemma in CompleteEdwardsCurve/Pre to match other changes to that file	jadep	2016-06-25
* \|	Merge branch 'master' of github.com:mit-plv/fiat-crypto into pointencoding_port	jadep	2016-06-24
\|\\|
* \|	merging point encoding port	jadep	2016-06-24
\|\ \
* \| \|	Ported PointEncodings to parameterize over field rather than modulus.	jadep	2016-06-24
\| \| *	Various nsatz and field tactic improvements	Jason Gross	2016-06-24
\| \| *	Add a version of common_denominator w/o oversimpl	Jason Gross	2016-06-24
\| \| *	Remove a useless intro	Jason Gross	2016-06-24
\| \|/
\| *	ExtendedCoordinates: group.	Andres Erbsen	2016-06-24
\| *	isomorphism_to_subgroup_group	Andres Erbsen	2016-06-24
\| *	Use Decidable machinery for is_eq_dec	Jason Gross	2016-06-24
\| *	nsatz_contradict can now handle invalid _ <> _ hypotheses	Jason Gross	2016-06-23
\| *	Add Unit.v	Jason Gross	2016-06-23
\| *	Add equality on sum types	Jason Gross	2016-06-23
\| *	Merge pull request #8 from mit-plv/rsloan-pipeline-example-init	Jason Gross	2016-06-23
\| \|\
\| \| *	Remove examples for 8.4 compatibility	Robert Sloan	2016-06-23
\| \| *	Remove vestigal BoundedWord machinery	Robert Sloan	2016-06-23
\| * \|	Improve some tactics and lemmas	Jason Gross	2016-06-23
\| * \|	[break_match] should not be local	Jason Gross	2016-06-23
\| \| *	Remove vestigal GaloisField machinery	Robert Sloan	2016-06-23
\| * \|	Add tactics to Tactics, at most 2 sq-roots to Algebra	Jason Gross	2016-06-23
\| \| *	Make Pipeline.v Build on 8.4	Robert Sloan	2016-06-23
\| \|/
\| *	Merge pull request #7 from mit-plv/rsloan-unstable	Rob Sloan	2016-06-23
\| \|\
\| \| *	Add Language.v, Conversion.v to _CoqProject	Robert Sloan	2016-06-23
\| * \|	surjective homomorphism from group makes a group	Andres Erbsen	2016-06-23
\| \| *	Merge branch 'master' of github.com:mit-plv/fiat-crypto into public/rsloan-un...	Robert Sloan	2016-06-23
\| \| \|\ \| \| \|/ \| \|/\|
\| \| *	QhasmUtil.v: Remove 8.4-incompatible intro name	Robert Sloan	2016-06-23
\| \| *	Pipeline: several new examples	Robert Sloan	2016-06-23
\| * \|	Make [nsatz_contradict] better at inequalities	Jason Gross	2016-06-23
\| \| *	Pseudize Lemmas for Dual Operations	Robert Sloan	2016-06-23
\| * \|	[field_algebra] now knows that 0 <> -0 is false	Jason Gross	2016-06-23
\| * \|	Work around bug #4851 in nsatz	Jason Gross	2016-06-23
\| * \|	Add tactics for canonicalizing field (in)equalities	Jason Gross	2016-06-23
\| * \|	Rename the nonzero lemma to an iff lemma	Jason Gross	2016-06-23
\| * \|	Add mul_nonzero_nonzero_and to Algebra.v	Jason Gross	2016-06-23