fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Stronger contexts	Jason Gross	2017-07-07
\|
*	README: recommend against Coq 8.5	Andres Erbsen	2017-07-07
\|
*	Remove some admitted lemmas	Jason Gross	2017-07-07
\|
*	enforce use of [F.zero], [F.one]; prove Ed25519 admits	Andres Erbsen	2017-07-07
\|
*	prove ModularArithmeticTheorems admits	Andres Erbsen	2017-07-06
\|
*	Curves/Edwards/Affine: prove point compression admits	Andres Erbsen	2017-07-06
\|
*	prove an admit in ArithmeticSynthesisTest	Andres Erbsen	2017-07-06
\|
*	make bench	Andres Erbsen	2017-07-06
\|
*	Don't remove Adam Langley when anonymizing repo	Jason Gross	2017-07-06
\|
*	make bench	Jason Gross	2017-07-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	``` make -j test make -j -k bench touch capture.sh make -k bench sudo etc/turboboost.sh off sudo etc/hyperthreading.sh off touch capture.sh make -k bench sudo etc/turboboost.sh on sudo etc/hyperthreading.sh on ```
*	Fix a typo that ends up not mattering	Jason Gross	2017-07-06
\|
*	benchmark NISTZ256 with and without adx	Andres Erbsen	2017-07-05
\|
*	capture.sh require constant TSC	Andres Erbsen	2017-07-05
\|
*	s/bash/sh	Andres Erbsen	2017-07-05
\|
*	make bench	Andres Erbsen	2017-07-05
\|
*	fix .h dependencies in makefile (closes #235)	Andres Erbsen	2017-07-05
\|
*	etc: add scripts to control turbo boost and hyper threading	Andres Erbsen	2017-07-05
\|
*	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
\| \|