fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
* \| \|	Allow side-conditions in common denom. all in hyps	Jason Gross	2016-06-29
* \| \|	Handle fractions in denominators	Jason Gross	2016-06-29
* \| \|	Clear symmetric duplicates in clear_algebraic_duplicates	Jason Gross	2016-06-29
\| * \|	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
* \| \|	Fix a typo in the previous commit	Jason Gross	2016-06-28
* \| \|	[super_nstaz]: Handle side-conditions from [nsatz]	Jason Gross	2016-06-28
\| \|/ \|/\|
* \|	Revert "CompleteEdwardsCurveTheorems: build on 8.4 after field_algebra cahnge"	Andres Erbsen	2016-06-28
* \|	No more anomalies from super_nsatz, hopefully	Jason Gross	2016-06-28
* \|	Fix field_algebra in 8.4	Jason Gross	2016-06-28
* \|	CompleteEdwardsCurveTheorems: build on 8.4 after field_algebra cahnge	Andres Erbsen	2016-06-28
* \|	Fix a typo (missing .)	Jason Gross	2016-06-28
* \|	Fix super_nsatz tactic to be better about ordering	Jason Gross	2016-06-28
* \|	EdDSARefinement: work around rewrite_strat for 8.4	Andres Erbsen	2016-06-28
* \|	Tuple: from_list_to_list	Andres Erbsen	2016-06-28
* \|	Try a faster way of solving some inequalities resulting from common_denominator	Jason Gross	2016-06-27
* \|	Actual fix for super_nsatz	Jason Gross	2016-06-27
* \|	Fix super_nstaz to not error	Jason Gross	2016-06-27
* \|	Add a super_nsatz tactic	Jason Gross	2016-06-27
* \|	eddsa refinement setup	Andres Erbsen	2016-06-27
\| *	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