fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	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
\|\ \| \| \| \|	Make Pipeline.v Build on 8.4
\| *	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
\|\ \| \| \| \|	Merge Assembly Machinery into Master
\| *	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 ↵	Robert Sloan	2016-06-23
\| \|\ \| \|/ \|/\| \| \|	public/rsloan-unstable
\| *	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
\| \| \| \| \| \| \| \| \| \|	Now our [nsatz] does not barf when you have duplicate equations in the context.
* \|	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
\| \|
\| *	Integrate Pseudize into Pipeline.v	Robert Sloan	2016-06-23
\| \|
\| *	Integrate Pseudize into Pipeline.v	Robert Sloan	2016-06-23
\| \|
\| *	Integrate Pseudize into Pipeline.v	Robert Sloan	2016-06-23
\| \|
\| *	Pseudize Let_In with minor notations	Robert Sloan	2016-06-23
\| \|
\| *	Pseudize Let_In	Robert Sloan	2016-06-23
\| \|
\| *	Add Pseudize, Vectorize, Wordize to the build process	Robert Sloan	2016-06-22
\| \|
\| *	Make Assembly modules 8.5-compatible	Robert Sloan	2016-06-22
\| \|
\| *	Merge with public master	Robert Sloan	2016-06-22
\| \|\ \| \|/ \|/\|
* \|	EdDSA.Notations: indentation	Andres Erbsen	2016-06-22
\| \|
* \|	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
\| \| \| \| \| \| \| \| \| \|	This prevents notation conflicts (see comment in Notations.v for more explanation).
* \|	Fix for broken abstract	Jason Gross	2016-06-22
\| \| \| \| \| \| \| \|	It breaks when used in [Instance ... := _.]
\| *	Replace NPeano -> Nat in src/Spec/EdDSA	Robert Sloan	2016-06-22
\| \|
* \|	Add decidability util file	Jason Gross	2016-06-22
\| \| \| \| \| \| \| \| \| \|	This will be useful for the Weierstrass curves, which require case-splitting on field equality.
* \|	Handle renaming of NPeano.pow to Nat.pow (#3)	Jason Gross	2016-06-22
\| \| \| \| \| \| \| \|	We leave ambiguous which [pow] and [modulo] we refer to, so that this builds in both 8.4 and 8.5
\| *	Merge with plv/master	Robert Sloan	2016-06-22
\| \|\ \| \|/ \|/\|
\| *	Merging Pipeline.v	Robert Sloan	2016-06-22
\| \|\
\| * \	squash commits + revert makefile	Robert Sloan	2016-06-22
\| \|\ \
\| * \| \|	Fix build process	Robert Sloan	2016-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix build process Fix build process
\| * \| \|	Full automation for relevant parts of pseudo conversion except lets	Robert Sloan	2016-06-22
\| \| \| \|
\| * \| \|	Reorganization of wordize.v	Robert Sloan	2016-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	first pseudo conversion lemma Decent machinery for automatic pseudo-conversion Decent machinery for automatic pseudo-conversion Decent machinery for automatic pseudo-conversion
\| * \| \|	Merging wordization and bounding together in Wordize.v	Robert Sloan	2016-06-22
\| \| \| \|
\| * \| \|	Really complex derivation of wand correctness	Robert Sloan	2016-06-22
\| \| \| \|
\| * \| \|	Proper word-based vectorization	Robert Sloan	2016-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Basic wordization lemmas Really complex derivation of wand correctness
\| * \| \|	ed25519: indentation fix	Andres Erbsen	2016-06-22
\| \| \| \|