fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Remove EdDSA	Benjamin Barenblat	2019-04-26
\| \| \| \| \|	Remove Spec/EdDSA.v and its reverse dependencies Spec/Ed25519.v and Primitives/EdDSARepChange.v. This code is no longer in use.
*	Import prim token notations before using them	Jason Gross	2018-08-24
\| \| \| \| \| \| \| \| \| \| \|	This is required for compatibility with https://github.com/coq/coq/pull/8064, where prim token notations no longer follow `Require`, but instead follow `Import`. c.f. https://github.com/coq/coq/pull/8064#issuecomment-415493362 Almost all changes were made via https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169#file-fix-py
*	minor updates needed to make it compile with bbv	Samuel Gruetter	2018-02-05
\| \| \| \|	removing lemma wordToNat_wzero is ok because it's already in bbv
*	ScalarMult: Z -> G -> G (closes #193)	Andres Erbsen	2017-06-14
\|
*	rename-everything	Andres Erbsen	2017-04-06
\|
*	use [positive] for [F] modulus, char_ge_C instead of char_gt_C	Andres Erbsen	2017-03-02
\|
*	alternative signing derivation	Andres Erbsen	2016-09-22
\| \| \| \|	cleanup
*	Derive EdDSA.verify from equational specification	Andres Erbsen	2016-09-16
\| \| \| \|	Experiments/SpecEd25519 will come back soon
*	Fully qualify [Require]s	Jason Gross	2016-09-08
\| \| \| \|	This way they won't become ambiguous if we add new files
*	added proofs about addition chain exponentiation for later use in ↵	jadep	2016-07-10
\| \| \| \|	ModularBaseSystem [pow], which we need for sqrt and inversion.
*	scalarmult support; EdDSA.sign produces valid signatures	Andres Erbsen	2016-06-27
\|
*	EdDSA: prove things about spec	Andres Erbsen	2016-06-25
\|
*	EdDSA.Notations: indentation	Andres Erbsen	2016-06-22
\|
*	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
*	EdDSA.v: resolve ambiguity based on ed25519.py	Andres Erbsen	2016-06-21
\|
*	Whitespace change	Jason Gross	2016-06-21
\|
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\|
*	port EdDSA spec	Andres Erbsen	2016-06-20
\|
*	before changing SRep from N to F l	Andres Erbsen	2016-05-27
\|
*	Changed name of Encoding to CanonicalEncoding, and changed notation to match.	jadep	2016-04-29
\|
*	consolidate and rename Edwards curve lemmas	Andres Erbsen	2016-04-25
\|
*	point_eq_dec	Andres Erbsen	2016-04-22
\|
*	ed25519 derivation: pair programming with jgross... slow progress	Andres Erbsen	2016-03-24
\|
*	nicer verify() derivation starter	Andres Erbsen	2016-03-21
\|
*	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 ```
*	Factor out some bedrock dependencies into WordUtil	Jason Gross	2016-02-25
\| \| \| \|	Also move a definition about words, with a TODO about location, into WordUtil.
*	instantiated FqEncoding and FlEncoding (also fixed indentation, which is why ↵	Jade Philipoom	2016-02-15
\| \| \| \|	the commit looks huge)
*	Spec/EdDSA: comments, remove prehashing	Andres Erbsen	2016-02-13
\|
*	Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v	Andres Erbsen	2016-02-13
\|
*	EdDSA spec ported over to new field implementation	Jade Philipoom	2016-02-13