fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Drop CSE from Fancy Machine	Jason Gross	2016-09-22
\| \| \| \| \|	By being careful about building the expressions in the first place, we no longer need it, and can rely on dead code elimination.
*	Better spec in Montgomery.ZBounded	Jason Gross	2016-09-07
\|
*	Add correctness theorems to Montgomery.ZBounded	Jason Gross	2016-08-31
\|
*	Add reduce via partial to Montgomery ZBounded	Jason Gross	2016-08-29
\|
*	Specify a type of bounded integers for mod arith	Jason Gross	2016-08-09
\| \| \| \|	Also use it to implement Montgomery reduction and Barrett reduction.
*	Work around broken lia in 8.4	Jason Gross	2016-08-09
\|
*	Add alternate form of Montgomery, which does better about bounds	Jason Gross	2016-08-09
\| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ----------------------------------------------------------------------- 0m06.96s \| Total \| 0m04.29s \|\| +0m02.67s ----------------------------------------------------------------------- 0m06.56s \| ModularArithmetic/Montgomery/ZProofs \| 0m03.82s \|\| +0m02.73s 0m00.40s \| ModularArithmetic/Montgomery/Z \| 0m00.47s \|\| -0m00.06s
*	Montgomery: Add a variant that does reduction through partial_reduce	Jason Gross	2016-08-08
\|
*	Fix a comment	Jason Gross	2016-08-05
\|
*	Define Montgomery reduction / multiplication on Z (#42)	Jason Gross	2016-08-05
	This is partly done for my own benefit, to internalize how Montgomery multiplication works, and partly done as a template for word-based Montgomery multiplication when the carrying does not take advantage of the fact that we are using a pseudomersenne prime.