fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	partition -> Partition.partition to prevent confusion with List.partition	jadep	2019-04-03
\|
*	update _CoqProject, fix indentations, and prune dependencies of new ↵	jadep	2019-04-03
\| \| \| \|	Arithmetic files
*	split up Arithmetic (imports etc. not yet fixed, does not build)	jadep	2019-04-03
\|
*	create directory for saturated arithmetic in preparation for splitting into ↵	jadep	2017-06-29
\| \| \| \|	multiple files
*	Merge branch 'addsubchains'	jadep	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
\| \|
\| *	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 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
\|/
*	proved eval_mod and eval_div (last remaining eval_ admits in Saturated)	jadep	2017-06-27
\|
*	Add a comment for nonzero_cps	Jason Gross	2017-06-26
\|
*	Factor out admitted proof into admitted lemma	Jason Gross	2017-06-26
\|
*	Add nonzero synthesis	Jason Gross	2017-06-26
\|
*	Prove map2_zselect	Jason Gross	2017-06-25
\|
*	Fixes #219	jadep	2017-06-25
\|
*	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
\|
*	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.
*	changed number of limbs partway through conditional_sub; was n, now S n	jadep	2017-06-20
\|
*	Remove duplicate [small p] hypothesis from small_conditional_sub	Jason Gross	2017-06-20
\|
*	Add conditional_sub_id to uncps globally	Jason Gross	2017-06-20
\|
*	defined conditional_sub (see #207) -- small_conditional_sub admitted, ↵	jadep	2017-06-20
\| \| \| \|	eval_conditional_sub proven
*	rename Columns.sub_cps to make it clear that no balance is added	jadep	2017-06-20
\|
*	Don't depend on classical axioms for small_add	Jason Gross	2017-06-20
\| \| \| \|	See [bug #5444](https://coq.inria.fr/bugs/show_bug.cgi?id=5444).
*	Weaken preconditions on small_add	Jason Gross	2017-06-20
\|
*	Strip trailing whitespace	Jason Gross	2017-06-20
\|
*	fixed precondition on small_add	jadep	2017-06-19
\|
*	proved small_scmul	jadep	2017-06-18
\|
*	proved eval_scmul	jadep	2017-06-18
\|
*	proved small_zero	jadep	2017-06-18
\|
*	proved small_drop_high	jadep	2017-06-18
\|
*	proved eval_drop_high	jadep	2017-06-18
\|
*	define strong small and re-prove small_add and small_compact with that ↵	jadep	2017-06-18
\| \| \| \|	definition
*	make scmul discard its carry in a saner way; rather than concatenating it in ↵	jadep	2017-06-18
\| \| \| \|	and then dropping it, we just ignore it
*	Drop the 0-carry bit before bounds analysis	Jason Gross	2017-06-17
\|
*	Fix scmul bounds issue	jadep	2017-06-17
\|
*	More eye-catching naming scheme for nm in saturated	Jason Gross	2017-06-17
\|
*	Make use of non-uniform tuple-based add	Jason Gross	2017-06-17
\| \| \| \|	Maybe it'll result in better output code with fewer zeros?
*	finish tuple-ifying Montgomery API	jadep	2017-06-16
\|
*	Switch to using tuples for word-by-word montgomery	Jason Gross	2017-06-16
\| \| \| \| \| \| \|	The new parameterized definitions and proofs are in WordByWord/Abstract/Dependent/; the old ones are untouched (and unused) in WordByWord/Abstract/. I replaced definitions I didn't know how to write in the Saturated API with the use of an axiom.
*	CPSify montgomery wbw reduction	Jason Gross	2017-06-15
\| \| \| \| \| \|	I didn't want to bother redoing all of the proofs that I'd already done, so instead I prove the cps'ified version equal to the non-cps version, and transfer over the proofs that way.
*	CPSify Saturated API in preparation for CPSifying Montgomery (see #194)	jadep	2017-06-15
\|
*	Fill in mul_split to wbw montgomery	Jason Gross	2017-06-13
\|
*	finish computational portions of operations needed for Montgomery, and ↵	jadep	2017-06-12
\| \| \| \|	sketch out some of the proofs as discussed in #157
*	add zero (as per #157)	jadep	2017-06-08
\|
*	start saturated-arithmetic API for use in Montgomery (see discussion in #157)	jadep	2017-06-08
\|
*	Don't rely on autogenerated names	Jason Gross	2017-06-05
\| \| \| \| \| \|	This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch).