fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Add support for more constants	Jason Gross	2017-05-14
\|
*	applied micro-optimizations from donna with [transitivity] and [ring] (as ↵	jadep	2017-05-14
\| \| \| \|	per #176)
*	Add constant, support pair-returning assignment	Jason Gross	2017-05-14
\|
*	More debug info in reification	Jason Gross	2017-05-14
\|
*	remove lingering [About]	jadephilipoom	2017-05-14
\|
*	remove redundant definition	jadep	2017-05-14
\|
*	make freeze use the correct versions of add_get_carry and zselect	jadep	2017-05-14
\|
*	add wrapper for add_get_carry and proofs for add_get_carry and zselect	jadep	2017-05-14
\|
*	Add lemma justifying compiler optimization for adc	Jason Gross	2017-05-14
\|
*	Fix notation binding levels so types work in nlet	Jason Gross	2017-05-14
\|
*	Add some reserved notations	Jason Gross	2017-05-14
\|
*	Ooops, I mixed up Bind Scope and Delimit Scope	Jason Gross	2017-05-14
\|
*	Fix some scoping	Jason Gross	2017-05-14
\|
*	Allow specifying type in nlet	Jason Gross	2017-05-14
\|
*	Comment out CSE in pipeline	Jason Gross	2017-05-14
\|
*	CSE without inlining arithmetic expressions	Jason Gross	2017-05-14
\| \| \| \| \| \| \| \| \| \|	This takes care of most of #158. The remaining bits are reworking the Wf and interpretation lemmas to actually work. (The former needs a only bit of rethinking and rephrasing to handle the fact that sometimes we change the stored symbolic expression from a complicated one to a fresh variable, while the latter needs major surgery, which Adam tells me is easy, and this is a note that when I come back to it, I should look at the email thread with Adam about CSE from last summer.)
*	Add Z.div_le_mono_nonneg	Jason Gross	2017-05-13
\|
*	Add mod_bound_min_max	Jason Gross	2017-05-13
\|
*	Add proper lemma for add_with_carry	Jason Gross	2017-05-13
\|
*	Change definition of add_get_carry	Jason Gross	2017-05-13
\| \| \| \| \|	The new definition is judgmentally equal to the old one, but is slightly easier to reify.
*	Add definitions for zselect and add_get_carry	Jason Gross	2017-05-13
\| \| \| \|	In ZUtil/Definitions.v
*	Add flatten_binding_list_SmartVarfMap2_pair_in_generalize2	Jason Gross	2017-05-13
\|
*	Support destructuring dlet and slet	Jason Gross	2017-05-13
\| \| \| \| \|	The current way to support it is a kludge around the fact that `x binder` only works for recursive notations
*	Add Zdiv_0_r to zsimplify	Jason Gross	2017-05-13
\|
*	Split off pull_Zmod, push_Zmod from ZUtil	Jason Gross	2017-05-13
\|
*	Split off more ZUtil things	Jason Gross	2017-05-13
\|
*	Split off more of ZUtil	Jason Gross	2017-05-13
\|
*	Split off more of ZUtil	Jason Gross	2017-05-13
\|
*	Split off ZUtil initial hint databases	Jason Gross	2017-05-13
\|
*	Remove an unneeded require import	Jason Gross	2017-05-13
\|
*	Split off Proper ZUtil lemmas	Jason Gross	2017-05-12
\|
*	Remove dead code in ZUtil (shiftl_by)	Jason Gross	2017-05-12
\|
*	Split off notation and defs in ZUtil	Jason Gross	2017-05-12
\|
*	Add reserved notations	Jason Gross	2017-05-11
\|
*	Remove dead Ltac code from ZUtil	Jason Gross	2017-05-11
\|
*	Suppress a warning about unused intropatterns	Jason Gross	2017-05-11
\|
*	s/appcontext/context/	Jason Gross	2017-05-11
\| \| \| \|	They mean the same thing since 8.5, and appcontext is deprecated.
*	Clean up implementation	Jason Gross	2017-05-01
\| \| \| \|	With help from Andres
*	Use columns rather than positional	Jason Gross	2017-05-01
\| \| \| \|	With help from Jade.
*	Use mod (weight (S i) / weight i), not mod (weight i)	Jason Gross	2017-05-01
\|
*	Initial stab at word-by-word montgomery	Jason Gross	2017-05-01
\| \| \| \| \| \| \| \| \| \| \| \|	I think I got the loop itself wrong, though: 1. I'm worried that it'll overflow off the end of the positional representation, since I'm not actually dividing by 2^s 2. I'm not carrying/reducing anywhere, so the getting the nth value might be wrong 3. I'm not sure if I got indexing right. But I want to submit this early version to get comments, before I put more effort into it.
*	plug in tuple-select rather than using context variables	jadep	2017-05-01
\|
*	add Tuple.map_cps to CPSUtil	jadep	2017-05-01
\|
*	move some lemmas to Core and define a tuple-select operation	jadep	2017-05-01
\|
*	move hints and context outside section (this is what happens when you ↵	jadep	2017-05-01
\| \| \| \|	'organize' code last-minute and don't check that it still works)
*	first synthesis of freeze code	jadep	2017-05-01
\|
*	Fix base-case for compact_digit (for a list [x;y], we want to do div/mod on ↵	jadep	2017-05-01
\| \| \| \|	x and y, not x and (y mod _).
*	stricter divmod proofs	jadep	2017-05-01
\|
*	proved freeze, removed initial carry step (the correctness proof of that ↵	jadep	2017-05-01
\| \| \| \|	step needs bounds-checker)
*	prove compact obeys div/mod rule	jadep	2017-05-01
\|