fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\|\ \| \| \| \| \| \|	includes broken files to be removed in next commit
\| *	[F q] is [Algebra.field]	Andres Erbsen	2016-06-20
\| \|
\| *	move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems	Andres Erbsen	2016-06-17
\| \|
\| *	Z is integral domain	Andres Erbsen	2016-06-16
\| \|
* \|	More changes for 8.5	Jason Gross	2016-06-10
\| \| \| \| \| \| \| \|	[Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior
* \|	8.5 fixes	Jason Gross	2016-06-10
\|/
*	F: pow_nat_iter_op_correct	Andres Erbsen	2016-05-18
\|
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵	jadep	2016-04-28
\| \| \| \|	general contexts.
*	refactor field lemmas out of ed25519	Andres Erbsen	2016-04-25
\|
*	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 ```
*	CompleteEdwardsCurveTheorems: associativity proof that times out on Qed	Andres Erbsen	2016-03-03
\|
*	ModularArithmetic: reasonable-time FieldToZ inv implementation	Andres Erbsen	2016-02-26
\|
*	efficient powmod	Andres Erbsen	2016-02-17
\|
*	proved sqrt_solutions, the last remaining admit for point encodings	Jade Philipoom	2016-02-16
\|
*	moved two non-primality-dependent lemmas to ModularArithmeticTheorems from ↵	Jade Philipoom	2016-02-15
\| \| \| \|	PrimeFieldTheorems
*	added square roots and an assortment of lemmas about prime fields/rings	Jade Philipoom	2016-02-15
\|
*	update F Coercions and tutorial	Andres Erbsen	2016-02-14
\|
*	prove existance of F inv, implement pow -- CompleteEdwardsCurve.unifiedAdd ↵	Andres Erbsen	2016-02-13
\| \| \| \|	Closed Under Global Context
*	implement F_opp	Andres Erbsen	2016-02-12
\|
*	port some edwards curve theorems	Andres Erbsen	2016-02-12
\|
*	make field on F automatically clean up the constant-vomit it expands	Andres Erbsen	2016-02-11
\|
*	port several theorems from GF to F	Andres Erbsen	2016-02-11
\|
*	Define F m, a replacement for GF with several benefits.	Andres Erbsen	2016-02-11
	- F has a human readable complete specification - F is a parametric type, not a parametric module - Different F instances can be disambiguated by type inference, which is more conventient that notation scopes. - F has significant support for non-prime moduli - It should be relatively easy to port existing GF code to F. Since the repository currently contains code referencing both F and GF, it makes sense to keep the names different for now. Later, F may or may not be renamed to GF.