fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	proved an admit in field homomorphisms that turned out to be unprovable; I ↵	jadep	2016-07-15
\| \| \| \|	added another precondition and pushed it through everywhere but one place in ExtendedCoordinates, where I was stuck.
*	s/conservative_common_denominator/common_denominator/g	Andres Erbsen	2016-07-11
\|
*	remove field_algebra	Andres Erbsen	2016-07-11
\|
*	wrap nsatz in Algebra	Andres Erbsen	2016-07-11
\|
*	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
\| \| \|
\| \| *	Remove a useless intro	Jason Gross	2016-06-24
\| \|/
\| *	Integrate Pseudize into Pipeline.v	Robert Sloan	2016-06-23
\| \|
\| *	Pseudize Let_In	Robert Sloan	2016-06-23
\| \|
\| *	Fix broken notations (hopefully)	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).
\| *	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\| \|
\| *	move nsatz into tactics directory	Andres Erbsen	2016-06-20
\| \|
\| *	port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try ↵	Andres Erbsen	2016-06-18
\| \| \| \| \| \| \| \|	fewer nonzero ports. remove FField and FNsatz
\| *	edwards curve addition respects field homomorphism	Andres Erbsen	2016-06-16
\| \|
\| *	prove ring admits	Andres Erbsen	2016-06-16
\| \|
\| *	edwards curve preliminaries: replace oncurve proof with nsatz	Andres Erbsen	2016-06-16
\| \|
\| *	nsatz: reimplement, integrate, demonstrate	Andres Erbsen	2016-06-15
\| \|
\| *	refactor nsatz wrappers into algebra file	Andres Erbsen	2016-06-14
\| \|
\| *	[field] and [nsatz] do things now again	Andres Erbsen	2016-06-14
\| \|
\| *	stuck because overloading-by-typeclasses sucks	Andres Erbsen	2016-06-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Using typeclasses for overloading clutters all users of the typeclass with an extra layer of indirection that would need to be unfolded in all proofs. Condemning all downstream Ltac to handling a new layer of definitions that have no semantic dignificance is suboptimal design (and encourages even worse design decisions like unfolding during rewriting). Overloading should be fully resolved during type inference, the resulting code must not be distinguishable from having the overloading resolved manually before entering the code.
* \|	Minor 8.5 changes	Jason Gross	2016-06-10
\| \|
* \|	More changes for 8.5	Jason Gross	2016-06-10
\| \| \| \| \| \| \| \|	[Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior
\| *	generic field definition	Andres Erbsen	2016-06-07
\|/
*	Finish absolutizing imports	Jason Gross	2016-03-10
\| \| \| \| \| \| \| \| \| \| \| \|	The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" \| xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
*	port some edwards curve theorems	Andres Erbsen	2016-02-12