fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Split up DoubleBoundedProofs, add proofs	Jason Gross	2016-10-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Some help from jadep on BitwiseOr. After \| File Name \| Before \|\| Change -------------------------------------------------------------------------------------- 0m39.26s \| Total \| 0m36.03s \|\| +0m03.23s -------------------------------------------------------------------------------------- N/A \| BoundedArithmetic/DoubleBoundedProofs \| 0m21.20s \|\| -0m21.19s 0m07.47s \| BoundedArithmetic/Double/Proofs/Multiply \| N/A \|\| +0m07.46s 0m06.70s \| BoundedArithmetic/Double/Proofs/SpreadLeftImmediate \| N/A \|\| +0m06.70s 0m05.14s \| BoundedArithmetic/Double/Proofs/RippleCarryAddSub \| N/A \|\| +0m05.13s 0m02.75s \| BoundedArithmetic/Double/Proofs/Decode \| N/A \|\| +0m02.75s 0m08.06s \| BoundedArithmetic/ArchitectureToZLikeProofs \| 0m08.05s \|\| +0m00.00s 0m02.01s \| Specific/FancyMachine256/Barrett \| 0m02.13s \|\| -0m00.12s 0m02.00s \| Specific/FancyMachine256/Montgomery \| 0m02.06s \|\| -0m00.06s 0m01.75s \| Specific/FancyMachine256/Core \| 0m01.66s \|\| +0m00.09s 0m00.90s \| BoundedArithmetic/Double/Proofs/LoadImmediate \| N/A \|\| +0m00.90s 0m00.88s \| BoundedArithmetic/Double/Proofs/BitwiseOr \| N/A \|\| +0m00.88s 0m00.58s \| BoundedArithmetic/Double/Proofs/SelectConditional \| N/A \|\| +0m00.57s 0m00.53s \| BoundedArithmetic/ArchitectureToZLike \| 0m00.47s \|\| +0m00.06s 0m00.49s \| BoundedArithmetic/Double/Core \| N/A \|\| +0m00.49s N/A \| BoundedArithmetic/DoubleBounded \| 0m00.46s \|\| -0m00.46s
*	Add bitwise and, remove mkl from fancy	Jason Gross	2016-10-03
\|
*	Work around bug #5112 ([Arguments id /] broken)	Jason Gross	2016-10-03
\|
*	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.
*	Use dlet, not llet	Jason Gross	2016-09-22
\|
*	Don't inline everything in Montgomery and Barrett	Jason Gross	2016-09-22
\| \| \| \| \| \|	We still use CSE in fancy machine, because we want to lift the ldi's above the rest of the code. However, on a quick inspection, the algorithm no longer needs CSE to be duplicate-free.
*	Make use of named syntax, do reg assign for fancy	Jason Gross	2016-09-22
\|
*	Add reserved notation for Let, change #	Jason Gross	2016-09-17
\| \| \| \| \|	We reserve [a # b] in Notations.v, and make it's level compatible with the notation declared in the std lib for Q.
*	Split off lemmas about [InlineConst]	Jason Gross	2016-09-16
\|
*	Move FancyMachine from Experiments to Specific	Jason Gross	2016-09-08
	Quoting Andres: > I am leaning towards putting this in Specifc instead of Experiments -- it > seems like complete result on its own, these files are unlikely to be reused > for something else, and I don't think we are expecting to need to remove it > any time soon. Currently, `Specific` code does not quantify over anything (no > context variables), but this seems secondary. We could make versions of this > with the curve constants plugged in, though.