fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
* \|	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
\| \|
\| *	More C Notations for uin8_t-valued addcarryx	Jason Gross	2017-06-29
\| \|
\| *	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