fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Try out stronger land, lor bounds	Jason Gross	2018-06-27
\|
*	Add is_tighter_than_bool lemmas	Jason Gross	2018-06-27
\|
*	Add lnot mod pull/push lemmas	Jason Gross	2018-06-27
\|
*	Add missing Z.lnot_0 hints	Jason Gross	2018-06-27
\|
*	Add more Z const hints	Jason Gross	2018-06-27
\|
*	Remove lneg in favor of lnot_modulo (lneg was wrong)	Jason Gross	2018-06-27
\|
*	Add some Z.land, Z.lor hints	Jason Gross	2018-06-27
\|
*	Add a couple of zrange lemmas	Jason Gross	2018-06-26
\|
*	Add specialize_all_ways, fix a proof in ↵	Jason Gross	2018-06-26
\| \| \| \|	src/Compilers/Z/ArithmeticSimplifierInterp.v
*	Add Z.bneg, Z.lneg	Jason Gross	2018-06-26
\|
*	Slightly better definitions of some ZUtil functions	Jason Gross	2018-06-26
\| \| \| \| \|	This way we can just directly reify most of the primitives we care about.
*	Add list_beq	Jason Gross	2018-06-22
\|
*	Add Option.List.bind_list	Jason Gross	2018-06-21
\|
*	Add [freeze] to Arithmetic	Jason Gross	2018-06-21
\|
*	Add extend_to_length for non-uniform-length add, sub	Jason Gross	2018-06-19
\|
*	Add seq_add, seq_len_0	Jason Gross	2018-06-19
\|
*	Add a comment about sub	Jason Gross	2018-06-18
\|
*	More compact printing of ASTs in errors	Jason Gross	2018-06-18
\|
*	Add another prime example	Jason Gross	2018-06-18
\|
*	Fix a typo in to-C shifts	Jason Gross	2018-06-18
\|
*	Don't duplicate error message printing in OCaml	Jason Gross	2018-06-18
\|
*	Pass around lists of strings for error messages	Jason Gross	2018-06-17
\| \| \| \| \| \| \| \| \| \|	This allows us to get back an error message in Saturated Solinas in OCaml on P256 x32 in reasonable time without blowing the stack. There's the slight oddity that the list of string in the success case is joined by the empty string, but the list of string in the error case is joined by newline. Probably meanas that I chose the wrong abstraction barrier somewhere.
*	Add ShowLines	Jason Gross	2018-06-17
\|
*	New pipeline, split among files	Jason Gross	2018-06-17
\|
*	Reserve a notatoin for ;;	Jason Gross	2018-06-16
\|
*	Add zrange equality	Jason Gross	2018-06-15
\|
*	Add ErrorT monad, and Show class	Jason Gross	2018-06-15
\|
*	Add decimal_string_of_Z	Jason Gross	2018-06-15
\|
*	Add some lemmas and defs to ListUtil.FoldBool	Jason Gross	2018-06-14
\|
*	Set universe polymorphism in CPSNotations	Jason Gross	2018-06-14
\| \| \| \| \| \|	This bypasses universe inconsistencies that arise when trying to return continuations from other continuations, which is a scenario that comes up frequently with cpsbind.
*	Add notations for cpsbind, cps_option_bind	Jason Gross	2018-06-14
\|
*	Actually use primitive projections in PrimitiveHList	Jason Gross	2018-06-13
\|
*	Minor refactoring	Jason Gross	2018-06-13
\| \| \| \|	Note that List.repeat (ListUtil.List.repeat) rather than repeat (Coq.Lists.List.repeat) was interfering with extraction
*	Add PrimitiveHList, PrimitiveProd	Jason Gross	2018-06-13
\|
*	Move Option.List.map to OptionList.map to fix name clashes in Tuple	Jason Gross	2018-06-04
\|
*	Add Option.List.map	Jason Gross	2018-06-04
\|
*	Move cps notations into a scope	Jason Gross	2018-06-01
\|
*	Add more bind reserved notations	Jason Gross	2018-05-31
\|
*	fix over-indented line	Jade Philipoom	2018-05-31
\|
*	prove prefancy->fancy for barrett special case	Jade Philipoom	2018-05-31
\|
*	move around some Lets so that 8.8 doesn't error	Jade Philipoom	2018-05-31
\|
*	relocate ok_expr tactics and fix an admit with a silly bounds relaxation hack	Jade Philipoom	2018-05-31
\|
*	Proved pre-fancy barrett reduction correct (except 1 admit for bounds	Jade Philipoom	2018-05-31
\| \| \| \| \|	that are correct but for which bounds relaxation loses necessary information) and add explanatory comments.
*	temporary workaround for #352	Jade Philipoom	2018-05-31
\|
*	Define machine model, write prefancy->fancy pass, and prove Montgomery code ↵	Jade Philipoom	2018-05-31
\| \| \| \|	correct
*	[WIP] shifting adds	Jade Philipoom	2018-05-31
\|
*	change order of additions so that they a) make more sense and b) are more ↵	Jade Philipoom	2018-05-31
\| \| \| \|	suited to shifting adds
*	tweak binders so that shifts from base conversion get inlined	Jade Philipoom	2018-05-31
\|
*	remove unneeded comment and extra whitespace	Jade Philipoom	2018-05-31
\|
*	end-to-end proof for montgomery	Jade Philipoom	2018-05-31
\|