fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	benchmarking: correct for differences in CPU and TSC frequency	Andres Erbsen	2017-07-05
\|
*	make bench	Andres Erbsen	2017-07-04
\|
*	use att style assembly with icc, test it	Andres Erbsen	2017-07-04
\|
*	test p256 mixed addition	Andres Erbsen	2017-07-04
\| \| \| \| \|	passed after fixing some stupid typos in glue code -- no conceptual issues.
*	work around GCC issues 81294 and 81300	Andres Erbsen	2017-07-03
\|
*	fix mulx argument order using sed, test feadd, femul (fails due to #234)	Andres Erbsen	2017-07-03
\|
*	Don't set COQPATH in travis	Jason Gross	2017-07-03
\| \| \| \|	We don't need it
*	Fix a mis-aligned comment marker in CNotations script	Jason Gross	2017-07-03
\|
*	test display target on travis	Jason Gross	2017-07-03
\|
*	Fix display target	Jason Gross	2017-07-03
\|
*	Remove tabs from .travis.yml	Jason Gross	2017-07-03
\|
*	Clean up .travis.yml	Jason Gross	2017-07-03
\| \| \| \|	It's more readable now
*	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
\|\
* \|	Closed under the global context	Andres Erbsen	2017-07-02
\| \|
* \|	prove [MontgomeryAPI.small_add]	Andres Erbsen	2017-07-02
\| \|
* \|	fix [small_div] arguments	Andres Erbsen	2017-07-02
\| \|
* \|	crypto-defects.md: analyze CVE-2014-3570	Andres Erbsen	2017-07-02
\| \|
* \|	[small] admits progress...	Andres Erbsen	2017-07-01
\| \|
* \|	make display	Andres Erbsen	2017-07-01
\| \|
* \|	proved small_sat_add	jadep	2017-07-01
\| \|
* \|	changes to log files after running make c	jadep	2017-07-01
\| \|
* \|	change opp to runtime_opp	jadep	2017-07-01
\| \|
* \|	make bench: include all benchmarks	Andres Erbsen	2017-07-01
\| \|
* \|	proved remaining [eval] admits in MontgomeryAPI	jadep	2017-07-01
\| \|
* \|	benchmark OpenSSL p256 C code	Andres Erbsen	2017-07-01
\| \|
* \|	openssl curve25519 license	Andres Erbsen	2017-07-01
\| \|
* \|	benchmark OpenSSL curve25519	Andres Erbsen	2017-07-01
\| \|
* \|	Prove saturated carrying-subtraction-chain correct	jadep	2017-07-01
\| \|
* \|	Prove saturated carrying-addition-chain correct	jadep	2017-06-30
\| \|
* \|	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
\| \|
* \|	create directory for saturated arithmetic in preparation for splitting into ↵	jadep	2017-06-29
\| \| \| \| \| \| \| \|	multiple files
* \|	Merge branch 'addsubchains'	jadep	2017-06-29
\|\ \
\| * \|	Update .gitignore with things from make bench	Jason Gross	2017-06-29
\| \| \|
\| * \|	Add proper dependencies on .h file in Makefile	Jason Gross	2017-06-29
\| \| \|
\| * \|	Remove a [Check]	Jason Gross	2017-06-29
\| \| \|
* \| \|	new add/carry chain logic with admitted proofs	jadep	2017-06-29
\| \| \|
* \| \|	Skeleton for add/subtract chains (see #222)	jadep	2017-06-29
\| \| \|
* \| \|	Add wrappers for subborrow and add_with_get_carry so they work when it is ↵	jadep	2017-06-29
\| \| \| \| \| \| \| \| \| \| \| \|	not known that they split on a power of 2
\| \| *	make display	Jason Gross	2017-06-29
\| \| \|
\| \| *	change notation `_ == _ ? _ : _ ` to `cmovznz(_, _, _)`	Jason Gross	2017-06-29
\| \| \| \| \| \| \| \| \| \| \| \|	This closes #228
* \| \|	Update .gitignore with things from make bench	Jason Gross	2017-06-29
\| \|/ \|/\|
* \|	Fix comment-in-string issues	Jason Gross	2017-06-29
\| \|
* \|	More C Notations for uin8_t-valued addcarryx	Jason Gross	2017-06-29
\| \|
* \|	Add proper dependencies on .h file in Makefile	Jason Gross	2017-06-29
\| \|
* \|	Remove a [Check]	Jason Gross	2017-06-29
\| \|
\| *	Fix comment-in-string issues	Jason Gross	2017-06-29
\| \|