fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix CSE_sym denote	Jason Gross	2017-07-07
\|
*	Fix proofs broken by previous commit	Jason Gross	2017-07-07
\|
*	Stronger contexts	Jason Gross	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
\|
*	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
\|
*	make bench	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
\|
*	Fix a mis-aligned comment marker in CNotations script	Jason Gross	2017-07-03
\|
*	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
\|\
* \|	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
\| \|
* \|	[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
\| \|
* \|	proved remaining [eval] admits in MontgomeryAPI	jadep	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
\|\ \
\| * \|	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
* \|	Fix comment-in-string issues	Jason Gross	2017-06-29
\| \|
* \|	More C Notations for uin8_t-valued addcarryx	Jason Gross	2017-06-29
\| \|
* \|	Remove a [Check]	Jason Gross	2017-06-29
\| \|
\| *	Fix comment-in-string issues	Jason Gross	2017-06-29
\| \|
\| *	make display	Jason Gross	2017-06-29
\| \|