fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix display target	Jason Gross	2017-07-03
\|
*	X25519 test (passed on first try)	Andres Erbsen	2017-07-02
\|
*	automate P256 integration	Andres Erbsen	2017-07-02
\|
*	Merge branch 'use-cmovznz' of https://github.com/JasonGross/fiat-crypto	Andres Erbsen	2017-07-02
\|\
* \|	make display	Andres Erbsen	2017-07-01
\| \|
* \|	changes to log files after running make c	jadep	2017-07-01
\| \|
* \|	add missing import	jadep	2017-06-30
\| \|
* \|	Fix misnamed references in Specific/ (broke after saturated arithetic reorg)	jadep	2017-06-30
\| \|
* \|	Reorganization of saturated arithmetic	jadep	2017-06-29
\| \|
\| *	make display	Jason Gross	2017-06-29
\| \|
* \|	make display	Jason Gross	2017-06-29
\| \|
* \|	Fix unfolding to not unfold sub_with_get_borrow in P256	Jason Gross	2017-06-29
\|/
*	Use -std=gnu11 for older versions of gcc	Jason Gross	2017-06-28
\|
*	match C code in Jacobian addition	Andres Erbsen	2017-06-27
\|
*	p256 compilation and benchmarks with manual kludges	Andres Erbsen	2017-06-27
\|
*	More proof fixing	Jason Gross	2017-06-26
\|
*	Remove an admit	Jason Gross	2017-06-26
\| \| \| \|	This proof should possibly be factored out and go elsewhere.....
*	make display	Jason Gross	2017-06-26
\|
*	Add nonzero synthesis	Jason Gross	2017-06-26
\|
*	make display on p256	Andres Erbsen	2017-06-25
\|
*	make display	Jason Gross	2017-06-25
\|
*	make display	Jason Gross	2017-06-24
\|
*	Fix some things not being unfolded	Jason Gross	2017-06-24
\|
*	make display	Jason Gross	2017-06-24
\|
*	Clean up some montgomery wbw instantiation, make display	Jason Gross	2017-06-24
\|
*	Remove admits	Jason Gross	2017-06-24
\|
*	make bench	Andres Erbsen	2017-06-23
\|
*	Fix an issue with notations	Jason Gross	2017-06-22
\| \| \| \| \|	CNotations breaks writing of Gallina and Ltac `match`. So we need to import it very, very late.
*	make display	Jason Gross	2017-06-22
\|
*	Add (partially admitted) integration tests for add, sub, opp	Jason Gross	2017-06-22
\|
*	P256: Partial work on add, sub, opp	Jason Gross	2017-06-22
\| \| \| \|	Partial work towards #218
*	Fix an [sz] that shouldn't have been removed in the previous commit	Jason Gross	2017-06-22
\|
*	P256: Keep around < eval N bounds	Jason Gross	2017-06-22
\| \| \| \| \| \|	This closes #220 The code before the glue part of the pipeline is getting kind-of ugly...
*	Add sig_conj_by_impl2	Jason Gross	2017-06-22
\|
*	move Specifi p256 files into their own directory	Andres Erbsen	2017-06-22
\|
*	Fix some minor naming bugs in sig_assoc tactics	Jason Gross	2017-06-22
\|
*	Add tighter bounds to MontgomeryP256{,_128}	Jason Gross	2017-06-22
\|
*	compile src/Specific/IntegrationTestMontgomeryP256.s	Andres Erbsen	2017-06-21
\|
*	Use is_bounded_by_None_repeat_In_iff_lt, remove axiom	Jason Gross	2017-06-20
\| \| \| \|	This actually closes #211
*	make display	Jason Gross	2017-06-20
\|
*	make display	Jason Gross	2017-06-20
\|
*	make display	Jason Gross	2017-06-20
\|
*	Enable a-nf for montgomery	Jason Gross	2017-06-20
\| \| \| \|	This fixes adc-fusion, and closes #214.
*	make display	Jason Gross	2017-06-20
\|
*	make display	Jason Gross	2017-06-20
\|
*	make display	Jason Gross	2017-06-20
\|
*	make display (new conditional_sub)	Jason Gross	2017-06-20
\|
*	Make use of new conditional_subtract	Jason Gross	2017-06-20
\|
*	make bench	Jason Gross	2017-06-20
\|
*	check in icc-compiled IntegrationTestMontgomeryP256.s	Andres Erbsen	2017-06-20
\|