fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	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
\|
*	Change a proof in src/Util/Option	Jason Gross	2018-04-18
\| \| \| \| \| \|	This was causing issues with bug minimization because some hints seem to follow [Require], not [Import], and so when [eauto] got stronger, this proof was failing.
*	Merge pull request #335 from mit-plv/cpsloops	Andres Erbsen	2018-04-18
\|\ \| \| \| \|	comprehensive loops framework with complete proof theory
* \|	add a list lemma	Jade Philipoom	2018-04-11
\| \|
* \|	add some lemmas aboud div and mod	Jade Philipoom	2018-04-11
\| \|
* \|	Add new assembly-mimicking operations rshi, cc_m, and cc_l	Jade Philipoom	2018-04-11
\| \|
* \|	prove stronger bound on quotient error for barrett reduction	Jade Philipoom	2018-04-11
\| \|
* \|	Update number/string conversions	Jason Gross	2018-04-09
\| \| \| \| \| \| \| \|	To updated version of https://github.com/coq/coq/pull/6597
* \|	pass-through after Andres's review in #334	Jade Philipoom	2018-04-03
\| \|
* \|	move some lemmas to ZUtil/ListUtil	Jade Philipoom	2018-04-03
\| \|
* \|	move some lemmas/hints to ListUtil	Jade Philipoom	2018-04-03
\| \|
* \|	Add Zdiv_0_l to zsimplify dbs	Jason Gross	2018-03-27
\| \|
\| *	move Loops from Experiments to Util	Andres Erbsen	2018-03-27
\| \|
\| *	remove old loops code	Andres Erbsen	2018-03-27
\| \|
* \|	Add list_case, a definition for match on list	Jason Gross	2018-03-27
\|/
*	Add another reserved notation for App_fst	Jason Gross	2018-03-21
\|
*	Don't use deprecated compat notations in ZUtil	Jason Gross	2018-03-07
\|
*	git submodule update --remote --recursive	Andres Erbsen	2018-02-24
\|