fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Update display logs	Jason Gross	2017-10-31
\|
*	Update display logs	Jason Gross	2017-10-31
\|
*	Add more constant notations	Jason Gross	2017-10-31
\|
*	Update display logs	Jason Gross	2017-10-29
\|
*	Update display logs	Jason Gross	2017-10-29
\|
*	Update display logs	Jason Gross	2017-10-29
\|
*	Add more constant notations	Jason Gross	2017-10-29
\|
*	check in p384 generated code	Andres Erbsen	2017-10-26
\|
*	automate some proofs; also remove trace-based reasoning in favor of ↵	jadep	2017-10-26
\| \| \| \|	induction on fuel
*	invariants don't need to know the fuel	jadep	2017-10-26
\|
*	WIP: loops	jadep	2017-10-26
\|
*	Add inversion_wf_one_constr	Jason Gross	2017-10-24
\|
*	Add MapBaseTypeWf, generalize src/Compilers/MapBaseType.v a bit	Jason Gross	2017-10-24
\|
*	Generalize In_flatten_binding_list_untransfer_interp_flat_type	Jason Gross	2017-10-24
\|
*	Add In_flatten_binding_list_untransfer_interp_flat_type	Jason Gross	2017-10-24
\|
*	Add wff_SmartPairf_SmartValf	Jason Gross	2017-10-24
\|
*	Add MapBaseType	Jason Gross	2017-10-23
\|
*	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 {un,}transfer_interp_flat_type, lift_flat_type	Jason Gross	2017-10-23
\|
*	Add InlineConstAndOpByRewrite	Jason Gross	2017-10-23
\|
*	Add inline_const_and_op{f,} specializations	Jason Gross	2017-10-22
\|
*	Add another unfolding database	Jason Gross	2017-10-22
\|
*	Factor out fold_right_cps2_specialized_step, add mapi_with'_cps2	Jason Gross	2017-10-22
\|
*	Add ZExtended/InlineConstAndOp.v	Jason Gross	2017-10-22
\|
*	Add StripExpr	Jason Gross	2017-10-22
\|
*	Add tight and loose bounds, no carry in add, sub	Jason Gross	2017-10-22
\| \| \| \| \| \| \| \|	Following Andres' suggestions to allow making ladderstep from other synthesis things. It went though mostly without a hitch, though there were a number of boilerplate changes needed.
*	Unfold P.bound1 in fenz	Jason Gross	2017-10-21
\| \| \| \|	This will lead to prettier printout
*	Add MapType	Jason Gross	2017-10-21
\|
*	Add SmartValf_option	Jason Gross	2017-10-20
\|
*	Add ZExtended/Syntax.v	Jason Gross	2017-10-20
\|
*	Add GeneralizeVar{Wf,Interp}.v	Jason Gross	2017-10-20
\|
*	Generalize wf_compile a bit	Jason Gross	2017-10-20
\|
*	Add GeneralizeVar	Jason Gross	2017-10-20
\|
*	Add a version of exprf that lives in Set	Jason Gross	2017-10-20
\|
*	Add Z.InlineConstAndOp*	Jason Gross	2017-10-20
\|
*	Add InlineConstAndOpInterp.v	Jason Gross	2017-10-20
\|
*	Add interpf_invert_PairsConst	Jason Gross	2017-10-20
\|
*	Add InlineConstAndOpWf.v	Jason Gross	2017-10-20
\|
*	Add wff_SmartPairf_SmartVarfMap_same	Jason Gross	2017-10-20
\|
*	Add SmartVarVarf_Pair, SmartPairfSmartVarVarf_SmartVarf	Jason Gross	2017-10-20
\|
*	Add wff_invert_PairsConst	Jason Gross	2017-10-20
\|
*	Better typing on postprocess_for_const_and_op	Jason Gross	2017-10-20
\|
*	Add InlineConstAndOp	Jason Gross	2017-10-20
\|
*	Add curry{3,4}	Jason Gross	2017-10-20
\|
*	Fix arguments of previous commit	Jason Gross	2017-10-20
\|
*	Add invert_PairsConst	Jason Gross	2017-10-20
\|
*	Add invert_Pairs	Jason Gross	2017-10-20
\|
*	Allow partial-inlining in the inliner	Jason Gross	2017-10-20
\| \| \| \| \| \|	This will allow fusing arithmetic simplification with constant inlining, which is required for compilation to reified terms to work well, and will hopefully eventually allow cleaning up the pipeline.