fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix the sense of op_{get,with}_carry in Saturated	Jason Gross	2017-06-29
\| \| \| \|	Now it lines up with the things in Z.Definitions
*	Fix unfolding to not unfold sub_with_get_borrow in P256	Jason Gross	2017-06-29
\|
*	Adapt to new arguments of saturated things	Jason Gross	2017-06-29
\|
*	Fix type signatures of saturated things for WBW	Jason Gross	2017-06-29
\| \| \| \| \|	This required admitting some proofs. @jadephilipoom, please sanity-check this.
*	new add/carry chain logic with admitted proofs	jadep	2017-06-29
\|
*	Skeleton for add/subtract chains (see #222)	jadep	2017-06-28
\|
*	Add wrappers for subborrow and add_with_get_carry so they work when it is ↵	jadep	2017-06-28
\| \| \| \|	not known that they split on a power of 2
*	Use -std=gnu11 for older versions of gcc	Jason Gross	2017-06-28
\|
*	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
\|