fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add find_Name_and_val_transfer_interp_flat_type_None	Jason Gross	2017-10-23
\|
*	Add find_Name_and_val_transfer_interp_flat_type	Jason Gross	2017-10-23
\|
*	Factor out some code in src/Compilers/Named/MapType.v	Jason Gross	2017-10-23
\|
*	Add MapType	Jason Gross	2017-10-21
\|
*	Generalize wf_compile a bit	Jason Gross	2017-10-20
\|
*	Fix some type annotations for better non-unfolding	Jason Gross	2017-10-17
\|
*	Stronger contexts	Jason Gross	2017-07-07
\|
*	Push bounds side conditions through the pipeline	Jason Gross	2017-06-12
\| \| \| \|	This will (hopefully) be useful for karatsuba.
*	Add CompileInterpSideConditions.v	Jason Gross	2017-06-12
\|
*	Add snd_interpf_side_conditions_gen_Some	Jason Gross	2017-06-12
\|
*	Add Named.InterpSideConditions	Jason Gross	2017-06-12
\|
*	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).
*	Add more context proper lemmas	Jason Gross	2017-05-16
\|
*	Flip argument order on interp for easier Proper lemmas	Jason Gross	2017-05-16
\|
*	Add context_equiv and prove some Proper lemmas	Jason Gross	2017-05-16
\|
*	Flip order of extendb, lookup arguments	Jason Gross	2017-05-16
\| \| \| \|	This allows better Proper lemmas
*	Remove useless argument	Jason Gross	2017-05-16
\|
*	Add Interp_compile	Jason Gross	2017-05-16
\|
*	Slightly better type for Interp_InterpToPHOAS	Jason Gross	2017-05-16
\|
*	Add Named.ExprInversion	Jason Gross	2017-05-15
\|
*	Add Wf_from_unit	Jason Gross	2017-05-15
\| \| \| \| \|	This one is much easier to compute with, and it means we can get rid of a lot of pesky Named.wff proofs.
*	Add src/Compilers/Z/Named/DeadCodeEliminationInterp.v	Jason Gross	2017-05-15
\|
*	Add DeadCodeEliminationInterp	Jason Gross	2017-05-15
\|
*	Add a stronger lemma to registerassigninterp	Jason Gross	2017-05-15
\|
*	Add GetNames	Jason Gross	2017-05-14
\|
*	Add Named.default_names_for	Jason Gross	2017-05-14
\|
*	Add Named.CountLets	Jason Gross	2017-05-14
\|
*	Split off EliminateDeadCode	Jason Gross	2017-05-14
\|
*	Fix some scoping	Jason Gross	2017-05-14
\|
*	Allow specifying type in nlet	Jason Gross	2017-05-14
\|
*	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
*	Prove interp correctness of register reassign	Jason Gross	2017-04-13
\|
*	Add Named.Syntax.Interp	Jason Gross	2017-04-13
\|
*	Add lookupb_remove	Jason Gross	2017-04-13
\|
*	Add lookupb_removeb_same	Jason Gross	2017-04-13
\|
*	Add lookupb_remove_not_in	Jason Gross	2017-04-13
\|
*	Add ContextOnOk	Jason Gross	2017-04-13
\|
*	Remove dead code in comments	Jason Gross	2017-04-13
\|
*	Reorder parameters for ease of partial instantiation, add symbolic_expr_dec	Jason Gross	2017-04-10
\|
*	Add lookupb_extendb_full	Jason Gross	2017-04-10
\|
*	Relax extendb, and prove a property about length	Jason Gross	2017-04-10
\|
*	Add AListContext, WeakListContext	Jason Gross	2017-04-10
\|
*	Split off Compilers.Named.Context	Jason Gross	2017-04-10
\|
*	rename-everything	Andres Erbsen	2017-04-06