fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	match C code in Jacobian addition	Andres Erbsen	2017-06-27
\|
*	p256 compilation and benchmarks with manual kludges	Andres Erbsen	2017-06-27
\|
*	proved eval_mod and eval_div (last remaining eval_ admits in Saturated)	jadep	2017-06-27
\|
*	More proof fixing	Jason Gross	2017-06-26
\|
*	Add a comment for nonzero_cps	Jason Gross	2017-06-26
\|
*	Fix a broken proof	Jason Gross	2017-06-26
\|
*	Factor out admitted proof into admitted lemma	Jason Gross	2017-06-26
\|
*	Remove an admit	Jason Gross	2017-06-26
\| \| \| \|	This proof should possibly be factored out and go elsewhere.....
*	make display	Jason Gross	2017-06-26
\|
*	Add nonzero synthesis	Jason Gross	2017-06-26
\|
*	remove unused admit (has been moved to Tuple.v)	jadep	2017-06-26
\|
*	indentation	Jason Gross	2017-06-25
\|
*	Prove map2_zselect	Jason Gross	2017-06-25
\|
*	Prove map2_append	Jason Gross	2017-06-25
\|
*	Allow disabling adc-fusion	Jason Gross	2017-06-25
\|
*	make display on p256	Andres Erbsen	2017-06-25
\|
*	Fixes #219	jadep	2017-06-25
\|
*	write and prove Tuple.map2_cps	jadep	2017-06-25
\|
*	make display	Jason Gross	2017-06-25
\|
*	Convert adc to sbb when doing [0 - x]	Jason Gross	2017-06-25
\| \| \| \|	Actually this time
*	Revert "Convert adc to sbb when doing [0 - x]"	Jason Gross	2017-06-25
\| \| \| \| \| \|	This reverts commit ecff47dbc867261b81c6e268eca99e5b5ab28805. It was wrong
*	Convert adc to sbb when doing [0 - x]	Jason Gross	2017-06-24
\|
*	make display	Jason Gross	2017-06-24
\|
*	Fix some things not being unfolded	Jason Gross	2017-06-24
\|
*	make display	Jason Gross	2017-06-24
\|
*	Propogate neg through constant multiplication	Jason Gross	2017-06-24
\|
*	Clean up some montgomery wbw instantiation, make display	Jason Gross	2017-06-24
\|
*	Remove admits	Jason Gross	2017-06-24
\|
*	Fill in axioms for sub_then_maybe_add; this required fiddling with updated ↵	jadep	2017-06-24
\| \| \| \|	arguments since more context variables were used in the definitions than in the placeholder axioms
*	made conditional_add a wrapper, defined and proved sub_then_maybe_add	jadep	2017-06-24
\|
*	Make a 'conditionals' section in Columns, and move conditional_add there	jadep	2017-06-24
\|
*	make bench	Andres Erbsen	2017-06-23
\|
*	Weierstrass Jacobian mixed addition	Andres Erbsen	2017-06-23
\|
*	Fix an issue with notations	Jason Gross	2017-06-22
\| \| \| \| \|	CNotations breaks writing of Gallina and Ltac `match`. So we need to import it very, very late.
*	Add notation for logical or	Jason Gross	2017-06-22
\|
*	make display	Jason Gross	2017-06-22
\|
*	Add (partially admitted) integration tests for add, sub, opp	Jason Gross	2017-06-22
\|
*	Fix a typo in push_Zmod that was causing looping	Jason Gross	2017-06-22
\|
*	P256: Partial work on add, sub, opp	Jason Gross	2017-06-22
\| \| \| \|	Partial work towards #218
*	Fix an [sz] that shouldn't have been removed in the previous commit	Jason Gross	2017-06-22
\|
*	P256: Keep around < eval N bounds	Jason Gross	2017-06-22
\| \| \| \| \| \|	This closes #220 The code before the glue part of the pipeline is getting kind-of ugly...
*	Add sig_conj_by_impl2	Jason Gross	2017-06-22
\|
*	Work around bug #5615 (constr not being updated)	Jason Gross	2017-06-22
\| \| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5615, Ltac should be able to bind references and not just names, in which names are slippery, slippery objects.
*	move Specifi p256 files into their own directory	Andres Erbsen	2017-06-22
\|
*	Fix some minor naming bugs in sig_assoc tactics	Jason Gross	2017-06-22
\|
*	Add tighter bounds to MontgomeryP256{,_128}	Jason Gross	2017-06-22
\|
*	Account for future changes of #219	Jason Gross	2017-06-22
\| \| \| \| \|	Note that this makes the axiom we added false. It has a very long and descriptive name to account for this fact.
*	src/Demo.v: a 200-line introduction to BaseSystem ideas	Andres Erbsen	2017-06-21
\|
*	Prove In_to_list_left_tl, In_left_hd, to_list_left_append	Jason Gross	2017-06-21
\|
*	Prove some admitted lemmas about uweight	Jason Gross	2017-06-21
\| \| \| \|	Not sure if locally adding hypotheses is the best way to do it.