fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Update display logs	Jason Gross	2017-11-01
\|
*	Add more constant notations	Jason Gross	2017-11-01
\|
*	Update display logs	Jason Gross	2017-11-01
\|
*	Add cps versions of id_with_alt	Jason Gross	2017-11-01
\|
*	Update display logs	Jason Gross	2017-11-01
\|
*	Update display logs	Jason Gross	2017-11-01
\|
*	Add more constant notations	Jason Gross	2017-11-01
\|
*	Update display logs	Jason Gross	2017-11-01
\|
*	Add more constant notations	Jason Gross	2017-11-01
\|
*	Make use of from_associational_cps in more places	Jason Gross	2017-11-01
\|
*	More use of Z.eqb_cps	Jason Gross	2017-11-01
\|
*	Switch to AddWithGetCarry in ZExtended	Jason Gross	2017-10-31
\|
*	Add MapBaseType	Jason Gross	2017-10-31
\|
*	Add unextend_op	Jason Gross	2017-10-31
\|
*	Generalize MapBaseType a bit	Jason Gross	2017-10-31
\|
*	Add invert_PairsConst_gen	Jason Gross	2017-10-31
\|
*	add ZToSignedWord, signedWordToZ	Jason Gross	2017-10-31
\|
*	Add wneg_inj	Jason Gross	2017-10-31
\|
*	Fix ZToWord, add wring_eq_ext, speed up some proofs	Jason Gross	2017-10-31
\|
*	Add Bedrock.Word.ZToWord	Jason Gross	2017-10-31
\|
*	Remove trailing spaces	Jason Gross	2017-10-31
\|
*	Bump coq submodule	Jason Gross	2017-10-31
\|
*	Fix smithers build	Jason Gross	2017-10-31
\|
*	fibe: WIP scalarmult for benchmarking field operations	Andres Erbsen	2017-10-31
\|
*	Update display logs	Jason Gross	2017-10-31
\|
*	Update display logs	Jason Gross	2017-10-31
\|
*	Add more constant notations	Jason Gross	2017-10-31
\|
*	Update display logs	Jason Gross	2017-10-29
\|
*	Update display logs	Jason Gross	2017-10-29
\|
*	make update-_CoqProject	Jason Gross	2017-10-29
\|
*	Update display logs	Jason Gross	2017-10-29
\|
*	Add more constant notations	Jason Gross	2017-10-29
\|
*	add prettyprint.py, to eventually replace extract-*.sh	Andres Erbsen	2017-10-28
\|
*	fix python montgomery ladder	Andres Erbsen	2017-10-28
\|
*	check in p384 generated code	Andres Erbsen	2017-10-26
\|
*	gmpxx.c: s/32/modulus_bytes/	Andres Erbsen	2017-10-26
\|
*	add python reference for x25519	Andres Erbsen	2017-10-26
\|
*	add gmpxx.cpp: a higher-level implementation	Andres Erbsen	2017-10-26
\|
*	automate some proofs; also remove trace-based reasoning in favor of ↵	jadep	2017-10-26
\| \| \| \|	induction on fuel
*	invariants don't need to know the fuel	jadep	2017-10-26
\|
*	WIP: loops	jadep	2017-10-26
\|
*	Remove NISTP256/AMD128 from lite target	Jason Gross	2017-10-25
\| \| \|	This hopefully fixes #262
*	Add a missing line continuation in Makefile	Jason Gross	2017-10-24
\|
*	Don't build feadd,fesub,fecarry .c files	Jason Gross	2017-10-24
\| \| \| \|	They don't work with the testing infrastructure, currently.
*	Add inversion_wf_one_constr	Jason Gross	2017-10-24
\|
*	Add MapBaseTypeWf, generalize src/Compilers/MapBaseType.v a bit	Jason Gross	2017-10-24
\|
*	Generalize In_flatten_binding_list_untransfer_interp_flat_type	Jason Gross	2017-10-24
\|
*	Add In_flatten_binding_list_untransfer_interp_flat_type	Jason Gross	2017-10-24
\|
*	Add wff_SmartPairf_SmartValf	Jason Gross	2017-10-24
\|
*	Add MapBaseType	Jason Gross	2017-10-23
\|