fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Update display logs and c files	Jason Gross	2017-11-12
\|
*	Add more constant notations	Jason Gross	2017-11-12
\|
*	Update display logs and c files	Jason Gross	2017-11-12
\|
*	Add more constant notations	Jason Gross	2017-11-12
\|
*	generate LaTeX tables from some of the benchmarks	jadep	2017-11-12
\|
*	Update display logs and c files	Jason Gross	2017-11-12
\|
*	Add more constant notations	Jason Gross	2017-11-12
\|
*	Update display logs and c files	Jason Gross	2017-11-12
\|
*	Add more constant notations	Jason Gross	2017-11-12
\|
*	andres doesn't know what year it is	jadep	2017-11-12
\|
*	Add autosolve admit package	Jason Gross	2017-11-12
\|
*	Remove outdated C128 files	Jason Gross	2017-11-12
\|
*	add reflexivity to reify autosolve	Jason Gross	2017-11-12
\|
*	Use abstract in ring autosolve	Jason Gross	2017-11-12
\|
*	add back incorrectly deleted files	jadep	2017-11-12
\|
*	automatic modifications to _Coqproject with new files	jadep	2017-11-12
\|
*	new autogenerated files	jadep	2017-11-12
\|
*	update remake-curves.sh and Makefile	jadep	2017-11-12
\|
*	changes to parameter-generation script	jadep	2017-11-12
\|
*	fix comment	jadep	2017-11-12
\|
*	benchmark montgomery32, gmpvar, and gmpsec on 32-bit android	Andres Erbsen	2017-11-11
\| \| \| \| \| \| \| \|	Despite significant effort, I did not manage to compiler gmpxx in a way that would allow it to be dynamically linked with the c++ standard library on android, or statically link the library in a way that would result in a file executable on Android. Somebody who understands C and Android dynamic linking might be able to do better.
*	Add Decidable2Bool	Jason Gross	2017-11-11
\|
*	Add ListUtil.Forall	Jason Gross	2017-11-11
\|
*	First intro and split in Zring_prod_eq_tac, before cbv -	Jason Gross	2017-11-11
\|
*	Also unfold tuple for reification	Jason Gross	2017-11-11
\|
*	Update display logs and c files	Jason Gross	2017-11-10
\|
*	Update display logs and c files	Jason Gross	2017-11-10
\|
*	Update display logs and c files	Jason Gross	2017-11-10
\|
*	Handle more base types in Z.Reify	Jason Gross	2017-11-10
\|
*	Add more fine-grained cmovnz notations	Jason Gross	2017-11-10
\| \| \| \| \| \|	Builds, but haven't tested the output This closes #265
*	benchmark solinas32 on a 32-bit processor	Andres Erbsen	2017-11-10
\|
*	More modularity in autosolve	Jason Gross	2017-11-10
\|
*	first benchmark on 32-bit Android	Andres Erbsen	2017-11-10
\|
*	Handle tuples in reification	Jason Gross	2017-11-10
\|
*	Add unfold_flat_interp_tuple	Jason Gross	2017-11-10
\|
*	Use match in flat_interp_{,un}tuple'	Jason Gross	2017-11-10
\| \| \| \| \| \|	This way, when we unfold them, we don't create multiple copies of the argument. This is needed for proper reification of x25519 alternate mul, square code in the new pipeline
*	Separate case for handling option matches in autosolve	Jason Gross	2017-11-10
\|
*	Add cbn [val] in autosolve	Jason Gross	2017-11-10
\|
*	Update make_curve.py for python3	Jason Gross	2017-11-10
\| \| \| \| \| \|	In python2, we require unicode. In python3, "unicode" as a type doesn't exist. So we do a feature-check-kludge to set unicode to str if it doesn't exist.
*	Revert "Update make_curve.py for python3"	Jason Gross	2017-11-10
\| \| \| \| \| \|	This reverts commit a5fc7539c5688190f7622266c8e0959efbca80be. Didn't actually work
*	Update make_curve.py for python3	Jason Gross	2017-11-10
\| \| \| \| \| \| \| \|	In python2, we require unicode. In python3, "unicode" as a type doesn't exist. In most places, we can replace the isinstance check for str/unicode with basestring. In one place where we need to output unicode, we do a terrible hack to set unicode to str if it doesn't exist.
*	Fix opacity of dec_Forall, dec_Exists	Jason Gross	2017-11-10
\|
*	Add dec_if_bool	Jason Gross	2017-11-10
\|
*	Generalize Tuple.dec_fieldwise	Jason Gross	2017-11-09
\|
*	Generalize Forall2_forall_iff	Jason Gross	2017-11-09
\|
*	More generalization of fieldwise'_Proper to dependent types	Jason Gross	2017-11-09
\|
*	Generalize fieldwise Proper lemmas	Jason Gross	2017-11-09
\|
*	Remove from the lite target the slowest file currently in it	Jason Gross	2017-11-09
\| \| \| \|	It takes 7m29.22s on Travis
*	Add fieldwise_lift_and	Jason Gross	2017-11-09
\|
*	Add more versions of fieldwise_Proper	Jason Gross	2017-11-09
\|