fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	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.)
*	Don't needlessly extend the context in CSE	Jason Gross	2017-04-17
\|
*	Prove antisymmetry of CSE leb	Jason Gross	2017-04-17
\|
*	Ask for leb on op codes and base types, not flat types	Jason Gross	2017-04-14
\|
*	Add support for cse-modulo-normalization	Jason Gross	2017-04-14
\|
*	SOp needs to hold the type of the arguments, for denote	Jason Gross	2017-04-12
\|
*	Hold types in SFst and SSnd	Jason Gross	2017-04-12
\| \| \| \|	Needed for writing denote
*	Extend cse context when inlining	Jason Gross	2017-04-11
\|
*	Generalize prepend_prefix	Jason Gross	2017-04-10
\|
*	Reorder parameters for ease of partial instantiation, add symbolic_expr_dec	Jason Gross	2017-04-10
\|
*	Fix CSE to correctly symbolize expressions	Jason Gross	2017-04-10
\| \| \| \| \| \|	The ones using variables from different parts of the same let-binder were getting stored as a reference to the let-binder, and losing information about which component they were in.
*	Key on flat_type not base_type, in CSE	Jason Gross	2017-04-10
\| \| \| \| \| \|	Using [lookup] and [extend] was causing issues in proving wf, and they were unnecessary. It's fine to treat each flat_type as a unit, because we'll never be looking for a projection of an expression in the context.
*	Use Named.Context in CSE, so we can reuse context lemmas	Jason Gross	2017-04-10
\|
*	rename-everything	Andres Erbsen	2017-04-06