fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Add ZUtil, list lemmas	Jason Gross	2018-07-02
\|
*	Fix a notation issue in previous commit	Jason Gross	2018-07-02
\|
*	Add more ListUtil proofs	Jason Gross	2018-07-02
\|
*	Add some list lemmas	Jason Gross	2018-07-02
\|
*	Make all parameters implicit	Jasper Hugunin	2018-07-02
\|
*	Prefer relations of the form [eq ==> eq ==> ... ==> eq] in setoids	Jason Gross	2018-07-01
\| \| \| \|	Also make it easy to redeclare such instances.
*	Add useful list lemmas	Jason Gross	2018-06-29
\|
*	Add ZUtil.Sorting	Jason Gross	2018-06-29
\|
*	Revert "Add more schemes for prod"	Jason Gross	2018-06-28
\| \| \| \| \| \|	This reverts commit 5d38a03f5a9f69a78a582cc9cc1c350dc6596cd3. Some of these already exist in Datatypes
*	Add more schemes for prod	Jason Gross	2018-06-28
\|
*	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 seq_add, seq_len_0	Jason Gross	2018-06-19
\|
*	Add ShowLines	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
\|
*	Move function argument out of fixpoint of List.map2	Jason Gross	2018-05-21
\| \| \| \| \|	This allows us to make use of nested fixpoints involving map2, because the function argument can be inlined for guard checking now.
*	Backtrack on moving a notation to Notations.v, to fix conflict	Jason Gross	2018-05-06
\|
*	Fix notations to not conflict with bbv	Jason Gross	2018-05-06
\|
*	More reserved notations	Jason Gross	2018-05-06
\|
*	Add another notation	Jason Gross	2018-05-06
\|
*	Fix a typo in last commit	Jason Gross	2018-05-06
\|
*	Add a reserved notation for #v	Jason Gross	2018-05-06
\|
*	Fix bounds analysis for saturated ops and remove unneeded comment	Jade Philipoom	2018-04-30
\|
*	Util.Loops: remove non-stdlib dependencies	Andres Erbsen	2018-04-26
\|
*	add instructions cc_m, rshi, and sub_with_get_borrow to pipeline in ↵	Jade Philipoom	2018-04-19
\| \| \| \|	preparation for reifying barrett; tweaked definition of cc_l
*	Fix a proof	Jason Gross	2018-04-18
\|