fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Don't use UIP in inversion_wff	Jason Gross	2016-12-03
\|
*	Add inversion_wff	Jason Gross	2016-12-03
\|
*	Add WfInversion	Jason Gross	2016-12-03
\|
*	More powerful inversion_option	Jason Gross	2016-12-03
\|
*	Move things to ExprInversion	Jason Gross	2016-12-03
\|
*	Add invert_Var	Jason Gross	2016-12-03
\|
*	Arguments for invert_Op	Jason Gross	2016-12-03
\|
*	Fewer autogenerated names	Jason Gross	2016-12-03
\|
*	Add invert_Op	Jason Gross	2016-12-03
\|
*	Change some default names	Jason Gross	2016-12-03
\|
*	Initial (not fully working) version of MapWithInterpInfo	Jason Gross	2016-12-02
\|
*	Add SmartFlatTypeMapUnInterp	Jason Gross	2016-12-02
\|
*	Add invert_LetIn	Jason Gross	2016-12-02
\|
*	Arguments for invert_Pair	Jason Gross	2016-12-02
\|
*	Add invert_Pair	Jason Gross	2016-12-02
\|
*	Add SmartFlatTypeMapInterp	Jason Gross	2016-12-02
\|
*	SmartFlatTypeMap arguments	Jason Gross	2016-12-02
\|
*	Add SmartFlatTypeMap	Jason Gross	2016-12-02
\|
*	Various application lemmas	Jason Gross	2016-11-23
\|
*	Add lemmas about application	Jason Gross	2016-11-22
\|
*	Add interp_all_binders_for'	Jason Gross	2016-11-22
\|
*	Remove an admit	Jason Gross	2016-11-17
\|
*	Add interpf_LetIn	Jason Gross	2016-11-17
\|
*	: assert is not valid 8.4 syntax	Jason Gross	2016-11-17
\|
*	Add Un{Return,Abs}_eta	Jason Gross	2016-11-16
\|
*	Add : assert to a bunch of arguments	Jason Gross	2016-11-16
\| \| \| \|	See https://coq.inria.fr/bugs/show_bug.cgi?id=5181#c3
*	Split fixedpoint in interpf	Jason Gross	2016-11-16
\|
*	Arguments for Un{Return,Abs}	Jason Gross	2016-11-16
\|
*	Add UnReturn, UnAbs	Jason Gross	2016-11-16
\|
*	Support for 128-bit words	Jason Gross	2016-11-14
\| \| \| \| \|	I haven't found a good way to genericize the proofs of relatedness things, mostly because Modules and functors are annoying.
*	Add word-size-independent interpretations	Jason Gross	2016-11-14
\|
*	Fix reification of neg	Jason Gross	2016-11-11
\| \| \| \|	Note that we don't actually use reified neg anywhwere. If we did, the previous commit wouldn't've built...
*	Make [neg] a unary operation in reflection	Jason Gross	2016-11-11
\| \| \| \| \| \|	It now takes a meta-level [Z] argument which is the bit width. I haven't modified any of the extraction directives, so I don't know if extraction still works nicely.
*	Remove more conditional subtract	Jason Gross	2016-11-11
\|
*	Remove extra conditional subtract things	Jason Gross	2016-11-11
\|
*	Remove special code for reified conditional sub	Jason Gross	2016-11-11
\|
*	More proof fixes	Jason Gross	2016-11-10
\|
*	Minimize diff with master, fix some proofs that were broken	Jason Gross	2016-11-10
\|
*	Merge with master	Rob Sloan	2016-11-09
\|\
\| *	Fix for 8.4	Jason Gross	2016-11-09
\| \|
\| *	Switch to accurate bounds for lor	Jason Gross	2016-11-09
\| \| \| \| \| \| \| \| \| \| \| \|	When the arguments are, e.g., 2^k - 2 and 2^(k-1)-1, the upper bound is 2^k - 1, not 2^(k-1)-1. Thanks, Rob
* \|	Rebase + remove WordizeUtil dependency from Z/Interpretations	Rob Sloan	2016-11-09
\|\ \
\| \| *	Remove last admitted lemma in src/Reflection/Z/Interpretations/Relations.v	Jason Gross	2016-11-09
\| \|/
* \|	Finished WordUtil, word operations in Z/Interpretation	Rob Sloan	2016-11-09
\| \|
* \|	Not quite done with WordUtil lemmas.	Robert Sloan	2016-11-08
\|\ \
\| \| *	Fix for Coq 8.4	Jason Gross	2016-11-08
\| \| \|
\| \| *	Some fixes for 8.4 differences	Jason Gross	2016-11-08
\| \| \|
\| \| *	More progress on src/Reflection/Z/Interpretations/Relations.v	Jason Gross	2016-11-08
\| \| \|
\| \| *	Fix 8.4 build ([value] is a constant)	Jason Gross	2016-11-08
\| \|/
\| *	Factor related_Z_op (except conditional_sub)	Jason Gross	2016-11-08
\| \|