fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Bundle arguments to Barrett Reduction	Jason Gross	2016-10-10
\|
*	Work around bug #4165 (broken context) in 8.4	Jason Gross	2016-08-10
\| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=4165, context replacement is broken (in the presence of [let]).
*	Specify a type of bounded integers for mod arith	Jason Gross	2016-08-09
\| \| \| \|	Also use it to implement Montgomery reduction and Barrett reduction.
*	Implement Barrett Reduction following HAC 14.42 (#45)	Jason Gross	2016-08-04
\| \| \| \| \| \|	From http://cacr.uwaterloo.ca/hac/about/chap14.pdf This should take care of most of #43, at least the specification on Z part of it.
*	Add a generalized version of Barrett Reduction (#44)	Jason Gross	2016-08-04
\| \| \| \| \| \| \| \| \|	In this version, we split up the integer division so that we are less likely to overflow in intermediate computations. This is still not the version in HAC 14.42; that version also does early reduction modulo b^(k+1). This is work towards #43
*	Split up proof in BarrettReduction.Z	Jason Gross	2016-07-21
\| \| \| \| \| \|	In particular, we do equality reasoning in one place and inequality reasoning in another. This makes it very clear how the inequality reasoning follows from the equality reasoning.
*	Implement and prove Barrett reduction on Z (#18)	Jason Gross	2016-07-03
	Implement and prove Barrett reduction on Z This will serve as the high-level algorithm for modular reduction. We follow Wikipedia very closely, except where we can do better (I believe @jadephilipoom is updating Wikipedia).