fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add ZRange.intersection	Jason Gross	2018-02-23
\|
*	Fix a typo	Jason Gross	2018-02-23
\|
*	Add some bounds operations to ZRange	Jason Gross	2018-02-23
\|
*	Add ZRange.opp	Jason Gross	2018-02-23
\|
*	Make the Montgomery reduction test case use 128-bit multiplications and	Jade Philipoom	2018-02-23
\| \| \| \| \| \| \| \|	Columns arithmetic. This includes: - writing flatten_column in terms of list_rect instead of matches, so it can be reified - adding list_rect, shiftl, and List.length to various IRs - dead code elimination
*	fix leftover %RT	Jade Philipoom	2018-02-23
\|
*	Get bounds analysis working	Jade Philipoom	2018-02-23
\|
*	fixed inlining of opaque pairs as per Jason's recommendation	Jade Philipoom	2018-02-23
\|
*	rename compact_digit to flatten_column	Jade Philipoom	2018-02-23
\|
*	make compact_digit consume a bound argument rather than a weight-function index	Jade Philipoom	2018-02-23
\|
*	use Z.div and Z.modulo in saturated arith, since we can now change to ↵	Jade Philipoom	2018-02-23
\| \| \| \|	bitshifts reflectively
*	remove leftover [Eval compute] and extra space	Jade Philipoom	2018-02-23
\|
*	Fix naming issue	Jade Philipoom	2018-02-23
\|
*	move things from ZUtil.v into Div.v	Jade Philipoom	2018-02-23
\|
*	define mul and add placeholders for new operations in bounds parts	Jade Philipoom	2018-02-23
\|
*	Add non-CPS version of Saturated/Core	Jade Philipoom	2018-02-23
\|
*	add three proofs to ZUtil	Jade Philipoom	2018-02-23
\|
*	add two proofs about lists	Jade Philipoom	2018-02-23
\|
*	Add non-CPS version of associational multiplication with mul_split	Jade Philipoom	2018-02-23
\|
*	preliminary version of Montgomery reduce in new pipeline; includes adding ↵	Jade Philipoom	2018-02-23
\| \| \| \|	support for Z.leb and several saturated-arith operations (add_get_carry, add_with_get_carry, sub_get_borrow, mul_split, zselect, and add_modulo)
*	add proof about Z.equiv_modulo	Jade Philipoom	2018-02-23
\|
*	add equivalence proof for Montgomery reduce_via_partial_alt	Jade Philipoom	2018-02-23
\|
*	create rewrite database for saturated operations on Z	Jade Philipoom	2018-02-23
\|
*	Add new modular addition operation on Z	Jade Philipoom	2018-02-23
\|
*	Fix balance on sub	Jason Gross	2018-02-19
\| \| \| \| \| \| \|	With some help from @jadephilipoom Previously, the carrying was removing the effect of `coef`, and we were getting too small a balance.
*	A bit more uniformity in handling the prime, implicits	Jason Gross	2018-02-19
\|
*	[experiments] Fill in opp and sub	Jason Gross	2018-02-19
\|
*	Remove the mod on eval_add	Jason Gross	2018-02-19
\|
*	Remove runtime_scope	Jason Gross	2018-02-19
\| \| \| \|	As per https://github.com/mit-plv/fiat-crypto/pull/315#discussion_r169085799
*	[experiments] Add some more arithmetic operations	Jason Gross	2018-02-19
\|
*	NumTheoryUtil: make coqprime dependencies explicit	Andres Erbsen	2018-02-19
\|
*	Take in n, compute limbwidth	Jason Gross	2018-02-18
\|
*	Rename type_descr to second_order, as per PR request	Jason Gross	2018-02-18
\|
*	Rename AutoReify	Jason Gross	2018-02-18
\|
*	Speed up the pipeline by 3x, restoring previous performance	Jason Gross	2018-02-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Apparently using `refine eq_refl` rather than `subst <name for evar>; reflexivity` was resulting in βδ reduction of `chained_carries` in `carry_mulmod`. The β reduction resulted in us getting a different cps'd term. I do not know why this particular β reduction resulted in a 3x slowdown in partial reduction; it seems like anything that cared about sharing should either get sharing from the top-level in `carry_mulmod`, or should have no difference in sharing between the terms ```coq (fun n s c p idxs => fold_right (fun a b => @carry_reduce n s c a b) p (rev idxs)) n s c p idxs ``` and ```coq fold_right (fun a b => @carry_reduce n s c a b) p (rev idxs)) ``` This feels fragile, and I am mystified. Note for the future: I went about debugging this by integrating little bits of this PR one by one, seeing which one caused the slowdown, and then, when I realized it was use of `carry_mulmod`, I took the reified terms and made a goal asserting their equality, and then took the terms apart with `f_equal` and `extensionality` until I found the difference.
*	Remove mul_rargs record	Jason Gross	2018-02-18
\|
*	Make use of expand_lists tactic	Jason Gross	2018-02-18
\|
*	Rename carry_mulmod_correct to eval_carry_mulmod to fit with other lemmas	Jason Gross	2018-02-18
\|
*	Add GallinaReify.AutoReify	Jason Gross	2018-02-18
\|
*	Simplify the pipeline a bit	Jason Gross	2018-02-18
\|
*	Remove try_transport_untranslate	Jason Gross	2018-02-18
\|
*	Respond to some code review comments	Jason Gross	2018-02-18
\|
*	Do a large chunk of the bounds pipeline	Jason Gross	2018-02-18
\|
*	WIP on more general continuations	Jason Gross	2018-02-18
\|
*	Add notations for type reification	Jason Gross	2018-02-18
\|
*	Add some imports to experiments	Jason Gross	2018-02-18
\|
*	Strip the pointed instance names off of the default value in list expansion	Jason Gross	2018-02-18
\| \| \| \|	This is required for reification to work, it seems
*	Add expand_lists tactic	Jason Gross	2018-02-18
\|
*	Add pointed types	Jason Gross	2018-02-18
\| \| \| \|	For filling in default values
*	Fix a proof for Coq 8.7	Jason Gross	2018-02-17
\|